--- a/src/HOL/Complex/CLim.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/CLim.thy Tue Sep 06 23:16:48 2005 +0200
@@ -126,7 +126,7 @@
apply (rule_tac z = xa in eq_Abs_hcomplex)
apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff
CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
apply (drule_tac x = u in spec, auto)
apply (drule_tac x = s in spec, auto, ultra)
apply (drule sym, auto)
@@ -196,8 +196,9 @@
apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
CInfinitesimal_hcmod_iff hcmod hypreal_diff
Infinitesimal_FreeUltrafilterNat_iff
+ star_of_def star_n_def
Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
apply (drule_tac x = u in spec, auto)
apply (drule_tac x = s in spec, auto, ultra)
apply (drule sym, auto)
@@ -241,7 +242,7 @@
apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def
Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod)
-apply (auto simp add: hypreal_of_real_def hypreal_diff)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def hypreal_diff)
apply (drule_tac x = r in spec, clarify)
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -427,7 +428,7 @@
apply (auto simp add: NSCLIM_def NSCRLIM_def)
apply (auto dest!: spec)
apply (rule_tac z = x in eq_Abs_hcomplex)
-apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
+apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def star_of_def star_n_def)
done
lemma CLIM_CRLIM_Re_Im_iff:
--- a/src/HOL/Complex/CStar.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/CStar.thy Tue Sep 06 23:16:48 2005 +0200
@@ -44,11 +44,11 @@
starfunRC :: "(real => complex) => hypreal => hcomplex"
("*fRc* _" [80] 80)
- "*fRc* f == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. f (X n)}))"
+ "*fRc* f == (%x. Abs_hcomplex(\<Union>X \<in> Rep_star(x). hcomplexrel``{%n. f (X n)}))"
starfunRC_n :: "(nat => (real => complex)) => hypreal => hcomplex"
("*fRcn* _" [80] 80)
- "*fRcn* F == (%x. Abs_hcomplex(\<Union>X \<in> Rep_hypreal(x). hcomplexrel``{%n. (F n)(X n)}))"
+ "*fRcn* F == (%x. Abs_hcomplex(\<Union>X \<in> Rep_star(x). hcomplexrel``{%n. (F n)(X n)}))"
InternalRCFuns :: "(hypreal => hcomplex) set"
"InternalRCFuns == {X. \<exists>F. X = *fRcn* F}"
@@ -57,11 +57,11 @@
starfunCR :: "(complex => real) => hcomplex => hypreal"
("*fcR* _" [80] 80)
- "*fcR* f == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. f (X n)}))"
+ "*fcR* f == (%x. Abs_star(\<Union>X \<in> Rep_hcomplex(x). starrel``{%n. f (X n)}))"
starfunCR_n :: "(nat => (complex => real)) => hcomplex => hypreal"
("*fcRn* _" [80] 80)
- "*fcRn* F == (%x. Abs_hypreal(\<Union>X \<in> Rep_hcomplex(x). hyprel``{%n. (F n)(X n)}))"
+ "*fcRn* F == (%x. Abs_star(\<Union>X \<in> Rep_hcomplex(x). starrel``{%n. (F n)(X n)}))"
InternalCRFuns :: "(hcomplex => hypreal) set"
"InternalCRFuns == {X. \<exists>F. X = *fcRn* F}"
@@ -227,7 +227,7 @@
done
lemma starfunRC:
- "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) =
+ "( *fRc* f) (Abs_star(starrel``{%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"
apply (simp add: starfunRC_def)
apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra)
@@ -235,9 +235,9 @@
lemma starfunCR:
"( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. f (X n)})"
+ Abs_star(starrel `` {%n. f (X n)})"
apply (simp add: starfunCR_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
apply (auto iff add: hcomplexrel_iff, ultra)
done
@@ -251,7 +251,7 @@
lemma starfunRC_mult:
"( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunRC hcomplex_mult)
done
declare starfunRC_mult [symmetric, simp]
@@ -272,7 +272,7 @@
declare starfunC_add [symmetric, simp]
lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunRC hcomplex_add)
done
declare starfunRC_add [symmetric, simp]
@@ -290,7 +290,7 @@
done
lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfunRC hcomplex_minus)
done
@@ -329,7 +329,7 @@
lemma starfunC_starfunRC_o2:
"(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
apply (simp add: starfunRC starfunC)
done
@@ -352,13 +352,13 @@
done
lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: starfunRC hcomplex_of_complex_def)
done
lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k"
apply (cases z)
-apply (simp add: starfunCR hypreal_of_real_def)
+apply (simp add: starfunCR hypreal_of_real_def star_of_def star_n_def)
done
lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"
@@ -369,7 +369,7 @@
lemma starfunRC_inverse:
"inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfunRC hcomplex_inverse)
done
declare starfunRC_inverse [symmetric, simp]
@@ -387,11 +387,11 @@
lemma starfunRC_eq [simp]:
"( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)"
-by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def)
+by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def)
lemma starfunCR_eq [simp]:
"( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)"
-by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def)
+by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def)
lemma starfunC_capprox:
"( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"
@@ -428,8 +428,8 @@
lemma starfunRC_lambda_cancel:
"( *fRc* (%h. f (x + h))) y = ( *fRc* f) (hypreal_of_real x + y)"
-apply (cases y)
-apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
+apply (rule_tac z=y in eq_Abs_star)
+apply (simp add: starfunRC hypreal_of_real_def star_of_def star_n_def hypreal_add)
done
lemma starfunC_lambda_cancel2:
@@ -446,8 +446,8 @@
lemma starfunRC_lambda_cancel2:
"( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)"
-apply (cases y)
-apply (simp add: starfunRC hypreal_of_real_def hypreal_add)
+apply (rule_tac z=y in eq_Abs_star)
+apply (simp add: starfunRC hypreal_of_real_def star_of_def star_n_def hypreal_add)
done
lemma starfunC_mult_CFinite_capprox:
--- a/src/HOL/Complex/NSCA.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/NSCA.thy Tue Sep 06 23:16:48 2005 +0200
@@ -80,7 +80,7 @@
lemma SReal_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) \<in> Reals"
-by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def)
+by (simp add: hcomplex_of_complex_def hcmod SReal_def hypreal_of_real_def star_of_def star_n_def)
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals"
apply (subst hcomplex_number_of [symmetric])
@@ -135,7 +135,7 @@
"z \<in> SComplex ==> hcmod z \<in> Reals"
apply (simp add: SComplex_def SReal_def)
apply (rule_tac z = z in eq_Abs_hcomplex)
-apply (auto simp add: hcmod hypreal_of_real_def hcomplex_of_complex_def cmod_def)
+apply (auto simp add: hcmod hypreal_of_real_def star_of_def star_n_def hcomplex_of_complex_def cmod_def)
apply (rule_tac x = "cmod r" in exI)
apply (simp add: cmod_def, ultra)
done
@@ -660,8 +660,8 @@
lemma hcomplex_capproxD1:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})
- ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) @=
- Abs_hypreal(hyprel `` {%n. Re(Y n)})"
+ ==> Abs_star(starrel `` {%n. Re(X n)}) @=
+ Abs_star(starrel `` {%n. Re(Y n)})"
apply (auto simp add: approx_FreeUltrafilterNat_iff)
apply (drule capprox_minus_iff [THEN iffD1])
apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
@@ -679,8 +679,8 @@
(* same proof *)
lemma hcomplex_capproxD2:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})
- ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) @=
- Abs_hypreal(hyprel `` {%n. Im(Y n)})"
+ ==> Abs_star(starrel `` {%n. Im(X n)}) @=
+ Abs_star(starrel `` {%n. Im(Y n)})"
apply (auto simp add: approx_FreeUltrafilterNat_iff)
apply (drule capprox_minus_iff [THEN iffD1])
apply (auto simp add: hcomplex_minus hcomplex_add mem_cinfmal_iff [symmetric] CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff2)
@@ -695,16 +695,16 @@
done
lemma hcomplex_capproxI:
- "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) @=
- Abs_hypreal(hyprel `` {%n. Re(Y n)});
- Abs_hypreal(hyprel `` {%n. Im(X n)}) @=
- Abs_hypreal(hyprel `` {%n. Im(Y n)})
+ "[| Abs_star(starrel `` {%n. Re(X n)}) @=
+ Abs_star(starrel `` {%n. Re(Y n)});
+ Abs_star(starrel `` {%n. Im(X n)}) @=
+ Abs_star(starrel `` {%n. Im(Y n)})
|] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})"
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] hypreal_minus hypreal_add hcomplex_minus hcomplex_add CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
apply (drule_tac x = "u/2" in spec)
apply (drule_tac x = "u/2" in spec, auto, ultra)
apply (drule sym, drule sym)
@@ -719,22 +719,22 @@
lemma capprox_approx_iff:
"(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) =
- (Abs_hypreal(hyprel `` {%n. Re(X n)}) @= Abs_hypreal(hyprel `` {%n. Re(Y n)}) &
- Abs_hypreal(hyprel `` {%n. Im(X n)}) @= Abs_hypreal(hyprel `` {%n. Im(Y n)}))"
+ (Abs_star(starrel `` {%n. Re(X n)}) @= Abs_star(starrel `` {%n. Re(Y n)}) &
+ Abs_star(starrel `` {%n. Im(X n)}) @= Abs_star(starrel `` {%n. Im(Y n)}))"
apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2)
done
lemma hcomplex_of_hypreal_capprox_iff [simp]:
"(hcomplex_of_hypreal x @c= hcomplex_of_hypreal z) = (x @= z)"
-apply (cases x, cases z)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=z in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal capprox_approx_iff)
done
lemma CFinite_HFinite_Re:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite
- ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite"
+ ==> Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
apply (rule_tac x = u in exI, ultra)
apply (drule sym, case_tac "X x")
apply (auto simp add: complex_mod numeral_2_eq_2 simp del: realpow_Suc)
@@ -746,9 +746,9 @@
lemma CFinite_HFinite_Im:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite
- ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite"
+ ==> Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
apply (rule_tac x = u in exI, ultra)
apply (drule sym, case_tac "X x")
apply (auto simp add: complex_mod simp del: realpow_Suc)
@@ -758,12 +758,12 @@
done
lemma HFinite_Re_Im_CFinite:
- "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite;
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite
+ "[| Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite;
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite
|] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite"
apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff)
apply (rename_tac Y Z u v)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
apply (rule_tac x = "2* (u + v) " in exI)
apply ultra
apply (drule sym, case_tac "X x")
@@ -779,42 +779,42 @@
lemma CFinite_HFinite_iff:
"(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CFinite) =
- (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HFinite &
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HFinite)"
+ (Abs_star(starrel `` {%n. Re(X n)}) \<in> HFinite &
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> HFinite)"
by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re)
lemma SComplex_Re_SReal:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex
- ==> Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+ ==> Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals"
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
apply (rule_tac x = "Re r" in exI, ultra)
done
lemma SComplex_Im_SReal:
"Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex
- ==> Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+ ==> Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals"
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
apply (rule_tac x = "Im r" in exI, ultra)
done
lemma Reals_Re_Im_SComplex:
- "[| Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals;
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals
+ "[| Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals;
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals
|] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex"
-apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def)
+apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def)
apply (rule_tac x = "Complex r ra" in exI, ultra)
done
lemma SComplex_SReal_iff:
"(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> SComplex) =
- (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Reals &
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Reals)"
+ (Abs_star(starrel `` {%n. Re(X n)}) \<in> Reals &
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> Reals)"
by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex)
lemma CInfinitesimal_Infinitesimal_iff:
"(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinitesimal) =
- (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> Infinitesimal &
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> Infinitesimal)"
+ (Abs_star(starrel `` {%n. Re(X n)}) \<in> Infinitesimal &
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> Infinitesimal)"
by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff)
lemma eq_Abs_hcomplex_EX:
@@ -835,8 +835,8 @@
apply (rule_tac z = x in eq_Abs_hcomplex)
apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff)
apply (drule st_part_Ex, safe)+
-apply (rule_tac z = t in eq_Abs_hypreal)
-apply (rule_tac z = ta in eq_Abs_hypreal, auto)
+apply (rule_tac z = t in eq_Abs_star)
+apply (rule_tac z = ta in eq_Abs_star, auto)
apply (rule_tac x = "%n. Complex (xa n) (xb n) " in exI)
apply auto
done
@@ -1135,13 +1135,13 @@
lemma CFinite_HFinite_hcomplex_of_hypreal:
"z \<in> HFinite ==> hcomplex_of_hypreal z \<in> CFinite"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal CFinite_HFinite_iff hypreal_zero_def [symmetric])
done
lemma SComplex_SReal_hcomplex_of_hypreal:
"x \<in> Reals ==> hcomplex_of_hypreal x \<in> SComplex"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal SComplex_SReal_iff hypreal_zero_def [symmetric])
done
@@ -1172,36 +1172,36 @@
lemma CInfinite_HInfinite_iff:
"(Abs_hcomplex(hcomplexrel ``{%n. X n}) \<in> CInfinite) =
- (Abs_hypreal(hyprel `` {%n. Re(X n)}) \<in> HInfinite |
- Abs_hypreal(hyprel `` {%n. Im(X n)}) \<in> HInfinite)"
+ (Abs_star(starrel `` {%n. Re(X n)}) \<in> HInfinite |
+ Abs_star(starrel `` {%n. Im(X n)}) \<in> HInfinite)"
by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_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) =
(x \<in> Infinitesimal & y \<in> Infinitesimal)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinitesimal_Infinitesimal_iff)
done
lemma hcomplex_split_CFinite_iff:
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CFinite) =
(x \<in> HFinite & y \<in> HFinite)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CFinite_HFinite_iff)
done
lemma hcomplex_split_SComplex_iff:
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> SComplex) =
(x \<in> Reals & y \<in> Reals)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal SComplex_SReal_iff)
done
lemma hcomplex_split_CInfinite_iff:
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y \<in> CInfinite) =
(x \<in> HInfinite | y \<in> HInfinite)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal CInfinite_HInfinite_iff)
done
@@ -1209,7 +1209,8 @@
"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y @c=
hcomplex_of_hypreal x' + iii * hcomplex_of_hypreal y') =
(x @= x' & y @= y')"
-apply (cases x, cases y, cases x', cases y')
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
+apply (rule_tac z=x' in eq_Abs_star, rule_tac z=y' in eq_Abs_star)
apply (simp add: iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal capprox_approx_iff)
done
--- a/src/HOL/Complex/NSComplex.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy Tue Sep 06 23:16:48 2005 +0200
@@ -48,17 +48,17 @@
(*--- real and Imaginary parts ---*)
hRe :: "hcomplex => hypreal"
- "hRe(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Re (X n)})"
+ "hRe(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Re (X n)})"
hIm :: "hcomplex => hypreal"
- "hIm(z) == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. Im (X n)})"
+ "hIm(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Im (X n)})"
(*----------- modulus ------------*)
hcmod :: "hcomplex => hypreal"
- "hcmod z == Abs_hypreal(UN X: Rep_hcomplex(z).
- hyprel `` {%n. cmod (X n)})"
+ "hcmod z == Abs_star(UN X: Rep_hcomplex(z).
+ starrel `` {%n. cmod (X n)})"
(*------ imaginary unit ----------*)
@@ -76,16 +76,16 @@
"hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})"
harg :: "hcomplex => hypreal"
- "harg z == Abs_hypreal(UN X:Rep_hcomplex(z). hyprel `` {%n. arg(X n)})"
+ "harg z == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. arg(X n)})"
(* abbreviation for (cos a + i sin a) *)
hcis :: "hypreal => hcomplex"
- "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
+ "hcis a == Abs_hcomplex(UN X:Rep_star(a). hcomplexrel `` {%n. cis (X n)})"
(*----- injection from hyperreals -----*)
hcomplex_of_hypreal :: "hypreal => hcomplex"
- "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
+ "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_star(r).
hcomplexrel `` {%n. complex_of_real (X n)})"
(* abbreviation for r*(cos a + i sin a) *)
@@ -186,17 +186,17 @@
lemma hRe:
"hRe(Abs_hcomplex (hcomplexrel `` {X})) =
- Abs_hypreal(hyprel `` {%n. Re(X n)})"
+ Abs_star(starrel `` {%n. Re(X n)})"
apply (simp add: hRe_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
apply (auto iff: hcomplexrel_iff, ultra)
done
lemma hIm:
"hIm(Abs_hcomplex (hcomplexrel `` {X})) =
- Abs_hypreal(hyprel `` {%n. Im(X n)})"
+ Abs_star(starrel `` {%n. Im(X n)})"
apply (simp add: hIm_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
apply (auto iff: hcomplexrel_iff, ultra)
done
@@ -452,7 +452,7 @@
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
lemma hcomplex_of_hypreal:
- "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
+ "hcomplex_of_hypreal (Abs_star(starrel `` {%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
apply (simp add: hcomplex_of_hypreal_def)
apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
@@ -460,7 +460,7 @@
lemma hcomplex_of_hypreal_cancel_iff [iff]:
"(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal)
done
@@ -472,19 +472,19 @@
lemma hcomplex_of_hypreal_minus [simp]:
"hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
done
lemma hcomplex_of_hypreal_inverse [simp]:
"hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
done
lemma hcomplex_of_hypreal_add [simp]:
"hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
done
@@ -495,7 +495,7 @@
lemma hcomplex_of_hypreal_mult [simp]:
"hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
done
@@ -507,35 +507,35 @@
done
lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (auto simp add: hcomplex_of_hypreal hRe)
done
lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
done
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
"hcomplex_of_hypreal epsilon \<noteq> 0"
-by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
+by (auto simp add: hcomplex_of_hypreal epsilon_def star_n_def hcomplex_zero_def)
subsection{*HComplex theorems*}
lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
done
lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
done
text{*Relates the two nonstandard constructions*}
lemma HComplex_eq_Abs_hcomplex_Complex:
- "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) =
+ "HComplex (Abs_star (starrel `` {X})) (Abs_star (starrel `` {Y})) =
Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})";
by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm)
@@ -551,10 +551,10 @@
lemma hcmod:
"hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
- Abs_hypreal(hyprel `` {%n. cmod (X n)})"
+ Abs_star(starrel `` {%n. cmod (X n)})"
apply (simp add: hcmod_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
apply (auto iff: hcomplexrel_iff, ultra)
done
@@ -565,7 +565,7 @@
by (simp add: hcomplex_one_def hcmod hypreal_one_num)
lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
done
@@ -578,7 +578,8 @@
apply (rule iffI)
prefer 2 apply simp
apply (simp add: HComplex_def iii_def)
-apply (cases x, cases y, cases x', cases y')
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star,
+ rule_tac z=x' in eq_Abs_star, rule_tac z=y' in eq_Abs_star)
apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal)
apply (ultra+)
done
@@ -651,7 +652,7 @@
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
"hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hcnj hcomplex_of_hypreal)
done
@@ -755,6 +756,7 @@
del: realpow_Suc)
apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
hypreal_add [symmetric] hypreal_mult [symmetric]
+ star_n_def [symmetric] star_of_def [symmetric]
hypreal_of_real_def [symmetric])
done
@@ -793,14 +795,14 @@
lemma hcmod_add_less:
"[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
-apply (cases x, cases y, cases r, cases s)
+apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
apply (auto intro: complex_mod_add_less)
done
lemma hcmod_mult_less:
"[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
-apply (cases x, cases y, cases r, cases s)
+apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
apply (auto intro: complex_mod_mult_less)
done
@@ -824,7 +826,7 @@
lemma hcomplex_of_hypreal_hyperpow:
"hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (cases x, cases n)
+apply (rule_tac z=x in eq_Abs_star, cases n)
apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
done
@@ -942,7 +944,7 @@
lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun
hypreal_mult hypreal_add hcmod numeral_2_eq_2)
done
@@ -985,7 +987,7 @@
"inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
@@ -1001,18 +1003,18 @@
lemma hRe_mult_i_eq[simp]:
"hRe (iii * hcomplex_of_hypreal y) = 0"
-apply (simp add: iii_def, cases y)
+apply (simp add: iii_def, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
done
lemma hIm_mult_i_eq [simp]:
"hIm (iii * hcomplex_of_hypreal y) = y"
-apply (simp add: iii_def, cases y)
+apply (simp add: iii_def, rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
done
lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
done
@@ -1025,22 +1027,22 @@
lemma harg:
"harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
- Abs_hypreal(hyprel `` {%n. arg (X n)})"
+ Abs_star(starrel `` {%n. arg (X n)})"
apply (simp add: harg_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
apply (auto iff: hcomplexrel_iff, ultra)
done
lemma cos_harg_i_mult_zero_pos:
"0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
done
lemma cos_harg_i_mult_zero_neg:
"y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult
hcomplex_add hypreal_zero_num hypreal_less starfun harg, ultra)
done
@@ -1052,7 +1054,7 @@
lemma hcomplex_of_hypreal_zero_iff [simp]:
"(hcomplex_of_hypreal y = 0) = (y = 0)"
-apply (cases y)
+apply (rule_tac z=y in eq_Abs_star)
apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
done
@@ -1065,10 +1067,10 @@
lemma lemma_hypreal_P_EX2:
"(\<exists>(x::hypreal) y. P x y) =
- (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
+ (\<exists>f g. P (Abs_star(starrel `` {f})) (Abs_star(starrel `` {g})))"
apply auto
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal, auto)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star, auto)
done
lemma hcomplex_split_polar:
@@ -1082,7 +1084,7 @@
done
lemma hcis:
- "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
+ "hcis (Abs_star(starrel `` {%n. X n})) =
Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
apply (simp add: hcis_def)
apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra)
@@ -1092,12 +1094,12 @@
"hcis a =
(hcomplex_of_hypreal(( *f* cos) a) +
iii * hcomplex_of_hypreal(( *f* sin) a))"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
done
lemma hrcis:
- "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
+ "hrcis (Abs_star(starrel `` {%n. X n})) (Abs_star(starrel `` {%n. Y n})) =
Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
@@ -1125,7 +1127,7 @@
lemma hcmod_unit_one [simp]:
"hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal
hcomplex_mult hcmod hcomplex_add hypreal_one_def)
done
@@ -1149,13 +1151,13 @@
lemma hrcis_mult:
"hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
-apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
+apply (simp add: hrcis_def, rule_tac z=r1 in eq_Abs_star, rule_tac z=r2 in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
hcomplex_mult cis_mult [symmetric])
done
lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
-apply (cases a, cases b)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
done
@@ -1163,12 +1165,12 @@
by (simp add: hcomplex_one_def hcis hypreal_zero_num)
lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
-apply (simp add: hcomplex_zero_def, cases a)
+apply (simp add: hcomplex_zero_def, rule_tac z=a in eq_Abs_star)
apply (simp add: hrcis hypreal_zero_num)
done
lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
-apply (cases r)
+apply (rule_tac z=r in eq_Abs_star)
apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
done
@@ -1180,7 +1182,7 @@
lemma hcis_hypreal_of_nat_Suc_mult:
"hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
done
@@ -1192,12 +1194,12 @@
lemma hcis_hypreal_of_hypnat_Suc_mult:
"hcis (hypreal_of_hypnat (n + 1) * a) =
hcis a * hcis (hypreal_of_hypnat n * a)"
-apply (cases a, cases n)
+apply (rule_tac z=a in eq_Abs_star, cases n)
apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
done
lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-apply (cases a, cases n)
+apply (rule_tac z=a in eq_Abs_star, cases n)
apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
done
@@ -1212,23 +1214,23 @@
done
lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hcomplex_inverse hcis hypreal_minus)
done
lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
-apply (cases a, cases r)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=r in eq_Abs_star)
apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
apply (simp add: real_divide_def)
done
lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hcis starfun hRe)
done
lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hcis starfun hIm)
done
@@ -1317,15 +1319,15 @@
lemma hRe_hcomplex_of_complex:
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
-by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
+by (simp add: hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def hRe)
lemma hIm_hcomplex_of_complex:
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
-by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
+by (simp add: hcomplex_of_complex_def hypreal_of_real_def star_of_def star_n_def hIm)
lemma hcmod_hcomplex_of_complex:
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
-by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
+by (simp add: hypreal_of_real_def star_of_def star_n_def hcomplex_of_complex_def hcmod)
subsection{*Numerals and Arithmetic*}
@@ -1365,6 +1367,7 @@
"hcomplex_of_hypreal (hypreal_of_real x) =
hcomplex_of_complex (complex_of_real x)"
by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def
+ star_of_def star_n_def
complex_of_real_def)
lemma hcomplex_hypreal_number_of:
--- a/src/HOL/Hyperreal/HLog.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HLog.thy Tue Sep 06 23:16:48 2005 +0200
@@ -12,7 +12,7 @@
(* should be in NSA.ML *)
lemma epsilon_ge_zero [simp]: "0 \<le> epsilon"
-by (simp add: epsilon_def hypreal_zero_num hypreal_le)
+by (simp add: epsilon_def star_n_def hypreal_zero_num hypreal_le)
lemma hpfinite_witness: "epsilon : {x. 0 \<le> x & x : HFinite}"
by auto
@@ -24,29 +24,29 @@
"x powhr a == ( *f* exp) (a * ( *f* ln) x)"
hlog :: "[hypreal,hypreal] => hypreal"
- "hlog a x == Abs_hypreal(\<Union>A \<in> Rep_hypreal(a).\<Union>X \<in> Rep_hypreal(x).
- hyprel `` {%n. log (A n) (X n)})"
+ "hlog a x == Abs_star(\<Union>A \<in> Rep_star(a).\<Union>X \<in> Rep_star(x).
+ starrel `` {%n. log (A n) (X n)})"
lemma powhr:
- "(Abs_hypreal(hyprel `` {X})) powhr (Abs_hypreal(hyprel `` {Y})) =
- Abs_hypreal(hyprel `` {%n. (X n) powr (Y n)})"
+ "(Abs_star(starrel `` {X})) powhr (Abs_star(starrel `` {Y})) =
+ Abs_star(starrel `` {%n. (X n) powr (Y n)})"
by (simp add: powhr_def starfun hypreal_mult powr_def)
lemma powhr_one_eq_one [simp]: "1 powhr a = 1"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_one_num)
done
lemma powhr_mult:
"[| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_zero_num hypreal_mult hypreal_less, ultra)
apply (simp add: powr_mult)
done
lemma powhr_gt_zero [simp]: "0 < x powhr a"
-apply (cases a, cases x)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star)
apply (simp add: hypreal_zero_def powhr hypreal_less hypreal_zero_num)
done
@@ -54,34 +54,34 @@
by (rule powhr_gt_zero [THEN hypreal_not_refl2, THEN not_sym])
lemma hypreal_divide:
- "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) =
- (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))"
+ "(Abs_star(starrel `` {X}))/(Abs_star(starrel `` {Y})) =
+ (Abs_star(starrel `` {%n. (X n::real)/(Y n)}))"
by (simp add: divide_inverse hypreal_zero_num hypreal_inverse hypreal_mult)
lemma powhr_divide:
"[| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_divide hypreal_zero_num hypreal_less, ultra)
apply (simp add: powr_divide)
done
lemma powhr_add: "x powhr (a + b) = (x powhr a) * (x powhr b)"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_add hypreal_mult powr_add)
done
lemma powhr_powhr: "(x powhr a) powhr b = x powhr (a * b)"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_mult powr_powr)
done
lemma powhr_powhr_swap: "(x powhr a) powhr b = (x powhr b) powhr a"
-apply (cases x, cases b, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=b in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr powr_powr_swap)
done
lemma powhr_minus: "x powhr (-a) = inverse (x powhr a)"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: powhr hypreal_minus hypreal_inverse hypreal_less powr_minus)
done
@@ -89,12 +89,12 @@
by (simp add: divide_inverse powhr_minus)
lemma powhr_less_mono: "[| a < b; 1 < x |] ==> x powhr a < x powhr b"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
done
lemma powhr_less_cancel: "[| x powhr a < x powhr b; 1 < x |] ==> a < b"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
apply (simp add: powhr hypreal_one_num hypreal_less, ultra)
done
@@ -107,26 +107,26 @@
by (simp add: linorder_not_less [symmetric])
lemma hlog:
- "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) =
- Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})"
+ "hlog (Abs_star(starrel `` {X})) (Abs_star(starrel `` {Y})) =
+ Abs_star(starrel `` {%n. log (X n) (Y n)})"
apply (simp add: hlog_def)
-apply (rule arg_cong [where f=Abs_hypreal], auto, ultra)
+apply (rule arg_cong [where f=Abs_star], auto, ultra)
done
lemma hlog_starfun_ln: "( *f* ln) x = hlog (( *f* exp) 1) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hlog log_ln hypreal_one_num)
done
lemma powhr_hlog_cancel [simp]:
"[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powhr (hlog a x) = x"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
done
lemma hlog_powhr_cancel [simp]:
"[| 0 < a; a \<noteq> 1 |] ==> hlog a (a powhr y) = y"
-apply (cases y, cases a)
+apply (rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: hlog powhr hypreal_zero_num hypreal_less hypreal_one_num, ultra)
apply (auto intro: log_powr_cancel)
done
@@ -134,27 +134,27 @@
lemma hlog_mult:
"[| 0 < a; a \<noteq> 1; 0 < x; 0 < y |]
==> hlog a (x * y) = hlog a x + hlog a y"
-apply (cases x, cases y, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: hlog powhr hypreal_zero_num hypreal_one_num hypreal_less hypreal_add hypreal_mult, ultra)
apply (simp add: log_mult)
done
lemma hlog_as_starfun:
"[| 0 < a; a \<noteq> 1 |] ==> hlog a x = ( *f* ln) x / ( *f* ln) a"
-apply (cases x, cases a)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star)
apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_divide log_def)
done
lemma hlog_eq_div_starfun_ln_mult_hlog:
"[| 0 < a; a \<noteq> 1; 0 < b; b \<noteq> 1; 0 < x |]
==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
-apply (cases x, cases a, cases b)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star)
apply (simp add: hlog starfun hypreal_zero_num hypreal_one_num hypreal_less hypreal_divide hypreal_mult, ultra)
apply (auto dest: log_eq_div_ln_mult_log)
done
lemma powhr_as_starfun: "x powhr a = ( *f* exp) (a * ( *f* ln) x)"
-apply (cases a, cases x)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star)
apply (simp add: powhr starfun hypreal_mult powr_def)
done
@@ -180,12 +180,12 @@
by (rule hlog_as_starfun, auto)
lemma hlog_one [simp]: "hlog a 1 = 0"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hypreal_one_num hypreal_zero_num hlog)
done
lemma hlog_eq_one [simp]: "[| 0 < a; a \<noteq> 1 |] ==> hlog a a = 1"
-apply (cases a)
+apply (rule_tac z=a in eq_Abs_star)
apply (simp add: hypreal_one_num hypreal_zero_num hlog hypreal_less, ultra)
apply (auto intro: log_eq_one)
done
@@ -202,7 +202,7 @@
lemma hlog_less_cancel_iff [simp]:
"[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x < hlog a y) = (x < y)"
-apply (cases a, cases x, cases y)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (auto simp add: hlog hypreal_less hypreal_zero_num hypreal_one_num, ultra+)
done
--- a/src/HOL/Hyperreal/HSeries.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy Tue Sep 06 23:16:48 2005 +0200
@@ -14,8 +14,8 @@
constdefs
sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
"sumhr p ==
- (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).
- hyprel ``{%n::nat. setsum f {X n..<Y n}})) p"
+ (%(M,N,f). Abs_star(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).
+ starrel ``{%n::nat. setsum f {X n..<Y n}})) p"
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80)
"f NSsums s == (%n. setsum f {0..<n}) ----NS> s"
@@ -30,9 +30,9 @@
lemma sumhr:
"sumhr(Abs_hypnat(hypnatrel``{%n. M n}),
Abs_hypnat(hypnatrel``{%n. N n}), f) =
- Abs_hypreal(hyprel `` {%n. setsum f {M n..<N n}})"
+ Abs_star(starrel `` {%n. setsum f {M n..<N n}})"
apply (simp add: sumhr_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
apply (auto, ultra)
done
@@ -78,7 +78,7 @@
lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
apply (cases m, cases n)
-apply (simp add: sumhr hypreal_of_real_def hypreal_mult setsum_mult)
+apply (simp add: sumhr hypreal_of_real_def star_of_def star_n_def hypreal_mult setsum_mult)
done
lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
@@ -107,6 +107,7 @@
"sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
apply (cases n)
apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat
+ star_of_def star_n_def
hypreal_mult real_of_nat_def)
done
@@ -139,7 +140,7 @@
lemma sumhr_hypreal_omega_minus_one: "sumhr(0, whn, %i. 1) = omega - 1"
by (simp add: hypnat_omega_def hypnat_zero_def omega_def hypreal_one_def
- sumhr hypreal_diff real_of_nat_def)
+ sumhr hypreal_diff real_of_nat_def star_n_def)
lemma sumhr_minus_one_realpow_zero [simp]:
"sumhr(0, whn + whn, %i. (-1) ^ (i+1)) = 0"
@@ -152,7 +153,7 @@
==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =
(hypreal_of_nat (na - m) * hypreal_of_real r)"
by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq hypreal_of_real_def
- real_of_nat_def hypreal_mult cong: setsum_ivl_cong)
+ real_of_nat_def star_of_def star_n_def hypreal_mult cong: setsum_ivl_cong)
lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
apply (cases N)
--- a/src/HOL/Hyperreal/HTranscendental.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Tue Sep 06 23:16:48 2005 +0200
@@ -54,13 +54,13 @@
by (simp add: starfun hypreal_one_num)
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow
simp del: hpowr_Suc realpow_Suc)
done
lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto intro: FreeUltrafilterNat_subset
simp add: hypreal_less starfun hrealpow hypreal_zero_num
simp del: hpowr_Suc realpow_Suc)
@@ -82,7 +82,7 @@
lemma hypreal_sqrt_mult_distrib:
"[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
apply (auto intro: real_sqrt_mult_distrib)
done
@@ -120,7 +120,7 @@
done
lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
apply (auto intro: real_sqrt_gt_zero)
done
@@ -129,7 +129,7 @@
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
done
@@ -141,7 +141,7 @@
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
"( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
done
@@ -161,7 +161,7 @@
done
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: starfun hypreal_add hrealpow hypreal_le
del: hpowr_Suc realpow_Suc)
done
@@ -292,7 +292,7 @@
by (auto intro: STAR_exp_Infinitesimal)
lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
-apply (cases x, cases y)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (simp add: starfun hypreal_add hypreal_mult exp_add)
done
@@ -301,7 +301,7 @@
apply (rule st_hypreal_of_real [THEN subst])
apply (rule approx_st_eq, auto)
apply (rule approx_minus_iff [THEN iffD2])
-apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
+apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
apply (insert exp_converges [of x])
apply (simp add: sums_def)
@@ -310,7 +310,7 @@
done
lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
apply (erule exp_ge_add_one_self_aux)
done
@@ -324,7 +324,7 @@
done
lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
done
@@ -338,7 +338,7 @@
done
lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
done
@@ -346,7 +346,7 @@
TRY a NS one today!!!
Goal "x @= 1 ==> ( *f* ln) x @= 1"
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","x")] eq_Abs_star 1);
by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
@@ -356,12 +356,12 @@
lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun)
done
lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_zero_num hypreal_less)
done
@@ -369,22 +369,22 @@
by (auto simp add: starfun)
lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
done
lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
done
lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
done
lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
done
@@ -395,15 +395,15 @@
done
lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
apply (simp add: ln_inverse)
done
lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
apply (rule_tac x = "exp u" in exI)
apply (ultra, arith)
done
@@ -449,7 +449,7 @@
done
lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
done
--- a/src/HOL/Hyperreal/HyperArith.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy Tue Sep 06 23:16:48 2005 +0200
@@ -13,6 +13,7 @@
subsection{*Numerals and Arithmetic*}
+(*
instance hypreal :: number ..
defs (overloaded)
@@ -21,11 +22,11 @@
instance hypreal :: number_ring
by (intro_classes, simp add: hypreal_number_of_def)
-
+*)
text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
-by (simp add: hypreal_number_of_def real_number_of_def)
+by (simp add: hypreal_of_real_def)
@@ -130,10 +131,11 @@
done
lemma hypreal_of_nat:
- "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
-apply (induct m)
-apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def
- hypreal_one_def hypreal_add)
+ "hypreal_of_nat m = Abs_star(starrel``{%n. real m})"
+apply (fold star_n_def star_of_def)
+apply (induct m)
+apply (simp_all add: hypreal_of_nat_def real_of_nat_def
+ hypreal_add)
done
lemma hypreal_of_nat_Suc:
--- a/src/HOL/Hyperreal/HyperDef.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Sep 06 23:16:48 2005 +0200
@@ -8,10 +8,13 @@
header{*Construction of Hyperreals Using Ultrafilters*}
theory HyperDef
-imports Filter "../Real/Real"
+(*imports Filter "../Real/Real"*)
+imports StarClasses "../Real/Real"
uses ("fuf.ML") (*Warning: file fuf.ML refers to the name Hyperdef!*)
begin
+types hypreal = "real star"
+(*
constdefs
FreeUltrafilterNat :: "nat set set" ("\<U>")
@@ -46,17 +49,33 @@
hypreal_divide_def:
"P / Q::hypreal == P * inverse Q"
+*)
+
+lemma hypreal_zero_def: "0 == Abs_star(starrel``{%n. 0})"
+by (simp only: star_zero_def star_of_def star_n_def)
+
+lemma hypreal_one_def: "1 == Abs_star(starrel``{%n. 1})"
+by (simp only: star_one_def star_of_def star_n_def)
+
+lemma hypreal_diff_def: "x - y == x + -(y::hypreal)"
+by (rule diff_def)
+
+lemma hypreal_divide_def: "P / Q::hypreal == P * inverse Q"
+by (rule divide_inverse [THEN eq_reflection])
constdefs
hypreal_of_real :: "real => hypreal"
- "hypreal_of_real r == Abs_hypreal(hyprel``{%n. r})"
+(* "hypreal_of_real r == Abs_hypreal(hyprel``{%n. r})" *)
+ "hypreal_of_real r == star_of r"
omega :: hypreal -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
- "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})"
+(* "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})" *)
+ "omega == star_n (%n. real (Suc n))"
epsilon :: hypreal -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
- "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})"
+(* "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})" *)
+ "epsilon == star_n (%n. inverse (real (Suc n)))"
syntax (xsymbols)
omega :: hypreal ("\<omega>")
@@ -66,7 +85,7 @@
omega :: hypreal ("\<omega>")
epsilon :: hypreal ("\<epsilon>")
-
+(*
defs (overloaded)
hypreal_add_def:
@@ -85,7 +104,7 @@
hypreal_less_def: "(x < (y::hypreal)) == (x \<le> y & x \<noteq> y)"
hrabs_def: "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
-
+*)
subsection{*The Set of Naturals is not Finite*}
@@ -116,7 +135,7 @@
lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
by (rule not_finite_nat [THEN freeultrafilter_Ex])
-lemma FreeUltrafilterNat_mem [simp]: "freeultrafilter FreeUltrafilterNat"
+lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
apply (unfold FreeUltrafilterNat_def)
apply (rule someI_ex)
apply (rule FreeUltrafilterNat_Ex)
@@ -210,53 +229,49 @@
by (auto, ultra)
-subsection{*Properties of @{term hyprel}*}
+subsection{*Properties of @{term starrel}*}
-text{*Proving that @{term hyprel} is an equivalence relation*}
+text{*Proving that @{term starrel} is an equivalence relation*}
-lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
-by (simp add: hyprel_def)
+lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
+by (simp add: starrel_def)
-lemma hyprel_refl: "(x,x) \<in> hyprel"
-by (simp add: hyprel_def)
+lemma starrel_refl: "(x,x) \<in> starrel"
+by (simp add: starrel_def)
-lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
-by (simp add: hyprel_def eq_commute)
+lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel"
+by (simp add: starrel_def eq_commute)
-lemma hyprel_trans:
- "[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
-by (simp add: hyprel_def, ultra)
+lemma starrel_trans:
+ "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel"
+by (simp add: starrel_def, ultra)
-lemma equiv_hyprel: "equiv UNIV hyprel"
-apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
-apply (blast intro: hyprel_sym hyprel_trans)
-done
+lemma equiv_starrel: "equiv UNIV starrel"
+by (rule StarType.equiv_starrel)
-(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) \<in> hyprel) *)
-lemmas equiv_hyprel_iff =
- eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp]
+(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
+lemmas equiv_starrel_iff =
+ eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp]
-lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
-by (simp add: hypreal_def hyprel_def quotient_def, blast)
+lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
+by (simp add: star_def starrel_def quotient_def, blast)
+declare Abs_star_inject [simp] Abs_star_inverse [simp]
+declare equiv_starrel [THEN eq_equiv_class_iff, simp]
+declare starrel_iff [iff]
-declare Abs_hypreal_inject [simp] Abs_hypreal_inverse [simp]
-declare equiv_hyprel [THEN eq_equiv_class_iff, simp]
-declare hyprel_iff [iff]
+lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
-lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel]
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
-lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
-by (simp add: hyprel_def)
-
-lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
-apply (simp add: hypreal_def)
+lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
+apply (simp add: star_def)
apply (auto elim!: quotientE equalityCE)
done
-lemma Rep_hypreal_nonempty [simp]: "Rep_hypreal x \<noteq> {}"
-by (insert Rep_hypreal [of x], auto)
-
+lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
+by (insert Rep_star [of x], auto)
subsection{*@{term hypreal_of_real}:
the Injection from @{typ real} to @{typ hypreal}*}
@@ -266,128 +281,116 @@
apply (simp add: hypreal_of_real_def split: split_if_asm)
done
-lemma eq_Abs_hypreal:
- "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
-apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
-apply (drule_tac f = Abs_hypreal in arg_cong)
-apply (force simp add: Rep_hypreal_inverse)
-done
+lemma eq_Abs_star:
+ "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P"
+by (fold star_n_def, auto intro: star_cases)
+(*
theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]:
- "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+ "(!!x. z = star_n x ==> P) ==> P"
by (rule eq_Abs_hypreal [of z], blast)
-
+*)
subsection{*Hyperreal Addition*}
-
+(*
lemma hypreal_add_congruent2:
- "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n + Y n})"
+ "congruent2 starrel starrel (%X Y. starrel``{%n. X n + Y n})"
by (simp add: congruent2_def, auto, ultra)
-
-lemma hypreal_add:
- "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =
- Abs_hypreal(hyprel``{%n. X n + Y n})"
-by (simp add: hypreal_add_def
- UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_add_congruent2])
+*)
+lemma hypreal_add [unfolded star_n_def]:
+ "star_n X + star_n Y = star_n (%n. X n + Y n)"
+by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n)
lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (cases z, cases w)
-apply (simp add: add_ac hypreal_add)
-done
+by (rule add_commute)
lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypreal_add real_add_assoc)
-done
+by (rule add_assoc)
lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-by (cases z, simp add: hypreal_zero_def hypreal_add)
+by (rule comm_monoid_add_class.add_0)
-instance hypreal :: comm_monoid_add
+(*instance hypreal :: comm_monoid_add
by intro_classes
(assumption |
- rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
+ rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+*)
lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
-by (simp add: hypreal_add_zero_left hypreal_add_commute)
+by (rule OrderedGroup.add_0_right)
subsection{*Additive inverse on @{typ hypreal}*}
-
-lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
+(*
+lemma hypreal_minus_congruent: "(%X. starrel``{%n. - (X n)}) respects starrel"
by (force simp add: congruent_def)
+*)
+lemma hypreal_minus [unfolded star_n_def]:
+ "- star_n X = star_n (%n. -(X n))"
+by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n)
-lemma hypreal_minus:
- "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse]
- UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
-
-lemma hypreal_diff:
- "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =
- Abs_hypreal(hyprel``{%n. X n - Y n})"
-by (simp add: hypreal_diff_def hypreal_minus hypreal_add)
+lemma hypreal_diff [unfolded star_n_def]:
+ "star_n X - star_n Y = star_n (%n. X n - Y n)"
+by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n)
lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
+by (rule right_minus)
lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
-by (simp add: hypreal_add_commute)
+by (rule left_minus)
subsection{*Hyperreal Multiplication*}
-
+(*
lemma hypreal_mult_congruent2:
- "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n * Y n})"
+ "congruent2 starrel starrel (%X Y. starrel``{%n. X n * Y n})"
by (simp add: congruent2_def, auto, ultra)
+*)
-lemma hypreal_mult:
- "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =
- Abs_hypreal(hyprel``{%n. X n * Y n})"
-by (simp add: hypreal_mult_def
- UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_mult_congruent2])
+lemma hypreal_mult [unfolded star_n_def]:
+ "star_n X * star_n Y = star_n (%n. X n * Y n)"
+by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n)
lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-by (cases z, cases w, simp add: hypreal_mult mult_ac)
+by (rule mult_commute)
lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-by (cases z1, cases z2, cases z3, simp add: hypreal_mult mult_assoc)
+by (rule mult_assoc)
lemma hypreal_mult_1: "(1::hypreal) * z = z"
-by (cases z, simp add: hypreal_one_def hypreal_mult)
+by (rule mult_1_left)
lemma hypreal_add_mult_distrib:
"((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-by (cases z1, cases z2, cases w, simp add: hypreal_mult hypreal_add left_distrib)
+by (rule left_distrib)
text{*one and zero are distinct*}
lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
-by (simp add: hypreal_zero_def hypreal_one_def)
+by (rule zero_neq_one)
subsection{*Multiplicative Inverse on @{typ hypreal} *}
-
+(*
lemma hypreal_inverse_congruent:
- "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
+ "(%X. starrel``{%n. if X n = 0 then 0 else inverse(X n)}) respects starrel"
by (auto simp add: congruent_def, ultra)
-
-lemma hypreal_inverse:
- "inverse (Abs_hypreal(hyprel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse]
- UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
+*)
+lemma hypreal_inverse [unfolded star_n_def]:
+ "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))"
+apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
+apply (rule_tac f=star_n in arg_cong)
+apply (rule ext)
+apply simp
+done
lemma hypreal_mult_inverse:
"x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (cases x)
-apply (simp add: hypreal_one_def hypreal_zero_def hypreal_inverse hypreal_mult)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
-done
+by (rule right_inverse)
lemma hypreal_mult_inverse_left:
"x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
-by (simp add: hypreal_mult_inverse hypreal_mult_commute)
+by (rule left_inverse)
+(*
instance hypreal :: field
proof
fix x y z :: hypreal
@@ -408,62 +411,57 @@
show "inverse 0 = (0::hypreal)"
by (simp add: hypreal_inverse hypreal_zero_def)
qed
-
+*)
subsection{*Properties of The @{text "\<le>"} Relation*}
-lemma hypreal_le:
- "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =
+lemma hypreal_le [unfolded star_n_def]:
+ "star_n X \<le> star_n Y =
({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (simp add: hypreal_le_def)
-apply (auto intro!: lemma_hyprel_refl, ultra)
-done
+by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-by (cases w, simp add: hypreal_le)
+by (rule order_refl)
lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-by (cases i, cases j, cases k, simp add: hypreal_le, ultra)
+by (rule order_trans)
lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-by (cases z, cases w, simp add: hypreal_le, ultra)
+by (rule order_antisym)
(* Axiom 'order_less_le' of class 'order': *)
lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: hypreal_less_def)
+by (rule order_less_le)
+(*
instance hypreal :: order
by intro_classes
(assumption |
rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
-
+*)
(* Axiom 'linorder_linear' of class 'linorder': *)
lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
-apply (cases z, cases w)
-apply (auto simp add: hypreal_le, ultra)
-done
+by (rule linorder_linear)
+(*
instance hypreal :: linorder
by intro_classes (rule hypreal_le_linear)
+*)
lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
by (auto)
lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_le hypreal_add)
-done
+by (rule add_left_mono)
lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult
- linorder_not_le [symmetric], ultra)
-done
+by (rule mult_strict_left_mono)
subsection{*The Hyperreals Form an Ordered Field*}
+(*
instance hypreal :: ordered_field
proof
fix x y z :: hypreal
@@ -474,6 +472,7 @@
show "\<bar>x\<bar> = (if x < 0 then -x else x)"
by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
qed
+*)
lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
by auto
@@ -490,41 +489,37 @@
lemma hypreal_of_real_add [simp]:
"hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_minus [simp]:
"hypreal_of_real (-r) = - hypreal_of_real r"
-by (auto simp add: hypreal_of_real_def hypreal_minus)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_diff [simp]:
"hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
-by (simp add: diff_minus)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_mult [simp]:
"hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
-by (simp add: hypreal_of_real_def hypreal_one_def)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
-by (simp add: hypreal_of_real_def hypreal_zero_def)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_le_iff [simp]:
"(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)"
-apply (simp add: hypreal_le_def hypreal_of_real_def, auto)
-apply (rule_tac [2] x = "%n. w" in exI, safe)
-apply (rule_tac [3] x = "%n. z" in exI, auto)
-apply (rule FreeUltrafilterNat_P, ultra)
-done
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_less_iff [simp]:
"(hypreal_of_real w < hypreal_of_real z) = (w < z)"
-by (simp add: linorder_not_le [symmetric])
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_eq_iff [simp]:
"(hypreal_of_real w = hypreal_of_real z) = (w = z)"
-by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
+by (simp add: hypreal_of_real_def)
text{*As above, for 0*}
@@ -548,60 +543,45 @@
lemma hypreal_of_real_inverse [simp]:
"hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
-apply (case_tac "r=0", simp)
-apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1])
-apply (auto simp add: hypreal_of_real_mult [symmetric])
-done
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_divide [simp]:
"hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
-by (simp add: hypreal_divide_def real_divide_def)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
-by (induct n, simp_all)
+by (simp add: hypreal_of_real_def)
lemma hypreal_of_real_of_int [simp]: "hypreal_of_real (of_int z) = of_int z"
-proof (cases z)
- case (1 n)
- thus ?thesis by simp
-next
- case (2 n)
- thus ?thesis
- by (simp only: of_int_minus hypreal_of_real_minus, simp)
-qed
+by (simp add: hypreal_of_real_def)
subsection{*Misc Others*}
-lemma hypreal_less:
- "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) =
- ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-by (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
+lemma hypreal_less [unfolded star_n_def]:
+ "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
-lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
-by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_zero_num [unfolded star_n_def]: "0 = star_n (%n. 0)"
+by (simp add: star_zero_def star_of_def)
-lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})"
-by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_one_num [unfolded star_n_def]: "1 = star_n (%n. 1)"
+by (simp add: star_one_def star_of_def)
lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-by (auto simp add: omega_def hypreal_less hypreal_zero_num)
-
-lemma hypreal_hrabs:
- "abs (Abs_hypreal (hyprel `` {X})) =
- Abs_hypreal(hyprel `` {%n. abs (X n)})"
-apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
-apply ultra
-apply ultra
-apply arith
+apply (simp only: omega_def star_zero_def star_less_def star_of_def)
+apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
done
+lemma hypreal_hrabs [unfolded star_n_def]:
+ "abs (star_n X) = star_n (%n. abs (X n))"
+by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n)
subsection{*Existence of Infinite Hyperreal Number*}
-
+(*
lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
by (simp add: omega_def)
-
+*)
text{*Existence of infinite number not corresponding to any real number.
Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
@@ -618,6 +598,7 @@
lemma not_ex_hypreal_of_real_eq_omega:
"~ (\<exists>x. hypreal_of_real x = omega)"
apply (simp add: omega_def hypreal_of_real_def)
+apply (simp add: star_of_def star_n_eq_iff)
apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric]
lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
done
@@ -638,36 +619,40 @@
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
by (auto simp add: epsilon_def hypreal_of_real_def
+ star_of_def star_n_eq_iff
lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (simp add: epsilon_def hypreal_zero_def)
+by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
+ del: star_of_zero)
lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
-by (simp add: hypreal_inverse omega_def epsilon_def)
+apply (simp add: epsilon_def omega_def star_inverse_def)
+apply (simp add: Ifun_of_def star_of_def Ifun_star_n)
+done
ML
{*
-val hrabs_def = thm "hrabs_def";
-val hypreal_hrabs = thm "hypreal_hrabs";
+(* val hrabs_def = thm "hrabs_def"; *)
+(* val hypreal_hrabs = thm "hypreal_hrabs"; *)
val hypreal_zero_def = thm "hypreal_zero_def";
-val hypreal_one_def = thm "hypreal_one_def";
-val hypreal_minus_def = thm "hypreal_minus_def";
-val hypreal_diff_def = thm "hypreal_diff_def";
-val hypreal_inverse_def = thm "hypreal_inverse_def";
-val hypreal_divide_def = thm "hypreal_divide_def";
+(* val hypreal_one_def = thm "hypreal_one_def"; *)
+(* val hypreal_minus_def = thm "hypreal_minus_def"; *)
+(* val hypreal_diff_def = thm "hypreal_diff_def"; *)
+(* val hypreal_inverse_def = thm "hypreal_inverse_def"; *)
+(* val hypreal_divide_def = thm "hypreal_divide_def"; *)
val hypreal_of_real_def = thm "hypreal_of_real_def";
val omega_def = thm "omega_def";
val epsilon_def = thm "epsilon_def";
-val hypreal_add_def = thm "hypreal_add_def";
-val hypreal_mult_def = thm "hypreal_mult_def";
-val hypreal_less_def = thm "hypreal_less_def";
-val hypreal_le_def = thm "hypreal_le_def";
+(* val hypreal_add_def = thm "hypreal_add_def"; *)
+(* val hypreal_mult_def = thm "hypreal_mult_def"; *)
+(* val hypreal_less_def = thm "hypreal_less_def"; *)
+(* val hypreal_le_def = thm "hypreal_le_def"; *)
val finite_exhausts = thm "finite_exhausts";
val finite_not_covers = thm "finite_not_covers";
@@ -689,15 +674,15 @@
val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
-val hyprel_iff = thm "hyprel_iff";
-val hyprel_in_hypreal = thm "hyprel_in_hypreal";
-val Abs_hypreal_inverse = thm "Abs_hypreal_inverse";
-val lemma_hyprel_refl = thm "lemma_hyprel_refl";
+val starrel_iff = thm "starrel_iff";
+val starrel_in_hypreal = thm "starrel_in_hypreal";
+val Abs_star_inverse = thm "Abs_star_inverse";
+val lemma_starrel_refl = thm "lemma_starrel_refl";
val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-val eq_Abs_hypreal = thm "eq_Abs_hypreal";
-val hypreal_minus_congruent = thm "hypreal_minus_congruent";
+val eq_Abs_star = thm "eq_Abs_star";
+(* val hypreal_minus_congruent = thm "hypreal_minus_congruent"; *)
val hypreal_minus = thm "hypreal_minus";
val hypreal_add = thm "hypreal_add";
val hypreal_diff = thm "hypreal_diff";
@@ -712,7 +697,7 @@
val hypreal_mult_assoc = thm "hypreal_mult_assoc";
val hypreal_mult_1 = thm "hypreal_mult_1";
val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
-val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
+(* val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; *)
val hypreal_inverse = thm "hypreal_inverse";
val hypreal_mult_inverse = thm "hypreal_mult_inverse";
val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
@@ -741,7 +726,7 @@
val hypreal_one_num = thm "hypreal_one_num";
val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
-val Rep_hypreal_omega = thm"Rep_hypreal_omega";
+(* val Rep_hypreal_omega = thm"Rep_hypreal_omega"; *)
val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
val lemma_finite_omega_set = thm"lemma_finite_omega_set";
val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
--- a/src/HOL/Hyperreal/HyperNat.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy Tue Sep 06 23:16:48 2005 +0200
@@ -692,24 +692,24 @@
constdefs
hypreal_of_hypnat :: "hypnat => hypreal"
"hypreal_of_hypnat N ==
- Abs_hypreal(\<Union>X \<in> Rep_hypnat(N). hyprel``{%n::nat. real (X n)})"
+ Abs_star(\<Union>X \<in> Rep_hypnat(N). starrel``{%n::nat. real (X n)})"
lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
by (simp add: hypreal_of_nat_def)
(*WARNING: FRAGILE!*)
-lemma lemma_hyprel_FUFN:
- "(Ya \<in> hyprel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
+lemma lemma_starrel_FUFN:
+ "(Ya \<in> starrel ``{%n. f(n)}) = ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
by force
lemma hypreal_of_hypnat:
"hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. real (X n)})"
+ Abs_star(starrel `` {%n. real (X n)})"
apply (simp add: hypreal_of_hypnat_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (rule_tac f = Abs_star in arg_cong)
apply (auto elim: FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset]
- simp add: lemma_hyprel_FUFN)
+ simp add: lemma_starrel_FUFN)
done
lemma hypreal_of_hypnat_inject [simp]:
@@ -756,7 +756,7 @@
apply (cases n)
apply (auto simp add: hypreal_of_hypnat hypreal_inverse
HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
apply (drule_tac x = "m + 1" in spec, ultra)
done
--- a/src/HOL/Hyperreal/HyperPow.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy Tue Sep 06 23:16:48 2005 +0200
@@ -10,14 +10,14 @@
imports HyperArith HyperNat
begin
-instance hypreal :: power ..
+(* instance hypreal :: power .. *)
consts hpowr :: "[hypreal,nat] => hypreal"
+(*
primrec
hpowr_0: "r ^ 0 = (1::hypreal)"
hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
-
instance hypreal :: recpower
proof
fix z :: hypreal
@@ -25,7 +25,13 @@
show "z^0 = 1" by simp
show "z^(Suc n) = z * (z^n)" by simp
qed
+*)
+lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)"
+by (rule power_0)
+
+lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
+by (rule power_Suc)
consts
"pow" :: "[hypreal,hypnat] => hypreal" (infixr 80)
@@ -35,8 +41,8 @@
(* hypernatural powers of hyperreals *)
hyperpow_def:
"(R::hypreal) pow (N::hypnat) ==
- Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
- hyprel``{%n::nat. (X n) ^ (Y n)})"
+ Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_hypnat(N).
+ starrel``{%n::nat. (X n) ^ (Y n)})"
lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
by simp
@@ -84,9 +90,9 @@
done
lemma hrealpow:
- "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
+ "Abs_star(starrel``{%n. X n}) ^ m = Abs_star(starrel``{%n. (X n::real) ^ m})"
apply (induct_tac "m")
-apply (auto simp add: hypreal_one_def hypreal_mult)
+apply (auto simp add: hypreal_one_def hypreal_mult power_0)
done
lemma hrealpow_sum_square_expand:
@@ -115,16 +121,16 @@
subsection{*Powers with Hypernatural Exponents*}
-lemma hyperpow_congruent: "(%X Y. hyprel``{%n. (X n ^ Y n)}) respects hyprel"
+lemma hyperpow_congruent: "(%X Y. starrel``{%n. (X n ^ Y n)}) respects starrel"
by (auto simp add: congruent_def intro!: ext, fuf+)
lemma hyperpow:
- "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
- Abs_hypreal(hyprel``{%n. X n ^ Y n})"
+ "Abs_star(starrel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
+ Abs_star(starrel``{%n. X n ^ Y n})"
apply (unfold hyperpow_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (auto intro!: lemma_hyprel_refl bexI
- simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel
+apply (rule_tac f = Abs_star in arg_cong)
+apply (auto intro!: lemma_starrel_refl bexI
+ simp add: starrel_in_hypreal [THEN Abs_star_inverse] equiv_starrel
hyperpow_congruent, fuf)
done
@@ -138,54 +144,54 @@
lemma hyperpow_not_zero [rule_format (no_asm)]:
"r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
+apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow)
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
lemma hyperpow_inverse:
"r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, cases r)
+apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
apply (rule FreeUltrafilterNat_subset)
apply (auto dest: realpow_not_zero intro: power_inverse)
done
lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (cases n, cases r)
+apply (cases n, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
done
lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (cases n, cases m, cases r)
+apply (cases n, cases m, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
done
lemma hyperpow_one [simp]: "r pow (1::hypnat) = r"
-apply (unfold hypnat_one_def, cases r)
+apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow)
done
lemma hyperpow_two:
"r pow ((1::hypnat) + (1::hypnat)) = r * r"
-apply (unfold hypnat_one_def, cases r)
+apply (unfold hypnat_one_def, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow hypnat_add hypreal_mult)
done
lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def, cases n, cases r)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
simp add: hyperpow hypreal_less hypreal_le)
done
lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def, cases n, cases r)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
simp add: hyperpow hypreal_le)
done
lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def, cases n, cases x, cases y)
+apply (simp add: hypreal_zero_def, cases n, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_le hypreal_less)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
apply (auto intro: power_mono)
@@ -204,7 +210,7 @@
done
lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (cases n, cases r, cases s)
+apply (cases n, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
done
@@ -248,7 +254,7 @@
lemma hyperpow_less_le:
"[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (cases n, cases N, cases r)
+apply (cases n, cases N, rule_tac z=r in eq_Abs_star)
apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
hypreal_zero_def hypreal_one_def)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -263,7 +269,7 @@
lemma hyperpow_realpow:
"(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
-by (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
+by (simp add: hypreal_of_real_def star_of_def star_n_def hypnat_of_nat_eq hyperpow)
lemma hyperpow_SReal [simp]:
"(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
@@ -301,7 +307,7 @@
lemma hrealpow_hyperpow_Infinitesimal_iff:
"(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
apply (simp add: hrealpow hyperpow hypnat_of_nat_eq)
done
--- a/src/HOL/Hyperreal/Lim.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Tue Sep 06 23:16:48 2005 +0200
@@ -226,9 +226,9 @@
"f -- x --> L ==> f -- x --NS> L"
apply (simp add: LIM_def NSLIM_def approx_def)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = xa in eq_Abs_hypreal)
-apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, clarify)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & \<bar>(xa n) + - x\<bar> < s --> \<bar>f (xa n) + - L\<bar> < u")
@@ -270,10 +270,10 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (auto simp add: starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add, blast)
apply (drule spec, drule mp, assumption)
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -451,9 +451,9 @@
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: add_commute)
-apply (rule_tac [2] z = x in eq_Abs_hypreal)
-apply (rule_tac [4] z = x in eq_Abs_hypreal)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
+apply (rule_tac [2] z = x in eq_Abs_star)
+apply (rule_tac [4] z = x in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
done
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
@@ -579,10 +579,10 @@
lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
apply (simp add: isNSUCont_def isUCont_def approx_def)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
apply (auto simp add: starfun hypreal_minus hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u")
@@ -620,8 +620,8 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2u, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (drule_tac x = "Abs_hypreal (hyprel``{Y})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{Y})" in spec)
apply (simp add: starfun hypreal_minus hypreal_add, auto)
apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
--- a/src/HOL/Hyperreal/NSA.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Tue Sep 06 23:16:48 2005 +0200
@@ -1774,32 +1774,33 @@
subsection{*Alternative Definitions for @{term HFinite} using Free Ultrafilter*}
lemma FreeUltrafilterNat_Rep_hypreal:
- "[| X \<in> Rep_hypreal x; Y \<in> Rep_hypreal x |]
+ "[| X \<in> Rep_star x; Y \<in> Rep_star x |]
==> {n. X n = Y n} \<in> FreeUltrafilterNat"
-by (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
+by (rule_tac z = x in eq_Abs_star, auto, ultra)
lemma HFinite_FreeUltrafilterNat:
"x \<in> HFinite
- ==> \<exists>X \<in> Rep_hypreal x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
-apply (cases x)
+ ==> \<exists>X \<in> Rep_star x. \<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat"
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x]
+ star_of_def star_n_def
hypreal_less SReal_iff hypreal_minus hypreal_of_real_def)
apply (rule_tac x=x in bexI)
apply (rule_tac x=y in exI, auto, ultra)
done
lemma FreeUltrafilterNat_HFinite:
- "\<exists>X \<in> Rep_hypreal x.
+ "\<exists>X \<in> Rep_star x.
\<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> HFinite"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: HFinite_def abs_less_iff minus_less_iff [of x])
apply (rule_tac x = "hypreal_of_real u" in bexI)
-apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def, ultra+)
+apply (auto simp add: hypreal_less SReal_iff hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+)
done
lemma HFinite_FreeUltrafilterNat_iff:
- "(x \<in> HFinite) = (\<exists>X \<in> Rep_hypreal x.
+ "(x \<in> HFinite) = (\<exists>X \<in> Rep_star x.
\<exists>u. {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
apply (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
done
@@ -1828,7 +1829,7 @@
ultrafilter for Infinite numbers!
-------------------------------------*)
lemma FreeUltrafilterNat_const_Finite:
- "[| xa: Rep_hypreal x;
+ "[| xa: Rep_star x;
{n. abs (xa n) = u} \<in> FreeUltrafilterNat
|] ==> x \<in> HFinite"
apply (rule FreeUltrafilterNat_HFinite)
@@ -1838,7 +1839,7 @@
done
lemma HInfinite_FreeUltrafilterNat:
- "x \<in> HInfinite ==> \<exists>X \<in> Rep_hypreal x.
+ "x \<in> HInfinite ==> \<exists>X \<in> Rep_star x.
\<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat"
apply (frule HInfinite_HFinite_iff [THEN iffD1])
apply (cut_tac x = x in Rep_hypreal_nonempty)
@@ -1861,7 +1862,7 @@
by (auto intro: order_less_asym)
lemma FreeUltrafilterNat_HInfinite:
- "\<exists>X \<in> Rep_hypreal x. \<forall>u.
+ "\<exists>X \<in> Rep_star x. \<forall>u.
{n. u < abs (X n)} \<in> FreeUltrafilterNat
==> x \<in> HInfinite"
apply (rule HInfinite_HFinite_iff [THEN iffD2])
@@ -1875,7 +1876,7 @@
done
lemma HInfinite_FreeUltrafilterNat_iff:
- "(x \<in> HInfinite) = (\<exists>X \<in> Rep_hypreal x.
+ "(x \<in> HInfinite) = (\<exists>X \<in> Rep_star x.
\<forall>u. {n. u < abs (X n)} \<in> FreeUltrafilterNat)"
by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
@@ -1883,31 +1884,31 @@
subsection{*Alternative Definitions for @{term Infinitesimal} using Free Ultrafilter*}
lemma Infinitesimal_FreeUltrafilterNat:
- "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_hypreal x.
+ "x \<in> Infinitesimal ==> \<exists>X \<in> Rep_star x.
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat"
apply (simp add: Infinitesimal_def)
apply (auto simp add: abs_less_iff minus_less_iff [of x])
-apply (cases x)
-apply (auto, rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (rule_tac z = x in eq_Abs_star)
+apply (auto, rule bexI [OF _ lemma_starrel_refl], safe)
apply (drule hypreal_of_real_less_iff [THEN iffD2])
apply (drule_tac x = "hypreal_of_real u" in bspec, auto)
-apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra)
+apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra)
done
lemma FreeUltrafilterNat_Infinitesimal:
- "\<exists>X \<in> Rep_hypreal x.
+ "\<exists>X \<in> Rep_star x.
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat
==> x \<in> Infinitesimal"
apply (simp add: Infinitesimal_def)
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: abs_less_iff abs_interval_iff minus_less_iff [of x])
apply (auto simp add: SReal_iff)
apply (drule_tac [!] x=y in spec)
-apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def, ultra+)
+apply (auto simp add: hypreal_less hypreal_minus hypreal_of_real_def star_of_def star_n_def, ultra+)
done
lemma Infinitesimal_FreeUltrafilterNat_iff:
- "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_hypreal x.
+ "(x \<in> Infinitesimal) = (\<exists>X \<in> Rep_star x.
\<forall>u. 0 < u --> {n. abs (X n) < u} \<in> FreeUltrafilterNat)"
apply (blast intro!: Infinitesimal_FreeUltrafilterNat FreeUltrafilterNat_Infinitesimal)
done
@@ -2008,7 +2009,7 @@
text{*@{term omega} is a member of @{term HInfinite}*}
-lemma hypreal_omega: "hyprel``{%n::nat. real (Suc n)} \<in> hypreal"
+lemma hypreal_omega: "starrel``{%n::nat. real (Suc n)} \<in> star"
by auto
lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
@@ -2017,10 +2018,10 @@
done
theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
-apply (simp add: omega_def)
+apply (simp add: omega_def star_n_def)
apply (auto intro!: FreeUltrafilterNat_HInfinite)
apply (rule bexI)
-apply (rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule_tac [2] lemma_starrel_refl, auto)
apply (simp (no_asm) add: real_of_nat_Suc diff_less_eq [symmetric] FreeUltrafilterNat_omega)
done
@@ -2122,13 +2123,13 @@
-----------------------------------------------------*)
lemma real_seq_to_hypreal_Infinitesimal:
"\<forall>n. abs(X n + -x) < inverse(real(Suc n))
- ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
-apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
+ ==> Abs_star(starrel``{X}) + -hypreal_of_real x \<in> Infinitesimal"
+apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset simp add: hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add Infinitesimal_FreeUltrafilterNat_iff hypreal_inverse)
done
lemma real_seq_to_hypreal_approx:
"\<forall>n. abs(X n + -x) < inverse(real(Suc n))
- ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
+ ==> Abs_star(starrel``{X}) @= hypreal_of_real x"
apply (subst approx_minus_iff)
apply (rule mem_infmal_iff [THEN subst])
apply (erule real_seq_to_hypreal_Infinitesimal)
@@ -2136,14 +2137,14 @@
lemma real_seq_to_hypreal_approx2:
"\<forall>n. abs(x + -X n) < inverse(real(Suc n))
- ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x"
+ ==> Abs_star(starrel``{X}) @= hypreal_of_real x"
apply (simp add: abs_minus_add_cancel real_seq_to_hypreal_approx)
done
lemma real_seq_to_hypreal_Infinitesimal2:
"\<forall>n. abs(X n + -Y n) < inverse(real(Suc n))
- ==> Abs_hypreal(hyprel``{X}) +
- -Abs_hypreal(hyprel``{Y}) \<in> Infinitesimal"
+ ==> Abs_star(starrel``{X}) +
+ -Abs_star(starrel``{Y}) \<in> Infinitesimal"
by (auto intro!: bexI
dest: FreeUltrafilterNat_inverse_real_of_posnat
FreeUltrafilterNat_all FreeUltrafilterNat_Int
--- a/src/HOL/Hyperreal/NatStar.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Tue Sep 06 23:16:48 2005 +0200
@@ -33,12 +33,12 @@
starfunNat :: "(nat => real) => hypnat => hypreal"
("*fNat* _" [80] 80)
- "*fNat* f == (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. f (X n)}))"
+ "*fNat* f == (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. f (X n)}))"
starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
("*fNatn* _" [80] 80)
"*fNatn* F ==
- (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))"
+ (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. (F n)(X n)}))"
InternalNatFuns :: "(hypnat => hypreal) set"
"InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
@@ -194,9 +194,9 @@
(* f::nat=>real *)
lemma starfunNat:
"( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. f (X n)})"
+ Abs_star(starrel `` {%n. f (X n)})"
apply (simp add: starfunNat_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_star])
apply (auto, ultra)
done
@@ -287,7 +287,7 @@
lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
apply (cases z)
-apply (simp add: starfunNat hypreal_of_real_def)
+apply (simp add: starfunNat hypreal_of_real_def star_of_def star_n_def)
done
lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat k"
@@ -312,7 +312,7 @@
lemma starfunNat_eq [simp]:
"( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"
-by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def)
+by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def star_of_def star_n_def)
lemma starfunNat2_eq [simp]:
"( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"
@@ -362,7 +362,7 @@
lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
apply (cases N)
-apply (simp add: hyperpow hypreal_of_real_def starfunNat)
+apply (simp add: hyperpow hypreal_of_real_def star_of_def star_n_def starfunNat)
done
lemma starfunNat_pow2:
@@ -372,7 +372,7 @@
done
lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
-apply (rule_tac z = R in eq_Abs_hypreal)
+apply (rule_tac z = R in eq_Abs_star)
apply (simp add: hyperpow starfun hypnat_of_nat_eq)
done
@@ -401,9 +401,9 @@
lemma starfunNat_n:
"( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. f n (X n)})"
+ Abs_star(starrel `` {%n. f n (X n)})"
apply (simp add: starfunNat_n_def)
-apply (rule_tac f = Abs_hypreal in arg_cong, auto, ultra)
+apply (rule_tac f = Abs_star in arg_cong, auto, ultra)
done
text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
@@ -436,7 +436,7 @@
lemma starfunNat_n_const_fun [simp]:
"( *fNatn* (%i x. k)) z = hypreal_of_real k"
apply (cases z)
-apply (simp add: starfunNat_n hypreal_of_real_def)
+apply (simp add: starfunNat_n hypreal_of_real_def star_of_def star_n_def)
done
lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
@@ -445,7 +445,7 @@
done
lemma starfunNat_n_eq [simp]:
- "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"
+ "( *fNatn* f) (hypnat_of_nat n) = Abs_star(starrel `` {%i. f i n})"
by (simp add: starfunNat_n hypnat_of_nat_eq)
lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)"
--- a/src/HOL/Hyperreal/SEQ.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Tue Sep 06 23:16:48 2005 +0200
@@ -70,7 +70,7 @@
lemma SEQ_Infinitesimal:
"( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
done
@@ -95,8 +95,9 @@
apply (rule_tac z = N in eq_Abs_hypnat)
apply (rule approx_minus_iff [THEN iffD2])
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
+ star_of_def star_n_def
hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hyprel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
apply (drule_tac x = u in spec, safe)
apply (drule_tac x = no in spec, fuf)
apply (blast dest: less_imp_le)
@@ -162,7 +163,7 @@
lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
- hypreal_of_real L \<approx> 0 |] ==> False"
-apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
+apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
apply (rename_tac "Y")
apply (drule_tac x = r in spec, safe)
apply (drule FreeUltrafilterNat_Int, assumption)
@@ -506,7 +507,7 @@
apply (rule_tac z = N in eq_Abs_hypnat)
apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff
HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hyprel_refl])
+apply (rule bexI [OF _ lemma_starrel_refl])
apply (drule_tac f = Xa in lemma_Bseq)
apply (rule_tac x = "K+1" in exI)
apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
@@ -537,9 +538,9 @@
lemma real_seq_to_hypreal_HInfinite:
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
- ==> Abs_hypreal(hyprel``{X o f}) : HInfinite"
+ ==> Abs_star(starrel``{X o f}) : HInfinite"
apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
-apply (rule bexI [OF _ lemma_hyprel_refl], clarify)
+apply (rule bexI [OF _ lemma_starrel_refl], clarify)
apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
apply (drule FreeUltrafilterNat_all)
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
@@ -1163,15 +1164,15 @@
subsection{*Hyperreals and Sequences*}
text{*A bounded sequence is a finite hyperreal*}
-lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite"
-by (auto intro!: bexI lemma_hyprel_refl
+lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_star(starrel``{X}) : HFinite"
+by (auto intro!: bexI lemma_starrel_refl
intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
Bseq_iff1a)
text{*A sequence converging to zero defines an infinitesimal*}
lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
- "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal"
+ "X ----NS> 0 ==> Abs_star(starrel``{X}) : Infinitesimal"
apply (simp add: NSLIMSEQ_def)
apply (drule_tac x = whn in bspec)
apply (simp add: HNatInfinite_whn)
--- a/src/HOL/Hyperreal/Star.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Star.thy Tue Sep 06 23:16:48 2005 +0200
@@ -13,27 +13,27 @@
constdefs
(* nonstandard extension of sets *)
starset :: "real set => hypreal set" ("*s* _" [80] 80)
- "*s* A == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
+ "*s* A == {x. \<forall>X \<in> Rep_star(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
(* internal sets *)
starset_n :: "(nat => real set) => hypreal set" ("*sn* _" [80] 80)
- "*sn* As == {x. \<forall>X \<in> Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
+ "*sn* As == {x. \<forall>X \<in> Rep_star(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"
InternalSets :: "hypreal set set"
"InternalSets == {X. \<exists>As. X = *sn* As}"
(* nonstandard extension of function *)
is_starext :: "[hypreal => hypreal, real => real] => bool"
- "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_hypreal(x). \<exists>Y \<in> Rep_hypreal(y).
+ "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
starfun :: "(real => real) => hypreal => hypreal" ("*f* _" [80] 80)
- "*f* f == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. f(X n)}))"
+ "*f* f == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. f(X n)}))"
(* internal functions *)
starfun_n :: "(nat => (real => real)) => hypreal => hypreal"
("*fn* _" [80] 80)
- "*fn* F == (%x. Abs_hypreal(\<Union>X \<in> Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))"
+ "*fn* F == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. (F n)(X n)}))"
InternalFuns :: "(hypreal => hypreal) set"
"InternalFuns == {X. \<exists>F. X = *fn* F}"
@@ -69,7 +69,7 @@
prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
apply (drule FreeUltrafilterNat_Compl_mem)
apply (drule bspec, assumption)
-apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
+apply (rule_tac z = x in eq_Abs_star, auto, ultra)
done
lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
@@ -80,7 +80,7 @@
lemma STAR_Compl: "*s* -A = -( *s* A)"
apply (auto simp add: starset_def)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
apply (auto dest!: bspec, ultra)
apply (drule FreeUltrafilterNat_Compl_mem, ultra)
done
@@ -97,23 +97,23 @@
done
lemma STAR_mem: "a \<in> A ==> hypreal_of_real a : *s* A"
-apply (simp add: starset_def hypreal_of_real_def)
+apply (simp add: starset_def hypreal_of_real_def star_of_def star_n_def)
apply (auto intro: FreeUltrafilterNat_subset)
done
lemma STAR_hypreal_of_real_image_subset: "hypreal_of_real ` A <= *s* A"
apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def)
apply (blast intro: FreeUltrafilterNat_subset)
done
lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def SReal_def)
-apply (simp add: hypreal_of_real_def [symmetric])
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def SReal_def)
+apply (fold star_n_def star_of_def hypreal_of_real_def)
apply (rule imageI, rule ccontr)
apply (drule bspec)
-apply (rule lemma_hyprel_refl)
+apply (rule lemma_starrel_refl)
prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
done
@@ -125,22 +125,22 @@
lemma STAR_real_seq_to_hypreal:
"\<forall>n. (X n) \<notin> M
- ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
+ ==> Abs_star(starrel``{X}) \<notin> *s* M"
apply (simp add: starset_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
done
lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
apply (simp add: starset_def)
-apply (auto simp add: hypreal_of_real_def)
-apply (rule_tac z = xa in eq_Abs_hypreal)
+apply (auto simp add: hypreal_of_real_def star_of_def star_n_def)
+apply (rule_tac z = xa in eq_Abs_star)
apply (auto intro: FreeUltrafilterNat_subset)
done
declare STAR_singleton [simp]
lemma STAR_not_mem: "x \<notin> F ==> hypreal_of_real x \<notin> *s* F"
-apply (auto simp add: starset_def hypreal_of_real_def)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (auto simp add: starset_def hypreal_of_real_def star_of_def star_n_def)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
done
lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
@@ -176,49 +176,49 @@
lemma hrabs_is_starext_rabs: "is_starext abs abs"
apply (simp add: is_starext_def, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal, auto)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star, auto)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl)
apply (auto dest!: spec
simp add: hypreal_minus abs_if hypreal_zero_def
hypreal_le hypreal_less)
apply (arith | ultra)+
done
-lemma Rep_hypreal_FreeUltrafilterNat:
- "[| X \<in> Rep_hypreal z; Y \<in> Rep_hypreal z |]
+lemma Rep_star_FreeUltrafilterNat:
+ "[| X \<in> Rep_star z; Y \<in> Rep_star z |]
==> {n. X n = Y n} : FreeUltrafilterNat"
-apply (cases z)
+apply (rule_tac z = z in eq_Abs_star)
apply (auto, ultra)
done
text{*Nonstandard extension of functions*}
-lemma starfun_congruent: "(%X. hyprel``{%n. f (X n)}) respects hyprel"
+lemma starfun_congruent: "(%X. starrel``{%n. f (X n)}) respects starrel"
by (simp add: congruent_def, auto, ultra)
lemma starfun:
- "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
- Abs_hypreal(hyprel `` {%n. f (X n)})"
+ "( *f* f) (Abs_star(starrel``{%n. X n})) =
+ Abs_star(starrel `` {%n. f (X n)})"
apply (simp add: starfun_def)
-apply (rule_tac f = Abs_hypreal in arg_cong)
-apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse]
- UN_equiv_class [OF equiv_hyprel starfun_congruent])
+apply (rule_tac f = Abs_star in arg_cong)
+apply (simp add: starrel_in_hypreal [THEN Abs_star_inverse]
+ UN_equiv_class [OF equiv_starrel starfun_congruent])
done
lemma starfun_if_eq:
"w \<noteq> hypreal_of_real x
==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
-apply (cases w)
-apply (simp add: hypreal_of_real_def starfun, ultra)
+apply (rule_tac z = w in eq_Abs_star)
+apply (simp add: hypreal_of_real_def star_of_def star_n_def starfun, ultra)
done
(*-------------------------------------------
multiplication: ( *f) x ( *g) = *(f x g)
------------------------------------------*)
lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
-by (cases xa, simp add: starfun hypreal_mult)
+by (rule_tac z = xa in eq_Abs_star, simp add: starfun hypreal_mult)
declare starfun_mult [symmetric, simp]
@@ -226,7 +226,7 @@
addition: ( *f) + ( *g) = *(f + g)
---------------------------------------*)
lemma starfun_add: "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"
-by (cases xa, simp add: starfun hypreal_add)
+by (rule_tac z = xa in eq_Abs_star, simp add: starfun hypreal_add)
declare starfun_add [symmetric, simp]
(*--------------------------------------------
@@ -234,7 +234,7 @@
-------------------------------------------*)
lemma starfun_minus: "- ( *f* f) x = ( *f* (%x. - f x)) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun hypreal_minus)
done
declare starfun_minus [symmetric, simp]
@@ -257,7 +257,7 @@
lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun)
done
@@ -268,8 +268,8 @@
text{*NS extension of constant function*}
lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real k"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def)
done
declare starfun_const_fun [simp]
@@ -277,12 +277,12 @@
text{*the NS extension of the identity function*}
lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real a"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun)
done
lemma starfun_Id: "( *f* (%x. x)) x = x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun)
done
declare starfun_Id [simp]
@@ -291,8 +291,8 @@
lemma is_starext_starfun: "is_starext ( *f* f) f"
apply (simp add: is_starext_def, auto)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
apply (auto intro!: bexI simp add: starfun)
done
@@ -301,7 +301,7 @@
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
apply (simp add: is_starext_def)
apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
apply (drule_tac x = x in spec)
apply (drule_tac x = "( *f* f) x" in spec)
apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
@@ -314,7 +314,7 @@
version for real arguments. i.e they are the same
for all real arguments*}
lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
-by (auto simp add: starfun hypreal_of_real_def)
+by (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def)
declare starfun_eq [simp]
@@ -323,13 +323,13 @@
(* useful for NS definition of derivatives *)
lemma starfun_lambda_cancel: "( *f* (%h. f (x + h))) xa = ( *f* f) (hypreal_of_real x + xa)"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_add)
done
lemma starfun_lambda_cancel2: "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"
-apply (cases xa)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_add)
done
lemma starfun_mult_HFinite_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m;
@@ -355,13 +355,13 @@
by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun hypreal_inverse hypreal_zero_def)
done
declare starfun_inverse_inverse [simp]
lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun hypreal_inverse)
done
declare starfun_inverse [symmetric, simp]
@@ -371,7 +371,7 @@
declare starfun_divide [symmetric, simp]
lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
done
@@ -380,7 +380,7 @@
lemma starfun_mem_starset:
"( *f* f) x : *s* A ==> x : *s* {x. f x \<in> A}"
apply (simp add: starset_def)
-apply (cases x)
+apply (rule_tac z = x in eq_Abs_star)
apply (auto simp add: starfun)
apply (rename_tac "X")
apply (drule_tac x = "%n. f (X n) " in bspec)
@@ -391,8 +391,8 @@
applied entrywise to equivalence class representative.
This is easily proved using starfun and ns extension thm*}
lemma hypreal_hrabs:
- "abs (Abs_hypreal (hyprel``{X})) = Abs_hypreal(hyprel `` {%n. abs (X n)})"
-by (simp add: starfun_rabs_hrabs [symmetric] starfun)
+ "abs (Abs_star (starrel``{X})) = Abs_star(starrel `` {%n. abs (X n)})"
+by (rule hypreal_hrabs)
text{*nonstandard extension of set through nonstandard extension
of rabs function i.e hrabs. A more general result should be
@@ -402,9 +402,10 @@
"*s* {x. abs (x + - y) < r} =
{x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
apply (simp add: starset_def, safe)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
apply (auto intro!: exI dest!: bspec
- simp add: hypreal_minus hypreal_of_real_def hypreal_add
+ simp add: hypreal_minus hypreal_of_real_def hypreal_add
+ star_of_def star_n_def
hypreal_hrabs hypreal_less)
apply ultra
done
@@ -413,9 +414,10 @@
"*s* {x. abs (f x + - y) < r} =
{x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
apply (simp add: starset_def, safe)
-apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (rule_tac [!] z = x in eq_Abs_star)
apply (auto intro!: exI dest!: bspec
simp add: hypreal_minus hypreal_of_real_def hypreal_add
+ star_of_def star_n_def
hypreal_hrabs hypreal_less starfun)
apply ultra
done
@@ -425,17 +427,18 @@
move both theorems??*}
lemma Infinitesimal_FreeUltrafilterNat_iff2:
"(x \<in> Infinitesimal) =
- (\<exists>X \<in> Rep_hypreal(x).
+ (\<exists>X \<in> Rep_star(x).
\<forall>m. {n. abs(X n) < inverse(real(Suc m))}
\<in> FreeUltrafilterNat)"
-apply (cases x)
-apply (auto intro!: bexI lemma_hyprel_refl
+apply (rule_tac z = x in eq_Abs_star)
+apply (auto intro!: bexI lemma_starrel_refl
simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def
+ star_of_def star_n_def
hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_eq)
apply (drule_tac x = n in spec, ultra)
done
-lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
+lemma approx_FreeUltrafilterNat_iff: "(Abs_star(starrel``{X}) @= Abs_star(starrel``{Y})) =
(\<forall>m. {n. abs (X n + - Y n) <
inverse(real(Suc m))} : FreeUltrafilterNat)"
apply (subst approx_minus_iff)
@@ -447,7 +450,7 @@
lemma inj_starfun: "inj starfun"
apply (rule inj_onI)
apply (rule ext, rule ccontr)
-apply (drule_tac x = "Abs_hypreal (hyprel ``{%n. xa}) " in fun_cong)
+apply (drule_tac x = "Abs_star (starrel ``{%n. xa}) " in fun_cong)
apply (auto simp add: starfun)
done
@@ -480,7 +483,7 @@
val starset_n_starset = thm "starset_n_starset";
val starfun_n_starfun = thm "starfun_n_starfun";
val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs";
-val Rep_hypreal_FreeUltrafilterNat = thm "Rep_hypreal_FreeUltrafilterNat";
+val Rep_star_FreeUltrafilterNat = thm "Rep_star_FreeUltrafilterNat";
val starfun_congruent = thm "starfun_congruent";
val starfun = thm "starfun";
val starfun_mult = thm "starfun_mult";
--- a/src/HOL/Hyperreal/Transcendental.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Sep 06 23:16:48 2005 +0200
@@ -2473,7 +2473,7 @@
by (erule DERIV_fun_exp)
lemma STAR_exp_ln: "0 < z ==> ( *f* (%x. exp (ln x))) z = z"
-apply (rule_tac z = z in eq_Abs_hypreal)
+apply (rule_tac z = z in eq_Abs_star)
apply (auto simp add: starfun hypreal_zero_def hypreal_less)
done
--- a/src/HOL/Hyperreal/fuf.ML Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/fuf.ML Tue Sep 06 23:16:48 2005 +0200
@@ -22,10 +22,10 @@
| get_fuf_hyps (x::xs) zs =
case (concl_of x) of
(_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
- Const ("HyperDef.FreeUltrafilterNat",_)))) => get_fuf_hyps xs
+ Const ("StarType.FreeUltrafilterNat",_)))) => get_fuf_hyps xs
((x RS FreeUltrafilterNat_Compl_mem)::zs)
|(_ $ (Const ("op :",_) $ _ $
- Const ("HyperDef.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs)
+ Const ("StarType.FreeUltrafilterNat",_))) => get_fuf_hyps xs (x::zs)
| _ => get_fuf_hyps xs zs;
fun inter_prems [] = raise FUFempty