Updated Files with new theorems

--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -132,15 +132,13 @@
 by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
 qed "FreeUltrafilterNat_all";
 
-(*-----------------------------------------
+(*-------------------------------------------------------
      Define and use Ultrafilter tactics
- -----------------------------------------*)
+ -------------------------------------------------------*)
 use "fuf.ML";
 
-
-
-(*------------------------------------------------------
-   Now prove one further property of our free ultrafilter
+(*-------------------------------------------------------
+  Now prove one further property of our free ultrafilter
  -------------------------------------------------------*)
 Goal "X Un Y: FreeUltrafilterNat \
 \     ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
@@ -148,9 +146,9 @@
 by (Ultra_tac 1);
 qed "FreeUltrafilterNat_Un";
 
-(*------------------------------------------------------------------------
-                       Properties of hyprel
- ------------------------------------------------------------------------*)
+(*-------------------------------------------------------
+   Properties of hyprel
+ -------------------------------------------------------*)
 
 (** Proving that hyprel is an equivalence relation **)
 (** Natural deduction for hyprel **)
@@ -453,10 +451,10 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
     hypreal_add,real_minus_add_distrib]));
 qed "hypreal_minus_add_distrib";
+Addsimps [hypreal_minus_add_distrib];
 
 Goal "-(y + -(x::hypreal)) = x + -y";
-by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
-    hypreal_add_commute]) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
 qed "hypreal_minus_distrib1";
 
 Goal "(x + - (y::hypreal)) + (y + - z) = x + -z";
@@ -478,21 +476,21 @@
 Addsimps [hypreal_add_minus_cancel2];
 
 Goal "y + -(x + y) = -(x::hypreal)";
-by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib]) 1);
+by (Full_simp_tac 1);
 by (rtac (hypreal_add_left_commute RS subst) 1);
 by (Full_simp_tac 1);
 qed "hypreal_add_minus_cancel";
 Addsimps [hypreal_add_minus_cancel];
 
 Goal "y + -(y + x) = -(x::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_minus_add_distrib,
-              hypreal_add_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
 qed "hypreal_add_minus_cancelc";
 Addsimps [hypreal_add_minus_cancelc];
 
 Goal "(z + -x) + (y + -z) = (y + -(x::hypreal))";
 by (full_simp_tac (simpset() addsimps [hypreal_minus_add_distrib
-    RS sym, hypreal_add_left_cancel] @ hypreal_add_ac) 1); 
+    RS sym, hypreal_add_left_cancel] @ hypreal_add_ac 
+    delsimps [hypreal_minus_add_distrib]) 1); 
 qed "hypreal_add_minus_cancel3";
 Addsimps [hypreal_add_minus_cancel3];
 
@@ -511,6 +509,15 @@
 qed "hypreal_add_minus_cancel5";
 Addsimps [hypreal_add_minus_cancel5];
 
+Goal "z + ((- z) + w) = (w::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_add_minus_cancelA";
+
+Goal "(-z) + (z + w) = (w::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
+qed "hypreal_minus_add_cancelA";
+
+Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
 
 (**** hyperreal multiplication: hypreal_mult  ****)
 
@@ -594,7 +601,6 @@
 by Auto_tac;
 qed "hypreal_minus_mult_commute";
 
-
 (*-----------------------------------------------------------------------------
     A few more theorems
  ----------------------------------------------------------------------------*)
@@ -623,6 +629,17 @@
 bind_thms ("hypreal_mult_simps", [hypreal_mult_1, hypreal_mult_1_right]);
 Addsimps hypreal_mult_simps;
 
+(* 07/00 *)
+
+Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
+by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
+qed "hypreal_diff_mult_distrib";
+
+Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
+by (simp_tac (simpset() addsimps [hypreal_mult_commute', 
+				  hypreal_diff_mult_distrib]) 1);
+qed "hypreal_diff_mult_distrib2";
+
 (*** one and zero are distinct ***)
 Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
 by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
@@ -715,6 +732,11 @@
 
 bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
 
+Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
+by (auto_tac (claset() addIs [ccontr] addDs 
+    [hypreal_mult_not_0],simpset()));
+qed "hypreal_mult_zero_disj";
+
 Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
 by (blast_tac (claset() addDs [hypreal_mult_not_0]) 1);
 qed "hypreal_mult_self_not_zero";
@@ -789,6 +811,7 @@
 
 (*** y < y ==> P ***)
 bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
+AddSEs [hypreal_less_irrefl];
 
 Goal "!!(x::hypreal). x < y ==> x ~= y";
 by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
@@ -809,7 +832,7 @@
     [hypreal_less_not_refl]) 1);
 qed "hypreal_less_asym";
 
-(*--------------------------------------------------------
+(*-------------------------------------------------------
   TODO: The following theorem should have been proved 
   first and then used througout the proofs as it probably 
   makes many of them more straightforward. 
@@ -827,6 +850,7 @@
  ---------------------------------------------------------------------------------*)
 (*** sum order ***)
 
+(***
 Goalw [hypreal_zero_def] 
       "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y";
 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
@@ -849,6 +873,8 @@
 by (ultra_tac (claset() addIs [rename_numerals real_mult_order],
 	       simpset()) 1);
 qed "hypreal_mult_order";
+****)
+
 
 (*---------------------------------------------------------------------------------
                          Trichotomy of the hyperreals
@@ -885,44 +911,23 @@
 (*----------------------------------------------------------------------------
             More properties of <
  ----------------------------------------------------------------------------*)
-Goal "!!(A::hypreal). A < B ==> A + C < B + C";
-by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSIs [exI],simpset() addsimps
-    [hypreal_less_def,hypreal_add]));
-by (Ultra_tac 1);
-qed "hypreal_add_less_mono1";
-
-Goal "!!(A::hypreal). A < B ==> C + A < C + B";
-by (auto_tac (claset() addIs [hypreal_add_less_mono1],
-    simpset() addsimps [hypreal_add_commute]));
-qed "hypreal_add_less_mono2";
 
 Goal "((x::hypreal) < y) = (0 < y + -x)";
