src/HOL/Transcendental.thy
changeset 61609 77b453bd616f
parent 61552 980dd46a03fb
child 61649 268d88ec9087
--- a/src/HOL/Transcendental.thy	Tue Nov 03 11:20:21 2015 +0100
+++ b/src/HOL/Transcendental.thy	Tue Nov 10 14:18:41 2015 +0000
@@ -11,10 +11,11 @@
 begin
 
 lemma reals_Archimedean4:
-  assumes "0 < y" "0 \<le> x" 
+  assumes "0 < y" "0 \<le> x"
   obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
   using floor_correct [of "x/y"] assms
-  by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"])
+  apply (auto simp: field_simps intro!: that [of "nat (floor (x/y))"])
+by (metis (no_types, hide_lams)  divide_inverse divide_self_if floor_correct mult.left_commute mult.right_neutral mult_eq_0_iff order_refl order_trans real_mult_le_cancel_iff2)
 
 lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
 
@@ -24,11 +25,8 @@
 lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   by (metis of_nat_fact of_real_of_nat_eq)
 
-lemma real_fact_nat [simp]: "real (fact n :: nat) = fact n"
-  by (simp add: real_of_nat_def)
-
-lemma real_fact_int [simp]: "real (fact n :: int) = fact n"
-  by (metis of_int_of_nat_eq of_nat_fact real_of_int_def)
+lemma of_int_fact [simp]: "of_int (fact n :: int) = fact n"
+  by (metis of_int_of_nat_eq of_nat_fact)
 
 lemma norm_fact [simp]:
   "norm (fact n :: 'a :: {real_normed_algebra_1}) = fact n"
@@ -155,26 +153,26 @@
   moreover obtain N where N: "norm x / (1 - norm x) < of_int N"
     using ex_le_of_int
     by (meson ex_less_of_int)
-  ultimately have N0: "N>0" 
+  ultimately have N0: "N>0"
     by auto
-  then have *: "real (N + 1) * norm x / real N < 1"
+  then have *: "real_of_int (N + 1) * norm x / real_of_int N < 1"
     using N assms
     by (auto simp: field_simps)
   { fix n::nat
     assume "N \<le> int n"
-    then have "real N * real_of_nat (Suc n) \<le> real_of_nat n * real (1 + N)"
+    then have "real_of_int N * real_of_nat (Suc n) \<le> real_of_nat n * real_of_int (1 + N)"
       by (simp add: algebra_simps)
-    then have "(real N * real_of_nat (Suc n)) * (norm x * norm (x ^ n))
-               \<le> (real_of_nat n * real (1 + N)) * (norm x * norm (x ^ n))"
+    then have "(real_of_int N * real_of_nat (Suc n)) * (norm x * norm (x ^ n))
+               \<le> (real_of_nat n *  (1 + N)) * (norm x * norm (x ^ n))"
       using N0 mult_mono by fastforce
-    then have "real N * (norm x * (real_of_nat (Suc n) * norm (x ^ n)))
-         \<le> real_of_nat n * (norm x * (real (1 + N) * norm (x ^ n)))"
+    then have "real_of_int N * (norm x * (real_of_nat (Suc n) * norm (x ^ n)))
+         \<le> real_of_nat n * (norm x * ((1 + N) * norm (x ^ n)))"
       by (simp add: algebra_simps)
   } note ** = this
   show ?thesis using *
     apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
-    apply (simp add: N0 norm_mult field_simps ** 
-                del: of_nat_Suc real_of_int_add)
+    apply (simp add: N0 norm_mult field_simps **
+                del: of_nat_Suc of_int_add)
     done
 qed
 
@@ -184,16 +182,6 @@
 using powser_times_n_limit_0 [of "inverse x"]
 by (simp add: norm_divide divide_simps)
 
-lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) ---> (0::'a::real_normed_field)) sequentially"
-  apply (clarsimp simp: lim_sequentially norm_divide dist_norm divide_simps)
-  apply (auto simp: mult_ac dest!: ex_less_of_nat_mult [of _ 1])
-  by (metis le_eq_less_or_eq less_trans linordered_comm_semiring_strict_class.comm_mult_strict_left_mono 
-          of_nat_less_0_iff of_nat_less_iff zero_less_mult_iff zero_less_one)
-
-lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) ---> (0::'a::real_normed_field)) sequentially"
-  using lim_1_over_n
-  by (simp add: inverse_eq_divide)
-
 lemma sum_split_even_odd:
   fixes f :: "nat \<Rightarrow> real"
   shows
@@ -751,7 +739,7 @@
   then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
     using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
     by (simp add: mult.assoc) (auto simp: ac_simps)
-  then show ?thesis 
+  then show ?thesis
     by (simp add: diffs_def)
 qed
 
@@ -798,14 +786,14 @@
   shows   "((\<lambda>x. \<Sum>n. c n * x^n) has_field_derivative (\<Sum>n. diffs c n * x^n)) (at x)"
   using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
   by (force simp del: of_real_add)
-  
+
 lemma isCont_powser:
   fixes K x :: "'a::{real_normed_field,banach}"
   assumes "summable (\<lambda>n. c n * K ^ n)"
   assumes "norm x < norm K"
   shows   "isCont (\<lambda>x. \<Sum>n. c n * x^n) x"
   using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont)
-  
+
 lemmas isCont_powser' = isCont_o2[OF _ isCont_powser]
 
 lemma isCont_powser_converges_everywhere:
@@ -815,7 +803,7 @@
   using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
   by (force intro!: DERIV_isCont simp del: of_real_add)
 
