section ‹Bertrand's Ballot Theorem›
theory Ballot
imports
Complex_Main
"HOL-Library.FuncSet"
begin
subsection ‹Preliminaries›
lemma card_bij':
assumes "f ∈ A → B" "⋀x. x ∈ A ⟹ g (f x) = x"
and "g ∈ B → A" "⋀x. x ∈ B ⟹ f (g x) = x"
shows "card A = card B"
apply (rule bij_betw_same_card)
apply (rule bij_betwI)
apply fact+
done
subsection ‹Formalization of Problem Statement›
subsubsection ‹Basic Definitions›
datatype vote = A | B
definition
"all_countings a b = card {f ∈ {1 .. a + b} →⇩E {A, B}.
card {x ∈ {1 .. a + b}. f x = A} = a ∧ card {x ∈ {1 .. a + b}. f x = B} = b}"
definition
"valid_countings a b =
card {f∈{1..a+b} →⇩E {A, B}.
card {x∈{1..a+b}. f x = A} = a ∧ card {x∈{1..a+b}. f x = B} = b ∧
(∀m∈{1..a+b}. card {x∈{1..m}. f x = A} > card {x∈{1..m}. f x = B})}"
subsubsection ‹Equivalence with Set Cardinality›
lemma Collect_on_transfer:
assumes "rel_set R X Y"
shows "rel_fun (rel_fun R op =) (rel_set R) (λP. {x∈X. P x}) (λP. {y∈Y. P y})"
using assms unfolding rel_fun_def rel_set_def by fast
lemma rel_fun_trans:
"rel_fun P Q g g' ⟹ rel_fun R P f f' ⟹ rel_fun R Q (λx. g (f x)) (λy. g' (f' y))"
by (auto simp: rel_fun_def)
lemma rel_fun_trans2:
"rel_fun P1 (rel_fun P2 Q) g g' ⟹ rel_fun R P1 f1 f1' ⟹ rel_fun R P2 f2 f2' ⟹
rel_fun R Q (λx. g (f1 x) (f2 x)) (λy. g' (f1' y) (f2' y))"
by (auto simp: rel_fun_def)
lemma rel_fun_trans2':
"rel_fun R (op =) f1 f1' ⟹ rel_fun R (op =) f2 f2' ⟹
rel_fun R (op =) (λx. g (f1 x) (f2 x)) (λy. g (f1' y) (f2' y))"
by (auto simp: rel_fun_def)
lemma rel_fun_const: "rel_fun R (op =) (λx. a) (λy. a)"
by auto
lemma rel_fun_conj:
"rel_fun R (op =) f f' ⟹ rel_fun R (op =) g g' ⟹ rel_fun R (op =) (λx. f x ∧ g x) (λy. f' y ∧ g' y)"
by (auto simp: rel_fun_def)
lemma rel_fun_ball:
"(⋀i. i ∈ I ⟹ rel_fun R (op =) (f i) (f' i)) ⟹ rel_fun R (op =) (λx. ∀i∈I. f i x) (λy. ∀i∈I. f' i y)"
by (auto simp: rel_fun_def rel_set_def)
lemma
shows all_countings_set: "all_countings a b = card {V∈Pow {0..<a+b}. card V = a}"
(is "_ = card ?A")
and valid_countings_set: "valid_countings a b =
card {V∈Pow {0..<a+b}. card V = a ∧ (∀m∈{1..a+b}. card ({0..<m} ∩ V) > m - card ({0..<m} ∩ V))}"
(is "_ = card ?V")
proof -
define P where "P j i ⟷ i < a + b ∧ j = Suc i" for j i
have unique_P: "bi_unique P" and total_P: "⋀m. m ≤ a + b ⟹ rel_set P {1..m} {0..<m}"
by (auto simp add: bi_unique_def rel_set_def P_def Suc_le_eq gr0_conv_Suc)
have rel_fun_P: "⋀R f g. (⋀i. i < a+b ⟹ R (f (Suc i)) (g i)) ⟹ rel_fun P R f g"
by (simp add: rel_fun_def P_def)
define R where "R f V ⟷
V ⊆ {0..<a+b} ∧ f ∈ extensional {1..a+b} ∧ (∀i<a+b. i ∈ V ⟷ f (Suc i) = A)" for f V
{ fix f g :: "nat ⇒ vote" assume "f ∈ extensional {1..a + b}" "g ∈ extensional {1..a + b}"
moreover assume "∀i<a + b. (f (Suc i) = A) = (g (Suc i) = A)"
then have "∀i<a + b. f (Suc i) = g (Suc i)"
by (metis vote.nchotomy)
ultimately have "f i = g i" for i
by (cases "i ∈ {1..a+b}") (auto simp: extensional_def Suc_le_eq gr0_conv_Suc) }
then have unique_R: "bi_unique R"
by (auto simp: bi_unique_def R_def)
have "f ∈ extensional {1..a + b} ⟹ ∃V∈Pow {0..<a + b}. R f V" for f
by (intro bexI[of _ "{i. i < a+b ∧ f (Suc i) = A}"]) (auto simp add: R_def PiE_def)
moreover have "V ∈ Pow {0..<a + b} ⟹ ∃f∈extensional {1..a+b}. R f V" for V
by (intro bexI[of _ "λi∈{1..a+b}. if i - 1 ∈ V then A else B"]) (auto simp add: R_def PiE_def)
ultimately have total_R: "rel_set R (extensional {1..a+b}) (Pow {0..<a+b})"
by (auto simp: rel_set_def)
have P: "rel_fun R (rel_fun P op =) (λf x. f x = A) (λV y. y ∈ V)"
by (auto simp: P_def R_def Suc_le_eq gr0_conv_Suc rel_fun_def)
have eq_B: "x = B ⟷ x ≠ A" for x
by (cases x; simp)
{ fix f and m :: nat
have "card {x∈{1..m}. f x = B} = card ({1..m} - {x∈{1..m}. f x = A})"
by (simp add: eq_B set_diff_eq cong: conj_cong)
also have "… = m - card {x∈{1..m}. f x = A}"
by (subst card_Diff_subset) auto
finally have "card {x∈{1..m}. f x = B} = m - card {x∈{1..m}. f x = A}" . }
note card_B = this
note transfers = rel_fun_const card_transfer[THEN rel_funD, OF unique_R] rel_fun_conj rel_fun_ball
Collect_on_transfer[THEN rel_funD, OF total_R] Collect_on_transfer[THEN rel_funD, OF total_P]
rel_fun_trans[OF card_transfer, OF unique_P] rel_fun_trans[OF Collect_on_transfer[OF total_P]]
rel_fun_trans2'[where g="op ="] rel_fun_trans2'[where g="op <"] rel_fun_trans2'[where g="op -"]
have "all_countings a b = card {f ∈ extensional {1..a + b}. card {x ∈ {1..a + b}. f x = A} = a}"
using card_B by (simp add: all_countings_def PiE_iff vote.nchotomy cong: conj_cong)
also have "… = card {V∈Pow {0..<a+b}. card ({x∈{0 ..< a + b}. x ∈ V}) = a}"
by (intro P order_refl transfers)
finally show "all_countings a b = card ?A"
unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
have "valid_countings a b = card {f∈extensional {1..a+b}.
card {x∈{1..a+b}. f x = A} = a ∧ (∀m∈{1..a+b}. card {x∈{1..m}. f x = A} > m - card {x∈{1..m}. f x = A})}"
using card_B by (simp add: valid_countings_def PiE_iff vote.nchotomy cong: conj_cong)
also have "… = card {V∈Pow {0..<a+b}. card {x∈{0..<a+b}. x∈V} = a ∧
(∀m∈{1..a+b}. card {x∈{0..<m}. x∈V} > m - card {x∈{0..<m}. x∈V})}"
by (intro P order_refl transfers) auto
finally show "valid_countings a b = card ?V"
unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
qed
lemma all_countings: "all_countings a b = (a + b) choose a"
unfolding all_countings_set by (simp add: n_subsets)
subsection ‹Facts About @{term valid_countings}›
subsubsection ‹Non-Recursive Cases›
lemma card_V_eq_a: "V ⊆ {0..<a} ⟹ card V = a ⟷ V = {0..<a}"
using card_subset_eq[of "{0..<a}" V] by auto
lemma valid_countings_a_0: "valid_countings a 0 = 1"
by (simp add: valid_countings_set card_V_eq_a cong: conj_cong)
lemma valid_countings_eq_zero:
"a ≤ b ⟹ 0 < b ⟹ valid_countings a b = 0"
by (auto simp add: valid_countings_set Int_absorb1 intro!: bexI[of _ "a + b"])
lemma Ico_subset_finite: "i ⊆ {a ..< b::nat} ⟹ finite i"
by (auto dest: finite_subset)
lemma Icc_Suc2: "a ≤ b ⟹ {a..Suc b} = insert (Suc b) {a..b}"
by auto
lemma Ico_Suc2: "a ≤ b ⟹ {a..<Suc b} = insert b {a..<b}"
by auto
lemma valid_countings_Suc_Suc:
assumes "b < a"
shows "valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b"
proof -
let ?l = "Suc (a + b)"
let ?Q = "λV c. ∀m∈{1..c}. m - card ({0..<m} ∩ V) < card ({0..<m} ∩ V)"
let ?V = "λP. {V. (V ∈ Pow {0..<Suc ?l} ∧ P V) ∧ card V = Suc a ∧ ?Q V (Suc ?l)}"
have "valid_countings (Suc a) (Suc b) = card (?V (λV. ?l ∉ V)) + card (?V (λV. ?l ∈ V))"
unfolding valid_countings_set
by (subst card_Un_disjoint[symmetric]) (auto simp add: set_eq_iff intro!: arg_cong[where f=card])
also have "card (?V (λV. ?l ∈ V)) = valid_countings a (Suc b)"
unfolding valid_countings_set
proof (rule card_bij'[where f="λV. V - {?l}" and g="insert ?l"])
have *: "⋀m V. m ∈ {1..a + Suc b} ⟹ {0..<m} ∩ (V - {?l}) = {0..<m} ∩ V"
by auto
show "(λV. V - {?l}) ∈ ?V (λV. ?l ∈ V) → {V ∈ Pow {0..<a + Suc b}. card V = a ∧ ?Q V (a + Suc b)}"
by (auto simp: Ico_subset_finite *)
{ fix V assume V: "V ⊆ {0..<?l}"
then have "finite V" "?l ∉ V" "{0..<Suc ?l} ∩ V = V"
by (auto dest: finite_subset)
with V have "card (insert ?l V) = Suc (card V)"
"card ({0..<m} ∩ insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} ∩ V))"
if "m ≤ Suc ?l" for m
using that by auto }
then show "insert ?l ∈ {V ∈ Pow {0..<a + Suc b}. card V = a ∧ ?Q V (a + Suc b)} → ?V (λV. ?l ∈ V)"
using ‹b < a› by auto
qed auto
also have "card (?V (λV. ?l ∉ V)) = valid_countings (Suc a) b"
unfolding valid_countings_set
proof (intro arg_cong[where f="λP. card {x. P x}"] ext conj_cong)
fix V assume "V ∈ Pow {0..<Suc a + b}" and [simp]: "card V = Suc a"
then have [simp]: "V ⊆ {0..<Suc ?l}"
by auto
show "?Q V (Suc ?l) = ?Q V (Suc a + b)"
using ‹b<a› by (simp add: Int_absorb1 Icc_Suc2)
qed (auto simp: subset_eq less_Suc_eq)
finally show ?thesis
by simp
qed
lemma valid_countings:
"(a + b) * valid_countings a b = (a - b) * ((a + b) choose a)"
proof (induct a arbitrary: b)
case 0 show ?case
by (cases b) (simp_all add: valid_countings_eq_zero)
next
case (Suc a) note Suc_a = this
show ?case
proof (induct b)
case (Suc b) note Suc_b = this
show ?case
proof cases
assume "a ≤ b" then show ?thesis
by (simp add: valid_countings_eq_zero)
next
assume "¬ a ≤ b"
then have "b < a" by simp
have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
(Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
by (simp add: sign_simps)
also have "… = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
using ‹b<a› by (intro add_diff_assoc2 mult_mono) auto
also have "… = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
using ‹b<a› by (intro arg_cong2[where f="op -"] add_diff_assoc mult_mono) auto
also have "… = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
by (simp add: sign_simps)
finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
unfolding diff_mult_distrib by simp
have "(Suc a * Suc (a + b)) * ((Suc a + Suc b) * valid_countings (Suc a) (Suc b)) =
(Suc a + Suc b) * Suc a * ((a + Suc b) * valid_countings a (Suc b) + (Suc a + b) * valid_countings (Suc a) b)"
unfolding valid_countings_Suc_Suc[OF ‹b < a›] by (simp add: field_simps)
also have "... = (Suc a + Suc b) * ((a - Suc b) * (Suc a * (Suc (a + b) choose a)) +
(Suc a - b) * (Suc a * (Suc (a + b) choose Suc a)))"
unfolding Suc_a Suc_b by (simp add: field_simps)
also have "... = (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc (Suc a + b) * (Suc a + b choose a))"
unfolding Suc_times_binomial_add by (simp add: field_simps)
also have "... = Suc a * (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc a + Suc b choose Suc a)"
unfolding Suc_times_binomial_eq by (simp add: field_simps)
also have "... = (Suc a * Suc (a + b)) * ((Suc a - Suc b) * (Suc a + Suc b choose Suc a))"
unfolding rearrange by (simp only: mult_ac)
finally show ?thesis
unfolding mult_cancel1 by simp
qed
qed (simp add: valid_countings_a_0)
qed
lemma valid_countings_eq[code]:
"valid_countings a b = (if a + b = 0 then 1 else ((a - b) * ((a + b) choose a)) div (a + b))"
by (simp add: valid_countings[symmetric] valid_countings_a_0)
subsection ‹Relation Between @{term valid_countings} and @{term all_countings}›
lemma main_nat: "(a + b) * valid_countings a b = (a - b) * all_countings a b"
unfolding valid_countings all_countings ..
lemma main_real:
assumes "b < a"
shows "valid_countings a b = (a - b) / (a + b) * all_countings a b"
using assms
proof -
from main_nat[of a b] ‹b < a› have
"(real a + real b) * real (valid_countings a b) = (real a - real b) * real (all_countings a b)"
by (simp only: of_nat_add[symmetric] of_nat_mult[symmetric]) auto
from this ‹b < a› show ?thesis
by (subst mult_left_cancel[of "real a + real b", symmetric]) auto
qed
lemma
"valid_countings a b = (if a ≤ b then (if b = 0 then 1 else 0) else (a - b) / (a + b) * all_countings a b)"
proof (cases "a ≤ b")
case False
from this show ?thesis by (simp add: main_real)
next
case True
from this show ?thesis
by (auto simp add: valid_countings_a_0 all_countings valid_countings_eq_zero)
qed
subsubsection ‹Executable Definition›
declare all_countings_def [code del]
declare all_countings[code]
value "all_countings 1 0"
value "all_countings 0 1"
value "all_countings 1 1"
value "all_countings 2 1"
value "all_countings 1 2"
value "all_countings 2 4"
value "all_countings 4 2"
subsubsection ‹Executable Definition›
declare valid_countings_def [code del]
value "valid_countings 1 0"
value "valid_countings 0 1"
value "valid_countings 1 1"
value "valid_countings 2 1"
value "valid_countings 1 2"
value "valid_countings 2 4"
value "valid_countings 4 2"
end