# HG changeset patch
# User nipkow
# Date 1182098823 -7200
# Node ID 5caa2710dd5bf8b8ac9eb395eb35320177f011c6
# Parent  aed08cd6adae8e334dc5fb8dff10ffc9b57a1409
tuned laws for cancellation in divisions for fields.

diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Complex/ex/Sqrt.thy
--- a/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -44,8 +44,7 @@
   have "\<bar>x\<bar> = real ?k / real ?l"
   proof -
     from gcd have "real ?k / real ?l =
-        real (?gcd * ?k) / real (?gcd * ?l)"
-      by (simp add: mult_divide_cancel_left)
+        real (?gcd * ?k) / real (?gcd * ?l)" by simp
     also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
     also from x_rat have "\<dots> = \<bar>x\<bar>" ..
     finally show ?thesis ..
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -1469,13 +1469,7 @@
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
     (setprod f (A - {a}) :: 'a :: {field}) =
       (if a:A then setprod f A / f a else setprod f A)"
-  apply (erule finite_induct)
-   apply (auto simp add: insert_Diff_if)
-  apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
-  apply (erule ssubst)
-  apply (subst times_divide_eq_right [THEN sym])
-  apply (auto simp add: mult_ac times_divide_eq_right)
-  done
+by (erule finite_induct) (auto simp add: insert_Diff_if)
 
 lemma setprod_inversef: "finite A ==>
     ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -236,8 +236,7 @@
   show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
-    show "\<forall>z. f z - f x = ?g z * (z-x)"
-      by (simp add: nonzero_mult_divide_cancel_right')
+    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
     show "isCont ?g x" using der
       by (simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
@@ -248,8 +247,7 @@
   then obtain g where
     "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
   thus "(DERIV f x :> l)"
-     by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right'
-              cong: LIM_cong)
+     by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
 qed
 
 lemma DERIV_chain':
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Hyperreal/HDeriv.thy
--- a/src/HOL/Hyperreal/HDeriv.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -358,13 +358,13 @@
             del: inverse_mult_distrib inverse_minus_eq
                  minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
-apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
+apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib
             del: minus_mult_left [symmetric] minus_mult_right [symmetric])
 apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
 apply (rule inverse_add_Infinitesimal_approx2)
 apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
             simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
-apply (rule Infinitesimal_HFinite_mult2, auto)
+apply (rule Infinitesimal_HFinite_mult, auto)
 done
 
 subsubsection {* Equivalence of NS and Standard definitions *}
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -178,8 +178,6 @@
         (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
 apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
 apply (simp add: right_diff_distrib diff_divide_distrib h)
-apply (simp only: times_divide_eq_left [symmetric])
-apply (simp add: divide_self [OF h])
 apply (simp add: mult_assoc [symmetric])
 apply (cases "n", simp)
 apply (simp add: lemma_realpow_diff_sumr2 h
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Library/BigO.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -698,11 +698,7 @@
   apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
   apply (erule ssubst)
   apply (erule set_times_intro2)
-  apply (simp add: func_times) 
-  apply (rule ext)
-  apply (subst times_divide_eq_left [symmetric])
-  apply (subst divide_self)
-  apply (assumption, simp)
+  apply (simp add: func_times)
   done
 
 lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -977,7 +977,11 @@
 
 subsection {* Calculations with fractions *}
 
-lemma nonzero_mult_divide_cancel_left:
+text{* There is a whole bunch of simp-rules just for class @{text
+field} but none for class @{text field} and @{text nonzero_divides}
+because the latter are covered by a simproc. *}
+
+lemma nonzero_mult_divide_mult_cancel_left[simp]:
   assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
     shows "(c*a)/(c*b) = a/(b::'a::field)"
 proof -
@@ -992,21 +996,22 @@
     by (simp add: divide_inverse)
 qed
 
-lemma mult_divide_cancel_left:
+lemma mult_divide_mult_cancel_left:
      "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b = 0")
-apply (simp_all add: nonzero_mult_divide_cancel_left)
+apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
 done
 
-lemma nonzero_mult_divide_cancel_right:
+lemma nonzero_mult_divide_mult_cancel_right:
      "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
-by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left) 
+by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
 
-lemma mult_divide_cancel_right:
+lemma mult_divide_mult_cancel_right:
      "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
 apply (cases "b = 0")
-apply (simp_all add: nonzero_mult_divide_cancel_right)
+apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
 done
+
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   by (simp add: divide_inverse)
 
@@ -1032,39 +1037,46 @@
   apply (erule ssubst)
   apply (rule add_divide_distrib [THEN sym])
   apply (subst mult_commute)
-  apply (erule nonzero_mult_divide_cancel_left [THEN sym])
+  apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
   apply assumption
-  apply (erule nonzero_mult_divide_cancel_right [THEN sym])
+  apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
   apply assumption
 done
 
 
-lemma nonzero_mult_divide_cancel_right':
-  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
-proof -
-  assume b: "b \<noteq> 0"
-  have "a * b / b = a * (b / b)" by (simp add: times_divide_eq_right)
-  also have "\<dots> = a" by (simp add: divide_self b)
-  finally show "a * b / b = a" .
-qed
-
-lemma nonzero_mult_divide_cancel_left':
-  "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
-proof -
-  assume b: "a \<noteq> 0"
-  have "a * b / a = b * a / a" by (simp add: mult_commute)
-  also have "\<dots> = b * (a / a)" by (simp add: times_divide_eq_right)
-  also have "\<dots> = b" by (simp add: divide_self b)
-  finally show "a * b / a = b" .
-qed
-
 subsubsection{*Special Cancellation Simprules for Division*}
 
-(* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
-lemma mult_divide_cancel_left_if[simp]:
+lemma mult_divide_mult_cancel_left_if[simp]:
   fixes c :: "'a :: {field,division_by_zero}"
   shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
-by (simp add: mult_divide_cancel_left)
+by (simp add: mult_divide_mult_cancel_left)
+
+lemma nonzero_mult_divide_cancel_right[simp]:
+  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
+using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
+
+lemma nonzero_mult_divide_cancel_left[simp]:
+  "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
+using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
+
+
+lemma nonzero_divide_mult_cancel_right[simp]:
+  "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
+using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
+
+lemma nonzero_divide_mult_cancel_left[simp]:
+  "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
+using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
+
+
+lemma nonzero_mult_divide_mult_cancel_left2[simp]:
+     "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
+using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
+
+lemma nonzero_mult_divide_mult_cancel_right2[simp]:
+     "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
+using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
+
 
 (* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
 lemma mult_divide_cancel_right_if:
@@ -1113,6 +1125,7 @@
 by (simp add: times_divide_eq_left)
 *)
 
+
 subsection {* Division and Unary Minus *}
 
 lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/SetInterval.thy	Sun Jun 17 18:47:03 2007 +0200
@@ -739,12 +739,11 @@
 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: times_divide_eq_right [symmetric])
-  apply (simp add: right_distrib diff_minus mult_commute power_Suc)
-  done
+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
 
 
 subsection {* The formula for arithmetic sums *}
diff -r aed08cd6adae -r 5caa2710dd5b src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Sun Jun 17 13:39:50 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML	Sun Jun 17 18:47:03 2007 +0200
@@ -62,7 +62,7 @@
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
-  val cancel = @{thm mult_divide_cancel_left} RS trans
+  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   val neg_exchanges = false
 )
 
@@ -257,7 +257,7 @@
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_left_if}
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
 );
 
 val cancel_factors =