# HG changeset patch
# User paulson
# Date 1075721026 -3600
# Node ID c78c7da09519b882251502e5c8941faa2a7ecc8a
# Parent  b0064703967b2d837ee1133ef4dfcda5aec4825f
Conversion of HyperNat to Isar format and its declaration as a semiring

diff -r b0064703967b -r c78c7da09519 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -6,33 +6,6 @@
 
 theory NSComplex = NSInduct:
 
-(* ???MOVE to one of the hyperreal theories: HRealAbs??? *)
-lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
-apply (induct_tac "m")
-apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
-done
-
-lemma hypreal_of_nat_le_iff:
-      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
-apply (auto simp add: linorder_not_less [symmetric])
-done
-declare hypreal_of_nat_le_iff [simp]
-
-lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
-apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
-         del: hypreal_of_nat_zero)
-done
-declare hypreal_of_nat_ge_zero [simp]
-
-declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
-
-lemma hypreal_of_hypnat_ge_zero: "0 \<le> hypreal_of_hypnat n"
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
-done
-declare hypreal_of_hypnat_ge_zero [simp]
-declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
-
 constdefs
     hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
     "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
@@ -819,13 +792,13 @@
 
 lemma hcmod_hcomplex_of_hypreal_of_nat:
      "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
-apply auto
+apply (simp add: abs_if linorder_not_less) 
 done
 declare hcmod_hcomplex_of_hypreal_of_nat [simp]
 
 lemma hcmod_hcomplex_of_hypreal_of_hypnat:
      "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
-apply auto
+apply (simp add: abs_if linorder_not_less) 
 done
 declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
 
@@ -846,8 +819,8 @@
 done
 declare hcmod_ge_zero [simp]
 
-lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x"
-apply (auto intro: hrabs_eqI1)
+lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x" 
+apply (simp add: abs_if linorder_not_less) 
 done
 declare hrabs_hcmod_cancel [simp]
 
@@ -1817,9 +1790,7 @@
 val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
 val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
 val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
-val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
-val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
-val hypreal_of_hypnat_ge_zero = thm"hypreal_of_hypnat_ge_zero";
+
 val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
 val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
 val hcmod_minus = thm"hcmod_minus";
@@ -1909,7 +1880,6 @@
 val hrcis_zero_arg = thm"hrcis_zero_arg";
 val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
 val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
-val hypreal_of_nat = thm"hypreal_of_nat";
 val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
 val NSDeMoivre = thm"NSDeMoivre";
 val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
diff -r b0064703967b -r c78c7da09519 src/HOL/Complex/NSInduct.ML
--- a/src/HOL/Complex/NSInduct.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Complex/NSInduct.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -67,23 +67,6 @@
 by (Auto_tac);
 val lemma_hyp = result();
 
-Goal "(EX (v::nat=>nat). ALL (x::nat). P (g v) (f x)) = \
-\     (EX (v::nat=>nat). ALL x. EX f': Rep_hypnat(f x). P (g v) (Abs_hypnat(hypnatrel `` {f'})))"; 
-by (Auto_tac);
-by (ALLGOALS(res_inst_tac [("x","v")] exI));
-by (Step_tac 1);
-by (ALLGOALS(res_inst_tac [("z","f x")] eq_Abs_hypnat));
-by (Auto_tac);
-by (rtac bexI 1);
-by (dres_inst_tac [("x","x")] spec 3);
-by (dtac sym 1);
-by (Auto_tac);
-by (subgoal_tac 
-    "Abs_hypnat (hypnatrel `` {X}) = Abs_hypnat (hypnatrel `` {Y})" 1);
-by (Asm_simp_tac 1);
-by (Auto_tac);
-val lemma_hyp2 = result();
-
 Goalw [hSuc_def] "hSuc m ~= 0";
 by Auto_tac;
 qed "hSuc_not_zero";
@@ -99,12 +82,6 @@
 
 AddIffs [hSuc_not_zero,zero_not_hSuc,hSuc_hSuc_eq];
 
-Goalw [hypnat_le_def] "m <= (n::hypnat) | n <= m";
-by (auto_tac (claset() addDs [hypnat_less_trans],simpset()));
-qed "hypnat_le_linear";
-
-val hypnat_less_le = hypnat_less_imp_le;
-
 Goal "c : (S :: nat set) ==> (LEAST n. n : S) : S";
 by (etac LeastI 1);
 qed "nonempty_nat_set_Least_mem";
@@ -132,7 +109,8 @@
 by (dres_inst_tac [("x","n - 1")] bspec 1);
 by (Step_tac 1);
 by (dres_inst_tac [("x","n - 1")] spec 1);
-by (dres_inst_tac [("x","1"),("q1.0","n")] hypnat_add_le_mono1 2);
-by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
+by (dres_inst_tac [("c","1"),("a","n")] add_right_mono 2); 
+by (auto_tac ((claset(),simpset() addsimps [linorder_not_less RS sym])
+        delIffs [hypnat_neq0_conv]));
 qed "internal_induct";
 
diff -r b0064703967b -r c78c7da09519 src/HOL/Complex/ex/NSPrimes.ML
--- a/src/HOL/Complex/ex/NSPrimes.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Complex/ex/NSPrimes.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -74,7 +74,7 @@
 
 Goal "(hypnat_of_nat n <= 0) = (n = 0)";
 by (stac (hypnat_of_nat_zero RS sym) 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_le_iff RS sym]));
+by Auto_tac;
 qed "hypnat_of_nat_le_zero_iff";
 Addsimps [hypnat_of_nat_le_zero_iff];
 
@@ -107,8 +107,8 @@
 by Auto_tac;
 by (rtac exI 1 THEN Auto_tac);
 by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [symmetric hypnat_le_def,
-    hypnat_of_nat_zero_iff]));
+by (auto_tac (claset(),
+     simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
 qed "hypnat_dvd_all_hypnat_of_nat";
 
 
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HLog.ML
--- a/src/HOL/Hyperreal/HLog.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HLog.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -42,8 +42,8 @@
      "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) = \
 \     (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))";
 by (case_tac "Abs_hypreal (hyprel `` {Y}) = 0" 1);
-by (auto_tac (claset(),simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,
-    hypreal_zero_num,hypreal_inverse,hypreal_mult]));
+by (auto_tac (claset(),
+  simpset() addsimps [hypreal_zero_num,hypreal_inverse,hypreal_mult]));
 by (ALLGOALS(ultra_tac (claset(),simpset() addsimps [real_divide_def])));
 qed "hypreal_divide";
 
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HRealAbs.thy
--- a/src/HOL/Hyperreal/HRealAbs.thy	Thu Jan 29 16:51:17 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,149 +0,0 @@
-(*  Title       : HRealAbs.thy
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Description : Absolute value function for the hyperreals
-*) 
-
-theory HRealAbs = HyperArith:
-
-constdefs
-
-  hypreal_of_nat :: "nat => hypreal"
-  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
-
-
-lemma hrabs_number_of [simp]:
-     "abs (number_of v :: hypreal) =
-        (if neg (number_of v) then number_of (bin_minus v)
-         else number_of v)"
-by (simp add: hrabs_def)
-
-
-(*------------------------------------------------------------
-   Properties of the absolute value function over the reals
-   (adapted version of previously proved theorems about abs)
- ------------------------------------------------------------*)
-
-lemma hrabs_eqI1: "(0::hypreal)<=x ==> abs x = x"
-by (simp add: hrabs_def)
-
-lemma hrabs_eqI2: "(0::hypreal)<x ==> abs x = x"
-by (simp add: order_less_imp_le hrabs_eqI1)
-
-lemma hrabs_minus_eqI2: "x<(0::hypreal) ==> abs x = -x"
-by (simp add: linorder_not_less [symmetric] hrabs_def)
-
-lemma hrabs_minus_eqI1: "x<=(0::hypreal) ==> abs x = -x"
-by (auto dest: order_antisym simp add: hrabs_def)
-
-declare abs_mult [simp]
-
-lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
-apply (unfold hrabs_def)
-apply (simp split add: split_if_asm)
-done
-
-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"
-by (simp add: hrabs_def)
-
-lemma hrabs_eq_disj: "abs x = (y::hypreal) ==> x = y | -x = y"
-by (simp add: hrabs_def split add: split_if_asm)
-
-(* Needed in Geom.ML *)
-lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
-by (simp add: hrabs_def split add: split_if_asm)
-
-(* Needed in Geom.ML?? *)
-lemma hrabs_add_lemma_disj2: "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y"
-by (simp add: hrabs_def split add: split_if_asm)
-
-
-(*----------------------------------------------------------
-    Relating hrabs to abs through embedding of IR into IR*
- ----------------------------------------------------------*)
-lemma hypreal_of_real_hrabs:
-    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
-apply (unfold hypreal_of_real_def)
-apply (auto simp add: hypreal_hrabs)
-done
-
-
-(*----------------------------------------------------------------------------
-             Embedding of the naturals in the hyperreals
- ----------------------------------------------------------------------------*)
-
-lemma hypreal_of_nat_add [simp]:
-     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
-by (simp add: hypreal_of_nat_def)
-
-lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
-by (simp add: hypreal_of_nat_def)
-declare hypreal_of_nat_mult [simp]
-
-lemma hypreal_of_nat_less_iff:
-      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
-apply (simp add: hypreal_of_nat_def)
-done
-declare hypreal_of_nat_less_iff [symmetric, simp]
-
-(*------------------------------------------------------------*)
-(* naturals embedded in hyperreals                            *)
-(* is a hyperreal c.f. NS extension                           *)
-(*------------------------------------------------------------*)
-
-lemma hypreal_of_nat_iff:
-     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real m})"
-by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
-
-lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
-by (simp add: inj_on_def hypreal_of_nat_def)
-
-lemma hypreal_of_nat_Suc:
-     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
-by (simp add: hypreal_of_nat_def real_of_nat_Suc)
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-lemma hypreal_of_nat_number_of [simp]:
-     "hypreal_of_nat (number_of v :: nat) =
-         (if neg (number_of v) then 0
-          else (number_of v :: hypreal))"
-by (simp add: hypreal_of_nat_def)
-
-lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
-by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
-
-lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
-by (simp add: hypreal_of_nat_Suc)
-
-
-ML
-{*
-val hypreal_of_nat_def = thm"hypreal_of_nat_def";
-
-val hrabs_number_of = thm "hrabs_number_of";
-val hrabs_eqI1 = thm "hrabs_eqI1";
-val hrabs_eqI2 = thm "hrabs_eqI2";
-val hrabs_minus_eqI2 = thm "hrabs_minus_eqI2";
-val hrabs_minus_eqI1 = thm "hrabs_minus_eqI1";
-val hrabs_add_less = thm "hrabs_add_less";
-val hrabs_less_gt_zero = thm "hrabs_less_gt_zero";
-val hrabs_disj = thm "hrabs_disj";
-val hrabs_eq_disj = thm "hrabs_eq_disj";
-val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
-val hrabs_add_lemma_disj2 = thm "hrabs_add_lemma_disj2";
-val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
-val hypreal_of_nat_add = thm "hypreal_of_nat_add";
-val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
-val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
-val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
-val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
-val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
-val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
-val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
-val hypreal_of_nat_one = thm "hypreal_of_nat_one";
-*}
-
-end
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HSeries.ML
--- a/src/HOL/Hyperreal/HSeries.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HSeries.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -213,7 +213,7 @@
 
 Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
 \     ==> abs (sumhr (M, N, f)) @= 0";
-by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
+by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
 by (auto_tac (claset(), simpset() addsimps [approx_refl]));
 by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
 by (auto_tac (claset() addDs [approx_hrabs],
@@ -265,7 +265,7 @@
                  summable_convergent_sumr_iff, convergent_NSconvergent_iff,
                  NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
                  starfunNat_sumr]));
-by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
+by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
 by (auto_tac (claset(), simpset() addsimps [approx_refl]));
 by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
 by (rtac (approx_minus_iff RS iffD2) 2);
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HTranscendental.ML
--- a/src/HOL/Hyperreal/HTranscendental.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -609,7 +609,7 @@
 Goal "n : HNatInfinite \
 \     ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1";
 by (rtac STAR_sin_Infinitesimal_divide 1);
-by Auto_tac;
+by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
 val lemma_sin_pi = result();
 
 Goal "n : HNatInfinite \
@@ -626,7 +626,7 @@
 
 Goal "N : HNatInfinite \
 \     ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0";
-by Auto_tac;
+by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
 qed "pi_divide_HNatInfinite_not_zero";
 Addsimps [pi_divide_HNatInfinite_not_zero];
 
@@ -675,8 +675,8 @@
 
 Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N";
 by (rtac ccontr 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat_zero RS sym,
-    symmetric hypnat_le_def]));
+by (auto_tac (claset(),
+   simpset() addsimps [hypreal_of_hypnat_zero RS sym, linorder_not_less]));
 qed "HNatInfinite_hypreal_of_hypnat_gt_zero";
 
 bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero",
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HyperArith.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/HyperBin.thy
+(*  Title:      HOL/HyperArith.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
@@ -6,7 +6,7 @@
 
 header{*Binary arithmetic and Simplification for the Hyperreals*}
 
-theory HyperArith = HyperOrd
+theory HyperArith = HyperDef
 files ("hypreal_arith.ML"):
 
 subsection{*Binary Arithmetic for the Hyperreals*}
@@ -156,10 +156,7 @@
 by (simp add: hypreal_divide_def hypreal_minus_inverse)
 
 
-
-
-(** number_of related to hypreal_of_real.
-Could similar theorems be useful for other injections? **)
+subsection{*The Function @{term hypreal_of_real}*}
 
 lemma number_of_less_hypreal_of_real_iff [simp]:
      "(number_of w < hypreal_of_real z) = (number_of w < z)"
@@ -191,8 +188,114 @@
 apply (simp (no_asm))
 done
 
+subsection{*Absolute Value Function for the Hyperreals*}
+
+lemma hrabs_number_of [simp]:
+     "abs (number_of v :: hypreal) =
+        (if neg (number_of v) then number_of (bin_minus v)
+         else number_of v)"
+by (simp add: hrabs_def)
+
+
+declare abs_mult [simp]
+
+lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
+apply (unfold hrabs_def)
+apply (simp split add: split_if_asm)
+done
+
+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"
+by (simp add: hrabs_def)
+
+(* Needed in Geom.ML *)
+lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
+by (simp add: hrabs_def split add: split_if_asm)
+
+
+(*----------------------------------------------------------
+    Relating hrabs to abs through embedding of IR into IR*
+ ----------------------------------------------------------*)
+lemma hypreal_of_real_hrabs:
+    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
+apply (unfold hypreal_of_real_def)
+apply (auto simp add: hypreal_hrabs)
+done
+
+
+subsection{*Embedding the Naturals into the Hyperreals*}
+
+constdefs
+
+  hypreal_of_nat :: "nat => hypreal"
+  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
+
+
+lemma hypreal_of_nat_add [simp]:
+     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
+by (simp add: hypreal_of_nat_def)
+
+lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
+by (simp add: hypreal_of_nat_def)
+declare hypreal_of_nat_mult [simp]
+
+lemma hypreal_of_nat_less_iff:
+      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
+apply (simp add: hypreal_of_nat_def)
+done
+declare hypreal_of_nat_less_iff [symmetric, simp]
+
+(*------------------------------------------------------------*)
+(* naturals embedded in hyperreals                            *)
+(* is a hyperreal c.f. NS extension                           *)
+(*------------------------------------------------------------*)
+
+lemma hypreal_of_nat_iff:
+     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real m})"
+by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
+
+lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
+by (simp add: inj_on_def hypreal_of_nat_def)
+
+lemma hypreal_of_nat_Suc:
+     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
+by (simp add: hypreal_of_nat_def real_of_nat_Suc)
+
+(*"neg" is used in rewrite rules for binary comparisons*)
+lemma hypreal_of_nat_number_of [simp]:
+     "hypreal_of_nat (number_of v :: nat) =
+         (if neg (number_of v) then 0
+          else (number_of v :: hypreal))"
+by (simp add: hypreal_of_nat_def)
+
+lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
+by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
+
+lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
+by (simp add: hypreal_of_nat_Suc)
+
+lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
+apply (induct_tac "m")
+apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
+done
+
+lemma hypreal_of_nat_le_iff:
+      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
+apply (auto simp add: linorder_not_less [symmetric])
+done
+declare hypreal_of_nat_le_iff [simp]
+
+lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
+apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
+         del: hypreal_of_nat_zero)
+done
+declare hypreal_of_nat_ge_zero [simp]
+
+
 (*
-FIXME: we should have this, as for type int, but many proofs would break.
+FIXME: we should declare this, as for type int, but many proofs would break.
 It replaces x+-y by x-y.
 Addsimps [symmetric hypreal_diff_def]
 *)