-by (Step_tac 1);
-by (dres_inst_tac [("C","-x")] hypreal_add_less_mono1 1);
-by (dres_inst_tac [("C","x")] hypreal_add_less_mono1 2);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add,
+    hypreal_zero_def,hypreal_minus,hypreal_less]));
+by (ALLGOALS(Ultra_tac));
 qed "hypreal_less_minus_iff"; 
 
-Goal "((x::hypreal) < y) = (x + -y< 0)";
-by (Step_tac 1);
-by (dres_inst_tac [("C","-y")] hypreal_add_less_mono1 1);
-by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 2);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
+Goal "((x::hypreal) < y) = (x + -y < 0)";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add,
+    hypreal_zero_def,hypreal_minus,hypreal_less]));
+by (ALLGOALS(Ultra_tac));
 qed "hypreal_less_minus_iff2";
 
-Goal  "!!(y1 :: hypreal). [| z1 < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2";
-by (dtac (hypreal_less_minus_iff RS iffD1) 1);
-by (dtac (hypreal_less_minus_iff RS iffD1) 1);
-by (dtac hypreal_add_order 1 THEN assume_tac 1);
-by (thin_tac "0 < y2 + - z2" 1);
-by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac));
-qed "hypreal_add_less_mono";
-
 Goal "((x::hypreal) = y) = (0 = x + - y)";
 by Auto_tac;
 by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
@@ -935,6 +940,21 @@
 by Auto_tac;
 qed "hypreal_eq_minus_iff2"; 
 
+(* 07/00 *)
+Goal "(0::hypreal) - x = -x";
+by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
+qed "hypreal_diff_zero";
+
+Goal "x - (0::hypreal) = x";
+by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
+qed "hypreal_diff_zero_right";
+
+Goal "x - x = (0::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
+qed "hypreal_diff_self";
+
+Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self];
+
 Goal "(x = y + z) = (x + -z = (y::hypreal))";
 by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
 qed "hypreal_eq_minus_iff3";
@@ -957,6 +977,11 @@
 by Auto_tac;
 qed "hypreal_linear";
 
+Goal "((w::hypreal) ~= z) = (w<z | z<w)";
+by (cut_facts_tac [hypreal_linear] 1);
+by (Blast_tac 1);
+qed "hypreal_neq_iff";
+
 Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
 \          y < x ==> P |] ==> P";
 by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
@@ -1015,12 +1040,20 @@
 Goal "(x <= (y::hypreal)) = (x < y | x=y)";
 by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
 qed "hypreal_le_eq_less_or_eq";
+val hypreal_le_less = hypreal_le_eq_less_or_eq;
 
 Goal "w <= (w::hypreal)";
 by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
 qed "hypreal_le_refl";
 Addsimps [hypreal_le_refl];
 
+(* Axiom 'linorder_linear' of class 'linorder': *)
+Goal "(z::hypreal) <= w | w <= z";
+by (simp_tac (simpset() addsimps [hypreal_le_less]) 1);
+by (cut_facts_tac [hypreal_linear] 1);
+by (Blast_tac 1);
+qed "hypreal_le_linear";
+
 Goal "[| i <= j; j < k |] ==> i < (k::hypreal)";
 by (dtac hypreal_le_imp_less_or_eq 1);
 by (fast_tac (claset() addIs [hypreal_less_trans]) 1);
@@ -1041,217 +1074,35 @@
             fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
 qed "hypreal_le_anti_sym";
 
-Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
-by (auto_tac (claset() addDs [sym,hypreal_le_imp_less_or_eq]
-              addIs [hypreal_add_order],simpset()));
-qed "hypreal_add_order_le";            
-
-(*------------------------------------------------------------------------
- ------------------------------------------------------------------------*)
-
 Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
 by (rtac not_hypreal_leE 1);
 by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_hypreal_less";
 
+(* Axiom 'order_less_le' of class 'order': *)
+Goal "(w::hypreal) < z = (w <= z & w ~= z)";
+by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
+by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
+qed "hypreal_less_le";
+
 Goal "(0 < -R) = (R < (0::hypreal))";
-by (Step_tac 1);
-by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
-by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
+by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
+    hypreal_less,hypreal_minus]));
 qed "hypreal_minus_zero_less_iff";
+Addsimps [hypreal_minus_zero_less_iff];
 
 Goal "(-R < 0) = ((0::hypreal) < R)";
-by (Step_tac 1);
-by (dres_inst_tac [("C","R")] hypreal_add_less_mono1 1);
-by (dres_inst_tac [("C","-R")] hypreal_add_less_mono1 2);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
+by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
+    hypreal_less,hypreal_minus]));
+by (ALLGOALS(Ultra_tac));
 qed "hypreal_minus_zero_less_iff2";
 
