src/HOL/Number_Theory/Binomial.thy
author wenzelm
Sun Mar 13 22:55:50 2011 +0100 (2011-03-13)
changeset 41959 b460124855b8
parent 41541 1fa4725c4656
child 44872 a98ef45122f3
permissions -rw-r--r--
tuned headers;
     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