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