Theory Quorums

(*<*)
theory Quorums
imports Consensus_Types
begin
(*>*)

subsection ‹Quorums›
(******************************************************************************)


locale quorum = 
  fixes Quorum :: "'a set set"
  assumes 
    qintersect: "⟦ Q ∈ Quorum; Q' ∈ Quorum ⟧ ⟹ Q ∩ Q' ≠ {}"
    ― ‹Non-emptiness needed for some invariants of Coordinated Voting›
    and Quorum_not_empty: "∃Q. Q ∈ Quorum"

lemma (in quorum) quorum_non_empty: "Q ∈ Quorum ⟹ Q ≠ {}"
by (auto dest: qintersect)

lemma (in quorum) empty_not_quorum: "{} ∈ Quorum ⟹ False"
  using quorum_non_empty
  by blast

locale quorum_process = quorum Quorum
  for Quorum :: "process set set"

locale mono_quorum = quorum_process +
  assumes mono_quorum: "⟦ Q ∈ Quorum; Q ⊆ Q' ⟧ ⟹ Q' ∈ Quorum"

lemma (in mono_quorum) UNIV_quorum:
  "UNIV ∈ Quorum"
  using Quorum_not_empty mono_quorum
  by(blast)

definition majs :: "(process set) set" where
  "majs ≡ {S. card S > N div 2}"

lemma majsI:
  "N div 2 < card S ⟹ S ∈ majs"
  by(simp add: majs_def)

lemma card_Compl:
  fixes S :: "('a :: finite) set"
  shows "card (-S) = card (UNIV :: 'a set) - card S"
proof-
  have "card S + card (-S) = card (UNIV :: 'a set)"
    by(rule card_Un_disjoint[of S "-S", simplified Compl_partition, symmetric])
      (auto)
  thus ?thesis
    by simp
qed

lemma majorities_intersect:
  "card (Q :: process set) + card Q' > N ⟹ Q ∩ Q' ≠ {}"
  by (metis card_Un_disjoint card_mono finite not_le top_greatest)

interpretation majorities: mono_quorum majs
proof
  fix Q Q' assume "Q ∈ majs" "Q' ∈ majs"
  thus "Q ∩ Q' ≠ {}"
    by (intro majorities_intersect) (auto simp add: majs_def)
next
  show "∃Q. Q ∈ majs" 
    apply(rule_tac x=UNIV in exI)
    apply(auto simp add: majs_def intro!: div_less_dividend finite_UNIV_card_ge_0)
    done
next
  fix Q Q'
  assume "Q ∈ majs" "Q ⊆ Q'"
  thus "Q' ∈ majs" using card_mono[OF _ ‹Q ⊆ Q'›]
    by(auto simp add: majs_def)
qed

end