# 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"

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'›]