# HG changeset patch
# User huffman
# Date 1165964833 -3600
# Node ID b2d23672b003264e4fa959439be9b897329c363f
# Parent  4b93e949ac33d717242881de387bb729047d249a
generalized some lemmas; removed redundant lemmas; cleaned up some proofs

diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Complex/NSCA.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -132,10 +132,7 @@
 subsection{*The Finite Elements form a Subring*}
 
 lemma SComplex_subset_HFinite [simp]: "SComplex \<le> HFinite"
-apply (auto simp add: SComplex_def HFinite_def)
-apply (rule_tac x = "1 + hcmod (hcomplex_of_complex r) " in bexI)
-apply (auto intro: SReal_add)
-done
+by (auto simp add: SComplex_def)
 
 lemma HFinite_hcmod_hcomplex_of_complex [simp]:
      "hcmod (hcomplex_of_complex r) \<in> HFinite"
@@ -190,14 +187,6 @@
       |] ==> x \<in> Infinitesimal"
 by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
 
-lemma Infinitesimal_hcomplex_of_complex_mult:
-     "x \<in> Infinitesimal ==> x * hcomplex_of_complex r \<in> Infinitesimal"
-by (auto intro!: Infinitesimal_HFinite_mult simp add: Infinitesimal_hcmod_iff hcmod_mult)
-
-lemma Infinitesimal_hcomplex_of_complex_mult2:
-     "x \<in> Infinitesimal ==> hcomplex_of_complex r * x \<in> Infinitesimal"
-by (auto intro!: Infinitesimal_HFinite_mult2 simp add: Infinitesimal_hcmod_iff hcmod_mult)
-
 
 subsection{*The ``Infinitely Close'' Relation*}
 
@@ -209,7 +198,7 @@
 lemma approx_mult_subst_SComplex:
      "[| u @= x*hcomplex_of_complex v; x @= y |] 
       ==> u @= y*hcomplex_of_complex v"
-by (auto intro: approx_mult_subst2)
+by (rule approx_mult_subst_star_of)
 
 lemma approx_hcomplex_of_complex_HFinite:
      "x @= hcomplex_of_complex D ==> x \<in> HFinite"
@@ -247,6 +236,8 @@
 by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD]
             intro: approx_SComplex_mult_cancel)
 
+(* TODO: generalize following theorems: hcmod -> hnorm *)
+
 lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
 apply (subst hcmod_diff_commute)
 apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus)
@@ -273,9 +264,7 @@
 done
 
 lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y"
-by (auto intro: approx_hcmod_add_hcmod 
-         dest!: bex_Infinitesimal_iff2 [THEN iffD2]
-         simp add: mem_infmal_iff)
+by (rule approx_hnorm)
 
 
 subsection{*Zero is the Only Infinitesimal Complex Number*}
@@ -713,12 +702,4 @@
      "hcomplex_of_hypreal epsilon \<in> Infinitesimal"
 by (simp add: Infinitesimal_hcmod_iff)
 
-lemma hcomplex_of_complex_approx_zero_iff [simp]:
-     "(hcomplex_of_complex z @= 0) = (z = 0)"
-by (simp add: star_of_zero [symmetric] del: star_of_zero)
-
-lemma hcomplex_of_complex_approx_zero_iff2 [simp]:
-     "(0 @= hcomplex_of_complex z) = (z = 0)"
-by (simp add: star_of_zero [symmetric] del: star_of_zero)
-
 end
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/Deriv.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -483,8 +483,8 @@
          in add_commute [THEN subst])
 apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym]
                     Infinitesimal_add Infinitesimal_mult
-                    Infinitesimal_hypreal_of_real_mult
-                    Infinitesimal_hypreal_of_real_mult2
+                    Infinitesimal_star_of_mult
+                    Infinitesimal_star_of_mult2
           simp add: add_assoc [symmetric])
 done
 
@@ -536,7 +536,6 @@
             |] ==> D = 0"
 apply (simp add: nsderiv_def)
 apply (drule bspec, auto)
-apply (rule star_of_approx_iff [THEN iffD1], simp)
 done
 
 (* can be proved differently using NSLIM_isCont_iff *)
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -547,7 +547,7 @@
                    pi_divide_HNatInfinite_not_zero])
 apply (auto)
 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
-apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
+apply (auto intro: Reals_inverse simp add: divide_inverse mult_ac)
 done
 
 lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/HyperArith.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -20,16 +20,12 @@
 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
 by (blast intro!: order_le_less_trans abs_ge_zero)
 
-lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
+lemma hrabs_disj: "abs x = (x::'a::abs_if) | abs x = -x"
 by (simp add: abs_if)
 
 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
 by (simp add: abs_if split add: split_if_asm)
 
-lemma hypreal_of_real_hrabs:
-    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
-by (rule star_of_abs [symmetric])
-
 
 subsection{*Embedding the Naturals into the Hyperreals*}
 
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -198,38 +198,6 @@
 
 subsection{*Properties of @{term starrel}*}
 
-text{*Proving that @{term starrel} is an equivalence relation*}
-(*
-lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
-by (rule StarDef.starrel_iff)
-
-lemma starrel_refl: "(x,x) \<in> starrel"
-by (simp add: starrel_def)
-
-lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel"
-by (simp add: starrel_def eq_commute)
-
-lemma starrel_trans: 
-      "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel"
-by (simp add: starrel_def, ultra)
-
-lemma equiv_starrel: "equiv UNIV starrel"
-by (rule StarDef.equiv_starrel)
-
-lemmas equiv_starrel_iff =
-    eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] 
-
-lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
-
-lemma hypreal_empty_not_mem [simp]: "{} \<notin> star"
-apply (simp add: star_def)
-apply (auto elim!: quotientE equalityCE)
-done
-
-lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
-by (insert Rep_star [of x], auto)
-*)
-
 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
 by (simp add: starrel_def)
 
@@ -242,7 +210,7 @@
 subsection{*@{term hypreal_of_real}: 
             the Injection from @{typ real} to @{typ hypreal}*}
 
-lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
+lemma inj_star_of: "inj star_of"
 by (rule inj_onI, simp)
 
 lemma mem_Rep_star_iff: "(X \<in> Rep_star x) = (x = star_n X)"
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -841,7 +841,7 @@
 
 lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
 apply (simp add: isNSCont_def)
-apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs)
+apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
 done
 
 lemma isCont_abs [simp]: "isCont abs (a::real)"
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -165,47 +165,13 @@
 
 subsection{*Closure Laws for the Standard Reals*}
 
-lemma SReal_add [simp]:
-     "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
-apply (auto simp add: SReal_def)
-apply (rule_tac x = "r + ra" in exI, simp)
-done
-
-lemma SReal_diff [simp]:
-     "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x - y \<in> Reals"
-apply (auto simp add: SReal_def)
-apply (rule_tac x = "r - ra" in exI, simp)
-done
-
-lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
-apply (simp add: SReal_def, safe)
-apply (rule_tac x = "r * ra" in exI)
-apply (simp (no_asm))
+lemma Reals_minus_iff [simp]: "(-x \<in> Reals) = (x \<in> Reals)"
+apply auto
+apply (drule Reals_minus, auto)
 done
 
-lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
-apply (simp add: SReal_def)
-apply (blast intro: star_of_inverse [symmetric])
-done
-
-lemma SReal_divide: "[| (x::hypreal) \<in> Reals;  y \<in> Reals |] ==> x/y \<in> Reals"
-by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse)
-
-lemma SReal_minus: "(x::hypreal) \<in> Reals ==> -x \<in> Reals"
-apply (simp add: SReal_def)
-apply (blast intro: star_of_minus [symmetric])
-done
-
-lemma SReal_minus_iff [simp]: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
-apply auto
-apply (drule SReal_minus, auto)
-done
-
-lemma SReal_add_cancel:
-     "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
-apply (drule_tac x = y in SReal_minus)
-apply (drule SReal_add, assumption, auto)
-done
+lemma Reals_add_cancel: "\<lbrakk>x + y \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+by (drule (1) Reals_diff, simp)
 
 lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
 apply (auto simp add: SReal_def)
@@ -216,27 +182,8 @@
 lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
 by (simp add: SReal_def)
 
-lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals"
-apply (simp only: star_of_number_of [symmetric])
-apply (rule SReal_hypreal_of_real)
-done
-
-(** As always with numerals, 0 and 1 are special cases **)
-
-lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals"
-apply (subst numeral_0_eq_0 [symmetric])
-apply (rule SReal_number_of)
-done
-
-lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals"
-apply (subst numeral_1_eq_1 [symmetric])
-apply (rule SReal_number_of)
-done
-
 lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
