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
```