Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
authorpaulson <lp15@cam.ac.uk>
Tue Mar 10 15:20:40 2015 +0000 (2015-03-10)
changeset 59667651ea265d568
parent 59665 37adca7fd48f
child 59668 1c937d56a70a
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
src/Doc/Tutorial/Sets/Examples.thy
src/HOL/Algebra/Exponent.thy
src/HOL/Fact.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Int.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/NthRoot_Limits.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/ROOT
src/HOL/Rat.thy
     1.1 --- a/src/Doc/Tutorial/Sets/Examples.thy	Tue Mar 10 11:56:32 2015 +0100
     1.2 +++ b/src/Doc/Tutorial/Sets/Examples.thy	Tue Mar 10 15:20:40 2015 +0000
     1.3 @@ -1,4 +1,4 @@
     1.4 -theory Examples imports "~~/src/HOL/Number_Theory/Binomial" begin
     1.5 +theory Examples imports Complex_Main begin
     1.6  
     1.7  declare [[eta_contract = false]]
     1.8  
     2.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Mar 10 11:56:32 2015 +0100
     2.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Mar 10 15:20:40 2015 +0000
     2.3 @@ -6,7 +6,7 @@
     2.4  *)
     2.5  
     2.6  theory Exponent
     2.7 -imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Number_Theory/Binomial"
     2.8 +imports Main "~~/src/HOL/Number_Theory/Primes"
     2.9  begin
    2.10  
    2.11  section {*Sylow's Theorem*}
    2.12 @@ -35,7 +35,7 @@
    2.13  
    2.14  lemma prime_dvd_cases:
    2.15    fixes p::nat
    2.16 -  shows "[| p*k dvd m*n;  prime p |]  
    2.17 +  shows "[| p*k dvd m*n;  prime p |]
    2.18     ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    2.19  apply (simp add: prime_iff)
    2.20  apply (frule dvd_mult_left)
    2.21 @@ -48,10 +48,10 @@
    2.22  done
    2.23  
    2.24  
    2.25 -lemma prime_power_dvd_cases [rule_format (no_asm)]: 
    2.26 +lemma prime_power_dvd_cases [rule_format (no_asm)]:
    2.27  fixes p::nat
    2.28    shows "prime p
    2.29 -  ==> \<forall>m n. p^c dvd m*n -->  
    2.30 +  ==> \<forall>m n. p^c dvd m*n -->
    2.31          (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    2.32  apply (induct c)
    2.33  apply (metis dvd_1_left nat_power_eq_Suc_0_iff one_is_add)
    2.34 @@ -119,7 +119,7 @@
    2.35  lemma power_Suc_exponent_Not_dvd:
    2.36    "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
    2.37  apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
    2.38 - prefer 2 apply simp 
    2.39 + prefer 2 apply simp
    2.40  apply (rule ccontr)
    2.41  apply (drule exponent_ge, auto)
    2.42  done
    2.43 @@ -147,7 +147,7 @@
    2.44  by (metis mult_dvd_mono power_exponent_dvd)
    2.45  
    2.46  (* exponent_mult_add, opposite inclusion *)
    2.47 -lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
    2.48 +lemma exponent_mult_add2: "[| a > 0; b > 0 |]
    2.49    ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
    2.50  apply (case_tac "prime p")
    2.51  apply (rule leI, clarify)
    2.52 @@ -155,7 +155,7 @@
    2.53  apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
    2.54  apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
    2.55    prefer 3 apply assumption
    2.56 - prefer 2 apply simp 
    2.57 + prefer 2 apply simp
    2.58  apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
    2.59   apply (assumption, force, simp)
    2.60  apply (blast dest: power_Suc_exponent_Not_dvd)
    2.61 @@ -185,7 +185,7 @@
    2.62  text{*Main Combinatorial Argument*}
    2.63  
    2.64  lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
    2.65 -by (simp add: mult.commute[of a b]) 
    2.66 +by (simp add: mult.commute[of a b])
    2.67  
    2.68  lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
    2.69  apply (rule_tac P = "%x. x <= b * c" in subst)
    2.70 @@ -204,7 +204,7 @@
    2.71  apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2_nat gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less mult.commute not_add_less2 xt1(10))
    2.72  done
    2.73  
    2.74 -lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
    2.75 +lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]
    2.76    ==> (p^r) dvd (p^a) - k"
    2.77  apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
    2.78  apply (subgoal_tac "p^r dvd p^a*m")
    2.79 @@ -220,7 +220,7 @@
    2.80    "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
    2.81  by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
    2.82  
    2.83 -lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
    2.84 +lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]
    2.85    ==> (p^r) dvd (p^a)*m - k"
    2.86  apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
    2.87  apply (subgoal_tac "p^r dvd p^a*m")
    2.88 @@ -231,7 +231,7 @@
    2.89  apply (drule less_imp_Suc_add, auto)
    2.90  done
    2.91  
    2.92 -lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
    2.93 +lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]
    2.94    ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
    2.95  apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
    2.96  done
    2.97 @@ -241,16 +241,16 @@
    2.98  
    2.99  (*The bound K is needed; otherwise it's too weak to be used.*)
   2.100  lemma p_not_div_choose_lemma [rule_format]:
   2.101 -  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   2.102 +  "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
   2.103     ==> k<K --> exponent p ((j+k) choose k) = 0"
   2.104  apply (cases "prime p")
   2.105 - prefer 2 apply simp 
   2.106 + prefer 2 apply simp
   2.107  apply (induct k)
   2.108  apply (simp (no_asm))
   2.109  (*induction step*)
   2.110  apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
   2.111   prefer 2 apply (simp, clarify)
   2.112 -apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
   2.113 +apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) =
   2.114                      exponent p (Suc k)")
   2.115   txt{*First, use the assumed equation.  We simplify the LHS to
   2.116    @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
   2.117 @@ -276,7 +276,7 @@
   2.118  lemma const_p_fac_right:
   2.119    "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   2.120  apply (case_tac "prime p")
   2.121 - prefer 2 apply simp 
   2.122 + prefer 2 apply simp
   2.123  apply (frule_tac a = a in zero_less_prime_power)
   2.124  apply (rule_tac K = "p^a" in p_not_div_choose)
   2.125     apply simp
   2.126 @@ -294,14 +294,14 @@
   2.127  lemma const_p_fac:
   2.128    "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   2.129  apply (case_tac "prime p")
   2.130 - prefer 2 apply simp 
   2.131 + prefer 2 apply simp
   2.132  apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   2.133   prefer 2 apply (force simp add: prime_iff)
   2.134  txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
   2.135    insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   2.136    first
   2.137    transform the binomial coefficient, then use @{text exponent_mult_add}.*}
   2.138 -apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
   2.139 +apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
   2.140                      a + exponent p m")
   2.141   apply (simp add: exponent_mult_add)
   2.142  txt{*one subgoal left!*}
     3.1 --- a/src/HOL/Fact.thy	Tue Mar 10 11:56:32 2015 +0100
     3.2 +++ b/src/HOL/Fact.thy	Tue Mar 10 15:20:40 2015 +0000
     3.3 @@ -15,7 +15,7 @@
     3.4    fixes fact :: "'a \<Rightarrow> 'a"
     3.5  
     3.6  instantiation nat :: fact
     3.7 -begin 
     3.8 +begin
     3.9  
    3.10  fun
    3.11    fact_nat :: "nat \<Rightarrow> nat"
    3.12 @@ -31,11 +31,11 @@
    3.13  
    3.14  instantiation int :: fact
    3.15  
    3.16 -begin 
    3.17 +begin
    3.18  
    3.19  definition
    3.20    fact_int :: "int \<Rightarrow> int"
    3.21 -where  
    3.22 +where
    3.23    "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
    3.24  
    3.25  instance proof qed
    3.26 @@ -55,7 +55,7 @@
    3.27    "x >= (0::int) \<Longrightarrow> fact x >= 0"
    3.28    by (auto simp add: fact_int_def)
    3.29  
    3.30 -declare transfer_morphism_nat_int[transfer add return: 
    3.31 +declare transfer_morphism_nat_int[transfer add return:
    3.32      transfer_nat_int_factorial transfer_nat_int_factorial_closure]
    3.33  
    3.34  lemma transfer_int_nat_factorial:
    3.35 @@ -66,7 +66,7 @@
    3.36    "is_nat x \<Longrightarrow> fact x >= 0"
    3.37    by (auto simp add: fact_int_def)
    3.38  
    3.39 -declare transfer_morphism_int_nat[transfer add return: 
    3.40 +declare transfer_morphism_int_nat[transfer add return:
    3.41      transfer_int_nat_factorial transfer_int_nat_factorial_closure]
    3.42  
    3.43  
    3.44 @@ -87,10 +87,10 @@
    3.45  lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
    3.46    by simp
    3.47  
    3.48 -lemma fact_plus_one_int: 
    3.49 +lemma fact_plus_one_int:
    3.50    assumes "n >= 0"
    3.51    shows "fact ((n::int) + 1) = (n + 1) * fact n"
    3.52 -  using assms unfolding fact_int_def 
    3.53 +  using assms unfolding fact_int_def
    3.54    by (simp add: nat_add_distrib algebra_simps int_mult)
    3.55  
    3.56  lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
    3.57 @@ -153,7 +153,7 @@
    3.58    apply auto
    3.59    done
    3.60  
    3.61 -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
    3.62 +lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
    3.63    {i..j+1} = {i..j} Un {j+1}"
    3.64    by auto
    3.65  
    3.66 @@ -199,7 +199,7 @@
    3.67      case (Suc d')
    3.68      have "fact (n + Suc d') div fact n = Suc (n + d') * fact (n + d') div fact n"
    3.69        by simp
    3.70 -    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}" 
    3.71 +    also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
    3.72        unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
    3.73      also have "... = \<Prod>{n + 1..n + Suc d'}"
    3.74        by (simp add: atLeastAtMostSuc_conv setprod.insert)
    3.75 @@ -224,7 +224,7 @@
    3.76    apply arith
    3.77  done
    3.78  
    3.79 -lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow> 
    3.80 +lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
    3.81      fact (m + k) >= fact m"
    3.82    apply (case_tac "m < 0")
    3.83    apply auto
    3.84 @@ -266,7 +266,7 @@
    3.85    apply auto
    3.86  done
    3.87  
    3.88 -lemma fact_num_eq_if_nat: "fact (m::nat) = 
    3.89 +lemma fact_num_eq_if_nat: "fact (m::nat) =
    3.90    (if m=0 then 1 else m * fact (m - 1))"
    3.91  by (cases m) auto
    3.92  
    3.93 @@ -275,7 +275,7 @@
    3.94  by (cases "m + n") auto
    3.95  
    3.96  lemma fact_add_num_eq_if2_nat:
    3.97 -  "fact ((m::nat) + n) = 
    3.98 +  "fact ((m::nat) + n) =
    3.99      (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
   3.100  by (cases m) auto
   3.101  
   3.102 @@ -339,7 +339,7 @@
   3.103  lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
   3.104    by simp
   3.105  
   3.106 -lemma choose_reduce_nat: 
   3.107 +lemma choose_reduce_nat:
   3.108    "0 < (n::nat) \<Longrightarrow> 0 < k \<Longrightarrow>
   3.109      (n choose k) = ((n - 1) choose (k - 1)) + ((n - 1) choose k)"
   3.110    by (metis Suc_diff_1 binomial.simps(2) neq0_conv)
   3.111 @@ -404,7 +404,7 @@
   3.112      {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}"
   3.113    apply safe
   3.114       apply (auto intro: finite_subset [THEN card_insert_disjoint])
   3.115 -  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if 
   3.116 +  by (metis (full_types) Diff_insert_absorb Set.set_insert Zero_neq_Suc card_Diff_singleton_if
   3.117       card_eq_0_iff diff_Suc_1 in_mono subset_insert_iff)
   3.118  
   3.119  lemma finite_bex_subset [simp]:
   3.120 @@ -455,7 +455,7 @@
   3.121  subsection {* The binomial theorem (courtesy of Tobias Nipkow): *}
   3.122  
   3.123  text{* Avigad's version, generalized to any commutative ring *}
   3.124 -theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n = 
   3.125 +theorem binomial_ring: "(a+b::'a::{comm_ring_1,power})^n =
   3.126    (\<Sum>k=0..n. (of_nat (n choose k)) * a^k * b^(n-k))" (is "?P n")
   3.127  proof (induct n)
   3.128    case 0 then show "?P 0" by simp
   3.129 @@ -465,7 +465,7 @@
   3.130      by auto
   3.131    have decomp2: "{0..n} = {0} Un {1..n}"
   3.132      by auto
   3.133 -  have "(a+b)^(n+1) = 
   3.134 +  have "(a+b)^(n+1) =
   3.135        (a+b) * (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
   3.136      using Suc.hyps by simp
   3.137    also have "\<dots> = a*(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
   3.138 @@ -476,14 +476,14 @@
   3.139      by (auto simp add: setsum_right_distrib ac_simps)
   3.140    also have "\<dots> = (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
   3.141                    (\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
   3.142 -    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps  
   3.143 +    by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps
   3.144          del:setsum_cl_ivl_Suc)
   3.145    also have "\<dots> = a^(n+1) + b^(n+1) +
   3.146                    (\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
   3.147                    (\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
   3.148      by (simp add: decomp2)
   3.149    also have
   3.150 -      "\<dots> = a^(n+1) + b^(n+1) + 
   3.151 +      "\<dots> = a^(n+1) + b^(n+1) +
   3.152              (\<Sum>k=1..n. of_nat(n+1 choose k) * a^k * b^(n+1-k))"
   3.153      by (auto simp add: field_simps setsum.distrib [symmetric] choose_reduce_nat)
   3.154    also have "\<dots> = (\<Sum>k=0..n+1. of_nat (n+1 choose k) * a^k * b^(n+1-k))"
   3.155 @@ -518,7 +518,7 @@
   3.156        by simp
   3.157      from n h th0
   3.158      have "fact k * fact (n - k) * (n choose k) =
   3.159 -        k * (fact h * fact (m - h) * (m choose h)) + 
   3.160 +        k * (fact h * fact (m - h) * (m choose h)) +
   3.161          (m - h) * (fact k * fact (m - k) * (m choose k))"
   3.162        by (simp add: field_simps)
   3.163      also have "\<dots> = (k + (m - h)) * fact m"
   3.164 @@ -537,4 +537,644 @@
   3.165    using binomial_fact_lemma[OF kn]
   3.166    by (simp add: field_simps of_nat_mult [symmetric])
   3.167  
   3.168 +lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
   3.169 +  using binomial [of 1 "1" n]
   3.170 +  by (simp add: numeral_2_eq_2)
   3.171 +
   3.172 +lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
   3.173 +  by (induct n) auto
   3.174 +
   3.175 +lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
   3.176 +  by (induct n) auto
   3.177 +
   3.178 +lemma natsum_reverse_index:
   3.179 +  fixes m::nat
   3.180 +  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)"
   3.181 +  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
   3.182 +
   3.183 +text{*NW diagonal sum property*}
   3.184 +lemma sum_choose_diagonal:
   3.185 +  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
   3.186 +proof -
   3.187 +  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
   3.188 +    by (rule natsum_reverse_index) (simp add: assms)
   3.189 +  also have "... = Suc (n-m+m) choose m"
   3.190 +    by (rule sum_choose_lower)
   3.191 +  also have "... = Suc n choose m" using assms
   3.192 +    by simp
   3.193 +  finally show ?thesis .
   3.194 +qed
   3.195 +
   3.196 +subsection{* Pochhammer's symbol : generalized rising factorial *}
   3.197 +
   3.198 +text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
   3.199 +
   3.200 +definition "pochhammer (a::'a::comm_semiring_1) n =
   3.201 +  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
   3.202 +
   3.203 +lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
   3.204 +  by (simp add: pochhammer_def)
   3.205 +
   3.206 +lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
   3.207 +  by (simp add: pochhammer_def)
   3.208 +
   3.209 +lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
   3.210 +  by (simp add: pochhammer_def)
   3.211 +
   3.212 +lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   3.213 +  by (simp add: pochhammer_def)
   3.214 +
   3.215 +lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
   3.216 +proof -
   3.217 +  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
   3.218 +  then show ?thesis by (simp add: field_simps)
   3.219 +qed
   3.220 +
   3.221 +lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
   3.222 +proof -
   3.223 +  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
   3.224 +  then show ?thesis by simp
   3.225 +qed
   3.226 +
   3.227 +
   3.228 +lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
   3.229 +proof (cases n)
   3.230 +  case 0
   3.231 +  then show ?thesis by simp
   3.232 +next
   3.233 +  case (Suc n)
   3.234 +  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
   3.235 +qed
   3.236 +
   3.237 +lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
   3.238 +proof (cases "n = 0")
   3.239 +  case True
   3.240 +  then show ?thesis by (simp add: pochhammer_Suc_setprod)
   3.241 +next
   3.242 +  case False
   3.243 +  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
   3.244 +  have eq: "insert 0 {1 .. n} = {0..n}" by auto
   3.245 +  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)"
   3.246 +    apply (rule setprod.reindex_cong [where l = Suc])
   3.247 +    using False
   3.248 +    apply (auto simp add: fun_eq_iff field_simps)
   3.249 +    done
   3.250 +  show ?thesis
   3.251 +    apply (simp add: pochhammer_def)
   3.252 +    unfolding setprod.insert [OF *, unfolded eq]
   3.253 +    using ** apply (simp add: field_simps)
   3.254 +    done
   3.255 +qed
   3.256 +
   3.257 +lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
   3.258 +  unfolding fact_altdef_nat
   3.259 +  apply (cases n)
   3.260 +   apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
   3.261 +  apply (rule setprod.reindex_cong [where l = Suc])
   3.262 +    apply (auto simp add: fun_eq_iff)
   3.263 +  done
   3.264 +
   3.265 +lemma pochhammer_of_nat_eq_0_lemma:
   3.266 +  assumes "k > n"
   3.267 +  shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
   3.268 +proof (cases "n = 0")
   3.269 +  case True
   3.270 +  then show ?thesis
   3.271 +    using assms by (cases k) (simp_all add: pochhammer_rec)
   3.272 +next
   3.273 +  case False
   3.274 +  from assms obtain h where "k = Suc h" by (cases k) auto
   3.275 +  then show ?thesis
   3.276 +    by (simp add: pochhammer_Suc_setprod)
   3.277 +       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
   3.278 +qed
   3.279 +
   3.280 +lemma pochhammer_of_nat_eq_0_lemma':
   3.281 +  assumes kn: "k \<le> n"
   3.282 +  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0"
   3.283 +proof (cases k)
   3.284 +  case 0
   3.285 +  then show ?thesis by simp
   3.286 +next
   3.287 +  case (Suc h)
   3.288 +  then show ?thesis
   3.289 +    apply (simp add: pochhammer_Suc_setprod)
   3.290 +    using Suc kn apply (auto simp add: algebra_simps)
   3.291 +    done
   3.292 +qed
   3.293 +
   3.294 +lemma pochhammer_of_nat_eq_0_iff:
   3.295 +  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
   3.296 +  (is "?l = ?r")
   3.297 +  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
   3.298 +    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
   3.299 +  by (auto simp add: not_le[symmetric])
   3.300 +
   3.301 +lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
   3.302 +  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
   3.303 +  apply (cases n)
   3.304 +   apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
   3.305 +  apply (metis leD not_less_eq)
   3.306 +  done
   3.307 +
   3.308 +lemma pochhammer_eq_0_mono:
   3.309 +  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
   3.310 +  unfolding pochhammer_eq_0_iff by auto
   3.311 +
   3.312 +lemma pochhammer_neq_0_mono:
   3.313 +  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
   3.314 +  unfolding pochhammer_eq_0_iff by auto
   3.315 +
   3.316 +lemma pochhammer_minus:
   3.317 +  assumes kn: "k \<le> n"
   3.318 +  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
   3.319 +proof (cases k)
   3.320 +  case 0
   3.321 +  then show ?thesis by simp
   3.322 +next
   3.323 +  case (Suc h)
   3.324 +  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
   3.325 +    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
   3.326 +    by auto
   3.327 +  show ?thesis
   3.328 +    unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
   3.329 +    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
   3.330 +       (auto simp: of_nat_diff)
   3.331 +qed
   3.332 +
   3.333 +lemma pochhammer_minus':
   3.334 +  assumes kn: "k \<le> n"
   3.335 +  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
   3.336 +  unfolding pochhammer_minus[OF kn, where b=b]
   3.337 +  unfolding mult.assoc[symmetric]
   3.338 +  unfolding power_add[symmetric]
   3.339 +  by simp
   3.340 +
   3.341 +lemma pochhammer_same: "pochhammer (- of_nat n) n =
   3.342 +    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
   3.343 +  unfolding pochhammer_minus[OF le_refl[of n]]
   3.344 +  by (simp add: of_nat_diff pochhammer_fact)
   3.345 +
   3.346 +
   3.347 +subsection{* Generalized binomial coefficients *}
   3.348 +
   3.349 +definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   3.350 +  where "a gchoose n =
   3.351 +    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
   3.352 +
   3.353 +lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
   3.354 +  apply (simp_all add: gbinomial_def)
   3.355 +  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
   3.356 +   apply (simp del:setprod_zero_iff)
   3.357 +  apply simp
   3.358 +  done
   3.359 +
   3.360 +lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
   3.361 +proof (cases "n = 0")
   3.362 +  case True
   3.363 +  then show ?thesis by simp
   3.364 +next
   3.365 +  case False
   3.366 +  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
   3.367 +  have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
   3.368 +    by auto
   3.369 +  from False show ?thesis
   3.370 +    by (simp add: pochhammer_def gbinomial_def field_simps
   3.371 +      eq setprod.distrib[symmetric])
   3.372 +qed
   3.373 +
   3.374 +lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
   3.375 +proof -
   3.376 +  { assume kn: "k > n"
   3.377 +    then have ?thesis
   3.378 +      by (subst binomial_eq_0[OF kn])
   3.379 +         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
   3.380 +  moreover
   3.381 +  { assume "k=0" then have ?thesis by simp }
   3.382 +  moreover
   3.383 +  { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
   3.384 +    from k0 obtain h where h: "k = Suc h" by (cases k) auto
   3.385 +    from h
   3.386 +    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
   3.387 +      by (subst setprod_constant) auto
   3.388 +    have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
   3.389 +        using h kn
   3.390 +      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
   3.391 +         (auto simp: of_nat_diff)
   3.392 +    have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
   3.393 +        "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
   3.394 +        eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
   3.395 +      using h kn by auto
   3.396 +    from eq[symmetric]
   3.397 +    have ?thesis using kn
   3.398 +      apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
   3.399 +        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
   3.400 +      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
   3.401 +        of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
   3.402 +      unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
   3.403 +      unfolding mult.assoc[symmetric]
   3.404 +      unfolding setprod.distrib[symmetric]
   3.405 +      apply simp
   3.406 +      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
   3.407 +      apply (auto simp: of_nat_diff)
   3.408 +      done
   3.409 +  }
   3.410 +  moreover
   3.411 +  have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith
   3.412 +  ultimately show ?thesis by blast
   3.413 +qed
   3.414 +
   3.415 +lemma gbinomial_1[simp]: "a gchoose 1 = a"
   3.416 +  by (simp add: gbinomial_def)
   3.417 +
   3.418 +lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
   3.419 +  by (simp add: gbinomial_def)
   3.420 +
   3.421 +lemma gbinomial_mult_1:
   3.422 +  "a * (a gchoose n) =
   3.423 +    of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")
   3.424 +proof -
   3.425 +  have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
   3.426 +    unfolding gbinomial_pochhammer
   3.427 +      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
   3.428 +    by (simp add:  field_simps del: of_nat_Suc)
   3.429 +  also have "\<dots> = ?l" unfolding gbinomial_pochhammer
   3.430 +    by (simp add: field_simps)
   3.431 +  finally show ?thesis ..
   3.432 +qed
   3.433 +
   3.434 +lemma gbinomial_mult_1':
   3.435 +    "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   3.436 +  by (simp add: mult.commute gbinomial_mult_1)
   3.437 +
   3.438 +lemma gbinomial_Suc:
   3.439 +    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
   3.440 +  by (simp add: gbinomial_def)
   3.441 +
   3.442 +lemma gbinomial_mult_fact:
   3.443 +  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
   3.444 +    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   3.445 +  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
   3.446 +
   3.447 +lemma gbinomial_mult_fact':
   3.448 +  "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
   3.449 +    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   3.450 +  using gbinomial_mult_fact[of k a]
   3.451 +  by (subst mult.commute)
   3.452 +
   3.453 +
   3.454 +lemma gbinomial_Suc_Suc:
   3.455 +  "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
   3.456 +proof (cases k)
   3.457 +  case 0
   3.458 +  then show ?thesis by simp
   3.459 +next
   3.460 +  case (Suc h)
   3.461 +  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
   3.462 +    apply (rule setprod.reindex_cong [where l = Suc])
   3.463 +      using Suc
   3.464 +      apply auto
   3.465 +    done
   3.466 +  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
   3.467 +    ((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)"
   3.468 +    apply (simp add: Suc field_simps del: fact_Suc)
   3.469 +    unfolding gbinomial_mult_fact'
   3.470 +    apply (subst fact_Suc)
   3.471 +    unfolding of_nat_mult
   3.472 +    apply (subst mult.commute)
   3.473 +    unfolding mult.assoc
   3.474 +    unfolding gbinomial_mult_fact
   3.475 +    apply (simp add: field_simps)
   3.476 +    done
   3.477 +  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
   3.478 +    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
   3.479 +    by (simp add: field_simps Suc)
   3.480 +  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
   3.481 +    using eq0
   3.482 +    by (simp add: Suc setprod_nat_ivl_1_Suc)
   3.483 +  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
   3.484 +    unfolding gbinomial_mult_fact ..
   3.485 +  finally show ?thesis by (simp del: fact_Suc)
   3.486 +qed
   3.487 +
   3.488 +lemma gbinomial_reduce_nat:
   3.489 +  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
   3.490 +by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
   3.491 +
   3.492 +
   3.493 +lemma binomial_symmetric:
   3.494 +  assumes kn: "k \<le> n"
   3.495 +  shows "n choose k = n choose (n - k)"
   3.496 +proof-
   3.497 +  from kn have kn': "n - k \<le> n" by arith
   3.498 +  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
   3.499 +  have "fact k * fact (n - k) * (n choose k) =
   3.500 +    fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
   3.501 +  then show ?thesis using kn by simp
   3.502 +qed
   3.503 +
   3.504 +text{*Contributed by Manuel Eberl, generalised by LCP.
   3.505 +  Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
   3.506 +lemma gbinomial_altdef_of_nat:
   3.507 +  fixes k :: nat
   3.508 +    and x :: "'a :: {field_char_0,field_inverse_zero}"
   3.509 +  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
   3.510 +proof -
   3.511 +  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
   3.512 +    unfolding gbinomial_def
   3.513 +    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
   3.514 +  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
   3.515 +    unfolding fact_eq_rev_setprod_nat of_nat_setprod
   3.516 +    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
   3.517 +  finally show ?thesis .
   3.518 +qed
   3.519 +
   3.520 +lemma gbinomial_ge_n_over_k_pow_k:
   3.521 +  fixes k :: nat
   3.522 +    and x :: "'a :: linordered_field_inverse_zero"
   3.523 +  assumes "of_nat k \<le> x"
   3.524 +  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
   3.525 +proof -
   3.526 +  have x: "0 \<le> x"
   3.527 +    using assms of_nat_0_le_iff order_trans by blast
   3.528 +  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
   3.529 +    by (simp add: setprod_constant)
   3.530 +  also have "\<dots> \<le> x gchoose k"
   3.531 +    unfolding gbinomial_altdef_of_nat
   3.532 +  proof (safe intro!: setprod_mono)
   3.533 +    fix i :: nat
   3.534 +    assume ik: "i < k"
   3.535 +    from assms have "x * of_nat i \<ge> of_nat (i * k)"
   3.536 +      by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
   3.537 +    then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith
   3.538 +    then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
   3.539 +      using ik
   3.540 +      by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)
   3.541 +    then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
   3.542 +      unfolding of_nat_mult[symmetric] of_nat_le_iff .
   3.543 +    with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"
   3.544 +      using `i < k` by (simp add: field_simps)
   3.545 +  qed (simp add: x zero_le_divide_iff)
   3.546 +  finally show ?thesis .
   3.547 +qed
   3.548 +
   3.549 +text{*Versions of the theorems above for the natural-number version of "choose"*}
   3.550 +lemma binomial_altdef_of_nat:
   3.551 +  fixes n k :: nat
   3.552 +    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
   3.553 +  assumes "k \<le> n"
   3.554 +  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
   3.555 +using assms
   3.556 +by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
   3.557 +
   3.558 +lemma binomial_ge_n_over_k_pow_k:
   3.559 +  fixes k n :: nat
   3.560 +    and x :: "'a :: linordered_field_inverse_zero"
   3.561 +  assumes "k \<le> n"
   3.562 +  shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
   3.563 +by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)
   3.564 +
   3.565 +lemma binomial_le_pow:
   3.566 +  assumes "r \<le> n"
   3.567 +  shows "n choose r \<le> n ^ r"
   3.568 +proof -
   3.569 +  have "n choose r \<le> fact n div fact (n - r)"
   3.570 +    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
   3.571 +  with fact_div_fact_le_pow [OF assms] show ?thesis by auto
   3.572 +qed
   3.573 +
   3.574 +lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
   3.575 +    n choose k = fact n div (fact k * fact (n - k))"
   3.576 + by (subst binomial_fact_lemma [symmetric]) auto
   3.577 +
   3.578 +lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
   3.579 +by (metis binomial_fact_lemma dvd_def)
   3.580 +
   3.581 +lemma choose_dvd_int:
   3.582 +  assumes "(0::int) <= k" and "k <= n"
   3.583 +  shows "fact k * fact (n - k) dvd fact n"
   3.584 +  apply (subst tsub_eq [symmetric], rule assms)
   3.585 +  apply (rule choose_dvd_nat [transferred])
   3.586 +  using assms apply auto
   3.587 +  done
   3.588 +
   3.589 +lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
   3.590 +by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
   3.591 +
   3.592 +lemma choose_mult_lemma:
   3.593 +     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
   3.594 +proof -
   3.595 +  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
   3.596 +        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
   3.597 +    by (simp add: assms binomial_altdef_nat)
   3.598 +  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
   3.599 +    apply (subst div_mult_div_if_dvd)
   3.600 +    apply (auto simp: fact_fact_dvd_fact)
   3.601 +    apply (metis add.assoc add.commute fact_fact_dvd_fact)
   3.602 +    done
   3.603 +  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
   3.604 +    apply (subst div_mult_div_if_dvd [symmetric])
   3.605 +    apply (auto simp: fact_fact_dvd_fact)
   3.606 +    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
   3.607 +    done
   3.608 +  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
   3.609 +    apply (subst div_mult_div_if_dvd)
   3.610 +    apply (auto simp: fact_fact_dvd_fact)
   3.611 +    apply(metis mult.left_commute)
   3.612 +    done
   3.613 +  finally show ?thesis
   3.614 +    by (simp add: binomial_altdef_nat mult.commute)
   3.615 +qed
   3.616 +
   3.617 +text{*The "Subset of a Subset" identity*}
   3.618 +lemma choose_mult:
   3.619 +  assumes "k\<le>m" "m\<le>n"
   3.620 +    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
   3.621 +using assms choose_mult_lemma [of "m-k" "n-m" k]
   3.622 +by simp
   3.623 +
   3.624 +
   3.625 +subsection {* Binomial coefficients *}
   3.626 +
   3.627 +lemma choose_one: "(n::nat) choose 1 = n"
   3.628 +  by simp
   3.629 +
   3.630 +(*FIXME: messy and apparently unused*)
   3.631 +lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow>
   3.632 +    (ALL n. P (Suc n) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow>
   3.633 +    P (Suc n) (Suc k))) \<longrightarrow> (ALL k <= n. P n k)"
   3.634 +  apply (induct n)
   3.635 +  apply auto
   3.636 +  apply (case_tac "k = 0")
   3.637 +  apply auto
   3.638 +  apply (case_tac "k = Suc n")
   3.639 +  apply auto
   3.640 +  apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
   3.641 +  done
   3.642 +
   3.643 +lemma card_UNION:
   3.644 +  assumes "finite A" and "\<forall>k \<in> A. finite k"
   3.645 +  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
   3.646 +  (is "?lhs = ?rhs")
   3.647 +proof -
   3.648 +  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
   3.649 +  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
   3.650 +    by(subst setsum_right_distrib) simp
   3.651 +  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
   3.652 +    using assms by(subst setsum.Sigma)(auto)
   3.653 +  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))"
   3.654 +    by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
   3.655 +  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))"
   3.656 +    using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
   3.657 +  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)))"
   3.658 +    using assms by(subst setsum.Sigma) auto
   3.659 +  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
   3.660 +  proof(rule setsum.cong[OF refl])
   3.661 +    fix x
   3.662 +    assume x: "x \<in> \<Union>A"
   3.663 +    def K \<equiv> "{X \<in> A. x \<in> X}"
   3.664 +    with `finite A` have K: "finite K" by auto
   3.665 +    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
   3.666 +    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
   3.667 +      using assms by(auto intro!: inj_onI)
   3.668 +    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
   3.669 +      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
   3.670 +        simp add: card_gt_0_iff[folded Suc_le_eq]
   3.671 +        dest: finite_subset intro: card_mono)
   3.672 +    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
   3.673 +      by (rule setsum.reindex_cong [where l = snd]) fastforce
   3.674 +    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)))"
   3.675 +      using assms by(subst setsum.Sigma) auto
   3.676 +    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))"
   3.677 +      by(subst setsum_right_distrib) simp
   3.678 +    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
   3.679 +    proof(rule setsum.mono_neutral_cong_right[rule_format])
   3.680 +      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
   3.681 +        by(auto simp add: K_def intro: card_mono)
   3.682 +    next
   3.683 +      fix i
   3.684 +      assume "i \<in> {1..card A} - {1..card K}"
   3.685 +      hence i: "i \<le> card A" "card K < i" by auto
   3.686 +      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}"
   3.687 +        by(auto simp add: K_def)
   3.688 +      also have "\<dots> = {}" using `finite A` i
   3.689 +        by(auto simp add: K_def dest: card_mono[rotated 1])
   3.690 +      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
   3.691 +        by(simp only:) simp
   3.692 +    next
   3.693 +      fix i
   3.694 +      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)"
   3.695 +        (is "?lhs = ?rhs")
   3.696 +        by(rule setsum.cong)(auto simp add: K_def)
   3.697 +      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
   3.698 +    qed simp
   3.699 +    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
   3.700 +      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
   3.701 +    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
   3.702 +      by(subst (2) setsum_head_Suc)(simp_all )
   3.703 +    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
   3.704 +      using K by(subst n_subsets[symmetric]) simp_all
   3.705 +    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
   3.706 +      by(subst setsum_right_distrib[symmetric]) simp
   3.707 +    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
   3.708 +      by(subst binomial_ring)(simp add: ac_simps)
   3.709 +    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
   3.710 +    finally show "?lhs x = 1" .
   3.711 +  qed
   3.712 +  also have "nat \<dots> = card (\<Union>A)" by simp
   3.713 +  finally show ?thesis ..
   3.714 +qed
   3.715 +
   3.716 +text{* The number of nat lists of length @{text m} summing to @{text N} is
   3.717 +@{term "(N + m - 1) choose N"}: *}
   3.718 +
   3.719 +lemma card_length_listsum_rec:
   3.720 +  assumes "m\<ge>1"
   3.721 +  shows "card {l::nat list. length l = m \<and> listsum l = N} =
   3.722 +    (card {l. length l = (m - 1) \<and> listsum l = N} +
   3.723 +    card {l. length l = m \<and> listsum l + 1 =  N})"
   3.724 +    (is "card ?C = (card ?A + card ?B)")
   3.725 +proof -
   3.726 +  let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
   3.727 +  let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
   3.728 +  let ?f ="\<lambda> l. 0#l"
   3.729 +  let ?g ="\<lambda> l. (hd l + 1) # tl l"
   3.730 +  have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp
   3.731 +  have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs"
   3.732 +    by(auto simp add: neq_Nil_conv)
   3.733 +  have f: "bij_betw ?f ?A ?A'"
   3.734 +    apply(rule bij_betw_byWitness[where f' = tl])
   3.735 +    using assms
   3.736 +    by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
   3.737 +  have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs"
   3.738 +    by (metis 1 listsum_simps(2) 2)
   3.739 +  have g: "bij_betw ?g ?B ?B'"
   3.740 +    apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"])
   3.741 +    using assms
   3.742 +    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
   3.743 +      simp del: length_greater_0_conv length_0_conv)
   3.744 +  { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}"
   3.745 +    using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto }
   3.746 +    note fin = this
   3.747 +  have fin_A: "finite ?A" using fin[of _ "N+1"]
   3.748 +    by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"],
   3.749 +      auto simp: member_le_listsum_nat less_Suc_eq_le)
   3.750 +  have fin_B: "finite ?B"
   3.751 +    by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"],
   3.752 +      auto simp: member_le_listsum_nat less_Suc_eq_le fin)
   3.753 +  have uni: "?C = ?A' \<union> ?B'" by auto
   3.754 +  have disj: "?A' \<inter> ?B' = {}" by auto
   3.755 +  have "card ?C = card(?A' \<union> ?B')" using uni by simp
   3.756 +  also have "\<dots> = card ?A + card ?B"
   3.757 +    using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
   3.758 +      bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
   3.759 +    by presburger
   3.760 +  finally show ?thesis .
   3.761 +qed
   3.762 +
   3.763 +lemma card_length_listsum: --"By Holden Lee, tidied by Tobias Nipkow"
   3.764 +  "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
   3.765 +proof (cases m)
   3.766 +  case 0 then show ?thesis
   3.767 +    by (cases N) (auto simp: cong: conj_cong)
   3.768 +next
   3.769 +  case (Suc m')
   3.770 +    have m: "m\<ge>1" by (simp add: Suc)
   3.771 +    then show ?thesis
   3.772 +    proof (induct "N + m - 1" arbitrary: N m)
   3.773 +      case 0   -- "In the base case, the only solution is [0]."
   3.774 +      have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
   3.775 +        by (auto simp: length_Suc_conv)
   3.776 +      have "m=1 \<and> N=0" using 0 by linarith
   3.777 +      then show ?case by simp
   3.778 +    next
   3.779 +      case (Suc k)
   3.780 +
   3.781 +      have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} =
   3.782 +        (N + (m - 1) - 1) choose N"
   3.783 +      proof cases
   3.784 +        assume "m = 1"
   3.785 +        with Suc.hyps have "N\<ge>1" by auto
   3.786 +        with `m = 1` show ?thesis by (simp add: binomial_eq_0)
   3.787 +      next
   3.788 +        assume "m \<noteq> 1" thus ?thesis using Suc by fastforce
   3.789 +      qed
   3.790 +
   3.791 +      from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} =
   3.792 +        (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
   3.793 +      proof -
   3.794 +        have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith
   3.795 +        from Suc have "N>0 \<Longrightarrow>
   3.796 +          card {l::nat list. size l = m \<and> listsum l + 1 = N} =
   3.797 +          ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)
   3.798 +        thus ?thesis by auto
   3.799 +      qed
   3.800 +
   3.801 +      from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} +
   3.802 +          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
   3.803 +        by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
   3.804 +      thus ?case using card_length_listsum_rec[OF Suc.prems] by auto
   3.805 +    qed
   3.806 +qed
   3.807 +
   3.808  end
     4.1 --- a/src/HOL/Fields.thy	Tue Mar 10 11:56:32 2015 +0100
     4.2 +++ b/src/HOL/Fields.thy	Tue Mar 10 15:20:40 2015 +0000
     4.3 @@ -91,7 +91,7 @@
     4.4  apply auto
     4.5  done
     4.6  
     4.7 -lemma inverse_unique: 
     4.8 +lemma inverse_unique:
     4.9    assumes ab: "a * b = 1"
    4.10    shows "inverse a = b"
    4.11  proof -
    4.12 @@ -121,7 +121,7 @@
    4.13  lemma inverse_1 [simp]: "inverse 1 = 1"
    4.14  by (rule inverse_unique) simp
    4.15  
    4.16 -lemma nonzero_inverse_mult_distrib: 
    4.17 +lemma nonzero_inverse_mult_distrib:
    4.18    assumes "a \<noteq> 0" and "b \<noteq> 0"
    4.19    shows "inverse (a * b) = inverse b * inverse a"
    4.20  proof -
    4.21 @@ -199,7 +199,7 @@
    4.22  proof -
    4.23    assume [simp]: "c \<noteq> 0"
    4.24    have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
    4.25 -  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc) 
    4.26 +  also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc)
    4.27    finally show ?thesis .
    4.28  qed
    4.29  
    4.30 @@ -262,7 +262,7 @@
    4.31  proof cases
    4.32    assume "a=0" thus ?thesis by simp
    4.33  next
    4.34 -  assume "a\<noteq>0" 
    4.35 +  assume "a\<noteq>0"
    4.36    thus ?thesis by (simp add: nonzero_inverse_minus_eq)
    4.37  qed
    4.38  
    4.39 @@ -271,7 +271,7 @@
    4.40  proof cases
    4.41    assume "a=0" thus ?thesis by simp
    4.42  next
    4.43 -  assume "a\<noteq>0" 
    4.44 +  assume "a\<noteq>0"
    4.45    thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
    4.46  qed
    4.47  
    4.48 @@ -394,7 +394,7 @@
    4.49  
    4.50  lemma divide_minus1 [simp]: "x / - 1 = - x"
    4.51    using nonzero_minus_divide_right [of "1" x] by simp
    4.52 -  
    4.53 +
    4.54  end
    4.55  
    4.56  class field_inverse_zero = field +
    4.57 @@ -409,10 +409,10 @@
    4.58  lemma inverse_mult_distrib [simp]:
    4.59    "inverse (a * b) = inverse a * inverse b"
    4.60  proof cases
    4.61 -  assume "a \<noteq> 0 & b \<noteq> 0" 
    4.62 +  assume "a \<noteq> 0 & b \<noteq> 0"
    4.63    thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps)
    4.64  next
    4.65 -  assume "~ (a \<noteq> 0 & b \<noteq> 0)" 
    4.66 +  assume "~ (a \<noteq> 0 & b \<noteq> 0)"
    4.67    thus ?thesis by force
    4.68  qed
    4.69  
    4.70 @@ -470,13 +470,13 @@
    4.71  
    4.72  lemma minus_divide_divide:
    4.73    "(- a) / (- b) = a / b"
    4.74 -apply (cases "b=0", simp) 
    4.75 -apply (simp add: nonzero_minus_divide_divide) 
    4.76 +apply (cases "b=0", simp)
    4.77 +apply (simp add: nonzero_minus_divide_divide)
    4.78  done
    4.79  
    4.80  lemma inverse_eq_1_iff [simp]:
    4.81    "inverse x = 1 \<longleftrightarrow> x = 1"
    4.82 -  by (insert inverse_eq_iff_eq [of x 1], simp) 
    4.83 +  by (insert inverse_eq_iff_eq [of x 1], simp)
    4.84  
    4.85  lemma divide_eq_0_iff [simp]:
    4.86    "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
    4.87 @@ -489,7 +489,7 @@
    4.88    done
    4.89  
    4.90  lemma divide_cancel_left [simp]:
    4.91 -  "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 
    4.92 +  "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
    4.93    apply (cases "c=0", simp)
    4.94    apply (simp add: divide_inverse)
    4.95    done
    4.96 @@ -524,19 +524,19 @@
    4.97  class linordered_field = field + linordered_idom
    4.98  begin
    4.99  
   4.100 -lemma positive_imp_inverse_positive: 
   4.101 -  assumes a_gt_0: "0 < a" 
   4.102 +lemma positive_imp_inverse_positive:
   4.103 +  assumes a_gt_0: "0 < a"
   4.104    shows "0 < inverse a"
   4.105  proof -
   4.106 -  have "0 < a * inverse a" 
   4.107 +  have "0 < a * inverse a"
   4.108      by (simp add: a_gt_0 [THEN less_imp_not_eq2])
   4.109 -  thus "0 < inverse a" 
   4.110 +  thus "0 < inverse a"
   4.111      by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
   4.112  qed
   4.113  
   4.114  lemma negative_imp_inverse_negative:
   4.115    "a < 0 \<Longrightarrow> inverse a < 0"
   4.116 -  by (insert positive_imp_inverse_positive [of "-a"], 
   4.117 +  by (insert positive_imp_inverse_positive [of "-a"],
   4.118      simp add: nonzero_inverse_minus_eq less_imp_not_eq)
   4.119  
   4.120  lemma inverse_le_imp_le:
   4.121 @@ -577,7 +577,7 @@
   4.122  proof
   4.123    fix x::'a
   4.124    have m1: "- (1::'a) < 0" by simp
   4.125 -  from add_strict_right_mono[OF m1, where c=x] 
   4.126 +  from add_strict_right_mono[OF m1, where c=x]
   4.127    have "(- 1) + x < x" by simp
   4.128    thus "\<exists>y. y < x" by blast
   4.129  qed
   4.130 @@ -587,7 +587,7 @@
   4.131  proof
   4.132    fix x::'a
   4.133    have m1: " (1::'a) > 0" by simp
   4.134 -  from add_strict_right_mono[OF m1, where c=x] 
   4.135 +  from add_strict_right_mono[OF m1, where c=x]
   4.136    have "1 + x > x" by simp
   4.137    thus "\<exists>y. y > x" by blast
   4.138  qed
   4.139 @@ -606,13 +606,13 @@
   4.140  lemma inverse_less_imp_less:
   4.141    "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
   4.142  apply (simp add: less_le [of "inverse a"] less_le [of "b"])
   4.143 -apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
   4.144 +apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
   4.145  done
   4.146  
   4.147  text{*Both premises are essential. Consider -1 and 1.*}
   4.148  lemma inverse_less_iff_less [simp]:
   4.149    "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   4.150 -  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   4.151 +  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
   4.152  
   4.153  lemma le_imp_inverse_le:
   4.154    "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
   4.155 @@ -620,42 +620,42 @@
   4.156  
   4.157  lemma inverse_le_iff_le [simp]:
   4.158    "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   4.159 -  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   4.160 +  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
   4.161  
   4.162  
   4.163  text{*These results refer to both operands being negative.  The opposite-sign
   4.164  case is trivial, since inverse preserves signs.*}
   4.165  lemma inverse_le_imp_le_neg:
   4.166    "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
   4.167 -apply (rule classical) 
   4.168 -apply (subgoal_tac "a < 0") 
   4.169 +apply (rule classical)
   4.170 +apply (subgoal_tac "a < 0")
   4.171   prefer 2 apply force
   4.172  apply (insert inverse_le_imp_le [of "-b" "-a"])
   4.173 -apply (simp add: nonzero_inverse_minus_eq) 
   4.174 +apply (simp add: nonzero_inverse_minus_eq)
   4.175  done
   4.176  
   4.177  lemma less_imp_inverse_less_neg:
   4.178     "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
   4.179 -apply (subgoal_tac "a < 0") 
   4.180 - prefer 2 apply (blast intro: less_trans) 
   4.181 +apply (subgoal_tac "a < 0")
   4.182 + prefer 2 apply (blast intro: less_trans)
   4.183  apply (insert less_imp_inverse_less [of "-b" "-a"])
   4.184 -apply (simp add: nonzero_inverse_minus_eq) 
   4.185 +apply (simp add: nonzero_inverse_minus_eq)
   4.186  done
   4.187  
   4.188  lemma inverse_less_imp_less_neg:
   4.189     "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
   4.190 -apply (rule classical) 
   4.191 -apply (subgoal_tac "a < 0") 
   4.192 +apply (rule classical)
   4.193 +apply (subgoal_tac "a < 0")
   4.194   prefer 2
   4.195   apply force
   4.196  apply (insert inverse_less_imp_less [of "-b" "-a"])
   4.197 -apply (simp add: nonzero_inverse_minus_eq) 
   4.198 +apply (simp add: nonzero_inverse_minus_eq)
   4.199  done
   4.200  
   4.201  lemma inverse_less_iff_less_neg [simp]:
   4.202    "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   4.203  apply (insert inverse_less_iff_less [of "-b" "-a"])
   4.204 -apply (simp del: inverse_less_iff_less 
   4.205 +apply (simp del: inverse_less_iff_less
   4.206              add: nonzero_inverse_minus_eq)
   4.207  done
   4.208  
   4.209 @@ -665,7 +665,7 @@
   4.210  
   4.211  lemma inverse_le_iff_le_neg [simp]:
   4.212    "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   4.213 -  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   4.214 +  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
   4.215  
   4.216  lemma one_less_inverse:
   4.217    "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
   4.218 @@ -682,7 +682,7 @@
   4.219    from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c"
   4.220      using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps)
   4.221    also have "... \<longleftrightarrow> a * c \<le> b"
   4.222 -    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   4.223 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   4.224    finally show ?thesis .
   4.225  qed
   4.226  
   4.227 @@ -693,7 +693,7 @@
   4.228    from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c"
   4.229      using mult_less_cancel_right [of a c "b / c"] by auto
   4.230    also have "... = (a*c < b)"
   4.231 -    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   4.232 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   4.233    finally show ?thesis .
   4.234  qed
   4.235  
   4.236 @@ -704,7 +704,7 @@
   4.237    from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c"
   4.238      using mult_less_cancel_right [of "b / c" c a] by auto
   4.239    also have "... \<longleftrightarrow> b < a * c"
   4.240 -    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   4.241 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   4.242    finally show ?thesis .
   4.243  qed
   4.244  
   4.245 @@ -715,7 +715,7 @@
   4.246    from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c"
   4.247      using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps)
   4.248    also have "... \<longleftrightarrow> b \<le> a * c"
   4.249 -    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   4.250 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   4.251    finally show ?thesis .
   4.252  qed
   4.253  
   4.254 @@ -726,7 +726,7 @@
   4.255    from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c"
   4.256      using mult_le_cancel_right [of "b / c" c a] by auto
   4.257    also have "... \<longleftrightarrow> b \<le> a * c"
   4.258 -    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   4.259 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   4.260    finally show ?thesis .
   4.261  qed
   4.262  
   4.263 @@ -737,7 +737,7 @@
   4.264    from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c"
   4.265      using mult_less_cancel_right [of "b / c" c a] by auto
   4.266    also have "... \<longleftrightarrow> b < a * c"
   4.267 -    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
   4.268 +    by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc)
   4.269    finally show ?thesis .
   4.270  qed
   4.271  
   4.272 @@ -746,9 +746,9 @@
   4.273    shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b"
   4.274  proof -
   4.275    from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c"
   4.276 -    using mult_le_cancel_right [of a c "b / c"] by auto 
   4.277 +    using mult_le_cancel_right [of a c "b / c"] by auto
   4.278    also have "... \<longleftrightarrow> a * c \<le> b"
   4.279 -    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   4.280 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   4.281    finally show ?thesis .
   4.282  qed
   4.283  
   4.284 @@ -759,7 +759,7 @@
   4.285    from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c"
   4.286      using mult_less_cancel_right [of a c "b / c"] by auto
   4.287    also have "... \<longleftrightarrow> a * c < b"
   4.288 -    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
   4.289 +    by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc)
   4.290    finally show ?thesis .
   4.291  qed
   4.292  
   4.293 @@ -842,7 +842,7 @@
   4.294  by(simp add:field_simps)
   4.295  
   4.296  lemma divide_nonneg_neg:
   4.297 -  "0 <= x ==> y < 0 ==> x / y <= 0" 
   4.298 +  "0 <= x ==> y < 0 ==> x / y <= 0"
   4.299  by(simp add:field_simps)
   4.300  
   4.301  lemma divide_neg_neg:
   4.302 @@ -855,7 +855,7 @@
   4.303  
   4.304  lemma divide_strict_right_mono:
   4.305       "[|a < b; 0 < c|] ==> a / c < b / c"
   4.306 -by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono 
   4.307 +by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
   4.308                positive_imp_inverse_positive)
   4.309  
   4.310  
   4.311 @@ -865,7 +865,7 @@
   4.312  apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
   4.313  done
   4.314  
   4.315 -text{*The last premise ensures that @{term a} and @{term b} 
   4.316 +text{*The last premise ensures that @{term a} and @{term b}
   4.317        have the same sign*}
   4.318  lemma divide_strict_left_mono:
   4.319    "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
   4.320 @@ -895,7 +895,7 @@
   4.321      z < x / y"
   4.322  by(simp add:field_simps)
   4.323  
   4.324 -lemma frac_le: "0 <= x ==> 
   4.325 +lemma frac_le: "0 <= x ==>
   4.326      x <= y ==> 0 < w ==> w <= z  ==> x / z <= y / w"
   4.327    apply (rule mult_imp_div_pos_le)
   4.328    apply simp
   4.329 @@ -905,7 +905,7 @@
   4.330    apply simp_all
   4.331  done
   4.332  
   4.333 -lemma frac_less: "0 <= x ==> 
   4.334 +lemma frac_less: "0 <= x ==>
   4.335      x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
   4.336    apply (rule mult_imp_div_pos_less)
   4.337    apply simp
   4.338 @@ -915,7 +915,7 @@
   4.339    apply simp_all
   4.340  done
   4.341  
   4.342 -lemma frac_less2: "0 < x ==> 
   4.343 +lemma frac_less2: "0 < x ==>
   4.344      x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
   4.345    apply (rule mult_imp_div_pos_less)
   4.346    apply simp_all
   4.347 @@ -933,7 +933,7 @@
   4.348  subclass unbounded_dense_linorder
   4.349  proof
   4.350    fix x y :: 'a
   4.351 -  from less_add_one show "\<exists>y. x < y" .. 
   4.352 +  from less_add_one show "\<exists>y. x < y" ..
   4.353    from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
   4.354    then have "x - 1 < x + 1 - 1" by simp
   4.355    then have "x - 1 < x" by (simp add: algebra_simps)
   4.356 @@ -943,14 +943,14 @@
   4.357  
   4.358  lemma nonzero_abs_inverse:
   4.359       "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
   4.360 -apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq 
   4.361 +apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
   4.362                        negative_imp_inverse_negative)
   4.363 -apply (blast intro: positive_imp_inverse_positive elim: less_asym) 
   4.364 +apply (blast intro: positive_imp_inverse_positive elim: less_asym)
   4.365  done
   4.366  
   4.367  lemma nonzero_abs_divide:
   4.368       "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   4.369 -  by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
   4.370 +  by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
   4.371  
   4.372  lemma field_le_epsilon:
   4.373    assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
   4.374 @@ -1003,10 +1003,10 @@
   4.375  qed
   4.376  
   4.377  lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
   4.378 -  by (simp add: not_le [symmetric] one_le_inverse_iff) 
   4.379 +  by (simp add: not_le [symmetric] one_le_inverse_iff)
   4.380  
   4.381  lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
   4.382 -  by (simp add: not_less [symmetric] one_less_inverse_iff) 
   4.383 +  by (simp add: not_less [symmetric] one_less_inverse_iff)
   4.384  
   4.385  lemma [divide_simps]:
   4.386    shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
   4.387 @@ -1060,13 +1060,13 @@
   4.388       "[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/c"
   4.389  by (force simp add: divide_strict_right_mono le_less)
   4.390  
   4.391 -lemma divide_right_mono_neg: "a <= b 
   4.392 +lemma divide_right_mono_neg: "a <= b
   4.393      ==> c <= 0 ==> b / c <= a / c"
   4.394  apply (drule divide_right_mono [of _ _ "- c"])
   4.395  apply auto
   4.396  done
   4.397  
   4.398 -lemma divide_left_mono_neg: "a <= b 
   4.399 +lemma divide_left_mono_neg: "a <= b
   4.400      ==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
   4.401    apply (drule divide_left_mono [of _ _ "- c"])
   4.402    apply (auto simp add: mult.commute)
   4.403 @@ -1162,28 +1162,28 @@
   4.404  by (auto simp add: divide_eq_eq)
   4.405  
   4.406  lemma abs_inverse [simp]:
   4.407 -     "\<bar>inverse a\<bar> = 
   4.408 +     "\<bar>inverse a\<bar> =
   4.409        inverse \<bar>a\<bar>"
   4.410 -apply (cases "a=0", simp) 
   4.411 -apply (simp add: nonzero_abs_inverse) 
   4.412 +apply (cases "a=0", simp)
   4.413 +apply (simp add: nonzero_abs_inverse)
   4.414  done
   4.415  
   4.416  lemma abs_divide [simp]:
   4.417       "\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
   4.418 -apply (cases "b=0", simp) 
   4.419 -apply (simp add: nonzero_abs_divide) 
   4.420 +apply (cases "b=0", simp)
   4.421 +apply (simp add: nonzero_abs_divide)
   4.422  done
   4.423  
   4.424 -lemma abs_div_pos: "0 < y ==> 
   4.425 +lemma abs_div_pos: "0 < y ==>
   4.426      \<bar>x\<bar> / y = \<bar>x / y\<bar>"
   4.427    apply (subst abs_divide)
   4.428    apply (simp add: order_less_imp_le)
   4.429  done
   4.430  
   4.431 -lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)" 
   4.432 +lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)"
   4.433  by (auto simp: zero_le_divide_iff)
   4.434  
   4.435 -lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)" 
   4.436 +lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)"
   4.437  by (auto simp: divide_le_0_iff)
   4.438  
   4.439  lemma field_le_mult_one_interval:
   4.440 @@ -1208,5 +1208,5 @@
   4.441  
   4.442  code_identifier
   4.443    code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   4.444 - 
   4.445 +
   4.446  end
     5.1 --- a/src/HOL/GCD.thy	Tue Mar 10 11:56:32 2015 +0100
     5.2 +++ b/src/HOL/GCD.thy	Tue Mar 10 15:20:40 2015 +0000
     5.3 @@ -28,7 +28,7 @@
     5.4  section {* Greatest common divisor and least common multiple *}
     5.5  
     5.6  theory GCD
     5.7 -imports Fact
     5.8 +imports Main
     5.9  begin
    5.10  
    5.11  declare One_nat_def [simp del]
    5.12 @@ -50,7 +50,7 @@
    5.13  class semiring_gcd = comm_semiring_1 + gcd +
    5.14    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    5.15  		and gcd_dvd2 [iff]: "gcd a b dvd b"
    5.16 -		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 
    5.17 +		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    5.18  
    5.19  class ring_gcd = comm_ring_1 + semiring_gcd
    5.20  
    5.21 @@ -266,10 +266,10 @@
    5.22    then show "k dvd gcd m n"
    5.23      by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
    5.24  qed
    5.25 -  
    5.26 +
    5.27  instance int :: ring_gcd
    5.28    by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
    5.29 -  
    5.30 +
    5.31  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
    5.32    by (metis gcd_dvd1 dvd_trans)
    5.33  
    5.34 @@ -1753,12 +1753,12 @@
    5.35  
    5.36  
    5.37  text \<open>Fact aliasses\<close>
    5.38 -  
    5.39 -lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat] 
    5.40 +
    5.41 +lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
    5.42    and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
    5.43    and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
    5.44  
    5.45 -lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int] 
    5.46 +lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
    5.47    and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
    5.48    and gcd_greatest_int = gcd_greatest [where ?'a = int]
    5.49  
     6.1 --- a/src/HOL/HOLCF/Universal.thy	Tue Mar 10 11:56:32 2015 +0100
     6.2 +++ b/src/HOL/HOLCF/Universal.thy	Tue Mar 10 15:20:40 2015 +0000
     6.3 @@ -325,8 +325,6 @@
     6.4    qed
     6.5  qed
     6.6  
     6.7 -no_notation binomial (infixl "choose" 65)
     6.8 -
     6.9  definition
    6.10    choose :: "'a compact_basis set \<Rightarrow> 'a compact_basis"
    6.11  where
     7.1 --- a/src/HOL/Int.thy	Tue Mar 10 11:56:32 2015 +0100
     7.2 +++ b/src/HOL/Int.thy	Tue Mar 10 15:20:40 2015 +0000
     7.3 @@ -1599,4 +1599,8 @@
     7.4  lifting_update int.lifting
     7.5  lifting_forget int.lifting
     7.6  
     7.7 +text{*Also the class for fields with characteristic zero.*}
     7.8 +class field_char_0 = field + ring_char_0
     7.9 +subclass (in linordered_field) field_char_0 ..
    7.10 +
    7.11  end
     8.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 10 11:56:32 2015 +0100
     8.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 10 15:20:40 2015 +0000
     8.3 @@ -5,7 +5,7 @@
     8.4  section{* A formalization of formal power series *}
     8.5  
     8.6  theory Formal_Power_Series
     8.7 -imports "~~/src/HOL/Number_Theory/Binomial"
     8.8 +imports Complex_Main
     8.9  begin
    8.10  
    8.11  
     9.1 --- a/src/HOL/Library/NthRoot_Limits.thy	Tue Mar 10 11:56:32 2015 +0100
     9.2 +++ b/src/HOL/Library/NthRoot_Limits.thy	Tue Mar 10 15:20:40 2015 +0000
     9.3 @@ -1,13 +1,7 @@
     9.4  theory NthRoot_Limits
     9.5 -  imports Complex_Main "~~/src/HOL/Number_Theory/Binomial"
     9.6 +  imports Complex_Main
     9.7  begin
     9.8  
     9.9 -text {*
    9.10 -
    9.11 -This does not fit into @{text Complex_Main}, as it depends on @{text Binomial}
    9.12 -
    9.13 -*}
    9.14 -
    9.15  lemma LIMSEQ_root: "(\<lambda>n. root n n) ----> 1"
    9.16  proof -
    9.17    def x \<equiv> "\<lambda>n. root n n - 1"
    10.1 --- a/src/HOL/Number_Theory/Binomial.thy	Tue Mar 10 11:56:32 2015 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,656 +0,0 @@
    10.4 -(*  Title:      HOL/Number_Theory/Binomial.thy
    10.5 -    Authors:    Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
    10.6 -
    10.7 -Defines the "choose" function, and establishes basic properties.
    10.8 -*)
    10.9 -
   10.10 -section {* Binomial *}
   10.11 -
   10.12 -theory Binomial
   10.13 -imports Cong Fact Complex_Main
   10.14 -begin
   10.15 -
   10.16 -lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
   10.17 -  using binomial [of 1 "1" n]
   10.18 -  by (simp add: numeral_2_eq_2)
   10.19 -
   10.20 -lemma sum_choose_lower: "(\<Sum>k=0..n. (r+k) choose k) = Suc (r+n) choose n"
   10.21 -  by (induct n) auto
   10.22 -
   10.23 -lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
   10.24 -  by (induct n) auto
   10.25 -
   10.26 -lemma natsum_reverse_index:
   10.27 -  fixes m::nat
   10.28 -  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)"
   10.29 -  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
   10.30 -
   10.31 -text{*NW diagonal sum property*}
   10.32 -lemma sum_choose_diagonal:
   10.33 -  assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
   10.34 -proof -
   10.35 -  have "(\<Sum>k=0..m. (n-k) choose (m-k)) = (\<Sum>k=0..m. (n-m+k) choose k)"
   10.36 -    by (rule natsum_reverse_index) (simp add: assms)
   10.37 -  also have "... = Suc (n-m+m) choose m"
   10.38 -    by (rule sum_choose_lower)
   10.39 -  also have "... = Suc n choose m" using assms
   10.40 -    by simp
   10.41 -  finally show ?thesis .
   10.42 -qed
   10.43 -
   10.44 -subsection{* Pochhammer's symbol : generalized rising factorial *}
   10.45 -
   10.46 -text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
   10.47 -
   10.48 -definition "pochhammer (a::'a::comm_semiring_1) n =
   10.49 -  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
   10.50 -
   10.51 -lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
   10.52 -  by (simp add: pochhammer_def)
   10.53 -
   10.54 -lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
   10.55 -  by (simp add: pochhammer_def)
   10.56 -
   10.57 -lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
   10.58 -  by (simp add: pochhammer_def)
   10.59 -
   10.60 -lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   10.61 -  by (simp add: pochhammer_def)
   10.62 -
   10.63 -lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
   10.64 -proof -
   10.65 -  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
   10.66 -  then show ?thesis by (simp add: field_simps)
   10.67 -qed
   10.68 -
   10.69 -lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
   10.70 -proof -
   10.71 -  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
   10.72 -  then show ?thesis by simp
   10.73 -qed
   10.74 -
   10.75 -
   10.76 -lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
   10.77 -proof (cases n)
   10.78 -  case 0
   10.79 -  then show ?thesis by simp
   10.80 -next
   10.81 -  case (Suc n)
   10.82 -  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
   10.83 -qed
   10.84 -
   10.85 -lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
   10.86 -proof (cases "n = 0")
   10.87 -  case True
   10.88 -  then show ?thesis by (simp add: pochhammer_Suc_setprod)
   10.89 -next
   10.90 -  case False
   10.91 -  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
   10.92 -  have eq: "insert 0 {1 .. n} = {0..n}" by auto
   10.93 -  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)"
   10.94 -    apply (rule setprod.reindex_cong [where l = Suc])
   10.95 -    using False
   10.96 -    apply (auto simp add: fun_eq_iff field_simps)
   10.97 -    done
   10.98 -  show ?thesis
   10.99 -    apply (simp add: pochhammer_def)
  10.100 -    unfolding setprod.insert [OF *, unfolded eq]
  10.101 -    using ** apply (simp add: field_simps)
  10.102 -    done
  10.103 -qed
  10.104 -
  10.105 -lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
  10.106 -  unfolding fact_altdef_nat
  10.107 -  apply (cases n)
  10.108 -   apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
  10.109 -  apply (rule setprod.reindex_cong [where l = Suc])
  10.110 -    apply (auto simp add: fun_eq_iff)
  10.111 -  done
  10.112 -
  10.113 -lemma pochhammer_of_nat_eq_0_lemma:
  10.114 -  assumes "k > n"
  10.115 -  shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
  10.116 -proof (cases "n = 0")
  10.117 -  case True
  10.118 -  then show ?thesis
  10.119 -    using assms by (cases k) (simp_all add: pochhammer_rec)
  10.120 -next
  10.121 -  case False
  10.122 -  from assms obtain h where "k = Suc h" by (cases k) auto
  10.123 -  then show ?thesis
  10.124 -    by (simp add: pochhammer_Suc_setprod)
  10.125 -       (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
  10.126 -qed
  10.127 -
  10.128 -lemma pochhammer_of_nat_eq_0_lemma':
  10.129 -  assumes kn: "k \<le> n"
  10.130 -  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0"
  10.131 -proof (cases k)
  10.132 -  case 0
  10.133 -  then show ?thesis by simp
  10.134 -next
  10.135 -  case (Suc h)
  10.136 -  then show ?thesis
  10.137 -    apply (simp add: pochhammer_Suc_setprod)
  10.138 -    using Suc kn apply (auto simp add: algebra_simps)
  10.139 -    done
  10.140 -qed
  10.141 -
  10.142 -lemma pochhammer_of_nat_eq_0_iff:
  10.143 -  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
  10.144 -  (is "?l = ?r")
  10.145 -  using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
  10.146 -    pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
  10.147 -  by (auto simp add: not_le[symmetric])
  10.148 -
  10.149 -
  10.150 -lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
  10.151 -  apply (auto simp add: pochhammer_of_nat_eq_0_iff)
  10.152 -  apply (cases n)
  10.153 -   apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
  10.154 -  apply (metis leD not_less_eq)
  10.155 -  done
  10.156 -
  10.157 -
  10.158 -lemma pochhammer_eq_0_mono:
  10.159 -  "pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
  10.160 -  unfolding pochhammer_eq_0_iff by auto
  10.161 -
  10.162 -lemma pochhammer_neq_0_mono:
  10.163 -  "pochhammer a m \<noteq> (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a n \<noteq> 0"
  10.164 -  unfolding pochhammer_eq_0_iff by auto
  10.165 -
  10.166 -lemma pochhammer_minus:
  10.167 -  assumes kn: "k \<le> n"
  10.168 -  shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
  10.169 -proof (cases k)
  10.170 -  case 0
  10.171 -  then show ?thesis by simp
  10.172 -next
  10.173 -  case (Suc h)
  10.174 -  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
  10.175 -    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
  10.176 -    by auto
  10.177 -  show ?thesis
  10.178 -    unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
  10.179 -    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
  10.180 -       (auto simp: of_nat_diff)
  10.181 -qed
  10.182 -
  10.183 -lemma pochhammer_minus':
  10.184 -  assumes kn: "k \<le> n"
  10.185 -  shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k"
  10.186 -  unfolding pochhammer_minus[OF kn, where b=b]
  10.187 -  unfolding mult.assoc[symmetric]
  10.188 -  unfolding power_add[symmetric]
  10.189 -  by simp
  10.190 -
  10.191 -lemma pochhammer_same: "pochhammer (- of_nat n) n =
  10.192 -    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
  10.193 -  unfolding pochhammer_minus[OF le_refl[of n]]
  10.194 -  by (simp add: of_nat_diff pochhammer_fact)
  10.195 -
  10.196 -
  10.197 -subsection{* Generalized binomial coefficients *}
  10.198 -
  10.199 -definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
  10.200 -  where "a gchoose n =
  10.201 -    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
  10.202 -
  10.203 -lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
  10.204 -  apply (simp_all add: gbinomial_def)
  10.205 -  apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
  10.206 -   apply (simp del:setprod_zero_iff)
  10.207 -  apply simp
  10.208 -  done
  10.209 -
  10.210 -lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
  10.211 -proof (cases "n = 0")
  10.212 -  case True
  10.213 -  then show ?thesis by simp
  10.214 -next
  10.215 -  case False
  10.216 -  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
  10.217 -  have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
  10.218 -    by auto
  10.219 -  from False show ?thesis
  10.220 -    by (simp add: pochhammer_def gbinomial_def field_simps
  10.221 -      eq setprod.distrib[symmetric])
  10.222 -qed
  10.223 -
  10.224 -
  10.225 -lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
  10.226 -proof -
  10.227 -  { assume kn: "k > n"
  10.228 -    then have ?thesis
  10.229 -      by (subst binomial_eq_0[OF kn]) 
  10.230 -         (simp add: gbinomial_pochhammer field_simps  pochhammer_of_nat_eq_0_iff) }
  10.231 -  moreover
  10.232 -  { assume "k=0" then have ?thesis by simp }
  10.233 -  moreover
  10.234 -  { assume kn: "k \<le> n" and k0: "k\<noteq> 0"
  10.235 -    from k0 obtain h where h: "k = Suc h" by (cases k) auto
  10.236 -    from h
  10.237 -    have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
  10.238 -      by (subst setprod_constant) auto
  10.239 -    have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
  10.240 -        using h kn
  10.241 -      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
  10.242 -         (auto simp: of_nat_diff)
  10.243 -    have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
  10.244 -        "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
  10.245 -        eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
  10.246 -      using h kn by auto
  10.247 -    from eq[symmetric]
  10.248 -    have ?thesis using kn
  10.249 -      apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
  10.250 -        gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
  10.251 -      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
  10.252 -        of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
  10.253 -      unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
  10.254 -      unfolding mult.assoc[symmetric]
  10.255 -      unfolding setprod.distrib[symmetric]
  10.256 -      apply simp
  10.257 -      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
  10.258 -      apply (auto simp: of_nat_diff)
  10.259 -      done
  10.260 -  }
  10.261 -  moreover
  10.262 -  have "k > n \<or> k = 0 \<or> (k \<le> n \<and> k \<noteq> 0)" by arith
  10.263 -  ultimately show ?thesis by blast
  10.264 -qed
  10.265 -
  10.266 -lemma gbinomial_1[simp]: "a gchoose 1 = a"
  10.267 -  by (simp add: gbinomial_def)
  10.268 -
  10.269 -lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
  10.270 -  by (simp add: gbinomial_def)
  10.271 -
  10.272 -lemma gbinomial_mult_1:
  10.273 -  "a * (a gchoose n) =
  10.274 -    of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")
  10.275 -proof -
  10.276 -  have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
  10.277 -    unfolding gbinomial_pochhammer
  10.278 -      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
  10.279 -    by (simp add:  field_simps del: of_nat_Suc)
  10.280 -  also have "\<dots> = ?l" unfolding gbinomial_pochhammer
  10.281 -    by (simp add: field_simps)
  10.282 -  finally show ?thesis ..
  10.283 -qed
  10.284 -
  10.285 -lemma gbinomial_mult_1':
  10.286 -    "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
  10.287 -  by (simp add: mult.commute gbinomial_mult_1)
  10.288 -
  10.289 -lemma gbinomial_Suc:
  10.290 -    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
  10.291 -  by (simp add: gbinomial_def)
  10.292 -
  10.293 -lemma gbinomial_mult_fact:
  10.294 -  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
  10.295 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
  10.296 -  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
  10.297 -
  10.298 -lemma gbinomial_mult_fact':
  10.299 -  "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
  10.300 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
  10.301 -  using gbinomial_mult_fact[of k a]
  10.302 -  by (subst mult.commute)
  10.303 -
  10.304 -
  10.305 -lemma gbinomial_Suc_Suc:
  10.306 -  "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
  10.307 -proof (cases k)
  10.308 -  case 0
  10.309 -  then show ?thesis by simp
  10.310 -next
  10.311 -  case (Suc h)
  10.312 -  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
  10.313 -    apply (rule setprod.reindex_cong [where l = Suc])
  10.314 -      using Suc
  10.315 -      apply auto
  10.316 -    done
  10.317 -  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
  10.318 -    ((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)"
  10.319 -    apply (simp add: Suc field_simps del: fact_Suc)
  10.320 -    unfolding gbinomial_mult_fact'
  10.321 -    apply (subst fact_Suc)
  10.322 -    unfolding of_nat_mult
  10.323 -    apply (subst mult.commute)
  10.324 -    unfolding mult.assoc
  10.325 -    unfolding gbinomial_mult_fact
  10.326 -    apply (simp add: field_simps)
  10.327 -    done
  10.328 -  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
  10.329 -    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
  10.330 -    by (simp add: field_simps Suc)
  10.331 -  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
  10.332 -    using eq0
  10.333 -    by (simp add: Suc setprod_nat_ivl_1_Suc)
  10.334 -  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
  10.335 -    unfolding gbinomial_mult_fact ..
  10.336 -  finally show ?thesis by (simp del: fact_Suc)
  10.337 -qed
  10.338 -
  10.339 -lemma gbinomial_reduce_nat:
  10.340 -  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
  10.341 -by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
  10.342 -
  10.343 -
  10.344 -lemma binomial_symmetric:
  10.345 -  assumes kn: "k \<le> n"
  10.346 -  shows "n choose k = n choose (n - k)"
  10.347 -proof-
  10.348 -  from kn have kn': "n - k \<le> n" by arith
  10.349 -  from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn']
  10.350 -  have "fact k * fact (n - k) * (n choose k) =
  10.351 -    fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp
  10.352 -  then show ?thesis using kn by simp
  10.353 -qed
  10.354 -
  10.355 -text{*Contributed by Manuel Eberl, generalised by LCP.
  10.356 -  Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"} *}
  10.357 -lemma gbinomial_altdef_of_nat:
  10.358 -  fixes k :: nat
  10.359 -    and x :: "'a :: {field_char_0,field_inverse_zero}"
  10.360 -  shows "x gchoose k = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
  10.361 -proof -
  10.362 -  have "(x gchoose k) = (\<Prod>i<k. x - of_nat i) / of_nat (fact k)"
  10.363 -    unfolding gbinomial_def
  10.364 -    by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
  10.365 -  also have "\<dots> = (\<Prod>i<k. (x - of_nat i) / of_nat (k - i) :: 'a)"
  10.366 -    unfolding fact_eq_rev_setprod_nat of_nat_setprod
  10.367 -    by (auto simp add: setprod_dividef intro!: setprod.cong of_nat_diff[symmetric])
  10.368 -  finally show ?thesis .
  10.369 -qed
  10.370 -
  10.371 -lemma gbinomial_ge_n_over_k_pow_k:
  10.372 -  fixes k :: nat
  10.373 -    and x :: "'a :: linordered_field_inverse_zero"
  10.374 -  assumes "of_nat k \<le> x"
  10.375 -  shows "(x / of_nat k :: 'a) ^ k \<le> x gchoose k"
  10.376 -proof -
  10.377 -  have x: "0 \<le> x"
  10.378 -    using assms of_nat_0_le_iff order_trans by blast
  10.379 -  have "(x / of_nat k :: 'a) ^ k = (\<Prod>i<k. x / of_nat k :: 'a)"
  10.380 -    by (simp add: setprod_constant)
  10.381 -  also have "\<dots> \<le> x gchoose k"
  10.382 -    unfolding gbinomial_altdef_of_nat
  10.383 -  proof (safe intro!: setprod_mono)
  10.384 -    fix i :: nat
  10.385 -    assume ik: "i < k"
  10.386 -    from assms have "x * of_nat i \<ge> of_nat (i * k)"
  10.387 -      by (metis mult.commute mult_le_cancel_right of_nat_less_0_iff of_nat_mult)
  10.388 -    then have "x * of_nat k - x * of_nat i \<le> x * of_nat k - of_nat (i * k)" by arith
  10.389 -    then have "x * of_nat (k - i) \<le> (x - of_nat i) * of_nat k"
  10.390 -      using ik 
  10.391 -      by (simp add: algebra_simps zero_less_mult_iff of_nat_diff of_nat_mult)
  10.392 -    then have "x * of_nat (k - i) \<le> (x - of_nat i) * (of_nat k :: 'a)"
  10.393 -      unfolding of_nat_mult[symmetric] of_nat_le_iff .
  10.394 -    with assms show "x / of_nat k \<le> (x - of_nat i) / (of_nat (k - i) :: 'a)"
  10.395 -      using `i < k` by (simp add: field_simps)
  10.396 -  qed (simp add: x zero_le_divide_iff)
  10.397 -  finally show ?thesis .
  10.398 -qed
  10.399 -
  10.400 -text{*Versions of the theorems above for the natural-number version of "choose"*}
  10.401 -lemma binomial_altdef_of_nat:
  10.402 -  fixes n k :: nat
  10.403 -    and x :: "'a :: {field_char_0,field_inverse_zero}"  --{*the point is to constrain @{typ 'a}*}
  10.404 -  assumes "k \<le> n"
  10.405 -  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
  10.406 -using assms
  10.407 -by (simp add: gbinomial_altdef_of_nat binomial_gbinomial of_nat_diff)
  10.408 -
  10.409 -lemma binomial_ge_n_over_k_pow_k:
  10.410 -  fixes k n :: nat
  10.411 -    and x :: "'a :: linordered_field_inverse_zero"
  10.412 -  assumes "k \<le> n"
  10.413 -  shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
  10.414 -by (simp add: assms gbinomial_ge_n_over_k_pow_k binomial_gbinomial of_nat_diff)  
  10.415 -  
  10.416 -lemma binomial_le_pow:
  10.417 -  assumes "r \<le> n"
  10.418 -  shows "n choose r \<le> n ^ r"
  10.419 -proof -
  10.420 -  have "n choose r \<le> fact n div fact (n - r)"
  10.421 -    using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
  10.422 -  with fact_div_fact_le_pow [OF assms] show ?thesis by auto
  10.423 -qed
  10.424 -
  10.425 -lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
  10.426 -    n choose k = fact n div (fact k * fact (n - k))"
  10.427 - by (subst binomial_fact_lemma [symmetric]) auto
  10.428 -
  10.429 -lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
  10.430 -by (metis binomial_fact_lemma dvd_def)
  10.431 -
  10.432 -lemma choose_dvd_int: 
  10.433 -  assumes "(0::int) <= k" and "k <= n"
  10.434 -  shows "fact k * fact (n - k) dvd fact n"
  10.435 -  apply (subst tsub_eq [symmetric], rule assms)
  10.436 -  apply (rule choose_dvd_nat [transferred])
  10.437 -  using assms apply auto
  10.438 -  done
  10.439 -
  10.440 -lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
  10.441 -by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
  10.442 -
  10.443 -lemma choose_mult_lemma:
  10.444 -     "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
  10.445 -proof -
  10.446 -  have "((m+r+k) choose (m+k)) * ((m+k) choose k) =
  10.447 -        fact (m+r + k) div (fact (m + k) * fact (m+r - m)) * (fact (m + k) div (fact k * fact m))"
  10.448 -    by (simp add: assms binomial_altdef_nat)
  10.449 -  also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
  10.450 -    apply (subst div_mult_div_if_dvd)
  10.451 -    apply (auto simp: fact_fact_dvd_fact)
  10.452 -    apply (metis add.assoc add.commute fact_fact_dvd_fact)
  10.453 -    done
  10.454 -  also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
  10.455 -    apply (subst div_mult_div_if_dvd [symmetric])
  10.456 -    apply (auto simp: fact_fact_dvd_fact)
  10.457 -    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
  10.458 -    done
  10.459 -  also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
  10.460 -    apply (subst div_mult_div_if_dvd)
  10.461 -    apply (auto simp: fact_fact_dvd_fact)
  10.462 -    apply(metis mult.left_commute)
  10.463 -    done
  10.464 -  finally show ?thesis
  10.465 -    by (simp add: binomial_altdef_nat mult.commute)
  10.466 -qed
  10.467 -
  10.468 -text{*The "Subset of a Subset" identity*}
  10.469 -lemma choose_mult:
  10.470 -  assumes "k\<le>m" "m\<le>n"
  10.471 -    shows "(n choose m) * (m choose k) = (n choose k) * ((n-k) choose (m-k))"
  10.472 -using assms choose_mult_lemma [of "m-k" "n-m" k]
  10.473 -by simp
  10.474 -
  10.475 -
  10.476 -subsection {* Binomial coefficients *}
  10.477 -
  10.478 -lemma choose_one: "(n::nat) choose 1 = n"
  10.479 -  by simp
  10.480 -
  10.481 -(*FIXME: messy and apparently unused*)
  10.482 -lemma binomial_induct [rule_format]: "(ALL (n::nat). P n n) \<longrightarrow> 
  10.483 -    (ALL n. P (Suc n) 0) \<longrightarrow> (ALL n. (ALL k < n. P n k \<longrightarrow> P n (Suc k) \<longrightarrow>
  10.484 -    P (Suc n) (Suc k))) \<longrightarrow> (ALL k <= n. P n k)"
  10.485 -  apply (induct n)
  10.486 -  apply auto
  10.487 -  apply (case_tac "k = 0")
  10.488 -  apply auto
  10.489 -  apply (case_tac "k = Suc n")
  10.490 -  apply auto
  10.491 -  apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
  10.492 -  done
  10.493 -
  10.494 -lemma card_UNION:
  10.495 -  assumes "finite A" and "\<forall>k \<in> A. finite k"
  10.496 -  shows "card (\<Union>A) = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * int (card (\<Inter>I)))"
  10.497 -  (is "?lhs = ?rhs")
  10.498 -proof -
  10.499 -  have "?rhs = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (- 1) ^ (card I + 1) * (\<Sum>_\<in>\<Inter>I. 1))" by simp
  10.500 -  also have "\<dots> = nat (\<Sum>I | I \<subseteq> A \<and> I \<noteq> {}. (\<Sum>_\<in>\<Inter>I. (- 1) ^ (card I + 1)))" (is "_ = nat ?rhs")
  10.501 -    by(subst setsum_right_distrib) simp
  10.502 -  also have "?rhs = (\<Sum>(I, _)\<in>Sigma {I. I \<subseteq> A \<and> I \<noteq> {}} Inter. (- 1) ^ (card I + 1))"
  10.503 -    using assms by(subst setsum.Sigma)(auto)
  10.504 -  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))"
  10.505 -    by (rule setsum.reindex_cong [where l = "\<lambda>(x, y). (y, x)"]) (auto intro: inj_onI simp add: split_beta)
  10.506 -  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))"
  10.507 -    using assms by(auto intro!: setsum.mono_neutral_cong_right finite_SigmaI2 intro: finite_subset[where B="\<Union>A"])
  10.508 -  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)))" 
  10.509 -    using assms by(subst setsum.Sigma) auto
  10.510 -  also have "\<dots> = (\<Sum>_\<in>\<Union>A. 1)" (is "setsum ?lhs _ = _")
  10.511 -  proof(rule setsum.cong[OF refl])
  10.512 -    fix x
  10.513 -    assume x: "x \<in> \<Union>A"
  10.514 -    def K \<equiv> "{X \<in> A. x \<in> X}"
  10.515 -    with `finite A` have K: "finite K" by auto
  10.516 -    let ?I = "\<lambda>i. {I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I}"
  10.517 -    have "inj_on snd (SIGMA i:{1..card A}. ?I i)"
  10.518 -      using assms by(auto intro!: inj_onI)
  10.519 -    moreover have [symmetric]: "snd ` (SIGMA i:{1..card A}. ?I i) = {I. I \<subseteq> A \<and> I \<noteq> {} \<and> x \<in> \<Inter>I}"
  10.520 -      using assms by(auto intro!: rev_image_eqI[where x="(card a, a)" for a]
  10.521 -        simp add: card_gt_0_iff[folded Suc_le_eq]
  10.522 -        dest: finite_subset intro: card_mono)
  10.523 -    ultimately have "?lhs x = (\<Sum>(i, I)\<in>(SIGMA i:{1..card A}. ?I i). (- 1) ^ (i + 1))"
  10.524 -      by (rule setsum.reindex_cong [where l = snd]) fastforce
  10.525 -    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)))"
  10.526 -      using assms by(subst setsum.Sigma) auto
  10.527 -    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))"
  10.528 -      by(subst setsum_right_distrib) simp
  10.529 -    also have "\<dots> = (\<Sum>i=1..card K. (- 1) ^ (i + 1) * (\<Sum>I|I \<subseteq> K \<and> card I = i. 1))" (is "_ = ?rhs")
  10.530 -    proof(rule setsum.mono_neutral_cong_right[rule_format])
  10.531 -      show "{1..card K} \<subseteq> {1..card A}" using `finite A`
  10.532 -        by(auto simp add: K_def intro: card_mono)
  10.533 -    next
  10.534 -      fix i
  10.535 -      assume "i \<in> {1..card A} - {1..card K}"
  10.536 -      hence i: "i \<le> card A" "card K < i" by auto
  10.537 -      have "{I. I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I} = {I. I \<subseteq> K \<and> card I = i}" 
  10.538 -        by(auto simp add: K_def)
  10.539 -      also have "\<dots> = {}" using `finite A` i
  10.540 -        by(auto simp add: K_def dest: card_mono[rotated 1])
  10.541 -      finally show "(- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> A \<and> card I = i \<and> x \<in> \<Inter>I. 1 :: int) = 0"
  10.542 -        by(simp only:) simp
  10.543 -    next
  10.544 -      fix i
  10.545 -      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)"
  10.546 -        (is "?lhs = ?rhs")
  10.547 -        by(rule setsum.cong)(auto simp add: K_def)
  10.548 -      thus "(- 1) ^ (i + 1) * ?lhs = (- 1) ^ (i + 1) * ?rhs" by simp
  10.549 -    qed simp
  10.550 -    also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}" using assms
  10.551 -      by(auto simp add: card_eq_0_iff K_def dest: finite_subset)
  10.552 -    hence "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
  10.553 -      by(subst (2) setsum_head_Suc)(simp_all )
  10.554 -    also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
  10.555 -      using K by(subst n_subsets[symmetric]) simp_all
  10.556 -    also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
  10.557 -      by(subst setsum_right_distrib[symmetric]) simp
  10.558 -    also have "\<dots> =  - ((-1 + 1) ^ card K) + 1"
  10.559 -      by(subst binomial_ring)(simp add: ac_simps)
  10.560 -    also have "\<dots> = 1" using x K by(auto simp add: K_def card_gt_0_iff)
  10.561 -    finally show "?lhs x = 1" .
  10.562 -  qed
  10.563 -  also have "nat \<dots> = card (\<Union>A)" by simp
  10.564 -  finally show ?thesis ..
  10.565 -qed
  10.566 -
  10.567 -text{* The number of nat lists of length @{text m} summing to @{text N} is
  10.568 -@{term "(N + m - 1) choose N"}: *} 
  10.569 -
  10.570 -lemma card_length_listsum_rec:
  10.571 -  assumes "m\<ge>1"
  10.572 -  shows "card {l::nat list. length l = m \<and> listsum l = N} =
  10.573 -    (card {l. length l = (m - 1) \<and> listsum l = N} +
  10.574 -    card {l. length l = m \<and> listsum l + 1 =  N})"
  10.575 -    (is "card ?C = (card ?A + card ?B)")
  10.576 -proof - 
  10.577 -  let ?A'="{l. length l = m \<and> listsum l = N \<and> hd l = 0}"
  10.578 -  let ?B'="{l. length l = m \<and> listsum l = N \<and> hd l \<noteq> 0}"
  10.579 -  let ?f ="\<lambda> l. 0#l"
  10.580 -  let ?g ="\<lambda> l. (hd l + 1) # tl l"
  10.581 -  have 1: "\<And>xs x. xs \<noteq> [] \<Longrightarrow> x = hd xs \<Longrightarrow> x # tl xs = xs" by simp
  10.582 -  have 2: "\<And>xs. (xs::nat list) \<noteq> [] \<Longrightarrow> listsum(tl xs) = listsum xs - hd xs"
  10.583 -    by(auto simp add: neq_Nil_conv)
  10.584 -  have f: "bij_betw ?f ?A ?A'"
  10.585 -    apply(rule bij_betw_byWitness[where f' = tl])
  10.586 -    using assms 
  10.587 -    by (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
  10.588 -  have 3: "\<And>xs:: nat list. xs \<noteq> [] \<Longrightarrow> hd xs + (listsum xs - hd xs) = listsum xs"
  10.589 -    by (metis 1 listsum_simps(2) 2)
  10.590 -  have g: "bij_betw ?g ?B ?B'"
  10.591 -    apply(rule bij_betw_byWitness[where f' = "\<lambda> l. (hd l - 1) # tl l"])
  10.592 -    using assms
  10.593 -    by (auto simp: 2 length_0_conv[symmetric] intro!: 3
  10.594 -      simp del: length_greater_0_conv length_0_conv)
  10.595 -  { fix M N :: nat have "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}"
  10.596 -    using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto }
  10.597 -    note fin = this
  10.598 -  have fin_A: "finite ?A" using fin[of _ "N+1"]
  10.599 -    by (intro finite_subset[where ?A = "?A" and ?B = "{xs. size xs = m - 1 \<and> set xs \<subseteq> {0..<N+1}}"], 
  10.600 -      auto simp: member_le_listsum_nat less_Suc_eq_le)
  10.601 -  have fin_B: "finite ?B"
  10.602 -    by (intro finite_subset[where ?A = "?B" and ?B = "{xs. size xs = m \<and> set xs \<subseteq> {0..<N}}"], 
  10.603 -      auto simp: member_le_listsum_nat less_Suc_eq_le fin)
  10.604 -  have uni: "?C = ?A' \<union> ?B'" by auto
  10.605 -  have disj: "?A' \<inter> ?B' = {}" by auto
  10.606 -  have "card ?C = card(?A' \<union> ?B')" using uni by simp
  10.607 -  also have "\<dots> = card ?A + card ?B"
  10.608 -    using card_Un_disjoint[OF _ _ disj] bij_betw_finite[OF f] bij_betw_finite[OF g]
  10.609 -      bij_betw_same_card[OF f] bij_betw_same_card[OF g] fin_A fin_B
  10.610 -    by presburger
  10.611 -  finally show ?thesis .
  10.612 -qed
  10.613 -
  10.614 -lemma card_length_listsum: --"By Holden Lee, tidied by Tobias Nipkow"
  10.615 -  "card {l::nat list. size l = m \<and> listsum l = N} = (N + m - 1) choose N"
  10.616 -proof (cases m)
  10.617 -  case 0 then show ?thesis
  10.618 -    by (cases N) (auto simp: cong: conj_cong)
  10.619 -next
  10.620 -  case (Suc m')
  10.621 -    have m: "m\<ge>1" by (simp add: Suc)
  10.622 -    then show ?thesis
  10.623 -    proof (induct "N + m - 1" arbitrary: N m)
  10.624 -      case 0   -- "In the base case, the only solution is [0]."
  10.625 -      have [simp]: "{l::nat list. length l = Suc 0 \<and> (\<forall>n\<in>set l. n = 0)} = {[0]}"
  10.626 -        by (auto simp: length_Suc_conv)
  10.627 -      have "m=1 \<and> N=0" using 0 by linarith
  10.628 -      then show ?case by simp
  10.629 -    next
  10.630 -      case (Suc k)
  10.631 -      
  10.632 -      have c1: "card {l::nat list. size l = (m - 1) \<and> listsum l =  N} = 
  10.633 -        (N + (m - 1) - 1) choose N"
  10.634 -      proof cases
  10.635 -        assume "m = 1"
  10.636 -        with Suc.hyps have "N\<ge>1" by auto
  10.637 -        with `m = 1` show ?thesis by (simp add: binomial_eq_0)
  10.638 -      next
  10.639 -        assume "m \<noteq> 1" thus ?thesis using Suc by fastforce
  10.640 -      qed
  10.641 -    
  10.642 -      from Suc have c2: "card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
  10.643 -        (if N>0 then ((N - 1) + m - 1) choose (N - 1) else 0)"
  10.644 -      proof -
  10.645 -        have aux: "\<And>m n. n > 0 \<Longrightarrow> Suc m = n \<longleftrightarrow> m = n - 1" by arith
  10.646 -        from Suc have "N>0 \<Longrightarrow>
  10.647 -          card {l::nat list. size l = m \<and> listsum l + 1 = N} = 
  10.648 -          ((N - 1) + m - 1) choose (N - 1)" by (simp add: aux)
  10.649 -        thus ?thesis by auto
  10.650 -      qed
  10.651 -    
  10.652 -      from Suc.prems have "(card {l::nat list. size l = (m - 1) \<and> listsum l = N} + 
  10.653 -          card {l::nat list. size l = m \<and> listsum l + 1 = N}) = (N + m - 1) choose N"
  10.654 -        by (auto simp: c1 c2 choose_reduce_nat[of "N + m - 1" N] simp del: One_nat_def)
  10.655 -      thus ?case using card_length_listsum_rec[OF Suc.prems] by auto
  10.656 -    qed
  10.657 -qed
  10.658 -
  10.659 -end
    11.1 --- a/src/HOL/Number_Theory/Cong.thy	Tue Mar 10 11:56:32 2015 +0100
    11.2 +++ b/src/HOL/Number_Theory/Cong.thy	Tue Mar 10 15:20:40 2015 +0000
    11.3 @@ -461,15 +461,7 @@
    11.4  
    11.5  lemma cong_to_1'_nat: "[(a::nat) = 1] (mod n) \<longleftrightarrow>
    11.6      a = 0 \<and> n = 1 \<or> (\<exists>m. a = 1 + m * n)"
    11.7 -  apply (cases "n = 1")
    11.8 -  apply auto [1]
    11.9 -  apply (drule_tac x = "a - 1" in spec)
   11.10 -  apply force
   11.11 -  apply (cases "a = 0", simp add: cong_0_1_nat)
   11.12 -  apply (rule iffI)
   11.13 -  apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult.commute mult_eq_if)
   11.14 -  apply (metis cong_add_lcancel_0_nat cong_mult_self_nat)
   11.15 -  done
   11.16 +by (metis add.right_neutral cong_0_1_nat cong_iff_lin_nat cong_to_1_nat dvd_div_mult_self leI le_add_diff_inverse less_one mult_eq_if)
   11.17  
   11.18  lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
   11.19    by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
   11.20 @@ -579,7 +571,7 @@
   11.21        [x = y] (mod (PROD i:A. m i))"
   11.22    apply (induct set: finite)
   11.23    apply auto
   11.24 -  apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat)
   11.25 +  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
   11.26    done
   11.27  
   11.28  lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
   11.29 @@ -835,7 +827,7 @@
   11.30           [x = y] (mod (PROD i:A. m i))"
   11.31    apply (induct set: finite)
   11.32    apply auto
   11.33 -  apply (metis coprime_cong_mult_nat mult.commute setprod_coprime_nat)
   11.34 +  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
   11.35    done
   11.36  
   11.37  lemma chinese_remainder_unique_nat:
    12.1 --- a/src/HOL/Number_Theory/Fib.thy	Tue Mar 10 11:56:32 2015 +0100
    12.2 +++ b/src/HOL/Number_Theory/Fib.thy	Tue Mar 10 15:20:40 2015 +0000
    12.3 @@ -11,7 +11,7 @@
    12.4  section {* Fib *}
    12.5  
    12.6  theory Fib
    12.7 -imports Binomial
    12.8 +imports Main "../GCD"
    12.9  begin
   12.10  
   12.11  
    13.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 11:56:32 2015 +0100
    13.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 15:20:40 2015 +0000
    13.3 @@ -28,7 +28,7 @@
    13.4  section {* Primes *}
    13.5  
    13.6  theory Primes
    13.7 -imports "~~/src/HOL/GCD"
    13.8 +imports "~~/src/HOL/GCD" "~~/src/HOL/Fact"
    13.9  begin
   13.10  
   13.11  declare [[coercion int]]
    14.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 11:56:32 2015 +0100
    14.2 +++ b/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 15:20:40 2015 +0000
    14.3 @@ -8,10 +8,7 @@
    14.4  section {* Residue rings *}
    14.5  
    14.6  theory Residues
    14.7 -imports
    14.8 -  UniqueFactorization
    14.9 -  Binomial
   14.10 -  MiscAlgebra
   14.11 +imports UniqueFactorization MiscAlgebra
   14.12  begin
   14.13  
   14.14  (*
   14.15 @@ -275,15 +272,15 @@
   14.16    then have cop: "\<And>x. x \<in> {1::nat..p - 1} \<Longrightarrow> coprime x p"
   14.17      by blast
   14.18    { fix x::nat assume *: "1 < x" "x < p" and "x dvd p"
   14.19 -    have "coprime x p" 
   14.20 +    have "coprime x p"
   14.21        apply (rule cop)
   14.22        using * apply auto
   14.23        done
   14.24      with `x dvd p` `1 < x` have "False" by auto }
   14.25 -  then show ?thesis 
   14.26 -    using `2 \<le> p` 
   14.27 +  then show ?thesis
   14.28 +    using `2 \<le> p`
   14.29      by (simp add: prime_def)
   14.30 -       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
   14.31 +       (metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0
   14.32                not_numeral_le_zero one_dvd)
   14.33  qed
   14.34  
   14.35 @@ -367,7 +364,7 @@
   14.36    also have "phi p = nat p - 1"
   14.37      by (rule phi_prime, rule assms)
   14.38    finally show ?thesis
   14.39 -    by (metis nat_int) 
   14.40 +    by (metis nat_int)
   14.41  qed
   14.42  
   14.43  lemma fermat_theorem_nat:
   14.44 @@ -441,7 +438,7 @@
   14.45  lemma wilson_theorem:
   14.46    assumes "prime p" shows "[fact (p - 1) = - 1] (mod p)"
   14.47  proof (cases "p = 2")
   14.48 -  case True 
   14.49 +  case True
   14.50    then show ?thesis
   14.51      by (simp add: cong_int_def fact_altdef_nat)
   14.52  next
    15.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 11:56:32 2015 +0100
    15.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 15:20:40 2015 +0000
    15.3 @@ -1,5 +1,5 @@
    15.4  (*  Title:      HOL/Probability/Probability_Mass_Function.thy
    15.5 -    Author:     Johannes Hölzl, TU München 
    15.6 +    Author:     Johannes Hölzl, TU München
    15.7      Author:     Andreas Lochbihler, ETH Zurich
    15.8  *)
    15.9  
   15.10 @@ -8,7 +8,6 @@
   15.11  theory Probability_Mass_Function
   15.12  imports
   15.13    Giry_Monad
   15.14 -  "~~/src/HOL/Number_Theory/Binomial"
   15.15    "~~/src/HOL/Library/Multiset"
   15.16  begin
   15.17  
   15.18 @@ -52,14 +51,14 @@
   15.19      fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
   15.20      then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
   15.21        by (metis infinite_arbitrarily_large)
   15.22 -    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" 
   15.23 +    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
   15.24        by auto
   15.25      { fix x assume "x \<in> X"
   15.26        from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
   15.27        then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
   15.28      note singleton_sets = this
   15.29      have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
   15.30 -      using `?M \<noteq> 0` 
   15.31 +      using `?M \<noteq> 0`
   15.32        by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
   15.33      also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
   15.34        by (rule setsum_mono) fact
   15.35 @@ -82,7 +81,7 @@
   15.36    assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)"
   15.37    then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S"
   15.38      by auto
   15.39 -  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = 
   15.40 +  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) =
   15.41      (\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)"
   15.42      by (subst emeasure_UN_countable)
   15.43         (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
   15.44 @@ -136,7 +135,7 @@
   15.45  interpretation pmf_as_measure .
   15.46  
   15.47  lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
   15.48 -  by transfer blast 
   15.49 +  by transfer blast
   15.50  
   15.51  lemma sets_measure_pmf_count_space[measurable_cong]:
   15.52    "sets (measure_pmf M) = sets (count_space UNIV)"
   15.53 @@ -353,10 +352,10 @@
   15.54  
   15.55    have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
   15.56      by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
   15.57 -    
   15.58 +
   15.59    show "prob_space (f \<guillemotright>= g)"
   15.60      using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
   15.61 -  then interpret fg: prob_space "f \<guillemotright>= g" . 
   15.62 +  then interpret fg: prob_space "f \<guillemotright>= g" .
   15.63    show [simp]: "sets (f \<guillemotright>= g) = UNIV"
   15.64      using sets_eq_imp_space_eq[OF s_f]
   15.65      by (subst sets_bind[where N="count_space UNIV"]) auto
   15.66 @@ -385,7 +384,7 @@
   15.67    by transfer (simp add: bind_const' prob_space_imp_subprob_space)
   15.68  
   15.69  lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
   15.70 -  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind  
   15.71 +  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind
   15.72    by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
   15.73  
   15.74  lemma bind_pmf_cong:
   15.75 @@ -415,7 +414,7 @@
   15.76    using measurable_measure_pmf[of N]
   15.77    unfolding measure_pmf_bind
   15.78    by (subst emeasure_bind[where N="count_space UNIV"]) auto
   15.79 -                                
   15.80 +
   15.81  lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
   15.82    by (auto intro!: prob_space_return simp: AE_return measure_return)
   15.83  
   15.84 @@ -451,7 +450,7 @@
   15.85  proof -
   15.86    have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
   15.87       (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
   15.88 -    unfolding map_pmf_def[abs_def] comp_def by transfer_prover 
   15.89 +    unfolding map_pmf_def[abs_def] comp_def by transfer_prover
   15.90    then show ?thesis
   15.91      by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
   15.92  qed
   15.93 @@ -468,7 +467,7 @@
   15.94    using map_pmf_id unfolding id_def .
   15.95  
   15.96  lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g"
   15.97 -  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) 
   15.98 +  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def)
   15.99  
  15.100  lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M"
  15.101    using map_pmf_compose[of f g] by (simp add: comp_def)
  15.102 @@ -665,7 +664,7 @@
  15.103    show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
  15.104    proof (rule measure_eqI)
  15.105      fix A :: "'a set"
  15.106 -    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
  15.107 +    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
  15.108        (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
  15.109        by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
  15.110      also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
  15.111 @@ -706,9 +705,9 @@
  15.112  
  15.113  setup_lifting td_pmf_embed_pmf
  15.114  
  15.115 -lemma set_pmf_transfer[transfer_rule]: 
  15.116 +lemma set_pmf_transfer[transfer_rule]:
  15.117    assumes "bi_total A"
  15.118 -  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"  
  15.119 +  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"
  15.120    using `bi_total A`
  15.121    by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
  15.122       metis+
  15.123 @@ -888,14 +887,14 @@
  15.124  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
  15.125  for R p q
  15.126  where
  15.127 -  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; 
  15.128 +  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y;
  15.129       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
  15.130    \<Longrightarrow> rel_pmf R p q"
  15.131  
  15.132  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
  15.133  proof -
  15.134    show "map_pmf id = id" by (rule map_pmf_id)
  15.135 -  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
  15.136 +  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
  15.137    show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p"
  15.138      by (intro map_pmf_cong refl)
  15.139  
  15.140 @@ -1042,7 +1041,7 @@
  15.141                     map_pair)
  15.142  qed
  15.143  
  15.144 -lemma rel_pmf_reflI: 
  15.145 +lemma rel_pmf_reflI:
  15.146    assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
  15.147    shows "rel_pmf P p p"
  15.148    by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
  15.149 @@ -1089,7 +1088,7 @@
  15.150      and q: "q = map_pmf snd pq"
  15.151      and P: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> rel_pmf P x y"
  15.152      by cases auto
  15.153 -  from P obtain PQ 
  15.154 +  from P obtain PQ
  15.155      where PQ: "\<And>x y a b. \<lbrakk> (x, y) \<in> set_pmf pq; (a, b) \<in> set_pmf (PQ x y) \<rbrakk> \<Longrightarrow> P a b"
  15.156      and x: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf fst (PQ x y) = x"
  15.157      and y: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf snd (PQ x y) = y"
  15.158 @@ -1112,12 +1111,12 @@
  15.159  
  15.160  text {*
  15.161    Proof that @{const rel_pmf} preserves orders.
  15.162 -  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, 
  15.163 -  Theoretical Computer Science 12(1):19--37, 1980, 
  15.164 +  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
  15.165 +  Theoretical Computer Science 12(1):19--37, 1980,
  15.166    @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
  15.167  *}
  15.168  
  15.169 -lemma 
  15.170 +lemma
  15.171    assumes *: "rel_pmf R p q"
  15.172    and refl: "reflp R" and trans: "transp R"
  15.173    shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
  15.174 @@ -1174,7 +1173,7 @@
  15.175      hence "measure (measure_pmf p) (?E x) \<noteq> 0"
  15.176        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
  15.177      hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
  15.178 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" 
  15.179 +    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
  15.180        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
  15.181    ultimately show "inf R R\<inverse>\<inverse> x y"
  15.182      by (auto simp add: pq_def)
  15.183 @@ -1235,13 +1234,13 @@
  15.184  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
  15.185    by (auto simp add: set_pmf_iff UNIV_bool)
  15.186  
  15.187 -lemma nn_integral_bernoulli_pmf[simp]: 
  15.188 +lemma nn_integral_bernoulli_pmf[simp]:
  15.189    assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
  15.190    shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
  15.191    by (subst nn_integral_measure_pmf_support[of UNIV])
  15.192       (auto simp: UNIV_bool field_simps)
  15.193  
  15.194 -lemma integral_bernoulli_pmf[simp]: 
  15.195 +lemma integral_bernoulli_pmf[simp]:
  15.196    assumes [simp]: "0 \<le> p" "p \<le> 1"
  15.197    shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
  15.198    by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
  15.199 @@ -1277,7 +1276,7 @@
  15.200  
  15.201  lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M"
  15.202  proof
  15.203 -  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"  
  15.204 +  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
  15.205      using M_not_empty
  15.206      by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
  15.207                    setsum_divide_distrib[symmetric])
  15.208 @@ -1300,7 +1299,7 @@
  15.209  
  15.210  lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S"
  15.211  proof
  15.212 -  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"  
  15.213 +  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
  15.214      using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto
  15.215  qed simp
  15.216  
    16.1 --- a/src/HOL/ROOT	Tue Mar 10 11:56:32 2015 +0100
    16.2 +++ b/src/HOL/ROOT	Tue Mar 10 15:20:40 2015 +0000
    16.3 @@ -285,7 +285,6 @@
    16.4      (* Preliminaries from set and number theory *)
    16.5      "~~/src/HOL/Library/FuncSet"
    16.6      "~~/src/HOL/Number_Theory/Primes"
    16.7 -    "~~/src/HOL/Number_Theory/Binomial"
    16.8      "~~/src/HOL/Library/Permutation"
    16.9    theories
   16.10      (*** New development, based on explicit structures ***)
    17.1 --- a/src/HOL/Rat.thy	Tue Mar 10 11:56:32 2015 +0100
    17.2 +++ b/src/HOL/Rat.thy	Tue Mar 10 15:20:40 2015 +0000
    17.3 @@ -638,10 +638,6 @@
    17.4  
    17.5  subsection {* Embedding from Rationals to other Fields *}
    17.6  
    17.7 -class field_char_0 = field + ring_char_0
    17.8 -
    17.9 -subclass (in linordered_field) field_char_0 ..
   17.10 -
   17.11  context field_char_0
   17.12  begin
   17.13