src/HOL/Transcendental.thy

 
 lemma sumr_diff_mult_const2: "sum f {..<n} - of_nat n * r = (\<Sum>i<n. f i - r)"
   for r :: "'a::ring_1"
   by (simp add: sum_subtractf)
 
-lemma lemma_realpow_rev_sumr:
-  "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) = (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
-  by (subst sum.nat_diff_reindex[symmetric]) simp
-
 lemma lemma_termdiff2:
   fixes h :: "'a::field"
   assumes h: "h \<noteq> 0"
   shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
          h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
     (is "?lhs = ?rhs")
 proof (cases n)
-  case (Suc n)
+  case (Suc m)
   have 0: "\<And>x k. (\<Sum>n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
                  (\<Sum>j<Suc k.  h * ((h + z) ^ j * z ^ (x + k - j)))"
-    apply (rule sum.cong [OF refl])
-    by (simp add: power_add [symmetric] mult.commute)
-  have *: "(\<Sum>i<n. z ^ i * ((z + h) ^ (n - i) - z ^ (n - i))) =
-           (\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
-    apply (rule sum.cong [OF refl])
-    apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
-        simp del: sum.lessThan_Suc power_Suc)
-    done
-  have "h * ?lhs = h * ?rhs"
-    apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
-    using Suc
-    apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
+    by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong)
+  have *: "(\<Sum>i<m. z ^ i * ((z + h) ^ (m - i) - z ^ (m - i))) =
+           (\<Sum>i<m. \<Sum>j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))"
+    by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
+        simp del: sum.lessThan_Suc power_Suc intro: sum.cong)
+  have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)"
+    by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
+  also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ p * z ^ (m - p)) - of_nat (Suc m) * z ^ m)"
+    by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
         del: power_Suc sum.lessThan_Suc of_nat_Suc)
-    apply (subst lemma_realpow_rev_sumr)
-    apply (subst sumr_diff_mult_const2)
-    apply (simp add: lemma_termdiff1 sum_distrib_left *)
-    done
+  also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ (m - p) * z ^ p) - of_nat (Suc m) * z ^ m)"
+    by (subst sum.nat_diff_reindex[symmetric]) simp
+  also have "... = h * (\<Sum>i<Suc m. (z + h) ^ (m - i) * z ^ i - z ^ m)"
+    by (simp add: sum_subtractf)
+  also have "... = h * ?rhs"
+    by (simp add: lemma_termdiff1 sum_distrib_left Suc *)
+  finally have "h * ?lhs = h * ?rhs" .
   then show ?thesis
     by (simp add: h)
 qed auto
 
 
 lemma real_sum_nat_ivl_bounded2:
   fixes K :: "'a::linordered_semidom"
-  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
-    and K: "0 \<le> K"
+  assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" and K: "0 \<le> K"
   shows "sum f {..<n-k} \<le> of_nat n * K"
-  apply (rule order_trans [OF sum_mono [OF f]])
-  apply (auto simp: mult_right_mono K)
-  done
+proof -
+  have "sum f {..<n-k} \<le> (\<Sum>i<n - k. K)"
+    by (rule sum_mono [OF f]) auto
+  also have "... \<le> of_nat n * K"
+    by (auto simp: mult_right_mono K)
+  finally show ?thesis .
+qed
 
 lemma lemma_termdiff3:
   fixes h z :: "'a::real_normed_field"
   assumes 1: "h \<noteq> 0"
     and 2: "norm z \<le> K"

     by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult.commute norm_mult)
   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   proof (rule mult_right_mono [OF _ norm_ge_zero])
     from norm_ge_zero 2 have K: "0 \<le> K"
       by (rule order_trans)
