renaming HOL/Fact.thy -> Binomial.thy
authorpaulson <lp15@cam.ac.uk>
Tue Mar 10 16:12:35 2015 +0000 (2015-03-10)
changeset 59669de7792ea4090
parent 59668 1c937d56a70a
child 59670 dee043d19729
child 59730 b7c394c7a619
renaming HOL/Fact.thy -> Binomial.thy
src/HOL/Binomial.thy
src/HOL/Fact.thy
src/HOL/Import/Import_Setup.thy
src/HOL/Library/Permutations.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Transcendental.thy
src/HOL/ex/Birthday_Paradox.thy
     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.61 +declare transfer_morphism_nat_int[transfer add return:
    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.72 +declare transfer_morphism_int_nat[transfer add return:
    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.97 +  by (simp add: nat_add_distrib algebra_simps int_mult)
    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.216 +apply (auto dest!: less_imp_Suc_add)
   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.276 +lemma fact_add_num_eq_if_nat:
   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.280 +lemma fact_add_num_eq_if2_nat:
   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.289 +  then show ?case by (simp add: add_le_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.377 +   apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   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.403 +  by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   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.679 +   apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
   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.713 +  unfolding power_add[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.965 +by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
   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.976 +    apply (metis add.assoc add.commute 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.61 -declare transfer_morphism_nat_int[transfer add return:
    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.72 -declare transfer_morphism_int_nat[transfer add return:
    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.97 -  by (simp add: nat_add_distrib algebra_simps int_mult)
    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.216 -apply (auto dest!: less_imp_Suc_add)
   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.276 -lemma fact_add_num_eq_if_nat:
   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.280 -lemma fact_add_num_eq_if2_nat:
   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.289 -  then show ?case by (simp add: add_le_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.377 -   apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   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.403 -  by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
   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.679 -   apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
   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.713 -  unfolding power_add[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.965 -by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
   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.976 -    apply (metis add.assoc add.commute 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.20    apply (simp add: prime_def)
    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.174 -by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute 
   5.175 -  gcd_nat.right_neutral mult_0) 
   5.176 +by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
   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.190      from dvd_add[OF dv] assms
   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.201    from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   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.45    by (induct n) (auto simp add: real_of_nat_Suc distrib_left exp_add mult.commute)
    6.46 -  
    6.47 +
    6.48  text {* Strict monotonicity of exponential. *}
    6.49  
    6.50 -lemma exp_ge_add_one_self_aux: 
    6.51 +lemma exp_ge_add_one_self_aux:
    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.65      by (simp add: exp_def)
    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.71      by (simp add: exp_def)
    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.223        by (metis div_add power_add le_add_diff_inverse odd_add)
   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.315 -theorem cos_add: 
   6.316 +theorem cos_add:
   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.359 -lemma sin_cos_squared_add [simp]: 
   6.360 +
   6.361 +lemma sin_cos_squared_add [simp]:
   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.367 -lemma sin_cos_squared_add2 [simp]:  
   6.368 +lemma sin_cos_squared_add2 [simp]:
   6.369    fixes x :: "'a::{real_normed_field,banach}"
   6.370    shows "(cos x)\<^sup>2 + (sin x)\<^sup>2 = 1"
   6.371    by (subst add.commute, rule sin_cos_squared_add)
   6.372  
   6.373 -lemma sin_cos_squared_add3 [simp]:  
   6.374 +lemma sin_cos_squared_add3 [simp]:
   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.493 -lemma sin_add: 
   6.494 +lemma sin_add:
   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.508    by (simp add: cos_of_real)
   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.513    by (simp add: sin_of_real)
   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.526      apply (simp add: cos_zero_iff)
   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.544      apply (simp add: sin_zero_iff)
   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.554    apply (simp_all add: field_simps)
   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.568  lemma tan_add:
   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.574        by (simp add: add_tan_eq lemma_tan_add1 field_simps) (simp add: tan_def)
   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.582    using tan_add [of x x] by (simp add: power2_eq_square)
   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.6  theory Birthday_Paradox
     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