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