--- 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) \<noteq> 0")
+apply (subgoal_tac "xa - (hcomplex_of_complex x) \<noteq> 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 \<noteq> 0;
+ "[| (x - y) / z = hcomplex_of_complex D + yb; z \<noteq> 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])
--- 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
--- 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"
--- 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:
- "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
- \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
+ "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa - x\<bar> < s \<longrightarrow>
+ \<bar>(f xa - f x) / (xa - x) - f' x\<bar> * 2 < e;
0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
\<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
apply auto
@@ -427,7 +427,7 @@
apply (rule add_mono)
apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
prefer 2 apply simp
-apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' + - x\<bar> < s --> ?P x'" in thin_rl)
+apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' - x\<bar> < 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 "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
@@ -856,7 +856,7 @@
lemma Cauchy_iff2:
"Cauchy X =
- (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
+ (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
apply (simp add: Cauchy_def, auto)
apply (drule reals_Archimedean, safe)
apply (drule_tac x = n in spec, auto)
--- 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 =
- (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s
- --> norm (f x + -L) < r)"
+ (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> 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 = (\<forall>h \<in> 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 = (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r)"
+ "isUCont f = (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x - y\<bar> < s --> \<bar>f x - f y\<bar> < r)"
isNSUCont :: "(real=>real) => bool"
"isNSUCont f = (\<forall>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 "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x + - a) < s \<and> \<not> norm (f x + -L) < r
+ shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x - a) < s \<and> \<not> norm (f x - L) < r
==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and>
- norm (x + -a) < inverse(real(Suc n)) \<and> \<not> norm (f x + -L) < r"
+ norm (x - a) < inverse(real(Suc n)) \<and> \<not> 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 "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x + - a) < s \<and> \<not> norm (f x + -L) < r
+ shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x - a) < s \<and> \<not> norm (f x - L) < r
==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and>
- norm (X n + -a) < inverse(real(Suc n)) \<and> \<not> norm(f (X n) + -L) < r"
+ norm (X n - a) < inverse(real(Suc n)) \<and> \<not> norm(f (X n) - L) < r"
apply (drule lemma_LIM)
apply (drule choice, blast)
done
@@ -259,9 +259,9 @@
done
lemma lemma_simp: "\<forall>n. X n \<noteq> a &
- norm (X n + - a) < inverse (real(Suc n)) &
- \<not> norm (f (X n) + - L) < r ==>
- \<forall>n. norm (X n + - a) < inverse (real(Suc n))"
+ norm (X n - a) < inverse (real(Suc n)) &
+ \<not> norm (f (X n) - L) < r ==>
+ \<forall>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 "\<forall>n::nat. abs ((Xa n) + - (Xb n)) < s --> abs (f (Xa n) + - f (Xb n)) < u")
+apply (subgoal_tac "\<forall>n::nat. abs ((Xa n) - (Xb n)) < s --> abs (f (Xa n) - f (Xb n)) < u")
prefer 2 apply blast
-apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
+apply (erule_tac V = "\<forall>x y. \<bar>x - y\<bar> < s --> \<bar>f x - f y\<bar> < u" in thin_rl)
apply (erule ultra, simp)
done
-lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
- ==> \<forall>n::nat. \<exists>z y. \<bar>z + -y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z + -f y\<bar>"
+lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z - y\<bar> < s & r \<le> \<bar>f z - f y\<bar>
+ ==> \<forall>n::nat. \<exists>z y. \<bar>z - y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z - f y\<bar>"
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:
- "\<forall>s>0.\<exists>z y. \<bar>z + - y\<bar> < s & r \<le> \<bar>f z + -f y\<bar>
+ "\<forall>s>0.\<exists>z y. \<bar>z - y\<bar> < s & r \<le> \<bar>f z - f y\<bar>
==> \<exists>X Y. \<forall>n::nat.
- abs(X n + -(Y n)) < inverse(real(Suc n)) &
- r \<le> abs(f (X n) + -f (Y n))"
+ abs(X n - Y n) < inverse(real(Suc n)) &
+ r \<le> abs(f (X n) - f (Y n))"
apply (drule lemma_LIMu)
apply (drule choice, safe)
apply (drule choice, blast)
done
-lemma lemma_simpu: "\<forall>n. \<bar>X n + -Y n\<bar> < inverse (real(Suc n)) &
- r \<le> abs (f (X n) + - f(Y n)) ==>
- \<forall>n. \<bar>X n + - Y n\<bar> < inverse (real(Suc n))"
+lemma lemma_simpu: "\<forall>n. \<bar>X n - Y n\<bar> < inverse (real(Suc n)) &
+ r \<le> abs (f (X n) - f(Y n)) ==>
+ \<forall>n. \<bar>X n - Y n\<bar> < 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 \<noteq> a) = (x + -a \<noteq> (0::hypreal))"
+lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x - a \<noteq> (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 \<noteq> (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 \<noteq> 0;
+lemma lemma_nsderiv2: "[| (x - y) / z = hypreal_of_real D + yb; z \<noteq> 0;
z \<in> Infinitesimal; yb \<in> Infinitesimal |]
- ==> x + y \<approx> 0"
+ ==> x - y \<approx> 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 "(\<lambda>h. (f (x + h) + - f x) / h) -- 0 --NS> D"
- hence deriv: "(\<lambda>h. - ((f(x+h) + - f x) / h)) -- 0 --NS> - D"
+ assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D"
+ hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
by (rule NSLIM_minus)
- have "\<forall>h. - ((f (x + h) + - f x) / h) = (- f (x + h) + f x) / h"
+ have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
by (simp add: minus_divide_left)
with deriv
show "(\<lambda>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 \<in> Infinitesimal; h \<noteq> 0 |]
- ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \<approx> 0"
+ ==> ( *f* f) (hypreal_of_real(x) + h) - hypreal_of_real(f x) \<approx> 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) \<noteq> hypreal_of_real (g x);
( *f* g) (hypreal_of_real(x) + xa) \<approx> 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))
\<approx> 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 \<in> Infinitesimal; xa \<noteq> 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
\<approx> 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 \<noteq> 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) \<noteq> 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) \<noteq> 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 "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
proof -
{
- from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (X x + -L) < r" by (unfold LIM_def)
+ from prems have Xdef: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r" by (unfold LIM_def)
fix S
assume as: "(\<forall>n. S n \<noteq> a) \<and> S ----> a"
then have "S ----> a" by auto
- then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n + -a) < r))" by (unfold LIMSEQ_def)
+ then have Sdef: "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (S n - a) < r))" by (unfold LIMSEQ_def)
{
fix r
- from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
+ from Xdef have Xdef2: "0 < r --> (\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
{
assume rgz: "0 < r"
- from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r" by simp
- then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r)" by auto
- then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < s \<longrightarrow> norm (X x + -L) < r" by auto
+ from Xdef2 rgz have "\<exists>s > 0. \<forall>x. x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r" by simp
+ then obtain s where sdef: "s > 0 \<and> (\<forall>x. x\<noteq>a \<and> \<bar>x - a\<bar> < s \<longrightarrow> norm (X x - L) < r)" by auto
+ then have aux: "\<forall>x. x\<noteq>a \<and> \<bar>x - a\<bar> < s \<longrightarrow> norm (X x - L) < r" by auto
{
fix n
- from aux have "S n \<noteq> a \<and> \<bar>S n + -a\<bar> < s \<longrightarrow> norm (X (S n) + -L) < r" by simp
- with as have imp2: "\<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" by auto
+ from aux have "S n \<noteq> a \<and> \<bar>S n - a\<bar> < s \<longrightarrow> norm (X (S n) - L) < r" by simp
+ with as have imp2: "\<bar>S n - a\<bar> < s --> norm (X (S n) - L) < r" by auto
}
- hence "\<forall>n. \<bar>S n + -a\<bar> < s --> norm (X (S n) + -L) < r" ..
+ hence "\<forall>n. \<bar>S n - a\<bar> < s --> norm (X (S n) - L) < r" ..
moreover
- from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
- then obtain no where "\<forall>n. no \<le> n --> \<bar>S n + -a\<bar> < s" by auto
- ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by simp
- hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) + -L) < r" by auto
+ from Sdef sdef have imp1: "\<exists>no. \<forall>n. no \<le> n --> \<bar>S n - a\<bar> < s" by auto
+ then obtain no where "\<forall>n. no \<le> n --> \<bar>S n - a\<bar> < s" by auto
+ ultimately have "\<forall>n. no \<le> n \<longrightarrow> norm (X (S n) - L) < r" by simp
+ hence "\<exists>no. \<forall>n. no \<le> n \<longrightarrow> norm (X (S n) - L) < r" by auto
}
}
- hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) + -L) < r))" by simp
+ hence "(\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X (S n) - L) < r))" by simp
hence "(\<lambda>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 "\<not> (X -- a --> L)"
- hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (X x + -L) < r)" by (unfold LIM_def)
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x + -a\<bar> < s --> norm (X x + -L) < r)" by simp
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" by (simp add: linorder_not_less)
- then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r))" by auto
+ hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def)
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less)
+ then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto
- let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
+ let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
have "?F ----> a"
proof -
{
@@ -2293,21 +2293,21 @@
"inverse (real (Suc n)) \<le> inverse (real (Suc m))"
by auto
moreover have
- "\<bar>?F n + -a\<bar> < inverse (real (Suc n))"
+ "\<bar>?F n - a\<bar> < inverse (real (Suc n))"
proof -
from rdef have
- "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
+ "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
by simp
hence
- "(?F n)\<noteq>a \<and> \<bar>(?F n) + -a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) + -L) \<ge> r"
+ "(?F n)\<noteq>a \<and> \<bar>(?F n) - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r"
by (simp add: some_eq_ex [symmetric])
thus ?thesis by simp
qed
moreover from nodef have
"inverse (real (Suc m)) < e" .
- ultimately have "\<bar>?F n + -a\<bar> < e" by arith
+ ultimately have "\<bar>?F n - a\<bar> < e" by arith
}
- then have "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n + -a\<bar> < e" by auto
+ then have "\<exists>no. \<forall>n. no \<le> n --> \<bar>?F n - a\<bar> < e" by auto
}
thus ?thesis by (unfold LIMSEQ_def, simp)
qed
@@ -2317,7 +2317,7 @@
{
fix n
from rdef have
- "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r"
+ "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
by simp
hence "?F n \<noteq> a" by (simp add: some_eq_ex [symmetric])
}
@@ -2333,15 +2333,15 @@
obtain n where "n = no + 1" by simp
then have nolen: "no \<le> n" by simp
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x + -a\<bar> < s \<and> norm (X x + -L) \<ge> r)" ..
+ from rdef have "\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" ..
- then have "\<exists>x. x\<noteq>a \<and> \<bar>x + -a\<bar> < inverse (real (Suc n)) \<and> norm (X x + -L) \<ge> r" by simp
+ then have "\<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r" by simp
- hence "norm (X (?F n) + -L) \<ge> r" by (simp add: some_eq_ex [symmetric])
- with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r" by auto
+ hence "norm (X (?F n) - L) \<ge> r" by (simp add: some_eq_ex [symmetric])
+ with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by auto
}
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> r)" by simp
- with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) + -L) \<ge> e)" by auto
+ then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
+ with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
qed
ultimately show False by simp
@@ -2364,14 +2364,7 @@
fixes a::real
assumes "a < c"
shows "\<exists>b. a < b \<and> b < c"
-proof
- let ?b = "(a + c) / 2"
- have "a < ?b" by simp
- moreover
- have "?b < c" by simp
- ultimately
- show "a < ?b \<and> ?b < c" by simp
-qed
+by (rule dense)
lemma LIM_offset:
assumes "(\<lambda>x. f x) -- a --> L"
@@ -2379,26 +2372,26 @@
proof -
have "f -- a --> L" .
hence
- fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x + -a) < s --> norm (f x + -L) < r"
+ fd: "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (f x - L) < r"
by (unfold LIM_def)
{
fix r::real
assume rgz: "0 < r"
- with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> norm (x + -a) < s --> norm (f x + -L) < r" by simp
- then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> norm (x + -a) < s \<longrightarrow> norm (f x + -L) < r" by auto
- from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> norm ((x+c) + -a) < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
+ with fd have "\<exists>s > 0. \<forall>x. x\<noteq>a \<and> norm (x - a) < s --> norm (f x - L) < r" by simp
+ then obtain s where sgz: "s > 0" and ax: "\<forall>x. x\<noteq>a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" by auto
+ from ax have ax2: "\<forall>x. (x+c)\<noteq>a \<and> norm ((x+c) - a) < s \<longrightarrow> norm (f (x+c) - L) < r" by auto
{
fix x
- from ax2 have nt: "(x+c)\<noteq>a \<and> norm ((x+c) + -a) < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
+ from ax2 have nt: "(x+c)\<noteq>a \<and> norm ((x+c) - a) < s \<longrightarrow> norm (f (x+c) - L) < r" ..
moreover have "((x+c)\<noteq>a) = (x\<noteq>(a-c))" by auto
- moreover have "((x+c) + -a) = (x + -(a-c))" by simp
- ultimately have "x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" by simp
+ moreover have "((x+c) - a) = (x - (a-c))" by simp
+ ultimately have "x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" by simp
}
- then have "\<forall>x. x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" ..
- with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> norm (x + -(a-c)) < s \<longrightarrow> norm (f (x+c) + -L) < r" by auto
+ then have "\<forall>x. x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" ..
+ with sgz have "\<exists>s > 0. \<forall>x. x\<noteq>(a-c) \<and> norm (x - (a-c)) < s \<longrightarrow> norm (f (x+c) - L) < r" by auto
}
then have
- "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & norm (x + -(a-c)) < s --> norm (f (x+c) + -L) < r" by simp
+ "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & norm (x - (a-c)) < s --> norm (f (x+c) - L) < r" by simp
thus ?thesis by (fold LIM_def)
qed
--- a/src/HOL/Hyperreal/Ln.thy Sun Sep 17 16:44:51 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Mon Sep 18 07:48:07 2006 +0200
@@ -380,7 +380,7 @@
apply (rule conjI)
prefer 2
apply clarsimp
- apply (subgoal_tac "(ln (x + xa) + - ln x) / xa + - (1 / x) =
+ apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) =
(ln (1 + xa / x) - xa / x) / xa")
apply (erule ssubst)
apply (subst abs_divide)
@@ -405,7 +405,6 @@
apply (erule conjE, assumption)
apply force
apply simp
- apply (subst diff_minus [THEN sym])+
apply (subst ln_div [THEN sym])
apply arith
apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq
--- a/src/HOL/Hyperreal/NSA.thy Sun Sep 17 16:44:51 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Mon Sep 18 07:48:07 2006 +0200
@@ -28,7 +28,7 @@
approx :: "['a::real_normed_vector star, 'a star] => bool"
(infixl "@=" 50)
--{*the `infinitely close' relation*}
- "(x @= y) = ((x + -y) \<in> Infinitesimal)"
+ "(x @= y) = ((x - y) \<in> Infinitesimal)"
st :: "hypreal => hypreal"
--{*the standard part of a hyperreal*}
@@ -150,6 +150,12 @@
apply (rule_tac x = "r + ra" in exI, simp)
done
+lemma SReal_diff [simp]:
+ "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x - y \<in> Reals"
+apply (auto simp add: SReal_def)
+apply (rule_tac x = "r - ra" in exI, simp)
+done
+
lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
apply (simp add: SReal_def, safe)
apply (rule_tac x = "r * ra" in exI)
@@ -607,11 +613,11 @@
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
by (simp add: Infinitesimal_def approx_def)
-lemma approx_minus_iff: " (x @= y) = (x + -y @= 0)"
+lemma approx_minus_iff: " (x @= y) = (x - y @= 0)"
by (simp add: approx_def)
lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
-by (simp add: approx_def add_commute)
+by (simp add: approx_def diff_minus add_commute)
lemma approx_refl [iff]: "x @= x"
by (simp add: approx_def Infinitesimal_def)
@@ -621,13 +627,14 @@
lemma approx_sym: "x @= y ==> y @= x"
apply (simp add: approx_def)
-apply (rule hypreal_minus_distrib1 [THEN subst])
-apply (erule Infinitesimal_minus_iff [THEN iffD2])
+apply (drule Infinitesimal_minus_iff [THEN iffD2])
+apply simp
done
lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
apply (simp add: approx_def)
-apply (drule Infinitesimal_add, assumption, auto)
+apply (drule (1) Infinitesimal_add)
+apply (simp add: diff_def)
done
lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
@@ -680,7 +687,7 @@
*}
lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
-by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff)
+by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
apply (simp add: monad_def)
@@ -695,16 +702,16 @@
lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
proof (unfold approx_def)
- assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
- have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp
+ assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal"
+ have "a + c - (b + d) = (a - b) + (c - d)" by simp
also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
- finally show "a + c + - (b + d) \<in> Infinitesimal" .
+ finally show "a + c - (b + d) \<in> Infinitesimal" .
qed
lemma approx_minus: "a @= b ==> -a @= -b"
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (drule approx_minus_iff [THEN iffD1])
-apply (simp (no_asm) add: add_commute)
+apply (simp add: add_commute diff_def)
done
lemma approx_minus2: "-a @= -b ==> a @= b"
@@ -719,16 +726,14 @@
lemma approx_mult1:
fixes a b c :: "'a::real_normed_algebra star"
shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
-by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left
- left_distrib [symmetric]
- del: minus_mult_left [symmetric])
+by (simp add: approx_def Infinitesimal_HFinite_mult
+ left_diff_distrib [symmetric])
lemma approx_mult2:
fixes a b c :: "'a::real_normed_algebra star"
shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
-by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right
- right_distrib [symmetric]
- del: minus_mult_right [symmetric])
+by (simp add: approx_def Infinitesimal_HFinite_mult2
+ right_diff_distrib [symmetric])
lemma approx_mult_subst:
fixes u v x y :: "'a::real_normed_algebra star"
@@ -756,7 +761,7 @@
by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
mem_infmal_iff [THEN iffD1] approx_trans2)
-lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x + -z = y) = (x @= z)"
+lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)"
by (simp add: approx_def)
lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"
@@ -997,20 +1002,18 @@
lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
apply safe
apply (simp add: approx_def)
-apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
+apply (simp only: star_of_diff [symmetric])
apply (simp only: star_of_Infinitesimal_iff_0)
-apply (simp only: diff_minus [symmetric] right_minus_eq)
+apply simp
done
lemma SReal_approx_iff:
"[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
apply auto
apply (simp add: approx_def)
-apply (drule_tac x = y in SReal_minus)
-apply (drule SReal_add, assumption)
-apply (drule SReal_Infinitesimal_zero, assumption)
-apply (drule sym)
-apply (simp add: hypreal_eq_minus_iff [symmetric])
+apply (drule (1) SReal_diff)
+apply (drule (1) SReal_Infinitesimal_zero)
+apply simp
done
lemma number_of_approx_iff [simp]:
@@ -1201,7 +1204,7 @@
"[| (x::hypreal) \<in> HFinite;
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
- ==> abs (x + -t) < r"
+ ==> abs (x - t) < r"
apply (frule lemma_st_part1a)
apply (frule_tac [4] lemma_st_part2a, auto)
apply (drule order_le_imp_less_or_eq)+
@@ -1210,14 +1213,14 @@
lemma lemma_st_part_major2:
"[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
- ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
+ ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
by (blast dest!: lemma_st_part_major)
text{*Existence of real and Standard Part Theorem*}
lemma lemma_st_part_Ex:
"(x::hypreal) \<in> HFinite
- ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
+ ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
apply (frule lemma_st_part_lub, safe)
apply (frule isLubD1a)
apply (blast dest: lemma_st_part_major2)
@@ -1338,7 +1341,7 @@
fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
shows
"[| x \<in> HFinite - Infinitesimal;
- h \<in> Infinitesimal |] ==> inverse(x + h) + -inverse x @= h"
+ h \<in> 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])
@@ -1698,7 +1701,7 @@
lemma monad_hrabs_less:
"[| y \<in> monad x; 0 < hypreal_of_real e |]
- ==> abs (y + -x) < 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])
apply (auto dest!: InfinitesimalD)
@@ -2231,13 +2234,13 @@
|X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
-----------------------------------------------------*)
lemma real_seq_to_hypreal_Infinitesimal:
- "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
- ==> star_n X + -star_of x \<in> Infinitesimal"
-apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_minus star_of_def star_n_add Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
+ "\<forall>n. norm(X n - x) < inverse(real(Suc n))
+ ==> star_n X - star_of x \<in> Infinitesimal"
+apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
done
lemma real_seq_to_hypreal_approx:
- "\<forall>n. norm(X n + -x) < inverse(real(Suc n))
+ "\<forall>n. norm(X n - x) < inverse(real(Suc n))
==> star_n X @= star_of x"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
@@ -2245,22 +2248,21 @@
done
lemma real_seq_to_hypreal_approx2:
- "\<forall>n. norm(x + -X n) < inverse(real(Suc n))
+ "\<forall>n. norm(x - X n) < inverse(real(Suc n))
==> star_n X @= star_of x"
apply (rule real_seq_to_hypreal_approx)
apply (subst norm_minus_cancel [symmetric])
apply (simp del: norm_minus_cancel)
-apply (subst add_commute, assumption)
done
lemma real_seq_to_hypreal_Infinitesimal2:
- "\<forall>n. norm(X n + -Y n) < inverse(real(Suc n))
- ==> star_n X + -star_n Y \<in> Infinitesimal"
+ "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
+ ==> star_n X - star_n Y \<in> Infinitesimal"
by (auto intro!: bexI
dest: FreeUltrafilterNat_inverse_real_of_posnat
FreeUltrafilterNat_all FreeUltrafilterNat_Int
intro: order_less_trans FreeUltrafilterNat_subset
- simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus
- star_n_add star_n_inverse)
+ simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
+ star_n_inverse)
end
--- a/src/HOL/Hyperreal/SEQ.thy Sun Sep 17 16:44:51 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Mon Sep 18 07:48:07 2006 +0200
@@ -17,7 +17,7 @@
LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----> (_))" [60, 60] 60)
--{*Standard definition of convergence of sequence*}
- "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n + -L) < r))"
+ "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
("((_)/ ----NS> (_))" [60, 60] 60)
@@ -58,7 +58,7 @@
Cauchy :: "(nat => 'a::real_normed_vector) => bool"
--{*Standard definition of the Cauchy condition*}
- "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm((X m) + -(X n)) < e)"
+ "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
NSCauchy :: "(nat => 'a::real_normed_vector) => bool"
--{*Nonstandard definition*}
@@ -82,7 +82,7 @@
subsection{*LIMSEQ and NSLIMSEQ*}
lemma LIMSEQ_iff:
- "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n + -L) < r)"
+ "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
by (simp add: LIMSEQ_def)
lemma NSLIMSEQ_iff:
@@ -98,7 +98,7 @@
apply (simp add: HNatInfinite_FreeUltrafilterNat_iff)
apply (rule approx_minus_iff [THEN iffD2])
apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def
- star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
+ star_n_diff Infinitesimal_FreeUltrafilterNat_iff)
apply (drule_tac x = u in spec, safe)
apply (drule_tac x = no in spec)
apply (erule ultra, simp add: less_imp_le)
@@ -157,13 +157,13 @@
by auto
lemma lemmaLIM2:
- "{n. norm (X (f n) + - L) < r} Int {n. r \<le> norm (X (f n) + - L)} = {}"
+ "{n. norm (X (f n) - L) < r} Int {n. r \<le> norm (X (f n) - L)} = {}"
by auto
-lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> norm (X (f n) + - L);
- ( *f* X) (star_n f) +
+lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> norm (X (f n) - L);
+ ( *f* X) (star_n f)
- star_of L \<approx> 0 |] ==> False"
-apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (auto simp add: starfun mem_infmal_iff [symmetric] star_of_def star_n_diff Infinitesimal_FreeUltrafilterNat_iff)
apply (drule_tac x = r in spec, safe)
apply (drule FreeUltrafilterNat_all)
apply (drule FreeUltrafilterNat_Int, assumption)
@@ -774,9 +774,9 @@
done
lemma lemmaCauchy2:
- "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> norm (X m + - X n) < u} Int
+ "{n. \<forall>m n. M \<le> m & M \<le> (n::nat) --> norm (X m - X n) < u} Int
{n. M \<le> xa n} Int {n. M \<le> x n} \<le>
- {n. norm (X (xa n) + - X (x n)) < u}"
+ {n. norm (X (xa n) - X (x n)) < u}"
by blast
lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
@@ -785,7 +785,7 @@
apply (rule_tac x = N in star_cases)
apply (rule approx_minus_iff [THEN iffD2])
apply (rule mem_infmal_iff [THEN iffD1])
-apply (auto simp add: starfun star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (auto simp add: starfun star_n_diff Infinitesimal_FreeUltrafilterNat_iff)
apply (drule spec, auto)
apply (drule_tac M = M in lemmaCauchy1)
apply (drule_tac M = M in lemmaCauchy1)
@@ -806,7 +806,7 @@
apply (auto simp add: starfun)
apply (drule approx_minus_iff [THEN iffD1])
apply (drule mem_infmal_iff [THEN iffD2])
-apply (auto simp add: star_n_minus star_n_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (auto simp add: star_n_diff Infinitesimal_FreeUltrafilterNat_iff)
done
@@ -816,10 +816,10 @@
text{*A Cauchy sequence is bounded -- this is the standard
proof mechanization rather than the nonstandard proof*}
-lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M + - X n) < (1::real)
+lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
==> \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
apply (clarify, drule spec, drule (1) mp)
-apply (fold diff_def, simp only: norm_minus_commute)
+apply (simp only: norm_minus_commute)
apply (drule order_le_less_trans [OF norm_triangle_ineq2])
apply simp
done
--- a/src/HOL/Hyperreal/Star.thy Sun Sep 17 16:44:51 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy Mon Sep 18 07:48:07 2006 +0200
@@ -329,19 +329,19 @@
star_n_inverse star_n_less hypreal_of_nat_eq)
lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
- (\<forall>r>0. {n. norm (X n + - Y n) < r} : FreeUltrafilterNat)"
+ (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
-apply (simp add: star_n_minus star_n_add)
+apply (simp add: star_n_diff)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
done
lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
- (\<forall>m. {n. norm (X n + - Y n) <
+ (\<forall>m. {n. norm (X n - Y n) <
inverse(real(Suc m))} : FreeUltrafilterNat)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
-apply (simp add: star_n_minus star_n_add)
+apply (simp add: star_n_diff)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
done