# HG changeset patch
# User huffman
# Date 1126046930 -7200
# Node ID c6eecde058e48458fc8fa4a970f66ccfce229342
# Parent  ad73fb6144cf0b0f128cc83870559941eda67505
replace type hypnat with nat star

diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -127,7 +127,7 @@
   (* hypernatural powers of nonstandard complex numbers *)
   hcpow_def:
   "(z::hcomplex) hcpow (n::hypnat)
-      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_hypnat(n).
+      == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_star(n).
              hcomplexrel `` {%n. (X n) ^ (Y n)})"
 
 
@@ -817,7 +817,7 @@
 
 lemma hcpow:
   "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
-   Abs_hypnat(hypnatrel``{%n. Y n}) =
+   Abs_star(starrel``{%n. Y n}) =
    Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
 apply (simp add: hcpow_def)
 apply (rule_tac f = Abs_hcomplex in arg_cong)
@@ -826,12 +826,12 @@
 
 lemma hcomplex_of_hypreal_hyperpow:
      "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
-apply (rule_tac z=x in eq_Abs_star, cases n)
+apply (rule_tac z=x in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
 done
 
 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
-apply (cases x, cases n)
+apply (cases x, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
 done
 
@@ -882,18 +882,18 @@
 lemma hcpow_minus:
      "(-x::hcomplex) hcpow n =
       (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
-apply (cases x, cases n)
+apply (cases x, rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
 apply (auto simp add: neg_power_if, ultra)
 done
 
 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
-apply (cases r, cases s, cases n)
+apply (cases r, cases s, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
 done
 
 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
-apply (simp add: hcomplex_zero_def hypnat_one_def, cases n)
+apply (simp add: hcomplex_zero_def hypnat_one_def, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcpow hypnat_add)
 done
 
@@ -901,7 +901,7 @@
 by (simp add: hSuc_def)
 
 lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
-apply (cases r, cases n)
+apply (cases r, rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hcpow hcomplex_zero_def, ultra)
 done
 
@@ -1194,12 +1194,12 @@
 lemma hcis_hypreal_of_hypnat_Suc_mult:
      "hcis (hypreal_of_hypnat (n + 1) * a) =
       hcis a * hcis (hypreal_of_hypnat n * a)"
-apply (rule_tac z=a in eq_Abs_star, cases n)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
 done
 
 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
-apply (rule_tac z=a in eq_Abs_star, cases n)
+apply (rule_tac z=a in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
 done
 
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -14,7 +14,7 @@
 constdefs 
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    "sumhr p == 
-      (%(M,N,f). Abs_star(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
+      (%(M,N,f). Abs_star(\<Union>X \<in> Rep_star(M). \<Union>Y \<in> Rep_star(N).  
                              starrel ``{%n::nat. setsum f {X n..<Y n}})) p"
 
   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
@@ -28,8 +28,8 @@
 
 
 lemma sumhr: 
-     "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
-            Abs_hypnat(hypnatrel``{%n. N n}), f) =  
+     "sumhr(Abs_star(starrel``{%n. M n}),  
+            Abs_star(starrel``{%n. N n}), f) =  
       Abs_star(starrel `` {%n. setsum f {M n..<N n}})"
 apply (simp add: sumhr_def)
 apply (rule arg_cong [where f = Abs_star])
@@ -38,7 +38,7 @@
 
 text{*Base case in definition of @{term sumr}*}
 lemma sumhr_zero [simp]: "sumhr (m,0,f) = 0"
-apply (cases m)
+apply (rule_tac z=m in eq_Abs_star)
 apply (simp add: hypnat_zero_def sumhr symmetric hypreal_zero_def)
 done
 
@@ -46,43 +46,43 @@
 lemma sumhr_if: 
      "sumhr(m,n+1,f) = 
       (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *fNat* f) n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypnat_one_def sumhr hypnat_add hypnat_le starfunNat
            hypreal_add hypreal_zero_def,   ultra+)
 done
 
 lemma sumhr_Suc_zero [simp]: "sumhr (n + 1, n, f) = 0"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (simp add: hypnat_one_def sumhr hypnat_add hypreal_zero_def)
 done
 
 lemma sumhr_eq_bounds [simp]: "sumhr (n,n,f) = 0"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypreal_zero_def)
 done
 
 lemma sumhr_Suc [simp]: "sumhr (m,m + 1,f) = ( *fNat* f) m"
-apply (cases m)
+apply (rule_tac z=m in eq_Abs_star)
 apply (simp add: sumhr hypnat_one_def  hypnat_add starfunNat)
 done
 
 lemma sumhr_add_lbound_zero [simp]: "sumhr(m+k,k,f) = 0"
-apply (cases m, cases k)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=k in eq_Abs_star)
 apply (simp add: sumhr hypnat_add hypreal_zero_def)
 done
 
 lemma sumhr_add: "sumhr (m,n,f) + sumhr(m,n,g) = sumhr(m,n,%i. f i + g i)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypreal_add setsum_addf)
 done
 
 lemma sumhr_mult: "hypreal_of_real r * sumhr(m,n,f) = sumhr(m,n,%n. r * f n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypreal_of_real_def star_of_def star_n_def hypreal_mult setsum_mult)
 done
 
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
-apply (cases n, cases p)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=p in eq_Abs_star)
 apply (auto elim!: FreeUltrafilterNat_subset simp 
             add: hypnat_zero_def sumhr hypreal_add hypnat_less setsum_add_nat_ivl)
 done
@@ -91,7 +91,7 @@
 by (drule_tac f1 = f in sumhr_split_add [symmetric], simp)
 
 lemma sumhr_hrabs: "abs(sumhr(m,n,f)) \<le> sumhr(m,n,%i. abs(f i))"
-apply (cases n, cases m)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=m in eq_Abs_star)
 apply (simp add: sumhr hypreal_le hypreal_hrabs setsum_abs)
 done
 
@@ -105,26 +105,26 @@
 
 lemma sumhr_const:
      "sumhr(0, n, %i. r) = hypreal_of_hypnat n * hypreal_of_real r"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypnat_zero_def hypreal_of_real_def hypreal_of_hypnat 
                  star_of_def star_n_def
                  hypreal_mult real_of_nat_def)
 done
 
 lemma sumhr_less_bounds_zero [simp]: "n < m ==> sumhr(m,n,f) = 0"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (auto elim: FreeUltrafilterNat_subset 
             simp add: sumhr hypnat_less hypreal_zero_def)
 done
 
 lemma sumhr_minus: "sumhr(m, n, %i. - f i) = - sumhr(m, n, f)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypreal_minus setsum_negf)
 done
 
 lemma sumhr_shift_bounds:
      "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: sumhr hypnat_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
 done
 
