6917
|
1 |
(* Title: HOL/IntDiv.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1999 University of Cambridge
|
|
5 |
|
|
6 |
The division operators div, mod and the divides relation "dvd"
|
|
7 |
*)
|
|
8 |
|
|
9 |
Addsimps [zless_nat_conj];
|
|
10 |
|
|
11 |
(*** Uniqueness and monotonicity of quotients and remainders ***)
|
|
12 |
|
|
13 |
Goal "[| r' + b*q' <= r + b*q; #0 <= r'; #0 < b; r < b |] \
|
|
14 |
\ ==> q' <= (q::int)";
|
|
15 |
by (subgoal_tac "r' + b * (q'-q) <= r" 1);
|
|
16 |
by (simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2]) 2);
|
|
17 |
by (subgoal_tac "#0 < b * (#1 + q - q')" 1);
|
|
18 |
by (etac order_le_less_trans 2);
|
|
19 |
by (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
|
|
20 |
zadd_zmult_distrib2]) 2);
|
|
21 |
by (subgoal_tac "b * q' < b * (#1 + q)" 1);
|
|
22 |
by (full_simp_tac (simpset() addsimps zcompare_rls@[zdiff_zmult_distrib2,
|
|
23 |
zadd_zmult_distrib2]) 2);
|
|
24 |
by (Asm_full_simp_tac 1);
|
|
25 |
qed "unique_quotient_lemma";
|
|
26 |
|
|
27 |
Goal "[| r' + b*q' <= r + b*q; r <= #0; b < #0; b < r' |] \
|
|
28 |
\ ==> q <= (q'::int)";
|
|
29 |
by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")]
|
|
30 |
unique_quotient_lemma 1);
|
|
31 |
by (auto_tac (claset(),
|
|
32 |
simpset() addsimps zcompare_rls@[zmult_zminus_right]));
|
|
33 |
qed "unique_quotient_lemma_neg";
|
|
34 |
|
|
35 |
|
|
36 |
Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= #0 |] \
|
|
37 |
\ ==> q = q'";
|
|
38 |
by (asm_full_simp_tac
|
|
39 |
(simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1);
|
|
40 |
by Safe_tac;
|
|
41 |
by (ALLGOALS Asm_full_simp_tac);
|
|
42 |
by (REPEAT
|
|
43 |
(blast_tac (claset() addIs [order_antisym]
|
|
44 |
addDs [order_eq_refl RS unique_quotient_lemma,
|
|
45 |
order_eq_refl RS unique_quotient_lemma_neg,
|
|
46 |
sym]) 1));
|
|
47 |
qed "unique_quotient";
|
|
48 |
|
|
49 |
|
|
50 |
Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= #0 |] \
|
|
51 |
\ ==> r = r'";
|
|
52 |
by (subgoal_tac "q = q'" 1);
|
|
53 |
by (blast_tac (claset() addIs [unique_quotient]) 2);
|
|
54 |
by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1);
|
|
55 |
qed "unique_remainder";
|
|
56 |
|
|
57 |
|
|
58 |
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***)
|
|
59 |
|
|
60 |
Goal "adjust a b (q,r) = (if #0 <= r-b then (#2*q + #1, r-b) \
|
|
61 |
\ else (#2*q, r))";
|
|
62 |
by (simp_tac (simpset() addsimps [adjust_def]) 1);
|
|
63 |
qed "adjust_eq";
|
|
64 |
Addsimps [adjust_eq];
|
|
65 |
|
|
66 |
(*Proving posDivAlg's termination condition*)
|
|
67 |
val [tc] = posDivAlg.tcs;
|
|
68 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
|
|
69 |
by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
|
|
70 |
val lemma = result();
|
|
71 |
|
|
72 |
(* removing the termination condition from the generated theorems *)
|
|
73 |
|
|
74 |
bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.rules);
|
|
75 |
|
|
76 |
(**use with simproc to avoid re-proving the premise*)
|
|
77 |
Goal "#0 < b ==> \
|
|
78 |
\ posDivAlg (a,b) = \
|
|
79 |
\ (if a<b then (#0,a) else adjust a b (posDivAlg(a, #2*b)))";
|
|
80 |
by (rtac (posDivAlg_raw_eqn RS trans) 1);
|
|
81 |
by (Asm_simp_tac 1);
|
|
82 |
qed "posDivAlg_eqn";
|
|
83 |
|
|
84 |
val posDivAlg_induct = lemma RS posDivAlg.induct;
|
|
85 |
|
|
86 |
|
|
87 |
(*Correctness of posDivAlg: it computes quotients correctly*)
|
|
88 |
Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
|
|
89 |
by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
|
|
90 |
by Auto_tac;
|
|
91 |
by (ALLGOALS
|
|
92 |
(asm_full_simp_tac (simpset() addsimps [quorem_def,
|
|
93 |
pos_times_pos_is_pos])));
|
|
94 |
(*base case: a<b*)
|
|
95 |
by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
|
|
96 |
(*main argument*)
|
|
97 |
by (stac posDivAlg_eqn 1);
|
|
98 |
by (ALLGOALS Asm_simp_tac);
|
|
99 |
by (etac splitE 1);
|
|
100 |
by Auto_tac;
|
|
101 |
(*the "add one" case*)
|
|
102 |
by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
|
|
103 |
(*the "just double" case*)
|
|
104 |
by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
|
|
105 |
qed_spec_mp "posDivAlg_correct";
|
|
106 |
|
|
107 |
|
|
108 |
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***)
|
|
109 |
|
|
110 |
(*Proving negDivAlg's termination condition*)
|
|
111 |
val [tc] = negDivAlg.tcs;
|
|
112 |
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
|
|
113 |
by (auto_tac (claset(), simpset() addsimps [zmult_2_right]));
|
|
114 |
val lemma = result();
|
|
115 |
|
|
116 |
(* removing the termination condition from the generated theorems *)
|
|
117 |
|
|
118 |
bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.rules);
|
|
119 |
|
|
120 |
(**use with simproc to avoid re-proving the premise*)
|
|
121 |
Goal "#0 < b ==> \
|
|
122 |
\ negDivAlg (a,b) = \
|
|
123 |
\ (if #0<=a+b then (#-1,a+b) else adjust a b (negDivAlg(a, #2*b)))";
|
|
124 |
by (rtac (negDivAlg_raw_eqn RS trans) 1);
|
|
125 |
by (Asm_simp_tac 1);
|
|
126 |
qed "negDivAlg_eqn";
|
|
127 |
|
|
128 |
val negDivAlg_induct = lemma RS negDivAlg.induct;
|
|
129 |
|
|
130 |
|
|
131 |
(*Correctness of negDivAlg: it computes quotients correctly
|
|
132 |
It doesn't work if a=0 because the 0/b=0 rather than -1*)
|
|
133 |
Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
|
|
134 |
by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
|
|
135 |
by Auto_tac;
|
|
136 |
by (ALLGOALS
|
|
137 |
(asm_full_simp_tac (simpset() addsimps [quorem_def,
|
|
138 |
pos_times_pos_is_pos])));
|
|
139 |
(*base case: 0<=a+b*)
|
|
140 |
by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
|
|
141 |
(*main argument*)
|
|
142 |
by (stac negDivAlg_eqn 1);
|
|
143 |
by (ALLGOALS Asm_simp_tac);
|
|
144 |
by (etac splitE 1);
|
|
145 |
by Auto_tac;
|
|
146 |
(*the "add one" case*)
|
|
147 |
by (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
|
|
148 |
(*the "just double" case*)
|
|
149 |
by (asm_full_simp_tac (simpset() addsimps zcompare_rls@[zmult_2_right]) 1);
|
|
150 |
qed_spec_mp "negDivAlg_correct";
|
|
151 |
|
|
152 |
|
|
153 |
(*** Existence shown by proving the division algorithm to be correct ***)
|
|
154 |
|
|
155 |
(*the case a=0*)
|
|
156 |
Goal "b ~= #0 ==> quorem ((#0,b), (#0,#0))";
|
|
157 |
by (auto_tac (claset(),
|
|
158 |
simpset() addsimps [quorem_def, linorder_neq_iff]));
|
|
159 |
qed "quorem_0";
|
|
160 |
|
|
161 |
Goal "posDivAlg (#0, b) = (#0, #0)";
|
|
162 |
by (stac posDivAlg_raw_eqn 1);
|
|
163 |
by Auto_tac;
|
|
164 |
qed "posDivAlg_0";
|
|
165 |
Addsimps [posDivAlg_0];
|
|
166 |
|
|
167 |
Goal "negDivAlg (#-1, b) = (#-1, b-#1)";
|
|
168 |
by (stac negDivAlg_raw_eqn 1);
|
|
169 |
by Auto_tac;
|
|
170 |
qed "negDivAlg_minus1";
|
|
171 |
Addsimps [negDivAlg_minus1];
|
|
172 |
|
|
173 |
Goalw [negateSnd_def] "negateSnd(q,r) = (q,-r)";
|
|
174 |
by Auto_tac;
|
|
175 |
qed "negateSnd_eq";
|
|
176 |
Addsimps [negateSnd_eq];
|
|
177 |
|
|
178 |
Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
|
|
179 |
by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
|
|
180 |
qed "quorem_neg";
|
|
181 |
|
|
182 |
Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))";
|
|
183 |
by (auto_tac (claset(),
|
|
184 |
simpset() addsimps [quorem_0, divAlg_def]));
|
|
185 |
by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct,
|
|
186 |
negDivAlg_correct]));
|
|
187 |
by (auto_tac (claset(),
|
|
188 |
simpset() addsimps [quorem_def, linorder_neq_iff]));
|
|
189 |
qed "divAlg_correct";
|
|
190 |
|
|
191 |
Goal "b ~= (#0::int) ==> a = b * (a div b) + (a mod b)";
|
|
192 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
|
|
193 |
by (auto_tac (claset(),
|
|
194 |
simpset() addsimps [quorem_def, div_def, mod_def]));
|
|
195 |
qed "zmod_zdiv_equality";
|
|
196 |
(*the name mod_div_equality would hide the other one proved in Divides.ML
|
|
197 |
existing users aren't using name spaces for theorems*)
|
|
198 |
|
|
199 |
Goal "(#0::int) < b ==> #0 <= a mod b & a mod b < b";
|
|
200 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
|
|
201 |
by (auto_tac (claset(),
|
|
202 |
simpset() addsimps [quorem_def, mod_def]));
|
|
203 |
bind_thm ("pos_mod_sign", result() RS conjunct1);
|
|
204 |
bind_thm ("pos_mod_bound", result() RS conjunct2);
|
|
205 |
|
|
206 |
Goal "b < (#0::int) ==> a mod b <= #0 & b < a mod b";
|
|
207 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1);
|
|
208 |
by (auto_tac (claset(),
|
|
209 |
simpset() addsimps [quorem_def, div_def, mod_def]));
|
|
210 |
bind_thm ("neg_mod_sign", result() RS conjunct1);
|
|
211 |
bind_thm ("neg_mod_bound", result() RS conjunct2);
|
|
212 |
|
|
213 |
|
|
214 |
(*** Computation of division and remainder ***)
|
|
215 |
|
|
216 |
Goal "(#0::int) div b = #0";
|
|
217 |
by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
|
|
218 |
qed "div_zero";
|
|
219 |
|
|
220 |
Goal "(#0::int) mod b = #0";
|
|
221 |
by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
|
|
222 |
qed "mod_zero";
|
|
223 |
|
|
224 |
Addsimps [div_zero, mod_zero];
|
|
225 |
|
|
226 |
(** a positive, b positive **)
|
|
227 |
|
|
228 |
Goal "[| #0 < a; #0 < b |] ==> a div b = fst (posDivAlg(a,b))";
|
|
229 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
|
|
230 |
qed "div_pos_pos";
|
|
231 |
|
|
232 |
Goal "[| #0 < a; #0 < b |] ==> a mod b = snd (posDivAlg(a,b))";
|
|
233 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
|
|
234 |
qed "mod_pos_pos";
|
|
235 |
|
|
236 |
(** a negative, b positive **)
|
|
237 |
|
|
238 |
Goal "[| a < #0; #0 < b |] ==> a div b = fst (negDivAlg(a,b))";
|
|
239 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
|
|
240 |
qed "div_neg_pos";
|
|
241 |
|
|
242 |
Goal "[| a < #0; #0 < b |] ==> a mod b = snd (negDivAlg(a,b))";
|
|
243 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
|
|
244 |
qed "mod_neg_pos";
|
|
245 |
|
|
246 |
(** a positive, b negative **)
|
|
247 |
|
|
248 |
Goal "[| #0 < a; b < #0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))";
|
|
249 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
|
|
250 |
qed "div_pos_neg";
|
|
251 |
|
|
252 |
Goal "[| #0 < a; b < #0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))";
|
|
253 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
|
|
254 |
qed "mod_pos_neg";
|
|
255 |
|
|
256 |
(** a negative, b negative **)
|
|
257 |
|
|
258 |
Goal "[| a < #0; b < #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))";
|
|
259 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1);
|
|
260 |
qed "div_neg_neg";
|
|
261 |
|
|
262 |
Goal "[| a < #0; b < #0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))";
|
|
263 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1);
|
|
264 |
qed "mod_neg_neg";
|
|
265 |
|
|
266 |
Addsimps (map (read_instantiate_sg (sign_of IntDiv.thy)
|
|
267 |
[("a", "number_of ?v"), ("b", "number_of ?w")])
|
|
268 |
[div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg,
|
|
269 |
mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg,
|
|
270 |
posDivAlg_eqn, negDivAlg_eqn]);
|
|
271 |
|
|
272 |
|
|
273 |
(** Special-case simplification **)
|
|
274 |
|
|
275 |
Goal "a mod (#1::int) = #0";
|
|
276 |
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1);
|
|
277 |
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2);
|
|
278 |
by Auto_tac;
|
|
279 |
qed "zmod_1";
|
|
280 |
Addsimps [zmod_1];
|
|
281 |
|
|
282 |
Goal "a div (#1::int) = a";
|
|
283 |
by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1);
|
|
284 |
by Auto_tac;
|
|
285 |
qed "zdiv_1";
|
|
286 |
Addsimps [zdiv_1];
|
|
287 |
|
|
288 |
Goal "a mod (#-1::int) = #0";
|
|
289 |
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1);
|
|
290 |
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2);
|
|
291 |
by Auto_tac;
|
|
292 |
qed "zmod_minus1";
|
|
293 |
Addsimps [zmod_minus1];
|
|
294 |
|
|
295 |
Goal "a div (#-1::int) = -a";
|
|
296 |
by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1);
|
|
297 |
by Auto_tac;
|
|
298 |
qed "zdiv_minus1";
|
|
299 |
Addsimps [zdiv_minus1];
|
|
300 |
|
|
301 |
|
|
302 |
(** Monotonicity results **)
|
|
303 |
|
|
304 |
|
|
305 |
Goal "[| a <= a'; #0 < (b::int) |] ==> a div b <= a' div b";
|
|
306 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
|
|
307 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
|
|
308 |
by Auto_tac;
|
|
309 |
by (rtac unique_quotient_lemma 1);
|
|
310 |
by (etac subst 1);
|
|
311 |
by (etac subst 1);
|
|
312 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound])));
|
|
313 |
qed "zdiv_mono1";
|
|
314 |
|
|
315 |
Goal "[| a <= a'; (b::int) < #0 |] ==> a' div b <= a div b";
|
|
316 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1);
|
|
317 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 2);
|
|
318 |
by Auto_tac;
|
|
319 |
by (rtac unique_quotient_lemma_neg 1);
|
|
320 |
by (etac subst 1);
|
|
321 |
by (etac subst 1);
|
|
322 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound])));
|
|
323 |
qed "zdiv_mono1_neg";
|
|
324 |
|
|
325 |
|
|
326 |
|
|
327 |
(** The division algorithm in ML **)
|
|
328 |
|
|
329 |
fun posDivAlg (a,b) =
|
|
330 |
if a<b then (0,a)
|
|
331 |
else let val (q,r) = posDivAlg(a, 2*b)
|
|
332 |
in if 0<=r-b then (2*q+1, r-b)
|
|
333 |
else (2*q, r)
|
|
334 |
end;
|
|
335 |
|
|
336 |
fun negDivAlg (a,b) =
|
|
337 |
if 0<=a+b then (~1,a+b)
|
|
338 |
else let val (q,r) = negDivAlg(a, 2*b)
|
|
339 |
in if 0<=r-b then (2*q+1, r-b)
|
|
340 |
else (2*q, r)
|
|
341 |
end;
|
|
342 |
|
|
343 |
fun negateSnd (q,r:int) = (q,~r);
|
|
344 |
|
|
345 |
fun divAlg (a,b) = if 0<=a then
|
|
346 |
if b>0 then posDivAlg (a,b)
|
|
347 |
else if a=0 then (0,0)
|
|
348 |
else negateSnd (negDivAlg (~a,~b))
|
|
349 |
else
|
|
350 |
if 0<b then negDivAlg (a,b)
|
|
351 |
else negateSnd (posDivAlg (~a,~b));
|