-lemma powser_limit_0: 
+lemma powser_limit_0:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
   assumes s: "0 < s"
       and sm: "\<And>x. norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
@@ -835,16 +823,16 @@
     by (blast intro: DERIV_continuous)
   then have "((\<lambda>x. \<Sum>n. a n * x ^ n) ---> a 0) (at 0)"
     by (simp add: continuous_within powser_zero)
-  then show ?thesis 
+  then show ?thesis
     apply (rule Lim_transform)
     apply (auto simp add: LIM_eq)
     apply (rule_tac x="s" in exI)
-    using s 
+    using s
     apply (auto simp: sm [THEN sums_unique])
     done
 qed
 
-lemma powser_limit_0_strong: 
+lemma powser_limit_0_strong:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
   assumes s: "0 < s"
       and sm: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> (\<lambda>n. a n * x ^ n) sums (f x)"
@@ -906,7 +894,7 @@
       from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def]
       obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
         by auto
-      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound simp del: real_of_nat_Suc)
+      have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound simp del: of_nat_Suc)
       thus "0 < x" unfolding \<open>x = ?s n\<close> .
     qed
   qed auto
@@ -964,9 +952,8 @@
     qed auto
     also have "\<dots> = of_nat (card {..<?N}) * ?r"
       by (rule setsum_constant)
-    also have "\<dots> = real ?N * ?r"
-      unfolding real_eq_of_nat by auto
-    also have "\<dots> = r/3" by (auto simp del: real_of_nat_Suc)
+    also have "\<dots> = real ?N * ?r" by simp
+    also have "\<dots> = r/3" by (auto simp del: of_nat_Suc)
     finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
 
     from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
@@ -1050,9 +1037,10 @@
                 unfolding power_add[symmetric] using \<open>p \<le> n\<close> by auto
             qed
             also have "\<dots> = real (Suc n) * R' ^ n"
-              unfolding setsum_constant card_atLeastLessThan real_of_nat_def by auto
+              unfolding setsum_constant card_atLeastLessThan by auto
             finally show "\<bar>\<Sum>p<Suc n. x ^ p * y ^ (n - p)\<bar> \<le> \<bar>real (Suc n)\<bar> * \<bar>R' ^ n\<bar>"
