28 wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)), |
28 wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)), |
29 ab, |
29 ab, |
30 %<a,b> f. if (a$<b | b$<=#0) then <#0,a> |
30 %<a,b> f. if (a$<b | b$<=#0) then <#0,a> |
31 else adjust(a, b, f ` <a,#2$*b>))" |
31 else adjust(a, b, f ` <a,#2$*b>))" |
32 |
32 |
33 (**TO BE COMPLETED**) |
33 |
|
34 (*for the case a<0, b>0*) |
|
35 constdefs negDivAlg :: "i => i" |
|
36 (*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a $- b))"*) |
|
37 "negDivAlg(ab) == |
|
38 wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)), |
|
39 ab, |
|
40 %<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b> |
|
41 else adjust(a, b, f ` <a,#2$*b>))" |
|
42 |
|
43 (*for the general case b\\<noteq>0*) |
|
44 |
|
45 constdefs |
|
46 negateSnd :: "i => i" |
|
47 "negateSnd == %<q,r>. <q, $-r>" |
|
48 |
|
49 (*The full division algorithm considers all possible signs for a, b |
|
50 including the special case a=0, b<0, because negDivAlg requires a<0*) |
|
51 divAlg :: "i => i" |
|
52 "divAlg == |
|
53 %<a,b>. if #0 $<= a then |
|
54 if #0 $<= b then posDivAlg (<a,b>) |
|
55 else if a=#0 then <#0,#0> |
|
56 else negateSnd (negDivAlg (<$-a,$-b>)) |
|
57 else |
|
58 if #0$<b then negDivAlg (<a,b>) |
|
59 else negateSnd (posDivAlg (<$-a,$-b>))" |
|
60 |
|
61 zdiv :: [i,i]=>i (infixl "zdiv" 70) |
|
62 "a zdiv b == fst (divAlg (<intify(a), intify(b)>))" |
|
63 |
|
64 zmod :: [i,i]=>i (infixl "zmod" 70) |
|
65 "a zmod b == snd (divAlg (<intify(a), intify(b)>))" |
34 |
66 |
35 end |
67 end |