# HG changeset patch
# User nipkow
# Date 1181913032 -7200
# Node ID 0b5a400c7595e1678ef43f37d5dc61044ae34894
# Parent  2cc3352f6c3c89442eeaa83d5427b898a653e047
made divide_self a simp rule

diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -1463,7 +1463,7 @@
   apply (subst setprod_Un_Int [symmetric], auto)
   apply (subgoal_tac "finite (A Int B)")
   apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
-  apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
+  apply (subst times_divide_eq_right [THEN sym], auto)
   done
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
@@ -1474,7 +1474,7 @@
   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 divide_self)
+  apply (auto simp add: mult_ac times_divide_eq_right)
   done
 
 lemma setprod_inversef: "finite A ==>
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -48,7 +48,7 @@
 by (simp add: deriv_def)
 
 lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
-by (simp add: deriv_def divide_self cong: LIM_cong)
+by (simp add: deriv_def cong: LIM_cong)
 
 lemma add_diff_add:
   fixes a b c d :: "'a::ab_group_add"
@@ -81,7 +81,7 @@
   hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
     by simp
   hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
-    by (simp cong: LIM_cong add: divide_self)
+    by (simp cong: LIM_cong)
   thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
     by (simp add: LIM_def)
 qed
@@ -232,7 +232,7 @@
 proof -
   assume b: "b \<noteq> 0"
   have "a * b / b = a * (b / b)" by simp
-  also have "\<dots> = a" by (simp add: divide_self b)
+  also have "\<dots> = a" by (simp add: b)
   finally show "a * b / b = a" .
 qed
 
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Hyperreal/FrechetDeriv.thy
--- a/src/HOL/Hyperreal/FrechetDeriv.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -480,7 +480,7 @@
  apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
  apply (subst diff_divide_distrib)
  apply (subst times_divide_eq_left [symmetric])
- apply (simp cong: LIM_cong add: divide_self)
+ apply (simp cong: LIM_cong)
  apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
 done
 
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Hyperreal/HDeriv.thy
--- a/src/HOL/Hyperreal/HDeriv.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -338,7 +338,7 @@
 
 text{*Differentiation of natural number powers*}
 lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
-by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if)
+by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
 
 lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
 by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -770,7 +770,7 @@
 lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
 by (simp add: divide_inverse)
 
-lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
+lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
   by (simp add: divide_inverse)
 
 lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
@@ -1008,12 +1008,6 @@
 apply (simp_all add: nonzero_mult_divide_cancel_right)
 done
 
-(*For ExtractCommonTerm*)
-lemma mult_divide_cancel_eq_if:
-     "(c*a) / (c*b) = 
-      (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
-  by (simp add: mult_divide_cancel_left)
-
 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
   by (simp add: divide_inverse)
 
@@ -1052,6 +1046,7 @@
   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)
+(* also used at ML level *)
 
 lemma mult_divide_cancel_right_if [simp]:
   fixes c :: "'a :: {field,division_by_zero}"
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/SetInterval.thy	Fri Jun 15 15:10:32 2007 +0200
@@ -742,7 +742,7 @@
   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] divide_self)
+  apply (simp add: times_divide_eq_right [symmetric])
   apply (simp add: right_distrib diff_minus mult_commute power_Suc)
   done
 
diff -r 2cc3352f6c3c -r 0b5a400c7595 src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Fri Jun 15 09:10:06 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML	Fri Jun 15 15:10:32 2007 +0200
@@ -272,7 +272,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_eq_if}
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_left_if}
 );
 
 (*The number_ring class is necessary because the simprocs refer to the