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