src/HOL/Divides.thy
changeset 24993 92dfacb32053
parent 24748 ee0a0eb6b738
child 25062 af5ef0d4d655
     1.1 --- a/src/HOL/Divides.thy	Fri Oct 12 08:20:45 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 12 08:20:46 2007 +0200
     1.3 @@ -11,9 +11,7 @@
     1.4  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.5  begin
     1.6  
     1.7 -(*We use the same class for div and mod;
     1.8 -  moreover, dvd is defined whenever multiplication is*)
     1.9 -class div = type +
    1.10 +class div = times +
    1.11    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
    1.12    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
    1.13  
    1.14 @@ -23,12 +21,12 @@
    1.15    mod_def: "m mod n == wfrec (pred_nat^+)
    1.16                            (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    1.17  
    1.18 -definition (in times)
    1.19 +definition (in div)
    1.20    dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
    1.21  where
    1.22    [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
    1.23  
    1.24 -class dvd_mod = times + div + zero + -- {* for code generation *}
    1.25 +class dvd_mod = div + zero + -- {* for code generation *}
    1.26    assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    1.27  
    1.28  definition
    1.29 @@ -903,7 +901,7 @@
    1.30    unfolding divmod_def by simp
    1.31  
    1.32  instance nat :: dvd_mod
    1.33 -  by default (simp add: times_class.dvd [symmetric] dvd_eq_mod_eq_0)
    1.34 +  by default (simp add: dvd_eq_mod_eq_0)
    1.35  
    1.36  code_modulename SML
    1.37    Divides Nat