-apply (simp only: divide_inverse)
-apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
-done
+by simp
 
 text{*epsilon is not in Reals because it is an infinitesimal*}
 lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
@@ -260,7 +207,7 @@
 
 lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
 apply (auto simp add: SReal_def)
-apply (rule inj_hypreal_of_real [THEN inv_f_f, THEN subst], blast)
+apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
 done
 
 lemma SReal_hypreal_of_real_image:
@@ -298,20 +245,20 @@
 
 lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
 apply (simp add: HFinite_def)
-apply (blast intro!: SReal_add hnorm_add_less)
+apply (blast intro!: Reals_add hnorm_add_less)
 done
 
 lemma HFinite_mult:
   fixes x y :: "'a::real_normed_algebra star"
   shows "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
 apply (simp add: HFinite_def)
-apply (blast intro!: SReal_mult hnorm_mult_less)
+apply (blast intro!: Reals_mult hnorm_mult_less)
 done
 
 lemma HFinite_scaleHR:
   "[|x \<in> HFinite; y \<in> HFinite|] ==> scaleHR x y \<in> HFinite"
 apply (simp add: HFinite_def)
-apply (blast intro!: SReal_mult hnorm_scaleHR_less)
+apply (blast intro!: Reals_mult hnorm_scaleHR_less)
 done
 
 lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
@@ -321,15 +268,12 @@
 apply (simp add: HFinite_def)
 apply (rule_tac x="star_of (norm x) + 1" in bexI)
 apply (transfer, simp)
-apply (blast intro: SReal_add SReal_hypreal_of_real Reals_1)
+apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
 done
 
 lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
 by (auto simp add: SReal_def)
 
-lemma HFinite_hypreal_of_real: "hypreal_of_real x \<in> HFinite"
-by (rule HFinite_star_of)
-
 lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
 by (simp add: HFinite_def)
 
@@ -341,15 +285,15 @@
 by (simp add: HFinite_def)
 
 lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
-by (unfold star_number_def, rule HFinite_star_of)
+unfolding star_number_def by (rule HFinite_star_of)
 
 (** As always with numerals, 0 and 1 are special cases **)
 
 lemma HFinite_0 [simp]: "0 \<in> HFinite"
-by (unfold star_zero_def, rule HFinite_star_of)
+unfolding star_zero_def by (rule HFinite_star_of)
 
 lemma HFinite_1 [simp]: "1 \<in> HFinite"
-by (unfold star_one_def, rule HFinite_star_of)
+unfolding star_one_def by (rule HFinite_star_of)
 
 lemma HFinite_bounded:
   "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
@@ -422,7 +366,7 @@
 apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
 apply (subgoal_tac "0 < r / t")
 apply (rule hnorm_mult_less)
-apply (simp add: InfinitesimalD SReal_divide)
+apply (simp add: InfinitesimalD Reals_divide)
 apply assumption
 apply (simp only: divide_pos_pos)
 apply (erule order_le_less_trans [OF hnorm_ge_zero])
@@ -452,7 +396,7 @@
 apply (subgoal_tac "0 < r / t")
 apply (rule hnorm_mult_less)
 apply assumption
-apply (simp add: InfinitesimalD SReal_divide)
+apply (simp add: InfinitesimalD Reals_divide)
 apply (simp only: divide_pos_pos)
 apply (erule order_le_less_trans [OF hnorm_ge_zero])
 done
@@ -471,7 +415,7 @@
 lemma Compl_HFinite: "- HFinite = HInfinite"
 apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
 apply (rule_tac y="r + 1" in order_less_le_trans, simp)
-apply (simp add: SReal_add Reals_1)
+apply simp
 done
 
 lemma HInfinite_inverse_Infinitesimal:
@@ -481,7 +425,7 @@
 apply (subgoal_tac "x \<noteq> 0")
 apply (rule inverse_less_imp_less)
 apply (simp add: nonzero_hnorm_inverse)
-apply (simp add: HInfinite_def SReal_inverse)
+apply (simp add: HInfinite_def Reals_inverse)
 apply assumption
 apply (clarify, simp add: Compl_HFinite [symmetric])
 done
@@ -584,7 +528,7 @@
 apply (unfold Infinitesimal_def, clarify, rename_tac r s)
 apply (simp only: linorder_not_less hnorm_mult)
 apply (drule_tac x = "r * s" in bspec)
