# HG changeset patch # User huffman # Date 1158454585 -7200 # Node ID 2116b7a371c7d52efc4ea7571196da175f510de6 # Parent 759c8f2ead69aca3d75745e1a20575bcb1189260 removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants diff -r 759c8f2ead69 -r 2116b7a371c7 src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Sun Sep 17 02:53:36 2006 +0200 +++ b/src/HOL/Complex/CLim.thy Sun Sep 17 02:56:25 2006 +0200 @@ -45,8 +45,8 @@ NSCLIM :: "[complex=>complex,complex,complex] => bool" ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60) "f -- a --NSC> L = (\x. (x \ hcomplex_of_complex a & - x @c= hcomplex_of_complex a - --> ( *f* f) x @c= hcomplex_of_complex L))" + x @= hcomplex_of_complex a + --> ( *f* f) x @= hcomplex_of_complex L))" (* f: C --> R *) CRLIM :: "[complex=>real,complex,real] => bool" @@ -59,7 +59,7 @@ NSCRLIM :: "[complex=>real,complex,real] => bool" ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60) "f -- a --NSCR> L = (\x. (x \ hcomplex_of_complex a & - x @c= hcomplex_of_complex a + x @= hcomplex_of_complex a --> ( *f* f) x @= hypreal_of_real L))" @@ -68,15 +68,15 @@ (* NS definition dispenses with limit notions *) isNSContc :: "[complex=>complex,complex] => bool" - "isNSContc f a = (\y. y @c= hcomplex_of_complex a --> - ( *f* f) y @c= hcomplex_of_complex (f a))" + "isNSContc f a = (\y. y @= hcomplex_of_complex a --> + ( *f* f) y @= hcomplex_of_complex (f a))" isContCR :: "[complex=>real,complex] => bool" "isContCR f a = (f -- a --CR> (f a))" (* NS definition dispenses with limit notions *) isNSContCR :: "[complex=>real,complex] => bool" - "isNSContCR f a = (\y. y @c= hcomplex_of_complex a --> + "isNSContCR f a = (\y. y @= hcomplex_of_complex a --> ( *f* f) y @= hypreal_of_real (f a))" (* differentiation: D is derivative of function f at x *) @@ -86,9 +86,9 @@ nscderiv :: "[complex=>complex,complex,complex] => bool" ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) - "NSCDERIV f x :> D = (\h \ CInfinitesimal - {0}. + "NSCDERIV f x :> D = (\h \ Infinitesimal - {0}. (( *f* f)(hcomplex_of_complex x + h) - - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)" + - hcomplex_of_complex (f x))/h @= hcomplex_of_complex D)" cdifferentiable :: "[complex=>complex,complex] => bool" (infixl "cdifferentiable" 60) @@ -105,7 +105,7 @@ --> cmod(f x - f y) < r)))" isNSUContc :: "(complex=>complex) => bool" - "isNSUContc f = (\x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)" + "isNSUContc f = (\x y. x @= y --> ( *f* f) x @= ( *f* f) y)" @@ -122,10 +122,11 @@ lemma CLIM_NSCLIM: "f -- x --C> L ==> f -- x --NSC> L" -apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) +apply (simp add: CLIM_def NSCLIM_def approx_def, auto) apply (rule_tac x = xa in star_cases) apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff - CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) + Infinitesimal_hcmod_iff hcmod diff_def [symmetric]) +apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (drule_tac x = u in spec, auto) apply (drule_tac x = s in spec, auto, ultra) apply (auto) @@ -167,14 +168,15 @@ apply (simp add: CLIM_def NSCLIM_def) apply (rule ccontr) apply (auto simp add: eq_Abs_star_ALL starfun - CInfinitesimal_capprox_minus [symmetric] star_n_diff - CInfinitesimal_hcmod_iff star_of_def star_n_eq_iff - Infinitesimal_FreeUltrafilterNat_iff hcmod) + Infinitesimal_approx_minus [symmetric] star_n_diff + Infinitesimal_hcmod_iff star_of_def star_n_eq_iff + hcmod) +apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (simp add: linorder_not_less) apply (drule lemma_skolemize_CLIM2, safe) apply (drule_tac x = X in spec, auto) -apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) -apply (simp add: CInfinitesimal_hcmod_iff star_of_def +apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_Infinitesimal]) +apply (simp add: Infinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod) apply (drule_tac x = r in spec, clarify) apply (drule FreeUltrafilterNat_all, ultra) @@ -189,13 +191,13 @@ subsection{*Limit of Complex to Real Function*} lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L" -apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) +apply (simp add: CRLIM_def NSCRLIM_def approx_def, auto) apply (rule_tac x = xa in star_cases) apply (auto simp add: starfun star_n_diff - CInfinitesimal_hcmod_iff hcmod - Infinitesimal_FreeUltrafilterNat_iff + Infinitesimal_hcmod_iff hcmod star_of_def star_n_eq_iff - Infinitesimal_approx_minus [symmetric]) + diff_def [symmetric]) +apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (drule_tac x = u in spec, auto) apply (drule_tac x = s in spec, auto, ultra) apply (auto) @@ -227,18 +229,19 @@ by auto lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L" -apply (simp add: CRLIM_def NSCRLIM_def capprox_def) +apply (simp add: CRLIM_def NSCRLIM_def approx_def) apply (rule ccontr) apply (auto simp add: eq_Abs_star_ALL starfun star_n_diff - CInfinitesimal_hcmod_iff + Infinitesimal_hcmod_iff hcmod Infinitesimal_approx_minus [symmetric] star_of_def star_n_eq_iff - Infinitesimal_FreeUltrafilterNat_iff) + diff_def [symmetric]) +apply (auto simp add: Infinitesimal_FreeUltrafilterNat_iff) apply (simp add: linorder_not_less) apply (drule lemma_skolemize_CRLIM2, safe) apply (drule_tac x = X in spec, auto) -apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal]) -apply (simp add: CInfinitesimal_hcmod_iff star_of_def +apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_Infinitesimal]) +apply (simp add: Infinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod) apply (drule_tac x = r in spec, clarify) apply (drule FreeUltrafilterNat_all, ultra) @@ -266,7 +269,7 @@ lemma NSCLIM_add: "[| f -- x --NSC> l; g -- x --NSC> m |] ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)" -by (auto simp: NSCLIM_def intro!: capprox_add) +by (auto simp: NSCLIM_def intro!: approx_add) lemma CLIM_add: "[| f -- x --C> l; g -- x --C> m |] @@ -278,7 +281,7 @@ lemma NSCLIM_mult: "[| f -- x --NSC> l; g -- x --NSC> m |] ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)" -by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite) +by (auto simp add: NSCLIM_def intro!: approx_mult_HFinite) lemma CLIM_mult: "[| f -- x --C> l; g -- x --C> m |] @@ -320,7 +323,7 @@ ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)" apply (simp add: NSCLIM_def, clarify) apply (drule spec) -apply (force simp add: hcomplex_of_complex_capprox_inverse) +apply (force simp add: hcomplex_of_complex_approx_inverse) done lemma CLIM_inverse: @@ -350,7 +353,7 @@ lemma NSCLIM_not_zero: "k \ 0 ==> ~ ((%x. k) -- x --NSC> 0)" apply (auto simp del: star_of_zero simp add: NSCLIM_def) apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI) -apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym] +apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] simp del: star_of_zero) done @@ -395,7 +398,7 @@ (*** NSCLIM_self hence CLIM_self ***) lemma NSCLIM_self: "(%x. x) -- a --NSC> a" -by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox) +by (auto simp add: NSCLIM_def intro: starfunC_Idfun_approx) lemma CLIM_self: "(%x. x) -- a --C> a" by (simp add: CLIM_NSCLIM_iff NSCLIM_self) @@ -403,7 +406,7 @@ (** another equivalence result **) lemma NSCLIM_NSCRLIM_iff: "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)" -apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff) +apply (auto simp add: NSCLIM_def NSCRLIM_def Infinitesimal_approx_minus [symmetric] Infinitesimal_hcmod_iff) apply (auto dest!: spec) apply (rule_tac [!] x = xa in star_cases) apply (auto simp add: star_n_diff starfun hcmod mem_infmal_iff star_of_def) @@ -425,7 +428,7 @@ apply (auto simp add: NSCLIM_def NSCRLIM_def) apply (auto dest!: spec) apply (rule_tac x = x in star_cases) -apply (simp add: capprox_approx_iff starfun star_of_def) +apply (simp add: approx_approx_iff starfun star_of_def) done lemma CLIM_CRLIM_Re_Im_iff: @@ -437,8 +440,8 @@ subsection{*Continuity*} lemma isNSContcD: - "[| isNSContc f a; y @c= hcomplex_of_complex a |] - ==> ( *f* f) y @c= hcomplex_of_complex (f a)" + "[| isNSContc f a; y @= hcomplex_of_complex a |] + ==> ( *f* f) y @= hcomplex_of_complex (f a)" by (simp add: isNSContc_def) lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) " @@ -475,8 +478,8 @@ apply (simp add: NSCLIM_def, auto) apply (drule_tac x = "hcomplex_of_complex a + x" in spec) apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp) -apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]]) -apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1]) +apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) +apply (rule_tac [4] approx_minus_iff2 [THEN iffD1]) prefer 3 apply (simp add: compare_rls add_commute) apply (rule_tac [2] x = x in star_cases) apply (rule_tac [4] x = x in star_cases) @@ -495,11 +498,11 @@ lemma isContc_add: "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a" -by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) +by (auto intro: approx_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) lemma isContc_mult: "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a" -by (auto intro!: starfun_mult_CFinite_capprox +by (auto intro!: starfun_mult_HFinite_approx [simplified starfun_mult [symmetric]] simp add: isNSContc_isContc_iff [symmetric] isNSContc_def) @@ -541,7 +544,7 @@ subsection{*Functions from Complex to Reals*} lemma isNSContCRD: - "[| isNSContCR f a; y @c= hcomplex_of_complex a |] + "[| isNSContCR f a; y @= hcomplex_of_complex a |] ==> ( *f* f) y @= hypreal_of_real (f a)" by (simp add: isNSContCR_def) @@ -570,7 +573,7 @@ by (erule isNSContCR_isContCR_iff [THEN iffD1]) lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)" -by (auto intro: capprox_hcmod_approx +by (auto intro: approx_hcmod_approx simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] isNSContCR_def) @@ -607,7 +610,7 @@ lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E" apply (simp add: nscderiv_def) apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"] - intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3) + intro!: inj_hcomplex_of_complex [THEN injD] dest: approx_trans3) done @@ -643,7 +646,7 @@ apply (drule_tac x = xa in bspec) apply (rule_tac [3] ccontr) apply (drule_tac [3] x = h in spec) -apply (auto simp add: mem_cinfmal_iff starfun_lambda_cancel) +apply (auto simp add: mem_infmal_iff starfun_lambda_cancel) done (*** 2nd equivalence ***) @@ -653,8 +656,8 @@ lemma NSCDERIV_iff2: "(NSCDERIV f x :> D) = - (\xa. xa \ hcomplex_of_complex x & xa @c= hcomplex_of_complex x --> - ( *f* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)" + (\xa. xa \ hcomplex_of_complex x & xa @= hcomplex_of_complex x --> + ( *f* (%z. (f z - f x) / (z - x))) xa @= hcomplex_of_complex D)" by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)" @@ -662,19 +665,19 @@ lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x" apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus) -apply (drule capprox_minus_iff [THEN iffD1]) +apply (drule approx_minus_iff [THEN iffD1]) apply (subgoal_tac "xa + - (hcomplex_of_complex x) \ 0") prefer 2 apply (simp add: compare_rls) apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec) prefer 2 apply (simp add: add_assoc [symmetric]) -apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute) -apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1) -apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD] +apply (auto simp add: mem_infmal_iff [symmetric] add_commute) +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 - CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult, - THEN mem_cinfmal_iff [THEN iffD1]]) -apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2]) + HFinite_hcomplex_of_complex [THEN [2] Infinitesimal_HFinite_mult, + THEN mem_infmal_iff [THEN iffD1]]) +apply (blast intro: approx_trans mult_commute [THEN subst] approx_minus_iff [THEN iffD2]) done lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x" @@ -695,7 +698,7 @@ ==> NSCDERIV (%x. f x + g x) x :> Da + Db" apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) apply (auto dest!: spec simp add: add_divide_distrib diff_minus) -apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add) +apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in approx_add) apply (auto simp add: add_ac) done @@ -712,13 +715,13 @@ lemma lemma_nscderiv2: "[| (x + y) / z = hcomplex_of_complex D + yb; z \ 0; - z : CInfinitesimal; yb : CInfinitesimal |] - ==> x + y @c= 0" + z : Infinitesimal; yb : Infinitesimal |] + ==> 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 (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add - simp add: mem_cinfmal_iff [symmetric]) -apply (erule CInfinitesimal_subset_CFinite [THEN subsetD]) +apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add + simp add: mem_infmal_iff [symmetric]) +apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) done lemma NSCDERIV_mult: @@ -728,18 +731,18 @@ apply (auto dest!: spec simp add: starfun_lambda_cancel lemma_nscderiv1) apply (simp (no_asm) add: add_divide_distrib) -apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+ +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] - capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]]) -apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc) + 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]) -apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym] - CInfinitesimal_add CInfinitesimal_mult - CInfinitesimal_hcomplex_of_complex_mult - CInfinitesimal_hcomplex_of_complex_mult2 +apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] + Infinitesimal_add Infinitesimal_mult + Infinitesimal_hcomplex_of_complex_mult + Infinitesimal_hcomplex_of_complex_mult2 simp add: add_assoc [symmetric]) done @@ -796,18 +799,18 @@ lemma NSCDERIV_zero: "[| NSCDERIV g x :> D; ( *f* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x); - xa : CInfinitesimal; xa \ 0 + xa : Infinitesimal; xa \ 0 |] ==> D = 0" apply (simp add: nscderiv_def) apply (drule bspec, auto) done -lemma NSCDERIV_capprox: - "[| NSCDERIV f x :> D; h: CInfinitesimal; h \ 0 |] - ==> ( *f* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0" -apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric]) -apply (rule CInfinitesimal_ratio) -apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto) +lemma NSCDERIV_approx: + "[| NSCDERIV f x :> D; h: Infinitesimal; h \ 0 |] + ==> ( *f* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @= 0" +apply (simp add: nscderiv_def mem_infmal_iff [symmetric]) +apply (rule Infinitesimal_ratio) +apply (rule_tac [3] approx_hcomplex_of_complex_HFinite, auto) done @@ -822,11 +825,11 @@ lemma NSCDERIVD1: "[| NSCDERIV f (g x) :> Da; ( *f* g) (hcomplex_of_complex(x) + xa) \ hcomplex_of_complex (g x); - ( *f* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|] + ( *f* g) (hcomplex_of_complex(x) + xa) @= hcomplex_of_complex (g x)|] ==> (( *f* f) (( *f* g) (hcomplex_of_complex(x) + xa)) - hcomplex_of_complex (f (g x))) / (( *f* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) - @c= hcomplex_of_complex (Da)" + @= hcomplex_of_complex (Da)" by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def) (*--------------------------------------------------*) @@ -838,10 +841,10 @@ (*--------------------------------------------------*) lemma NSCDERIVD2: - "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \ 0 |] + "[| NSCDERIV g x :> Db; xa: Infinitesimal; xa \ 0 |] ==> (( *f* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa - @c= hcomplex_of_complex (Db)" -by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfun_lambda_cancel) + @= hcomplex_of_complex (Db)" +by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_infmal_iff starfun_lambda_cancel) lemma lemma_complex_chain: "(z::hcomplex) \ 0 ==> x*y = (x*inverse(z))*(z*y)" by auto @@ -851,17 +854,17 @@ theorem NSCDERIV_chain: "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] ==> NSCDERIV (f o g) x :> Da * Db" -apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric]) +apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_infmal_iff [symmetric]) apply safe -apply (frule_tac f = g in NSCDERIV_capprox) +apply (frule_tac f = g in NSCDERIV_approx) apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric]) apply (case_tac "( *f* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ") apply (drule_tac g = g in NSCDERIV_zero) apply (auto simp add: divide_inverse) apply (rule_tac z1 = "( *f* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst]) apply (simp (no_asm_simp)) -apply (rule capprox_mult_hcomplex_of_complex) -apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] +apply (rule approx_mult_hcomplex_of_complex) +apply (auto intro!: NSCDERIVD1 intro: approx_minus_iff [THEN iffD2] simp add: diff_minus [symmetric] divide_inverse [symmetric]) apply (blast intro: NSCDERIVD2) done @@ -914,8 +917,8 @@ by auto (*used once, in NSCDERIV_inverse*) -lemma CInfinitesimal_add_not_zero: - "[| h: CInfinitesimal; x \ 0 |] ==> hcomplex_of_complex x + h \ 0" +lemma Infinitesimal_add_not_zero: + "[| h: Infinitesimal; x \ 0 |] ==> hcomplex_of_complex x + h \ 0" apply clarify apply (drule equals_zero_I, auto) done @@ -924,7 +927,7 @@ lemma NSCDERIV_inverse: "x \ 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))" apply (simp add: nscderiv_def Ball_def, clarify) -apply (frule CInfinitesimal_add_not_zero [where x=x]) +apply (frule Infinitesimal_add_not_zero [where x=x]) apply (auto simp add: starfun_inverse_inverse diff_minus simp del: minus_mult_left [symmetric] minus_mult_right [symmetric]) apply (simp add: add_commute numeral_2_eq_2 inverse_add @@ -933,12 +936,12 @@ del: inverse_minus_eq inverse_mult_distrib minus_mult_right [symmetric] minus_mult_left [symmetric]) apply (simp only: mult_assoc [symmetric] right_distrib) -apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans) -apply (rule inverse_add_CInfinitesimal_capprox2) -apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal - intro: CFinite_mult - simp add: inverse_minus_eq [symmetric]) -apply (rule CInfinitesimal_CFinite_mult2, auto) +apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in approx_trans) +apply (rule inverse_add_Infinitesimal_approx2) +apply (auto dest!: hcomplex_of_complex_HFinite_diff_Infinitesimal + intro: HFinite_mult + simp add: inverse_minus_eq [symmetric] HFinite_minus_iff) +apply (rule Infinitesimal_HFinite_mult2, auto) done lemma CDERIV_inverse: diff -r 759c8f2ead69 -r 2116b7a371c7 src/HOL/Complex/CStar.thy --- a/src/HOL/Complex/CStar.thy Sun Sep 17 02:53:36 2006 +0200 +++ b/src/HOL/Complex/CStar.thy Sun Sep 17 02:56:25 2006 +0200 @@ -32,27 +32,11 @@ apply (simp add: star_of_def starfun star_n_eq_iff, ultra) done -lemma starfun_capprox: - "( *f* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)" -by auto - lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" apply (cases Z) apply (simp add: hcpow starfun hypnat_of_nat_eq) done -lemma starfun_mult_CFinite_capprox: - "[| ( *f* f) y @c= l; ( *f* g) y @c= m; l: CFinite; m: CFinite |] - ==> ( *f* (%x. f x * g x)) y @c= l * m" -apply (drule capprox_mult_CFinite, assumption+) -apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) -done - -lemma starfun_add_capprox: - "[| ( *f* f) y @c= l; ( *f* g) y @c= m |] - ==> ( *f* (%x. f x + g x)) y @c= l + m" -by (auto intro: capprox_add) - lemma starfunCR_cmod: "*f* cmod = hcmod" apply (rule ext) apply (rule_tac x = x in star_cases) @@ -79,14 +63,14 @@ done lemma starfunC_approx_Re_Im_iff: - "(( *f* f) x @c= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & + "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) & (( *f* (%x. Im(f x))) x @= hIm (z)))" apply (cases x, cases z) -apply (simp add: starfun hIm hRe capprox_approx_iff) +apply (simp add: starfun hIm hRe approx_approx_iff) done -lemma starfunC_Idfun_capprox: - "x @c= hcomplex_of_complex a ==> ( *f* (%x. x)) x @c= hcomplex_of_complex a" +lemma starfunC_Idfun_approx: + "x @= hcomplex_of_complex a ==> ( *f* (%x. x)) x @= hcomplex_of_complex a" by simp end diff -r 759c8f2ead69 -r 2116b7a371c7 src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Sun Sep 17 02:53:36 2006 +0200 +++ b/src/HOL/Complex/NSCA.thy Sun Sep 17 02:56:25 2006 +0200 @@ -10,34 +10,13 @@ begin definition - - CInfinitesimal :: "hcomplex set" - "CInfinitesimal = {x. \r \ Reals. 0 < r --> hcmod x < r}" - - capprox :: "[hcomplex,hcomplex] => bool" (infixl "@c=" 50) - --{*the ``infinitely close'' relation*} - "x @c= y = ((x - y) \ CInfinitesimal)" - (* standard complex numbers reagarded as an embedded subset of NS complex *) SComplex :: "hcomplex set" "SComplex = {x. \r. x = hcomplex_of_complex r}" - CFinite :: "hcomplex set" - "CFinite = {x. \r \ Reals. hcmod x < r}" - - CInfinite :: "hcomplex set" - "CInfinite = {x. \r \ Reals. r < hcmod x}" - stc :: "hcomplex => hcomplex" --{* standard part map*} - "stc x = (SOME r. x \ CFinite & r:SComplex & r @c= x)" - - cmonad :: "hcomplex => hcomplex set" - "cmonad x = {y. x @c= y}" - - cgalaxy :: "hcomplex => hcomplex set" - "cgalaxy x = {y. (x - y) \ CFinite}" - + "stc x = (SOME r. x \ HFinite & r:SComplex & r @= x)" subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} @@ -151,21 +130,8 @@ subsection{*The Finite Elements form a Subring*} -lemma CFinite_add: "[|x \ CFinite; y \ CFinite|] ==> (x+y) \ CFinite" -apply (simp add: CFinite_def) -apply (blast intro!: SReal_add hcmod_add_less) -done - -lemma CFinite_mult: "[|x \ CFinite; y \ CFinite|] ==> x*y \ CFinite" -apply (simp add: CFinite_def) -apply (blast intro!: SReal_mult hcmod_mult_less) -done - -lemma CFinite_minus_iff [simp]: "(-x \ CFinite) = (x \ CFinite)" -by (simp add: CFinite_def) - -lemma SComplex_subset_CFinite [simp]: "SComplex \ CFinite" -apply (auto simp add: SComplex_def CFinite_def) +lemma SComplex_subset_HFinite [simp]: "SComplex \ HFinite" +apply (auto simp add: SComplex_def HFinite_def) apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI) apply (auto intro: SReal_add) done @@ -174,491 +140,207 @@ "hcmod (hcomplex_of_complex r) \ HFinite" by (auto intro!: SReal_subset_HFinite [THEN subsetD]) -lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \ CFinite" -by (auto intro!: SComplex_subset_CFinite [THEN subsetD]) - -lemma CFiniteD: "x \ CFinite ==> \t \ Reals. hcmod x < t" -by (simp add: CFinite_def) +lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \ HFinite" +by (rule HFinite_star_of) -lemma CFinite_hcmod_iff: "(x \ CFinite) = (hcmod x \ HFinite)" -by (simp add: CFinite_def HFinite_def) +lemma HFinite_hcmod_iff: "(x \ HFinite) = (hcmod x \ HFinite)" +by (simp add: HFinite_def) -lemma CFinite_number_of [simp]: "number_of w \ CFinite" -by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]]) - -lemma CFinite_bounded: "[|x \ CFinite; y \ hcmod x; 0 \ y |] ==> y: HFinite" -by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff) +lemma HFinite_bounded_hcmod: + "[|x \ HFinite; y \ hcmod x; 0 \ y |] ==> y: HFinite" +by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff) subsection{*The Complex Infinitesimals form a Subring*} - -lemma CInfinitesimal_zero [iff]: "0 \ CInfinitesimal" -by (simp add: CInfinitesimal_def) lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x" by auto -lemma CInfinitesimal_hcmod_iff: - "(z \ CInfinitesimal) = (hcmod z \ Infinitesimal)" -by (simp add: CInfinitesimal_def Infinitesimal_def) - -lemma one_not_CInfinitesimal [simp]: "1 \ CInfinitesimal" -by (simp add: CInfinitesimal_hcmod_iff) +lemma Infinitesimal_hcmod_iff: + "(z \ Infinitesimal) = (hcmod z \ Infinitesimal)" +by (simp add: Infinitesimal_def) -lemma CInfinitesimal_add: - "[| x \ CInfinitesimal; y \ CInfinitesimal |] ==> (x+y) \ CInfinitesimal" -apply (auto simp add: CInfinitesimal_hcmod_iff) -apply (rule hrabs_le_Infinitesimal) -apply (rule_tac y = "hcmod y" in Infinitesimal_add, auto) -done - -lemma CInfinitesimal_minus_iff [simp]: - "(-x:CInfinitesimal) = (x:CInfinitesimal)" -by (simp add: CInfinitesimal_def) - -lemma CInfinitesimal_diff: - "[| x \ CInfinitesimal; y \ CInfinitesimal |] ==> x-y \ CInfinitesimal" -by (simp add: diff_minus CInfinitesimal_add) - -lemma CInfinitesimal_mult: - "[| x \ CInfinitesimal; y \ CInfinitesimal |] ==> x * y \ CInfinitesimal" -by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult) +lemma HInfinite_hcmod_iff: "(z \ HInfinite) = (hcmod z \ HInfinite)" +by (simp add: HInfinite_def) -lemma CInfinitesimal_CFinite_mult: - "[| x \ CInfinitesimal; y \ CFinite |] ==> (x * y) \ CInfinitesimal" -by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult) - -lemma CInfinitesimal_CFinite_mult2: - "[| x \ CInfinitesimal; y \ CFinite |] ==> (y * x) \ CInfinitesimal" -by (auto dest: CInfinitesimal_CFinite_mult simp add: mult_commute) - -lemma CInfinite_hcmod_iff: "(z \ CInfinite) = (hcmod z \ HInfinite)" -by (simp add: CInfinite_def HInfinite_def) +lemma HFinite_diff_Infinitesimal_hcmod: + "x \ HFinite - Infinitesimal ==> hcmod x \ HFinite - Infinitesimal" +by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff) -lemma CInfinite_inverse_CInfinitesimal: - "x \ CInfinite ==> inverse x \ CInfinitesimal" -by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse) - -lemma CInfinite_mult: "[|x \ CInfinite; y \ CInfinite|] ==> (x*y): CInfinite" -by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult) +lemma hcmod_less_Infinitesimal: + "[| e \ Infinitesimal; hcmod x < hcmod e |] ==> x \ Infinitesimal" +by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff) -lemma CInfinite_minus_iff [simp]: "(-x \ CInfinite) = (x \ CInfinite)" -by (simp add: CInfinite_def) - -lemma CFinite_sum_squares: - "[|a \ CFinite; b \ CFinite; c \ CFinite|] - ==> a*a + b*b + c*c \ CFinite" -by (auto intro: CFinite_mult CFinite_add) - -lemma not_CInfinitesimal_not_zero: "x \ CInfinitesimal ==> x \ 0" -by auto +lemma hcmod_le_Infinitesimal: + "[| e \ Infinitesimal; hcmod x \ hcmod e |] ==> x \ Infinitesimal" +by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff) -lemma not_CInfinitesimal_not_zero2: "x \ CFinite - CInfinitesimal ==> x \ 0" -by auto - -lemma CFinite_diff_CInfinitesimal_hcmod: - "x \ CFinite - CInfinitesimal ==> hcmod x \ HFinite - Infinitesimal" -by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff) - -lemma hcmod_less_CInfinitesimal: - "[| e \ CInfinitesimal; hcmod x < hcmod e |] ==> x \ CInfinitesimal" -by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff) +lemma Infinitesimal_interval_hcmod: + "[| e \ Infinitesimal; + e' \ Infinitesimal; + hcmod e' < hcmod x ; hcmod x < hcmod e + |] ==> x \ Infinitesimal" +by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff) -lemma hcmod_le_CInfinitesimal: - "[| e \ CInfinitesimal; hcmod x \ hcmod e |] ==> x \ CInfinitesimal" -by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff) - -lemma CInfinitesimal_interval: - "[| e \ CInfinitesimal; - e' \ CInfinitesimal; - hcmod e' < hcmod x ; hcmod x < hcmod e - |] ==> x \ CInfinitesimal" -by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff) - -lemma CInfinitesimal_interval2: - "[| e \ CInfinitesimal; - e' \ CInfinitesimal; +lemma Infinitesimal_interval2_hcmod: + "[| e \ Infinitesimal; + e' \ Infinitesimal; hcmod e' \ hcmod x ; hcmod x \ hcmod e - |] ==> x \ CInfinitesimal" -by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff) - -lemma not_CInfinitesimal_mult: - "[| x \ CInfinitesimal; y \ CInfinitesimal|] ==> (x*y) \ CInfinitesimal" -apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult) -apply (drule not_Infinitesimal_mult, auto) -done - -lemma CInfinitesimal_mult_disj: - "x*y \ CInfinitesimal ==> x \ CInfinitesimal | y \ CInfinitesimal" -by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult) + |] ==> x \ Infinitesimal" +by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff) -lemma CFinite_CInfinitesimal_diff_mult: - "[| x \ CFinite - CInfinitesimal; y \ CFinite - CInfinitesimal |] - ==> x*y \ CFinite - CInfinitesimal" -by (blast dest: CFinite_mult not_CInfinitesimal_mult) +lemma Infinitesimal_hcomplex_of_complex_mult: + "x \ Infinitesimal ==> x * hcomplex_of_complex r \ Infinitesimal" +by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult) -lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \ CFinite" -by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff) - -lemma CInfinitesimal_hcomplex_of_complex_mult: - "x \ CInfinitesimal ==> x * hcomplex_of_complex r \ CInfinitesimal" -by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult) - -lemma CInfinitesimal_hcomplex_of_complex_mult2: - "x \ CInfinitesimal ==> hcomplex_of_complex r * x \ CInfinitesimal" -by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult) +lemma Infinitesimal_hcomplex_of_complex_mult2: + "x \ Infinitesimal ==> hcomplex_of_complex r * x \ Infinitesimal" +by (auto intro!: Infinitesimal_HFinite_mult2 simp add: Infinitesimal_hcmod_iff hcmod_mult) subsection{*The ``Infinitely Close'' Relation*} (* Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)" -by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_hcmod_iff])); +by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); *) -lemma mem_cinfmal_iff: "x:CInfinitesimal = (x @c= 0)" -by (simp add: CInfinitesimal_hcmod_iff capprox_def) - -lemma capprox_minus_iff: "(x @c= y) = (x + -y @c= 0)" -by (simp add: capprox_def diff_minus) - -lemma capprox_minus_iff2: "(x @c= y) = (-y + x @c= 0)" -by (simp add: capprox_def diff_minus add_commute) - -lemma capprox_refl [simp]: "x @c= x" -by (simp add: capprox_def) - -lemma capprox_sym: "x @c= y ==> y @c= x" -by (simp add: capprox_def CInfinitesimal_def hcmod_diff_commute) - -lemma capprox_trans: "[| x @c= y; y @c= z |] ==> x @c= z" -apply (simp add: capprox_def) -apply (drule CInfinitesimal_add, assumption) -apply (simp add: diff_minus) -done - -lemma capprox_trans2: "[| r @c= x; s @c= x |] ==> r @c= s" -by (blast intro: capprox_sym capprox_trans) +lemma approx_mult_subst_SComplex: + "[| u @= x*hcomplex_of_complex v; x @= y |] + ==> u @= y*hcomplex_of_complex v" +by (auto intro: approx_mult_subst2) -lemma capprox_trans3: "[| x @c= r; x @c= s|] ==> r @c= s" -by (blast intro: capprox_sym capprox_trans) - -lemma number_of_capprox_reorient [simp]: - "(number_of w @c= x) = (x @c= number_of w)" -by (blast intro: capprox_sym) - -lemma CInfinitesimal_capprox_minus: "(x-y \ CInfinitesimal) = (x @c= y)" -by (simp add: diff_minus capprox_minus_iff [symmetric] mem_cinfmal_iff) - -lemma capprox_monad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))" -by (auto simp add: cmonad_def dest: capprox_sym elim!: capprox_trans equalityCE) - -lemma Infinitesimal_capprox: - "[| x \ CInfinitesimal; y \ CInfinitesimal |] ==> x @c= y" -apply (simp add: mem_cinfmal_iff) -apply (blast intro: capprox_trans capprox_sym) -done - -lemma capprox_add: "[| a @c= b; c @c= d |] ==> a+c @c= b+d" -apply (simp add: capprox_def diff_minus) -apply (rule minus_add_distrib [THEN ssubst]) -apply (rule add_assoc [THEN ssubst]) -apply (rule_tac b1 = c in add_left_commute [THEN subst]) -apply (rule add_assoc [THEN subst]) -apply (blast intro: CInfinitesimal_add) -done +lemma approx_hcomplex_of_complex_HFinite: + "x @= hcomplex_of_complex D ==> x \ HFinite" +by (rule approx_star_of_HFinite) -lemma capprox_minus: "a @c= b ==> -a @c= -b" -apply (rule capprox_minus_iff [THEN iffD2, THEN capprox_sym]) -apply (drule capprox_minus_iff [THEN iffD1]) -apply (simp add: add_commute) -done - -lemma capprox_minus2: "-a @c= -b ==> a @c= b" -by (auto dest: capprox_minus) - -lemma capprox_minus_cancel [simp]: "(-a @c= -b) = (a @c= b)" -by (blast intro: capprox_minus capprox_minus2) - -lemma capprox_add_minus: "[| a @c= b; c @c= d |] ==> a + -c @c= b + -d" -by (blast intro!: capprox_add capprox_minus) - -lemma capprox_mult1: - "[| a @c= b; c \ CFinite|] ==> a*c @c= b*c" -apply (simp add: capprox_def diff_minus) -apply (simp only: CInfinitesimal_CFinite_mult minus_mult_left left_distrib [symmetric]) -done - -lemma capprox_mult2: "[|a @c= b; c \ CFinite|] ==> c*a @c= c*b" -by (simp add: capprox_mult1 mult_commute) +lemma approx_mult_hcomplex_of_complex: + "[|a @= hcomplex_of_complex b; c @= hcomplex_of_complex d |] + ==> a*c @= hcomplex_of_complex b * hcomplex_of_complex d" +by (rule approx_mult_star_of) -lemma capprox_mult_subst: - "[|u @c= v*x; x @c= y; v \ CFinite|] ==> u @c= v*y" -by (blast intro: capprox_mult2 capprox_trans) - -lemma capprox_mult_subst2: - "[| u @c= x*v; x @c= y; v \ CFinite |] ==> u @c= y*v" -by (blast intro: capprox_mult1 capprox_trans) - -lemma capprox_mult_subst_SComplex: - "[| u @c= x*hcomplex_of_complex v; x @c= y |] - ==> u @c= y*hcomplex_of_complex v" -by (auto intro: capprox_mult_subst2) - -lemma capprox_eq_imp: "a = b ==> a @c= b" -by (simp add: capprox_def) - -lemma CInfinitesimal_minus_capprox: "x \ CInfinitesimal ==> -x @c= x" -by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2) - -lemma bex_CInfinitesimal_iff: "(\y \ CInfinitesimal. x - z = y) = (x @c= z)" -by (unfold capprox_def, blast) - -lemma bex_CInfinitesimal_iff2: "(\y \ CInfinitesimal. x = z + y) = (x @c= z)" -by (simp add: bex_CInfinitesimal_iff [symmetric], force) - -lemma CInfinitesimal_add_capprox: - "[| y \ CInfinitesimal; x + y = z |] ==> x @c= z" -apply (rule bex_CInfinitesimal_iff [THEN iffD1]) -apply (drule CInfinitesimal_minus_iff [THEN iffD2]) -apply (simp add: eq_commute compare_rls) +lemma approx_SComplex_mult_cancel_zero: + "[| a \ SComplex; a \ 0; a*x @= 0 |] ==> x @= 0" +apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) +apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done -lemma CInfinitesimal_add_capprox_self: "y \ CInfinitesimal ==> x @c= x + y" -apply (rule bex_CInfinitesimal_iff [THEN iffD1]) -apply (drule CInfinitesimal_minus_iff [THEN iffD2]) -apply (simp add: eq_commute compare_rls) -done - -lemma CInfinitesimal_add_capprox_self2: "y \ CInfinitesimal ==> x @c= y + x" -by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute) - -lemma CInfinitesimal_add_minus_capprox_self: - "y \ CInfinitesimal ==> x @c= x + -y" -by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2]) +lemma approx_mult_SComplex1: "[| a \ SComplex; x @= 0 |] ==> x*a @= 0" +by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1) -lemma CInfinitesimal_add_cancel: - "[| y \ CInfinitesimal; x+y @c= z|] ==> x @c= z" -apply (drule_tac x = x in CInfinitesimal_add_capprox_self [THEN capprox_sym]) -apply (erule capprox_trans3 [THEN capprox_sym], assumption) -done - -lemma CInfinitesimal_add_right_cancel: - "[| y \ CInfinitesimal; x @c= z + y|] ==> x @c= z" -apply (drule_tac x = z in CInfinitesimal_add_capprox_self2 [THEN capprox_sym]) -apply (erule capprox_trans3 [THEN capprox_sym]) -apply (simp add: add_commute) -apply (erule capprox_sym) -done +lemma approx_mult_SComplex2: "[| a \ SComplex; x @= 0 |] ==> a*x @= 0" +by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult2) -lemma capprox_add_left_cancel: "d + b @c= d + c ==> b @c= c" -apply (drule capprox_minus_iff [THEN iffD1]) -apply (simp add: minus_add_distrib capprox_minus_iff [symmetric] add_ac) -done - -lemma capprox_add_right_cancel: "b + d @c= c + d ==> b @c= c" -apply (rule capprox_add_left_cancel) -apply (simp add: add_commute) -done - -lemma capprox_add_mono1: "b @c= c ==> d + b @c= d + c" -apply (rule capprox_minus_iff [THEN iffD2]) -apply (simp add: capprox_minus_iff [symmetric] add_ac) -done +lemma approx_mult_SComplex_zero_cancel_iff [simp]: + "[|a \ SComplex; a \ 0 |] ==> (a*x @= 0) = (x @= 0)" +by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2) -lemma capprox_add_mono2: "b @c= c ==> b + a @c= c + a" -apply (simp (no_asm_simp) add: add_commute capprox_add_mono1) -done - -lemma capprox_add_left_iff [iff]: "(a + b @c= a + c) = (b @c= c)" -by (fast elim: capprox_add_left_cancel capprox_add_mono1) - -lemma capprox_add_right_iff [iff]: "(b + a @c= c + a) = (b @c= c)" -by (simp add: add_commute) - -lemma capprox_CFinite: "[| x \ CFinite; x @c= y |] ==> y \ CFinite" -apply (drule bex_CInfinitesimal_iff2 [THEN iffD2], safe) -apply (drule CInfinitesimal_subset_CFinite [THEN subsetD, THEN CFinite_minus_iff [THEN iffD2]]) -apply (drule CFinite_add) -apply (assumption, auto) +lemma approx_SComplex_mult_cancel: + "[| a \ SComplex; a \ 0; a* w @= a*z |] ==> w @= z" +apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) +apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done -lemma capprox_hcomplex_of_complex_CFinite: - "x @c= hcomplex_of_complex D ==> x \ CFinite" -by (rule capprox_sym [THEN [2] capprox_CFinite], auto) +lemma approx_SComplex_mult_cancel_iff1 [simp]: + "[| a \ SComplex; a \ 0|] ==> (a* w @= a*z) = (w @= z)" +by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD] + intro: approx_SComplex_mult_cancel) -lemma capprox_mult_CFinite: - "[|a @c= b; c @c= d; b \ CFinite; d \ CFinite|] ==> a*c @c= b*d" -apply (rule capprox_trans) -apply (rule_tac [2] capprox_mult2) -apply (rule capprox_mult1) -prefer 2 apply (blast intro: capprox_CFinite capprox_sym, auto) -done - -lemma capprox_mult_hcomplex_of_complex: - "[|a @c= hcomplex_of_complex b; c @c= hcomplex_of_complex d |] - ==> a*c @c= hcomplex_of_complex b * hcomplex_of_complex d" -apply (blast intro!: capprox_mult_CFinite capprox_hcomplex_of_complex_CFinite CFinite_hcomplex_of_complex) -done - -lemma capprox_SComplex_mult_cancel_zero: - "[| a \ SComplex; a \ 0; a*x @c= 0 |] ==> x @c= 0" -apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]]) -apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) +lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)" +apply (subst hcmod_diff_commute) +apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) done -lemma capprox_mult_SComplex1: "[| a \ SComplex; x @c= 0 |] ==> x*a @c= 0" -by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1) - -lemma capprox_mult_SComplex2: "[| a \ SComplex; x @c= 0 |] ==> a*x @c= 0" -by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult2) - -lemma capprox_mult_SComplex_zero_cancel_iff [simp]: - "[|a \ SComplex; a \ 0 |] ==> (a*x @c= 0) = (x @c= 0)" -by (blast intro: capprox_SComplex_mult_cancel_zero capprox_mult_SComplex2) - -lemma capprox_SComplex_mult_cancel: - "[| a \ SComplex; a \ 0; a* w @c= a*z |] ==> w @c= z" -apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]]) -apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) -done +lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)" +by (simp add: approx_hcmod_approx_zero) -lemma capprox_SComplex_mult_cancel_iff1 [simp]: - "[| a \ SComplex; a \ 0|] ==> (a* w @c= a*z) = (w @c= z)" -by (auto intro!: capprox_mult2 SComplex_subset_CFinite [THEN subsetD] - intro: capprox_SComplex_mult_cancel) - -lemma capprox_hcmod_approx_zero: "(x @c= y) = (hcmod (y - x) @= 0)" -apply (rule capprox_minus_iff [THEN ssubst]) -apply (simp add: capprox_def CInfinitesimal_hcmod_iff mem_infmal_iff diff_minus [symmetric] hcmod_diff_commute) -done - -lemma capprox_approx_zero_iff: "(x @c= 0) = (hcmod x @= 0)" -by (simp add: capprox_hcmod_approx_zero) - -lemma capprox_minus_zero_cancel_iff [simp]: "(-x @c= 0) = (x @c= 0)" -by (simp add: capprox_hcmod_approx_zero) +lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)" +by (simp add: approx_def) lemma Infinitesimal_hcmod_add_diff: - "u @c= 0 ==> hcmod(x + u) - hcmod x \ Infinitesimal" + "u @= 0 ==> hcmod(x + u) - hcmod x \ Infinitesimal" +apply (drule approx_approx_zero_iff [THEN iffD1]) apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2) -apply (auto dest: capprox_approx_zero_iff [THEN iffD1] - simp add: mem_infmal_iff [symmetric] diff_def) +apply (auto simp add: mem_infmal_iff [symmetric] diff_def) apply (rule_tac c1 = "hcmod x" in add_le_cancel_left [THEN iffD1]) apply (auto simp add: diff_minus [symmetric]) done -lemma approx_hcmod_add_hcmod: "u @c= 0 ==> hcmod(x + u) @= hcmod x" +lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x" apply (rule approx_minus_iff [THEN iffD2]) apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) done -lemma capprox_hcmod_approx: "x @c= y ==> hcmod x @= hcmod y" +lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y" by (auto intro: approx_hcmod_add_hcmod - dest!: bex_CInfinitesimal_iff2 [THEN iffD2] - simp add: mem_cinfmal_iff) + dest!: bex_Infinitesimal_iff2 [THEN iffD2] + simp add: mem_infmal_iff) subsection{*Zero is the Only Infinitesimal Complex Number*} -lemma CInfinitesimal_less_SComplex: - "[| x \ SComplex; y \ CInfinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x" -by (auto intro!: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: CInfinitesimal_hcmod_iff) +lemma Infinitesimal_less_SComplex: + "[| x \ SComplex; y \ Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x" +by (auto intro: Infinitesimal_less_SReal SComplex_hcmod_SReal simp add: Infinitesimal_hcmod_iff) -lemma SComplex_Int_CInfinitesimal_zero: "SComplex Int CInfinitesimal = {0}" -apply (auto simp add: SComplex_def CInfinitesimal_hcmod_iff) -apply (cut_tac r = r in SReal_hcmod_hcomplex_of_complex) -apply (drule_tac A = Reals in IntI, assumption) -apply (subgoal_tac "hcmod (hcomplex_of_complex r) = 0") -apply simp -apply (simp add: SReal_Int_Infinitesimal_zero) -done - -lemma SComplex_CInfinitesimal_zero: - "[| x \ SComplex; x \ CInfinitesimal|] ==> x = 0" -by (cut_tac SComplex_Int_CInfinitesimal_zero, blast) +lemma SComplex_Int_Infinitesimal_zero: "SComplex Int Infinitesimal = {0}" +by (auto simp add: SComplex_def Infinitesimal_hcmod_iff) -lemma SComplex_CFinite_diff_CInfinitesimal: - "[| x \ SComplex; x \ 0 |] ==> x \ CFinite - CInfinitesimal" -by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD]) - -lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal: - "hcomplex_of_complex x \ 0 - ==> hcomplex_of_complex x \ CFinite - CInfinitesimal" -by (rule SComplex_CFinite_diff_CInfinitesimal, auto) +lemma SComplex_Infinitesimal_zero: + "[| x \ SComplex; x \ Infinitesimal|] ==> x = 0" +by (cut_tac SComplex_Int_Infinitesimal_zero, blast) -lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]: - "(hcomplex_of_complex x \ CInfinitesimal) = (x=0)" -apply (auto) -apply (rule ccontr) -apply (rule hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN DiffD2], auto) -done +lemma SComplex_HFinite_diff_Infinitesimal: + "[| x \ SComplex; x \ 0 |] ==> x \ HFinite - Infinitesimal" +by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD]) -lemma number_of_not_CInfinitesimal [simp]: - "number_of w \ (0::hcomplex) ==> number_of w \ CInfinitesimal" -by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero]) +lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: + "hcomplex_of_complex x \ 0 + ==> hcomplex_of_complex x \ HFinite - Infinitesimal" +by (rule SComplex_HFinite_diff_Infinitesimal, auto) -lemma capprox_SComplex_not_zero: - "[| y \ SComplex; x @c= y; y\ 0 |] ==> x \ 0" -by (auto dest: SComplex_CInfinitesimal_zero capprox_sym [THEN mem_cinfmal_iff [THEN iffD2]]) +lemma hcomplex_of_complex_Infinitesimal_iff_0: + "(hcomplex_of_complex x \ Infinitesimal) = (x=0)" +by (rule star_of_Infinitesimal_iff_0) -lemma CFinite_diff_CInfinitesimal_capprox: - "[| x @c= y; y \ CFinite - CInfinitesimal |] - ==> x \ CFinite - CInfinitesimal" -apply (auto intro: capprox_sym [THEN [2] capprox_CFinite] - simp add: mem_cinfmal_iff) -apply (drule capprox_trans3, assumption) -apply (blast dest: capprox_sym) -done +lemma number_of_not_Infinitesimal [simp]: + "number_of w \ (0::hcomplex) ==> (number_of w::hcomplex) \ Infinitesimal" +by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) -lemma CInfinitesimal_ratio: - "[| y \ 0; y \ CInfinitesimal; x/y \ CFinite |] ==> x \ CInfinitesimal" -apply (drule CInfinitesimal_CFinite_mult2, assumption) -apply (simp add: divide_inverse mult_assoc) -done +lemma approx_SComplex_not_zero: + "[| y \ SComplex; x @= y; y\ 0 |] ==> x \ 0" +by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) -lemma SComplex_capprox_iff: - "[|x \ SComplex; y \ SComplex|] ==> (x @c= y) = (x = y)" -apply auto -apply (simp add: capprox_def) -apply (subgoal_tac "x-y = 0", simp) -apply (rule SComplex_CInfinitesimal_zero) -apply (simp add: SComplex_diff, assumption) -done +lemma SComplex_approx_iff: + "[|x \ SComplex; y \ SComplex|] ==> (x @= y) = (x = y)" +by (auto simp add: SComplex_def) -lemma number_of_capprox_iff [simp]: - "(number_of v @c= number_of w) = (number_of v = (number_of w :: hcomplex))" -by (rule SComplex_capprox_iff, auto) - -lemma number_of_CInfinitesimal_iff [simp]: - "(number_of w \ CInfinitesimal) = (number_of w = (0::hcomplex))" +lemma number_of_Infinitesimal_iff [simp]: + "((number_of w :: hcomplex) \ Infinitesimal) = + (number_of w = (0::hcomplex))" apply (rule iffI) -apply (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero]) +apply (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) apply (simp (no_asm_simp)) done -lemma hcomplex_of_complex_approx_iff [simp]: - "(hcomplex_of_complex k @c= hcomplex_of_complex m) = (k = m)" -apply auto -apply (rule inj_hcomplex_of_complex [THEN injD]) -apply (rule SComplex_capprox_iff [THEN iffD1], auto) -done +lemma hcomplex_of_complex_approx_iff: + "(hcomplex_of_complex k @= hcomplex_of_complex m) = (k = m)" +by (rule star_of_approx_iff) -lemma hcomplex_of_complex_capprox_number_of_iff [simp]: - "(hcomplex_of_complex k @c= number_of w) = (k = number_of w)" +lemma hcomplex_of_complex_approx_number_of_iff [simp]: + "(hcomplex_of_complex k @= number_of w) = (k = number_of w)" by (subst hcomplex_of_complex_approx_iff [symmetric], auto) -lemma capprox_unique_complex: - "[| r \ SComplex; s \ SComplex; r @c= x; s @c= x|] ==> r = s" -by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2) +lemma approx_unique_complex: + "[| r \ SComplex; s \ SComplex; r @= x; s @= x|] ==> r = s" +by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) -lemma hcomplex_capproxD1: - "star_n X @c= star_n Y +lemma hcomplex_approxD1: + "star_n X @= star_n Y ==> star_n (%n. Re(X n)) @= star_n (%n. Re(Y n))" -apply (simp add: approx_FreeUltrafilterNat_iff2, safe) -apply (drule capprox_minus_iff [THEN iffD1]) -apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) +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 (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) @@ -669,12 +351,12 @@ done (* same proof *) -lemma hcomplex_capproxD2: - "star_n X @c= star_n Y +lemma hcomplex_approxD2: + "star_n X @= star_n Y ==> star_n (%n. Im(X n)) @= star_n (%n. Im(Y n))" -apply (simp add: approx_FreeUltrafilterNat_iff2, safe) -apply (drule capprox_minus_iff [THEN iffD1]) -apply (simp add: star_n_minus star_n_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2) +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 (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) @@ -684,14 +366,14 @@ simp del: realpow_Suc) done -lemma hcomplex_capproxI: +lemma hcomplex_approxI: "[| star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)); star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)) - |] ==> star_n X @c= star_n Y" + |] ==> star_n X @= star_n Y" apply (drule approx_minus_iff [THEN iffD1]) apply (drule approx_minus_iff [THEN iffD1]) -apply (rule capprox_minus_iff [THEN iffD2]) -apply (auto simp add: mem_cinfmal_iff [symmetric] mem_infmal_iff [symmetric] star_n_add star_n_minus CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) +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 (drule_tac x = "u/2" in spec) apply (drule_tac x = "u/2" in spec, auto, ultra) apply (case_tac "X x") @@ -703,23 +385,23 @@ apply (simp add: power2_eq_square) done -lemma capprox_approx_iff: - "(star_n X @c= star_n Y) = +lemma approx_approx_iff: + "(star_n X @= star_n Y) = (star_n (%n. Re(X n)) @= star_n (%n. Re(Y n)) & star_n (%n. Im(X n)) @= star_n (%n. Im(Y n)))" -apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2) +apply (blast intro: hcomplex_approxI hcomplex_approxD1 hcomplex_approxD2) done -lemma hcomplex_of_hypreal_capprox_iff [simp]: - "(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)" +lemma hcomplex_of_hypreal_approx_iff [simp]: + "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)" apply (cases x, cases z) -apply (simp add: hcomplex_of_hypreal capprox_approx_iff) +apply (simp add: hcomplex_of_hypreal approx_approx_iff) done -lemma CFinite_HFinite_Re: - "star_n X \ CFinite +lemma HFinite_HFinite_Re: + "star_n X \ HFinite ==> star_n (%n. Re(X n)) \ HFinite" -apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) +apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rule_tac x = u in exI, ultra) apply (case_tac "X x") apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc) @@ -729,10 +411,10 @@ apply (auto simp add: numeral_2_eq_2 [symmetric]) done -lemma CFinite_HFinite_Im: - "star_n X \ CFinite +lemma HFinite_HFinite_Im: + "star_n X \ HFinite ==> star_n (%n. Im(X n)) \ HFinite" -apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) +apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rule_tac x = u in exI, ultra) apply (case_tac "X x") apply (auto simp add: complex_mod simp del: realpow_Suc) @@ -741,11 +423,11 @@ apply (drule real_sqrt_ge_abs2 [THEN [2] order_less_le_trans], auto) done -lemma HFinite_Re_Im_CFinite: +lemma HFinite_Re_Im_HFinite: "[| star_n (%n. Re(X n)) \ HFinite; star_n (%n. Im(X n)) \ HFinite - |] ==> star_n X \ CFinite" -apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) + |] ==> star_n X \ HFinite" +apply (auto simp add: HFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rename_tac u v) apply (rule_tac x = "2* (u + v) " in exI) apply ultra @@ -760,11 +442,11 @@ apply (simp add: power2_eq_square) done -lemma CFinite_HFinite_iff: - "(star_n X \ CFinite) = +lemma HFinite_HFinite_iff: + "(star_n X \ HFinite) = (star_n (%n. Re(X n)) \ HFinite & star_n (%n. Im(X n)) \ HFinite)" -by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re) +by (blast intro: HFinite_Re_Im_HFinite HFinite_HFinite_Im HFinite_HFinite_Re) lemma SComplex_Re_SReal: "star_n X \ SComplex @@ -794,11 +476,11 @@ star_n (%n. Im(X n)) \ Reals)" by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) -lemma CInfinitesimal_Infinitesimal_iff: - "(star_n X \ CInfinitesimal) = +lemma Infinitesimal_Infinitesimal_iff: + "(star_n X \ Infinitesimal) = (star_n (%n. Re(X n)) \ Infinitesimal & star_n (%n. Im(X n)) \ Infinitesimal)" -by (simp add: mem_cinfmal_iff mem_infmal_iff star_n_zero_num capprox_approx_iff) +by (simp add: mem_infmal_iff star_n_zero_num approx_approx_iff) lemma eq_Abs_star_EX: "(\t. P t) = (\X. P (star_n X))" @@ -809,9 +491,9 @@ by (simp add: Bex_def ex_star_eq) (* Here we go - easy proof now!! *) -lemma stc_part_Ex: "x:CFinite ==> \t \ SComplex. x @c= t" +lemma stc_part_Ex: "x:HFinite ==> \t \ SComplex. x @= t" apply (cases x) -apply (auto simp add: CFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff capprox_approx_iff) +apply (auto simp add: HFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff approx_approx_iff) apply (drule st_part_Ex, safe)+ apply (rule_tac x = t in star_cases) apply (rule_tac x = ta in star_cases, auto) @@ -819,215 +501,99 @@ apply auto done -lemma stc_part_Ex1: "x:CFinite ==> EX! t. t \ SComplex & x @c= t" +lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \ SComplex & x @= t" apply (drule stc_part_Ex, safe) -apply (drule_tac [2] capprox_sym, drule_tac [2] capprox_sym, drule_tac [2] capprox_sym) -apply (auto intro!: capprox_unique_complex) -done - -lemma CFinite_Int_CInfinite_empty: "CFinite Int CInfinite = {}" -by (simp add: CFinite_def CInfinite_def, auto) - -lemma CFinite_not_CInfinite: "x \ CFinite ==> x \ CInfinite" -by (insert CFinite_Int_CInfinite_empty, blast) - -text{*Not sure this is a good idea!*} -declare CFinite_Int_CInfinite_empty [simp] - -lemma not_CFinite_CInfinite: "x\ CFinite ==> x \ CInfinite" -by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff) - -lemma CInfinite_CFinite_disj: "x \ CInfinite | x \ CFinite" -by (blast intro: not_CFinite_CInfinite) - -lemma CInfinite_CFinite_iff: "(x \ CInfinite) = (x \ CFinite)" -by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite) - -lemma CFinite_CInfinite_iff: "(x \ CFinite) = (x \ CInfinite)" -by (simp add: CInfinite_CFinite_iff) - -lemma CInfinite_diff_CFinite_CInfinitesimal_disj: - "x \ CInfinitesimal ==> x \ CInfinite | x \ CFinite - CInfinitesimal" -by (fast intro: not_CFinite_CInfinite) - -lemma CFinite_inverse: - "[| x \ CFinite; x \ CInfinitesimal |] ==> inverse x \ CFinite" -apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj) -apply (auto dest!: CInfinite_inverse_CInfinitesimal) -done - -lemma CFinite_inverse2: "x \ CFinite - CInfinitesimal ==> inverse x \ CFinite" -by (blast intro: CFinite_inverse) - -lemma CInfinitesimal_inverse_CFinite: - "x \ CInfinitesimal ==> inverse(x) \ CFinite" -apply (drule CInfinite_diff_CFinite_CInfinitesimal_disj) -apply (blast intro: CFinite_inverse CInfinite_inverse_CInfinitesimal CInfinitesimal_subset_CFinite [THEN subsetD]) +apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym) +apply (auto intro!: approx_unique_complex) done - -lemma CFinite_not_CInfinitesimal_inverse: - "x \ CFinite - CInfinitesimal ==> inverse x \ CFinite - CInfinitesimal" -apply (auto intro: CInfinitesimal_inverse_CFinite) -apply (drule CInfinitesimal_CFinite_mult2, assumption) -apply (simp add: not_CInfinitesimal_not_zero) -done - -lemma capprox_inverse: - "[| x @c= y; y \ CFinite - CInfinitesimal |] ==> inverse x @c= inverse y" -apply (frule CFinite_diff_CInfinitesimal_capprox, assumption) -apply (frule not_CInfinitesimal_not_zero2) -apply (frule_tac x = x in not_CInfinitesimal_not_zero2) -apply (drule CFinite_inverse2)+ -apply (drule capprox_mult2, assumption, auto) -apply (drule_tac c = "inverse x" in capprox_mult1, assumption) -apply (auto intro: capprox_sym simp add: mult_assoc) -done - -lemmas hcomplex_of_complex_capprox_inverse = - hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse] - -lemma inverse_add_CInfinitesimal_capprox: - "[| x \ CFinite - CInfinitesimal; - h \ CInfinitesimal |] ==> inverse(x + h) @c= inverse x" -by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self) - -lemma inverse_add_CInfinitesimal_capprox2: - "[| x \ CFinite - CInfinitesimal; - h \ CInfinitesimal |] ==> inverse(h + x) @c= inverse x" -apply (rule add_commute [THEN subst]) -apply (blast intro: inverse_add_CInfinitesimal_capprox) -done - -lemma inverse_add_CInfinitesimal_approx_CInfinitesimal: - "[| x \ CFinite - CInfinitesimal; - h \ CInfinitesimal |] ==> inverse(x + h) - inverse x @c= h" -apply (rule capprox_trans2) -apply (auto intro: inverse_add_CInfinitesimal_capprox - simp add: mem_cinfmal_iff diff_minus capprox_minus_iff [symmetric]) -done - -lemma CInfinitesimal_square_iff [iff]: - "(x*x \ CInfinitesimal) = (x \ CInfinitesimal)" -by (simp add: CInfinitesimal_hcmod_iff hcmod_mult) - -lemma capprox_CFinite_mult_cancel: - "[| a \ CFinite-CInfinitesimal; a*w @c= a*z |] ==> w @c= z" -apply safe -apply (frule CFinite_inverse, assumption) -apply (drule not_CInfinitesimal_not_zero) -apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric]) -done - -lemma capprox_CFinite_mult_cancel_iff1: - "a \ CFinite-CInfinitesimal ==> (a * w @c= a * z) = (w @c= z)" -by (auto intro: capprox_mult2 capprox_CFinite_mult_cancel) +lemmas hcomplex_of_complex_approx_inverse = + hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse] subsection{*Theorems About Monads*} -lemma capprox_cmonad_iff: "(x @c= y) = (cmonad(x)=cmonad(y))" -apply (simp add: cmonad_def) -apply (auto dest: capprox_sym elim!: capprox_trans equalityCE) -done - -lemma CInfinitesimal_cmonad_eq: - "e \ CInfinitesimal ==> cmonad (x+e) = cmonad x" -by (fast intro!: CInfinitesimal_add_capprox_self [THEN capprox_sym] capprox_cmonad_iff [THEN iffD1]) - -lemma mem_cmonad_iff: "(u \ cmonad x) = (-u \ cmonad (-x))" -by (simp add: cmonad_def) - -lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \ cmonad 0)" -by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def) - -lemma cmonad_zero_minus_iff: "(x \ cmonad 0) = (-x \ cmonad 0)" -by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric]) - -lemma cmonad_zero_hcmod_iff: "(x \ cmonad 0) = (hcmod x:monad 0)" -by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric] CInfinitesimal_hcmod_iff Infinitesimal_monad_zero_iff [symmetric]) - -lemma mem_cmonad_self [simp]: "x \ cmonad x" -by (simp add: cmonad_def) +lemma monad_zero_hcmod_iff: "(x \ monad 0) = (hcmod x:monad 0)" +by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff) subsection{*Theorems About Standard Part*} -lemma stc_capprox_self: "x \ CFinite ==> stc x @c= x" +lemma stc_approx_self: "x \ HFinite ==> stc x @= x" apply (simp add: stc_def) apply (frule stc_part_Ex, safe) apply (rule someI2) -apply (auto intro: capprox_sym) +apply (auto intro: approx_sym) done -lemma stc_SComplex: "x \ CFinite ==> stc x \ SComplex" +lemma stc_SComplex: "x \ HFinite ==> stc x \ SComplex" apply (simp add: stc_def) apply (frule stc_part_Ex, safe) apply (rule someI2) -apply (auto intro: capprox_sym) +apply (auto intro: approx_sym) done -lemma stc_CFinite: "x \ CFinite ==> stc x \ CFinite" -by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]]) +lemma stc_HFinite: "x \ HFinite ==> stc x \ HFinite" +by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]]) lemma stc_SComplex_eq [simp]: "x \ SComplex ==> stc x = x" apply (simp add: stc_def) apply (rule some_equality) -apply (auto intro: SComplex_subset_CFinite [THEN subsetD]) -apply (blast dest: SComplex_capprox_iff [THEN iffD1]) +apply (auto intro: SComplex_subset_HFinite [THEN subsetD]) +apply (blast dest: SComplex_approx_iff [THEN iffD1]) done lemma stc_hcomplex_of_complex: "stc (hcomplex_of_complex x) = hcomplex_of_complex x" by auto -lemma stc_eq_capprox: - "[| x \ CFinite; y \ CFinite; stc x = stc y |] ==> x @c= y" -by (auto dest!: stc_capprox_self elim!: capprox_trans3) +lemma stc_eq_approx: + "[| x \ HFinite; y \ HFinite; stc x = stc y |] ==> x @= y" +by (auto dest!: stc_approx_self elim!: approx_trans3) -lemma capprox_stc_eq: - "[| x \ CFinite; y \ CFinite; x @c= y |] ==> stc x = stc y" -by (blast intro: capprox_trans capprox_trans2 SComplex_capprox_iff [THEN iffD1] - dest: stc_capprox_self stc_SComplex) +lemma approx_stc_eq: + "[| x \ HFinite; y \ HFinite; x @= 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_capprox_iff: - "[| x \ CFinite; y \ CFinite|] ==> (x @c= y) = (stc x = stc y)" -by (blast intro: capprox_stc_eq stc_eq_capprox) +lemma stc_eq_approx_iff: + "[| x \ HFinite; y \ HFinite|] ==> (x @= y) = (stc x = stc y)" +by (blast intro: approx_stc_eq stc_eq_approx) -lemma stc_CInfinitesimal_add_SComplex: - "[| x \ SComplex; e \ CInfinitesimal |] ==> stc(x + e) = x" +lemma stc_Infinitesimal_add_SComplex: + "[| x \ SComplex; e \ Infinitesimal |] ==> stc(x + e) = x" apply (frule stc_SComplex_eq [THEN subst]) prefer 2 apply assumption -apply (frule SComplex_subset_CFinite [THEN subsetD]) -apply (frule CInfinitesimal_subset_CFinite [THEN subsetD]) +apply (frule SComplex_subset_HFinite [THEN subsetD]) +apply (frule Infinitesimal_subset_HFinite [THEN subsetD]) apply (drule stc_SComplex_eq) -apply (rule capprox_stc_eq) -apply (auto intro: CFinite_add simp add: CInfinitesimal_add_capprox_self [THEN capprox_sym]) +apply (rule approx_stc_eq) +apply (auto intro: HFinite_add simp add: Infinitesimal_add_approx_self [THEN approx_sym]) done -lemma stc_CInfinitesimal_add_SComplex2: - "[| x \ SComplex; e \ CInfinitesimal |] ==> stc(e + x) = x" +lemma stc_Infinitesimal_add_SComplex2: + "[| x \ SComplex; e \ Infinitesimal |] ==> stc(e + x) = x" apply (rule add_commute [THEN subst]) -apply (blast intro!: stc_CInfinitesimal_add_SComplex) +apply (blast intro!: stc_Infinitesimal_add_SComplex) done -lemma CFinite_stc_CInfinitesimal_add: - "x \ CFinite ==> \e \ CInfinitesimal. x = stc(x) + e" -by (blast dest!: stc_capprox_self [THEN capprox_sym] bex_CInfinitesimal_iff2 [THEN iffD2]) +lemma HFinite_stc_Infinitesimal_add: + "x \ HFinite ==> \e \ Infinitesimal. x = stc(x) + e" +by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2]) lemma stc_add: - "[| x \ CFinite; y \ CFinite |] ==> stc (x + y) = stc(x) + stc(y)" -apply (frule CFinite_stc_CInfinitesimal_add) -apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe) + "[| x \ HFinite; y \ HFinite |] ==> stc (x + y) = stc(x) + stc(y)" +apply (frule HFinite_stc_Infinitesimal_add) +apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe) apply (subgoal_tac "stc (x + y) = stc ((stc x + e) + (stc y + ea))") apply (drule_tac [2] sym, drule_tac [2] sym) prefer 2 apply simp apply (simp (no_asm_simp) add: add_ac) apply (drule stc_SComplex)+ apply (drule SComplex_add, assumption) -apply (drule CInfinitesimal_add, assumption) +apply (drule Infinitesimal_add, assumption) apply (rule add_assoc [THEN subst]) -apply (blast intro!: stc_CInfinitesimal_add_SComplex2) +apply (blast intro!: stc_Infinitesimal_add_SComplex2) done lemma stc_number_of [simp]: "stc (number_of w) = number_of w" @@ -1039,37 +605,26 @@ lemma stc_one [simp]: "stc 1 = 1" by simp -lemma stc_minus: "y \ CFinite ==> stc(-y) = -stc(y)" -apply (frule CFinite_minus_iff [THEN iffD2]) +lemma stc_minus: "y \ HFinite ==> stc(-y) = -stc(y)" +apply (frule HFinite_minus_iff [THEN iffD2]) apply (rule hcomplex_add_minus_eq_minus) apply (drule stc_add [symmetric], assumption) apply (simp add: add_commute) done lemma stc_diff: - "[| x \ CFinite; y \ CFinite |] ==> stc (x-y) = stc(x) - stc(y)" + "[| x \ HFinite; y \ HFinite |] ==> stc (x-y) = stc(x) - stc(y)" apply (simp add: diff_minus) apply (frule_tac y1 = y in stc_minus [symmetric]) -apply (drule_tac x1 = y in CFinite_minus_iff [THEN iffD2]) +apply (drule_tac x1 = y in HFinite_minus_iff [THEN iffD2]) apply (auto intro: stc_add) done -lemma lemma_stc_mult: - "[| x \ CFinite; y \ CFinite; - e \ CInfinitesimal; - ea: CInfinitesimal |] - ==> e*y + x*ea + e*ea: CInfinitesimal" -apply (frule_tac x = e and y = y in CInfinitesimal_CFinite_mult) -apply (frule_tac [2] x = ea and y = x in CInfinitesimal_CFinite_mult) -apply (drule_tac [3] CInfinitesimal_mult) -apply (auto intro: CInfinitesimal_add simp add: add_ac mult_ac) -done - lemma stc_mult: - "[| x \ CFinite; y \ CFinite |] + "[| x \ HFinite; y \ HFinite |] ==> stc (x * y) = stc(x) * stc(y)" -apply (frule CFinite_stc_CInfinitesimal_add) -apply (frule_tac x = y in CFinite_stc_CInfinitesimal_add, safe) +apply (frule HFinite_stc_Infinitesimal_add) +apply (frule_tac x = y in HFinite_stc_Infinitesimal_add, safe) apply (subgoal_tac "stc (x * y) = stc ((stc x + e) * (stc y + ea))") apply (drule_tac [2] sym, drule_tac [2] sym) prefer 2 apply simp @@ -1078,43 +633,43 @@ apply (simp add: left_distrib right_distrib) apply (drule stc_SComplex)+ apply (simp (no_asm_use) add: add_assoc) -apply (rule stc_CInfinitesimal_add_SComplex) +apply (rule stc_Infinitesimal_add_SComplex) apply (blast intro!: SComplex_mult) -apply (drule SComplex_subset_CFinite [THEN subsetD])+ +apply (drule SComplex_subset_HFinite [THEN subsetD])+ apply (rule add_assoc [THEN subst]) -apply (blast intro!: lemma_stc_mult) +apply (blast intro!: lemma_st_mult) done -lemma stc_CInfinitesimal: "x \ CInfinitesimal ==> stc x = 0" +lemma stc_Infinitesimal: "x \ Infinitesimal ==> stc x = 0" apply (rule stc_zero [THEN subst]) -apply (rule capprox_stc_eq) -apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD] - simp add: mem_cinfmal_iff [symmetric]) +apply (rule approx_stc_eq) +apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] + simp add: mem_infmal_iff [symmetric]) done -lemma stc_not_CInfinitesimal: "stc(x) \ 0 ==> x \ CInfinitesimal" -by (fast intro: stc_CInfinitesimal) +lemma stc_not_Infinitesimal: "stc(x) \ 0 ==> x \ Infinitesimal" +by (fast intro: stc_Infinitesimal) lemma stc_inverse: - "[| x \ CFinite; stc x \ 0 |] + "[| x \ HFinite; stc x \ 0 |] ==> stc(inverse x) = inverse (stc x)" apply (rule_tac c1 = "stc x" in hcomplex_mult_left_cancel [THEN iffD1]) -apply (auto simp add: stc_mult [symmetric] stc_not_CInfinitesimal CFinite_inverse) +apply (auto simp add: stc_mult [symmetric] stc_not_Infinitesimal HFinite_inverse) apply (subst right_inverse, auto) done lemma stc_divide [simp]: - "[| x \ CFinite; y \ CFinite; stc y \ 0 |] + "[| x \ HFinite; y \ HFinite; stc y \ 0 |] ==> stc(x/y) = (stc x) / (stc y)" -by (simp add: divide_inverse stc_mult stc_not_CInfinitesimal CFinite_inverse stc_inverse) +by (simp add: divide_inverse stc_mult stc_not_Infinitesimal HFinite_inverse stc_inverse) -lemma stc_idempotent [simp]: "x \ CFinite ==> stc(stc(x)) = stc(x)" -by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq) +lemma stc_idempotent [simp]: "x \ HFinite ==> stc(stc(x)) = stc(x)" +by (blast intro: stc_HFinite stc_approx_self approx_stc_eq) -lemma CFinite_HFinite_hcomplex_of_hypreal: - "z \ HFinite ==> hcomplex_of_hypreal z \ CFinite" +lemma HFinite_HFinite_hcomplex_of_hypreal: + "z \ HFinite ==> hcomplex_of_hypreal z \ HFinite" apply (cases z) -apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff star_n_zero_num [symmetric]) +apply (simp add: hcomplex_of_hypreal HFinite_HFinite_iff star_n_zero_num [symmetric]) done lemma SComplex_SReal_hcomplex_of_hypreal: @@ -1128,44 +683,44 @@ apply (frule st_part_Ex, safe) apply (rule someI2) apply (auto intro: approx_sym) -apply (drule CFinite_HFinite_hcomplex_of_hypreal) +apply (drule HFinite_HFinite_hcomplex_of_hypreal) apply (frule stc_part_Ex, safe) apply (rule someI2) -apply (auto intro: capprox_sym intro!: capprox_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal) +apply (auto intro: approx_sym intro!: approx_unique_complex dest: SComplex_SReal_hcomplex_of_hypreal) done (* -Goal "x \ CFinite ==> hcmod(stc x) = st(hcmod x)" -by (dtac stc_capprox_self 1) -by (auto_tac (claset(),simpset() addsimps [bex_CInfinitesimal_iff2 RS sym])); +Goal "x \ HFinite ==> hcmod(stc x) = st(hcmod x)" +by (dtac stc_approx_self 1) +by (auto_tac (claset(),simpset() addsimps [bex_Infinitesimal_iff2 RS sym])); approx_hcmod_add_hcmod *) -lemma CInfinitesimal_hcnj_iff [simp]: - "(hcnj z \ CInfinitesimal) = (z \ CInfinitesimal)" -by (simp add: CInfinitesimal_hcmod_iff) +lemma Infinitesimal_hcnj_iff [simp]: + "(hcnj z \ Infinitesimal) = (z \ Infinitesimal)" +by (simp add: Infinitesimal_hcmod_iff) -lemma CInfinite_HInfinite_iff: - "(star_n X \ CInfinite) = +lemma HInfinite_HInfinite_iff: + "(star_n X \ HInfinite) = (star_n (%n. Re(X n)) \ HInfinite | star_n (%n. Im(X n)) \ HInfinite)" -by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff) +by (simp add: HInfinite_HFinite_iff HFinite_HFinite_iff) text{*These theorems should probably be deleted*} -lemma hcomplex_split_CInfinitesimal_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ CInfinitesimal) = +lemma hcomplex_split_Infinitesimal_iff: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ Infinitesimal) = (x \ Infinitesimal & y \ Infinitesimal)" apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff) +apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal Infinitesimal_Infinitesimal_iff) done -lemma hcomplex_split_CFinite_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ CFinite) = +lemma hcomplex_split_HFinite_iff: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ HFinite) = (x \ HFinite & y \ HFinite)" apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CFinite_HFinite_iff) +apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HFinite_HFinite_iff) done lemma hcomplex_split_SComplex_iff: @@ -1175,38 +730,36 @@ apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal SComplex_SReal_iff) done -lemma hcomplex_split_CInfinite_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ CInfinite) = +lemma hcomplex_split_HInfinite_iff: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \ HInfinite) = (x \ HInfinite | y \ HInfinite)" apply (cases x, cases y) -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal CInfinite_HInfinite_iff) +apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal HInfinite_HInfinite_iff) done -lemma hcomplex_split_capprox_iff: - "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c= +lemma hcomplex_split_approx_iff: + "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @= hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') = (x @= x' & y @= y')" apply (cases x, cases y, cases x', cases y') -apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal capprox_approx_iff) +apply (simp add: iii_def star_of_def star_n_add star_n_mult hcomplex_of_hypreal approx_approx_iff) done -lemma complex_seq_to_hcomplex_CInfinitesimal: +lemma complex_seq_to_hcomplex_Infinitesimal: "\n. cmod (X n - x) < inverse (real (Suc n)) ==> - star_n X - hcomplex_of_complex x \ CInfinitesimal" -apply (simp add: star_n_diff CInfinitesimal_hcmod_iff star_of_def Infinitesimal_FreeUltrafilterNat_iff hcmod) -apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset) -done + star_n X - hcomplex_of_complex x \ Infinitesimal" +by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def]) -lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]: - "hcomplex_of_hypreal epsilon \ CInfinitesimal" -by (simp add: CInfinitesimal_hcmod_iff) +lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]: + "hcomplex_of_hypreal epsilon \ Infinitesimal" +by (simp add: Infinitesimal_hcmod_iff) lemma hcomplex_of_complex_approx_zero_iff [simp]: - "(hcomplex_of_complex z @c= 0) = (z = 0)" + "(hcomplex_of_complex z @= 0) = (z = 0)" by (simp add: star_of_zero [symmetric] del: star_of_zero) lemma hcomplex_of_complex_approx_zero_iff2 [simp]: - "(0 @c= hcomplex_of_complex z) = (z = 0)" + "(0 @= hcomplex_of_complex z) = (z = 0)" by (simp add: star_of_zero [symmetric] del: star_of_zero) end