-              unfolding abs_real_of_nat_cancel abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF \<open>0 < R'\<close>]]] .
+              unfolding  abs_of_nonneg[OF zero_le_power[OF less_imp_le[OF \<open>0 < R'\<close>]]]
+              by linarith
             show "0 \<le> \<bar>f n\<bar> * \<bar>x - y\<bar>"
               unfolding abs_mult[symmetric] by auto
           qed
@@ -1064,7 +1052,7 @@
       {
         fix n
         show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
-          by (auto intro!: derivative_eq_intros simp del: power_Suc simp: real_of_nat_def)
+          by (auto intro!: derivative_eq_intros simp del: power_Suc)
       }
       {
         fix x
@@ -1112,7 +1100,7 @@
 lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z::'a::real_normed_field. pochhammer z n) z"
   by (induction n) (auto intro!: continuous_intros simp: pochhammer_rec')
 
-lemma continuous_on_pochhammer [continuous_intros]: 
+lemma continuous_on_pochhammer [continuous_intros]:
   fixes A :: "'a :: real_normed_field set"
   shows "continuous_on A (\<lambda>z. pochhammer z n)"
   by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
@@ -1133,7 +1121,7 @@
   obtain r :: real where r0: "0 < r" and r1: "r < 1"
     using dense [OF zero_less_one] by fast
   obtain N :: nat where N: "norm x < real N * r"
-    using ex_less_of_nat_mult r0 real_of_nat_def by auto
+    using ex_less_of_nat_mult r0 by auto
   from r1 show ?thesis
   proof (rule summable_ratio_test [rule_format])
     fix n :: nat
@@ -1164,7 +1152,7 @@
     by (simp add: norm_power_ineq)
 qed
 
-lemma summable_exp: 
+lemma summable_exp:
   fixes x :: "'a::{real_normed_field,banach}"
   shows "summable (\<lambda>n. inverse (fact n) * x^n)"
   using summable_exp_generic [where x=x]
@@ -1190,7 +1178,7 @@
   apply (simp del: of_real_add)
   done
 
-declare DERIV_exp[THEN DERIV_chain2, derivative_intros] 
+declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
         DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
 lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
@@ -1279,7 +1267,7 @@
              (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
              (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
     by (simp only: setsum.distrib [symmetric] scaleR_left_distrib [symmetric]
-                   real_of_nat_add [symmetric]) simp
+                   of_nat_add [symmetric]) simp
   also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
     by (simp only: scaleR_right.setsum)
   finally show
@@ -1338,7 +1326,7 @@
     by (induct n) (auto simp add: distrib_left exp_add mult.commute)
 
 corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
-  by (simp add: exp_of_nat_mult real_of_nat_def)
+  by (simp add: exp_of_nat_mult)
 
 lemma exp_setsum: "finite I \<Longrightarrow> exp(setsum f I) = setprod (\<lambda>x. exp(f x)) I"
   by (induction I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
@@ -1480,7 +1468,7 @@
 definition ln_real :: "real \<Rightarrow> real"
   where "ln_real x = (THE u. exp u = x)"
 
-instance 
+instance
 by intro_classes (simp add: ln_real_def)
 
 end
@@ -1488,106 +1476,106 @@
 lemma powr_eq_0_iff [simp]: "w powr z = 0 \<longleftrightarrow> w = 0"
   by (simp add: powr_def)
 
-lemma ln_exp [simp]: 
+lemma ln_exp [simp]:
   fixes x::real shows "ln (exp x) = x"
   by (simp add: ln_real_def)
 
-lemma exp_ln [simp]: 
+lemma exp_ln [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> exp (ln x) = x"
   by (auto dest: exp_total)
 
-lemma exp_ln_iff [simp]: 
+lemma exp_ln_iff [simp]:
   fixes x::real shows "exp (ln x) = x \<longleftrightarrow> 0 < x"
   by (metis exp_gt_zero exp_ln)
 
-lemma ln_unique: 
+lemma ln_unique:
   fixes x::real shows "exp y = x \<Longrightarrow> ln x = y"
   by (erule subst, rule ln_exp)
 
-lemma ln_mult:  
+lemma ln_mult:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   by (rule ln_unique) (simp add: exp_add)
 
-lemma ln_setprod: 
-  fixes f:: "'a => real" 
+lemma ln_setprod:
+  fixes f:: "'a => real"
   shows
     "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i > 0\<rbrakk> \<Longrightarrow> ln(setprod f I) = setsum (\<lambda>x. ln(f x)) I"
   by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
 
-lemma ln_inverse: 
+lemma ln_inverse:
   fixes x::real shows "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   by (rule ln_unique) (simp add: exp_minus)
 
-lemma ln_div: 
+lemma ln_div:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
   by (rule ln_unique) (simp add: exp_diff)
 
 lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   by (rule ln_unique) (simp add: exp_real_of_nat_mult)
 
-lemma ln_less_cancel_iff [simp]: 
+lemma ln_less_cancel_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   by (subst exp_less_cancel_iff [symmetric]) simp
 
-lemma ln_le_cancel_iff [simp]: 
+lemma ln_le_cancel_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
   by (simp add: linorder_not_less [symmetric])
 
-lemma ln_inj_iff [simp]: 
+lemma ln_inj_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   by (simp add: order_eq_iff)
 
-lemma ln_add_one_self_le_self [simp]: 
+lemma ln_add_one_self_le_self [simp]:
   fixes x::real shows "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   apply (rule exp_le_cancel_iff [THEN iffD1])
   apply (simp add: exp_ge_add_one_self_aux)
   done
 
-lemma ln_less_self [simp]: 
+lemma ln_less_self [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> ln x < x"
   by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
 
-lemma ln_ge_zero [simp]: 
+lemma ln_ge_zero [simp]:
   fixes x::real shows "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
   using ln_le_cancel_iff [of 1 x] by simp
 
-lemma ln_ge_zero_imp_ge_one: 
+lemma ln_ge_zero_imp_ge_one:
   fixes x::real shows "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
   using ln_le_cancel_iff [of 1 x] by simp
 
-lemma ln_ge_zero_iff [simp]: 
+lemma ln_ge_zero_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
   using ln_le_cancel_iff [of 1 x] by simp
 
-lemma ln_less_zero_iff [simp]: 
+lemma ln_less_zero_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
   using ln_less_cancel_iff [of x 1] by simp
 
-lemma ln_gt_zero: 
+lemma ln_gt_zero:
   fixes x::real shows "1 < x \<Longrightarrow> 0 < ln x"
   using ln_less_cancel_iff [of 1 x] by simp
 
-lemma ln_gt_zero_imp_gt_one: 
+lemma ln_gt_zero_imp_gt_one:
   fixes x::real shows "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
   using ln_less_cancel_iff [of 1 x] by simp
 
-lemma ln_gt_zero_iff [simp]: 
+lemma ln_gt_zero_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
   using ln_less_cancel_iff [of 1 x] by simp
 
-lemma ln_eq_zero_iff [simp]: 
+lemma ln_eq_zero_iff [simp]:
   fixes x::real shows "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
   using ln_inj_iff [of x 1] by simp
 
-lemma ln_less_zero: 
+lemma ln_less_zero:
   fixes x::real shows "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
   by simp
 
-lemma ln_neg_is_const: 
+lemma ln_neg_is_const:
   fixes x::real shows "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
   by (auto simp add: ln_real_def intro!: arg_cong[where f=The])
 
-lemma isCont_ln: 
+lemma isCont_ln:
   fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
 proof cases
   assume "0 < x"
@@ -1603,7 +1591,7 @@
                 intro!: exI[of _ "\<bar>x\<bar>"])
 qed
 
-lemma tendsto_ln [tendsto_intros]: 
+lemma tendsto_ln [tendsto_intros]:
   fixes a::real shows
   "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
   by (rule isCont_tendsto_compose [OF isCont_ln])
@@ -1709,9 +1697,9 @@
     have "(2::nat) * 2 ^ n \<le> fact (n + 2)"
       by (induct n) simp_all
     hence "real ((2::nat) * 2 ^ n) \<le> real_of_nat (fact (n + 2))"
-      by (simp only: real_of_nat_le_iff)
+      by (simp only: of_nat_le_iff)
     hence "((2::real) * 2 ^ n) \<le> fact (n + 2)"
-      unfolding of_nat_fact real_of_nat_def
+      unfolding of_nat_fact
       by (simp add: of_nat_mult of_nat_power)
     hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
       by (rule le_imp_inverse_le) simp
@@ -1843,7 +1831,7 @@
 qed
 
 lemma ln_one_minus_pos_lower_bound:
-  fixes x::real 
+  fixes x::real
   shows "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
 proof -
   assume a: "0 <= x" and b: "x <= (1 / 2)"
@@ -1973,13 +1961,13 @@
   fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
   using exp_ge_add_one_self[of "ln x"] by simp
 
-corollary ln_diff_le: 
-  fixes x::real 
+corollary ln_diff_le:
+  fixes x::real
   shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x - ln y \<le> (x - y) / y"
   by (simp add: ln_div [symmetric] diff_divide_distrib ln_le_minus_one)
 
 lemma ln_eq_minus_one:
-  fixes x::real 
+  fixes x::real
   assumes "0 < x" "ln x = x - 1"
   shows "x = 1"
 proof -
@@ -2328,7 +2316,7 @@
 lemma le_log_iff:
   assumes "1 < b" "x > 0"
   shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> (x::real)"
-  using assms 
+  using assms
   apply auto
   apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff
                powr_log_cancel zero_less_one)
@@ -2358,10 +2346,10 @@
   by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
 
 lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
-  by (induct n) (simp_all add: ac_simps powr_add real_of_nat_Suc)
+  by (induct n) (simp_all add: ac_simps powr_add of_nat_Suc)
 
 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
-  unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
+  by (metis of_nat_numeral powr_realpow)
 
 lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
 by(simp add: powr_realpow_numeral)
@@ -2517,7 +2505,7 @@
 qed
 
 lemma tendsto_powr [tendsto_intros]:
-  fixes a::real 
+  fixes a::real
   assumes f: "(f ---> a) F" and g: "(g ---> b) F" and a: "a \<noteq> 0"
   shows "((\<lambda>x. f x powr g x) ---> a powr b) F"
   unfolding powr_def
@@ -2561,7 +2549,7 @@
 next
   { assume "a = 0"
     with f f_nonneg have "LIM x inf F (principal {x. f x \<noteq> 0}). f x :> at_right 0"
-      by (auto simp add: filterlim_at eventually_inf_principal le_less 
+      by (auto simp add: filterlim_at eventually_inf_principal le_less
                elim: eventually_elim1 intro: tendsto_mono inf_le1)
     then have "((\<lambda>x. exp (g x * ln (f x))) ---> 0) (inf F (principal {x. f x \<noteq> 0}))"
       by (auto intro!: filterlim_compose[OF exp_at_bot] filterlim_compose[OF ln_at_0]
@@ -2770,10 +2758,10 @@
   by (metis Reals_cases Reals_of_real cos_of_real)
 
 lemma diffs_sin_coeff: "diffs sin_coeff = cos_coeff"
-  by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
+  by (simp add: diffs_def sin_coeff_Suc del: of_nat_Suc)
 
 lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
-  by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
+  by (simp add: diffs_def cos_coeff_Suc del: of_nat_Suc)
 
 text\<open>Now at last we can get the derivatives of exp, sin and cos\<close>
 
@@ -2884,7 +2872,7 @@
 
 lemma DERIV_fun_cos:
      "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. cos(g x)) x :> -sin(g x) * m"
-  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
+  by (auto intro!: derivative_eq_intros)
 
 subsection \<open>Deriving the Addition Formulas\<close>
 
@@ -2903,7 +2891,7 @@
     have "(cos_coeff n * cos_coeff (p - n)) *\<^sub>R (x^n * y^(p-n)) =
           (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)"
     using \<open>n\<le>p\<close>
-      by (auto simp: * algebra_simps cos_coeff_def binomial_fact real_of_nat_def)
+      by (auto simp: * algebra_simps cos_coeff_def binomial_fact)
   }
   then have "(\<lambda>p. \<Sum>n\<le>p. 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) =
@@ -2942,7 +2930,7 @@
           (if even p \<and> odd n
           then -((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0)"
     using \<open>n\<le>p\<close>
-      by (auto simp:  algebra_simps sin_coeff_def binomial_fact real_of_nat_def)
+      by (auto simp:  algebra_simps sin_coeff_def binomial_fact)
   }
   then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n
                then - ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n) else 0) =
@@ -2977,7 +2965,7 @@
                   else 0)"
       by (auto simp: setsum_right_distrib field_simps scaleR_conv_of_real nonzero_of_real_divide)
     also have "... = cos_coeff p *\<^sub>R ((x + y) ^ p)"
-      by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real real_of_nat_def atLeast0AtMost)
+      by (simp add: cos_coeff_def binomial_ring [of x y]  scaleR_conv_of_real atLeast0AtMost)
     finally have "(\<Sum>n\<le>p. if even p
                   then ((-1) ^ (p div 2) * (p choose n) / (fact p)) *\<^sub>R (x^n) * y^(p-n)
                   else 0) = cos_coeff p *\<^sub>R ((x + y) ^ p)" .
@@ -3114,7 +3102,7 @@
 
 lemma DERIV_fun_pow: "DERIV g x :> m ==>
       DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
-  by (auto intro!: derivative_eq_intros simp: real_of_nat_def)
+  by (auto intro!: derivative_eq_intros simp:)
 
 lemma DERIV_fun_exp:
      "DERIV g x :> m ==> DERIV (\<lambda>x. exp(g x)) x :> exp(g x) * m"
@@ -3155,7 +3143,7 @@
     hence "x * x * x * x ^ (n * 4) < ?k2 * ?k3 * x * x ^ (n * 4)"
       by (intro mult_strict_right_mono zero_less_power \<open>0 < x\<close>)
     thus "0 < ?f n"
-      by (simp add: real_of_nat_def divide_simps mult_ac del: mult_Suc)
+      by (simp add: divide_simps mult_ac del: mult_Suc)
 qed
   have sums: "?f sums sin x"
     by (rule sin_paired [THEN sums_group], simp)
@@ -3183,7 +3171,7 @@
 
 lemmas realpow_num_eq_if = power_eq_if
 
-lemma sumr_pos_lt_pair: 
+lemma sumr_pos_lt_pair:
   fixes f :: "nat \<Rightarrow> real"
   shows "\<lbrakk>summable f;
         \<And>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
@@ -3212,13 +3200,12 @@
     { fix d
       let ?six4d = "Suc (Suc (Suc (Suc (Suc (Suc (4 * d))))))"
       have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))"
-        unfolding real_of_nat_mult
-        by (rule mult_strict_mono) (simp_all add: fact_less_mono)
+        unfolding of_nat_mult   by (rule mult_strict_mono) (simp_all add: fact_less_mono)
       then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))"
-        by (simp only: fact.simps(2) [of "Suc (?six4d)"] real_of_nat_def of_nat_mult of_nat_fact)
+        by (simp only: fact.simps(2) [of "Suc (?six4d)"] of_nat_mult of_nat_fact)
       then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))"
         by (simp add: inverse_eq_divide less_divide_eq)
