# HG changeset patch # User paulson # Date 1096983050 -7200 # Node ID 1eb23f805c066b38dc90485f54b265c443a5cda7 # Parent 4d332d10fa3d63534dd57716ac7d6ab1ab1e9c8e new simprules for abs and for things like a/b<1 diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Complex/NSCA.thy Tue Oct 05 15:30:50 2004 +0200 @@ -673,7 +673,7 @@ simp del: realpow_Suc) apply (rule_tac y="abs(Z x)" in order_le_less_trans) apply (drule_tac t = "Z x" in sym) -apply (auto simp add: abs_eqI1 simp del: realpow_Suc) +apply (auto simp del: realpow_Suc) done (* same proof *) @@ -691,7 +691,7 @@ apply (auto simp add: complex_minus complex_add complex_mod simp del: realpow_Suc) apply (rule_tac y="abs(Z x)" in order_le_less_trans) apply (drule_tac t = "Z x" in sym) -apply (auto simp add: abs_eqI1 simp del: realpow_Suc) +apply (auto simp del: realpow_Suc) done lemma hcomplex_capproxI: diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/HTranscendental.thy Tue Oct 05 15:30:50 2004 +0200 @@ -458,17 +458,12 @@ lemma starfun_ln_Infinitesimal_less_zero: "[| x \ Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0" -apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) -apply (drule bspec [where x = 1]) -apply (auto simp add: abs_if) -done +by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) lemma starfun_ln_HInfinite_gt_zero: "[| x \ HInfinite; 0 < x |] ==> 0 < ( *f* ln) x" -apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) -apply (drule bspec [where x = 1]) -apply (auto simp add: abs_if) -done +by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) + (* Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x" diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/HyperDef.thy Tue Oct 05 15:30:50 2004 +0200 @@ -623,20 +623,12 @@ "abs (Abs_hypreal (hyprel `` {X})) = Abs_hypreal(hyprel `` {%n. abs (X n)})" apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus) -apply (ultra, arith)+ +apply ultra +apply ultra +apply arith done - -lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \ y|] ==> r < x+y" -by (auto dest: add_less_le_mono) - -text{*The precondition could be weakened to @{term "0\x"}*} -lemma hypreal_mult_less_mono: - "[| u u*x < v* y" - by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) - - subsection{*Existence of Infinite Hyperreal Number*} lemma Rep_hypreal_omega: "Rep_hypreal(omega) \ hypreal" @@ -784,7 +776,6 @@ val hypreal_one_num = thm "hypreal_one_num"; val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; -val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono"; val Rep_hypreal_omega = thm"Rep_hypreal_omega"; val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj"; val lemma_finite_omega_set = thm"lemma_finite_omega_set"; diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/HyperPow.thy Tue Oct 05 15:30:50 2004 +0200 @@ -216,6 +216,11 @@ lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1) = x pow (1 + 1)" by (simp add: hyperpow_hrabs) +text{*The precondition could be weakened to @{term "0\x"}*} +lemma hypreal_mult_less_mono: + "[| u u*x < v* y" + by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) + lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)" apply (auto simp add: hyperpow_two) apply (rule_tac y = "1*1" in order_le_less_trans) diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Tue Oct 05 15:30:50 2004 +0200 @@ -430,9 +430,9 @@ apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst]) apply (rule add_mono) apply (rule_tac y = "(e/2) * \v - x\" in order_trans) - prefer 2 apply (simp, arith) + prefer 2 apply simp apply (erule_tac [!] V= "\x'. x' ~= x & \x' + - x\ < s --> ?P x'" in thin_rl) -apply (drule_tac x = v in spec, simp, arith) +apply (drule_tac x = v in spec, simp) apply (drule_tac x = u in spec, auto, arith) apply (subgoal_tac "\f u - f x - f' x * (u - x)\ = \f x - f u - f' x * (x - u)\") apply (rule order_trans) diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Oct 05 15:30:50 2004 +0200 @@ -328,7 +328,7 @@ prefer 2 apply blast apply (drule_tac [2] diff=diff in Maclaurin) apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe) -apply (rule_tac [!] x = t in exI, auto, arith+) +apply (rule_tac [!] x = t in exI, auto) done lemma Maclaurin_all_lt_objl: diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/NSA.thy Tue Oct 05 15:30:50 2004 +0200 @@ -22,12 +22,12 @@ HInfinite :: "hypreal set" "HInfinite == {x. \r \ Reals. r < abs x}" - (* infinitely close *) approx :: "[hypreal, hypreal] => bool" (infixl "@=" 50) + --{*the `infinitely close' relation*} "x @= y == (x + -y) \ Infinitesimal" - (* standard part map *) st :: "hypreal => hypreal" + --{*the standard part of a hyperreal*} "st == (%x. @r. x \ HFinite & r \ Reals & r @= x)" monad :: "hypreal => hypreal set" @@ -39,8 +39,8 @@ defs (overloaded) - (*standard real numbers as a subset of the hyperreals*) SReal_def: "Reals == {x. \r. x = hypreal_of_real r}" + --{*the standard real numbers as a subset of the hyperreals*} syntax (xsymbols) approx :: "[hypreal, hypreal] => bool" (infixl "\" 50) @@ -50,7 +50,7 @@ -subsection{*Closure Laws for Standard Reals*} +subsection{*Closure Laws for the Standard Reals*} lemma SReal_add [simp]: "[| (x::hypreal) \ Reals; y \ Reals |] ==> x + y \ Reals" @@ -78,12 +78,11 @@ apply (blast intro: hypreal_of_real_minus [symmetric]) done -lemma SReal_minus_iff: "(-x \ Reals) = ((x::hypreal) \ Reals)" +lemma SReal_minus_iff [simp]: "(-x \ Reals) = ((x::hypreal) \ Reals)" apply auto apply (erule_tac [2] SReal_minus) apply (drule SReal_minus, auto) done -declare SReal_minus_iff [simp] lemma SReal_add_cancel: "[| (x::hypreal) + y \ Reals; y \ Reals |] ==> x \ Reals" @@ -96,37 +95,32 @@ apply (auto simp add: hypreal_of_real_hrabs) done -lemma SReal_hypreal_of_real: "hypreal_of_real x \ Reals" +lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \ Reals" by (simp add: SReal_def) -declare SReal_hypreal_of_real [simp] -lemma SReal_number_of: "(number_of w ::hypreal) \ Reals" +lemma SReal_number_of [simp]: "(number_of w ::hypreal) \ Reals" apply (simp only: hypreal_number_of [symmetric]) apply (rule SReal_hypreal_of_real) done -declare SReal_number_of [simp] (** As always with numerals, 0 and 1 are special cases **) -lemma Reals_0: "(0::hypreal) \ Reals" +lemma Reals_0 [simp]: "(0::hypreal) \ Reals" apply (subst numeral_0_eq_0 [symmetric]) apply (rule SReal_number_of) done -declare Reals_0 [simp] -lemma Reals_1: "(1::hypreal) \ Reals" +lemma Reals_1 [simp]: "(1::hypreal) \ Reals" apply (subst numeral_1_eq_1 [symmetric]) apply (rule SReal_number_of) done -declare Reals_1 [simp] lemma SReal_divide_number_of: "r \ Reals ==> r/(number_of w::hypreal) \ Reals" apply (unfold hypreal_divide_def) apply (blast intro!: SReal_number_of SReal_mult SReal_inverse) done -(* Infinitesimal epsilon not in Reals *) - +text{*epsilon is not in Reals because it is an infinitesimal*} lemma SReal_epsilon_not_mem: "epsilon \ Reals" apply (simp add: SReal_def) apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym]) @@ -163,9 +157,8 @@ apply (rule_tac x = "hypreal_of_real r" in bexI, auto) done -(*------------------------------------------------------------------ - Completeness of Reals - ------------------------------------------------------------------*) +text{*Completeness of Reals, but both lemmas are unused.*} + lemma SReal_sup_lemma: "P \ Reals ==> ((\x \ P. y < x) = (\X. hypreal_of_real X \ P & y < hypreal_of_real X))" @@ -182,14 +175,13 @@ apply (auto, rule_tac x = ya in exI, auto) done -(*------------------------------------------------------ - lifting of ub and property of lub - -------------------------------------------------------*) + +subsection{*Lifting of the Ub and Lub Properties*} + lemma hypreal_of_real_isUb_iff: "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = (isUb (UNIV :: real set) Q Y)" -apply (simp add: isUb_def setle_def) -done +by (simp add: isUb_def setle_def) lemma hypreal_of_real_isLub1: "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) @@ -215,7 +207,6 @@ (isLub (UNIV :: real set) Q Y)" by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2) -(* lemmas *) lemma lemma_isUb_hypreal_of_real: "isUb Reals P Y ==> \Yo. isUb Reals P (hypreal_of_real Yo)" by (auto simp add: SReal_iff isUb_def) @@ -233,7 +224,8 @@ ==> \t::hypreal. isLub Reals P t" apply (frule SReal_hypreal_of_real_image) apply (auto, drule lemma_isUb_hypreal_of_real) -apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff) +apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2 + simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff) done @@ -265,27 +257,23 @@ lemma HFiniteD: "x \ HFinite ==> \t \ Reals. abs x < t" by (simp add: HFinite_def) -lemma HFinite_hrabs_iff: "(abs x \ HFinite) = (x \ HFinite)" +lemma HFinite_hrabs_iff [iff]: "(abs x \ HFinite) = (x \ HFinite)" by (simp add: HFinite_def) -declare HFinite_hrabs_iff [iff] -lemma HFinite_number_of: "number_of w \ HFinite" +lemma HFinite_number_of [simp]: "number_of w \ HFinite" by (rule SReal_number_of [THEN SReal_subset_HFinite [THEN subsetD]]) -declare HFinite_number_of [simp] (** As always with numerals, 0 and 1 are special cases **) -lemma HFinite_0: "0 \ HFinite" +lemma HFinite_0 [simp]: "0 \ HFinite" apply (subst numeral_0_eq_0 [symmetric]) apply (rule HFinite_number_of) done -declare HFinite_0 [simp] -lemma HFinite_1: "1 \ HFinite" +lemma HFinite_1 [simp]: "1 \ HFinite" apply (subst numeral_1_eq_1 [symmetric]) apply (rule HFinite_number_of) done -declare HFinite_1 [simp] lemma HFinite_bounded: "[|x \ HFinite; y \ x; 0 \ y |] ==> y \ HFinite" apply (case_tac "x \ 0") @@ -302,9 +290,8 @@ "x \ Infinitesimal ==> \r \ Reals. 0 < r --> abs x < r" by (simp add: Infinitesimal_def) -lemma Infinitesimal_zero: "0 \ Infinitesimal" +lemma Infinitesimal_zero [iff]: "0 \ Infinitesimal" by (simp add: Infinitesimal_def) -declare Infinitesimal_zero [iff] lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x" by auto @@ -317,9 +304,8 @@ apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of) done -lemma Infinitesimal_minus_iff: "(-x:Infinitesimal) = (x:Infinitesimal)" +lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)" by (simp add: Infinitesimal_def) -declare Infinitesimal_minus_iff [simp] lemma Infinitesimal_diff: "[| x \ Infinitesimal; y \ Infinitesimal |] ==> x-y \ Infinitesimal" @@ -368,6 +354,9 @@ apply (auto simp add: mult_ac) done +lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \ y|] ==> r < x+y" +by (auto dest: add_less_le_mono) + lemma HInfinite_add_ge_zero: "[|x \ HInfinite; 0 \ y; 0 \ x|] ==> (x + y): HInfinite" by (auto intro!: hypreal_add_zero_less_le_mono @@ -406,9 +395,9 @@ lemma not_Infinitesimal_not_zero2: "x \ HFinite - Infinitesimal ==> x \ 0" by auto -lemma Infinitesimal_hrabs_iff: "(abs x \ Infinitesimal) = (x \ Infinitesimal)" +lemma Infinitesimal_hrabs_iff [iff]: + "(abs x \ Infinitesimal) = (x \ Infinitesimal)" by (auto simp add: abs_if) -declare Infinitesimal_hrabs_iff [iff] lemma HFinite_diff_Infinitesimal_hrabs: "x \ HFinite - Infinitesimal ==> abs x \ HFinite - Infinitesimal" @@ -486,9 +475,8 @@ lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)" by (simp add: approx_def hypreal_add_commute) -lemma approx_refl: "x @= x" +lemma approx_refl [iff]: "x @= x" by (simp add: approx_def Infinitesimal_def) -declare approx_refl [iff] lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" by (simp add: hypreal_add_commute) @@ -543,8 +531,6 @@ val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image"; val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image"; val SReal_dense = thm "SReal_dense"; -val SReal_sup_lemma = thm "SReal_sup_lemma"; -val SReal_sup_lemma2 = thm "SReal_sup_lemma2"; val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff"; val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1"; val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2"; @@ -669,11 +655,9 @@ lemma approx_minus2: "-a @= -b ==> a @= b" by (auto dest: approx_minus) -lemma approx_minus_cancel: "(-a @= -b) = (a @= b)" +lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)" by (blast intro: approx_minus approx_minus2) -declare approx_minus_cancel [simp] - lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d" by (blast intro!: approx_add approx_minus) @@ -683,8 +667,7 @@ del: minus_mult_left [symmetric]) lemma approx_mult2: "[|a @= b; c: HFinite|] ==> c*a @= c*b" -apply (simp (no_asm_simp) add: approx_mult1 hypreal_mult_commute) -done +by (simp add: approx_mult1 hypreal_mult_commute) lemma approx_mult_subst: "[|u @= v*x; x @= y; v \ HFinite|] ==> u @= v*y" by (blast intro: approx_mult2 approx_trans) @@ -756,19 +739,13 @@ done lemma approx_add_mono2: "b @= c ==> b + a @= c + a" -apply (simp (no_asm_simp) add: hypreal_add_commute approx_add_mono1) -done +by (simp add: hypreal_add_commute approx_add_mono1) -lemma approx_add_left_iff: "(a + b @= a + c) = (b @= c)" +lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)" by (fast elim: approx_add_left_cancel approx_add_mono1) -declare approx_add_left_iff [simp] - -lemma approx_add_right_iff: "(b + a @= c + a) = (b @= c)" -apply (simp (no_asm) add: hypreal_add_commute) -done - -declare approx_add_right_iff [simp] +lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)" +by (simp add: hypreal_add_commute) lemma approx_HFinite: "[| x \ HFinite; x @= y |] ==> y \ HFinite" apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe) @@ -791,8 +768,8 @@ lemma approx_mult_hypreal_of_real: "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] ==> a*c @= hypreal_of_real b*hypreal_of_real d" -apply (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite HFinite_hypreal_of_real) -done +by (blast intro!: approx_mult_HFinite approx_hypreal_of_real_HFinite + HFinite_hypreal_of_real) lemma approx_SReal_mult_cancel_zero: "[| a \ Reals; a \ 0; a*x @= 0 |] ==> x @= 0" @@ -800,17 +777,15 @@ apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric]) done -(* REM comments: newly added *) lemma approx_mult_SReal1: "[| a \ Reals; x @= 0 |] ==> x*a @= 0" by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) lemma approx_mult_SReal2: "[| a \ Reals; x @= 0 |] ==> a*x @= 0" by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) -lemma approx_mult_SReal_zero_cancel_iff: +lemma approx_mult_SReal_zero_cancel_iff [simp]: "[|a \ Reals; a \ 0 |] ==> (a*x @= 0) = (x @= 0)" by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) -declare approx_mult_SReal_zero_cancel_iff [simp] lemma approx_SReal_mult_cancel: "[| a \ Reals; a \ 0; a* w @= a*z |] ==> w @= z" @@ -818,10 +793,10 @@ apply (auto dest: approx_mult2 simp add: hypreal_mult_assoc [symmetric]) done -lemma approx_SReal_mult_cancel_iff1: +lemma approx_SReal_mult_cancel_iff1 [simp]: "[| a \ Reals; a \ 0|] ==> (a* w @= a*z) = (w @= z)" -by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel) -declare approx_SReal_mult_cancel_iff1 [simp] +by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] + intro: approx_SReal_mult_cancel) lemma approx_le_bound: "[| z \ f; f @= g; g \ z |] ==> f @= z" apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto) @@ -873,26 +848,23 @@ "hypreal_of_real x \ 0 ==> hypreal_of_real x \ HFinite - Infinitesimal" by (rule SReal_HFinite_diff_Infinitesimal, auto) -lemma hypreal_of_real_Infinitesimal_iff_0: +lemma hypreal_of_real_Infinitesimal_iff_0 [iff]: "(hypreal_of_real x \ Infinitesimal) = (x=0)" apply auto apply (rule ccontr) apply (rule hypreal_of_real_HFinite_diff_Infinitesimal [THEN DiffD2], auto) done -declare hypreal_of_real_Infinitesimal_iff_0 [iff] -lemma number_of_not_Infinitesimal: +lemma number_of_not_Infinitesimal [simp]: "number_of w \ (0::hypreal) ==> number_of w \ Infinitesimal" by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero]) -declare number_of_not_Infinitesimal [simp] (*again: 1 is a special case, but not 0 this time*) -lemma one_not_Infinitesimal: "1 \ Infinitesimal" +lemma one_not_Infinitesimal [simp]: "1 \ Infinitesimal" apply (subst numeral_1_eq_1 [symmetric]) apply (rule number_of_not_Infinitesimal) apply (simp (no_asm)) done -declare one_not_Infinitesimal [simp] lemma approx_SReal_not_zero: "[| y \ Reals; x @= y; y\ 0 |] ==> x \ 0" apply (cut_tac x = 0 and y = y in linorder_less_linear, simp) @@ -940,10 +912,9 @@ apply (simp add: hypreal_eq_minus_iff [symmetric]) done -lemma number_of_approx_iff: +lemma number_of_approx_iff [simp]: "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))" by (auto simp add: SReal_approx_iff) -declare number_of_approx_iff [simp] (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) lemma [simp]: "(0 @= number_of w) = ((number_of w :: hypreal) = 0)" @@ -953,18 +924,16 @@ "~ (0 @= 1)" "~ (1 @= 0)" by (auto simp only: SReal_number_of SReal_approx_iff Reals_0 Reals_1) -lemma hypreal_of_real_approx_iff: +lemma hypreal_of_real_approx_iff [simp]: "(hypreal_of_real k @= hypreal_of_real m) = (k = m)" apply auto apply (rule inj_hypreal_of_real [THEN injD]) apply (rule SReal_approx_iff [THEN iffD1], auto) done -declare hypreal_of_real_approx_iff [simp] -lemma hypreal_of_real_approx_number_of_iff: +lemma hypreal_of_real_approx_number_of_iff [simp]: "(hypreal_of_real k @= number_of w) = (k = number_of w)" by (subst hypreal_of_real_approx_iff [symmetric], auto) -declare hypreal_of_real_approx_number_of_iff [simp] (*And also for 0 and 1.*) (*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*) @@ -1060,25 +1029,22 @@ apply (auto dest: order_less_le_trans) done -lemma lemma_hypreal_le_swap: "((x::hypreal) \ t + r) = (x + -t \ r)" -by auto - lemma lemma_st_part1a: "[| x \ HFinite; isLub Reals {s. s \ Reals & s < x} t; r \ Reals; 0 < r |] ==> x + -t \ r" -by (blast intro!: lemma_hypreal_le_swap [THEN iffD1] lemma_st_part_le1) - -lemma lemma_hypreal_le_swap2: "(t + -r \ x) = (-(x + -t) \ (r::hypreal))" -by auto +apply (subgoal_tac "x \ t+r") +apply (auto intro: lemma_st_part_le1) +done lemma lemma_st_part2a: "[| x \ HFinite; isLub Reals {s. s \ Reals & s < x} t; r \ Reals; 0 < r |] ==> -(x + -t) \ r" -apply (blast intro!: lemma_hypreal_le_swap2 [THEN iffD1] lemma_st_part_le2) +apply (subgoal_tac "(t + -r \ x)") +apply (auto intro: lemma_st_part_le2) done lemma lemma_SReal_ub: @@ -1137,9 +1103,8 @@ ==> \r \ Reals. 0 < r --> abs (x + -t) < r" by (blast dest!: lemma_st_part_major) -(*---------------------------------------------- - Existence of real and Standard Part Theorem - ----------------------------------------------*) + +text{*Existence of real and Standard Part Theorem*} lemma lemma_st_part_Ex: "x \ HFinite ==> \t \ Reals. \r \ Reals. 0 < r --> abs (x + -t) < r" apply (frule lemma_st_part_lub, safe) @@ -1153,9 +1118,7 @@ apply (drule lemma_st_part_Ex, auto) done -(*-------------------------------- - Unique real infinitely close - -------------------------------*) +text{*There is a unique real infinitely close*} lemma st_part_Ex1: "x \ HFinite ==> EX! t. t \ Reals & x @= t" apply (drule st_part_Ex, safe) apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) @@ -1164,12 +1127,10 @@ subsection{* Finite, Infinite and Infinitesimal*} -lemma HFinite_Int_HInfinite_empty: "HFinite Int HInfinite = {}" - +lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}" apply (simp add: HFinite_def HInfinite_def) apply (auto dest: order_less_trans) done -declare HFinite_Int_HInfinite_empty [simp] lemma HFinite_not_HInfinite: assumes x: "x \ HFinite" shows "x \ HInfinite" @@ -1254,7 +1215,8 @@ "[| x \ HFinite - Infinitesimal; h \ Infinitesimal |] ==> inverse(x + h) + -inverse x @= h" apply (rule approx_trans2) -apply (auto intro: inverse_add_Infinitesimal_approx simp add: mem_infmal_iff approx_minus_iff [symmetric]) +apply (auto intro: inverse_add_Infinitesimal_approx + simp add: mem_infmal_iff approx_minus_iff [symmetric]) done lemma Infinitesimal_square_iff: "(x \ Infinitesimal) = (x*x \ Infinitesimal)" @@ -1265,15 +1227,13 @@ done declare Infinitesimal_square_iff [symmetric, simp] -lemma HFinite_square_iff: "(x*x \ HFinite) = (x \ HFinite)" +lemma HFinite_square_iff [simp]: "(x*x \ HFinite) = (x \ HFinite)" apply (auto intro: HFinite_mult) apply (auto dest: HInfinite_mult simp add: HFinite_HInfinite_iff) done -declare HFinite_square_iff [simp] -lemma HInfinite_square_iff: "(x*x \ HInfinite) = (x \ HInfinite)" +lemma HInfinite_square_iff [simp]: "(x*x \ HInfinite) = (x \ HInfinite)" by (auto simp add: HInfinite_HFinite_iff) -declare HInfinite_square_iff [simp] lemma approx_HFinite_mult_cancel: "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z" @@ -1332,10 +1292,9 @@ by (auto intro: HInfinite_gt_SReal) -lemma not_HInfinite_one: "1 \ HInfinite" +lemma not_HInfinite_one [simp]: "1 \ HInfinite" apply (simp (no_asm) add: HInfinite_HFinite_iff) done -declare not_HInfinite_one [simp] lemma approx_hrabs_disj: "abs x @= x | abs x @= -x" by (cut_tac x = x in hrabs_disj, auto) @@ -1364,19 +1323,18 @@ apply (auto simp add: monad_zero_minus_iff [symmetric]) done -lemma mem_monad_self: "x \ monad x" +lemma mem_monad_self [simp]: "x \ monad x" by (simp add: monad_def) -declare mem_monad_self [simp] + -(*------------------------------------------------------------------ - Proof that x @= y ==> abs x @= abs y - ------------------------------------------------------------------*) -lemma approx_subset_monad: "x @= y ==> {x,y}\monad x" +subsection{*Proof that @{term "x @= y"} implies @{term"\x\ @= \y\"}*} + +lemma approx_subset_monad: "x @= y ==> {x,y} \ monad x" apply (simp (no_asm)) apply (simp add: approx_monad_iff) done -lemma approx_subset_monad2: "x @= y ==> {x,y}\monad y" +lemma approx_subset_monad2: "x @= y ==> {x,y} \ monad y" apply (drule approx_sym) apply (fast dest: approx_subset_monad) done @@ -1432,24 +1390,12 @@ "[|x < 0; x \ Infinitesimal; x @= y|] ==> y < 0" by (blast dest: Ball_mem_monad_less_zero approx_subset_monad) -lemma approx_hrabs1: - "[| x @= y; x < 0; x \ Infinitesimal |] ==> abs x @= abs y" -apply (frule lemma_approx_less_zero) -apply (assumption+) -apply (simp add: abs_if) -done - -lemma approx_hrabs2: - "[| x @= y; 0 < x; x \ Infinitesimal |] ==> abs x @= abs y" -apply (frule lemma_approx_gt_zero) -apply (assumption+) -apply (simp add: abs_if) -done - -lemma approx_hrabs: "x @= y ==> abs x @= abs y" -apply (rule_tac Q = "x \ Infinitesimal" in excluded_middle [THEN disjE]) -apply (rule_tac x1 = x and y1 = 0 in linorder_less_linear [THEN disjE]) -apply (auto intro: approx_hrabs1 approx_hrabs2 Infinitesimal_approx_hrabs) +theorem approx_hrabs: "x @= y ==> abs x @= abs y" +apply (case_tac "x \ Infinitesimal") +apply (simp add: Infinitesimal_approx_hrabs) +apply (rule linorder_cases [of 0 x]) +apply (frule lemma_approx_gt_zero [of x y]) +apply (auto simp add: lemma_approx_less_zero [of x y]) done lemma approx_hrabs_zero_cancel: "abs(x) @= 0 ==> x @= 0" @@ -1480,9 +1426,6 @@ apply (auto intro: approx_trans2) done -lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" -by arith - (* interesting slightly counterintuitive theorem: necessary for proving that an open interval is an NS open set *) @@ -1500,7 +1443,8 @@ ==> abs (hypreal_of_real r + x) < hypreal_of_real y" apply (drule_tac x = "hypreal_of_real r" in approx_hrabs_add_Infinitesimal) apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]]) -apply (auto intro!: Infinitesimal_add_hypreal_of_real_less simp add: hypreal_of_real_hrabs) +apply (auto intro!: Infinitesimal_add_hypreal_of_real_less + simp add: hypreal_of_real_hrabs) done lemma Infinitesimal_add_hrabs_hypreal_of_real_less2: @@ -1523,11 +1467,11 @@ "[| u \ Infinitesimal; v \ Infinitesimal; hypreal_of_real x + u \ hypreal_of_real y + v |] ==> x \ y" -apply (blast intro!: hypreal_of_real_le_iff [THEN iffD1] hypreal_of_real_le_add_Infininitesimal_cancel) -done +by (blast intro!: hypreal_of_real_le_iff [THEN iffD1] + hypreal_of_real_le_add_Infininitesimal_cancel) lemma hypreal_of_real_less_Infinitesimal_le_zero: - "[| hypreal_of_real x < e; e \ Infinitesimal |] ==> hypreal_of_real x \ 0" + "[| hypreal_of_real x < e; e \ Infinitesimal |] ==> hypreal_of_real x \ 0" apply (rule linorder_not_less [THEN iffD1], safe) apply (drule Infinitesimal_interval) apply (drule_tac [4] SReal_hypreal_of_real [THEN SReal_Infinitesimal_zero], auto) @@ -1540,81 +1484,73 @@ apply (subgoal_tac "h = - hypreal_of_real x", auto) done -lemma Infinitesimal_square_cancel: +lemma Infinitesimal_square_cancel [simp]: "x*x + y*y \ Infinitesimal ==> x*x \ Infinitesimal" apply (rule Infinitesimal_interval2) apply (rule_tac [3] zero_le_square, assumption) apply (auto simp add: zero_le_square) done -declare Infinitesimal_square_cancel [simp] -lemma HFinite_square_cancel: "x*x + y*y \ HFinite ==> x*x \ HFinite" +lemma HFinite_square_cancel [simp]: "x*x + y*y \ HFinite ==> x*x \ HFinite" apply (rule HFinite_bounded, assumption) apply (auto simp add: zero_le_square) done -declare HFinite_square_cancel [simp] -lemma Infinitesimal_square_cancel2: +lemma Infinitesimal_square_cancel2 [simp]: "x*x + y*y \ Infinitesimal ==> y*y \ Infinitesimal" apply (rule Infinitesimal_square_cancel) apply (rule hypreal_add_commute [THEN subst]) apply (simp (no_asm)) done -declare Infinitesimal_square_cancel2 [simp] -lemma HFinite_square_cancel2: "x*x + y*y \ HFinite ==> y*y \ HFinite" +lemma HFinite_square_cancel2 [simp]: "x*x + y*y \ HFinite ==> y*y \ HFinite" apply (rule HFinite_square_cancel) apply (rule hypreal_add_commute [THEN subst]) apply (simp (no_asm)) done -declare HFinite_square_cancel2 [simp] -lemma Infinitesimal_sum_square_cancel: +lemma Infinitesimal_sum_square_cancel [simp]: "x*x + y*y + z*z \ Infinitesimal ==> x*x \ Infinitesimal" apply (rule Infinitesimal_interval2, assumption) apply (rule_tac [2] zero_le_square, simp) apply (insert zero_le_square [of y]) apply (insert zero_le_square [of z], simp) done -declare Infinitesimal_sum_square_cancel [simp] -lemma HFinite_sum_square_cancel: "x*x + y*y + z*z \ HFinite ==> x*x \ HFinite" +lemma HFinite_sum_square_cancel [simp]: + "x*x + y*y + z*z \ HFinite ==> x*x \ HFinite" apply (rule HFinite_bounded, assumption) apply (rule_tac [2] zero_le_square) apply (insert zero_le_square [of y]) apply (insert zero_le_square [of z], simp) done -declare HFinite_sum_square_cancel [simp] -lemma Infinitesimal_sum_square_cancel2: +lemma Infinitesimal_sum_square_cancel2 [simp]: "y*y + x*x + z*z \ Infinitesimal ==> x*x \ Infinitesimal" apply (rule Infinitesimal_sum_square_cancel) apply (simp add: add_ac) done -declare Infinitesimal_sum_square_cancel2 [simp] -lemma HFinite_sum_square_cancel2: +lemma HFinite_sum_square_cancel2 [simp]: "y*y + x*x + z*z \ HFinite ==> x*x \ HFinite" apply (rule HFinite_sum_square_cancel) apply (simp add: add_ac) done -declare HFinite_sum_square_cancel2 [simp] -lemma Infinitesimal_sum_square_cancel3: +lemma Infinitesimal_sum_square_cancel3 [simp]: "z*z + y*y + x*x \ Infinitesimal ==> x*x \ Infinitesimal" apply (rule Infinitesimal_sum_square_cancel) apply (simp add: add_ac) done -declare Infinitesimal_sum_square_cancel3 [simp] -lemma HFinite_sum_square_cancel3: +lemma HFinite_sum_square_cancel3 [simp]: "z*z + y*y + x*x \ HFinite ==> x*x \ HFinite" apply (rule HFinite_sum_square_cancel) apply (simp add: add_ac) done -declare HFinite_sum_square_cancel3 [simp] -lemma monad_hrabs_less: "[| y \ monad x; 0 < hypreal_of_real e |] +lemma monad_hrabs_less: + "[| y \ monad x; 0 < hypreal_of_real e |] ==> abs (y + -x) < hypreal_of_real e" apply (drule mem_monad_approx [THEN approx_sym]) apply (drule bex_Infinitesimal_iff [THEN iffD2]) @@ -1656,8 +1592,7 @@ apply (blast dest: SReal_approx_iff [THEN iffD1]) done -(* ???should be added to simpset *) -lemma st_hypreal_of_real: "st (hypreal_of_real x) = hypreal_of_real x" +lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x" by (rule SReal_hypreal_of_real [THEN st_SReal_eq]) lemma st_eq_approx: "[| x \ HFinite; y \ HFinite; st x = st y |] ==> x @= y" @@ -1718,9 +1653,8 @@ finally show ?thesis . qed -lemma st_number_of: "st (number_of w) = number_of w" +lemma st_number_of [simp]: "st (number_of w) = number_of w" by (rule SReal_number_of [THEN st_SReal_eq]) -declare st_number_of [simp] (*the theorem above for the special cases of zero and one*) lemma [simp]: "st 0 = 0" "st 1 = 1" @@ -1740,7 +1674,6 @@ apply (simp (no_asm_simp) add: st_add) done -(* lemma *) lemma lemma_st_mult: "[| x \ HFinite; y \ HFinite; e \ Infinitesimal; ea \ Infinitesimal |] ==> e*y + x*ea + e*ea \ Infinitesimal" @@ -1787,16 +1720,13 @@ apply (subst hypreal_mult_inverse, auto) done -lemma st_divide: +lemma st_divide [simp]: "[| x \ HFinite; y \ HFinite; st y \ 0 |] ==> st(x/y) = (st x) / (st y)" -apply (auto simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse) -done -declare st_divide [simp] +by (simp add: hypreal_divide_def st_mult st_not_Infinitesimal HFinite_inverse st_inverse) -lemma st_idempotent: "x \ HFinite ==> st(st(x)) = st(x)" +lemma st_idempotent [simp]: "x \ HFinite ==> st(st(x)) = st(x)" by (blast intro: st_HFinite st_approx_self approx_st_eq) -declare st_idempotent [simp] lemma Infinitesimal_add_st_less: "[| x \ HFinite; y \ HFinite; u \ Infinitesimal; st x < st y |] @@ -2021,10 +1951,10 @@ done -(*------------------------------------------------------------------------- - Proof that omega is an infinite number and - hence that epsilon is an infinitesimal number. - -------------------------------------------------------------------------*) +subsection{*Proof that @{term omega} is an infinite number*} + +text{*It will follow that epsilon is an infinitesimal number.*} + lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}" by (auto simp add: less_Suc_eq) @@ -2077,9 +2007,7 @@ lemma Compl_real_le_eq: "- {n::nat. real n \ u} = {n. u < real n}" by (auto dest!: order_le_less_trans simp add: linorder_not_le) -(*----------------------------------------------- - Omega is a member of HInfinite - -----------------------------------------------*) +text{*@{term omega} is a member of @{term HInfinite}*} lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \ hypreal" by auto @@ -2089,31 +2017,27 @@ apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq) done -lemma HInfinite_omega: "omega: HInfinite" +theorem HInfinite_omega [simp]: "omega \ HInfinite" apply (simp add: omega_def) apply (auto intro!: FreeUltrafilterNat_HInfinite) apply (rule bexI) apply (rule_tac [2] lemma_hyprel_refl, auto) apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega) done -declare HInfinite_omega [simp] (*----------------------------------------------- Epsilon is a member of Infinitesimal -----------------------------------------------*) -lemma Infinitesimal_epsilon: "epsilon \ Infinitesimal" +lemma Infinitesimal_epsilon [simp]: "epsilon \ Infinitesimal" by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega simp add: hypreal_epsilon_inverse_omega) -declare Infinitesimal_epsilon [simp] -lemma HFinite_epsilon: "epsilon \ HFinite" +lemma HFinite_epsilon [simp]: "epsilon \ HFinite" by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) -declare HFinite_epsilon [simp] -lemma epsilon_approx_zero: "epsilon @= 0" +lemma epsilon_approx_zero [simp]: "epsilon @= 0" apply (simp (no_asm) add: mem_infmal_iff [symmetric]) done -declare epsilon_approx_zero [simp] (*------------------------------------------------------------------------ Needed for proof that we define a hyperreal [n. 0 \ f n) --> 0 \ sumr m n f" -apply (induct_tac "n", auto) -apply (drule_tac x = n in spec, arith) -done - -lemma sumr_ge_zero2 [rule_format (no_asm)]: - "(\n. m \ n --> 0 \ f n) --> 0 \ sumr m n f" +lemma sumr_ge_zero [rule_format]: "(\n. m \ n --> 0 \ f n) --> 0 \ sumr m n f" apply (induct_tac "n", auto) apply (drule_tac x = n in spec, arith) done lemma rabs_sumr_rabs_cancel [simp]: - "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))" -apply (induct_tac "n") -apply (auto, arith) -done + "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" +by (induct_tac "n", simp_all add: add_increasing) lemma sumr_zero [rule_format]: "\n. N \ n --> f n = 0 ==> N \ m --> sumr m n f = 0" @@ -480,9 +472,6 @@ val sumr_diff_mult_const = thm "sumr_diff_mult_const"; val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero"; val sumr_le2 = thm "sumr_le2"; -val sumr_ge_zero = thm "sumr_ge_zero"; -val sumr_ge_zero2 = thm "sumr_ge_zero2"; -val sumr_rabs_ge_zero = thm "sumr_rabs_ge_zero"; val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel"; val sumr_zero = thm "sumr_zero"; val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2"; diff -r 4d332d10fa3d -r 1eb23f805c06 src/HOL/Hyperreal/Transcendental.thy --- a/src/HOL/Hyperreal/Transcendental.thy Mon Oct 04 15:28:03 2004 +0200 +++ b/src/HOL/Hyperreal/Transcendental.thy Tue Oct 05 15:30:50 2004 +0200 @@ -52,13 +52,13 @@ lemma real_root_zero [simp]: "root (Suc n) 0 = 0" -apply (unfold root_def) +apply (simp add: root_def) apply (safe intro!: some_equality power_0_Suc elim!: realpow_zero_zero) done lemma real_root_pow_pos: "0 < x ==> (root(Suc n) x) ^ (Suc n) = x" -apply (unfold root_def) +apply (simp add: root_def) apply (drule_tac n = n in realpow_pos_nth2) apply (auto intro: someI2) done @@ -68,7 +68,7 @@ lemma real_root_pos: "0 < x ==> root(Suc n) (x ^ (Suc n)) = x" -apply (unfold root_def) +apply (simp add: root_def) apply (rule some_equality) apply (frule_tac [2] n = n in zero_less_power) apply (auto simp add: zero_less_mult_iff) @@ -83,17 +83,18 @@ lemma real_root_pos_pos: "0 < x ==> 0 \ root(Suc n) x" -apply (unfold root_def) +apply (simp add: root_def) apply (drule_tac n = n in realpow_pos_nth2) apply (safe, rule someI2) -apply (auto intro!: order_less_imp_le dest: zero_less_power simp add: zero_less_mult_iff) +apply (auto intro!: order_less_imp_le dest: zero_less_power + simp add: zero_less_mult_iff) done lemma real_root_pos_pos_le: "0 \ x ==> 0 \ root(Suc n) x" by (auto dest!: real_le_imp_less_or_eq dest: real_root_pos_pos) lemma real_root_one [simp]: "root (Suc n) 1 = 1" -apply (unfold root_def) +apply (simp add: root_def) apply (rule some_equality, auto) apply (rule ccontr) apply (rule_tac x = u and y = 1 in linorder_cases) @@ -105,19 +106,19 @@ subsection{*Square Root*} -(*lcp: needed now because 2 is a binary numeral!*) +text{*needed because 2 is a binary numeral!*} lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))" -apply (simp (no_asm) del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 add: nat_numeral_0_eq_0 [symmetric]) -done +by (simp del: nat_numeral_0_eq_0 nat_numeral_1_eq_1 + add: nat_numeral_0_eq_0 [symmetric]) lemma real_sqrt_zero [simp]: "sqrt 0 = 0" -by (unfold sqrt_def, auto) +by (simp add: sqrt_def) lemma real_sqrt_one [simp]: "sqrt 1 = 1" -by (unfold sqrt_def, auto) +by (simp add: sqrt_def) lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\ = x) = (0 \ x)" -apply (unfold sqrt_def) +apply (simp add: sqrt_def) apply (rule iffI) apply (cut_tac r = "root 2 x" in realpow_two_le) apply (simp add: numeral_2_eq_2) @@ -136,7 +137,7 @@ lemma real_pow_sqrt_eq_sqrt_pow: "0 \ x ==> (sqrt x)\ = sqrt(x\)" -apply (unfold sqrt_def) +apply (simp add: sqrt_def) apply (subst numeral_2_eq_2) apply (auto intro: real_root_pow_pos2 [THEN ssubst] real_root_pos2 [THEN ssubst] simp del: realpow_Suc) done @@ -162,8 +163,7 @@ by auto lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)" -apply (unfold sqrt_def root_def) -apply (subst numeral_2_eq_2) +apply (simp add: sqrt_def root_def) apply (drule realpow_pos_nth2 [where n=1], safe) apply (rule someI2, auto) done @@ -178,7 +178,7 @@ (*we need to prove something like this: lemma "[|r ^ n = a; 0 0 < r|] ==> root n a = r" apply (case_tac n, simp) -apply (unfold root_def) +apply (simp add: root_def) apply (rule someI2 [of _ r], safe) apply (auto simp del: realpow_Suc dest: power_inject_base) *) @@ -197,13 +197,15 @@ apply (simp add: zero_le_mult_iff real_sqrt_ge_zero) done -lemma real_sqrt_mult_distrib2: "[|0\x; 0\y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)" +lemma real_sqrt_mult_distrib2: + "[|0\x; 0\y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)" by (auto intro: real_sqrt_mult_distrib simp add: order_le_less) lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \ sqrt (x\ + y\)" by (auto intro!: real_sqrt_ge_zero) -lemma real_sqrt_sum_squares_mult_ge_zero [simp]: "0 \ sqrt ((x\ + y\)*(xa\ + ya\))" +lemma real_sqrt_sum_squares_mult_ge_zero [simp]: + "0 \ sqrt ((x\ + y\)*(xa\ + ya\))" by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff) lemma real_sqrt_sum_squares_mult_squared_eq [simp]: @@ -239,7 +241,7 @@ apply (auto dest: real_sqrt_not_eq_zero) done -lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \ x ==> ((sqrt x = 0) = (x = 0))" +lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \ x ==> ((sqrt x = 0) = (x=0))" by (auto simp add: real_sqrt_eq_zero_cancel) lemma real_sqrt_sum_squares_ge1 [simp]: "x \ sqrt(x\ + y\)" @@ -274,9 +276,9 @@ apply (subst fact_Suc) apply (subst real_of_nat_mult) apply (auto simp add: abs_mult inverse_mult_distrib) -apply (auto simp add: mult_assoc [symmetric] abs_eqI2 positive_imp_inverse_positive) +apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive) apply (rule order_less_imp_le) -apply (rule_tac z1 = "real (Suc na) " in real_mult_less_iff1 [THEN iffD1]) +apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1]) apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse) apply (erule order_less_trans) apply (auto simp add: mult_less_cancel_left mult_ac) @@ -288,40 +290,39 @@ (if even n then 0 else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n)" -apply (unfold real_divide_def) -apply (rule_tac g = " (%n. inverse (real (fact n)) * \x\ ^ n) " in summable_comparison_test) +apply (rule_tac g = "(%n. inverse (real (fact n)) * \x\ ^ n)" in summable_comparison_test) apply (rule_tac [2] summable_exp) apply (rule_tac x = 0 in exI) -apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff) +apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff) done lemma summable_cos: "summable (%n. (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n)" -apply (unfold real_divide_def) -apply (rule_tac g = " (%n. inverse (real (fact n)) * \x\ ^ n) " in summable_comparison_test) +apply (rule_tac g = "(%n. inverse (real (fact n)) * \x\ ^ n)" in summable_comparison_test) apply (rule_tac [2] summable_exp) apply (rule_tac x = 0 in exI) -apply (auto simp add: power_abs [symmetric] abs_mult zero_le_mult_iff) +apply (auto simp add: divide_inverse power_abs [symmetric] zero_le_mult_iff) done -lemma lemma_STAR_sin [simp]: "(if even n then 0 +lemma lemma_STAR_sin [simp]: + "(if even n then 0 else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0" -apply (induct_tac "n", auto) -done - -lemma lemma_STAR_cos [simp]: "0 < n --> +by (induct_tac "n", auto) + +lemma lemma_STAR_cos [simp]: + "0 < n --> (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" -apply (induct_tac "n", auto) -done - -lemma lemma_STAR_cos1 [simp]: "0 < n --> +by (induct_tac "n", auto) + +lemma lemma_STAR_cos1 [simp]: + "0 < n --> (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" -apply (induct_tac "n", auto) -done - -lemma lemma_STAR_cos2 [simp]: "sumr 1 n (%n. if even n +by (induct_tac "n", auto) + +lemma lemma_STAR_cos2 [simp]: + "sumr 1 n (%n. if even n then (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n else 0) = 0" @@ -330,7 +331,7 @@ done lemma exp_converges: "(%n. inverse (real (fact n)) * x ^ n) sums exp(x)" -apply (unfold exp_def) +apply (simp add: exp_def) apply (rule summable_exp [THEN summable_sums]) done @@ -338,7 +339,7 @@ "(%n. (if even n then 0 else (- 1) ^ ((n - Suc 0) div 2)/(real (fact n))) * x ^ n) sums sin(x)" -apply (unfold sin_def) +apply (simp add: sin_def) apply (rule summable_sin [THEN summable_sums]) done @@ -346,11 +347,12 @@ "(%n. (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) * x ^ n) sums cos(x)" -apply (unfold cos_def) +apply (simp add: cos_def) apply (rule summable_cos [THEN summable_sums]) done -lemma lemma_realpow_diff [rule_format (no_asm)]: "p \ n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y" +lemma lemma_realpow_diff [rule_format (no_asm)]: + "p \ n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y" apply (induct_tac "n", auto) apply (subgoal_tac "p = Suc n") apply (simp (no_asm_simp), auto) @@ -372,16 +374,18 @@ apply (auto simp add: mult_ac) done -lemma lemma_realpow_diff_sumr2: "x ^ (Suc n) - y ^ (Suc n) = +lemma lemma_realpow_diff_sumr2: + "x ^ (Suc n) - y ^ (Suc n) = (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))" apply (induct_tac "n", simp) apply (auto simp del: sumr_Suc) apply (subst sumr_Suc) apply (drule sym) -apply (auto simp add: lemma_realpow_diff_sumr right_distrib real_diff_def mult_ac simp del: sumr_Suc) +apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc) done -lemma lemma_realpow_rev_sumr: "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) = +lemma lemma_realpow_rev_sumr: + "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) = sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))" apply (case_tac "x = y") apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc) @@ -413,7 +417,7 @@ apply (rule_tac a2 = "z ^ n" in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE]) apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left) -apply (rule_tac x = "K * inverse (1 - (\z\ * inverse (\x\))) " in exI) +apply (rule_tac x = "K * inverse (1 - (\z\ * inverse (\x\)))" in exI) apply (auto intro!: sums_mult simp add: mult_assoc) apply (subgoal_tac "\z ^ n\ * inverse (\x\ ^ n) = (\z\ * inverse (\x\)) ^ n") apply (auto simp add: power_abs [symmetric]) @@ -425,7 +429,8 @@ apply (auto simp add: abs_mult [symmetric] mult_assoc) done -lemma powser_inside: "[| summable (%n. f(n) * (x ^ n)); \z\ < \x\ |] +lemma powser_inside: + "[| summable (%n. f(n) * (x ^ n)); \z\ < \x\ |] ==> summable (%n. f(n) * (z ^ n))" apply (drule_tac z = "\z\" in powser_insidea) apply (auto intro: summable_rabs_cancel simp add: power_abs [symmetric]) @@ -447,13 +452,15 @@ apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def) done -lemma lemma_diffs2: "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) = +lemma lemma_diffs2: + "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) = sumr 0 n (%n. (diffs c)(n) * (x ^ n)) - (real n * c(n) * x ^ (n - Suc 0))" by (auto simp add: lemma_diffs) -lemma diffs_equiv: "summable (%n. (diffs c)(n) * (x ^ n)) ==> +lemma diffs_equiv: + "summable (%n. (diffs c)(n) * (x ^ n)) ==> (%n. real n * c(n) * (x ^ (n - Suc 0))) sums (suminf(%n. (diffs c)(n) * (x ^ n)))" apply (subgoal_tac " (%n. real n * c (n) * (x ^ (n - Suc 0))) ----> 0") @@ -473,7 +480,7 @@ sumr 0 m (%p. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))" apply (rule sumr_subst) -apply (auto simp add: right_distrib real_diff_def power_add [symmetric] mult_ac) +apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac) done lemma less_add_one: "m < n ==> (\d. n = m + d + Suc 0)" @@ -483,7 +490,8 @@ by arith -lemma lemma_termdiff2: " h \ 0 ==> +lemma lemma_termdiff2: + " h \ 0 ==> (((z + h) ^ n) - (z ^ n)) * inverse h - real n * (z ^ (n - Suc 0)) = h * sumr 0 (n - Suc 0) (%p. (z ^ p) * @@ -499,13 +507,14 @@ apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc) apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib sumdiff lemma_termdiff1 sumr_mult) -apply (auto intro!: sumr_subst simp add: real_diff_def real_add_assoc) +apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc) apply (simp add: diff_minus [symmetric] less_iff_Suc_add) apply (auto simp add: sumr_mult lemma_realpow_diff_sumr2 mult_ac simp del: sumr_Suc realpow_Suc) done -lemma lemma_termdiff3: "[| h \ 0; \z\ \ K; \z + h\ \ K |] +lemma lemma_termdiff3: + "[| h \ 0; \z\ \ K; \z + h\ \ K |] ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0)) \ real n * real (n - Suc 0) * K ^ (n - 2) * \h\" apply (subst lemma_termdiff2, assumption) @@ -524,7 +533,7 @@ apply (simp (no_asm_simp) add: power_add del: sumr_Suc) apply (auto intro!: mult_mono simp del: sumr_Suc) apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc) -apply (rule_tac j = "real (Suc d) * (K ^ d) " in real_le_trans) +apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans) apply (subgoal_tac [2] "0 \ K") apply (drule_tac [2] n = d in zero_le_power) apply (auto simp del: sumr_Suc) @@ -537,29 +546,28 @@ "[| 0 < k; (\h. 0 < \h\ & \h\ < k --> \f h\ \ K * \h\) |] ==> f -- 0 --> 0" -apply (unfold LIM_def, auto) +apply (simp add: LIM_def, auto) apply (subgoal_tac "0 \ K") -apply (drule_tac [2] x = "k/2" in spec) -apply (frule_tac [2] real_less_half_sum) -apply (drule_tac [2] real_gt_half_sum) -apply (auto simp add: abs_eqI2) -apply (rule_tac [2] c = "k/2" in mult_right_le_imp_le) -apply (auto intro: abs_ge_zero [THEN real_le_trans]) + prefer 2 + apply (drule_tac x = "k/2" in spec) +apply (simp add: ); + apply (subgoal_tac "0 \ K*k", simp add: zero_le_mult_iff) + apply (force intro: order_trans [of _ "\f (k / 2)\ * 2"]) apply (drule real_le_imp_less_or_eq, auto) -apply (subgoal_tac "0 < (r * inverse K) * inverse 2") -apply (rule_tac [2] real_mult_order)+ -apply (drule_tac ?d1.0 = "r * inverse K * inverse 2" and ?d2.0 = k in real_lbound_gt_zero) -apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff) -apply (rule_tac [2] y="\f (k / 2)\ * 2" in order_trans, auto) +apply (subgoal_tac "0 < (r * inverse K) / 2") +apply (drule_tac ?d1.0 = "(r * inverse K) / 2" and ?d2.0 = k in real_lbound_gt_zero) +apply (auto simp add: positive_imp_inverse_positive zero_less_mult_iff zero_less_divide_iff) apply (rule_tac x = e in exI, auto) apply (rule_tac y = "K * \x\" in order_le_less_trans) -apply (rule_tac [2] y = "K * e" in order_less_trans) -apply (rule_tac [3] c = "inverse K" in mult_right_less_imp_less, force) +apply (force ); +apply (rule_tac y = "K * e" in order_less_trans) apply (simp add: mult_less_cancel_left) +apply (rule_tac c = "inverse K" in mult_right_less_imp_less) apply (auto simp add: mult_ac) done -lemma lemma_termdiff5: "[| 0 < k; +lemma lemma_termdiff5: + "[| 0 < k; summable f; \h. 0 < \h\ & \h\ < k --> (\n. abs(g(h) (n::nat)) \ (f(n) * \h\)) |] @@ -602,7 +610,7 @@ apply (subgoal_tac "summable (%n. \diffs (diffs c) n\ * (r ^ n))") apply (rule_tac [2] x = K in powser_insidea, auto) apply (subgoal_tac [2] "\r\ = r", auto) -apply (rule_tac [2] y1 = "\x\" in order_trans [THEN abs_eqI1], auto) +apply (rule_tac [2] y1 = "\x\" in order_trans [THEN abs_eq], auto) apply (simp add: diffs_def mult_assoc [symmetric]) apply (subgoal_tac "\n. real (Suc n) * real (Suc (Suc n)) * \c (Suc (Suc n))\ * (r ^ n) @@ -640,7 +648,8 @@ apply (drule abs_ge_zero [THEN order_le_less_trans]) apply (simp add: mult_assoc) apply (rule mult_left_mono) -apply (rule add_commute [THEN subst]) + prefer 2 apply arith +apply (subst add_commute) apply (simp (no_asm) add: mult_assoc [symmetric]) apply (rule lemma_termdiff3) apply (auto intro: abs_triangle_ineq [THEN order_trans], arith) @@ -654,8 +663,8 @@ \x\ < \K\ |] ==> DERIV (%x. suminf (%n. c(n) * (x ^ n))) x :> suminf (%n. (diffs c)(n) * (x ^ n))" -apply (unfold deriv_def) -apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h) " in LIM_trans) +apply (simp add: deriv_def) +apply (rule_tac g = "%h. suminf (%n. ((c (n) * ( (x + h) ^ n)) - (c (n) * (x ^ n))) * inverse h)" in LIM_trans) apply (simp add: LIM_def, safe) apply (rule_tac x = "\K\ - \x\" in exI) apply (auto simp add: less_diff_eq) @@ -666,11 +675,11 @@ apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside) apply (auto simp add: add_commute) apply (drule_tac x="(\n. c n * (xa + x) ^ n)" in sums_diff, assumption) -apply (drule_tac x = " (%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult) +apply (drule_tac x = "(%n. c n * (xa + x) ^ n - c n * x ^ n) " and c = "inverse xa" in sums_mult) apply (rule sums_unique) apply (simp add: diff_def divide_inverse add_ac mult_ac) apply (rule LIM_zero_cancel) -apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))) " in LIM_trans) +apply (rule_tac g = "%h. suminf (%n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0)))))" in LIM_trans) prefer 2 apply (blast intro: termdiffs_aux) apply (simp add: LIM_def, safe) apply (rule_tac x = "\K\ - \x\" in exI) @@ -686,12 +695,12 @@ apply (auto intro!: summable_sums) apply (rule_tac [2] powser_inside, rule_tac [4] powser_inside) apply (auto simp add: add_commute) -apply (frule_tac x = " (%n. c n * (xa + x) ^ n) " and y = " (%n. c n * x ^ n) " in sums_diff, assumption) +apply (frule_tac x = "(%n. c n * (xa + x) ^ n) " and y = "(%n. c n * x ^ n)" in sums_diff, assumption) apply (simp add: suminf_diff [OF sums_summable sums_summable] right_diff_distrib [symmetric]) -apply (frule_tac x = " (%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult) +apply (frule_tac x = "(%n. c n * ((xa + x) ^ n - x ^ n))" and c = "inverse xa" in sums_mult) apply (simp add: sums_summable [THEN suminf_mult2]) -apply (frule_tac x = " (%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = " (%n. real n * c n * x ^ (n - Suc 0))" in sums_diff) +apply (frule_tac x = "(%n. inverse xa * (c n * ((xa + x) ^ n - x ^ n))) " and y = "(%n. real n * c n * x ^ (n - Suc 0))" in sums_diff) apply assumption apply (simp add: suminf_diff [OF sums_summable sums_summable] add_ac mult_ac) apply (rule_tac f = suminf in arg_cong) @@ -704,13 +713,7 @@ lemma exp_fdiffs: "diffs (%n. inverse(real (fact n))) = (%n. inverse(real (fact n)))" -apply (unfold diffs_def) -apply (rule ext) -apply (subst fact_Suc) -apply (subst real_of_nat_mult) -apply (subst inverse_mult_distrib) -apply (auto simp add: mult_assoc [symmetric]) -done +by (simp add: diffs_def mult_assoc [symmetric] del: mult_Suc) lemma sin_fdiffs: "diffs(%n. if even n then 0 @@ -718,13 +721,8 @@ = (%n. if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0)" -apply (unfold diffs_def real_divide_def) -apply (rule ext) -apply (subst fact_Suc) -apply (subst real_of_nat_mult) -apply (subst even_nat_Suc) -apply (subst inverse_mult_distrib, auto) -done +by (auto intro!: ext + simp add: diffs_def divide_inverse simp del: mult_Suc) lemma sin_fdiffs2: "diffs(%n. if even n then 0 @@ -732,24 +730,17 @@ = (if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0)" -apply (unfold diffs_def real_divide_def) -apply (subst fact_Suc) -apply (subst real_of_nat_mult) -apply (subst even_nat_Suc) -apply (subst inverse_mult_distrib, auto) -done +by (auto intro!: ext + simp add: diffs_def divide_inverse simp del: mult_Suc) lemma cos_fdiffs: "diffs(%n. if even n then (- 1) ^ (n div 2)/(real (fact n)) else 0) = (%n. - (if even n then 0 else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n))))" -apply (unfold diffs_def real_divide_def) -apply (rule ext) -apply (subst fact_Suc) -apply (subst real_of_nat_mult) -apply (auto simp add: mult_assoc odd_Suc_mult_two_ex) -done +by (auto intro!: ext + simp add: diffs_def divide_inverse odd_Suc_mult_two_ex + simp del: mult_Suc) lemma cos_fdiffs2: @@ -757,11 +748,9 @@ (- 1) ^ (n div 2)/(real (fact n)) else 0) n = - (if even n then 0 else (- 1) ^ ((n - Suc 0)div 2)/(real (fact n)))" -apply (unfold diffs_def real_divide_def) -apply (subst fact_Suc) -apply (subst real_of_nat_mult) -apply (auto simp add: mult_assoc odd_Suc_mult_two_ex) -done +by (auto intro!: ext + simp add: diffs_def divide_inverse odd_Suc_mult_two_ex + simp del: mult_Suc) text{*Now at last we can get the derivatives of exp, sin and cos*} @@ -775,10 +764,10 @@ by (auto intro!: ext simp add: exp_def) lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)" -apply (unfold exp_def) +apply (simp add: exp_def) apply (subst lemma_exp_ext) apply (subgoal_tac "DERIV (%u. suminf (%n. inverse (real (fact n)) * u ^ n)) x :> suminf (%n. diffs (%n. inverse (real (fact n))) n * x ^ n) ") -apply (rule_tac [2] K = "1 + \x\ " in termdiffs) +apply (rule_tac [2] K = "1 + \x\" in termdiffs) apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith) done @@ -796,17 +785,17 @@ by (auto intro!: ext simp add: cos_def) lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)" -apply (unfold cos_def) +apply (simp add: cos_def) apply (subst lemma_sin_ext) apply (auto simp add: sin_fdiffs2 [symmetric]) -apply (rule_tac K = "1 + \x\ " in termdiffs) +apply (rule_tac K = "1 + \x\" in termdiffs) apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith) done lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)" apply (subst lemma_cos_ext) apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left) -apply (rule_tac K = "1 + \x\ " in termdiffs) +apply (rule_tac K = "1 + \x\" in termdiffs) apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith) done @@ -824,9 +813,9 @@ lemma exp_ge_add_one_self [simp]: "0 \ x ==> (1 + x) \ exp(x)" apply (drule real_le_imp_less_or_eq, auto) -apply (unfold exp_def) +apply (simp add: exp_def) apply (rule real_le_trans) -apply (rule_tac [2] n = 2 and f = " (%n. inverse (real (fact n)) * x ^ n) " in series_pos_le) +apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le) apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff) done @@ -902,7 +891,7 @@ by (auto intro: positive_imp_inverse_positive) lemma abs_exp_cancel [simp]: "\exp x\ = exp x" -by (auto simp add: abs_eqI2) +by auto lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" apply (induct_tac "n") @@ -910,7 +899,7 @@ done lemma exp_diff: "exp(x - y) = exp(x)/(exp y)" -apply (unfold real_diff_def real_divide_def) +apply (simp add: diff_minus divide_inverse) apply (simp (no_asm) add: exp_add exp_minus) done @@ -992,7 +981,7 @@ lemma ln_div: "[|0 < x; 0 < y|] ==> ln(x/y) = ln x - ln y" -apply (unfold real_divide_def) +apply (simp add: divide_inverse) apply (auto simp add: positive_imp_inverse_positive ln_mult ln_inverse) done @@ -1086,9 +1075,9 @@ by (auto intro: series_zero) lemma cos_zero [simp]: "cos 0 = 1" -apply (unfold cos_def) +apply (simp add: cos_def) apply (rule sums_unique [symmetric]) -apply (cut_tac n = 1 and f = " (%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n) " in lemma_series_zero2) +apply (cut_tac n = 1 and f = "(%n. (if even n then (- 1) ^ (n div 2) / (real (fact n)) else 0) * 0 ^ n)" in lemma_series_zero2) apply auto done @@ -1137,7 +1126,8 @@ done (* most useful *) -lemma DERIV_cos_cos_mult3 [simp]: "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))" +lemma DERIV_cos_cos_mult3 [simp]: + "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))" apply (rule lemma_DERIV_subst) apply (rule DERIV_cos_cos_mult2, auto) done @@ -1145,12 +1135,13 @@ lemma DERIV_sin_circle_all: "\x. DERIV (%x. (sin x)\ + (cos x)\) x :> (2*cos(x)*sin(x) - 2*cos(x)*sin(x))" -apply (unfold real_diff_def, safe) -apply (rule DERIV_add) +apply (simp only: diff_minus, safe) +apply (rule DERIV_add) apply (auto simp add: numeral_2_eq_2) done -lemma DERIV_sin_circle_all_zero [simp]: "\x. DERIV (%x. (sin x)\