--- a/src/HOL/Integ/IntDiv.thy Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/Integ/IntDiv.thy Mon Oct 22 11:54:22 2001 +0200
@@ -12,27 +12,27 @@
quorem :: "(int*int) * (int*int) => bool"
"quorem == %((a,b), (q,r)).
a = b*q + r &
- (if Numeral0 < b then Numeral0<=r & r<b else b<r & r <= Numeral0)"
+ (if 0 < b then 0<=r & r<b else b<r & r <= 0)"
- adjust :: "[int, int, int*int] => int*int"
- "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b)
- else (2*q, r)"
+ adjust :: "[int, int*int] => int*int"
+ "adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b)
+ else (2*q, r)"
(** the division algorithm **)
(*for the case a>=0, b>0*)
consts posDivAlg :: "int*int => int*int"
-recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))"
+recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
"posDivAlg (a,b) =
- (if (a<b | b<=Numeral0) then (Numeral0,a)
- else adjust a b (posDivAlg(a, 2*b)))"
+ (if (a<b | b<=0) then (0,a)
+ else adjust b (posDivAlg(a, 2*b)))"
(*for the case a<0, b>0*)
consts negDivAlg :: "int*int => int*int"
recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
"negDivAlg (a,b) =
- (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b)
- else adjust a b (negDivAlg(a, 2*b)))"
+ (if (0<=a+b | b<=0) then (-1,a+b)
+ else adjust b (negDivAlg(a, 2*b)))"
(*for the general case b~=0*)
@@ -44,12 +44,12 @@
including the special case a=0, b<0, because negDivAlg requires a<0*)
divAlg :: "int*int => int*int"
"divAlg ==
- %(a,b). if Numeral0<=a then
- if Numeral0<=b then posDivAlg (a,b)
- else if a=Numeral0 then (Numeral0,Numeral0)
+ %(a,b). if 0<=a then
+ if 0<=b then posDivAlg (a,b)
+ else if a=0 then (0,0)
else negateSnd (negDivAlg (-a,-b))
else
- if Numeral0<b then negDivAlg (a,b)
+ if 0<b then negDivAlg (a,b)
else negateSnd (posDivAlg (-a,-b))"
instance