src/HOL/ex/Ballot.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 63040 eb4ddd18d635 child 63540 f8652d0534fa permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*   Title: HOL/ex/Ballot.thy
```
```     2      Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com>
```
```     3      Author: Johannes Hölzl <hoelzl@in.tum.de>
```
```     4 *)
```
```     5
```
```     6 section \<open>Bertrand's Ballot Theorem\<close>
```
```     7
```
```     8 theory Ballot
```
```     9 imports
```
```    10   Complex_Main
```
```    11   "~~/src/HOL/Library/FuncSet"
```
```    12 begin
```
```    13
```
```    14 subsection \<open>Preliminaries\<close>
```
```    15
```
```    16 lemma card_bij':
```
```    17   assumes "f \<in> A \<rightarrow> B" "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
```
```    18     and "g \<in> B \<rightarrow> A" "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
```
```    19   shows "card A = card B"
```
```    20   apply (rule bij_betw_same_card)
```
```    21   apply (rule bij_betwI)
```
```    22   apply fact+
```
```    23   done
```
```    24
```
```    25 subsection \<open>Formalization of Problem Statement\<close>
```
```    26
```
```    27 subsubsection \<open>Basic Definitions\<close>
```
```    28
```
```    29 datatype vote = A | B
```
```    30
```
```    31 definition
```
```    32   "all_countings a b = card {f \<in> {1 .. a + b} \<rightarrow>\<^sub>E {A, B}.
```
```    33       card {x \<in> {1 .. a + b}. f x = A} = a \<and> card {x \<in> {1 .. a + b}. f x = B} = b}"
```
```    34
```
```    35 definition
```
```    36   "valid_countings a b =
```
```    37     card {f\<in>{1..a+b} \<rightarrow>\<^sub>E {A, B}.
```
```    38       card {x\<in>{1..a+b}. f x = A} = a \<and> card {x\<in>{1..a+b}. f x = B} = b \<and>
```
```    39       (\<forall>m\<in>{1..a+b}. card {x\<in>{1..m}. f x = A} > card {x\<in>{1..m}. f x = B})}"
```
```    40
```
```    41 subsubsection \<open>Equivalence with Set Cardinality\<close>
```
```    42
```
```    43 lemma Collect_on_transfer:
```
```    44   assumes "rel_set R X Y"
```
```    45   shows "rel_fun (rel_fun R op =) (rel_set R) (\<lambda>P. {x\<in>X. P x}) (\<lambda>P. {y\<in>Y. P y})"
```
```    46   using assms unfolding rel_fun_def rel_set_def by fast
```
```    47
```
```    48 lemma rel_fun_trans:
```
```    49   "rel_fun P Q g g' \<Longrightarrow> rel_fun R P f f' \<Longrightarrow> rel_fun R Q (\<lambda>x. g (f x)) (\<lambda>y. g' (f' y))"
```
```    50   by (auto simp: rel_fun_def)
```
```    51
```
```    52 lemma rel_fun_trans2:
```
```    53   "rel_fun P1 (rel_fun P2 Q) g g' \<Longrightarrow> rel_fun R P1 f1 f1' \<Longrightarrow> rel_fun R P2 f2 f2' \<Longrightarrow>
```
```    54     rel_fun R Q (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g' (f1' y) (f2' y))"
```
```    55   by (auto simp: rel_fun_def)
```
```    56
```
```    57 lemma rel_fun_trans2':
```
```    58   "rel_fun R (op =) f1 f1' \<Longrightarrow> rel_fun R (op =) f2 f2' \<Longrightarrow>
```
```    59     rel_fun R (op =) (\<lambda>x. g (f1 x) (f2 x)) (\<lambda>y. g (f1' y) (f2' y))"
```
```    60   by (auto simp: rel_fun_def)
```
```    61
```
```    62 lemma rel_fun_const: "rel_fun R (op =) (\<lambda>x. a) (\<lambda>y. a)"
```
```    63   by auto
```
```    64
```
```    65 lemma rel_fun_conj:
```
```    66   "rel_fun R (op =) f f' \<Longrightarrow> rel_fun R (op =) g g' \<Longrightarrow> rel_fun R (op =) (\<lambda>x. f x \<and> g x) (\<lambda>y. f' y \<and> g' y)"
```
```    67   by (auto simp: rel_fun_def)
```
```    68
```
```    69 lemma rel_fun_ball:
```
```    70   "(\<And>i. i \<in> I \<Longrightarrow> rel_fun R (op =) (f i) (f' i)) \<Longrightarrow> rel_fun R (op =) (\<lambda>x. \<forall>i\<in>I. f i x) (\<lambda>y. \<forall>i\<in>I. f' i y)"
```
```    71   by (auto simp: rel_fun_def rel_set_def)
```
```    72
```
```    73 lemma
```
```    74   shows all_countings_set: "all_countings a b = card {V\<in>Pow {0..<a+b}. card V = a}"
```
```    75       (is "_ = card ?A")
```
```    76     and valid_countings_set: "valid_countings a b =
```
```    77       card {V\<in>Pow {0..<a+b}. card V = a \<and> (\<forall>m\<in>{1..a+b}. card ({0..<m} \<inter> V) > m - card ({0..<m} \<inter> V))}"
```
```    78       (is "_ = card ?V")
```
```    79 proof -
```
```    80   define P where "P j i \<longleftrightarrow> i < a + b \<and> j = Suc i" for j i
```
```    81   have unique_P: "bi_unique P" and total_P: "\<And>m. m \<le> a + b \<Longrightarrow> rel_set P {1..m} {0..<m}"
```
```    82     by (auto simp add: bi_unique_def rel_set_def P_def Suc_le_eq gr0_conv_Suc)
```
```    83   have rel_fun_P: "\<And>R f g. (\<And>i. i < a+b \<Longrightarrow> R (f  (Suc i)) (g i)) \<Longrightarrow> rel_fun P R f g"
```
```    84     by (simp add: rel_fun_def P_def)
```
```    85
```
```    86   define R where "R f V \<longleftrightarrow>
```
```    87     V \<subseteq> {0..<a+b} \<and> f \<in> extensional {1..a+b} \<and> (\<forall>i<a+b. i \<in> V \<longleftrightarrow> f (Suc i) = A)" for f V
```
```    88   { fix f g :: "nat \<Rightarrow> vote" assume "f \<in> extensional {1..a + b}" "g \<in> extensional {1..a + b}"
```
```    89     moreover assume "\<forall>i<a + b. (f (Suc i) = A) = (g (Suc i) = A)"
```
```    90     then have "\<forall>i<a + b. f (Suc i) = g (Suc i)"
```
```    91       by (metis vote.nchotomy)
```
```    92     ultimately have "f i = g i" for i
```
```    93       by (cases "i \<in> {1..a+b}") (auto simp: extensional_def Suc_le_eq gr0_conv_Suc) }
```
```    94   then have unique_R: "bi_unique R"
```
```    95     by (auto simp: bi_unique_def R_def)
```
```    96
```
```    97   have "f \<in> extensional {1..a + b} \<Longrightarrow> \<exists>V\<in>Pow {0..<a + b}. R f V" for f
```
```    98     by (intro bexI[of _ "{i. i < a+b \<and> f (Suc i) = A}"]) (auto simp add: R_def PiE_def)
```
```    99   moreover have "V \<in> Pow {0..<a + b} \<Longrightarrow> \<exists>f\<in>extensional {1..a+b}. R f V" for V
```
```   100     by (intro bexI[of _ "\<lambda>i\<in>{1..a+b}. if i - 1 \<in> V then A else B"]) (auto simp add: R_def PiE_def)
```
```   101   ultimately have total_R: "rel_set R (extensional {1..a+b}) (Pow {0..<a+b})"
```
```   102     by (auto simp: rel_set_def)
```
```   103
```
```   104   have P: "rel_fun R (rel_fun P op =) (\<lambda>f x. f x = A) (\<lambda>V y. y \<in> V)"
```
```   105     by (auto simp: P_def R_def Suc_le_eq gr0_conv_Suc rel_fun_def)
```
```   106
```
```   107   have eq_B: "x = B \<longleftrightarrow> x \<noteq> A" for x
```
```   108     by (cases x; simp)
```
```   109
```
```   110   { fix f and m :: nat
```
```   111     have "card {x\<in>{1..m}. f x = B} = card ({1..m} - {x\<in>{1..m}. f x = A})"
```
```   112       by (simp add: eq_B set_diff_eq cong: conj_cong)
```
```   113     also have "\<dots> = m - card {x\<in>{1..m}. f x = A}"
```
```   114       by (subst card_Diff_subset) auto
```
```   115     finally have "card {x\<in>{1..m}. f x = B} = m - card {x\<in>{1..m}. f x = A}" . }
```
```   116   note card_B = this
```
```   117
```
```   118   note transfers = rel_fun_const card_transfer[THEN rel_funD, OF unique_R] rel_fun_conj rel_fun_ball
```
```   119     Collect_on_transfer[THEN rel_funD, OF total_R] Collect_on_transfer[THEN rel_funD, OF total_P]
```
```   120     rel_fun_trans[OF card_transfer, OF unique_P] rel_fun_trans[OF Collect_on_transfer[OF total_P]]
```
```   121     rel_fun_trans2'[where g="op ="] rel_fun_trans2'[where g="op <"] rel_fun_trans2'[where g="op -"]
```
```   122
```
```   123   have "all_countings a b = card {f \<in> extensional {1..a + b}. card {x \<in> {1..a + b}. f x = A} = a}"
```
```   124     using card_B by (simp add: all_countings_def PiE_iff vote.nchotomy cong: conj_cong)
```
```   125   also have "\<dots> = card {V\<in>Pow {0..<a+b}. card ({x\<in>{0 ..< a + b}. x \<in> V}) = a}"
```
```   126     by (intro P order_refl transfers)
```
```   127   finally show "all_countings a b = card ?A"
```
```   128     unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
```
```   129
```
```   130   have "valid_countings a b = card {f\<in>extensional {1..a+b}.
```
```   131       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})}"
```
```   132     using card_B by (simp add: valid_countings_def PiE_iff vote.nchotomy cong: conj_cong)
```
```   133   also have "\<dots> = card {V\<in>Pow {0..<a+b}. card {x\<in>{0..<a+b}. x\<in>V} = a \<and>
```
```   134     (\<forall>m\<in>{1..a+b}. card {x\<in>{0..<m}. x\<in>V} > m - card {x\<in>{0..<m}. x\<in>V})}"
```
```   135     by (intro P order_refl transfers) auto
```
```   136   finally show "valid_countings a b = card ?V"
```
```   137     unfolding Int_def[symmetric] by (simp add: Int_absorb1 cong: conj_cong)
```
```   138 qed
```
```   139
```
```   140 lemma all_countings: "all_countings a b = (a + b) choose a"
```
```   141   unfolding all_countings_set by (simp add: n_subsets)
```
```   142
```
```   143 subsection \<open>Facts About @{term valid_countings}\<close>
```
```   144
```
```   145 subsubsection \<open>Non-Recursive Cases\<close>
```
```   146
```
```   147 lemma card_V_eq_a: "V \<subseteq> {0..<a} \<Longrightarrow> card V = a \<longleftrightarrow> V = {0..<a}"
```
```   148   using card_subset_eq[of "{0..<a}" V] by auto
```
```   149
```
```   150 lemma valid_countings_a_0: "valid_countings a 0 = 1"
```
```   151   by (simp add: valid_countings_set card_V_eq_a cong: conj_cong)
```
```   152
```
```   153 lemma valid_countings_eq_zero:
```
```   154   "a \<le> b \<Longrightarrow> 0 < b \<Longrightarrow> valid_countings a b = 0"
```
```   155   by (auto simp add: valid_countings_set Int_absorb1 intro!: bexI[of _ "a + b"])
```
```   156
```
```   157 lemma Ico_subset_finite: "i \<subseteq> {a ..< b::nat} \<Longrightarrow> finite i"
```
```   158   by (auto dest: finite_subset)
```
```   159
```
```   160 lemma Icc_Suc2: "a \<le> b \<Longrightarrow> {a..Suc b} = insert (Suc b) {a..b}"
```
```   161   by auto
```
```   162
```
```   163 lemma Ico_Suc2: "a \<le> b \<Longrightarrow> {a..<Suc b} = insert b {a..<b}"
```
```   164   by auto
```
```   165
```
```   166 lemma valid_countings_Suc_Suc:
```
```   167   assumes "b < a"
```
```   168   shows "valid_countings (Suc a) (Suc b) = valid_countings a (Suc b) + valid_countings (Suc a) b"
```
```   169 proof -
```
```   170   let ?l = "Suc (a + b)"
```
```   171   let ?Q = "\<lambda>V c. \<forall>m\<in>{1..c}. m - card ({0..<m} \<inter> V) < card ({0..<m} \<inter> V)"
```
```   172   let ?V = "\<lambda>P. {V. (V \<in> Pow {0..<Suc ?l} \<and> P V) \<and> card V = Suc a \<and> ?Q V (Suc ?l)}"
```
```   173   have "valid_countings (Suc a) (Suc b) = card (?V (\<lambda>V. ?l \<notin> V)) + card (?V (\<lambda>V. ?l \<in> V))"
```
```   174     unfolding valid_countings_set
```
```   175     by (subst card_Un_disjoint[symmetric]) (auto simp add: set_eq_iff intro!: arg_cong[where f=card])
```
```   176   also have "card (?V (\<lambda>V. ?l \<in> V)) = valid_countings a (Suc b)"
```
```   177     unfolding valid_countings_set
```
```   178   proof (rule card_bij'[where f="\<lambda>V. V - {?l}" and g="insert ?l"])
```
```   179     have *: "\<And>m V. m \<in> {1..a + Suc b} \<Longrightarrow> {0..<m} \<inter> (V - {?l}) = {0..<m} \<inter> V"
```
```   180       by auto
```
```   181     show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}"
```
```   182       by (auto simp: Ico_subset_finite *)
```
```   183     { fix V assume "V \<subseteq> {0..<?l}"
```
```   184       moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
```
```   185         by (auto dest: finite_subset)
```
```   186       ultimately have "card (insert ?l V) = Suc (card V)"
```
```   187         "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
```
```   188         if "m \<le> Suc ?l" for m
```
```   189         using that by auto }
```
```   190     then show "insert ?l \<in> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)} \<rightarrow> ?V (\<lambda>V. ?l \<in> V)"
```
```   191       using \<open>b < a\<close> by auto
```
```   192   qed auto
```
```   193   also have "card (?V (\<lambda>V. ?l \<notin> V)) = valid_countings (Suc a) b"
```
```   194     unfolding valid_countings_set
```
```   195   proof (intro arg_cong[where f="\<lambda>P. card {x. P x}"] ext conj_cong)
```
```   196     fix V assume "V \<in> Pow {0..<Suc a + b}" and [simp]: "card V = Suc a"
```
```   197     then have [simp]: "V \<subseteq> {0..<Suc ?l}"
```
```   198       by auto
```
```   199     show "?Q V (Suc ?l) = ?Q V (Suc a + b)"
```
```   200       using \<open>b<a\<close> by (simp add: Int_absorb1 Icc_Suc2)
```
```   201   qed (auto simp: subset_eq less_Suc_eq)
```
```   202   finally show ?thesis
```
```   203     by simp
```
```   204 qed
```
```   205
```
```   206 lemma valid_countings:
```
```   207   "(a + b) * valid_countings a b = (a - b) * ((a + b) choose a)"
```
```   208 proof (induct a arbitrary: b)
```
```   209   case 0 show ?case
```
```   210     by (cases b) (simp_all add: valid_countings_eq_zero)
```
```   211 next
```
```   212   case (Suc a) note Suc_a = this
```
```   213   show ?case
```
```   214   proof (induct b)
```
```   215     case (Suc b) note Suc_b = this
```
```   216     show ?case
```
```   217     proof cases
```
```   218       assume "a \<le> b" then show ?thesis
```
```   219         by (simp add: valid_countings_eq_zero)
```
```   220     next
```
```   221       assume "\<not> a \<le> b"
```
```   222       then have "b < a" by simp
```
```   223
```
```   224       have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
```
```   225         (Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
```
```   226         by (simp add: sign_simps)
```
```   227       also have "\<dots> = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
```
```   228         using \<open>b<a\<close> by (intro add_diff_assoc2 mult_mono) auto
```
```   229       also have "\<dots> = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
```
```   230         using \<open>b<a\<close> by (intro arg_cong2[where f="op -"] add_diff_assoc mult_mono) auto
```
```   231       also have "\<dots> = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
```
```   232         by (simp add: sign_simps)
```
```   233       finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
```
```   234         unfolding diff_mult_distrib by simp
```
```   235
```
```   236       have "(Suc a * Suc (a + b)) * ((Suc a + Suc b) * valid_countings (Suc a) (Suc b)) =
```
```   237         (Suc a + Suc b) * Suc a * ((a + Suc b) * valid_countings a (Suc b) + (Suc a + b) * valid_countings (Suc a) b)"
```
```   238         unfolding valid_countings_Suc_Suc[OF \<open>b < a\<close>] by (simp add: field_simps)
```
```   239       also have "... = (Suc a + Suc b) * ((a - Suc b) * (Suc a * (Suc (a + b) choose a)) +
```
```   240         (Suc a - b) * (Suc a * (Suc (a + b) choose Suc a)))"
```
```   241         unfolding Suc_a Suc_b by (simp add: field_simps)
```
```   242       also have "... = (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc (Suc a + b) * (Suc a + b choose a))"
```
```   243         unfolding Suc_times_binomial_add by (simp add: field_simps)
```
```   244       also have "... = Suc a * (Suc a * (a - Suc b) + (Suc a - b) * Suc b) * (Suc a + Suc b choose Suc a)"
```
```   245         unfolding Suc_times_binomial_eq by (simp add: field_simps)
```
```   246       also have "... = (Suc a * Suc (a + b)) * ((Suc a - Suc b) * (Suc a + Suc b choose Suc a))"
```
```   247         unfolding rearrange by (simp only: mult_ac)
```
```   248       finally show ?thesis
```
```   249         unfolding mult_cancel1 by simp
```
```   250     qed
```
```   251   qed (simp add: valid_countings_a_0)
```
```   252 qed
```
```   253
```
```   254 lemma valid_countings_eq[code]:
```
```   255   "valid_countings a b = (if a + b = 0 then 1 else ((a - b) * ((a + b) choose a)) div (a + b))"
```
```   256   by (simp add: valid_countings[symmetric] valid_countings_a_0)
```
```   257
```
```   258 subsection \<open>Relation Between @{term valid_countings} and @{term all_countings}\<close>
```
```   259
```
```   260 lemma main_nat: "(a + b) * valid_countings a b = (a - b) * all_countings a b"
```
```   261   unfolding valid_countings all_countings ..
```
```   262
```
```   263 lemma main_real:
```
```   264   assumes "b < a"
```
```   265   shows "valid_countings a b = (a - b) / (a + b) * all_countings a b"
```
```   266 using assms
```
```   267 proof -
```
```   268   from main_nat[of a b] \<open>b < a\<close> have
```
```   269     "(real a + real b) * real (valid_countings a b) = (real a - real b) * real (all_countings a b)"
```
```   270     by (simp only: of_nat_add[symmetric] of_nat_mult[symmetric]) auto
```
```   271   from this \<open>b < a\<close> show ?thesis
```
```   272     by (subst mult_left_cancel[of "real a + real b", symmetric]) auto
```
```   273 qed
```
```   274
```
```   275 lemma
```
```   276   "valid_countings a b = (if a \<le> b then (if b = 0 then 1 else 0) else (a - b) / (a + b) * all_countings a b)"
```
```   277 proof (cases "a \<le> b")
```
```   278   case False
```
```   279     from this show ?thesis by (simp add: main_real)
```
```   280 next
```
```   281   case True
```
```   282     from this show ?thesis
```
```   283       by (auto simp add: valid_countings_a_0 all_countings valid_countings_eq_zero)
```
```   284 qed
```
```   285
```
```   286 subsubsection \<open>Executable Definition\<close>
```
```   287
```
```   288 declare all_countings_def [code del]
```
```   289 declare all_countings[code]
```
```   290
```
```   291 value "all_countings 1 0"
```
```   292 value "all_countings 0 1"
```
```   293 value "all_countings 1 1"
```
```   294 value "all_countings 2 1"
```
```   295 value "all_countings 1 2"
```
```   296 value "all_countings 2 4"
```
```   297 value "all_countings 4 2"
```
```   298
```
```   299 subsubsection \<open>Executable Definition\<close>
```
```   300
```
```   301 declare valid_countings_def [code del]
```
```   302
```
```   303 value "valid_countings 1 0"
```
```   304 value "valid_countings 0 1"
```
```   305 value "valid_countings 1 1"
```
```   306 value "valid_countings 2 1"
```
```   307 value "valid_countings 1 2"
```
```   308 value "valid_countings 2 4"
```
```   309 value "valid_countings 4 2"
```
```   310
```
```   311 end
```