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