author wenzelm Sun, 31 Jul 2016 17:25:38 +0200 changeset 63569 7e0b0db5e9ac parent 63568 e63c8f2fbd28 child 63570 1826a90b9cbc
misc tuning and modernization;
 src/HOL/Complex.thy file | annotate | diff | comparison | revisions src/HOL/MacLaurin.thy file | annotate | diff | comparison | revisions src/HOL/Taylor.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Complex.thy	Sat Jul 30 21:10:02 2016 +0200
+++ b/src/HOL/Complex.thy	Sun Jul 31 17:25:38 2016 +0200
@@ -1,7 +1,6 @@
(*  Title:       HOL/Complex.thy
-    Author:      Jacques D. Fleuriot
-    Copyright:   2001 University of Edinburgh
-    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
+    Author:      Jacques D. Fleuriot, 2001 University of Edinburgh
+    Author:      Lawrence C Paulson, 2003/4
*)

section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
@@ -11,9 +10,9 @@
begin

text \<open>
-We use the \<open>codatatype\<close> command to define the type of complex numbers. This allows us to use
-\<open>primcorec\<close> to define complex functions by defining their real and imaginary result
-separately.
+  We use the \<^theory_text>\<open>codatatype\<close> command to define the type of complex numbers. This
+  allows us to use \<^theory_text>\<open>primcorec\<close> to define complex functions by defining their
+  real and imaginary result separately.
\<close>

codatatype complex = Complex (Re: real) (Im: real)
@@ -21,59 +20,68 @@
lemma complex_surj: "Complex (Re z) (Im z) = z"
by (rule complex.collapse)

-lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
+lemma complex_eqI [intro?]: "Re x = Re y \<Longrightarrow> Im x = Im y \<Longrightarrow> x = y"
by (rule complex.expand) simp

lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
by (auto intro: complex.expand)

+

begin

-primcorec zero_complex where
-  "Re 0 = 0"
-| "Im 0 = 0"
+primcorec zero_complex
+  where
+    "Re 0 = 0"
+  | "Im 0 = 0"

-primcorec plus_complex where
-  "Re (x + y) = Re x + Re y"
-| "Im (x + y) = Im x + Im y"
+primcorec plus_complex
+  where
+    "Re (x + y) = Re x + Re y"
+  | "Im (x + y) = Im x + Im y"

-primcorec uminus_complex where
-  "Re (- x) = - Re x"
-| "Im (- x) = - Im x"
+primcorec uminus_complex
+  where
+    "Re (- x) = - Re x"
+  | "Im (- x) = - Im x"

-primcorec minus_complex where
-  "Re (x - y) = Re x - Re y"
-| "Im (x - y) = Im x - Im y"
+primcorec minus_complex
+  where
+    "Re (x - y) = Re x - Re y"
+  | "Im (x - y) = Im x - Im y"

instance
-  by intro_classes (simp_all add: complex_eq_iff)
+  by standard (simp_all add: complex_eq_iff)

end

+
subsection \<open>Multiplication and Division\<close>

instantiation complex :: field
begin

-primcorec one_complex where
-  "Re 1 = 1"
-| "Im 1 = 0"
+primcorec one_complex
+  where
+    "Re 1 = 1"
+  | "Im 1 = 0"

-primcorec times_complex where
-  "Re (x * y) = Re x * Re y - Im x * Im y"
-| "Im (x * y) = Re x * Im y + Im x * Re y"
+primcorec times_complex
+  where
+    "Re (x * y) = Re x * Re y - Im x * Im y"
+  | "Im (x * y) = Re x * Im y + Im x * Re y"

-primcorec inverse_complex where
-  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
-| "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
+primcorec inverse_complex
+  where
+    "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
+  | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"

-definition "x div (y::complex) = x * inverse y"
+definition "x div y = x * inverse y" for x y :: complex

instance
-  by intro_classes
+  by standard
distrib_left distrib_right right_diff_distrib left_diff_distrib
@@ -81,11 +89,11 @@
end

lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"

lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
unfolding divide_complex_def times_complex.sel inverse_complex.sel

lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
@@ -99,14 +107,16 @@
lemma Im_power_real [simp]: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
by (induct n) simp_all

+
subsection \<open>Scalar Multiplication\<close>

instantiation complex :: real_field
begin

-primcorec scaleR_complex where
-  "Re (scaleR r x) = r * Re x"
-| "Im (scaleR r x) = r * Im x"
+primcorec scaleR_complex
+  where
+    "Re (scaleR r x) = r * Re x"
+  | "Im (scaleR r x) = r * Im x"

instance
proof
@@ -127,6 +137,7 @@

end

+
subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>

abbreviation complex_of_real :: "real \<Rightarrow> complex"
@@ -173,14 +184,15 @@
lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc)

-lemma of_real_Re [simp]:
-    "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
+lemma of_real_Re [simp]: "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
by (auto simp: Reals_def)

lemma complex_Re_fact [simp]: "Re (fact n) = fact n"
proof -
-  have "(fact n :: complex) = of_real (fact n)" by simp
-  also have "Re \<dots> = fact n" by (subst Re_complex_of_real) simp_all
+  have "(fact n :: complex) = of_real (fact n)"
+    by simp
+  also have "Re \<dots> = fact n"
+    by (subst Re_complex_of_real) simp_all
finally show ?thesis .
qed

@@ -190,9 +202,10 @@

subsection \<open>The Complex Number $i$\<close>

-primcorec "ii" :: complex  ("\<i>") where
-  "Re ii = 0"
-| "Im ii = 1"
+primcorec "ii" :: complex  ("\<i>")
+  where
+    "Re \<i> = 0"
+  | "Im \<i> = 1"

lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
@@ -203,31 +216,31 @@
lemma fun_complex_eq: "f = (\<lambda>x. Re (f x) + \<i> * Im (f x))"

-lemma i_squared [simp]: "ii * ii = -1"
+lemma i_squared [simp]: "\<i> * \<i> = -1"

-lemma power2_i [simp]: "ii\<^sup>2 = -1"
+lemma power2_i [simp]: "\<i>\<^sup>2 = -1"

-lemma inverse_i [simp]: "inverse ii = - ii"
+lemma inverse_i [simp]: "inverse \<i> = - \<i>"
by (rule inverse_unique) simp

-lemma divide_i [simp]: "x / ii = - ii * x"
+lemma divide_i [simp]: "x / \<i> = - \<i> * x"

-lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
+lemma complex_i_mult_minus [simp]: "\<i> * (\<i> * x) = - x"

-lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
+lemma complex_i_not_zero [simp]: "\<i> \<noteq> 0"

-lemma complex_i_not_one [simp]: "ii \<noteq> 1"
+lemma complex_i_not_one [simp]: "\<i> \<noteq> 1"

-lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
+lemma complex_i_not_numeral [simp]: "\<i> \<noteq> numeral w"

-lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
+lemma complex_i_not_neg_numeral [simp]: "\<i> \<noteq> - numeral w"

lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
@@ -236,18 +249,19 @@
lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
by (metis mult.commute power2_i power_mult)

-lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
+lemma Re_ii_times [simp]: "Re (\<i> * z) = - Im z"
by simp

-lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
+lemma Im_ii_times [simp]: "Im (\<i> * z) = Re z"
by simp

-lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
+lemma ii_times_eq_iff: "\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)"
by auto

-lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
+lemma divide_numeral_i [simp]: "z / (numeral n * \<i>) = - (\<i> * z) / numeral n"
by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)

+
subsection \<open>Vector Norm\<close>

instantiation complex :: real_normed_field
@@ -258,11 +272,9 @@
abbreviation cmod :: "complex \<Rightarrow> real"
where "cmod \<equiv> norm"

-definition complex_sgn_def:
-  "sgn x = x /\<^sub>R cmod x"
+definition complex_sgn_def: "sgn x = x /\<^sub>R cmod x"

-definition dist_complex_def:
-  "dist x y = cmod (x - y)"
+definition dist_complex_def: "dist x y = cmod (x - y)"

definition uniformity_complex_def [code del]:
"(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
@@ -270,23 +282,26 @@
definition open_complex_def [code del]:
"open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"

-instance proof
+instance
+proof
fix r :: real and x y :: complex and S :: "complex set"
show "(norm x = 0) = (x = 0)"
show "norm (x + y) \<le> norm x + norm y"
by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq)
show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
-    by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
+    by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric]
+        real_sqrt_mult)
show "norm (x * y) = norm x * norm y"
-    by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
+    by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric]
+        power2_eq_square algebra_simps)
qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+

