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**)
+