theory Ballot imports
Complex_Main "HOL-Library.FuncSet" begin
subsection \<open>Preliminaries\<close>
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 \<open>Formalization of Problem Statement\<close>
subsubsection \<open>Basic Definitions\<close>
datatype vote = A | B
definition "all_countings a b = card {f \ {1 .. a + b} \\<^sub>E {A, B}.
card {x \<in> {1 .. a + b}. f x = A} = a \<and> card {x \<in> {1 .. a + b}. f x = B} = b}"
definition "valid_countings a b =
card {f\<in>{1..a+b} \<rightarrow>\<^sub>E {A, B}.
card {x\<in>{1..a+b}. f x = A} = a \<and> card {x\<in>{1..a+b}. f x = B} = b \<and>
(\<forall>m\<in>{1..a+b}. card {x\<in>{1..m}. f x = A} > card {x\<in>{1..m}. f x = B})}"
subsubsection \<open>Equivalence with Set Cardinality\<close>
lemma Collect_on_transfer: assumes"rel_set R X Y" shows"rel_fun (rel_fun R (=)) (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 (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g' (f1' y) (f2' y))" by (auto simp: rel_fun_def)
lemma rel_fun_trans2': "rel_fun R (=) f1 f1' \ rel_fun R (=) f2 f2' \
rel_fun R (=) (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g (f1' y) (f2' y))" by (auto simp: rel_fun_def)
lemma rel_fun_const: "rel_fun R (=) (\x. a) (\y. a)" by auto
lemma rel_fun_conj: "rel_fun R (=) f f' \ rel_fun R (=) g g' \ rel_fun R (=) (\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 (=) (f i) (f' i)) \ rel_fun R (=) (\x. \i\I. f i x) (\y. \i\I. f' i y)" by (auto simp: rel_fun_def rel_set_def)
have"valid_countings a b = card {f\extensional {1..a+b}.
card {x\<in>{1..a+b}. f x = A} = a \<and> (\<forall>m\<in>{1..a+b}. card {x\<in>{1..m}. f x = A} > m - card {x\<in>{1..m}. f x = A})}" using card_B by (simp add: valid_countings_def PiE_iff vote.nchotomy cong: conj_cong) alsohave"\ = card {V\Pow {0..{0..V} = a \
(\<forall>m\<in>{1..a+b}. card {x\<in>{0..<m}. x\<in>V} > m - card {x\<in>{0..<m}. x\<in>V})}" by (intro P order_refl transfers) auto finallyshow"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 \<open>Facts About \<^term>\<open>valid_countings\<close>\<close>
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" thenhave"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: algebra_simps) alsohave"\ = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b" using\<open>b<a\<close> by (intro add_diff_assoc2 mult_mono) auto alsohave"\ = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b" using\<open>b<a\<close> by (intro arg_cong2[where f="(-)"] add_diff_assoc mult_mono) auto alsohave"\ = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))" by (simp add: algebra_simps) finallyhave 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 \<open>b < a\<close>] by (simp add: field_simps) alsohave"... = (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) alsohave"... = (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) alsohave"... = 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) alsohave"... = (Suc a * Suc (a + b)) * ((Suc a - Suc b) * (Suc a + Suc b choose Suc a))" unfolding rearrange by (simp only: mult_ac) finallyshow ?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 \<open>Relation Between \<^term>\<open>valid_countings\<close> and \<^term>\<open>all_countings\<close>\<close>
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] \<open>b < a\<close> 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 \<open>b < a\<close> 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