# HG changeset patch
# User paulson
# Date 976700085 -3600
# Node ID a196b944569b6d5bcd44d5036a493cff8d691648
# Parent  58b6cfd8ecf3bad90cfd22bd35a7fbbe2c5ef33a
another round of tidying-up

diff -r 58b6cfd8ecf3 -r a196b944569b src/HOL/Real/RealArith.ML
--- a/src/HOL/Real/RealArith.ML	Wed Dec 13 10:34:31 2000 +0100
+++ b/src/HOL/Real/RealArith.ML	Wed Dec 13 10:34:45 2000 +0100
@@ -28,6 +28,16 @@
 qed "real_inverse_less_0_iff";
 AddIffs [real_inverse_less_0_iff];
 
+Goal "((#0::real) <= inverse x) = (#0 <= x)";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
+qed "real_0_le_inverse_iff";
+AddIffs [real_0_le_inverse_iff];
+
+Goal "(inverse x <= (#0::real)) = (x <= #0)";
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
+qed "real_inverse_le_0_iff";
+AddIffs [real_inverse_le_0_iff];
+
 Goalw [real_divide_def] "x/(#0::real) = #0";
 by (stac (rename_numerals INVERSE_ZERO) 1); 
 by (Simp_tac 1); 
@@ -59,9 +69,12 @@
 (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
     but not (yet?) for k*m < n*k. **)
 
-bind_thm ("real_minus_less_minus", real_less_swap_iff RS sym);
 bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym);
 
+Goal "(-y < -x) = ((x::real) < y)";
+by (arith_tac 1);
+qed "real_minus_less_minus";
+
 Goal "[| i<j;  k < (0::real) |] ==> j*k < i*k";
 by (rtac (real_minus_less_minus RS iffD1) 1);
 by (auto_tac (claset(), 
diff -r 58b6cfd8ecf3 -r a196b944569b src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Wed Dec 13 10:34:31 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML	Wed Dec 13 10:34:45 2000 +0100
@@ -96,12 +96,6 @@
 by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
 qed "real_less_all_real2";
 
-Goal "((x::real) < y) = (-y < -x)";
-by (rtac (real_less_sum_gt_0_iff RS subst) 1);
-by (res_inst_tac [("W1","x")] (real_less_sum_gt_0_iff RS subst) 1);
-by (simp_tac (simpset() addsimps [real_add_commute]) 1);
-qed "real_less_swap_iff";
-
 Goal "[| R + L = S;  (0::real) < L |] ==> R < S";
 by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
 by (auto_tac (claset(), simpset() addsimps real_add_ac));
@@ -117,32 +111,6 @@
 				real_ex_add_positive_left_less]) 1);
 qed "real_less_iff_add";
 
-Goal "((0::real) < x) = (-x < x)";
-by Safe_tac;
-by (rtac ccontr 2 THEN forward_tac 
-    [real_leI RS real_le_imp_less_or_eq] 2);
-by (Step_tac 2);
-by (dtac (real_minus_zero_less_iff RS iffD2) 2);
-by (blast_tac (claset() addIs [real_less_trans]) 2);
-by (auto_tac (claset(),
-	      simpset() addsimps 
- 	        [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
-qed "real_gt_zero_iff";
-
-Goal "(x < (0::real)) = (x < -x)";
-by (rtac (real_minus_zero_less_iff RS subst) 1);
-by (stac real_gt_zero_iff 1);
-by (Full_simp_tac 1);
-qed "real_lt_zero_iff";
-
-Goalw [real_le_def] "((0::real) <= x) = (-x <= x)";
-by (auto_tac (claset(), simpset() addsimps [real_lt_zero_iff RS sym]));
-qed "real_ge_zero_iff";
-
-Goalw [real_le_def] "(x <= (0::real)) = (x <= -x)";
-by (auto_tac (claset(), simpset() addsimps [real_gt_zero_iff RS sym]));
-qed "real_le_zero_iff";
-
 Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
 by (auto_tac (claset() addSIs [preal_leI],
     simpset() addsimps [real_less_le_iff RS sym]));