--- a/src/HOL/Hyperreal/Lim.thy Fri Sep 09 17:47:37 2005 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Fri Sep 09 19:34:22 2005 +0200
@@ -226,12 +226,12 @@
"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_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 (rule_tac x = xa in star_cases)
+apply (auto simp add: real_add_minus_iff starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
+apply (rule bexI [OF _ Rep_star_star_n], 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")
+apply (subgoal_tac "\<forall>n::nat. (Xa n) \<noteq> x & \<bar>(Xa n) + - x\<bar> < s --> \<bar>f (Xa n) + - L\<bar> < u")
prefer 2 apply blast
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -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_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_tac x = "star_n X" in spec)
+apply (auto simp add: starfun star_n_minus star_of_def star_n_add star_n_eq_iff)
apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add, blast)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_of_def star_n_minus star_n_add star_n_eq_iff, 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_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)
+apply (rule_tac [2] x = x in star_cases)
+apply (rule_tac [4] x = x in star_cases)
+apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
done
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
@@ -579,13 +579,13 @@
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_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_starrel_refl, safe)
+apply (rule_tac x = x in star_cases)
+apply (rule_tac x = y in star_cases)
+apply (auto simp add: starfun star_n_minus star_n_add)
+apply (rule bexI [OF _ Rep_star_star_n], 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")
+apply (subgoal_tac "\<forall>n::nat. abs ((Xa n) + - (Xb n)) < s --> abs (f (Xa n) + - f (Xb n)) < u")
prefer 2 apply blast
apply (erule_tac V = "\<forall>x y. \<bar>x + - y\<bar> < s --> \<bar>f x + - f y\<bar> < u" in thin_rl)
apply (drule FreeUltrafilterNat_all, ultra)
@@ -620,11 +620,11 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2u, safe)
-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_tac x = "star_n X" in spec)
+apply (drule_tac x = "star_n Y" in spec)
+apply (simp add: starfun star_n_minus star_n_add, auto)
apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus star_n_add, blast)
apply (drule_tac x = r in spec, clarify)
apply (drule FreeUltrafilterNat_all, ultra)
done