# HG changeset patch
# User paulson
# Date 1071585489 -3600
# Node ID 7c84fd26add1c6cb26294e2ea24de69d7fb816df
# Parent  bcba1d67f8541e03309df42f71156008699621c0
converted Hyperreal/HyperOrd to new-style theory

diff -r bcba1d67f854 -r 7c84fd26add1 src/HOL/Hyperreal/HyperOrd.ML
--- a/src/HOL/Hyperreal/HyperOrd.ML	Mon Dec 15 17:08:41 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,529 +0,0 @@
-(*  Title:	 Real/Hyperreal/HyperOrd.ML
-    Author:      Jacques D. Fleuriot
-    Copyright:   1998 University of Cambridge
-                 2000 University of Edinburgh
-    Description: Type "hypreal" is a linear order and also 
-                 satisfies plus_ac0: + is an AC-operator with zero
-*)
-
-(**** The simproc abel_cancel ****)
-
-(*** Two lemmas needed for the simprocs ***)
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-Goal "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)";
-by (stac hypreal_add_left_commute 1);
-by (rtac hypreal_add_left_cancel 1);
-qed "hypreal_add_cancel_21";
-
-(*A further rule to deal with the case that
-  everything gets cancelled on the right.*)
-Goal "((x::hypreal) + (y + z) = y) = (x = -z)";
-by (stac hypreal_add_left_commute 1);
-by (res_inst_tac [("t", "y")] (hypreal_add_zero_right RS subst) 1
-    THEN stac hypreal_add_left_cancel 1);
-by (simp_tac (simpset() addsimps [hypreal_eq_diff_eq RS sym]) 1);
-qed "hypreal_add_cancel_end";
-
-
-structure Hyperreal_Cancel_Data =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-
-  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
-  val T			= Type("HyperDef.hypreal",[])
-  val zero		= Const ("0", T)
-  val restrict_to_left  = restrict_to_left
-  val add_cancel_21	= hypreal_add_cancel_21
-  val add_cancel_end	= hypreal_add_cancel_end
-  val add_left_cancel	= hypreal_add_left_cancel
-  val add_assoc		= hypreal_add_assoc
-  val add_commute	= hypreal_add_commute
-  val add_left_commute	= hypreal_add_left_commute
-  val add_0		= hypreal_add_zero_left
-  val add_0_right	= hypreal_add_zero_right
-
-  val eq_diff_eq	= hypreal_eq_diff_eq
-  val eqI_rules		= [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
-  fun dest_eqI th = 
-      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
-	      (HOLogic.dest_Trueprop (concl_of th)))
-
-  val diff_def		= hypreal_diff_def
-  val minus_add_distrib	= hypreal_minus_add_distrib
-  val minus_minus	= hypreal_minus_minus
-  val minus_0		= hypreal_minus_zero
-  val add_inverses	= [hypreal_add_minus, hypreal_add_minus_left]
-  val cancel_simps	= [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
-end;
-
-structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
-
-Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
-
-Goal "- (z - y) = y - (z::hypreal)";
-by (Simp_tac 1);
-qed "hypreal_minus_diff_eq";
-Addsimps [hypreal_minus_diff_eq];
-
-
-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";
-
-Goalw [hypreal_zero_def] 
-      "((0::hypreal) < x) = (-x < x)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_less, hypreal_minus]));
-by (ALLGOALS(Ultra_tac));
-qed "hypreal_gt_zero_iff";
-
-Goal "(A::hypreal) < 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 < (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_zero_def] "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + 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_less_def,hypreal_add]));
-by (auto_tac (claset() addSIs [exI],
-              simpset() addsimps [hypreal_less_def,hypreal_add]));
-by (ultra_tac (claset() addIs [real_add_order], simpset()) 1);
-qed "hypreal_add_order";
-
-Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y";
-by (auto_tac (claset() addDs [sym, order_le_imp_less_or_eq]
-                       addIs [hypreal_add_order],
-              simpset()));
-qed "hypreal_add_order_le";            
-
-Goalw [hypreal_zero_def] "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * 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() addSIs [exI],
-              simpset() addsimps [hypreal_less_def,hypreal_mult]));
-by (ultra_tac (claset() addIs [real_mult_order], simpset()) 1);
-qed "hypreal_mult_order";
-
-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; 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 < (1::hypreal)";
-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 order_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le],
-              simpset()));
-qed "hypreal_le_add_order";
-
-(*** Monotonicity results ***)
-
-Goal "(v+z < w+z) = (v < (w::hypreal))";
-by (Simp_tac 1);
-qed "hypreal_add_right_cancel_less";
-
-Goal "(z+v < z+w) = (v < (w::hypreal))";
-by (Simp_tac 1);
-qed "hypreal_add_left_cancel_less";
-
-Addsimps [hypreal_add_right_cancel_less, 
-          hypreal_add_left_cancel_less];
-
-Goal "(v+z <= w+z) = (v <= (w::hypreal))";
-by (Simp_tac 1);
-qed "hypreal_add_right_cancel_le";
-
-Goal "(z+v <= z+w) = (v <= (w::hypreal))";
-by (Simp_tac 1);
-qed "hypreal_add_left_cancel_le";
-
-Addsimps [hypreal_add_right_cancel_le, hypreal_add_left_cancel_le];
-
-Goal  "[| (z1::hypreal) < 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
-                delsimps [hypreal_minus_add_distrib]));
-qed "hypreal_add_less_mono";
-
-Goal "(q1::hypreal) <= q2  ==> x + q1 <= x + q2";
-by (dtac order_le_imp_less_or_eq 1);
-by (Step_tac 1);
-by (auto_tac (claset() addSIs [order_less_imp_le,hypreal_add_less_mono1],
-              simpset() addsimps [hypreal_add_commute]));
-qed "hypreal_add_left_le_mono1";
-
-Goal "(q1::hypreal) <= 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 "[|(i::hypreal)<=j;  k<=l |] ==> i + k <= j + l";
-by (etac (hypreal_add_le_mono1 RS order_trans) 1);
-by (Simp_tac 1);
-qed "hypreal_add_le_mono";
-
-Goal "[|(i::hypreal)<j;  k<=l |] ==> i + k < j + l";
-by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
-                       addIs [hypreal_add_less_mono1,hypreal_add_less_mono],
-    simpset()));
-qed "hypreal_add_less_le_mono";
-
-Goal "[|(i::hypreal)<=j;  k<l |] ==> i + k < j + l";
-by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
-                       addIs [hypreal_add_less_mono2,hypreal_add_less_mono],
-              simpset()));
-qed "hypreal_add_le_less_mono";
-
-Goal "(A::hypreal) + C < B + C ==> A < B";
-by (Full_simp_tac 1);
-qed "hypreal_less_add_right_cancel";
-
-Goal "(C::hypreal) + A < C + B ==> A < B";
-by (Full_simp_tac 1);
-qed "hypreal_less_add_left_cancel";
-
-Goal "[|r < x; (0::hypreal) <= y|] ==> r < x + y";
-by (auto_tac (claset() addDs [hypreal_add_less_le_mono],
-    simpset()));
-qed "hypreal_add_zero_less_le_mono";
-
-Goal "!!(A::hypreal). A + C <= B + C ==> A <= B";
-by (dres_inst_tac [("x","-C")] hypreal_add_le_mono1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
-qed "hypreal_le_add_right_cancel";
-
-Goal "!!(A::hypreal). C + A <= C + B ==> A <= B";
-by (dres_inst_tac [("x","-C")] hypreal_add_left_le_mono1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
-qed "hypreal_le_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,order_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 order_le_less_trans],
-      simpset() addsimps [hypreal_minus_zero_less_iff]));
-qed "hypreal_less_minus_square";
-Addsimps [hypreal_less_minus_square];
-
-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 order_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";
-
-val prem1::prem2::prem3::rest = goal thy
-     "[| (0::hypreal)<y; x<r; y*r<t*s |] ==> y*x<t*s";
-by (rtac ([[prem1,prem2] MRS hypreal_mult_less_mono2, prem3] 
-          MRS order_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 order_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")] order_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [hypreal_mult_le_less_trans]) 1);
-qed "hypreal_mult_le_le_trans";
-
-Goal "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y";
-by (etac (hypreal_mult_less_mono1 RS order_less_trans) 1);
-by (assume_tac 1);
-by (etac hypreal_mult_less_mono2 1);
-by (assume_tac 1);
-qed "hypreal_mult_less_mono";
-
-(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
-Goal "[| x < y;  r1 < r2;  (0::hypreal) <= r1;  0 <= x|] ==> r1 * x < r2 * y";
-by (subgoal_tac "0<r2" 1);
-by (blast_tac (claset() addIs [order_le_less_trans]) 2); 
-by (case_tac "x=0" 1);
-by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
-	               addIs [hypreal_mult_less_mono, hypreal_mult_order],
-	      simpset()));
-qed "hypreal_mult_less_mono'";
-
-Goal "0 < x ==> 0 < inverse (x::hypreal)";
-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 hypreal_inverse_not_zero) 1);
-by (EVERY1[dtac order_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_inverse_gt_0";
-
-Goal "x < 0 ==> inverse (x::hypreal) < 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 (stac (hypreal_minus_inverse RS sym) 1);
-by (auto_tac (claset() addIs [hypreal_inverse_gt_0],  simpset()));
-qed "hypreal_inverse_less_0";
-
-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];
-
-(*lcp: new lemma unfortunately needed...*)
-Goal "-(x*x) <= (y*y::real)";
-by (rtac order_trans 1);
-by (rtac real_le_square 2);
-by Auto_tac;
-qed "minus_square_le_square";
-
-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,
-				  minus_square_le_square]));
-qed "hypreal_self_le_add_pos2";
-Addsimps [hypreal_self_le_add_pos2];
-
-
-(*----------------------------------------------------------------------------
-               Existence of infinite hyperreal number
- ----------------------------------------------------------------------------*)
-
-Goalw [omega_def] "Rep_hypreal(omega) : 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 n} = {} | \
-\     (EX y. {n::nat. x = real n} = {y})";
-by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset()));
-qed "lemma_omega_empty_singleton_disj";
-
-Goal "finite {n::nat. x = real 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 = omega)";
-by (auto_tac (claset(),
-    simpset() addsimps [real_of_nat_Suc, diff_eq_eq RS sym, 
-                    lemma_finite_omega_set RS FreeUltrafilterNat_finite]));
-qed "not_ex_hypreal_of_real_eq_omega";
-
-Goal "hypreal_of_real x ~= omega";
-by (cut_facts_tac [not_ex_hypreal_of_real_eq_omega] 1);
-by Auto_tac;
-qed "hypreal_of_real_not_eq_omega";
-
-(* existence of infinitesimal number also not *)
-(* corresponding to any real number *)
-
-Goal "inverse (real (x::nat)) = inverse (real y) ==> x = y";
-by (rtac (inj_real_of_nat RS injD) 1);
-by (Asm_full_simp_tac 1); 
-qed "real_of_nat_inverse_inj";
-
-Goal "{n::nat. x = inverse(real(Suc n))} = {} | \
-\     (EX y. {n::nat. x = inverse(real(Suc n))} = {y})";
-by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq]));
-qed "lemma_epsilon_empty_singleton_disj";
-
-Goal "finite {n. x = inverse(real(Suc n))}";
-by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1);
-by Auto_tac;
-qed "lemma_finite_epsilon_set";
-
-Goalw [epsilon_def,hypreal_of_real_def] 
-      "~ (EX x. hypreal_of_real x = epsilon)";
-by (auto_tac (claset(),
-  simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite]));
-qed "not_ex_hypreal_of_real_eq_epsilon";
-
-Goal "hypreal_of_real x ~= epsilon";
-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] "epsilon ~= 0";
-by Auto_tac;  
-by (auto_tac (claset(),
-     simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym]));
-qed "hypreal_epsilon_not_zero";
-
-Goal "epsilon = inverse(omega)";
-by (asm_full_simp_tac (simpset() addsimps 
-                     [hypreal_inverse, omega_def, epsilon_def]) 1);
-qed "hypreal_epsilon_inverse_omega";
-
-
-(* this proof is so much simpler than one for reals!! *)
-Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
-      simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def]));
-by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1);
-qed "hypreal_inverse_less_swap";
-
-Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
-by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset()));
-by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
-by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
-by (rtac hypreal_inverse_less_swap 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_gt_0]));
-qed "hypreal_inverse_less_iff";
-
-Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)";
-by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
-                                hypreal_inverse_gt_0]) 1);
-qed "hypreal_mult_inverse_less_mono1";
-
-Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y";
-by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
-                                hypreal_inverse_gt_0]) 1);
-qed "hypreal_mult_inverse_less_mono2";
-
-Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
-by (forw_inst_tac [("x","x*z")] hypreal_mult_inverse_less_mono1 1);
-by (dtac (hypreal_not_refl2 RS not_sym) 2);
-by (auto_tac (claset() addSDs [hypreal_mult_inverse],
-              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 [("y","r")] order_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 [order_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 order_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"; 
-
-(*----------------------------------------------------------------------------
-     Some convenient biconditionals for products of signs 
- ----------------------------------------------------------------------------*)
-
-Goal "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
- by (auto_tac (claset(), 
-               simpset() addsimps [order_le_less, linorder_not_less, 
-                              hypreal_mult_order, hypreal_mult_less_zero1]));
-by (ALLGOALS (rtac ccontr)); 
-by (auto_tac (claset(), 
-              simpset() addsimps [order_le_less, linorder_not_less]));
-by (ALLGOALS (etac rev_mp)); 
-by (ALLGOALS (dtac hypreal_mult_less_zero THEN' assume_tac));
-by (auto_tac (claset() addDs [order_less_not_sym], 
-              simpset() addsimps [hypreal_mult_commute]));  
-qed "hypreal_0_less_mult_iff";
-
-Goal "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
-by (auto_tac (claset() addDs [hypreal_mult_zero_disj],
-              simpset() addsimps [order_le_less, linorder_not_less,
-                                  hypreal_0_less_mult_iff]));
-qed "hypreal_0_le_mult_iff";
-
-Goal "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)";
-by (auto_tac (claset(), 
-              simpset() addsimps [hypreal_0_le_mult_iff, 
-                                  linorder_not_le RS sym]));
-by (auto_tac (claset() addDs [order_less_not_sym],  
-              simpset() addsimps [linorder_not_le]));
-qed "hypreal_mult_less_0_iff";
-
-Goal "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
-by (auto_tac (claset() addDs [order_less_not_sym], 
-              simpset() addsimps [hypreal_0_less_mult_iff, 
-                                  linorder_not_less RS sym]));
-qed "hypreal_mult_le_0_iff";
-
-Goal "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0";
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_commute,
-    hypreal_mult_less_zero]));
-qed "hypreal_mult_less_zero2";
diff -r bcba1d67f854 -r 7c84fd26add1 src/HOL/Hyperreal/HyperOrd.thy
--- a/src/HOL/Hyperreal/HyperOrd.thy	Mon Dec 15 17:08:41 2003 +0100
+++ b/src/HOL/Hyperreal/HyperOrd.thy	Tue Dec 16 15:38:09 2003 +0100
@@ -5,11 +5,543 @@
                  satisfies plus_ac0: + is an AC-operator with zero
 *)
 
-HyperOrd = HyperDef +
+theory HyperOrd = HyperDef:
+
+
+method_setup fuf = {*
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts =>
+            fuf_tac (Classical.get_local_claset ctxt,
+                     Simplifier.get_local_simpset ctxt) 1)) *}
+    "free ultrafilter tactic"
+
+method_setup ultra = {*
+    Method.ctxt_args (fn ctxt =>
+        Method.METHOD (fn facts =>
+            ultra_tac (Classical.get_local_claset ctxt,
+                       Simplifier.get_local_simpset ctxt) 1)) *}
+    "ultrafilter tactic"
+
+
+instance hypreal :: order
+  by (intro_classes,
+      (assumption | 
+       rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym
+            hypreal_less_le)+)
+
+instance hypreal :: linorder 
+  by (intro_classes, rule hypreal_le_linear)
+
+instance hypreal :: plus_ac0
+  by (intro_classes,
+      (assumption | 
+       rule hypreal_add_commute hypreal_add_assoc hypreal_add_zero_left)+)
+
+(**** The simproc abel_cancel ****)
+
+(*** Two lemmas needed for the simprocs ***)
+
+(*Deletion of other terms in the formula, seeking the -x at the front of z*)
+lemma hypreal_add_cancel_21: "((x::hypreal) + (y + z) = y + u) = ((x + z) = u)"
+apply (subst hypreal_add_left_commute)
+apply (rule hypreal_add_left_cancel)
+done
+
+(*A further rule to deal with the case that
+  everything gets cancelled on the right.*)
+lemma hypreal_add_cancel_end: "((x::hypreal) + (y + z) = y) = (x = -z)"
+apply (subst hypreal_add_left_commute)
+apply (rule_tac t = y in hypreal_add_zero_right [THEN subst], subst hypreal_add_left_cancel)
+apply (simp (no_asm) add: hypreal_eq_diff_eq [symmetric])
+done
+
+ML{*
+val hypreal_add_cancel_21 = thm "hypreal_add_cancel_21";
+val hypreal_add_cancel_end = thm "hypreal_add_cancel_end";
+
+structure Hyperreal_Cancel_Data =
+struct
+  val ss		= HOL_ss
+  val eq_reflection	= eq_reflection
+
+  val sg_ref		= Sign.self_ref (Theory.sign_of (the_context ()))
+  val T			= Type("HyperDef.hypreal",[])
+  val zero		= Const ("0", T)
+  val restrict_to_left  = restrict_to_left
+  val add_cancel_21	= hypreal_add_cancel_21
+  val add_cancel_end	= hypreal_add_cancel_end
+  val add_left_cancel	= hypreal_add_left_cancel
+  val add_assoc		= hypreal_add_assoc
+  val add_commute	= hypreal_add_commute
+  val add_left_commute	= hypreal_add_left_commute
+  val add_0		= hypreal_add_zero_left
+  val add_0_right	= hypreal_add_zero_right
+
+  val eq_diff_eq	= hypreal_eq_diff_eq
+  val eqI_rules		= [hypreal_less_eqI, hypreal_eq_eqI, hypreal_le_eqI]
+  fun dest_eqI th = 
+      #1 (HOLogic.dest_bin "op =" HOLogic.boolT
+	      (HOLogic.dest_Trueprop (concl_of th)))
+
+  val diff_def		= hypreal_diff_def
+  val minus_add_distrib	= hypreal_minus_add_distrib
+  val minus_minus	= hypreal_minus_minus
+  val minus_0		= hypreal_minus_zero
+  val add_inverses	= [hypreal_add_minus, hypreal_add_minus_left]
+  val cancel_simps	= [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]
+end;
+
+structure Hyperreal_Cancel = Abel_Cancel (Hyperreal_Cancel_Data);
+
+Addsimprocs [Hyperreal_Cancel.sum_conv, Hyperreal_Cancel.rel_conv];
+*}
+
+lemma hypreal_minus_diff_eq: "- (z - y) = y - (z::hypreal)"
+apply (simp (no_asm))
+done
+declare hypreal_minus_diff_eq [simp]
+
+
+lemma hypreal_less_swap_iff: "((x::hypreal) < y) = (-y < -x)"
+apply (subst hypreal_less_minus_iff)
+apply (rule_tac x1 = x in hypreal_less_minus_iff [THEN ssubst])
+apply (simp (no_asm) add: hypreal_add_commute)
+done
+
+lemma hypreal_gt_zero_iff: 
+      "((0::hypreal) < x) = (-x < x)"
+apply (unfold hypreal_zero_def)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (auto simp add: hypreal_less hypreal_minus, ultra+)
+done
+
+lemma hypreal_add_less_mono1: "(A::hypreal) < B ==> A + C < B + C"
+apply (rule_tac z = A in eq_Abs_hypreal)
+apply (rule_tac z = B in eq_Abs_hypreal)
+apply (rule_tac z = C in eq_Abs_hypreal)
+apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
+done
+
+lemma hypreal_add_less_mono2: "!!(A::hypreal). A < B ==> C + A < C + B"
+by (auto intro: hypreal_add_less_mono1 simp add: hypreal_add_commute)
+
+lemma hypreal_lt_zero_iff: "(x < (0::hypreal)) = (x < -x)"
+apply (rule hypreal_minus_zero_less_iff [THEN subst])
+apply (subst hypreal_gt_zero_iff)
+apply (simp (no_asm_use))
+done
+
+lemma hypreal_add_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + y"
+apply (unfold hypreal_zero_def)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (auto simp add: hypreal_less_def hypreal_add)
+apply (auto intro!: exI simp add: hypreal_less_def hypreal_add, ultra)
+done
+
+lemma hypreal_add_order_le: "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"
+by (auto dest: sym order_le_imp_less_or_eq intro: hypreal_add_order)
+
+lemma hypreal_mult_order: "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * y"
+apply (unfold hypreal_zero_def)
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (auto intro!: exI simp add: hypreal_less_def hypreal_mult, ultra)
+apply (auto intro: real_mult_order)
+done
+
+lemma hypreal_mult_less_zero1: "[| x < 0; y < 0 |] ==> (0::hypreal) < x * y"
+apply (drule hypreal_minus_zero_less_iff [THEN iffD2])+
+apply (drule hypreal_mult_order, assumption, simp)
+done
+
+lemma hypreal_mult_less_zero: "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"
+apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
+apply (drule hypreal_mult_order, assumption)
+apply (rule hypreal_minus_zero_less_iff [THEN iffD1], simp)
+done
+
+lemma hypreal_zero_less_one: "0 < (1::hypreal)"
+apply (unfold hypreal_one_def hypreal_zero_def hypreal_less_def)
+apply (rule_tac x = "%n. 0" in exI)
+apply (rule_tac x = "%n. 1" in exI)
+apply (auto simp add: real_zero_less_one FreeUltrafilterNat_Nat_set)
+done
+
+lemma hypreal_le_add_order: "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"
+apply (drule order_le_imp_less_or_eq)+
+apply (auto intro: hypreal_add_order order_less_imp_le)
+done
+
+(*** Monotonicity results ***)
+
+lemma hypreal_add_right_cancel_less: "(v+z < w+z) = (v < (w::hypreal))"
+apply (simp (no_asm))
+done
+
+lemma hypreal_add_left_cancel_less: "(z+v < z+w) = (v < (w::hypreal))"
+apply (simp (no_asm))
+done
+
+declare hypreal_add_right_cancel_less [simp] 
+        hypreal_add_left_cancel_less [simp]
+
+lemma hypreal_add_right_cancel_le: "(v+z <= w+z) = (v <= (w::hypreal))"
+apply (simp (no_asm))
+done
+
+lemma hypreal_add_left_cancel_le: "(z+v <= z+w) = (v <= (w::hypreal))"
+apply (simp (no_asm))
+done
+
+declare hypreal_add_right_cancel_le [simp] hypreal_add_left_cancel_le [simp]
+
+lemma hypreal_add_less_mono: "[| (z1::hypreal) < y1; z2 < y2 |] ==> z1 + z2 < y1 + y2"
+apply (drule hypreal_less_minus_iff [THEN iffD1])
+apply (drule hypreal_less_minus_iff [THEN iffD1])
+apply (drule hypreal_add_order, assumption)
+apply (erule_tac V = "0 < y2 + - z2" in thin_rl)
+apply (drule_tac C = "z1 + z2" in hypreal_add_less_mono1)
+apply (auto simp add: hypreal_minus_add_distrib [symmetric]
+              hypreal_add_ac simp del: hypreal_minus_add_distrib)
+done
+
+lemma hypreal_add_left_le_mono1: "(q1::hypreal) <= q2  ==> x + q1 <= x + q2"
+apply (drule order_le_imp_less_or_eq)
+apply (auto intro: order_less_imp_le hypreal_add_less_mono1 simp add: hypreal_add_commute)
+done
+
+lemma hypreal_add_le_mono1: "(q1::hypreal) <= q2  ==> q1 + x <= q2 + x"
+by (auto dest: hypreal_add_left_le_mono1 simp add: hypreal_add_commute)
+
+lemma hypreal_add_le_mono: "[|(i::hypreal)<=j;  k<=l |] ==> i + k <= j + l"
+apply (erule hypreal_add_le_mono1 [THEN order_trans])
+apply (simp (no_asm))
+done
+
+lemma hypreal_add_less_le_mono: "[|(i::hypreal)<j;  k<=l |] ==> i + k < j + l"
+by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono1 hypreal_add_less_mono)
+
+lemma hypreal_add_le_less_mono: "[|(i::hypreal)<=j;  k<l |] ==> i + k < j + l"
+by (auto dest!: order_le_imp_less_or_eq intro: hypreal_add_less_mono2 hypreal_add_less_mono)
+
+lemma hypreal_less_add_right_cancel: "(A::hypreal) + C < B + C ==> A < B"
+apply (simp (no_asm_use))
+done
+
+lemma hypreal_less_add_left_cancel: "(C::hypreal) + A < C + B ==> A < B"
+apply (simp (no_asm_use))
+done
+
+lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) <= y|] ==> r < x + y"
+by (auto dest: hypreal_add_less_le_mono)
+
+lemma hypreal_le_add_right_cancel: "!!(A::hypreal). A + C <= B + C ==> A <= B"
+apply (drule_tac x = "-C" in hypreal_add_le_mono1)
+apply (simp add: hypreal_add_assoc)
+done
+
+lemma hypreal_le_add_left_cancel: "!!(A::hypreal). C + A <= C + B ==> A <= B"
+apply (drule_tac x = "-C" in hypreal_add_left_le_mono1)
+apply (simp add: hypreal_add_assoc [symmetric])
+done
+
+lemma hypreal_le_square: "(0::hypreal) <= x*x"
+apply (rule_tac x = 0 and y = x in hypreal_linear_less2)
+apply (auto intro: hypreal_mult_order hypreal_mult_less_zero1 order_less_imp_le)
+done
+declare hypreal_le_square [simp]
+
+lemma hypreal_less_minus_square: "- (x*x) <= (0::hypreal)"
+apply (unfold hypreal_le_def)
+apply (auto dest!: hypreal_le_square [THEN order_le_less_trans] 
+            simp add: hypreal_minus_zero_less_iff)
+done
+declare hypreal_less_minus_square [simp]
+
+lemma hypreal_mult_0_less: "(0*x<r)=((0::hypreal)<r)"
+apply (simp (no_asm))
+done
+
+lemma hypreal_mult_less_mono1: "[| (0::hypreal) < z; x < y |] ==> x*z < y*z"
+apply (rotate_tac 1)
+apply (drule hypreal_less_minus_iff [THEN iffD1])
+apply (rule hypreal_less_minus_iff [THEN iffD2])
+apply (drule hypreal_mult_order, assumption)
+apply (simp add: hypreal_add_mult_distrib2 hypreal_mult_commute)
+done
 
