src/HOL/Divides.thy
author paulson
Mon Jul 19 15:18:16 1999 +0200 (1999-07-19)
changeset 7029 08d4eb8500dd
parent 6865 5577ffe4c2f1
child 8902 a705822f4e2a
permissions -rw-r--r--
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
     1 (*  Title:      HOL/Divides.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1999  University of Cambridge
     5 
     6 The division operators div, mod and the divides relation "dvd"
     7 *)
     8 
     9 Divides = Arith +
    10 
    11 (*We use the same sort for div and mod;
    12   moreover, dvd is defined whenever multiplication is*)
    13 axclass
    14   div < term
    15 
    16 instance
    17   nat :: {div}
    18 
    19 consts
    20   div  :: ['a::div, 'a]  => 'a          (infixl 70)
    21   mod  :: ['a::div, 'a]  => 'a          (infixl 70)
    22   dvd  :: ['a::times, 'a] => bool       (infixl 70) 
    23 
    24 
    25 (*Remainder and quotient are defined here by algorithms and later proved to
    26   satisfy the traditional definition (theorem mod_div_equality)
    27 *)
    28 defs
    29 
    30   mod_def   "m mod n == wfrec (trancl pred_nat)
    31                           (%f j. if j<n | n=0 then j else f (j-n)) m"
    32 
    33   div_def   "m div n == wfrec (trancl pred_nat) 
    34                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    35 
    36 (*The definition of dvd is polymorphic!*)
    37   dvd_def   "m dvd n == EX k. n = m*k"
    38 
    39 end