@@ -156,7 +156,7 @@
              real_of_nat_def star_of_def star_n_def hypreal_mult cong: setsum_ivl_cong)
 
 lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
 apply (simp add: hypnat_zero_def starfunNat sumhr)
 done
 
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -266,10 +266,8 @@
 lemma coshr_zero [simp]: "coshr 0 = 1"
 apply (simp add: coshr_def sumhr_split_add
                    [OF hypnat_one_less_hypnat_omega, symmetric]) 
-apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def 
-         hypnat_add hypnat_omega_def st_add [symmetric] 
-         hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
-       del: hypnat_add_zero_left)
+apply (simp add: sumhr hypnat_zero_def hypnat_one_def hypnat_omega_def)
+apply (simp add: hypreal_one_def [symmetric] hypreal_zero_def [symmetric])
 done
 
 lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
@@ -301,6 +299,7 @@
 apply (rule st_hypreal_of_real [THEN subst])
 apply (rule approx_st_eq, auto)
 apply (rule approx_minus_iff [THEN iffD2])
+apply (simp only: mem_infmal_iff [symmetric])
 apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
 apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
 apply (insert exp_converges [of x]) 
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -11,6 +11,8 @@
 imports Star
 begin
 
+types hypnat = "nat star"
+(*
 constdefs
     hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
     "hypnatrel == {p. \<exists>X Y. p = ((X::nat=>nat),Y) &
@@ -20,20 +22,26 @@
     by (auto simp add: quotient_def)
 
 instance hypnat :: "{ord, zero, one, plus, times, minus}" ..
-
+*)
 consts whn :: hypnat
 
 
-defs (overloaded)
+defs
+  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
+  hypnat_omega_def:  "whn == Abs_star(starrel``{%n::nat. n})"
+
+lemma hypnat_zero_def:  "0 == Abs_star(starrel``{%n::nat. 0})"
+by (simp only: star_zero_def star_of_def star_n_def)
+
+lemma hypnat_one_def:   "1 == Abs_star(starrel``{%n::nat. 1})"
+by (simp only: star_one_def star_of_def star_n_def)
 
   (** hypernatural arithmetic **)
-
+(*
   hypnat_zero_def:  "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
   hypnat_one_def:   "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
-
-  (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
-  hypnat_omega_def:  "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
-
+*)
+(*
   hypnat_add_def:
   "P + Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
                 hypnatrel``{%n::nat. X n + Y n})"
@@ -45,15 +53,9 @@
   hypnat_minus_def:
   "P - Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
                 hypnatrel``{%n::nat. X n - Y n})"
-
-  hypnat_le_def:
-  "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) & Y \<in> Rep_hypnat(Q) &
-                            {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
+*)
 
-  hypnat_less_def: "(x < (y::hypnat)) == (x \<le> y & x \<noteq> y)"
-
-
-
+(*
 subsection{*Properties of @{term hypnatrel}*}
 
 text{*Proving that @{term hypnatrel} is an equivalence relation*}
@@ -78,8 +80,9 @@
 apply (simp add: equiv_def refl_def sym_def trans_def hypnatrel_refl)
 apply (blast intro: hypnatrel_sym hypnatrel_trans)
 done
-
+*)
 (* (hypnatrel `` {x} = hypnatrel `` {y}) = ((x,y) \<in> hypnatrel) *)
+(*
 lemmas equiv_hypnatrel_iff =
     eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
 
@@ -118,156 +121,124 @@
 theorem hypnat_cases [case_names Abs_hypnat, cases type: hypnat]:
     "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
 by (rule eq_Abs_hypnat [of z], blast)
-
+*)
 subsection{*Hypernat Addition*}
-
+(*
 lemma hypnat_add_congruent2:
      "(%X Y. hypnatrel``{%n. X n + Y n}) respects2 hypnatrel"
 by (simp add: congruent2_def, auto, ultra)
-
+*)
 lemma hypnat_add:
-  "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
-   Abs_hypnat(hypnatrel``{%n. X n + Y n})"
-by (simp add: hypnat_add_def 
-    UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_add_congruent2])
+  "Abs_star(starrel``{%n. X n}) + Abs_star(starrel``{%n. Y n}) =
+   Abs_star(starrel``{%n. X n + Y n})"
+by (rule hypreal_add)
 
 lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
-apply (cases z, cases w)
-apply (simp add: add_ac hypnat_add)
-done
+by (rule add_commute)
 
 lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypnat_add nat_add_assoc)
-done
+by (rule add_assoc)
 
 lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
-apply (cases z)
-apply (simp add: hypnat_zero_def hypnat_add)
-done
+by (rule comm_monoid_add_class.add_0)
 
+(*
 instance hypnat :: comm_monoid_add
   by intro_classes
     (assumption |
       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+
-
+*)
 
 subsection{*Subtraction inverse on @{typ hypreal}*}
 
-
+(*
 lemma hypnat_minus_congruent2:
-    "(%X Y. hypnatrel``{%n. X n - Y n}) respects2 hypnatrel"
+    "(%X Y. starrel``{%n. X n - Y n}) respects2 starrel"
 by (simp add: congruent2_def, auto, ultra)
-
+*)
 lemma hypnat_minus:
-  "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
-   Abs_hypnat(hypnatrel``{%n. X n - Y n})"
-by (simp add: hypnat_minus_def 
-  UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_minus_congruent2])
+  "Abs_star(starrel``{%n. X n}) - Abs_star(starrel``{%n. Y n}) =
+   Abs_star(starrel``{%n. X n - Y n})"
+by (rule hypreal_diff)
 