-instance hypreal :: order (hypreal_le_refl,hypreal_le_trans,hypreal_le_anti_sym,hypreal_less_le)
-instance hypreal :: linorder (hypreal_le_linear)
+lemma hypreal_mult_less_mono2: "[| (0::hypreal)<z; x<y |] ==> z*x<z*y"
+apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_less_mono1)
+done
+
+lemma hypreal_mult_le_less_mono1: "[| (0::hypreal)<=z; x<y |] ==> x*z<=y*z"
+apply (rule hypreal_less_or_eq_imp_le)
+apply (drule order_le_imp_less_or_eq)
+apply (auto intro: hypreal_mult_less_mono1)
+done
+
+lemma hypreal_mult_le_less_mono2: "[| (0::hypreal)<=z; x<y |] ==> z*x<=z*y"
+apply (simp (no_asm_simp) add: hypreal_mult_commute hypreal_mult_le_less_mono1)
+done
+
+lemma hypreal_mult_less_mono: "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
+apply (erule hypreal_mult_less_mono1 [THEN order_less_trans], assumption)
+apply (erule hypreal_mult_less_mono2, assumption)
+done
+
+(*UNUSED at present but possibly more useful than hypreal_mult_less_mono*)
+lemma hypreal_mult_less_mono': "[| x < y;  r1 < r2;  (0::hypreal) <= r1;  0 <= x|] ==> r1 * x < r2 * y"
+apply (subgoal_tac "0<r2")
+prefer 2 apply (blast intro: order_le_less_trans)
+apply (case_tac "x=0")
+apply (auto dest!: order_le_imp_less_or_eq intro: hypreal_mult_less_mono hypreal_mult_order)
+done
+
+lemma hypreal_inverse_gt_0: "0 < x ==> 0 < inverse (x::hypreal)"
+apply (rule ccontr) 
+apply (drule hypreal_leI) 
+apply (frule hypreal_minus_zero_less_iff2 [THEN iffD2])
+apply (frule hypreal_not_refl2 [THEN not_sym])
+apply (drule hypreal_not_refl2 [THEN not_sym, THEN hypreal_inverse_not_zero])
+apply (drule order_le_imp_less_or_eq, safe) 
+apply (drule hypreal_mult_less_zero1, assumption)
+apply (auto intro: hypreal_zero_less_one [THEN hypreal_less_asym]
+            simp add: hypreal_minus_zero_less_iff)
+done
+
+lemma hypreal_inverse_less_0: "x < 0 ==> inverse (x::hypreal) < 0"
+apply (frule hypreal_not_refl2)
+apply (drule hypreal_minus_zero_less_iff [THEN iffD2])
+apply (rule hypreal_minus_zero_less_iff [THEN iffD1])
+apply (subst hypreal_minus_inverse [symmetric])
+apply (auto intro: hypreal_inverse_gt_0)
+done
+
+lemma hypreal_self_le_add_pos: "(x::hypreal)*x <= x*x + y*y"
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (auto simp add: hypreal_mult hypreal_add hypreal_le)
+done
+declare hypreal_self_le_add_pos [simp]
+
+(*lcp: new lemma unfortunately needed...*)
+lemma minus_square_le_square: "-(x*x) <= (y*y::real)"
+apply (rule order_trans)
+apply (rule_tac [2] real_le_square, auto)
+done
+
+lemma hypreal_self_le_add_pos2: "(x::hypreal)*x <= x*x + y*y + z*z"
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = z in eq_Abs_hypreal)
+apply (auto simp add: hypreal_mult hypreal_add hypreal_le minus_square_le_square)
+done
+declare hypreal_self_le_add_pos2 [simp]
+
+
+(*----------------------------------------------------------------------------
+               Existence of infinite hyperreal number
+ ----------------------------------------------------------------------------*)
+
+lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal"
+
+apply (unfold omega_def)
+apply (rule Rep_hypreal)
+done
+
+(* existence of infinite number not corresponding to any real number *)
+(* use assumption that member FreeUltrafilterNat is not finite       *)
+(* a few lemmas first *)
+
+lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
+      (EX y. {n::nat. x = real n} = {y})"
+by (force dest: inj_real_of_nat [THEN injD])
+
+lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
+by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
+
+lemma not_ex_hypreal_of_real_eq_omega: 
+      "~ (EX x. hypreal_of_real x = omega)"
+apply (unfold omega_def hypreal_of_real_def)
+apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
+done
+
+lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega"
+by (cut_tac not_ex_hypreal_of_real_eq_omega, auto)
+
+(* existence of infinitesimal number also not *)
+(* corresponding to any real number *)
+
+lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y"
+by (rule inj_real_of_nat [THEN injD], simp)
+
+lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} |  
+      (EX y. {n::nat. x = inverse(real(Suc n))} = {y})"
+apply (auto simp add: inj_real_of_nat [THEN inj_eq])
+done
+
+lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}"
+by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
+
+lemma not_ex_hypreal_of_real_eq_epsilon: 
+      "~ (EX x. hypreal_of_real x = epsilon)"
+apply (unfold epsilon_def hypreal_of_real_def)
+apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
+done
+
+lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon"
+by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
+
+lemma hypreal_epsilon_not_zero: "epsilon ~= 0"
+by (unfold epsilon_def hypreal_zero_def, auto)
+
+lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
+by (simp add: hypreal_inverse omega_def epsilon_def)
+
+
+(* this proof is so much simpler than one for reals!! *)
+lemma hypreal_inverse_less_swap: "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"
+apply (rule_tac z = x in eq_Abs_hypreal)
+apply (rule_tac z = r in eq_Abs_hypreal)
+apply (auto simp add: hypreal_inverse hypreal_less hypreal_zero_def, ultra)
+done
 