-    } 
+    }
     then show ?thesis
       by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
   qed
@@ -3367,6 +3354,9 @@
 lemma cos_periodic_pi [simp]: "cos (x + pi) = - cos x"
   by (simp add: cos_add)
 
+lemma cos_periodic_pi2 [simp]: "cos (pi + x) = - cos x"
+  by (simp add: cos_add)
+
 lemma sin_periodic [simp]: "sin (x + 2*pi) = sin x"
   by (simp add: sin_add sin_double cos_double)
 
@@ -3374,13 +3364,13 @@
   by (simp add: cos_add sin_double cos_double)
 
 lemma cos_npi [simp]: "cos (real n * pi) = (- 1) ^ n"
-  by (induct n) (auto simp: real_of_nat_Suc distrib_right)
+  by (induct n) (auto simp: distrib_right)
 
 lemma cos_npi2 [simp]: "cos (pi * real n) = (- 1) ^ n"
   by (metis cos_npi mult.commute)
 
 lemma sin_npi [simp]: "sin (real (n::nat) * pi) = 0"
-  by (induct n) (auto simp: real_of_nat_Suc distrib_right)
+  by (induct n) (auto simp: of_nat_Suc distrib_right)
 
 lemma sin_npi2 [simp]: "sin (pi * real (n::nat)) = 0"
   by (simp add: mult.commute [of pi])