-Goal "((x::hypreal) < y) = (-y < -x)";
-by (stac hypreal_less_minus_iff 1);
-by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-qed "hypreal_less_swap_iff";
-
-Goal "((0::hypreal) < x) = (-x < x)";
-by (Step_tac 1);
-by (rtac ccontr 2 THEN forward_tac 
-    [hypreal_leI RS hypreal_le_imp_less_or_eq] 2);
-by (Step_tac 2);
-by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2);
-by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2);
-by (Auto_tac );
-by (ftac hypreal_add_order 1 THEN assume_tac 1);
-by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
-qed "hypreal_gt_zero_iff";
-
-Goal "(x < (0::hypreal)) = (x < -x)";
-by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
-by (stac hypreal_gt_zero_iff 1);
-by (Full_simp_tac 1);
-qed "hypreal_lt_zero_iff";
-
-Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym]));
-qed "hypreal_ge_zero_iff";
-
-Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym]));
-qed "hypreal_le_zero_iff";
-
-Goal "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y";
-by (REPEAT(dtac (hypreal_minus_zero_less_iff RS iffD2) 1));
-by (dtac hypreal_mult_order 1 THEN assume_tac 1);
-by (Asm_full_simp_tac 1);
-qed "hypreal_mult_less_zero1";
-
-Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y";
-by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypreal_mult_order,
-    hypreal_less_imp_le],simpset()));
-qed "hypreal_le_mult_order";
-
-Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y";
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac hypreal_le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset()));
-qed "real_mult_le_zero1";
-
-Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)";
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (dtac hypreal_le_imp_less_or_eq 1 THEN etac disjE 1);
-by Auto_tac;
-by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
-by (rtac (hypreal_minus_zero_less_iff RS subst) 1);
-by (blast_tac (claset() addDs [hypreal_mult_order] 
-    addIs [hypreal_minus_mult_eq2 RS ssubst]) 1);
-qed "hypreal_mult_le_zero";
-
-Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)";
-by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
-by (dtac hypreal_mult_order 1 THEN assume_tac 1);
-by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
-by (Asm_full_simp_tac 1);
-qed "hypreal_mult_less_zero";
-
-Goalw [hypreal_one_def,hypreal_zero_def,hypreal_less_def] "0 < 1hr";
-by (res_inst_tac [("x","%n. #0")] exI 1);
-by (res_inst_tac [("x","%n. #1")] exI 1);
-by (auto_tac (claset(),simpset() addsimps [real_zero_less_one,
-    FreeUltrafilterNat_Nat_set]));
-qed "hypreal_zero_less_one";
-
-Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y";
-by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypreal_add_order,
-    hypreal_less_imp_le],simpset()));
-qed "hypreal_le_add_order";
-
-Goal "!!(q1::hypreal). q1 <= q2  ==> x + q1 <= x + q2";
-by (dtac hypreal_le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (auto_tac (claset() addSIs [hypreal_le_refl,
-    hypreal_less_imp_le,hypreal_add_less_mono1],
-    simpset() addsimps [hypreal_add_commute]));
-qed "hypreal_add_left_le_mono1";
-
-Goal "!!(q1::hypreal). q1 <= q2  ==> q1 + x <= q2 + x";
-by (auto_tac (claset() addDs [hypreal_add_left_le_mono1],
-    simpset() addsimps [hypreal_add_commute]));
-qed "hypreal_add_le_mono1";
-
-Goal "!!k l::hypreal. [|i<=j;  k<=l |] ==> i + k <= j + l";
-by (etac (hypreal_add_le_mono1 RS hypreal_le_trans) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
-(*j moves to the end because it is free while k, l are bound*)
-by (etac hypreal_add_le_mono1 1);
-qed "hypreal_add_le_mono";
-
-Goal "!!k l::hypreal. [|i<j;  k<=l |] ==> i + k < j + l";
-by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
-    addIs [hypreal_add_less_mono1,hypreal_add_less_mono],simpset()));
-qed "hypreal_add_less_le_mono";
-
-Goal "!!k l::hypreal. [|i<=j;  k<l |] ==> i + k < j + l";
-by (auto_tac (claset() addSDs [hypreal_le_imp_less_or_eq] 
-    addIs [hypreal_add_less_mono2,hypreal_add_less_mono],simpset()));
-qed "hypreal_add_le_less_mono";
-
-Goal "(0*x<r)=((0::hypreal)<r)";
-by (Simp_tac 1);
-qed "hypreal_mult_0_less";
-
-Goal "[| (0::hypreal) < z; x < y |] ==> x*z < y*z";       
-by (rotate_tac 1 1);
-by (dtac (hypreal_less_minus_iff RS iffD1) 1);
-by (rtac (hypreal_less_minus_iff RS iffD2) 1);
-by (dtac hypreal_mult_order 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_mult_distrib2,
-					   hypreal_mult_commute ]) 1);
-qed "hypreal_mult_less_mono1";
-
-Goal "[| (0::hypreal)<z; x<y |] ==> z*x<z*y";       
-by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,hypreal_mult_less_mono1]) 1);
-qed "hypreal_mult_less_mono2";
-
-Goal "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z";
-by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac hypreal_le_imp_less_or_eq]);
-by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset()));
-qed "hypreal_mult_le_less_mono1";
-
-Goal "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y";
-by (asm_simp_tac (simpset() addsimps [hypreal_mult_commute,
-				      hypreal_mult_le_less_mono1]) 1);
-qed "hypreal_mult_le_less_mono2";
-
-Goal "[| (0::hypreal)<=z; x<=y |] ==> z*x<=z*y";
-by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [hypreal_mult_le_less_mono2,hypreal_le_refl],simpset()));
-qed "hypreal_mult_le_le_mono1";
-
-val prem1::prem2::prem3::rest = goal (the_context ())
-     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
-by (rtac ([([prem1,prem2] MRS hypreal_mult_less_mono2),prem3] MRS hypreal_less_trans) 1);
-qed "hypreal_mult_less_trans";
-
-Goal "[| 0<=y; x<r; y*r<t*s; (0::hypreal)<t*s|] ==> y*x<t*s";
-by (dtac hypreal_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addEs [(hypreal_mult_0_less RS iffD2),hypreal_mult_less_trans]) 1);
-qed "hypreal_mult_le_less_trans";
-
-Goal "[| 0 <= y; x <= r; y*r < t*s; (0::hypreal) < t*s|] ==> y*x < t*s";
-by (dres_inst_tac [("x","x")] hypreal_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
-qed "hypreal_mult_le_le_trans";
-
-Goal "[| 0 < r1; r1 <r2; (0::hypreal) < x; x < y|] \
-\                     ==> r1 * x < r2 * y";
-by (dres_inst_tac [("x","x")] hypreal_mult_less_mono2 1);
-by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 2);
-by (dres_inst_tac [("x","r1")] hypreal_mult_less_mono1 3);
-by Auto_tac;
-by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
-qed "hypreal_mult_less_mono";
-
-Goal "[| 0 < r1; r1 <r2; 0 < y|] \
-\                           ==> (0::hypreal) < r2 * y";
-by (dres_inst_tac [("R1.0","0")] hypreal_less_trans 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [hypreal_mult_order]) 1);
-qed "hypreal_mult_order_trans";
-
-Goal "[| 0 < r1; r1 <= r2; (0::hypreal) <= x; x <= y |] \
-\                  ==> r1 * x <= r2 * y";
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypreal_mult_less_mono,
-    hypreal_mult_less_mono1,hypreal_mult_less_mono2,
-    hypreal_mult_order_trans,hypreal_mult_order],simpset()));
-qed "hypreal_mult_le_mono";
+Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= (0::hypreal))";
+by (simp_tac (simpset() addsimps 
+    [hypreal_minus_zero_less_iff2]) 1);
+qed "hypreal_minus_zero_le_iff";
 
 (*----------------------------------------------------------
   hypreal_of_real preserves field and order properties
@@ -1291,26 +1142,6 @@
 by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
 qed "hypreal_of_real_minus";
 
-Goal "0 < x ==> 0 < hrinv x";
-by (EVERY1[rtac ccontr, dtac hypreal_leI]);
-by (forward_tac [hypreal_minus_zero_less_iff2 RS iffD2] 1);
-by (forward_tac [hypreal_not_refl2 RS not_sym] 1);
-by (dtac (hypreal_not_refl2 RS not_sym RS hrinv_not_zero) 1);
-by (EVERY1[dtac hypreal_le_imp_less_or_eq, Step_tac]); 
-by (dtac hypreal_mult_less_zero1 1 THEN assume_tac 1);
-by (auto_tac (claset() addIs [hypreal_zero_less_one RS hypreal_less_asym],
-    simpset() addsimps [hypreal_minus_zero_less_iff]));
-qed "hypreal_hrinv_gt_zero";
-
-Goal "x < 0 ==> hrinv x < 0";
-by (ftac hypreal_not_refl2 1);
-by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
-by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
-by (dtac (hypreal_minus_hrinv RS sym) 1);
-by (auto_tac (claset() addIs [hypreal_hrinv_gt_zero],
-    simpset()));
-qed "hypreal_hrinv_less_zero";
-
 Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real  #1 = 1hr";
 by (Step_tac 1);
 qed "hypreal_of_real_one";
@@ -1346,136 +1177,10 @@
 by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
 qed "hypreal_add_self";
 
-Goal "1hr < 1hr + 1hr";
-by (rtac (hypreal_less_minus_iff RS iffD2) 1);
-by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one,
-    hypreal_add_assoc]) 1);
-qed "hypreal_one_less_two";
-
-Goal "0 < 1hr + 1hr";
-by (rtac ([hypreal_zero_less_one,
-          hypreal_one_less_two] MRS hypreal_less_trans) 1);
-qed "hypreal_zero_less_two";
-
-Goal "1hr + 1hr ~= 0";
-by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1);
-qed "hypreal_two_not_zero";
-Addsimps [hypreal_two_not_zero];
-
-Goal "x*hrinv(1hr + 1hr) + x*hrinv(1hr + 1hr) = x";
-by (stac hypreal_add_self 1);
-by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
-qed "hypreal_sum_of_halves";
-
 Goal "z ~= 0 ==> x*y = (x*hrinv(z))*(z*y)";
 by (asm_simp_tac (simpset() addsimps hypreal_mult_ac)  1);
 qed "lemma_chain";
 
