--- 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)
+
subsection \<open>Addition and Subtraction\<close>
instantiation complex :: ab_group_add
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
(simp_all add: complex_eq_iff divide_complex_def
distrib_left distrib_right right_diff_distrib left_diff_distrib
power2_eq_square add_divide_distrib [symmetric])
@@ -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)"
- unfolding divide_complex_def by (simp add: add_divide_distrib)
+ by (simp add: divide_complex_def add_divide_distrib)
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
- by (simp_all add: divide_simps)
+ by (simp add: divide_simps)
lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
by (simp add: power2_eq_square)
@@ -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"
by (simp add: complex_eq_iff)
@@ -203,31 +216,31 @@
lemma fun_complex_eq: "f = (\<lambda>x. Re (f x) + \<i> * Im (f x))"
by (simp add: fun_eq_iff complex_eq)
-lemma i_squared [simp]: "ii * ii = -1"
+lemma i_squared [simp]: "\<i> * \<i> = -1"
by (simp add: complex_eq_iff)
-lemma power2_i [simp]: "ii\<^sup>2 = -1"
+lemma power2_i [simp]: "\<i>\<^sup>2 = -1"
by (simp add: power2_eq_square)
-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"
by (simp add: divide_complex_def)
-lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
+lemma complex_i_mult_minus [simp]: "\<i> * (\<i> * x) = - x"
by (simp add: mult.assoc [symmetric])
-lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
+lemma complex_i_not_zero [simp]: "\<i> \<noteq> 0"
by (simp add: complex_eq_iff)
-lemma complex_i_not_one [simp]: "ii \<noteq> 1"
+lemma complex_i_not_one [simp]: "\<i> \<noteq> 1"
by (simp add: complex_eq_iff)
-lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
+lemma complex_i_not_numeral [simp]: "\<i> \<noteq> numeral w"
by (simp add: complex_eq_iff)
-lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
+lemma complex_i_not_neg_numeral [simp]: "\<i> \<noteq> - numeral w"
by (simp add: complex_eq_iff)
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)"
by (simp add: norm_complex_def complex_eq_iff)
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"
by (simp add: norm_complex_def)
lemma cmod_unit_one: "cmod (cos a + \<i> * sin a) = 1"
@@ -296,8 +311,7 @@
by (simp add: norm_mult cmod_unit_one)
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)
apply (simp add: norm_mult)
done
@@ -324,33 +338,31 @@
lemma cmod_eq_Im: "Re z = 0 \<Longrightarrow> cmod z = \<bar>Im z\<bar>"
by (simp add: norm_complex_def)
-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"
by (simp add: norm_complex_def)
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>"
by (metis add.commute add_le_cancel_left norm_complex_def real_sqrt_abs real_sqrt_le_iff)
-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])
- (auto simp add: norm_complex_def)
+ 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)
- apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
+ apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
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"
by (simp add: complex_eq_iff)
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
@@ -450,7 +465,7 @@
lemma complex_cnj_zero [simp]: "cnj 0 = 0"
by (simp add: complex_eq_iff)
-lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
+lemma complex_cnj_zero_iff [iff]: "cnj z = 0 \<longleftrightarrow> z = 0"
by (simp add: complex_eq_iff)
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"
by (simp add: complex_eq_iff)
-lemma complex_cnj_i [simp]: "cnj ii = - ii"
+lemma complex_cnj_i [simp]: "cnj \<i> = - \<i>"
by (simp add: complex_eq_iff)
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
by (simp add: complex_eq_iff)
-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>"
by (simp add: complex_eq_iff)
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"
- using complex_cnj_add complex_cnj_scaleR
- 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"
by (auto simp add: Im_divide)
-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"
by (simp add: complex_eq_iff sum_power2_gt_zero_iff)
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"
by (simp add: complex_eq_iff)
@@ -700,27 +717,28 @@
by (simp add: complex_eq_iff cos_add sin_add)
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)"
by (simp add: complex_eq_iff)
lemma cis_divide: "cis a / cis b = cis (a - b)"
by (simp add: divide_complex_def cis_mult)
-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)"
by (auto simp add: DeMoivre)
-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)"
by (auto simp add: DeMoivre)
lemma cis_pi: "cis pi = -1"
by (simp add: complex_eq_iff)
+
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"
by (simp add: rcis_def)
@@ -737,7 +755,7 @@
lemma cis_rcis_eq: "cis a = rcis 1 a"
by (simp add: rcis_def)
-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)"
by (simp add: rcis_def cis_mult)
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)"
by (simp add: divide_inverse rcis_def)
-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
- power2_eq_square of_nat_Suc add_nonneg_eq_0_iff)
- 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
+ power2_eq_square add_nonneg_eq_0_iff)
+ then show ?thesis
+ by (simp add: field_simps)
+ 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"
by (simp add: exp_eq_polar complex_eq_iff)
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"
by (simp add: arg_def)
@@ -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"
by (simp_all add: complex_eq_iff)
- 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"
+ by (simp add: d_def)
qed (simp add: assms del: Re_sgn Im_sgn)
with \<open>z \<noteq> 0\<close> show "arg z = x"
- unfolding arg_def by simp
+ by (simp add: arg_def)
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)"
by (simp add: complex_eq_iff norm_complex_def)
@@ -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"
by (simp add: norm_complex_def power2_eq_square)
- moreover
- have "\<bar>Re z\<bar> \<le> cmod z"
+ moreover have "\<bar>Re z\<bar> \<le> cmod z"
by (simp add: norm_complex_def)
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)
+ by (simp add: power2_eq_iff[symmetric])
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"
- by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 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 (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2
+ 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"
by (simp add: isCont_difg n)
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"
+ by (simp add: difg_Suc_eq_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>
-lemma exp_lower_taylor_quadratic:
- 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)"
-by (simp only: cos_add sin_add of_nat_Suc add_divide_distrib distrib_right, auto)
+lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"
+ by (auto simp: cos_add sin_add add_divide_distrib distrib_right)
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)"
-by (simp only: cos_add sin_add of_nat_Suc distrib_right add_divide_distrib, auto)
+lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"
+ by (auto simp: cos_add sin_add distrib_right add_divide_distrib)
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"
+ by (rule DERIV_add)
+ 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"
+ by (rule DERIV_add)
+ 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