end

-declare uniformity_Abort[where 'a=complex, code]
+declare uniformity_Abort[where 'a = complex, code]

-lemma norm_ii [simp]: "norm ii = 1"
+lemma norm_ii [simp]: "norm \<i> = 1"

lemma cmod_unit_one: "cmod (cos a + \<i> * sin a) = 1"
@@ -296,8 +311,7 @@

lemma complex_Re_le_cmod: "Re x \<le> cmod x"
-  unfolding norm_complex_def
-  by (rule real_sqrt_sum_squares_ge1)
+  unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1)

lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
by (rule order_trans [OF _ norm_ge_zero]) simp
@@ -314,7 +328,7 @@
lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
apply (subst complex_eq)
apply (rule order_trans)
-  apply (rule norm_triangle_ineq)
+   apply (rule norm_triangle_ineq)
done

@@ -324,33 +338,31 @@
lemma cmod_eq_Im: "Re z = 0 \<Longrightarrow> cmod z = \<bar>Im z\<bar>"

-lemma cmod_power2: "cmod z ^ 2 = (Re z)^2 + (Im z)^2"
+lemma cmod_power2: "(cmod z)\<^sup>2 = (Re z)\<^sup>2 + (Im z)\<^sup>2"

lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \<le> 0 \<longleftrightarrow> Re z = - cmod z"
using abs_Re_le_cmod[of z] by auto

-lemma cmod_Re_le_iff: "Im x = Im y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> abs (Re x) \<le> abs (Re y)"
+lemma cmod_Re_le_iff: "Im x = Im y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> \<bar>Re x\<bar> \<le> \<bar>Re y\<bar>"

-lemma cmod_Im_le_iff: "Re x = Re y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> abs (Im x) \<le> abs (Im y)"
+lemma cmod_Im_le_iff: "Re x = Re y \<Longrightarrow> cmod x \<le> cmod y \<longleftrightarrow> \<bar>Im x\<bar> \<le> \<bar>Im y\<bar>"
by (metis add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)

lemma Im_eq_0: "\<bar>Re z\<bar> = cmod z \<Longrightarrow> Im z = 0"
-  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2])
+  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) (auto simp add: norm_complex_def)

-lemma abs_sqrt_wlog:
-  fixes x::"'a::linordered_idom"
-  assumes "\<And>x::'a. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)" shows "P \<bar>x\<bar> (x\<^sup>2)"
-by (metis abs_ge_zero assms power2_abs)
+lemma abs_sqrt_wlog: "(\<And>x. x \<ge> 0 \<Longrightarrow> P x (x\<^sup>2)) \<Longrightarrow> P \<bar>x\<bar> (x\<^sup>2)"
+  for x::"'a::linordered_idom"
+  by (metis abs_ge_zero power2_abs)

lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
unfolding norm_complex_def
apply (rule abs_sqrt_wlog [where x="Re z"])
apply (rule abs_sqrt_wlog [where x="Im z"])
apply (rule power2_le_imp_le)
done

lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
@@ -372,10 +384,10 @@
subsection \<open>Completeness of the Complexes\<close>

lemma bounded_linear_Re: "bounded_linear Re"
-  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
+  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)

lemma bounded_linear_Im: "bounded_linear Im"
-  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
+  by (rule bounded_linear_intro [where K=1]) (simp_all add: norm_complex_def)

lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
@@ -404,15 +416,15 @@
unfolding complex.collapse .
qed (auto intro: tendsto_intros)

-lemma continuous_complex_iff: "continuous F f \<longleftrightarrow>
-    continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
-  unfolding continuous_def tendsto_complex_iff ..
+lemma continuous_complex_iff:
+  "continuous F f \<longleftrightarrow> continuous F (\<lambda>x. Re (f x)) \<and> continuous F (\<lambda>x. Im (f x))"
+  by (simp only: continuous_def tendsto_complex_iff)

lemma has_vector_derivative_complex_iff: "(f has_vector_derivative x) F \<longleftrightarrow>
((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
-  unfolding has_vector_derivative_def has_field_derivative_def has_derivative_def tendsto_complex_iff
-  by (simp add: field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
+  by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def
+      tendsto_complex_iff field_simps bounded_linear_scaleR_left bounded_linear_mult_right)

lemma has_field_derivative_Re[derivative_intros]:
"(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"
@@ -426,22 +438,25 @@
proof
fix X :: "nat \<Rightarrow> complex"
assume X: "Cauchy X"
-  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) \<longlonglongrightarrow> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
-    by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
+  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) \<longlonglongrightarrow>
+    Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
+    by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1]
+        Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
then show "convergent X"
unfolding complex.collapse by (rule convergentI)
qed

-declare
-  DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
+declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
+

subsection \<open>Complex Conjugation\<close>

-primcorec cnj :: "complex \<Rightarrow> complex" where
-  "Re (cnj z) = Re z"
-| "Im (cnj z) = - Im z"
+primcorec cnj :: "complex \<Rightarrow> complex"
+  where
+    "Re (cnj z) = Re z"
+  | "Im (cnj z) = - Im z"

-lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
+lemma complex_cnj_cancel_iff [simp]: "cnj x = cnj y \<longleftrightarrow> x = y"

lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
@@ -450,7 +465,7 @@
lemma complex_cnj_zero [simp]: "cnj 0 = 0"

-lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
+lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \<longleftrightarrow> z = 0"

lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
@@ -504,13 +519,13 @@
lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"

-lemma complex_cnj_i [simp]: "cnj ii = - ii"
+lemma complex_cnj_i [simp]: "cnj \<i> = - \<i>"

lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"

-lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
+lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * \<i>"

lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
@@ -529,17 +544,16 @@
by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp

lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"
-  by (induction n arbitrary: z) (simp_all add: pochhammer_rec)
+  by (induct n arbitrary: z) (simp_all add: pochhammer_rec)

lemma bounded_linear_cnj: "bounded_linear cnj"
-  by (rule bounded_linear_intro [where K=1], simp)
+  using complex_cnj_add complex_cnj_scaleR by (rule bounded_linear_intro [where K=1]) simp

lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
-lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
-lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
-lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
-lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
+  and isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
+  and continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
+  and continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
+  and has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]

lemma lim_cnj: "((\<lambda>x. cnj(f x)) \<longlongrightarrow> cnj l) F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)
@@ -548,7 +562,7 @@
by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum)

-subsection\<open>Basic Lemmas\<close>
+subsection \<open>Basic Lemmas\<close>

lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
@@ -557,11 +571,11 @@
by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)

lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
-by (cases z)
-   (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
-         simp del: of_real_power)
+  by (cases z)
+    (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
+      simp del: of_real_power)

-lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)^2"
+lemma complex_div_cnj: "a / b = (a * cnj b) / (norm b)\<^sup>2"
using complex_norm_square by auto

lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
@@ -570,12 +584,12 @@
lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"

-lemma complex_div_gt_0:
-  "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
-proof cases
-  assume "b = 0" then show ?thesis by auto
+lemma complex_div_gt_0: "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
+proof (cases "b = 0")
+  case True
+  then show ?thesis by auto
next
-  assume "b \<noteq> 0"
+  case False
then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2"
then show ?thesis
@@ -586,22 +600,22 @@
and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
using complex_div_gt_0 by auto

-lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+lemma Re_complex_div_ge_0: "Re (a / b) \<ge> 0 \<longleftrightarrow> Re (a * cnj b) \<ge> 0"
by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)

-lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+lemma Im_complex_div_ge_0: "Im (a / b) \<ge> 0 \<longleftrightarrow> Im (a * cnj b) \<ge> 0"
by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)

-lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+lemma Re_complex_div_lt_0: "Re (a / b) < 0 \<longleftrightarrow> Re (a * cnj b) < 0"
by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)

-lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+lemma Im_complex_div_lt_0: "Im (a / b) < 0 \<longleftrightarrow> Im (a * cnj b) < 0"
by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)

-lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+lemma Re_complex_div_le_0: "Re (a / b) \<le> 0 \<longleftrightarrow> Re (a * cnj b) \<le> 0"
by (metis not_le Re_complex_div_gt_0)

-lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+lemma Im_complex_div_le_0: "Im (a / b) \<le> 0 \<longleftrightarrow> Im (a * cnj b) \<le> 0"
by (metis Im_complex_div_gt_0 not_le)