@@ -3419,33 +3409,33 @@
   apply (simp add: field_simps)
   done
 
-lemma sin_diff_sin: 
+lemma sin_diff_sin:
   fixes w :: "'a::{real_normed_field,banach,field}"
   shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
   apply (simp add: mult.assoc sin_times_cos)
   apply (simp add: field_simps)
   done
 
-lemma cos_plus_cos: 
+lemma cos_plus_cos:
   fixes w :: "'a::{real_normed_field,banach,field}"
   shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
   apply (simp add: mult.assoc cos_times_cos)
   apply (simp add: field_simps)
   done
 
-lemma cos_diff_cos: 
+lemma cos_diff_cos:
   fixes w :: "'a::{real_normed_field,banach,field}"
   shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
   apply (simp add: mult.assoc sin_times_sin)
   apply (simp add: field_simps)
   done
 
-lemma cos_double_cos: 
+lemma cos_double_cos:
   fixes z :: "'a::{real_normed_field,banach}"
   shows "cos(2 * z) = 2 * cos z ^ 2 - 1"
 by (simp add: cos_double sin_squared_eq)
 
-lemma cos_double_sin: 
+lemma cos_double_sin:
   fixes z :: "'a::{real_normed_field,banach}"
   shows "cos(2 * z) = 1 - 2 * sin z ^ 2"
 by (simp add: cos_double sin_squared_eq)
@@ -3466,7 +3456,7 @@
   by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
 
 lemma cos_2pi_minus [simp]: "cos (2*pi - x) = cos x"
-  by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi 
+  by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi
            diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
 
 lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
@@ -3566,13 +3556,6 @@
     done
 qed
 
-lemma reals_Archimedean4':
-     "\<lbrakk>0 < y; 0 \<le> x\<rbrakk> \<Longrightarrow> \<exists>n. real n * y \<le> x \<and> x < real (Suc n) * y"
-apply (rule_tac x="nat (floor (x/y))" in exI)
-using floor_correct [of "x/y"]
-apply (auto simp: Real.real_of_nat_Suc field_simps)
-done
-
 lemma cos_zero_lemma:
      "\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
       \<exists>n::nat. odd n & x = real n * (pi/2)"