-lemma hypnat_minus_zero: "z - z = (0::hypnat)"
-apply (cases z)
-apply (simp add: hypnat_zero_def hypnat_minus)
-done
+lemma hypnat_minus_zero: "!!z. z - z = (0::hypnat)"
+by transfer (rule diff_self_eq_0)
 
-lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
-apply (cases n)
-apply (simp add: hypnat_minus hypnat_zero_def)
-done
+lemma hypnat_diff_0_eq_0: "!!n. (0::hypnat) - n = 0"
+by transfer (rule diff_0_eq_0)
 
 declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
 
-lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
-apply (cases m, cases n)
-apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
-done
+lemma hypnat_add_is_0: "!!m n. (m+n = (0::hypnat)) = (m=0 & n=0)"
+by transfer (rule add_is_0)
 
 declare hypnat_add_is_0 [iff]
 
-lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
-apply (cases i, cases j, cases k)
-apply (simp add: hypnat_minus hypnat_add diff_diff_left)
-done
+lemma hypnat_diff_diff_left: "!!i j k. (i::hypnat) - j - k = i - (j+k)"
+by transfer (rule diff_diff_left)
 
-lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
-by (simp add: hypnat_diff_diff_left hypnat_add_commute)
+lemma hypnat_diff_commute: "!!i j k. (i::hypnat) - j - k = i-k-j"
+by transfer (rule diff_commute)
 
-lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_inverse: "!!m n. ((n::hypnat) + m) - n = m"
+by transfer (rule diff_add_inverse)
 declare hypnat_diff_add_inverse [simp]
 
-lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_inverse2:  "!!m n. ((m::hypnat) + n) - n = m"
+by transfer (rule diff_add_inverse2)
 declare hypnat_diff_add_inverse2 [simp]
 
-lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
-apply (cases k, cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_cancel: "!!k m n. ((k::hypnat) + m) - (k+n) = m - n"
+by transfer (rule diff_cancel)
 declare hypnat_diff_cancel [simp]
 
-lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
-by (simp add: hypnat_add_commute [of _ k])
+lemma hypnat_diff_cancel2: "!!k m n. ((m::hypnat) + k) - (n+k) = m - n"
+by transfer (rule diff_cancel2)
 declare hypnat_diff_cancel2 [simp]
 
-lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
-apply (cases m, cases n)
-apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
-done
+lemma hypnat_diff_add_0: "!!m n. (n::hypnat) - (n+m) = (0::hypnat)"
+by transfer (rule diff_add_0)
 declare hypnat_diff_add_0 [simp]
 
 
 subsection{*Hyperreal Multiplication*}
-
+(*
 lemma hypnat_mult_congruent2:
-    "(%X Y. hypnatrel``{%n. X n * Y n}) respects2 hypnatrel"
+    "(%X Y. starrel``{%n. X n * Y n}) respects2 starrel"
 by (simp add: congruent2_def, auto, ultra)
-
+*)
 lemma hypnat_mult:
-  "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
-   Abs_hypnat(hypnatrel``{%n. X n * Y n})"
-by (simp add: hypnat_mult_def
-   UN_equiv_class2 [OF equiv_hypnatrel equiv_hypnatrel hypnat_mult_congruent2])
+  "Abs_star(starrel``{%n. X n}) * Abs_star(starrel``{%n. Y n}) =
+   Abs_star(starrel``{%n. X n * Y n})"
+by (rule hypreal_mult)
 
 lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
-by (cases z, cases w, simp add: hypnat_mult mult_ac)
+by (rule mult_commute)
 
 lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
-apply (cases z1, cases z2, cases z3)
-apply (simp add: hypnat_mult mult_assoc)
-done
+by (rule mult_assoc)
 
 lemma hypnat_mult_1: "(1::hypnat) * z = z"
-apply (cases z)
-apply (simp add: hypnat_mult hypnat_one_def)
-done
+by (rule mult_1_left)
 
-lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
-apply (cases k, cases m, cases n)
-apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
-done
+lemma hypnat_diff_mult_distrib: "!!k m n. ((m::hypnat) - n) * k = (m * k) - (n * k)"
+by transfer (rule diff_mult_distrib)
 
-lemma hypnat_diff_mult_distrib2: "(k::hypnat) * (m - n) = (k * m) - (k * n)"
-by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
+lemma hypnat_diff_mult_distrib2: "!!k m n. (k::hypnat) * (m - n) = (k * m) - (k * n)"
+by transfer (rule diff_mult_distrib2)
 
 lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
-apply (cases z1, cases z2, cases w)
-apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
-done
+by (rule left_distrib)
 
 lemma hypnat_add_mult_distrib2: "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)"
-by (simp add: hypnat_mult_commute [of w] hypnat_add_mult_distrib)
+by (rule right_distrib)
 
 text{*one and zero are distinct*}
 lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)"
-by (auto simp add: hypnat_zero_def hypnat_one_def)
+by (rule zero_neq_one)
 declare hypnat_zero_not_eq_one [THEN not_sym, simp]
 
-
+(*
 text{*The hypernaturals form a @{text comm_semiring_1_cancel}: *}
 instance hypnat :: comm_semiring_1_cancel
 proof
@@ -281,64 +252,50 @@
   hence "(k+i) - k = (k+j) - k" by simp
   thus "i=j" by simp
 qed
-
+*)
 
 subsection{*Properties of The @{text "\<le>"} Relation*}
 
 lemma hypnat_le:
-      "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
+      "(Abs_star(starrel``{%n. X n}) \<le> Abs_star(starrel``{%n. Y n})) =
        ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