lemma Re_divide_of_real [simp]: "Re (z / of_real r) = Re z / r"
@@ -655,34 +669,37 @@
lemma series_comparison_complex:
fixes f:: "nat \<Rightarrow> 'a::banach"
assumes sg: "summable g"
-     and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
-     and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
+    and "\<And>n. g n \<in> \<real>" "\<And>n. Re (g n) \<ge> 0"
+    and fg: "\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> norm(g n)"
shows "summable f"
proof -
-  have g: "\<And>n. cmod (g n) = Re (g n)" using assms
-    by (metis abs_of_nonneg in_Reals_norm)
+  have g: "\<And>n. cmod (g n) = Re (g n)"
+    using assms by (metis abs_of_nonneg in_Reals_norm)
show ?thesis
apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
using sg
-    apply (auto simp: summable_def)
-    apply (rule_tac x="Re s" in exI)
-    apply (auto simp: g sums_Re)
+     apply (auto simp: summable_def)
+     apply (rule_tac x = "Re s" in exI)
+     apply (auto simp: g sums_Re)
apply (metis fg g)
done
qed

-subsection\<open>Polar Form for Complex Numbers\<close>
+
+subsection \<open>Polar Form for Complex Numbers\<close>

lemma complex_unimodular_polar:
-  assumes "(norm z = 1)"
-  obtains t where "0 \<le> t" "t < 2*pi" "z = Complex (cos t) (sin t)"
-by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)
+  assumes "norm z = 1"
+  obtains t where "0 \<le> t" "t < 2 * pi" "z = Complex (cos t) (sin t)"
+  by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms)
+

subsubsection \<open>$\cos \theta + i \sin \theta$\<close>

-primcorec cis :: "real \<Rightarrow> complex" where
-  "Re (cis a) = cos a"
-| "Im (cis a) = sin a"
+primcorec cis :: "real \<Rightarrow> complex"
+  where
+    "Re (cis a) = cos a"
+  | "Im (cis a) = sin a"

lemma cis_zero [simp]: "cis 0 = 1"
@@ -700,27 +717,28 @@

lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-  by (induct n, simp_all add: of_nat_Suc algebra_simps cis_mult)
+  by (induct n) (simp_all add: algebra_simps cis_mult)

-lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
+lemma cis_inverse [simp]: "inverse (cis a) = cis (- a)"

lemma cis_divide: "cis a / cis b = cis (a - b)"

-lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
+lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"

-lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
+lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"

lemma cis_pi: "cis pi = -1"

+
subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>

-definition rcis :: "real \<Rightarrow> real \<Rightarrow> complex" where
-  "rcis r a = complex_of_real r * cis a"
+definition rcis :: "real \<Rightarrow> real \<Rightarrow> complex"
+  where "rcis r a = complex_of_real r * cis a"

lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
@@ -737,7 +755,7 @@
lemma cis_rcis_eq: "cis a = rcis 1 a"

-lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
+lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1 * r2) (a + b)"

lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
@@ -752,31 +770,37 @@
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
by (simp add: rcis_def power_mult_distrib DeMoivre)

-lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
+lemma rcis_inverse: "inverse(rcis r a) = rcis (1 / r) (- a)"

-lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
+lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1 / r2) (a - b)"
by (simp add: rcis_def cis_divide [symmetric])

+
subsubsection \<open>Complex exponential\<close>

lemma cis_conv_exp: "cis b = exp (\<i> * b)"
proof -
-  { fix n :: nat
+  have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
+      of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
+    for n :: nat
+  proof -
have "\<i> ^ n = fact n *\<^sub>R (cos_coeff n + \<i> * sin_coeff n)"
by (induct n)
-         (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
-    then have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
-        of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
-      by (simp add: field_simps) }
-  then show ?thesis using sin_converges [of b] cos_converges [of b]
+        (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
+    then show ?thesis
+  qed
+  then show ?thesis
+    using sin_converges [of b] cos_converges [of b]
by (auto simp add: cis.ctr exp_def simp del: of_real_mult
-             intro!: sums_unique sums_add sums_mult sums_of_real)
+        intro!: sums_unique sums_add sums_mult sums_of_real)
qed

lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"
-  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
+  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp
+  by (cases z) simp

lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
unfolding exp_eq_polar by simp
@@ -793,25 +817,27 @@
lemma complex_exp_exists: "\<exists>a r. z = complex_of_real r * exp a"
apply (insert rcis_Ex [of z])
apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric])
-  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
+  apply (rule_tac x = "\<i> * complex_of_real a" in exI)
+  apply auto
done

-lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
+lemma exp_pi_i [simp]: "exp (of_real pi * \<i>) = -1"
by (metis cis_conv_exp cis_pi mult.commute)

-lemma exp_pi_i' [simp]: "exp(ii * of_real pi) = -1"
+lemma exp_pi_i' [simp]: "exp (\<i> * of_real pi) = -1"
using cis_conv_exp cis_pi by auto

-lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
+lemma exp_two_pi_i [simp]: "exp (2 * of_real pi * \<i>) = 1"

lemma exp_two_pi_i' [simp]: "exp (\<i> * (of_real pi * 2)) = 1"
by (metis exp_two_pi_i mult.commute)

+
subsubsection \<open>Complex argument\<close>

-definition arg :: "complex \<Rightarrow> real" where
-  "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi))"
+definition arg :: "complex \<Rightarrow> real"
+  where "arg z = (if z = 0 then 0 else (SOME a. sgn z = cis a \<and> - pi < a \<and> a \<le> pi))"

lemma arg_zero: "arg 0 = 0"
@@ -828,41 +854,45 @@
assume a: "sgn z = cis a \<and> - pi < a \<and> a \<le> pi"
from a assms have "- (2*pi) < d \<and> d < 2*pi"
unfolding d_def by simp
-    moreover from a assms have "cos a = cos x" and "sin a = sin x"
+    moreover
+    from a assms have "cos a = cos x" and "sin a = sin x"
-    hence cos: "cos d = 1" unfolding d_def cos_diff by simp
-    moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
+    then have cos: "cos d = 1"
+      by (simp add: d_def cos_diff)
+    moreover from cos have "sin d = 0"
+      by (rule cos_one_sin_zero)
ultimately have "d = 0"
-      unfolding sin_zero_iff
-      by (auto elim!: evenE dest!: less_2_cases)
-    thus "a = x" unfolding d_def by simp
+      by (auto simp: sin_zero_iff elim!: evenE dest!: less_2_cases)
+    then show "a = x"
qed (simp add: assms del: Re_sgn Im_sgn)
with \<open>z \<noteq> 0\<close> show "arg z = x"
-    unfolding arg_def by simp
qed