@@ -3580,7 +3563,7 @@
 apply (auto simp: )
 apply (subgoal_tac "0 \<le> x - real n * pi &
                     (x - real n * pi) \<le> pi & (cos (x - real n * pi) = 0) ")
-apply (auto simp: algebra_simps real_of_nat_Suc)
+apply (auto simp: algebra_simps of_nat_Suc)
  prefer 2 apply (simp add: cos_diff)
 apply (simp add: cos_diff)
 apply (subgoal_tac "EX! x. 0 \<le> x & x \<le> pi & cos x = 0")
@@ -3589,7 +3572,7 @@
 apply (drule_tac x = "pi/2" in spec)
 apply (simp add: cos_diff)
 apply (rule_tac x = "Suc (2 * n)" in exI)
-apply (simp add: real_of_nat_Suc algebra_simps, auto)
+apply (simp add: of_nat_Suc algebra_simps, auto)
 done
 
 lemma sin_zero_lemma:
@@ -3597,7 +3580,7 @@
       \<exists>n::nat. even n & x = real n * (pi/2)"
 apply (subgoal_tac "\<exists>n::nat. ~ even n & x + pi/2 = real n * (pi/2) ")
  apply (clarify, rule_tac x = "n - 1" in exI)
- apply (auto elim!: oddE simp add: real_of_nat_Suc field_simps)[1]
+ apply (auto elim!: oddE simp add: of_nat_Suc field_simps)[1]
  apply (rule cos_zero_lemma)
  apply (auto simp: cos_add)
 done
@@ -3611,7 +3594,7 @@
     assume "odd n"
     then obtain m where "n = 2 * m + 1" ..
     then have "cos (real n * pi / 2) = 0"
-      by (simp add: field_simps real_of_nat_Suc) (simp add: cos_add add_divide_distrib)
+      by (simp add: field_simps of_nat_Suc) (simp add: cos_add add_divide_distrib)
   } note * = this
   show ?thesis
   apply (rule iffI)
@@ -3637,18 +3620,18 @@
 
 
 lemma cos_zero_iff_int:
-     "cos x = 0 \<longleftrightarrow> (\<exists>n::int. odd n & x = real n * (pi/2))"
+     "cos x = 0 \<longleftrightarrow> (\<exists>n::int. odd n \<and> x = of_int n * (pi/2))"
 proof safe
   assume "cos x = 0"
-  then show "\<exists>n::int. odd n & x = real n * (pi/2)"
+  then show "\<exists>n::int. odd n & x = of_int n * (pi/2)"
     apply (simp add: cos_zero_iff, safe)
-    apply (metis even_int_iff real_of_int_of_nat_eq)
+    apply (metis even_int_iff of_int_of_nat_eq)
     apply (rule_tac x="- (int n)" in exI, simp)
     done
 next
   fix n::int
   assume "odd n"
-  then show "cos (real n * (pi / 2)) = 0"
+  then show "cos (of_int n * (pi / 2)) = 0"
     apply (simp add: cos_zero_iff)
     apply (case_tac n rule: int_cases2, simp)
     apply (rule disjI2)
@@ -3657,18 +3640,18 @@
 qed
 
 lemma sin_zero_iff_int:
-     "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = real n * (pi/2)))"
+     "sin x = 0 \<longleftrightarrow> (\<exists>n::int. even n & (x = of_int n * (pi/2)))"
 proof safe
   assume "sin x = 0"
-  then show "\<exists>n::int. even n \<and> x = real n * (pi / 2)"
+  then show "\<exists>n::int. even n \<and> x = of_int n * (pi / 2)"
     apply (simp add: sin_zero_iff, safe)
-    apply (metis even_int_iff real_of_int_of_nat_eq)
+    apply (metis even_int_iff of_int_of_nat_eq)
     apply (rule_tac x="- (int n)" in exI, simp)
     done
 next
   fix n::int
   assume "even n"
-  then show "sin (real n * (pi / 2)) = 0"
+  then show "sin (of_int n * (pi / 2)) = 0"
     apply (simp add: sin_zero_iff)
     apply (case_tac n rule: int_cases2, simp)
     apply (rule disjI2)
@@ -3677,13 +3660,11 @@
 qed
 
 lemma sin_zero_iff_int2:
-  "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
+  "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = of_int n * pi)"
   apply (simp only: sin_zero_iff_int)
   apply (safe elim!: evenE)
   apply (simp_all add: field_simps)
-  apply (subst real_numeral(1) [symmetric])
-  apply (simp only: real_of_int_mult [symmetric] real_of_int_inject)
-  apply auto
+  using dvd_triv_left apply fastforce
   done
 
 lemma cos_monotone_0_pi:
@@ -3691,7 +3672,6 @@
   shows "cos x < cos y"
 proof -
   have "- (x - y) < 0" using assms by auto
-
   from MVT2[OF \<open>y < x\<close> DERIV_cos[THEN impI, THEN allI]]
   obtain z where "y < z" and "z < x" and cos_diff: "cos x - cos y = (x - y) * - sin z"
     by auto
@@ -3790,8 +3770,7 @@
   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
     by (auto simp: algebra_simps sin_add)
   thus ?thesis
-    by (simp add: real_of_nat_Suc distrib_right add_divide_distrib
-                  mult.commute [of pi])
+    by (simp add: distrib_right add_divide_distrib add.commute mult.commute [of pi])
 qed
 
 lemma cos_2npi [simp]: "cos (2 * real (n::nat) * pi) = 1"
@@ -3811,7 +3790,7 @@
   done
 
 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
