--- a/src/ZF/Integ/IntDiv.thy Thu Sep 07 15:31:09 2000 +0200
+++ b/src/ZF/Integ/IntDiv.thy Thu Sep 07 17:36:37 2000 +0200
@@ -18,45 +18,5 @@
"adjust(a,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 $+ #1))"
- "posDivAlg <a,b> =
- (if (a$<b | b$<=#0) then <#0,a>
- else adjust a 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 (#0$<=a$+b | b$<=#0) then <#-1,a$+b>
- else adjust a b (negDivAlg<a,#2$*b>))"
-
-(*for the general case b~=0*)
-
-constdefs
- negateSnd :: "int*int => int*int"
- "negateSnd == %<q,r>. <q,-r>"
-
- (*The full division algorithm considers all possible signs for a, b
- including the special case a=0, b<0, because negDivAlg requires a<0*)
- divAlg :: "int*int => int*int"
- "divAlg ==
- %<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 #0$<b then negDivAlg <a,b>
- else negateSnd (posDivAlg <-a,-b>)"
-
-defs
- div_def "a div b == fst (divAlg <a,b>)"
- mod_def "a mod b == snd (divAlg <a,b>)"
-
-**)
end