-    have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
-      apply (erule subst)
-      apply (simp only: norm_mult norm_power power_add)
-      apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
-      done
+    have le_Kn: "norm ((z + h) ^ i * z ^ j) \<le> K ^ n" if "i + j = n" for i j n
+    proof -
+      have "norm (z + h) ^ i * norm z ^ j \<le> K ^ i * K ^ j"
+        by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
+      also have "... = K^n"
+        by (metis power_add that)
+      finally show ?thesis
+        by (simp add: norm_mult norm_power) 
+    qed
+    then have "\<And>p q.
+       \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)"
+      by simp
+    then
     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) \<le>
         of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
-      apply (intro
-          order_trans [OF norm_sum]
-          real_sum_nat_ivl_bounded2
-          mult_nonneg_nonneg
-          of_nat_0_le_iff
-          zero_le_power K)
-      apply (rule le_Kn, simp)
-      done
+      by (intro order_trans [OF norm_sum]
+          real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K)
   qed
   also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
     by (simp only: mult.assoc)
   finally show ?thesis .
 qed

     then have "summable (\<lambda>n. diffs (diffs (\<lambda>n. norm (c n))) n * r ^ n)"
       using r by (simp add: diffs_def norm_mult norm_power del: of_nat_Suc)
     then have "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
-      (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
-      apply (rule ext)
-      apply (case_tac n)
-      apply (simp_all add: diffs_def r_neq_0)
-      done
+               (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
+      by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split)
     finally have "summable
       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
       by (rule diffs_equiv [THEN sums_summable])
     also have
       "(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
        (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
-      apply (rule ext)
-      apply (case_tac n, simp)
-      apply (rename_tac nat)
-      apply (case_tac nat, simp)
-      apply (simp add: r_neq_0)
-      done
+      by (rule ext) (simp add: r_neq_0 split: nat_diff_split)
     finally show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
   next
-    fix h :: 'a
-    fix n :: nat
+    fix h :: 'a and n
     assume h: "h \<noteq> 0"
     assume "norm h < r - norm x"
     then have "norm x + norm h < r" by simp
-    with norm_triangle_ineq have xh: "norm (x + h) < r"
+    with norm_triangle_ineq 
+    have xh: "norm (x + h) < r"
       by (rule order_le_less_trans)
-    show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
+    have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))
+    \<le> real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))"
+      by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh)
+    then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
       norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
-      apply (simp only: norm_mult mult.assoc)
-      apply (rule mult_left_mono [OF _ norm_ge_zero])
-      apply (simp add: mult.assoc [symmetric])
-      apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
-      done
+      by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero])
   qed
 qed
 
 lemma termdiffs:
   fixes K x :: "'a::{real_normed_field,banach}"

   fixes K x :: "'a::{real_normed_field,banach}"
   assumes sm: "summable (\<lambda>n. c n * K ^ n)"
     and K: "norm x < norm K"
   shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
 proof -
-  have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
-    using K
-    apply (auto simp: norm_divide field_simps)
-    apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
-     apply (auto simp: mult_2_right norm_triangle_mono)
-    done
+  have "norm K + norm x < norm K + norm K"
+    using K by force
+  then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
+    by (auto simp: norm_triangle_lt norm_divide field_simps)
   then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
     by simp
   have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
     by (metis K2 summable_norm_cancel [OF powser_insidea [OF sm]] add.commute of_real_add)
   moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs c n * x ^ n)"
     by (blast intro: sm termdiff_converges powser_inside)
   moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
     by (blast intro: sm termdiff_converges powser_inside)
   ultimately show ?thesis
-    apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
-    using K
-      apply (auto simp: field_simps)
-    apply (simp flip: of_real_add)
-    done
+    by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+       (use K in \<open>auto simp: field_simps simp flip: of_real_add\<close>)
 qed
 
 lemma termdiffs_strong_converges_everywhere:
   fixes K x :: "'a::{real_normed_field,banach}"
   assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)"

     by (rule termdiffs_strong) (use s in \<open>auto simp: norm_divide\<close>)
   then have "isCont (\<lambda>x. \<Sum>n. a n * x ^ n) 0"
     by (blast intro: DERIV_continuous)
   then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)"
     by (simp add: continuous_within)