@@ -201,6 +304,27 @@
 {*
 val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
 val hypreal_le_add_order = thm"hypreal_le_add_order";
+
+val hypreal_of_nat_def = thm"hypreal_of_nat_def";
+
+val hrabs_number_of = thm "hrabs_number_of";
+val hrabs_add_less = thm "hrabs_add_less";
+val hrabs_less_gt_zero = thm "hrabs_less_gt_zero";
+val hrabs_disj = thm "hrabs_disj";
+val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
+val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
+val hypreal_of_nat_add = thm "hypreal_of_nat_add";
+val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
+val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
+val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
+val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
+val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
+val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
+val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
+val hypreal_of_nat_one = thm "hypreal_of_nat_one";
+val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
+val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
+val hypreal_of_nat = thm"hypreal_of_nat";
 *}
 
 end
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -323,22 +323,21 @@
 done
 
 lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
-apply (rule_tac z = z in eq_Abs_hypreal)
-apply (rule_tac z = w in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of z])
+apply (rule eq_Abs_hypreal [of w])
 apply (simp add: add_ac hypreal_add)
 done
 
 lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
-apply (rule_tac z = z1 in eq_Abs_hypreal)
-apply (rule_tac z = z2 in eq_Abs_hypreal)
-apply (rule_tac z = z3 in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of z1])
+apply (rule eq_Abs_hypreal [of z2])
+apply (rule eq_Abs_hypreal [of z3])
 apply (simp add: hypreal_add real_add_assoc)
 done
 
 lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
-apply (unfold hypreal_zero_def)
-apply (rule_tac z = z in eq_Abs_hypreal)
-apply (simp add: hypreal_add)
+apply (rule eq_Abs_hypreal [of z])
+apply (simp add: hypreal_zero_def hypreal_add)
 done
 
 instance hypreal :: plus_ac0
@@ -395,15 +394,15 @@
 done
 
 lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
-apply (rule_tac z = z in eq_Abs_hypreal)
-apply (rule_tac z = w in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of z])
+apply (rule eq_Abs_hypreal [of w])
 apply (simp add: hypreal_mult mult_ac)
 done
 
 lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
-apply (rule_tac z = z1 in eq_Abs_hypreal)
-apply (rule_tac z = z2 in eq_Abs_hypreal)
-apply (rule_tac z = z3 in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of z1])
+apply (rule eq_Abs_hypreal [of z2])
+apply (rule eq_Abs_hypreal [of z3])
 apply (simp add: hypreal_mult mult_assoc)
 done
 
@@ -415,9 +414,9 @@
 
 lemma hypreal_add_mult_distrib:
      "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
-apply (rule_tac z = z1 in eq_Abs_hypreal)
-apply (rule_tac z = z2 in eq_Abs_hypreal)
-apply (rule_tac z = w in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of z1])
+apply (rule eq_Abs_hypreal [of z2])
+apply (rule eq_Abs_hypreal [of w])
 apply (simp add: hypreal_mult hypreal_add left_distrib)
 done
 
@@ -448,7 +447,7 @@
 lemma hypreal_mult_inverse: 
      "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
 apply (unfold hypreal_one_def hypreal_zero_def)
-apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule eq_Abs_hypreal [of x])
 apply (simp add: hypreal_inverse hypreal_mult)
 apply (drule FreeUltrafilterNat_Compl_mem)
 apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
@@ -616,9 +615,6 @@
 apply auto
 done
 
-lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0"
-  by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
-
 lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)"
 by simp
 
@@ -646,7 +642,8 @@
 by (simp add: Ring_and_Field.inverse_add mult_assoc)
 
 
-subsection{*@{term hypreal_of_real} Preserves Field and Order Properties*}
+subsection{*The Embedding @{term hypreal_of_real} Preserves Field and 
+      Order Properties*}
 
 lemma hypreal_of_real_add [simp]: 
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
@@ -890,13 +887,10 @@
 val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
 val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
 val hypreal_inverse = thm "hypreal_inverse";
-val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO";
-val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO";
 val hypreal_mult_inverse = thm "hypreal_mult_inverse";
 val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
 val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
 val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
