author paulson Tue Mar 10 16:12:35 2015 +0000 (2015-03-10) changeset 59669 de7792ea4090 parent 59668 1c937d56a70a child 59670 dee043d19729 child 59730 b7c394c7a619
renaming HOL/Fact.thy -> Binomial.thy
 src/HOL/Binomial.thy file | annotate | diff | revisions src/HOL/Fact.thy file | annotate | diff | revisions src/HOL/Import/Import_Setup.thy file | annotate | diff | revisions src/HOL/Library/Permutations.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions src/HOL/ex/Birthday_Paradox.thy file | annotate | diff | revisions
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Binomial.thy	Tue Mar 10 16:12:35 2015 +0000
1.3 @@ -0,0 +1,1180 @@
1.4 +(*  Title       : Binomial.thy
1.5 +    Author      : Jacques D. Fleuriot
1.6 +    Copyright   : 1998  University of Cambridge
1.7 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
1.8 +    The integer version of factorial and other additions by Jeremy Avigad.
1.9 +*)
1.10 +
1.11 +section{*Factorial Function, Binomial Coefficients and Binomial Theorem*}
1.12 +
1.13 +theory Binomial
1.14 +imports Main
1.15 +begin
1.16 +
1.17 +class fact =
1.18 +  fixes fact :: "'a \<Rightarrow> 'a"
1.19 +
1.20 +instantiation nat :: fact
1.21 +begin
1.22 +
1.23 +fun
1.24 +  fact_nat :: "nat \<Rightarrow> nat"
1.25 +where
1.26 +  fact_0_nat: "fact_nat 0 = Suc 0"
1.27 +| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
1.28 +
1.29 +instance ..
1.30 +
1.31 +end
1.32 +
1.33 +(* definitions for the integers *)
1.34 +
1.35 +instantiation int :: fact
1.36 +
1.37 +begin
1.38 +
1.39 +definition
1.40 +  fact_int :: "int \<Rightarrow> int"
1.41 +where
1.42 +  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
1.43 +
1.44 +instance proof qed
1.45 +
1.46 +end
1.47 +
1.48 +
1.49 +subsection {* Set up Transfer *}
1.50 +
1.51 +lemma transfer_nat_int_factorial:
1.52 +  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
1.53 +  unfolding fact_int_def
1.54 +  by auto
1.55 +
1.56 +
1.57 +lemma transfer_nat_int_factorial_closure:
1.58 +  "x >= (0::int) \<Longrightarrow> fact x >= 0"
1.59 +  by (auto simp add: fact_int_def)
1.60 +
1.62 +    transfer_nat_int_factorial transfer_nat_int_factorial_closure]
1.63 +
1.64 +lemma transfer_int_nat_factorial:
1.65 +  "fact (int x) = int (fact x)"
1.66 +  unfolding fact_int_def by auto
1.67 +
1.68 +lemma transfer_int_nat_factorial_closure:
1.69 +  "is_nat x \<Longrightarrow> fact x >= 0"
1.70 +  by (auto simp add: fact_int_def)
1.71 +
1.73 +    transfer_int_nat_factorial transfer_int_nat_factorial_closure]
1.74 +
1.75 +
1.76 +subsection {* Factorial *}
1.77 +
1.78 +lemma fact_0_int [simp]: "fact (0::int) = 1"
1.79 +  by (simp add: fact_int_def)
1.80 +
1.81 +lemma fact_1_nat [simp]: "fact (1::nat) = 1"
1.82 +  by simp
1.83 +
1.84 +lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
1.85 +  by simp
1.86 +
1.87 +lemma fact_1_int [simp]: "fact (1::int) = 1"
1.88 +  by (simp add: fact_int_def)
1.89 +
1.90 +lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
1.91 +  by simp
1.92 +
1.93 +lemma fact_plus_one_int:
1.94 +  assumes "n >= 0"
1.95 +  shows "fact ((n::int) + 1) = (n + 1) * fact n"
1.96 +  using assms unfolding fact_int_def
1.98 +
1.99 +lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.100 +  apply (subgoal_tac "n = Suc (n - 1)")
1.101 +  apply (erule ssubst)
1.102 +  apply (subst fact_Suc)
1.103 +  apply simp_all
1.104 +  done
1.105 +
1.106 +lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.107 +  apply (subgoal_tac "n = (n - 1) + 1")
1.108 +  apply (erule ssubst)
1.109 +  apply (subst fact_plus_one_int)
1.110 +  apply simp_all
1.111 +  done
1.112 +
1.113 +lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
1.114 +  apply (induct n)
1.115 +  apply (auto simp add: fact_plus_one_nat)
1.116 +  done
1.117 +
1.118 +lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
1.119 +  by (simp add: fact_int_def)
1.120 +
1.121 +lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
1.122 +  by (insert fact_nonzero_nat [of n], arith)
1.123 +
1.124 +lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
1.125 +  by (auto simp add: fact_int_def)
1.126 +
1.127 +lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
1.128 +  by (insert fact_nonzero_nat [of n], arith)
1.129 +
1.130 +lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
1.131 +  by (insert fact_nonzero_nat [of n], arith)
1.132 +
1.133 +lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
1.134 +  apply (auto simp add: fact_int_def)
1.135 +  apply (subgoal_tac "1 = int 1")
1.136 +  apply (erule ssubst)
1.137 +  apply (subst zle_int)
1.138 +  apply auto
1.139 +  done
1.140 +
1.141 +lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.142 +  apply (induct n)
1.143 +  apply force
1.144 +  apply (auto simp only: fact_Suc)
1.145 +  apply (subgoal_tac "m = Suc n")
1.146 +  apply (erule ssubst)
1.147 +  apply (rule dvd_triv_left)
1.148 +  apply auto
1.149 +  done
1.150 +
1.151 +lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
1.152 +  apply (case_tac "1 <= n")
1.153 +  apply (induct n rule: int_ge_induct)
1.154 +  apply (auto simp add: fact_plus_one_int)
1.155 +  apply (subgoal_tac "m = i + 1")
1.156 +  apply auto
1.157 +  done
1.158 +
1.159 +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
1.160 +  {i..j+1} = {i..j} Un {j+1}"
1.161 +  by auto
1.162 +
1.163 +lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
1.164 +  by auto
1.165 +
1.166 +lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
1.167 +  by auto
1.168 +
1.169 +lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
1.170 +  apply (induct n)
1.171 +  apply force
1.172 +  apply (subst fact_Suc)
1.173 +  apply (subst interval_Suc)
1.174 +  apply auto
1.175 +done
1.176 +
1.177 +lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
1.178 +  apply (induct n rule: int_ge_induct)
1.179 +  apply force
1.180 +  apply (subst fact_plus_one_int, assumption)
1.181 +  apply (subst interval_plus_one_int)
1.182 +  apply auto
1.183 +done
1.184 +
1.185 +lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
1.186 +  by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
1.187 +
1.188 +lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
1.189 +  by (auto simp add: dvd_imp_mod_0 fact_dvd)
1.190 +
1.191 +lemma fact_div_fact:
1.192 +  assumes "m \<ge> (n :: nat)"
1.193 +  shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
1.194 +proof -
1.195 +  obtain d where "d = m - n" by auto
1.196 +  from assms this have "m = n + d" by auto
1.197 +  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
1.198 +  proof (induct d)
1.199 +    case 0
1.200 +    show ?case by simp
1.201 +  next
1.202 +    case (Suc d')
1.203 +    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
1.204 +      by simp
1.205 +    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
1.206 +      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
1.207 +    also have "... = \<Prod>{n + 1..n + Suc d'}"
1.208 +      by (simp add: atLeastAtMostSuc_conv setprod.insert)
1.209 +    finally show ?case .
1.210 +  qed
1.211 +  from this `m = n + d` show ?thesis by simp
1.212 +qed
1.213 +
1.214 +lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
1.215 +apply (drule le_imp_less_or_eq)
1.217 +apply (induct_tac k, auto)
1.218 +done
1.219 +
1.220 +lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
1.221 +  unfolding fact_int_def by auto
1.222 +
1.223 +lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
1.224 +  apply (case_tac "m >= 0")
1.225 +  apply auto
1.226 +  apply (frule fact_gt_zero_int)
1.227 +  apply arith
1.228 +done
1.229 +
1.230 +lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
1.231 +    fact (m + k) >= fact m"
1.232 +  apply (case_tac "m < 0")
1.233 +  apply auto
1.234 +  apply (induct k rule: int_ge_induct)
1.235 +  apply auto
1.236 +  apply (subst add.assoc [symmetric])
1.237 +  apply (subst fact_plus_one_int)
1.238 +  apply auto
1.239 +  apply (erule order_trans)
1.240 +  apply (subst mult_le_cancel_right1)
1.241 +  apply (subgoal_tac "fact (m + i) >= 0")
1.242 +  apply arith
1.243 +  apply auto
1.244 +done
1.245 +
1.246 +lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
1.247 +  apply (insert fact_mono_int_aux [of "n - m" "m"])
1.248 +  apply auto
1.249 +done
1.250 +
1.251 +text{*Note that @{term "fact 0 = fact 1"}*}
1.252 +lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
1.253 +apply (drule_tac m = m in less_imp_Suc_add, auto)
1.254 +apply (induct_tac k, auto)
1.255 +done
1.256 +
1.257 +lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
1.258 +    fact m < fact ((m + 1) + k)"
1.259 +  apply (induct k rule: int_ge_induct)
1.260 +  apply (simp add: fact_plus_one_int)
1.261 +  apply (subst (2) fact_reduce_int)
1.262 +  apply (auto simp add: ac_simps)
1.263 +  apply (erule order_less_le_trans)
1.264 +  apply auto
1.265 +  done
1.266 +
1.267 +lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
1.268 +  apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
1.269 +  apply auto
1.270 +done
1.271 +
1.272 +lemma fact_num_eq_if_nat: "fact (m::nat) =
1.273 +  (if m=0 then 1 else m * fact (m - 1))"
1.274 +by (cases m) auto
1.275 +
1.277 +  "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
1.278 +by (cases "m + n") auto
1.279 +
1.281 +  "fact ((m::nat) + n) =
1.282 +    (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
1.283 +by (cases m) auto
1.284 +
1.285 +lemma fact_le_power: "fact n \<le> n^n"
1.286 +proof (induct n)
1.287 +  case (Suc n)
1.288 +  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
1.290 +qed simp
1.291 +
1.292 +subsection {* @{term fact} and @{term of_nat} *}
1.293 +
1.294 +lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
1.295 +by auto
1.296 +
1.297 +lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
1.298 +
1.299 +lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
1.300 +by simp
1.301 +
1.302 +lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
1.303 +by (auto simp add: positive_imp_inverse_positive)
1.304 +
1.305 +lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
1.306 +by (auto intro: order_less_imp_le)
1.307 +
1.308 +lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
1.309 +  unfolding fact_altdef_nat
1.310 +  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
1.311 +
1.312 +lemma fact_div_fact_le_pow:
1.313 +  assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
1.314 +proof -
1.315 +  have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
1.316 +    by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
1.317 +  with assms show ?thesis
1.318 +    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
1.319 +qed
1.320 +
1.321 +lemma fact_numeral:  --{*Evaluation for specific numerals*}
1.322 +  "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
1.323 +  by (simp add: numeral_eq_Suc)
1.324 +
1.325 +
1.326 +text {* This development is based on the work of Andy Gordon and
1.327 +  Florian Kammueller. *}
1.328 +
1.329 +subsection {* Basic definitions and lemmas *}
1.330 +
1.331 +primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
1.332 +where
1.333 +  "0 choose k = (if k = 0 then 1 else 0)"
1.334 +| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
1.335 +
1.336 +lemma binomial_n_0 [simp]: "(n choose 0) = 1"
1.337 +  by (cases n) simp_all
1.338 +
1.339 +lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
1.340 +  by simp
1.341 +
1.342 +lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
1.343 +  by simp
1.344 +
1.345 +lemma choose_reduce_nat:
1.346 +  "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>
1.347 +    (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
1.348 +  by (metis Suc_diff_1 binomial.simps(2) neq0_conv)
1.349 +
1.350 +lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"
1.351 +  by (induct n arbitrary: k) auto
1.352 +
1.353 +declare binomial.simps [simp del]
1.354 +
1.355 +lemma binomial_n_n [simp]: "n choose n = 1"
1.356 +  by (induct n) (simp_all add: binomial_eq_0)
1.357 +
1.358 +lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"
1.359 +  by (induct n) simp_all
1.360 +
1.361 +lemma binomial_1 [simp]: "n choose Suc 0 = n"
1.362 +  by (induct n) simp_all
1.363 +
1.364 +lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"
1.365 +  by (induct n k rule: diff_induct) simp_all
1.366 +
1.367 +lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k"
1.368 +  by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)
1.369 +
1.370 +lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n"
1.371 +  by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)
1.372 +
1.373 +lemma Suc_times_binomial_eq:
1.374 +  "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
1.375 +  apply (induct n arbitrary: k, simp add: binomial.simps)
1.376 +  apply (case_tac k)
1.378 +  done
1.379 +
1.380 +text{*The absorption property*}
1.381 +lemma Suc_times_binomial:
1.382 +  "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
1.383 +  using Suc_times_binomial_eq by auto
1.384 +
1.385 +text{*This is the well-known version of absorption, but it's harder to use because of the
1.386 +  need to reason about division.*}
1.387 +lemma binomial_Suc_Suc_eq_times:
1.388 +    "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
1.389 +  by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
1.390 +
1.391 +text{*Another version of absorption, with -1 instead of Suc.*}
1.392 +lemma times_binomial_minus1_eq:
1.393 +  "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
1.394 +  using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
1.395 +  by (auto split add: nat_diff_split)
1.396 +
1.397 +
1.398 +subsection {* Combinatorial theorems involving @{text "choose"} *}
1.399 +
1.400 +text {*By Florian Kamm\"uller, tidied by LCP.*}
1.401 +
1.402 +lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1"
1.404 +
1.405 +lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow>
1.406 +    {s. s \<subseteq> insert x M \<and> card s = Suc k} =
1.407 +    {s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}"
1.408 +  apply safe
1.409 +     apply (auto intro: finite_subset [THEN card_insert_disjoint])
1.410 +  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if
1.411 +     card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)
1.412 +
1.413 +lemma finite_bex_subset [simp]:
1.414 +  assumes "finite B"
1.415 +    and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
1.416 +  shows "finite {x. \<exists>A \<subseteq> B. P x A}"
1.417 +  by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)
1.418 +
1.419 +text{*There are as many subsets of @{term A} having cardinality @{term k}
1.420 + as there are sets obtained from the former by inserting a fixed element
1.421 + @{term x} into each.*}
1.422 +lemma constr_bij:
1.423 +   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow>
1.424 +    card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} =
1.425 +    card {B. B \<subseteq> A & card(B) = k}"
1.426 +  apply (rule card_bij_eq [where f = "\<lambda>s. s - {x}" and g = "insert x"])
1.427 +  apply (auto elim!: equalityE simp add: inj_on_def)
1.428 +  apply (metis card_Diff_singleton_if finite_subset in_mono)
1.429 +  done
1.430 +
1.431 +text {*
1.432 +  Main theorem: combinatorial statement about number of subsets of a set.
1.433 +*}
1.434 +
1.435 +theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)"
1.436 +proof (induct k arbitrary: A)
1.437 +  case 0 then show ?case by (simp add: card_s_0_eq_empty)
1.438 +next
1.439 +  case (Suc k)
1.440 +  show ?case using `finite A`
1.441 +  proof (induct A)
1.442 +    case empty show ?case by (simp add: card_s_0_eq_empty)
1.443 +  next
1.444 +    case (insert x A)
1.445 +    then show ?case using Suc.hyps
1.446 +      apply (simp add: card_s_0_eq_empty choose_deconstruct)
1.447 +      apply (subst card_Un_disjoint)
1.448 +         prefer 4 apply (force simp add: constr_bij)
1.449 +        prefer 3 apply force
1.450 +       prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
1.451 +         finite_subset [of _ "Pow (insert x F)" for F])
1.452 +      apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
1.453 +      done
1.454 +  qed
1.455 +qed
1.456 +
1.457 +
1.458 +subsection {* The binomial theorem (courtesy of Tobias Nipkow): *}
1.459 +
1.460 +text{* Avigad's version, generalized to any commutative ring *}
1.461 +theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n =
1.462 +  (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
1.463 +proof (induct n)
1.464 +  case 0 then show "?P 0" by simp
1.465 +next
1.466 +  case (Suc n)
1.467 +  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
1.468 +    by auto
1.469 +  have decomp2: "{0..n} = {0} Un {1..n}"
1.470 +    by auto
1.471 +  have "(a+b)^(n+1) =
1.472 +      (a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
1.473 +    using Suc.hyps by simp
1.474 +  also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
1.475 +                   b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
1.476 +    by (rule distrib_right)
1.477 +  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
1.478 +                  (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
1.479 +    by (auto simp add: setsum_right_distrib ac_simps)
1.480 +  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
1.481 +                  (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
1.482 +    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps
1.483 +        del:setsum_cl_ivl_Suc)
1.484 +  also have "\<dots> = a^(n+1) + b^(n+1) +
1.485 +                  (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
1.486 +                  (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
1.487 +    by (simp add: decomp2)
1.488 +  also have
1.489 +      "\<dots> = a^(n+1) + b^(n+1) +
1.490 +            (\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
1.491 +    by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat)
1.492 +  also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
1.493 +    using decomp by (simp add: field_simps)
1.494 +  finally show "?P (Suc n)" by simp
1.495 +qed
1.496 +
1.497 +text{* Original version for the naturals *}
1.498 +corollary binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
1.499 +    using binomial_ring [of "int a" "int b" n]
1.500 +  by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]
1.501 +           of_nat_setsum [symmetric]
1.502 +           of_nat_eq_iff of_nat_id)
1.503 +
1.504 +lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
1.505 +proof (induct n arbitrary: k rule: nat_less_induct)
1.506 +  fix n k assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m - x) * (m choose x) =
1.507 +                      fact m" and kn: "k \<le> n"
1.508 +  let ?ths = "fact k * fact (n - k) * (n choose k) = fact n"
1.509 +  { assume "n=0" then have ?ths using kn by simp }
1.510 +  moreover
1.511 +  { assume "k=0" then have ?ths using kn by simp }
1.512 +  moreover
1.513 +  { assume nk: "n=k" then have ?ths by simp }
1.514 +  moreover
1.515 +  { fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m"
1.516 +    from n have mn: "m < n" by arith
1.517 +    from hm have hm': "h \<le> m" by arith
1.518 +    from hm h n kn have km: "k \<le> m" by arith
1.519 +    have "m - h = Suc (m - Suc h)" using  h km hm by arith
1.520 +    with km h have th0: "fact (m - h) = (m - h) * fact (m - k)"
1.521 +      by simp
1.522 +    from n h th0
1.523 +    have "fact k * fact (n - k) * (n choose k) =
1.524 +        k * (fact h * fact (m - h) * (m choose h)) +
1.525 +        (m - h) * (fact k * fact (m - k) * (m choose k))"
1.526 +      by (simp add: field_simps)
1.527 +    also have "\<dots> = (k + (m - h)) * fact m"
1.528 +      using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
1.529 +      by (simp add: field_simps)
1.530 +    finally have ?ths using h n km by simp }
1.531 +  moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)"
1.532 +    using kn by presburger
1.533 +  ultimately show ?ths by blast
1.534 +qed
1.535 +
1.536 +lemma binomial_fact:
1.537 +  assumes kn: "k \<le> n"
1.538 +  shows "(of_nat (n choose k) :: 'a::{field,ring_char_0}) =
1.539 +    of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
1.540 +  using binomial_fact_lemma[OF kn]
1.541 +  by (simp add: field_simps of_nat_mult [symmetric])
1.542 +
1.543 +lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
1.544 +  using binomial [of 1 "1" n]
1.545 +  by (simp add: numeral_2_eq_2)
1.546 +
1.547 +lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
1.548 +  by (induct n) auto
1.549 +
1.550 +lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
1.551 +  by (induct n) auto
1.552 +
1.553 +lemma natsum_reverse_index:
1.554 +  fixes m::nat
1.555 +  shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
1.556 +  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
1.557 +
1.558 +text{*NW diagonal sum property*}
1.559 +lemma sum_choose_diagonal:
1.560 +  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
1.561 +proof -
1.562 +  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
1.563 +    by (rule natsum_reverse_index) (simp add: assms)
1.564 +  also have "... = Suc (n-m+m) choose m"
1.565 +    by (rule sum_choose_lower)
1.566 +  also have "... = Suc n choose m" using assms
1.567 +    by simp
1.568 +  finally show ?thesis .
1.569 +qed
1.570 +
1.571 +subsection{* Pochhammer's symbol : generalized rising factorial *}
1.572 +
1.573 +text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
1.574 +
1.575 +definition "pochhammer (a::'a::comm_semiring_1) n =
1.576 +  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
1.577 +
1.578 +lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
1.579 +  by (simp add: pochhammer_def)
1.580 +
1.581 +lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
1.582 +  by (simp add: pochhammer_def)
1.583 +
1.584 +lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
1.585 +  by (simp add: pochhammer_def)
1.586 +
1.587 +lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
1.588 +  by (simp add: pochhammer_def)
1.589 +
1.590 +lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
1.591 +proof -
1.592 +  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
1.593 +  then show ?thesis by (simp add: field_simps)
1.594 +qed
1.595 +
1.596 +lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
1.597 +proof -
1.598 +  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
1.599 +  then show ?thesis by simp
1.600 +qed
1.601 +
1.602 +
1.603 +lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
1.604 +proof (cases n)
1.605 +  case 0
1.606 +  then show ?thesis by simp
1.607 +next
1.608 +  case (Suc n)
1.609 +  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
1.610 +qed
1.611 +
1.612 +lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
1.613 +proof (cases "n = 0")
1.614 +  case True
1.615 +  then show ?thesis by (simp add: pochhammer_Suc_setprod)
1.616 +next
1.617 +  case False
1.618 +  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
1.619 +  have eq: "insert 0 {1 .. n} = {0..n}" by auto
1.620 +  have **: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
1.621 +    apply (rule setprod.reindex_cong [where l = Suc])
1.622 +    using False
1.623 +    apply (auto simp add: fun_eq_iff field_simps)
1.624 +    done
1.625 +  show ?thesis
1.626 +    apply (simp add: pochhammer_def)
1.627 +    unfolding setprod.insert [OF *, unfolded eq]
1.628 +    using ** apply (simp add: field_simps)
1.629 +    done
1.630 +qed
1.631 +
1.632 +lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
1.633 +  unfolding fact_altdef_nat
1.634 +  apply (cases n)
1.635 +   apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
1.636 +  apply (rule setprod.reindex_cong [where l = Suc])
1.637 +    apply (auto simp add: fun_eq_iff)
1.638 +  done
1.639 +
1.640 +lemma pochhammer_of_nat_eq_0_lemma:
1.641 +  assumes "k > n"
1.642 +  shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
1.643 +proof (cases "n = 0")
1.644 +  case True
1.645 +  then show ?thesis
1.646 +    using assms by (cases k) (simp_all add: pochhammer_rec)
1.647 +next
1.648 +  case False
1.649 +  from assms obtain h where "k = Suc h" by (cases k) auto
1.650 +  then show ?thesis
1.651 +    by (simp add: pochhammer_Suc_setprod)
1.652 +       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
1.653 +qed
1.654 +
1.655 +lemma pochhammer_of_nat_eq_0_lemma':
1.656 +  assumes kn: "k \<le> n"
1.657 +  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0"
1.658 +proof (cases k)
1.659 +  case 0
1.660 +  then show ?thesis by simp
1.661 +next
1.662 +  case (Suc h)
1.663 +  then show ?thesis
1.664 +    apply (simp add: pochhammer_Suc_setprod)
1.665 +    using Suc kn apply (auto simp add: algebra_simps)
1.666 +    done
1.667 +qed
1.668 +
1.669 +lemma pochhammer_of_nat_eq_0_iff:
1.670 +  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
1.671 +  (is "?l = ?r")
1.672 +  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
1.673 +    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
1.674 +  by (auto simp add: not_le[symmetric])
1.675 +
1.676 +lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
1.677 +  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
1.678 +  apply (cases n)
1.680 +  apply (metis leD not_less_eq)
1.681 +  done
1.682 +
1.683 +lemma pochhammer_eq_0_mono:
1.684 +  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
1.685 +  unfolding pochhammer_eq_0_iff by auto
1.686 +
1.687 +lemma pochhammer_neq_0_mono:
1.688 +  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
1.689 +  unfolding pochhammer_eq_0_iff by auto
1.690 +
1.691 +lemma pochhammer_minus:
1.692 +  assumes kn: "k \<le> n"
1.693 +  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
1.694 +proof (cases k)
1.695 +  case 0
1.696 +  then show ?thesis by simp
1.697 +next
1.698 +  case (Suc h)
1.699 +  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
1.700 +    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
1.701 +    by auto
1.702 +  show ?thesis
1.703 +    unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
1.704 +    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
1.705 +       (auto simp: of_nat_diff)
1.706 +qed
1.707 +
1.708 +lemma pochhammer_minus':
1.709 +  assumes kn: "k \<le> n"
1.710 +  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
1.711 +  unfolding pochhammer_minus[OF kn, where b=b]
1.712 +  unfolding mult.assoc[symmetric]
1.714 +  by simp
1.715 +
1.716 +lemma pochhammer_same: "pochhammer (- of_nat n) n =
1.717 +    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
1.718 +  unfolding pochhammer_minus[OF le_refl[of n]]
1.719 +  by (simp add: of_nat_diff pochhammer_fact)
1.720 +
1.721 +
1.722 +subsection{* Generalized binomial coefficients *}
1.723 +
1.724 +definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
1.725 +  where "a gchoose n =
1.726 +    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
1.727 +
1.728 +lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
1.729 +  apply (simp_all add: gbinomial_def)
1.730 +  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
1.731 +   apply (simp del:setprod_zero_iff)
1.732 +  apply simp
1.733 +  done
1.734 +
1.735 +lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
1.736 +proof (cases "n = 0")
1.737 +  case True
1.738 +  then show ?thesis by simp
1.739 +next
1.740 +  case False
1.741 +  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
1.742 +  have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
1.743 +    by auto
1.744 +  from False show ?thesis
1.745 +    by (simp add: pochhammer_def gbinomial_def field_simps
1.746 +      eq setprod.distrib[symmetric])
1.747 +qed
1.748 +
1.749 +lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
1.750 +proof -
1.751 +  { assume kn: "k > n"
1.752 +    then have ?thesis
1.753 +      by (subst binomial_eq_0[OF kn])
1.754 +         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
1.755 +  moreover
1.756 +  { assume "k=0" then have ?thesis by simp }
1.757 +  moreover
1.758 +  { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
1.759 +    from k0 obtain h where h: "k = Suc h" by (cases k) auto
1.760 +    from h
1.761 +    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
1.762 +      by (subst setprod_constant) auto
1.763 +    have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
1.764 +        using h kn
1.765 +      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
1.766 +         (auto simp: of_nat_diff)
1.767 +    have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
1.768 +        "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
1.769 +        eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
1.770 +      using h kn by auto
1.771 +    from eq[symmetric]
1.772 +    have ?thesis using kn
1.773 +      apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
1.774 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
1.775 +      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
1.776 +        of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
1.777 +      unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
1.778 +      unfolding mult.assoc[symmetric]
1.779 +      unfolding setprod.distrib[symmetric]
1.780 +      apply simp
1.781 +      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
1.782 +      apply (auto simp: of_nat_diff)
1.783 +      done
1.784 +  }
1.785 +  moreover
1.786 +  have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith
1.787 +  ultimately show ?thesis by blast
1.788 +qed
1.789 +
1.790 +lemma gbinomial_1[simp]: "a gchoose 1 = a"
1.791 +  by (simp add: gbinomial_def)
1.792 +
1.793 +lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
1.794 +  by (simp add: gbinomial_def)
1.795 +
1.796 +lemma gbinomial_mult_1:
1.797 +  "a * (a gchoose n) =
1.798 +    of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")
1.799 +proof -
1.800 +  have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
1.801 +    unfolding gbinomial_pochhammer
1.802 +      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
1.803 +    by (simp add:  field_simps del: of_nat_Suc)
1.804 +  also have "\<dots> = ?l" unfolding gbinomial_pochhammer
1.805 +    by (simp add: field_simps)
1.806 +  finally show ?thesis ..
1.807 +qed
1.808 +
1.809 +lemma gbinomial_mult_1':
1.810 +    "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
1.811 +  by (simp add: mult.commute gbinomial_mult_1)
1.812 +
1.813 +lemma gbinomial_Suc:
1.814 +    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
1.815 +  by (simp add: gbinomial_def)
1.816 +
1.817 +lemma gbinomial_mult_fact:
1.818 +  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
1.819 +    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
1.820 +  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
1.821 +
1.822 +lemma gbinomial_mult_fact':
1.823 +  "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
1.824 +    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
1.825 +  using gbinomial_mult_fact[of k a]
1.826 +  by (subst mult.commute)
1.827 +
1.828 +
1.829 +lemma gbinomial_Suc_Suc:
1.830 +  "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
1.831 +proof (cases k)
1.832 +  case 0
1.833 +  then show ?thesis by simp
1.834 +next
1.835 +  case (Suc h)
1.836 +  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
1.837 +    apply (rule setprod.reindex_cong [where l = Suc])
1.838 +      using Suc
1.839 +      apply auto
1.840 +    done
1.841 +  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
1.842 +    ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
1.843 +    apply (simp add: Suc field_simps del: fact_Suc)
1.844 +    unfolding gbinomial_mult_fact'
1.845 +    apply (subst fact_Suc)
1.846 +    unfolding of_nat_mult
1.847 +    apply (subst mult.commute)
1.848 +    unfolding mult.assoc
1.849 +    unfolding gbinomial_mult_fact
1.850 +    apply (simp add: field_simps)
1.851 +    done
1.852 +  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
1.853 +    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
1.854 +    by (simp add: field_simps Suc)
1.855 +  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
1.856 +    using eq0
1.857 +    by (simp add: Suc setprod_nat_ivl_1_Suc)
1.858 +  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
1.859 +    unfolding gbinomial_mult_fact ..
1.860 +  finally show ?thesis by (simp del: fact_Suc)
1.861 +qed
1.862 +
1.863 +lemma gbinomial_reduce_nat:
1.864 +  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
1.865 +by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
1.866 +
1.867 +
1.868 +lemma binomial_symmetric:
1.869 +  assumes kn: "k \<le> n"
1.870 +  shows "n choose k = n choose (n - k)"
1.871 +proof-
1.872 +  from kn have kn': "n - k \<le> n" by arith
1.873 +  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
1.874 +  have "fact k * fact (n - k) * (n choose k) =
1.875 +    fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
1.876 +  then show ?thesis using kn by simp
1.877 +qed
1.878 +
1.879 +text{*Contributed by Manuel Eberl, generalised by LCP.
1.880 +  Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
1.881 +lemma gbinomial_altdef_of_nat:
1.882 +  fixes k :: nat
1.883 +    and x :: "'a :: {field_char_0,field_inverse_zero}"
1.884 +  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
1.885 +proof -
1.886 +  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
1.887 +    unfolding gbinomial_def
1.888 +    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
1.889 +  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
1.890 +    unfolding fact_eq_rev_setprod_nat of_nat_setprod
1.891 +    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
1.892 +  finally show ?thesis .
1.893 +qed
1.894 +
1.895 +lemma gbinomial_ge_n_over_k_pow_k:
1.896 +  fixes k :: nat
1.897 +    and x :: "'a :: linordered_field_inverse_zero"
1.898 +  assumes "of_nat k \<le> x"
1.899 +  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
1.900 +proof -
1.901 +  have x: "0 \<le> x"
1.902 +    using assms of_nat_0_le_iff order_trans by blast
1.903 +  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
1.904 +    by (simp add: setprod_constant)
1.905 +  also have "\<dots> \<le> x gchoose k"
1.906 +    unfolding gbinomial_altdef_of_nat
1.907 +  proof (safe intro!: setprod_mono)
1.908 +    fix i :: nat
1.909 +    assume ik: "i < k"
1.910 +    from assms have "x * of_nat i \<ge> of_nat (i * k)"
1.911 +      by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
1.912 +    then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith
1.913 +    then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
1.914 +      using ik
1.915 +      by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)
1.916 +    then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
1.917 +      unfolding of_nat_mult[symmetric] of_nat_le_iff .
1.918 +    with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"
1.919 +      using `i < k` by (simp add: field_simps)
1.920 +  qed (simp add: x zero_le_divide_iff)
1.921 +  finally show ?thesis .
1.922 +qed
1.923 +
1.924 +text{*Versions of the theorems above for the natural-number version of "choose"*}
1.925 +lemma binomial_altdef_of_nat:
1.926 +  fixes n k :: nat
1.927 +    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
1.928 +  assumes "k \<le> n"
1.929 +  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
1.930 +using assms
1.931 +by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
1.932 +
1.933 +lemma binomial_ge_n_over_k_pow_k:
1.934 +  fixes k n :: nat
1.935 +    and x :: "'a :: linordered_field_inverse_zero"
1.936 +  assumes "k \<le> n"
1.937 +  shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
1.938 +by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
1.939 +
1.940 +lemma binomial_le_pow:
1.941 +  assumes "r \<le> n"
1.942 +  shows "n choose r \<le> n ^ r"
1.943 +proof -
1.944 +  have "n choose r \<le> fact n div fact (n - r)"
1.945 +    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
1.946 +  with fact_div_fact_le_pow [OF assms] show ?thesis by auto
1.947 +qed
1.948 +
1.949 +lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
1.950 +    n choose k = fact n div (fact k * fact (n - k))"
1.951 + by (subst binomial_fact_lemma [symmetric]) auto
1.952 +
1.953 +lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
1.954 +by (metis binomial_fact_lemma dvd_def)
1.955 +
1.956 +lemma choose_dvd_int:
1.957 +  assumes "(0::int) <= k" and "k <= n"
1.958 +  shows "fact k * fact (n - k) dvd fact n"
1.959 +  apply (subst tsub_eq [symmetric], rule assms)
1.960 +  apply (rule choose_dvd_nat [transferred])
1.961 +  using assms apply auto
1.962 +  done
1.963 +
1.964 +lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
1.966 +
1.967 +lemma choose_mult_lemma:
1.968 +     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
1.969 +proof -
1.970 +  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
1.971 +        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
1.972 +    by (simp add: assms binomial_altdef_nat)
1.973 +  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
1.974 +    apply (subst div_mult_div_if_dvd)
1.975 +    apply (auto simp: fact_fact_dvd_fact)
1.977 +    done
1.978 +  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
1.979 +    apply (subst div_mult_div_if_dvd [symmetric])
1.980 +    apply (auto simp: fact_fact_dvd_fact)
1.981 +    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
1.982 +    done
1.983 +  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
1.984 +    apply (subst div_mult_div_if_dvd)
1.985 +    apply (auto simp: fact_fact_dvd_fact)
1.986 +    apply(metis mult.left_commute)
1.987 +    done
1.988 +  finally show ?thesis
1.989 +    by (simp add: binomial_altdef_nat mult.commute)
1.990 +qed
1.991 +
1.992 +text{*The "Subset of a Subset" identity*}
1.993 +lemma choose_mult:
1.994 +  assumes "k\<le>m" "m\<le>n"
1.995 +    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
1.996 +using assms choose_mult_lemma [of "m-k" "n-m" k]
1.997 +by simp
1.998 +
1.999 +
1.1000 +subsection {* Binomial coefficients *}
1.1001 +
1.1002 +lemma choose_one: "(n::nat) choose 1 = n"
1.1003 +  by simp
1.1004 +
1.1005 +(*FIXME: messy and apparently unused*)
1.1006 +lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
1.1007 +    (ALL n. P (Suc n) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow>
1.1008 +    P (Suc n) (Suc k))) \<longrightarrow> (ALL k <= n. P n k)"
1.1009 +  apply (induct n)
1.1010 +  apply auto
1.1011 +  apply (case_tac "k = 0")
1.1012 +  apply auto
1.1013 +  apply (case_tac "k = Suc n")
1.1014 +  apply auto
1.1015 +  apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
1.1016 +  done
1.1017 +
1.1018 +lemma card_UNION:
1.1019 +  assumes "finite A" and "\<forall>k \<in> A. finite k"
1.1020 +  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
1.1021 +  (is "?lhs = ?rhs")
1.1022 +proof -
1.1023 +  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
1.1024 +  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
1.1025 +    by(subst setsum_right_distrib) simp
1.1026 +  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
1.1027 +    using assms by(subst setsum.Sigma)(auto)
1.1028 +  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
1.1029 +    by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
1.1030 +  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
1.1031 +    using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
1.1032 +  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
1.1033 +    using assms by(subst setsum.Sigma) auto
1.1034 +  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
1.1035 +  proof(rule setsum.cong[OF refl])
1.1036 +    fix x
1.1037 +    assume x: "x \<in> \<Union>A"
1.1038 +    def K \<equiv> "{X \<in> A. x \<in> X}"
1.1039 +    with `finite A` have K: "finite K" by auto
1.1040 +    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
1.1041 +    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
1.1042 +      using assms by(auto intro!: inj_onI)
1.1043 +    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
1.1044 +      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
1.1045 +        simp add: card_gt_0_iff[folded Suc_le_eq]
1.1046 +        dest: finite_subset intro: card_mono)
1.1047 +    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
1.1048 +      by (rule setsum.reindex_cong [where l = snd]) fastforce
1.1049 +    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
1.1050 +      using assms by(subst setsum.Sigma) auto
1.1051 +    also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
1.1052 +      by(subst setsum_right_distrib) simp
1.1053 +    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
1.1054 +    proof(rule setsum.mono_neutral_cong_right[rule_format])
1.1055 +      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
1.1056 +        by(auto simp add: K_def intro: card_mono)
1.1057 +    next
1.1058 +      fix i
1.1059 +      assume "i \<in> {1..card A} - {1..card K}"
1.1060 +      hence i: "i \<le> card A" "card K < i" by auto
1.1061 +      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
1.1062 +        by(auto simp add: K_def)
1.1063 +      also have "\<dots> = {}" using `finite A` i
1.1064 +        by(auto simp add: K_def dest: card_mono[rotated 1])
1.1065 +      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
1.1066 +        by(simp only:) simp
1.1067 +    next
1.1068 +      fix i
1.1069 +      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
1.1070 +        (is "?lhs = ?rhs")
1.1071 +        by(rule setsum.cong)(auto simp add: K_def)
1.1072 +      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
1.1073 +    qed simp
1.1074 +    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
1.1075 +      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
1.1076 +    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
1.1077 +      by(subst (2) setsum_head_Suc)(simp_all )
1.1078 +    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
1.1079 +      using K by(subst n_subsets[symmetric]) simp_all
1.1080 +    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
1.1081 +      by(subst setsum_right_distrib[symmetric]) simp
1.1082 +    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
1.1083 +      by(subst binomial_ring)(simp add: ac_simps)
1.1084 +    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
1.1085 +    finally show "?lhs x = 1" .
1.1086 +  qed
1.1087 +  also have "nat \<dots> = card (\<Union>A)" by simp
1.1088 +  finally show ?thesis ..
1.1089 +qed
1.1090 +
1.1091 +text{* The number of nat lists of length @{text m} summing to @{text N} is
1.1092 +@{term "(N + m - 1) choose N"}: *}
1.1093 +
1.1094 +lemma card_length_listsum_rec:
1.1095 +  assumes "m\<ge>1"
1.1096 +  shows "card {l::nat list. length l = m \<and> listsum l = N} =
1.1097 +    (card {l. length l = (m - 1) \<and> listsum l = N} +
1.1098 +    card {l. length l = m \<and> listsum l + 1 =  N})"
1.1099 +    (is "card ?C = (card ?A + card ?B)")
1.1100 +proof -
1.1101 +  let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
1.1102 +  let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
1.1103 +  let ?f ="\<lambda> l. 0#l"
1.1104 +  let ?g ="\<lambda> l. (hd l + 1) # tl l"
1.1105 +  have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp
1.1106 +  have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs"
1.1107 +    by(auto simp add: neq_Nil_conv)
1.1108 +  have f: "bij_betw ?f ?A ?A'"
1.1109 +    apply(rule bij_betw_byWitness[where f' = tl])
1.1110 +    using assms
1.1111 +    by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
1.1112 +  have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs"
1.1113 +    by (metis 1 listsum_simps(2) 2)
1.1114 +  have g: "bij_betw ?g ?B ?B'"
1.1115 +    apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"])
1.1116 +    using assms
1.1117 +    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
1.1118 +      simp del: length_greater_0_conv length_0_conv)
1.1119 +  { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}"
1.1120 +    using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto }
1.1121 +    note fin = this
1.1122 +  have fin_A: "finite ?A" using fin[of _ "N+1"]
1.1123 +    by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"],
1.1124 +      auto simp: member_le_listsum_nat less_Suc_eq_le)
1.1125 +  have fin_B: "finite ?B"
1.1126 +    by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"],
1.1127 +      auto simp: member_le_listsum_nat less_Suc_eq_le fin)
1.1128 +  have uni: "?C = ?A' \<union> ?B'" by auto
1.1129 +  have disj: "?A' \<inter> ?B' = {}" by auto
1.1130 +  have "card ?C = card(?A' \<union> ?B')" using uni by simp
1.1131 +  also have "\<dots> = card ?A + card ?B"
1.1132 +    using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
1.1133 +      bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
1.1134 +    by presburger
1.1135 +  finally show ?thesis .
1.1136 +qed
1.1137 +
1.1138 +lemma card_length_listsum: --"By Holden Lee, tidied by Tobias Nipkow"
1.1139 +  "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
1.1140 +proof (cases m)
1.1141 +  case 0 then show ?thesis
1.1142 +    by (cases N) (auto simp: cong: conj_cong)
1.1143 +next
1.1144 +  case (Suc m')
1.1145 +    have m: "m\<ge>1" by (simp add: Suc)
1.1146 +    then show ?thesis
1.1147 +    proof (induct "N + m - 1" arbitrary: N m)
1.1148 +      case 0   -- "In the base case, the only solution is [0]."
1.1149 +      have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
1.1150 +        by (auto simp: length_Suc_conv)
1.1151 +      have "m=1 \<and> N=0" using 0 by linarith
1.1152 +      then show ?case by simp
1.1153 +    next
1.1154 +      case (Suc k)
1.1155 +
1.1156 +      have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} =
1.1157 +        (N + (m - 1) - 1) choose N"
1.1158 +      proof cases
1.1159 +        assume "m = 1"
1.1160 +        with Suc.hyps have "N\<ge>1" by auto
1.1161 +        with `m = 1` show ?thesis by (simp add: binomial_eq_0)
1.1162 +      next
1.1163 +        assume "m \<noteq> 1" thus ?thesis using Suc by fastforce
1.1164 +      qed
1.1165 +
1.1166 +      from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
1.1167 +        (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
1.1168 +      proof -
1.1169 +        have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith
1.1170 +        from Suc have "N>0 \<Longrightarrow>
1.1171 +          card {l::nat list. size l = m \<and> listsum l + 1 = N} =
1.1172 +          ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)
1.1173 +        thus ?thesis by auto
1.1174 +      qed
1.1175 +
1.1176 +      from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
1.1177 +          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
1.1178 +        by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
1.1179 +      thus ?case using card_length_listsum_rec[OF Suc.prems] by auto
1.1180 +    qed
1.1181 +qed
1.1182 +
1.1183 +end
```
```     2.1 --- a/src/HOL/Fact.thy	Tue Mar 10 15:21:26 2015 +0000
2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,1180 +0,0 @@
2.4 -(*  Title       : Fact.thy
2.5 -    Author      : Jacques D. Fleuriot
2.6 -    Copyright   : 1998  University of Cambridge
2.7 -    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
2.8 -    The integer version of factorial and other additions by Jeremy Avigad.
2.9 -*)
2.10 -
2.11 -section{*Factorial Function*}
2.12 -
2.13 -theory Fact
2.14 -imports Main
2.15 -begin
2.16 -
2.17 -class fact =
2.18 -  fixes fact :: "'a \<Rightarrow> 'a"
2.19 -
2.20 -instantiation nat :: fact
2.21 -begin
2.22 -
2.23 -fun
2.24 -  fact_nat :: "nat \<Rightarrow> nat"
2.25 -where
2.26 -  fact_0_nat: "fact_nat 0 = Suc 0"
2.27 -| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
2.28 -
2.29 -instance ..
2.30 -
2.31 -end
2.32 -
2.33 -(* definitions for the integers *)
2.34 -
2.35 -instantiation int :: fact
2.36 -
2.37 -begin
2.38 -
2.39 -definition
2.40 -  fact_int :: "int \<Rightarrow> int"
2.41 -where
2.42 -  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
2.43 -
2.44 -instance proof qed
2.45 -
2.46 -end
2.47 -
2.48 -
2.49 -subsection {* Set up Transfer *}
2.50 -
2.51 -lemma transfer_nat_int_factorial:
2.52 -  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
2.53 -  unfolding fact_int_def
2.54 -  by auto
2.55 -
2.56 -
2.57 -lemma transfer_nat_int_factorial_closure:
2.58 -  "x >= (0::int) \<Longrightarrow> fact x >= 0"
2.59 -  by (auto simp add: fact_int_def)
2.60 -
2.62 -    transfer_nat_int_factorial transfer_nat_int_factorial_closure]
2.63 -
2.64 -lemma transfer_int_nat_factorial:
2.65 -  "fact (int x) = int (fact x)"
2.66 -  unfolding fact_int_def by auto
2.67 -
2.68 -lemma transfer_int_nat_factorial_closure:
2.69 -  "is_nat x \<Longrightarrow> fact x >= 0"
2.70 -  by (auto simp add: fact_int_def)
2.71 -
2.73 -    transfer_int_nat_factorial transfer_int_nat_factorial_closure]
2.74 -
2.75 -
2.76 -subsection {* Factorial *}
2.77 -
2.78 -lemma fact_0_int [simp]: "fact (0::int) = 1"
2.79 -  by (simp add: fact_int_def)
2.80 -
2.81 -lemma fact_1_nat [simp]: "fact (1::nat) = 1"
2.82 -  by simp
2.83 -
2.84 -lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
2.85 -  by simp
2.86 -
2.87 -lemma fact_1_int [simp]: "fact (1::int) = 1"
2.88 -  by (simp add: fact_int_def)
2.89 -
2.90 -lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
2.91 -  by simp
2.92 -
2.93 -lemma fact_plus_one_int:
2.94 -  assumes "n >= 0"
2.95 -  shows "fact ((n::int) + 1) = (n + 1) * fact n"
2.96 -  using assms unfolding fact_int_def
2.98 -
2.99 -lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
2.100 -  apply (subgoal_tac "n = Suc (n - 1)")
2.101 -  apply (erule ssubst)
2.102 -  apply (subst fact_Suc)
2.103 -  apply simp_all
2.104 -  done
2.105 -
2.106 -lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
2.107 -  apply (subgoal_tac "n = (n - 1) + 1")
2.108 -  apply (erule ssubst)
2.109 -  apply (subst fact_plus_one_int)
2.110 -  apply simp_all
2.111 -  done
2.112 -
2.113 -lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
2.114 -  apply (induct n)
2.115 -  apply (auto simp add: fact_plus_one_nat)
2.116 -  done
2.117 -
2.118 -lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
2.119 -  by (simp add: fact_int_def)
2.120 -
2.121 -lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
2.122 -  by (insert fact_nonzero_nat [of n], arith)
2.123 -
2.124 -lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
2.125 -  by (auto simp add: fact_int_def)
2.126 -
2.127 -lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
2.128 -  by (insert fact_nonzero_nat [of n], arith)
2.129 -
2.130 -lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
2.131 -  by (insert fact_nonzero_nat [of n], arith)
2.132 -
2.133 -lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
2.134 -  apply (auto simp add: fact_int_def)
2.135 -  apply (subgoal_tac "1 = int 1")
2.136 -  apply (erule ssubst)
2.137 -  apply (subst zle_int)
2.138 -  apply auto
2.139 -  done
2.140 -
2.141 -lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
2.142 -  apply (induct n)
2.143 -  apply force
2.144 -  apply (auto simp only: fact_Suc)
2.145 -  apply (subgoal_tac "m = Suc n")
2.146 -  apply (erule ssubst)
2.147 -  apply (rule dvd_triv_left)
2.148 -  apply auto
2.149 -  done
2.150 -
2.151 -lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
2.152 -  apply (case_tac "1 <= n")
2.153 -  apply (induct n rule: int_ge_induct)
2.154 -  apply (auto simp add: fact_plus_one_int)
2.155 -  apply (subgoal_tac "m = i + 1")
2.156 -  apply auto
2.157 -  done
2.158 -
2.159 -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
2.160 -  {i..j+1} = {i..j} Un {j+1}"
2.161 -  by auto
2.162 -
2.163 -lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
2.164 -  by auto
2.165 -
2.166 -lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
2.167 -  by auto
2.168 -
2.169 -lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
2.170 -  apply (induct n)
2.171 -  apply force
2.172 -  apply (subst fact_Suc)
2.173 -  apply (subst interval_Suc)
2.174 -  apply auto
2.175 -done
2.176 -
2.177 -lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
2.178 -  apply (induct n rule: int_ge_induct)
2.179 -  apply force
2.180 -  apply (subst fact_plus_one_int, assumption)
2.181 -  apply (subst interval_plus_one_int)
2.182 -  apply auto
2.183 -done
2.184 -
2.185 -lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
2.186 -  by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
2.187 -
2.188 -lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
2.189 -  by (auto simp add: dvd_imp_mod_0 fact_dvd)
2.190 -
2.191 -lemma fact_div_fact:
2.192 -  assumes "m \<ge> (n :: nat)"
2.193 -  shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
2.194 -proof -
2.195 -  obtain d where "d = m - n" by auto
2.196 -  from assms this have "m = n + d" by auto
2.197 -  have "fact (n + d) div (fact n) = \<Prod>{n + 1..n + d}"
2.198 -  proof (induct d)
2.199 -    case 0
2.200 -    show ?case by simp
2.201 -  next
2.202 -    case (Suc d')
2.203 -    have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
2.204 -      by simp
2.205 -    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
2.206 -      unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
2.207 -    also have "... = \<Prod>{n + 1..n + Suc d'}"
2.208 -      by (simp add: atLeastAtMostSuc_conv setprod.insert)
2.209 -    finally show ?case .
2.210 -  qed
2.211 -  from this `m = n + d` show ?thesis by simp
2.212 -qed
2.213 -
2.214 -lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
2.215 -apply (drule le_imp_less_or_eq)
2.217 -apply (induct_tac k, auto)
2.218 -done
2.219 -
2.220 -lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
2.221 -  unfolding fact_int_def by auto
2.222 -
2.223 -lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
2.224 -  apply (case_tac "m >= 0")
2.225 -  apply auto
2.226 -  apply (frule fact_gt_zero_int)
2.227 -  apply arith
2.228 -done
2.229 -
2.230 -lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
2.231 -    fact (m + k) >= fact m"
2.232 -  apply (case_tac "m < 0")
2.233 -  apply auto
2.234 -  apply (induct k rule: int_ge_induct)
2.235 -  apply auto
2.236 -  apply (subst add.assoc [symmetric])
2.237 -  apply (subst fact_plus_one_int)
2.238 -  apply auto
2.239 -  apply (erule order_trans)
2.240 -  apply (subst mult_le_cancel_right1)
2.241 -  apply (subgoal_tac "fact (m + i) >= 0")
2.242 -  apply arith
2.243 -  apply auto
2.244 -done
2.245 -
2.246 -lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
2.247 -  apply (insert fact_mono_int_aux [of "n - m" "m"])
2.248 -  apply auto
2.249 -done
2.250 -
2.251 -text{*Note that @{term "fact 0 = fact 1"}*}
2.252 -lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
2.253 -apply (drule_tac m = m in less_imp_Suc_add, auto)
2.254 -apply (induct_tac k, auto)
2.255 -done
2.256 -
2.257 -lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
2.258 -    fact m < fact ((m + 1) + k)"
2.259 -  apply (induct k rule: int_ge_induct)
2.260 -  apply (simp add: fact_plus_one_int)
2.261 -  apply (subst (2) fact_reduce_int)
2.262 -  apply (auto simp add: ac_simps)
2.263 -  apply (erule order_less_le_trans)
2.264 -  apply auto
2.265 -  done
2.266 -
2.267 -lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
2.268 -  apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
2.269 -  apply auto
2.270 -done
2.271 -
2.272 -lemma fact_num_eq_if_nat: "fact (m::nat) =
2.273 -  (if m=0 then 1 else m * fact (m - 1))"
2.274 -by (cases m) auto
2.275 -
2.277 -  "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
2.278 -by (cases "m + n") auto
2.279 -
2.281 -  "fact ((m::nat) + n) =
2.282 -    (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
2.283 -by (cases m) auto
2.284 -
2.285 -lemma fact_le_power: "fact n \<le> n^n"
2.286 -proof (induct n)
2.287 -  case (Suc n)
2.288 -  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
2.290 -qed simp
2.291 -
2.292 -subsection {* @{term fact} and @{term of_nat} *}
2.293 -
2.294 -lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
2.295 -by auto
2.296 -
2.297 -lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
2.298 -
2.299 -lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
2.300 -by simp
2.301 -
2.302 -lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
2.303 -by (auto simp add: positive_imp_inverse_positive)
2.304 -
2.305 -lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
2.306 -by (auto intro: order_less_imp_le)
2.307 -
2.308 -lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
2.309 -  unfolding fact_altdef_nat
2.310 -  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
2.311 -
2.312 -lemma fact_div_fact_le_pow:
2.313 -  assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
2.314 -proof -
2.315 -  have "\<And>r. r \<le> n \<Longrightarrow> \<Prod>{n - r..n} = (n - r) * \<Prod>{Suc (n - r)..n}"
2.316 -    by (subst setprod.insert[symmetric]) (auto simp: atLeastAtMost_insertL)
2.317 -  with assms show ?thesis
2.318 -    by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
2.319 -qed
2.320 -
2.321 -lemma fact_numeral:  --{*Evaluation for specific numerals*}
2.322 -  "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
2.323 -  by (simp add: numeral_eq_Suc)
2.324 -
2.325 -
2.326 -text {* This development is based on the work of Andy Gordon and
2.327 -  Florian Kammueller. *}
2.328 -
2.329 -subsection {* Basic definitions and lemmas *}
2.330 -
2.331 -primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
2.332 -where
2.333 -  "0 choose k = (if k = 0 then 1 else 0)"
2.334 -| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
2.335 -
2.336 -lemma binomial_n_0 [simp]: "(n choose 0) = 1"
2.337 -  by (cases n) simp_all
2.338 -
2.339 -lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
2.340 -  by simp
2.341 -
2.342 -lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
2.343 -  by simp
2.344 -
2.345 -lemma choose_reduce_nat:
2.346 -  "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>
2.347 -    (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
2.348 -  by (metis Suc_diff_1 binomial.simps(2) neq0_conv)
2.349 -
2.350 -lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"
2.351 -  by (induct n arbitrary: k) auto
2.352 -
2.353 -declare binomial.simps [simp del]
2.354 -
2.355 -lemma binomial_n_n [simp]: "n choose n = 1"
2.356 -  by (induct n) (simp_all add: binomial_eq_0)
2.357 -
2.358 -lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"
2.359 -  by (induct n) simp_all
2.360 -
2.361 -lemma binomial_1 [simp]: "n choose Suc 0 = n"
2.362 -  by (induct n) simp_all
2.363 -
2.364 -lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"
2.365 -  by (induct n k rule: diff_induct) simp_all
2.366 -
2.367 -lemma binomial_eq_0_iff [simp]: "n choose k = 0 \<longleftrightarrow> n < k"
2.368 -  by (metis binomial_eq_0 less_numeral_extra(3) not_less zero_less_binomial)
2.369 -
2.370 -lemma zero_less_binomial_iff [simp]: "n choose k > 0 \<longleftrightarrow> k \<le> n"
2.371 -  by (metis binomial_eq_0_iff not_less0 not_less zero_less_binomial)
2.372 -
2.373 -lemma Suc_times_binomial_eq:
2.374 -  "Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
2.375 -  apply (induct n arbitrary: k, simp add: binomial.simps)
2.376 -  apply (case_tac k)
2.378 -  done
2.379 -
2.380 -text{*The absorption property*}
2.381 -lemma Suc_times_binomial:
2.382 -  "Suc k * (Suc n choose Suc k) = Suc n * (n choose k)"
2.383 -  using Suc_times_binomial_eq by auto
2.384 -
2.385 -text{*This is the well-known version of absorption, but it's harder to use because of the
2.386 -  need to reason about division.*}
2.387 -lemma binomial_Suc_Suc_eq_times:
2.388 -    "(Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
2.389 -  by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
2.390 -
2.391 -text{*Another version of absorption, with -1 instead of Suc.*}
2.392 -lemma times_binomial_minus1_eq:
2.393 -  "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))"
2.394 -  using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
2.395 -  by (auto split add: nat_diff_split)
2.396 -
2.397 -
2.398 -subsection {* Combinatorial theorems involving @{text "choose"} *}
2.399 -
2.400 -text {*By Florian Kamm\"uller, tidied by LCP.*}
2.401 -
2.402 -lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1"
2.404 -
2.405 -lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow>
2.406 -    {s. s \<subseteq> insert x M \<and> card s = Suc k} =
2.407 -    {s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}"
2.408 -  apply safe
2.409 -     apply (auto intro: finite_subset [THEN card_insert_disjoint])
2.410 -  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if
2.411 -     card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)
2.412 -
2.413 -lemma finite_bex_subset [simp]:
2.414 -  assumes "finite B"
2.415 -    and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
2.416 -  shows "finite {x. \<exists>A \<subseteq> B. P x A}"
2.417 -  by (metis (no_types) assms finite_Collect_bounded_ex finite_Collect_subsets)
2.418 -
2.419 -text{*There are as many subsets of @{term A} having cardinality @{term k}
2.420 - as there are sets obtained from the former by inserting a fixed element
2.421 - @{term x} into each.*}
2.422 -lemma constr_bij:
2.423 -   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow>
2.424 -    card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} =
2.425 -    card {B. B \<subseteq> A & card(B) = k}"
2.426 -  apply (rule card_bij_eq [where f = "\<lambda>s. s - {x}" and g = "insert x"])
2.427 -  apply (auto elim!: equalityE simp add: inj_on_def)
2.428 -  apply (metis card_Diff_singleton_if finite_subset in_mono)
2.429 -  done
2.430 -
2.431 -text {*
2.432 -  Main theorem: combinatorial statement about number of subsets of a set.
2.433 -*}
2.434 -
2.435 -theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)"
2.436 -proof (induct k arbitrary: A)
2.437 -  case 0 then show ?case by (simp add: card_s_0_eq_empty)
2.438 -next
2.439 -  case (Suc k)
2.440 -  show ?case using `finite A`
2.441 -  proof (induct A)
2.442 -    case empty show ?case by (simp add: card_s_0_eq_empty)
2.443 -  next
2.444 -    case (insert x A)
2.445 -    then show ?case using Suc.hyps
2.446 -      apply (simp add: card_s_0_eq_empty choose_deconstruct)
2.447 -      apply (subst card_Un_disjoint)
2.448 -         prefer 4 apply (force simp add: constr_bij)
2.449 -        prefer 3 apply force
2.450 -       prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
2.451 -         finite_subset [of _ "Pow (insert x F)" for F])
2.452 -      apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
2.453 -      done
2.454 -  qed
2.455 -qed
2.456 -
2.457 -
2.458 -subsection {* The binomial theorem (courtesy of Tobias Nipkow): *}
2.459 -
2.460 -text{* Avigad's version, generalized to any commutative ring *}
2.461 -theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n =
2.462 -  (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
2.463 -proof (induct n)
2.464 -  case 0 then show "?P 0" by simp
2.465 -next
2.466 -  case (Suc n)
2.467 -  have decomp: "{0..n+1} = {0} Un {n+1} Un {1..n}"
2.468 -    by auto
2.469 -  have decomp2: "{0..n} = {0} Un {1..n}"
2.470 -    by auto
2.471 -  have "(a+b)^(n+1) =
2.472 -      (a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
2.473 -    using Suc.hyps by simp
2.474 -  also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
2.475 -                   b*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
2.476 -    by (rule distrib_right)
2.477 -  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^(k+1) * b^(n-k)) +
2.478 -                  (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k+1))"
2.479 -    by (auto simp add: setsum_right_distrib ac_simps)
2.480 -  also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
2.481 -                  (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
2.482 -    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps
2.483 -        del:setsum_cl_ivl_Suc)
2.484 -  also have "\<dots> = a^(n+1) + b^(n+1) +
2.485 -                  (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
2.486 -                  (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
2.487 -    by (simp add: decomp2)
2.488 -  also have
2.489 -      "\<dots> = a^(n+1) + b^(n+1) +
2.490 -            (\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
2.491 -    by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat)
2.492 -  also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
2.493 -    using decomp by (simp add: field_simps)
2.494 -  finally show "?P (Suc n)" by simp
2.495 -qed
2.496 -
2.497 -text{* Original version for the naturals *}
2.498 -corollary binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))"
2.499 -    using binomial_ring [of "int a" "int b" n]
2.500 -  by (simp only: of_nat_add [symmetric] of_nat_mult [symmetric] of_nat_power [symmetric]
2.501 -           of_nat_setsum [symmetric]
2.502 -           of_nat_eq_iff of_nat_id)
2.503 -
2.504 -lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
2.505 -proof (induct n arbitrary: k rule: nat_less_induct)
2.506 -  fix n k assume H: "\<forall>m<n. \<forall>x\<le>m. fact x * fact (m - x) * (m choose x) =
2.507 -                      fact m" and kn: "k \<le> n"
2.508 -  let ?ths = "fact k * fact (n - k) * (n choose k) = fact n"
2.509 -  { assume "n=0" then have ?ths using kn by simp }
2.510 -  moreover
2.511 -  { assume "k=0" then have ?ths using kn by simp }
2.512 -  moreover
2.513 -  { assume nk: "n=k" then have ?ths by simp }
2.514 -  moreover
2.515 -  { fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m"
2.516 -    from n have mn: "m < n" by arith
2.517 -    from hm have hm': "h \<le> m" by arith
2.518 -    from hm h n kn have km: "k \<le> m" by arith
2.519 -    have "m - h = Suc (m - Suc h)" using  h km hm by arith
2.520 -    with km h have th0: "fact (m - h) = (m - h) * fact (m - k)"
2.521 -      by simp
2.522 -    from n h th0
2.523 -    have "fact k * fact (n - k) * (n choose k) =
2.524 -        k * (fact h * fact (m - h) * (m choose h)) +
2.525 -        (m - h) * (fact k * fact (m - k) * (m choose k))"
2.526 -      by (simp add: field_simps)
2.527 -    also have "\<dots> = (k + (m - h)) * fact m"
2.528 -      using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
2.529 -      by (simp add: field_simps)
2.530 -    finally have ?ths using h n km by simp }
2.531 -  moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)"
2.532 -    using kn by presburger
2.533 -  ultimately show ?ths by blast
2.534 -qed
2.535 -
2.536 -lemma binomial_fact:
2.537 -  assumes kn: "k \<le> n"
2.538 -  shows "(of_nat (n choose k) :: 'a::{field,ring_char_0}) =
2.539 -    of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
2.540 -  using binomial_fact_lemma[OF kn]
2.541 -  by (simp add: field_simps of_nat_mult [symmetric])
2.542 -
2.543 -lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
2.544 -  using binomial [of 1 "1" n]
2.545 -  by (simp add: numeral_2_eq_2)
2.546 -
2.547 -lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
2.548 -  by (induct n) auto
2.549 -
2.550 -lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
2.551 -  by (induct n) auto
2.552 -
2.553 -lemma natsum_reverse_index:
2.554 -  fixes m::nat
2.555 -  shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
2.556 -  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
2.557 -
2.558 -text{*NW diagonal sum property*}
2.559 -lemma sum_choose_diagonal:
2.560 -  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
2.561 -proof -
2.562 -  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
2.563 -    by (rule natsum_reverse_index) (simp add: assms)
2.564 -  also have "... = Suc (n-m+m) choose m"
2.565 -    by (rule sum_choose_lower)
2.566 -  also have "... = Suc n choose m" using assms
2.567 -    by simp
2.568 -  finally show ?thesis .
2.569 -qed
2.570 -
2.571 -subsection{* Pochhammer's symbol : generalized rising factorial *}
2.572 -
2.573 -text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
2.574 -
2.575 -definition "pochhammer (a::'a::comm_semiring_1) n =
2.576 -  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
2.577 -
2.578 -lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
2.579 -  by (simp add: pochhammer_def)
2.580 -
2.581 -lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
2.582 -  by (simp add: pochhammer_def)
2.583 -
2.584 -lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
2.585 -  by (simp add: pochhammer_def)
2.586 -
2.587 -lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
2.588 -  by (simp add: pochhammer_def)
2.589 -
2.590 -lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
2.591 -proof -
2.592 -  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
2.593 -  then show ?thesis by (simp add: field_simps)
2.594 -qed
2.595 -
2.596 -lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
2.597 -proof -
2.598 -  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
2.599 -  then show ?thesis by simp
2.600 -qed
2.601 -
2.602 -
2.603 -lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
2.604 -proof (cases n)
2.605 -  case 0
2.606 -  then show ?thesis by simp
2.607 -next
2.608 -  case (Suc n)
2.609 -  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
2.610 -qed
2.611 -
2.612 -lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
2.613 -proof (cases "n = 0")
2.614 -  case True
2.615 -  then show ?thesis by (simp add: pochhammer_Suc_setprod)
2.616 -next
2.617 -  case False
2.618 -  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
2.619 -  have eq: "insert 0 {1 .. n} = {0..n}" by auto
2.620 -  have **: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
2.621 -    apply (rule setprod.reindex_cong [where l = Suc])
2.622 -    using False
2.623 -    apply (auto simp add: fun_eq_iff field_simps)
2.624 -    done
2.625 -  show ?thesis
2.626 -    apply (simp add: pochhammer_def)
2.627 -    unfolding setprod.insert [OF *, unfolded eq]
2.628 -    using ** apply (simp add: field_simps)
2.629 -    done
2.630 -qed
2.631 -
2.632 -lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
2.633 -  unfolding fact_altdef_nat
2.634 -  apply (cases n)
2.635 -   apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
2.636 -  apply (rule setprod.reindex_cong [where l = Suc])
2.637 -    apply (auto simp add: fun_eq_iff)
2.638 -  done
2.639 -
2.640 -lemma pochhammer_of_nat_eq_0_lemma:
2.641 -  assumes "k > n"
2.642 -  shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
2.643 -proof (cases "n = 0")
2.644 -  case True
2.645 -  then show ?thesis
2.646 -    using assms by (cases k) (simp_all add: pochhammer_rec)
2.647 -next
2.648 -  case False
2.649 -  from assms obtain h where "k = Suc h" by (cases k) auto
2.650 -  then show ?thesis
2.651 -    by (simp add: pochhammer_Suc_setprod)
2.652 -       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
2.653 -qed
2.654 -
2.655 -lemma pochhammer_of_nat_eq_0_lemma':
2.656 -  assumes kn: "k \<le> n"
2.657 -  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0"
2.658 -proof (cases k)
2.659 -  case 0
2.660 -  then show ?thesis by simp
2.661 -next
2.662 -  case (Suc h)
2.663 -  then show ?thesis
2.664 -    apply (simp add: pochhammer_Suc_setprod)
2.665 -    using Suc kn apply (auto simp add: algebra_simps)
2.666 -    done
2.667 -qed
2.668 -
2.669 -lemma pochhammer_of_nat_eq_0_iff:
2.670 -  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
2.671 -  (is "?l = ?r")
2.672 -  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
2.673 -    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
2.674 -  by (auto simp add: not_le[symmetric])
2.675 -
2.676 -lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
2.677 -  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
2.678 -  apply (cases n)
2.680 -  apply (metis leD not_less_eq)
2.681 -  done
2.682 -
2.683 -lemma pochhammer_eq_0_mono:
2.684 -  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
2.685 -  unfolding pochhammer_eq_0_iff by auto
2.686 -
2.687 -lemma pochhammer_neq_0_mono:
2.688 -  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
2.689 -  unfolding pochhammer_eq_0_iff by auto
2.690 -
2.691 -lemma pochhammer_minus:
2.692 -  assumes kn: "k \<le> n"
2.693 -  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
2.694 -proof (cases k)
2.695 -  case 0
2.696 -  then show ?thesis by simp
2.697 -next
2.698 -  case (Suc h)
2.699 -  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
2.700 -    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
2.701 -    by auto
2.702 -  show ?thesis
2.703 -    unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
2.704 -    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
2.705 -       (auto simp: of_nat_diff)
2.706 -qed
2.707 -
2.708 -lemma pochhammer_minus':
2.709 -  assumes kn: "k \<le> n"
2.710 -  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
2.711 -  unfolding pochhammer_minus[OF kn, where b=b]
2.712 -  unfolding mult.assoc[symmetric]
2.714 -  by simp
2.715 -
2.716 -lemma pochhammer_same: "pochhammer (- of_nat n) n =
2.717 -    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
2.718 -  unfolding pochhammer_minus[OF le_refl[of n]]
2.719 -  by (simp add: of_nat_diff pochhammer_fact)
2.720 -
2.721 -
2.722 -subsection{* Generalized binomial coefficients *}
2.723 -
2.724 -definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
2.725 -  where "a gchoose n =
2.726 -    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
2.727 -
2.728 -lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
2.729 -  apply (simp_all add: gbinomial_def)
2.730 -  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
2.731 -   apply (simp del:setprod_zero_iff)
2.732 -  apply simp
2.733 -  done
2.734 -
2.735 -lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
2.736 -proof (cases "n = 0")
2.737 -  case True
2.738 -  then show ?thesis by simp
2.739 -next
2.740 -  case False
2.741 -  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
2.742 -  have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
2.743 -    by auto
2.744 -  from False show ?thesis
2.745 -    by (simp add: pochhammer_def gbinomial_def field_simps
2.746 -      eq setprod.distrib[symmetric])
2.747 -qed
2.748 -
2.749 -lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
2.750 -proof -
2.751 -  { assume kn: "k > n"
2.752 -    then have ?thesis
2.753 -      by (subst binomial_eq_0[OF kn])
2.754 -         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
2.755 -  moreover
2.756 -  { assume "k=0" then have ?thesis by simp }
2.757 -  moreover
2.758 -  { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
2.759 -    from k0 obtain h where h: "k = Suc h" by (cases k) auto
2.760 -    from h
2.761 -    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
2.762 -      by (subst setprod_constant) auto
2.763 -    have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
2.764 -        using h kn
2.765 -      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
2.766 -         (auto simp: of_nat_diff)
2.767 -    have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
2.768 -        "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
2.769 -        eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
2.770 -      using h kn by auto
2.771 -    from eq[symmetric]
2.772 -    have ?thesis using kn
2.773 -      apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
2.774 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
2.775 -      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
2.776 -        of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
2.777 -      unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
2.778 -      unfolding mult.assoc[symmetric]
2.779 -      unfolding setprod.distrib[symmetric]
2.780 -      apply simp
2.781 -      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
2.782 -      apply (auto simp: of_nat_diff)
2.783 -      done
2.784 -  }
2.785 -  moreover
2.786 -  have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith
2.787 -  ultimately show ?thesis by blast
2.788 -qed
2.789 -
2.790 -lemma gbinomial_1[simp]: "a gchoose 1 = a"
2.791 -  by (simp add: gbinomial_def)
2.792 -
2.793 -lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
2.794 -  by (simp add: gbinomial_def)
2.795 -
2.796 -lemma gbinomial_mult_1:
2.797 -  "a * (a gchoose n) =
2.798 -    of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")
2.799 -proof -
2.800 -  have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
2.801 -    unfolding gbinomial_pochhammer
2.802 -      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
2.803 -    by (simp add:  field_simps del: of_nat_Suc)
2.804 -  also have "\<dots> = ?l" unfolding gbinomial_pochhammer
2.805 -    by (simp add: field_simps)
2.806 -  finally show ?thesis ..
2.807 -qed
2.808 -
2.809 -lemma gbinomial_mult_1':
2.810 -    "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
2.811 -  by (simp add: mult.commute gbinomial_mult_1)
2.812 -
2.813 -lemma gbinomial_Suc:
2.814 -    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
2.815 -  by (simp add: gbinomial_def)
2.816 -
2.817 -lemma gbinomial_mult_fact:
2.818 -  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
2.819 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
2.820 -  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
2.821 -
2.822 -lemma gbinomial_mult_fact':
2.823 -  "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
2.824 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
2.825 -  using gbinomial_mult_fact[of k a]
2.826 -  by (subst mult.commute)
2.827 -
2.828 -
2.829 -lemma gbinomial_Suc_Suc:
2.830 -  "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
2.831 -proof (cases k)
2.832 -  case 0
2.833 -  then show ?thesis by simp
2.834 -next
2.835 -  case (Suc h)
2.836 -  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
2.837 -    apply (rule setprod.reindex_cong [where l = Suc])
2.838 -      using Suc
2.839 -      apply auto
2.840 -    done
2.841 -  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
2.842 -    ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
2.843 -    apply (simp add: Suc field_simps del: fact_Suc)
2.844 -    unfolding gbinomial_mult_fact'
2.845 -    apply (subst fact_Suc)
2.846 -    unfolding of_nat_mult
2.847 -    apply (subst mult.commute)
2.848 -    unfolding mult.assoc
2.849 -    unfolding gbinomial_mult_fact
2.850 -    apply (simp add: field_simps)
2.851 -    done
2.852 -  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
2.853 -    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
2.854 -    by (simp add: field_simps Suc)
2.855 -  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
2.856 -    using eq0
2.857 -    by (simp add: Suc setprod_nat_ivl_1_Suc)
2.858 -  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
2.859 -    unfolding gbinomial_mult_fact ..
2.860 -  finally show ?thesis by (simp del: fact_Suc)
2.861 -qed
2.862 -
2.863 -lemma gbinomial_reduce_nat:
2.864 -  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
2.865 -by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
2.866 -
2.867 -
2.868 -lemma binomial_symmetric:
2.869 -  assumes kn: "k \<le> n"
2.870 -  shows "n choose k = n choose (n - k)"
2.871 -proof-
2.872 -  from kn have kn': "n - k \<le> n" by arith
2.873 -  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
2.874 -  have "fact k * fact (n - k) * (n choose k) =
2.875 -    fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
2.876 -  then show ?thesis using kn by simp
2.877 -qed
2.878 -
2.879 -text{*Contributed by Manuel Eberl, generalised by LCP.
2.880 -  Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
2.881 -lemma gbinomial_altdef_of_nat:
2.882 -  fixes k :: nat
2.883 -    and x :: "'a :: {field_char_0,field_inverse_zero}"
2.884 -  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
2.885 -proof -
2.886 -  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
2.887 -    unfolding gbinomial_def
2.888 -    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
2.889 -  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
2.890 -    unfolding fact_eq_rev_setprod_nat of_nat_setprod
2.891 -    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
2.892 -  finally show ?thesis .
2.893 -qed
2.894 -
2.895 -lemma gbinomial_ge_n_over_k_pow_k:
2.896 -  fixes k :: nat
2.897 -    and x :: "'a :: linordered_field_inverse_zero"
2.898 -  assumes "of_nat k \<le> x"
2.899 -  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
2.900 -proof -
2.901 -  have x: "0 \<le> x"
2.902 -    using assms of_nat_0_le_iff order_trans by blast
2.903 -  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
2.904 -    by (simp add: setprod_constant)
2.905 -  also have "\<dots> \<le> x gchoose k"
2.906 -    unfolding gbinomial_altdef_of_nat
2.907 -  proof (safe intro!: setprod_mono)
2.908 -    fix i :: nat
2.909 -    assume ik: "i < k"
2.910 -    from assms have "x * of_nat i \<ge> of_nat (i * k)"
2.911 -      by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
2.912 -    then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith
2.913 -    then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
2.914 -      using ik
2.915 -      by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)
2.916 -    then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
2.917 -      unfolding of_nat_mult[symmetric] of_nat_le_iff .
2.918 -    with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"
2.919 -      using `i < k` by (simp add: field_simps)
2.920 -  qed (simp add: x zero_le_divide_iff)
2.921 -  finally show ?thesis .
2.922 -qed
2.923 -
2.924 -text{*Versions of the theorems above for the natural-number version of "choose"*}
2.925 -lemma binomial_altdef_of_nat:
2.926 -  fixes n k :: nat
2.927 -    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
2.928 -  assumes "k \<le> n"
2.929 -  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
2.930 -using assms
2.931 -by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
2.932 -
2.933 -lemma binomial_ge_n_over_k_pow_k:
2.934 -  fixes k n :: nat
2.935 -    and x :: "'a :: linordered_field_inverse_zero"
2.936 -  assumes "k \<le> n"
2.937 -  shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
2.938 -by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
2.939 -
2.940 -lemma binomial_le_pow:
2.941 -  assumes "r \<le> n"
2.942 -  shows "n choose r \<le> n ^ r"
2.943 -proof -
2.944 -  have "n choose r \<le> fact n div fact (n - r)"
2.945 -    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
2.946 -  with fact_div_fact_le_pow [OF assms] show ?thesis by auto
2.947 -qed
2.948 -
2.949 -lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
2.950 -    n choose k = fact n div (fact k * fact (n - k))"
2.951 - by (subst binomial_fact_lemma [symmetric]) auto
2.952 -
2.953 -lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
2.954 -by (metis binomial_fact_lemma dvd_def)
2.955 -
2.956 -lemma choose_dvd_int:
2.957 -  assumes "(0::int) <= k" and "k <= n"
2.958 -  shows "fact k * fact (n - k) dvd fact n"
2.959 -  apply (subst tsub_eq [symmetric], rule assms)
2.960 -  apply (rule choose_dvd_nat [transferred])
2.961 -  using assms apply auto
2.962 -  done
2.963 -
2.964 -lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
2.966 -
2.967 -lemma choose_mult_lemma:
2.968 -     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
2.969 -proof -
2.970 -  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
2.971 -        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
2.972 -    by (simp add: assms binomial_altdef_nat)
2.973 -  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
2.974 -    apply (subst div_mult_div_if_dvd)
2.975 -    apply (auto simp: fact_fact_dvd_fact)
2.977 -    done
2.978 -  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
2.979 -    apply (subst div_mult_div_if_dvd [symmetric])
2.980 -    apply (auto simp: fact_fact_dvd_fact)
2.981 -    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
2.982 -    done
2.983 -  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
2.984 -    apply (subst div_mult_div_if_dvd)
2.985 -    apply (auto simp: fact_fact_dvd_fact)
2.986 -    apply(metis mult.left_commute)
2.987 -    done
2.988 -  finally show ?thesis
2.989 -    by (simp add: binomial_altdef_nat mult.commute)
2.990 -qed
2.991 -
2.992 -text{*The "Subset of a Subset" identity*}
2.993 -lemma choose_mult:
2.994 -  assumes "k\<le>m" "m\<le>n"
2.995 -    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
2.996 -using assms choose_mult_lemma [of "m-k" "n-m" k]
2.997 -by simp
2.998 -
2.999 -
2.1000 -subsection {* Binomial coefficients *}
2.1001 -
2.1002 -lemma choose_one: "(n::nat) choose 1 = n"
2.1003 -  by simp
2.1004 -
2.1005 -(*FIXME: messy and apparently unused*)
2.1006 -lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
2.1007 -    (ALL n. P (Suc n) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow>
2.1008 -    P (Suc n) (Suc k))) \<longrightarrow> (ALL k <= n. P n k)"
2.1009 -  apply (induct n)
2.1010 -  apply auto
2.1011 -  apply (case_tac "k = 0")
2.1012 -  apply auto
2.1013 -  apply (case_tac "k = Suc n")
2.1014 -  apply auto
2.1015 -  apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
2.1016 -  done
2.1017 -
2.1018 -lemma card_UNION:
2.1019 -  assumes "finite A" and "\<forall>k \<in> A. finite k"
2.1020 -  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
2.1021 -  (is "?lhs = ?rhs")
2.1022 -proof -
2.1023 -  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
2.1024 -  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
2.1025 -    by(subst setsum_right_distrib) simp
2.1026 -  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
2.1027 -    using assms by(subst setsum.Sigma)(auto)
2.1028 -  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:UNIV. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
2.1029 -    by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
2.1030 -  also have "\<dots> = (\<Sum>(x, I)\<in>(SIGMA x:\<Union>A. {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}). (- 1) ^ (card I + 1))"
2.1031 -    using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
2.1032 -  also have "\<dots> = (\<Sum>x\<in>\<Union>A. (\<Sum>I|I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I. (- 1) ^ (card I + 1)))"
2.1033 -    using assms by(subst setsum.Sigma) auto
2.1034 -  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
2.1035 -  proof(rule setsum.cong[OF refl])
2.1036 -    fix x
2.1037 -    assume x: "x \<in> \<Union>A"
2.1038 -    def K \<equiv> "{X \<in> A. x \<in> X}"
2.1039 -    with `finite A` have K: "finite K" by auto
2.1040 -    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
2.1041 -    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
2.1042 -      using assms by(auto intro!: inj_onI)
2.1043 -    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
2.1044 -      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
2.1045 -        simp add: card_gt_0_iff[folded Suc_le_eq]
2.1046 -        dest: finite_subset intro: card_mono)
2.1047 -    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
2.1048 -      by (rule setsum.reindex_cong [where l = snd]) fastforce
2.1049 -    also have "\<dots> = (\<Sum>i=1..card A. (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. (- 1) ^ (i + 1)))"
2.1050 -      using assms by(subst setsum.Sigma) auto
2.1051 -    also have "\<dots> = (\<Sum>i=1..card A. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1))"
2.1052 -      by(subst setsum_right_distrib) simp
2.1053 -    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
2.1054 -    proof(rule setsum.mono_neutral_cong_right[rule_format])
2.1055 -      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
2.1056 -        by(auto simp add: K_def intro: card_mono)
2.1057 -    next
2.1058 -      fix i
2.1059 -      assume "i \<in> {1..card A} - {1..card K}"
2.1060 -      hence i: "i \<le> card A" "card K < i" by auto
2.1061 -      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
2.1062 -        by(auto simp add: K_def)
2.1063 -      also have "\<dots> = {}" using `finite A` i
2.1064 -        by(auto simp add: K_def dest: card_mono[rotated 1])
2.1065 -      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
2.1066 -        by(simp only:) simp
2.1067 -    next
2.1068 -      fix i
2.1069 -      have "(\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1) = (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)"
2.1070 -        (is "?lhs = ?rhs")
2.1071 -        by(rule setsum.cong)(auto simp add: K_def)
2.1072 -      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
2.1073 -    qed simp
2.1074 -    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
2.1075 -      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
2.1076 -    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
2.1077 -      by(subst (2) setsum_head_Suc)(simp_all )
2.1078 -    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
2.1079 -      using K by(subst n_subsets[symmetric]) simp_all
2.1080 -    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
2.1081 -      by(subst setsum_right_distrib[symmetric]) simp
2.1082 -    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
2.1083 -      by(subst binomial_ring)(simp add: ac_simps)
2.1084 -    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
2.1085 -    finally show "?lhs x = 1" .
2.1086 -  qed
2.1087 -  also have "nat \<dots> = card (\<Union>A)" by simp
2.1088 -  finally show ?thesis ..
2.1089 -qed
2.1090 -
2.1091 -text{* The number of nat lists of length @{text m} summing to @{text N} is
2.1092 -@{term "(N + m - 1) choose N"}: *}
2.1093 -
2.1094 -lemma card_length_listsum_rec:
2.1095 -  assumes "m\<ge>1"
2.1096 -  shows "card {l::nat list. length l = m \<and> listsum l = N} =
2.1097 -    (card {l. length l = (m - 1) \<and> listsum l = N} +
2.1098 -    card {l. length l = m \<and> listsum l + 1 =  N})"
2.1099 -    (is "card ?C = (card ?A + card ?B)")
2.1100 -proof -
2.1101 -  let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
2.1102 -  let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
2.1103 -  let ?f ="\<lambda> l. 0#l"
2.1104 -  let ?g ="\<lambda> l. (hd l + 1) # tl l"
2.1105 -  have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp
2.1106 -  have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs"
2.1107 -    by(auto simp add: neq_Nil_conv)
2.1108 -  have f: "bij_betw ?f ?A ?A'"
2.1109 -    apply(rule bij_betw_byWitness[where f' = tl])
2.1110 -    using assms
2.1111 -    by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
2.1112 -  have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs"
2.1113 -    by (metis 1 listsum_simps(2) 2)
2.1114 -  have g: "bij_betw ?g ?B ?B'"
2.1115 -    apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"])
2.1116 -    using assms
2.1117 -    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
2.1118 -      simp del: length_greater_0_conv length_0_conv)
2.1119 -  { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}"
2.1120 -    using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto }
2.1121 -    note fin = this
2.1122 -  have fin_A: "finite ?A" using fin[of _ "N+1"]
2.1123 -    by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"],
2.1124 -      auto simp: member_le_listsum_nat less_Suc_eq_le)
2.1125 -  have fin_B: "finite ?B"
2.1126 -    by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"],
2.1127 -      auto simp: member_le_listsum_nat less_Suc_eq_le fin)
2.1128 -  have uni: "?C = ?A' \<union> ?B'" by auto
2.1129 -  have disj: "?A' \<inter> ?B' = {}" by auto
2.1130 -  have "card ?C = card(?A' \<union> ?B')" using uni by simp
2.1131 -  also have "\<dots> = card ?A + card ?B"
2.1132 -    using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
2.1133 -      bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
2.1134 -    by presburger
2.1135 -  finally show ?thesis .
2.1136 -qed
2.1137 -
2.1138 -lemma card_length_listsum: --"By Holden Lee, tidied by Tobias Nipkow"
2.1139 -  "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
2.1140 -proof (cases m)
2.1141 -  case 0 then show ?thesis
2.1142 -    by (cases N) (auto simp: cong: conj_cong)
2.1143 -next
2.1144 -  case (Suc m')
2.1145 -    have m: "m\<ge>1" by (simp add: Suc)
2.1146 -    then show ?thesis
2.1147 -    proof (induct "N + m - 1" arbitrary: N m)
2.1148 -      case 0   -- "In the base case, the only solution is [0]."
2.1149 -      have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
2.1150 -        by (auto simp: length_Suc_conv)
2.1151 -      have "m=1 \<and> N=0" using 0 by linarith
2.1152 -      then show ?case by simp
2.1153 -    next
2.1154 -      case (Suc k)
2.1155 -
2.1156 -      have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} =
2.1157 -        (N + (m - 1) - 1) choose N"
2.1158 -      proof cases
2.1159 -        assume "m = 1"
2.1160 -        with Suc.hyps have "N\<ge>1" by auto
2.1161 -        with `m = 1` show ?thesis by (simp add: binomial_eq_0)
2.1162 -      next
2.1163 -        assume "m \<noteq> 1" thus ?thesis using Suc by fastforce
2.1164 -      qed
2.1165 -
2.1166 -      from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
2.1167 -        (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
2.1168 -      proof -
2.1169 -        have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith
2.1170 -        from Suc have "N>0 \<Longrightarrow>
2.1171 -          card {l::nat list. size l = m \<and> listsum l + 1 = N} =
2.1172 -          ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)
2.1173 -        thus ?thesis by auto
2.1174 -      qed
2.1175 -
2.1176 -      from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
2.1177 -          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
2.1178 -        by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
2.1179 -      thus ?case using card_length_listsum_rec[OF Suc.prems] by auto
2.1180 -    qed
2.1181 -qed
2.1182 -
2.1183 -end
```
```     3.1 --- a/src/HOL/Import/Import_Setup.thy	Tue Mar 10 15:21:26 2015 +0000
3.2 +++ b/src/HOL/Import/Import_Setup.thy	Tue Mar 10 16:12:35 2015 +0000
3.3 @@ -6,7 +6,7 @@
3.4  section {* Importer machinery and required theorems *}
3.5
3.6  theory Import_Setup
3.7 -imports Main "~~/src/HOL/Fact"
3.8 +imports Main "~~/src/HOL/Binomial"
3.9  keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
3.10  begin
3.11
```
```     4.1 --- a/src/HOL/Library/Permutations.thy	Tue Mar 10 15:21:26 2015 +0000
4.2 +++ b/src/HOL/Library/Permutations.thy	Tue Mar 10 16:12:35 2015 +0000
4.3 @@ -5,7 +5,7 @@
4.4  section {* Permutations, both general and specifically on finite sets.*}
4.5
4.6  theory Permutations
4.7 -imports Fact
4.8 +imports Binomial
4.9  begin
4.10
4.11  subsection {* Transpositions *}
4.12 @@ -46,7 +46,7 @@
4.13
4.14  lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S"
4.15    by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on)
4.16 -
4.17 +
4.18  lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
4.19    unfolding permutes_def bij_betw_def inj_on_def
4.20    by auto (metis image_iff)+
```
```     5.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 15:21:26 2015 +0000
5.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 16:12:35 2015 +0000
5.3 @@ -28,7 +28,7 @@
5.4  section {* Primes *}
5.5
5.6  theory Primes
5.7 -imports "~~/src/HOL/GCD" "~~/src/HOL/Fact"
5.8 +imports "~~/src/HOL/GCD" "~~/src/HOL/Binomial"
5.9  begin
5.10
5.11  declare [[coercion int]]
5.12 @@ -72,7 +72,7 @@
5.13    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
5.14    done
5.15
5.16 -lemma prime_int_altdef:
5.17 +lemma prime_int_altdef:
5.18    "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
5.19      m = 1 \<or> m = p))"
5.21 @@ -90,7 +90,7 @@
5.22  lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
5.23    by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
5.24
5.25 -lemma prime_dvd_mult_int:
5.26 +lemma prime_dvd_mult_int:
5.27    fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
5.28    by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
5.29
5.30 @@ -99,7 +99,7 @@
5.31    by (rule iffI, rule prime_dvd_mult_nat, auto)
5.32
5.33  lemma prime_dvd_mult_eq_int [simp]:
5.34 -  fixes n::int
5.35 +  fixes n::int
5.36    shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
5.37    by (rule iffI, rule prime_dvd_mult_int, auto)
5.38
5.39 @@ -121,7 +121,7 @@
5.40    by (cases n) (auto elim: prime_dvd_power_nat)
5.41
5.42  lemma prime_dvd_power_int_iff:
5.43 -  fixes x::int
5.44 +  fixes x::int
5.45    shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
5.46    by (cases n) (auto elim: prime_dvd_power_int)
5.47
5.48 @@ -226,14 +226,14 @@
5.49
5.50  lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
5.51  proof-
5.52 -  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
5.53 +  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
5.54    from prime_factor_nat [OF f1]
5.55    obtain p where "prime p" and "p dvd fact n + 1" by auto
5.56    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
5.57    { assume "p \<le> n"
5.58 -    from `prime p` have "p \<ge> 1"
5.59 +    from `prime p` have "p \<ge> 1"
5.60        by (cases p, simp_all)
5.61 -    with `p <= n` have "p dvd fact n"
5.62 +    with `p <= n` have "p dvd fact n"
5.63        by (intro dvd_fact_nat)
5.64      with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
5.65        by (rule dvd_diff_nat)
5.66 @@ -245,7 +245,7 @@
5.67    with `prime p` and `p <= fact n + 1` show ?thesis by auto
5.68  qed
5.69
5.70 -lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
5.71 +lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
5.72    using next_prime_bound by auto
5.73
5.74  lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
5.75 @@ -263,12 +263,12 @@
5.76
5.77  text{*Versions for type nat only*}
5.78
5.79 -lemma prime_product:
5.80 +lemma prime_product:
5.81    fixes p::nat
5.82    assumes "prime (p * q)"
5.83    shows "p = 1 \<or> q = 1"
5.84  proof -
5.85 -  from assms have
5.86 +  from assms have
5.87      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
5.88      unfolding prime_nat_def by auto
5.89    from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
5.90 @@ -278,7 +278,7 @@
5.91    then show ?thesis by (simp add: Q)
5.92  qed
5.93
5.94 -lemma prime_exp:
5.95 +lemma prime_exp:
5.96    fixes p::nat
5.97    shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
5.98  proof(induct n)
5.99 @@ -301,7 +301,7 @@
5.100    ultimately show ?case by blast
5.101  qed
5.102
5.103 -lemma prime_power_mult:
5.104 +lemma prime_power_mult:
5.105    fixes p::nat
5.106    assumes p: "prime p" and xy: "x * y = p ^ k"
5.107    shows "\<exists>i j. x = p ^i \<and> y = p^ j"
5.108 @@ -312,28 +312,28 @@
5.109    case (Suc k x y)
5.110    from Suc.prems have pxy: "p dvd x*y" by auto
5.111    from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
5.112 -  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
5.113 +  from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
5.114    {assume px: "p dvd x"
5.115      then obtain d where d: "x = p*d" unfolding dvd_def by blast
5.116      from Suc.prems d  have "p*d*y = p^Suc k" by simp
5.117      hence th: "d*y = p^k" using p0 by simp
5.118      from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
5.119 -    with d have "x = p^Suc i" by simp
5.120 +    with d have "x = p^Suc i" by simp
5.121      with ij(2) have ?case by blast}
5.122 -  moreover
5.123 +  moreover
5.124    {assume px: "p dvd y"
5.125      then obtain d where d: "y = p*d" unfolding dvd_def by blast
5.126      from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
5.127      hence th: "d*x = p^k" using p0 by simp
5.128      from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
5.129 -    with d have "y = p^Suc i" by simp
5.130 +    with d have "y = p^Suc i" by simp
5.131      with ij(2) have ?case by blast}
5.132    ultimately show ?case  using pxyc by blast
5.133  qed
5.134
5.135 -lemma prime_power_exp:
5.136 +lemma prime_power_exp:
5.137    fixes p::nat
5.138 -  assumes p: "prime p" and n: "n \<noteq> 0"
5.139 +  assumes p: "prime p" and n: "n \<noteq> 0"
5.140      and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
5.141    using n xn
5.142  proof(induct n arbitrary: k)
5.143 @@ -343,7 +343,7 @@
5.144    {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
5.145    moreover
5.146    {assume n: "n \<noteq> 0"
5.147 -    from prime_power_mult[OF p th]
5.148 +    from prime_power_mult[OF p th]
5.149      obtain i j where ij: "x = p^i" "x^n = p^j"by blast
5.150      from Suc.hyps[OF n ij(2)] have ?case .}
5.151    ultimately show ?case by blast
5.152 @@ -351,14 +351,14 @@
5.153
5.154  lemma divides_primepow:
5.155    fixes p::nat
5.156 -  assumes p: "prime p"
5.157 +  assumes p: "prime p"
5.158    shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
5.159  proof
5.160 -  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
5.161 +  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
5.162      unfolding dvd_def  apply (auto simp add: mult.commute) by blast
5.163    from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
5.164    from e ij have "p^(i + j) = p^k" by (simp add: power_add)
5.165 -  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
5.166 +  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
5.167    hence "i \<le> k" by arith
5.168    with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
5.169  next
5.170 @@ -375,16 +375,16 @@
5.171  lemma bezout_gcd_nat:
5.172    fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
5.173    using bezout_nat[of a b]
5.175 -  gcd_nat.right_neutral mult_0)
5.177 +  gcd_nat.right_neutral mult_0)
5.178
5.179  lemma gcd_bezout_sum_nat:
5.180 -  fixes a::nat
5.181 -  assumes "a * x + b * y = d"
5.182 +  fixes a::nat
5.183 +  assumes "a * x + b * y = d"
5.184    shows "gcd a b dvd d"
5.185  proof-
5.186    let ?g = "gcd a b"
5.187 -    have dv: "?g dvd a*x" "?g dvd b * y"
5.188 +    have dv: "?g dvd a*x" "?g dvd b * y"
5.189        by simp_all
5.191      show ?thesis by auto
5.192 @@ -393,19 +393,19 @@
5.193
5.194  text {* A binary form of the Chinese Remainder Theorem. *}
5.195
5.196 -lemma chinese_remainder:
5.197 +lemma chinese_remainder:
5.198    fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
5.199    shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
5.200  proof-
5.202 -  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
5.203 +  obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
5.204      and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
5.205    then have d12: "d1 = 1" "d2 =1"
5.206      by (metis ab coprime_nat)+
5.207    let ?x = "v * a * x1 + u * b * x2"
5.208    let ?q1 = "v * x1 + u * y2"
5.209    let ?q2 = "v * y1 + u * x2"
5.210 -  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
5.211 +  from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
5.212    have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
5.213      by algebra+
5.214    thus ?thesis by blast
5.215 @@ -418,14 +418,14 @@
5.216    shows "\<exists>x y. a * x = b * y + 1"
5.217  by (metis assms bezout_nat gcd_nat.left_neutral)
5.218
5.219 -lemma bezout_prime:
5.220 +lemma bezout_prime:
5.221    assumes p: "prime p" and pa: "\<not> p dvd a"
5.222    shows "\<exists>x y. a*x = Suc (p*y)"
5.223  proof-
5.224    have ap: "coprime a p"
5.225 -    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
5.226 +    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
5.227    from coprime_bezout_strong[OF ap] show ?thesis
5.228 -    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
5.229 +    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
5.230  qed
5.231
5.232  end
```
```     6.1 --- a/src/HOL/Transcendental.thy	Tue Mar 10 15:21:26 2015 +0000
6.2 +++ b/src/HOL/Transcendental.thy	Tue Mar 10 16:12:35 2015 +0000
6.3 @@ -7,7 +7,7 @@
6.4  section{*Power Series, Transcendental Functions etc.*}
6.5
6.6  theory Transcendental
6.7 -imports Fact Series Deriv NthRoot
6.8 +imports Binomial Series Deriv NthRoot
6.9  begin
6.10
6.11  lemma root_test_convergence:
6.12 @@ -81,13 +81,13 @@
6.13  lemma power_diff_1_eq:
6.14    fixes x :: "'a::{comm_ring,monoid_mult}"
6.15    shows "n \<noteq> 0 \<Longrightarrow> x^n - 1 = (x - 1) * (\<Sum>i<n. (x^i))"
6.16 -using lemma_realpow_diff_sumr2 [of x _ 1]
6.17 +using lemma_realpow_diff_sumr2 [of x _ 1]
6.18    by (cases n) auto
6.19
6.20  lemma one_diff_power_eq':
6.21    fixes x :: "'a::{comm_ring,monoid_mult}"
6.22    shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^(n - Suc i))"
6.23 -using lemma_realpow_diff_sumr2 [of 1 _ x]
6.24 +using lemma_realpow_diff_sumr2 [of 1 _ x]
6.25    by (cases n) auto
6.26
6.27  lemma one_diff_power_eq:
6.28 @@ -419,7 +419,7 @@
6.29        by auto
6.30      ultimately show ?thesis by auto
6.31    qed
6.32 -  then show ?summable and ?pos and ?neg and ?f and ?g
6.33 +  then show ?summable and ?pos and ?neg and ?f and ?g
6.34      by safe
6.35  qed
6.36
6.37 @@ -1171,16 +1171,16 @@
6.38  lemma abs_exp_cancel [simp]: "\<bar>exp x::real\<bar> = exp x"
6.39    by simp
6.40
6.41 -(*FIXME: superseded by exp_of_nat_mult*)
6.42 -lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
6.43 +(*FIXME: superseded by exp_of_nat_mult*)
6.44 +lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
6.46 -
6.47 +
6.48  text {* Strict monotonicity of exponential. *}
6.49
6.52    assumes "0 \<le> (x::real)" shows "1+x \<le> exp(x)"
6.53  using order_le_imp_less_or_eq [OF assms]
6.54 -proof
6.55 +proof
6.56    assume "0 < x"
6.57    have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
6.58      by (auto simp add: numeral_2_eq_2)
6.59 @@ -1189,7 +1189,7 @@
6.60      using `0 < x`
6.61      apply (auto  simp add:  zero_le_mult_iff)
6.62      done
6.63 -  finally show "1+x \<le> exp x"
6.64 +  finally show "1+x \<le> exp x"
6.66  next
6.67    assume "0 = x"
6.68 @@ -1443,7 +1443,7 @@
6.69  proof -
6.70    have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
6.72 -  also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
6.73 +  also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
6.74      (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
6.75      by (rule suminf_split_initial_segment)
6.76    also have "?a = 1 + x"
6.77 @@ -1536,7 +1536,7 @@
6.78    ultimately have "1 - x <= 1 / (1 + x + x\<^sup>2)"
6.79      by (elim mult_imp_le_div_pos)
6.80    also have "... <= 1 / exp x"
6.81 -    by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
6.82 +    by (metis a abs_one b exp_bound exp_gt_zero frac_le less_eq_real_def real_sqrt_abs
6.83                real_sqrt_pow2_iff real_sqrt_power)
6.84    also have "... = exp (-x)"
6.85      by (auto simp add: exp_minus divide_inverse)
6.86 @@ -1584,7 +1584,7 @@
6.87    qed
6.88    finally have "exp (x - x\<^sup>2) <= exp (ln (1 + x))" .
6.89    thus ?thesis
6.90 -    by (metis exp_le_cancel_iff)
6.91 +    by (metis exp_le_cancel_iff)
6.92  qed
6.93
6.94  lemma ln_one_minus_pos_lower_bound:
6.95 @@ -1690,7 +1690,7 @@
6.96    also have "... = 1 + (y - x) / x"
6.97      using x a by (simp add: field_simps)
6.98    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
6.99 -    using x a
6.100 +    using x a
6.101      by (intro mult_left_mono ln_add_one_self_le_self) simp_all
6.102    also have "... = y - x" using a by simp
6.103    also have "... = (y - x) * ln (exp 1)" by simp
6.104 @@ -2204,7 +2204,7 @@
6.105    unfolding powr_def exp_inj_iff by simp
6.106
6.107  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
6.108 -  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
6.109 +  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
6.110              order.strict_trans2 powr_gt_zero zero_less_one)
6.111
6.112  lemma ln_powr_bound2:
6.113 @@ -2302,7 +2302,7 @@
6.114    have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
6.115      by (auto intro!: derivative_eq_intros)
6.116    then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
6.117 -    by (auto simp add: has_field_derivative_def field_has_derivative_at)
6.118 +    by (auto simp add: has_field_derivative_def field_has_derivative_at)
6.119    then have *: "((\<lambda>y. exp (ln (1 + x * y) / y)) ---> exp x) (at 0)"
6.120      by (rule tendsto_intros)
6.121    then show ?thesis
6.122 @@ -2367,15 +2367,15 @@
6.123    unfolding cos_coeff_def sin_coeff_def
6.124    by (simp del: mult_Suc) (auto elim: oddE)
6.125
6.126 -lemma summable_norm_sin:
6.127 +lemma summable_norm_sin:
6.128    fixes x :: "'a::{real_normed_algebra_1,banach}"
6.129    shows "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
6.130 -  unfolding sin_coeff_def
6.131 +  unfolding sin_coeff_def
6.132    apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
6.133    apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
6.134    done
6.135
6.136 -lemma summable_norm_cos:
6.137 +lemma summable_norm_cos:
6.138    fixes x :: "'a::{real_normed_algebra_1,banach}"
6.139    shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
6.140    unfolding cos_coeff_def
6.141 @@ -2405,7 +2405,7 @@
6.142      by (rule sin_converges)
6.143    finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
6.144    then show ?thesis
6.145 -    using sums_unique2 sums_of_real [OF sin_converges]
6.146 +    using sums_unique2 sums_of_real [OF sin_converges]
6.147      by blast
6.148  qed
6.149
6.150 @@ -2423,7 +2423,7 @@
6.151      by (rule cos_converges)
6.152    finally have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R x^n)) sums (cos (of_real x))" .
6.153    then show ?thesis
6.154 -    using sums_unique2 sums_of_real [OF cos_converges]
6.155 +    using sums_unique2 sums_of_real [OF cos_converges]
6.156      by blast
6.157  qed
6.158
6.159 @@ -2441,22 +2441,22 @@
6.160    unfolding sin_def cos_def scaleR_conv_of_real
6.161    apply (rule DERIV_cong)
6.162    apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
6.163 -  apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff
6.164 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_sin_coeff diffs_cos_coeff
6.165                summable_minus_iff scaleR_conv_of_real [symmetric]
6.166                summable_norm_sin [THEN summable_norm_cancel]
6.167                summable_norm_cos [THEN summable_norm_cancel])
6.168    done
6.169 -
6.170 +
6.171  declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
6.172
6.173 -lemma DERIV_cos [simp]:
6.174 +lemma DERIV_cos [simp]:
6.175    fixes x :: "'a::{real_normed_field,banach}"
6.176    shows "DERIV cos x :> -sin(x)"
6.177    unfolding sin_def cos_def scaleR_conv_of_real
6.178    apply (rule DERIV_cong)
6.179    apply (rule termdiffs [where K="of_real (norm x) + 1 :: 'a"])
6.180 -  apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus
6.181 -              diffs_sin_coeff diffs_cos_coeff
6.182 +  apply (simp_all add: norm_less_p1 diffs_of_real diffs_minus suminf_minus
6.183 +              diffs_sin_coeff diffs_cos_coeff
6.184                summable_minus_iff scaleR_conv_of_real [symmetric]
6.185                summable_norm_sin [THEN summable_norm_cancel]
6.186                summable_norm_cos [THEN summable_norm_cancel])
6.187 @@ -2469,7 +2469,7 @@
6.188    shows "isCont sin x"
6.189    by (rule DERIV_sin [THEN DERIV_isCont])
6.190
6.191 -lemma isCont_cos:
6.192 +lemma isCont_cos:
6.193    fixes x :: "'a::{real_normed_field,banach}"
6.194    shows "isCont cos x"
6.195    by (rule DERIV_cos [THEN DERIV_isCont])
6.196 @@ -2481,7 +2481,7 @@
6.197
6.198  (*FIXME A CONTEXT FOR F WOULD BE BETTER*)
6.199
6.200 -lemma isCont_cos' [simp]:
6.201 +lemma isCont_cos' [simp]:
6.202    fixes f:: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
6.203    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
6.204    by (rule isCont_o2 [OF _ isCont_cos])
6.205 @@ -2545,23 +2545,23 @@
6.206  subsection {*Deriving the Addition Formulas*}
6.207
6.208  text{*The the product of two cosine series*}
6.209 -lemma cos_x_cos_y:
6.210 +lemma cos_x_cos_y:
6.211    fixes x :: "'a::{real_normed_field,banach}"
6.212 -  shows "(\<lambda>p. \<Sum>n\<le>p.
6.213 -          if even p \<and> even n
6.214 -          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
6.215 +  shows "(\<lambda>p. \<Sum>n\<le>p.
6.216 +          if even p \<and> even n
6.217 +          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
6.218           sums (cos x * cos y)"
6.219  proof -
6.220    { fix n p::nat
6.221      assume "n\<le>p"
6.222      then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
6.224 -    have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
6.225 +    have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
6.226            (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
6.227      using `n\<le>p`
6.228        by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
6.229 -  }
6.230 -  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
6.231 +  }
6.232 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
6.233                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
6.234               (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
6.235      by simp
6.236 @@ -2574,11 +2574,11 @@
6.237  qed
6.238
6.239  text{*The product of two sine series*}
6.240 -lemma sin_x_sin_y:
6.241 +lemma sin_x_sin_y:
6.242    fixes x :: "'a::{real_normed_field,banach}"
6.243 -  shows "(\<lambda>p. \<Sum>n\<le>p.
6.244 -          if even p \<and> odd n
6.245 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
6.246 +  shows "(\<lambda>p. \<Sum>n\<le>p.
6.247 +          if even p \<and> odd n
6.248 +               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
6.249           sums (sin x * sin y)"
6.250  proof -
6.251    { fix n p::nat
6.252 @@ -2594,13 +2594,13 @@
6.253          apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
6.254          done
6.255      } then
6.256 -    have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
6.257 -          (if even p \<and> odd n
6.258 +    have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
6.259 +          (if even p \<and> odd n
6.260            then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
6.261      using `n\<le>p`
6.262        by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
6.263 -  }
6.264 -  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
6.265 +  }
6.266 +  then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
6.267                 then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
6.268               (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
6.269      by simp
6.270 @@ -2612,18 +2612,18 @@
6.271    finally show ?thesis .
6.272  qed
6.273
6.274 -lemma sums_cos_x_plus_y:
6.275 +lemma sums_cos_x_plus_y:
6.276    fixes x :: "'a::{real_normed_field,banach}"
6.277    shows
6.278 -  "(\<lambda>p. \<Sum>n\<le>p. if even p
6.279 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.280 -               else 0)
6.281 +  "(\<lambda>p. \<Sum>n\<le>p. if even p
6.282 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.283 +               else 0)
6.284          sums cos (x + y)"
6.285  proof -
6.286    { fix p::nat
6.287      have "(\<Sum>n\<le>p. if even p
6.288                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.289 -                  else 0) =
6.290 +                  else 0) =
6.291            (if even p
6.292                    then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.293                    else 0)"
6.294 @@ -2637,11 +2637,11 @@
6.295      finally have "(\<Sum>n\<le>p. if even p
6.296                    then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.297                    else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
6.298 -  }
6.299 -  then have "(\<lambda>p. \<Sum>n\<le>p.
6.300 -               if even p
6.301 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.302 -               else 0)
6.303 +  }
6.304 +  then have "(\<lambda>p. \<Sum>n\<le>p.
6.305 +               if even p
6.306 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
6.307 +               else 0)
6.308          = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
6.309          by simp
6.310     also have "... sums cos (x + y)"
6.311 @@ -2649,22 +2649,22 @@
6.312     finally show ?thesis .
6.313  qed
6.314
6.317    fixes x :: "'a::{real_normed_field,banach}"
6.318    shows "cos (x + y) = cos x * cos y - sin x * sin y"
6.319  proof -
6.320    { fix n p::nat
6.321      assume "n\<le>p"
6.322 -    then have "(if even p \<and> even n
6.323 +    then have "(if even p \<and> even n
6.324                 then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
6.325 -          (if even p \<and> odd n
6.326 +          (if even p \<and> odd n
6.327                 then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
6.328 -          = (if even p
6.329 +          = (if even p
6.330                 then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
6.331        by simp
6.332 -  }
6.333 -  then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
6.334 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
6.335 +  }
6.336 +  then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
6.337 +               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
6.338          sums (cos x * cos y - sin x * sin y)"
6.339      using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
6.340      by (simp add: setsum_subtractf [symmetric])
6.341 @@ -2683,7 +2683,7 @@
6.342  lemma sin_minus [simp]:
6.343    fixes x :: "'a::{real_normed_algebra_1,banach}"
6.344    shows "sin (-x) = -sin(x)"
6.345 -using sin_minus_converges [of x]
6.346 +using sin_minus_converges [of x]
6.347  by (auto simp: sin_def summable_norm_sin [THEN summable_norm_cancel] suminf_minus sums_iff equation_minus_iff)
6.348
6.349  lemma cos_minus_converges: "(\<lambda>n. (cos_coeff n *\<^sub>R (-x)^n)) sums cos(x)"
6.350 @@ -2698,72 +2698,72 @@
6.351    fixes x :: "'a::{real_normed_algebra_1,banach}"
6.352    shows "cos (-x) = cos(x)"
6.353  using cos_minus_converges [of x]
6.354 -by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
6.355 +by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
6.356                suminf_minus sums_iff equation_minus_iff)
6.357
6.358 -
6.360 +
6.362    fixes x :: "'a::{real_normed_field,banach}"
6.363    shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
6.364  using cos_add [of x "-x"]
6.365  by (simp add: power2_eq_square algebra_simps)
6.366
6.369    fixes x :: "'a::{real_normed_field,banach}"
6.370    shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
6.372
6.375    fixes x :: "'a::{real_normed_field,banach}"
6.376    shows "cos x * cos x + sin x * sin x = 1"
6.377    using sin_cos_squared_add2 [unfolded power2_eq_square] .
6.378
6.379 -lemma sin_squared_eq:
6.380 +lemma sin_squared_eq:
6.381    fixes x :: "'a::{real_normed_field,banach}"
6.382    shows "(sin x)\<^sup>2 = 1 - (cos x)\<^sup>2"
6.383    unfolding eq_diff_eq by (rule sin_cos_squared_add)
6.384
6.385 -lemma cos_squared_eq:
6.386 +lemma cos_squared_eq:
6.387    fixes x :: "'a::{real_normed_field,banach}"
6.388    shows "(cos x)\<^sup>2 = 1 - (sin x)\<^sup>2"
6.389    unfolding eq_diff_eq by (rule sin_cos_squared_add2)
6.390
6.391 -lemma abs_sin_le_one [simp]:
6.392 +lemma abs_sin_le_one [simp]:
6.393    fixes x :: real
6.394    shows "\<bar>sin x\<bar> \<le> 1"
6.395    by (rule power2_le_imp_le, simp_all add: sin_squared_eq)
6.396
6.397 -lemma sin_ge_minus_one [simp]:
6.398 +lemma sin_ge_minus_one [simp]:
6.399    fixes x :: real
6.400    shows "-1 \<le> sin x"
6.401    using abs_sin_le_one [of x] unfolding abs_le_iff by simp
6.402
6.403 -lemma sin_le_one [simp]:
6.404 +lemma sin_le_one [simp]:
6.405    fixes x :: real
6.406    shows "sin x \<le> 1"
6.407    using abs_sin_le_one [of x] unfolding abs_le_iff by simp
6.408
6.409 -lemma abs_cos_le_one [simp]:
6.410 +lemma abs_cos_le_one [simp]:
6.411    fixes x :: real
6.412    shows "\<bar>cos x\<bar> \<le> 1"
6.413    by (rule power2_le_imp_le, simp_all add: cos_squared_eq)
6.414
6.415 -lemma cos_ge_minus_one [simp]:
6.416 +lemma cos_ge_minus_one [simp]:
6.417    fixes x :: real
6.418    shows "-1 \<le> cos x"
6.419    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
6.420
6.421 -lemma cos_le_one [simp]:
6.422 +lemma cos_le_one [simp]:
6.423    fixes x :: real
6.424    shows "cos x \<le> 1"
6.425    using abs_cos_le_one [of x] unfolding abs_le_iff by simp
6.426
6.427 -lemma cos_diff:
6.428 +lemma cos_diff:
6.429    fixes x :: "'a::{real_normed_field,banach}"
6.430    shows "cos (x - y) = cos x * cos y + sin x * sin y"
6.431    using cos_add [of x "- y"] by simp
6.432
6.433 -lemma cos_double:
6.434 +lemma cos_double:
6.435    fixes x :: "'a::{real_normed_field,banach}"
6.436    shows "cos(2*x) = (cos x)\<^sup>2 - (sin x)\<^sup>2"
6.437    using cos_add [where x=x and y=x]
6.438 @@ -2786,7 +2786,7 @@
6.439     hence define pi.*}
6.440
6.441  lemma sin_paired:
6.442 -  fixes x :: real
6.443 +  fixes x :: real
6.444    shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
6.445  proof -
6.446    have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
6.447 @@ -2797,7 +2797,7 @@
6.448  qed
6.449
6.450  lemma sin_gt_zero_02:
6.451 -  fixes x :: real
6.452 +  fixes x :: real
6.453    assumes "0 < x" and "x < 2"
6.454    shows "0 < sin x"
6.455  proof -
6.456 @@ -2824,12 +2824,12 @@
6.457  qed
6.458
6.459  lemma cos_double_less_one:
6.460 -  fixes x :: real
6.461 +  fixes x :: real
6.462    shows "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
6.463    using sin_gt_zero_02 [where x = x] by (auto simp: cos_squared_eq cos_double)
6.464
6.465  lemma cos_paired:
6.466 -  fixes x :: real
6.467 +  fixes x :: real
6.468    shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
6.469  proof -
6.470    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
6.471 @@ -2927,7 +2927,7 @@
6.472  lemma cos_pi_half [simp]: "cos (pi / 2) = 0"
6.473    by (simp add: pi_half cos_is_zero [THEN theI'])
6.474
6.475 -lemma cos_of_real_pi_half [simp]:
6.476 +lemma cos_of_real_pi_half [simp]:
6.477    fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
6.478    shows "cos ((of_real pi / 2) :: 'a) = 0"
6.479  by (metis cos_pi_half cos_of_real eq_numeral_simps(4) nonzero_of_real_divide of_real_0 of_real_numeral)
6.480 @@ -2976,7 +2976,7 @@
6.481  lemma sin_of_real_pi_half [simp]:
6.482    fixes x :: "'a :: {real_field,banach,real_normed_algebra_1}"
6.483    shows "sin ((of_real pi / 2) :: 'a) = 1"
6.484 -  using sin_pi_half
6.485 +  using sin_pi_half
6.486  by (metis sin_pi_half eq_numeral_simps(4) nonzero_of_real_divide of_real_1 of_real_numeral sin_of_real)
6.487
6.488  lemma sin_cos_eq:
6.489 @@ -2995,7 +2995,7 @@
6.490    using sin_cos_eq [of "of_real pi / 2 - x"]
6.491    by simp
6.492
6.495    fixes x :: "'a::{real_normed_field,banach}"
6.496    shows "sin (x + y) = sin x * cos y + cos x * sin y"
6.497    using cos_add [of "of_real pi / 2 - x" "-y"]
6.498 @@ -3006,7 +3006,7 @@
6.499    shows "sin (x - y) = sin x * cos y - cos x * sin y"
6.500    using sin_add [of x "- y"] by simp
6.501
6.502 -lemma sin_double:
6.503 +lemma sin_double:
6.504    fixes x :: "'a::{real_normed_field,banach}"
6.505    shows "sin(2 * x) = 2 * sin x * cos x"
6.506    using sin_add [where x=x and y=x] by simp
6.507 @@ -3017,9 +3017,9 @@
6.509
6.510  lemma sin_of_real_pi [simp]: "sin (of_real pi) = 0"
6.511 -  using sin_add [where x = "pi/2" and y = "pi/2"]
6.512 +  using sin_add [where x = "pi/2" and y = "pi/2"]
6.514 -
6.515 +
6.516  lemma cos_pi [simp]: "cos pi = -1"
6.517    using cos_add [where x = "pi/2" and y = "pi/2"] by simp
6.518
6.519 @@ -3241,7 +3241,7 @@
6.520      done
6.521  next
6.522    fix n::int
6.523 -  assume "odd n"
6.524 +  assume "odd n"
6.525    then show "cos (real n * (pi / 2)) = 0"
6.527      apply (case_tac n rule: int_cases2, simp)
6.528 @@ -3250,7 +3250,7 @@
6.529      done
6.530  qed
6.531
6.532 -lemma sin_zero_iff_int:
6.533 +lemma sin_zero_iff_int:
6.534       "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = real n * (pi/2)))"
6.535  proof safe
6.536    assume "sin x = 0"
6.537 @@ -3261,7 +3261,7 @@
6.538      done
6.539  next
6.540    fix n::int
6.541 -  assume "even n"
6.542 +  assume "even n"
6.543    then show "sin (real n * (pi / 2)) = 0"
6.545      apply (case_tac n rule: int_cases2, simp)
6.546 @@ -3271,8 +3271,8 @@
6.547  qed
6.548
6.549  lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
6.550 -  apply (simp only: sin_zero_iff_int)
6.551 -  apply (safe elim!: evenE)
6.552 +  apply (simp only: sin_zero_iff_int)
6.553 +  apply (safe elim!: evenE)
6.555    using dvd_triv_left by fastforce
6.556
6.557 @@ -3337,7 +3337,7 @@
6.558      using pi_ge_two and assms by auto
6.559    from cos_monotone_0_pi'[OF this] show ?thesis
6.560      unfolding minus_sin_cos_eq[symmetric]
6.561 -    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
6.562 +    by (metis minus_sin_cos_eq mult.right_neutral neg_le_iff_le of_real_def real_scaleR_def)
6.563  qed
6.564
6.565  lemma sin_x_le_x:
6.566 @@ -3401,14 +3401,14 @@
6.567
6.569    fixes x :: "'a::{real_normed_field,banach}"
6.570 -  shows
6.571 +  shows
6.572       "\<lbrakk>cos x \<noteq> 0; cos y \<noteq> 0; cos (x + y) \<noteq> 0\<rbrakk>
6.573        \<Longrightarrow> tan(x + y) = (tan(x) + tan(y))/(1 - tan(x) * tan(y))"
6.575
6.576  lemma tan_double:
6.577    fixes x :: "'a::{real_normed_field,banach}"
6.578 -  shows
6.579 +  shows
6.580       "\<lbrakk>cos x \<noteq> 0; cos (2 * x) \<noteq> 0\<rbrakk>
6.581        \<Longrightarrow> tan (2 * x) = (2 * tan x) / (1 - (tan x)\<^sup>2)"
6.583 @@ -3463,7 +3463,7 @@
6.584
6.585  lemma continuous_within_tan [continuous_intros]:
6.586    fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
6.587 -  shows
6.588 +  shows
6.589    "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
6.590    unfolding continuous_within by (rule tendsto_tan)
6.591
6.592 @@ -4200,7 +4200,7 @@
6.593    shows "x\<^sup>2 < 1"
6.594  proof -
6.595    have "\<bar>x\<^sup>2\<bar> < 1"
6.596 -    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
6.597 +    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff)
6.598    thus ?thesis using zero_le_power2 by auto
6.599  qed
6.600
6.601 @@ -4594,7 +4594,7 @@
6.602      done
6.603    show ?thesis
6.604    proof (cases "0::real" y rule: linorder_cases)
6.605 -    case less
6.606 +    case less
6.607        then show ?thesis by (rule polar_ex1)
6.608    next
6.609      case equal
6.610 @@ -4602,7 +4602,7 @@
6.611          by (force simp add: intro!: cos_zero sin_zero)
6.612    next
6.613      case greater
6.614 -      then show ?thesis
6.615 +      then show ?thesis
6.616       using polar_ex1 [where y="-y"]
6.617      by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
6.618    qed
```
```     7.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Tue Mar 10 15:21:26 2015 +0000
7.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Tue Mar 10 16:12:35 2015 +0000
7.3 @@ -5,14 +5,14 @@
7.4  section {* A Formulation of the Birthday Paradox *}
7.5
7.7 -imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
7.8 +imports Main "~~/src/HOL/Binomial" "~~/src/HOL/Library/FuncSet"
7.9  begin
7.10
7.11  section {* Cardinality *}
7.12
7.13  lemma card_product_dependent:
7.14    assumes "finite S"
7.15 -  assumes "\<forall>x \<in> S. finite (T x)"
7.16 +  assumes "\<forall>x \<in> S. finite (T x)"
7.17    shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
7.18    using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def)
7.19
7.20 @@ -30,7 +30,7 @@
7.21      from `finite S` this have "finite (extensional_funcset S (T - {x}))"
7.22        by (rule finite_PiE)
7.23      moreover
7.24 -    have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
7.25 +    have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto
7.26      ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
7.27        by (auto intro: finite_subset)
7.28    } note finite_delete = this
7.29 @@ -62,7 +62,7 @@
7.30    have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
7.31    from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
7.32      by (auto intro!: finite_PiE)
7.33 -  have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
7.34 +  have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto
7.35    from assms this finite subset show ?thesis
7.36      by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on setprod_constant)
7.37  qed
```