src/HOL/Hyperreal/Lim.thy

 text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*)
 lemma LIM_NSLIM:
       "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
 
 

 apply (simp add: LIM_def NSLIM_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, clarify)
 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
 
 

 apply (drule_tac x = "hypreal_of_real a + x" in spec)
 apply (drule_tac [2] x = "-hypreal_of_real a + x" in spec, safe, simp)
 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)"
 by (rule NSLIM_h_iff)
 

 by (simp add: isUCont_def isCont_def LIM_def, meson)
 
 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)
 done
 

 apply (simp add: isNSUCont_def isUCont_def approx_def)
 apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
 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
 
 text{*Derivatives*}