-val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero";
 val hypreal_mult_not_0 = thm "hypreal_mult_not_0";
 val hypreal_minus_inverse = thm "hypreal_minus_inverse";
 val hypreal_inverse_distrib = thm "hypreal_inverse_distrib";
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperNat.ML
--- a/src/HOL/Hyperreal/HyperNat.ML	Thu Jan 29 16:51:17 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1334 +0,0 @@
-(*  Title       : HyperNat.ML
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-    Description : Explicit construction of hypernaturals using 
-                  ultrafilters
-*) 
-
-fun CLAIM_SIMP str thms =
-               prove_goal (the_context()) str
-               (fn prems => [cut_facts_tac prems 1,
-                   auto_tac (claset(),simpset() addsimps thms)]);
-fun CLAIM str = CLAIM_SIMP str [];
-
-(* blast confuses different versions of < *)
-DelIffs [order_less_irrefl];
-Addsimps [order_less_irrefl];
-
-(*------------------------------------------------------------------------
-                       Properties of hypnatrel
- ------------------------------------------------------------------------*)
-
-(** Proving that hyprel is an equivalence relation       **)
-(** Natural deduction for hypnatrel - similar to hyprel! **)
-
-Goalw [hypnatrel_def]
-     "((X,Y): hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)";
-by (Fast_tac 1);
-qed "hypnatrel_iff";
-
-Goalw [hypnatrel_def] 
-     "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hypnatrel";
-by (Fast_tac 1);
-qed "hypnatrelI";
-
-Goalw [hypnatrel_def]
-  "p: hypnatrel --> (EX X Y. \
-\                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
-by (Fast_tac 1);
-qed "hypnatrelE_lemma";
-
-val [major,minor] = Goal
-  "[| p: hypnatrel;  \
-\     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat |] \
-\            ==> Q |] \
-\  ==> Q";
-by (cut_facts_tac [major RS (hypnatrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "hypnatrelE";
-
-AddSIs [hypnatrelI];
-AddSEs [hypnatrelE];
-
-Goalw [hypnatrel_def] "(x,x): hypnatrel";
-by Auto_tac;
-qed "hypnatrel_refl";
-
-Goal "(x,y): hypnatrel ==> (y,x):hypnatrel";
-by (auto_tac (claset(), simpset() addsimps [hypnatrel_def, eq_commute]));
-qed "hypnatrel_sym";
-
-Goalw [hypnatrel_def]
-     "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
-by Auto_tac;
-by (Fuf_tac 1);
-qed_spec_mp "hypnatrel_trans";
-
-Goalw [equiv_def, refl_def, sym_def, trans_def]
-     "equiv UNIV hypnatrel";
-by (auto_tac (claset() addSIs [hypnatrel_refl] 
-                       addSEs [hypnatrel_sym,hypnatrel_trans] 
-                       delrules [hypnatrelI,hypnatrelE],
-              simpset()));
-qed "equiv_hypnatrel";
-
-val equiv_hypnatrel_iff =
-    [UNIV_I, UNIV_I] MRS (equiv_hypnatrel RS eq_equiv_class_iff);
-
-Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel``{x}:hypnat";
-by (Blast_tac 1);
-qed "hypnatrel_in_hypnat";
-
-Goal "inj_on Abs_hypnat hypnat";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_hypnat_inverse 1);
-qed "inj_on_Abs_hypnat";
-
-Addsimps [equiv_hypnatrel_iff,inj_on_Abs_hypnat RS inj_on_iff,
-          hypnatrel_iff, hypnatrel_in_hypnat, Abs_hypnat_inverse];
-
-Addsimps [equiv_hypnatrel RS eq_equiv_class_iff];
-val eq_hypnatrelD = equiv_hypnatrel RSN (2,eq_equiv_class);
-
-Goal "inj(Rep_hypnat)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_hypnat_inverse 1);
-qed "inj_Rep_hypnat";
-
-Goalw [hypnatrel_def] "x: hypnatrel `` {x}";
-by (Step_tac 1);
-by Auto_tac;
-qed "lemma_hypnatrel_refl";
-
-Addsimps [lemma_hypnatrel_refl];
-
-Goalw [hypnat_def] "{} ~: hypnat";
-by (auto_tac (claset() addSEs [quotientE],simpset()));
-qed "hypnat_empty_not_mem";
-
-Addsimps [hypnat_empty_not_mem];
-
-Goal "Rep_hypnat x ~= {}";
-by (cut_inst_tac [("x","x")] Rep_hypnat 1);
-by Auto_tac;
-qed "Rep_hypnat_nonempty";
-
-Addsimps [Rep_hypnat_nonempty];
-
-(*------------------------------------------------------------------------
-   hypnat_of_nat: the injection from nat to hypnat
- ------------------------------------------------------------------------*)
-Goal "inj(hypnat_of_nat)";
-by (rtac injI 1);
-by (rewtac hypnat_of_nat_def);
-by (dtac (inj_on_Abs_hypnat RS inj_onD) 1);
-by (REPEAT (rtac hypnatrel_in_hypnat 1));
-by (dtac eq_equiv_class 1);
-by (rtac equiv_hypnatrel 1);
-by (Fast_tac 1);
-by (rtac ccontr 1 THEN rotate_tac 1 1);
-by Auto_tac;
-qed "inj_hypnat_of_nat";
-
-val [prem] = Goal
-    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P";
-by (res_inst_tac [("x1","z")] 
-    (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1);
-by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1);
-by (res_inst_tac [("x","x")] prem 1);
-by (asm_full_simp_tac (simpset() addsimps [Rep_hypnat_inverse]) 1);
-qed "eq_Abs_hypnat";
-
-(*-----------------------------------------------------------
-   Addition for hyper naturals: hypnat_add 
- -----------------------------------------------------------*)
-Goalw [congruent2_def]
-     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})";
-by Safe_tac;
-by (ALLGOALS(Fuf_tac));
-qed "hypnat_add_congruent2";
-
-Goalw [hypnat_add_def]
-  "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel``{%n. X n + Y n})";
-by (asm_simp_tac
-    (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] 
-     MRS UN_equiv_class2]) 1);
-qed "hypnat_add";
-
-Goal "(z::hypnat) + w = w + z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps (add_ac @ [hypnat_add])) 1);
-qed "hypnat_add_commute";
-
-Goal "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypnat_add,add_assoc]) 1);
-qed "hypnat_add_assoc";
-
-(*For AC rewriting*)
-Goal "(x::hypnat)+(y+z)=y+(x+z)";
-by(rtac ([hypnat_add_assoc,hypnat_add_commute] MRS
-         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
-qed "hypnat_add_left_commute";
-
-(* hypnat addition is an AC operator *)
-val hypnat_add_ac = [hypnat_add_assoc,hypnat_add_commute,
-                      hypnat_add_left_commute];
-
-Goalw [hypnat_zero_def] "(0::hypnat) + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_add]) 1);
-qed "hypnat_add_zero_left";
-
-Goal "z + (0::hypnat) = z";
-by (simp_tac (simpset() addsimps 
-    [hypnat_add_zero_left,hypnat_add_commute]) 1);
-qed "hypnat_add_zero_right";
-
-Addsimps [hypnat_add_zero_left,hypnat_add_zero_right];
-
-(*-----------------------------------------------------------
-   Subtraction for hyper naturals: hypnat_minus
- -----------------------------------------------------------*)
-Goalw [congruent2_def]
-    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})";
-by Safe_tac;
-by (ALLGOALS(Fuf_tac));
-qed "hypnat_minus_congruent2";
- 
-Goalw [hypnat_minus_def]
-  "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel``{%n. X n - Y n})";
-by (asm_simp_tac
-    (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] 
-     MRS UN_equiv_class2]) 1);
-qed "hypnat_minus";
-
-Goalw [hypnat_zero_def] "z - z = (0::hypnat)";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
-qed "hypnat_minus_zero";
-
-Goalw [hypnat_zero_def] "(0::hypnat) - n = 0";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
-qed "hypnat_diff_0_eq_0";
-
-Addsimps [hypnat_minus_zero,hypnat_diff_0_eq_0];
-
-Goalw [hypnat_zero_def] "(m+n = (0::hypnat)) = (m=0 & n=0)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
-                       addDs [FreeUltrafilterNat_Int],
-              simpset() addsimps [hypnat_add] ));
-qed "hypnat_add_is_0";
-
-AddIffs [hypnat_add_is_0];
-
-Goal "!!i::hypnat. i-j-k = i - (j+k)";
-by (res_inst_tac [("z","i")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","j")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps 
-    [hypnat_minus,hypnat_add,diff_diff_left]) 1);
-qed "hypnat_diff_diff_left";
-
-Goal "!!i::hypnat. i-j-k = i-k-j";
-by (simp_tac (simpset() addsimps 
-    [hypnat_diff_diff_left, hypnat_add_commute]) 1);
-qed "hypnat_diff_commute";
-
-Goal "!!n::hypnat. (n+m) - n = m";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
-qed "hypnat_diff_add_inverse";
-Addsimps [hypnat_diff_add_inverse];
-
-Goal "!!n::hypnat.(m+n) - n = m";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
-qed "hypnat_diff_add_inverse2";
-Addsimps [hypnat_diff_add_inverse2];
-
-Goal "!!k::hypnat. (k+m) - (k+n) = m - n";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
-qed "hypnat_diff_cancel";
-Addsimps [hypnat_diff_cancel];
-
-Goal "!!m::hypnat. (m+k) - (n+k) = m - n";
-val hypnat_add_commute_k = read_instantiate [("w","k")] hypnat_add_commute;
-by (asm_simp_tac (simpset() addsimps ([hypnat_add_commute_k])) 1);
-qed "hypnat_diff_cancel2";
-Addsimps [hypnat_diff_cancel2];
-
-Goalw [hypnat_zero_def] "!!n::hypnat. n - (n+m) = (0::hypnat)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
-qed "hypnat_diff_add_0";
-Addsimps [hypnat_diff_add_0];
-
-(*-----------------------------------------------------------
-   Multiplication for hyper naturals: hypnat_mult
- -----------------------------------------------------------*)
-Goalw [congruent2_def]
-    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})";
-by Safe_tac;
-by (ALLGOALS(Fuf_tac));
-qed "hypnat_mult_congruent2";
-
-Goalw [hypnat_mult_def]
-  "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) = \
-\  Abs_hypnat(hypnatrel``{%n. X n * Y n})";
-by (asm_simp_tac
-    (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS
-     UN_equiv_class2]) 1);
-qed "hypnat_mult";
-
-Goal "(z::hypnat) * w = w * z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps ([hypnat_mult] @ mult_ac)) 1);
-qed "hypnat_mult_commute";
-
-Goal "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypnat_mult,mult_assoc]) 1);
-qed "hypnat_mult_assoc";
-
-
-Goal "(z1::hypnat) * (z2 * z3) = z2 * (z1 * z3)";
-by(rtac ([hypnat_mult_assoc,hypnat_mult_commute] MRS
-         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
-qed "hypnat_mult_left_commute";
-
-(* hypnat multiplication is an AC operator *)
-val hypnat_mult_ac = [hypnat_mult_assoc, hypnat_mult_commute, 
-                      hypnat_mult_left_commute];
-
-Goalw [hypnat_one_def] "(1::hypnat) * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
-qed "hypnat_mult_1";
-Addsimps [hypnat_mult_1];
-
-Goal "z * (1::hypnat) = z";
-by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
-qed "hypnat_mult_1_right";
-Addsimps [hypnat_mult_1_right];
-
-Goalw [hypnat_zero_def] "(0::hypnat) * z = 0";
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
-qed "hypnat_mult_0";
-Addsimps [hypnat_mult_0];
-
-Goal "z * (0::hypnat) = 0";
-by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
-qed "hypnat_mult_0_right";
-Addsimps [hypnat_mult_0_right];
-
-Goal "!!m::hypnat. (m - n) * k = (m * k) - (n * k)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypnat_mult,
-    hypnat_minus,diff_mult_distrib]) 1);
-qed "hypnat_diff_mult_distrib" ;
-
-Goal "!!m::hypnat. k * (m - n) = (k * m) - (k * n)";
-val hypnat_mult_commute_k = read_instantiate [("z","k")] hypnat_mult_commute;
-by (simp_tac (simpset() addsimps [hypnat_diff_mult_distrib, 
-                                  hypnat_mult_commute_k]) 1);
-qed "hypnat_diff_mult_distrib2" ;
-
-(*--------------------------
-    A Few more theorems
- -------------------------*)
-
-Goal "(z::hypnat) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
-by (asm_simp_tac (simpset() addsimps [hypnat_add_assoc RS sym]) 1);
-qed "hypnat_add_assoc_cong";
-
-Goal "(z::hypnat) + (v + w) = v + (z + w)";
-by (REPEAT (ares_tac [hypnat_add_commute RS hypnat_add_assoc_cong] 1));
-qed "hypnat_add_assoc_swap";
-
-Goal "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)";
-by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypnat_mult,hypnat_add,
-                                      add_mult_distrib]) 1);
-qed "hypnat_add_mult_distrib";
-Addsimps [hypnat_add_mult_distrib];
-
-val hypnat_mult_commute'= read_instantiate [("z","w")] hypnat_mult_commute;
-
-Goal "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [hypnat_mult_commute']) 1);
-qed "hypnat_add_mult_distrib2";
-Addsimps [hypnat_add_mult_distrib2];
-
-(*** (hypnat) one and zero are distinct ***)
-Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= (1::hypnat)";
-by Auto_tac;
-qed "hypnat_zero_not_eq_one";
-Addsimps [hypnat_zero_not_eq_one];
-Addsimps [hypnat_zero_not_eq_one RS not_sym];
-
-Goalw [hypnat_zero_def] "(m*n = (0::hypnat)) = (m=0 | n=0)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
-    simpset() addsimps [hypnat_mult]));
-by (ALLGOALS(Fuf_tac));
-qed "hypnat_mult_is_0";
-Addsimps [hypnat_mult_is_0];
-
-(*------------------------------------------------------------------
-                   Theorems for ordering 
- ------------------------------------------------------------------*)
-
-(* prove introduction and elimination rules for hypnat_less *)
-
-Goalw [hypnat_less_def]
- "(P < (Q::hypnat)) = (EX X Y. X : Rep_hypnat(P) & \
-\                             Y : Rep_hypnat(Q) & \
-\                             {n. X n < Y n} : FreeUltrafilterNat)";
-by (Fast_tac 1);
-qed "hypnat_less_iff";
-
-Goalw [hypnat_less_def]
- "[| {n. X n < Y n} : FreeUltrafilterNat; \
-\         X : Rep_hypnat(P); \
-\         Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)";
-by (Fast_tac 1);
-qed "hypnat_lessI";
-
-Goalw [hypnat_less_def]
-     "!! R1. [| R1 < (R2::hypnat); \
-\         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
-\         !!X. X : Rep_hypnat(R1) ==> P; \ 
-\         !!Y. Y : Rep_hypnat(R2) ==> P |] \
-\     ==> P";
-by Auto_tac;
-qed "hypnat_lessE";
-
-Goalw [hypnat_less_def]
- "R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
-\                                  X : Rep_hypnat(R1) & \
-\                                  Y : Rep_hypnat(R2))";
-by (Fast_tac 1);
-qed "hypnat_lessD";
-
-Goal "~ (R::hypnat) < R";
-by (res_inst_tac [("z","R")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
-by (Fuf_empty_tac 1);
-qed "hypnat_less_not_refl";
-Addsimps [hypnat_less_not_refl];
-
-bind_thm("hypnat_less_irrefl",hypnat_less_not_refl RS notE);
-
-Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by Auto_tac;
-by (Fuf_empty_tac 1);
-qed "hypnat_not_less0";
-AddIffs [hypnat_not_less0];
-
-(* n<(0::hypnat) ==> R *)
-bind_thm ("hypnat_less_zeroE", hypnat_not_less0 RS notE);
-
-Goalw [hypnat_less_def,hypnat_zero_def,hypnat_one_def]
-      "(n<(1::hypnat)) = (n=0)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addSIs [exI] addEs 
-    [FreeUltrafilterNat_subset],simpset()));
-by (Fuf_tac 1);
-qed "hypnat_less_one";
-AddIffs [hypnat_less_one];
-
-Goal "!!(R1::hypnat). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
-by (res_inst_tac [("z","R1")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","R2")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
-by (res_inst_tac [("x","X")] exI 1);
-by Auto_tac;
-by (res_inst_tac [("x","Ya")] exI 1);
-by Auto_tac;
-by (Fuf_tac 1);
-qed "hypnat_less_trans";
-
-Goal "!! (R1::hypnat). [| R1 < R2; R2 < R1 |] ==> P";
-by (dtac hypnat_less_trans 1 THEN assume_tac 1);
-by (Asm_full_simp_tac 1);
-qed "hypnat_less_asym";
-
-(*----- hypnat less iff less a.e -----*)
-(* See comments in HYPER for corresponding thm *)
-
-Goalw [hypnat_less_def]
-      "(Abs_hypnat(hypnatrel``{%n. X n}) < \
-\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
-\      ({n. X n < Y n} : FreeUltrafilterNat)";
-by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset()));
-by (Fuf_tac 1);
-qed "hypnat_less";
-
-Goal "~ m<n --> n+(m-n) = (m::hypnat)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypnat_minus,hypnat_add,hypnat_less]));
-by (dtac FreeUltrafilterNat_Compl_mem 1);
-by (Fuf_tac 1);
-qed_spec_mp "hypnat_add_diff_inverse";
-
-Goal "n<=m ==> n+(m-n) = (m::hypnat)";
-by (asm_full_simp_tac (simpset() addsimps 
-    [hypnat_add_diff_inverse, hypnat_le_def]) 1);
-qed "hypnat_le_add_diff_inverse";
-
-Goal "n<=m ==> (m-n)+n = (m::hypnat)";
-by (asm_simp_tac (simpset() addsimps [hypnat_le_add_diff_inverse, 
-    hypnat_add_commute]) 1);
-qed "hypnat_le_add_diff_inverse2";
-
-(*---------------------------------------------------------------------------------
-                    Hyper naturals as a linearly ordered field
- ---------------------------------------------------------------------------------*)
-Goalw [hypnat_zero_def] 
-     "[| (0::hypnat) < x; 0 < y |] ==> 0 < x + y";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps
-   [hypnat_less_def,hypnat_add]));
-by (REPEAT(Step_tac 1));
-by (Fuf_tac 1);
-qed "hypnat_add_order";
-
-Goalw [hypnat_zero_def] 
-      "!!(x::hypnat). [| (0::hypnat) < x; 0 < y |] ==> 0 < x * y";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypnat_less_def,hypnat_mult]));
-by (REPEAT(Step_tac 1));
-by (Fuf_tac 1);
-qed "hypnat_mult_order";
-
-(*---------------------------------------------------------------------------------
-                   Trichotomy of the hyper naturals
-  --------------------------------------------------------------------------------*)
-Goalw [hypnatrel_def] "EX x. x: hypnatrel `` {%n. 0}";
-by (res_inst_tac [("x","%n. 0")] exI 1);
-by (Step_tac 1);
-by Auto_tac;
-qed "lemma_hypnatrel_0_mem";
-
-(* linearity is actually proved further down! *)
-Goalw [hypnat_zero_def, hypnat_less_def]
-     "(0::hypnat) <  x | x = 0 | x < 0";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (Auto_tac );
-by (REPEAT(Step_tac 1));
-by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
-by (Fuf_tac 1);
-qed "hypnat_trichotomy";
-
-Goal "!!P. [| (0::hypnat) < x ==> P; \
-\             x = 0 ==> P; \
-\             x < 0 ==> P |] ==> P";
-by (cut_inst_tac [("x","x")] hypnat_trichotomy 1);
-by Auto_tac;
-qed "hypnat_trichotomyE";
-
-(*----------------------------------------------------------------------------
-            More properties of <
- ----------------------------------------------------------------------------*)
-Goal "!!(A::hypnat). A < B ==> A + C < B + C";
-by (res_inst_tac [("z","A")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","B")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","C")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [hypnat_less_def,hypnat_add]));
-by (REPEAT(Step_tac 1));
-by (Fuf_tac 1);
-qed "hypnat_add_less_mono1";
-
-Goal "!!(A::hypnat). A < B ==> C + A < C + B";
-by (auto_tac (claset() addIs [hypnat_add_less_mono1],
-              simpset() addsimps [hypnat_add_commute]));
-qed "hypnat_add_less_mono2";
-
-Goal "!!k l::hypnat. [|i<j;  k<l |] ==> i + k < j + l";
-by (etac (hypnat_add_less_mono1 RS hypnat_less_trans) 1);
-by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
-(*j moves to the end because it is free while k, l are bound*)
-by (etac hypnat_add_less_mono1 1);
-qed "hypnat_add_less_mono";
-
-(*---------------------------------------
-        hypnat_minus_less
- ---------------------------------------*)
-Goalw [hypnat_less_def,hypnat_zero_def] 
-      "((x::hypnat) < y) = ((0::hypnat) < y - x)";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypnat_minus]));
-by (REPEAT(Step_tac 1));
-by (REPEAT(Step_tac 2));
-by (ALLGOALS(fuf_tac (claset() addDs [sym],simpset())));
-
-(*** linearity ***)
-Goalw [hypnat_less_def] "(x::hypnat) < y | x = y | y < x";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (Auto_tac );
-by (REPEAT(Step_tac 1));
-by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
-by (Fuf_tac 1);
-qed "hypnat_linear";
-
-Goal "!!(x::hypnat). [| x < y ==> P;  x = y ==> P; \
-\                       y < x ==> P |] ==> P";
-by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1);
-by Auto_tac;
-qed "hypnat_linear_less2";
-
-Goal "((w::hypnat) ~= z) = (w<z | z<w)";
-by (cut_facts_tac [hypnat_linear] 1);
-by Auto_tac;
-qed "hypnat_neq_iff";
-
-(* Axiom 'order_less_le' of class 'order': *)
-Goal "((w::hypnat) < z) = (w <= z & w ~= z)";
-by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
-by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
-qed "hypnat_less_le";
-
-(*----------------------------------------------------------------------------
-                            Properties of <=
- ----------------------------------------------------------------------------*)
-
-(*------ hypnat le iff nat le a.e ------*)
-Goalw [hypnat_le_def,le_def]
-      "(Abs_hypnat(hypnatrel``{%n. X n}) <= \
-\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
-\      ({n. X n <= Y n} : FreeUltrafilterNat)";
-by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
-    simpset() addsimps [hypnat_less]));
-by (Fuf_tac 1 THEN Fuf_empty_tac 1);
-qed "hypnat_le";
-
-(*---------------------------------------------------------*)
-(*---------------------------------------------------------*)
-
-Goalw [hypnat_le_def] "z < w ==> z <= (w::hypnat)";
-by (fast_tac (claset() addEs [hypnat_less_asym]) 1);
-qed "hypnat_less_imp_le";
-
-Goalw [hypnat_le_def] "!!(x::hypnat). x <= y ==> x < y | x = y";
-by (cut_facts_tac [hypnat_linear] 1);
-by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
-qed "hypnat_le_imp_less_or_eq";
-
-Goalw [hypnat_le_def] "z<w | z=w ==> z <=(w::hypnat)";
-by (cut_facts_tac [hypnat_linear] 1);
-by (blast_tac (claset() addDs [hypnat_less_irrefl,hypnat_less_asym]) 1);
-qed "hypnat_less_or_eq_imp_le";
-
-Goal "(x <= (y::hypnat)) = (x < y | x=y)";
-by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, 
-                     hypnat_le_imp_less_or_eq] 1));
-qed "hypnat_le_less";
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-Goal "(z::hypnat) <= w | w <= z";
-by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
-by (cut_facts_tac [hypnat_linear] 1);
-by (Blast_tac 1);
-qed "hypnat_le_linear";
-
-Goal "w <= (w::hypnat)";
-by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
-qed "hypnat_le_refl";
-Addsimps [hypnat_le_refl];
-
-Goal "[| i <= j; j <= k |] ==> i <= (k::hypnat)";
-by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
-            rtac hypnat_less_or_eq_imp_le, 
-            fast_tac (claset() addIs [hypnat_less_trans])]);
-qed "hypnat_le_trans";
-
-Goal "[| z <= w; w <= z |] ==> z = (w::hypnat)";
-by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
-            fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]);
-qed "hypnat_le_anti_sym";
-
-Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
-by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypnat_mult_order, hypnat_less_imp_le],
-              simpset() addsimps [hypnat_le_refl]));
-qed "hypnat_le_mult_order";
-
-Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
-      "(0::hypnat) < (1::hypnat)";
-by (res_inst_tac [("x","%n. 0")] exI 1);
-by (res_inst_tac [("x","%n. Suc 0")] exI 1);
-by Auto_tac;
-qed "hypnat_zero_less_one";
-
-Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
-by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypnat_add_order,
-    hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
-qed "hypnat_le_add_order";
-
-Goal "!!(q1::hypnat). q1 <= q2  ==> x + q1 <= x + q2";
-by (dtac hypnat_le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (auto_tac (claset() addSIs [hypnat_le_refl,
-    hypnat_less_imp_le,hypnat_add_less_mono1],
-    simpset() addsimps [hypnat_add_commute]));
-qed "hypnat_add_le_mono2";
-
-Goal "!!(q1::hypnat). q1 <= q2  ==> q1 + x <= q2 + x";
-by (auto_tac (claset() addDs [hypnat_add_le_mono2],
-    simpset() addsimps [hypnat_add_commute]));
-qed "hypnat_add_le_mono1";
-
-Goal "!!k l::hypnat. [|i<=j;  k<=l |] ==> i + k <= j + l";
-by (etac (hypnat_add_le_mono1 RS hypnat_le_trans) 1);
-by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
-(*j moves to the end because it is free while k, l are bound*)
-by (etac hypnat_add_le_mono1 1);
-qed "hypnat_add_le_mono";
-
-Goalw [hypnat_zero_def]
-     "!!x::hypnat. [| (0::hypnat) < z; x < y |] ==> x * z < y * z";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypnat_less,hypnat_mult]));
-by (Fuf_tac 1);
-qed "hypnat_mult_less_mono1";
-
-Goal "!!x::hypnat. [| 0 < z; x < y |] ==> z * x < z * y";
-by (auto_tac (claset() addIs [hypnat_mult_less_mono1],
-              simpset() addsimps [hypnat_mult_commute]));
-qed "hypnat_mult_less_mono2";
-
-Addsimps [hypnat_mult_less_mono2,hypnat_mult_less_mono1];
-
-Goal "(x::hypnat) <= n + x";
-by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
-by (auto_tac (claset() addDs [(hypnat_less_imp_le RS
-    hypnat_add_le_mono1)],simpset() addsimps [hypnat_le_refl]));
-qed "hypnat_add_self_le";
-Addsimps [hypnat_add_self_le];
-
-Goal "(x::hypnat) < x + (1::hypnat)";
-by (cut_facts_tac [hypnat_zero_less_one 
-         RS hypnat_add_less_mono2] 1);
-by Auto_tac;
-qed "hypnat_add_one_self_less";
-Addsimps [hypnat_add_one_self_less];
-
-Goalw [hypnat_le_def] "~ x + (1::hypnat) <= x";
-by (Simp_tac 1);
-qed "not_hypnat_add_one_le_self";
-Addsimps [not_hypnat_add_one_le_self];
-
-Goal "((0::hypnat) < n) = ((1::hypnat) <= n)";
-by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
-qed "hypnat_gt_zero_iff";
-
-Addsimps  [hypnat_le_add_diff_inverse, hypnat_le_add_diff_inverse2,
-           hypnat_less_imp_le RS hypnat_le_add_diff_inverse2];
-
-Goal "(0 < n) = (EX m. n = m + (1::hypnat))";
-by (Step_tac 1);
-by (res_inst_tac [("x","m")] hypnat_trichotomyE 2);
-by (rtac hypnat_less_trans 2);
-by (res_inst_tac [("x","n - (1::hypnat)")] exI 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypnat_gt_zero_iff,hypnat_add_commute]));
-qed "hypnat_gt_zero_iff2";
-
-Goalw [hypnat_zero_def] "(0::hypnat) <= n";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps [hypnat_le]) 1);
-qed "hypnat_le_zero";
-Addsimps [hypnat_le_zero];
-
-(*------------------------------------------------------------------
-     hypnat_of_nat: properties embedding of naturals in hypernaturals
- -----------------------------------------------------------------*)
-    (** hypnat_of_nat preserves field and order properties **)
-
-Goalw [hypnat_of_nat_def] 
-      "hypnat_of_nat ((z1::nat) + z2) = \
-\      hypnat_of_nat z1 + hypnat_of_nat z2";
-by (asm_simp_tac (simpset() addsimps [hypnat_add]) 1);
-qed "hypnat_of_nat_add";
-
-Goalw [hypnat_of_nat_def] 
-      "hypnat_of_nat ((z1::nat) - z2) = \
-\      hypnat_of_nat z1 - hypnat_of_nat z2";
-by (asm_simp_tac (simpset() addsimps [hypnat_minus]) 1);
-qed "hypnat_of_nat_minus";
-
-Goalw [hypnat_of_nat_def] 
-      "hypnat_of_nat (z1 * z2) = hypnat_of_nat z1 * hypnat_of_nat z2";
-by (full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
-qed "hypnat_of_nat_mult";
-
-Goalw [hypnat_less_def,hypnat_of_nat_def] 
-      "(z1 < z2) = (hypnat_of_nat z1 < hypnat_of_nat z2)";
-by (auto_tac (claset() addSIs [exI] addIs 
-   [FreeUltrafilterNat_all],simpset()));
-by (rtac FreeUltrafilterNat_P 1 THEN Fuf_tac 1);
-qed "hypnat_of_nat_less_iff";
-Addsimps [hypnat_of_nat_less_iff RS sym];
-
-Goalw [hypnat_le_def,le_def] 
-      "(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)";
-by Auto_tac;
-qed "hypnat_of_nat_le_iff";
-
-Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat (Suc 0) = (1::hypnat)";
-by (Simp_tac 1);
-qed "hypnat_of_nat_one";
-
-Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
-by (Simp_tac 1);
-qed "hypnat_of_nat_zero";
-
-Goal "(hypnat_of_nat  n = 0) = (n = 0)";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
-    simpset() addsimps [hypnat_of_nat_def,
-    hypnat_zero_def]));
-qed "hypnat_of_nat_zero_iff";
-
-Goal "(hypnat_of_nat  n ~= 0) = (n ~= 0)";
-by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1);
-qed "hypnat_of_nat_not_zero_iff";
-
-Goalw [hypnat_of_nat_def,hypnat_one_def]
-     "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)";
-by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
-qed "hypnat_of_nat_Suc";
-
-(*---------------------------------------------------------------------------------
-              Existence of infinite hypernatural number
- ---------------------------------------------------------------------------------*)
-
-Goal "hypnatrel``{%n::nat. n} : hypnat";
-by Auto_tac;
-qed "hypnat_omega";
-
-Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat";
-by (rtac Rep_hypnat 1);
-qed "Rep_hypnat_omega";
-
-(* See Hyper.thy for similar argument*)
-(* existence of infinite number not corresponding to any natural number *)
-(* use assumption that member FreeUltrafilterNat is not finite       *)
-(* a few lemmas first *)
-
-Goalw [hypnat_omega_def,hypnat_of_nat_def]
-      "~ (EX x. hypnat_of_nat x = whn)";
-by (auto_tac (claset() addDs [FreeUltrafilterNat_not_finite], 
-              simpset()));
-qed "not_ex_hypnat_of_nat_eq_omega";
-
-Goal "hypnat_of_nat x ~= whn";
-by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1);
-by Auto_tac;
-qed "hypnat_of_nat_not_eq_omega";
-Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
-
-(*-----------------------------------------------------------
-    Properties of the set Nats of embedded natural numbers
-              (cf. set Reals in NSA.thy/NSA.ML)
- ----------------------------------------------------------*)
-
-(* Infinite hypernatural not in embedded Nats *)
-Goalw [SHNat_def] "whn ~: Nats";
-by Auto_tac;
-qed "SHNAT_omega_not_mem";
-Addsimps [SHNAT_omega_not_mem];
-
-(*-----------------------------------------------------------------------
-     Closure laws for members of (embedded) set standard naturals Nats
- -----------------------------------------------------------------------*)
-Goalw [SHNat_def] 
-     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x + y: Nats";
-by (Step_tac 1);
-by (res_inst_tac [("x","N + Na")] exI 1);
-by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1);
-qed "SHNat_add";
-
-Goalw [SHNat_def] 
-     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x - y: Nats";
-by (Step_tac 1);
-by (res_inst_tac [("x","N - Na")] exI 1);
-by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1);
-qed "SHNat_minus";
-
-Goalw [SHNat_def] 
-     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x * y: Nats";
-by (Step_tac 1);
-by (res_inst_tac [("x","N * Na")] exI 1);
-by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1);
-qed "SHNat_mult";
-
-Goal"!!x::hypnat. [| x + y : Nats; y: Nats |] ==> x: Nats";
-by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
-by Auto_tac;
-qed "SHNat_add_cancel";
-
-Goalw [SHNat_def] "hypnat_of_nat x : Nats";
-by (Blast_tac 1);
-qed "SHNat_hypnat_of_nat";
-Addsimps [SHNat_hypnat_of_nat];
-
-Goal "hypnat_of_nat (Suc 0) : Nats";
-by (Simp_tac 1);
-qed "SHNat_hypnat_of_nat_one";
-
-Goal "hypnat_of_nat 0 : Nats";
-by (Simp_tac 1);
-qed "SHNat_hypnat_of_nat_zero";
-
-Goal "(1::hypnat) : Nats";
-by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
-    hypnat_of_nat_one RS sym]) 1);
-qed "SHNat_one";
-
-Goal "(0::hypnat) : Nats";
-by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
-                                  hypnat_of_nat_zero RS sym]) 1);
-qed "SHNat_zero";
-
-Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
-          SHNat_one,SHNat_zero];
-
-Goal "(1::hypnat) + (1::hypnat) : Nats";
-by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
-qed "SHNat_two";
-
-Goalw [SHNat_def] "{x. hypnat_of_nat x : Nats} = (UNIV::nat set)";
-by Auto_tac;
-qed "SHNat_UNIV_nat";
-
-Goalw [SHNat_def] "(x: Nats) = (EX y. x = hypnat_of_nat  y)";
-by Auto_tac;
-qed "SHNat_iff";
-
-Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = Nats";
-by Auto_tac;
-qed "hypnat_of_nat_image";
-
-Goalw [SHNat_def] "inv hypnat_of_nat `Nats = (UNIV::nat set)";
-by Auto_tac;
-by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
-by (Blast_tac 1);
-qed "inv_hypnat_of_nat_image";
-
-Goalw [SHNat_def] 
-     "[| EX x. x: P; P <= Nats |] ==> EX Q. P = hypnat_of_nat ` Q";
-by (Blast_tac 1);
-qed "SHNat_hypnat_of_nat_image";
-
-Goalw [SHNat_def] 
-      "Nats = hypnat_of_nat ` (UNIV::nat set)";
-by Auto_tac;
-qed "SHNat_hypnat_of_nat_iff";
-
-Goalw [SHNat_def] "Nats <= (UNIV::hypnat set)";
-by Auto_tac;
-qed "SHNat_subset_UNIV";
-
-Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}";
-by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
-qed "leSuc_Un_eq";
-
-Goal "finite {n::nat. n <= m}";
-by (induct_tac "m" 1);
-by (auto_tac (claset(),simpset() addsimps [leSuc_Un_eq]));
-qed "finite_nat_le_segment";
-
-Goal "{n::nat. m < n} : FreeUltrafilterNat";
-by (cut_inst_tac [("m2","m")] (finite_nat_le_segment RS 
-    FreeUltrafilterNat_finite RS FreeUltrafilterNat_Compl_mem) 1);
-by (Fuf_tac 1);
-qed "lemma_unbounded_set";
-Addsimps [lemma_unbounded_set];
-
-Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def] 
-     "ALL n: Nats. n < whn";
-by (Clarify_tac 1);
-by (auto_tac (claset() addSIs [exI],simpset()));
-qed "hypnat_omega_gt_SHNat";
-
-Goal "hypnat_of_nat n < whn";
-by (cut_facts_tac [hypnat_omega_gt_SHNat] 1);
-by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1);
-by Auto_tac;
-qed "hypnat_of_nat_less_whn";
-Addsimps [hypnat_of_nat_less_whn];
-
-Goal "hypnat_of_nat n <= whn";
-by (rtac (hypnat_of_nat_less_whn RS hypnat_less_imp_le) 1);
-qed "hypnat_of_nat_le_whn";
-Addsimps [hypnat_of_nat_le_whn];
-
-Goal "0 < whn";
-by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
-by Auto_tac;
-qed "hypnat_zero_less_hypnat_omega";
-Addsimps [hypnat_zero_less_hypnat_omega];
-
-Goal "(1::hypnat) < whn";
-by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
-by Auto_tac;
-qed "hypnat_one_less_hypnat_omega";
-Addsimps [hypnat_one_less_hypnat_omega];
-
-(*--------------------------------------------------------------------------
-     Theorems about infinite hypernatural numbers -- HNatInfinite
- -------------------------------------------------------------------------*)
-Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite";
-by Auto_tac;
-qed "HNatInfinite_whn";
-Addsimps [HNatInfinite_whn];
-
-Goalw [HNatInfinite_def] "x: Nats ==> x ~: HNatInfinite";
-by (Simp_tac 1);
-qed "SHNat_not_HNatInfinite";
-
-Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: Nats";
-by (Asm_full_simp_tac 1);
-qed "not_HNatInfinite_SHNat";
-
-Goalw [HNatInfinite_def] "x ~: Nats ==> x: HNatInfinite";
-by (Simp_tac 1);
-qed "not_SHNat_HNatInfinite";
-
-Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: Nats";
-by (Asm_full_simp_tac 1);
-qed "HNatInfinite_not_SHNat";
-
-Goal "(x: Nats) = (x ~: HNatInfinite)";
-by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
-    not_HNatInfinite_SHNat]) 1);
-qed "SHNat_not_HNatInfinite_iff";
-
-Goal "(x ~: Nats) = (x: HNatInfinite)";
-by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
-    HNatInfinite_not_SHNat]) 1);
-qed "not_SHNat_HNatInfinite_iff";
-
-Goal "x : Nats | x : HNatInfinite";
-by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1);
-qed "SHNat_HNatInfinite_disj";
-
-(*-------------------------------------------------------------------
-   Proof of alternative definition for set of Infinite hypernatural 
-   numbers --- HNatInfinite = {N. ALL n: Nats. n < N}
- -------------------------------------------------------------------*)
-Goal "ALL N::nat. {n. f n ~= N} : FreeUltrafilterNat  \
-\     ==> {n. N < f n} : FreeUltrafilterNat";
-by (induct_tac "N" 1);
-by (dres_inst_tac [("x","0")] spec 1);
-by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1
-    THEN dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("x","Suc n")] spec 1);
-by (fuf_tac (claset() addSDs [Suc_leI],
-             simpset() addsimps [le_eq_less_or_eq]) 1);
-qed "HNatInfinite_FreeUltrafilterNat_lemma";
-
-(*** alternative definition ***)
-Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def] 
-     "HNatInfinite = {N. ALL n:Nats. n < N}";
-by (Step_tac 1);
-by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {%n. N})")] bspec 2);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
-by (auto_tac (claset() addSIs [exI] 
-                       addEs [HNatInfinite_FreeUltrafilterNat_lemma],
-    simpset() addsimps [FreeUltrafilterNat_Compl_iff1, 
-                 CLAIM "- {n. xa n = N} = {n. xa n ~= N}"]));
-qed "HNatInfinite_iff";
-
-(*--------------------------------------------------------------------
-   Alternative definition for HNatInfinite using Free ultrafilter
- --------------------------------------------------------------------*)
-Goal "x : HNatInfinite ==> EX X: Rep_hypnat x. \
-\                           ALL u. {n. u < X n}:  FreeUltrafilterNat";
-by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
-    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (EVERY[Auto_tac, rtac bexI 1, 
-    rtac lemma_hypnatrel_refl 2, Step_tac 1]);
-by (dres_inst_tac [("x","hypnat_of_nat u")] bspec 1);
-by (Simp_tac 1);
-by (auto_tac (claset(),
-    simpset() addsimps [hypnat_of_nat_def]));
-by (Fuf_tac 1);
-qed "HNatInfinite_FreeUltrafilterNat";
-
-Goal "EX X: Rep_hypnat x. ALL u. {n. u < X n}:  FreeUltrafilterNat \
-\     ==> x: HNatInfinite";
-by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
-    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
-by (rtac exI 1 THEN Auto_tac);
-qed "FreeUltrafilterNat_HNatInfinite";
-
-Goal "(x : HNatInfinite) = (EX X: Rep_hypnat x. \
-\          ALL u. {n. u < X n}:  FreeUltrafilterNat)";
-by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat,
-    FreeUltrafilterNat_HNatInfinite]) 1);
-qed "HNatInfinite_FreeUltrafilterNat_iff";
-
-Goal "x : HNatInfinite ==> (1::hypnat) < x";
-by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
-qed "HNatInfinite_gt_one";
-Addsimps [HNatInfinite_gt_one];
-
-Goal "0 ~: HNatInfinite";
-by (auto_tac (claset(),simpset() 
-    addsimps [HNatInfinite_iff]));
-by (dres_inst_tac [("a","(1::hypnat)")] equals0D 1);
-by (Asm_full_simp_tac 1);
-qed "zero_not_mem_HNatInfinite";
-Addsimps [zero_not_mem_HNatInfinite];
-
-Goal "x : HNatInfinite ==> x ~= 0";
-by Auto_tac;
-qed "HNatInfinite_not_eq_zero";
-
-Goal "x : HNatInfinite ==> (1::hypnat) <= x";
-by (blast_tac (claset() addIs [hypnat_less_imp_le,
-         HNatInfinite_gt_one]) 1);
-qed "HNatInfinite_ge_one";
-Addsimps [HNatInfinite_ge_one];
-
-(*--------------------------------------------------
-                   Closure Rules
- --------------------------------------------------*)
-Goal "[| x: HNatInfinite; y: HNatInfinite |] \
-\           ==> x + y: HNatInfinite";
-by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
-by (dtac bspec 1 THEN assume_tac 1);
-by (dtac (SHNat_zero RSN (2,bspec)) 1);
-by (dtac hypnat_add_less_mono 1 THEN assume_tac 1);
-by (Asm_full_simp_tac 1);
-qed "HNatInfinite_add";
-
-Goal "[| x: HNatInfinite; y: Nats |] ==> x + y: HNatInfinite";
-by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
-by (dres_inst_tac [("x","x + y")] SHNat_minus 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [SHNat_not_HNatInfinite_iff]));
-qed "HNatInfinite_SHNat_add";
-
-Goal "[| x: HNatInfinite; y: Nats |] ==> x - y: HNatInfinite";
-by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
-by (dres_inst_tac [("x","x - y")] SHNat_add 1);
-by (subgoal_tac "y <= x" 2);
-by (auto_tac (claset() addSDs [hypnat_le_add_diff_inverse2],
-    simpset() addsimps [not_SHNat_HNatInfinite_iff RS sym]));
-by (auto_tac (claset() addSIs [hypnat_less_imp_le],
-    simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
-qed "HNatInfinite_SHNat_diff";
-
-Goal "x: HNatInfinite ==> x + (1::hypnat): HNatInfinite";
-by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
-              simpset()));
-qed "HNatInfinite_add_one";
-
-Goal "x: HNatInfinite ==> x - (1::hypnat): HNatInfinite";
-by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
-by (dres_inst_tac [("x","x - (1::hypnat)"),("y","(1::hypnat)")] SHNat_add 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [not_SHNat_HNatInfinite_iff RS sym]));
-qed "HNatInfinite_minus_one";
-
-Goal "x : HNatInfinite ==> EX y. x = y + (1::hypnat)";
-by (res_inst_tac [("x","x - (1::hypnat)")] exI 1);
-by Auto_tac;
-qed "HNatInfinite_is_Suc";
-
-(*---------------------------------------------------------------
-       HNat : the hypernaturals embedded in the hyperreals
-       Obtained using the NS extension of the naturals
- --------------------------------------------------------------*)
- 
-Goalw [HNat_def,starset_def, hypreal_of_nat_def,hypreal_of_real_def] 
-     "hypreal_of_nat N : HNat";
-by Auto_tac;
-by (Ultra_tac 1);
-by (res_inst_tac [("x","N")] exI 1);
-by Auto_tac;  
-qed "HNat_hypreal_of_nat";
-Addsimps [HNat_hypreal_of_nat];
-
-Goalw [HNat_def,starset_def]
-     "[| x: HNat; y: HNat |] ==> x + y: HNat";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
-              simpset() addsimps [hypreal_add]));
-by (Ultra_tac 1);
-by (res_inst_tac [("x","no+noa")] exI 1);
-by Auto_tac;
-qed "HNat_add";
-
-Goalw [HNat_def,starset_def]
-     "[| x: HNat; y: HNat |] ==> x * y: HNat";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
-              simpset() addsimps [hypreal_mult]));
-by (Ultra_tac 1);
-by (res_inst_tac [("x","no*noa")] exI 1);
-by Auto_tac;
-qed "HNat_mult";
-
-(*---------------------------------------------------------------
-    Embedding of the hypernaturals into the hyperreal
- --------------------------------------------------------------*)
-
-(*WARNING: FRAGILE!*)
-Goal "(Ya : hyprel ``{%n. f(n)}) = \
-\     ({n. f n = Ya n} : FreeUltrafilterNat)";
-by Auto_tac;
-qed "lemma_hyprel_FUFN";
-
-Goalw [hypreal_of_hypnat_def]
-      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) = \
-\         Abs_hypreal(hyprel `` {%n. real (X n)})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (auto_tac (claset()
-                  addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
-              simpset() addsimps [lemma_hyprel_FUFN]));
-qed "hypreal_of_hypnat";
-
-Goal "inj(hypreal_of_hypnat)";
-by (rtac injI 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat]));
-qed "inj_hypreal_of_hypnat";
-
-Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)";
-by (auto_tac (claset(),simpset() addsimps [inj_hypreal_of_hypnat RS injD]));
-qed "hypreal_of_hypnat_eq_cancel";
-Addsimps [hypreal_of_hypnat_eq_cancel];
-
-Goal "(hypnat_of_nat n = hypnat_of_nat m) = (n = m)";
-by (auto_tac (claset() addDs [inj_hypnat_of_nat RS injD],
-              simpset()));
-qed "hypnat_of_nat_eq_cancel";
-Addsimps [hypnat_of_nat_eq_cancel];
-
-Goalw [hypnat_zero_def] 
-     "hypreal_of_hypnat 0 = 0";
-by (simp_tac (simpset() addsimps [hypreal_zero_def, hypreal_of_hypnat]) 1);
-qed "hypreal_of_hypnat_zero";
-
-Goalw [hypnat_one_def] 
-     "hypreal_of_hypnat (1::hypnat) = 1";
-by (simp_tac (simpset() addsimps [hypreal_one_def, hypreal_of_hypnat]) 1);
-qed "hypreal_of_hypnat_one";
-
-Goal "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps
-           [hypreal_of_hypnat, hypreal_add,hypnat_add,real_of_nat_add]) 1);
-qed "hypreal_of_hypnat_add";
-Addsimps [hypreal_of_hypnat_add];
-
-Goal "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps
-           [hypreal_of_hypnat, hypreal_mult,hypnat_mult,real_of_nat_mult]) 1);
-qed "hypreal_of_hypnat_mult";
-Addsimps [hypreal_of_hypnat_mult];
-
-Goal "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (asm_simp_tac (simpset() addsimps 
-    [hypreal_of_hypnat,hypreal_less,hypnat_less]) 1);
-qed "hypreal_of_hypnat_less_iff";
-Addsimps [hypreal_of_hypnat_less_iff];
-
-Goal "(hypreal_of_hypnat N = 0) = (N = 0)";
-by (simp_tac (simpset() addsimps [hypreal_of_hypnat_zero RS sym]) 1);
-qed "hypreal_of_hypnat_eq_zero_iff";
-Addsimps [hypreal_of_hypnat_eq_zero_iff];
-
-Goal "ALL n. N <= n ==> N = (0::hypnat)";
-by (dres_inst_tac [("x","0")] spec 1);
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_le,hypnat_zero_def]));
-qed "hypnat_eq_zero";
-Addsimps [hypnat_eq_zero];
-
-Goal "~ (ALL n. n = (0::hypnat))";
-by Auto_tac;
-by (res_inst_tac [("x","(1::hypnat)")] exI 1);
-by (Simp_tac 1);
-qed "hypnat_not_all_eq_zero";
-Addsimps [hypnat_not_all_eq_zero];
-
-Goal "n ~= 0 ==> (n <= (1::hypnat)) = (n = (1::hypnat))";
-by (auto_tac (claset(), simpset() addsimps [hypnat_le_less]));
-qed "hypnat_le_one_eq_one";
-Addsimps [hypnat_le_one_eq_one];
-
-
-
-
-(*MOVE UP*)
-Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
-    HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
-by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
-by Auto_tac;
-by (dres_inst_tac [("x","m + 1")] spec 1);
-by (Ultra_tac 1);
-qed "HNatInfinite_inverse_Infinitesimal";
-Addsimps [HNatInfinite_inverse_Infinitesimal];
-
-Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
-by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
-qed "HNatInfinite_inverse_not_zero";
-Addsimps [HNatInfinite_inverse_not_zero];
-
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -1,83 +1,1070 @@
 (*  Title       : HyperNat.thy
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Explicit construction of hypernaturals using 
-                  ultrafilters
-*) 
+*)
 