-instance hypreal :: plus_ac0(hypreal_add_commute,hypreal_add_assoc,hypreal_add_zero_left)
+lemma hypreal_inverse_less_iff: "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"
+apply (auto intro: hypreal_inverse_less_swap)
+apply (rule_tac t = r in hypreal_inverse_inverse [THEN subst])
+apply (rule_tac t = x in hypreal_inverse_inverse [THEN subst])
+apply (rule hypreal_inverse_less_swap)
+apply (auto simp add: hypreal_inverse_gt_0)
+done
+
+lemma hypreal_mult_inverse_less_mono1: "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)"
+by (blast intro!: hypreal_mult_less_mono1 hypreal_inverse_gt_0)
+
+lemma hypreal_mult_inverse_less_mono2: "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y"
+by (blast intro!: hypreal_mult_less_mono2 hypreal_inverse_gt_0)
+
+lemma hypreal_less_mult_right_cancel: "[| (0::hypreal) < z; x*z < y*z |] ==> x < y"
+apply (frule_tac x = "x*z" in hypreal_mult_inverse_less_mono1)
+apply (drule_tac [2] hypreal_not_refl2 [THEN not_sym])
+apply (auto dest!: hypreal_mult_inverse simp add: hypreal_mult_ac)
+done
+
+lemma hypreal_less_mult_left_cancel: "[| (0::hypreal) < z; z*x < z*y |] ==> x < y"
+by (auto intro: hypreal_less_mult_right_cancel simp add: hypreal_mult_commute)
+
+lemma hypreal_mult_less_gt_zero: "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y"
+apply (frule_tac y = r in order_less_trans)
+apply (drule_tac [2] z = ra and x = r in hypreal_mult_less_mono1)
+apply (drule_tac [3] z = x and x = ra in hypreal_mult_less_mono2)
+apply (auto intro: order_less_trans)
+done
+
+lemma hypreal_mult_le_ge_zero: "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y"
+apply (drule order_le_imp_less_or_eq)+
+apply (rule hypreal_less_or_eq_imp_le)
+apply (auto intro: hypreal_mult_less_mono1 hypreal_mult_less_mono2 hypreal_mult_less_gt_zero)
+done
+
+(*----------------------------------------------------------------------------
+     Some convenient biconditionals for products of signs 
+ ----------------------------------------------------------------------------*)
+
+lemma hypreal_0_less_mult_iff: "((0::hypreal) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
+ apply (auto simp add: order_le_less linorder_not_less hypreal_mult_order hypreal_mult_less_zero1)
+apply (rule_tac [!] ccontr)
+apply (auto simp add: order_le_less linorder_not_less)
+apply (erule_tac [!] rev_mp)
+apply (drule_tac [!] hypreal_mult_less_zero) 
+apply (auto dest: order_less_not_sym simp add: hypreal_mult_commute)
+done
+
+lemma hypreal_0_le_mult_iff: "((0::hypreal) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"
+by (auto dest: hypreal_mult_zero_disj simp add: order_le_less linorder_not_less hypreal_0_less_mult_iff)
+
+lemma hypreal_mult_less_0_iff: "(x*y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"
+apply (auto simp add: hypreal_0_le_mult_iff linorder_not_le [symmetric])
+apply (auto dest: order_less_not_sym simp add: linorder_not_le)
+done
+
+lemma hypreal_mult_le_0_iff: "(x*y <= (0::hypreal)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"
+by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric])
+
+lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0"
+by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero)
+
+
+ML
+{*
+val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21";
+val hypreal_add_cancel_end = thm"hypreal_add_cancel_end";
+val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq";
+val hypreal_less_swap_iff = thm"hypreal_less_swap_iff";
+val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff";
+val hypreal_add_less_mono1 = thm"hypreal_add_less_mono1";
+val hypreal_add_less_mono2 = thm"hypreal_add_less_mono2";
+val hypreal_lt_zero_iff = thm"hypreal_lt_zero_iff";
+val hypreal_add_order = thm"hypreal_add_order";
+val hypreal_add_order_le = thm"hypreal_add_order_le";
+val hypreal_mult_order = thm"hypreal_mult_order";
+val hypreal_mult_less_zero1 = thm"hypreal_mult_less_zero1";
+val hypreal_mult_less_zero = thm"hypreal_mult_less_zero";
+val hypreal_zero_less_one = thm"hypreal_zero_less_one";
+val hypreal_le_add_order = thm"hypreal_le_add_order";
+val hypreal_add_right_cancel_less = thm"hypreal_add_right_cancel_less";
+val hypreal_add_left_cancel_less = thm"hypreal_add_left_cancel_less";
+val hypreal_add_right_cancel_le = thm"hypreal_add_right_cancel_le";
+val hypreal_add_left_cancel_le = thm"hypreal_add_left_cancel_le";
+val hypreal_add_less_mono = thm"hypreal_add_less_mono";
+val hypreal_add_left_le_mono1 = thm"hypreal_add_left_le_mono1";
+val hypreal_add_le_mono1 = thm"hypreal_add_le_mono1";
+val hypreal_add_le_mono = thm"hypreal_add_le_mono";
+val hypreal_add_less_le_mono = thm"hypreal_add_less_le_mono";
+val hypreal_add_le_less_mono = thm"hypreal_add_le_less_mono";
+val hypreal_less_add_right_cancel = thm"hypreal_less_add_right_cancel";
+val hypreal_less_add_left_cancel = thm"hypreal_less_add_left_cancel";
+val hypreal_add_zero_less_le_mono = thm"hypreal_add_zero_less_le_mono";
+val hypreal_le_add_right_cancel = thm"hypreal_le_add_right_cancel";
+val hypreal_le_add_left_cancel = thm"hypreal_le_add_left_cancel";
+val hypreal_le_square = thm"hypreal_le_square";
+val hypreal_less_minus_square = thm"hypreal_less_minus_square";
+val hypreal_mult_0_less = thm"hypreal_mult_0_less";
+val hypreal_mult_less_mono1 = thm"hypreal_mult_less_mono1";
+val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
+val hypreal_mult_le_less_mono1 = thm"hypreal_mult_le_less_mono1";
+val hypreal_mult_le_less_mono2 = thm"hypreal_mult_le_less_mono2";
+val hypreal_mult_less_mono = thm"hypreal_mult_less_mono";
+val hypreal_mult_less_mono' = thm"hypreal_mult_less_mono'";
+val hypreal_inverse_gt_0 = thm"hypreal_inverse_gt_0";
+val hypreal_inverse_less_0 = thm"hypreal_inverse_less_0";
+val hypreal_self_le_add_pos = thm"hypreal_self_le_add_pos";
+val minus_square_le_square = thm"minus_square_le_square";
+val hypreal_self_le_add_pos2 = thm"hypreal_self_le_add_pos2";
+val Rep_hypreal_omega = thm"Rep_hypreal_omega";
+val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
+val lemma_finite_omega_set = thm"lemma_finite_omega_set";
+val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
+val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
+val real_of_nat_inverse_inj = thm"real_of_nat_inverse_inj";
+val lemma_epsilon_empty_singleton_disj = thm"lemma_epsilon_empty_singleton_disj";
+val lemma_finite_epsilon_set = thm"lemma_finite_epsilon_set";
+val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
+val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
+val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
+val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
+val hypreal_inverse_less_swap = thm"hypreal_inverse_less_swap";
+val hypreal_inverse_less_iff = thm"hypreal_inverse_less_iff";
+val hypreal_mult_inverse_less_mono1 = thm"hypreal_mult_inverse_less_mono1";
+val hypreal_mult_inverse_less_mono2 = thm"hypreal_mult_inverse_less_mono2";
+val hypreal_less_mult_right_cancel = thm"hypreal_less_mult_right_cancel";
+val hypreal_less_mult_left_cancel = thm"hypreal_less_mult_left_cancel";
+val hypreal_mult_less_gt_zero = thm"hypreal_mult_less_gt_zero";
+val hypreal_mult_le_ge_zero = thm"hypreal_mult_le_ge_zero";
+val hypreal_0_less_mult_iff = thm"hypreal_0_less_mult_iff";
+val hypreal_0_le_mult_iff = thm"hypreal_0_le_mult_iff";
+val hypreal_mult_less_0_iff = thm"hypreal_mult_less_0_iff";
+val hypreal_mult_le_0_iff = thm"hypreal_mult_le_0_iff";
+val hypreal_mult_less_zero2 = thm"hypreal_mult_less_zero2";
+*}
 
 end
diff -r bcba1d67f854 -r 7c84fd26add1 src/HOL/Hyperreal/fuf.ML
--- a/src/HOL/Hyperreal/fuf.ML	Mon Dec 15 17:08:41 2003 +0100
+++ b/src/HOL/Hyperreal/fuf.ML	Tue Dec 16 15:38:09 2003 +0100
@@ -60,14 +60,6 @@
 
 
 (*---------------------------------------------------------------
-  All in one -- not really needed.
- ---------------------------------------------------------------*)
-
-fun fuf_auto_tac css i = SOLVE (fuf_empty_tac css i) ORELSE TRY (fuf_tac css i);
-fun Fuf_auto_tac i = fuf_auto_tac (clasimpset ()) i;
-
-
-(*---------------------------------------------------------------
    In fact could make this the only tactic: just need to
    use contraposition and then look for empty set.
  ---------------------------------------------------------------*)
diff -r bcba1d67f854 -r 7c84fd26add1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Dec 15 17:08:41 2003 +0100
+++ b/src/HOL/IsaMakefile	Tue Dec 16 15:38:09 2003 +0100
@@ -153,7 +153,7 @@
   Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
   Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
-  Hyperreal/HyperOrd.ML Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
+  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
   Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\