diff -r 17256fe71aca -r ad73fb6144cf src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Sep 06 23:16:48 2005 +0200
@@ -8,10 +8,13 @@
 header{*Construction of Hyperreals Using Ultrafilters*}
 
 theory HyperDef
-imports Filter "../Real/Real"
+(*imports Filter "../Real/Real"*)
+imports StarClasses "../Real/Real"
 uses ("fuf.ML")  (*Warning: file fuf.ML refers to the name Hyperdef!*)
 begin
 
+types hypreal = "real star"
+(*
 constdefs
 
   FreeUltrafilterNat   :: "nat set set"    ("\<U>")
@@ -46,17 +49,33 @@
 
   hypreal_divide_def:
   "P / Q::hypreal == P * inverse Q"
+*)
+
+lemma hypreal_zero_def: "0 == Abs_star(starrel``{%n. 0})"
+by (simp only: star_zero_def star_of_def star_n_def)
+
+lemma hypreal_one_def: "1 == Abs_star(starrel``{%n. 1})"
+by (simp only: star_one_def star_of_def star_n_def)
+
+lemma hypreal_diff_def: "x - y == x + -(y::hypreal)"
+by (rule diff_def)
+
+lemma hypreal_divide_def: "P / Q::hypreal == P * inverse Q"
+by (rule divide_inverse [THEN eq_reflection])
 
 constdefs
 
   hypreal_of_real  :: "real => hypreal"
-  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n. r})"
+(*  "hypreal_of_real r         == Abs_hypreal(hyprel``{%n. r})" *)
+  "hypreal_of_real r == star_of r"
 
   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})"
+(*  "omega == Abs_hypreal(hyprel``{%n. real (Suc n)})" *)
+  "omega == star_n (%n. real (Suc n))"
 
   epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})"
+(*  "epsilon == Abs_hypreal(hyprel``{%n. inverse (real (Suc n))})" *)
+  "epsilon == star_n (%n. inverse (real (Suc n)))"
 
 syntax (xsymbols)
   omega   :: hypreal   ("\<omega>")
@@ -66,7 +85,7 @@
   omega   :: hypreal   ("\<omega>")
   epsilon :: hypreal   ("\<epsilon>")
 
-
+(*
 defs (overloaded)
 
   hypreal_add_def:
@@ -85,7 +104,7 @@
   hypreal_less_def: "(x < (y::hypreal)) == (x \<le> y & x \<noteq> y)"
 
   hrabs_def:  "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
-
+*)
 
 subsection{*The Set of Naturals is not Finite*}
 
@@ -116,7 +135,7 @@
 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U"
 by (rule not_finite_nat [THEN freeultrafilter_Ex])
 
-lemma FreeUltrafilterNat_mem [simp]: "freeultrafilter FreeUltrafilterNat"
+lemma FreeUltrafilterNat_mem: "freeultrafilter FreeUltrafilterNat"
 apply (unfold FreeUltrafilterNat_def)
 apply (rule someI_ex)
 apply (rule FreeUltrafilterNat_Ex)
@@ -210,53 +229,49 @@
 by (auto, ultra)
 
 
-subsection{*Properties of @{term hyprel}*}
+subsection{*Properties of @{term starrel}*}
 
-text{*Proving that @{term hyprel} is an equivalence relation*}
+text{*Proving that @{term starrel} is an equivalence relation*}
 
-lemma hyprel_iff: "((X,Y) \<in> hyprel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
-by (simp add: hyprel_def)
+lemma starrel_iff: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> FreeUltrafilterNat)"
+by (simp add: starrel_def)
 
-lemma hyprel_refl: "(x,x) \<in> hyprel"
-by (simp add: hyprel_def)
+lemma starrel_refl: "(x,x) \<in> starrel"
+by (simp add: starrel_def)
 
