code generation for dvd
authorhaftmann
Thu Jun 28 19:09:34 2007 +0200 (2007-06-28)
changeset 23512770e7f9f715b
parent 23511 7067f5e3670f
child 23513 2ebb50c0db4f
code generation for dvd
src/HOL/IntDiv.thy
     1.1 --- a/src/HOL/IntDiv.thy	Thu Jun 28 19:09:32 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Jun 28 19:09:34 2007 +0200
     1.3 @@ -1062,13 +1062,21 @@
     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 (simp add: dvd_def zmod_eq_0_iff)
     1.9 +
    1.10 +definition
    1.11 +  dvd_int :: "int \<Rightarrow> int \<Rightarrow> bool"
    1.12 +where
    1.13 +  "dvd_int = op dvd"
    1.14 +
    1.15 +lemmas [code inline] = dvd_int_def [symmetric]
    1.16 +lemmas [code, folded dvd_int_def, code func] = zdvd_iff_zmod_eq_0
    1.17  
    1.18  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    1.19    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
    1.20  
    1.21  lemma zdvd_0_right [iff]: "(m::int) dvd 0"
    1.22 -by (simp add: dvd_def)
    1.23 +  by (simp add: dvd_def)
    1.24  
    1.25  lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
    1.26    by (simp add: dvd_def)
    1.27 @@ -1077,10 +1085,10 @@
    1.28    by (simp add: dvd_def)
    1.29  
    1.30  lemma zdvd_refl [simp]: "m dvd (m::int)"
    1.31 -by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
    1.32 +  by (auto simp add: dvd_def intro: zmult_1_right [symmetric])
    1.33  
    1.34  lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"
    1.35 -by (auto simp add: dvd_def intro: mult_assoc)
    1.36 +  by (auto simp add: dvd_def intro: mult_assoc)
    1.37  
    1.38  lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"
    1.39    apply (simp add: dvd_def, auto)