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
--- 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";
--- 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
--- 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 **)
--- 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)";
--- 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 @