lemma arg_correct:
-  assumes "z \<noteq> 0" shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
+  assumes "z \<noteq> 0"
+  shows "sgn z = cis (arg z) \<and> -pi < arg z \<and> arg z \<le> pi"
proof (simp add: arg_def assms, rule someI_ex)
-  obtain r a where z: "z = rcis r a" using rcis_Ex by fast
+  obtain r a where z: "z = rcis r a"
+    using rcis_Ex by fast
with assms have "r \<noteq> 0" by auto
define b where "b = (if 0 < r then a else a + pi)"
have b: "sgn z = cis b"
-    unfolding z b_def rcis_def using \<open>r \<noteq> 0\<close>
-    by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
-  have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
-    by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
-  have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
-    by (case_tac x rule: int_diff_cases)
-       (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
+    using \<open>r \<noteq> 0\<close> by (simp add: z b_def rcis_def of_real_def sgn_scaleR sgn_if complex_eq_iff)
+  have cis_2pi_nat: "cis (2 * pi * real_of_nat n) = 1" for n
+    by (induct n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
+  have cis_2pi_int: "cis (2 * pi * real_of_int x) = 1" for x
+    by (cases x rule: int_diff_cases)
+      (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
define c where "c = b - 2 * pi * of_int \<lceil>(b - pi) / (2 * pi)\<rceil>"
have "sgn z = cis c"
-    unfolding b c_def
-    by (simp add: cis_divide [symmetric] cis_2pi_int)
+    by (simp add: b c_def cis_divide [symmetric] cis_2pi_int)
moreover have "- pi < c \<and> c \<le> pi"
using ceiling_correct [of "(b - pi) / (2*pi)"]
by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
-  ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
+  ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi"
+    by fast
qed

lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
@@ -877,11 +907,13 @@
lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
using cis_arg [of y] by (simp add: complex_eq_iff)

+
subsection \<open>Square root of complex numbers\<close>

-primcorec csqrt :: "complex \<Rightarrow> complex" where
-  "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
-| "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"
+primcorec csqrt :: "complex \<Rightarrow> complex"
+  where
+    "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
+  | "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"

lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \<Longrightarrow> Re x \<ge> 0 \<Longrightarrow> csqrt x = sqrt (Re x)"
@@ -902,22 +934,21 @@
by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)

lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
-proof cases
-  assume "Im z = 0" then show ?thesis
+proof (cases "Im z = 0")
+  case True
+  then show ?thesis
using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
by (cases "0::real" "Re z" rule: linorder_cases)
-       (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)
+      (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)
next
-  assume "Im z \<noteq> 0"
-  moreover
-  have "cmod z * cmod z - Re z * Re z = Im z * Im z"
+  case False
+  moreover have "cmod z * cmod z - Re z * Re z = Im z * Im z"
-  moreover
-  have "\<bar>Re z\<bar> \<le> cmod z"
+  moreover have "\<bar>Re z\<bar> \<le> cmod z"
ultimately show ?thesis
by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq
-                  field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
+        field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
qed

lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
@@ -937,15 +968,15 @@
shows "csqrt (b^2) = b"
proof -
have "csqrt (b^2) = b \<or> csqrt (b^2) = - b"
-    unfolding power2_eq_iff[symmetric] by (simp add: power2_csqrt)
moreover have "csqrt (b^2) \<noteq> -b \<or> b = 0"
-    using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff)
+    using csqrt_principal[of "b ^ 2"] assms
+    by (intro disjCI notI) (auto simp: complex_eq_iff)
ultimately show ?thesis
by auto
qed

-lemma csqrt_unique:
-    "w^2 = z \<Longrightarrow> (0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w) \<Longrightarrow> csqrt z = w"
+lemma csqrt_unique: "w\<^sup>2 = z \<Longrightarrow> 0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w \<Longrightarrow> csqrt z = w"
by (auto simp: csqrt_square)

lemma csqrt_minus [simp]:
@@ -964,6 +995,7 @@
finally show ?thesis .
qed

+
text \<open>Legacy theorem names\<close>

lemmas expand_complex_eq = complex_eq_iff
@@ -985,19 +1017,19 @@
and Complex_eq_numeral: "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
and Complex_eq_neg_numeral: "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)"
-    and Complex_eq_i: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
-    and i_mult_Complex: "ii * Complex a b = Complex (- b) a"
-    and Complex_mult_i: "Complex a b * ii = Complex (- b) a"
-    and i_complex_of_real: "ii * complex_of_real r = Complex 0 r"
-    and complex_of_real_i: "complex_of_real r * ii = Complex 0 r"
+    and Complex_eq_i: "Complex x y = \<i> \<longleftrightarrow> x = 0 \<and> y = 1"
+    and i_mult_Complex: "\<i> * Complex a b = Complex (- b) a"
+    and Complex_mult_i: "Complex a b * \<i> = Complex (- b) a"
+    and i_complex_of_real: "\<i> * complex_of_real r = Complex 0 r"
+    and complex_of_real_i: "complex_of_real r * \<i> = Complex 0 r"
and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y"
and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y"
and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
-    and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
+    and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa \<and> y = 0)"
and complex_cn: "cnj (Complex a b) = Complex a (- b)"
-    and Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
-    and Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
+    and Complex_setsum': "setsum (\<lambda>x. Complex (f x) 0) s = Complex (setsum f s) 0"
+    and Complex_setsum: "Complex (setsum f s) 0 = setsum (\<lambda>x. Complex (f x) 0) s"
and complex_of_real_def: "complex_of_real r = Complex r 0"
and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq)
--- a/src/HOL/MacLaurin.thy	Sat Jul 30 21:10:02 2016 +0200
+++ b/src/HOL/MacLaurin.thy	Sun Jul 31 17:25:38 2016 +0200
@@ -1,124 +1,105 @@
-(*  Author      : Jacques D. Fleuriot
-    Copyright   : 2001 University of Edinburgh
-    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
-    Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard Häupler, 2005
+(*  Title:      HOL/MacLaurin.thy
+    Author:     Jacques D. Fleuriot, 2001 University of Edinburgh
+    Author:     Lawrence C Paulson, 2004
+    Author:     Lukas Bulwahn and Bernhard Häupler, 2005
*)

-section\<open>MacLaurin Series\<close>
+section \<open>MacLaurin Series\<close>

theory MacLaurin
imports Transcendental
begin

-subsection\<open>Maclaurin's Theorem with Lagrange Form of Remainder\<close>
+subsection \<open>Maclaurin's Theorem with Lagrange Form of Remainder\<close>

-text\<open>This is a very long, messy proof even now that it's been broken down
-into lemmas.\<close>
+text \<open>This is a very long, messy proof even now that it's been broken down
+  into lemmas.\<close>

lemma Maclaurin_lemma:
-    "0 < h ==>
-     \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) +
-               (B * ((h^n) /(fact n)))"
-by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
+  "0 < h \<Longrightarrow>
+    \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) + (B * ((h^n) /(fact n)))"
+  by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp

-lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
-by arith
+lemma eq_diff_eq': "x = y - z \<longleftrightarrow> y = x + z"
+  for x y z :: real
+  by arith

-lemma fact_diff_Suc:
-  "n < Suc m \<Longrightarrow> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-  by (subst fact_reduce, auto)
+lemma fact_diff_Suc: "n < Suc m \<Longrightarrow> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+  by (subst fact_reduce) auto

lemma Maclaurin_lemma2:
fixes B
-  assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-      and INIT : "n = Suc k"
+  assumes DERIV: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    and INIT: "n = Suc k"
defines "difg \<equiv>
-      (\<lambda>m t::real. diff m t -
-         ((\<Sum>p<n - m. diff (m + p) 0 / (fact p) * t ^ p) + B * (t ^ (n - m) / (fact (n - m)))))"
-        (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
-  shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
+    (\<lambda>m t::real. diff m t -
+      ((\<Sum>p<n - m. diff (m + p) 0 / fact p * t ^ p) + B * (t ^ (n - m) / fact (n - m))))"
+    (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
+  shows "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
proof (rule allI impI)+
-  fix m and t::real
-  assume INIT2: "m < n & 0 \<le> t & t \<le> h"
+  fix m t
+  assume INIT2: "m < n \<and> 0 \<le> t \<and> t \<le> h"
have "DERIV (difg m) t :> diff (Suc m) t -
-    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) +
-     real (n - m) * t ^ (n - Suc m) * B / (fact (n - m)))"
-    unfolding difg_def
-    by (auto intro!: derivative_eq_intros DERIV[rule_format, OF INIT2])
+    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) +
+     real (n - m) * t ^ (n - Suc m) * B / fact (n - m))"
+    by (auto simp: difg_def intro!: derivative_eq_intros DERIV[rule_format, OF INIT2])
moreover
from INIT2 have intvl: "{..<n - m} = insert 0 (Suc  {..<n - Suc m})" and "0 < n - m"
unfolding atLeast0LessThan[symmetric] by auto
-  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
-      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
-    unfolding intvl
-    by (subst setsum.insert) (auto simp add: setsum.reindex)
+  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) =
+      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x))"
+    unfolding intvl by (subst setsum.insert) (auto simp add: setsum.reindex)
moreover
have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
-  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)) =
-            diff (Suc m + x) 0 * t^x / (fact x)"
+        less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
+  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x"
by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
moreover
-  have "(n - m) * t ^ (n - Suc m) * B / (fact (n - m)) =
-        B * (t ^ (n - Suc m) / (fact (n - Suc m)))"
-    using \<open>0 < n - m\<close>
-    by (simp add: divide_simps fact_reduce)
+  have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
+    using \<open>0 < n - m\<close> by (simp add: divide_simps fact_reduce)
ultimately show "DERIV (difg m) t :> difg (Suc m) t"
unfolding difg_def  by (simp add: mult.commute)
qed

