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