--- a/src/ZF/Integ/IntDiv.ML Mon Oct 22 12:01:35 2001 +0200
+++ b/src/ZF/Integ/IntDiv.ML Mon Oct 22 12:11:00 2001 +0200
@@ -333,9 +333,9 @@
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
-Goal "adjust(a, b, <q,r>) = (let diff = r$-b in \
+Goal "adjust(b, <q,r>) = (let diff = r$-b in \
\ if #0 $<= diff then <#2$*q $+ #1,diff> \
-\ else <#2$*q,r>)";
+\ else <#2$*q,r>)";
by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
qed "adjust_eq";
Addsimps [adjust_eq];
@@ -352,7 +352,7 @@
Goal "[| #0 $< b; a \\<in> int; b \\<in> int |] ==> \
\ posDivAlg(<a,b>) = \
-\ (if a$<b then <#0,a> else adjust(a, b, posDivAlg (<a, #2$*b>)))";
+\ (if a$<b then <#0,a> else adjust(b, posDivAlg (<a, #2$*b>)))";
by (rtac (posDivAlg_unfold RS trans) 1);
by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
by (asm_simp_tac (simpset() addsimps [vimage_iff, posDivAlg_termination]) 1);
@@ -513,7 +513,7 @@
Goal "[| #0 $< b; a \\<in> int; b \\<in> int |] ==> \
\ negDivAlg(<a,b>) = \
\ (if #0 $<= a$+b then <#-1,a$+b> \
-\ else adjust(a, b, negDivAlg (<a, #2$*b>)))";
+\ else adjust(b, negDivAlg (<a, #2$*b>)))";
by (rtac (negDivAlg_unfold RS trans) 1);
by (asm_simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
by (asm_simp_tac (simpset() addsimps [not_zle_iff_zless, vimage_iff,
--- a/src/ZF/Integ/IntDiv.thy Mon Oct 22 12:01:35 2001 +0200
+++ b/src/ZF/Integ/IntDiv.thy Mon Oct 22 12:11:00 2001 +0200
@@ -14,9 +14,9 @@
a = b$*q $+ r &
(#0$<b & #0$<=r & r$<b | ~(#0$<b) & b$<r & r $<= #0)"
- adjust :: "[i,i,i] => i"
- "adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
- else <#2$*q,r>"
+ adjust :: "[i,i] => i"
+ "adjust(b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
+ else <#2$*q,r>"
(** the division algorithm **)
@@ -28,7 +28,7 @@
wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
ab,
%<a,b> f. if (a$<b | b$<=#0) then <#0,a>
- else adjust(a, b, f ` <a,#2$*b>))"
+ else adjust(b, f ` <a,#2$*b>))"
(*for the case a<0, b>0*)
@@ -38,7 +38,7 @@
wfrec(measure(int*int, %<a,b>. nat_of ($- a $- b)),
ab,
%<a,b> f. if (#0 $<= a$+b | b$<=#0) then <#-1,a$+b>
- else adjust(a, b, f ` <a,#2$*b>))"
+ else adjust(b, f ` <a,#2$*b>))"
(*for the general case b\\<noteq>0*)