-apply (fast intro: SReal_mult)
+apply (fast intro: Reals_mult)
 apply (drule mp, blast intro: mult_pos_pos)
 apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
 apply (simp_all (no_asm_simp))
@@ -616,12 +560,12 @@
 apply (rule_tac x = 1 in bexI, auto)
 done
 
-lemma Infinitesimal_hypreal_of_real_mult:
+lemma Infinitesimal_star_of_mult:
   fixes x :: "'a::real_normed_algebra star"
   shows "x \<in> Infinitesimal ==> x * star_of r \<in> Infinitesimal"
 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult])
 
-lemma Infinitesimal_hypreal_of_real_mult2:
+lemma Infinitesimal_star_of_mult2:
   fixes x :: "'a::real_normed_algebra star"
   shows "x \<in> Infinitesimal ==> star_of r * x \<in> Infinitesimal"
 by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])
@@ -772,10 +716,6 @@
   shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
 by (auto intro: approx_mult_subst2)
 
-lemma approx_mult_subst_SReal:
-     "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
-by (rule approx_mult_subst_star_of)
-
 lemma approx_eq_imp: "a = b ==> a @= b"
 by (simp add: approx_def)
 
@@ -854,9 +794,6 @@
 lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
 by (rule approx_sym [THEN [2] approx_HFinite], auto)
 
-lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
-by (rule approx_star_of_HFinite)
-
 lemma approx_mult_HFinite:
   fixes a b c d :: "'a::real_normed_algebra star"
   shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
@@ -897,14 +834,9 @@
       ==> a*c @= star_of b*star_of d"
 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
 
-lemma approx_mult_hypreal_of_real:
-     "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
-      ==> a*c @= hypreal_of_real b*hypreal_of_real d"
-by (rule approx_mult_star_of)
-
 lemma approx_SReal_mult_cancel_zero:
      "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
-apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
+apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
 done
 
@@ -920,7 +852,7 @@
 
 lemma approx_SReal_mult_cancel:
      "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
-apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
+apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
 done
 
@@ -1012,13 +944,9 @@
      "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
 by simp
 
-lemma hypreal_of_real_Infinitesimal_iff_0:
-     "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
-by (rule star_of_Infinitesimal_iff_0)
-
 lemma number_of_not_Infinitesimal [simp]:
      "number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal"
-by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
+by (fast dest: Reals_number_of [THEN SReal_Infinitesimal_zero])
 
 (*again: 1 is a special case, but not 0 this time*)
 lemma one_not_Infinitesimal [simp]:
@@ -1056,7 +984,7 @@
   "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
 apply (simp add: divide_inverse)
 apply (auto intro!: Infinitesimal_HFinite_mult 
-            dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
+            dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 done
 
 (*------------------------------------------------------------------
@@ -1078,7 +1006,7 @@
   "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
 apply auto
 apply (simp add: approx_def)
-apply (drule (1) SReal_diff)
+apply (drule (1) Reals_diff)
 apply (drule (1) SReal_Infinitesimal_zero)
 apply simp
 done
@@ -1106,19 +1034,15 @@
 apply (unfold star_of_approx_iff)
 by (auto intro: sym)
 
-lemma hypreal_of_real_approx_iff:
-     "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
-by (rule star_of_approx_iff)
+lemma star_of_approx_number_of_iff [simp]:
+     "(star_of k @= number_of w) = (k = number_of w)"
+by (subst star_of_approx_iff [symmetric], auto)
 
-lemma hypreal_of_real_approx_number_of_iff [simp]:
-     "(hypreal_of_real k @= number_of w) = (k = number_of w)"
-by (subst hypreal_of_real_approx_iff [symmetric], auto)
+lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)"
+by (simp_all add: star_of_approx_iff [symmetric])
 
-(*And also for 0 and 1.*)
-(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
-lemma [simp]: "(hypreal_of_real k @= 0) = (k = 0)"
-              "(hypreal_of_real k @= 1) = (k = 1)"
-  by (simp_all add:  hypreal_of_real_approx_iff [symmetric])
+lemma star_of_approx_one_iff [simp]: "(star_of k @= 1) = (k = 1)"
+by (simp_all add: star_of_approx_iff [symmetric])
 
 lemma approx_unique_real:
      "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
@@ -1197,7 +1121,7 @@
 lemma lemma_st_part_nonempty:
   "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
 apply (drule HFiniteD, safe)
-apply (drule SReal_minus)
+apply (drule Reals_minus)
 apply (rule_tac x = "-t" in exI)
 apply (auto simp add: abs_less_iff)
 done
@@ -1221,8 +1145,8 @@
          r \<in> Reals;  0 < r |] ==> x \<le> t + r"
 apply (frule isLubD1a)
 apply (rule ccontr, drule linorder_not_le [THEN iffD2])
-apply (drule_tac x = t in SReal_add, assumption)
-apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto)
+apply (drule (1) Reals_add)
+apply (drule_tac y = "r + t" in isLubD1 [THEN setleD], auto)
 done
 
 lemma hypreal_setle_less_trans:
