1.1 --- a/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 22:11:55 2011 +0200
1.2 +++ b/src/HOL/Number_Theory/Binomial.thy Sat Sep 10 23:27:32 2011 +0200
1.3 @@ -20,40 +20,35 @@
1.4 subsection {* Main definitions *}
1.5
1.6 class binomial =
1.7 -
1.8 -fixes
1.9 - binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
1.10 + fixes binomial :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "choose" 65)
1.11
1.12 (* definitions for the natural numbers *)
1.13
1.14 instantiation nat :: binomial
1.15 -
1.16 begin
1.17
1.18 -fun
1.19 - binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.20 +fun binomial_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.21 where
1.22 "binomial_nat n k =
1.23 (if k = 0 then 1 else
1.24 if n = 0 then 0 else
1.25 (binomial (n - 1) k) + (binomial (n - 1) (k - 1)))"
1.26
1.27 -instance proof qed
1.28 +instance ..
1.29
1.30 end
1.31
1.32 (* definitions for the integers *)
1.33
1.34 instantiation int :: binomial
1.35 -
1.36 begin
1.37
1.38 -definition
1.39 - binomial_int :: "int => int \<Rightarrow> int"
1.40 -where
1.41 - "binomial_int n k = (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
1.42 - else 0)"
1.43 -instance proof qed
1.44 +definition binomial_int :: "int => int \<Rightarrow> int" where
1.45 + "binomial_int n k =
1.46 + (if n \<ge> 0 \<and> k \<ge> 0 then int (binomial (nat n) (nat k))
1.47 + else 0)"
1.48 +
1.49 +instance ..
1.50
1.51 end
1.52
1.53 @@ -97,10 +92,11 @@
1.54 by (induct n rule: induct'_nat, auto)
1.55
1.56 lemma zero_choose_int [rule_format,simp]: "(k::int) > n \<Longrightarrow> n choose k = 0"
1.57 - unfolding binomial_int_def apply (case_tac "n < 0")
1.58 + unfolding binomial_int_def
1.59 + apply (cases "n < 0")
1.60 apply force
1.61 apply (simp del: binomial_nat.simps)
1.62 -done
1.63 + done
1.64
1.65 lemma choose_reduce_nat: "(n::nat) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
1.66 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
1.67 @@ -108,10 +104,10 @@
1.68
1.69 lemma choose_reduce_int: "(n::int) > 0 \<Longrightarrow> 0 < k \<Longrightarrow>
1.70 (n choose k) = ((n - 1) choose k) + ((n - 1) choose (k - 1))"
1.71 - unfolding binomial_int_def apply (subst choose_reduce_nat)
1.72 - apply (auto simp del: binomial_nat.simps
1.73 - simp add: nat_diff_distrib)
1.74 -done
1.75 + unfolding binomial_int_def
1.76 + apply (subst choose_reduce_nat)
1.77 + apply (auto simp del: binomial_nat.simps simp add: nat_diff_distrib)
1.78 + done
1.79
1.80 lemma choose_plus_one_nat: "((n::nat) + 1) choose (k + 1) =
1.81 (n choose (k + 1)) + (n choose k)"
1.82 @@ -128,13 +124,13 @@
1.83 declare binomial_nat.simps [simp del]
1.84
1.85 lemma choose_self_nat [simp]: "((n::nat) choose n) = 1"
1.86 - by (induct n rule: induct'_nat, auto simp add: choose_plus_one_nat)
1.87 + by (induct n rule: induct'_nat) (auto simp add: choose_plus_one_nat)
1.88
1.89 lemma choose_self_int [simp]: "n \<ge> 0 \<Longrightarrow> ((n::int) choose n) = 1"
1.90 by (auto simp add: binomial_int_def)
1.91
1.92 lemma choose_one_nat [simp]: "(n::nat) choose 1 = n"
1.93 - by (induct n rule: induct'_nat, auto simp add: choose_reduce_nat)
1.94 + by (induct n rule: induct'_nat) (auto simp add: choose_reduce_nat)
1.95
1.96 lemma choose_one_int [simp]: "n \<ge> 0 \<Longrightarrow> (n::int) choose 1 = n"
1.97 by (auto simp add: binomial_int_def)
1.98 @@ -165,7 +161,7 @@
1.99 apply force
1.100 apply (subst choose_reduce_nat)
1.101 apply auto
1.102 -done
1.103 + done
1.104
1.105 lemma choose_pos_int: "n \<ge> 0 \<Longrightarrow> k >= 0 \<Longrightarrow> k \<le> n \<Longrightarrow>
1.106 ((n::int) choose k) > 0"
1.107 @@ -183,7 +179,7 @@
1.108 apply (drule_tac x = n in spec) back back
1.109 apply (drule_tac x = "k - 1" in spec) back back back
1.110 apply auto
1.111 -done
1.112 + done
1.113
1.114 lemma choose_altdef_aux_nat: "(k::nat) \<le> n \<Longrightarrow>
1.115 fact k * fact (n - k) * (n choose k) = fact n"
1.116 @@ -193,10 +189,9 @@
1.117 fix k :: nat and n
1.118 assume less: "k < n"
1.119 assume ih1: "fact k * fact (n - k) * (n choose k) = fact n"
1.120 - hence one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
1.121 + then have one: "fact (k + 1) * fact (n - k) * (n choose k) = (k + 1) * fact n"
1.122 by (subst fact_plus_one_nat, auto)
1.123 - assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) =
1.124 - fact n"
1.125 + assume ih2: "fact (k + 1) * fact (n - (k + 1)) * (n choose (k + 1)) = fact n"
1.126 with less have "fact (k + 1) * fact ((n - (k + 1)) + 1) *
1.127 (n choose (k + 1)) = (n - k) * fact n"
1.128 by (subst (2) fact_plus_one_nat, auto)
1.129 @@ -222,7 +217,7 @@
1.130 apply (frule choose_altdef_aux_nat)
1.131 apply (erule subst)
1.132 apply (simp add: mult_ac)
1.133 -done
1.134 + done
1.135
1.136
1.137 lemma choose_altdef_int:
1.138 @@ -238,7 +233,7 @@
1.139 (* why don't blast and auto get this??? *)
1.140 apply (rule exI)
1.141 apply (erule sym)
1.142 -done
1.143 + done
1.144
1.145 lemma choose_dvd_int:
1.146 assumes "(0::int) <= k" and "k <= n"
1.147 @@ -293,7 +288,8 @@
1.148 fixes S :: "'a set"
1.149 shows "finite S \<Longrightarrow> card {T. T \<le> S \<and> card T = k} = card S choose k"
1.150 proof (induct arbitrary: k set: finite)
1.151 - case empty show ?case by (auto simp add: Collect_conv_if)
1.152 + case empty
1.153 + show ?case by (auto simp add: Collect_conv_if)
1.154 next
1.155 case (insert x F)
1.156 note iassms = insert(1,2)
1.157 @@ -303,11 +299,11 @@
1.158 case zero
1.159 from iassms have "{T. T \<le> (insert x F) \<and> card T = 0} = {{}}"
1.160 by (auto simp: finite_subset)
1.161 - thus ?case by auto
1.162 + then show ?case by auto
1.163 next
1.164 case (plus1 k)
1.165 from iassms have fin: "finite (insert x F)" by auto
1.166 - hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
1.167 + then have "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
1.168 {T. T \<le> F & card T = k + 1} Un
1.169 {T. T \<le> insert x F & x : T & card T = k + 1}"
1.170 by auto
1.171 @@ -326,14 +322,14 @@
1.172 let ?f = "%T. T Un {x}"
1.173 from iassms have "inj_on ?f {T. T <= F & card T = k}"
1.174 unfolding inj_on_def by auto
1.175 - hence "card ({T. T <= F & card T = k}) =
1.176 + then have "card ({T. T <= F & card T = k}) =
1.177 card(?f ` {T. T <= F & card T = k})"
1.178 by (rule card_image [symmetric])
1.179 also have "?f ` {T. T <= F & card T = k} =
1.180 {T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1}" (is "?L=?R")
1.181 proof-
1.182 { fix S assume "S \<subseteq> F"
1.183 - hence "card(insert x S) = card S +1"
1.184 + then have "card(insert x S) = card S +1"
1.185 using iassms by (auto simp: finite_subset) }
1.186 moreover
1.187 { fix T assume 1: "T \<subseteq> insert x F" "x : T" "card T = k+1"
1.188 @@ -353,5 +349,4 @@
1.189 qed
1.190 qed
1.191
1.192 -
1.193 end