6917
|
1 |
(* Title: HOL/IntDiv.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 |
IntDiv = Bin + Recdef +
|
|
10 |
|
|
11 |
constdefs
|
|
12 |
quorem :: "(int*int) * (int*int) => bool"
|
|
13 |
"quorem == %((a,b), (q,r)).
|
|
14 |
a = b*q + r &
|
|
15 |
(if #0<b then #0<=r & r<b else b<r & r <= #0)"
|
|
16 |
|
|
17 |
adjust :: "[int, int, int*int] => int*int"
|
|
18 |
"adjust a b == %(q,r). if #0 <= r-b then (#2*q + #1, r-b)
|
|
19 |
else (#2*q, r)"
|
|
20 |
|
|
21 |
(** the division algorithm **)
|
|
22 |
|
|
23 |
(*for the case a>=0, b>0*)
|
|
24 |
consts posDivAlg :: "int*int => int*int"
|
|
25 |
recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + #1))"
|
|
26 |
"posDivAlg (a,b) =
|
|
27 |
(if (a<b | b<=#0) then (#0,a)
|
|
28 |
else adjust a b (posDivAlg(a, #2*b)))"
|
|
29 |
|
|
30 |
(*for the case a<0, b>0*)
|
|
31 |
consts negDivAlg :: "int*int => int*int"
|
|
32 |
recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
|
|
33 |
"negDivAlg (a,b) =
|
|
34 |
(if (#0<=a+b | b<=#0) then (#-1,a+b)
|
|
35 |
else adjust a b (negDivAlg(a, #2*b)))"
|
|
36 |
|
|
37 |
(*for the general case b~=0*)
|
|
38 |
|
|
39 |
constdefs
|
|
40 |
negateSnd :: "int*int => int*int"
|
|
41 |
"negateSnd == %(q,r). (q,-r)"
|
|
42 |
|
|
43 |
(*The full division algorithm considers all possible signs for a, b
|
|
44 |
including the special case a=0, b<0, because negDivAlg requires a<0*)
|
|
45 |
divAlg :: "int*int => int*int"
|
|
46 |
"divAlg ==
|
|
47 |
%(a,b). if #0<=a then
|
6993
|
48 |
if #0<=b then posDivAlg (a,b)
|
6917
|
49 |
else if a=#0 then (#0,#0)
|
|
50 |
else negateSnd (negDivAlg (-a,-b))
|
|
51 |
else
|
|
52 |
if #0<b then negDivAlg (a,b)
|
|
53 |
else negateSnd (posDivAlg (-a,-b))"
|
|
54 |
|
|
55 |
instance
|
|
56 |
int :: {div}
|
|
57 |
|
|
58 |
defs
|
|
59 |
div_def "a div b == fst (divAlg (a,b))"
|
|
60 |
mod_def "a mod b == snd (divAlg (a,b))"
|
|
61 |
|
|
62 |
|
|
63 |
end
|