author paulson Thu, 14 Sep 2000 11:34:13 +0200 changeset 9955 6ed42bcba707 parent 9954 734e0ec40f44 child 9956 e75e6a603e71
a bit more of division
 src/ZF/Integ/IntDiv.ML file | annotate | diff | comparison | revisions src/ZF/Integ/IntDiv.thy file | annotate | diff | comparison | revisions
```--- 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>)";
+
+
+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);
+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;
+                                           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**)
+```
```--- 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```