author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10214  77349ed89f45 
child 10559  d3fd54fc659b 
permissions  rwrr 
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) 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
3366
diff
changeset

22 
dvd :: ['a::times, 'a] => bool (infixl 70) 
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 (jn)) 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 (jn))) 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 

39 
end 