--- a/NEWS Wed Dec 30 17:55:43 2015 +0100
+++ b/NEWS Wed Dec 30 18:03:23 2015 +0100
@@ -506,6 +506,7 @@
notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
+ notation NSA.approx (infixl "@=" 50)
notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
--- a/src/HOL/NSA/CStar.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/CStar.thy Wed Dec 30 18:03:23 2015 +0100
@@ -52,8 +52,8 @@
by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
lemma starfunC_approx_Re_Im_iff:
- "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) &
- (( *f* (%x. Im(f x))) x @= hIm (z)))"
+ "(( *f* f) x \<approx> z) = ((( *f* (%x. Re(f x))) x \<approx> hRe (z)) &
+ (( *f* (%x. Im(f x))) x \<approx> hIm (z)))"
by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
end
--- a/src/HOL/NSA/HDeriv.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/HDeriv.thy Wed Dec 30 18:03:23 2015 +0100
@@ -17,7 +17,7 @@
("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
"NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}.
(( *f* f)(star_of x + h)
- - star_of (f x))/h @= star_of D)"
+ - star_of (f x))/h \<approx> star_of D)"
definition
NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
--- a/src/HOL/NSA/HLim.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/HLim.thy Wed Dec 30 18:03:23 2015 +0100
@@ -15,17 +15,17 @@
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
"f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
- (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
+ (\<forall>x. (x \<noteq> star_of a & x \<approx> star_of a --> ( *f* f) x \<approx> star_of L))"
definition
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
\<comment>\<open>NS definition dispenses with limit notions\<close>
- "isNSCont f a = (\<forall>y. y @= star_of a -->
- ( *f* f) y @= star_of (f a))"
+ "isNSCont f a = (\<forall>y. y \<approx> star_of a -->
+ ( *f* f) y \<approx> star_of (f a))"
definition
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+ "isNSUCont f = (\<forall>x y. x \<approx> y --> ( *f* f) x \<approx> ( *f* f) y)"
subsection \<open>Limits of Functions\<close>
--- a/src/HOL/NSA/HSeries.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/HSeries.thy Wed Dec 30 18:03:23 2015 +0100
@@ -129,8 +129,8 @@
lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
unfolding sumhr_app by transfer (rule refl)
-lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
- ==> \<bar>sumhr(M, N, f)\<bar> @= 0"
+lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
+ ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
apply (cut_tac x = M and y = N in linorder_less_linear)
apply (auto simp add: approx_refl)
apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
@@ -167,7 +167,7 @@
lemma NSsummable_NSCauchy:
"NSsummable f =
- (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> @= 0)"
+ (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
apply (auto simp add: summable_NSsummable_iff [symmetric]
summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
--- a/src/HOL/NSA/HTranscendental.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/HTranscendental.thy Wed Dec 30 18:03:23 2015 +0100
@@ -69,7 +69,7 @@
by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
lemma hypreal_sqrt_approx_zero [simp]:
- "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
+ "0 < x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
apply (auto simp add: mem_infmal_iff [symmetric])
apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
apply (auto intro: Infinitesimal_mult
@@ -78,18 +78,18 @@
done
lemma hypreal_sqrt_approx_zero2 [simp]:
- "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
+ "0 \<le> x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
by (auto simp add: order_le_less)
lemma hypreal_sqrt_sum_squares [simp]:
- "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
+ "(( *f* sqrt)(x*x + y*y + z*z) \<approx> 0) = (x*x + y*y + z*z \<approx> 0)"
apply (rule hypreal_sqrt_approx_zero2)
apply (rule add_nonneg_nonneg)+
apply (auto)
done
lemma hypreal_sqrt_sum_squares2 [simp]:
- "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
+ "(( *f* sqrt)(x*x + y*y) \<approx> 0) = (x*x + y*y \<approx> 0)"
apply (rule hypreal_sqrt_approx_zero2)
apply (rule add_nonneg_nonneg)
apply (auto)
@@ -242,12 +242,12 @@
apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
done
-lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
+lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
apply (transfer, simp)
done
-lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1"
+lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
apply (case_tac "x = 0")
apply (cut_tac [2] x = 0 in DERIV_exp)
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -260,7 +260,7 @@
apply (auto simp add: mem_infmal_iff)
done
-lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> @= 1"
+lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
by (auto intro: STAR_exp_Infinitesimal)
lemma STAR_exp_add:
@@ -354,7 +354,7 @@
done
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
- "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z"
+ "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
apply (simp add: STAR_exp_add)
apply (frule STAR_exp_Infinitesimal)
apply (drule approx_mult2)
@@ -425,7 +425,7 @@
lemma STAR_sin_Infinitesimal [simp]:
fixes x :: "'a::{real_normed_field,banach} star"
- shows "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
+ shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
apply (case_tac "x = 0")
apply (cut_tac [2] x = 0 in DERIV_sin)
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -451,7 +451,7 @@
lemma STAR_cos_Infinitesimal [simp]:
fixes x :: "'a::{real_normed_field,banach} star"
- shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
+ shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
apply (case_tac "x = 0")
apply (cut_tac [2] x = 0 in DERIV_cos)
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -467,7 +467,7 @@
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
by transfer (rule tan_zero)
-lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
+lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
apply (case_tac "x = 0")
apply (cut_tac [2] x = 0 in DERIV_tan)
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
@@ -479,7 +479,7 @@
lemma STAR_sin_cos_Infinitesimal_mult:
fixes x :: "'a::{real_normed_field,banach} star"
- shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
+ shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]
by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
@@ -496,24 +496,24 @@
lemma STAR_sin_Infinitesimal_divide:
fixes x :: "'a::{real_normed_field,banach} star"
- shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
+ shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
using DERIV_sin [of "0::'a"]
by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
(*------------------------------------------------------------------------*)
-(* sin* (1/n) * 1/(1/n) @= 1 for n = oo *)
+(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo *)
(*------------------------------------------------------------------------*)
lemma lemma_sin_pi:
"n \<in> HNatInfinite
- ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
+ ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
apply (rule STAR_sin_Infinitesimal_divide)
apply (auto simp add: zero_less_HNatInfinite)
done
lemma STAR_sin_inverse_HNatInfinite:
"n \<in> HNatInfinite
- ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
+ ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
apply (frule lemma_sin_pi)
apply (simp add: divide_inverse)
done
@@ -532,7 +532,7 @@
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
"n \<in> HNatInfinite
==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n
- @= hypreal_of_real pi"
+ \<approx> hypreal_of_real pi"
apply (frule STAR_sin_Infinitesimal_divide
[OF Infinitesimal_pi_divide_HNatInfinite
pi_divide_HNatInfinite_not_zero])
@@ -545,7 +545,7 @@
"n \<in> HNatInfinite
==> hypreal_of_hypnat n *
( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))
- @= hypreal_of_real pi"
+ \<approx> hypreal_of_real pi"
apply (rule mult.commute [THEN subst])
apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
done
@@ -558,7 +558,7 @@
lemma STAR_sin_pi_divide_n_approx:
"N \<in> HNatInfinite ==>
- ( *f* sin) (( *f* (%x. pi / real x)) N) @=
+ ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>
hypreal_of_real pi/(hypreal_of_hypnat N)"
apply (simp add: starfunNat_real_of_nat [symmetric])
apply (rule STAR_sin_Infinitesimal)
@@ -596,7 +596,7 @@
lemma STAR_cos_Infinitesimal_approx:
fixes x :: "'a::{real_normed_field,banach} star"
- shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
+ shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto simp add: Infinitesimal_approx_minus [symmetric]
add.assoc [symmetric] numeral_2_eq_2)
@@ -604,7 +604,7 @@
lemma STAR_cos_Infinitesimal_approx2:
fixes x :: hypreal \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
- shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
+ shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
--- a/src/HOL/NSA/NSA.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Wed Dec 30 18:03:23 2015 +0100
@@ -26,26 +26,23 @@
"HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
definition
- approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "@=" 50) where
+ approx :: "['a::real_normed_vector star, 'a star] => bool" (infixl "\<approx>" 50) where
\<comment>\<open>the `infinitely close' relation\<close>
- "(x @= y) = ((x - y) \<in> Infinitesimal)"
+ "(x \<approx> y) = ((x - y) \<in> Infinitesimal)"
definition
st :: "hypreal => hypreal" where
\<comment>\<open>the standard part of a hyperreal\<close>
- "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
+ "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r \<approx> x)"
definition
monad :: "'a::real_normed_vector star => 'a star set" where
- "monad x = {y. x @= y}"
+ "monad x = {y. x \<approx> y}"
definition
galaxy :: "'a::real_normed_vector star => 'a star set" where
"galaxy x = {y. (x + -y) \<in> HFinite}"
-notation (xsymbols)
- approx (infixl "\<approx>" 50)
-
lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
by (simp add: Reals_def image_def)
@@ -611,46 +608,46 @@
subsection\<open>The Infinitely Close Relation\<close>
-lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
+lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x \<approx> 0)"
by (simp add: Infinitesimal_def approx_def)
-lemma approx_minus_iff: " (x @= y) = (x - y @= 0)"
+lemma approx_minus_iff: " (x \<approx> y) = (x - y \<approx> 0)"
by (simp add: approx_def)
-lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
+lemma approx_minus_iff2: " (x \<approx> y) = (-y + x \<approx> 0)"
by (simp add: approx_def add.commute)
-lemma approx_refl [iff]: "x @= x"
+lemma approx_refl [iff]: "x \<approx> x"
by (simp add: approx_def Infinitesimal_def)
lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
by (simp add: add.commute)
-lemma approx_sym: "x @= y ==> y @= x"
+lemma approx_sym: "x \<approx> y ==> y \<approx> x"
apply (simp add: approx_def)
apply (drule Infinitesimal_minus_iff [THEN iffD2])
apply simp
done
-lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
+lemma approx_trans: "[| x \<approx> y; y \<approx> z |] ==> x \<approx> z"
apply (simp add: approx_def)
apply (drule (1) Infinitesimal_add)
apply simp
done
-lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
+lemma approx_trans2: "[| r \<approx> x; s \<approx> x |] ==> r \<approx> s"
by (blast intro: approx_sym approx_trans)
-lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
+lemma approx_trans3: "[| x \<approx> r; x \<approx> s|] ==> r \<approx> s"
by (blast intro: approx_sym approx_trans)
-lemma approx_reorient: "(x @= y) = (y @= x)"
+lemma approx_reorient: "(x \<approx> y) = (y \<approx> x)"
by (blast intro: approx_sym)
(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
simproc_setup approx_reorient_simproc
- ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
+ ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
\<open>
let val rule = @{thm approx_reorient} RS eq_reflection
fun proc phi ss ct =
@@ -661,21 +658,21 @@
in proc end
\<close>
-lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
+lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x \<approx> y)"
by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
-lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
+lemma approx_monad_iff: "(x \<approx> y) = (monad(x)=monad(y))"
apply (simp add: monad_def)
apply (auto dest: approx_sym elim!: approx_trans equalityCE)
done
lemma Infinitesimal_approx:
- "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
+ "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x \<approx> y"
apply (simp add: mem_infmal_iff)
apply (blast intro: approx_trans approx_sym)
done
-lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
+lemma approx_add: "[| a \<approx> b; c \<approx> d |] ==> a+c \<approx> 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
@@ -683,132 +680,132 @@
finally show "a + c - (b + d) \<in> Infinitesimal" .
qed
-lemma approx_minus: "a @= b ==> -a @= -b"
+lemma approx_minus: "a \<approx> b ==> -a \<approx> -b"
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
apply (drule approx_minus_iff [THEN iffD1])
apply (simp add: add.commute)
done
-lemma approx_minus2: "-a @= -b ==> a @= b"
+lemma approx_minus2: "-a \<approx> -b ==> a \<approx> b"
by (auto dest: approx_minus)
-lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
+lemma approx_minus_cancel [simp]: "(-a \<approx> -b) = (a \<approx> b)"
by (blast intro: approx_minus approx_minus2)
-lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
+lemma approx_add_minus: "[| a \<approx> b; c \<approx> d |] ==> a + -c \<approx> b + -d"
by (blast intro!: approx_add approx_minus)
-lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d"
+lemma approx_diff: "[| a \<approx> b; c \<approx> d |] ==> a - c \<approx> b - d"
using approx_add [of a b "- c" "- d"] by simp
lemma approx_mult1:
fixes a b c :: "'a::real_normed_algebra star"
- shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
+ shows "[| a \<approx> b; c: HFinite|] ==> a*c \<approx> b*c"
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"
+ shows "[|a \<approx> b; c: HFinite|] ==> c*a \<approx> c*b"
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"
- shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
+ shows "[|u \<approx> v*x; x \<approx> y; v \<in> HFinite|] ==> u \<approx> v*y"
by (blast intro: approx_mult2 approx_trans)
lemma approx_mult_subst2:
fixes u v x y :: "'a::real_normed_algebra star"
- shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
+ shows "[| u \<approx> x*v; x \<approx> y; v \<in> HFinite |] ==> u \<approx> y*v"
by (blast intro: approx_mult1 approx_trans)
lemma approx_mult_subst_star_of:
fixes u x y :: "'a::real_normed_algebra star"
- shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
+ shows "[| u \<approx> x*star_of v; x \<approx> y |] ==> u \<approx> y*star_of v"
by (auto intro: approx_mult_subst2)
-lemma approx_eq_imp: "a = b ==> a @= b"
+lemma approx_eq_imp: "a = b ==> a \<approx> b"
by (simp add: approx_def)
-lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
+lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x \<approx> x"
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 \<approx> z)"
by (simp add: approx_def)
-lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"
+lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x \<approx> z)"
by (force simp add: bex_Infinitesimal_iff [symmetric])
-lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z"
+lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x \<approx> z"
apply (rule bex_Infinitesimal_iff [THEN iffD1])
apply (drule Infinitesimal_minus_iff [THEN iffD2])
apply (auto simp add: add.assoc [symmetric])
done
-lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y"
+lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + y"
apply (rule bex_Infinitesimal_iff [THEN iffD1])
apply (drule Infinitesimal_minus_iff [THEN iffD2])
apply (auto simp add: add.assoc [symmetric])
done
-lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
+lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x \<approx> y + x"
by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)
-lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y"
+lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + -y"
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
-lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z"
+lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y \<approx> z|] ==> x \<approx> z"
apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
apply (erule approx_trans3 [THEN approx_sym], assumption)
done
lemma Infinitesimal_add_right_cancel:
- "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
+ "[| y \<in> Infinitesimal; x \<approx> z + y|] ==> x \<approx> z"
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
apply (erule approx_trans3 [THEN approx_sym])
apply (simp add: add.commute)
apply (erule approx_sym)
done
-lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c"
+lemma approx_add_left_cancel: "d + b \<approx> d + c ==> b \<approx> c"
apply (drule approx_minus_iff [THEN iffD1])
apply (simp add: approx_minus_iff [symmetric] ac_simps)
done
-lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
+lemma approx_add_right_cancel: "b + d \<approx> c + d ==> b \<approx> c"
apply (rule approx_add_left_cancel)
apply (simp add: add.commute)
done
-lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
+lemma approx_add_mono1: "b \<approx> c ==> d + b \<approx> d + c"
apply (rule approx_minus_iff [THEN iffD2])
apply (simp add: approx_minus_iff [symmetric] ac_simps)
done
-lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
+lemma approx_add_mono2: "b \<approx> c ==> b + a \<approx> c + a"
by (simp add: add.commute approx_add_mono1)
-lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
+lemma approx_add_left_iff [simp]: "(a + b \<approx> a + c) = (b \<approx> c)"
by (fast elim: approx_add_left_cancel approx_add_mono1)
-lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
+lemma approx_add_right_iff [simp]: "(b + a \<approx> c + a) = (b \<approx> c)"
by (simp add: add.commute)
-lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
+lemma approx_HFinite: "[| x \<in> HFinite; x \<approx> y |] ==> y \<in> HFinite"
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
apply (drule HFinite_add)
apply (auto simp add: add.assoc)
done
-lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
+lemma approx_star_of_HFinite: "x \<approx> star_of D ==> x \<in> HFinite"
by (rule approx_sym [THEN [2] approx_HFinite], auto)
lemma approx_mult_HFinite:
fixes a b c d :: "'a::real_normed_algebra star"
- shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
+ shows "[|a \<approx> b; c \<approx> d; b: HFinite; d: HFinite|] ==> a*c \<approx> b*d"
apply (rule approx_trans)
apply (rule_tac [2] approx_mult2)
apply (rule approx_mult1)
@@ -820,7 +817,7 @@
by transfer (rule scaleR_left_diff_distrib)
lemma approx_scaleR1:
- "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *\<^sub>R c"
+ "[| a \<approx> star_of b; c: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R c"
apply (unfold approx_def)
apply (drule (1) Infinitesimal_HFinite_scaleHR)
apply (simp only: scaleHR_left_diff_distrib)
@@ -828,12 +825,12 @@
done
lemma approx_scaleR2:
- "a @= b ==> c *\<^sub>R a @= c *\<^sub>R b"
+ "a \<approx> b ==> c *\<^sub>R a \<approx> c *\<^sub>R b"
by (simp add: approx_def Infinitesimal_scaleR2
scaleR_right_diff_distrib [symmetric])
lemma approx_scaleR_HFinite:
- "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *\<^sub>R d"
+ "[|a \<approx> star_of b; c \<approx> d; d: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R d"
apply (rule approx_trans)
apply (rule_tac [2] approx_scaleR2)
apply (rule approx_scaleR1)
@@ -842,38 +839,38 @@
lemma approx_mult_star_of:
fixes a c :: "'a::real_normed_algebra star"
- shows "[|a @= star_of b; c @= star_of d |]
- ==> a*c @= star_of b*star_of d"
+ shows "[|a \<approx> star_of b; c \<approx> star_of d |]
+ ==> a*c \<approx> star_of b*star_of d"
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
lemma approx_SReal_mult_cancel_zero:
- "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
-lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> x*a \<approx> 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
-lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> a*x \<approx> 0"
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
lemma approx_mult_SReal_zero_cancel_iff [simp]:
- "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+ "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
lemma approx_SReal_mult_cancel:
- "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
lemma approx_SReal_mult_cancel_iff1 [simp]:
- "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+ "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
intro: approx_SReal_mult_cancel)
-lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
+lemma approx_le_bound: "[| (z::hypreal) \<le> f; f \<approx> g; g \<le> z |] ==> f \<approx> z"
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
apply (rule_tac x = "g+y-z" in bexI)
apply (simp (no_asm))
@@ -968,13 +965,13 @@
done
lemma approx_SReal_not_zero:
- "[| (y::hypreal) \<in> \<real>; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+ "[| (y::hypreal) \<in> \<real>; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
done
lemma HFinite_diff_Infinitesimal_approx:
- "[| x @= y; y \<in> HFinite - Infinitesimal |]
+ "[| x \<approx> y; y \<in> HFinite - Infinitesimal |]
==> x \<in> HFinite - Infinitesimal"
apply (auto intro: approx_sym [THEN [2] approx_HFinite]
simp add: mem_infmal_iff)
@@ -1006,7 +1003,7 @@
subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
-lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
+lemma star_of_approx_iff [simp]: "(star_of x \<approx> star_of y) = (x = y)"
apply safe
apply (simp add: approx_def)
apply (simp only: star_of_diff [symmetric])
@@ -1015,7 +1012,7 @@
done
lemma SReal_approx_iff:
- "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)"
+ "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x \<approx> y) = (x = y)"
apply auto
apply (simp add: approx_def)
apply (drule (1) Reals_diff)
@@ -1024,40 +1021,40 @@
done
lemma numeral_approx_iff [simp]:
- "(numeral v @= (numeral w :: 'a::{numeral,real_normed_vector} star)) =
+ "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) =
(numeral v = (numeral w :: 'a))"
apply (unfold star_numeral_def)
apply (rule star_of_approx_iff)
done
-(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
+(*And also for 0 \<approx> #nn and 1 \<approx> #nn, #nn \<approx> 0 and #nn \<approx> 1.*)
lemma [simp]:
- "(numeral w @= (0::'a::{numeral,real_normed_vector} star)) =
+ "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) =
(numeral w = (0::'a))"
- "((0::'a::{numeral,real_normed_vector} star) @= numeral w) =
+ "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) =
(numeral w = (0::'a))"
- "(numeral w @= (1::'b::{numeral,one,real_normed_vector} star)) =
+ "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) =
(numeral w = (1::'b))"
- "((1::'b::{numeral,one,real_normed_vector} star) @= numeral w) =
+ "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) =
(numeral w = (1::'b))"
- "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
- "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
+ "~ (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))"
+ "~ (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))"
apply (unfold star_numeral_def star_zero_def star_one_def)
apply (unfold star_of_approx_iff)
by (auto intro: sym)
lemma star_of_approx_numeral_iff [simp]:
- "(star_of k @= numeral w) = (k = numeral w)"
+ "(star_of k \<approx> numeral w) = (k = numeral w)"
by (subst star_of_approx_iff [symmetric], auto)
-lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)"
+lemma star_of_approx_zero_iff [simp]: "(star_of k \<approx> 0) = (k = 0)"
by (simp_all add: star_of_approx_iff [symmetric])
-lemma star_of_approx_one_iff [simp]: "(star_of k @= 1) = (k = 1)"
+lemma star_of_approx_one_iff [simp]: "(star_of k \<approx> 1) = (k = 1)"
by (simp_all add: star_of_approx_iff [symmetric])
lemma approx_unique_real:
- "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s"
+ "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r \<approx> x; s \<approx> x|] ==> r = s"
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
@@ -1265,13 +1262,13 @@
done
lemma st_part_Ex:
- "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
+ "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x \<approx> t"
apply (simp add: approx_def Infinitesimal_def)
apply (drule lemma_st_part_Ex, auto)
done
text\<open>There is a unique real infinitely close\<close>
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
apply (drule st_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
apply (auto intro!: approx_unique_real)
@@ -1345,8 +1342,8 @@
lemma approx_inverse:
fixes x y :: "'a::real_normed_div_algebra star"
shows
- "[| x @= y; y \<in> HFinite - Infinitesimal |]
- ==> inverse x @= inverse y"
+ "[| x \<approx> y; y \<in> HFinite - Infinitesimal |]
+ ==> inverse x \<approx> inverse y"
apply (frule HFinite_diff_Infinitesimal_approx, assumption)
apply (frule not_Infinitesimal_not_zero2)
apply (frule_tac x = x in not_Infinitesimal_not_zero2)
@@ -1364,7 +1361,7 @@
fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x \<in> HFinite - Infinitesimal;
- h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
+ h \<in> Infinitesimal |] ==> inverse(x + h) \<approx> inverse x"
apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
done
@@ -1372,7 +1369,7 @@
fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x \<in> HFinite - Infinitesimal;
- h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
+ h \<in> Infinitesimal |] ==> inverse(h + x) \<approx> inverse x"
apply (rule add.commute [THEN subst])
apply (blast intro: inverse_add_Infinitesimal_approx)
done
@@ -1381,7 +1378,7 @@
fixes x h :: "'a::real_normed_div_algebra star"
shows
"[| x \<in> HFinite - Infinitesimal;
- h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"
+ h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x \<approx> h"
apply (rule approx_trans2)
apply (auto intro: inverse_add_Infinitesimal_approx
simp add: mem_infmal_iff approx_minus_iff [symmetric])
@@ -1411,7 +1408,7 @@
lemma approx_HFinite_mult_cancel:
fixes a w z :: "'a::real_normed_div_algebra star"
- shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
+ shows "[| a: HFinite-Infinitesimal; a* w \<approx> a*z |] ==> w \<approx> z"
apply safe
apply (frule HFinite_inverse, assumption)
apply (drule not_Infinitesimal_not_zero)
@@ -1420,7 +1417,7 @@
lemma approx_HFinite_mult_cancel_iff1:
fixes a w z :: "'a::real_normed_div_algebra star"
- shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
+ shows "a: HFinite-Infinitesimal ==> (a * w \<approx> a * z) = (w \<approx> z)"
by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
lemma HInfinite_HFinite_add_cancel:
@@ -1483,7 +1480,7 @@
apply (simp (no_asm) add: HInfinite_HFinite_iff)
done
-lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x"
+lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x"
by (cut_tac x = x in hrabs_disj, auto)
@@ -1514,36 +1511,36 @@
by (simp add: monad_def)
-subsection\<open>Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}\<close>
+subsection\<open>Proof that @{term "x \<approx> y"} implies @{term"\<bar>x\<bar> \<approx> \<bar>y\<bar>"}\<close>
-lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
+lemma approx_subset_monad: "x \<approx> y ==> {x,y} \<le> monad x"
apply (simp (no_asm))
apply (simp add: approx_monad_iff)
done
-lemma approx_subset_monad2: "x @= y ==> {x,y} \<le> monad y"
+lemma approx_subset_monad2: "x \<approx> y ==> {x,y} \<le> monad y"
apply (drule approx_sym)
apply (fast dest: approx_subset_monad)
done
-lemma mem_monad_approx: "u \<in> monad x ==> x @= u"
+lemma mem_monad_approx: "u \<in> monad x ==> x \<approx> u"
by (simp add: monad_def)
-lemma approx_mem_monad: "x @= u ==> u \<in> monad x"
+lemma approx_mem_monad: "x \<approx> u ==> u \<in> monad x"
by (simp add: monad_def)
-lemma approx_mem_monad2: "x @= u ==> x \<in> monad u"
+lemma approx_mem_monad2: "x \<approx> u ==> x \<in> monad u"
apply (simp add: monad_def)
apply (blast intro!: approx_sym)
done
-lemma approx_mem_monad_zero: "[| x @= y;x \<in> monad 0 |] ==> y \<in> monad 0"
+lemma approx_mem_monad_zero: "[| x \<approx> y;x \<in> monad 0 |] ==> y \<in> monad 0"
apply (drule mem_monad_approx)
apply (fast intro: approx_mem_monad approx_trans)
done
lemma Infinitesimal_approx_hrabs:
- "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
+ "[| x \<approx> y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
done
@@ -1570,32 +1567,32 @@
done
lemma lemma_approx_gt_zero:
- "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
+ "[|0 < (x::hypreal); x \<notin> Infinitesimal; x \<approx> y|] ==> 0 < y"
by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
lemma lemma_approx_less_zero:
- "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
+ "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x \<approx> y|] ==> y < 0"
by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
-theorem approx_hrabs: "(x::hypreal) @= y ==> \<bar>x\<bar> @= \<bar>y\<bar>"
+theorem approx_hrabs: "(x::hypreal) \<approx> y ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
by (drule approx_hnorm, simp)
-lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> @= 0 ==> x @= 0"
+lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> \<approx> 0 ==> x \<approx> 0"
apply (cut_tac x = x in hrabs_disj)
apply (auto dest: approx_minus)
done
lemma approx_hrabs_add_Infinitesimal:
- "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + e\<bar>"
+ "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>"
by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
lemma approx_hrabs_add_minus_Infinitesimal:
- "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + -e\<bar>"
+ "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + -e\<bar>"
by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
lemma hrabs_add_Infinitesimal_cancel:
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
- \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
+ \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
apply (auto intro: approx_trans2)
@@ -1603,7 +1600,7 @@
lemma hrabs_add_minus_Infinitesimal_cancel:
"[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
- \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
+ \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
apply (auto intro: approx_trans2)
@@ -1755,7 +1752,7 @@
subsection\<open>Theorems about Standard Part\<close>
-lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
+lemma st_approx_self: "x \<in> HFinite ==> st x \<approx> x"
apply (simp add: st_def)
apply (frule st_part_Ex, safe)
apply (rule someI2)
@@ -1786,14 +1783,14 @@
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 \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
+lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x \<approx> y"
by (auto dest!: st_approx_self elim!: approx_trans3)
lemma approx_st_eq:
- assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
+ assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x \<approx> y"
shows "st x = st y"
proof -
- have "st x @= x" "st y @= y" "st x \<in> \<real>" "st y \<in> \<real>"
+ have "st x \<approx> x" "st y \<approx> y" "st x \<in> \<real>" "st y \<in> \<real>"
by (simp_all add: st_approx_self st_SReal x y)
with xy show ?thesis
by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
@@ -1801,7 +1798,7 @@
lemma st_eq_approx_iff:
"[| x \<in> HFinite; y \<in> HFinite|]
- ==> (x @= y) = (st x = st y)"
+ ==> (x \<approx> y) = (st x = st y)"
by (blast intro: approx_st_eq st_eq_approx)
lemma st_Infinitesimal_add_SReal:
@@ -2120,12 +2117,12 @@
lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
-lemma epsilon_approx_zero [simp]: "\<epsilon> @= 0"
+lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0"
apply (simp (no_asm) add: mem_infmal_iff [symmetric])
done
(*------------------------------------------------------------------------
- Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
+ Needed for proof that we define a hyperreal [<X(n)] \<approx> hypreal_of_real a given
that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
@@ -2204,12 +2201,12 @@
lemma real_seq_to_hypreal_approx:
"\<forall>n. norm(X n - x) < inverse(real(Suc n))
- ==> star_n X @= star_of x"
+ ==> star_n X \<approx> star_of x"
by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)
lemma real_seq_to_hypreal_approx2:
"\<forall>n. norm(x - X n) < inverse(real(Suc n))
- ==> star_n X @= star_of x"
+ ==> star_n X \<approx> star_of x"
by (metis norm_minus_commute real_seq_to_hypreal_approx)
lemma real_seq_to_hypreal_Infinitesimal2:
--- a/src/HOL/NSA/NSCA.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/NSCA.thy Wed Dec 30 18:03:23 2015 +0100
@@ -16,7 +16,7 @@
definition \<comment>\<open>standard part map\<close>
stc :: "hcomplex => hcomplex" where
- "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+ "stc x = (SOME r. x \<in> HFinite & r:SComplex & r \<approx> x)"
subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
@@ -124,52 +124,52 @@
subsection\<open>The ``Infinitely Close'' Relation\<close>
(*
-Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
+Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z \<approx> hcmod w)"
by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
*)
lemma approx_SComplex_mult_cancel_zero:
- "[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+ "[| a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
-lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SComplex1: "[| a \<in> SComplex; x \<approx> 0 |] ==> x*a \<approx> 0"
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)
-lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SComplex2: "[| a \<in> SComplex; x \<approx> 0 |] ==> a*x \<approx> 0"
by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)
lemma approx_mult_SComplex_zero_cancel_iff [simp]:
- "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+ "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)
lemma approx_SComplex_mult_cancel:
- "[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+ "[| a \<in> SComplex; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
done
lemma approx_SComplex_mult_cancel_iff1 [simp]:
- "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+ "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]
intro: approx_SComplex_mult_cancel)
(* TODO: generalize following theorems: hcmod -> hnorm *)
-lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
+lemma approx_hcmod_approx_zero: "(x \<approx> y) = (hcmod (y - x) \<approx> 0)"
apply (subst hnorm_minus_commute)
apply (simp add: approx_def Infinitesimal_hcmod_iff)
done
-lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"
+lemma approx_approx_zero_iff: "(x \<approx> 0) = (hcmod x \<approx> 0)"
by (simp add: approx_hcmod_approx_zero)
-lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)"
+lemma approx_minus_zero_cancel_iff [simp]: "(-x \<approx> 0) = (x \<approx> 0)"
by (simp add: approx_def)
lemma Infinitesimal_hcmod_add_diff:
- "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
+ "u \<approx> 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
apply (drule approx_approx_zero_iff [THEN iffD1])
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
apply (auto simp add: mem_infmal_iff [symmetric])
@@ -177,7 +177,7 @@
apply auto
done
-lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"
+lemma approx_hcmod_add_hcmod: "u \<approx> 0 ==> hcmod(x + u) \<approx> hcmod x"
apply (rule approx_minus_iff [THEN iffD2])
apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
done
@@ -210,11 +210,11 @@
by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
lemma approx_SComplex_not_zero:
- "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+ "[| y \<in> SComplex; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
lemma SComplex_approx_iff:
- "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)"
+ "[|x \<in> SComplex; y \<in> SComplex|] ==> (x \<approx> y) = (x = y)"
by (auto simp add: Standard_def)
lemma numeral_Infinitesimal_iff [simp]:
@@ -226,7 +226,7 @@
done
lemma approx_unique_complex:
- "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
+ "[| r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x|] ==> r = s"
by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
@@ -335,7 +335,7 @@
by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
lemma hcomplex_of_hypreal_approx_iff [simp]:
- "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)"
+ "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)"
by (simp add: hcomplex_approx_iff)
lemma Standard_HComplex:
@@ -343,14 +343,14 @@
by (simp add: HComplex_def)
(* Here we go - easy proof now!! *)
-lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t"
+lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x \<approx> t"
apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)
apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)
apply (simp add: st_approx_self [THEN approx_sym])
apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
done
-lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x @= t"
+lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex & x \<approx> t"
apply (drule stc_part_Ex, safe)
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
apply (auto intro!: approx_unique_complex)
@@ -368,7 +368,7 @@
subsection\<open>Theorems About Standard Part\<close>
-lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
+lemma stc_approx_self: "x \<in> HFinite ==> stc x \<approx> x"
apply (simp add: stc_def)
apply (frule stc_part_Ex, safe)
apply (rule someI2)
@@ -403,16 +403,16 @@
by auto
lemma stc_eq_approx:
- "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y"
+ "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x \<approx> y"
by (auto dest!: stc_approx_self elim!: approx_trans3)
lemma approx_stc_eq:
- "[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y"
+ "[| x \<in> HFinite; y \<in> HFinite; x \<approx> y |] ==> stc x = stc y"
by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]
dest: stc_approx_self stc_SComplex)
lemma stc_eq_approx_iff:
- "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)"
+ "[| x \<in> HFinite; y \<in> HFinite|] ==> (x \<approx> y) = (stc x = stc y)"
by (blast intro: approx_stc_eq stc_eq_approx)
lemma stc_Infinitesimal_add_SComplex:
--- a/src/HOL/NSA/Star.thy Wed Dec 30 17:55:43 2015 +0100
+++ b/src/HOL/NSA/Star.thy Wed Dec 30 18:03:23 2015 +0100
@@ -189,7 +189,7 @@
(* this is trivial, given starfun_Id *)
lemma starfun_Idfun_approx:
- "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
+ "x \<approx> star_of a ==> ( *f* (%x. x)) x \<approx> star_of a"
by (simp only: starfun_Id)
text\<open>The Star-function is a (nonstandard) extension of the function\<close>
@@ -224,7 +224,7 @@
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
by (rule starfun_star_of)
-lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
+lemma starfun_approx: "( *f* f) (star_of a) \<approx> star_of (f a)"
by simp
(* useful for NS definition of derivatives *)
@@ -238,15 +238,15 @@
lemma starfun_mult_HFinite_approx:
fixes l m :: "'a::real_normed_algebra star"
- shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
+ shows "[| ( *f* f) x \<approx> l; ( *f* g) x \<approx> m;
l: HFinite; m: HFinite
- |] ==> ( *f* (%x. f x * g x)) x @= l * m"
+ |] ==> ( *f* (%x. f x * g x)) x \<approx> l * m"
apply (drule (3) approx_mult_HFinite)
apply (auto intro: approx_HFinite [OF _ approx_sym])
done
-lemma starfun_add_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m
- |] ==> ( *f* (%x. f x + g x)) x @= l + m"
+lemma starfun_add_approx: "[| ( *f* f) x \<approx> l; ( *f* g) x \<approx> m
+ |] ==> ( *f* (%x. f x + g x)) x \<approx> l + m"
by (auto intro: approx_add)
text\<open>Examples: hrabs is nonstandard extension of rabs
@@ -298,7 +298,7 @@
{x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
by (transfer, rule refl)
-text\<open>Another characterization of Infinitesimal and one of @= relation.
+text\<open>Another characterization of Infinitesimal and one of \<open>\<approx>\<close> relation.
In this theory since \<open>hypreal_hrabs\<close> proved here. Maybe
move both theorems??\<close>
lemma Infinitesimal_FreeUltrafilterNat_iff2:
@@ -317,7 +317,7 @@
apply (auto elim!: eventually_mono)
done
-lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
+lemma approx_FreeUltrafilterNat_iff: "star_n X \<approx> star_n Y =
(\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
@@ -325,7 +325,7 @@
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
done
-lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
+lemma approx_FreeUltrafilterNat_iff2: "star_n X \<approx> star_n Y =
(\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])