-by (simp only: cos_add sin_add real_of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
+by (simp only: cos_add sin_add of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"
   by (auto intro!: derivative_eq_intros)
@@ -3832,9 +3811,9 @@
   by simp
 
 lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> \<int>"
-  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
-
-lemma cos_one_2pi: 
+  by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_of_int)
+
+lemma cos_one_2pi:
     "cos(x) = 1 \<longleftrightarrow> (\<exists>n::nat. x = n * 2*pi) | (\<exists>n::nat. x = -(n * 2*pi))"
     (is "?lhs = ?rhs")
 proof
@@ -3852,7 +3831,7 @@
     show ?rhs
       using m me n
       by (auto simp: field_simps elim!: evenE)
-  next    
+  next
     fix n::nat
     assume n: "even n" "x = - (real n * (pi/2))"
     then obtain m where m: "n = 2 * m"
@@ -3872,9 +3851,9 @@
 lemma cos_one_2pi_int: "cos(x) = 1 \<longleftrightarrow> (\<exists>n::int. x = n * 2*pi)"
   apply auto  --\<open>FIXME simproc bug\<close>
   apply (auto simp: cos_one_2pi)
-  apply (metis real_of_int_of_nat_eq)
-  apply (metis mult_minus_right real_of_int_minus real_of_int_of_nat_eq)
-  by (metis mult_minus_right of_int_of_nat real_of_int_def real_of_nat_def)
+  apply (metis of_int_of_nat_eq)
+  apply (metis mult_minus_right of_int_minus of_int_of_nat_eq)
+  by (metis mult_minus_right of_int_of_nat )
 
 lemma sin_cos_sqrt: "0 \<le> sin(x) \<Longrightarrow> (sin(x) = sqrt(1 - (cos(x) ^ 2)))"
   using sin_squared_eq real_sqrt_unique by fastforce
@@ -3882,7 +3861,7 @@
 lemma sin_eq_0_pi: "-pi < x \<Longrightarrow> x < pi \<Longrightarrow> sin(x) = 0 \<Longrightarrow> x = 0"
   by (metis sin_gt_zero sin_minus minus_less_iff neg_0_less_iff_less not_less_iff_gr_or_eq)
 
-lemma cos_treble_cos: 
+lemma cos_treble_cos:
   fixes x :: "'a::{real_normed_field,banach}"
   shows "cos(3 * x) = 4 * cos(x) ^ 3 - 3 * cos x"
 proof -
@@ -3948,16 +3927,16 @@
   by (simp add: sin_cos_eq cos_60)
 
 lemma cos_integer_2pi: "n \<in> \<int> \<Longrightarrow> cos(2*pi * n) = 1"
-  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
+  by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute)
 
 lemma sin_integer_2pi: "n \<in> \<int> \<Longrightarrow> sin(2*pi * n) = 0"
   by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
 
-lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"
+lemma cos_int_2npi [simp]: "cos (2 * of_int (n::int) * pi) = 1"
   by (simp add: cos_one_2pi_int)
 
-lemma sin_int_2npi [simp]: "sin (2 * real (n::int) * pi) = 0"
-  by (metis Ints_real_of_int mult.assoc mult.commute sin_integer_2pi)
+lemma sin_int_2npi [simp]: "sin (2 * of_int (n::int) * pi) = 0"
+  by (metis Ints_of_int mult.assoc mult.commute sin_integer_2pi)
 
 lemma sincos_principal_value: "\<exists>y. (-pi < y \<and> y \<le> pi) \<and> (sin(y) = sin(x) \<and> cos(y) = cos(x))"
   apply (rule exI [where x="pi - (2*pi) * frac((pi - x) / (2*pi))"])
@@ -4201,27 +4180,29 @@
 next
   case (Suc n)
   have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi"
-    unfolding Suc_eq_plus1 real_of_nat_add real_of_one distrib_right by auto
+    unfolding Suc_eq_plus1 of_nat_add  distrib_right by auto
   show ?case unfolding split_pi_off using Suc by auto
 qed
 
-lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + real i * pi) = tan x"
+lemma tan_periodic_int[simp]: fixes i :: int shows "tan (x + of_int i * pi) = tan x"
 proof (cases "0 \<le> i")
   case True
-  hence i_nat: "real i = real (nat i)" by auto
-  show ?thesis unfolding i_nat by auto
+  hence i_nat: "of_int i = of_int (nat i)" by auto
+  show ?thesis unfolding i_nat
+    by (metis of_int_of_nat_eq tan_periodic_nat) 
 next
   case False
-  hence i_nat: "real i = - real (nat (-i))" by auto
-  have "tan x = tan (x + real i * pi - real i * pi)"
+  hence i_nat: "of_int i = - of_int (nat (-i))" by auto
+  have "tan x = tan (x + of_int i * pi - of_int i * pi)"
     by auto
-  also have "\<dots> = tan (x + real i * pi)"
-    unfolding i_nat mult_minus_left diff_minus_eq_add by (rule tan_periodic_nat)
+  also have "\<dots> = tan (x + of_int i * pi)"
+    unfolding i_nat mult_minus_left diff_minus_eq_add
+    by (metis of_int_of_nat_eq tan_periodic_nat)    
   finally show ?thesis by auto
 qed
 
 lemma tan_periodic_n[simp]: "tan (x + numeral n * pi) = tan x"
-  using tan_periodic_int[of _ "numeral n" ] unfolding real_numeral .
+  using tan_periodic_int[of _ "numeral n" ] by simp
 
 lemma tan_minus_45: "tan (-(pi/4)) = -1"
   unfolding tan_def by (simp add: sin_45 cos_45)
@@ -4292,7 +4273,7 @@
 
 lemma cot_periodic [simp]: "cot (x + 2*pi) = cot x"
   by (simp add: cot_def)
-  
+
 lemma cot_altdef: "cot x = inverse (tan x)"
   by (simp add: cot_def tan_def)
 
@@ -4494,7 +4475,7 @@
   by (metis arccos_cos cos_pi order_refl pi_ge_zero)
 
 lemma arccos_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos(-x) = pi - arccos x"
-  by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1 
+  by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1
     minus_diff_eq uminus_add_conv_diff)
 
 lemma sin_arccos_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> ~(sin(arccos x) = 0)"