-HyperNat = Star + 
+header{*Construction of Hypernaturals using Ultrafilters*}
+
+theory HyperNat = Star:
 
 constdefs
     hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
-    "hypnatrel == {p. EX X Y. p = ((X::nat=>nat),Y) & 
-                       {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}"
+    "hypnatrel == {p. \<exists>X Y. p = ((X::nat=>nat),Y) &
+                       {n::nat. X(n) = Y(n)} \<in> FreeUltrafilterNat}"
 
-typedef hypnat = "UNIV//hypnatrel"              (quotient_def)
+typedef hypnat = "UNIV//hypnatrel"
+    by (auto simp add: quotient_def)
 
-instance
-   hypnat  :: {ord, zero, one, plus, times, minus}
+instance hypnat :: ord ..
+instance hypnat :: zero ..
+instance hypnat :: one ..
+instance hypnat :: plus ..
+instance hypnat :: times ..
+instance hypnat :: minus ..
 
-consts
-  whn       :: hypnat
+consts whn :: hypnat
 
 constdefs
 
   (* embedding the naturals in the hypernaturals *)
-  hypnat_of_nat   :: nat => hypnat
+  hypnat_of_nat   :: "nat => hypnat"
   "hypnat_of_nat m  == Abs_hypnat(hypnatrel``{%n::nat. m})"
 
   (* hypernaturals as members of the hyperreals; the set is defined as  *)
   (* the nonstandard extension of set of naturals embedded in the reals *)
   HNat         :: "hypreal set"
