Theory Heard_Of.Majorities

theory Majorities
imports Main
begin

section ‹Utility Lemmas About Majorities›

text ‹
  Consensus algorithms usually ensure that a majority of processes
  proposes the same value before taking a decision,
  and we provide a few utility lemmas for reasoning about majorities.
›

text ‹
  Any two subsets ‹S› and ‹T› of a finite  set ‹E› such that
  the sum of their cardinalities is larger than the size of ‹E› have a
  non-empty intersection.
›
lemma abs_majorities_intersect:
    assumes crd: "card E < card S + card T"
        and s: "S ⊆ E" and t: "T ⊆ E" and e: "finite E"
    shows "S ∩ T ≠ {}"
proof (clarify)
  assume contra: "S ∩ T = {}"
  from s t e have "finite S" and "finite T" by (auto simp: finite_subset)
  with crd contra have "card E < card (S ∪ T)" by (auto simp add: card_Un_Int)
  moreover
  from s t e have "card (S ∪ T) ≤ card E" by (simp add: card_mono)
  ultimately
  show "False" by simp
qed

lemma abs_majoritiesE:
  assumes crd: "card E < card S + card T"
      and s: "S ⊆ E" and t: "T ⊆ E" and e: "finite E"
  obtains p where "p ∈ S" and "p ∈ T"
proof -
  from assms have "S ∩ T ≠ {}" by (rule abs_majorities_intersect)
  then obtain p where "p ∈ S ∩ T" by blast
  with that show ?thesis by auto
qed

text ‹Special case: both sets ‹S› and ‹T› are majorities.›

lemma abs_majoritiesE':
  assumes Smaj: "card S > (card E) div 2" and Tmaj: "card T > (card E) div 2"
      and s: "S ⊆ E" and t: "T ⊆ E" and e: "finite E"
  obtains p where "p ∈ S" and "p ∈ T"
proof (rule abs_majoritiesE[OF _ s t e])
  from Smaj Tmaj show "card E < card S + card T" by auto
qed

text ‹
  We restate the above theorems for the case where the base type
  is finite (taking ‹E› as the universal set).
›

lemma majorities_intersect:
  assumes crd: "card (UNIV::('a::finite) set) < card (S::'a set) + card T"
  shows "S ∩ T ≠ {}"
  by (rule abs_majorities_intersect[OF crd]) auto

lemma majoritiesE:
  assumes crd: "card (UNIV::('a::finite) set) < card (S::'a set) + card (T::'a set)"
  obtains p where "p ∈ S" and "p ∈ T"
using crd majorities_intersect by blast

lemma majoritiesE':
  assumes S: "card (S::('a::finite) set) > (card (UNIV::'a set)) div 2"
  and T: "card (T::'a set) > (card (UNIV::'a set)) div 2"
  obtains p where "p ∈ S" and "p ∈ T"
by (rule abs_majoritiesE'[OF S T]) auto

end (* theory Majorities *)