# HG changeset patch
# User huffman
# Date 1166130566 -3600
# Node ID 74909ecaf20acbab248cee3348f69438ac55fa04
# Parent  42e9fd3ec1a385ff4f5c2c04e7cb607df51a3661
remove ultra tactic and redundant FreeUltrafilterNat lemmas

diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/HyperDef.thy
--- 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)
diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/HyperNat.thy
--- 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
 
 
diff -r 42e9fd3ec1a3 -r 74909ecaf20a src/HOL/Hyperreal/NSA.thy
--- 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)