# HG changeset patch # User huffman # Date 1158558487 -7200 # Node ID 44eda2314aab9d6cfc6e145c78ae28990a5d6cd8 # Parent c2f672be85224013eb6c0747f05f449ea66cc6a0 replace (x + - y) with (x - y) diff -r c2f672be8522 -r 44eda2314aab src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Sun Sep 17 16:44:51 2006 +0200 +++ b/src/HOL/Complex/CLim.thy Mon Sep 18 07:48:07 2006 +0200 @@ -664,14 +664,15 @@ by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff) lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x" -apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus) +apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def) apply (drule approx_minus_iff [THEN iffD1]) -apply (subgoal_tac "xa + - (hcomplex_of_complex x) \ 0") +apply (subgoal_tac "xa - (hcomplex_of_complex x) \ 0") prefer 2 apply (simp add: compare_rls) -apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec) - prefer 2 apply (simp add: add_assoc [symmetric]) +apply (drule_tac x = "xa - hcomplex_of_complex x" in bspec) +apply (simp add: mem_infmal_iff) +apply (simp add: add_assoc [symmetric]) apply (auto simp add: mem_infmal_iff [symmetric] add_commute) -apply (drule_tac c = "xa + - hcomplex_of_complex x" in approx_mult1) +apply (drule_tac c = "xa - hcomplex_of_complex x" in approx_mult1) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult_assoc) apply (drule_tac x3 = D in @@ -714,11 +715,11 @@ by (simp add: right_diff_distrib) lemma lemma_nscderiv2: - "[| (x + y) / z = hcomplex_of_complex D + yb; z \ 0; + "[| (x - y) / z = hcomplex_of_complex D + yb; z \ 0; z : Infinitesimal; yb : Infinitesimal |] - ==> x + y @= 0" + ==> x - y @= 0" apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption) -apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl) +apply (erule_tac V = " (x - y) / z = hcomplex_of_complex D + yb" in thin_rl) apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: mem_infmal_iff [symmetric]) apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) @@ -727,15 +728,15 @@ lemma NSCDERIV_mult: "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" -apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) +apply (auto simp add: NSCDERIV_NSCLIM_iff NSCLIM_def) apply (auto dest!: spec - simp add: starfun_lambda_cancel lemma_nscderiv1) -apply (simp (no_asm) add: add_divide_distrib) + simp add: starfun_lambda_cancel lemma_nscderiv1) +apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib) apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ -apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric]) -apply (simp add: diff_minus) -apply (drule_tac D = Db in lemma_nscderiv2) -apply (drule_tac [4] +apply (auto simp add: times_divide_eq_right [symmetric] + simp del: times_divide_eq) +apply (drule_tac D = Db in lemma_nscderiv2, assumption+) +apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) apply (auto intro!: approx_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc) apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst]) diff -r c2f672be8522 -r 44eda2314aab src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Sun Sep 17 16:44:51 2006 +0200 +++ b/src/HOL/Complex/NSCA.thy Mon Sep 18 07:48:07 2006 +0200 @@ -340,13 +340,13 @@ ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) apply (drule approx_minus_iff [THEN iffD1]) -apply (simp add: star_n_minus star_n_add mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) +apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) apply (drule_tac x = m in spec) apply (erule ultra, rule FreeUltrafilterNat_all, clarify) -apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) +apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) apply (case_tac "X n") apply (case_tac "Y n") -apply (auto simp add: complex_minus complex_add complex_mod +apply (auto simp add: complex_diff complex_mod simp del: realpow_Suc) done @@ -356,13 +356,13 @@ ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" apply (simp (no_asm) add: approx_FreeUltrafilterNat_iff2, safe) apply (drule approx_minus_iff [THEN iffD1]) -apply (simp add: star_n_minus star_n_add mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) +apply (simp add: star_n_diff mem_infmal_iff [symmetric] Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) apply (drule_tac x = m in spec) apply (erule ultra, rule FreeUltrafilterNat_all, clarify) -apply (rule_tac y="cmod (X n + - Y n)" in order_le_less_trans) +apply (rule_tac y="cmod (X n - Y n)" in order_le_less_trans) apply (case_tac "X n") apply (case_tac "Y n") -apply (auto simp add: complex_minus complex_add complex_mod +apply (auto simp add: complex_diff complex_mod simp del: realpow_Suc) done @@ -373,14 +373,14 @@ apply (drule approx_minus_iff [THEN iffD1]) apply (drule approx_minus_iff [THEN iffD1]) apply (rule approx_minus_iff [THEN iffD2]) -apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) +apply (auto simp add: mem_infmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_diff Infinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) apply (drule_tac x = "u/2" in spec) apply (drule_tac x = "u/2" in spec, auto, ultra) apply (case_tac "X x") apply (case_tac "Y x") -apply (auto simp add: complex_minus complex_add complex_mod snd_conv fst_conv numeral_2_eq_2) +apply (auto simp add: complex_diff complex_mod snd_conv fst_conv numeral_2_eq_2) apply (rename_tac a b c d) -apply (subgoal_tac "sqrt (abs (a + - c) ^ 2 + abs (b + - d) ^ 2) < u") +apply (subgoal_tac "sqrt (abs (a - c) ^ 2 + abs (b - d) ^ 2) < u") apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto) apply (simp add: power2_eq_square) done diff -r c2f672be8522 -r 44eda2314aab src/HOL/Hyperreal/HTranscendental.thy --- a/src/HOL/Hyperreal/HTranscendental.thy Sun Sep 17 16:44:51 2006 +0200 +++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Sep 18 07:48:07 2006 +0200 @@ -267,7 +267,7 @@ simp add: mult_assoc) apply (rule approx_add_right_cancel [where d="-1"]) apply (rule approx_sym [THEN [2] approx_trans2]) -apply (auto simp add: mem_infmal_iff) +apply (auto simp add: diff_def mem_infmal_iff) done lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1" @@ -282,11 +282,11 @@ apply (rule approx_st_eq, auto) apply (rule approx_minus_iff [THEN iffD2]) apply (simp only: mem_infmal_iff [symmetric]) -apply (auto simp add: mem_infmal_iff [symmetric] star_of_def star_n_zero_num hypnat_omega_def sumhr star_n_minus star_n_add) +apply (auto simp add: mem_infmal_iff [symmetric] star_of_def star_n_zero_num hypnat_omega_def sumhr star_n_diff) apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal) apply (insert exp_converges [of x]) apply (simp add: sums_def) -apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"]) +apply (drule LIMSEQ_const [THEN [2] LIMSEQ_diff, where b = "exp x"]) apply (simp add: LIMSEQ_NSLIMSEQ_iff) done @@ -467,7 +467,8 @@ apply (drule approx_mult1 [where c = x]) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult_assoc) -apply (rule approx_add_right_cancel [where d = "-1"], auto) +apply (rule approx_add_right_cancel [where d = "-1"]) +apply (simp add: diff_def) done lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0" diff -r c2f672be8522 -r 44eda2314aab src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Sun Sep 17 16:44:51 2006 +0200 +++ b/src/HOL/Hyperreal/Integration.thy Mon Sep 18 07:48:07 2006 +0200 @@ -380,8 +380,8 @@ (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance they break the original proofs and make new proofs longer!*) lemma strad1: - "\\xa::real. xa \ x \ \xa + - x\ < s \ - \(f xa - f x) / (xa - x) + - f' x\ * 2 < e; + "\\xa::real. xa \ x \ \xa - x\ < s \ + \(f xa - f x) / (xa - x) - f' x\ * 2 < e; 0 < e; a \ x; x \ b; 0 < s\ \ \z. \z - x\ < s -->\f z - f x - f' x * (z - x)\ * 2 \ e * \z - x\" apply auto @@ -427,7 +427,7 @@ apply (rule add_mono) apply (rule_tac y = "(e/2) * \v - x\" in order_trans) prefer 2 apply simp -apply (erule_tac [!] V= "\x'. x' ~= x & \x' + - x\ < s --> ?P x'" in thin_rl) +apply (erule_tac [!] V= "\x'. x' ~= x & \x' - x\ < s --> ?P x'" in thin_rl) apply (drule_tac x = v in spec, simp add: times_divide_eq) apply (drule_tac x = u in spec, auto) apply (subgoal_tac "\f u - f x - f' x * (u - x)\ = \f x - f u - f' x * (x - u)\") @@ -856,7 +856,7 @@ lemma Cauchy_iff2: "Cauchy X = - (\j. (\M. \m \ M. \n \ M. \X m + - X n\ < inverse(real (Suc j))))" + (\j. (\M. \m \ M. \n \ M. \X m - X n\ < inverse(real (Suc j))))" apply (simp add: Cauchy_def, auto) apply (drule reals_Archimedean, safe) apply (drule_tac x = n in spec, auto) diff -r c2f672be8522 -r 44eda2314aab src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sun Sep 17 16:44:51 2006 +0200 +++ b/src/HOL/Hyperreal/Lim.thy Mon Sep 18 07:48:07 2006 +0200 @@ -18,8 +18,8 @@ LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) "f -- a --> L = - (\r > 0. \s > 0. \x. x \ a & norm (x + -a) < s - --> norm (f x + -L) < r)" + (\r > 0. \s > 0. \x. x \ a & norm (x - a) < s + --> norm (f x - L) < r)" NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) @@ -37,12 +37,12 @@ deriv:: "[real=>real,real,real] => bool" --{*Differentiation: D is derivative of function f at x*} ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) - "DERIV f x :> D = ((%h. (f(x + h) + -f x)/h) -- 0 --> D)" + "DERIV f x :> D = ((%h. (f(x + h) - f x)/h) -- 0 --> D)" nsderiv :: "[real=>real,real,real] => bool" ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) "NSDERIV f x :> D = (\h \ Infinitesimal - {0}. - (( *f* f)(hypreal_of_real x + h) + + (( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))/h @= hypreal_of_real D)" differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) @@ -54,10 +54,10 @@ increment :: "[real=>real,real,hypreal] => hypreal" "increment f x h = (@inc. f NSdifferentiable x & - inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" + inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))" isUCont :: "(real=>real) => bool" - "isUCont f = (\r > 0. \s > 0. \x y. \x + -y\ < s --> \f x + -f y\ < r)" + "isUCont f = (\r > 0. \s > 0. \x y. \x - y\ < s --> \f x - f y\ < r)" isNSUCont :: "(real=>real) => bool" "isNSUCont f = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" @@ -219,7 +219,7 @@ "f -- a --> L ==> f -- a --NS> L" apply (simp add: LIM_def NSLIM_def approx_def, safe) apply (rule_tac x="x" in star_cases) -apply (simp add: star_of_def star_n_minus star_n_add starfun) +apply (simp add: star_of_def star_n_diff starfun) apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe) apply (simp add: star_n_eq_iff) apply (drule_tac x = u in spec, clarify) @@ -233,18 +233,18 @@ lemma lemma_LIM: fixes L :: "'a::real_normed_vector" - shows "\s>0. \x. x \ a \ norm (x + - a) < s \ \ norm (f x + -L) < r + shows "\s>0. \x. x \ a \ norm (x - a) < s \ \ norm (f x - L) < r ==> \n::nat. \x. x \ a \ - norm (x + -a) < inverse(real(Suc n)) \ \ norm (f x + -L) < r" + norm (x - a) < inverse(real(Suc n)) \ \ norm (f x - L) < r" apply clarify apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) done lemma lemma_skolemize_LIM2: fixes L :: "'a::real_normed_vector" - shows "\s>0. \x. x \ a \ norm (x + - a) < s \ \ norm (f x + -L) < r + shows "\s>0. \x. x \ a \ norm (x - a) < s \ \ norm (f x - L) < r ==> \X. \n::nat. X n \ a \ - norm (X n + -a) < inverse(real(Suc n)) \ \ norm(f (X n) + -L) < r" + norm (X n - a) < inverse(real(Suc n)) \ \ norm(f (X n) - L) < r" apply (drule lemma_LIM) apply (drule choice, blast) done @@ -259,9 +259,9 @@ done lemma lemma_simp: "\n. X n \ a & - norm (X n + - a) < inverse (real(Suc n)) & - \ norm (f (X n) + - L) < r ==> - \n. norm (X n + - a) < inverse (real(Suc n))" + norm (X n - a) < inverse (real(Suc n)) & + \ norm (f (X n) - L) < r ==> + \n. norm (X n - a) < inverse (real(Suc n))" by auto @@ -275,7 +275,7 @@ apply (drule mp, rule conjI) apply (simp add: star_of_def star_n_eq_iff) apply (rule real_seq_to_hypreal_Infinitesimal, simp) -apply (simp add: starfun star_of_def star_n_minus star_n_add) +apply (simp add: starfun star_of_def star_n_diff) apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (drule spec, drule (1) mp) apply simp @@ -605,37 +605,37 @@ lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f" apply (simp add: isNSUCont_def isUCont_def approx_def) -apply (simp add: all_star_eq starfun star_n_minus star_n_add) +apply (simp add: all_star_eq starfun star_n_diff) apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe) apply (rename_tac Xa Xb u) apply (drule_tac x = u in spec, clarify) apply (drule_tac x = s in spec, clarify) -apply (subgoal_tac "\n::nat. abs ((Xa n) + - (Xb n)) < s --> abs (f (Xa n) + - f (Xb n)) < u") +apply (subgoal_tac "\n::nat. abs ((Xa n) - (Xb n)) < s --> abs (f (Xa n) - f (Xb n)) < u") prefer 2 apply blast -apply (erule_tac V = "\x y. \x + - y\ < s --> \f x + - f y\ < u" in thin_rl) +apply (erule_tac V = "\x y. \x - y\ < s --> \f x - f y\ < u" in thin_rl) apply (erule ultra, simp) done -lemma lemma_LIMu: "\s>0.\z y. \z + - y\ < s & r \ \f z + -f y\ - ==> \n::nat. \z y. \z + -y\ < inverse(real(Suc n)) & r \ \f z + -f y\" +lemma lemma_LIMu: "\s>0.\z y. \z - y\ < s & r \ \f z - f y\ + ==> \n::nat. \z y. \z - y\ < inverse(real(Suc n)) & r \ \f z - f y\" apply clarify apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) done lemma lemma_skolemize_LIM2u: - "\s>0.\z y. \z + - y\ < s & r \ \f z + -f y\ + "\s>0.\z y. \z - y\ < s & r \ \f z - f y\ ==> \X Y. \n::nat. - abs(X n + -(Y n)) < inverse(real(Suc n)) & - r \ abs(f (X n) + -f (Y n))" + abs(X n - Y n) < inverse(real(Suc n)) & + r \ abs(f (X n) - f (Y n))" apply (drule lemma_LIMu) apply (drule choice, safe) apply (drule choice, blast) done -lemma lemma_simpu: "\n. \X n + -Y n\ < inverse (real(Suc n)) & - r \ abs (f (X n) + - f(Y n)) ==> - \n. \X n + - Y n\ < inverse (real(Suc n))" +lemma lemma_simpu: "\n. \X n - Y n\ < inverse (real(Suc n)) & + r \ abs (f (X n) - f(Y n)) ==> + \n. \X n - Y n\ < inverse (real(Suc n))" by auto lemma isNSUCont_isUCont: @@ -648,24 +648,24 @@ apply (drule_tac x = "star_n Y" in spec) apply (drule mp) apply (rule real_seq_to_hypreal_Infinitesimal2, simp) -apply (simp add: all_star_eq starfun star_n_minus star_n_add) +apply (simp add: all_star_eq starfun star_n_diff) apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (drule spec, drule (1) mp) apply (drule FreeUltrafilterNat_all, ultra) done text{*Derivatives*} -lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --> D)" +lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)" by (simp add: deriv_def) lemma DERIV_NS_iff: - "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)" + "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)" by (simp add: deriv_def LIM_NSLIM_iff) -lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --> D" +lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D" by (simp add: deriv_def) -lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) + - f(x))/h) -- 0 --NS> D" +lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D" by (simp add: deriv_def LIM_NSLIM_iff) @@ -755,7 +755,7 @@ text{*first equivalence *} lemma NSDERIV_NSLIM_iff: - "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- 0 --NS> D)" + "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)" apply (simp add: nsderiv_def NSLIM_def, auto) apply (drule_tac x = xa in bspec) apply (rule_tac [3] ccontr) @@ -778,7 +778,7 @@ by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) (*FIXME DELETE*) -lemma hypreal_not_eq_minus_iff: "(x \ a) = (x + -a \ (0::hypreal))" +lemma hypreal_not_eq_minus_iff: "(x \ a) = (x - a \ (0::hypreal))" by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) lemma NSDERIVD5: @@ -791,7 +791,7 @@ apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1) apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1]) apply (subgoal_tac [2] "( *f* (%z. z-x)) u \ (0::hypreal) ") -apply (auto simp add: diff_minus +apply (auto simp add: approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] Infinitesimal_subset_HFinite [THEN subsetD]) done @@ -832,10 +832,10 @@ apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def) apply (drule approx_minus_iff [THEN iffD1]) apply (drule hypreal_not_eq_minus_iff [THEN iffD1]) -apply (drule_tac x = "-hypreal_of_real x + xa" in bspec) +apply (drule_tac x = "xa - hypreal_of_real x" in bspec) prefer 2 apply (simp add: add_assoc [symmetric]) apply (auto simp add: mem_infmal_iff [symmetric] add_commute) -apply (drule_tac c = "xa + -hypreal_of_real x" in approx_mult1) +apply (drule_tac c = "xa - hypreal_of_real x" in approx_mult1) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult_assoc) apply (drule_tac x3=D in @@ -869,9 +869,9 @@ lemma NSDERIV_add: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + g x) x :> Da + Db" apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) -apply (auto simp add: add_divide_distrib dest!: spec) +apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec) apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add) -apply (auto simp add: add_ac) +apply (auto simp add: diff_def add_ac) done (* Standard theorem *) @@ -883,14 +883,14 @@ text{*Product of functions - Proof is trivial but tedious and long due to rearrangement of terms*} -lemma lemma_nsderiv1: "((a::hypreal)*b) + -(c*d) = (b*(a + -c)) + (c*(b + -d))" -by (simp add: right_distrib) +lemma lemma_nsderiv1: "((a::hypreal)*b) - (c*d) = (b*(a - c)) + (c*(b - d))" +by (simp add: right_diff_distrib) -lemma lemma_nsderiv2: "[| (x + y) / z = hypreal_of_real D + yb; z \ 0; +lemma lemma_nsderiv2: "[| (x - y) / z = hypreal_of_real D + yb; z \ 0; z \ Infinitesimal; yb \ Infinitesimal |] - ==> x + y \ 0" + ==> x - y \ 0" apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption) -apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl) +apply (erule_tac V = "(x - y) / z = hypreal_of_real D + yb" in thin_rl) apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: mult_assoc mem_infmal_iff [symmetric]) apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) @@ -902,12 +902,12 @@ apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nsderiv1) -apply (simp (no_asm) add: add_divide_distrib) +apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib) apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ apply (auto simp add: times_divide_eq_right [symmetric] simp del: times_divide_eq) -apply (drule_tac D = Db in lemma_nsderiv2) -apply (drule_tac [4] +apply (drule_tac D = Db in lemma_nsderiv2, assumption+) +apply (drule_tac approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) apply (auto intro!: approx_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc) @@ -929,7 +929,7 @@ lemma NSDERIV_cmult: "NSDERIV f x :> D ==> NSDERIV (%x. c * f x) x :> c*D" apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff - minus_mult_right right_distrib [symmetric]) + minus_mult_right right_diff_distrib [symmetric]) apply (erule NSLIM_const [THEN NSLIM_mult]) done @@ -939,17 +939,17 @@ lemma DERIV_cmult: "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" apply (simp only: deriv_def times_divide_eq_right [symmetric] - NSDERIV_NSLIM_iff minus_mult_right right_distrib [symmetric]) + NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric]) apply (erule LIM_const [THEN LIM_mult2]) done text{*Negation of function*} lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D" proof (simp add: NSDERIV_NSLIM_iff) - assume "(\h. (f (x + h) + - f x) / h) -- 0 --NS> D" - hence deriv: "(\h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D" + assume "(\h. (f (x + h) - f x) / h) -- 0 --NS> D" + hence deriv: "(\h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D" by (rule NSLIM_minus) - have "\h. - ((f (x + h) + - f x) / h) = (- f (x + h) + f x) / h" + have "\h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h" by (simp add: minus_divide_left) with deriv show "(\h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp @@ -983,13 +983,13 @@ text{*(NS) Increment*} lemma incrementI: "f NSdifferentiable x ==> - increment f x h = ( *f* f) (hypreal_of_real(x) + h) + - -hypreal_of_real (f x)" + increment f x h = ( *f* f) (hypreal_of_real(x) + h) - + hypreal_of_real (f x)" by (simp add: increment_def) lemma incrementI2: "NSDERIV f x :> D ==> - increment f x h = ( *f* f) (hypreal_of_real(x) + h) + - -hypreal_of_real (f x)" + increment f x h = ( *f* f) (hypreal_of_real(x) + h) - + hypreal_of_real (f x)" apply (erule NSdifferentiableI [THEN incrementI]) done @@ -1001,7 +1001,7 @@ apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) apply (frule_tac b1 = "hypreal_of_real (D) + y" in hypreal_mult_right_cancel [THEN iffD2]) -apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) +apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) apply assumption apply (simp add: times_divide_eq_right [symmetric]) apply (auto simp add: left_distrib) @@ -1043,7 +1043,7 @@ (* can be proved differently using NSLIM_isCont_iff *) lemma NSDERIV_approx: "[| NSDERIV f x :> D; h \ Infinitesimal; h \ 0 |] - ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \ 0" + ==> ( *f* f) (hypreal_of_real(x) + h) - hypreal_of_real(f x) \ 0" apply (simp add: nsderiv_def) apply (simp add: mem_infmal_iff [symmetric]) apply (rule Infinitesimal_ratio) @@ -1061,8 +1061,8 @@ ( *f* g) (hypreal_of_real(x) + xa) \ hypreal_of_real (g x); ( *f* g) (hypreal_of_real(x) + xa) \ hypreal_of_real (g x) |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) - + - hypreal_of_real (f (g x))) - / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) + - hypreal_of_real (f (g x))) + / (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real (g x)) \ hypreal_of_real(Da)" by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric]) @@ -1074,7 +1074,7 @@ h --------------------------------------------------------------*) lemma NSDERIVD2: "[| NSDERIV g x :> Db; xa \ Infinitesimal; xa \ 0 |] - ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa + ==> (( *f* g) (hypreal_of_real(x) + xa) - hypreal_of_real(g x)) / xa \ hypreal_of_real(Db)" by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) @@ -1092,7 +1092,7 @@ apply (case_tac "( *f* g) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ") apply (drule_tac g = g in NSDERIV_zero) apply (auto simp add: divide_inverse) -apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa) + -hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) +apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa) - hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) apply (erule hypreal_not_eq_minus_iff [THEN iffD1]) apply (rule approx_mult_hypreal_of_real) apply (simp_all add: divide_inverse [symmetric]) @@ -1144,12 +1144,12 @@ "x \ 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ Suc (Suc 0)))" apply (simp add: nsderiv_def) apply (rule ballI, simp, clarify) -apply (frule Infinitesimal_add_not_zero) -prefer 2 apply (simp add: add_commute) -apply (auto simp add: starfun_inverse_inverse realpow_two - simp del: minus_mult_left [symmetric] minus_mult_right [symmetric]) +apply (frule (1) Infinitesimal_add_not_zero) +apply (simp add: add_commute) +(*apply (auto simp add: starfun_inverse_inverse realpow_two + simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*) apply (simp add: inverse_add inverse_mult_distrib [symmetric] - inverse_minus_eq [symmetric] add_ac mult_ac + inverse_minus_eq [symmetric] add_ac mult_ac diff_def del: inverse_mult_distrib inverse_minus_eq minus_mult_left [symmetric] minus_mult_right [symmetric]) apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib @@ -1181,18 +1181,18 @@ text{*Derivative of quotient*} lemma DERIV_quotient: "[| DERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] - ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ Suc (Suc 0))" + ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" apply (drule_tac f = g in DERIV_inverse_fun) apply (drule_tac [2] DERIV_mult) apply (assumption+) apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left - mult_ac + mult_ac diff_def del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric]) done lemma NSDERIV_quotient: "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - + -(e*f(x))) / (g(x) ^ Suc (Suc 0))" + - (e*f(x))) / (g(x) ^ Suc (Suc 0))" by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc) (* ------------------------------------------------------------------------ *) @@ -2230,35 +2230,35 @@ shows "\S. (\n. S n \ a) \ S ----> a \ (\n. X (S n)) ----> L" proof - { - from prems have Xdef: "\r > 0. \s > 0. \x. x \ a & norm (x + -a) < s --> norm (X x + -L) < r" by (unfold LIM_def) + from prems have Xdef: "\r > 0. \s > 0. \x. x \ a & norm (x - a) < s --> norm (X x - L) < r" by (unfold LIM_def) fix S assume as: "(\n. S n \ a) \ S ----> a" then have "S ----> a" by auto - then have Sdef: "(\r. 0 < r --> (\no. \n. no \ n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def) + then have Sdef: "(\r. 0 < r --> (\no. \n. no \ n --> norm (S n - a) < r))" by (unfold LIMSEQ_def) { fix r - from Xdef have Xdef2: "0 < r --> (\s > 0. \x. x \ a \ \x + -a\ < s --> norm (X x + -L) < r)" by simp + from Xdef have Xdef2: "0 < r --> (\s > 0. \x. x \ a \ \x - a\ < s --> norm (X x - L) < r)" by simp { assume rgz: "0 < r" - from Xdef2 rgz have "\s > 0. \x. x \ a \ \x + -a\ < s --> norm (X x + -L) < r" by simp - then obtain s where sdef: "s > 0 \ (\x. x\a \ \x + -a\ < s \ norm (X x + -L) < r)" by auto - then have aux: "\x. x\a \ \x + -a\ < s \ norm (X x + -L) < r" by auto + from Xdef2 rgz have "\s > 0. \x. x \ a \ \x - a\ < s --> norm (X x - L) < r" by simp + then obtain s where sdef: "s > 0 \ (\x. x\a \ \x - a\ < s \ norm (X x - L) < r)" by auto + then have aux: "\x. x\a \ \x - a\ < s \ norm (X x - L) < r" by auto { fix n - from aux have "S n \ a \ \S n + -a\ < s \ norm (X (S n) + -L) < r" by simp - with as have imp2: "\S n + -a\ < s --> norm (X (S n) + -L) < r" by auto + from aux have "S n \ a \ \S n - a\ < s \ norm (X (S n) - L) < r" by simp + with as have imp2: "\S n - a\ < s --> norm (X (S n) - L) < r" by auto } - hence "\n. \S n + -a\ < s --> norm (X (S n) + -L) < r" .. + hence "\n. \S n - a\ < s --> norm (X (S n) - L) < r" .. moreover - from Sdef sdef have imp1: "\no. \n. no \ n --> \S n + -a\ < s" by auto - then obtain no where "\n. no \ n --> \S n + -a\ < s" by auto - ultimately have "\n. no \ n \ norm (X (S n) + -L) < r" by simp - hence "\no. \n. no \ n \ norm (X (S n) + -L) < r" by auto + from Sdef sdef have imp1: "\no. \n. no \ n --> \S n - a\ < s" by auto + then obtain no where "\n. no \ n --> \S n - a\ < s" by auto + ultimately have "\n. no \ n \ norm (X (S n) - L) < r" by simp + hence "\no. \n. no \ n \ norm (X (S n) - L) < r" by auto } } - hence "(\r. 0 < r --> (\no. \n. no \ n --> norm (X (S n) + -L) < r))" by simp + hence "(\r. 0 < r --> (\no. \n. no \ n --> norm (X (S n) - L) < r))" by simp hence "(\n. X (S n)) ----> L" by (fold LIMSEQ_def) } thus ?thesis by simp @@ -2272,12 +2272,12 @@ shows "X -- a --> L" proof (rule ccontr) assume "\ (X -- a --> L)" - hence "\ (\r > 0. \s > 0. \x. x \ a & norm (x + -a) < s --> norm (X x + -L) < r)" by (unfold LIM_def) - hence "\r > 0. \s > 0. \x. \(x \ a \ \x + -a\ < s --> norm (X x + -L) < r)" by simp - hence "\r > 0. \s > 0. \x. (x \ a \ \x + -a\ < s \ norm (X x + -L) \ r)" by (simp add: linorder_not_less) - then obtain r where rdef: "r > 0 \ (\s > 0. \x. (x \ a \ \