src/HOL/Number_Theory/Binomial.thy
author haftmann
Mon Mar 08 09:38:58 2010 +0100 (2010-03-08)
changeset 35644 d20cf282342e
parent 32479 521cc9bf2958
child 35731 1bdaa24fb56d
permissions -rw-r--r--
transfer: avoid camel case
nipkow@31719
     1
(*  Title:      Binomial.thy
nipkow@31719
     2
    Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
nipkow@31719
     3
nipkow@31719
     4
avigad@32036
     5
Defines the "choose" function, and establishes basic properties.
nipkow@31719
     6
nipkow@31719
     7
The original theory "Binomial" was by Lawrence C. Paulson, based on
nipkow@31719
     8
the work of Andy Gordon and Florian Kammueller. The approach here,
nipkow@31719
     9
which derives the definition of binomial coefficients in terms of the
nipkow@31719
    10
factorial function, is due to Jeremy Avigad. The binomial theorem was
nipkow@31719
    11
formalized by Tobias Nipkow.
nipkow@31719
    12
nipkow@31719
    13
*)
nipkow@31719
    14
nipkow@31719
    15
nipkow@31719
    16
header {* Binomial *}
nipkow@31719
    17
nipkow@31719
    18
theory Binomial
avigad@32036
    19
imports Cong Fact
nipkow@31719
    20
begin
nipkow@31719
    21
nipkow@31719
    22
nipkow@31719
    23
subsection {* Main definitions *}
nipkow@31719
    24
nipkow@31719
    25
class binomial =
nipkow@31719
    26
nipkow@31719
    27
fixes 
nipkow@31719
    28
  binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
nipkow@31719
    29
nipkow@31719
    30
(* definitions for the natural numbers *)
nipkow@31719
    31
nipkow@31719
    32
instantiation nat :: binomial
nipkow@31719
    33
nipkow@31719
    34
begin 
nipkow@31719
    35
nipkow@31719
    36
fun
nipkow@31719
    37
  binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
nipkow@31719
    38
where
nipkow@31719
    39
  "binomial_nat n k =