lemma Maclaurin:
assumes h: "0 < h"
-  assumes n: "0 < n"
-  assumes diff_0: "diff 0 = f"
-  assumes diff_Suc:
-    "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
+    and n: "0 < n"
+    and diff_0: "diff 0 = f"
+    and diff_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
shows
-    "\<exists>t::real. 0 < t & t < h &
-              f h =
-              setsum (%m. (diff m 0 / (fact m)) * h ^ m) {..<n} +
-              (diff n t / (fact n)) * h ^ n"
+    "\<exists>t::real. 0 < t \<and> t < h \<and>
+      f h = setsum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n"
proof -
from n obtain m where m: "n = Suc m"
by (cases n) (simp add: n)
+  from m have "m < n" by simp

-  obtain B where f_h: "f h =
-        (\<Sum>m<n. diff m (0::real) / (fact m) * h ^ m) + B * (h ^ n / (fact n))"
+  obtain B where f_h: "f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + B * (h ^ n / fact n)"
using Maclaurin_lemma [OF h] ..

define g where [abs_def]: "g t =
-    f t - (setsum (\<lambda>m. (diff m 0 / (fact m)) * t^m) {..<n} + (B * (t^n / (fact n))))" for t
-
-  have g2: "g 0 = 0 & g h = 0"
-    by (simp add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)
+    f t - (setsum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t
+  have g2: "g 0 = 0" "g h = 0"
+    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 setsum.reindex)

define difg where [abs_def]: "difg m t =
-    diff m t - (setsum (%p. (diff (m + p) 0 / (fact p)) * (t ^ p)) {..<n-m}
-      + (B * ((t ^ (n - m)) / (fact (n - m)))))" for m t
-
+    diff m t - (setsum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} +
+      B * ((t ^ (n - m)) / fact (n - m)))" for m t
have difg_0: "difg 0 = g"
-    unfolding difg_def g_def by (simp add: diff_0)
-
-  have difg_Suc: "\<forall>(m::nat) t::real.
-        m < n \<and> (0::real) \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
+    by (simp add: difg_def g_def diff_0)
+  have difg_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
-
have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff setsum.reindex)
-
-  have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
+  have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x"
by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
-
-  have differentiable_difg:
-    "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> difg m differentiable (at x)"
+  have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)"
by (rule differentiableI [OF difg_Suc [rule_format]]) simp
-
-  have difg_Suc_eq_0: "\<And>m t. \<lbrakk>m < n; 0 \<le> t; t \<le> h; DERIV (difg m) t :> 0\<rbrakk>
-        \<Longrightarrow> difg (Suc m) t = 0"
+  have difg_Suc_eq_0:
+    "\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0"
by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp

-  have "m < n" using m by simp
-
have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
using \<open>m < n\<close>
proof (induct m)
@@ -126,7 +107,8 @@
show ?case
proof (rule Rolle)
show "0 < h" by fact
-      show "difg 0 0 = difg 0 h" by (simp add: difg_0 g2)
+      show "difg 0 0 = difg 0 h"
+        by (simp add: difg_0 g2)
show "\<forall>x. 0 \<le> x \<and> x \<le> h \<longrightarrow> isCont (difg (0::nat)) x"
show "\<forall>x. 0 < x \<and> x < h \<longrightarrow> difg (0::nat) differentiable (at x)"
@@ -134,8 +116,10 @@
qed
next
case (Suc m')
-    hence "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0" by simp
-    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0" by fast
+    then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m') t :> 0"
+      by simp
+    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
+      by fast
have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
proof (rule Rolle)
show "0 < t" by fact
@@ -146,448 +130,429 @@
show "\<forall>x. 0 < x \<and> x < t \<longrightarrow> difg (Suc m') differentiable (at x)"
using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: differentiable_difg)
qed
-    thus ?case
-      using \<open>t < h\<close> by auto
+    with \<open>t < h\<close> show ?case
+      by auto
qed
-  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0" by fast
-
-  hence "difg (Suc m) t = 0"
-    using \<open>m < n\<close> by (simp add: difg_Suc_eq_0)
-
+  then obtain t where "0 < t" "t < h" "DERIV (difg m) t :> 0"
+    by fast
+  with \<open>m < n\<close> have "difg (Suc m) t = 0"
show ?thesis
proof (intro exI conjI)
show "0 < t" by fact
show "t < h" by fact
show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
-      using \<open>difg (Suc m) t = 0\<close>
-      by (simp add: m f_h difg_def)
+      using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def)
qed
qed