-apply (simp add: hypnat_le_def)
-apply (auto intro!: lemma_hypnatrel_refl, ultra)
-done
+by (rule hypreal_le)
 
 lemma hypnat_le_refl: "w \<le> (w::hypnat)"
-apply (cases w)
-apply (simp add: hypnat_le)
-done
+by (rule order_refl)
 
 lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
-apply (cases i, cases j, cases k)
-apply (simp add: hypnat_le, ultra)
-done
+by (rule order_trans)
 
 lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
-apply (cases z, cases w)
-apply (simp add: hypnat_le, ultra)
-done
+by (rule order_antisym)
 
 (* Axiom 'order_less_le' of class 'order': *)
 lemma hypnat_less_le: "((w::hypnat) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: hypnat_less_def)
+by (rule order_less_le)
 
+(*
 instance hypnat :: order
   by intro_classes
     (assumption |
       rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
-
+*)
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
-apply (cases z, cases w)
-apply (auto simp add: hypnat_le, ultra)
-done
-
+by (rule linorder_linear)
+(*
 instance hypnat :: linorder
   by intro_classes (rule hypnat_le_linear)
-
+*)
 lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
-apply (cases x, cases y, cases z)
-apply (auto simp add: hypnat_le hypnat_add)
-done
+by (rule add_left_mono)
 
 lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
-apply (cases x, cases y, cases z)
-apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
-apply (auto simp add: hypnat_le, ultra)
-done
+by (rule mult_strict_left_mono)
 
 
 subsection{*The Hypernaturals Form an Ordered @{text comm_semiring_1_cancel} *}
-
+(*
 instance hypnat :: ordered_semidom
 proof
   fix x y z :: hypnat
@@ -350,62 +307,48 @@
   show "x < y ==> 0 < z ==> z * x < z * y"
     by (simp add: hypnat_mult_less_mono2)
 qed
-
-lemma hypnat_le_zero_cancel [iff]: "(n \<le> (0::hypnat)) = (n = 0)"
-apply (cases n)
-apply (simp add: hypnat_zero_def hypnat_le)
-done
+*)
+lemma hypnat_le_zero_cancel [iff]: "!!n. (n \<le> (0::hypnat)) = (n = 0)"
+by transfer (rule le_0_eq)
 
-lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
-apply (cases m, cases n)
-apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
-done
+lemma hypnat_mult_is_0 [simp]: "!!m n. (m*n = (0::hypnat)) = (m=0 | n=0)"
+by transfer (rule mult_is_0)
 
-lemma hypnat_diff_is_0_eq [simp]: "((m::hypnat) - n = 0) = (m \<le> n)"
-apply (cases m, cases n)
-apply (simp add: hypnat_le hypnat_minus hypnat_zero_def)
-done
+lemma hypnat_diff_is_0_eq [simp]: "!!m n. ((m::hypnat) - n = 0) = (m \<le> n)"
+by transfer (rule diff_is_0_eq)
 
 
 
 subsection{*Theorems for Ordering*}
 
 lemma hypnat_less:
-      "(Abs_hypnat(hypnatrel``{%n. X n}) < Abs_hypnat(hypnatrel``{%n. Y n})) =
+      "(Abs_star(starrel``{%n. X n}) < Abs_star(starrel``{%n. Y n})) =
        ({n. X n < Y n} \<in> FreeUltrafilterNat)"
-apply (auto simp add: hypnat_le  linorder_not_le [symmetric])
-apply (ultra+)
-done
+by (rule hypreal_less)
 
-lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
-apply (cases n)
-apply (auto simp add: hypnat_zero_def hypnat_less)
-done
+lemma hypnat_not_less0 [iff]: "!!n. ~ n < (0::hypnat)"
+by transfer (rule not_less0)
 
 lemma hypnat_less_one [iff]:
-      "(n < (1::hypnat)) = (n=0)"
-apply (cases n)
-apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
-done
+      "!!n. (n < (1::hypnat)) = (n=0)"
+by transfer (rule less_one)
+
+lemma hypnat_add_diff_inverse: "!!m n. ~ m<n ==> n+(m-n) = (m::hypnat)"
+by transfer (rule add_diff_inverse)
 
-lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
-apply (cases m, cases n)
-apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
-done
+lemma hypnat_le_add_diff_inverse [simp]: "!!m n. n \<le> m ==> n+(m-n) = (m::hypnat)"
+by transfer (rule le_add_diff_inverse)
 
-lemma hypnat_le_add_diff_inverse [simp]: "n \<le> m ==> n+(m-n) = (m::hypnat)"
-by (simp add: hypnat_add_diff_inverse linorder_not_less [symmetric])
-
-lemma hypnat_le_add_diff_inverse2 [simp]: "n\<le>m ==> (m-n)+n = (m::hypnat)"
-by (simp add: hypnat_le_add_diff_inverse hypnat_add_commute)
+lemma hypnat_le_add_diff_inverse2 [simp]: "!!m n. n\<le>m ==> (m-n)+n = (m::hypnat)"
+by transfer (rule le_add_diff_inverse2)
 
 declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]
 
-lemma hypnat_le0 [iff]: "(0::hypnat) \<le> n"
-by (simp add: linorder_not_less [symmetric])
+lemma hypnat_le0 [iff]: "!!n. (0::hypnat) \<le> n"
+by transfer (rule le0)
 
-lemma hypnat_add_self_le [simp]: "(x::hypnat) \<le> n + x"
-by (insert add_right_mono [of 0 n x], simp)
+lemma hypnat_add_self_le [simp]: "!!x n. (x::hypnat) \<le> n + x"
+by transfer (rule le_add2)
 
 lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
 by (insert add_strict_left_mono [OF zero_less_one], auto)
@@ -494,10 +437,10 @@
 
 subsection{*Existence of an infinite hypernatural number*}
 
-lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
+lemma hypnat_omega: "starrel``{%n::nat. n} \<in> star"
 by auto
 
-lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"
+lemma Rep_star_omega: "Rep_star(whn) \<in> star"
 by (simp add: hypnat_omega_def)
 
 text{*Existence of infinite number not corresponding to any natural number
@@ -530,7 +473,7 @@
 
 
 lemma hypnat_of_nat_eq:
-     "hypnat_of_nat m  = Abs_hypnat(hypnatrel``{%n::nat. m})"
+     "hypnat_of_nat m  = Abs_star(starrel``{%n::nat. m})"
 apply (induct m) 
 apply (simp_all add: hypnat_zero_def hypnat_one_def hypnat_add) 
 done
@@ -540,13 +483,7 @@
 
 lemma hypnat_omega_gt_SHNat:
      "n \<in> Nats ==> n < whn"
-apply (auto simp add: hypnat_of_nat_eq hypnat_less_def hypnat_le_def
-                      hypnat_omega_def SHNat_eq)
- prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
-apply (auto intro!: exI)
-apply (rule cofinite_mem_FreeUltrafilterNat)
-apply (simp add: Compl_Collect_le finite_nat_segment) 
-done
+by (auto simp add: hypnat_of_nat_eq hypnat_less hypnat_omega_def SHNat_eq)
 
 (* Infinite hypernatural not in embedded Nats *)
 lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
@@ -595,7 +532,7 @@
 
 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 z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto elim: HNatInfinite_FreeUltrafilterNat_lemma 
             simp add: hypnat_less FreeUltrafilterNat_Compl_iff1 
                       Collect_neg_eq [symmetric])
@@ -607,24 +544,24 @@
 
 lemma HNatInfinite_FreeUltrafilterNat:
      "x \<in> HNatInfinite 
-      ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
-apply (cases x)
+      ==> \<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
+apply (rule bexI [OF _ lemma_starrel_refl], clarify) 
 apply (auto simp add: hypnat_of_nat_def hypnat_less)
 done
 
 lemma FreeUltrafilterNat_HNatInfinite:
-     "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
+     "\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
       ==> x \<in> HNatInfinite"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_eq hypnat_of_nat_eq)
 apply (drule spec, ultra, auto) 
 done
 
 lemma HNatInfinite_FreeUltrafilterNat_iff:
      "(x \<in> HNatInfinite) = 