-  then show ?thesis
-    apply (rule Lim_transform)
+  moreover have "(\<lambda>x. f x - (\<Sum>n. a n * x ^ n)) \<midarrow>0\<rightarrow> 0"
     apply (clarsimp simp: LIM_eq)
     apply (rule_tac x=s in exI)
     using s sm sums_unique by fastforce
+  ultimately show ?thesis
+    by (rule Lim_transform)
 qed
 
 lemma powser_limit_0_strong:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
   assumes s: "0 < s"

   shows "(f \<longlongrightarrow> a 0) (at 0)"
 proof -
   have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
     by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
   show ?thesis
-    apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
-     apply (simp_all add: *)
-    done
+    by (simp add: * LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
 qed
 
 
 subsection \<open>Derivability of power series\<close>
 

 proof
   assume "0 < x"
   have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
     by (auto simp: numeral_2_eq_2)
   also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
-    apply (rule sum_le_suminf [OF summable_exp])
-    using \<open>0 < x\<close>
-    apply (auto  simp add: zero_le_mult_iff)
-    done
+  proof (rule sum_le_suminf [OF summable_exp])
+    show "\<forall>m\<in>- {..<2}. 0 \<le> inverse (fact m) * x ^ m"
+      using \<open>0 < x\<close> by (auto  simp add: zero_le_mult_iff)
+  qed auto
   finally show "1 + x \<le> exp x"
     by (simp add: exp_def)
 qed auto
 
 lemma exp_gt_one: "0 < x \<Longrightarrow> 1 < exp x"

 lemma exp_ge_add_one_self [simp]: "1 + x \<le> exp x"
   for x :: real
 proof (cases "0 \<le> x \<or> x \<le> -1")
   case True
   then show ?thesis
-    apply (rule disjE)
-     apply (simp add: exp_ge_add_one_self_aux)
-    using exp_ge_zero order_trans real_add_le_0_iff by blast
+    by (meson exp_ge_add_one_self_aux exp_ge_zero order.trans real_add_le_0_iff)
 next
   case False
   then have ln1: "ln (1 + x) \<le> x"
     using ln_one_minus_pos_upper_bound [of "-x"] by simp
   have "1 + x = exp (ln (1 + x))"

   by (simp add: powr_def)
 
 lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
   using powr_ge_pzero[of a x] by arith
 
+lemma inverse_powr: "\<And>y::real. 0 \<le> y \<Longrightarrow> inverse y powr a = inverse (y powr a)"
+    by (simp add: exp_minus ln_inverse powr_def)
+
 lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
   for a b x :: real
-  apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
-  apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
-  done
+    by (simp add: divide_inverse powr_mult inverse_powr)
 
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
   for a b x :: "'a::{ln,real_normed_field}"
   by (simp add: powr_def exp_add [symmetric] distrib_right)
 

   unfolding cos_coeff_def sin_coeff_def
   by (simp del: mult_Suc) (auto elim: oddE)
 
 lemma summable_norm_sin: "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
   for x :: "'a::{real_normed_algebra_1,banach}"
-  unfolding sin_coeff_def
-  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
-  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
-  done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+  show "\<exists>N. \<forall>n\<ge>N. norm (norm (sin_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+    unfolding sin_coeff_def
+    by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
 
 lemma summable_norm_cos: "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
   for x :: "'a::{real_normed_algebra_1,banach}"
-  unfolding cos_coeff_def
-  apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
-  apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
-  done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+  show "\<exists>N. \<forall>n\<ge>N. norm (norm (cos_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+    unfolding cos_coeff_def
+    by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
+
 
 lemma sin_converges: "(\<lambda>n. sin_coeff n *\<^sub>R x^n) sums sin x"
   unfolding sin_def
   by (metis (full_types) summable_norm_cancel summable_norm_sin summable_sums)
 

   qed
   also have "\<dots> sums (sin (of_real x))"
     by (rule sin_converges)
   finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
   then show ?thesis
-    using sums_unique2 sums_of_real [OF sin_converges]
-    by blast
+    using sums_unique2 sums_of_real [OF sin_converges] by blast
 qed
 
 corollary sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
   by (metis Reals_cases Reals_of_real sin_of_real)
 

   by (rule DERIV_cos [THEN DERIV_isCont])
 
 lemma continuous_on_cos_real: "continuous_on {a..b} cos" for a::real
   using continuous_at_imp_continuous_on isCont_cos by blast
 
+
+context
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::{real_normed_field,banach}"
+begin
+
 lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_o2 [OF _ isCont_sin])
 
