--- a/src/HOL/Hyperreal/HyperDef.thy Thu Dec 14 22:08:35 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Thu Dec 14 22:09:26 2006 +0100
@@ -102,7 +102,7 @@
text{*Also, proof of various properties of @{term FreeUltrafilterNat}:
an arbitrary free ultrafilter*}
-
+(*
lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
by (rule nat_infinite [THEN freeultrafilter_Ex])
@@ -190,11 +190,12 @@
text{*One further property of our free ultrafilter*}
+
lemma FreeUltrafilterNat_Un:
"X Un Y \<in> FreeUltrafilterNat
==> X \<in> FreeUltrafilterNat | Y \<in> FreeUltrafilterNat"
by (auto, ultra)
-
+*)
subsection{*Properties of @{term starrel}*}
@@ -301,7 +302,7 @@
apply (simp add: omega_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])
+ lemma_finite_omega_set [THEN FreeUltrafilterNat.finite])
done
lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
@@ -320,7 +321,7 @@
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
by (auto simp add: epsilon_def star_of_def star_n_eq_iff
- lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
+ 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)
--- a/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 22:08:35 2006 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy Thu Dec 14 22:09:26 2006 +0100
@@ -271,12 +271,10 @@
hypnat_omega_def: "whn = star_n (%n::nat. n)"
lemma hypnat_of_nat_neq_whn: "hypnat_of_nat n \<noteq> whn"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
- FreeUltrafilterNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
lemma whn_neq_hypnat_of_nat: "whn \<noteq> hypnat_of_nat n"
-by (simp add: hypnat_omega_def star_of_def star_n_eq_iff
- FreeUltrafilterNat.finite)
+by (simp add: hypnat_omega_def star_of_def star_n_eq_iff)
lemma whn_not_Nats [simp]: "whn \<notin> Nats"
by (simp add: Nats_def image_def whn_neq_hypnat_of_nat)
@@ -297,9 +295,10 @@
lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
apply (insert finite_atMost [of m])
-apply (simp add: atMost_def)
-apply (drule FreeUltrafilterNat_finite)
-apply (drule FreeUltrafilterNat_Compl_mem, ultra)
+apply (simp add: atMost_def)
+apply (drule FreeUltrafilterNat.finite)
+apply (drule FreeUltrafilterNat.not_memD)
+apply (simp add: Collect_neg_eq [symmetric] linorder_not_le)
done
lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
@@ -341,16 +340,14 @@
==> {n. N < f n} \<in> FreeUltrafilterNat"
apply (induct_tac N)
apply (drule_tac x = 0 in spec)
-apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
-apply (drule_tac x = "Suc n" in spec, ultra)
+apply (rule ccontr, drule FreeUltrafilterNat.not_memD, drule FreeUltrafilterNat.Int, assumption, simp)
+apply (drule_tac x = "Suc n" in spec)
+apply (elim ultra, auto)
done
lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
-apply (auto simp add: HNatInfinite_def SHNat_eq hypnat_of_nat_eq)
-apply (rule_tac x = x in star_cases)
-apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma
- simp add: star_n_less FreeUltrafilterNat_Compl_iff1
- star_n_eq_iff Collect_neg_eq [symmetric])
+apply (safe intro!: Nats_less_HNatInfinite)
+apply (auto simp add: HNatInfinite_def)
done
--- a/src/HOL/Hyperreal/NSA.thy Thu Dec 14 22:08:35 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy Thu Dec 14 22:09:26 2006 +0100
@@ -1972,7 +1972,7 @@
apply (drule HInfinite_HFinite_iff [THEN iffD1])
apply (simp add: HFinite_FreeUltrafilterNat_iff)
apply (rule allI, drule_tac x="u + 1" in spec)
-apply (drule FreeUltrafilterNat_Compl_mem)
+apply (drule FreeUltrafilterNat.not_memD)
apply (simp add: Collect_neg_eq [symmetric] linorder_not_less)
apply (erule ultra, simp)
done
@@ -1989,7 +1989,9 @@
apply (rule HInfinite_HFinite_iff [THEN iffD2])
apply (safe, drule HFinite_FreeUltrafilterNat, safe)
apply (drule_tac x = u in spec)
-apply ultra
+apply (drule (1) FreeUltrafilterNat.Int)
+apply (simp add: Collect_conj_eq [symmetric])
+apply (subgoal_tac "\<forall>n. \<not> (norm (X n) < u \<and> u < norm (X n))", auto)
done
lemma HInfinite_FreeUltrafilterNat_iff:
@@ -2090,13 +2092,13 @@
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
"{n. abs(real n) \<le> u} \<notin> FreeUltrafilterNat"
-by (blast intro!: FreeUltrafilterNat_finite finite_rabs_real_of_nat_le_real)
+by (blast intro!: FreeUltrafilterNat.finite finite_rabs_real_of_nat_le_real)
lemma FreeUltrafilterNat_nat_gt_real: "{n. u < real n} \<in> FreeUltrafilterNat"
-apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
+apply (rule ccontr, drule FreeUltrafilterNat.not_memD)
apply (subgoal_tac "- {n::nat. u < real n} = {n. real n \<le> u}")
prefer 2 apply force
-apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat_finite])
+apply (simp add: finite_real_of_nat_le_real [THEN FreeUltrafilterNat.finite])
done
(*--------------------------------------------------------------
@@ -2112,7 +2114,7 @@
lemma FreeUltrafilterNat_omega: "{n. u < real n} \<in> FreeUltrafilterNat"
apply (cut_tac u = u in rabs_real_of_nat_le_real_FreeUltrafilterNat)
-apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_real_le_eq)
+apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_real_le_eq)
done
theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
@@ -2187,7 +2189,7 @@
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
"0 < u ==> {n. u \<le> inverse(real(Suc n))} \<notin> FreeUltrafilterNat"
-by (blast intro!: FreeUltrafilterNat_finite finite_inverse_real_of_posnat_ge_real)
+by (blast intro!: FreeUltrafilterNat.finite finite_inverse_real_of_posnat_ge_real)
(*--------------------------------------------------------------
The complement of {n. u \<le> inverse(real(Suc n))} =
@@ -2204,7 +2206,7 @@
"0 < u ==>
{n. inverse(real(Suc n)) < u} \<in> FreeUltrafilterNat"
apply (cut_tac u = u in inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
-apply (auto dest: FreeUltrafilterNat_Compl_mem simp add: Compl_le_inverse_eq)
+apply (auto dest: FreeUltrafilterNat.not_memD simp add: Compl_le_inverse_eq)
done
text{* Example where we get a hyperreal from a real sequence
@@ -2220,7 +2222,7 @@
lemma real_seq_to_hypreal_Infinitesimal:
"\<forall>n. norm(X n - x) < inverse(real(Suc n))
==> star_n X - star_of 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: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
+apply (auto intro!: bexI dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat.Int intro: order_less_trans FreeUltrafilterNat.subset simp add: star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse)
done
lemma real_seq_to_hypreal_approx:
@@ -2244,8 +2246,8 @@
==> star_n X - star_n Y \<in> Infinitesimal"
by (auto intro!: bexI
dest: FreeUltrafilterNat_inverse_real_of_posnat
- FreeUltrafilterNat_all FreeUltrafilterNat_Int
- intro: order_less_trans FreeUltrafilterNat_subset
+ FreeUltrafilterNat.Int
+ intro: order_less_trans FreeUltrafilterNat.subset
simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_diff
star_n_inverse)