-lemma hyprel_sym [rule_format (no_asm)]: "(x,y) \<in> hyprel --> (y,x) \<in> hyprel"
-by (simp add: hyprel_def eq_commute)
+lemma starrel_sym [rule_format (no_asm)]: "(x,y) \<in> starrel --> (y,x) \<in> starrel"
+by (simp add: starrel_def eq_commute)
 
-lemma hyprel_trans: 
-      "[|(x,y) \<in> hyprel; (y,z) \<in> hyprel|] ==> (x,z) \<in> hyprel"
-by (simp add: hyprel_def, ultra)
+lemma starrel_trans: 
+      "[|(x,y) \<in> starrel; (y,z) \<in> starrel|] ==> (x,z) \<in> starrel"
+by (simp add: starrel_def, ultra)
 
-lemma equiv_hyprel: "equiv UNIV hyprel"
-apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
-apply (blast intro: hyprel_sym hyprel_trans) 
-done
+lemma equiv_starrel: "equiv UNIV starrel"
+by (rule StarType.equiv_starrel)
 
-(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) \<in> hyprel) *)
-lemmas equiv_hyprel_iff =
-    eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] 
+(* (starrel `` {x} = starrel `` {y}) = ((x,y) \<in> starrel) *)
+lemmas equiv_starrel_iff =
+    eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I, simp] 
 
-lemma hyprel_in_hypreal [simp]: "hyprel``{x}:hypreal"
-by (simp add: hypreal_def hyprel_def quotient_def, blast)
+lemma starrel_in_hypreal [simp]: "starrel``{x}:star"
+by (simp add: star_def starrel_def quotient_def, blast)
 
+declare Abs_star_inject [simp] Abs_star_inverse [simp]
+declare equiv_starrel [THEN eq_equiv_class_iff, simp]
+declare starrel_iff [iff]
 
-declare Abs_hypreal_inject [simp] Abs_hypreal_inverse [simp]
-declare equiv_hyprel [THEN eq_equiv_class_iff, simp]
-declare hyprel_iff [iff]
+lemmas eq_starrelD = eq_equiv_class [OF _ equiv_starrel]
 
-lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel]
+lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
+by (simp add: starrel_def)
 
-lemma lemma_hyprel_refl [simp]: "x \<in> hyprel `` {x}"
-by (simp add: hyprel_def)
-
-lemma hypreal_empty_not_mem [simp]: "{} \<notin> hypreal"
-apply (simp add: hypreal_def)
+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_hypreal x \<noteq> {}"
-by (insert Rep_hypreal [of x], auto)
-
+lemma Rep_hypreal_nonempty [simp]: "Rep_star x \<noteq> {}"
+by (insert Rep_star [of x], auto)
 
 subsection{*@{term hypreal_of_real}: 
             the Injection from @{typ real} to @{typ hypreal}*}
@@ -266,128 +281,116 @@
 apply (simp add: hypreal_of_real_def split: split_if_asm)
 done
 
-lemma eq_Abs_hypreal:
-    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
-apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
-apply (drule_tac f = Abs_hypreal in arg_cong)
-apply (force simp add: Rep_hypreal_inverse)
-done
+lemma eq_Abs_star:
+    "(!!x. z = Abs_star(starrel``{x}) ==> P) ==> P"
+by (fold star_n_def, auto intro: star_cases)
 
+(*
 theorem hypreal_cases [case_names Abs_hypreal, cases type: hypreal]:
-    "(!!x. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
+    "(!!x. z = star_n x ==> P) ==> P"
 by (rule eq_Abs_hypreal [of z], blast)
-
+*)
 
 subsection{*Hyperreal Addition*}
-
+(*
 lemma hypreal_add_congruent2: 
-    "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n + Y n})"
+    "congruent2 starrel starrel (%X Y. starrel``{%n. X n + Y n})"
 by (simp add: congruent2_def, auto, ultra)
-
-lemma hypreal_add: 
-  "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =  
-   Abs_hypreal(hyprel``{%n. X n + Y n})"
-by (simp add: hypreal_add_def 
-         UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_add_congruent2])
+*)
+lemma hypreal_add [unfolded star_n_def]: 
+  "star_n X + star_n Y = star_n (%n. X n + Y n)"
+by (simp add: star_add_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (cases z, cases w)
-apply (simp add: add_ac hypreal_add)
-done
+by (rule add_commute)
 
 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypreal_add real_add_assoc)