-(* FIXME a context for f would be better *)
-
 lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_o2 [OF _ isCont_cos])
 
 lemma tendsto_sin [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) \<longlongrightarrow> sin a) F"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_tendsto_compose [OF isCont_sin])
 
 lemma tendsto_cos [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) \<longlongrightarrow> cos a) F"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   by (rule isCont_tendsto_compose [OF isCont_cos])
 
 lemma continuous_sin [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   unfolding continuous_def by (rule tendsto_sin)
 
 lemma continuous_on_sin [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
   unfolding continuous_on_def by (auto intro: tendsto_sin)
+
+lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
+  unfolding continuous_def by (rule tendsto_cos)
+
+lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_cos)
+
+end
 
 lemma continuous_within_sin: "continuous (at z within s) sin"     
   for z :: "'a::{real_normed_field,banach}"
   by (simp add: continuous_within tendsto_sin)
 
-lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
-  unfolding continuous_def by (rule tendsto_cos)
-
-lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
-  for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
-  unfolding continuous_on_def by (auto intro: tendsto_cos)
-
 lemma continuous_within_cos: "continuous (at z within s) cos"
   for z :: "'a::{real_normed_field,banach}"
   by (simp add: continuous_within tendsto_cos)
 
 

 
 lemma cos_zero [simp]: "cos 0 = 1"
   by (simp add: cos_def cos_coeff_def scaleR_conv_of_real)
 
 lemma DERIV_fun_sin: "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. sin (g x)) x :> cos (g x) * m"
-  by (auto intro!: derivative_intros)
+  by (fact derivative_intros)
 
 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)
+  by (fact derivative_intros)
 
 
 subsection \<open>Deriving the Addition Formulas\<close>
 
 text \<open>The product of two cosine series.\<close>

     if "n \<le> p" for n p :: nat
   proof -
     have "(-1) ^ ((n - Suc 0) div 2) * (-1) ^ ((p - Suc n) div 2) = - ((-1 :: real) ^ (p div 2))"
       if np: "odd n" "even p"
     proof -
+      have "p > 0"
+        using \<open>n \<le> p\<close> neq0_conv that(1) by blast
+      then have \<section>: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))"
+        using \<open>even p\<close> by (auto simp add: dvd_def power_eq_if)
       from \<open>n \<le> p\<close> np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
         by arith+
       have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
         by simp
-      with \<open>n \<le> p\<close> np * show ?thesis
-        apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add)
-        apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus
-            mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
-        done
+      with \<open>n \<le> p\<close> np  \<section> * show ?thesis
+        by (simp add: flip: div_add power_add)
     qed
     then show ?thesis
       using \<open>n\<le>p\<close> by (auto simp: algebra_simps sin_coeff_def binomial_fact)
   qed
   then have "(\<lambda>p. \<Sum>n\<le>p. if even p \<and> odd n

   by (simp add: cos_double)
 
 lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
   by (simp add: sin_double)
 
