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
     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: ring_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 ring_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: ring_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: ring_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
   368       qed
   369     qed
   370   qed
   371 qed
   372 
   373 end