-done
+by (rule add_assoc)
 
 lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-by (cases z, simp add: hypreal_zero_def hypreal_add)
+by (rule comm_monoid_add_class.add_0)
 
-instance hypreal :: comm_monoid_add
+(*instance hypreal :: comm_monoid_add
   by intro_classes
     (assumption | 
-      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+
+      rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+*)
 
 lemma hypreal_add_zero_right [simp]: "z + (0::hypreal) = z"
-by (simp add: hypreal_add_zero_left hypreal_add_commute)
+by (rule OrderedGroup.add_0_right)
 
 
 subsection{*Additive inverse on @{typ hypreal}*}
-
-lemma hypreal_minus_congruent: "(%X. hyprel``{%n. - (X n)}) respects hyprel"
+(*
+lemma hypreal_minus_congruent: "(%X. starrel``{%n. - (X n)}) respects starrel"
 by (force simp add: congruent_def)
+*)
+lemma hypreal_minus [unfolded star_n_def]: 
+   "- star_n X = star_n (%n. -(X n))"
+by (simp add: star_minus_def Ifun_of_def star_of_def Ifun_star_n)
 
-lemma hypreal_minus: 
-   "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
-              UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
-
-lemma hypreal_diff:
-     "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =  
-      Abs_hypreal(hyprel``{%n. X n - Y n})"
-by (simp add: hypreal_diff_def hypreal_minus hypreal_add)
+lemma hypreal_diff [unfolded star_n_def]:
+     "star_n X - star_n Y = star_n (%n. X n - Y n)"
+by (simp add: star_diff_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_add_minus [simp]: "z + -z = (0::hypreal)"
-by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
+by (rule right_minus)
 
 lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
-by (simp add: hypreal_add_commute)
+by (rule left_minus)
 
 
 subsection{*Hyperreal Multiplication*}
-
+(*
 lemma hypreal_mult_congruent2: 
-    "congruent2 hyprel hyprel (%X Y. hyprel``{%n. X n * Y n})"
+    "congruent2 starrel starrel (%X Y. starrel``{%n. X n * Y n})"
 by (simp add: congruent2_def, auto, ultra)
+*)
 
-lemma hypreal_mult: 
-  "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =  
-   Abs_hypreal(hyprel``{%n. X n * Y n})"
-by (simp add: hypreal_mult_def
-        UN_equiv_class2 [OF equiv_hyprel equiv_hyprel hypreal_mult_congruent2])
+lemma hypreal_mult [unfolded star_n_def]: 
+  "star_n X * star_n Y = star_n (%n. X n * Y n)"
+by (simp add: star_mult_def Ifun2_of_def star_of_def Ifun_star_n)
 
 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-by (cases z, cases w, simp add: hypreal_mult mult_ac)
+by (rule mult_commute)
 
 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-by (cases z1, cases z2, cases z3, simp add: hypreal_mult mult_assoc)
+by (rule mult_assoc)
 
 lemma hypreal_mult_1: "(1::hypreal) * z = z"
-by (cases z, simp add: hypreal_one_def hypreal_mult)
+by (rule mult_1_left)
 
 lemma hypreal_add_mult_distrib:
      "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-by (cases z1, cases z2, cases w, simp add: hypreal_mult hypreal_add left_distrib)
+by (rule left_distrib)
 
 text{*one and zero are distinct*}
 lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
-by (simp add: hypreal_zero_def hypreal_one_def)
+by (rule zero_neq_one)
 
 
 subsection{*Multiplicative Inverse on @{typ hypreal} *}
-
+(*
 lemma hypreal_inverse_congruent: 
-  "(%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)}) respects hyprel"
+  "(%X. starrel``{%n. if X n = 0 then 0 else inverse(X n)}) respects starrel"
 by (auto simp add: congruent_def, ultra)
-
-lemma hypreal_inverse: 
-      "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
-       Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
-              UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
+*)
+lemma hypreal_inverse [unfolded star_n_def]: 
+      "inverse (star_n X) = star_n (%n. if X n = (0::real) then 0 else inverse(X n))"
+apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n)
+apply (rule_tac f=star_n in arg_cong)
+apply (rule ext)
+apply simp
+done
 
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
-apply (cases x)
-apply (simp add: hypreal_one_def hypreal_zero_def hypreal_inverse hypreal_mult)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
-done
+by (rule right_inverse)
 
 lemma hypreal_mult_inverse_left:
      "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
-by (simp add: hypreal_mult_inverse hypreal_mult_commute)
+by (rule left_inverse)
 
+(*
 instance hypreal :: field
 proof
   fix x y z :: hypreal
@@ -408,62 +411,57 @@
   show "inverse 0 = (0::hypreal)" 
     by (simp add: hypreal_inverse hypreal_zero_def)
 qed
-
+*)
 
 subsection{*Properties of The @{text "\<le>"} Relation*}
 
-lemma hypreal_le: 
-      "(Abs_hypreal(hyprel``{%n. X n}) \<le> Abs_hypreal(hyprel``{%n. Y n})) =  
+lemma hypreal_le [unfolded star_n_def]: 
+      "star_n X \<le> star_n Y =  
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (simp add: hypreal_le_def)
-apply (auto intro!: lemma_hyprel_refl, ultra)
-done
+by (simp add: star_le_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 
 lemma hypreal_le_refl: "w \<le> (w::hypreal)"
-by (cases w, simp add: hypreal_le)
+by (rule order_refl)
 
 lemma hypreal_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypreal)"
-by (cases i, cases j, cases k, simp add: hypreal_le, ultra)
+by (rule order_trans)
 
 lemma hypreal_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypreal)"