-  "HNat == *s* {n. EX no::nat. n = real no}"
+  "HNat == *s* {n. \<exists>no::nat. n = real no}"
 
   (* the set of infinite hypernatural numbers *)
   HNatInfinite :: "hypnat set"
-  "HNatInfinite == {n. n ~: Nats}"
+  "HNatInfinite == {n. n \<notin> Nats}"
 
-  (* explicit embedding of the hypernaturals in the hyperreals *)    
-  hypreal_of_hypnat :: hypnat => hypreal
-  "hypreal_of_hypnat N  == Abs_hypreal(UN X: Rep_hypnat(N). 
+  (* explicit embedding of the hypernaturals in the hyperreals *)
+  hypreal_of_hypnat :: "hypnat => hypreal"
+  "hypreal_of_hypnat N  == Abs_hypreal(\<Union>X \<in> Rep_hypnat(N).
                                        hyprel``{%n::nat. real (X n)})"
-  
-defs
+
+defs (overloaded)
 
   (** the overloaded constant "Nats" **)
-  
+
   (* set of naturals embedded in the hyperreals*)
-  SNat_def             "Nats == {n. EX N. n = hypreal_of_nat N}"  
+  SNat_def:  "Nats == {n. \<exists>N. n = hypreal_of_nat N}"
 
   (* set of naturals embedded in the hypernaturals*)
-  SHNat_def            "Nats == {n. EX N. n = hypnat_of_nat N}"  
+  SHNat_def: "Nats == {n. \<exists>N. n = hypnat_of_nat N}"
 
   (** hypernatural arithmetic **)
-  
-  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
-  hypnat_one_def       "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
+
+  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(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
+  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})"
 
-  hypnat_mult_def  
-  "P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
+  hypnat_mult_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_minus_def  
-  "P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
+  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_less_def
-  "P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) & 
-                               Y: Rep_hypnat(Q) & 
-                               {n::nat. X n < Y n} : FreeUltrafilterNat"
-  hypnat_le_def
-  "P <= (Q::hypnat) == ~(Q < P)" 
+  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"
 