@@ -1254,7 +1178,7 @@
       ==> t + -r \<le> x"
 apply (frule isLubD1a)
 apply (rule ccontr, drule linorder_not_le [THEN iffD1])
-apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption)
+apply (drule Reals_minus, drule_tac a = t in Reals_add, assumption)
 apply (drule lemma_st_part_gt_ub, assumption+)
 apply (drule isLub_le_isUb, assumption)
 apply (drule lemma_minus_le_zero)
@@ -1300,8 +1224,8 @@
          r \<in> Reals; 0 < r |]
       ==> x + -t \<noteq> r"
 apply auto
-apply (frule isLubD1a [THEN SReal_minus])
-apply (drule SReal_add_cancel, assumption)
+apply (frule isLubD1a [THEN Reals_minus])
+apply (drule Reals_add_cancel, assumption)
 apply (drule_tac x = x in lemma_SReal_lub)
 apply (drule hypreal_isLub_unique, assumption, auto)
 done
@@ -1313,8 +1237,8 @@
       ==> -(x + -t) \<noteq> r"
 apply (auto)
 apply (frule isLubD1a)
-apply (drule SReal_add_cancel, assumption)
-apply (drule_tac x = "-x" in SReal_minus, simp)
+apply (drule Reals_add_cancel, assumption)
+apply (drule_tac a = "-x" in Reals_minus, simp)
 apply (drule_tac x = x in lemma_SReal_lub)
 apply (drule hypreal_isLub_unique, assumption, auto)
 done
@@ -1710,7 +1634,7 @@
 apply (drule approx_sym [THEN bex_Infinitesimal_iff2 [THEN iffD2]])
 apply (auto intro!: Infinitesimal_add_hypreal_of_real_less
             simp del: star_of_abs
-            simp add: hypreal_of_real_hrabs)
+            simp add: star_of_abs [symmetric])
 done
 
 lemma Infinitesimal_add_hrabs_hypreal_of_real_less2:
@@ -1907,7 +1831,7 @@
 by (simp add: st_unique st_SReal st_approx_self approx_add)
 
 lemma st_number_of [simp]: "st (number_of w) = number_of w"
-by (rule SReal_number_of [THEN st_SReal_eq])
+by (rule Reals_number_of [THEN st_SReal_eq])
 
 (*the theorem above for the special cases of zero and one*)
 lemma [simp]: "st 0 = 0" "st 1 = 1"
@@ -2110,7 +2034,7 @@
       (\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
 apply safe
 apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
-apply (simp (no_asm_use) add: SReal_inverse)
+apply (simp (no_asm_use))
 apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
 prefer 2 apply assumption
 apply (simp add: real_of_nat_def)
diff -r 4b93e949ac33 -r b2d23672b003 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Dec 13 00:02:53 2006 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Dec 13 00:07:13 2006 +0100
@@ -1008,7 +1008,7 @@
 lemma NSLIMSEQ_imp_rabs: "f ----NS> (l::real) ==> (%n. \<bar>f n\<bar>) ----NS> \<bar>l\<bar>"
 apply (simp add: NSLIMSEQ_def)
 apply (auto intro: approx_hrabs 
-            simp add: starfun_abs hypreal_of_real_hrabs [symmetric])
+            simp add: starfun_abs)
 done
 
 text{* standard version *}
@@ -1114,7 +1114,7 @@
 apply (drule bspec, assumption)
 apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption)
 apply (simp add: hyperpow_add)
-apply (drule approx_mult_subst_SReal, assumption)
+apply (drule approx_mult_subst_star_of, assumption)
 apply (drule approx_trans3, assumption)
 apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric])
 done