10 |
10 |
11 constdefs |
11 constdefs |
12 quorem :: "(int*int) * (int*int) => bool" |
12 quorem :: "(int*int) * (int*int) => bool" |
13 "quorem == %((a,b), (q,r)). |
13 "quorem == %((a,b), (q,r)). |
14 a = b*q + r & |
14 a = b*q + r & |
15 (if #0<b then #0<=r & r<b else b<r & r <= #0)" |
15 (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)" |
16 |
16 |
17 adjust :: "[int, int, int*int] => int*int" |
17 adjust :: "[int, int, int*int] => int*int" |
18 "adjust a b == %(q,r). if #0 <= r-b then (#2*q + #1, r-b) |
18 "adjust a b == %(q,r). if Numeral0 <= r-b then (# 2*q + Numeral1, r-b) |
19 else (#2*q, r)" |
19 else (# 2*q, r)" |
20 |
20 |
21 (** the division algorithm **) |
21 (** the division algorithm **) |
22 |
22 |
23 (*for the case a>=0, b>0*) |
23 (*for the case a>=0, b>0*) |
24 consts posDivAlg :: "int*int => int*int" |
24 consts posDivAlg :: "int*int => int*int" |
25 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + #1))" |
25 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))" |
26 "posDivAlg (a,b) = |
26 "posDivAlg (a,b) = |
27 (if (a<b | b<=#0) then (#0,a) |
27 (if (a<b | b<=Numeral0) then (Numeral0,a) |
28 else adjust a b (posDivAlg(a, #2*b)))" |
28 else adjust a b (posDivAlg(a, # 2*b)))" |
29 |
29 |
30 (*for the case a<0, b>0*) |
30 (*for the case a<0, b>0*) |
31 consts negDivAlg :: "int*int => int*int" |
31 consts negDivAlg :: "int*int => int*int" |
32 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))" |
32 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))" |
33 "negDivAlg (a,b) = |
33 "negDivAlg (a,b) = |
34 (if (#0<=a+b | b<=#0) then (#-1,a+b) |
34 (if (Numeral0<=a+b | b<=Numeral0) then (# -1,a+b) |
35 else adjust a b (negDivAlg(a, #2*b)))" |
35 else adjust a b (negDivAlg(a, # 2*b)))" |
36 |
36 |
37 (*for the general case b~=0*) |
37 (*for the general case b~=0*) |
38 |
38 |
39 constdefs |
39 constdefs |
40 negateSnd :: "int*int => int*int" |
40 negateSnd :: "int*int => int*int" |
42 |
42 |
43 (*The full division algorithm considers all possible signs for a, b |
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*) |
44 including the special case a=0, b<0, because negDivAlg requires a<0*) |
45 divAlg :: "int*int => int*int" |
45 divAlg :: "int*int => int*int" |
46 "divAlg == |
46 "divAlg == |
47 %(a,b). if #0<=a then |
47 %(a,b). if Numeral0<=a then |
48 if #0<=b then posDivAlg (a,b) |
48 if Numeral0<=b then posDivAlg (a,b) |
49 else if a=#0 then (#0,#0) |
49 else if a=Numeral0 then (Numeral0,Numeral0) |
50 else negateSnd (negDivAlg (-a,-b)) |
50 else negateSnd (negDivAlg (-a,-b)) |
51 else |
51 else |
52 if #0<b then negDivAlg (a,b) |
52 if Numeral0<b then negDivAlg (a,b) |
53 else negateSnd (posDivAlg (-a,-b))" |
53 else negateSnd (posDivAlg (-a,-b))" |
54 |
54 |
55 instance |
55 instance |
56 int :: "Divides.div" (*avoid clash with 'div' token*) |
56 int :: "Divides.div" (*avoid clash with 'div' token*) |
57 |
57 |