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