removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
--- 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 = (\<forall>x. (x \<noteq> 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 = (\<forall>x. (x \<noteq> 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 = (\<forall>y. y @c= hcomplex_of_complex a -->
- ( *f* f) y @c= hcomplex_of_complex (f a))"
+ "isNSContc f a = (\<forall>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 = (\<forall>y. y @c= hcomplex_of_complex a -->
+ "isNSContCR f a = (\<forall>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 = (\<forall>h \<in> CInfinitesimal - {0}.
+ "NSCDERIV f x :> D = (\<forall>h \<in> 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 = (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"
+ "isNSUContc f = (\<forall>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 \<noteq> 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) =
- (\<forall>xa. xa \<noteq> hcomplex_of_complex x & xa @c= hcomplex_of_complex x -->
- ( *f* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"
+ (\<forall>xa. xa \<noteq> 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) \<noteq> 0")
prefer 2 apply (simp add: compare_rls)
apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
prefer 2 apply (simp add: add_assoc [symmetric])
-apply (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 \<noteq> 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 \<noteq> 0
+ xa : Infinitesimal; xa \<noteq> 0
|] ==> D = 0"
apply (simp add: nscderiv_def)
apply (drule bspec, auto)
done
-lemma NSCDERIV_capprox:
- "[| NSCDERIV f x :> D; h: CInfinitesimal; h \<noteq> 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 \<noteq> 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) \<noteq> 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 \<noteq> 0 |]
+ "[| NSCDERIV g x :> Db; xa: Infinitesimal; xa \<noteq> 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) \<noteq> 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 \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0"
+lemma Infinitesimal_add_not_zero:
+ "[| h: Infinitesimal; x \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0"
apply clarify
apply (drule equals_zero_I, auto)
done
@@ -924,7 +927,7 @@
lemma NSCDERIV_inverse:
"x \<noteq> 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:
--- 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
--- 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. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
-
- capprox :: "[hcomplex,hcomplex] => bool" (infixl "@c=" 50)
- --{*the ``infinitely close'' relation*}
- "x @c= y = ((x - y) \<in> CInfinitesimal)"
-
(* standard complex numbers reagarded as an embedded subset of NS complex *)
SComplex :: "hcomplex set"
"SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
- CFinite :: "hcomplex set"
- "CFinite = {x. \<exists>r \<in> Reals. hcmod x < r}"
-
- CInfinite :: "hcomplex set"
- "CInfinite = {x. \<forall>r \<in> Reals. r < hcmod x}"
-
stc :: "hcomplex => hcomplex"
--{* standard part map*}
- "stc x = (SOME r. x \<in> 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) \<in> CFinite}"
-
+ "stc x = (SOME r. x \<in> 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 \<in> CFinite; y \<in> CFinite|] ==> (x+y) \<in> CFinite"
-apply (simp add: CFinite_def)
-apply (blast intro!: SReal_add hcmod_add_less)
-done
-
-lemma CFinite_mult: "[|x \<in> CFinite; y \<in> CFinite|] ==> x*y \<in> CFinite"
-apply (simp add: CFinite_def)
-apply (blast intro!: SReal_mult hcmod_mult_less)
-done
-
-lemma CFinite_minus_iff [simp]: "(-x \<in> CFinite) = (x \<in> CFinite)"
-by (simp add: CFinite_def)
-
-lemma SComplex_subset_CFinite [simp]: "SComplex \<le> CFinite"
-apply (auto simp add: SComplex_def CFinite_def)
+lemma SComplex_subset_HFinite [simp]: "SComplex \<le> 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) \<in> HFinite"
by (auto intro!: SReal_subset_HFinite [THEN subsetD])
-lemma CFinite_hcomplex_of_complex [simp]: "hcomplex_of_complex x \<in> CFinite"
-by (auto intro!: SComplex_subset_CFinite [THEN subsetD])
-
-lemma CFiniteD: "x \<in> CFinite ==> \<exists>t \<in> Reals. hcmod x < t"
-by (simp add: CFinite_def)
+lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \<in> HFinite"
+by (rule HFinite_star_of)
-lemma CFinite_hcmod_iff: "(x \<in> CFinite) = (hcmod x \<in> HFinite)"
-by (simp add: CFinite_def HFinite_def)
+lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> HFinite)"
+by (simp add: HFinite_def)
-lemma CFinite_number_of [simp]: "number_of w \<in> CFinite"
-by (rule SComplex_number_of [THEN SComplex_subset_CFinite [THEN subsetD]])
-
-lemma CFinite_bounded: "[|x \<in> CFinite; y \<le> hcmod x; 0 \<le> y |] ==> y: HFinite"
-by (auto intro: HFinite_bounded simp add: CFinite_hcmod_iff)
+lemma HFinite_bounded_hcmod:
+ "[|x \<in> HFinite; y \<le> hcmod x; 0 \<le> 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 \<in> 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 \<in> CInfinitesimal) = (hcmod z \<in> Infinitesimal)"
-by (simp add: CInfinitesimal_def Infinitesimal_def)
-
-lemma one_not_CInfinitesimal [simp]: "1 \<notin> CInfinitesimal"
-by (simp add: CInfinitesimal_hcmod_iff)
+lemma Infinitesimal_hcmod_iff:
+ "(z \<in> Infinitesimal) = (hcmod z \<in> Infinitesimal)"
+by (simp add: Infinitesimal_def)
-lemma CInfinitesimal_add:
- "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> (x+y) \<in> 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 \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x-y \<in> CInfinitesimal"
-by (simp add: diff_minus CInfinitesimal_add)
-
-lemma CInfinitesimal_mult:
- "[| x \<in> CInfinitesimal; y \<in> CInfinitesimal |] ==> x * y \<in> CInfinitesimal"
-by (auto intro: Infinitesimal_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
+lemma HInfinite_hcmod_iff: "(z \<in> HInfinite) = (hcmod z \<in> HInfinite)"
+by (simp add: HInfinite_def)
-lemma CInfinitesimal_CFinite_mult:
- "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (x * y) \<in> CInfinitesimal"
-by (auto intro: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff hcmod_mult)
-
-lemma CInfinitesimal_CFinite_mult2:
- "[| x \<in> CInfinitesimal; y \<in> CFinite |] ==> (y * x) \<in> CInfinitesimal"
-by (auto dest: CInfinitesimal_CFinite_mult simp add: mult_commute)
-
-lemma CInfinite_hcmod_iff: "(z \<in> CInfinite) = (hcmod z \<in> HInfinite)"
-by (simp add: CInfinite_def HInfinite_def)
+lemma HFinite_diff_Infinitesimal_hcmod:
+ "x \<in> HFinite - Infinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
+by (simp add: HFinite_hcmod_iff Infinitesimal_hcmod_iff)
-lemma CInfinite_inverse_CInfinitesimal:
- "x \<in> CInfinite ==> inverse x \<in> CInfinitesimal"
-by (auto intro: HInfinite_inverse_Infinitesimal simp add: CInfinitesimal_hcmod_iff CInfinite_hcmod_iff hcmod_hcomplex_inverse)
-
-lemma CInfinite_mult: "[|x \<in> CInfinite; y \<in> CInfinite|] ==> (x*y): CInfinite"
-by (auto intro: HInfinite_mult simp add: CInfinite_hcmod_iff hcmod_mult)
+lemma hcmod_less_Infinitesimal:
+ "[| e \<in> Infinitesimal; hcmod x < hcmod e |] ==> x \<in> Infinitesimal"
+by (auto elim: hrabs_less_Infinitesimal simp add: Infinitesimal_hcmod_iff)
-lemma CInfinite_minus_iff [simp]: "(-x \<in> CInfinite) = (x \<in> CInfinite)"
-by (simp add: CInfinite_def)
-
-lemma CFinite_sum_squares:
- "[|a \<in> CFinite; b \<in> CFinite; c \<in> CFinite|]
- ==> a*a + b*b + c*c \<in> CFinite"
-by (auto intro: CFinite_mult CFinite_add)
-
-lemma not_CInfinitesimal_not_zero: "x \<notin> CInfinitesimal ==> x \<noteq> 0"
-by auto
+lemma hcmod_le_Infinitesimal:
+ "[| e \<in> Infinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> Infinitesimal"
+by (auto elim: hrabs_le_Infinitesimal simp add: Infinitesimal_hcmod_iff)
-lemma not_CInfinitesimal_not_zero2: "x \<in> CFinite - CInfinitesimal ==> x \<noteq> 0"
-by auto
-
-lemma CFinite_diff_CInfinitesimal_hcmod:
- "x \<in> CFinite - CInfinitesimal ==> hcmod x \<in> HFinite - Infinitesimal"
-by (simp add: CFinite_hcmod_iff CInfinitesimal_hcmod_iff)
-
-lemma hcmod_less_CInfinitesimal:
- "[| e \<in> CInfinitesimal; hcmod x < hcmod e |] ==> x \<in> CInfinitesimal"
-by (auto intro: hrabs_less_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
+lemma Infinitesimal_interval_hcmod:
+ "[| e \<in> Infinitesimal;
+ e' \<in> Infinitesimal;
+ hcmod e' < hcmod x ; hcmod x < hcmod e
+ |] ==> x \<in> Infinitesimal"
+by (auto intro: Infinitesimal_interval simp add: Infinitesimal_hcmod_iff)
-lemma hcmod_le_CInfinitesimal:
- "[| e \<in> CInfinitesimal; hcmod x \<le> hcmod e |] ==> x \<in> CInfinitesimal"
-by (auto intro: hrabs_le_Infinitesimal simp add: CInfinitesimal_hcmod_iff)
-
-lemma CInfinitesimal_interval:
- "[| e \<in> CInfinitesimal;
- e' \<in> CInfinitesimal;
- hcmod e' < hcmod x ; hcmod x < hcmod e
- |] ==> x \<in> CInfinitesimal"
-by (auto intro: Infinitesimal_interval simp add: CInfinitesimal_hcmod_iff)
-
-lemma CInfinitesimal_interval2:
- "[| e \<in> CInfinitesimal;
- e' \<in> CInfinitesimal;
+lemma Infinitesimal_interval2_hcmod:
+ "[| e \<in> Infinitesimal;
+ e' \<in> Infinitesimal;
hcmod e' \<le> hcmod x ; hcmod x \<le> hcmod e
- |] ==> x \<in> CInfinitesimal"
-by (auto intro: Infinitesimal_interval2 simp add: CInfinitesimal_hcmod_iff)
-
-lemma not_CInfinitesimal_mult:
- "[| x \<notin> CInfinitesimal; y \<notin> CInfinitesimal|] ==> (x*y) \<notin> CInfinitesimal"
-apply (auto simp add: CInfinitesimal_hcmod_iff hcmod_mult)
-apply (drule not_Infinitesimal_mult, auto)
-done
-
-lemma CInfinitesimal_mult_disj:
- "x*y \<in> CInfinitesimal ==> x \<in> CInfinitesimal | y \<in> CInfinitesimal"
-by (auto dest: Infinitesimal_mult_disj simp add: CInfinitesimal_hcmod_iff hcmod_mult)
+ |] ==> x \<in> Infinitesimal"
+by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
-lemma CFinite_CInfinitesimal_diff_mult:
- "[| x \<in> CFinite - CInfinitesimal; y \<in> CFinite - CInfinitesimal |]
- ==> x*y \<in> CFinite - CInfinitesimal"
-by (blast dest: CFinite_mult not_CInfinitesimal_mult)
+lemma Infinitesimal_hcomplex_of_complex_mult:
+ "x \<in> Infinitesimal ==> x * hcomplex_of_complex r \<in> Infinitesimal"
+by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult)
-lemma CInfinitesimal_subset_CFinite: "CInfinitesimal \<le> CFinite"
-by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
- simp add: CInfinitesimal_hcmod_iff CFinite_hcmod_iff)
-
-lemma CInfinitesimal_hcomplex_of_complex_mult:
- "x \<in> CInfinitesimal ==> x * hcomplex_of_complex r \<in> CInfinitesimal"
-by (auto intro!: Infinitesimal_HFinite_mult simp add: CInfinitesimal_hcmod_iff hcmod_mult)
-
-lemma CInfinitesimal_hcomplex_of_complex_mult2:
- "x \<in> CInfinitesimal ==> hcomplex_of_complex r * x \<in> CInfinitesimal"
-by (auto intro!: Infinitesimal_HFinite_mult2 simp add: CInfinitesimal_hcmod_iff hcmod_mult)
+lemma Infinitesimal_hcomplex_of_complex_mult2:
+ "x \<in> Infinitesimal ==> hcomplex_of_complex r * x \<in> 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 \<in> 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 \<in> CInfinitesimal; y \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> CFinite|] ==> u @c= v*y"
-by (blast intro: capprox_mult2 capprox_trans)
-
-lemma capprox_mult_subst2:
- "[| u @c= x*v; x @c= y; v \<in> 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 \<in> CInfinitesimal ==> -x @c= x"
-by (blast intro: CInfinitesimal_minus_iff [THEN iffD2] mem_cinfmal_iff [THEN iffD1] capprox_trans2)
-
-lemma bex_CInfinitesimal_iff: "(\<exists>y \<in> CInfinitesimal. x - z = y) = (x @c= z)"
-by (unfold capprox_def, blast)
-
-lemma bex_CInfinitesimal_iff2: "(\<exists>y \<in> CInfinitesimal. x = z + y) = (x @c= z)"
-by (simp add: bex_CInfinitesimal_iff [symmetric], force)
-
-lemma CInfinitesimal_add_capprox:
- "[| y \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> 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 \<in> CInfinitesimal ==> x @c= y + x"
-by (auto dest: CInfinitesimal_add_capprox_self simp add: add_commute)
-
-lemma CInfinitesimal_add_minus_capprox_self:
- "y \<in> CInfinitesimal ==> x @c= x + -y"
-by (blast intro!: CInfinitesimal_add_capprox_self CInfinitesimal_minus_iff [THEN iffD2])
+lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0"
+by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1)
-lemma CInfinitesimal_add_cancel:
- "[| y \<in> 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 \<in> 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 \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> CFinite; x @c= y |] ==> y \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> CFinite"
-by (rule capprox_sym [THEN [2] capprox_CFinite], auto)
+lemma approx_SComplex_mult_cancel_iff1 [simp]:
+ "[| a \<in> SComplex; a \<noteq> 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 \<in> CFinite; d \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
-by (auto dest: SComplex_subset_CFinite [THEN subsetD] capprox_mult1)
-
-lemma capprox_mult_SComplex2: "[| a \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> SComplex; a \<noteq> 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 \<in> SComplex; a \<noteq> 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 \<in> Infinitesimal"
+ "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
+apply (drule approx_approx_zero_iff [THEN iffD1])
apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
-apply (auto 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 \<in> SComplex; y \<in> 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 \<in> SComplex; y \<in> 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 \<in> SComplex; x \<in> 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 \<in> SComplex; x \<noteq> 0 |] ==> x \<in> CFinite - CInfinitesimal"
-by (auto dest: SComplex_CInfinitesimal_zero SComplex_subset_CFinite [THEN subsetD])
-
-lemma hcomplex_of_complex_CFinite_diff_CInfinitesimal:
- "hcomplex_of_complex x \<noteq> 0
- ==> hcomplex_of_complex x \<in> CFinite - CInfinitesimal"
-by (rule SComplex_CFinite_diff_CInfinitesimal, auto)
+lemma SComplex_Infinitesimal_zero:
+ "[| x \<in> SComplex; x \<in> Infinitesimal|] ==> x = 0"
+by (cut_tac SComplex_Int_Infinitesimal_zero, blast)
-lemma hcomplex_of_complex_CInfinitesimal_iff_0 [iff]:
- "(hcomplex_of_complex x \<in> 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 \<in> SComplex; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
+by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD])
-lemma number_of_not_CInfinitesimal [simp]:
- "number_of w \<noteq> (0::hcomplex) ==> number_of w \<notin> CInfinitesimal"
-by (fast dest: SComplex_number_of [THEN SComplex_CInfinitesimal_zero])
+lemma hcomplex_of_complex_HFinite_diff_Infinitesimal:
+ "hcomplex_of_complex x \<noteq> 0
+ ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"
+by (rule SComplex_HFinite_diff_Infinitesimal, auto)
-lemma capprox_SComplex_not_zero:
- "[| y \<in> SComplex; x @c= y; y\<noteq> 0 |] ==> x \<noteq> 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 \<in> Infinitesimal) = (x=0)"
+by (rule star_of_Infinitesimal_iff_0)
-lemma CFinite_diff_CInfinitesimal_capprox:
- "[| x @c= y; y \<in> CFinite - CInfinitesimal |]
- ==> x \<in> 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 \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal"
+by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero])
-lemma CInfinitesimal_ratio:
- "[| y \<noteq> 0; y \<in> CInfinitesimal; x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
-apply (drule CInfinitesimal_CFinite_mult2, assumption)
-apply (simp add: divide_inverse mult_assoc)
-done
+lemma approx_SComplex_not_zero:
+ "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
-lemma SComplex_capprox_iff:
- "[|x \<in> SComplex; y \<in> 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 \<in> SComplex; y \<in> 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 \<in> CInfinitesimal) = (number_of w = (0::hcomplex))"
+lemma number_of_Infinitesimal_iff [simp]:
+ "((number_of w :: hcomplex) \<in> 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 \<in> SComplex; s \<in> SComplex; r @c= x; s @c= x|] ==> r = s"
-by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2)
+lemma approx_unique_complex:
+ "[| r \<in> SComplex; s \<in> 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 \<in> CFinite
+lemma HFinite_HFinite_Re:
+ "star_n X \<in> HFinite
==> star_n (%n. Re(X n)) \<in> 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 \<in> CFinite
+lemma HFinite_HFinite_Im:
+ "star_n X \<in> HFinite
==> star_n (%n. Im(X n)) \<in> 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)) \<in> HFinite;
star_n (%n. Im(X n)) \<in> HFinite
- |] ==> star_n X \<in> CFinite"
-apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
+ |] ==> star_n X \<in> 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 \<in> CFinite) =
+lemma HFinite_HFinite_iff:
+ "(star_n X \<in> HFinite) =
(star_n (%n. Re(X n)) \<in> HFinite &
star_n (%n. Im(X n)) \<in> 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 \<in> SComplex
@@ -794,11 +476,11 @@
star_n (%n. Im(X n)) \<in> Reals)"
by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
-lemma CInfinitesimal_Infinitesimal_iff:
- "(star_n X \<in> CInfinitesimal) =
+lemma Infinitesimal_Infinitesimal_iff:
+ "(star_n X \<in> Infinitesimal) =
(star_n (%n. Re(X n)) \<in> Infinitesimal &
star_n (%n. Im(X n)) \<in> 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:
"(\<exists>t. P t) = (\<exists>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 ==> \<exists>t \<in> SComplex. x @c= t"
+lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> 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 \<in> SComplex & x @c= t"
+lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> 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 \<in> CFinite ==> x \<notin> 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\<notin> CFinite ==> x \<in> CInfinite"
-by (auto intro: not_HFinite_HInfinite simp add: CFinite_hcmod_iff CInfinite_hcmod_iff)
-
-lemma CInfinite_CFinite_disj: "x \<in> CInfinite | x \<in> CFinite"
-by (blast intro: not_CFinite_CInfinite)
-
-lemma CInfinite_CFinite_iff: "(x \<in> CInfinite) = (x \<notin> CFinite)"
-by (blast dest: CFinite_not_CInfinite not_CFinite_CInfinite)
-
-lemma CFinite_CInfinite_iff: "(x \<in> CFinite) = (x \<notin> CInfinite)"
-by (simp add: CInfinite_CFinite_iff)
-
-lemma CInfinite_diff_CFinite_CInfinitesimal_disj:
- "x \<notin> CInfinitesimal ==> x \<in> CInfinite | x \<in> CFinite - CInfinitesimal"
-by (fast intro: not_CFinite_CInfinite)
-
-lemma CFinite_inverse:
- "[| x \<in> CFinite; x \<notin> CInfinitesimal |] ==> inverse x \<in> CFinite"
-apply (cut_tac x = "inverse x" in CInfinite_CFinite_disj)
-apply (auto dest!: CInfinite_inverse_CInfinitesimal)
-done
-
-lemma CFinite_inverse2: "x \<in> CFinite - CInfinitesimal ==> inverse x \<in> CFinite"
-by (blast intro: CFinite_inverse)
-
-lemma CInfinitesimal_inverse_CFinite:
- "x \<notin> CInfinitesimal ==> inverse(x) \<in> 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 \<in> CFinite - CInfinitesimal ==> inverse x \<in> 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 \<in> 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 \<in> CFinite - CInfinitesimal;
- h \<in> CInfinitesimal |] ==> inverse(x + h) @c= inverse x"
-by (auto intro: capprox_inverse capprox_sym CInfinitesimal_add_capprox_self)
-
-lemma inverse_add_CInfinitesimal_capprox2:
- "[| x \<in> CFinite - CInfinitesimal;
- h \<in> 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 \<in> CFinite - CInfinitesimal;
- h \<in> 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 \<in> CInfinitesimal) = (x \<in> CInfinitesimal)"
-by (simp add: CInfinitesimal_hcmod_iff hcmod_mult)
-
-lemma capprox_CFinite_mult_cancel:
- "[| a \<in> 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 \<in> 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 \<in> 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 \<in> cmonad x) = (-u \<in> cmonad (-x))"
-by (simp add: cmonad_def)
-
-lemma CInfinitesimal_cmonad_zero_iff: "(x:CInfinitesimal) = (x \<in> cmonad 0)"
-by (auto intro: capprox_sym simp add: mem_cinfmal_iff cmonad_def)
-
-lemma cmonad_zero_minus_iff: "(x \<in> cmonad 0) = (-x \<in> cmonad 0)"
-by (simp add: CInfinitesimal_cmonad_zero_iff [symmetric])
-
-lemma cmonad_zero_hcmod_iff: "(x \<in> 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 \<in> cmonad x"
-by (simp add: cmonad_def)
+lemma monad_zero_hcmod_iff: "(x \<in> 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 \<in> CFinite ==> stc x @c= x"
+lemma stc_approx_self: "x \<in> 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 \<in> CFinite ==> stc x \<in> SComplex"
+lemma stc_SComplex: "x \<in> HFinite ==> stc x \<in> 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 \<in> CFinite ==> stc x \<in> CFinite"
-by (erule stc_SComplex [THEN SComplex_subset_CFinite [THEN subsetD]])
+lemma stc_HFinite: "x \<in> HFinite ==> stc x \<in> HFinite"
+by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]])
lemma stc_SComplex_eq [simp]: "x \<in> 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 \<in> CFinite; y \<in> CFinite; stc x = stc y |] ==> x @c= y"
-by (auto dest!: stc_capprox_self elim!: capprox_trans3)
+lemma stc_eq_approx:
+ "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y"
+by (auto dest!: stc_approx_self elim!: approx_trans3)
-lemma capprox_stc_eq:
- "[| x \<in> CFinite; y \<in> 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 \<in> HFinite; y \<in> 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 \<in> CFinite; y \<in> CFinite|] ==> (x @c= y) = (stc x = stc y)"
-by (blast intro: capprox_stc_eq stc_eq_capprox)
+lemma stc_eq_approx_iff:
+ "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)"
+by (blast intro: approx_stc_eq stc_eq_approx)
-lemma stc_CInfinitesimal_add_SComplex:
- "[| x \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(x + e) = x"
+lemma stc_Infinitesimal_add_SComplex:
+ "[| x \<in> SComplex; e \<in> 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 \<in> SComplex; e \<in> CInfinitesimal |] ==> stc(e + x) = x"
+lemma stc_Infinitesimal_add_SComplex2:
+ "[| x \<in> SComplex; e \<in> 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 \<in> CFinite ==> \<exists>e \<in> 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 \<in> HFinite ==> \<exists>e \<in> Infinitesimal. x = stc(x) + e"
+by (blast dest!: stc_approx_self [THEN approx_sym] bex_Infinitesimal_iff2 [THEN iffD2])
lemma stc_add:
- "[| x \<in> CFinite; y \<in> 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 \<in> HFinite; y \<in> 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 \<in> CFinite ==> stc(-y) = -stc(y)"
-apply (frule CFinite_minus_iff [THEN iffD2])
+lemma stc_minus: "y \<in> 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 \<in> CFinite; y \<in> CFinite |] ==> stc (x-y) = stc(x) - stc(y)"
+ "[| x \<in> HFinite; y \<in> 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 \<in> CFinite; y \<in> CFinite;
- e \<in> 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 \<in> CFinite; y \<in> CFinite |]
+ "[| x \<in> HFinite; y \<in> 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 \<in> CInfinitesimal ==> stc x = 0"
+lemma stc_Infinitesimal: "x \<in> 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) \<noteq> 0 ==> x \<notin> CInfinitesimal"
-by (fast intro: stc_CInfinitesimal)
+lemma stc_not_Infinitesimal: "stc(x) \<noteq> 0 ==> x \<notin> Infinitesimal"
+by (fast intro: stc_Infinitesimal)
lemma stc_inverse:
- "[| x \<in> CFinite; stc x \<noteq> 0 |]
+ "[| x \<in> HFinite; stc x \<noteq> 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 \<in> CFinite; y \<in> CFinite; stc y \<noteq> 0 |]
+ "[| x \<in> HFinite; y \<in> HFinite; stc y \<noteq> 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 \<in> CFinite ==> stc(stc(x)) = stc(x)"
-by (blast intro: stc_CFinite stc_capprox_self capprox_stc_eq)
+lemma stc_idempotent [simp]: "x \<in> HFinite ==> stc(stc(x)) = stc(x)"
+by (blast intro: stc_HFinite stc_approx_self approx_stc_eq)
-lemma CFinite_HFinite_hcomplex_of_hypreal:
- "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
+lemma HFinite_HFinite_hcomplex_of_hypreal:
+ "z \<in> HFinite ==> hcomplex_of_hypreal z \<in> 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 \<in> 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 \<in> 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 \<in> CInfinitesimal) = (z \<in> CInfinitesimal)"
-by (simp add: CInfinitesimal_hcmod_iff)
+lemma Infinitesimal_hcnj_iff [simp]:
+ "(hcnj z \<in> Infinitesimal) = (z \<in> Infinitesimal)"
+by (simp add: Infinitesimal_hcmod_iff)
-lemma CInfinite_HInfinite_iff:
- "(star_n X \<in> CInfinite) =
+lemma HInfinite_HInfinite_iff:
+ "(star_n X \<in> HInfinite) =
(star_n (%n. Re(X n)) \<in> HInfinite |
star_n (%n. Im(X n)) \<in> 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 \<in> CInfinitesimal) =
+lemma hcomplex_split_Infinitesimal_iff:
+ "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> Infinitesimal) =
(x \<in> Infinitesimal & y \<in> 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 \<in> CFinite) =
+lemma hcomplex_split_HFinite_iff:
+ "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HFinite) =
(x \<in> HFinite & y \<in> 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 \<in> CInfinite) =
+lemma hcomplex_split_HInfinite_iff:
+ "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> HInfinite) =
(x \<in> HInfinite | y \<in> 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:
"\<forall>n. cmod (X n - x) < inverse (real (Suc n)) ==>
- star_n X - hcomplex_of_complex x \<in> 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 \<in> Infinitesimal"
+by (rule real_seq_to_hypreal_Infinitesimal [folded diff_def])
-lemma CInfinitesimal_hcomplex_of_hypreal_epsilon [simp]:
- "hcomplex_of_hypreal epsilon \<in> CInfinitesimal"
-by (simp add: CInfinitesimal_hcmod_iff)
+lemma Infinitesimal_hcomplex_of_hypreal_epsilon [simp]:
+ "hcomplex_of_hypreal epsilon \<in> 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