# HG changeset patch
# User huffman
# Date 1231438059 28800
# Node ID 5ef7e97fd9e4aa34ea5649492faa6c35a170f4d2
# Parent  54bac26089bd9be92a9deed69d4f777dbbb7038f
move lemmas mult_minus{left,right} inside class ring

diff -r 54bac26089bd -r 5ef7e97fd9e4 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Jan 08 09:58:36 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Thu Jan 08 10:07:39 2009 -0800
@@ -235,19 +235,21 @@
 lemma minus_mult_right: "- (a * b) = a * - b"
   by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
 
+text{*Extract signs from products*}
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
-  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+  by simp
 
 lemma minus_mult_commute: "- a * b = a * - b"
-  by (simp add: minus_mult_left [symmetric] minus_mult_right [symmetric])
+  by simp
 
 lemma right_diff_distrib: "a * (b - c) = a * b - a * c"
-  by (simp add: right_distrib diff_minus 
-    minus_mult_left [symmetric] minus_mult_right [symmetric]) 
+  by (simp add: right_distrib diff_minus)
 
 lemma left_diff_distrib: "(a - b) * c = a * c - b * c"
-  by (simp add: left_distrib diff_minus 
-    minus_mult_left [symmetric] minus_mult_right [symmetric]) 
+  by (simp add: left_distrib diff_minus)
 
 lemmas ring_distribs =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
@@ -1246,19 +1248,19 @@
 subsection {* Division and Unary Minus *}
 
 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left)
+by (simp add: divide_inverse)
 
 lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a/b) = a / -(b::'a::field)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq minus_mult_right)
+by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
 lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a)/(-b) = a / (b::'a::field)"
 by (simp add: divide_inverse nonzero_inverse_minus_eq)
 
 lemma minus_divide_left: "- (a/b) = (-a) / (b::'a::field)"
-by (simp add: divide_inverse minus_mult_left [symmetric])
+by (simp add: divide_inverse)
 
 lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
-by (simp add: divide_inverse minus_mult_right [symmetric])
+by (simp add: divide_inverse)
 
 
 text{*The effect is to extract signs from divisions*}
@@ -1266,11 +1268,6 @@
 lemmas divide_minus_right = minus_divide_right [symmetric]
 declare divide_minus_left [simp]   divide_minus_right [simp]
 
-text{*Also, extract signs from products*}
-lemmas mult_minus_left = minus_mult_left [symmetric]
-lemmas mult_minus_right = minus_mult_right [symmetric]
-declare mult_minus_left [simp]   mult_minus_right [simp]
-
 lemma minus_divide_divide [simp]:
   "(-a)/(-b) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b=0", simp)