made divide_self a simp rule
authornipkow
Fri Jun 15 15:10:32 2007 +0200 (2007-06-15)
changeset 233980b5a400c7595
parent 23397 2cc3352f6c3c
child 23399 1766da98eaa9
made divide_self a simp rule
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/FrechetDeriv.thy
src/HOL/Hyperreal/HDeriv.thy
src/HOL/Ring_and_Field.thy
src/HOL/SetInterval.thy
src/HOL/int_factor_simprocs.ML
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jun 15 09:10:06 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jun 15 15:10:32 2007 +0200
     1.3 @@ -1463,7 +1463,7 @@
     1.4    apply (subst setprod_Un_Int [symmetric], auto)
     1.5    apply (subgoal_tac "finite (A Int B)")
     1.6    apply (frule setprod_nonzero_field [of "A Int B" f], assumption)
     1.7 -  apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self)
     1.8 +  apply (subst times_divide_eq_right [THEN sym], auto)
     1.9    done
    1.10  
    1.11  lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
    1.12 @@ -1474,7 +1474,7 @@
    1.13    apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
    1.14    apply (erule ssubst)
    1.15    apply (subst times_divide_eq_right [THEN sym])
    1.16 -  apply (auto simp add: mult_ac times_divide_eq_right divide_self)
    1.17 +  apply (auto simp add: mult_ac times_divide_eq_right)
    1.18    done
    1.19  
    1.20  lemma setprod_inversef: "finite A ==>
     2.1 --- a/src/HOL/Hyperreal/Deriv.thy	Fri Jun 15 09:10:06 2007 +0200
     2.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Fri Jun 15 15:10:32 2007 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4  by (simp add: deriv_def)
     2.5  
     2.6  lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
     2.7 -by (simp add: deriv_def divide_self cong: LIM_cong)
     2.8 +by (simp add: deriv_def cong: LIM_cong)
     2.9  
    2.10  lemma add_diff_add:
    2.11    fixes a b c d :: "'a::ab_group_add"
    2.12 @@ -81,7 +81,7 @@
    2.13    hence "(\<lambda>h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0"
    2.14      by simp
    2.15    hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
    2.16 -    by (simp cong: LIM_cong add: divide_self)
    2.17 +    by (simp cong: LIM_cong)
    2.18    thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
    2.19      by (simp add: LIM_def)
    2.20  qed
    2.21 @@ -232,7 +232,7 @@
    2.22  proof -
    2.23    assume b: "b \<noteq> 0"
    2.24    have "a * b / b = a * (b / b)" by simp
    2.25 -  also have "\<dots> = a" by (simp add: divide_self b)
    2.26 +  also have "\<dots> = a" by (simp add: b)
    2.27    finally show "a * b / b = a" .
    2.28  qed
    2.29  
     3.1 --- a/src/HOL/Hyperreal/FrechetDeriv.thy	Fri Jun 15 09:10:06 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Fri Jun 15 15:10:32 2007 +0200
     3.3 @@ -480,7 +480,7 @@
     3.4   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
     3.5   apply (subst diff_divide_distrib)
     3.6   apply (subst times_divide_eq_left [symmetric])
     3.7 - apply (simp cong: LIM_cong add: divide_self)
     3.8 + apply (simp cong: LIM_cong)
     3.9   apply (simp add: LIM_norm_zero_iff LIM_zero_iff)
    3.10  done
    3.11  
     4.1 --- a/src/HOL/Hyperreal/HDeriv.thy	Fri Jun 15 09:10:06 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/HDeriv.thy	Fri Jun 15 15:10:32 2007 +0200
     4.3 @@ -338,7 +338,7 @@
     4.4  
     4.5  text{*Differentiation of natural number powers*}
     4.6  lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
     4.7 -by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if)
     4.8 +by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
     4.9  
    4.10  lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c"
    4.11  by (cut_tac c = c and x = x in NSDERIV_Id [THEN NSDERIV_cmult], simp)
     5.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jun 15 09:10:06 2007 +0200
     5.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Jun 15 15:10:32 2007 +0200
     5.3 @@ -770,7 +770,7 @@
     5.4  lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
     5.5  by (simp add: divide_inverse)
     5.6  
     5.7 -lemma divide_self: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
     5.8 +lemma divide_self[simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
     5.9    by (simp add: divide_inverse)
    5.10  
    5.11  lemma divide_zero [simp]: "a / 0 = (0::'a::{field,division_by_zero})"
    5.12 @@ -1008,12 +1008,6 @@
    5.13  apply (simp_all add: nonzero_mult_divide_cancel_right)
    5.14  done
    5.15  
    5.16 -(*For ExtractCommonTerm*)
    5.17 -lemma mult_divide_cancel_eq_if:
    5.18 -     "(c*a) / (c*b) = 
    5.19 -      (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
    5.20 -  by (simp add: mult_divide_cancel_left)
    5.21 -
    5.22  lemma divide_1 [simp]: "a/1 = (a::'a::field)"
    5.23    by (simp add: divide_inverse)
    5.24  
    5.25 @@ -1052,6 +1046,7 @@
    5.26    fixes c :: "'a :: {field,division_by_zero}"
    5.27    shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
    5.28  by (simp add: mult_divide_cancel_left)
    5.29 +(* also used at ML level *)
    5.30  
    5.31  lemma mult_divide_cancel_right_if [simp]:
    5.32    fixes c :: "'a :: {field,division_by_zero}"
     6.1 --- a/src/HOL/SetInterval.thy	Fri Jun 15 09:10:06 2007 +0200
     6.2 +++ b/src/HOL/SetInterval.thy	Fri Jun 15 15:10:32 2007 +0200
     6.3 @@ -742,7 +742,7 @@
     6.4    apply (induct "n", auto)
     6.5    apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
     6.6    apply (auto simp add: mult_assoc left_distrib)
     6.7 -  apply (simp add: times_divide_eq_right [symmetric] divide_self)
     6.8 +  apply (simp add: times_divide_eq_right [symmetric])
     6.9    apply (simp add: right_distrib diff_minus mult_commute power_Suc)
    6.10    done
    6.11  
     7.1 --- a/src/HOL/int_factor_simprocs.ML	Fri Jun 15 09:10:06 2007 +0200
     7.2 +++ b/src/HOL/int_factor_simprocs.ML	Fri Jun 15 15:10:32 2007 +0200
     7.3 @@ -272,7 +272,7 @@
     7.4    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
     7.5    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
     7.6    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
     7.7 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_eq_if}
     7.8 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_left_if}
     7.9  );
    7.10  
    7.11  (*The number_ring class is necessary because the simprocs refer to the