-      (\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
+      (\<exists>X \<in> Rep_star x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
 by (blast intro: HNatInfinite_FreeUltrafilterNat 
                  FreeUltrafilterNat_HNatInfinite)
 
@@ -692,7 +629,7 @@
 constdefs
   hypreal_of_hypnat :: "hypnat => hypreal"
    "hypreal_of_hypnat N  == 
-      Abs_star(\<Union>X \<in> Rep_hypnat(N). starrel``{%n::nat. real (X n)})"
+      Abs_star(\<Union>X \<in> Rep_star(N). starrel``{%n::nat. real (X n)})"
 
 
 lemma HNat_hypreal_of_nat [simp]: "hypreal_of_nat N \<in> Nats"
@@ -704,7 +641,7 @@
 by force
 
 lemma hypreal_of_hypnat:
-      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
+      "hypreal_of_hypnat (Abs_star(starrel``{%n. X n})) =
        Abs_star(starrel `` {%n. real (X n)})"
 apply (simp add: hypreal_of_hypnat_def)
 apply (rule_tac f = Abs_star in arg_cong)
@@ -714,7 +651,7 @@
 
 lemma hypreal_of_hypnat_inject [simp]:
      "(hypreal_of_hypnat m = hypreal_of_hypnat n) = (m=n)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypreal_of_hypnat)
 done
 
@@ -726,19 +663,19 @@
 
 lemma hypreal_of_hypnat_add [simp]:
      "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
 done
 
 lemma hypreal_of_hypnat_mult [simp]:
      "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
 done
 
 lemma hypreal_of_hypnat_less_iff [simp]:
      "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
-apply (cases m, cases n)
+apply (rule_tac z=m in eq_Abs_star, rule_tac z=n in eq_Abs_star)
 apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
 done
 
@@ -747,13 +684,13 @@
 declare hypreal_of_hypnat_eq_zero_iff [simp]
 
 lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
 done
 
 lemma HNatInfinite_inverse_Infinitesimal [simp]:
      "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypreal_of_hypnat hypreal_inverse 
       HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
 apply (rule bexI, rule_tac [2] lemma_starrel_refl, auto)
@@ -776,17 +713,17 @@
 val hypnat_one_def = thm"hypnat_one_def";
 val hypnat_omega_def = thm"hypnat_omega_def";
 
-val hypnatrel_iff = thm "hypnatrel_iff";
-val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
-val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
-val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
-val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
-val eq_Abs_hypnat = thm "eq_Abs_hypnat";
+val starrel_iff = thm "starrel_iff";
+(* val starrel_in_hypnat = thm "starrel_in_hypnat"; *)
+val lemma_starrel_refl = thm "lemma_starrel_refl";
+(* val hypnat_empty_not_mem = thm "hypnat_empty_not_mem"; *)
+(* val Rep_star_nonempty = thm "Rep_star_nonempty"; *)
+val eq_Abs_star = thm "eq_Abs_star";
 val hypnat_add = thm "hypnat_add";
 val hypnat_add_commute = thm "hypnat_add_commute";
 val hypnat_add_assoc = thm "hypnat_add_assoc";
 val hypnat_add_zero_left = thm "hypnat_add_zero_left";
-val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2";
+(* val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2"; *)
 val hypnat_minus = thm "hypnat_minus";
 val hypnat_minus_zero = thm "hypnat_minus_zero";
 val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
@@ -798,7 +735,7 @@
 val hypnat_diff_cancel = thm "hypnat_diff_cancel";
 val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
 val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
-val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2";
+(* val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2"; *)
 val hypnat_mult = thm "hypnat_mult";
 val hypnat_mult_commute = thm "hypnat_mult_commute";
 val hypnat_mult_assoc = thm "hypnat_mult_assoc";
@@ -841,7 +778,7 @@
 val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
 val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
 val hypnat_omega = thm "hypnat_omega";
-val Rep_hypnat_omega = thm "Rep_hypnat_omega";
+val Rep_star_omega = thm "Rep_star_omega";
 val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
 val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
 val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -41,7 +41,7 @@
   (* hypernatural powers of hyperreals *)
   hyperpow_def:
   "(R::hypreal) pow (N::hypnat) ==
-      Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_hypnat(N).
+      Abs_star(\<Union>X \<in> Rep_star(R). \<Union>Y \<in> Rep_star(N).
                         starrel``{%n::nat. (X n) ^ (Y n)})"
 
 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
@@ -125,7 +125,7 @@
 by (auto simp add: congruent_def intro!: ext, fuf+)
 
 lemma hyperpow:
-  "Abs_star(starrel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
+  "Abs_star(starrel``{%n. X n}) pow Abs_star(starrel``{%n. Y n}) =
    Abs_star(starrel``{%n. X n ^ Y n})"
 apply (unfold hyperpow_def)
 apply (rule_tac f = Abs_star in arg_cong)
@@ -137,33 +137,33 @@
 lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
 apply (unfold hypnat_one_def)
 apply (simp (no_asm) add: hypreal_zero_def)
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
 apply (auto simp add: hyperpow hypnat_add)
 done
 declare hyperpow_zero [simp]
 
 lemma hyperpow_not_zero [rule_format (no_asm)]:
      "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow)
 apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma hyperpow_inverse:
      "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
-apply (simp (no_asm) add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp (no_asm) add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
 apply (rule FreeUltrafilterNat_subset)
 apply (auto dest: realpow_not_zero intro: power_inverse)
 done
 
 lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
-apply (cases n, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
 done
 
 lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
-apply (cases n, cases m, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=m in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 done
 
@@ -179,38 +179,38 @@
 done
 
 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
                    simp add: hyperpow hypreal_less hypreal_le)
 done
 
 lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=r in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
             simp add: hyperpow hypreal_le)
 done
 
 lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
-apply (simp add: hypreal_zero_def, cases n, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
+apply (simp add: hypreal_zero_def, rule_tac z=n in eq_Abs_star, rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_le hypreal_less)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 apply (auto intro: power_mono)
 done
 
 lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypreal_one_def hyperpow)
 done
 
 lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)"
 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 apply simp
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 done
 
 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (cases n, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 done
 
@@ -247,14 +247,14 @@
      "-1 pow ((1 + 1)*n) = (1::hypreal)"
 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
 apply simp
-apply (simp only: hypreal_one_def, cases n)
+apply (simp only: hypreal_one_def, rule_tac z=n in eq_Abs_star)
 apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
-                      left_distrib)
+                      hypnat_mult left_distrib)
 done
 
 lemma hyperpow_less_le:
      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (cases n, cases N, rule_tac z=r in eq_Abs_star)
+apply (rule_tac z=n in eq_Abs_star, rule_tac z=N in eq_Abs_star, rule_tac z=r in eq_Abs_star)
 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
             hypreal_zero_def hypreal_one_def)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -20,11 +20,11 @@
 
     starsetNat :: "nat set => hypnat set"          ("*sNat* _" [80] 80)
     "*sNat* A ==
-       {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
+       {x. \<forall>X\<in>Rep_star(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}"
 
    starsetNat_n :: "(nat => nat set) => hypnat set"      ("*sNatn* _" [80] 80)
     "*sNatn* As ==
-       {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
+       {x. \<forall>X\<in>Rep_star(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}"
 
    InternalNatSets :: "hypnat set set"
     "InternalNatSets == {X. \<exists>As. X = *sNatn* As}"
@@ -33,12 +33,12 @@
 
     starfunNat :: "(nat => real) => hypnat => hypreal"
                   ("*fNat* _" [80] 80)
-    "*fNat* f  == (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. f (X n)}))"
+    "*fNat* f  == (%x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. f (X n)}))"
 
    starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal"
                    ("*fNatn* _" [80] 80)
     "*fNatn* F ==
-      (%x. Abs_star(\<Union>X\<in>Rep_hypnat(x). starrel``{%n. (F n)(X n)}))"
+      (%x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. (F n)(X n)}))"
 
    InternalNatFuns :: "(hypnat => hypreal) set"
     "InternalNatFuns == {X. \<exists>F. X = *fNatn* F}"
@@ -47,12 +47,12 @@
 
    starfunNat2 :: "(nat => nat) => hypnat => hypnat"
                    ("*fNat2* _" [80] 80)
-    "*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})"
+    "*fNat2* f == %x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. f (X n)})"
 
    starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat"
                      ("*fNat2n* _" [80] 80)
     "*fNat2n* F == 
-        %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})"
+        %x. Abs_star(\<Union>X\<in>Rep_star(x). starrel``{%n. (F n)(X n)})"
 
    InternalNatFuns2 :: "(hypnat => hypnat) set"
     "InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}"
@@ -70,13 +70,13 @@
  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
 apply (drule FreeUltrafilterNat_Compl_mem)
 apply (drule bspec, assumption)
-apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra)
+apply (rule_tac z = x in eq_Abs_star, auto, ultra)
 done
 
 lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B"
 apply (auto simp add: starsetNat_n_def)
 apply (drule_tac x = Xa in bspec)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_star)
 apply (auto dest!: bspec, ultra+)
 done
 
@@ -104,15 +104,15 @@
 
 lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)"
 apply (auto simp add: starsetNat_def)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac [2] z = x in eq_Abs_star)
 apply (auto dest!: bspec, ultra+)
 done
 
 lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)"
 apply (auto simp add: starsetNat_n_def)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac [2] z = x in eq_Abs_star)
 apply (auto dest!: bspec, ultra+)
 done
 
@@ -121,8 +121,8 @@
 
 lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"
 apply (auto simp add: starsetNat_n_def)
