src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Mon Jun 25 14:49:32 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Jun 25 15:19:18 2007 +0200
@@ -780,7 +780,7 @@
   "(a*b = (0::'a::division_ring)) = (a = 0 | b = 0)"
 by simp
 *)
-
+(* subsumed by mult_cancel lemmas on ring_no_zero_divisors
 text{*Cancellation of equalities with a common factor*}
 lemma field_mult_cancel_right_lemma:
       assumes cnz: "c \<noteq> (0::'a::division_ring)"
@@ -800,7 +800,7 @@
 lemma field_mult_cancel_left [simp]:
      "(c*a = c*b) = (c = (0::'a::division_ring) | a=b)"
 by simp
-
+*)
 lemma nonzero_imp_inverse_nonzero:
   "a \<noteq> 0 ==> inverse a \<noteq> (0::'a::division_ring)"
 proof
@@ -837,7 +837,7 @@
   have "-a * inverse (- a) = -a * - inverse a"
     by simp
   thus ?thesis 
-    by (simp only: field_mult_cancel_left, simp)
+    by (simp only: mult_cancel_left, simp)
 qed
 
 lemma inverse_minus_eq [simp]:
@@ -1119,20 +1119,16 @@
 lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
 proof -
   assume [simp]: "c\<noteq>0"
-  have "(a = b/c) = (a*c = (b/c)*c)"
-    by (simp add: field_mult_cancel_right)
-  also have "... = (a*c = b)"
-    by (simp add: divide_inverse mult_assoc)
+  have "(a = b/c) = (a*c = (b/c)*c)" by simp
+  also have "... = (a*c = b)" by (simp add: divide_inverse mult_assoc)
   finally show ?thesis .
 qed
 
 lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
 proof -
   assume [simp]: "c\<noteq>0"
-  have "(b/c = a) = ((b/c)*c = a*c)"
-    by (simp add: field_mult_cancel_right)
-  also have "... = (b = a*c)"
-    by (simp add: divide_inverse mult_assoc) 
+  have "(b/c = a) = ((b/c)*c = a*c)"  by simp
+  also have "... = (b = a*c)"  by (simp add: divide_inverse mult_assoc) 
   finally show ?thesis .
 qed
 
@@ -1609,13 +1605,13 @@
 lemma divide_cancel_right [simp]:
      "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
 apply (cases "c=0", simp)
-apply (simp add: divide_inverse field_mult_cancel_right)
+apply (simp add: divide_inverse)
 done
 
 lemma divide_cancel_left [simp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
 apply (cases "c=0", simp)
-apply (simp add: divide_inverse field_mult_cancel_left)
+apply (simp add: divide_inverse)
 done