--- a/src/HOL/Divides.thy Thu May 17 19:29:39 2007 +0200
+++ b/src/HOL/Divides.thy Thu May 17 19:49:16 2007 +0200
@@ -8,6 +8,7 @@
theory Divides
imports Datatype Power
+uses "~~/src/Provers/Arith/cancel_div_mod.ML"
begin
(*We use the same class for div and mod;
@@ -31,11 +32,11 @@
notation
mod (infixl "mod" 70)
-instance nat :: "Divides.div"
+instance nat :: Divides.div
+ div_def: "m div n == wfrec (pred_nat^+)
+ (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
mod_def: "m mod n == wfrec (pred_nat^+)
- (%f j. if j<n | n=0 then j else f (j-n)) m"
- div_def: "m div n == wfrec (pred_nat^+)
- (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
+ (%f j. if j<n | n=0 then j else f (j-n)) m" ..
definition
(*The definition of dvd is polymorphic!*)