+context
+  fixes w :: "'a::{real_normed_field,banach}"
+
+begin
+
 lemma sin_times_sin: "sin w * sin z = (cos (w - z) - cos (w + z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: cos_diff cos_add)
 
 lemma sin_times_cos: "sin w * cos z = (sin (w + z) + sin (w - z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: sin_diff sin_add)
 
 lemma cos_times_sin: "cos w * sin z = (sin (w + z) - sin (w - z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: sin_diff sin_add)
 
 lemma cos_times_cos: "cos w * cos z = (cos (w - z) + cos (w + z)) / 2"
-  for w :: "'a::{real_normed_field,banach}"
   by (simp add: cos_diff cos_add)
+
+lemma cos_double_cos: "cos (2 * w) = 2 * cos w ^ 2 - 1"
+  by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin: "cos (2 * w) = 1 - 2 * sin w ^ 2"
+  by (simp add: cos_double sin_squared_eq)
+
+end
 
 lemma sin_plus_sin: "sin w + sin z = 2 * sin ((w + z) / 2) * cos ((w - z) / 2)"
   for w :: "'a::{real_normed_field,banach}" 
   apply (simp add: mult.assoc sin_times_cos)
   apply (simp add: field_simps)

 lemma cos_diff_cos: "cos w - cos z = 2 * sin ((w + z) / 2) * sin ((z - w) / 2)"
   for w :: "'a::{real_normed_field,banach,field}"
   apply (simp add: mult.assoc sin_times_sin)
   apply (simp add: field_simps)
   done
-
-lemma cos_double_cos: "cos (2 * z) = 2 * cos z ^ 2 - 1"
-  for z :: "'a::{real_normed_field,banach}"
-  by (simp add: cos_double sin_squared_eq)
-
-lemma cos_double_sin: "cos (2 * z) = 1 - 2 * sin z ^ 2"
-  for z :: "'a::{real_normed_field,banach}"
-  by (simp add: cos_double sin_squared_eq)
 
 lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
   by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
 
 lemma cos_pi_minus [simp]: "cos (pi - x) = - (cos x)"

   qed (use x in auto)
 qed
 
 lemma cos_zero_lemma:
   assumes "0 \<le> x" "cos x = 0"
-  shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2) \<and> n > 0"
+  shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2)"
 proof -
   have xle: "x < (1 + real_of_int \<lfloor>x/pi\<rfloor>) * pi"
     using floor_correct [of "x/pi"]
     by (simp add: add.commute divide_less_eq)
   obtain n where "real n * pi \<le> x" "x < real (Suc n) * pi"

     using pi_half_ge_zero uniq by fastforce
   ultimately show ?thesis
     by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps)
 qed
 
-lemma sin_zero_lemma: "0 \<le> x \<Longrightarrow> sin x = 0 \<Longrightarrow> \<exists>n::nat. even n \<and> x = real n * (pi/2)"
-  using cos_zero_lemma [of "x + pi/2"]
-  apply (clarsimp simp add: cos_add)
-  apply (rule_tac x = "n - 1" in exI)
-  apply (simp add: algebra_simps of_nat_diff)
-  done
+lemma sin_zero_lemma:
+  assumes "0 \<le> x" "sin x = 0"
+  shows "\<exists>n::nat. even n \<and> x = real n * (pi/2)"
+proof -
+  obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0"
+    using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add)
+  then have "x = real (n - 1) * (pi / 2)"
+    by (simp add: algebra_simps of_nat_diff)
+  then show ?thesis
+    by (simp add: \<open>odd n\<close>)
+qed
 
 lemma cos_zero_iff:
   "cos x = 0 \<longleftrightarrow> ((\<exists>n. odd n \<and> x = real n * (pi/2)) \<or> (\<exists>n. odd n \<and> x = - (real n * (pi/2))))"
   (is "?lhs = ?rhs")
 proof -

 proof
   show "x = 0" if "sin x = 0"
     using that assms by (auto simp: sin_zero_iff)
 qed auto
 
-lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
+lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>i. odd i \<and> x = of_int i * (pi/2))"
 proof -
   have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"
     by (metis even_of_nat of_int_of_nat_eq)
   have 2: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> - (real n * pi) = real_of_int i * pi"
     by (metis even_minus even_of_nat mult.commute mult_minus_right of_int_minus of_int_of_nat_eq)

     by (cases i rule: int_cases2) auto
   show ?thesis
     by (force simp: cos_zero_iff intro!: 1 2 3)
 qed
 
-lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>n. even n \<and> x = of_int n * (pi/2))"
+lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = of_int i * (pi/2))" (is "?lhs = ?rhs")
 proof safe
-  assume "sin x = 0"
+  assume ?lhs
+  then consider (plus) n where "even n" "x = real n * (pi/2)" | (minus) n where "even n"  "x = - (real n * (pi/2))"
+    using sin_zero_iff by auto
   then show "\<exists>n. even n \<and> x = of_int n * (pi/2)"
-    apply (simp add: sin_zero_iff, safe)
-     apply (metis even_of_nat of_int_of_nat_eq)
-    apply (rule_tac x="- (int n)" in exI)
-    apply simp
-    done
+  proof cases
+    case plus
+    then show ?rhs
+      by (metis even_of_nat of_int_of_nat_eq)
+  next
+    case minus
+    then show ?thesis
+      by (rule_tac x="- (int n)" in exI) simp
+  qed
 next
   fix i :: int
   assume "even i"
   then show "sin (of_int i * (pi/2)) = 0"
     by (cases i rule: int_cases2, simp_all add: sin_zero_iff)
 qed
 
-lemma sin_zero_iff_int2: "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)
-  using dvd_triv_left apply fastforce
-  done
+lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>i::int. x = of_int i * pi)"
+proof -
+  have "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = real_of_int i * (pi / 2))"
+    by (auto simp: sin_zero_iff_int)
+  also have "... = (\<exists>j. x = real_of_int (2*j) * (pi / 2))"
+    using dvd_triv_left by blast
+  also have "... = (\<exists>i::int. x = of_int i * pi)"
+    by auto
+  finally show ?thesis .
+qed
 
 lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
   by (simp add: sin_zero_iff_int2)
 
 lemma cos_monotone_0_pi:

   shows "sin y \<le> sin x"
   by (metis assms le_less sin_monotone_2pi)
 
 lemma sin_x_le_x:
   fixes x :: real
-  assumes x: "x \<ge> 0"
+  assumes "x \<ge> 0"
   shows "sin x \<le> x"
 proof -
   let ?f = "\<lambda>x. x - sin x"
-  from x have "?f x \<ge> ?f 0"
-    apply (rule DERIV_nonneg_imp_nondecreasing)
-    apply (intro allI impI exI[of _ "1 - cos x" for x])
-    apply (auto intro!: derivative_eq_intros simp: field_simps)
-    done
+  have "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 - cos u) (at u)"
+    by (auto intro!: derivative_eq_intros simp: field_simps)
+  then have "?f x \<ge> ?f 0"
+    by (metis cos_le_one diff_ge_0_iff_ge DERIV_nonneg_imp_nondecreasing [OF assms])
   then show "sin x \<le> x" by simp
 qed
 
 lemma sin_x_ge_neg_x:
   fixes x :: real
   assumes x: "x \<ge> 0"
   shows "sin x \<ge> - x"
 proof -
   let ?f = "\<lambda>x. x + sin x"
-  from x have "?f x \<ge> ?f 0"
-    apply (rule DERIV_nonneg_imp_nondecreasing)
-    apply (intro allI impI exI[of _ "1 + cos x" for x])
-    apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
-    done
+  have \<section>: "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 + cos u) (at u)"
+    by (auto intro!: derivative_eq_intros simp: field_simps)
+  have "?f x \<ge> ?f 0"
+    by (rule DERIV_nonneg_imp_nondecreasing [OF assms]) (use \<section> real_0_le_add_iff in force)
   then show "sin x \<ge> -x" by simp
 qed
 
 lemma abs_sin_x_le_abs_x: "\<bar>sin x\<bar> \<le> \<bar>x\<bar>"
   for x :: real

   have *: "(sin x * (sin x * 3)) = 3 - (cos x * (cos x * 3))"
     by (simp add: mult.assoc [symmetric] sin_squared_eq [unfolded power2_eq_square])
   have "cos(3 * x) = cos(2*x + x)"
     by simp
   also have "\<dots> = 4 * cos x ^ 3 - 3 * cos x"
