1.1 --- a/src/HOL/Divides.thy	Tue Jul 10 00:43:51 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Jul 10 09:23:10 2007 +0200
     1.3 @@ -14,23 +14,8 @@
     1.4  (*We use the same class for div and mod;
     1.5    moreover, dvd is defined whenever multiplication is*)
     1.6  class div = type +
     1.7 -  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.8 -  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9 -begin
    1.10 -
    1.11 -notation
    1.12 -  div (infixl "\<^loc>div" 70)
    1.13 -
    1.14 -notation
    1.15 -  mod (infixl "\<^loc>mod" 70)
    1.16 -
    1.17 -end
    1.18 -
    1.19 -notation
    1.20 -  div (infixl "div" 70)
    1.21 -
    1.22 -notation
    1.23 -  mod (infixl "mod" 70)
    1.24 +  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
    1.25 +  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
    1.26  
    1.27  instance nat :: Divides.div
    1.28    div_def: "m div n == wfrec (pred_nat^+)
    1.29 @@ -38,10 +23,15 @@
    1.30    mod_def: "m mod n == wfrec (pred_nat^+)
    1.31                            (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    1.32  
    1.33 -definition
    1.34 -  (*The definition of dvd is polymorphic!*)
    1.35 -  dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
    1.36 -  dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"
    1.37 +definition (in times)
    1.38 +  dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
    1.39 +where
    1.40 +  "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
    1.41 +lemmas dvd_def = dvd_def [folded times_class.dvd]
    1.42 +
    1.43 +class dvd_mod = times + div + zero + -- {* for code generation *}
    1.44 +  assumes dvd_def_mod: "times.dvd (op \<^loc>*) x y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.45 +lemmas dvd_def_mod [code func] = dvd_def_mod [folded times_class.dvd]
    1.46  
    1.47  definition
    1.48    quorem :: "(nat*nat) * (nat*nat) => bool" where
    1.49 @@ -511,6 +501,11 @@
    1.50    unfolding dvd_def
    1.51    by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
    1.52  
    1.53 +text {* @{term "op dvd"} is a partial order *}
    1.54 +
    1.55 +interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> m \<noteq> n"]
    1.56 +  by unfold_locales (auto intro: dvd_trans dvd_anti_sym)
    1.57 +
    1.58  lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
    1.59    unfolding dvd_def
    1.60    by (blast intro: add_mult_distrib2 [symmetric])
    1.61 @@ -885,6 +880,8 @@
    1.62  qed
    1.63  
    1.64  
    1.65 +
    1.66 +
    1.67  subsection {* Code generation for div, mod and dvd on nat *}
    1.68  
    1.69  definition [code func del]:
    1.70 @@ -907,14 +904,8 @@
    1.71  lemma mod_divmod [code]: "m mod n = snd (divmod m n)"
    1.72    unfolding divmod_def by simp
    1.73  
    1.74 -definition
    1.75 -  dvd_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
    1.76 -where
    1.77 -  "dvd_nat m n \<longleftrightarrow> n mod m = (0 \<Colon> nat)"
    1.78 -
    1.79 -lemma [code inline]:
    1.80 -  "op dvd = dvd_nat"
    1.81 -  by (auto simp add: dvd_nat_def dvd_eq_mod_eq_0 expand_fun_eq)
    1.82 +instance nat :: dvd_mod
    1.83 +  by default (simp add: times_class.dvd [symmetric] dvd_eq_mod_eq_0)
    1.84  
    1.85  code_modulename SML
    1.86    Divides Nat
    1.87 @@ -925,153 +916,6 @@
    1.88  code_modulename Haskell
    1.89    Divides Nat
    1.90  
    1.91 -hide (open) const divmod dvd_nat
    1.92 +hide (open) const divmod
    1.93  
    1.94 -subsection {* Legacy bindings *}
    1.95 -
    1.96 -ML
    1.97 -{*
    1.98 -val div_def = thm "div_def"
    1.99 -val mod_def = thm "mod_def"
   1.100 -val dvd_def = thm "dvd_def"
   1.101 -val quorem_def = thm "quorem_def"
   1.102 -
   1.103 -val wf_less_trans = thm "wf_less_trans";
   1.104 -val mod_eq = thm "mod_eq";
   1.105 -val div_eq = thm "div_eq";
   1.106 -val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
   1.107 -val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
   1.108 -val mod_less = thm "mod_less";
   1.109 -val mod_geq = thm "mod_geq";
   1.110 -val le_mod_geq = thm "le_mod_geq";
   1.111 -val mod_if = thm "mod_if";
   1.112 -val mod_1 = thm "mod_1";
   1.113 -val mod_self = thm "mod_self";
   1.114 -val mod_add_self2 = thm "mod_add_self2";
   1.115 -val mod_add_self1 = thm "mod_add_self1";
   1.116 -val mod_mult_self1 = thm "mod_mult_self1";
   1.117 -val mod_mult_self2 = thm "mod_mult_self2";
   1.118 -val mod_mult_distrib = thm "mod_mult_distrib";
   1.119 -val mod_mult_distrib2 = thm "mod_mult_distrib2";
   1.120 -val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
   1.121 -val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
   1.122 -val div_less = thm "div_less";
   1.123 -val div_geq = thm "div_geq";
   1.124 -val le_div_geq = thm "le_div_geq";
   1.125 -val div_if = thm "div_if";
   1.126 -val mod_div_equality = thm "mod_div_equality";
   1.127 -val mod_div_equality2 = thm "mod_div_equality2";
   1.128 -val div_mod_equality = thm "div_mod_equality";
   1.129 -val div_mod_equality2 = thm "div_mod_equality2";
   1.130 -val mult_div_cancel = thm "mult_div_cancel";
   1.131 -val mod_less_divisor = thm "mod_less_divisor";
   1.132 -val div_mult_self_is_m = thm "div_mult_self_is_m";
   1.133 -val div_mult_self1_is_m = thm "div_mult_self1_is_m";
   1.134 -val unique_quotient_lemma = thm "unique_quotient_lemma";
   1.135 -val unique_quotient = thm "unique_quotient";
   1.136 -val unique_remainder = thm "unique_remainder";
   1.137 -val div_0 = thm "div_0";
   1.138 -val mod_0 = thm "mod_0";
   1.139 -val div_mult1_eq = thm "div_mult1_eq";
   1.140 -val mod_mult1_eq = thm "mod_mult1_eq";
   1.141 -val mod_mult1_eq' = thm "mod_mult1_eq'";
   1.142 -val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
   1.143 -val div_add1_eq = thm "div_add1_eq";
   1.144 -val mod_add1_eq = thm "mod_add1_eq";
   1.145 -val mod_add_left_eq = thm "mod_add_left_eq";
   1.146 - val mod_add_right_eq = thm "mod_add_right_eq";
   1.147 -val mod_lemma = thm "mod_lemma";
   1.148 -val div_mult2_eq = thm "div_mult2_eq";
   1.149 -val mod_mult2_eq = thm "mod_mult2_eq";
   1.150 -val div_mult_mult_lemma = thm "div_mult_mult_lemma";
   1.151 -val div_mult_mult1 = thm "div_mult_mult1";
   1.152 -val div_mult_mult2 = thm "div_mult_mult2";
   1.153 -val div_1 = thm "div_1";
   1.154 -val div_self = thm "div_self";
   1.155 -val div_add_self2 = thm "div_add_self2";
   1.156 -val div_add_self1 = thm "div_add_self1";
   1.157 -val div_mult_self1 = thm "div_mult_self1";
   1.158 -val div_mult_self2 = thm "div_mult_self2";
   1.159 -val div_le_mono = thm "div_le_mono";
   1.160 -val div_le_mono2 = thm "div_le_mono2";
   1.161 -val div_le_dividend = thm "div_le_dividend";
   1.162 -val div_less_dividend = thm "div_less_dividend";
   1.163 -val mod_Suc = thm "mod_Suc";
   1.164 -val dvdI = thm "dvdI";
   1.165 -val dvdE = thm "dvdE";
   1.166 -val dvd_0_right = thm "dvd_0_right";
   1.167 -val dvd_0_left = thm "dvd_0_left";
   1.168 -val dvd_0_left_iff = thm "dvd_0_left_iff";
   1.169 -val dvd_1_left = thm "dvd_1_left";
   1.170 -val dvd_1_iff_1 = thm "dvd_1_iff_1";
   1.171 -val dvd_refl = thm "dvd_refl";
   1.172 -val dvd_trans = thm "dvd_trans";
   1.173 -val dvd_anti_sym = thm "dvd_anti_sym";
   1.174 -val dvd_add = thm "dvd_add";
   1.175 -val dvd_diff = thm "dvd_diff";
   1.176 -val dvd_diffD = thm "dvd_diffD";
   1.177 -val dvd_diffD1 = thm "dvd_diffD1";
   1.178 -val dvd_mult = thm "dvd_mult";
   1.179 -val dvd_mult2 = thm "dvd_mult2";
   1.180 -val dvd_reduce = thm "dvd_reduce";
   1.181 -val dvd_mod = thm "dvd_mod";
   1.182 -val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
   1.183 -val dvd_mod_iff = thm "dvd_mod_iff";
   1.184 -val dvd_mult_cancel = thm "dvd_mult_cancel";
   1.185 -val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
   1.186 -val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
   1.187 -val mult_dvd_mono = thm "mult_dvd_mono";
   1.188 -val dvd_mult_left = thm "dvd_mult_left";
   1.189 -val dvd_mult_right = thm "dvd_mult_right";
   1.190 -val dvd_imp_le = thm "dvd_imp_le";
   1.191 -val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
   1.192 -val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
   1.193 -val mod_eq_0_iff = thm "mod_eq_0_iff";
   1.194 -val mod_eqD = thm "mod_eqD";
   1.195 -*}
   1.196 -
   1.197 -(*
   1.198 -lemma split_div:
   1.199 -assumes m: "m \<noteq> 0"
   1.200 -shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
   1.201 -       (is "?P = ?Q")
   1.202 -proof
   1.203 -  assume P: ?P
   1.204 -  show ?Q
   1.205 -  proof (intro allI impI)
   1.206 -    fix i j
   1.207 -    assume n: "n = m*i + j" and j: "j < m"
   1.208 -    show "P i"
   1.209 -    proof (cases)
   1.210 -      assume "i = 0"
   1.211 -      with n j P show "P i" by simp
   1.212 -    next
   1.213 -      assume "i \<noteq> 0"
   1.214 -      with n j P show "P i" by (simp add:add_ac div_mult_self1)
   1.215 -    qed
   1.216 -  qed
   1.217 -next
   1.218 -  assume Q: ?Q
   1.219 -  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   1.220 -  show ?P by simp
   1.221 -qed
   1.222 -
   1.223 -lemma split_mod:
   1.224 -assumes m: "m \<noteq> 0"
   1.225 -shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
   1.226 -       (is "?P = ?Q")
   1.227 -proof
   1.228 -  assume P: ?P
   1.229 -  show ?Q
   1.230 -  proof (intro allI impI)
   1.231 -    fix i j
   1.232 -    assume "n = m*i + j" "j < m"
   1.233 -    thus "P j" using m P by(simp add:add_ac mult_ac)
   1.234 -  qed
   1.235 -next
   1.236 -  assume Q: ?Q
   1.237 -  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   1.238 -  show ?P by simp
   1.239 -qed
   1.240 -*)
   1.241  end

     2.1 --- a/src/HOL/IntDiv.thy	Tue Jul 10 00:43:51 2007 +0200
     2.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 10 09:23:10 2007 +0200
     2.3 @@ -1064,13 +1064,8 @@
     2.4  lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"
     2.5    by (simp add: dvd_def zmod_eq_0_iff)
     2.6  
     2.7 -definition
     2.8 -  dvd_int :: "int \<Rightarrow> int \<Rightarrow> bool"
     2.9 -where
    2.10 -  "dvd_int = op dvd"
    2.11 -
    2.12 -lemmas [code inline] = dvd_int_def [symmetric]
    2.13 -lemmas [code, folded dvd_int_def, code func] = zdvd_iff_zmod_eq_0
    2.14 +instance int :: dvd_mod
    2.15 +  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
    2.16  
    2.17  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    2.18    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]