-end
+  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*}
+
+lemma hypnatrel_iff:
+     "((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
+apply (unfold hypnatrel_def, fast)
+done
+
+lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
+by (unfold hypnatrel_def, auto)
+
+lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
+by (auto simp add: hypnatrel_def eq_commute)
+
+lemma hypnatrel_trans [rule_format (no_asm)]:
+     "(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
+apply (unfold hypnatrel_def, auto, ultra)
+done
+
+lemma equiv_hypnatrel:
+     "equiv UNIV hypnatrel"
+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]
+
+lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
+by (unfold hypnat_def hypnatrel_def quotient_def, blast)
+
+lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
+apply (rule inj_on_inverseI)
+apply (erule Abs_hypnat_inverse)
+done
+
+declare inj_on_Abs_hypnat [THEN inj_on_iff, simp]
+        Abs_hypnat_inverse [simp]
+
+declare equiv_hypnatrel [THEN eq_equiv_class_iff, simp]
+
+declare hypnatrel_iff [iff]
+
+
+lemma inj_Rep_hypnat: "inj(Rep_hypnat)"
+apply (rule inj_on_inverseI)
+apply (rule Rep_hypnat_inverse)
+done
+
+lemma lemma_hypnatrel_refl: "x \<in> hypnatrel `` {x}"
+by (simp add: hypnatrel_def)
+
+declare lemma_hypnatrel_refl [simp]
+
+lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
+apply (unfold hypnat_def)
+apply (auto elim!: quotientE equalityCE)
+done
+
+declare hypnat_empty_not_mem [simp]
+
+lemma Rep_hypnat_nonempty: "Rep_hypnat x \<noteq> {}"
+by (cut_tac x = x in Rep_hypnat, auto)
+
+declare Rep_hypnat_nonempty [simp]
+
+subsection{*@{term hypnat_of_nat}:
+            the Injection from @{typ nat} to @{typ hypnat}*}
+
+lemma inj_hypnat_of_nat: "inj(hypnat_of_nat)"
+apply (rule inj_onI)
+apply (unfold hypnat_of_nat_def)
+apply (drule inj_on_Abs_hypnat [THEN inj_onD])
+apply (rule hypnatrel_in_hypnat)+
+apply (drule eq_equiv_class)
+apply (rule equiv_hypnatrel)
+apply (simp_all split: split_if_asm)
+done
+
+lemma eq_Abs_hypnat:
+    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
+apply (rule_tac x1=z in Rep_hypnat [unfolded hypnat_def, THEN quotientE])
+apply (drule_tac f = Abs_hypnat in arg_cong)
+apply (force simp add: Rep_hypnat_inverse)
+done
+
+subsection{*Hypernat Addition*}
+
+lemma hypnat_add_congruent2:
+     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
+apply (unfold congruent2_def, auto, ultra)
+done
+
+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 hypnat_add_congruent2])
+
+lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
+apply (rule eq_Abs_hypnat [of z])
+apply (rule eq_Abs_hypnat [of w])
+apply (simp add: add_ac hypnat_add)
+done
+
+lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
+apply (rule eq_Abs_hypnat [of z1])
+apply (rule eq_Abs_hypnat [of z2])
+apply (rule eq_Abs_hypnat [of z3])
+apply (simp add: hypnat_add nat_add_assoc)
+done
+
+lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: hypnat_zero_def hypnat_add)
+done
+
+instance hypnat :: plus_ac0
+  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:
+    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
+apply (unfold congruent2_def, auto, ultra)
+done
+
+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 hypnat_minus_congruent2])
+
+lemma hypnat_minus_zero: "z - z = (0::hypnat)"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: hypnat_zero_def hypnat_minus)
+done
+
+lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_minus hypnat_zero_def)
+done
+
+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 (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
+done
+
+declare hypnat_add_is_0 [iff]
+
+lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
+apply (rule eq_Abs_hypnat [of i])
+apply (rule eq_Abs_hypnat [of j])
+apply (rule eq_Abs_hypnat [of k])
+apply (simp add: hypnat_minus hypnat_add diff_diff_left)
+done
+
+lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
+by (simp add: hypnat_diff_diff_left hypnat_add_commute)
+
+lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_minus hypnat_add)
+done
+declare hypnat_diff_add_inverse [simp]
+
+lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_minus hypnat_add)
+done
+declare hypnat_diff_add_inverse2 [simp]
+
+lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
+apply (rule eq_Abs_hypnat [of k])
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_minus hypnat_add)
+done
+declare hypnat_diff_cancel [simp]
+
+lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
+by (simp add: hypnat_add_commute [of _ k])
+declare hypnat_diff_cancel2 [simp]
+
+lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
+done
+declare hypnat_diff_add_0 [simp]
+
+
+subsection{*Hyperreal Multiplication*}
+
+lemma hypnat_mult_congruent2:
+    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
+by (unfold 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 hypnat_mult_congruent2])
+
+lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
+apply (rule eq_Abs_hypnat [of z])
+apply (rule eq_Abs_hypnat [of w])
+apply (simp add: hypnat_mult mult_ac)
+done
+
+lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
+apply (rule eq_Abs_hypnat [of z1])
+apply (rule eq_Abs_hypnat [of z2])
+apply (rule eq_Abs_hypnat [of z3])
+apply (simp add: hypnat_mult mult_assoc)
+done
+
+lemma hypnat_mult_1: "(1::hypnat) * z = z"
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: hypnat_mult hypnat_one_def)
+done
+
+lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
+apply (rule eq_Abs_hypnat [of k])
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
+done
+
+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_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
+apply (rule eq_Abs_hypnat [of z1])
+apply (rule eq_Abs_hypnat [of z2])
+apply (rule eq_Abs_hypnat [of w])
+apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
+done
+
+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)
+
+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)
+declare hypnat_zero_not_eq_one [THEN not_sym, simp]
+
+
+text{*The Hypernaturals Form A Semiring*}
+instance hypnat :: semiring
+proof
+  fix i j k :: hypnat
+  show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc)
+  show "i + j = j + i" by (rule hypnat_add_commute)
+  show "0 + i = i" by simp
+  show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc)
+  show "i * j = j * i" by (rule hypnat_mult_commute)
+  show "1 * i = i" by (rule hypnat_mult_1)
+  show "(i + j) * k = i * k + j * k" by (simp add: hypnat_add_mult_distrib)
+  show "0 \<noteq> (1::hypnat)" by (rule hypnat_zero_not_eq_one)
+  assume "k+i = k+j"
+  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})) =
+       ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
+apply (unfold hypnat_le_def)
+apply (auto intro!: lemma_hypnatrel_refl, ultra)
+done
+
+lemma hypnat_le_refl: "w \<le> (w::hypnat)"
+apply (rule eq_Abs_hypnat [of w])
+apply (simp add: hypnat_le)
+done
+
+lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
+apply (rule eq_Abs_hypnat [of i])
+apply (rule eq_Abs_hypnat [of j])
+apply (rule eq_Abs_hypnat [of k])
+apply (simp add: hypnat_le, ultra)
+done
+
+lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
+apply (rule eq_Abs_hypnat [of z])
+apply (rule eq_Abs_hypnat [of w])
+apply (simp add: hypnat_le, ultra)
+done
+
+(* 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)
+
+instance hypnat :: order
+proof qed
+ (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 (rule eq_Abs_hypnat [of z])
+apply (rule eq_Abs_hypnat [of w])
+apply (auto simp add: hypnat_le, ultra)
+done
+
+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 (rule eq_Abs_hypnat [of x])
+apply (rule eq_Abs_hypnat [of y])
+apply (rule eq_Abs_hypnat [of z])
+apply (auto simp add: hypnat_le hypnat_add)
+done
+
+lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
+apply (rule eq_Abs_hypnat [of x])
+apply (rule eq_Abs_hypnat [of y])
+apply (rule eq_Abs_hypnat [of z])
+apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
+apply (auto simp add: hypnat_le, ultra)
+done
+
+
+subsection{*The Hypernaturals Form an Ordered Semiring*}
+
+instance hypnat :: ordered_semiring
+proof
+  fix x y z :: hypnat
+  show "0 < (1::hypnat)"
+    by (simp add: hypnat_zero_def hypnat_one_def linorder_not_le [symmetric],
+        simp add: hypnat_le)
+  show "x \<le> y ==> z + x \<le> z + y"
+    by (rule hypnat_add_left_mono)
+  show "x < y ==> 0 < z ==> z * x < z * y"
+    by (simp add: hypnat_mult_less_mono2)
+qed
+
+lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
+done
+
+
+subsection{*Theorems for Ordering*}
+
+lemma hypnat_less:
+      "(Abs_hypnat(hypnatrel``{%n. X n}) < Abs_hypnat(hypnatrel``{%n. Y n})) =
+       ({n. X n < Y n} \<in> FreeUltrafilterNat)"
+apply (auto simp add: hypnat_le  linorder_not_le [symmetric])
+apply (ultra+)
+done
+
+lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypnat_zero_def hypnat_less)
+done
+
+lemma hypnat_less_one [iff]:
+      "(n < (1::hypnat)) = (n=0)"
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
+done
+
+lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
+done
+
+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)
+
+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_add_self_le [simp]: "(x::hypnat) \<le> n + x"
+by (insert add_right_mono [of 0 n x], simp)
+
+lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
+by (insert add_strict_left_mono [OF zero_less_one], auto)
+
+lemma hypnat_neq0_conv [iff]: "(n \<noteq> 0) = (0 < (n::hypnat))"
+by (simp add: order_less_le)
+
+lemma hypnat_gt_zero_iff: "((0::hypnat) < n) = ((1::hypnat) \<le> n)"
+by (auto simp add: linorder_not_less [symmetric])
+
+lemma hypnat_gt_zero_iff2: "(0 < n) = (\<exists>m. n = m + (1::hypnat))"
+apply safe
+ apply (rule_tac x = "n - (1::hypnat) " in exI)
+ apply (simp add: hypnat_gt_zero_iff) 
+apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto) 
+done
+
+subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and 
+      Order Properties*}
+
+lemma hypnat_of_nat_add:
+      "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
+by (simp add: hypnat_of_nat_def hypnat_add)
+
+lemma hypnat_of_nat_minus:
+      "hypnat_of_nat ((z::nat) - w) = hypnat_of_nat z - hypnat_of_nat w"
+by (simp add: hypnat_of_nat_def hypnat_minus)
+
+lemma hypnat_of_nat_mult:
+      "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
+by (simp add: hypnat_of_nat_def hypnat_mult)
+
+lemma hypnat_of_nat_less_iff [simp]:
+      "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
+by (simp add: hypnat_less hypnat_of_nat_def)
+
+lemma hypnat_of_nat_le_iff [simp]:
+      "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
+by (simp add: linorder_not_less [symmetric])
+
+lemma hypnat_of_nat_one: "hypnat_of_nat (Suc 0) = (1::hypnat)"
+by (simp add: hypnat_of_nat_def hypnat_one_def)
+
+lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
+by (simp add: hypnat_of_nat_def hypnat_zero_def)
+
+lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
+by (auto intro: FreeUltrafilterNat_P 
+         simp add: hypnat_of_nat_def hypnat_zero_def)
+
+lemma hypnat_of_nat_Suc:
+     "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
+by (auto simp add: hypnat_add hypnat_of_nat_def hypnat_one_def)
+
+
+subsection{*Existence of an Infinite Hypernatural Number*}
+
+lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
+by auto
+
+lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"
+by (simp add: hypnat_omega_def)
+
+text{*Existence of infinite number not corresponding to any natural number
+follows because member @{term FreeUltrafilterNat} is not finite.
+See @{text HyperDef.thy} for similar argument.*}
+
+lemma not_ex_hypnat_of_nat_eq_omega:
+      "~ (\<exists>x. hypnat_of_nat x = whn)"
+apply (simp add: hypnat_omega_def hypnat_of_nat_def)
+apply (auto dest: FreeUltrafilterNat_not_finite)
+done
+
+lemma hypnat_of_nat_not_eq_omega: "hypnat_of_nat x \<noteq> whn"
+by (cut_tac not_ex_hypnat_of_nat_eq_omega, auto)
+declare hypnat_of_nat_not_eq_omega [THEN not_sym, simp]
+
+
+subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
+
+(* Infinite hypernatural not in embedded Nats *)
+lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
+by (simp add: SHNat_def)
+
+(*-----------------------------------------------------------------------
+     Closure laws for members of (embedded) set standard naturals Nats
+ -----------------------------------------------------------------------*)
+lemma SHNat_add:
+     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x + y \<in> Nats"
+apply (simp add: SHNat_def, safe)
+apply (rule_tac x = "N + Na" in exI)
+apply (simp add: hypnat_of_nat_add)
+done
+
+lemma SHNat_minus:
+     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x - y \<in> Nats"
+apply (simp add: SHNat_def, safe)
+apply (rule_tac x = "N - Na" in exI)
+apply (simp add: hypnat_of_nat_minus)
+done
+
+lemma SHNat_mult:
+     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x * y \<in> Nats"
+apply (simp add: SHNat_def, safe)
+apply (rule_tac x = "N * Na" in exI)
+apply (simp (no_asm) add: hypnat_of_nat_mult)
+done
+
+lemma SHNat_add_cancel: "!!x::hypnat. [| x + y \<in> Nats; y \<in> Nats |] ==> x \<in> Nats"
+by (drule_tac x = "x+y" in SHNat_minus, auto)
+
+lemma SHNat_hypnat_of_nat [simp]: "hypnat_of_nat x \<in> Nats"
+by (simp add: SHNat_def, blast)
+
+lemma SHNat_hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) \<in> Nats"
+by simp
+
+lemma SHNat_hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 \<in> Nats"
+by simp
+
+lemma SHNat_one [simp]: "(1::hypnat) \<in> Nats"
+by (simp add: hypnat_of_nat_one [symmetric])
+
+lemma SHNat_zero [simp]: "(0::hypnat) \<in> Nats"
+by (simp add: hypnat_of_nat_zero [symmetric])
+
+lemma SHNat_iff: "(x \<in> Nats) = (\<exists>y. x = hypnat_of_nat  y)"
+by (simp add: SHNat_def)
+
+lemma SHNat_hypnat_of_nat_iff:
+      "Nats = hypnat_of_nat ` (UNIV::nat set)"
+by (auto simp add: SHNat_def)
+
+lemma leSuc_Un_eq: "{n. n \<le> Suc m} = {n. n \<le> m} Un {n. n = Suc m}"
+by (auto simp add: le_Suc_eq)
+
+lemma finite_nat_le_segment: "finite {n::nat. n \<le> m}"
+apply (induct_tac "m")
+apply (auto simp add: leSuc_Un_eq)
+done
+
+lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
+by (insert finite_nat_le_segment
+                [THEN FreeUltrafilterNat_finite, 
+                 THEN FreeUltrafilterNat_Compl_mem, of m], ultra)
+
+(*????hyperdef*)
+lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
+apply (drule FreeUltrafilterNat_finite)  
+apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
+done
+
+lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
+by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
+
+lemma hypnat_omega_gt_SHNat:
+     "n \<in> Nats ==> n < whn"
+apply (auto simp add: SHNat_def hypnat_of_nat_def hypnat_less_def 
+                      hypnat_le_def hypnat_omega_def)
+ 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
+
+lemma hypnat_of_nat_less_whn: "hypnat_of_nat n < whn"
+by (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"], auto)
+declare hypnat_of_nat_less_whn [simp]
+
+lemma hypnat_of_nat_le_whn: "hypnat_of_nat n \<le> whn"
+by (rule hypnat_of_nat_less_whn [THEN order_less_imp_le])
+declare hypnat_of_nat_le_whn [simp]
+
+lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
+by (simp add: hypnat_omega_gt_SHNat)
+
+lemma hypnat_one_less_hypnat_omega [simp]: "(1::hypnat) < whn"
+by (simp add: hypnat_omega_gt_SHNat)
+
+
+subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
+
+lemma HNatInfinite_whn: "whn \<in> HNatInfinite"
+by (simp add: HNatInfinite_def SHNat_def)
+declare HNatInfinite_whn [simp]
+
+lemma SHNat_not_HNatInfinite: "x \<in> Nats ==> x \<notin> HNatInfinite"
+by (simp add: HNatInfinite_def)
+
+lemma not_HNatInfinite_SHNat: "x \<notin> HNatInfinite ==> x \<in> Nats"
+by (simp add: HNatInfinite_def)
+
+lemma not_SHNat_HNatInfinite: "x \<notin> Nats ==> x \<in> HNatInfinite"
+by (simp add: HNatInfinite_def)
+
+lemma HNatInfinite_not_SHNat: "x \<in> HNatInfinite ==> x \<notin> Nats"
+by (simp add: HNatInfinite_def)
+
+lemma SHNat_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
+by (blast intro!: SHNat_not_HNatInfinite not_HNatInfinite_SHNat)
+
+lemma not_SHNat_HNatInfinite_iff: "(x \<notin> Nats) = (x \<in> HNatInfinite)"
+by (blast intro!: not_SHNat_HNatInfinite HNatInfinite_not_SHNat)
+
+lemma SHNat_HNatInfinite_disj: "x \<in> Nats | x \<in> HNatInfinite"
+by (simp add: SHNat_not_HNatInfinite_iff)
+
+
+subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
+@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
+
+(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
+lemma HNatInfinite_FreeUltrafilterNat_lemma: "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
+      ==> {n. N < f n} \<in> FreeUltrafilterNat"
+apply (induct_tac "N")
+apply (drule_tac x = 0 in spec)
+apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
+apply (drule_tac x = "Suc n" in spec, ultra)
+done
+
+lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
+apply (unfold HNatInfinite_def SHNat_def hypnat_of_nat_def, safe)
+apply (drule_tac [2] x = "Abs_hypnat (hypnatrel `` {%n. N}) " in bspec)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (auto simp add: hypnat_less)
+apply (auto  elim: HNatInfinite_FreeUltrafilterNat_lemma 
+           simp add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
+done
+
+subsection{*Alternative Characterization of @{term HNatInfinite} using 
+Free Ultrafilter*}
+
+lemma HNatInfinite_FreeUltrafilterNat:
+     "x \<in> HNatInfinite 
+      ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
+apply (rule eq_Abs_hypnat [of x])
+apply (auto simp add: HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
+apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
+apply (drule_tac x = "hypnat_of_nat u" in bspec, simp) 
+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
+      ==> x \<in> HNatInfinite"
+apply (rule eq_Abs_hypnat [of x])
+apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
+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)"
+apply (blast intro: HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite)
+done
+
+lemma HNatInfinite_gt_one: "x \<in> HNatInfinite ==> (1::hypnat) < x"
+by (auto simp add: HNatInfinite_iff)
+declare HNatInfinite_gt_one [simp]
+
+lemma zero_not_mem_HNatInfinite: "0 \<notin> HNatInfinite"
+apply (auto simp add: HNatInfinite_iff)
+apply (drule_tac a = " (1::hypnat) " in equals0D)
+apply simp
+done
+declare zero_not_mem_HNatInfinite [simp]
+
+lemma HNatInfinite_not_eq_zero: "x \<in> HNatInfinite ==> 0 < x"
+apply (drule HNatInfinite_gt_one) 
+apply (auto simp add: order_less_trans [OF zero_less_one])
+done
+
+lemma HNatInfinite_ge_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) \<le> x"
+by (blast intro: order_less_imp_le HNatInfinite_gt_one)
+
+
+subsection{*Closure Rules*}
+
+lemma HNatInfinite_add: "[| x \<in> HNatInfinite; y \<in> HNatInfinite |]
+            ==> x + y \<in> HNatInfinite"
+apply (auto simp add: HNatInfinite_iff)
+apply (drule bspec, assumption)
+apply (drule bspec [OF _ SHNat_zero])
+apply (drule add_strict_mono, assumption, simp)
+done
+
+lemma HNatInfinite_SHNat_add: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
+apply (rule ccontr, drule not_HNatInfinite_SHNat)
+apply (drule_tac x = "x + y" in SHNat_minus)
+apply (auto simp add: SHNat_not_HNatInfinite_iff)
+done
+
+lemma HNatInfinite_SHNat_diff: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x - y \<in> HNatInfinite"
+apply (rule ccontr, drule not_HNatInfinite_SHNat)
+apply (drule_tac x = "x - y" in SHNat_add)
+apply (subgoal_tac [2] "y \<le> x")
+apply (auto dest!: hypnat_le_add_diff_inverse2 simp add: not_SHNat_HNatInfinite_iff [symmetric])
+apply (auto intro!: order_less_imp_le simp add: not_SHNat_HNatInfinite_iff HNatInfinite_iff)
+done
+
+lemma HNatInfinite_add_one: "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
+by (auto intro: HNatInfinite_SHNat_add)
+
+lemma HNatInfinite_minus_one: "x \<in> HNatInfinite ==> x - (1::hypnat) \<in> HNatInfinite"
+apply (rule ccontr, drule not_HNatInfinite_SHNat)
+apply (drule_tac x = "x - (1::hypnat) " and y = " (1::hypnat) " in SHNat_add)
+apply (auto simp add: not_SHNat_HNatInfinite_iff [symmetric])
+done
+
+lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
+apply (rule_tac x = "x - (1::hypnat) " in exI)
+apply auto
+done
+
+
+subsection{*@{term HNat}: the Hypernaturals Embedded in the Hyperreals*}
+
+text{*Obtained using the nonstandard extension of the naturals*}
+
+lemma HNat_hypreal_of_nat: "hypreal_of_nat N \<in> HNat"
+apply (simp add: HNat_def starset_def hypreal_of_nat_def hypreal_of_real_def, auto, ultra)
+apply (rule_tac x = N in exI, auto)
+done
+declare HNat_hypreal_of_nat [simp]
+
+lemma HNat_add: "[| x \<in> HNat; y \<in> HNat |] ==> x + y \<in> HNat"
+apply (simp add: HNat_def starset_def)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_add, ultra)
+apply (rule_tac x = "no+noa" in exI, auto)
+done
+
+lemma HNat_mult:
+     "[| x \<in> HNat; y \<in> HNat |] ==> x * y \<in> HNat"
+apply (simp add: HNat_def starset_def)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_mult, ultra)
+apply (rule_tac x = "no*noa" in exI, auto)
+done
+
+
+subsection{*Embedding of the Hypernaturals into the Hyperreals*}
+
+(*WARNING: FRAGILE!*)
+lemma lemma_hyprel_FUFN: "(Ya \<in> hyprel ``{%n. f(n)}) =
+      ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
+apply auto
+done
+
+lemma hypreal_of_hypnat:
+      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
+       Abs_hypreal(hyprel `` {%n. real (X n)})"
+apply (simp add: hypreal_of_hypnat_def)
+apply (rule_tac f = Abs_hypreal in arg_cong)
+apply (auto elim: FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] 
+       simp add: lemma_hyprel_FUFN)
+done
+
+lemma inj_hypreal_of_hypnat: "inj(hypreal_of_hypnat)"
+apply (rule inj_onI)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = y in eq_Abs_hypnat)
+apply (auto simp add: hypreal_of_hypnat)
+done
+
+declare inj_hypreal_of_hypnat [THEN inj_eq, simp]
+declare inj_hypnat_of_nat [THEN inj_eq, simp]
+
+lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
+by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)
+
+lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
+by (simp add: hypnat_one_def hypreal_one_def hypreal_of_hypnat)
+
+lemma hypreal_of_hypnat_add [simp]:
+     "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
+apply (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+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 (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+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 (rule eq_Abs_hypnat [of m])
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
+done
+
+lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
+by (simp add: hypreal_of_hypnat_zero [symmetric])
+declare hypreal_of_hypnat_eq_zero_iff [simp]
+
+lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
+apply (rule eq_Abs_hypnat [of n])
+apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
+done
+
+(*????DELETE??*)
+lemma hypnat_eq_zero: "\<forall>n. N \<le> n ==> N = (0::hypnat)"
+apply (drule_tac x = 0 in spec)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (auto simp add: hypnat_le hypnat_zero_def)
+done
+
+(*????DELETE??*)
+lemma hypnat_not_all_eq_zero: "~ (\<forall>n. n = (0::hypnat))"
+by auto
+
+(*????DELETE??*)
+lemma hypnat_le_one_eq_one: "n \<noteq> 0 ==> (n \<le> (1::hypnat)) = (n = (1::hypnat))"
+by (auto simp add: order_le_less)
+
+(*WHERE DO THESE BELONG???*)
+lemma HNatInfinite_inverse_Infinitesimal: "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypreal_of_hypnat hypreal_inverse HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
+apply (drule_tac x = "m + 1" in spec, ultra)
+done
+declare HNatInfinite_inverse_Infinitesimal [simp]
+
+lemma HNatInfinite_inverse_not_zero: "n \<in> HNatInfinite ==> hypreal_of_hypnat n \<noteq> 0"
+by (simp add: HNatInfinite_not_eq_zero)
+
+
+
+ML
+{*
+val hypnat_of_nat_def = thm"hypnat_of_nat_def";
+val HNat_def = thm"HNat_def";
+val HNatInfinite_def = thm"HNatInfinite_def";
+val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
+val SNat_def = thm"SNat_def";
+val SHNat_def = thm"SHNat_def";
+val hypnat_zero_def = thm"hypnat_zero_def";
+val hypnat_one_def = thm"hypnat_one_def";
+val hypnat_omega_def = thm"hypnat_omega_def";
+
+val hypnatrel_iff = thm "hypnatrel_iff";
+val hypnatrel_refl = thm "hypnatrel_refl";
+val hypnatrel_sym = thm "hypnatrel_sym";
+val hypnatrel_trans = thm "hypnatrel_trans";
+val equiv_hypnatrel = thm "equiv_hypnatrel";
+val equiv_hypnatrel_iff = thms "equiv_hypnatrel_iff";
+val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
+val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat";
+val inj_Rep_hypnat = thm "inj_Rep_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 inj_hypnat_of_nat = thm "inj_hypnat_of_nat";
+val eq_Abs_hypnat = thm "eq_Abs_hypnat";
+val hypnat_add_congruent2 = thm "hypnat_add_congruent2";
+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 = thm "hypnat_minus";
+val hypnat_minus_zero = thm "hypnat_minus_zero";
+val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
+val hypnat_add_is_0 = thm "hypnat_add_is_0";
+val hypnat_diff_diff_left = thm "hypnat_diff_diff_left";
+val hypnat_diff_commute = thm "hypnat_diff_commute";
+val hypnat_diff_add_inverse = thm "hypnat_diff_add_inverse";
+val hypnat_diff_add_inverse2 = thm "hypnat_diff_add_inverse2";
+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 = thm "hypnat_mult";
+val hypnat_mult_commute = thm "hypnat_mult_commute";
+val hypnat_mult_assoc = thm "hypnat_mult_assoc";
+val hypnat_mult_1 = thm "hypnat_mult_1";
+val hypnat_diff_mult_distrib = thm "hypnat_diff_mult_distrib";
+val hypnat_diff_mult_distrib2 = thm "hypnat_diff_mult_distrib2";
+val hypnat_add_mult_distrib = thm "hypnat_add_mult_distrib";
+val hypnat_add_mult_distrib2 = thm "hypnat_add_mult_distrib2";
+val hypnat_zero_not_eq_one = thm "hypnat_zero_not_eq_one";
+val hypnat_le = thm "hypnat_le";
+val hypnat_le_refl = thm "hypnat_le_refl";
+val hypnat_le_trans = thm "hypnat_le_trans";
+val hypnat_le_anti_sym = thm "hypnat_le_anti_sym";
+val hypnat_less_le = thm "hypnat_less_le";
+val hypnat_le_linear = thm "hypnat_le_linear";
+val hypnat_add_left_mono = thm "hypnat_add_left_mono";
+val hypnat_mult_less_mono2 = thm "hypnat_mult_less_mono2";
+val hypnat_mult_is_0 = thm "hypnat_mult_is_0";
+val hypnat_less = thm "hypnat_less";
+val hypnat_not_less0 = thm "hypnat_not_less0";
+val hypnat_less_one = thm "hypnat_less_one";
+val hypnat_add_diff_inverse = thm "hypnat_add_diff_inverse";
+val hypnat_le_add_diff_inverse = thm "hypnat_le_add_diff_inverse";
+val hypnat_le_add_diff_inverse2 = thm "hypnat_le_add_diff_inverse2";
+val hypnat_le0 = thm "hypnat_le0";
+val hypnat_add_self_le = thm "hypnat_add_self_le";
+val hypnat_add_one_self_less = thm "hypnat_add_one_self_less";
+val hypnat_neq0_conv = thm "hypnat_neq0_conv";
+val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
+val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
+val hypnat_of_nat_add = thm "hypnat_of_nat_add";
+val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
+val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
+val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
+val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
+val hypnat_of_nat_one = thm "hypnat_of_nat_one";
+val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
+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 not_ex_hypnat_of_nat_eq_omega = thm "not_ex_hypnat_of_nat_eq_omega";
+val hypnat_of_nat_not_eq_omega = thm "hypnat_of_nat_not_eq_omega";
+val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
+val SHNat_add = thm "SHNat_add";
+val SHNat_minus = thm "SHNat_minus";
+val SHNat_mult = thm "SHNat_mult";
+val SHNat_add_cancel = thm "SHNat_add_cancel";
+val SHNat_hypnat_of_nat = thm "SHNat_hypnat_of_nat";
+val SHNat_hypnat_of_nat_one = thm "SHNat_hypnat_of_nat_one";
+val SHNat_hypnat_of_nat_zero = thm "SHNat_hypnat_of_nat_zero";
+val SHNat_one = thm "SHNat_one";
+val SHNat_zero = thm "SHNat_zero";
+val SHNat_iff = thm "SHNat_iff";
+val SHNat_hypnat_of_nat_iff = thm "SHNat_hypnat_of_nat_iff";
+val leSuc_Un_eq = thm "leSuc_Un_eq";
+val finite_nat_le_segment = thm "finite_nat_le_segment";
+val lemma_unbounded_set = thm "lemma_unbounded_set";
+val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
+val Compl_Collect_le = thm "Compl_Collect_le";
+val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
+val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
+val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
+val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
+val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
+val HNatInfinite_whn = thm "HNatInfinite_whn";
+val SHNat_not_HNatInfinite = thm "SHNat_not_HNatInfinite";
+val not_HNatInfinite_SHNat = thm "not_HNatInfinite_SHNat";
+val not_SHNat_HNatInfinite = thm "not_SHNat_HNatInfinite";
+val HNatInfinite_not_SHNat = thm "HNatInfinite_not_SHNat";
+val SHNat_not_HNatInfinite_iff = thm "SHNat_not_HNatInfinite_iff";
+val not_SHNat_HNatInfinite_iff = thm "not_SHNat_HNatInfinite_iff";
+val SHNat_HNatInfinite_disj = thm "SHNat_HNatInfinite_disj";
+val HNatInfinite_FreeUltrafilterNat_lemma = thm "HNatInfinite_FreeUltrafilterNat_lemma";
+val HNatInfinite_iff = thm "HNatInfinite_iff";
+val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
+val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
+val HNatInfinite_FreeUltrafilterNat_iff = thm "HNatInfinite_FreeUltrafilterNat_iff";
+val HNatInfinite_gt_one = thm "HNatInfinite_gt_one";
+val zero_not_mem_HNatInfinite = thm "zero_not_mem_HNatInfinite";
+val HNatInfinite_not_eq_zero = thm "HNatInfinite_not_eq_zero";
+val HNatInfinite_ge_one = thm "HNatInfinite_ge_one";
+val HNatInfinite_add = thm "HNatInfinite_add";
+val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
+val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
+val HNatInfinite_add_one = thm "HNatInfinite_add_one";
+val HNatInfinite_minus_one = thm "HNatInfinite_minus_one";
+val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
+val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
+val HNat_add = thm "HNat_add";
+val HNat_mult = thm "HNat_mult";
+val lemma_hyprel_FUFN = thm "lemma_hyprel_FUFN";
+val hypreal_of_hypnat = thm "hypreal_of_hypnat";
+val inj_hypreal_of_hypnat = thm "inj_hypreal_of_hypnat";
+val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
+val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
+val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
+val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
+val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
+val hypreal_of_hypnat_eq_zero_iff = thm "hypreal_of_hypnat_eq_zero_iff";
+val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
+val hypnat_eq_zero = thm "hypnat_eq_zero";
+val hypnat_not_all_eq_zero = thm "hypnat_not_all_eq_zero";
+val hypnat_le_one_eq_one = thm "hypnat_le_one_eq_one";
+val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
+val HNatInfinite_inverse_not_zero = thm "HNatInfinite_inverse_not_zero";
+*}
+
+end
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperOrd.thy
--- a/src/HOL/Hyperreal/HyperOrd.thy	Thu Jan 29 16:51:17 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-theory HyperOrd = HyperDef:
-
-
-
-ML
-{*
-*}
-
-end
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -6,23 +6,7 @@
 
 header{*Exponentials on the Hyperreals*}
 
-theory HyperPow = HRealAbs + HyperNat + RealPow:
-
-instance hypnat :: order
-  by (intro_classes,
-      (assumption | 
-       rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+)
-
-                          
-text{*Type @{typ hypnat} is linearly ordered*}
-instance hypnat :: linorder 
-  by (intro_classes, rule hypnat_le_linear)
-
-instance hypnat :: plus_ac0
-  by (intro_classes,
-      (assumption | 
-       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
-
+theory HyperPow = HyperArith + HyperNat + RealPow:
 
 instance hypreal :: power ..
 
@@ -57,12 +41,10 @@
 done
 
 lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
-apply (simp add: power_abs); 
-done
+by (simp add: power_abs)
 
 lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
-apply (auto simp add: zero_le_mult_iff)
-done
+by (auto simp add: zero_le_mult_iff)
 declare hrealpow_two_le [simp]
 
 lemma hrealpow_two_le_add_order:
@@ -85,8 +67,7 @@
 text{*FIXME: DELETE THESE*}
 lemma hypreal_three_squares_add_zero_iff:
      "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
-apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff)
-apply auto
+apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
 done
 
 lemma hrealpow_three_squares_add_zero_iff [simp]:
@@ -105,24 +86,19 @@
 lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
 apply (induct_tac "n")
 apply (auto simp add: hypreal_of_nat_Suc left_distrib)
-apply (cut_tac n = "n" in two_hrealpow_ge_one)
-apply arith
+apply (cut_tac n = n in two_hrealpow_ge_one, arith)
 done
 declare two_hrealpow_gt [simp] 
 
 lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
-apply (induct_tac "n")
-apply auto
-done
+by (induct_tac "n", auto)
 
 lemma double_lemma: "n+n = (2*n::nat)"
-apply auto
-done
+by auto
 
 (*ugh: need to get rid fo the n+n*)
 lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
-apply (auto simp add: double_lemma hrealpow_minus_one)
-done
+by (auto simp add: double_lemma hrealpow_minus_one)
 declare hrealpow_minus_one2 [simp]
 
 lemma hrealpow:
@@ -163,25 +139,23 @@
      "congruent hyprel
      (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
 apply (unfold congruent_def)
-apply (auto intro!: ext)
-apply fuf+
+apply (auto intro!: ext, fuf+)
 done
 
 lemma hyperpow:
   "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
    Abs_hypreal(hyprel``{%n. X n ^ Y n})"
 apply (unfold hyperpow_def)
-apply (rule_tac f = "Abs_hypreal" in arg_cong)
+apply (rule_tac f = Abs_hypreal in arg_cong)
 apply (auto intro!: lemma_hyprel_refl bexI 
            simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
-                     hyperpow_congruent)
-apply fuf
+                     hyperpow_congruent, fuf)
 done
 
 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_hypnat)
 apply (auto simp add: hyperpow hypnat_add)
 done
 declare hyperpow_zero [simp]
@@ -189,39 +163,38 @@
 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)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 apply (auto simp add: hyperpow)
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply ultra
+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)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 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 (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 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 (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "m" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = m in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
 done
 
 lemma hyperpow_one: "r pow (1::hypnat) = r"
 apply (unfold hypnat_one_def)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = r in eq_Abs_hypreal)
 apply (auto simp add: hyperpow)
 done
 declare hyperpow_one [simp]
@@ -229,38 +202,38 @@
 lemma hyperpow_two:
      "r pow ((1::hypnat) + (1::hypnat)) = r * r"
 apply (unfold hypnat_one_def)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = r in eq_Abs_hypreal)
 apply (auto simp add: hyperpow hypnat_add hypreal_mult)
 done
 
 lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
 apply (simp add: hypreal_zero_def)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 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)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 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)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply (rule_tac z = "y" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
 apply (auto simp add: hyperpow hypreal_le hypreal_less)
-apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption)
+apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
 apply (auto intro: power_mono)
 done
 
 lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
-apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_hypnat)
 apply (auto simp add: hypreal_one_def hyperpow)
 done
 declare hyperpow_eq_one [simp]
@@ -268,28 +241,24 @@
 lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
 apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
 apply simp
-apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = n in eq_Abs_hypnat)
 apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
 done
 declare hrabs_hyperpow_minus_one [simp]
 
 lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
-apply (rule_tac z = "s" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
+apply (rule_tac z = s in eq_Abs_hypreal)
 apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
 done
 
 lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
-apply (auto simp add: hyperpow_two zero_le_mult_iff)
-done
+by (auto simp add: hyperpow_two zero_le_mult_iff)
 declare hyperpow_two_le [simp]
 
-lemma hrabs_hyperpow_two:
-     "abs(x pow (1 + 1)) = x pow (1 + 1)"
-apply (simp (no_asm) add: hrabs_eqI1)
-done
-declare hrabs_hyperpow_two [simp]
+lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
+by (simp add: hrabs_def hyperpow_two_le)
 
 lemma hyperpow_two_hrabs:
      "abs(x) pow (1 + 1)  = x pow (1 + 1)"
@@ -301,8 +270,7 @@
      "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
 apply (auto simp add: hyperpow_two)
 apply (rule_tac y = "1*1" in order_le_less_trans)
-apply (rule_tac [2] hypreal_mult_less_mono)
-apply auto
+apply (rule_tac [2] hypreal_mult_less_mono, auto)
 done
 
 lemma hyperpow_two_ge_one:
@@ -312,8 +280,7 @@
 
 lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
 apply (rule_tac y = "1 pow n" in order_trans)
-apply (rule_tac [2] hyperpow_le)
-apply auto
+apply (rule_tac [2] hyperpow_le, auto)
 done
 declare two_hyperpow_ge_one [simp]
 
@@ -322,21 +289,21 @@
 apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
 apply simp
 apply (simp only: hypreal_one_def)
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus)
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus
+                      left_distrib)
 done
 declare hyperpow_minus_one2 [simp]
 
 lemma hyperpow_less_le:
      "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
