--- 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