author | wenzelm |
Sat, 27 Oct 2001 00:00:05 +0200 | |
changeset 11954 | 3d1780208bf3 |
parent 10789 | 260fa2c67e3e |
child 12338 | de0f4a63baa5 |
permissions | -rw-r--r-- |
3366 | 1 |
(* Title: HOL/Divides.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
3366 | 5 |
|
6 |
The division operators div, mod and the divides relation "dvd" |
|
7 |
*) |
|
8 |
||
10214 | 9 |
Divides = NatArith + |
3366 | 10 |
|
8902 | 11 |
(*We use the same class for div and mod; |
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
12 |
moreover, dvd is defined whenever multiplication is*) |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
13 |
axclass |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
14 |
div < term |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
15 |
|
8961 | 16 |
instance nat :: div |
17 |
instance nat :: plus_ac0 (add_commute,add_assoc,add_0) |
|
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
18 |
|
3366 | 19 |
consts |
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
20 |
div :: ['a::div, 'a] => 'a (infixl 70) |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
21 |
mod :: ['a::div, 'a] => 'a (infixl 70) |
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10559
diff
changeset
|
22 |
dvd :: ['a::times, 'a] => bool (infixl 50) |
3366 | 23 |
|
24 |
||
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
25 |
(*Remainder and quotient are defined here by algorithms and later proved to |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
26 |
satisfy the traditional definition (theorem mod_div_equality) |
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
27 |
*) |
3366 | 28 |
defs |
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
29 |
|
3366 | 30 |
mod_def "m mod n == wfrec (trancl pred_nat) |
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
6865
diff
changeset
|
31 |
(%f j. if j<n | n=0 then j else f (j-n)) m" |
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
32 |
|
3366 | 33 |
div_def "m div n == wfrec (trancl pred_nat) |
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
6865
diff
changeset
|
34 |
(%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" |
3366 | 35 |
|
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset
|
36 |
(*The definition of dvd is polymorphic!*) |
3366 | 37 |
dvd_def "m dvd n == EX k. n = m*k" |
38 |
||
10559
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
39 |
(*This definition helps prove the harder properties of div and mod. |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
40 |
It is copied from IntDiv.thy; should it be overloaded?*) |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
41 |
constdefs |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
42 |
quorem :: "(nat*nat) * (nat*nat) => bool" |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
43 |
"quorem == %((a,b), (q,r)). |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
44 |
a = b*q + r & |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
45 |
(if 0<b then 0<=r & r<b else b<r & r <=0)" |
d3fd54fc659b
many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents:
10214
diff
changeset
|
46 |
|
3366 | 47 |
end |