# HG changeset patch
# User nipkow
# Date 1008181341 -3600
# Node ID 0a01efff43e99e72a4fc96a5b96f56a31dac6535
# Parent  d2848ccc9757f5852aeb45ce4dc7e2b086613917
new rewrite rules for use by arith_tac to take care of uminus.

mods due to reorienting and renaming of real_minus_mult_eq1/2

diff -r d2848ccc9757 -r 0a01efff43e9 src/HOL/Real/RealArith0.ML
--- a/src/HOL/Real/RealArith0.ML	Wed Dec 12 19:21:54 2001 +0100
+++ b/src/HOL/Real/RealArith0.ML	Wed Dec 12 19:22:21 2001 +0100
@@ -99,8 +99,7 @@
 
 (** 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_mult_minus_right", real_minus_mult_eq2 RS sym);
+(* unused?? bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym); *)
 
 Goal "(-y < -x) = ((x::real) < y)";
 by (arith_tac 1);
@@ -109,16 +108,16 @@
 
 Goal "[| i<j;  k < (0::real) |] ==> j*k < i*k";
 by (rtac (real_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(), 
-              simpset() delsimps [real_minus_mult_eq2 RS sym]
+by (auto_tac (claset(),
+              simpset() delsimps [real_mult_minus_eq2]
                         addsimps [real_minus_mult_eq2])); 
 qed "real_mult_less_mono1_neg";
 
 Goal "[| i<j;  k < (0::real) |] ==> k*j < k*i";
 by (rtac (real_minus_less_minus RS iffD1) 1);
 by (auto_tac (claset(), 
-              simpset() delsimps [real_minus_mult_eq1 RS sym]
-                            addsimps [real_minus_mult_eq1]));;
+              simpset() delsimps [real_mult_minus_eq1]
+                        addsimps [real_minus_mult_eq1])); 
 qed "real_mult_less_mono2_neg";
 
 Goal "[| i <= j;  k <= (0::real) |] ==> j*k <= i*k";
diff -r d2848ccc9757 -r 0a01efff43e9 src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Wed Dec 12 19:21:54 2001 +0100
+++ b/src/HOL/Real/RealBin.ML	Wed Dec 12 19:22:21 2001 +0100
@@ -366,17 +366,19 @@
 (*To let us treat subtraction as addition*)
 val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus];
 
-(*push the unary minus down: - x * y = x * - y *)
+(*push the unary minus down: - x * y = x * - y
 val real_minus_mult_eq_1_to_2 = 
     [real_minus_mult_eq1 RS sym, real_minus_mult_eq2] MRS trans |> standard;
+same as real_minus_mult_commute
+*)
 
 (*to extract again any uncancelled minuses*)
 val real_minus_from_mult_simps = 
-    [real_minus_minus, real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
+    [real_minus_minus, real_mult_minus_eq1, real_mult_minus_eq2];
 
 (*combine unary minus with numeric literals, however nested within a product*)
 val real_mult_minus_simps =
-    [real_mult_assoc, real_minus_mult_eq1, real_minus_mult_eq_1_to_2];
+    [real_mult_assoc, real_minus_mult_eq1, real_minus_mult_commute];
 
 (*Apply the given rewrite (if present) just once*)
 fun trans_tac None      = all_tac
diff -r d2848ccc9757 -r 0a01efff43e9 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Wed Dec 12 19:21:54 2001 +0100
+++ b/src/HOL/Real/RealDef.ML	Wed Dec 12 19:22:21 2001 +0100
@@ -367,21 +367,23 @@
 
 Addsimps [real_mult_0_right, real_mult_0];
 
-Goal "-(x * y) = (-x) * (y::real)";
+Goal "(-x) * (y::real) = -(x * y)";
 by (res_inst_tac [("z","x")] eq_Abs_REAL 1);
 by (res_inst_tac [("z","y")] eq_Abs_REAL 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [real_minus,real_mult] 
                                  @ preal_mult_ac @ preal_add_ac));
-qed "real_minus_mult_eq1";
+qed "real_mult_minus_eq1";
+Addsimps [real_mult_minus_eq1];
+
+bind_thm("real_minus_mult_eq1", real_mult_minus_eq1 RS sym);
 
-Goal "-(x * y) = x * (- y :: real)";
-by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute,
-				  real_minus_mult_eq1]) 1);
-qed "real_minus_mult_eq2";
+Goal "x * (- y :: real) = -(x * y)";
+by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute]) 1);
+qed "real_mult_minus_eq2";
+Addsimps [real_mult_minus_eq2];
 
-(*Pull negations out*)
-Addsimps [real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
+bind_thm("real_minus_mult_eq2", real_mult_minus_eq2 RS sym);
 
 Goal "(- (1::real)) * z = -z";
 by (Simp_tac 1);
@@ -395,15 +397,13 @@
 Addsimps [real_mult_minus_1_right];
 
 Goal "(-x) * (-y) = x * (y::real)";
-by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
-				       real_minus_mult_eq1 RS sym]) 1);
+by (Simp_tac 1);
 qed "real_minus_mult_cancel";
 
 Addsimps [real_minus_mult_cancel];
 
 Goal "(-x) * y = x * (- y :: real)";
-by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
-				       real_minus_mult_eq1 RS sym]) 1);
+by (Simp_tac 1);
 qed "real_minus_mult_commute";
 
 (** Lemmas **)
diff -r d2848ccc9757 -r 0a01efff43e9 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Wed Dec 12 19:21:54 2001 +0100
+++ b/src/HOL/Real/RealPow.ML	Wed Dec 12 19:22:21 2001 +0100
@@ -305,8 +305,7 @@
 
 Goalw [real_diff_def] "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)";
 by (simp_tac (simpset() addsimps 
-              [real_add_mult_distrib2, real_add_mult_distrib, 
-               real_minus_mult_eq2 RS sym] @ real_mult_ac) 1);
+            [real_add_mult_distrib2, real_add_mult_distrib] @ real_mult_ac) 1);
 qed "realpow_two_diff";
 
 Goalw [real_diff_def] "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)";
diff -r d2848ccc9757 -r 0a01efff43e9 src/HOL/Real/real_arith0.ML
--- a/src/HOL/Real/real_arith0.ML	Wed Dec 12 19:21:54 2001 +0100
+++ b/src/HOL/Real/real_arith0.ML	Wed Dec 12 19:22:21 2001 +0100
@@ -20,7 +20,7 @@
      real_add_minus, real_add_minus_left,
      real_mult_0, real_mult_0_right,
      real_mult_1, real_mult_1_right,
-     real_mult_minus_1, real_mult_minus_1_right];
+     real_mult_minus_eq1, real_mult_minus_eq2];
 
 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
                Real_Numeral_Simprocs.cancel_numerals @