# HG changeset patch
# User nipkow
# Date 1182777558 -7200
# Node ID 84e9216a6d0efa24ab4a932d8b1d287fda6bcf91
# Parent  e4dd6beeafabc0f2f161a0bb612dba0d243feaa4
removed redundant lemmas

diff -r e4dd6beeafab -r 84e9216a6d0e 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
 
 
diff -r e4dd6beeafab -r 84e9216a6d0e src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jun 25 14:49:32 2007 +0200
+++ b/src/HOL/SetInterval.thy	Mon Jun 25 15:19:18 2007 +0200
@@ -739,12 +739,7 @@
 lemma geometric_sum:
   "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
   (x ^ n - 1) / (x - 1::'a::{field, recpower})"
-apply (induct "n", auto)
-apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
-apply (auto simp add: mult_assoc left_distrib)
-apply (simp add: right_distrib diff_minus mult_commute power_Suc)
-done
-
+by (induct "n") (simp_all add:field_simps power_Suc)
 
 subsection {* The formula for arithmetic sums *}