-    apply (simp only: cos_add cos_double sin_double)
-    apply (simp add: * field_simps power2_eq_square power3_eq_cube)
-    done
+    unfolding cos_add cos_double sin_double
+    by (simp add: * field_simps power2_eq_square power3_eq_cube)
   finally show ?thesis .
 qed
 
 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
 proof -

 
 lemma sin_int_2pin [simp]: "sin ((2 * pi) * of_int n) = 0"
   by (metis Ints_of_int 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))"])
-  apply (auto simp: field_simps frac_lt_1)
-   apply (simp_all add: frac_def field_simps)
-   apply (simp_all add: add_divide_distrib diff_divide_distrib)
-   apply (simp_all add: sin_add cos_add mult.assoc [symmetric])
-  done
+proof -
+  define y where "y \<equiv> pi - (2 * pi) * frac ((pi - x) / (2 * pi))"
+  have "-pi < y"" y \<le> pi"
+    by (auto simp: field_simps frac_lt_1 y_def)
+  moreover
+  have "sin y = sin x" "cos y = cos x"
+    unfolding y_def
+     apply (simp_all add: frac_def divide_simps sin_add cos_add)
+    by (metis sin_int_2pin cos_int_2pin diff_zero add.right_neutral mult.commute mult.left_neutral mult_zero_left)+
+  ultimately
+  show ?thesis by metis
+qed
 
 
 subsection \<open>Tangent\<close>
 
 definition tan :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"

   show "- sqrt (1 - x\<^sup>2) \<noteq> 0"
     using abs_square_eq_1 assms by force
 qed (use assms isCont_arccos in auto)
 
 lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
-proof (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
-  show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
-    apply (rule derivative_eq_intros | simp)+
+proof (rule DERIV_inverse_function)
+  have "inverse ((cos (arctan x))\<^sup>2) = 1 + x\<^sup>2"
     by (metis arctan cos_arctan_not_zero power_inverse tan_sec)
+  then show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
+    by (auto intro!: derivative_eq_intros)
   show "\<And>y. \<lbrakk>x - 1 < y; y < x + 1\<rbrakk> \<Longrightarrow> tan (arctan y) = y"
     using tan_arctan by blast
   show "1 + x\<^sup>2 \<noteq> 0"
     by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
 qed (use isCont_arctan in auto)

 
 lemma arctan_inverse:
   assumes "x \<noteq> 0"
   shows "arctan (1 / x) = sgn x * pi/2 - arctan x"
 proof (rule arctan_unique)
+  have \<section>: "x > 0 \<Longrightarrow> arctan x < pi"
+    using arctan_bounded [of x] by linarith 
   show "- (pi/2) < sgn x * pi/2 - arctan x"
-    using arctan_bounded [of x] assms
-    unfolding sgn_real_def
-    apply (auto simp: arctan algebra_simps)
-    apply (drule zero_less_arctan_iff [THEN iffD2], arith)
-    done
+    using assms by (auto simp: sgn_real_def arctan algebra_simps \<section>)
   show "sgn x * pi/2 - arctan x < pi/2"
     using arctan_bounded [of "- x"] assms
-    unfolding sgn_real_def arctan_minus
-    by (auto simp: algebra_simps)
+    by (auto simp: algebra_simps sgn_real_def arctan_minus)
   show "tan (sgn x * pi/2 - arctan x) = 1 / x"
-    unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
-    unfolding sgn_real_def
+    unfolding tan_inverse [of "arctan x", unfolded tan_arctan] sgn_real_def
     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
 qed
 
 theorem pi_series: "pi / 4 = (\<Sum>k. (-1)^k * 1 / real (k * 2 + 1))"
   (is "_ = ?SUM")

 
 lemma cos_x_y_le_one: "\<bar>x / sqrt (x\<^sup>2 + y\<^sup>2)\<bar> \<le> 1"
   by (rule power2_le_imp_le [OF _ zero_le_one])
     (simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
 
-lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
-
-lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
-
 lemma polar_Ex: "\<exists>r::real. \<exists>a. x = r * cos a \<and> y = r * sin a"
 proof -
-  have polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a \<and> y = r * sin a" for y
-    apply (rule exI [where x = "sqrt (x\<^sup>2 + y\<^sup>2)"])
-    apply (rule exI [where x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))"])
-    apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
-        real_sqrt_mult [symmetric] right_diff_distrib)
-    done
+  have polar_ex1: "\<exists>r a. x = r * cos a \<and> y = r * sin a" if "0 < y" for y
+  proof -
+    have "x = sqrt (x\<^sup>2 + y\<^sup>2) * cos (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+      by (simp add: cos_arccos_abs [OF cos_x_y_le_one])
+    moreover have "y = sqrt (x\<^sup>2 + y\<^sup>2) * sin (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+      using that
+      by (simp add: sin_arccos_abs [OF cos_x_y_le_one] power_divide right_diff_distrib flip: real_sqrt_mult)
+    ultimately show ?thesis
+      by blast
+  qed
   show ?thesis
   proof (cases "0::real" y rule: linorder_cases)
     case less
     then show ?thesis
       by (rule polar_ex1)

 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) =
