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' ≠ {}"
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