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