# HG changeset patch
# User paulson
# Date 968924053 -7200
# Node ID 6ed42bcba70737c4e2509493055c094d85b6b29a
# Parent  734e0ec40f44b31cbc43e6badc4bb60671358070
a bit more of division

diff -r 734e0ec40f44 -r 6ed42bcba707 src/ZF/Integ/IntDiv.ML
--- a/src/ZF/Integ/IntDiv.ML	Wed Sep 13 22:49:17 2000 +0200
+++ b/src/ZF/Integ/IntDiv.ML	Thu Sep 14 11:34:13 2000 +0200
@@ -372,3 +372,64 @@
 qed "unique_remainder";
 
 
+(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
+
+
+Goal "adjust(a, b, <q,r>) = (let diff = r$-b in \
+\                         if #0 $<= diff then <#2$*q $+ #1,diff>  \
+\                                       else <#2$*q,r>)";
+by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1);
+qed "adjust_eq";
+Addsimps [adjust_eq];
+
+
+Goal "\\<lbrakk>#0 $< b; \\<not> a $< b\\<rbrakk>   \
+\     \\<Longrightarrow> nat_of(a $- #2 $\\<times> b $+ #1) < nat_of(a $- b $+ #1)";
+by (simp_tac (simpset() addsimps [zless_nat_conj]) 1);
+by (asm_full_simp_tac (simpset() addsimps [not_zless_iff_zle,
+                       zless_add1_iff_zle]@zcompare_rls) 1); 
+qed "posDivAlg_termination";
+
+val lemma = wf_measure RS (posDivAlg_def RS def_wfrec RS trans);
+
+Goal "[| #0 $< b; a: int; b: int |] ==> \
+\     posDivAlg(<a,b>) =      \
+\      (if a$<b then <#0,a> else adjust(a, b, posDivAlg (<a, #2$*b>)))";
+by (rtac lemma 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); 
+qed "posDivAlg_eqn";
+
+val [prem] =
+Goal "[| !!a b. [| a: int; b: int; \
+\                  ~ (a $< b | b $<= #0) --> P(<a, #2 $* b>) |] \
+\               ==> P(<a,b>) |] \
+\     ==> <u,v>: int*int \\<longrightarrow> P(<u,v>)"; 
+by (res_inst_tac [("a","<u,v>")] wf_induct 1);
+by (res_inst_tac [("A","int*int"), ("f","%<a,b>.nat_of (a $- b $+ #1)")] 
+                 wf_measure 1);
+by (Clarify_tac 1);
+by (rtac prem 1);
+by (dres_inst_tac [("x","<xa, #2 $\\<times> y>")] spec 3); 
+by Auto_tac;  
+by (asm_full_simp_tac (simpset() addsimps [not_zle_iff_zless, 
+                                           posDivAlg_termination]) 1); 
+val lemma = result() RS mp;
+
+
+val prems =
+Goal "[| u: int; v: int; \
+\        !!a b. [| a: int; b: int; ~ (a $< b | b $<= #0) --> P(a, #2 $* b) |] \
+\             ==> P(a,b) |] \
+\     ==> P(u,v)";
+by (subgoal_tac "(%<x,y>. P(x,y))(<u,v>)" 1);
+by (Asm_full_simp_tac 1); 
+by (rtac lemma 1);
+by (simp_tac (simpset() addsimps prems) 2);
+by (Full_simp_tac 1);  
+by (resolve_tac prems 1);
+by Auto_tac;  
+qed "posDivAlg_induct";
+
+(**TO BE COMPLETED**)
+
diff -r 734e0ec40f44 -r 6ed42bcba707 src/ZF/Integ/IntDiv.thy
--- a/src/ZF/Integ/IntDiv.thy	Wed Sep 13 22:49:17 2000 +0200
+++ b/src/ZF/Integ/IntDiv.thy	Thu Sep 14 11:34:13 2000 +0200
@@ -6,7 +6,7 @@
 The division operators div, mod
 *)
 
-IntDiv = IntArith + 
+IntDiv = IntArith + OrderArith + 
 
 constdefs
   quorem :: "[i,i] => o"
@@ -19,4 +19,17 @@
                             else <#2$*q,r>"
 
 
+(** the division algorithm **)
+
+constdefs posDivAlg :: "i => i"
+(*for the case a>=0, b>0*)
+(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))"*)
+    "posDivAlg(ab) ==
+       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>))"
+
+(**TO BE COMPLETED**)
+
 end