lemma Maclaurin_objl:
-  "0 < h & n>0 & diff 0 = f &
-  (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
-   --> (\<exists>t::real. 0 < t & t < h &
-            f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
-                  diff n t / (fact n) * h ^ n)"
-by (blast intro: Maclaurin)
-
+  "0 < h \<and> n > 0 \<and> diff 0 = f \<and>
+    (\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
+    (\<exists>t. 0 < t \<and> t < h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n)"
+  for n :: nat and h :: real
+  by (blast intro: Maclaurin)

lemma Maclaurin2:
-  assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
-  and DERIV: "\<forall>m t::real.
-  m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
-  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
-  (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
-  diff n t / (fact n) * h ^ n"
-proof (cases "n")
-  case 0 with INIT1 INIT2 show ?thesis by fastforce
+  fixes n :: nat
+    and h :: real
+  assumes INIT1: "0 < h"
+    and INIT2: "diff 0 = f"
+    and DERIV: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n"
+proof (cases n)
+  case 0
+  with INIT1 INIT2 show ?thesis by fastforce
next
case Suc
-  hence "n > 0" by simp
-  from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
-    f h =
-    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
+  then have "n > 0" by simp
+  from INIT1 this INIT2 DERIV
+  have "\<exists>t>0. t < h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
by (rule Maclaurin)
-  thus ?thesis by fastforce
+  then show ?thesis by fastforce
qed

lemma Maclaurin2_objl:
-     "0 < h & diff 0 = f &
-       (\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t)
-    --> (\<exists>t::real. 0 < t &
-              t \<le> h &
-              f h =
-              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
-              diff n t / (fact n) * h ^ n)"
-by (blast intro: Maclaurin2)
+  "0 < h \<and> diff 0 = f \<and>
+    (\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
+    (\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n)"
+  for n :: nat and h :: real
+  by (blast intro: Maclaurin2)

lemma Maclaurin_minus:
-  fixes h::real
+  fixes n :: nat and h :: real
assumes "h < 0" "0 < n" "diff 0 = f"
-  and DERIV: "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
-  shows "\<exists>t. h < t & t < 0 &
-         f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
-         diff n t / (fact n) * h ^ n"
+    and DERIV: "\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+  shows "\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
proof -
-  txt "Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format."
+  txt \<open>Transform \<open>ABL'\<close> into \<open>derivative_intros\<close> format.\<close>
note DERIV' = DERIV_chain'[OF _ DERIV[rule_format], THEN DERIV_cong]
-  from assms
-  have "\<exists>t>0. t < - h \<and>
-    f (- (- h)) =
-    (\<Sum>m<n.
-    (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
+  let ?sum = "\<lambda>t.
+    (\<Sum>m<n. (- 1) ^ m * diff m (- 0) / (fact m) * (- h) ^ m) +
(- 1) ^ n * diff n (- t) / (fact n) * (- h) ^ n"
+  from assms have "\<exists>t>0. t < - h \<and> f (- (- h)) = ?sum t"
by (intro Maclaurin) (auto intro!: derivative_eq_intros DERIV')
-  then guess t ..
-  moreover
-  have "(- 1) ^ n * diff n (- t) * (- h) ^ n / (fact n) = diff n (- t) * h ^ n / (fact n)"
-    by (auto simp add: power_mult_distrib[symmetric])
+  then obtain t where "0 < t" "t < - h" "f (- (- h)) = ?sum t"
+    by blast
+  moreover have "(- 1) ^ n * diff n (- t) * (- h) ^ n / fact n = diff n (- t) * h ^ n / fact n"
+    by (auto simp: power_mult_distrib[symmetric])
moreover
-  have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / (fact m)) = (\<Sum>m<n. diff m 0 * h ^ m / (fact m))"
+    have "(\<Sum>m<n. (- 1) ^ m * diff m 0 * (- h) ^ m / fact m) = (\<Sum>m<n. diff m 0 * h ^ m / fact m)"
by (auto intro: setsum.cong simp add: power_mult_distrib[symmetric])
-  ultimately have " h < - t \<and>
-    - t < 0 \<and>
-    f h =
-    (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
+  ultimately have "h < - t \<and> - t < 0 \<and>
+    f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n (- t) / (fact n) * h ^ n"
by auto
-  thus ?thesis ..
+  then show ?thesis ..
qed

lemma Maclaurin_minus_objl:
-  fixes h::real
+  fixes n :: nat and h :: real
shows
-     "(h < 0 & n > 0 & diff 0 = f &
-       (\<forall>m t.
-          m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t))
-    --> (\<exists>t. h < t &
-              t < 0 &
-              f h =
-              (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) +
-              diff n t / (fact n) * h ^ n)"
-by (blast intro: Maclaurin_minus)
+    "h < 0 \<and> n > 0 \<and> diff 0 = f \<and>
+      (\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
+    (\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n)"
+  by (blast intro: Maclaurin_minus)

-subsection\<open>More Convenient "Bidirectional" Version.\<close>
+subsection \<open>More Convenient "Bidirectional" Version.\<close>

(* not good for PVS sin_approx, cos_approx *)

lemma Maclaurin_bi_le_lemma:
-  "n>0 \<Longrightarrow>
-   diff 0 0 =
-   (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
-by (induct "n") auto
+  "n > 0 \<Longrightarrow>
+    diff 0 0 = (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
+  by (induct n) auto

lemma Maclaurin_bi_le:
-   assumes "diff 0 = f"
-   and DERIV : "\<forall>m t::real. m < n & \<bar>t\<bar> \<le> \<bar>x\<bar> --> DERIV (diff m) t :> diff (Suc m) t"
-   shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
-              f x =
-              (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
-     diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
-proof cases
-  assume "n = 0" with \<open>diff 0 = f\<close> show ?thesis by force
+  fixes n :: nat and x :: real
+  assumes "diff 0 = f"
+    and DERIV : "\<forall>m t. m < n \<and> \<bar>t\<bar> \<le> \<bar>x\<bar> \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) + diff n t / (fact n) * x ^ n"
+    (is "\<exists>t. _ \<and> f x = ?f x t")
+proof (cases "n = 0")
+  case True
+  with \<open>diff 0 = f\<close> show ?thesis by force
next
-  assume "n \<noteq> 0"
+  case False
show ?thesis
proof (cases rule: linorder_cases)
-    assume "x = 0" with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV
-    have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by (auto simp add: Maclaurin_bi_le_lemma)
-    thus ?thesis ..
+    assume "x = 0"
+    with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
+      by (auto simp add: Maclaurin_bi_le_lemma)
+    then show ?thesis ..
next
assume "x < 0"
-    with \<open>n \<noteq> 0\<close> DERIV
-    have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t" by (intro Maclaurin_minus) auto
-    then guess t ..
-    with \<open>x < 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
-    thus ?thesis ..
+    with \<open>n \<noteq> 0\<close> DERIV have "\<exists>t>x. t < 0 \<and> diff 0 x = ?f x t"
+      by (intro Maclaurin_minus) auto
+    then obtain t where "x < t" "t < 0"
+      "diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
+      by blast
+    with \<open>x < 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
+      by simp
+    then show ?thesis ..
next
assume "x > 0"
-    with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV
-    have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t" by (intro Maclaurin) auto
-    then guess t ..
+    with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<exists>t>0. t < x \<and> diff 0 x = ?f x t"
+      by (intro Maclaurin) auto
+    then obtain t where "0 < t" "t < x"
+      "diff 0 x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
+      by blast
with \<open>x > 0\<close> \<open>diff 0 = f\<close> have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
-    thus ?thesis ..
+    then show ?thesis ..
qed
qed

lemma Maclaurin_all_lt:
-  fixes x::real
-  assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
-  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
-  shows "\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> & f x =
-    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
-                (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
+  fixes x :: real
+  assumes INIT1: "diff 0 = f"
+    and INIT2: "0 < n"
+    and INIT3: "x \<noteq> 0"
+    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
+  shows "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x =
+      (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n"
+    (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
proof (cases rule: linorder_cases)
-  assume "x = 0" with INIT3 show "?thesis"..
+  assume "x = 0"
+  with INIT3 show ?thesis ..
next
assume "x < 0"
-  with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t" by (intro Maclaurin_minus) auto
-  then guess t ..
-  with \<open>x < 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
-  thus ?thesis ..
+  with assms have "\<exists>t>x. t < 0 \<and> f x = ?f x t"
+    by (intro Maclaurin_minus) auto
+  then obtain t where "t > x" "t < 0" "f x = ?f x t"
+    by blast
+  with \<open>x < 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
+    by simp
+  then show ?thesis ..
next
assume "x > 0"
-  with assms have "\<exists>t>0. t < x \<and> f x = ?f x t " by (intro Maclaurin) auto
-  then guess t ..
-  with \<open>x > 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" by simp
-  thus ?thesis ..
+  with assms have "\<exists>t>0. t < x \<and> f x = ?f x t"
+    by (intro Maclaurin) auto
+  then obtain t where "t > 0" "t < x" "f x = ?f x t"
+    by blast
+  with \<open>x > 0\<close> have "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
+    by simp
+  then show ?thesis ..
qed

lemma Maclaurin_all_lt_objl:
-  fixes x::real
+  fixes x :: real
shows
-     "diff 0 = f &
-      (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
-      x ~= 0 & n > 0
-      --> (\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> &
-               f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
-                     (diff n t / (fact n)) * x ^ n)"
-by (blast intro: Maclaurin_all_lt)
+    "diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<and> x \<noteq> 0 \<and> n > 0 \<longrightarrow>
+    (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and>
+      f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n)"
+  by (blast intro: Maclaurin_all_lt)

-lemma Maclaurin_zero [rule_format]:
-     "x = (0::real)
-      ==> n \<noteq> 0 -->
-          (\<Sum>m<n. (diff m (0::real) / (fact m)) * x ^ m) =
-          diff 0 0"
-by (induct n, auto)
+lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0"
+  for x :: real and n :: nat
+  by (induct n) auto

lemma Maclaurin_all_le:
+  fixes x :: real and n :: nat
assumes INIT: "diff 0 = f"
-  and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
-  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> & f x =
-    (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
-    (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
-proof cases
-  assume "n = 0" with INIT show ?thesis by force
-  next
-  assume "n \<noteq> 0"
+    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n"
+    (is "\<exists>t. _ \<and> f x = ?f x t")
+proof (cases "n = 0")
+  case True
+  with INIT show ?thesis by force
+next
+  case False
show ?thesis
-  proof cases
-    assume "x = 0"
+  proof (cases "x = 0")
+    case True
with \<open>n \<noteq> 0\<close> have "(\<Sum>m<n. diff m 0 / (fact m) * x ^ m) = diff 0 0"
by (intro Maclaurin_zero) auto
-    with INIT \<open>x = 0\<close> \<open>n \<noteq> 0\<close> have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0" by force
-    thus ?thesis ..
+    with INIT \<open>x = 0\<close> \<open>n \<noteq> 0\<close> have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
+      by force
+    then show ?thesis ..
next
-    assume "x \<noteq> 0"
+    case False
with INIT \<open>n \<noteq> 0\<close> DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t"
by (intro Maclaurin_all_lt) auto
-    then guess t ..
-    hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t" by simp
-    thus ?thesis ..
+    then obtain t where "0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> f x = ?f x t" ..
+    then have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x t"
+      by simp
+    then show ?thesis ..
qed
qed

lemma Maclaurin_all_le_objl:
-  "diff 0 = f &
-      (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
-      --> (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
-              f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
-                    (diff n t / (fact n)) * x ^ n)"
-by (blast intro: Maclaurin_all_le)
+  "diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<longrightarrow>
+    (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n)"
+  for x :: real and n :: nat
+  by (blast intro: Maclaurin_all_le)

-subsection\<open>Version for Exponential Function\<close>
+subsection \<open>Version for Exponential Function\<close>

lemma Maclaurin_exp_lt:
-  fixes x::real
+  fixes x :: real and n :: nat
shows
-  "[| x ~= 0; n > 0 |]
-      ==> (\<exists>t. 0 < \<bar>t\<bar> &
-                \<bar>t\<bar> < \<bar>x\<bar> &
-                exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
-                        (exp t / (fact n)) * x ^ n)"
-by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
-
+    "x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow>
+      (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n)"
+ using Maclaurin_all_lt_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto

lemma Maclaurin_exp_le:
-     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
-            exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
-                       (exp t / (fact n)) * x ^ n"
-by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
+  fixes x :: real and n :: nat
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
+  using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
+
+lemma exp_lower_taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
+  for x :: real
+  using Maclaurin_exp_le [of x 3] by (auto simp: numeral_3_eq_3 power2_eq_square)
+
+
+subsection \<open>Version for Sine Function\<close>

-  fixes x::real
-  shows "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
-  using Maclaurin_exp_le [of x 3]
-  by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc)
+lemma mod_exhaust_less_4: "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = 3"
+  for m :: nat
+  by auto
+
+lemma Suc_Suc_mult_two_diff_two [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (2 * n - 2)) = 2 * n"
+  by (induct n) auto
+
+lemma lemma_Suc_Suc_4n_diff_2 [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (4 * n - 2)) = 4 * n"
+  by (induct n) auto
+
+lemma Suc_mult_two_diff_one [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (2 * n - 1) = 2 * n"
+  by (induct n) auto

-subsection\<open>Version for Sine Function\<close>
-
-lemma mod_exhaust_less_4:
-  "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
-by auto
-
-lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
-  "n\<noteq>0 --> Suc (Suc (2 * n - 2)) = 2*n"
-by (induct "n", auto)
+text \<open>It is unclear why so many variant results are needed.\<close>

-lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]:
-  "n\<noteq>0 --> Suc (Suc (4*n - 2)) = 4*n"
-by (induct "n", auto)
-
-lemma Suc_mult_two_diff_one [rule_format, simp]:
-  "n\<noteq>0 --> Suc (2 * n - 1) = 2*n"
-by (induct "n", auto)
-
-
-text\<open>It is unclear why so many variant results are needed.\<close>
-
-lemma sin_expansion_lemma:
-     "sin (x + real (Suc m) * pi / 2) =
-      cos (x + real (m) * pi / 2)"
+lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"

lemma Maclaurin_sin_expansion2:
-     "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
-       sin x =
-       (\<Sum>m<n. sin_coeff m * x ^ m)
-      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-apply (cut_tac f = sin and n = n and x = x
-        and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
-apply safe
-    apply (simp)
-   apply (simp add: sin_expansion_lemma del: of_nat_Suc)
-   apply (force intro!: derivative_eq_intros)
-  apply (subst (asm) setsum.neutral, auto)[1]
- apply (rule ccontr, simp)
- apply (drule_tac x = x in spec, simp)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-done
+  "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
+    sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin_all_lt_objl
+    [where f = sin and n = n and x = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
+  apply safe
+      apply simp
+     apply (simp add: sin_expansion_lemma del: of_nat_Suc)
+     apply (force intro!: derivative_eq_intros)
+    apply (subst (asm) setsum.neutral; auto)
+   apply (rule ccontr)
+   apply simp
+   apply (drule_tac x = x in spec)
+   apply simp
+  apply (erule ssubst)
+  apply (rule_tac x = t in exI)
+  apply simp
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+  done

lemma Maclaurin_sin_expansion:
-     "\<exists>t. sin x =
-       (\<Sum>m<n. sin_coeff m * x ^ m)
-      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-apply (insert Maclaurin_sin_expansion2 [of x n])
-apply (blast intro: elim:)
-done
+  "\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin_sin_expansion2 [of x n] by blast

lemma Maclaurin_sin_expansion3:
-     "[| n > 0; 0 < x |] ==>
-       \<exists>t. 0 < t & t < x &
-       sin x =
-       (\<Sum>m<n. sin_coeff m * x ^ m)
-      + ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
-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)
-apply safe
+  "n > 0 \<Longrightarrow> 0 < x \<Longrightarrow>
+    \<exists>t. 0 < t \<and> t < x \<and>
+       sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin_objl
+    [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
+  apply safe
+    apply simp
+   apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
+   apply (force intro!: derivative_eq_intros)
+  apply (erule ssubst)
+  apply (rule_tac x = t in exI)
+  apply simp
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+  done
+
+lemma Maclaurin_sin_expansion4:
+  "0 < x \<Longrightarrow>
+    \<exists>t. 0 < t \<and> t \<le> x \<and>
+      sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin2_objl
+    [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
+  apply safe
apply simp
apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
apply (force intro!: derivative_eq_intros)
apply (erule ssubst)
-  apply (rule_tac x = t in exI, simp)
- apply (rule setsum.cong[OF refl])
- apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-done
-
-lemma Maclaurin_sin_expansion4:
-     "0 < x ==>
-       \<exists>t. 0 < t & t \<le> x &
-       sin x =
-       (\<Sum>m<n. sin_coeff m * x ^ m)
-      + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-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)
-apply safe
-    apply simp
-   apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
-   apply (force intro!: derivative_eq_intros)
-  apply (erule ssubst)
-  apply (rule_tac x = t in exI, simp)
- apply (rule setsum.cong[OF refl])
- apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-done
+  apply (rule_tac x = t in exI)
+  apply simp
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+  done

-subsection\<open>Maclaurin Expansion for Cosine Function\<close>
+subsection \<open>Maclaurin Expansion for Cosine Function\<close>

-lemma sumr_cos_zero_one [simp]:
-  "(\<Sum>m<(Suc n). cos_coeff m * 0 ^ m) = 1"
-by (induct "n", auto)
+lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1"
+  by (induct n) auto

-lemma cos_expansion_lemma:
-  "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
+lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"

lemma Maclaurin_cos_expansion:
-     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
-       cos x =
-       (\<Sum>m<n. cos_coeff m * x ^ m)
-      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-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)
-apply safe
-    apply (simp (no_asm))
-   apply (simp (no_asm) add: cos_expansion_lemma del: of_nat_Suc)
-  apply (case_tac "n", simp)
-  apply (simp del: setsum_lessThan_Suc)
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
-done
+  "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
+    cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin_all_lt_objl
+    [where f = cos and n = n and x = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
+  apply safe
+      apply simp
+     apply (simp add: cos_expansion_lemma del: of_nat_Suc)
+    apply (cases n)
+     apply simp
+    apply (simp del: setsum_lessThan_Suc)
+   apply (rule ccontr)
+   apply simp
+   apply (drule_tac x = x in spec)
+   apply simp
+  apply (erule ssubst)
+  apply (rule_tac x = t in exI)
+  apply simp
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
+  done

lemma Maclaurin_cos_expansion2:
-     "[| 0 < x; n > 0 |] ==>
-       \<exists>t. 0 < t & t < x &
-       cos x =
-       (\<Sum>m<n. cos_coeff m * x ^ m)
-      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-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)
-apply safe
+  "0 < x \<Longrightarrow> n > 0 \<Longrightarrow>
+    \<exists>t. 0 < t \<and> t < x \<and>
+      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  using Maclaurin_objl
+    [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
+  apply safe
+    apply simp
+   apply (simp add: cos_expansion_lemma del: of_nat_Suc)
+  apply (erule ssubst)
+  apply (rule_tac x = t in exI)
apply simp
-  apply (simp (no_asm) add: cos_expansion_lemma del: of_nat_Suc)
- apply (erule ssubst)
- apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
-done
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
+  done

lemma Maclaurin_minus_cos_expansion:
-     "[| x < 0; n > 0 |] ==>
-       \<exists>t. x < t & t < 0 &
-       cos x =
-       (\<Sum>m<n. cos_coeff m * x ^ m)
-      + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
-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)
-apply safe
+  "x < 0 \<Longrightarrow> n > 0 \<Longrightarrow>
+    \<exists>t. x < t \<and> t < 0 \<and>
+      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
+  using Maclaurin_minus_objl
+    [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n *pi)"]
+  apply safe
+    apply simp
+   apply (simp add: cos_expansion_lemma del: of_nat_Suc)
+  apply (erule ssubst)
+  apply (rule_tac x = t in exI)
apply simp
- apply (simp (no_asm) add: cos_expansion_lemma del: of_nat_Suc)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
-done
+  apply (rule setsum.cong[OF refl])
+  apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
+  done
+

-(* ------------------------------------------------------------------------- *)
-(* Version for ln(1 +/- x). Where is it??                                    *)
-(* ------------------------------------------------------------------------- *)
+(* Version for ln(1 +/- x). Where is it?? *)
+

-lemma sin_bound_lemma:
-    "[|x = y; \<bar>u\<bar> \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
-by auto
+lemma sin_bound_lemma: "x = y \<Longrightarrow> \<bar>u\<bar> \<le> v \<Longrightarrow> \<bar>(x + u) - y\<bar> \<le> v"
+  for x y u v :: real
+  by auto

-lemma Maclaurin_sin_bound:
-  "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
+lemma Maclaurin_sin_bound: "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse (fact n) * \<bar>x\<bar> ^ n"
proof -
-  have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
-    by (rule_tac mult_right_mono,simp_all)
-  note est = this[simplified]
-  let ?diff = "\<lambda>(n::nat) x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then -sin(x) else -cos(x)"
+  have est: "x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" for x y :: real
+    by (rule mult_right_mono) simp_all
+  let ?diff = "\<lambda>(n::nat) x.
+    if n mod 4 = 0 then sin x
+    else if n mod 4 = 1 then cos x
+    else if n mod 4 = 2 then - sin x
+    else - cos x"
have diff_0: "?diff 0 = sin" by simp
have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x"
-    apply (clarify)
+    apply clarify
apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
apply (cut_tac m=m in mod_exhaust_less_4)
-    apply (safe, auto intro!: derivative_eq_intros)
+    apply safe
+       apply (auto intro!: derivative_eq_intros)
done
from Maclaurin_all_le [OF diff_0 DERIV_diff]
-  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
-    t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) +
-      ?diff n t / (fact n) * x ^ n" by fast
-  have diff_m_0:
-    "\<And>m. ?diff m 0 = (if even m then 0
-         else (- 1) ^ ((m - Suc 0) div 2))"
+  obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>"
+    and t2: "sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / (fact n) * x ^ n"
+    by fast
+  have diff_m_0: "\<And>m. ?diff m 0 = (if even m then 0 else (- 1) ^ ((m - Suc 0) div 2))"
apply (subst even_even_mod_4_iff)
apply (cut_tac m=m in mod_exhaust_less_4)
-    apply (elim disjE, simp_all)
-    apply (safe dest!: mod_eqD, simp_all)
+    apply (elim disjE)
+       apply simp_all
+     apply (safe dest!: mod_eqD)
+     apply simp_all
done
show ?thesis
unfolding sin_coeff_def
apply (subst t2)
apply (rule sin_bound_lemma)
-    apply (rule setsum.cong[OF refl])
-    apply (subst diff_m_0, simp)
+     apply (rule setsum.cong[OF refl])
+     apply (subst diff_m_0, simp)
+    using est
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
-                simp add: est ac_simps divide_inverse power_abs [symmetric] abs_mult)
+        simp: ac_simps divide_inverse power_abs [symmetric] abs_mult)
done
qed

--- a/src/HOL/Taylor.thy	Sat Jul 30 21:10:02 2016 +0200
+++ b/src/HOL/Taylor.thy	Sun Jul 31 17:25:38 2016 +0200
@@ -9,91 +9,97 @@
begin

text \<open>
-We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
-to prove Taylor's theorem.
+  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
+  to prove Taylor's theorem.
\<close>

-lemma taylor_up:
-  assumes INIT: "n>0" "diff 0 = f"
-  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
-  and INTERV: "a \<le> c" "c < b"
-  shows "\<exists>t::real. c < t & t < b &
-    f b = (\<Sum>m<n. (diff m c / (fact m)) * (b - c)^m) + (diff n t / (fact n)) * (b - c)^n"
+lemma taylor_up:
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
+    and INTERV: "a \<le> c" "c < b"
+  shows "\<exists>t::real. c < t \<and> t < b \<and>
+    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
proof -
-  from INTERV have "0 < b-c" by arith
-  moreover
-  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  from INTERV have "0 < b - c" by arith
+  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
+    by auto
moreover
-  have "ALL m t. m < n & 0 <= t & t <= b - c --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
proof (intro strip)
fix m t
-    assume "m < n & 0 <= t & t <= b - c"
-    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
-    moreover
-    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
-    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)"
+    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
+    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
+      by auto
+    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
+    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
by (rule DERIV_chain2)
-    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
+    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+      by simp
qed
-  ultimately obtain x where
-        "0 < x & x < b - c &
-        f (b - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (b - c) ^ m) +
-          diff n (x + c) / (fact n) * (b - c) ^ n"
+  ultimately obtain x where
+    "0 < x \<and> x < b - c \<and>
+      f (b - c + c) =
+        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
by (rule Maclaurin [THEN exE])
-  then have "c<x+c & x+c<b \<and> f b = (\<Sum>m<n. diff m c / (fact m) * (b - c) ^ m) +
-    diff n (x+c) / (fact n) * (b - c) ^ n"
+   then have "c < x + c \<and> x + c < b \<and> f b =
+     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
by fastforce
-  thus ?thesis by fastforce
+  then show ?thesis by fastforce
qed

lemma taylor_down:
-  fixes a::real
-  assumes INIT: "n>0" "diff 0 = f"
-  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
-  and INTERV: "a < c" "c \<le> b"
-  shows "\<exists> t. a < t & t < c &
-    f a = (\<Sum>m<n. (diff m c / (fact m)) * (a - c)^m) + (diff n t / (fact n)) * (a - c)^n"
+  fixes a :: real and n :: nat
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
+    and INTERV: "a < c" "c \<le> b"
+  shows "\<exists>t. a < t \<and> t < c \<and>
+    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
proof -
from INTERV have "a-c < 0" by arith
-  moreover
-  from INIT have "n>0" "((\<lambda>m x. diff m (x + c)) 0) = (\<lambda>x. f (x + c))" by auto
+  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
+    by auto
moreover
-  have "ALL m t. m < n & a-c <= t & t <= 0 --> DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+  have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
proof (rule allI impI)+
fix m t
-    assume "m < n & a-c <= t & t <= 0"
-    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)" by auto
-    moreover
-    from DERIV_ident and DERIV_const have "DERIV (%x. x + c) t :> 1+0" by (rule DERIV_add)
-    ultimately have "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1+0)" by (rule DERIV_chain2)
-    thus "DERIV (%x. diff m (x + c)) t :> diff (Suc m) (t + c)" by simp
+    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
+    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
+      by auto
+    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
+    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
+      by (rule DERIV_chain2)
+    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+      by simp
qed
-  ultimately obtain x where
-         "a - c < x & x < 0 &
-      f (a - c + c) = (\<Sum>m<n. diff m (0 + c) / (fact m) * (a - c) ^ m) +
-        diff n (x + c) / (fact n) * (a - c) ^ n"
-     by (rule Maclaurin_minus [THEN exE])
-  then have "a<x+c & x+c<c \<and> f a = (\<Sum>m<n. diff m c / (fact m) * (a - c) ^ m) +
-      diff n (x+c) / (fact n) * (a - c) ^ n"
+  ultimately obtain x where
+    "a - c < x \<and> x < 0 \<and>
+      f (a - c + c) =
+        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
+    by (rule Maclaurin_minus [THEN exE])
+  then have "a < x + c \<and> x + c < c \<and>
+    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
by fastforce
-  thus ?thesis by fastforce
+  then show ?thesis by fastforce
qed

-lemma taylor:
-  fixes a::real
-  assumes INIT: "n>0" "diff 0 = f"
-  and DERIV: "(\<forall> m t. m < n & a \<le> t & t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t))"
-  and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
-  shows "\<exists> t. (if x<c then (x < t & t < c) else (c < t & t < x)) &
-    f x = (\<Sum>m<n. (diff m c / (fact m)) * (x - c)^m) + (diff n t / (fact n)) * (x - c)^n"
-proof (cases "x<c")
+theorem taylor:
+  fixes a :: real and n :: nat
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
+  shows "\<exists>t.
+    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
+    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
+proof (cases "x < c")
case True
note INIT
-  moreover from DERIV and INTERV
-  have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    by fastforce
+  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    using DERIV and INTERV by fastforce
moreover note True
-  moreover from INTERV have "c \<le> b" by simp
+  moreover from INTERV have "c \<le> b"
+    by simp
ultimately have "\<exists>t>x. t < c \<and> f x =
(\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
by (rule taylor_down)
@@ -101,13 +107,14 @@
next
case False
note INIT
-  moreover from DERIV and INTERV
-  have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    by fastforce
-  moreover from INTERV have "a \<le> c" by arith
-  moreover from False and INTERV have "c < x" by arith
+  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    using DERIV and INTERV by fastforce
+  moreover from INTERV have "a \<le> c"
+    by arith
+  moreover from False and INTERV have "c < x"
+    by arith
ultimately have "\<exists>t>c. t < x \<and> f x =
-    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
+    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
by (rule taylor_up)
with False show ?thesis by simp
qed`