# HG changeset patch
# User paulson
# Date 1003745460 -7200
# Node ID 0493188cff4240c2a020dfd81cf2e3e17f3c2cfb
# Parent  181bd2050cf4c21bb4f9ba4f4f2ed960a8ebe3dc
deleted the redundant first argument of adjust(a,b)

diff -r 181bd2050cf4 -r 0493188cff42 src/ZF/Integ/IntDiv.ML
--- 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, 
diff -r 181bd2050cf4 -r 0493188cff42 src/ZF/Integ/IntDiv.thy
--- 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*)