-apply (rule_tac [2] z = x in eq_Abs_hypnat)
-apply (rule_tac [3] z = x in eq_Abs_hypnat)
+apply (rule_tac [2] z = x in eq_Abs_star)
+apply (rule_tac [3] z = x in eq_Abs_star)
 apply (auto dest!: bspec, ultra+)
 done
 
@@ -154,7 +154,7 @@
 apply (simp add: hypnat_of_nat_eq [symmetric])
 apply (rule imageI, rule ccontr)
 apply (drule bspec)
-apply (rule lemma_hypnatrel_refl)
+apply (rule lemma_starrel_refl)
 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
 done
 
@@ -186,14 +186,14 @@
 lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f"
 by (simp add: starfunNat2_n_def starfunNat2_def)
 
-lemma starfunNat_congruent: "(%X. hypnatrel``{%n. f (X n)}) respects hypnatrel"
+lemma starfunNat_congruent: "(%X. starrel``{%n. f (X n)}) respects starrel"
 apply (simp add: congruent_def, safe)
 apply (ultra+)
 done
 
 (* f::nat=>real *)
 lemma starfunNat:
-      "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+      "( *fNat* f) (Abs_star(starrel``{%n. X n})) =
        Abs_star(starrel `` {%n. f (X n)})"
 apply (simp add: starfunNat_def)
 apply (rule arg_cong [where f = Abs_star])
@@ -202,25 +202,25 @@
 
 (* f::nat=>nat *)
 lemma starfunNat2:
-      "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
-       Abs_hypnat(hypnatrel `` {%n. f (X n)})"
+      "( *fNat2* f) (Abs_star(starrel``{%n. X n})) =
+       Abs_star(starrel `` {%n. f (X n)})"
 apply (simp add: starfunNat2_def)
-apply (rule arg_cong [where f = Abs_hypnat])
-apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse]
-         UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent])
+apply (rule arg_cong [where f = Abs_star])
+apply (simp add: starrel_in_hypreal [THEN Abs_star_inverse]
+         UN_equiv_class [OF equiv_starrel starfunNat_congruent])
 done
 
 subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*}
 
 lemma starfunNat_mult:
      "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat hypreal_mult)
 done
 
 lemma starfunNat2_mult:
      "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat2 hypnat_mult)
 done
 
@@ -228,19 +228,19 @@
 
 lemma starfunNat_add:
      "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat hypreal_add)
 done
 
 lemma starfunNat2_add:
      "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat2 hypnat_add)
 done
 
 lemma starfunNat2_minus:
      "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat2 hypnat_minus)
 done
 
@@ -251,7 +251,7 @@
 lemma starfunNatNat2_o:
      "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (simp add: starfunNat2 starfunNat)
 done
 
@@ -264,7 +264,7 @@
 (***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****)
 lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (simp add: starfunNat2)
 done
 
@@ -272,7 +272,7 @@
 
 lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (simp add: starfunNat starfun)
 done
 
@@ -286,23 +286,23 @@
 text{*NS extension of constant function*}
 
 lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat  k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat2 hypnat_of_nat_eq)
 done
 
 lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfunNat hypreal_minus)
 done
 
 lemma starfunNat_inverse:
      "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfunNat hypreal_inverse)
 done
 
@@ -330,7 +330,7 @@
      "\<forall>n. N \<le> n --> f n \<le> g n
       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n"
 apply safe
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
 done
 
@@ -339,7 +339,7 @@
      "\<forall>n. N \<le> n --> f n < g n
       ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n"
 apply safe
-apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_star)
 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto)
 done
 
@@ -347,27 +347,27 @@
 
 lemma starfunNat_shift_one:
      "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
 apply (simp add: starfunNat hypnat_one_def hypnat_add)
 done
 
 text{*Nonstandard extension with absolute value*}
 
 lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
 apply (simp add: starfunNat hypreal_hrabs)
 done
 
 text{*The hyperpow function as a nonstandard extension of realpow*}
 
 lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
 apply (simp add: hyperpow hypreal_of_real_def star_of_def star_n_def starfunNat)
 done
 
 lemma starfunNat_pow2:
      "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"
-apply (cases N)
+apply (rule_tac z=N in eq_Abs_star)
 apply (simp add: hyperpow hypnat_of_nat_eq starfunNat)
 done
 
@@ -381,7 +381,7 @@
 
 lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat"
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (simp add: hypreal_of_hypnat starfunNat)
 done
 
@@ -396,11 +396,11 @@
 text{*Internal functions - some redundancy with *fNat* now*}
 
 lemma starfunNat_n_congruent:
-      "(%X. hypnatrel``{%n. f n (X n)}) respects hypnatrel"
+      "(%X. starrel``{%n. f n (X n)}) respects starrel"
 by (auto simp add: congruent_def, ultra+)
 
 lemma starfunNat_n:
-     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) =
+     "( *fNatn* f) (Abs_star(starrel``{%n. X n})) =
       Abs_star(starrel `` {%n. f n (X n)})"
 apply (simp add: starfunNat_n_def)
 apply (rule_tac f = Abs_star in arg_cong, auto, ultra)
@@ -410,7 +410,7 @@
 
 lemma starfunNat_n_mult:
      "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat_n hypreal_mult)
 done
 
@@ -418,7 +418,7 @@
 
 lemma starfunNat_n_add:
      "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat_n hypreal_add)
 done
 
@@ -426,7 +426,7 @@
 
 lemma starfunNat_n_add_minus:
      "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat_n hypreal_minus hypreal_add)
 done
 
@@ -435,12 +435,12 @@
 
 lemma starfunNat_n_const_fun [simp]:
      "( *fNatn* (%i x. k)) z = hypreal_of_real  k"
-apply (cases z)
+apply (rule_tac z=z in eq_Abs_star)
 apply (simp add: starfunNat_n hypreal_of_real_def star_of_def star_n_def)
 done
 
 lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"
-apply (cases x)
+apply (rule_tac z=x in eq_Abs_star)
 apply (simp add: starfunNat_n hypreal_minus)
 done
 
