# HG changeset patch # User wenzelm # Date 1451495003 -3600 # Node ID 3af5a06577c70f8da51c325f52f77e920f9cdb97 # Parent 1b5845c62fa029db717e878c2685287420fea502 more symbols; diff -r 1b5845c62fa0 -r 3af5a06577c7 NEWS --- 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) diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/CStar.thy --- 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 \ z) = ((( *f* (%x. Re(f x))) x \ hRe (z)) & + (( *f* (%x. Im(f x))) x \ hIm (z)))" by (simp add: hcomplex_approx_iff starfun_Re starfun_Im) end diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/HDeriv.thy --- 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 = (\h \ Infinitesimal - {0}. (( *f* f)(star_of x + h) - - star_of (f x))/h @= star_of D)" + - star_of (f x))/h \ star_of D)" definition NSdifferentiable :: "['a::real_normed_field \ 'a, 'a] \ bool" diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/HLim.thy --- 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" ("((_)/ \(_)/\\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where "f \a\\<^sub>N\<^sub>S L = - (\x. (x \ star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" + (\x. (x \ star_of a & x \ star_of a --> ( *f* f) x \ star_of L))" definition isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where \\NS definition dispenses with limit notions\ - "isNSCont f a = (\y. y @= star_of a --> - ( *f* f) y @= star_of (f a))" + "isNSCont f a = (\y. y \ star_of a --> + ( *f* f) y \ star_of (f a))" definition isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where - "isNSUCont f = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" + "isNSUCont f = (\x y. x \ y --> ( *f* f) x \ ( *f* f) y)" subsection \Limits of Functions\ diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/HSeries.thy --- 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.. \sumhr(M, N, f)\ @= 0" +lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \ sumhr(0, N, f) + ==> \sumhr(M, N, f)\ \ 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 = - (\M \ HNatInfinite. \N \ HNatInfinite. \sumhr(M,N,f)\ @= 0)" + (\M \ HNatInfinite. \N \ HNatInfinite. \sumhr(M,N,f)\ \ 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) diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/HTranscendental.thy --- 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) \ 0) = (x \ 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 \ x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)" + "0 \ x ==> (( *f* sqrt)(x) \ 0) = (x \ 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) \ 0) = (x*x + y*y + z*z \ 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) \ 0) = (x*x + y*y \ 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) \ 1" apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp) apply (transfer, simp) done -lemma STAR_exp_Infinitesimal: "x \ Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1" +lemma STAR_exp_Infinitesimal: "x \ Infinitesimal ==> ( *f* exp) (x::hypreal) \ 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) \ @= 1" +lemma STAR_exp_epsilon [simp]: "( *f* exp) \ \ 1" by (auto intro: STAR_exp_Infinitesimal) lemma STAR_exp_add: @@ -354,7 +354,7 @@ done lemma starfun_exp_add_HFinite_Infinitesimal_approx: - "[|x \ Infinitesimal; z \ HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z" + "[|x \ Infinitesimal; z \ HFinite |] ==> ( *f* exp) (z + x::hypreal) \ ( *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 \ Infinitesimal ==> ( *f* sin) x @= x" + shows "x \ Infinitesimal ==> ( *f* sin) x \ 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 \ Infinitesimal ==> ( *f* cos) x @= 1" + shows "x \ Infinitesimal ==> ( *f* cos) x \ 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 \ Infinitesimal ==> ( *f* tan) x @= x" +lemma STAR_tan_Infinitesimal: "x \ Infinitesimal ==> ( *f* tan) x \ 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 \ Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x" + shows "x \ Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \ 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 \ Infinitesimal; x \ 0 |] ==> ( *f* sin) x/x @= 1" + shows "[|x \ Infinitesimal; x \ 0 |] ==> ( *f* sin) x/x \ 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) \ 1 for n = oo *) (*------------------------------------------------------------------------*) lemma lemma_sin_pi: "n \ 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)) \ 1" apply (rule STAR_sin_Infinitesimal_divide) apply (auto simp add: zero_less_HNatInfinite) done lemma STAR_sin_inverse_HNatInfinite: "n \ HNatInfinite - ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1" + ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \ 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 \ HNatInfinite ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n - @= hypreal_of_real pi" + \ 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 \ HNatInfinite ==> hypreal_of_hypnat n * ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) - @= hypreal_of_real pi" + \ 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 \ HNatInfinite ==> - ( *f* sin) (( *f* (%x. pi / real x)) N) @= + ( *f* sin) (( *f* (%x. pi / real x)) N) \ 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 \ Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2" + shows "x \ Infinitesimal ==> ( *f* cos) x \ 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 \\perhaps could be generalised, like many other hypreal results\ - shows "x \ Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2" + shows "x \ Infinitesimal ==> ( *f* cos) x \ 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) diff -r 1b5845c62fa0 -r 3af5a06577c7 src/HOL/NSA/NSA.thy --- 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. \r \ 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 "\" 50) where \\the `infinitely close' relation\ - "(x @= y) = ((x - y) \ Infinitesimal)" + "(x \ y) = ((x - y) \ Infinitesimal)" definition st :: "hypreal => hypreal" where \\the standard part of a hyperreal\ - "st = (%x. @r. x \ HFinite & r \ \ & r @= x)" + "st = (%x. @r. x \ HFinite & r \ \ & r \ x)" definition monad :: "'a::real_normed_vector star => 'a star set" where - "monad x = {y. x @= y}" + "monad x = {y. x \ y}" definition galaxy :: "'a::real_normed_vector star => 'a star set" where "galaxy x = {y. (x + -y) \ HFinite}" -notation (xsymbols) - approx (infixl "\" 50) - lemma SReal_def: "\ == {x. \r. x = hypreal_of_real r}" by (simp add: Reals_def image_def) @@ -611,46 +608,46 @@ subsection\The Infinitely Close Relation\ -lemma mem_infmal_iff: "(x \ Infinitesimal) = (x @= 0)" +lemma mem_infmal_iff: "(x \ 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)" +lemma approx_minus_iff2: " (x \ y) = (-y + x \ 0)" by (simp add: approx_def add.commute) -lemma approx_refl [iff]: "x @= x" +lemma approx_refl [iff]: "x \ 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 \ y ==> y \ 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 \ y; y \ z |] ==> x \ 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 \ x; s \ x |] ==> r \ s" by (blast intro: approx_sym approx_trans) -lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s" +lemma approx_trans3: "[| x \ r; x \ s|] ==> r \ s" by (blast intro: approx_sym approx_trans) -lemma approx_reorient: "(x @= y) = (y @= x)" +lemma approx_reorient: "(x \ y) = (y \ 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 \ x" | "1 \ y" | "numeral w \ z" | "- 1 \ y" | "- numeral w \ r") = \ let val rule = @{thm approx_reorient} RS eq_reflection fun proc phi ss ct = @@ -661,21 +658,21 @@ in proc end \ -lemma Infinitesimal_approx_minus: "(x-y \ Infinitesimal) = (x @= y)" +lemma Infinitesimal_approx_minus: "(x-y \ Infinitesimal) = (x \ 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 \ y) = (monad(x)=monad(y))" apply (simp add: monad_def) apply (auto dest: approx_sym elim!: approx_trans equalityCE) done lemma Infinitesimal_approx: - "[| x \ Infinitesimal; y \ Infinitesimal |] ==> x @= y" + "[| x \ Infinitesimal; y \ Infinitesimal |] ==> x \ 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 \ b; c \ d |] ==> a+c \ b+d" proof (unfold approx_def) assume inf: "a - b \ Infinitesimal" "c - d \ Infinitesimal" have "a + c - (b + d) = (a - b) + (c - d)" by simp @@ -683,132 +680,132 @@ finally show "a + c - (b + d) \ Infinitesimal" . qed -lemma approx_minus: "a @= b ==> -a @= -b" +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 add: add.commute) done -lemma approx_minus2: "-a @= -b ==> a @= b" +lemma approx_minus2: "-a \ -b ==> a \ b" by (auto dest: approx_minus) -lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)" +lemma approx_minus_cancel [simp]: "(-a \ -b) = (a \ 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 \ b; c \ d |] ==> a + -c \ b + -d" by (blast intro!: approx_add approx_minus) -lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d" +lemma approx_diff: "[| a \ b; c \ d |] ==> a - c \ 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 \ b; c: HFinite|] ==> a*c \ 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 \ b; c: HFinite|] ==> c*a \ 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 \ HFinite|] ==> u @= v*y" + shows "[|u \ v*x; x \ y; v \ HFinite|] ==> u \ 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 \ HFinite |] ==> u @= y*v" + shows "[| u \ x*v; x \ y; v \ HFinite |] ==> u \ 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 \ x*star_of v; x \ y |] ==> u \ 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 \ b" by (simp add: approx_def) -lemma Infinitesimal_minus_approx: "x \ Infinitesimal ==> -x @= x" +lemma Infinitesimal_minus_approx: "x \ Infinitesimal ==> -x \ x" by (blast intro: Infinitesimal_minus_iff [THEN iffD2] mem_infmal_iff [THEN iffD1] approx_trans2) -lemma bex_Infinitesimal_iff: "(\y \ Infinitesimal. x - z = y) = (x @= z)" +lemma bex_Infinitesimal_iff: "(\y \ Infinitesimal. x - z = y) = (x \ z)" by (simp add: approx_def) -lemma bex_Infinitesimal_iff2: "(\y \ Infinitesimal. x = z + y) = (x @= z)" +lemma bex_Infinitesimal_iff2: "(\y \ Infinitesimal. x = z + y) = (x \ z)" by (force simp add: bex_Infinitesimal_iff [symmetric]) -lemma Infinitesimal_add_approx: "[| y \ Infinitesimal; x + y = z |] ==> x @= z" +lemma Infinitesimal_add_approx: "[| y \ Infinitesimal; x + y = z |] ==> x \ 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 \ Infinitesimal ==> x @= x + y" +lemma Infinitesimal_add_approx_self: "y \ Infinitesimal ==> x \ 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 \ Infinitesimal ==> x @= y + x" +lemma Infinitesimal_add_approx_self2: "y \ Infinitesimal ==> x \ y + x" by (auto dest: Infinitesimal_add_approx_self simp add: add.commute) -lemma Infinitesimal_add_minus_approx_self: "y \ Infinitesimal ==> x @= x + -y" +lemma Infinitesimal_add_minus_approx_self: "y \ Infinitesimal ==> x \ x + -y" by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2]) -lemma Infinitesimal_add_cancel: "[| y \ Infinitesimal; x+y @= z|] ==> x @= z" +lemma Infinitesimal_add_cancel: "[| y \ Infinitesimal; x+y \ z|] ==> x \ 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 \ Infinitesimal; x @= z + y|] ==> x @= z" + "[| y \ Infinitesimal; x \ z + y|] ==> x \ 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 \ d + c ==> b \ 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 \ c + d ==> b \ 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 \ c ==> d + b \ 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 \ c ==> b + a \ 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 \ a + c) = (b \ 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 \ c + a) = (b \ c)" by (simp add: add.commute) -lemma approx_HFinite: "[| x \ HFinite; x @= y |] ==> y \ HFinite" +lemma approx_HFinite: "[| x \ HFinite; x \ y |] ==> y \ 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 \ HFinite" +lemma approx_star_of_HFinite: "x \ star_of D ==> x \ 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 \ b; c \ d; b: HFinite; d: HFinite|] ==> a*c \ 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 \ star_of b; c: HFinite|] ==> scaleHR a c \ 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 \ b ==> c *\<^sub>R a \ 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 \ star_of b; c \ d; d: HFinite|] ==> scaleHR a c \ 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 \ star_of b; c \ star_of d |] + ==> a*c \ 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) \ \; a \ 0; a*x @= 0 |] ==> x @= 0" + "[| (a::hypreal) \ \; a \ 0; a*x \ 0 |] ==> x \ 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) \ \; x @= 0 |] ==> x*a @= 0" +lemma approx_mult_SReal1: "[| (a::hypreal) \ \; x \ 0 |] ==> x*a \ 0" by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1) -lemma approx_mult_SReal2: "[| (a::hypreal) \ \; x @= 0 |] ==> a*x @= 0" +lemma approx_mult_SReal2: "[| (a::hypreal) \ \; x \ 0 |] ==> a*x \ 0" by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2) lemma approx_mult_SReal_zero_cancel_iff [simp]: - "[|(a::hypreal) \ \; a \ 0 |] ==> (a*x @= 0) = (x @= 0)" + "[|(a::hypreal) \ \; a \ 0 |] ==> (a*x \ 0) = (x \ 0)" by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2) lemma approx_SReal_mult_cancel: - "[| (a::hypreal) \ \; a \ 0; a* w @= a*z |] ==> w @= z" + "[| (a::hypreal) \ \; a \ 0; a* w \ a*z |] ==> w \ 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) \ \; a \ 0|] ==> (a* w @= a*z) = (w @= z)" + "[| (a::hypreal) \ \; a \ 0|] ==> (a* w \ a*z) = (w \ z)" by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD] intro: approx_SReal_mult_cancel) -lemma approx_le_bound: "[| (z::hypreal) \ f; f @= g; g \ z |] ==> f @= z" +lemma approx_le_bound: "[| (z::hypreal) \ f; f \ g; g \ z |] ==> f \ 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) \ \; x @= y; y\ 0 |] ==> x \ 0" + "[| (y::hypreal) \ \; x \ y; y\ 0 |] ==> x \ 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 \ HFinite - Infinitesimal |] + "[| x \ y; y \ HFinite - Infinitesimal |] ==> x \ HFinite - Infinitesimal" apply (auto intro: approx_sym [THEN [2] approx_HFinite] simp add: mem_infmal_iff) @@ -1006,7 +1003,7 @@ subsection\Uniqueness: Two Infinitely Close Reals are Equal\ -lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)" +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_diff [symmetric]) @@ -1015,7 +1012,7 @@ done lemma SReal_approx_iff: - "[|(x::hypreal) \ \; y \ \|] ==> (x @= y) = (x = y)" + "[|(x::hypreal) \ \; y \ \|] ==> (x \ 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 \ (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 \ #nn and 1 \ #nn, #nn \ 0 and #nn \ 1.*) lemma [simp]: - "(numeral w @= (0::'a::{numeral,real_normed_vector} star)) = + "(numeral w \ (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) \ numeral w) = (numeral w = (0::'a))" - "(numeral w @= (1::'b::{numeral,one,real_normed_vector} star)) = + "(numeral w \ (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) \ 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 \ (1::'c::{zero_neq_one,real_normed_vector} star))" + "~ (1 \ (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 \ 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 \ 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 \ 1) = (k = 1)" by (simp_all add: star_of_approx_iff [symmetric]) lemma approx_unique_real: - "[| (r::hypreal) \ \; s \ \; r @= x; s @= x|] ==> r = s" + "[| (r::hypreal) \ \; s \ \; r \ x; s \ x|] ==> r = s" by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2) @@ -1265,13 +1262,13 @@ done lemma st_part_Ex: - "(x::hypreal) \ HFinite ==> \t \ Reals. x @= t" + "(x::hypreal) \ HFinite ==> \t \ Reals. x \ t" apply (simp add: approx_def Infinitesimal_def) apply (drule lemma_st_part_Ex, auto) done text\There is a unique real infinitely close\ -lemma st_part_Ex1: "x \ HFinite ==> EX! t::hypreal. t \ \ & x @= t" +lemma st_part_Ex1: "x \ HFinite ==> EX! t::hypreal. t \ \ & x \ 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 \ HFinite - Infinitesimal |] - ==> inverse x @= inverse y" + "[| x \ y; y \ HFinite - Infinitesimal |] + ==> inverse x \ 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 \ HFinite - Infinitesimal; - h \ Infinitesimal |] ==> inverse(x + h) @= inverse x" + h \ Infinitesimal |] ==> inverse(x + h) \ 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 \ HFinite - Infinitesimal; - h \ Infinitesimal |] ==> inverse(h + x) @= inverse x" + h \