-Goal "0 < r ==> 0 < r*hrinv(1hr+1hr)";
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero 
-          RS hypreal_mult_less_mono1) 1);
-by Auto_tac;
-qed "hypreal_half_gt_zero";
-
-(* TODO: remove redundant  0 < x *)
-Goal "[| 0 < r; 0 < x; r < x |] ==> hrinv x < hrinv r";
-by (ftac hypreal_hrinv_gt_zero 1);
-by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1);
-by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
-         not_sym RS hypreal_mult_hrinv]) 1);
-by (ftac hypreal_hrinv_gt_zero 1);
-by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1);
-by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS 
-         not_sym RS hypreal_mult_hrinv_left,hypreal_mult_assoc RS sym]) 1);
-qed "hypreal_hrinv_less_swap";
-
-Goal "[| 0 < r; 0 < x|] ==> (r < x) = (hrinv x < hrinv r)";
-by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],simpset()));
-by (res_inst_tac [("t","r")] (hypreal_hrinv_hrinv RS subst) 1);
-by (etac (hypreal_not_refl2 RS not_sym) 1);
-by (res_inst_tac [("t","x")] (hypreal_hrinv_hrinv RS subst) 1);
-by (etac (hypreal_not_refl2 RS not_sym) 1);
-by (auto_tac (claset() addIs [hypreal_hrinv_less_swap],
-    simpset() addsimps [hypreal_hrinv_gt_zero]));
-qed "hypreal_hrinv_less_iff";
-
-Goal "[| 0 < z; x < y |] ==> x*hrinv(z) < y*hrinv(z)";
-by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
-    hypreal_hrinv_gt_zero]) 1);
-qed "hypreal_mult_hrinv_less_mono1";
-
-Goal "[| 0 < z; x < y |] ==> hrinv(z)*x < hrinv(z)*y";
-by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
-    hypreal_hrinv_gt_zero]) 1);
-qed "hypreal_mult_hrinv_less_mono2";
-
-Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
-by (forw_inst_tac [("x","x*z")] hypreal_mult_hrinv_less_mono1 1);
-by (dtac (hypreal_not_refl2 RS not_sym) 2);
-by (auto_tac (claset() addSDs [hypreal_mult_hrinv],
-              simpset() addsimps hypreal_mult_ac));
-qed "hypreal_less_mult_right_cancel";
-
-Goal "[| (0::hypreal) < z; z*x < z*y |] ==> x < y";
-by (auto_tac (claset() addIs [hypreal_less_mult_right_cancel],
-    simpset() addsimps [hypreal_mult_commute]));
-qed "hypreal_less_mult_left_cancel";
-
-Goal "[| 0 < r; (0::hypreal) < ra; \
-\                 r < x; ra < y |] \
-\              ==> r*ra < x*y";
-by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
-by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
-by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
-by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
-qed "hypreal_mult_less_gt_zero"; 
-
-Goal "[| 0 < r; (0::hypreal) < ra; \
-\                 r <= x; ra <= y |] \
-\              ==> r*ra <= x*y";
-by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
-by (rtac hypreal_less_or_eq_imp_le 1);
-by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
-    hypreal_mult_less_mono2,hypreal_mult_less_gt_zero],
-    simpset()));
-qed "hypreal_mult_le_ge_zero"; 
-
-Goal "EX (x::hypreal). x < y";
-by (rtac (hypreal_add_zero_right RS subst) 1);
-by (res_inst_tac [("x","y + -1hr")] exI 1);
-by (auto_tac (claset() addSIs [hypreal_add_less_mono2],
-    simpset() addsimps [hypreal_minus_zero_less_iff2,
-    hypreal_zero_less_one] delsimps [hypreal_add_zero_right]));
-qed "hypreal_less_Ex";
-
-Goal "!!(A::hypreal). A + C < B + C ==> A < B";
-by (dres_inst_tac [("C","-C")] hypreal_add_less_mono1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
-qed "hypreal_less_add_right_cancel";
-
-Goal "!!(A::hypreal). C + A < C + B ==> A < B";
-by (dres_inst_tac [("C","-C")] hypreal_add_less_mono2 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_less_add_left_cancel";
-
-Goal "(0::hypreal) <= x*x";
-by (res_inst_tac [("x","0"),("y","x")] hypreal_linear_less2 1);
-by (auto_tac (claset() addIs [hypreal_mult_order,
-    hypreal_mult_less_zero1,hypreal_less_imp_le],
-    simpset()));
-qed "hypreal_le_square";
-Addsimps [hypreal_le_square];
-
-Goalw [hypreal_le_def] "- (x*x) <= (0::hypreal)";
-by (auto_tac (claset() addSDs [(hypreal_le_square RS 
-    hypreal_le_less_trans)],simpset() addsimps 
-    [hypreal_minus_zero_less_iff,hypreal_less_not_refl]));
-qed "hypreal_less_minus_square";
-Addsimps [hypreal_less_minus_square];
-
 Goal "[|x ~= 0; y ~= 0 |] ==> \
 \                   hrinv(x) + hrinv(y) = (x + y)*hrinv(x*y)";
 by (asm_full_simp_tac (simpset() addsimps [hypreal_hrinv_distrib,
@@ -1486,19 +1191,16 @@
 qed "hypreal_hrinv_add";
 
 Goal "x = -x ==> x = (0::hypreal)";
-by (dtac (hypreal_eq_minus_iff RS iffD1 RS sym) 1);
-by (Asm_full_simp_tac 1);
-by (dtac (hypreal_add_self RS subst) 1);
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [hypreal_two_not_zero RSN
-               (2,hypreal_mult_not_0)]) 1);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
+    hypreal_zero_def]));
+by (Ultra_tac 1);
 qed "hypreal_self_eq_minus_self_zero";
 
 Goal "(x + x = 0) = (x = (0::hypreal))";