@@ -539,13 +539,13 @@
 constdefs
 
   starPNat :: "(nat => bool) => hypnat => bool"  ("*pNat* _" [80] 80)
-  "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
+  "*pNat* P == (%x. \<exists>X. (X \<in> Rep_star(x) &
                       {n. P(X n)} \<in> FreeUltrafilterNat))"
 
 
   starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
                ("*pNat2* _" [80] 80)
-  "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
+  "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_star(x) & Y \<in> Rep_star(y) &
                       {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
 
   hSuc :: "hypnat => hypnat"
@@ -553,7 +553,7 @@
 
 
 lemma starPNat:
-     "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
+     "(( *pNat* P) (Abs_star(starrel``{%n. X n}))) =
       ({n. P (X n)} \<in> FreeUltrafilterNat)"
 by (auto simp add: starPNat_def, ultra)
 
@@ -564,7 +564,7 @@
     "(( *pNat* P) 0 &
             (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
        --> ( *pNat* P)(n)"
-apply (cases n)
+apply (rule_tac z=n in eq_Abs_star)
 apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
 apply (erule nat_induct)
 apply (drule_tac x = "hypnat_of_nat n" in spec)
@@ -579,8 +579,8 @@
 by (insert hypnat_induct_obj [of P n], auto)
 
 lemma starPNat2:
-"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
-             (Abs_hypnat(hypnatrel``{%n. Y n}))) =
+"(( *pNat2* P) (Abs_star(starrel``{%n. X n}))
+             (Abs_star(starrel``{%n. Y n}))) =
       ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
 by (auto simp add: starPNat2_def, ultra)
 
@@ -588,17 +588,17 @@
 apply (simp add: starPNat2_def)
 apply (rule ext)
 apply (rule ext)
-apply (rule_tac z = x in eq_Abs_hypnat)
-apply (rule_tac z = y in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
 apply (auto, ultra)
 done
 
 lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
 by (simp add: starPNat2_eq_iff)
 
-lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
+lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_star(starrel `` {x})))"
 apply auto
-apply (rule_tac z = h in eq_Abs_hypnat, auto)
+apply (rule_tac z = h in eq_Abs_star, auto)
 done
 
 lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
@@ -615,7 +615,7 @@
 lemma nonempty_InternalNatSet_has_least:
     "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
 apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
-apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_star)
 apply (auto dest!: bspec simp add: hypnat_le)
 apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
 apply (ultra, force dest: nonempty_nat_set_Least_mem)
diff -r ad73fb6144cf -r c6eecde058e4 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Tue Sep 06 23:16:48 2005 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Sep 07 00:48:50 2005 +0200
@@ -92,7 +92,7 @@
       "X ----> L ==> X ----NS> L"
 apply (simp add: LIMSEQ_def NSLIMSEQ_def)
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_star)
 apply (rule approx_minus_iff [THEN iffD2])
 apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def
               star_of_def star_n_def
@@ -145,9 +145,9 @@
 
 text{* thus, the sequence defines an infinite hypernatural! *}
 lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n
-          ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite"
+          ==> Abs_star (starrel `` {f}) : HNatInfinite"
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
 apply (erule FreeUltrafilterNat_NSLIMSEQ)
 done
 
@@ -161,7 +161,7 @@
 by auto
 
 lemma lemmaLIM3: "[| 0 < r; \<forall>n. r \<le> \<bar>X (f n) + - L\<bar>;
-           ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) +
+           ( *fNat* X) (Abs_star (starrel `` {f})) +
            - hypreal_of_real  L \<approx> 0 |] ==> False"
 apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
 apply (rename_tac "Y")
@@ -179,7 +179,7 @@
 apply (rule ccontr, simp, safe)
 txt{* skolemization step *}
 apply (drule choice, safe)
-apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec)
+apply (drule_tac x = "Abs_star (starrel``{f}) " in bspec)
 apply (drule_tac [2] approx_minus_iff [THEN iffD1])
 apply (simp_all add: linorder_not_less)
 apply (blast intro: HNatInfinite_NSLIMSEQ)
@@ -504,7 +504,7 @@
 
 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
 apply (simp add: Bseq_def NSBseq_def, safe)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_star)
 apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff 
                       HNatInfinite_FreeUltrafilterNat_iff)
 apply (rule bexI [OF _ lemma_starrel_refl]) 
@@ -567,9 +567,9 @@
 
 lemma HNatInfinite_skolem_f:
      "\<forall>N. real(Suc N) < \<bar>X (f N)\<bar>
-      ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite"
+      ==> Abs_star(starrel``{f}) : HNatInfinite"
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule bexI [OF _ lemma_hypnatrel_refl], safe)
+apply (rule bexI [OF _ lemma_starrel_refl], safe)
 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
 apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
 apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} =
@@ -762,7 +762,7 @@
 subsubsection{*Standard Implies Nonstandard*}
 
 lemma lemmaCauchy1:
-     "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite
+     "Abs_star (starrel `` {x}) : HNatInfinite
       ==> {n. M \<le> x n} : FreeUltrafilterNat"
 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
 apply (drule_tac x = M in spec, ultra)
@@ -776,8 +776,8 @@
 
 lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X"
 apply (simp add: Cauchy_def NSCauchy_def, safe)
-apply (rule_tac z = M in eq_Abs_hypnat)
-apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = M in eq_Abs_star)
+apply (rule_tac z = N in eq_Abs_star)
 apply (rule approx_minus_iff [THEN iffD2])
 apply (rule mem_infmal_iff [THEN iffD1])
 apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff)
@@ -797,7 +797,7 @@
 apply (rule ccontr, simp)
 apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib)  
 apply (drule bspec, assumption)
-apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); 
+apply (drule_tac x = "Abs_star (starrel `` {fa}) " in bspec); 
 apply (auto simp add: starfunNat)
 apply (drule approx_minus_iff [THEN iffD1])
 apply (drule mem_infmal_iff [THEN iffD2])