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