src/HOL/Divides.thy
author nipkow
Fri Jan 05 14:28:10 2001 +0100 (2001-01-05)
changeset 10789 260fa2c67e3e
parent 10559 d3fd54fc659b
child 12338 de0f4a63baa5
permissions -rw-r--r--
Changed priority of dvd from 70 to 50 as befits a relation.
     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 = NatArith +
    10 
    11 (*We use the same class for div and mod;
    12   moreover, dvd is defined whenever multiplication is*)
    13 axclass
    14   div < term
    15 
    16 instance  nat :: div
    17 instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
    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 50) 
    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 (*This definition helps prove the harder properties of div and mod.
    40   It is copied from IntDiv.thy; should it be overloaded?*)
    41 constdefs
    42   quorem :: "(nat*nat) * (nat*nat) => bool"
    43     "quorem == %((a,b), (q,r)).
    44                       a = b*q + r &
    45                       (if 0<b then 0<=r & r<b else b<r & r <=0)"
    46 
    47 end