src/HOL/Divides.thy
changeset 22993 838c66e760b5
parent 22916 8caf6da610e2
child 23017 00c0e4c42396
     1.1 --- a/src/HOL/Divides.thy	Thu May 17 19:29:39 2007 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu May 17 19:49:16 2007 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  theory Divides
     1.6  imports Datatype Power
     1.7 +uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     1.8  begin
     1.9  
    1.10  (*We use the same class for div and mod;
    1.11 @@ -31,11 +32,11 @@
    1.12  notation
    1.13    mod (infixl "mod" 70)
    1.14  
    1.15 -instance nat :: "Divides.div"
    1.16 +instance nat :: Divides.div
    1.17 +  div_def: "m div n == wfrec (pred_nat^+)
    1.18 +                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    1.19    mod_def: "m mod n == wfrec (pred_nat^+)
    1.20 -                          (%f j. if j<n | n=0 then j else f (j-n)) m"
    1.21 -  div_def: "m div n == wfrec (pred_nat^+)
    1.22 -                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.23 +                          (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    1.24  
    1.25  definition
    1.26    (*The definition of dvd is polymorphic!*)