-by (cases z, cases w, simp add: hypreal_le, ultra)
+by (rule order_antisym)
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma hypreal_less_le: "((w::hypreal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: hypreal_less_def)
+by (rule order_less_le)
 
+(*
 instance hypreal :: order
   by intro_classes
     (assumption |
       rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym hypreal_less_le)+
-
+*)
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypreal_le_linear: "(z::hypreal) \<le> w | w \<le> z"
-apply (cases z, cases w)
-apply (auto simp add: hypreal_le, ultra)
-done
+by (rule linorder_linear)
 
+(*
 instance hypreal :: linorder 
   by intro_classes (rule hypreal_le_linear)
+*)
 
 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
 by (auto)
 
 lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_le hypreal_add) 
-done
+by (rule add_left_mono)
 
 lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypreal_zero_def hypreal_le hypreal_mult 
-                      linorder_not_le [symmetric], ultra) 
-done
+by (rule mult_strict_left_mono)
 
 
 subsection{*The Hyperreals Form an Ordered Field*}
 
+(*
 instance hypreal :: ordered_field
 proof
   fix x y z :: hypreal
@@ -474,6 +472,7 @@
   show "\<bar>x\<bar> = (if x < 0 then -x else x)"
     by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
 qed
+*)
 
 lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
 by auto
@@ -490,41 +489,37 @@
 
 lemma hypreal_of_real_add [simp]: 
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_minus [simp]:
      "hypreal_of_real (-r) = - hypreal_of_real  r"
-by (auto simp add: hypreal_of_real_def hypreal_minus)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_diff [simp]: 
      "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
-by (simp add: diff_minus) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_mult [simp]: 
      "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
