src/HOL/Divides.thy
author paulson
Fri May 30 15:15:57 1997 +0200 (1997-05-30)
changeset 3366 2402c6ab1561
child 6865 5577ffe4c2f1
permissions -rw-r--r--
Moving div and mod from Arith to Divides
Moving dvd from ex/Primes to Divides
paulson@3366
     1
(*  Title:      HOL/Divides.thy
paulson@3366
     2
    ID:         $Id$
paulson@3366
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3366
     4
    Copyright   1993  University of Cambridge
paulson@3366
     5
paulson@3366
     6
The division operators div, mod and the divides relation "dvd"
paulson@3366
     7
*)
paulson@3366
     8
paulson@3366
     9
Divides = Arith +
paulson@3366
    10
paulson@3366
    11
consts
paulson@3366
    12
  div, mod  :: [nat, nat] => nat          (infixl 70)
paulson@3366
    13
  dvd     :: [nat,nat]=>bool              (infixl 70) 
paulson@3366
    14
paulson@3366
    15
paulson@3366
    16
defs
paulson@3366
    17
  mod_def   "m mod n == wfrec (trancl pred_nat)
paulson@3366
    18
                          (%f j. if j<n then j else f (j-n)) m"
paulson@3366
    19
  div_def   "m div n == wfrec (trancl pred_nat) 
paulson@3366
    20
                          (%f j. if j<n then 0 else Suc (f (j-n))) m"
paulson@3366
    21
paulson@3366
    22
  dvd_def   "m dvd n == EX k. n = m*k"
paulson@3366
    23
paulson@3366
    24
end