remove redundant simp attributes for zdvd rules
authorhuffman
Tue Feb 17 07:13:29 2009 -0800 (2009-02-17)
changeset 2995032db77615915
parent 29949 20a506b8256d
child 29951 a70bc5190534
remove redundant simp attributes for zdvd rules
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/IntDiv.thy	Tue Feb 17 06:59:33 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Feb 17 07:13:29 2009 -0800
     1.3 @@ -1177,23 +1177,23 @@
     1.4  lemma zdvd_1_left: "1 dvd (m::int)"
     1.5    by (rule one_dvd) (* already declared [simp] *)
     1.6  
     1.7 -lemma zdvd_refl [simp]: "m dvd (m::int)"
     1.8 -  by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
     1.9 +lemma zdvd_refl: "m dvd (m::int)"
    1.10 +  by (rule dvd_refl) (* already declared [simp] *)
    1.11  
    1.12  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    1.13    by (rule dvd_trans)
    1.14  
    1.15 -lemma zdvd_zminus_iff[simp]: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
    1.16 -  by (rule dvd_minus_iff)
    1.17 +lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
    1.18 +  by (rule dvd_minus_iff) (* already declared [simp] *)
    1.19  
    1.20 -lemma zdvd_zminus2_iff[simp]: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.21 -  by (rule minus_dvd_iff)
    1.22 +lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.23 +  by (rule minus_dvd_iff) (* already declared [simp] *)
    1.24  
    1.25 -lemma zdvd_abs1[simp]: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
    1.26 -  by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
    1.27 +lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)"
    1.28 +  by (rule abs_dvd_iff) (* already declared [simp] *)
    1.29  
    1.30 -lemma zdvd_abs2[simp]: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    1.31 -  by (cases "j > 0") (simp_all add: zdvd_zminus_iff)
    1.32 +lemma zdvd_abs2: "( (i::int) dvd \<bar>j\<bar>) = (i dvd j)" 
    1.33 +  by (rule dvd_abs_iff) (* already declared [simp] *)
    1.34  
    1.35  lemma zdvd_anti_sym:
    1.36      "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"