-by Auto_tac;
-by (dtac (hypreal_add_self RS subst) 1);
-by (rtac ccontr 1 THEN rtac hypreal_mult_not_0E 1);
-by Auto_tac;
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add,
+    hypreal_zero_def]));
 qed "hypreal_add_self_zero_cancel";
 Addsimps [hypreal_add_self_zero_cancel];
 
@@ -1525,16 +1227,17 @@
 Addsimps [hypreal_minus_eq_cancel];
 
 Goal "x < x + 1hr";
-by (cut_inst_tac [("C","x")] 
-    (hypreal_zero_less_one RS hypreal_add_less_mono2) 1);
-by (Asm_full_simp_tac 1);
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add,
+    hypreal_one_def,hypreal_less]));
 qed "hypreal_less_self_add_one";
 Addsimps [hypreal_less_self_add_one];
 
 Goal "((x::hypreal) + x = y + y) = (x = y)";
-by (auto_tac (claset() addIs [hypreal_two_not_zero RS 
-     hypreal_mult_left_cancel RS iffD1],simpset() addsimps 
-     [hypreal_add_mult_distrib]));
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [hypreal_add]));
+by (ALLGOALS(Ultra_tac));
 qed "hypreal_add_self_cancel";
 Addsimps [hypreal_add_self_cancel];
 
@@ -1552,44 +1255,19 @@
 qed "hypreal_add_self_minus_cancel2";
 Addsimps [hypreal_add_self_minus_cancel2];
 