-apply (rule_tac z = "n" in eq_Abs_hypnat)
-apply (rule_tac z = "N" in eq_Abs_hypnat)
-apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = n in eq_Abs_hypnat)
+apply (rule_tac z = N in eq_Abs_hypnat)
+apply (rule_tac z = r in eq_Abs_hypreal)
 apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
             hypreal_zero_def hypreal_one_def)
 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
-apply (erule FreeUltrafilterNat_Int)
-apply assumption; 
+apply (erule FreeUltrafilterNat_Int, assumption)
 apply (auto intro: power_decreasing)
 done
 
@@ -358,14 +325,12 @@
 declare hyperpow_SReal [simp]
 
 lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
-apply (drule HNatInfinite_is_Suc)
-apply auto
-done
+by (drule HNatInfinite_is_Suc, auto)
 declare hyperpow_zero_HNatInfinite [simp]
 
 lemma hyperpow_le_le:
      "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
-apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq)
+apply (drule order_le_less [of n, THEN iffD1])
 apply (auto intro: hyperpow_less_le)
 done
 
@@ -385,14 +350,13 @@
 lemma Infinitesimal_hyperpow:
      "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
 apply (rule hrabs_le_Infinitesimal)
-apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
-apply auto
+apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
 done
 
 lemma hrealpow_hyperpow_Infinitesimal_iff:
      "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
 apply (unfold hypnat_of_nat_def)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: hrealpow hyperpow)
 done
 
@@ -400,8 +364,8 @@
      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 by (force intro!: Infinitesimal_hyperpow
           simp add: hrealpow_hyperpow_Infinitesimal_iff 
-                    hypnat_of_nat_less_iff hypnat_of_nat_zero
-          simp del: hypnat_of_nat_less_iff [symmetric])
+                    hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
+          simp del: hypnat_of_nat_less_iff)
 
 ML
 {*
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -5,7 +5,7 @@
 
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
-theory NSA = HRealAbs + RComplete:
+theory NSA = HyperArith + RComplete:
 
 constdefs
 
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/NatStar.ML
--- a/src/HOL/Hyperreal/NatStar.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -209,7 +209,7 @@
 \      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
 by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
-   [hypnatrel_in_hypnat RS Abs_hypnat_inverse,
+   [hypnatrel_in_hypnat RS thm"Abs_hypnat_inverse",
     [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
 qed "starfunNat2";
 
@@ -406,7 +406,7 @@
 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
 by (auto_tac (claset(), 
-       simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse]));
+       simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat, starfun_inverse_inverse]));
 qed "starfunNat_inverse_real_of_nat_eq";
 
 (*----------------------------------------------------------
@@ -488,6 +488,6 @@
 \     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
 by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
+by (auto_tac (claset(), simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat]));
 qed "starfunNat_inverse_real_of_nat_Infinitesimal";
 Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/SEQ.ML
--- a/src/HOL/Hyperreal/SEQ.ML	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML	Mon Feb 02 12:23:46 2004 +0100
@@ -4,6 +4,13 @@
     Description : Theory of sequence and series of real numbers
 *) 
 
+fun CLAIM_SIMP str thms =
+               prove_goal (the_context()) str
+               (fn prems => [cut_facts_tac prems 1,
+                   auto_tac (claset(),simpset() addsimps thms)]);
+
+fun CLAIM str = CLAIM_SIMP str [];
+
 (*---------------------------------------------------------------------------
    Example of an hypersequence (i.e. an extended standard sequence) 
    whose term with an hypernatural suffix is an infinitesimal i.e. 
diff -r b0064703967b -r c78c7da09519 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Mon Feb 02 12:23:46 2004 +0100
@@ -58,55 +58,44 @@
 
 lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
 
-apply (unfold starset_def)
-apply auto
+apply (unfold starset_def, auto)
 done
 declare STAR_real_set [simp]
 
 lemma STAR_empty_set: "*s* {} = {}"
-apply (unfold starset_def)
-apply safe
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply (drule_tac x = "%n. xa n" in bspec)
-apply auto
+apply (unfold starset_def, safe)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (drule_tac x = "%n. xa n" in bspec, auto)
 done
 declare STAR_empty_set [simp]
 
 lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
-apply (unfold starset_def)
-apply auto
+apply (unfold starset_def, auto)
   prefer 3 apply (blast intro: FreeUltrafilterNat_subset)
  prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
 apply (drule FreeUltrafilterNat_Compl_mem)
-apply (drule bspec , assumption)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply auto
-apply ultra
+apply (drule bspec, assumption)
+apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
 done
 
 lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
-apply (unfold starset_def)
-apply auto
+apply (unfold starset_def, auto)
 prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
 apply (blast intro: FreeUltrafilterNat_subset)+
 done
 
 lemma STAR_Compl: "*s* -A = -( *s* A)"
 apply (auto simp add: starset_def)
-apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
-apply (auto dest!: bspec);
-apply ultra
-apply (drule FreeUltrafilterNat_Compl_mem)
-apply ultra
+apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (auto dest!: bspec, ultra)
+apply (drule FreeUltrafilterNat_Compl_mem, ultra)
 done
 
 lemma STAR_mem_Compl: "x \<notin> *s* F ==> x : *s* (- F)"
-apply (auto simp add: STAR_Compl)
-done
+by (auto simp add: STAR_Compl)
 
 lemma STAR_diff: "*s* (A - B) = *s* A - *s* B"
-apply (auto simp add: Diff_eq STAR_Int STAR_Compl)
-done
+by (auto simp add: Diff_eq STAR_Int STAR_Compl)
 
 lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
 apply (unfold starset_def)
@@ -128,46 +117,40 @@
 apply (unfold starset_def)
 apply (auto simp add: hypreal_of_real_def SReal_def)
 apply (simp add: hypreal_of_real_def [symmetric])
-apply (rule imageI , rule ccontr)
+apply (rule imageI, rule ccontr)
 apply (drule bspec)
 apply (rule lemma_hyprel_refl)
-prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
-apply auto
+prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
 done
 
 lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> ALL y: A. x \<noteq> hypreal_of_real y"
-apply auto
-done
+by auto
 
 lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
-apply auto
-done
+by auto
 
 lemma STAR_real_seq_to_hypreal:
     "ALL n. (X n) \<notin> M
           ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
 apply (unfold starset_def)
-apply (auto , rule bexI , rule_tac [2] lemma_hyprel_refl)
-apply auto
+apply (auto, rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
 done
 
 lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
 apply (unfold starset_def)
 apply (auto simp add: hypreal_of_real_def)
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto intro: FreeUltrafilterNat_subset)
 done
 declare STAR_singleton [simp]
 
 lemma STAR_not_mem: "x \<notin> F ==> hypreal_of_real x \<notin> *s* F"
 apply (auto simp add: starset_def hypreal_of_real_def)
-apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
-apply auto
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
 done
 
 lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
-apply (blast dest: STAR_subset)
-done
+by (blast dest: STAR_subset)
 
 (*------------------------------------------------------------------
    Nonstandard extension of a set (defined using a constant
@@ -177,8 +160,7 @@
 lemma starset_n_starset:
      "ALL n. (As n = A) ==> *sn* As = *s* A"
 
-apply (unfold starset_n_def starset_def)
-apply auto
+apply (unfold starset_n_def starset_def, auto)
 done
 
 
@@ -194,8 +176,7 @@
 lemma starfun_n_starfun:
      "ALL n. (F n = f) ==> *fn* F = *f* f"
 
-apply (unfold starfun_n_def starfun_def)
-apply auto
+apply (unfold starfun_n_def starfun_def, auto)
 done
 
 
@@ -212,21 +193,19 @@
 
 lemma hrabs_is_starext_rabs: "is_starext abs abs"
 
-apply (unfold is_starext_def)
-apply safe
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply (rule_tac z = "y" in eq_Abs_hypreal)
-apply auto
-apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
-apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
+apply (unfold is_starext_def, safe)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal, auto)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
+apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
 apply (auto dest!: spec simp add: hypreal_minus hrabs_def hypreal_zero_def hypreal_le_def hypreal_less_def)
 apply (arith | ultra)+
 done
 
 lemma Rep_hypreal_FreeUltrafilterNat: "[| X: Rep_hypreal z; Y: Rep_hypreal z |]
       ==> {n. X n = Y n} : FreeUltrafilterNat"
-apply (rule_tac z = "z" in eq_Abs_hypreal)
-apply (auto , ultra)
+apply (rule_tac z = z in eq_Abs_hypreal)
+apply (auto, ultra)
 done
 
 (*-----------------------------------------------------------------------
@@ -234,44 +213,41 @@
  -----------------------------------------------------------------------*)
 
 lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
-apply (unfold congruent_def)
-apply auto
-apply ultra
-done
+by (unfold congruent_def, auto, ultra)
 
 lemma starfun:
       "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
        Abs_hypreal(hyprel `` {%n. f (X n)})"
 apply (unfold starfun_def)
-apply (rule_tac f = "Abs_hypreal" in arg_cong)
+apply (rule_tac f = Abs_hypreal in arg_cong)
 apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
                  UN_equiv_class [OF equiv_hyprel starfun_congruent])
 done
 
 (*-------------------------------------------
-  multiplication: ( *f ) x ( *g ) = *(f x g)
+  multiplication: ( *f) x ( *g) = *(f x g)
  ------------------------------------------*)
 lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_mult)
 done
 declare starfun_mult [symmetric, simp]
 
 (*---------------------------------------
-  addition: ( *f ) + ( *g ) = *(f + g)
+  addition: ( *f) + ( *g) = *(f + g)
  ---------------------------------------*)
 lemma starfun_add: "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_add)
 done
 declare starfun_add [symmetric, simp]
 
 (*--------------------------------------------
-  subtraction: ( *f ) + -( *g ) = *(f + -g)
+  subtraction: ( *f) + -( *g) = *(f + -g)
  -------------------------------------------*)
 
 lemma starfun_minus: "- ( *f* f) x = ( *f* (%x. - f x)) x"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_minus)
 done
 declare starfun_minus [symmetric, simp]
@@ -290,12 +266,12 @@
 declare starfun_diff [symmetric, simp]
 
 (*--------------------------------------
-  composition: ( *f ) o ( *g ) = *(f o g)
+  composition: ( *f) o ( *g) = *(f o g)
  ---------------------------------------*)
 
 lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
 apply (rule ext)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun)
 done
 
@@ -308,7 +284,7 @@
   NS extension of constant function
  --------------------------------------*)
 lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_of_real_def)
 done
 
@@ -319,12 +295,12 @@
  ----------------------------------------------------*)
 
 lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun)
 done
 
 lemma starfun_Id: "( *f* (%x. x)) x = x"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun)
 done
 declare starfun_Id [simp]
@@ -335,10 +311,9 @@
 
 lemma is_starext_starfun: "is_starext ( *f* f) f"
 
-apply (unfold is_starext_def)
-apply auto
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply (rule_tac z = "y" in eq_Abs_hypreal)
+apply (unfold is_starext_def, auto)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
 apply (auto intro!: bexI simp add: starfun)
 done
 
@@ -350,16 +325,14 @@
 
 apply (unfold is_starext_def)
 apply (rule ext)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
-apply (drule_tac x = "x" in spec)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (drule_tac x = x in spec)
 apply (drule_tac x = "( *f* f) x" in spec)
-apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun)
-apply ultra
+apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
 done
 
 lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
-apply (blast intro: is_starfun_starext is_starext_starfun)
-done
+by (blast intro: is_starfun_starext is_starext_starfun)
 
 (*--------------------------------------------------------
    extented function has same solution as its standard
@@ -367,31 +340,28 @@
    for all real arguments
  -------------------------------------------------------*)
 lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
-apply (auto simp add: starfun hypreal_of_real_def)
-done
+by (auto simp add: starfun hypreal_of_real_def)
 
 declare starfun_eq [simp]
 
 lemma starfun_approx: "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)"
-apply auto
-done
+by auto
 
 (* useful for NS definition of derivatives *)
 lemma starfun_lambda_cancel: "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)"
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
 done
 
 lemma starfun_lambda_cancel2: "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"
-apply (rule_tac z = "xa" in eq_Abs_hypreal)
+apply (rule_tac z = xa in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
 done
 
 lemma starfun_mult_HFinite_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m;
                   l: HFinite; m: HFinite
                |] ==>  ( *f* (%x. f x * g x)) xa @= l * m"
-apply (drule approx_mult_HFinite)
-apply (assumption)+
+apply (drule approx_mult_HFinite, assumption+)
 apply (auto intro: approx_HFinite [OF _ approx_sym])
 done
 
@@ -410,30 +380,28 @@
 (* use the theorem we proved above instead          *)
 
 lemma starfun_rabs_hrabs: "*f* abs = abs"
-apply (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
-done
+by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
 
 lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_inverse hypreal_zero_def)
 done
 declare starfun_inverse_inverse [simp]
 
 lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun hypreal_inverse)
 done
 declare starfun_inverse [symmetric, simp]
 
 lemma starfun_divide:
   "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
-apply (unfold hypreal_divide_def real_divide_def)
-apply auto
+apply (unfold hypreal_divide_def real_divide_def, auto)
 done
 declare starfun_divide [symmetric, simp]
 
 lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
 done
 
@@ -444,11 +412,11 @@
 lemma starfun_mem_starset:
       "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"
 apply (unfold starset_def)
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto simp add: starfun)
 apply (rename_tac "X")
 apply (drule_tac x = "%n. f (X n) " in bspec)
-apply (auto , ultra)
+apply (auto, ultra)
 done
 
 (*------------------------------------------------------------
@@ -470,21 +438,17 @@
 lemma STAR_rabs_add_minus:
    "*s* {x. abs (x + - y) < r} =
      {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def)
-apply safe
-apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
-apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less)
-apply ultra
+apply (unfold starset_def, safe)
+apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less, ultra)
 done
 
 lemma STAR_starfun_rabs_add_minus:
   "*s* {x. abs (f x + - y) < r} =
        {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
-apply (unfold starset_def)
-apply safe
-apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
-apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun)
-apply ultra
+apply (unfold starset_def, safe)
+apply (rule_tac [!] z = x in eq_Abs_hypreal)
+apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
 done
 
 (*-------------------------------------------------------------------
@@ -496,12 +460,11 @@
       (EX X:Rep_hypreal(x).
         ALL m. {n. abs(X n) < inverse(real(Suc m))}
                : FreeUltrafilterNat)"
-apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_hypreal)
 apply (auto intro!: bexI lemma_hyprel_refl 
             simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def 
      hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def)
-apply (drule_tac x = "n" in spec)
-apply ultra
+apply (drule_tac x = n in spec, ultra)
 done
 
 lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
@@ -510,13 +473,12 @@
 apply (subst approx_minus_iff)
 apply (rule mem_infmal_iff [THEN subst])
 apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff2)
-apply (drule_tac x = "m" in spec)
-apply ultra
+apply (drule_tac x = m in spec, ultra)
 done
 
 lemma inj_starfun: "inj starfun"
 apply (rule inj_onI)
-apply (rule ext , rule ccontr)
+apply (rule ext, rule ccontr)
 apply (drule_tac x = "Abs_hypreal (hyprel ``{%n. xa}) " in fun_cong)
 apply (auto simp add: starfun)
 done
diff -r b0064703967b -r c78c7da09519 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jan 29 16:51:17 2004 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 02 12:23:46 2004 +0100
@@ -146,10 +146,9 @@
   Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
   Hyperreal/Fact.ML Hyperreal/Fact.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy\
-  Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
-  Hyperreal/HyperArith.thy \
-  Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
-  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
+  Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
+  Hyperreal/HyperArith.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
+  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
   Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\