-by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_one [simp]: "hypreal_of_real 1 = (1::hypreal)"
-by (simp add: hypreal_of_real_def hypreal_one_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_zero [simp]: "hypreal_of_real 0 = 0"
-by (simp add: hypreal_of_real_def hypreal_zero_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_le_iff [simp]: 
      "(hypreal_of_real w \<le> hypreal_of_real z) = (w \<le> z)"
-apply (simp add: hypreal_le_def hypreal_of_real_def, auto)
-apply (rule_tac [2] x = "%n. w" in exI, safe)
-apply (rule_tac [3] x = "%n. z" in exI, auto)
-apply (rule FreeUltrafilterNat_P, ultra)
-done
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_less_iff [simp]: 
      "(hypreal_of_real w < hypreal_of_real z) = (w < z)"
-by (simp add: linorder_not_le [symmetric]) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_eq_iff [simp]:
      "(hypreal_of_real w = hypreal_of_real z) = (w = z)"
-by (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
+by (simp add: hypreal_of_real_def)
 
 text{*As above, for 0*}
 
@@ -548,60 +543,45 @@
 
 lemma hypreal_of_real_inverse [simp]:
      "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
-apply (case_tac "r=0", simp)
-apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1])
-apply (auto simp add: hypreal_of_real_mult [symmetric])
-done
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_divide [simp]:
      "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
-by (simp add: hypreal_divide_def real_divide_def)
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
-by (induct n, simp_all) 
+by (simp add: hypreal_of_real_def)
 
 lemma hypreal_of_real_of_int [simp]:  "hypreal_of_real (of_int z) = of_int z"
-proof (cases z)
-  case (1 n)
-    thus ?thesis  by simp
-next
-  case (2 n)
-    thus ?thesis
-      by (simp only: of_int_minus hypreal_of_real_minus, simp)
-qed
+by (simp add: hypreal_of_real_def)
 
 
 subsection{*Misc Others*}
 
-lemma hypreal_less: 
-      "(Abs_hypreal(hyprel``{%n. X n}) < Abs_hypreal(hyprel``{%n. Y n})) =  
-       ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-by (auto simp add: hypreal_le linorder_not_le [symmetric], ultra+)
+lemma hypreal_less [unfolded star_n_def]: 
+      "star_n X < star_n Y = ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+by (simp add: star_less_def Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 
-lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
-by (simp add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_zero_num [unfolded star_n_def]: "0 = star_n (%n. 0)"
+by (simp add: star_zero_def star_of_def)
 
-lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})"
-by (simp add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
+lemma hypreal_one_num [unfolded star_n_def]: "1 = star_n (%n. 1)"
+by (simp add: star_one_def star_of_def)
 
 lemma hypreal_omega_gt_zero [simp]: "0 < omega"
-by (auto simp add: omega_def hypreal_less hypreal_zero_num)
-
-lemma hypreal_hrabs:
-     "abs (Abs_hypreal (hyprel `` {X})) = 
-      Abs_hypreal(hyprel `` {%n. abs (X n)})"
-apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
-apply ultra
-apply ultra
-apply arith
+apply (simp only: omega_def star_zero_def star_less_def star_of_def)
+apply (simp add: Ipred2_of_def star_of_def Ifun_star_n unstar_star_n)
 done
 
+lemma hypreal_hrabs [unfolded star_n_def]:
+     "abs (star_n X) = star_n (%n. abs (X n))"
+by (simp add: star_abs_def Ifun_of_def star_of_def Ifun_star_n)
 
 subsection{*Existence of Infinite Hyperreal Number*}
-
+(*
 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
 by (simp add: omega_def)
-
+*)
 text{*Existence of infinite number not corresponding to any real number.
 Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
 
@@ -618,6 +598,7 @@
 lemma not_ex_hypreal_of_real_eq_omega: 
       "~ (\<exists>x. hypreal_of_real x = omega)"
 apply (simp add: omega_def hypreal_of_real_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])
 done
@@ -638,36 +619,40 @@
 
 lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
 by (auto simp add: epsilon_def hypreal_of_real_def 
+                   star_of_def star_n_eq_iff
                    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)
 
 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
-by (simp add: epsilon_def hypreal_zero_def)
+by (simp add: epsilon_def star_zero_def star_of_def star_n_eq_iff
+         del: star_of_zero)
 
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
-by (simp add: hypreal_inverse omega_def epsilon_def)
+apply (simp add: epsilon_def omega_def star_inverse_def)
+apply (simp add: Ifun_of_def star_of_def Ifun_star_n)
+done
 
 
 ML
 {*
-val hrabs_def = thm "hrabs_def";
-val hypreal_hrabs = thm "hypreal_hrabs";
+(* val hrabs_def = thm "hrabs_def"; *)
+(* val hypreal_hrabs = thm "hypreal_hrabs"; *)
 
 val hypreal_zero_def = thm "hypreal_zero_def";
-val hypreal_one_def = thm "hypreal_one_def";
-val hypreal_minus_def = thm "hypreal_minus_def";
-val hypreal_diff_def = thm "hypreal_diff_def";
-val hypreal_inverse_def = thm "hypreal_inverse_def";
-val hypreal_divide_def = thm "hypreal_divide_def";
+(* val hypreal_one_def = thm "hypreal_one_def"; *)
+(* val hypreal_minus_def = thm "hypreal_minus_def"; *)
+(* val hypreal_diff_def = thm "hypreal_diff_def"; *)
+(* val hypreal_inverse_def = thm "hypreal_inverse_def"; *)
+(* val hypreal_divide_def = thm "hypreal_divide_def"; *)
 val hypreal_of_real_def = thm "hypreal_of_real_def";
 val omega_def = thm "omega_def";
 val epsilon_def = thm "epsilon_def";
-val hypreal_add_def = thm "hypreal_add_def";
-val hypreal_mult_def = thm "hypreal_mult_def";
-val hypreal_less_def = thm "hypreal_less_def";
-val hypreal_le_def = thm "hypreal_le_def";
+(* val hypreal_add_def = thm "hypreal_add_def"; *)
+(* val hypreal_mult_def = thm "hypreal_mult_def"; *)
+(* val hypreal_less_def = thm "hypreal_less_def"; *)
+(* val hypreal_le_def = thm "hypreal_le_def"; *)
 
 val finite_exhausts = thm "finite_exhausts";
 val finite_not_covers = thm "finite_not_covers";
@@ -689,15 +674,15 @@
 val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
 val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
 val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
-val hyprel_iff = thm "hyprel_iff";
-val hyprel_in_hypreal = thm "hyprel_in_hypreal";
-val Abs_hypreal_inverse = thm "Abs_hypreal_inverse";
-val lemma_hyprel_refl = thm "lemma_hyprel_refl";
+val starrel_iff = thm "starrel_iff";
+val starrel_in_hypreal = thm "starrel_in_hypreal";
+val Abs_star_inverse = thm "Abs_star_inverse";
+val lemma_starrel_refl = thm "lemma_starrel_refl";
 val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
 val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
 val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-val eq_Abs_hypreal = thm "eq_Abs_hypreal";
-val hypreal_minus_congruent = thm "hypreal_minus_congruent";
+val eq_Abs_star = thm "eq_Abs_star";
+(* val hypreal_minus_congruent = thm "hypreal_minus_congruent"; *)
 val hypreal_minus = thm "hypreal_minus";
 val hypreal_add = thm "hypreal_add";
 val hypreal_diff = thm "hypreal_diff";
@@ -712,7 +697,7 @@
 val hypreal_mult_assoc = thm "hypreal_mult_assoc";
 val hypreal_mult_1 = thm "hypreal_mult_1";
 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
-val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
+(* val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; *)
 val hypreal_inverse = thm "hypreal_inverse";
 val hypreal_mult_inverse = thm "hypreal_mult_inverse";
 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
@@ -741,7 +726,7 @@
 val hypreal_one_num = thm "hypreal_one_num";
 val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
 
-val Rep_hypreal_omega = thm"Rep_hypreal_omega";
+(* val Rep_hypreal_omega = thm"Rep_hypreal_omega"; *)
 val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
 val lemma_finite_omega_set = thm"lemma_finite_omega_set";
 val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";