--- 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 ==>
--- 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
--- 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
--- 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)
--- 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}"
--- 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
--- 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