+(* of course, can prove this by "transfer" as well *)
 Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))";
 by Auto_tac;
 by (dres_inst_tac [("x1","z")] 
     (hypreal_add_right_cancel RS iffD2) 1);
 by (asm_full_simp_tac (simpset() addsimps 
-    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac) 1);
+    [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac
+    delsimps [hypreal_minus_add_distrib]) 1);
 by (asm_full_simp_tac (simpset() addsimps 
      [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1);
 qed "hypreal_add_self_minus_cancel3";
 Addsimps [hypreal_add_self_minus_cancel3];
 
-(* check why this does not work without 2nd substiution anymore! *)
-Goal "x < y ==> x < (x + y)*hrinv(1hr + 1hr)";
-by (dres_inst_tac [("C","x")] hypreal_add_less_mono2 1);
-by (dtac (hypreal_add_self RS subst) 1);
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
-          hypreal_mult_less_mono1) 1);
-by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
-          (hypreal_mult_hrinv RS subst)],simpset() 
-          addsimps [hypreal_mult_assoc]));
-qed "hypreal_less_half_sum";
-
-(* check why this does not work without 2nd substiution anymore! *)
-Goal "x < y ==> (x + y)*hrinv(1hr + 1hr) < y";
-by (dres_inst_tac [("C","y")] hypreal_add_less_mono1 1);
-by (dtac (hypreal_add_self RS subst) 1);
-by (dtac (hypreal_zero_less_two RS hypreal_hrinv_gt_zero RS 
-          hypreal_mult_less_mono1) 1);
-by (auto_tac (claset() addDs [hypreal_two_not_zero RS 
-          (hypreal_mult_hrinv RS subst)],simpset() 
-          addsimps [hypreal_mult_assoc]));
-qed "hypreal_gt_half_sum";
-
-Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
-by (blast_tac (claset() addSIs [hypreal_less_half_sum,
-    hypreal_gt_half_sum]) 1);
-qed "hypreal_dense";
-
 Goal "(x * x = 0) = (x = (0::hypreal))";
 by Auto_tac;
 by (blast_tac (claset() addIs [hypreal_mult_not_0E]) 1);
@@ -1601,249 +1279,84 @@
 qed "hypreal_mult_self_eq_zero_iff2";
 Addsimps [hypreal_mult_self_eq_zero_iff2];
 
-Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))";
-by Auto_tac;
-by (dtac (sym RS (hypreal_eq_minus_iff3 RS iffD1))  1);
-by (dtac (sym RS (hypreal_eq_minus_iff4 RS iffD1))  2);
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (cut_inst_tac [("x1","x")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 1);
-by (cut_inst_tac [("x1","y")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 2);
-by (auto_tac (claset() addDs [sym],simpset()));
-by (dres_inst_tac [("x1","y")] (hypreal_less_minus_square 
-    RS hypreal_le_less_trans) 1);
-by (dres_inst_tac [("x1","x")] (hypreal_less_minus_square 
-    RS hypreal_le_less_trans) 2);
-by (auto_tac (claset(),simpset() addsimps 
-       [hypreal_less_not_refl]));
-qed "hypreal_squares_add_zero_iff";
-Addsimps [hypreal_squares_add_zero_iff];
+Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
+by (rtac hypreal_less_minus_iff2 1);
+qed "hypreal_less_eq_diff";
 
-Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
-by (cut_inst_tac [("x1","x")] (hypreal_le_square 
-        RS hypreal_le_imp_less_or_eq) 1);
-by (auto_tac (claset() addSIs 
-              [hypreal_add_order_le],simpset()));
-qed "hypreal_sum_squares3_gt_zero";
+(*** Subtraction laws ***)
 
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero2";
-
-Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
-by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
-qed "hypreal_sum_squares3_gt_zero3";
+Goal "x + (y - z) = (x + y) - (z::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_add_diff_eq";
 
-Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
-by Auto_tac;
-by (ALLGOALS(rtac ccontr));
-by (ALLGOALS(dtac hypreal_mult_self_not_zero));
-by (auto_tac (claset() addDs [hypreal_not_refl2 RS not_sym,
-   hypreal_sum_squares3_gt_zero3,hypreal_sum_squares3_gt_zero,
-   hypreal_sum_squares3_gt_zero2],simpset() delsimps
-   [hypreal_mult_self_eq_zero_iff]));
-qed "hypreal_three_squares_add_zero_iff";
-Addsimps [hypreal_three_squares_add_zero_iff];
+Goal "(x - y) + z = (x + z) - (y::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_diff_add_eq";
 
-Addsimps [rename_numerals real_le_square];
-Goal "(x::hypreal)*x <= x*x + y*y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [hypreal_mult,hypreal_add,hypreal_le]));
-qed "hypreal_self_le_add_pos";
-Addsimps [hypreal_self_le_add_pos];
+Goal "(x - y) - z = x - (y + (z::hypreal))";
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_diff_diff_eq";
 
-Goal "(x::hypreal)*x <= x*x + y*y + z*z";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
-				  rename_numerals real_le_add_order]));
-qed "hypreal_self_le_add_pos2";
-Addsimps [hypreal_self_le_add_pos2];
+Goal "x - (y - z) = (x + z) - (y::hypreal)";
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_diff_diff_eq2";
 
-(*---------------------------------------------------------------------------------
-             Embedding of the naturals in the hyperreals
- ---------------------------------------------------------------------------------*)
-Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
-by (full_simp_tac (simpset() addsimps 
-    [pnat_one_iff RS sym,real_of_preal_def]) 1);
-by (fold_tac [real_one_def]);
-by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1);
-qed "hypreal_of_posnat_one";
-
-Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr";
-by (full_simp_tac (simpset() addsimps 
-		   [real_of_preal_def,
-		    rename_numerals (real_one_def RS meta_eq_to_obj_eq),
-		    hypreal_add,hypreal_of_real_def,pnat_two_eq,
-		    hypreal_one_def, real_add,
-		    prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ 
-		    pnat_add_ac) 1);
-qed "hypreal_of_posnat_two";
+Goal "(x-y < z) = (x < z + (y::hypreal))";
+by (stac hypreal_less_eq_diff 1);
+by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1);
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_diff_less_eq";
 
-Goalw [hypreal_of_posnat_def]
-          "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \
-\          hypreal_of_posnat (n1 + n2) + 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one RS sym,
-    hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym,
-    preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1);
-qed "hypreal_of_posnat_add";
-
-Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr";
-by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1);
-by (rtac (hypreal_of_posnat_add RS subst) 1);
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1);
-qed "hypreal_of_posnat_add_one";
+Goal "(x < z-y) = (x + (y::hypreal) < z)";
+by (stac hypreal_less_eq_diff 1);
+by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1);
+by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
+qed "hypreal_less_diff_eq";
 
