remove type-specific proofs
authorhuffman
Thu Jan 08 12:25:22 2009 -0800 (2009-01-08)
changeset 2941097916a925a69
parent 29409 f0a8fe83bc07
child 29411 85bc8b63747c
remove type-specific proofs
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/IntDiv.thy	Thu Jan 08 10:43:09 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Jan 08 12:25:22 2009 -0800
     1.3 @@ -1137,50 +1137,31 @@
     1.4  subsection {* The Divides Relation *}
     1.5  
     1.6  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
     1.7 -  by (simp add: dvd_def zmod_eq_0_iff)
     1.8 +  by (rule dvd_eq_mod_eq_0)
     1.9  
    1.10  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.11    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    1.12  
    1.13 -lemma zdvd_0_right [iff]: "(m::int) dvd 0"
    1.14 -  by (simp add: dvd_def)
    1.15 +lemma zdvd_0_right: "(m::int) dvd 0"
    1.16 +  by (rule dvd_0_right) (* already declared [iff] *)
    1.17  
    1.18 -lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
    1.19 -  by (simp add: dvd_def)
    1.20 +lemma zdvd_0_left: "(0 dvd (m::int)) = (m = 0)"
    1.21 +  by (rule dvd_0_left_iff) (* already declared [noatp,simp] *)
    1.22  
    1.23 -lemma zdvd_1_left [iff]: "1 dvd (m::int)"
    1.24 -  by (simp add: dvd_def)
    1.25 +lemma zdvd_1_left: "1 dvd (m::int)"
    1.26 +  by (rule one_dvd) (* already declared [simp] *)
    1.27  
    1.28  lemma zdvd_refl [simp]: "m dvd (m::int)"
    1.29 -  by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
    1.30 +  by (rule dvd_refl) (* TODO: declare generic dvd_refl [simp] *)
    1.31  
    1.32  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    1.33 -  by (auto simp add: dvd_def intro: mult_assoc)
    1.34 +  by (rule dvd_trans)
    1.35  
    1.36  lemma zdvd_zminus_iff: "m dvd -n \<longleftrightarrow> m dvd (n::int)"
    1.37 -proof
    1.38 -  assume "m dvd - n"
    1.39 -  then obtain k where "- n = m * k" ..
    1.40 -  then have "n = m * - k" by simp
    1.41 -  then show "m dvd n" ..
    1.42 -next
    1.43 -  assume "m dvd n"
    1.44 -  then have "m dvd n * -1" by (rule dvd_mult2)
    1.45 -  then show "m dvd - n" by simp
    1.46 -qed
    1.47 +  by (rule dvd_minus_iff)
    1.48  
    1.49  lemma zdvd_zminus2_iff: "-m dvd n \<longleftrightarrow> m dvd (n::int)"
    1.50 -proof
    1.51 -  assume "- m dvd n"
    1.52 -  then obtain k where "n = - m * k" ..
    1.53 -  then have "n = m * - k" by simp
    1.54 -  then show "m dvd n" ..
    1.55 -next
    1.56 -  assume "m dvd n"
    1.57 -  then obtain k where "n = m * k" ..
    1.58 -  then have "n = - m * - k" by simp
    1.59 -  then show "- m dvd n" ..
    1.60 -qed
    1.61 +  by (rule minus_dvd_iff)
    1.62  
    1.63  lemma zdvd_abs1: "( \<bar>i::int\<bar> dvd j) = (i dvd j)" 
    1.64    by (cases "i > 0") (simp_all add: zdvd_zminus2_iff)
    1.65 @@ -1195,9 +1176,7 @@
    1.66    done
    1.67  
    1.68  lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"
    1.69 -  apply (simp add: dvd_def)
    1.70 -  apply (blast intro: right_distrib [symmetric])
    1.71 -  done
    1.72 +  by (rule dvd_add)
    1.73  
    1.74  lemma zdvd_dvd_eq: assumes anz:"a \<noteq> 0" and ab: "(a::int) dvd b" and ba:"b dvd a" 
    1.75    shows "\<bar>a\<bar> = \<bar>b\<bar>"
    1.76 @@ -1212,9 +1191,7 @@
    1.77  qed
    1.78  
    1.79  lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"
    1.80 -  apply (simp add: dvd_def)
    1.81 -  apply (blast intro: right_diff_distrib [symmetric])
    1.82 -  done
    1.83 +  by (rule Ring_and_Field.dvd_diff)
    1.84  
    1.85  lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
    1.86    apply (subgoal_tac "m = n + (m - n)")
    1.87 @@ -1223,34 +1200,22 @@
    1.88    done
    1.89  
    1.90  lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"
    1.91 -  apply (simp add: dvd_def)
    1.92 -  apply (blast intro: mult_left_commute)
    1.93 -  done
    1.94 +  by (rule dvd_mult)
    1.95  
    1.96  lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"
    1.97 -  apply (subst mult_commute)
    1.98 -  apply (erule zdvd_zmult)
    1.99 -  done
   1.100 +  by (rule dvd_mult2)
   1.101  
   1.102 -lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"
   1.103 -  apply (rule zdvd_zmult)
   1.104 -  apply (rule zdvd_refl)
   1.105 -  done
   1.106 +lemma zdvd_triv_right: "(k::int) dvd m * k"
   1.107 +  by (rule dvd_triv_right) (* already declared [simp] *)
   1.108  
   1.109 -lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"
   1.110 -  apply (rule zdvd_zmult2)
   1.111 -  apply (rule zdvd_refl)
   1.112 -  done
   1.113 +lemma zdvd_triv_left: "(k::int) dvd k * m"
   1.114 +  by (rule dvd_triv_left) (* already declared [simp] *)
   1.115  
   1.116  lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"
   1.117 -  apply (simp add: dvd_def)
   1.118 -  apply (simp add: mult_assoc, blast)
   1.119 -  done
   1.120 +  by (rule dvd_mult_left)
   1.121  
   1.122  lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"
   1.123 -  apply (rule zdvd_zmultD2)
   1.124 -  apply (subst mult_commute, assumption)
   1.125 -  done
   1.126 +  by (rule dvd_mult_right)
   1.127  
   1.128  lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"
   1.129    by (rule mult_dvd_mono)
   1.130 @@ -1301,7 +1266,7 @@
   1.131    {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
   1.132      with h have False by (simp add: mult_assoc)}
   1.133    hence "n = m * h" by blast
   1.134 -  thus ?thesis by blast
   1.135 +  thus ?thesis by simp
   1.136  qed
   1.137  
   1.138  lemma zdvd_zmult_cancel_disj[simp]:
   1.139 @@ -1339,8 +1304,8 @@
   1.140        then show ?thesis by (simp only: negative_eq_positive) auto
   1.141      qed
   1.142    qed
   1.143 -  then show ?thesis by (auto elim!: dvdE simp only: zmult_int [symmetric])
   1.144 -qed 
   1.145 +  then show ?thesis by (auto elim!: dvdE simp only: zdvd_triv_left int_mult)
   1.146 +qed
   1.147  
   1.148  lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
   1.149  proof
   1.150 @@ -1372,10 +1337,10 @@
   1.151    by (auto simp add: dvd_int_iff)
   1.152  
   1.153  lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
   1.154 -  by (simp add: zdvd_zminus2_iff)
   1.155 +  by (rule minus_dvd_iff)
   1.156  
   1.157  lemma dvd_zminus_iff [iff]: "(z dvd -w) = (z dvd (w::int))"
   1.158 -  by (simp add: zdvd_zminus_iff)
   1.159 +  by (rule dvd_minus_iff)
   1.160  
   1.161  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
   1.162    apply (rule_tac z=n in int_cases)