src/HOL/Divides.thy
changeset 6865 5577ffe4c2f1
parent 3366 2402c6ab1561
child 7029 08d4eb8500dd
     1.1 --- a/src/HOL/Divides.thy	Thu Jul 01 10:32:57 1999 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Jul 01 10:33:50 1999 +0200
     1.3 @@ -1,24 +1,39 @@
     1.4  (*  Title:      HOL/Divides.thy
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 +    Copyright   1999  University of Cambridge
     1.9  
    1.10  The division operators div, mod and the divides relation "dvd"
    1.11  *)
    1.12  
    1.13  Divides = Arith +
    1.14  
    1.15 +(*We use the same sort for div and mod;
    1.16 +  moreover, dvd is defined whenever multiplication is*)
    1.17 +axclass
    1.18 +  div < term
    1.19 +
    1.20 +instance
    1.21 +  nat :: {div}
    1.22 +
    1.23  consts
    1.24 -  div, mod  :: [nat, nat] => nat          (infixl 70)
    1.25 -  dvd     :: [nat,nat]=>bool              (infixl 70) 
    1.26 +  div  :: ['a::div, 'a]  => 'a          (infixl 70)
    1.27 +  mod  :: ['a::div, 'a]  => 'a          (infixl 70)
    1.28 +  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
    1.29  
    1.30  
    1.31 +(*Remainder and quotient are defined here by algorithms and later proved to
    1.32 +  satisfy the traditional definition (theorem mod_div_equality)
    1.33 +*)
    1.34  defs
    1.35 +
    1.36    mod_def   "m mod n == wfrec (trancl pred_nat)
    1.37                            (%f j. if j<n then j else f (j-n)) m"
    1.38 +
    1.39    div_def   "m div n == wfrec (trancl pred_nat) 
    1.40                            (%f j. if j<n then 0 else Suc (f (j-n))) m"
    1.41  
    1.42 +(*The definition of dvd is polymorphic!*)
    1.43    dvd_def   "m dvd n == EX k. n = m*k"
    1.44  
    1.45  end