-    (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-proof -
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+proof -
+  have "\<And>i j. \<lbrakk>m + n - i < j; a i \<noteq> 0\<rbrakk> \<Longrightarrow> b j = 0"
+    by (meson le_add_diff leI le_less_trans m n)
+  then have \<section>: "(\<Sum>(i,j)\<in>(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0"
+    by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
   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))"
     by (rule sum_product)
   also have "\<dots> = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
     using assms by (auto simp: sum_up_index_split)
   also have "\<dots> = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
-    apply (simp add: add_ac sum.Sigma product_atMost_eq_Un)
-    apply (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
-    apply (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE)
-    done
+    by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \<section>)
   also have "\<dots> = (\<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 sum.Sigma)
+  also have "... = (\<Sum>k\<le>m + n. \<Sum>i\<le>k. a i * x ^ i * (b (k - i) * x ^ (k - i)))"
+    by (rule sum.triangle_reindex_eq)
   also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-    apply (subst sum.triangle_reindex_eq)
-    apply (auto simp: algebra_simps sum_distrib_left intro!: sum.cong)
-    apply (metis le_add_diff_inverse power_add)
-    done
+    by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong)
   finally show ?thesis .
 qed
 
 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) =
-    (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+         (\<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 only: of_nat_mult [symmetric] of_nat_power [symmetric]
       of_nat_eq_iff Int.int_sum [symmetric])
 
 lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)

     (x - y) * ((\<Sum>j<n. \<Sum>k<n-j. a(j + k + 1) * y^k * x^j))"
 proof -
   have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
     if "j < n" for j :: nat
   proof -
-    have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
-      apply (auto simp: bij_betw_def inj_on_def)
-      apply (rule_tac x="x + Suc j" in image_eqI, auto)
-      done
+    have "\<And>k. k < n - j \<Longrightarrow> k \<in> (\<lambda>i. i - Suc j) ` {Suc j..n}"
+      by (rule_tac x="k + Suc j" in image_eqI, auto)
+    then have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
+      by (auto simp: bij_betw_def inj_on_def)
     then show ?thesis
       by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
   qed
   then show ?thesis
     by (simp add: polyfun_diff [OF assms] sum_distrib_right)