-Goalw [real_of_posnat_def,hypreal_of_posnat_def] 
-      "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)";
-by (rtac refl 1);
-qed "hypreal_of_real_of_posnat";
-
-Goalw [hypreal_of_posnat_def] 
-      "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)";
-by Auto_tac;
-qed "hypreal_of_posnat_less_iff";
-
-Addsimps [hypreal_of_posnat_less_iff RS sym];
-(*---------------------------------------------------------------------------------
-               Existence of infinite hyperreal number
- ---------------------------------------------------------------------------------*)
-
-Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal";
-by Auto_tac;
-qed "hypreal_omega";
+Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))";
+by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1);
+qed "hypreal_diff_le_eq";
 
-Goalw [omega_def] "Rep_hypreal(whr) : hypreal";
-by (rtac Rep_hypreal 1);
-qed "Rep_hypreal_omega";
-
-(* existence of infinite number not corresponding to any real number *)
-(* use assumption that member FreeUltrafilterNat is not finite       *)
-(* a few lemmas first *)
-
-Goal "{n::nat. x = real_of_posnat n} = {} | \
-\     (EX y. {n::nat. x = real_of_posnat n} = {y})";
-by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset()));
-qed "lemma_omega_empty_singleton_disj";
+Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)";
+by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
+qed "hypreal_le_diff_eq";
 
-Goal "finite {n::nat. x = real_of_posnat n}";
-by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1);
-by Auto_tac;
-qed "lemma_finite_omega_set";
-
-Goalw [omega_def,hypreal_of_real_def] 
-      "~ (EX x. hypreal_of_real x = whr)";
-by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set 
-    RS FreeUltrafilterNat_finite]));
-qed "not_ex_hypreal_of_real_eq_omega";
-
-Goal "hypreal_of_real x ~= whr";
-by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
-by Auto_tac;
-qed "hypreal_of_real_not_eq_omega";
+Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))";
+by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
+qed "hypreal_diff_eq_eq";
 
-(* existence of infinitesimal number also not *)
-(* corresponding to any real number *)
-
-Goal "{n::nat. x = rinv(real_of_posnat n)} = {} | \
-\     (EX y. {n::nat. x = rinv(real_of_posnat n)} = {y})";
-by (Step_tac 1 THEN Step_tac 1);
-by (auto_tac (claset() addIs [real_of_posnat_rinv_inj],simpset()));
-qed "lemma_epsilon_empty_singleton_disj";
-
-Goal "finite {n::nat. x = rinv(real_of_posnat n)}";
-by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
-by Auto_tac;
-qed "lemma_finite_epsilon_set";
+Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)";
+by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
+qed "hypreal_eq_diff_eq";
 
-Goalw [epsilon_def,hypreal_of_real_def] 
-      "~ (EX x. hypreal_of_real x = ehr)";
-by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set 
-    RS FreeUltrafilterNat_finite]));
-qed "not_ex_hypreal_of_real_eq_epsilon";
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+  to the top and then moving negative terms to the other side.  
+  Use with hypreal_add_ac*)
+val hypreal_compare_rls = 
+  [symmetric hypreal_diff_def,
+   hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, hypreal_diff_diff_eq2, 
+   hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, hypreal_le_diff_eq, 
+   hypreal_diff_eq_eq, hypreal_eq_diff_eq];
 
-Goal "hypreal_of_real x ~= ehr";
-by (cut_facts_tac [not_ex_hypreal_of_real_eq_epsilon] 1);
-by Auto_tac;
-qed "hypreal_of_real_not_eq_epsilon";
-
-Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
-by (auto_tac (claset(),
-     simpset() addsimps [rename_numerals real_of_posnat_rinv_not_zero]));
-qed "hypreal_epsilon_not_zero";
 
-Addsimps [rename_numerals real_of_posnat_not_eq_zero];
-Goalw [omega_def,hypreal_zero_def] "whr ~= 0";
-by (Simp_tac 1);
-qed "hypreal_omega_not_zero";
-
-Goal "ehr = hrinv(whr)";
-by (asm_full_simp_tac (simpset() addsimps 
-    [hypreal_hrinv,omega_def,epsilon_def]
-    addsplits [split_if]) 1);
-qed "hypreal_epsilon_hrinv_omega";
+(** For the cancellation simproc.
+    The idea is to cancel like terms on opposite sides by subtraction **)
 
-(*----------------------------------------------------------------
-     Another embedding of the naturals in the 
-    hyperreals (see hypreal_of_posnat)
- ----------------------------------------------------------------*)
-Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1);
-qed "hypreal_of_nat_zero";
-
-Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
-    hypreal_add_assoc]) 1);
-qed "hypreal_of_nat_one";
+Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')";
+by (stac hypreal_less_eq_diff 1);
+by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1);
+by (Asm_simp_tac 1);
+qed "hypreal_less_eqI";
 
-Goalw [hypreal_of_nat_def]
-      "hypreal_of_nat n1 + hypreal_of_nat n2 = \
-\      hypreal_of_nat (n1 + n2)";
-by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1);
-by (simp_tac (simpset() addsimps [hypreal_of_posnat_add,
-    hypreal_add_assoc RS sym]) 1);
-by (rtac (hypreal_add_commute RS subst) 1);
-by (simp_tac (simpset() addsimps [hypreal_add_left_cancel,
-    hypreal_add_assoc]) 1);
-qed "hypreal_of_nat_add";
-
-Goal "hypreal_of_nat 2 = 1hr + 1hr";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_one 
-    RS sym,hypreal_of_nat_add]) 1);
-qed "hypreal_of_nat_two";
+Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')";
+by (dtac hypreal_less_eqI 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1);
+qed "hypreal_le_eqI";
 
