src/HOL/Divides.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Divides.thy	Fri May 30 15:15:57 1997 +0200
@@ -0,0 +1,24 @@
+(*  Title:      HOL/Divides.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+The division operators div, mod and the divides relation "dvd"
+*)
+
+Divides = Arith +
+
+consts
+  div, mod  :: [nat, nat] => nat          (infixl 70)
+  dvd     :: [nat,nat]=>bool              (infixl 70) 
+
+
+defs
+  mod_def   "m mod n == wfrec (trancl pred_nat)
+                          (%f j. if j<n then j else f (j-n)) m"
+  div_def   "m div n == wfrec (trancl pred_nat) 
+                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
+
+  dvd_def   "m dvd n == EX k. n = m*k"
+
+end