@@ -4746,7 +4727,7 @@
          \<Longrightarrow> (sin(x) \<le> sin(y) \<longleftrightarrow> x \<le> y)"
 by (meson leD le_less_linear sin_monotone_2pi sin_monotone_2pi_le)
 
-lemma sin_inj_pi: 
+lemma sin_inj_pi:
     "\<lbrakk>-(pi/2) \<le> x; x \<le> pi/2;-(pi/2) \<le> y; y \<le> pi/2; sin(x) = sin(y)\<rbrakk> \<Longrightarrow> x = y"
 by (metis arcsin_sin)
 
@@ -4772,24 +4753,24 @@
 proof -
   have x1: "x \<le> 1"
     using assms
-    by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2) 
+    by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2)
   moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
     by (auto simp: arccos)
   moreover have "y = sqrt (1 - x\<^sup>2)" using assms
     by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
-  ultimately show ?thesis using assms arccos_le_pi2 [of x] 
+  ultimately show ?thesis using assms arccos_le_pi2 [of x]
     by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
-qed    
+qed
 
 lemma sincos_total_pi:
   assumes "0 \<le> y" and "x\<^sup>2 + y\<^sup>2 = 1"
     shows "\<exists>t. 0 \<le> t \<and> t \<le> pi \<and> x = cos t \<and> y = sin t"
 proof (cases rule: le_cases [of 0 x])
-  case le from sincos_total_pi_half [OF le]  
+  case le from sincos_total_pi_half [OF le]
   show ?thesis
     by (metis pi_ge_two pi_half_le_two add.commute add_le_cancel_left add_mono assms)
 next
-  case ge 
+  case ge
   then have "0 \<le> -x"
     by simp
   then obtain t where "t\<ge>0" "t \<le> pi/2" "-x = cos t" "y = sin t"
@@ -4798,17 +4779,17 @@
     by (metis \<open>0 \<le> - x\<close> power2_minus)
   then show ?thesis
     by (rule_tac x="pi-t" in exI, auto)
-qed    
-    
+qed
+
 lemma sincos_total_2pi_le:
   assumes "x\<^sup>2 + y\<^sup>2 = 1"
     shows "\<exists>t. 0 \<le> t \<and> t \<le> 2*pi \<and> x = cos t \<and> y = sin t"
 proof (cases rule: le_cases [of 0 y])
-  case le from sincos_total_pi [OF le]  
+  case le from sincos_total_pi [OF le]
   show ?thesis
     by (metis assms le_add_same_cancel1 mult.commute mult_2_right order.trans)
 next
-  case ge 
+  case ge
   then have "0 \<le> -y"
     by simp
   then obtain t where "t\<ge>0" "t \<le> pi" "x = cos t" "-y = sin t"
@@ -4817,7 +4798,7 @@
     by (metis \<open>0 \<le> - y\<close> power2_minus)
   then show ?thesis
     by (rule_tac x="2*pi-t" in exI, auto)
-qed    
+qed
 
 lemma sincos_total_2pi:
   assumes "x\<^sup>2 + y\<^sup>2 = 1"
@@ -4855,7 +4836,7 @@
   done
 
 lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
-  using arccos_less_mono [of y x] 
+  using arccos_less_mono [of y x]
   by (simp add: not_le [symmetric])
 
 lemma arccos_less_arccos: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y < arccos x"
@@ -4934,7 +4915,7 @@
   moreover
   have "\<bar>336/527\<bar> < (1 :: real)" by auto
   from arctan_add[OF less_imp_le[OF 17] this]
-  have "arctan(1/7) + arctan (336/527) = arctan (2879/3353)"  by auto 
+  have "arctan(1/7) + arctan (336/527) = arctan (2879/3353)"  by auto
   ultimately have I: "5 * arctan(1/7) = arctan (2879/3353)"  by auto
   have 379: "\<bar>3/79\<bar> < (1 :: real)" by auto
   with arctan_double
@@ -5272,7 +5253,7 @@
     }
     have "?a 1 ----> 0"
       unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
-      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: real_of_nat_Suc)
+      by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: of_nat_Suc)
     have "?diff 1 ----> 0"
     proof (rule LIMSEQ_I)
       fix r :: real
@@ -5459,7 +5440,7 @@
 lemma polynomial_product: (*with thanks to Chaitanya Mangla*)
   fixes x:: "'a :: idom"
   assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
-  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
+  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
          (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
 proof -
   have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
@@ -5473,19 +5454,19 @@
   also have "... = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
     by (auto simp: pairs_le_eq_Sigma setsum.Sigma)
   also have "... = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-    apply (subst setsum_triangle_reindex_eq)  
+    apply (subst setsum_triangle_reindex_eq)
     apply (auto simp: algebra_simps setsum_right_distrib intro!: setsum.cong)
     by (metis le_add_diff_inverse power_add)
   finally show ?thesis .
 qed
 
-lemma polynomial_product_nat: 
+lemma polynomial_product_nat:
   fixes x:: nat
   assumes m: "\<And>i. i>m \<Longrightarrow> (a i) = 0" and n: "\<And>j. j>n \<Longrightarrow> (b j) = 0"
-  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = 
+  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
          (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
   using polynomial_product [of m a n b x] assms
-  by (simp add: Int.zpower_int Int.zmult_int Int.int_setsum [symmetric])
+  by (simp only: of_nat_mult [symmetric] of_nat_power [symmetric] int_int_eq Int.int_setsum [symmetric])
 
 lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
     fixes x :: "'a::idom"