-Goalw [hypreal_of_nat_def] 
-      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)";
-by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset()));
-by (dres_inst_tac [("C","1hr")] hypreal_add_less_mono1 1);
-by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
-qed "hypreal_of_nat_less_iff";
-Addsimps [hypreal_of_nat_less_iff RS sym];
+Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')";
+by Safe_tac;
+by (ALLGOALS
+    (asm_full_simp_tac
+     (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
+qed "hypreal_eq_eqI";
 
-(* naturals embedded in hyperreals is an hyperreal *)
-Goalw [hypreal_of_nat_def,real_of_nat_def] 
-      "hypreal_of_nat  m = Abs_hypreal(hyprel^^{%n. real_of_nat m})";
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def,
-    hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add]));
-qed "hypreal_of_nat_iff";
-
-Goal "inj hypreal_of_nat";
-by (rtac injI 1);
-by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
-        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
-        real_add_right_cancel,inj_real_of_nat RS injD]));
-qed "inj_hypreal_of_nat";
-
-Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def,
-       real_of_posnat_def,hypreal_one_def,real_of_nat_def] 
-       "hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
-by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
-qed "hypreal_of_nat_real_of_nat";

--- a/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/Hyperreal/README.html	Thu Sep 21 12:11:38 2000 +0200
@@ -9,7 +9,39 @@
 
 <LI><A HREF="Filter.html">Filter</A>
 Theory of Filters and Ultrafilters.
-Main result is a version of the Ultrafilter Theorem proved using Zorn's Lemma.
+Main result is a version of the Ultrafilter Theorem proved using
+Zorn's Lemma. 
+
+<LI><A HREF="HyperDef.html">HyperDef</A>
+Ultrapower construction of the hyperreals
+
+<LI><A HREF="NSA.html">NSA</A>
+Theory defining sets of infinite numbers, infinitesimals, 
+the infinitely close relation, and their various algebraic properties.
+
+<LI><A HREF="HyperNat.html">HyperNat</A>
+Ultrapower construction of the hypernaturals
+
+<LI><A HREF="HyperPow.html">HyperPow</A>
+Powers theory for the hyperreals
+
+<LI><A HREF="Star.html">Star</A>
+Nonstandard extensions of real sets and real functions
+
+<LI><A HREF="NatStar.html">NatStar</A>
+Nonstandard extensions of sets of naturals and functions on the natural
+numbers
+
+<LI><A HREF="SEQ.html">SEQ</A>
+Theory of sequences developed using standard and nonstandard analysis
+
+<LI><A HREF="Lim.html">Lim</A>
+Theory of limits, continuous functions, and derivatives
+
+<LI><A HREF="Series.html">Series</A>
+Standard theory of finite summation and infinite series
+
+
 </UL>
 
 <P>Last modified on $Date$
@@ -21,3 +53,4 @@
 </ADDRESS>
 </BODY></HTML>
 
+

--- a/src/HOL/Real/ROOT.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/ROOT.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -3,7 +3,13 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
+Construction of the Reals using Dedekind Cuts, Ultrapower Construction
+of the hyperreals, and mechanization of Nonstandard Real Analysis  
+                        by Jacques Fleuriot
 *)
 
-with_path "Hyperreal" use_thy "HyperDef";
+time_use_thy "Real";
+with_path "Hyperreal" use_thy "Series";
+
+
+

--- a/src/HOL/Real/RealAbs.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/RealAbs.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -271,3 +271,14 @@
 by (auto_tac (claset(),simpset() addsimps [abs_interval_iff]));
 qed "abs_diff_less_imp_gt_zero4";
 
+Goalw [abs_real_def] 
+     " abs(x) <= abs(x + (-y)) + abs((y::real))";
+by Auto_tac;
+qed "abs_triangle_ineq_minus_cancel";
+
+Goal "abs ((x::real) + y + (-l + -m)) <= abs(x + -l) + abs(y + -m)";
+by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
+by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
+by (rtac (real_add_assoc RS subst) 1);
+by (rtac abs_triangle_ineq 1);
+qed "abs_sum_triangle_ineq";

--- a/src/HOL/Real/RealDef.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -422,10 +422,6 @@
 				       real_minus_mult_eq1 RS sym]) 1);
 qed "real_minus_mult_commute";
 
-(*-----------------------------------------------------------------------------
-
- ----------------------------------------------------------------------------*)
-
 (** Lemmas **)
 
 Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
@@ -653,9 +649,6 @@
 (* [| x < y;  ~P ==> y < x |] ==> P *)
 bind_thm ("real_less_asym", real_less_not_sym RS swap);
 
-(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
-    (****** Map and more real_less ******)
-(*** mapping from preal into real ***)
 Goalw [real_of_preal_def] 
      "real_of_preal ((z1::preal) + z2) = \
 \     real_of_preal z1 + real_of_preal z2";

--- a/src/HOL/Real/RealOrd.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -428,6 +428,12 @@
 qed "real_of_posnat_rinv_gt_zero";
 Addsimps [real_of_posnat_rinv_gt_zero];
 
+Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \
+\     real_of_nat (Suc N)";
+by (simp_tac (simpset() addsimps [real_of_nat_def,real_of_posnat_Suc,
+    real_add_assoc,(real_of_posnat_def RS meta_eq_to_obj_eq) RS sym]) 1);
+qed "real_of_preal_real_of_nat_Suc";
+
 Goal "x+x = x*(1r+1r)";
 by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
 qed "real_add_self";

--- a/src/HOL/Real/RealPow.ML	Thu Sep 21 10:42:49 2000 +0200
+++ b/src/HOL/Real/RealPow.ML	Thu Sep 21 12:11:38 2000 +0200
@@ -107,6 +107,11 @@
 qed "abs_realpow_minus_one";
 Addsimps [abs_realpow_minus_one];
 
+Goal "abs((#-1) ^ n) = (#1::real)";
+by (rtac (simplify (simpset()) abs_realpow_minus_one) 1);
+qed "abs_realpow_minus_one2";
+Addsimps [abs_realpow_minus_one2];
+
 Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
 by (induct_tac "n" 1);
 by (auto_tac (claset(),simpset() addsimps real_mult_ac));