The factorial function, "fact", now has type "nat => 'a"
authorpaulson <lp15@cam.ac.uk>
Mon Mar 16 15:30:00 2015 +0000 (2015-03-16)
changeset 59730b7c394c7a619
parent 59669 de7792ea4090
child 59731 7fccaeec22f0
The factorial function, "fact", now has type "nat => 'a"
NEWS
src/HOL/Binomial.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Permutations.thy
src/HOL/MacLaurin.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/Proofs/Extraction/Util.thy
src/HOL/Taylor.thy
src/HOL/Transcendental.thy
src/HOL/ex/Birthday_Paradox.thy
     1.1 --- a/NEWS	Tue Mar 10 16:12:35 2015 +0000
     1.2 +++ b/NEWS	Mon Mar 16 15:30:00 2015 +0000
     1.3 @@ -80,6 +80,12 @@
     1.4    type, so in particular on "real" and "complex" uniformly.
     1.5    Minor INCOMPATIBILITY: type constraints may be needed.
     1.6  
     1.7 +* The factorial function, "fact", now has type "nat => 'a" (of a sort that admits
     1.8 +  numeric types including nat, int, real and complex. INCOMPATIBILITY:
     1.9 +  an expression such as "fact 3 = 6" may require a type constraint, and the combination
    1.10 +  "real (fact k)" is likely to be unsatisfactory. If a type conversion is still necessary,
    1.11 +  then use "of_nat (fact k)".
    1.12 +
    1.13  * removed functions "natfloor" and "natceiling",
    1.14    use "nat o floor" and "nat o ceiling" instead.
    1.15    A few of the lemmas have been retained and adapted: in their names
     2.1 --- a/src/HOL/Binomial.thy	Tue Mar 10 16:12:35 2015 +0000
     2.2 +++ b/src/HOL/Binomial.thy	Mon Mar 16 15:30:00 2015 +0000
     2.3 @@ -11,182 +11,99 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -class fact =
     2.8 -  fixes fact :: "'a \<Rightarrow> 'a"
     2.9 +subsection {* Factorial *}
    2.10 +
    2.11 +fun fact :: "nat \<Rightarrow> ('a::{semiring_char_0,semiring_no_zero_divisors})"
    2.12 +  where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
    2.13  
    2.14 -instantiation nat :: fact
    2.15 -begin
    2.16 +lemmas fact_Suc = fact.simps(2)
    2.17 +
    2.18 +lemma fact_1 [simp]: "fact 1 = 1"
    2.19 +  by simp
    2.20 +
    2.21 +lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
    2.22 +  by simp
    2.23  
    2.24 -fun
    2.25 -  fact_nat :: "nat \<Rightarrow> nat"
    2.26 -where
    2.27 -  fact_0_nat: "fact_nat 0 = Suc 0"
    2.28 -| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
    2.29 +lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
    2.30 +  by (induct n) (auto simp add: algebra_simps of_nat_mult)
    2.31 + 
    2.32 +lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
    2.33 +  by (cases n) auto
    2.34  
    2.35 -instance ..
    2.36 +lemma fact_nonzero [simp]: "fact n \<noteq> 0"
    2.37 +  apply (induct n)
    2.38 +  apply auto
    2.39 +  using of_nat_eq_0_iff by fastforce
    2.40 +
    2.41 +lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
    2.42 +  by (induct n) (auto simp: le_Suc_eq)
    2.43  
    2.44 -end
    2.45 -
    2.46 -(* definitions for the integers *)
    2.47 -
    2.48 -instantiation int :: fact
    2.49 -
    2.50 +context
    2.51 +  fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
    2.52  begin
    2.53 +  
    2.54 +  lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
    2.55 +    by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
    2.56 +  
    2.57 +  lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
    2.58 +    by (metis le0 fact.simps(1) fact_mono)
    2.59 +  
    2.60 +  lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
    2.61 +    using fact_ge_1 less_le_trans zero_less_one by blast
    2.62 +  
    2.63 +  lemma fact_ge_zero [simp]: "fact n \<ge> (0 :: 'a)"
    2.64 +    by (simp add: less_imp_le)
    2.65  
    2.66 -definition
    2.67 -  fact_int :: "int \<Rightarrow> int"
    2.68 -where
    2.69 -  "fact_int x = (if x >= 0 then int (fact (nat x)) else 0)"
    2.70 -
    2.71 -instance proof qed
    2.72 +  lemma fact_not_neg [simp]: "~ (fact n < (0 :: 'a))"
    2.73 +    by (simp add: not_less_iff_gr_or_eq)
    2.74 +    
    2.75 +  lemma fact_le_power:
    2.76 +      "fact n \<le> (of_nat (n^n) ::'a)"
    2.77 +  proof (induct n)
    2.78 +    case (Suc n)
    2.79 +    then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
    2.80 +      by (rule order_trans) (simp add: power_mono)
    2.81 +    have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
    2.82 +      by (simp add: algebra_simps)
    2.83 +    also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)"
    2.84 +      by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono)
    2.85 +    also have "... \<le> (of_nat (Suc n ^ Suc n) ::'a)"
    2.86 +      by (metis of_nat_mult order_refl power_Suc)
    2.87 +    finally show ?case .
    2.88 +  qed simp
    2.89  
    2.90  end
    2.91  
    2.92 -
    2.93 -subsection {* Set up Transfer *}
    2.94 -
    2.95 -lemma transfer_nat_int_factorial:
    2.96 -  "(x::int) >= 0 \<Longrightarrow> fact (nat x) = nat (fact x)"
    2.97 -  unfolding fact_int_def
    2.98 -  by auto
    2.99 -
   2.100 -
   2.101 -lemma transfer_nat_int_factorial_closure:
   2.102 -  "x >= (0::int) \<Longrightarrow> fact x >= 0"
   2.103 -  by (auto simp add: fact_int_def)
   2.104 -
   2.105 -declare transfer_morphism_nat_int[transfer add return:
   2.106 -    transfer_nat_int_factorial transfer_nat_int_factorial_closure]
   2.107 -
   2.108 -lemma transfer_int_nat_factorial:
   2.109 -  "fact (int x) = int (fact x)"
   2.110 -  unfolding fact_int_def by auto
   2.111 -
   2.112 -lemma transfer_int_nat_factorial_closure:
   2.113 -  "is_nat x \<Longrightarrow> fact x >= 0"
   2.114 -  by (auto simp add: fact_int_def)
   2.115 -
   2.116 -declare transfer_morphism_int_nat[transfer add return:
   2.117 -    transfer_int_nat_factorial transfer_int_nat_factorial_closure]
   2.118 -
   2.119 -
   2.120 -subsection {* Factorial *}
   2.121 -
   2.122 -lemma fact_0_int [simp]: "fact (0::int) = 1"
   2.123 -  by (simp add: fact_int_def)
   2.124 +text{*Note that @{term "fact 0 = fact 1"}*}
   2.125 +lemma fact_less_mono_nat: "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: nat)"
   2.126 +  by (induct n) (auto simp: less_Suc_eq)
   2.127  
   2.128 -lemma fact_1_nat [simp]: "fact (1::nat) = 1"
   2.129 -  by simp
   2.130 -
   2.131 -lemma fact_Suc_0_nat [simp]: "fact (Suc 0) = Suc 0"
   2.132 -  by simp
   2.133 -
   2.134 -lemma fact_1_int [simp]: "fact (1::int) = 1"
   2.135 -  by (simp add: fact_int_def)
   2.136 -
   2.137 -lemma fact_plus_one_nat: "fact ((n::nat) + 1) = (n + 1) * fact n"
   2.138 -  by simp
   2.139 -
   2.140 -lemma fact_plus_one_int:
   2.141 -  assumes "n >= 0"
   2.142 -  shows "fact ((n::int) + 1) = (n + 1) * fact n"
   2.143 -  using assms unfolding fact_int_def
   2.144 -  by (simp add: nat_add_distrib algebra_simps int_mult)
   2.145 +lemma fact_less_mono:
   2.146 +  fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
   2.147 +  shows "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a)"
   2.148 +  by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
   2.149  
   2.150 -lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   2.151 -  apply (subgoal_tac "n = Suc (n - 1)")
   2.152 -  apply (erule ssubst)
   2.153 -  apply (subst fact_Suc)
   2.154 -  apply simp_all
   2.155 -  done
   2.156 -
   2.157 -lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   2.158 -  apply (subgoal_tac "n = (n - 1) + 1")
   2.159 -  apply (erule ssubst)
   2.160 -  apply (subst fact_plus_one_int)
   2.161 -  apply simp_all
   2.162 -  done
   2.163 -
   2.164 -lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
   2.165 -  apply (induct n)
   2.166 -  apply (auto simp add: fact_plus_one_nat)
   2.167 -  done
   2.168 +lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
   2.169 +  by (metis One_nat_def fact_ge_1)
   2.170  
   2.171 -lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
   2.172 -  by (simp add: fact_int_def)
   2.173 -
   2.174 -lemma fact_gt_zero_nat [simp]: "fact (n :: nat) > 0"
   2.175 -  by (insert fact_nonzero_nat [of n], arith)
   2.176 -
   2.177 -lemma fact_gt_zero_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) > 0"
   2.178 -  by (auto simp add: fact_int_def)
   2.179 -
   2.180 -lemma fact_ge_one_nat [simp]: "fact (n :: nat) >= 1"
   2.181 -  by (insert fact_nonzero_nat [of n], arith)
   2.182 -
   2.183 -lemma fact_ge_Suc_0_nat [simp]: "fact (n :: nat) >= Suc 0"
   2.184 -  by (insert fact_nonzero_nat [of n], arith)
   2.185 +lemma dvd_fact: 
   2.186 +  shows "1 \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
   2.187 +  by (induct n) (auto simp: dvdI le_Suc_eq)
   2.188  
   2.189 -lemma fact_ge_one_int [simp]: "n >= 0 \<Longrightarrow> fact (n :: int) >= 1"
   2.190 -  apply (auto simp add: fact_int_def)
   2.191 -  apply (subgoal_tac "1 = int 1")
   2.192 -  apply (erule ssubst)
   2.193 -  apply (subst zle_int)
   2.194 -  apply auto
   2.195 -  done
   2.196 -
   2.197 -lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   2.198 -  apply (induct n)
   2.199 -  apply force
   2.200 -  apply (auto simp only: fact_Suc)
   2.201 -  apply (subgoal_tac "m = Suc n")
   2.202 -  apply (erule ssubst)
   2.203 -  apply (rule dvd_triv_left)
   2.204 -  apply auto
   2.205 -  done
   2.206 +lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
   2.207 +  by (induct n) (auto simp: atLeastAtMostSuc_conv)
   2.208  
   2.209 -lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
   2.210 -  apply (case_tac "1 <= n")
   2.211 -  apply (induct n rule: int_ge_induct)
   2.212 -  apply (auto simp add: fact_plus_one_int)
   2.213 -  apply (subgoal_tac "m = i + 1")
   2.214 -  apply auto
   2.215 -  done
   2.216 -
   2.217 -lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow>
   2.218 -  {i..j+1} = {i..j} Un {j+1}"
   2.219 -  by auto
   2.220 -
   2.221 -lemma interval_Suc: "i <= Suc j \<Longrightarrow> {i..Suc j} = {i..j} Un {Suc j}"
   2.222 -  by auto
   2.223 -
   2.224 -lemma interval_plus_one_int: "(i::int) <= j + 1 \<Longrightarrow> {i..j+1} = {i..j} Un {j+1}"
   2.225 -  by auto
   2.226 +lemma fact_altdef: "fact n = setprod of_nat {1..n}"
   2.227 +  by (induct n) (auto simp: atLeastAtMostSuc_conv)
   2.228  
   2.229 -lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
   2.230 -  apply (induct n)
   2.231 -  apply force
   2.232 -  apply (subst fact_Suc)
   2.233 -  apply (subst interval_Suc)
   2.234 -  apply auto
   2.235 -done
   2.236 +lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
   2.237 +  by (induct m) (auto simp: le_Suc_eq)
   2.238  
   2.239 -lemma fact_altdef_int: "n >= 0 \<Longrightarrow> fact (n::int) = (PROD i:{1..n}. i)"
   2.240 -  apply (induct n rule: int_ge_induct)
   2.241 -  apply force
   2.242 -  apply (subst fact_plus_one_int, assumption)
   2.243 -  apply (subst interval_plus_one_int)
   2.244 -  apply auto
   2.245 -done
   2.246 -
   2.247 -lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd fact (m::nat)"
   2.248 -  by (auto simp add: fact_altdef_nat intro!: setprod_dvd_setprod_subset)
   2.249 -
   2.250 -lemma fact_mod: "m \<le> (n::nat) \<Longrightarrow> fact n mod fact m = 0"
   2.251 -  by (auto simp add: dvd_imp_mod_0 fact_dvd)
   2.252 +lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a :: {semiring_div,linordered_semidom}) = 0"
   2.253 +  by (auto simp add: fact_dvd)
   2.254  
   2.255  lemma fact_div_fact:
   2.256 -  assumes "m \<ge> (n :: nat)"
   2.257 +  assumes "m \<ge> n"
   2.258    shows "(fact m) div (fact n) = \<Prod>{n + 1..m}"
   2.259  proof -
   2.260    obtain d where "d = m - n" by auto
   2.261 @@ -202,107 +119,17 @@
   2.262      also from Suc.hyps have "... = Suc (n + d') * \<Prod>{n + 1..n + d'}"
   2.263        unfolding div_mult1_eq[of _ "fact (n + d')"] by (simp add: fact_mod)
   2.264      also have "... = \<Prod>{n + 1..n + Suc d'}"
   2.265 -      by (simp add: atLeastAtMostSuc_conv setprod.insert)
   2.266 +      by (simp add: atLeastAtMostSuc_conv)
   2.267      finally show ?case .
   2.268    qed
   2.269    from this `m = n + d` show ?thesis by simp
   2.270  qed
   2.271  
   2.272 -lemma fact_mono_nat: "(m::nat) \<le> n \<Longrightarrow> fact m \<le> fact n"
   2.273 -apply (drule le_imp_less_or_eq)
   2.274 -apply (auto dest!: less_imp_Suc_add)
   2.275 -apply (induct_tac k, auto)
   2.276 -done
   2.277 -
   2.278 -lemma fact_neg_int [simp]: "m < (0::int) \<Longrightarrow> fact m = 0"
   2.279 -  unfolding fact_int_def by auto
   2.280 -
   2.281 -lemma fact_ge_zero_int [simp]: "fact m >= (0::int)"
   2.282 -  apply (case_tac "m >= 0")
   2.283 -  apply auto
   2.284 -  apply (frule fact_gt_zero_int)
   2.285 -  apply arith
   2.286 -done
   2.287 -
   2.288 -lemma fact_mono_int_aux [rule_format]: "k >= (0::int) \<Longrightarrow>
   2.289 -    fact (m + k) >= fact m"
   2.290 -  apply (case_tac "m < 0")
   2.291 -  apply auto
   2.292 -  apply (induct k rule: int_ge_induct)
   2.293 -  apply auto
   2.294 -  apply (subst add.assoc [symmetric])
   2.295 -  apply (subst fact_plus_one_int)
   2.296 -  apply auto
   2.297 -  apply (erule order_trans)
   2.298 -  apply (subst mult_le_cancel_right1)
   2.299 -  apply (subgoal_tac "fact (m + i) >= 0")
   2.300 -  apply arith
   2.301 -  apply auto
   2.302 -done
   2.303 -
   2.304 -lemma fact_mono_int: "(m::int) <= n \<Longrightarrow> fact m <= fact n"
   2.305 -  apply (insert fact_mono_int_aux [of "n - m" "m"])
   2.306 -  apply auto
   2.307 -done
   2.308 -
   2.309 -text{*Note that @{term "fact 0 = fact 1"}*}
   2.310 -lemma fact_less_mono_nat: "[| (0::nat) < m; m < n |] ==> fact m < fact n"
   2.311 -apply (drule_tac m = m in less_imp_Suc_add, auto)
   2.312 -apply (induct_tac k, auto)
   2.313 -done
   2.314 -
   2.315 -lemma fact_less_mono_int_aux: "k >= 0 \<Longrightarrow> (0::int) < m \<Longrightarrow>
   2.316 -    fact m < fact ((m + 1) + k)"
   2.317 -  apply (induct k rule: int_ge_induct)
   2.318 -  apply (simp add: fact_plus_one_int)
   2.319 -  apply (subst (2) fact_reduce_int)
   2.320 -  apply (auto simp add: ac_simps)
   2.321 -  apply (erule order_less_le_trans)
   2.322 -  apply auto
   2.323 -  done
   2.324 -
   2.325 -lemma fact_less_mono_int: "(0::int) < m \<Longrightarrow> m < n \<Longrightarrow> fact m < fact n"
   2.326 -  apply (insert fact_less_mono_int_aux [of "n - (m + 1)" "m"])
   2.327 -  apply auto
   2.328 -done
   2.329 -
   2.330 -lemma fact_num_eq_if_nat: "fact (m::nat) =
   2.331 -  (if m=0 then 1 else m * fact (m - 1))"
   2.332 +lemma fact_num_eq_if: 
   2.333 +    "fact m = (if m=0 then 1 else of_nat m * fact (m - 1))"
   2.334  by (cases m) auto
   2.335  
   2.336 -lemma fact_add_num_eq_if_nat:
   2.337 -  "fact ((m::nat) + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
   2.338 -by (cases "m + n") auto
   2.339 -
   2.340 -lemma fact_add_num_eq_if2_nat:
   2.341 -  "fact ((m::nat) + n) =
   2.342 -    (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
   2.343 -by (cases m) auto
   2.344 -
   2.345 -lemma fact_le_power: "fact n \<le> n^n"
   2.346 -proof (induct n)
   2.347 -  case (Suc n)
   2.348 -  then have "fact n \<le> Suc n ^ n" by (rule le_trans) (simp add: power_mono)
   2.349 -  then show ?case by (simp add: add_le_mono)
   2.350 -qed simp
   2.351 -
   2.352 -subsection {* @{term fact} and @{term of_nat} *}
   2.353 -
   2.354 -lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
   2.355 -by auto
   2.356 -
   2.357 -lemma of_nat_fact_gt_zero [simp]: "(0::'a::{linordered_semidom}) < of_nat(fact n)" by auto
   2.358 -
   2.359 -lemma of_nat_fact_ge_zero [simp]: "(0::'a::linordered_semidom) \<le> of_nat(fact n)"
   2.360 -by simp
   2.361 -
   2.362 -lemma inv_of_nat_fact_gt_zero [simp]: "(0::'a::linordered_field) < inverse (of_nat (fact n))"
   2.363 -by (auto simp add: positive_imp_inverse_positive)
   2.364 -
   2.365 -lemma inv_of_nat_fact_ge_zero [simp]: "(0::'a::linordered_field) \<le> inverse (of_nat (fact n))"
   2.366 -by (auto intro: order_less_imp_le)
   2.367 -
   2.368 -lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
   2.369 +lemma fact_eq_rev_setprod_nat: "fact k = (\<Prod>i<k. k - i)"
   2.370    unfolding fact_altdef_nat
   2.371    by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
   2.372  
   2.373 @@ -317,7 +144,7 @@
   2.374  
   2.375  lemma fact_numeral:  --{*Evaluation for specific numerals*}
   2.376    "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
   2.377 -  by (simp add: numeral_eq_Suc)
   2.378 +  by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)
   2.379  
   2.380  
   2.381  text {* This development is based on the work of Andy Gordon and
   2.382 @@ -532,10 +359,11 @@
   2.383  
   2.384  lemma binomial_fact:
   2.385    assumes kn: "k \<le> n"
   2.386 -  shows "(of_nat (n choose k) :: 'a::{field,ring_char_0}) =
   2.387 -    of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
   2.388 +  shows "(of_nat (n choose k) :: 'a::field_char_0) =
   2.389 +         (fact n) / (fact k * fact(n - k))"
   2.390    using binomial_fact_lemma[OF kn]
   2.391 -  by (simp add: field_simps of_nat_mult [symmetric])
   2.392 +  apply (simp add: field_simps)
   2.393 +  by (metis mult.commute of_nat_fact of_nat_mult)
   2.394  
   2.395  lemma choose_row_sum: "(\<Sum>k=0..n. n choose k) = 2^n"
   2.396    using binomial [of 1 "1" n]
   2.397 @@ -626,8 +454,8 @@
   2.398      done
   2.399  qed
   2.400  
   2.401 -lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
   2.402 -  unfolding fact_altdef_nat
   2.403 +lemma pochhammer_fact: "fact n = pochhammer 1 n"
   2.404 +  unfolding fact_altdef
   2.405    apply (cases n)
   2.406     apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod)
   2.407    apply (rule setprod.reindex_cong [where l = Suc])
   2.408 @@ -711,7 +539,7 @@
   2.409    by simp
   2.410  
   2.411  lemma pochhammer_same: "pochhammer (- of_nat n) n =
   2.412 -    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
   2.413 +    ((- 1) ^ n :: 'a::{semiring_char_0,comm_ring_1,semiring_no_zero_divisors}) * (fact n)"
   2.414    unfolding pochhammer_minus[OF le_refl[of n]]
   2.415    by (simp add: of_nat_diff pochhammer_fact)
   2.416  
   2.417 @@ -720,7 +548,7 @@
   2.418  
   2.419  definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   2.420    where "a gchoose n =
   2.421 -    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
   2.422 +    (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
   2.423  
   2.424  lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
   2.425    apply (simp_all add: gbinomial_def)
   2.426 @@ -729,7 +557,7 @@
   2.427    apply simp
   2.428    done
   2.429  
   2.430 -lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
   2.431 +lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / (fact n)"
   2.432  proof (cases "n = 0")
   2.433    case True
   2.434    then show ?thesis by simp
   2.435 @@ -743,7 +571,8 @@
   2.436        eq setprod.distrib[symmetric])
   2.437  qed
   2.438  
   2.439 -lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
   2.440 +lemma binomial_gbinomial: 
   2.441 +    "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
   2.442  proof -
   2.443    { assume kn: "k > n"
   2.444      then have ?thesis
   2.445 @@ -769,10 +598,10 @@
   2.446      have ?thesis using kn
   2.447        apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
   2.448          gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
   2.449 -      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h
   2.450 +      apply (simp add: pochhammer_Suc_setprod fact_altdef h 
   2.451          of_nat_setprod setprod.distrib[symmetric] eq' del: One_nat_def power_Suc)
   2.452        unfolding setprod.union_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
   2.453 -      unfolding mult.assoc[symmetric]
   2.454 +      unfolding mult.assoc
   2.455        unfolding setprod.distrib[symmetric]
   2.456        apply simp
   2.457        apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
   2.458 @@ -791,40 +620,46 @@
   2.459    by (simp add: gbinomial_def)
   2.460  
   2.461  lemma gbinomial_mult_1:
   2.462 -  "a * (a gchoose n) =
   2.463 +  fixes a :: "'a :: field_char_0"
   2.464 +  shows "a * (a gchoose n) =
   2.465      of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"  (is "?l = ?r")
   2.466  proof -
   2.467 -  have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
   2.468 +  have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
   2.469      unfolding gbinomial_pochhammer
   2.470 -      pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
   2.471 -    by (simp add:  field_simps del: of_nat_Suc)
   2.472 +      pochhammer_Suc of_nat_mult right_diff_distrib power_Suc
   2.473 +    apply (simp del: of_nat_Suc fact.simps)
   2.474 +    apply (auto simp add: field_simps simp del: of_nat_Suc)
   2.475 +    done
   2.476    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
   2.477      by (simp add: field_simps)
   2.478    finally show ?thesis ..
   2.479  qed
   2.480  
   2.481  lemma gbinomial_mult_1':
   2.482 -    "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   2.483 +  fixes a :: "'a :: field_char_0"
   2.484 +  shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   2.485    by (simp add: mult.commute gbinomial_mult_1)
   2.486  
   2.487  lemma gbinomial_Suc:
   2.488 -    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))"
   2.489 +    "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / (fact (Suc k))"
   2.490    by (simp add: gbinomial_def)
   2.491  
   2.492  lemma gbinomial_mult_fact:
   2.493 -  "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) =
   2.494 +  fixes a :: "'a::field_char_0"
   2.495 +  shows
   2.496 +   "fact (Suc k) * (a gchoose (Suc k)) =
   2.497      (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   2.498 -  by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
   2.499 +  by (simp_all add: gbinomial_Suc field_simps del: fact.simps)
   2.500  
   2.501  lemma gbinomial_mult_fact':
   2.502 -  "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
   2.503 -    (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   2.504 +  fixes a :: "'a::field_char_0"
   2.505 +  shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   2.506    using gbinomial_mult_fact[of k a]
   2.507    by (subst mult.commute)
   2.508  
   2.509 -
   2.510  lemma gbinomial_Suc_Suc:
   2.511 -  "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
   2.512 +  fixes a :: "'a :: field_char_0"
   2.513 +  shows "(a + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
   2.514  proof (cases k)
   2.515    case 0
   2.516    then show ?thesis by simp
   2.517 @@ -835,31 +670,42 @@
   2.518        using Suc
   2.519        apply auto
   2.520      done
   2.521 -  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
   2.522 -    ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
   2.523 -    apply (simp add: Suc field_simps del: fact_Suc)
   2.524 +  have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
   2.525 +        (a gchoose Suc h) * (fact (Suc (Suc h))) +
   2.526 +        (a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
   2.527 +    by (simp add: Suc field_simps del: fact.simps)
   2.528 +  also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + 
   2.529 +                   (\<Prod>i = 0..Suc h. a - of_nat i)"
   2.530 +    by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
   2.531 +  also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) + 
   2.532 +                   (\<Prod>i = 0..Suc h. a - of_nat i)"
   2.533 +    by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
   2.534 +  also have "... =  of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) + 
   2.535 +                    (\<Prod>i = 0..Suc h. a - of_nat i)"
   2.536 +    by (metis gbinomial_mult_fact mult.commute)
   2.537 +  also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
   2.538 +                   (of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
   2.539 +    by (simp add: field_simps)
   2.540 +  also have "... = 
   2.541 +    ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
   2.542      unfolding gbinomial_mult_fact'
   2.543 -    apply (subst fact_Suc)
   2.544 -    unfolding of_nat_mult
   2.545 -    apply (subst mult.commute)
   2.546 -    unfolding mult.assoc
   2.547 -    unfolding gbinomial_mult_fact
   2.548 -    apply (simp add: field_simps)
   2.549 -    done
   2.550 +    by (simp add: comm_semiring_class.distrib field_simps Suc)
   2.551    also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
   2.552      unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
   2.553      by (simp add: field_simps Suc)
   2.554    also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
   2.555      using eq0
   2.556      by (simp add: Suc setprod_nat_ivl_1_Suc)
   2.557 -  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
   2.558 +  also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
   2.559      unfolding gbinomial_mult_fact ..
   2.560 -  finally show ?thesis by (simp del: fact_Suc)
   2.561 +  finally show ?thesis
   2.562 +    by (metis fact_nonzero mult_cancel_left) 
   2.563  qed
   2.564  
   2.565  lemma gbinomial_reduce_nat:
   2.566 -  "0 < k \<Longrightarrow> (a::'a::field_char_0) gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
   2.567 -by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
   2.568 +  fixes a :: "'a :: field_char_0"
   2.569 +  shows "0 < k \<Longrightarrow> a gchoose k = (a - 1) gchoose (k - 1) + ((a - 1) gchoose k)"
   2.570 +  by (metis Suc_pred' diff_add_cancel gbinomial_Suc_Suc)
   2.571  
   2.572  
   2.573  lemma binomial_symmetric:
   2.574 @@ -947,19 +793,16 @@
   2.575      n choose k = fact n div (fact k * fact (n - k))"
   2.576   by (subst binomial_fact_lemma [symmetric]) auto
   2.577  
   2.578 -lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
   2.579 -by (metis binomial_fact_lemma dvd_def)
   2.580 -
   2.581 -lemma choose_dvd_int:
   2.582 -  assumes "(0::int) <= k" and "k <= n"
   2.583 -  shows "fact k * fact (n - k) dvd fact n"
   2.584 -  apply (subst tsub_eq [symmetric], rule assms)
   2.585 -  apply (rule choose_dvd_nat [transferred])
   2.586 -  using assms apply auto
   2.587 +lemma choose_dvd: "k \<le> n \<Longrightarrow> fact k * fact (n - k) dvd (fact n :: 'a :: {semiring_div,linordered_semidom})"
   2.588 +  unfolding dvd_def
   2.589 +  apply (rule exI [where x="of_nat (n choose k)"])
   2.590 +  using binomial_fact_lemma [of k n, THEN arg_cong [where f = of_nat and 'b='a]]
   2.591 +  apply (auto simp: of_nat_mult)
   2.592    done
   2.593  
   2.594 -lemma fact_fact_dvd_fact: fixes k::nat shows "fact k * fact n dvd fact (n + k)"
   2.595 -by (metis add.commute add_diff_cancel_left' choose_dvd_nat le_add2)
   2.596 +lemma fact_fact_dvd_fact: 
   2.597 +    "fact k * fact n dvd (fact (k+n) :: 'a :: {semiring_div,linordered_semidom})"
   2.598 +by (metis add.commute add_diff_cancel_left' choose_dvd le_add2)
   2.599  
   2.600  lemma choose_mult_lemma:
   2.601       "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)"
   2.602 @@ -969,18 +812,17 @@
   2.603      by (simp add: assms binomial_altdef_nat)
   2.604    also have "... = fact (m+r+k) div (fact r * (fact k * fact m))"
   2.605      apply (subst div_mult_div_if_dvd)
   2.606 -    apply (auto simp: fact_fact_dvd_fact)
   2.607 +    apply (auto simp: algebra_simps fact_fact_dvd_fact)
   2.608      apply (metis add.assoc add.commute fact_fact_dvd_fact)
   2.609      done
   2.610    also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
   2.611      apply (subst div_mult_div_if_dvd [symmetric])
   2.612 -    apply (auto simp: fact_fact_dvd_fact)
   2.613 -    apply (metis dvd_trans dvd.dual_order.refl fact_fact_dvd_fact mult_dvd_mono mult.left_commute)
   2.614 +    apply (auto simp add: algebra_simps)
   2.615 +    apply (metis fact_fact_dvd_fact dvd.order.trans nat_mult_dvd_cancel_disj)
   2.616      done
   2.617    also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
   2.618      apply (subst div_mult_div_if_dvd)
   2.619 -    apply (auto simp: fact_fact_dvd_fact)
   2.620 -    apply(metis mult.left_commute)
   2.621 +    apply (auto simp: fact_fact_dvd_fact algebra_simps)
   2.622      done
   2.623    finally show ?thesis
   2.624      by (simp add: binomial_altdef_nat mult.commute)
   2.625 @@ -1009,7 +851,7 @@
   2.626    apply auto
   2.627    apply (case_tac "k = Suc n")
   2.628    apply auto
   2.629 -  apply (metis Suc_le_eq fact_nat.cases le_Suc_eq le_eq_less_or_eq)
   2.630 +  apply (metis Suc_le_eq fact.cases le_Suc_eq le_eq_less_or_eq)
   2.631    done
   2.632  
   2.633  lemma card_UNION:
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 10 16:12:35 2015 +0000
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 16 15:30:00 2015 +0000
     3.3 @@ -905,11 +905,11 @@
     3.4        float_round_up prec (x * (ub_sin_cos_aux prec n (i + 2) (k * i * (i + 1)) x)))"
     3.5  
     3.6  lemma cos_aux:
     3.7 -  shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^(2 * i))" (is "?lb")
     3.8 -  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
     3.9 +  shows "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i))) * x ^(2 * i))" (is "?lb")
    3.10 +  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i))) * x^(2 * i)) \<le> (ub_sin_cos_aux prec n 1 1 (x * x))" (is "?ub")
    3.11  proof -
    3.12    have "0 \<le> real (x * x)" by auto
    3.13 -  let "?f n" = "fact (2 * n)"
    3.14 +  let "?f n" = "fact (2 * n) :: nat"
    3.15  
    3.16    { fix n
    3.17      have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
    3.18 @@ -935,15 +935,15 @@
    3.19    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
    3.20    have "0 < x * x" using `0 < x` by simp
    3.21  
    3.22 -  { fix x n have "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i))) * x ^ (2 * i))
    3.23 -    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
    3.24 +  { fix x n have "(\<Sum> i=0..<n. (-1::real) ^ i * (1/(fact (2 * i))) * x ^ (2 * i))
    3.25 +    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
    3.26    proof -
    3.27      have "?sum = ?sum + (\<Sum> j = 0 ..< n. 0)" by auto
    3.28      also have "\<dots> =
    3.29 -      (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / (real (fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
    3.30 -    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / (real (fact i)) * x ^ i else 0)"
    3.31 +      (\<Sum> j = 0 ..< n. (- 1) ^ ((2 * j) div 2) / ((fact (2 * j))) * x ^(2 * j)) + (\<Sum> j = 0 ..< n. 0)" by auto
    3.32 +    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then (- 1) ^ (i div 2) / ((fact i)) * x ^ i else 0)"
    3.33        unfolding sum_split_even_odd atLeast0LessThan ..
    3.34 -    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / (real (fact i)) else 0) * x ^ i)"
    3.35 +    also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then (- 1) ^ (i div 2) / ((fact i)) else 0) * x ^ i)"
    3.36        by (rule setsum.cong) auto
    3.37      finally show ?thesis by assumption
    3.38    qed } note morph_to_if_power = this
    3.39 @@ -952,8 +952,8 @@
    3.40    { fix n :: nat assume "0 < n"
    3.41      hence "0 < 2 * n" by auto
    3.42      obtain t where "0 < t" and "t < real x" and
    3.43 -      cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/(real (fact i)) else 0) * (real x) ^ i)
    3.44 -      + (cos (t + 1/2 * (2 * n) * pi) / real (fact (2*n))) * (real x)^(2*n)"
    3.45 +      cos_eq: "cos x = (\<Sum> i = 0 ..< 2 * n. (if even(i) then ((- 1) ^ (i div 2))/((fact i)) else 0) * (real x) ^ i)
    3.46 +      + (cos (t + 1/2 * (2 * n) * pi) / (fact (2*n))) * (real x)^(2*n)"
    3.47        (is "_ = ?SUM + ?rest / ?fact * ?pow")
    3.48        using Maclaurin_cos_expansion2[OF `0 < real x` `0 < 2 * n`]
    3.49        unfolding cos_coeff_def atLeast0LessThan by auto
    3.50 @@ -1020,22 +1020,22 @@
    3.51  qed
    3.52  
    3.53  lemma sin_aux: assumes "0 \<le> real x"
    3.54 -  shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
    3.55 -  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/real (fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
    3.56 +  shows "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> (\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i + 1))) * x^(2 * i + 1))" (is "?lb")
    3.57 +  and "(\<Sum> i=0..<n. (- 1) ^ i * (1/(fact (2 * i + 1))) * x^(2 * i + 1)) \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))" (is "?ub")
    3.58  proof -
    3.59    have "0 \<le> real (x * x)" by auto
    3.60 -  let "?f n" = "fact (2 * n + 1)"
    3.61 +  let "?f n" = "fact (2 * n + 1) :: nat"
    3.62  
    3.63    { fix n
    3.64      have F: "\<And>m. ((\<lambda>i. i + 2) ^^ n) m = m + 2 * n" by (induct n) auto
    3.65      have "?f (Suc n) = ?f n * ((\<lambda>i. i + 2) ^^ n) 2 * (((\<lambda>i. i + 2) ^^ n) 2 + 1)"
    3.66 -      unfolding F by auto } note f_eq = this
    3.67 -
    3.68 +      unfolding F by auto } 
    3.69 +  note f_eq = this
    3.70    from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
    3.71      OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
    3.72    show "?lb" and "?ub" using `0 \<le> real x`
    3.73      unfolding power_add power_one_right mult.assoc[symmetric] setsum_left_distrib[symmetric]
    3.74 -    unfolding mult.commute[where 'a=real]
    3.75 +    unfolding mult.commute[where 'a=real] real_fact_nat
    3.76      by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
    3.77  qed
    3.78  
    3.79 @@ -1046,14 +1046,15 @@
    3.80    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
    3.81    have "0 < x * x" using `0 < x` by simp
    3.82  
    3.83 -  { fix x n have "(\<Sum> j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
    3.84 -    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
    3.85 +  { fix x::real and n 
    3.86 +    have "(\<Sum>j = 0 ..< n. (- 1) ^ (((2 * j + 1) - Suc 0) div 2) / ((fact (2 * j + 1))) * x ^(2 * j + 1))
    3.87 +    = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * x ^ i)" (is "?SUM = _")
    3.88      proof -
    3.89        have pow: "!!i. x ^ (2 * i + 1) = x * x ^ (2 * i)" by auto
    3.90        have "?SUM = (\<Sum> j = 0 ..< n. 0) + ?SUM" by auto
    3.91 -      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i)) * x ^ i)"
    3.92 +      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / ((fact i)) * x ^ i)"
    3.93          unfolding sum_split_even_odd atLeast0LessThan ..
    3.94 -      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / (real (fact i))) * x ^ i)"
    3.95 +      also have "\<dots> = (\<Sum> i = 0 ..< 2 * n. (if even i then 0 else (- 1) ^ ((i - Suc 0) div 2) / ((fact i))) * x ^ i)"
    3.96          by (rule setsum.cong) auto
    3.97        finally show ?thesis by assumption
    3.98      qed } note setsum_morph = this
    3.99 @@ -1061,8 +1062,8 @@
   3.100    { fix n :: nat assume "0 < n"
   3.101      hence "0 < 2 * n + 1" by auto
   3.102      obtain t where "0 < t" and "t < real x" and
   3.103 -      sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)
   3.104 -      + (sin (t + 1/2 * (2 * n + 1) * pi) / real (fact (2*n + 1))) * (real x)^(2*n + 1)"
   3.105 +      sin_eq: "sin x = (\<Sum> i = 0 ..< 2 * n + 1. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)
   3.106 +      + (sin (t + 1/2 * (2 * n + 1) * pi) / (fact (2*n + 1))) * (real x)^(2*n + 1)"
   3.107        (is "_ = ?SUM + ?rest / ?fact * ?pow")
   3.108        using Maclaurin_sin_expansion3[OF `0 < 2 * n + 1` `0 < real x`]
   3.109        unfolding sin_coeff_def atLeast0LessThan by auto
   3.110 @@ -1079,7 +1080,7 @@
   3.111      {
   3.112        assume "even n"
   3.113        have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le>
   3.114 -            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
   3.115 +            (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
   3.116          using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   3.117        also have "\<dots> \<le> ?SUM" by auto
   3.118        also have "\<dots> \<le> sin x"
   3.119 @@ -1100,7 +1101,7 @@
   3.120            by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
   3.121          thus ?thesis unfolding sin_eq by auto
   3.122        qed
   3.123 -      also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/(real (fact i))) * (real x) ^ i)"
   3.124 +      also have "\<dots> \<le> (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else ((- 1) ^ ((i - Suc 0) div 2))/((fact i))) * (real x) ^ i)"
   3.125           by auto
   3.126        also have "\<dots> \<le> (x * ub_sin_cos_aux prec n 2 1 (x * x))"
   3.127          using sin_aux[OF `0 \<le> real x`] unfolding setsum_morph[symmetric] by auto
   3.128 @@ -1534,18 +1535,19 @@
   3.129  proof -
   3.130    { fix n
   3.131      have F: "\<And> m. ((\<lambda>i. i + 1) ^^ n) m = n + m" by (induct n, auto)
   3.132 -    have "fact (Suc n) = fact n * ((\<lambda>i. i + 1) ^^ n) 1" unfolding F by auto } note f_eq = this
   3.133 +    have "fact (Suc n) = fact n * ((\<lambda>i::nat. i + 1) ^^ n) 1" unfolding F by auto 
   3.134 +  } note f_eq = this
   3.135  
   3.136    note bounds = horner_bounds_nonpos[where f="fact" and lb="lb_exp_horner prec" and ub="ub_exp_horner prec" and j'=0 and s=1,
   3.137      OF assms f_eq lb_exp_horner.simps ub_exp_horner.simps]
   3.138  
   3.139 -  { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / real (fact j) * real x ^ j)"
   3.140 +  { have "lb_exp_horner prec (get_even n) 1 1 x \<le> (\<Sum>j = 0..<get_even n. 1 / (fact j) * real x ^ j)"
   3.141        using bounds(1) by auto
   3.142      also have "\<dots> \<le> exp x"
   3.143      proof -
   3.144 -      obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
   3.145 +      obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / (fact m)) + exp t / (fact (get_even n)) * (real x) ^ (get_even n)"
   3.146          using Maclaurin_exp_le unfolding atLeast0LessThan by blast
   3.147 -      moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
   3.148 +      moreover have "0 \<le> exp t / (fact (get_even n)) * (real x) ^ (get_even n)"
   3.149          by (auto simp: zero_le_even_power)
   3.150        ultimately show ?thesis using get_odd exp_gt_zero by auto
   3.151      qed
   3.152 @@ -1562,11 +1564,11 @@
   3.153        show ?thesis by (rule less_imp_le, auto simp add: power_less_zero_eq `real x < 0`)
   3.154      qed
   3.155  
   3.156 -    obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / real (fact m)) + exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n)"
   3.157 +    obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_odd n. (real x) ^ m / (fact m)) + exp t / (fact (get_odd n)) * (real x) ^ (get_odd n)"
   3.158        using Maclaurin_exp_le unfolding atLeast0LessThan by blast
   3.159 -    moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
   3.160 +    moreover have "exp t / (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
   3.161        by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero)
   3.162 -    ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
   3.163 +    ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / (fact j) * real x ^ j)"
   3.164        using get_odd exp_gt_zero by auto
   3.165      also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x"
   3.166        using bounds(2) by auto
   3.167 @@ -3229,16 +3231,9 @@
   3.168    qed
   3.169  qed
   3.170  
   3.171 -lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
   3.172 -proof (induct k)
   3.173 -  case 0
   3.174 -  show ?case by simp
   3.175 -next
   3.176 -  case (Suc k)
   3.177 -  have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
   3.178 -  hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
   3.179 -  thus ?case using Suc by auto
   3.180 -qed
   3.181 +lemma setprod_fact: "real (\<Prod> {1..<1 + k}) = fact (k :: nat)"
   3.182 +  using fact_altdef_nat Suc_eq_plus1_left atLeastLessThanSuc_atLeastAtMost real_fact_nat 
   3.183 +  by presburger
   3.184  
   3.185  lemma approx_tse:
   3.186    assumes "bounded_by xs vs"
   3.187 @@ -3258,10 +3253,11 @@
   3.188    obtain n
   3.189      where DERIV: "\<forall> m z. m < n \<and> real lx \<le> z \<and> z \<le> real ux \<longrightarrow> DERIV (F m) z :> F (Suc m) z"
   3.190      and hyp: "\<And> (t::real). t \<in> {lx .. ux} \<Longrightarrow>
   3.191 -           (\<Sum> j = 0..<n. inverse (real (fact j)) * F j c * (xs!x - c)^j) +
   3.192 -             inverse (real (fact n)) * F n t * (xs!x - c)^n
   3.193 +           (\<Sum> j = 0..<n. inverse(fact j) * F j c * (xs!x - c)^j) +
   3.194 +             inverse ((fact n)) * F n t * (xs!x - c)^n
   3.195               \<in> {l .. u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
   3.196 -    unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact by blast
   3.197 +    unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact
   3.198 +    by blast
   3.199  
   3.200    have bnd_xs: "xs ! x \<in> { lx .. ux }"
   3.201      using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
   3.202 @@ -3284,8 +3280,8 @@
   3.203        from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
   3.204        obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
   3.205          and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
   3.206 -           (\<Sum>m = 0..<Suc n'. F m c / real (fact m) * (xs ! x - c) ^ m) +
   3.207 -           F (Suc n') t / real (fact (Suc n')) * (xs ! x - c) ^ Suc n'"
   3.208 +           (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
   3.209 +           F (Suc n') t / (fact (Suc n')) * (xs ! x - c) ^ Suc n'"
   3.210          unfolding atLeast0LessThan by blast
   3.211  
   3.212        from t_bnd bnd_xs bnd_c have *: "t \<in> {lx .. ux}"
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 10 16:12:35 2015 +0000
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 16 15:30:00 2015 +0000
     4.3 @@ -8,6 +8,7 @@
     4.4  imports Complex_Main
     4.5  begin
     4.6  
     4.7 +lemmas fact_Suc = fact.simps(2)
     4.8  
     4.9  subsection {* The type of formal power series*}
    4.10  
    4.11 @@ -2866,7 +2867,7 @@
    4.12      fix n
    4.13      have "?l$n = ?r $ n"
    4.14        apply (auto simp add: E_def field_simps power_Suc[symmetric]
    4.15 -        simp del: fact_Suc of_nat_Suc power_Suc)
    4.16 +        simp del: fact.simps of_nat_Suc power_Suc)
    4.17        apply (simp add: of_nat_mult field_simps)
    4.18        done
    4.19    }
    4.20 @@ -2882,11 +2883,11 @@
    4.21      by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
    4.22    {
    4.23      fix n
    4.24 -    have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
    4.25 +    have "a$n = a$0 * c ^ n/ (fact n)"
    4.26        apply (induct n)
    4.27        apply simp
    4.28        unfolding th
    4.29 -      using fact_gt_zero_nat
    4.30 +      using fact_gt_zero
    4.31        apply (simp add: field_simps del: of_nat_Suc fact_Suc)
    4.32        apply (drule sym)
    4.33        apply (simp add: field_simps of_nat_mult)
    4.34 @@ -2985,33 +2986,6 @@
    4.35    apply (simp add: cond_value_iff cond_application_beta setsum.delta' cong del: if_weak_cong)
    4.36    done
    4.37  
    4.38 -text{* The generalized binomial theorem as a  consequence of @{thm E_add_mult} *}
    4.39 -
    4.40 -lemma gbinomial_theorem:
    4.41 -  "((a::'a::{field_char_0,field_inverse_zero})+b) ^ n =
    4.42 -    (\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
    4.43 -proof -
    4.44 -  from E_add_mult[of a b]
    4.45 -  have "(E (a + b)) $ n = (E a * E b)$n" by simp
    4.46 -  then have "(a + b) ^ n =
    4.47 -    (\<Sum>i::nat = 0::nat..n. a ^ i * b ^ (n - i)  * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
    4.48 -    by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
    4.49 -  then show ?thesis
    4.50 -    apply simp
    4.51 -    apply (rule setsum.cong)
    4.52 -    apply simp_all
    4.53 -    apply (frule binomial_fact[where ?'a = 'a, symmetric])
    4.54 -    apply (simp add: field_simps of_nat_mult)
    4.55 -    done
    4.56 -qed
    4.57 -
    4.58 -text{* And the nat-form -- also available from Binomial.thy *}
    4.59 -lemma binomial_theorem: "(a+b) ^ n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
    4.60 -  using gbinomial_theorem[of "of_nat a" "of_nat b" n]
    4.61 -  unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric]
    4.62 -    of_nat_setsum[symmetric]
    4.63 -  by simp
    4.64 -
    4.65  
    4.66  subsubsection{* Logarithmic series *}
    4.67  
    4.68 @@ -3290,7 +3264,7 @@
    4.69            unfolding m1nk
    4.70            unfolding m h pochhammer_Suc_setprod
    4.71            apply (simp add: field_simps del: fact_Suc)
    4.72 -          unfolding fact_altdef_nat id_def
    4.73 +          unfolding fact_altdef id_def
    4.74            unfolding of_nat_setprod
    4.75            unfolding setprod.distrib[symmetric]
    4.76            apply auto
    4.77 @@ -3823,7 +3797,7 @@
    4.78          THEN spec, of "\<lambda>x. x < e"]
    4.79        have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially"
    4.80          apply safe
    4.81 -        apply (auto simp: eventually_nhds)
    4.82 +        apply (auto simp: eventually_nhds) --{*slow*}
    4.83          done
    4.84        then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially)
    4.85        have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially)
     5.1 --- a/src/HOL/Library/Permutations.thy	Tue Mar 10 16:12:35 2015 +0000
     5.2 +++ b/src/HOL/Library/Permutations.thy	Mon Mar 16 15:30:00 2015 +0000
     5.3 @@ -190,7 +190,7 @@
     5.4      from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
     5.5        using `finite F` by auto
     5.6      then have "finite ?pF"
     5.7 -      using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
     5.8 +      by (auto intro: card_ge_0_finite)
     5.9      then have pF'f: "finite ?pF'"
    5.10        using H0 `finite F`
    5.11        apply (simp only: Collect_split Collect_mem_eq)
    5.12 @@ -258,7 +258,7 @@
    5.13  lemma finite_permutations:
    5.14    assumes fS: "finite S"
    5.15    shows "finite {p. p permutes S}"
    5.16 -  using card_permutations[OF refl fS] fact_gt_zero_nat
    5.17 +  using card_permutations[OF refl fS] 
    5.18    by (auto intro: card_ge_0_finite)
    5.19  
    5.20  
    5.21 @@ -280,26 +280,6 @@
    5.22      by simp
    5.23  qed
    5.24  
    5.25 -lemma setsum_permute:
    5.26 -  assumes "p permutes S"
    5.27 -  shows "setsum f S = setsum (f \<circ> p) S"
    5.28 -  using assms by (fact setsum.permute)
    5.29 -
    5.30 -lemma setsum_permute_natseg:
    5.31 -  assumes pS: "p permutes {m .. n}"
    5.32 -  shows "setsum f {m .. n} = setsum (f \<circ> p) {m .. n}"
    5.33 -  using setsum_permute [OF pS, of f ] pS by blast
    5.34 -
    5.35 -lemma setprod_permute:
    5.36 -  assumes "p permutes S"
    5.37 -  shows "setprod f S = setprod (f \<circ> p) S"
    5.38 -  using assms by (fact setprod.permute)
    5.39 -
    5.40 -lemma setprod_permute_natseg:
    5.41 -  assumes pS: "p permutes {m .. n}"
    5.42 -  shows "setprod f {m .. n} = setprod (f \<circ> p) {m .. n}"
    5.43 -  using setprod_permute [OF pS, of f ] pS by blast
    5.44 -
    5.45  
    5.46  subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *}
    5.47  
     6.1 --- a/src/HOL/MacLaurin.thy	Tue Mar 10 16:12:35 2015 +0000
     6.2 +++ b/src/HOL/MacLaurin.thy	Mon Mar 16 15:30:00 2015 +0000
     6.3 @@ -17,47 +17,52 @@
     6.4  
     6.5  lemma Maclaurin_lemma:
     6.6      "0 < h ==>
     6.7 -     \<exists>B. f h = (\<Sum>m<n. (j m / real (fact m)) * (h^m)) +
     6.8 -               (B * ((h^n) / real(fact n)))"
     6.9 -by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / real (fact m)) * h^m)) * real(fact n) / (h^n)"]) simp
    6.10 +     \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) +
    6.11 +               (B * ((h^n) /(fact n)))"
    6.12 +by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
    6.13  
    6.14  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
    6.15  by arith
    6.16  
    6.17  lemma fact_diff_Suc [rule_format]:
    6.18    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    6.19 -  by (subst fact_reduce_nat, auto)
    6.20 +  by (subst fact_reduce, auto)
    6.21  
    6.22  lemma Maclaurin_lemma2:
    6.23    fixes B
    6.24    assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    6.25 -    and INIT : "n = Suc k"
    6.26 -  defines "difg \<equiv> (\<lambda>m t. diff m t - ((\<Sum>p<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
    6.27 -    B * (t ^ (n - m) / real (fact (n - m)))))" (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
    6.28 +      and INIT : "n = Suc k"
    6.29 +  defines "difg \<equiv> 
    6.30 +      (\<lambda>m t::real. diff m t - 
    6.31 +         ((\<Sum>p<n - m. diff (m + p) 0 / (fact p) * t ^ p) + B * (t ^ (n - m) / (fact (n - m)))))" 
    6.32 +        (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
    6.33    shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
    6.34  proof (rule allI impI)+
    6.35 -  fix m t assume INIT2: "m < n & 0 \<le> t & t \<le> h"
    6.36 +  fix m and t::real
    6.37 +  assume INIT2: "m < n & 0 \<le> t & t \<le> h"
    6.38    have "DERIV (difg m) t :> diff (Suc m) t -
    6.39 -    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) +
    6.40 -     real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)))" unfolding difg_def
    6.41 +    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) +
    6.42 +     real (n - m) * t ^ (n - Suc m) * B / (fact (n - m)))" 
    6.43 +    unfolding difg_def
    6.44      by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2]
    6.45               simp: real_of_nat_def[symmetric])
    6.46    moreover
    6.47    from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
    6.48      unfolding atLeast0LessThan[symmetric] by auto
    6.49 -  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / real (fact x)) =
    6.50 -      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)))"
    6.51 +  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
    6.52 +      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
    6.53      unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
    6.54    moreover
    6.55 -  have fact_neq_0: "\<And>x::nat. real (fact x) + real x * real (fact x) \<noteq> 0"
    6.56 -    by (metis fact_gt_zero_nat not_add_less1 real_of_nat_add real_of_nat_mult real_of_nat_zero_iff)
    6.57 -  have "\<And>x. real (Suc x) * t ^ x * diff (Suc m + x) 0 / real (fact (Suc x)) =
    6.58 -      diff (Suc m + x) 0 * t^x / real (fact x)"
    6.59 -    by (auto simp: field_simps real_of_nat_Suc fact_neq_0 intro!: nonzero_divide_eq_eq[THEN iffD2])
    6.60 +  have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
    6.61 +    by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff not_real_of_nat_less_zero)
    6.62 +  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)) =
    6.63 +            diff (Suc m + x) 0 * t^x / (fact x)"
    6.64 +    by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
    6.65    moreover
    6.66 -  have "real (n - m) * t ^ (n - Suc m) * B / real (fact (n - m)) =
    6.67 -      B * (t ^ (n - Suc m) / real (fact (n - Suc m)))"
    6.68 -    using `0 < n - m` by (simp add: fact_reduce_nat)
    6.69 +  have "(n - m) * t ^ (n - Suc m) * B / (fact (n - m)) =
    6.70 +        B * (t ^ (n - Suc m) / (fact (n - Suc m)))"
    6.71 +    using `0 < n - m`
    6.72 +    by (simp add: divide_simps fact_reduce)
    6.73    ultimately show "DERIV (difg m) t :> difg (Suc m) t"
    6.74      unfolding difg_def by simp
    6.75  qed
    6.76 @@ -69,29 +74,27 @@
    6.77    assumes diff_Suc:
    6.78      "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
    6.79    shows
    6.80 -    "\<exists>t. 0 < t & t < h &
    6.81 +    "\<exists>t::real. 0 < t & t < h &
    6.82                f h =
    6.83 -              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {..<n} +
    6.84 -              (diff n t / real (fact n)) * h ^ n"
    6.85 +              setsum (%m. (diff m 0 / (fact m)) * h ^ m) {..<n} +
    6.86 +              (diff n t / (fact n)) * h ^ n"
    6.87  proof -
    6.88    from n obtain m where m: "n = Suc m"
    6.89      by (cases n) (simp add: n)
    6.90  
    6.91    obtain B where f_h: "f h =
    6.92 -        (\<Sum>m<n. diff m (0\<Colon>real) / real (fact m) * h ^ m) +
    6.93 -        B * (h ^ n / real (fact n))"
    6.94 +        (\<Sum>m<n. diff m (0\<Colon>real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))"
    6.95      using Maclaurin_lemma [OF h] ..
    6.96  
    6.97    def g \<equiv> "(\<lambda>t. f t -
    6.98 -    (setsum (\<lambda>m. (diff m 0 / real(fact m)) * t^m) {..<n}
    6.99 -      + (B * (t^n / real(fact n)))))"
   6.100 +    (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n)))))"
   6.101  
   6.102    have g2: "g 0 = 0 & g h = 0"
   6.103      by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
   6.104  
   6.105    def difg \<equiv> "(%m t. diff m t -
   6.106 -    (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {..<n-m}
   6.107 -      + (B * ((t ^ (n - m)) / real (fact (n - m))))))"
   6.108 +    (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
   6.109 +      + (B * ((t ^ (n - m)) / (fact (n - m))))))"
   6.110  
   6.111    have difg_0: "difg 0 = g"
   6.112      unfolding difg_def g_def by (simp add: diff_0)
   6.113 @@ -146,7 +149,6 @@
   6.114      thus ?case
   6.115        using `t < h` by auto
   6.116    qed
   6.117 -
   6.118    then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
   6.119  
   6.120    hence "difg (Suc m) t = 0"
   6.121 @@ -156,30 +158,28 @@
   6.122    proof (intro exI conjI)
   6.123      show "0 < t" by fact
   6.124      show "t < h" by fact
   6.125 -    show "f h =
   6.126 -      (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.127 -      diff n t / real (fact n) * h ^ n"
   6.128 +    show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
   6.129        using `difg (Suc m) t = 0`
   6.130 -      by (simp add: m f_h difg_def del: fact_Suc)
   6.131 +      by (simp add: m f_h difg_def)
   6.132    qed
   6.133  qed
   6.134  
   6.135  lemma Maclaurin_objl:
   6.136    "0 < h & n>0 & diff 0 = f &
   6.137    (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   6.138 -   --> (\<exists>t. 0 < t & t < h &
   6.139 -            f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.140 -                  diff n t / real (fact n) * h ^ n)"
   6.141 +   --> (\<exists>t::real. 0 < t & t < h &
   6.142 +            f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
   6.143 +                  diff n t / (fact n) * h ^ n)"
   6.144  by (blast intro: Maclaurin)
   6.145  
   6.146  
   6.147  lemma Maclaurin2:
   6.148    assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
   6.149 -  and DERIV: "\<forall>m t.
   6.150 +  and DERIV: "\<forall>m t::real.
   6.151    m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
   6.152    shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
   6.153 -  (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.154 -  diff n t / real (fact n) * h ^ n"
   6.155 +  (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
   6.156 +  diff n t / (fact n) * h ^ n"
   6.157  proof (cases "n")
   6.158    case 0 with INIT1 INIT2 show ?thesis by fastforce
   6.159  next
   6.160 @@ -187,28 +187,28 @@
   6.161    hence "n > 0" by simp
   6.162    from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
   6.163      f h =
   6.164 -    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n"
   6.165 +    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
   6.166      by (rule Maclaurin)
   6.167    thus ?thesis by fastforce
   6.168  qed
   6.169  
   6.170  lemma Maclaurin2_objl:
   6.171       "0 < h & diff 0 = f &
   6.172 -       (\<forall>m t.
   6.173 -          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   6.174 -    --> (\<exists>t. 0 < t &
   6.175 +       (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
   6.176 +    --> (\<exists>t::real. 0 < t &
   6.177                t \<le> h &
   6.178                f h =
   6.179 -              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.180 -              diff n t / real (fact n) * h ^ n)"
   6.181 +              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
   6.182 +              diff n t / (fact n) * h ^ n)"
   6.183  by (blast intro: Maclaurin2)
   6.184  
   6.185  lemma Maclaurin_minus:
   6.186 +  fixes h::real
   6.187    assumes "h < 0" "0 < n" "diff 0 = f"
   6.188    and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
   6.189    shows "\<exists>t. h < t & t < 0 &
   6.190 -         f h = (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.191 -         diff n t / real (fact n) * h ^ n"
   6.192 +         f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
   6.193 +         diff n t / (fact n) * h ^ n"
   6.194  proof -
   6.195    txt "Transform @{text ABL'} into @{text derivative_intros} format."
   6.196    note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
   6.197 @@ -216,33 +216,35 @@
   6.198    have "\<exists>t>0. t < - h \<and>
   6.199      f (- (- h)) =
   6.200      (\<Sum>m<n.
   6.201 -    (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
   6.202 -    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n"
   6.203 +    (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
   6.204 +    (- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
   6.205      by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
   6.206    then guess t ..
   6.207    moreover
   6.208 -  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
   6.209 +  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
   6.210      by (auto simp add: power_mult_distrib[symmetric])
   6.211    moreover
   6.212 -  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m<n. diff m 0 * h ^ m / real (fact m))"
   6.213 +  have "(SUM m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (SUM m<n. diff m 0 * h ^ m / (fact m))"
   6.214      by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
   6.215    ultimately have " h < - t \<and>
   6.216      - t < 0 \<and>
   6.217      f h =
   6.218 -    (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
   6.219 +    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
   6.220      by auto
   6.221    thus ?thesis ..
   6.222  qed
   6.223  
   6.224  lemma Maclaurin_minus_objl:
   6.225 +  fixes h::real
   6.226 +  shows
   6.227       "(h < 0 & n > 0 & diff 0 = f &
   6.228         (\<forall>m t.
   6.229            m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
   6.230      --> (\<exists>t. h < t &
   6.231                t < 0 &
   6.232                f h =
   6.233 -              (\<Sum>m<n. diff m 0 / real (fact m) * h ^ m) +
   6.234 -              diff n t / real (fact n) * h ^ n)"
   6.235 +              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
   6.236 +              diff n t / (fact n) * h ^ n)"
   6.237  by (blast intro: Maclaurin_minus)
   6.238  
   6.239  
   6.240 @@ -250,20 +252,19 @@
   6.241  
   6.242  (* not good for PVS sin_approx, cos_approx *)
   6.243  
   6.244 -lemma Maclaurin_bi_le_lemma [rule_format]:
   6.245 -  "n>0 \<longrightarrow>
   6.246 +lemma Maclaurin_bi_le_lemma:
   6.247 +  "n>0 \<Longrightarrow>
   6.248     diff 0 0 =
   6.249 -   (\<Sum>m<n. diff m 0 * 0 ^ m / real (fact m)) +
   6.250 -   diff n 0 * 0 ^ n / real (fact n)"
   6.251 +   (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
   6.252  by (induct "n") auto
   6.253  
   6.254  lemma Maclaurin_bi_le:
   6.255     assumes "diff 0 = f"
   6.256 -   and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
   6.257 +   and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
   6.258     shows "\<exists>t. abs t \<le> abs x &
   6.259                f x =
   6.260 -              (\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) +
   6.261 -     diff n t / real (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   6.262 +              (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
   6.263 +     diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   6.264  proof cases
   6.265    assume "n = 0" with `diff 0 = f` show ?thesis by force
   6.266  next
   6.267 @@ -291,11 +292,12 @@
   6.268  qed
   6.269  
   6.270  lemma Maclaurin_all_lt:
   6.271 +  fixes x::real
   6.272    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
   6.273    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
   6.274    shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
   6.275 -    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   6.276 -                (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
   6.277 +    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
   6.278 +                (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
   6.279  proof (cases rule: linorder_cases)
   6.280    assume "x = 0" with INIT3 show "?thesis"..
   6.281  next
   6.282 @@ -314,28 +316,30 @@
   6.283  
   6.284  
   6.285  lemma Maclaurin_all_lt_objl:
   6.286 +  fixes x::real
   6.287 +  shows
   6.288       "diff 0 = f &
   6.289        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
   6.290        x ~= 0 & n > 0
   6.291        --> (\<exists>t. 0 < abs t & abs t < abs x &
   6.292 -               f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   6.293 -                     (diff n t / real (fact n)) * x ^ n)"
   6.294 +               f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
   6.295 +                     (diff n t / (fact n)) * x ^ n)"
   6.296  by (blast intro: Maclaurin_all_lt)
   6.297  
   6.298  lemma Maclaurin_zero [rule_format]:
   6.299       "x = (0::real)
   6.300        ==> n \<noteq> 0 -->
   6.301 -          (\<Sum>m<n. (diff m (0::real) / real (fact m)) * x ^ m) =
   6.302 +          (\<Sum>m<n. (diff m (0::real) / (fact m)) * x ^ m) =
   6.303            diff 0 0"
   6.304  by (induct n, auto)
   6.305  
   6.306  
   6.307  lemma Maclaurin_all_le:
   6.308    assumes INIT: "diff 0 = f"
   6.309 -  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
   6.310 +  and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
   6.311    shows "\<exists>t. abs t \<le> abs x & f x =
   6.312 -    (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   6.313 -    (diff n t / real (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   6.314 +    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
   6.315 +    (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
   6.316  proof cases
   6.317    assume "n = 0" with INIT show ?thesis by force
   6.318    next
   6.319 @@ -343,7 +347,7 @@
   6.320    show ?thesis
   6.321    proof cases
   6.322      assume "x = 0"
   6.323 -    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0"
   6.324 +    with `n \<noteq> 0` have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
   6.325        by (intro Maclaurin_zero) auto
   6.326      with INIT `x = 0` `n \<noteq> 0` have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
   6.327      thus ?thesis ..
   6.328 @@ -357,28 +361,32 @@
   6.329    qed
   6.330  qed
   6.331  
   6.332 -lemma Maclaurin_all_le_objl: "diff 0 = f &
   6.333 +lemma Maclaurin_all_le_objl:
   6.334 +  "diff 0 = f &
   6.335        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
   6.336 -      --> (\<exists>t. abs t \<le> abs x &
   6.337 -              f x = (\<Sum>m<n. (diff m 0 / real (fact m)) * x ^ m) +
   6.338 -                    (diff n t / real (fact n)) * x ^ n)"
   6.339 +      --> (\<exists>t::real. abs t \<le> abs x &
   6.340 +              f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
   6.341 +                    (diff n t / (fact n)) * x ^ n)"
   6.342  by (blast intro: Maclaurin_all_le)
   6.343  
   6.344  
   6.345  subsection{*Version for Exponential Function*}
   6.346  
   6.347 -lemma Maclaurin_exp_lt: "[| x ~= 0; n > 0 |]
   6.348 +lemma Maclaurin_exp_lt:
   6.349 +  fixes x::real
   6.350 +  shows
   6.351 +  "[| x ~= 0; n > 0 |]
   6.352        ==> (\<exists>t. 0 < abs t &
   6.353                  abs t < abs x &
   6.354 -                exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
   6.355 -                        (exp t / real (fact n)) * x ^ n)"
   6.356 +                exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
   6.357 +                        (exp t / (fact n)) * x ^ n)"
   6.358  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
   6.359  
   6.360  
   6.361  lemma Maclaurin_exp_le:
   6.362 -     "\<exists>t. abs t \<le> abs x &
   6.363 -            exp x = (\<Sum>m<n. (x ^ m) / real (fact m)) +
   6.364 -                       (exp t / real (fact n)) * x ^ n"
   6.365 +     "\<exists>t::real. abs t \<le> abs x &
   6.366 +            exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
   6.367 +                       (exp t / (fact n)) * x ^ n"
   6.368  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
   6.369  
   6.370  
   6.371 @@ -412,7 +420,7 @@
   6.372       "\<exists>t. abs t \<le> abs x &
   6.373         sin x =
   6.374         (\<Sum>m<n. sin_coeff m * x ^ m)
   6.375 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.376 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.377  apply (cut_tac f = sin and n = n and x = x
   6.378          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
   6.379  apply safe
   6.380 @@ -431,7 +439,7 @@
   6.381  lemma Maclaurin_sin_expansion:
   6.382       "\<exists>t. sin x =
   6.383         (\<Sum>m<n. sin_coeff m * x ^ m)
   6.384 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.385 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.386  apply (insert Maclaurin_sin_expansion2 [of x n])
   6.387  apply (blast intro: elim:)
   6.388  done
   6.389 @@ -441,7 +449,7 @@
   6.390         \<exists>t. 0 < t & t < x &
   6.391         sin x =
   6.392         (\<Sum>m<n. sin_coeff m * x ^ m)
   6.393 -      + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
   6.394 +      + ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
   6.395  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
   6.396  apply safe
   6.397  apply simp
   6.398 @@ -458,7 +466,7 @@
   6.399         \<exists>t. 0 < t & t \<le> x &
   6.400         sin x =
   6.401         (\<Sum>m<n. sin_coeff m * x ^ m)
   6.402 -      + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.403 +      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.404  apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
   6.405  apply safe
   6.406  apply simp
   6.407 @@ -482,10 +490,10 @@
   6.408  by (simp only: cos_add sin_add real_of_nat_Suc distrib_right add_divide_distrib, auto)
   6.409  
   6.410  lemma Maclaurin_cos_expansion:
   6.411 -     "\<exists>t. abs t \<le> abs x &
   6.412 +     "\<exists>t::real. abs t \<le> abs x &
   6.413         cos x =
   6.414         (\<Sum>m<n. cos_coeff m * x ^ m)
   6.415 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.416 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.417  apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
   6.418  apply safe
   6.419  apply (simp (no_asm))
   6.420 @@ -505,7 +513,7 @@
   6.421         \<exists>t. 0 < t & t < x &
   6.422         cos x =
   6.423         (\<Sum>m<n. cos_coeff m * x ^ m)
   6.424 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.425 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.426  apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
   6.427  apply safe
   6.428  apply simp
   6.429 @@ -521,7 +529,7 @@
   6.430         \<exists>t. x < t & t < 0 &
   6.431         cos x =
   6.432         (\<Sum>m<n. cos_coeff m * x ^ m)
   6.433 -      + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
   6.434 +      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
   6.435  apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
   6.436  apply safe
   6.437  apply simp
   6.438 @@ -542,7 +550,7 @@
   6.439  
   6.440  lemma Maclaurin_sin_bound:
   6.441    "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
   6.442 -  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
   6.443 +  \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
   6.444  proof -
   6.445    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   6.446      by (rule_tac mult_right_mono,simp_all)
   6.447 @@ -557,8 +565,8 @@
   6.448      done
   6.449    from Maclaurin_all_le [OF diff_0 DERIV_diff]
   6.450    obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
   6.451 -    t2: "sin x = (\<Sum>m<n. ?diff m 0 / real (fact m) * x ^ m) +
   6.452 -      ?diff n t / real (fact n) * x ^ n" by fast
   6.453 +    t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) +
   6.454 +      ?diff n t / (fact n) * x ^ n" by fast
   6.455    have diff_m_0:
   6.456      "\<And>m. ?diff m 0 = (if even m then 0
   6.457           else (- 1) ^ ((m - Suc 0) div 2))"
     7.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Mar 10 16:12:35 2015 +0000
     7.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Mar 16 15:30:00 2015 +0000
     7.3 @@ -8,6 +8,10 @@
     7.4  imports  "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
     7.5  begin
     7.6  
     7.7 +
     7.8 +lemma cmod_fact [simp]: "cmod (fact n) = fact n"
     7.9 +  by (metis norm_of_nat of_nat_fact)
    7.10 +
    7.11  subsection{*General lemmas*}
    7.12  
    7.13  lemma has_derivative_mult_right:
    7.14 @@ -26,7 +30,7 @@
    7.15  
    7.16  lemma fact_cancel:
    7.17    fixes c :: "'a::real_field"
    7.18 -  shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
    7.19 +  shows "of_nat (Suc n) * c / (fact (Suc n)) = c / (fact n)"
    7.20    by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
    7.21  
    7.22  lemma linear_times:
    7.23 @@ -985,7 +989,7 @@
    7.24        and B: "\<And>x. x \<in> s \<Longrightarrow> cmod (f (Suc n) x) \<le> B"
    7.25        and w: "w \<in> s"
    7.26        and z: "z \<in> s"
    7.27 -    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / of_nat (fact i)))
    7.28 +    shows "cmod(f 0 z - (\<Sum>i\<le>n. f i w * (z-w) ^ i / (fact i)))
    7.29            \<le> B * cmod(z - w)^(Suc n) / fact n"
    7.30  proof -
    7.31    have wzs: "closed_segment w z \<subseteq> s" using assms
    7.32 @@ -994,48 +998,46 @@
    7.33      assume "u \<in> closed_segment w z"
    7.34      then have "u \<in> s"
    7.35        by (metis wzs subsetD)
    7.36 -    have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / of_nat (fact i) +
    7.37 -                      f (Suc i) u * (z-u)^i / of_nat (fact i)) = 
    7.38 -              f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
    7.39 +    have "(\<Sum>i\<le>n. f i u * (- of_nat i * (z-u)^(i - 1)) / (fact i) +
    7.40 +                      f (Suc i) u * (z-u)^i / (fact i)) = 
    7.41 +              f (Suc n) u * (z-u) ^ n / (fact n)"
    7.42      proof (induction n)
    7.43        case 0 show ?case by simp
    7.44      next
    7.45        case (Suc n)
    7.46 -      have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / of_nat (fact i) +
    7.47 -                             f (Suc i) u * (z-u) ^ i / of_nat (fact i)) =  
    7.48 -           f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
    7.49 -           f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
    7.50 -           f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
    7.51 +      have "(\<Sum>i\<le>Suc n. f i u * (- of_nat i * (z-u) ^ (i - 1)) / (fact i) +
    7.52 +                             f (Suc i) u * (z-u) ^ i / (fact i)) =  
    7.53 +           f (Suc n) u * (z-u) ^ n / (fact n) +
    7.54 +           f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / (fact (Suc n)) -
    7.55 +           f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / (fact (Suc n))"
    7.56          using Suc by simp
    7.57 -      also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
    7.58 +      also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n))"
    7.59        proof -
    7.60 -        have "of_nat(fact(Suc n)) *
    7.61 -             (f(Suc n) u *(z-u) ^ n / of_nat(fact n) +
    7.62 -               f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / of_nat(fact(Suc n)) -
    7.63 -               f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / of_nat(fact(Suc n))) =
    7.64 -            (of_nat(fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / of_nat(fact n) +
    7.65 -            (of_nat(fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / of_nat(fact(Suc n))) -
    7.66 -            (of_nat(fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / of_nat(fact(Suc n))"
    7.67 -          by (simp add: algebra_simps del: fact_Suc)
    7.68 -        also have "... =
    7.69 -                   (of_nat (fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / of_nat (fact n) +
    7.70 -                   (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    7.71 -                   (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    7.72 -          by (simp del: fact_Suc)
    7.73 -        also have "... = 
    7.74 -                   (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
    7.75 -                   (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    7.76 -                   (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    7.77 -          by (simp only: fact_Suc of_nat_mult ac_simps) simp
    7.78 +        have "(fact(Suc n)) *
    7.79 +             (f(Suc n) u *(z-u) ^ n / (fact n) +
    7.80 +               f(Suc(Suc n)) u *((z-u) *(z-u) ^ n) / (fact(Suc n)) -
    7.81 +               f(Suc n) u *((1 + of_nat n) *(z-u) ^ n) / (fact(Suc n))) =
    7.82 +            ((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
    7.83 +            ((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
    7.84 +            ((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
    7.85 +          by (simp add: algebra_simps del: fact.simps)
    7.86 +        also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
    7.87 +                         (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    7.88 +                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    7.89 +          by (simp del: fact.simps)
    7.90 +        also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
    7.91 +                         (f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
    7.92 +                         (f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
    7.93 +          by (simp only: fact.simps of_nat_mult ac_simps) simp
    7.94          also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
    7.95            by (simp add: algebra_simps)
    7.96          finally show ?thesis
    7.97 -        by (simp add: mult_left_cancel [where c = "of_nat (fact (Suc n))", THEN iffD1] del: fact_Suc)
    7.98 +        by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
    7.99        qed
   7.100        finally show ?case .
   7.101      qed
   7.102 -    then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / of_nat (fact i))) 
   7.103 -                has_field_derivative f (Suc n) u * (z-u) ^ n / of_nat (fact n))
   7.104 +    then have "((\<lambda>v. (\<Sum>i\<le>n. f i v * (z - v)^i / (fact i))) 
   7.105 +                has_field_derivative f (Suc n) u * (z-u) ^ n / (fact n))
   7.106                 (at u within s)"
   7.107        apply (intro derivative_eq_intros)
   7.108        apply (blast intro: assms `u \<in> s`)
   7.109 @@ -1055,22 +1057,22 @@
   7.110        by (metis norm_ge_zero zero_le_power mult_right_mono  B [OF us])
   7.111      finally have "cmod (f (Suc n) u) * cmod (z - u) ^ n \<le> B * cmod (z - w) ^ n" .
   7.112    } note cmod_bound = this
   7.113 -  have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (fact i)) = (\<Sum>i\<le>n. (f i z / of_nat (fact i)) * 0 ^ i)"
   7.114 +  have "(\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)) = (\<Sum>i\<le>n. (f i z / (fact i)) * 0 ^ i)"
   7.115      by simp
   7.116 -  also have "\<dots> = f 0 z / of_nat (fact 0)"
   7.117 +  also have "\<dots> = f 0 z / (fact 0)"
   7.118      by (subst setsum_zero_power) simp
   7.119 -  finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / of_nat (fact i))) 
   7.120 -            \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / of_nat (fact i)) -
   7.121 -                    (\<Sum>i\<le>n. f i z * (z - z) ^ i / of_nat (fact i)))"
   7.122 +  finally have "cmod (f 0 z - (\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i))) 
   7.123 +                \<le> cmod ((\<Sum>i\<le>n. f i w * (z - w) ^ i / (fact i)) -
   7.124 +                        (\<Sum>i\<le>n. f i z * (z - z) ^ i / (fact i)))"
   7.125      by (simp add: norm_minus_commute)
   7.126 -  also have "... \<le> B * cmod (z - w) ^ n / real_of_nat (fact n) * cmod (w - z)"
   7.127 +  also have "... \<le> B * cmod (z - w) ^ n / (fact n) * cmod (w - z)"
   7.128      apply (rule complex_differentiable_bound 
   7.129 -      [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / of_nat(fact n)"
   7.130 +      [where f' = "\<lambda>w. f (Suc n) w * (z - w)^n / (fact n)"
   7.131           and s = "closed_segment w z", OF convex_segment])
   7.132      apply (auto simp: ends_in_segment real_of_nat_def DERIV_subset [OF sum_deriv wzs]
   7.133                    norm_divide norm_mult norm_power divide_le_cancel cmod_bound)
   7.134      done
   7.135 -  also have "...  \<le> B * cmod (z - w) ^ Suc n / real (fact n)"
   7.136 +  also have "...  \<le> B * cmod (z - w) ^ Suc n / (fact n)"
   7.137      by (simp add: algebra_simps norm_minus_commute real_of_nat_def)
   7.138    finally show ?thesis .
   7.139  qed
   7.140 @@ -1102,40 +1104,40 @@
   7.141    assumes "\<And>i x. \<lbrakk>x \<in> closed_segment w z; i \<le> n\<rbrakk> \<Longrightarrow> ((f i) has_field_derivative f (Suc i) x) (at x)"
   7.142      shows "\<exists>u. u \<in> closed_segment w z \<and>
   7.143              Re (f 0 z) =
   7.144 -            Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / of_nat (fact i)) +
   7.145 -                (f (Suc n) u * (z-u)^n / of_nat (fact n)) * (z - w))"
   7.146 +            Re ((\<Sum>i = 0..n. f i w * (z - w) ^ i / (fact i)) +
   7.147 +                (f (Suc n) u * (z-u)^n / (fact n)) * (z - w))"
   7.148  proof -
   7.149    { fix u
   7.150      assume u: "u \<in> closed_segment w z"
   7.151      have "(\<Sum>i = 0..n.
   7.152                 (f (Suc i) u * (z-u) ^ i - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) /
   7.153 -               of_nat (fact i)) =
   7.154 +               (fact i)) =
   7.155            f (Suc 0) u -
   7.156               (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
   7.157 -             of_nat (fact (Suc n)) +
   7.158 +             (fact (Suc n)) +
   7.159               (\<Sum>i = 0..n.
   7.160                   (f (Suc (Suc i)) u * ((z-u) ^ Suc i) - of_nat (Suc i) * (f (Suc i) u * (z-u) ^ i)) /
   7.161 -                 of_nat (fact (Suc i)))"
   7.162 +                 (fact (Suc i)))"
   7.163         by (subst setsum_Suc_reindex) simp
   7.164      also have "... = f (Suc 0) u -
   7.165               (f (Suc (Suc n)) u * ((z-u) ^ Suc n) - (of_nat (Suc n)) * (z-u) ^ n * f (Suc n) u) /
   7.166 -             of_nat (fact (Suc n)) +
   7.167 +             (fact (Suc n)) +
   7.168               (\<Sum>i = 0..n.
   7.169 -                 f (Suc (Suc i)) u * ((z-u) ^ Suc i) / of_nat (fact (Suc i))  - 
   7.170 -                 f (Suc i) u * (z-u) ^ i / of_nat (fact i))"
   7.171 +                 f (Suc (Suc i)) u * ((z-u) ^ Suc i) / (fact (Suc i))  - 
   7.172 +                 f (Suc i) u * (z-u) ^ i / (fact i))"
   7.173        by (simp only: diff_divide_distrib fact_cancel ac_simps)
   7.174      also have "... = f (Suc 0) u -
   7.175               (f (Suc (Suc n)) u * (z-u) ^ Suc n - of_nat (Suc n) * (z-u) ^ n * f (Suc n) u) /
   7.176 -             of_nat (fact (Suc n)) +
   7.177 -             f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n)) - f (Suc 0) u"
   7.178 +             (fact (Suc n)) +
   7.179 +             f (Suc (Suc n)) u * (z-u) ^ Suc n / (fact (Suc n)) - f (Suc 0) u"
   7.180        by (subst setsum_Suc_diff) auto
   7.181 -    also have "... = f (Suc n) u * (z-u) ^ n / of_nat (fact n)"
   7.182 +    also have "... = f (Suc n) u * (z-u) ^ n / (fact n)"
   7.183        by (simp only: algebra_simps diff_divide_distrib fact_cancel)
   7.184      finally have "(\<Sum>i = 0..n. (f (Suc i) u * (z - u) ^ i 
   7.185 -                             - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / of_nat (fact i)) =
   7.186 -                  f (Suc n) u * (z - u) ^ n / of_nat (fact n)" .
   7.187 -    then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / of_nat (fact i)) has_field_derivative
   7.188 -                f (Suc n) u * (z - u) ^ n / of_nat (fact n))  (at u)"
   7.189 +                             - of_nat i * (f i u * (z-u) ^ (i - Suc 0))) / (fact i)) =
   7.190 +                  f (Suc n) u * (z - u) ^ n / (fact n)" .
   7.191 +    then have "((\<lambda>u. \<Sum>i = 0..n. f i u * (z - u) ^ i / (fact i)) has_field_derivative
   7.192 +                f (Suc n) u * (z - u) ^ n / (fact n))  (at u)"
   7.193        apply (intro derivative_eq_intros)+
   7.194        apply (force intro: u assms)
   7.195        apply (rule refl)+
   7.196 @@ -1143,8 +1145,8 @@
   7.197        done
   7.198    }
   7.199    then show ?thesis
   7.200 -    apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / of_nat (fact i)"
   7.201 -               "\<lambda>u. (f (Suc n) u * (z-u)^n / of_nat (fact n))"])
   7.202 +    apply (cut_tac complex_mvt_line [of w z "\<lambda>u. \<Sum>i = 0..n. f i u * (z-u) ^ i / (fact i)"
   7.203 +               "\<lambda>u. (f (Suc n) u * (z-u)^n / (fact n))"])
   7.204      apply (auto simp add: intro: open_closed_segment)
   7.205      done
   7.206  qed
     8.1 --- a/src/HOL/NSA/HTranscendental.thy	Tue Mar 10 16:12:35 2015 +0000
     8.2 +++ b/src/HOL/NSA/HTranscendental.thy	Mon Mar 16 15:30:00 2015 +0000
     8.3 @@ -14,7 +14,7 @@
     8.4  definition
     8.5    exphr :: "real => hypreal" where
     8.6      --{*define exponential function using standard part *}
     8.7 -  "exphr x =  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
     8.8 +  "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
     8.9  
    8.10  definition
    8.11    sinhr :: "real => hypreal" where
    8.12 @@ -213,7 +213,7 @@
    8.13  done
    8.14  
    8.15  lemma HFinite_exp [simp]:
    8.16 -     "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
    8.17 +     "sumhr (0, whn, %n. inverse (fact n) * x ^ n) \<in> HFinite"
    8.18  unfolding sumhr_app
    8.19  apply (simp only: star_zero_def starfun2_star_of atLeast0LessThan)
    8.20  apply (rule NSBseqD2)
     9.1 --- a/src/HOL/NSA/NSComplex.thy	Tue Mar 10 16:12:35 2015 +0000
     9.2 +++ b/src/HOL/NSA/NSComplex.thy	Mon Mar 16 15:30:00 2015 +0000
     9.3 @@ -654,5 +654,4 @@
     9.4        "hIm(numeral v :: hcomplex) = 0"
     9.5  by transfer (rule complex_Im_numeral)
     9.6  
     9.7 -(* TODO: add neg_numeral rules above *)
     9.8  end
    10.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Mar 10 16:12:35 2015 +0000
    10.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Mar 16 15:30:00 2015 +0000
    10.3 @@ -226,7 +226,7 @@
    10.4  
    10.5  lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
    10.6  proof-
    10.7 -  have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
    10.8 +  have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
    10.9    from prime_factor_nat [OF f1]
   10.10    obtain p where "prime p" and "p dvd fact n + 1" by auto
   10.11    then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
   10.12 @@ -234,7 +234,7 @@
   10.13      from `prime p` have "p \<ge> 1"
   10.14        by (cases p, simp_all)
   10.15      with `p <= n` have "p dvd fact n"
   10.16 -      by (intro dvd_fact_nat)
   10.17 +      by (intro dvd_fact)
   10.18      with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
   10.19        by (rule dvd_diff_nat)
   10.20      then have "p dvd 1" by simp
    11.1 --- a/src/HOL/Number_Theory/Residues.thy	Tue Mar 10 16:12:35 2015 +0000
    11.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Mar 16 15:30:00 2015 +0000
    11.3 @@ -384,7 +384,7 @@
    11.4  
    11.5  lemma (in residues_prime) wilson_theorem1:
    11.6    assumes a: "p > 2"
    11.7 -  shows "[fact (p - 1) = - 1] (mod p)"
    11.8 +  shows "[fact (p - 1) = (-1::int)] (mod p)"
    11.9  proof -
   11.10    let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}"
   11.11    have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)"
   11.12 @@ -430,9 +430,9 @@
   11.13      apply (subst res_prime_units_eq)
   11.14      apply (simp add: int_setprod zmod_int setprod_int_eq)
   11.15      done
   11.16 -  finally have "fact (p - 1) mod p = \<ominus> \<one>".
   11.17 -  then show ?thesis
   11.18 -    by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
   11.19 +  finally have "fact (p - 1) mod p = (\<ominus> \<one> :: int)".
   11.20 +  then show ?thesis  
   11.21 +    by (metis of_nat_fact Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq)
   11.22  qed
   11.23  
   11.24  lemma wilson_theorem:
    12.1 --- a/src/HOL/Probability/Distributions.thy	Tue Mar 10 16:12:35 2015 +0000
    12.2 +++ b/src/HOL/Probability/Distributions.thy	Mon Mar 16 15:30:00 2015 +0000
    12.3 @@ -83,7 +83,9 @@
    12.4        (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (fact k)) \<partial>lborel)"
    12.5      by (intro nn_integral_multc[symmetric]) auto
    12.6    also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
    12.7 -    by (intro nn_integral_cong) (simp add: field_simps)
    12.8 +    apply (intro nn_integral_cong)
    12.9 +    apply (simp add: field_simps)
   12.10 +    by (metis (no_types) divide_inverse mult.commute mult.left_commute mult.left_neutral times_ereal.simps(1))
   12.11    also have "\<dots> = ereal (?F k a - ?F k 0)"
   12.12    proof (rule nn_integral_FTC_Icc)
   12.13      fix x assume "x \<in> {0..a}"
   12.14 @@ -93,13 +95,13 @@
   12.15      next
   12.16        case (Suc k)
   12.17        have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
   12.18 -        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k))"
   12.19 +        ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k))"
   12.20          by (intro DERIV_diff Suc)
   12.21             (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
   12.22                   simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
   12.23        also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
   12.24          by simp
   12.25 -      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / real (fact (Suc k)) = ?f (Suc k) x"
   12.26 +      also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k)) = ?f (Suc k) x"
   12.27          by (auto simp: field_simps simp del: fact_Suc)
   12.28             (simp_all add: real_of_nat_Suc field_simps)
   12.29        finally show ?case .
   12.30 @@ -122,7 +124,8 @@
   12.31      apply (metis nat_ceiling_le_eq)
   12.32      done
   12.33  
   12.34 -  have "((\<lambda>x. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / real (fact n))) * fact k) ---> (1 - (\<Sum>n\<le>k. 0 / real (fact n))) * fact k) at_top"
   12.35 +  have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
   12.36 +        (1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
   12.37      by (intro tendsto_intros tendsto_power_div_exp_0) simp
   12.38    then show "?X ----> fact k"
   12.39      by (subst nn_intergal_power_times_exp_Icc)
   12.40 @@ -514,7 +517,7 @@
   12.41        by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
   12.42    
   12.43      let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
   12.44 -    let ?C = "real (fact (Suc (k\<^sub>1 + k\<^sub>2))) / (real (fact k\<^sub>1) * real (fact k\<^sub>2))"
   12.45 +    let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))"
   12.46      let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
   12.47      let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)"
   12.48  
   12.49 @@ -919,10 +922,12 @@
   12.50  lemma
   12.51    fixes k :: nat
   12.52    shows gaussian_moment_even_pos:
   12.53 -    "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
   12.54 -       ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" (is "?even")
   12.55 +    "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
   12.56 +       ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 
   12.57 +       (is "?even")
   12.58      and gaussian_moment_odd_pos:
   12.59 -      "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" (is "?odd")
   12.60 +      "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" 
   12.61 +      (is "?odd")
   12.62  proof -
   12.63    let ?M = "\<lambda>k x. exp (- x\<^sup>2) * x^k :: real"
   12.64  
   12.65 @@ -997,9 +1002,11 @@
   12.66    proof (induct k)
   12.67      case (Suc k)
   12.68      note step[OF this]
   12.69 -    also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * (real (fact (2 * k)) / real (2 ^ (2 * k) * fact k)))) =
   12.70 -      sqrt pi / 2 * (real (fact (2 * Suc k)) / real (2 ^ (2 * Suc k) * fact (Suc k)))"
   12.71 -      by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
   12.72 +    also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) =
   12.73 +      sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))"
   12.74 +      apply (simp add: field_simps del: fact_Suc)
   12.75 +      apply (simp add: real_of_nat_def of_nat_mult field_simps)
   12.76 +      done
   12.77      finally show ?case
   12.78        by simp
   12.79    qed (insert gaussian_moment_0, simp)
   12.80 @@ -1008,7 +1015,7 @@
   12.81    proof (induct k)
   12.82      case (Suc k)
   12.83      note step[OF this]
   12.84 -    also have "(real (2 * k + 1 + 1) / 2 * (real (fact k) / 2)) = real (fact (Suc k)) / 2"
   12.85 +    also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2"
   12.86        by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
   12.87      finally show ?case
   12.88        by simp
   12.89 @@ -1036,7 +1043,7 @@
   12.90      by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult
   12.91                     real_sqrt_divide power_mult eq)
   12.92    also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 
   12.93 -    (inverse (sqrt 2 * \<sigma>) * (real (fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * real (fact k)))"
   12.94 +    (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))"
   12.95      by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult
   12.96                     power2_eq_square)
   12.97    finally show ?thesis
   12.98 @@ -1047,10 +1054,10 @@
   12.99  lemma normal_moment_abs_odd:
  12.100    "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))"
  12.101  proof -
  12.102 -  have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
  12.103 +  have "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
  12.104      by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto
  12.105    from has_bochner_integral_even_function[OF this]
  12.106 -  have "has_bochner_integral lborel (\<lambda>x. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
  12.107 +  have "has_bochner_integral lborel (\<lambda>x::real. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
  12.108      by simp
  12.109    then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))
  12.110        (fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))"
  12.111 @@ -1059,7 +1066,7 @@
  12.112      (\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))"
  12.113      by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult)
  12.114    also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 
  12.115 -    (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * real (fact k) * sqrt (2 / pi)))"
  12.116 +    (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))"
  12.117      by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide
  12.118                     real_sqrt_mult)
  12.119    finally show ?thesis
    13.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 16:12:35 2015 +0000
    13.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Mar 16 15:30:00 2015 +0000
    13.3 @@ -1321,9 +1321,7 @@
    13.4  begin
    13.5  
    13.6  lift_definition poisson_pmf :: "nat pmf" is "\<lambda>k. rate ^ k / fact k * exp (-rate)"
    13.7 -proof
    13.8 -  (* Proof by Manuel Eberl *)
    13.9 -
   13.10 +proof  (* by Manuel Eberl *)
   13.11    have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
   13.12      by (simp add: field_simps divide_inverse [symmetric])
   13.13    have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
   13.14 @@ -1332,10 +1330,10 @@
   13.15    also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
   13.16      by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
   13.17    also have "... = exp rate" unfolding exp_def
   13.18 -    by (simp add: field_simps divide_inverse [symmetric] transfer_int_nat_factorial)
   13.19 +    by (simp add: field_simps divide_inverse [symmetric])
   13.20    also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
   13.21      by (simp add: mult_exp_exp)
   13.22 -  finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
   13.23 +  finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
   13.24  qed (simp add: rate_pos[THEN less_imp_le])
   13.25  
   13.26  lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)"
    14.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Tue Mar 10 16:12:35 2015 +0000
    14.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Mon Mar 16 15:30:00 2015 +0000
    14.3 @@ -210,8 +210,8 @@
    14.4  
    14.5  lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
    14.6  proof -
    14.7 -  let ?k = "fact n + 1"
    14.8 -  have "1 < fact n + 1" by simp
    14.9 +  let ?k = "fact n + (1::nat)"
   14.10 +  have "1 < ?k" by simp
   14.11    then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
   14.12    have "n < p"
   14.13    proof -
    15.1 --- a/src/HOL/Proofs/Extraction/Util.thy	Tue Mar 10 16:12:35 2015 +0000
    15.2 +++ b/src/HOL/Proofs/Extraction/Util.thy	Mon Mar 16 15:30:00 2015 +0000
    15.3 @@ -5,7 +5,7 @@
    15.4  section {* Auxiliary lemmas used in program extraction examples *}
    15.5  
    15.6  theory Util
    15.7 -imports Old_Datatype
    15.8 +imports "~~/src/HOL/Library/Old_Datatype"
    15.9  begin
   15.10  
   15.11  text {*
    16.1 --- a/src/HOL/Taylor.thy	Tue Mar 10 16:12:35 2015 +0000
    16.2 +++ b/src/HOL/Taylor.thy	Mon Mar 16 15:30:00 2015 +0000
    16.3 @@ -17,8 +17,8 @@
    16.4    assumes INIT: "n>0" "diff 0 = f"
    16.5    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
    16.6    and INTERV: "a \<le> c" "c < b" 
    16.7 -  shows "\<exists> t. c < t & t < b & 
    16.8 -    f b = (\<Sum>m<n. (diff m c / real (fact m)) * (b - c)^m) + (diff n t / real (fact n)) * (b - c)^n"
    16.9 +  shows "\<exists>t::real. c < t & t < b & 
   16.10 +    f b = (\<Sum>m<n. (diff m c / (fact m)) * (b - c)^m) + (diff n t / (fact n)) * (b - c)^n"
   16.11  proof -
   16.12    from INTERV have "0 < b-c" by arith
   16.13    moreover 
   16.14 @@ -35,31 +35,24 @@
   16.15        by (rule DERIV_chain2)
   16.16      thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
   16.17    qed
   16.18 -  ultimately 
   16.19 -  have EX:"EX t>0. t < b - c & 
   16.20 -    f (b - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
   16.21 -      diff n (t + c) / real (fact n) * (b - c) ^ n" 
   16.22 -    by (rule Maclaurin)
   16.23 -  show ?thesis
   16.24 -  proof -
   16.25 -    from EX obtain x where 
   16.26 -      X: "0 < x & x < b - c & 
   16.27 -        f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / real (fact m) * (b - c) ^ m) +
   16.28 -          diff n (x + c) / real (fact n) * (b - c) ^ n" ..
   16.29 -    let ?H = "x + c"
   16.30 -    from X have "c<?H & ?H<b \<and> f b = (\<Sum>m<n. diff m c / real (fact m) * (b - c) ^ m) +
   16.31 -      diff n ?H / real (fact n) * (b - c) ^ n"
   16.32 -      by fastforce
   16.33 -    thus ?thesis by fastforce
   16.34 -  qed
   16.35 +  ultimately obtain x where 
   16.36 +        "0 < x & x < b - c & 
   16.37 +        f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b - c) ^ m) +
   16.38 +          diff n (x + c) / (fact n) * (b - c) ^ n"
   16.39 +     by (rule Maclaurin [THEN exE])
   16.40 +  then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b - c) ^ m) +
   16.41 +    diff n (x+c) / (fact n) * (b - c) ^ n"
   16.42 +    by fastforce
   16.43 +  thus ?thesis by fastforce
   16.44  qed
   16.45  
   16.46  lemma taylor_down:
   16.47 +  fixes a::real
   16.48    assumes INIT: "n>0" "diff 0 = f"
   16.49    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   16.50    and INTERV: "a < c" "c \<le> b"
   16.51    shows "\<exists> t. a < t & t < c & 
   16.52 -    f a = (\<Sum>m<n. (diff m c / real (fact m)) * (a - c)^m) + (diff n t / real (fact n)) * (a - c)^n" 
   16.53 +    f a = (\<Sum>m<n. (diff m c / (fact m)) * (a - c)^m) + (diff n t / (fact n)) * (a - c)^n" 
   16.54  proof -
   16.55    from INTERV have "a-c < 0" by arith
   16.56    moreover 
   16.57 @@ -75,30 +68,24 @@
   16.58      ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
   16.59      thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
   16.60    qed
   16.61 -  ultimately 
   16.62 -  have EX: "EX t>a - c. t < 0 &
   16.63 -    f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
   16.64 -      diff n (t + c) / real (fact n) * (a - c) ^ n" 
   16.65 -    by (rule Maclaurin_minus)
   16.66 -  show ?thesis
   16.67 -  proof -
   16.68 -    from EX obtain x where X: "a - c < x & x < 0 &
   16.69 -      f (a - c + c) = (SUM m<n. diff m (0 + c) / real (fact m) * (a - c) ^ m) +
   16.70 -        diff n (x + c) / real (fact n) * (a - c) ^ n" ..
   16.71 -    let ?H = "x + c"
   16.72 -    from X have "a<?H & ?H<c \<and> f a = (\<Sum>m<n. diff m c / real (fact m) * (a - c) ^ m) +
   16.73 -      diff n ?H / real (fact n) * (a - c) ^ n"
   16.74 -      by fastforce
   16.75 -    thus ?thesis by fastforce
   16.76 -  qed
   16.77 +  ultimately obtain x where 
   16.78 +         "a - c < x & x < 0 &
   16.79 +      f (a - c + c) = (SUM m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
   16.80 +        diff n (x + c) / (fact n) * (a - c) ^ n"
   16.81 +     by (rule Maclaurin_minus [THEN exE])
   16.82 +  then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
   16.83 +      diff n (x+c) / (fact n) * (a - c) ^ n"
   16.84 +    by fastforce
   16.85 +  thus ?thesis by fastforce
   16.86  qed
   16.87  
   16.88  lemma taylor:
   16.89 +  fixes a::real
   16.90    assumes INIT: "n>0" "diff 0 = f"
   16.91    and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
   16.92    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c" 
   16.93    shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
   16.94 -    f x = (\<Sum>m<n. (diff m c / real (fact m)) * (x - c)^m) + (diff n t / real (fact n)) * (x - c)^n" 
   16.95 +    f x = (\<Sum>m<n. (diff m c / (fact m)) * (x - c)^m) + (diff n t / (fact n)) * (x - c)^n" 
   16.96  proof (cases "x<c")
   16.97    case True
   16.98    note INIT
   16.99 @@ -107,8 +94,8 @@
  16.100      by fastforce
  16.101    moreover note True
  16.102    moreover from INTERV have "c \<le> b" by simp
  16.103 -  ultimately have EX: "\<exists>t>x. t < c \<and> f x =
  16.104 -    (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n"
  16.105 +  ultimately have "\<exists>t>x. t < c \<and> f x =
  16.106 +    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
  16.107      by (rule taylor_down)
  16.108    with True show ?thesis by simp
  16.109  next
  16.110 @@ -119,8 +106,8 @@
  16.111      by fastforce
  16.112    moreover from INTERV have "a \<le> c" by arith
  16.113    moreover from False and INTERV have "c < x" by arith
  16.114 -  ultimately have EX: "\<exists>t>c. t < x \<and> f x =
  16.115 -    (\<Sum>m<n. diff m c / real (fact m) * (x - c) ^ m) + diff n t / real (fact n) * (x - c) ^ n" 
  16.116 +  ultimately have "\<exists>t>c. t < x \<and> f x =
  16.117 +    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n" 
  16.118      by (rule taylor_up)
  16.119    with False show ?thesis by simp
  16.120  qed
    17.1 --- a/src/HOL/Transcendental.thy	Tue Mar 10 16:12:35 2015 +0000
    17.2 +++ b/src/HOL/Transcendental.thy	Mon Mar 16 15:30:00 2015 +0000
    17.3 @@ -10,6 +10,12 @@
    17.4  imports Binomial Series Deriv NthRoot
    17.5  begin
    17.6  
    17.7 +lemma of_real_fact [simp]: "of_real (fact n) = fact n"
    17.8 +  by (metis of_nat_fact of_real_of_nat_eq)
    17.9 +
   17.10 +lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
   17.11 +  by (simp add: real_of_nat_def)
   17.12 +
   17.13  lemma root_test_convergence:
   17.14    fixes f :: "nat \<Rightarrow> 'a::banach"
   17.15    assumes f: "(\<lambda>n. root n (norm (f n))) ----> x" -- "could be weakened to lim sup"
   17.16 @@ -54,13 +60,13 @@
   17.17        (x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))"
   17.18  proof (induct n)
   17.19    case (Suc n)
   17.20 -  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
   17.21 +  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x^n) - y * (y * y ^ n)"
   17.22      by simp
   17.23 -  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
   17.24 +  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x^n)"
   17.25      by (simp add: algebra_simps)
   17.26 -  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
   17.27 +  also have "... = y * ((x - y) * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
   17.28      by (simp only: Suc)
   17.29 -  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
   17.30 +  also have "... = (x - y) * (y * (\<Sum>p<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x^n)"
   17.31      by (simp only: mult.left_commute)
   17.32    also have "... = (x - y) * (\<Sum>p<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
   17.33      by (simp add: field_simps Suc_diff_le setsum_left_distrib setsum_right_distrib)
   17.34 @@ -100,40 +106,40 @@
   17.35  
   17.36  lemma powser_insidea:
   17.37    fixes x z :: "'a::real_normed_div_algebra"
   17.38 -  assumes 1: "summable (\<lambda>n. f n * x ^ n)"
   17.39 +  assumes 1: "summable (\<lambda>n. f n * x^n)"
   17.40      and 2: "norm z < norm x"
   17.41    shows "summable (\<lambda>n. norm (f n * z ^ n))"
   17.42  proof -
   17.43    from 2 have x_neq_0: "x \<noteq> 0" by clarsimp
   17.44 -  from 1 have "(\<lambda>n. f n * x ^ n) ----> 0"
   17.45 +  from 1 have "(\<lambda>n. f n * x^n) ----> 0"
   17.46      by (rule summable_LIMSEQ_zero)
   17.47 -  hence "convergent (\<lambda>n. f n * x ^ n)"
   17.48 +  hence "convergent (\<lambda>n. f n * x^n)"
   17.49      by (rule convergentI)
   17.50 -  hence "Cauchy (\<lambda>n. f n * x ^ n)"
   17.51 +  hence "Cauchy (\<lambda>n. f n * x^n)"
   17.52      by (rule convergent_Cauchy)
   17.53 -  hence "Bseq (\<lambda>n. f n * x ^ n)"
   17.54 +  hence "Bseq (\<lambda>n. f n * x^n)"
   17.55      by (rule Cauchy_Bseq)
   17.56 -  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"
   17.57 +  then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x^n) \<le> K"
   17.58      by (simp add: Bseq_def, safe)
   17.59    have "\<exists>N. \<forall>n\<ge>N. norm (norm (f n * z ^ n)) \<le>
   17.60 -                   K * norm (z ^ n) * inverse (norm (x ^ n))"
   17.61 +                   K * norm (z ^ n) * inverse (norm (x^n))"
   17.62    proof (intro exI allI impI)
   17.63      fix n::nat
   17.64      assume "0 \<le> n"
   17.65 -    have "norm (norm (f n * z ^ n)) * norm (x ^ n) =
   17.66 -          norm (f n * x ^ n) * norm (z ^ n)"
   17.67 +    have "norm (norm (f n * z ^ n)) * norm (x^n) =
   17.68 +          norm (f n * x^n) * norm (z ^ n)"
   17.69        by (simp add: norm_mult abs_mult)
   17.70      also have "\<dots> \<le> K * norm (z ^ n)"
   17.71        by (simp only: mult_right_mono 4 norm_ge_zero)
   17.72 -    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x ^ n)) * norm (x ^ n))"
   17.73 +    also have "\<dots> = K * norm (z ^ n) * (inverse (norm (x^n)) * norm (x^n))"
   17.74        by (simp add: x_neq_0)
   17.75 -    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x ^ n)) * norm (x ^ n)"
   17.76 +    also have "\<dots> = K * norm (z ^ n) * inverse (norm (x^n)) * norm (x^n)"
   17.77        by (simp only: mult.assoc)
   17.78      finally show "norm (norm (f n * z ^ n)) \<le>
   17.79 -                  K * norm (z ^ n) * inverse (norm (x ^ n))"
   17.80 +                  K * norm (z ^ n) * inverse (norm (x^n))"
   17.81        by (simp add: mult_le_cancel_right x_neq_0)
   17.82    qed
   17.83 -  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   17.84 +  moreover have "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
   17.85    proof -
   17.86      from 2 have "norm (norm (z * inverse x)) < 1"
   17.87        using x_neq_0
   17.88 @@ -142,7 +148,7 @@
   17.89        by (rule summable_geometric)
   17.90      hence "summable (\<lambda>n. K * norm (z * inverse x) ^ n)"
   17.91        by (rule summable_mult)
   17.92 -    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x ^ n)))"
   17.93 +    thus "summable (\<lambda>n. K * norm (z ^ n) * inverse (norm (x^n)))"
   17.94        using x_neq_0
   17.95        by (simp add: norm_mult nonzero_norm_inverse power_mult_distrib
   17.96                      power_inverse norm_power mult.assoc)
   17.97 @@ -154,7 +160,7 @@
   17.98  lemma powser_inside:
   17.99    fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
  17.100    shows
  17.101 -    "summable (\<lambda>n. f n * (x ^ n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
  17.102 +    "summable (\<lambda>n. f n * (x^n)) \<Longrightarrow> norm z < norm x \<Longrightarrow>
  17.103        summable (\<lambda>n. f n * (z ^ n))"
  17.104    by (rule powser_insidea [THEN summable_norm_cancel])
  17.105  
  17.106 @@ -581,7 +587,7 @@
  17.107    fixes x :: "'a::{real_normed_field,banach}"
  17.108    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
  17.109      and 2: "norm x < norm K"
  17.110 -  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h
  17.111 +  shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
  17.112               - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
  17.113  proof -
  17.114    from dense [OF 2]
  17.115 @@ -629,7 +635,7 @@
  17.116      hence "norm x + norm h < r" by simp
  17.117      with norm_triangle_ineq have xh: "norm (x + h) < r"
  17.118        by (rule order_le_less_trans)
  17.119 -    show "norm (c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))
  17.120 +    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))
  17.121            \<le> norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
  17.122        apply (simp only: norm_mult mult.assoc)
  17.123        apply (rule mult_left_mono [OF _ norm_ge_zero])
  17.124 @@ -645,11 +651,11 @@
  17.125        and 2: "summable (\<lambda>n. (diffs c) n * K ^ n)"
  17.126        and 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
  17.127        and 4: "norm x < norm K"
  17.128 -  shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
  17.129 +  shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. (diffs c) n * x^n)"
  17.130    unfolding DERIV_def
  17.131  proof (rule LIM_zero_cancel)
  17.132 -  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
  17.133 -            - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
  17.134 +  show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
  17.135 +            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
  17.136    proof (rule LIM_equal2)
  17.137      show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
  17.138    next
  17.139 @@ -658,18 +664,18 @@
  17.140      hence "norm x + norm h < norm K" by simp
  17.141      hence 5: "norm (x + h) < norm K"
  17.142        by (rule norm_triangle_ineq [THEN order_le_less_trans])
  17.143 -    have "summable (\<lambda>n. c n * x ^ n)"
  17.144 +    have "summable (\<lambda>n. c n * x^n)"
  17.145        and "summable (\<lambda>n. c n * (x + h) ^ n)"
  17.146 -      and "summable (\<lambda>n. diffs c n * x ^ n)"
  17.147 +      and "summable (\<lambda>n. diffs c n * x^n)"
  17.148        using 1 2 4 5 by (auto elim: powser_inside)
  17.149 -    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
  17.150 -          (\<Sum>n. (c n * (x + h) ^ n - c n * x ^ n) / h - of_nat n * c n * x ^ (n - Suc 0))"
  17.151 +    then have "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
  17.152 +          (\<Sum>n. (c n * (x + h) ^ n - c n * x^n) / h - of_nat n * c n * x ^ (n - Suc 0))"
  17.153        by (intro sums_unique sums_diff sums_divide diffs_equiv summable_sums)
  17.154 -    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x ^ n)) / h - (\<Sum>n. diffs c n * x ^ n) =
  17.155 -          (\<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)))"
  17.156 +    then show "((\<Sum>n. c n * (x + h) ^ n) - (\<Sum>n. c n * x^n)) / h - (\<Sum>n. diffs c n * x^n) =
  17.157 +          (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
  17.158        by (simp add: algebra_simps)
  17.159    next
  17.160 -    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
  17.161 +    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
  17.162        by (rule termdiffs_aux [OF 3 4])
  17.163    qed
  17.164  qed
  17.165 @@ -889,7 +895,7 @@
  17.166            fix n
  17.167            have le: "\<bar>f n\<bar> * 1 \<le> \<bar>f n\<bar> * real (Suc n)"
  17.168              by (rule mult_left_mono) auto
  17.169 -          show "norm (f n * x ^ n) \<le> norm (f n * real (Suc n) * x ^ n)"
  17.170 +          show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
  17.171              unfolding real_norm_def abs_mult
  17.172              by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
  17.173          qed (rule powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`])
  17.174 @@ -925,14 +931,14 @@
  17.175  subsection {* Exponential Function *}
  17.176  
  17.177  definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
  17.178 -  where "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
  17.179 +  where "exp = (\<lambda>x. \<Sum>n. x^n /\<^sub>R fact n)"
  17.180  
  17.181  lemma summable_exp_generic:
  17.182    fixes x :: "'a::{real_normed_algebra_1,banach}"
  17.183 -  defines S_def: "S \<equiv> \<lambda>n. x ^ n /\<^sub>R real (fact n)"
  17.184 +  defines S_def: "S \<equiv> \<lambda>n. x^n /\<^sub>R fact n"
  17.185    shows "summable S"
  17.186  proof -
  17.187 -  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R real (Suc n)"
  17.188 +  have S_Suc: "\<And>n. S (Suc n) = (x * S n) /\<^sub>R (Suc n)"
  17.189      unfolding S_def by (simp del: mult_Suc)
  17.190    obtain r :: real where r0: "0 < r" and r1: "r < 1"
  17.191      using dense [OF zero_less_one] by fast
  17.192 @@ -959,26 +965,29 @@
  17.193  
  17.194  lemma summable_norm_exp:
  17.195    fixes x :: "'a::{real_normed_algebra_1,banach}"
  17.196 -  shows "summable (\<lambda>n. norm (x ^ n /\<^sub>R real (fact n)))"
  17.197 +  shows "summable (\<lambda>n. norm (x^n /\<^sub>R fact n))"
  17.198  proof (rule summable_norm_comparison_test [OF exI, rule_format])
  17.199 -  show "summable (\<lambda>n. norm x ^ n /\<^sub>R real (fact n))"
  17.200 +  show "summable (\<lambda>n. norm x^n /\<^sub>R fact n)"
  17.201      by (rule summable_exp_generic)
  17.202    fix n
  17.203 -  show "norm (x ^ n /\<^sub>R real (fact n)) \<le> norm x ^ n /\<^sub>R real (fact n)"
  17.204 +  show "norm (x^n /\<^sub>R fact n) \<le> norm x^n /\<^sub>R fact n"
  17.205      by (simp add: norm_power_ineq)
  17.206  qed
  17.207  
  17.208 -lemma summable_exp: "summable (\<lambda>n. inverse (real (fact n)) * x ^ n)"
  17.209 -  using summable_exp_generic [where x=x] by simp
  17.210 -
  17.211 -lemma exp_converges: "(\<lambda>n. x ^ n /\<^sub>R real (fact n)) sums exp x"
  17.212 +lemma summable_exp: 
  17.213 +  fixes x :: "'a::{real_normed_field,banach}"
  17.214 +  shows "summable (\<lambda>n. inverse (fact n) * x^n)"
  17.215 +  using summable_exp_generic [where x=x]
  17.216 +  by (simp add: scaleR_conv_of_real nonzero_of_real_inverse)
  17.217 +
  17.218 +lemma exp_converges: "(\<lambda>n. x^n /\<^sub>R fact n) sums exp x"
  17.219    unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
  17.220  
  17.221 -
  17.222  lemma exp_fdiffs:
  17.223 -      "diffs (\<lambda>n. inverse(real (fact n))) = (\<lambda>n. inverse(real (fact n)))"
  17.224 -  by (simp add: diffs_def mult.assoc [symmetric] real_of_nat_def of_nat_mult
  17.225 -        del: mult_Suc of_nat_Suc)
  17.226 +  fixes XXX :: "'a::{real_normed_field,banach}"
  17.227 +  shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
  17.228 +  by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
  17.229 +           del: mult_Suc of_nat_Suc)
  17.230  
  17.231  lemma diffs_of_real: "diffs (\<lambda>n. of_real (f n)) = (\<lambda>n. of_real (diffs f n))"
  17.232    by (simp add: diffs_def)
  17.233 @@ -997,7 +1006,7 @@
  17.234  lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
  17.235  proof -
  17.236    from summable_norm[OF summable_norm_exp, of x]
  17.237 -  have "norm (exp x) \<le> (\<Sum>n. inverse (real (fact n)) * norm (x ^ n))"
  17.238 +  have "norm (exp x) \<le> (\<Sum>n. inverse (fact n) * norm (x^n))"
  17.239      by (simp add: exp_def)
  17.240    also have "\<dots> \<le> exp (norm x)"
  17.241      using summable_exp_generic[of "norm x"] summable_norm_exp[of x]
  17.242 @@ -1047,7 +1056,7 @@
  17.243  
  17.244  lemma exp_series_add_commuting:
  17.245    fixes x y :: "'a::{real_normed_algebra_1, banach}"
  17.246 -  defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
  17.247 +  defines S_def: "S \<equiv> \<lambda>x n. x^n /\<^sub>R fact n"
  17.248    assumes comm: "x * y = y * x"
  17.249    shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
  17.250  proof (induct n)
  17.251 @@ -1182,9 +1191,9 @@
  17.252  using order_le_imp_less_or_eq [OF assms]
  17.253  proof
  17.254    assume "0 < x"
  17.255 -  have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
  17.256 +  have "1+x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
  17.257      by (auto simp add: numeral_2_eq_2)
  17.258 -  also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
  17.259 +  also have "... \<le> (\<Sum>n. inverse (fact n) * x^n)"
  17.260      apply (rule setsum_le_suminf [OF summable_exp])
  17.261      using `0 < x`
  17.262      apply (auto  simp add:  zero_le_mult_iff)
  17.263 @@ -1297,7 +1306,7 @@
  17.264  lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
  17.265    by (rule ln_unique) (simp add: exp_diff)
  17.266  
  17.267 -lemma ln_realpow: "0 < x \<Longrightarrow> ln (x ^ n) = real n * ln x"
  17.268 +lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
  17.269    by (rule ln_unique) (simp add: exp_real_of_nat_mult)
  17.270  
  17.271  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
  17.272 @@ -1424,7 +1433,7 @@
  17.273        fix x :: real
  17.274        assume "x \<in> {- 1<..<1}"
  17.275        hence "norm (-x) < 1" by auto
  17.276 -      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
  17.277 +      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
  17.278          unfolding One_nat_def
  17.279          by (auto simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
  17.280      qed
  17.281 @@ -1439,12 +1448,14 @@
  17.282    thus ?thesis by auto
  17.283  qed
  17.284  
  17.285 -lemma exp_first_two_terms: "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  17.286 +lemma exp_first_two_terms:
  17.287 +  fixes x :: "'a::{real_normed_field,banach}"
  17.288 +  shows "exp x = 1 + x + (\<Sum> n. inverse(fact (n+2)) * (x ^ (n+2)))"
  17.289  proof -
  17.290 -  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x ^ n))"
  17.291 -    by (simp add: exp_def)
  17.292 +  have "exp x = suminf (\<lambda>n. inverse(fact n) * (x^n))"
  17.293 +    by (simp add: exp_def scaleR_conv_of_real nonzero_of_real_inverse)
  17.294    also from summable_exp have "... = (\<Sum> n. inverse(fact(n+2)) * (x ^ (n+2))) +
  17.295 -    (\<Sum> n::nat<2. inverse(fact n) * (x ^ n))" (is "_ = _ + ?a")
  17.296 +    (\<Sum> n::nat<2. inverse(fact n) * (x^n))" (is "_ = _ + ?a")
  17.297      by (rule suminf_split_initial_segment)
  17.298    also have "?a = 1 + x"
  17.299      by (simp add: numeral_2_eq_2)
  17.300 @@ -1458,21 +1469,22 @@
  17.301    assume b: "x <= 1"
  17.302    {
  17.303      fix n :: nat
  17.304 -    have "2 * 2 ^ n \<le> fact (n + 2)"
  17.305 +    have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
  17.306        by (induct n) simp_all
  17.307 -    hence "real ((2::nat) * 2 ^ n) \<le> real (fact (n + 2))"
  17.308 +    hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
  17.309        by (simp only: real_of_nat_le_iff)
  17.310 -    hence "2 * 2 ^ n \<le> real (fact (n + 2))"
  17.311 -      by simp
  17.312 -    hence "inverse (fact (n + 2)) \<le> inverse (2 * 2 ^ n)"
  17.313 +    hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
  17.314 +      unfolding of_nat_fact real_of_nat_def
  17.315 +      by (simp add: of_nat_mult of_nat_power)
  17.316 +    hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
  17.317        by (rule le_imp_inverse_le) simp
  17.318 -    hence "inverse (fact (n + 2)) \<le> 1/2 * (1/2)^n"
  17.319 +    hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
  17.320        by (simp add: power_inverse)
  17.321      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
  17.322        by (rule mult_mono)
  17.323          (rule mult_mono, simp_all add: power_le_one a b)
  17.324      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
  17.325 -      unfolding power_add by (simp add: ac_simps del: fact_Suc) }
  17.326 +      unfolding power_add by (simp add: ac_simps del: fact.simps) }
  17.327    note aux1 = this
  17.328    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
  17.329      by (intro sums_mult geometric_sums, simp)
  17.330 @@ -2140,7 +2152,7 @@
  17.331  lemma log_powr: "log b (x powr y) = y * log b x"
  17.332    by (simp add: log_def ln_powr)
  17.333  
  17.334 -lemma log_nat_power: "0 < x \<Longrightarrow> log b (x ^ n) = real n * log b x"
  17.335 +lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
  17.336    by (simp add: log_powr powr_realpow [symmetric])
  17.337  
  17.338  lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
  17.339 @@ -2342,10 +2354,10 @@
  17.340  subsection {* Sine and Cosine *}
  17.341  
  17.342  definition sin_coeff :: "nat \<Rightarrow> real" where
  17.343 -  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / real (fact n))"
  17.344 +  "sin_coeff = (\<lambda>n. if even n then 0 else (- 1) ^ ((n - Suc 0) div 2) / (fact n))"
  17.345  
  17.346  definition cos_coeff :: "nat \<Rightarrow> real" where
  17.347 -  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / real (fact n) else 0)"
  17.348 +  "cos_coeff = (\<lambda>n. if even n then ((- 1) ^ (n div 2)) / (fact n) else 0)"
  17.349  
  17.350  definition sin :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
  17.351    where "sin = (\<lambda>x. \<Sum>n. sin_coeff n *\<^sub>R x^n)"
  17.352 @@ -2377,7 +2389,7 @@
  17.353  
  17.354  lemma summable_norm_cos:
  17.355    fixes x :: "'a::{real_normed_algebra_1,banach}"
  17.356 -  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x ^ n))"
  17.357 +  shows "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
  17.358    unfolding cos_coeff_def
  17.359    apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
  17.360    apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
  17.361 @@ -2398,7 +2410,7 @@
  17.362    have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R  x^n)) = (\<lambda>n. sin_coeff n *\<^sub>R  (of_real x)^n)"
  17.363    proof
  17.364      fix n
  17.365 -    show "of_real (sin_coeff n *\<^sub>R  x ^ n) = sin_coeff n *\<^sub>R of_real x ^ n"
  17.366 +    show "of_real (sin_coeff n *\<^sub>R  x^n) = sin_coeff n *\<^sub>R of_real x^n"
  17.367        by (simp add: scaleR_conv_of_real)
  17.368    qed
  17.369    also have "... sums (sin (of_real x))"
  17.370 @@ -2416,7 +2428,7 @@
  17.371    have "(\<lambda>n. of_real (cos_coeff n *\<^sub>R  x^n)) = (\<lambda>n. cos_coeff n *\<^sub>R  (of_real x)^n)"
  17.372    proof
  17.373      fix n
  17.374 -    show "of_real (cos_coeff n *\<^sub>R  x ^ n) = cos_coeff n *\<^sub>R of_real x ^ n"
  17.375 +    show "of_real (cos_coeff n *\<^sub>R  x^n) = cos_coeff n *\<^sub>R of_real x^n"
  17.376        by (simp add: scaleR_conv_of_real)
  17.377    qed
  17.378    also have "... sums (cos (of_real x))"
  17.379 @@ -2549,7 +2561,7 @@
  17.380    fixes x :: "'a::{real_normed_field,banach}"
  17.381    shows "(\<lambda>p. \<Sum>n\<le>p.
  17.382            if even p \<and> even n
  17.383 -          then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.384 +          then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.385           sums (cos x * cos y)"
  17.386  proof -
  17.387    { fix n p::nat
  17.388 @@ -2557,12 +2569,12 @@
  17.389      then have *: "even n \<Longrightarrow> even p \<Longrightarrow> (-1) ^ (n div 2) * (-1) ^ ((p - n) div 2) = (-1 :: real) ^ (p div 2)"
  17.390        by (metis div_add power_add le_add_diff_inverse odd_add)
  17.391      have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
  17.392 -          (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.393 +          (if even p \<and> even n then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.394      using `n\<le>p`
  17.395        by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
  17.396    }
  17.397    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> even n
  17.398 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  17.399 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  17.400               (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
  17.401      by simp
  17.402    also have "... = (\<lambda>p. \<Sum>n\<le>p. (cos_coeff n *\<^sub>R x^n) * (cos_coeff (p - n) *\<^sub>R y^(p-n)))"
  17.403 @@ -2578,7 +2590,7 @@
  17.404    fixes x :: "'a::{real_normed_field,banach}"
  17.405    shows "(\<lambda>p. \<Sum>n\<le>p.
  17.406            if even p \<and> odd n
  17.407 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.408 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.409           sums (sin x * sin y)"
  17.410  proof -
  17.411    { fix n p::nat
  17.412 @@ -2596,12 +2608,12 @@
  17.413      } then
  17.414      have "(sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
  17.415            (if even p \<and> odd n
  17.416 -          then -((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.417 +          then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.418      using `n\<le>p`
  17.419        by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
  17.420    }
  17.421    then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
  17.422 -               then - ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  17.423 +               then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
  17.424               (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n * sin_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)))"
  17.425      by simp
  17.426    also have "... = (\<lambda>p. \<Sum>n\<le>p. (sin_coeff n *\<^sub>R x^n) * (sin_coeff (p - n) *\<^sub>R y^(p-n)))"
  17.427 @@ -2616,31 +2628,31 @@
  17.428    fixes x :: "'a::{real_normed_field,banach}"
  17.429    shows
  17.430    "(\<lambda>p. \<Sum>n\<le>p. if even p
  17.431 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.432 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.433                 else 0)
  17.434          sums cos (x + y)"
  17.435  proof -
  17.436    { fix p::nat
  17.437      have "(\<Sum>n\<le>p. if even p
  17.438 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.439 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.440                    else 0) =
  17.441            (if even p
  17.442 -                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.443 +                  then \<Sum>n\<le>p. ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.444                    else 0)"
  17.445        by simp
  17.446      also have "... = (if even p
  17.447 -                  then of_real ((-1) ^ (p div 2) / of_nat (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
  17.448 +                  then of_real ((-1) ^ (p div 2) / (fact p)) * (\<Sum>n\<le>p. (p choose n) *\<^sub>R (x^n) * y^(p-n))
  17.449                    else 0)"
  17.450        by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
  17.451      also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
  17.452        by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
  17.453      finally have "(\<Sum>n\<le>p. if even p
  17.454 -                  then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.455 +                  then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.456                    else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
  17.457    }
  17.458    then have "(\<lambda>p. \<Sum>n\<le>p.
  17.459                 if even p
  17.460 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.461 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
  17.462                 else 0)
  17.463          = (\<lambda>p. cos_coeff p *\<^sub>R ((x+y)^p))"
  17.464          by simp
  17.465 @@ -2656,15 +2668,15 @@
  17.466    { fix n p::nat
  17.467      assume "n\<le>p"
  17.468      then have "(if even p \<and> even n
  17.469 -               then ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
  17.470 +               then ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) -
  17.471            (if even p \<and> odd n
  17.472 -               then - ((- 1) ^ (p div 2) * int (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.473 +               then - ((- 1) ^ (p div 2) * int (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)
  17.474            = (if even p
  17.475 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.476 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
  17.477        by simp
  17.478    }
  17.479    then have "(\<lambda>p. \<Sum>n\<le>p. (if even p
  17.480 -               then ((-1) ^ (p div 2) * (p choose n) / of_nat (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
  17.481 +               then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0))
  17.482          sums (cos x * cos y - sin x * sin y)"
  17.483      using sums_diff [OF cos_x_cos_y [of x y] sin_x_sin_y [of x y]]
  17.484      by (simp add: setsum_subtractf [symmetric])
  17.485 @@ -2701,7 +2713,6 @@
  17.486  by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
  17.487                suminf_minus sums_iff equation_minus_iff)
  17.488  
  17.489 -
  17.490  lemma sin_cos_squared_add [simp]:
  17.491    fixes x :: "'a::{real_normed_field,banach}"
  17.492    shows "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
  17.493 @@ -2787,7 +2798,7 @@
  17.494  
  17.495  lemma sin_paired:
  17.496    fixes x :: real
  17.497 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n + 1))) * x ^ (2 * n + 1)) sums  sin x"
  17.498 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n + 1)) * x ^ (2 * n + 1)) sums  sin x"
  17.499  proof -
  17.500    have "(\<lambda>n. \<Sum>k = n*2..<n * 2 + 2. sin_coeff k * x ^ k) sums sin x"
  17.501      apply (rule sums_group)
  17.502 @@ -2801,7 +2812,7 @@
  17.503    assumes "0 < x" and "x < 2"
  17.504    shows "0 < sin x"
  17.505  proof -
  17.506 -  let ?f = "\<lambda>n. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / real (fact (2*k+1)) * x^(2*k+1)"
  17.507 +  let ?f = "\<lambda>n::nat. \<Sum>k = n*2..<n*2+2. (- 1) ^ k / (fact (2*k+1)) * x^(2*k+1)"
  17.508    have pos: "\<forall>n. 0 < ?f n"
  17.509    proof
  17.510      fix n :: nat
  17.511 @@ -2812,9 +2823,8 @@
  17.512      hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
  17.513        by (intro mult_strict_right_mono zero_less_power `0 < x`)
  17.514      thus "0 < ?f n"
  17.515 -      by (simp del: mult_Suc,
  17.516 -        simp add: less_divide_eq field_simps del: mult_Suc)
  17.517 -  qed
  17.518 +      by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
  17.519 +qed
  17.520    have sums: "?f sums sin x"
  17.521      by (rule sin_paired [THEN sums_group], simp)
  17.522    show "0 < sin x"
  17.523 @@ -2830,7 +2840,7 @@
  17.524  
  17.525  lemma cos_paired:
  17.526    fixes x :: real
  17.527 -  shows "(\<lambda>n. (- 1) ^ n /(real (fact (2 * n))) * x ^ (2 * n)) sums cos x"
  17.528 +  shows "(\<lambda>n. (- 1) ^ n / (fact (2 * n)) * x ^ (2 * n)) sums cos x"
  17.529  proof -
  17.530    have "(\<lambda>n. \<Sum>k = n * 2..<n * 2 + 2. cos_coeff k * x ^ k) sums cos x"
  17.531      apply (rule sums_group)
  17.532 @@ -2860,29 +2870,28 @@
  17.533  lemma cos_two_less_zero [simp]:
  17.534    "cos 2 < (0::real)"
  17.535  proof -
  17.536 -  note fact_Suc [simp del]
  17.537 -  from cos_paired
  17.538 -  have "(\<lambda>n. - ((- 1) ^ n / real (fact (2 * n)) * 2 ^ (2 * n))) sums - cos 2"
  17.539 -    by (rule sums_minus)
  17.540 -  then have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n)))) sums - cos 2"
  17.541 +  note fact.simps(2) [simp del]
  17.542 +  from sums_minus [OF cos_paired]
  17.543 +  have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
  17.544      by simp
  17.545 -  then have **: "summable (\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  17.546 +  then have **: "summable (\<lambda>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  17.547      by (rule sums_summable)
  17.548 -  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  17.549 -    by (simp add: fact_num_eq_if_nat realpow_num_eq_if)
  17.550 -  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1) ^ n  * 2 ^ (2 * n) / real (fact (2 * n))))
  17.551 -    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  17.552 +  have "0 < (\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  17.553 +    by (simp add: fact_num_eq_if realpow_num_eq_if)
  17.554 +  moreover have "(\<Sum>n<Suc (Suc (Suc 0)). - ((- 1::real) ^ n  * 2 ^ (2 * n) / (fact (2 * n))))
  17.555 +    < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  17.556    proof -
  17.557      { fix d
  17.558 -      have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  17.559 -       < real (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  17.560 -           fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  17.561 -        by (simp only: real_of_nat_mult) (auto intro!: mult_strict_mono fact_less_mono_nat)
  17.562 -      then have "4 * real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  17.563 -        < real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  17.564 -        by (simp only: fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
  17.565 -      then have "4 * inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))))
  17.566 -        < inverse (real (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  17.567 +      have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  17.568 +            < (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))) *
  17.569 +              fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))))"
  17.570 +        unfolding real_of_nat_mult
  17.571 +        by (rule mult_strict_mono) (simp_all add: fact_less_mono)
  17.572 +      then have "(4::real) * (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))
  17.573 +        <  (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))"
  17.574 +        by (simp only: fact.simps(2) [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"] real_of_nat_def of_nat_mult of_nat_fact)
  17.575 +      then have "(4::real) * inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))))
  17.576 +        < inverse (fact (Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))))"
  17.577          by (simp add: inverse_eq_divide less_divide_eq)
  17.578      }
  17.579      note *** = this
  17.580 @@ -2890,9 +2899,9 @@
  17.581      from ** show ?thesis by (rule sumr_pos_lt_pair)
  17.582        (simp add: divide_inverse mult.assoc [symmetric] ***)
  17.583    qed
  17.584 -  ultimately have "0 < (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  17.585 +  ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  17.586      by (rule order_less_trans)
  17.587 -  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1) ^ n * 2 ^ (2 * n) / real (fact (2 * n))))"
  17.588 +  moreover from * have "- cos 2 = (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
  17.589      by (rule sums_unique)
  17.590    ultimately have "(0::real) < - cos 2" by simp
  17.591    then show ?thesis by simp
    18.1 --- a/src/HOL/ex/Birthday_Paradox.thy	Tue Mar 10 16:12:35 2015 +0000
    18.2 +++ b/src/HOL/ex/Birthday_Paradox.thy	Mon Mar 16 15:30:00 2015 +0000
    18.3 @@ -51,7 +51,7 @@
    18.4      using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
    18.5      by (simp add: fact_mod)
    18.6    also have "... = fact (card T) div fact (card T - card (insert x S))"
    18.7 -    using insert by (simp add: fact_reduce_nat[of "card T"])
    18.8 +    using insert by (simp add: fact_reduce[of "card T"])
    18.9    finally show ?case .
   18.10  qed
   18.11