nipkow@31719
    40
   (if k = 0 then 1 else
nipkow@31719
    41
    if n = 0 then 0 else
nipkow@31719
    42
      (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
nipkow@31719
    43
nipkow@31719
    44
instance proof qed
nipkow@31719
    45
nipkow@31719
    46
end
nipkow@31719
    47
nipkow@31719
    48
(* definitions for the integers *)
nipkow@31719
    49
nipkow@31719
    50
instantiation int :: binomial
nipkow@31719
    51
nipkow@31719
    52
begin 
nipkow@31719
    53
nipkow@31719
    54
definition
nipkow@31719
    55
  binomial_int :: "int => int \<Rightarrow> int"
nipkow@31719
    56
where
nipkow@31719
    57
  "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
nipkow@31719
    58
      else 0)"
nipkow@31719
    59
instance proof qed
nipkow@31719
    60
nipkow@31719
    61
end
nipkow@31719
    62
nipkow@31719
    63
nipkow@31719
    64
subsection {* Set up Transfer *}
nipkow@31719
    65
nipkow@31719
    66
lemma transfer_nat_int_binomial:
nipkow@31719
    67
  "(n::int) >= 0 \<Longrightarrow> k >= 0 \<Longrightarrow> binomial (nat n) (nat k) = 
nipkow@31719
    68
      nat (binomial n k)"
avigad@32036
    69
  unfolding binomial_int_def 
nipkow@31719
    70
  by auto
nipkow@31719
    71
avigad@32036
    72
lemma transfer_nat_int_binomial_closure:
nipkow@31719
    73
  "n >= (0::int) \<Longrightarrow> k >= 0 \<Longrightarrow> binomial n k >= 0"
avigad@32036
    74
  by (auto simp add: binomial_int_def)
nipkow@31719
    75
haftmann@35644
    76
declare transfer_morphism_nat_int[transfer add return: 
avigad@32036
    77
    transfer_nat_int_binomial transfer_nat_int_binomial_closure]
nipkow@31719
    78
nipkow@31719
    79
lemma transfer_int_nat_binomial:
nipkow@31719
    80
  "binomial (int n) (int k) = int (binomial n k)"
nipkow@31719
    81
  unfolding fact_int_def binomial_int_def by auto
nipkow@31719
    82
avigad@32036
    83
lemma transfer_int_nat_binomial_closure:
nipkow@31719
    84
  "is_nat n \<Longrightarrow> is_nat k \<Longrightarrow> binomial n k >= 0"
avigad@32036
    85
  by (auto simp add: binomial_int_def)
nipkow@31719
    86
haftmann@35644
    87
declare transfer_morphism_int_nat[transfer add return: 
avigad@32036
    88
    transfer_int_nat_binomial transfer_int_nat_binomial_closure]
nipkow@31719
    89
nipkow@31719
    90
nipkow@31719
    91
subsection {* Binomial coefficients *}
nipkow@31719
    92
nipkow@31952
    93
lemma choose_zero_nat [simp]: "(n::nat) choose 0 = 1"
nipkow@31719
    94
  by simp
nipkow@31719
    95
nipkow@31952
    96
lemma choose_zero_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 0 = 1"
nipkow@31719
    97
  by (simp add: binomial_int_def)
nipkow@31719
    98
nipkow@31952
    99
lemma zero_choose_nat [rule_format,simp]: "ALL (k::nat) > n. n choose k = 0"
nipkow@31952
   100
  by (induct n rule: induct'_nat, auto)
nipkow@31719
   101
nipkow@31952
   102
lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
nipkow@31719
   103
  unfolding binomial_int_def apply (case_tac "n < 0")
nipkow@31719
   104
  apply force
nipkow@31719
   105
  apply (simp del: binomial_nat.simps)
nipkow@31719
   106
done
nipkow@31719
   107
nipkow@31952
   108
lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
nipkow@31719
   109
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
nipkow@31719
   110
  by simp
nipkow@31719
   111
nipkow@31952
   112
lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
nipkow@31719
   113
    (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
nipkow@31952
   114
  unfolding binomial_int_def apply (subst choose_reduce_nat)
nipkow@31719
   115
    apply (auto simp del: binomial_nat.simps 
nipkow@31719
   116
      simp add: nat_diff_distrib)
nipkow@31719
   117
done
nipkow@31719
   118
nipkow@31952
   119
lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) = 
nipkow@31719
   120
    (n choose (k + 1)) + (n choose k)"
nipkow@31952
   121
  by (simp add: choose_reduce_nat)
nipkow@31719
   122
nipkow@31952
   123
lemma choose_Suc_nat: "(Suc n) choose (Suc k) = 
nipkow@31719
   124
    (n choose (Suc k)) + (n choose k)"
nipkow@31952
   125
  by (simp add: choose_reduce_nat One_nat_def)
nipkow@31719
   126
nipkow@31952
   127
lemma choose_plus_one_int: "n \<ge> 0 \<Longrightarrow> k \<ge> 0 \<Longrightarrow> ((n::int) + 1) choose (k + 1) = 
nipkow@31719
   128
    (n choose (k + 1)) + (n choose k)"
nipkow@31952
   129
  by (simp add: binomial_int_def choose_plus_one_nat nat_add_distrib del: binomial_nat.simps)
nipkow@31719
   130
nipkow@31719
   131
declare binomial_nat.simps [simp del]
nipkow@31719
   132
nipkow@31952
   133
lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
nipkow@31952
   134
  by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
nipkow@31719
   135
nipkow@31952
   136
lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
nipkow@31719
   137
  by (auto simp add: binomial_int_def)
nipkow@31719
   138
nipkow@31952
   139
lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
nipkow@31952
   140
  by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
nipkow@31719
   141
nipkow@31952
   142
lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
nipkow@31719
   143
  by (auto simp add: binomial_int_def)
nipkow@31719
   144
nipkow@31952
   145
lemma plus_one_choose_self_nat [simp]: "(n::nat) + 1 choose n = n + 1"
nipkow@31952
   146
  apply (induct n rule: induct'_nat, force)
nipkow@31719
   147
  apply (case_tac "n = 0")
nipkow@31719
   148
  apply auto
nipkow@31952
   149
  apply (subst choose_reduce_nat)
nipkow@31719
   150
  apply (auto simp add: One_nat_def)  
nipkow@31719
   151
  (* natdiff_cancel_numerals introduces Suc *)
nipkow@31719
   152
done
nipkow@31719
   153
nipkow@31952
   154
lemma Suc_choose_self_nat [simp]: "(Suc n) choose n = Suc n"
nipkow@31952
   155
  using plus_one_choose_self_nat by (simp add: One_nat_def)
nipkow@31719
   156
nipkow@31952
   157
lemma plus_one_choose_self_int [rule_format, simp]: 
nipkow@31719
   158
    "(n::int) \<ge> 0 \<longrightarrow> n + 1 choose n = n + 1"
nipkow@31719
   159
   by (auto simp add: binomial_int_def nat_add_distrib)
nipkow@31719
   160
nipkow@31719
   161
(* bounded quantification doesn't work with the unicode characters? *)
nipkow@31952
   162
lemma choose_pos_nat [rule_format]: "ALL k <= (n::nat). 
nipkow@31719
   163
    ((n::nat) choose k) > 0"
nipkow@31952
   164
  apply (induct n rule: induct'_nat) 
nipkow@31719
   165
  apply force
nipkow@31719
   166
  apply clarify
nipkow@31719
   167
  apply (case_tac "k = 0")
nipkow@31719
   168
  apply force
nipkow@31952
   169
  apply (subst choose_reduce_nat)
nipkow@31719
   170
  apply auto
nipkow@31719
   171
done
nipkow@31719
   172
nipkow@31952
   173
lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
nipkow@31719
   174
    ((n::int) choose k) > 0"
nipkow@31952
   175
  by (auto simp add: binomial_int_def choose_pos_nat)
nipkow@31719
   176
nipkow@31719
   177
lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
nipkow@31719
   178
    (ALL n. P (n + 1) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (k + 1) \<longrightarrow>
nipkow@31719
   179
    P (n + 1) (k + 1))) \<longrightarrow> (ALL k <= n. P n k)"
nipkow@31952
   180
  apply (induct n rule: induct'_nat)
nipkow@31719
   181
  apply auto
nipkow@31719
   182
  apply (case_tac "k = 0")
nipkow@31719
   183
  apply auto
nipkow@31719
   184
  apply (case_tac "k = n + 1")
nipkow@31719
   185
  apply auto
nipkow@31719
   186
  apply (drule_tac x = n in spec) back back 
nipkow@31719
   187
  apply (drule_tac x = "k - 1" in spec) back back back
nipkow@31719
   188
  apply auto
nipkow@31719
   189
done
nipkow@31719
   190
nipkow@31952
   191
lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow> 
nipkow@31719
   192
    fact k * fact (n - k) * (n choose k) = fact n"
nipkow@31719
   193
  apply (rule binomial_induct [of _ k n])
nipkow@31719
   194
  apply auto
nipkow@31719
   195
proof -
nipkow@31719
   196
  fix k :: nat and n
nipkow@31719
   197
  assume less: "k < n"
nipkow@31719
   198
  assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
nipkow@31719
   199
  hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
nipkow@31952
   200
    by (subst fact_plus_one_nat, auto)
nipkow@31719
   201
  assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = 
nipkow@31719
   202
      fact n"
nipkow@31719
   203
  with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) * 
nipkow@31719
   204
      (n choose (k + 1)) = (n - k) * fact n"
nipkow@31952
   205
    by (subst (2) fact_plus_one_nat, auto)
nipkow@31719
   206
  with less have two: "fact (k + 1) * fact (n - k) * (n choose (k + 1)) = 
nipkow@31719
   207
      (n - k) * fact n" by simp
nipkow@31719
   208
  have "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) =
nipkow@31719
   209
      fact (k + 1) * fact (n - k) * (n choose (k + 1)) + 
nipkow@31719
   210
      fact (k + 1) * fact (n - k) * (n choose k)" 
nipkow@31952
   211
    by (subst choose_reduce_nat, auto simp add: ring_simps)
nipkow@31719
   212
  also note one
nipkow@31719
   213
  also note two
nipkow@31719
   214
  also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
nipkow@31952
   215
    apply (subst fact_plus_one_nat)
nipkow@31719
   216
    apply (subst left_distrib [symmetric])
nipkow@31719
   217
    apply simp
nipkow@31719
   218
    done
nipkow@31719
   219
  finally show "fact (k + 1) * fact (n - k) * (n + 1 choose (k + 1)) = 
nipkow@31719
   220
    fact (n + 1)" .
nipkow@31719
   221
qed
nipkow@31719
   222
nipkow@31952
   223
lemma choose_altdef_nat: "(k::nat) \<le> n \<Longrightarrow> 
nipkow@31719
   224
    n choose k = fact n div (fact k * fact (n - k))"
nipkow@31952
   225
  apply (frule choose_altdef_aux_nat)
nipkow@31719
   226
  apply (erule subst)
nipkow@31719
   227
  apply (simp add: mult_ac)
nipkow@31719
   228
done
nipkow@31719
   229
nipkow@31719
   230
nipkow@31952
   231
lemma choose_altdef_int: 
nipkow@31719
   232
  assumes "(0::int) <= k" and "k <= n"
nipkow@31719
   233
  shows "n choose k = fact n div (fact k * fact (n - k))"
nipkow@31719
   234
  
nipkow@31719
   235
  apply (subst tsub_eq [symmetric], rule prems)
nipkow@31952
   236
  apply (rule choose_altdef_nat [transferred])
nipkow@31719
   237
  using prems apply auto
nipkow@31719
   238
done
nipkow@31719
   239
nipkow@31952
   240
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
nipkow@31952
   241
  unfolding dvd_def apply (frule choose_altdef_aux_nat)
nipkow@31719
   242
  (* why don't blast and auto get this??? *)
nipkow@31719
   243
  apply (rule exI)
nipkow@31719
   244
  apply (erule sym)
nipkow@31719
   245
done
nipkow@31719
   246
nipkow@31952
   247
lemma choose_dvd_int: 
nipkow@31719
   248
  assumes "(0::int) <= k" and "k <= n"
nipkow@31719
   249
  shows "fact k * fact (n - k) dvd fact n"
nipkow@31719
   250
 
nipkow@31719
   251
  apply (subst tsub_eq [symmetric], rule prems)
nipkow@31952
   252
  apply (rule choose_dvd_nat [transferred])
nipkow@31719
   253
  using prems apply auto
nipkow@31719
   254
done
nipkow@31719
   255
nipkow@31719
   256
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
nipkow@31719
   257
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n = 
nipkow@31719
   258
  (SUM k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
nipkow@31952
   259
proof (induct n rule: induct'_nat)
nipkow@31719
   260
  show "?P 0" by simp
nipkow@31719
   261
next
nipkow@31719
   262
  fix n
nipkow@31719
   263
  assume ih: "?P n"
nipkow@31719
   264
  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
nipkow@31719
   265
    by auto
nipkow@31719
   266
  have decomp2: "{0..n} = {0} Un {1..n}"
nipkow@31719
   267
    by auto
nipkow@31719
   268
  have decomp3: "{1..n+1} = {n+1} Un {1..n}"
nipkow@31719
   269
    by auto
nipkow@31719
   270
  have "(a+b)^(n+1) = 
nipkow@31719
   271
      (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
nipkow@31719
   272
    using ih by (simp add: power_plus_one)
nipkow@31719
   273
  also have "... =  a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
nipkow@31719
   274
                   b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
nipkow@31719
   275
    by (rule distrib)
nipkow@31719
   276
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
nipkow@31719
   277
                  (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
nipkow@31719
   278
    by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
nipkow@31719
   279
  also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
nipkow@31719
   280
                  (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
nipkow@31719
   281
    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le 
nipkow@31719
   282
             power_Suc ring_simps One_nat_def del:setsum_cl_ivl_Suc)
nipkow@31719
   283
  also have "... = a^(n+1) + b^(n+1) +
nipkow@31719
   284
                  (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
nipkow@31719
   285
                  (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
nipkow@31719
   286
    by (simp add: decomp2 decomp3)
nipkow@31719
   287
  also have
nipkow@31719
   288
      "... = a^(n+1) + b^(n+1) + 
nipkow@31719
   289
         (SUM k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
nipkow@31719
   290
    by (auto simp add: ring_simps setsum_addf [symmetric]
nipkow@31952
   291
      choose_reduce_nat)
nipkow@31719
   292
  also have "... = (SUM k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
nipkow@31719
   293
    using decomp by (simp add: ring_simps)
nipkow@31719
   294
  finally show "?P (n + 1)" by simp
nipkow@31719
   295
qed
nipkow@31719
   296
nipkow@31719
   297
lemma set_explicit: "{S. S = T \<and> P S} = (if P T then {T} else {})"
nipkow@31719
   298
  by auto
nipkow@31719
   299
nipkow@31952
   300
lemma card_subsets_nat [rule_format]:
nipkow@31719
   301
  fixes S :: "'a set"
nipkow@31719
   302
  assumes "finite S"
nipkow@31719
   303
  shows "ALL k. card {T. T \<le> S \<and> card T = k} = card S choose k" 
nipkow@31719
   304
      (is "?P S")
nipkow@31719
   305
using `finite S`
nipkow@31719
   306
proof (induct set: finite)
nipkow@31719
   307
  show "?P {}" by (auto simp add: set_explicit)
nipkow@31719
   308
  next fix x :: "'a" and F
nipkow@31719
   309
  assume iassms: "finite F" "x ~: F"
nipkow@31719
   310
  assume ih: "?P F"
nipkow@31719
   311
  show "?P (insert x F)" (is "ALL k. ?Q k")
nipkow@31719
   312
  proof
nipkow@31719
   313
    fix k
nipkow@31719
   314
    show "card {T. T \<subseteq> (insert x F) \<and> card T = k} = 
nipkow@31719
   315
        card (insert x F) choose k" (is "?Q k")
nipkow@31952
   316
    proof (induct k rule: induct'_nat)
nipkow@31719
   317
      from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
nipkow@31719
   318
        apply auto
nipkow@31719
   319
        apply (subst (asm) card_0_eq)
nipkow@31719
   320
        apply (auto elim: finite_subset)
nipkow@31719
   321
        done
nipkow@31719
   322
      thus "?Q 0" 
nipkow@31719
   323
        by auto
nipkow@31719
   324
      next fix k
nipkow@31719
   325
      show "?Q (k + 1)"
nipkow@31719
   326
      proof -
nipkow@31719
   327
        from iassms have fin: "finite (insert x F)" by auto
nipkow@31719
   328
        hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
nipkow@31719
   329
          {T. T \<le> F & card T = k + 1} Un 
nipkow@31719
   330
          {T. T \<le> insert x F & x : T & card T = k + 1}"
nipkow@31719
   331
          by (auto intro!: subsetI)
nipkow@31719
   332
        with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
nipkow@31719
   333
          card ({T. T \<subseteq> F \<and> card T = k + 1}) + 
nipkow@31719
   334
          card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
nipkow@31719
   335
          apply (subst card_Un_disjoint [symmetric])
nipkow@31719
   336
          apply auto
nipkow@31719
   337
          (* note: nice! Didn't have to say anything here *)
nipkow@31719
   338
          done
nipkow@31719
   339
        also from ih have "card ({T. T \<subseteq> F \<and> card T = k + 1}) = 
nipkow@31719
   340
          card F choose (k+1)" by auto
nipkow@31719
   341
        also have "card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}) =
nipkow@31719
   342
          card ({T. T <= F & card T = k})"
nipkow@31719
   343
        proof -
nipkow@31719
   344
          let ?f = "%T. T Un {x}"
nipkow@31719
   345
          from iassms have "inj_on ?f {T. T <= F & card T = k}"
nipkow@31719
   346
            unfolding inj_on_def by (auto intro!: subsetI)
nipkow@31719
   347
          hence "card ({T. T <= F & card T = k}) = 
nipkow@31719
   348
            card(?f ` {T. T <= F & card T = k})"
nipkow@31719
   349
            by (rule card_image [symmetric])
nipkow@31719
   350
          also from iassms fin have "?f ` {T. T <= F & card T = k} = 
nipkow@31719
   351
            {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}"
nipkow@31719
   352
            unfolding image_def 
nipkow@31719
   353
            (* I can't figure out why this next line takes so long *)
nipkow@31719
   354
            apply auto
nipkow@31719
   355
            apply (frule (1) finite_subset, force)
nipkow@31719
   356
            apply (rule_tac x = "xa - {x}" in exI)
nipkow@31719
   357
            apply (subst card_Diff_singleton)
nipkow@31719
   358
            apply (auto elim: finite_subset)
nipkow@31719
   359
            done
nipkow@31719
   360
          finally show ?thesis by (rule sym)
nipkow@31719
   361
        qed
nipkow@31719
   362
        also from ih have "card ({T. T <= F & card T = k}) = card F choose k"
nipkow@31719
   363
          by auto
nipkow@31719
   364
        finally have "card ({T. T \<le> insert x F \<and> card T = k + 1}) = 
nipkow@31719
   365
          card F choose (k + 1) + (card F choose k)".
nipkow@31952
   366
        with iassms choose_plus_one_nat show ?thesis
nipkow@31719
   367
          by auto
nipkow@31719
   368
      qed
nipkow@31719
   369
    qed
nipkow@31719
   370
  qed
nipkow@31719
   371
qed
nipkow@31719
   372
nipkow@31719
   373
end