1 (* Title: HOL/Divides.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The division operators div, mod and the divides relation "dvd" |
|
7 *) |
|
8 |
|
9 |
|
10 (** Less-then properties **) |
|
11 |
|
12 bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS |
|
13 def_wfrec RS trans); |
|
14 |
|
15 Goal "(%m. m mod n) = wfrec (trancl pred_nat) \ |
|
16 \ (%f j. if j<n | n=0 then j else f (j-n))"; |
|
17 by (simp_tac (simpset() addsimps [mod_def]) 1); |
|
18 qed "mod_eq"; |
|
19 |
|
20 Goal "(%m. m div n) = wfrec (trancl pred_nat) \ |
|
21 \ (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"; |
|
22 by (simp_tac (simpset() addsimps [div_def]) 1); |
|
23 qed "div_eq"; |
|
24 |
|
25 |
|
26 (** Aribtrary definitions for division by zero. Useful to simplify |
|
27 certain equations **) |
|
28 |
|
29 Goal "a div 0 = (0::nat)"; |
|
30 by (rtac (div_eq RS wf_less_trans) 1); |
|
31 by (Asm_simp_tac 1); |
|
32 qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*) |
|
33 |
|
34 Goal "a mod 0 = (a::nat)"; |
|
35 by (rtac (mod_eq RS wf_less_trans) 1); |
|
36 by (Asm_simp_tac 1); |
|
37 qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*) |
|
38 |
|
39 fun div_undefined_case_tac s i = |
|
40 case_tac s i THEN |
|
41 Full_simp_tac (i+1) THEN |
|
42 asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, |
|
43 DIVISION_BY_ZERO_MOD]) i; |
|
44 |
|
45 (*** Remainder ***) |
|
46 |
|
47 Goal "m<n ==> m mod n = (m::nat)"; |
|
48 by (rtac (mod_eq RS wf_less_trans) 1); |
|
49 by (Asm_simp_tac 1); |
|
50 qed "mod_less"; |
|
51 Addsimps [mod_less]; |
|
52 |
|
53 Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n"; |
|
54 by (div_undefined_case_tac "n=0" 1); |
|
55 by (rtac (mod_eq RS wf_less_trans) 1); |
|
56 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
|
57 qed "mod_geq"; |
|
58 |
|
59 (*Avoids the ugly ~m<n above*) |
|
60 Goal "(n::nat) <= m ==> m mod n = (m-n) mod n"; |
|
61 by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1); |
|
62 qed "le_mod_geq"; |
|
63 |
|
64 Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)"; |
|
65 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); |
|
66 qed "mod_if"; |
|
67 |
|
68 Goal "m mod Suc 0 = 0"; |
|
69 by (induct_tac "m" 1); |
|
70 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq]))); |
|
71 qed "mod_1"; |
|
72 Addsimps [mod_1]; |
|
73 |
|
74 Goal "n mod n = (0::nat)"; |
|
75 by (div_undefined_case_tac "n=0" 1); |
|
76 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); |
|
77 qed "mod_self"; |
|
78 Addsimps [mod_self]; |
|
79 |
|
80 Goal "(m+n) mod n = m mod (n::nat)"; |
|
81 by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1); |
|
82 by (stac (mod_geq RS sym) 2); |
|
83 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
|
84 qed "mod_add_self2"; |
|
85 |
|
86 Goal "(n+m) mod n = m mod (n::nat)"; |
|
87 by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); |
|
88 qed "mod_add_self1"; |
|
89 |
|
90 Addsimps [mod_add_self1, mod_add_self2]; |
|
91 |
|
92 Goal "(m + k*n) mod n = m mod (n::nat)"; |
|
93 by (induct_tac "k" 1); |
|
94 by (ALLGOALS |
|
95 (asm_simp_tac |
|
96 (simpset() addsimps [read_instantiate [("y","n")] add_left_commute]))); |
|
97 qed "mod_mult_self1"; |
|
98 |
|
99 Goal "(m + n*k) mod n = m mod (n::nat)"; |
|
100 by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); |
|
101 qed "mod_mult_self2"; |
|
102 |
|
103 Addsimps [mod_mult_self1, mod_mult_self2]; |
|
104 |
|
105 Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)"; |
|
106 by (div_undefined_case_tac "n=0" 1); |
|
107 by (div_undefined_case_tac "k=0" 1); |
|
108 by (induct_thm_tac nat_less_induct "m" 1); |
|
109 by (stac mod_if 1); |
|
110 by (Asm_simp_tac 1); |
|
111 by (asm_simp_tac (simpset() addsimps [mod_geq, |
|
112 diff_less, diff_mult_distrib]) 1); |
|
113 qed "mod_mult_distrib"; |
|
114 |
|
115 Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)"; |
|
116 by (asm_simp_tac |
|
117 (simpset() addsimps [read_instantiate [("m","k")] mult_commute, |
|
118 mod_mult_distrib]) 1); |
|
119 qed "mod_mult_distrib2"; |
|
120 |
|
121 Goal "(m*n) mod n = (0::nat)"; |
|
122 by (div_undefined_case_tac "n=0" 1); |
|
123 by (induct_tac "m" 1); |
|
124 by (Asm_simp_tac 1); |
|
125 by (rename_tac "k" 1); |
|
126 by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1); |
|
127 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); |
|
128 qed "mod_mult_self_is_0"; |
|
129 |
|
130 Goal "(n*m) mod n = (0::nat)"; |
|
131 by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1); |
|
132 qed "mod_mult_self1_is_0"; |
|
133 Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0]; |
|
134 |
|
135 |
|
136 (*** Quotient ***) |
|
137 |
|
138 Goal "m<n ==> m div n = (0::nat)"; |
|
139 by (rtac (div_eq RS wf_less_trans) 1); |
|
140 by (Asm_simp_tac 1); |
|
141 qed "div_less"; |
|
142 Addsimps [div_less]; |
|
143 |
|
144 Goal "[| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
|
145 by (rtac (div_eq RS wf_less_trans) 1); |
|
146 by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); |
|
147 qed "div_geq"; |
|
148 |
|
149 (*Avoids the ugly ~m<n above*) |
|
150 Goal "[| 0<n; n<=m |] ==> m div n = Suc((m-n) div n)"; |
|
151 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); |
|
152 qed "le_div_geq"; |
|
153 |
|
154 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"; |
|
155 by (asm_simp_tac (simpset() addsimps [div_geq]) 1); |
|
156 qed "div_if"; |
|
157 |
|
158 |
|
159 (*Main Result about quotient and remainder.*) |
|
160 Goal "(m div n)*n + m mod n = (m::nat)"; |
|
161 by (div_undefined_case_tac "n=0" 1); |
|
162 by (induct_thm_tac nat_less_induct "m" 1); |
|
163 by (stac mod_if 1); |
|
164 by (ALLGOALS (asm_simp_tac |
|
165 (simpset() addsimps [add_assoc, div_geq, |
|
166 add_diff_inverse, diff_less]))); |
|
167 qed "mod_div_equality"; |
|
168 |
|
169 (* a simple rearrangement of mod_div_equality: *) |
|
170 Goal "(n::nat) * (m div n) = m - (m mod n)"; |
|
171 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); |
|
172 by (full_simp_tac (simpset() addsimps mult_ac) 1); |
|
173 by (arith_tac 1); |
|
174 qed "mult_div_cancel"; |
|
175 |
|
176 Goal "0<n ==> m mod n < (n::nat)"; |
|
177 by (induct_thm_tac nat_less_induct "m" 1); |
|
178 by (case_tac "na<n" 1); |
|
179 (*case n le na*) |
|
180 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2); |
|
181 (*case na<n*) |
|
182 by (Asm_simp_tac 1); |
|
183 qed "mod_less_divisor"; |
|
184 Addsimps [mod_less_divisor]; |
|
185 |
|
186 (*** More division laws ***) |
|
187 |
|
188 Goal "0<n ==> (m*n) div n = (m::nat)"; |
|
189 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1); |
|
190 by Auto_tac; |
|
191 qed "div_mult_self_is_m"; |
|
192 |
|
193 Goal "0<n ==> (n*m) div n = (m::nat)"; |
|
194 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1); |
|
195 qed "div_mult_self1_is_m"; |
|
196 Addsimps [div_mult_self_is_m, div_mult_self1_is_m]; |
|
197 |
|
198 (*mod_mult_distrib2 above is the counterpart for remainder*) |
|
199 |
|
200 |
|
201 (*** Proving facts about div and mod using quorem ***) |
|
202 |
|
203 Goal "[| b*q' + r' <= b*q + r; 0 < b; r < b |] \ |
|
204 \ ==> q' <= (q::nat)"; |
|
205 by (rtac leI 1); |
|
206 by (stac less_iff_Suc_add 1); |
|
207 by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2])); |
|
208 qed "unique_quotient_lemma"; |
|
209 |
|
210 Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |] \ |
|
211 \ ==> q = q'"; |
|
212 by (asm_full_simp_tac |
|
213 (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1); |
|
214 by Auto_tac; |
|
215 by (REPEAT |
|
216 (blast_tac (claset() addIs [order_antisym] |
|
217 addDs [order_eq_refl RS unique_quotient_lemma, |
|
218 sym]) 1)); |
|
219 qed "unique_quotient"; |
|
220 |
|
221 Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); 0 < b |] \ |
|
222 \ ==> r = r'"; |
|
223 by (subgoal_tac "q = q'" 1); |
|
224 by (blast_tac (claset() addIs [unique_quotient]) 2); |
|
225 by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1); |
|
226 qed "unique_remainder"; |
|
227 |
|
228 Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))"; |
|
229 by (cut_inst_tac [("m","a"),("n","b")] mod_div_equality 1); |
|
230 by (auto_tac |
|
231 (claset() addEs [sym], |
|
232 simpset() addsimps mult_ac@[Divides.quorem_def])); |
|
233 qed "quorem_div_mod"; |
|
234 |
|
235 Goal "[| quorem((a,b),(q,r)); 0 < b |] ==> a div b = q"; |
|
236 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); |
|
237 qed "quorem_div"; |
|
238 |
|
239 Goal "[| quorem((a,b),(q,r)); 0 < b |] ==> a mod b = r"; |
|
240 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); |
|
241 qed "quorem_mod"; |
|
242 |
|
243 (** A dividend of zero **) |
|
244 |
|
245 Goal "0 div m = (0::nat)"; |
|
246 by (div_undefined_case_tac "m=0" 1); |
|
247 by (Asm_simp_tac 1); |
|
248 qed "div_0"; |
|
249 |
|
250 Goal "0 mod m = (0::nat)"; |
|
251 by (div_undefined_case_tac "m=0" 1); |
|
252 by (Asm_simp_tac 1); |
|
253 qed "mod_0"; |
|
254 Addsimps [div_0, mod_0]; |
|
255 |
|
256 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **) |
|
257 |
|
258 Goal "[| quorem((b,c),(q,r)); 0 < c |] \ |
|
259 \ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; |
|
260 by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1); |
|
261 by (auto_tac |
|
262 (claset(), |
|
263 simpset() addsimps split_ifs@mult_ac@ |
|
264 [Divides.quorem_def, add_mult_distrib2])); |
|
265 val lemma = result(); |
|
266 |
|
267 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"; |
|
268 by (div_undefined_case_tac "c = 0" 1); |
|
269 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
|
270 qed "div_mult1_eq"; |
|
271 |
|
272 Goal "(a*b) mod c = a*(b mod c) mod (c::nat)"; |
|
273 by (div_undefined_case_tac "c = 0" 1); |
|
274 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
|
275 qed "mod_mult1_eq"; |
|
276 |
|
277 Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c"; |
|
278 by (rtac trans 1); |
|
279 by (res_inst_tac [("s","b*a mod c")] trans 1); |
|
280 by (rtac mod_mult1_eq 2); |
|
281 by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute]))); |
|
282 qed "mod_mult1_eq'"; |
|
283 |
|
284 Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"; |
|
285 by (rtac (mod_mult1_eq' RS trans) 1); |
|
286 by (rtac mod_mult1_eq 1); |
|
287 qed "mod_mult_distrib_mod"; |
|
288 |
|
289 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
|
290 |
|
291 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c |] \ |
|
292 \ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; |
|
293 by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1); |
|
294 by (auto_tac |
|
295 (claset(), |
|
296 simpset() addsimps split_ifs@mult_ac@ |
|
297 [Divides.quorem_def, add_mult_distrib2])); |
|
298 val lemma = result(); |
|
299 |
|
300 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
|
301 Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"; |
|
302 by (div_undefined_case_tac "c = 0" 1); |
|
303 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
|
304 MRS lemma RS quorem_div]) 1); |
|
305 qed "div_add1_eq"; |
|
306 |
|
307 Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"; |
|
308 by (div_undefined_case_tac "c = 0" 1); |
|
309 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
|
310 MRS lemma RS quorem_mod]) 1); |
|
311 qed "mod_add1_eq"; |
|
312 |
|
313 |
|
314 (*** proving a div (b*c) = (a div b) div c ***) |
|
315 |
|
316 (** first, a lemma to bound the remainder **) |
|
317 |
|
318 Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"; |
|
319 by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1); |
|
320 by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); |
|
321 by Auto_tac; |
|
322 by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); |
|
323 by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1); |
|
324 val mod_lemma = result(); |
|
325 |
|
326 Goal "[| quorem ((a,b), (q,r)); 0 < b; 0 < c |] \ |
|
327 \ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; |
|
328 by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1); |
|
329 by (auto_tac |
|
330 (claset(), |
|
331 simpset() addsimps mult_ac@ |
|
332 [Divides.quorem_def, add_mult_distrib2 RS sym, |
|
333 mod_lemma])); |
|
334 val lemma = result(); |
|
335 |
|
336 Goal "a div (b*c) = (a div b) div (c::nat)"; |
|
337 by (div_undefined_case_tac "b=0" 1); |
|
338 by (div_undefined_case_tac "c=0" 1); |
|
339 by (force_tac (claset(), |
|
340 simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1); |
|
341 qed "div_mult2_eq"; |
|
342 |
|
343 Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"; |
|
344 by (div_undefined_case_tac "b=0" 1); |
|
345 by (div_undefined_case_tac "c=0" 1); |
|
346 by (cut_inst_tac [("m", "a"), ("n","b")] mod_div_equality 1); |
|
347 by (auto_tac (claset(), |
|
348 simpset() addsimps [mult_commute, |
|
349 quorem_div_mod RS lemma RS quorem_mod])); |
|
350 qed "mod_mult2_eq"; |
|
351 |
|
352 |
|
353 (*** Cancellation of common factors in "div" ***) |
|
354 |
|
355 Goal "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"; |
|
356 by (stac div_mult2_eq 1); |
|
357 by Auto_tac; |
|
358 val lemma1 = result(); |
|
359 |
|
360 Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b"; |
|
361 by (div_undefined_case_tac "b = 0" 1); |
|
362 by (auto_tac |
|
363 (claset(), |
|
364 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
|
365 lemma1, lemma2])); |
|
366 qed "div_mult_mult1"; |
|
367 |
|
368 Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b"; |
|
369 by (dtac div_mult_mult1 1); |
|
370 by (auto_tac (claset(), simpset() addsimps [mult_commute])); |
|
371 qed "div_mult_mult2"; |
|
372 |
|
373 Addsimps [div_mult_mult1, div_mult_mult2]; |
|
374 |
|
375 |
|
376 (*** Distribution of factors over "mod" |
|
377 |
|
378 Could prove these as in Integ/IntDiv.ML, but we already have |
|
379 mod_mult_distrib and mod_mult_distrib2 above! |
|
380 |
|
381 Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"; |
|
382 qed "mod_mult_mult1"; |
|
383 |
|
384 Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)"; |
|
385 qed "mod_mult_mult2"; |
|
386 ***) |
|
387 |
|
388 (*** Further facts about div and mod ***) |
|
389 |
|
390 Goal "m div Suc 0 = m"; |
|
391 by (induct_tac "m" 1); |
|
392 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); |
|
393 qed "div_1"; |
|
394 Addsimps [div_1]; |
|
395 |
|
396 Goal "0<n ==> n div n = (1::nat)"; |
|
397 by (asm_simp_tac (simpset() addsimps [div_geq]) 1); |
|
398 qed "div_self"; |
|
399 Addsimps [div_self]; |
|
400 |
|
401 Goal "0<n ==> (m+n) div n = Suc (m div n)"; |
|
402 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1); |
|
403 by (stac (div_geq RS sym) 2); |
|
404 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
|
405 qed "div_add_self2"; |
|
406 |
|
407 Goal "0<n ==> (n+m) div n = Suc (m div n)"; |
|
408 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); |
|
409 qed "div_add_self1"; |
|
410 |
|
411 Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"; |
|
412 by (stac div_add1_eq 1); |
|
413 by (stac div_mult1_eq 1); |
|
414 by (Asm_simp_tac 1); |
|
415 qed "div_mult_self1"; |
|
416 |
|
417 Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)"; |
|
418 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); |
|
419 qed "div_mult_self2"; |
|
420 |
|
421 Addsimps [div_mult_self1, div_mult_self2]; |
|
422 |
|
423 (* Monotonicity of div in first argument *) |
|
424 Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)"; |
|
425 by (div_undefined_case_tac "k=0" 1); |
|
426 by (induct_thm_tac nat_less_induct "n" 1); |
|
427 by (Clarify_tac 1); |
|
428 by (case_tac "n<k" 1); |
|
429 (* 1 case n<k *) |
|
430 by (Asm_simp_tac 1); |
|
431 (* 2 case n >= k *) |
|
432 by (case_tac "m<k" 1); |
|
433 (* 2.1 case m<k *) |
|
434 by (Asm_simp_tac 1); |
|
435 (* 2.2 case m>=k *) |
|
436 by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1); |
|
437 qed_spec_mp "div_le_mono"; |
|
438 |
|
439 (* Antimonotonicity of div in second argument *) |
|
440 Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)"; |
|
441 by (subgoal_tac "0<n" 1); |
|
442 by (Asm_simp_tac 2); |
|
443 by (induct_thm_tac nat_less_induct "k" 1); |
|
444 by (rename_tac "k" 1); |
|
445 by (case_tac "k<n" 1); |
|
446 by (Asm_simp_tac 1); |
|
447 by (subgoal_tac "~(k<m)" 1); |
|
448 by (Asm_simp_tac 2); |
|
449 by (asm_simp_tac (simpset() addsimps [div_geq]) 1); |
|
450 by (subgoal_tac "(k-n) div n <= (k-m) div n" 1); |
|
451 by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2)); |
|
452 by (rtac le_trans 1); |
|
453 by (Asm_simp_tac 1); |
|
454 by (asm_simp_tac (simpset() addsimps [diff_less]) 1); |
|
455 qed "div_le_mono2"; |
|
456 |
|
457 Goal "m div n <= (m::nat)"; |
|
458 by (div_undefined_case_tac "n=0" 1); |
|
459 by (subgoal_tac "m div n <= m div 1" 1); |
|
460 by (Asm_full_simp_tac 1); |
|
461 by (rtac div_le_mono2 1); |
|
462 by (ALLGOALS Asm_simp_tac); |
|
463 qed "div_le_dividend"; |
|
464 Addsimps [div_le_dividend]; |
|
465 |
|
466 (* Similar for "less than" *) |
|
467 Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)"; |
|
468 by (induct_thm_tac nat_less_induct "m" 1); |
|
469 by (rename_tac "m" 1); |
|
470 by (case_tac "m<n" 1); |
|
471 by (Asm_full_simp_tac 1); |
|
472 by (subgoal_tac "0<n" 1); |
|
473 by (Asm_simp_tac 2); |
|
474 by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1); |
|
475 by (case_tac "n<m" 1); |
|
476 by (subgoal_tac "(m-n) div n < (m-n)" 1); |
|
477 by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); |
|
478 by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); |
|
479 by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); |
|
480 (* case n=m *) |
|
481 by (subgoal_tac "m=n" 1); |
|
482 by (Asm_simp_tac 2); |
|
483 by (Asm_simp_tac 1); |
|
484 qed_spec_mp "div_less_dividend"; |
|
485 Addsimps [div_less_dividend]; |
|
486 |
|
487 (*** Further facts about mod (mainly for the mutilated chess board ***) |
|
488 |
|
489 Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; |
|
490 by (div_undefined_case_tac "n=0" 1); |
|
491 by (induct_thm_tac nat_less_induct "m" 1); |
|
492 by (case_tac "Suc(na)<n" 1); |
|
493 (* case Suc(na) < n *) |
|
494 by (forward_tac [lessI RS less_trans] 1 |
|
495 THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1); |
|
496 (* case n <= Suc(na) *) |
|
497 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, |
|
498 mod_geq]) 1); |
|
499 by (auto_tac (claset(), |
|
500 simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq])); |
|
501 qed "mod_Suc"; |
|
502 |
|
503 |
|
504 (************************************************) |
|
505 (** Divides Relation **) |
|
506 (************************************************) |
|
507 |
|
508 Goalw [dvd_def] "n = m * k ==> m dvd n"; |
|
509 by (Blast_tac 1); |
|
510 qed "dvdI"; |
|
511 |
|
512 Goalw [dvd_def] "!!P. [|m dvd n; !!k. n = m*k ==> P|] ==> P"; |
|
513 by (Blast_tac 1); |
|
514 qed "dvdE"; |
|
515 |
|
516 Goalw [dvd_def] "m dvd (0::nat)"; |
|
517 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); |
|
518 qed "dvd_0_right"; |
|
519 AddIffs [dvd_0_right]; |
|
520 |
|
521 Goalw [dvd_def] "0 dvd m ==> m = (0::nat)"; |
|
522 by Auto_tac; |
|
523 qed "dvd_0_left"; |
|
524 |
|
525 Goal "(0 dvd (m::nat)) = (m = 0)"; |
|
526 by (blast_tac (claset() addIs [dvd_0_left]) 1); |
|
527 qed "dvd_0_left_iff"; |
|
528 AddIffs [dvd_0_left_iff]; |
|
529 |
|
530 Goalw [dvd_def] "Suc 0 dvd k"; |
|
531 by (Simp_tac 1); |
|
532 qed "dvd_1_left"; |
|
533 AddIffs [dvd_1_left]; |
|
534 |
|
535 Goal "(m dvd Suc 0) = (m = Suc 0)"; |
|
536 by (simp_tac (simpset() addsimps [dvd_def]) 1); |
|
537 qed "dvd_1_iff_1"; |
|
538 Addsimps [dvd_1_iff_1]; |
|
539 |
|
540 Goalw [dvd_def] "m dvd (m::nat)"; |
|
541 by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); |
|
542 qed "dvd_refl"; |
|
543 Addsimps [dvd_refl]; |
|
544 |
|
545 Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"; |
|
546 by (blast_tac (claset() addIs [mult_assoc] ) 1); |
|
547 qed "dvd_trans"; |
|
548 |
|
549 Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)"; |
|
550 by (force_tac (claset() addDs [mult_eq_self_implies_10], |
|
551 simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1); |
|
552 qed "dvd_anti_sym"; |
|
553 |
|
554 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"; |
|
555 by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); |
|
556 qed "dvd_add"; |
|
557 |
|
558 Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"; |
|
559 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); |
|
560 qed "dvd_diff"; |
|
561 |
|
562 Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)"; |
|
563 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); |
|
564 by (blast_tac (claset() addIs [dvd_add]) 1); |
|
565 qed "dvd_diffD"; |
|
566 |
|
567 Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)"; |
|
568 by (dres_inst_tac [("m","m")] dvd_diff 1); |
|
569 by Auto_tac; |
|
570 qed "dvd_diffD1"; |
|
571 |
|
572 Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)"; |
|
573 by (blast_tac (claset() addIs [mult_left_commute]) 1); |
|
574 qed "dvd_mult"; |
|
575 |
|
576 Goal "k dvd m ==> k dvd (m*n :: nat)"; |
|
577 by (stac mult_commute 1); |
|
578 by (etac dvd_mult 1); |
|
579 qed "dvd_mult2"; |
|
580 |
|
581 (* k dvd (m*k) *) |
|
582 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; |
|
583 |
|
584 Goal "(k dvd n + k) = (k dvd (n::nat))"; |
|
585 by (rtac iffI 1); |
|
586 by (etac dvd_add 2); |
|
587 by (rtac dvd_refl 2); |
|
588 by (subgoal_tac "n = (n+k)-k" 1); |
|
589 by (Simp_tac 2); |
|
590 by (etac ssubst 1); |
|
591 by (etac dvd_diff 1); |
|
592 by (rtac dvd_refl 1); |
|
593 qed "dvd_reduce"; |
|
594 |
|
595 Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"; |
|
596 by (div_undefined_case_tac "n=0" 1); |
|
597 by Auto_tac; |
|
598 by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1); |
|
599 qed "dvd_mod"; |
|
600 |
|
601 Goal "[| (k::nat) dvd m mod n; k dvd n |] ==> k dvd m"; |
|
602 by (subgoal_tac "k dvd (m div n)*n + m mod n" 1); |
|
603 by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); |
|
604 by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); |
|
605 qed "dvd_mod_imp_dvd"; |
|
606 |
|
607 Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"; |
|
608 by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); |
|
609 qed "dvd_mod_iff"; |
|
610 |
|
611 Goalw [dvd_def] "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"; |
|
612 by (etac exE 1); |
|
613 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); |
|
614 qed "dvd_mult_cancel"; |
|
615 |
|
616 Goal "0<m ==> (m*n dvd m) = (n = (1::nat))"; |
|
617 by Auto_tac; |
|
618 by (subgoal_tac "m*n dvd m*1" 1); |
|
619 by (dtac dvd_mult_cancel 1); |
|
620 by Auto_tac; |
|
621 qed "dvd_mult_cancel1"; |
|
622 |
|
623 Goal "0<m ==> (n*m dvd m) = (n = (1::nat))"; |
|
624 by (stac mult_commute 1); |
|
625 by (etac dvd_mult_cancel1 1); |
|
626 qed "dvd_mult_cancel2"; |
|
627 |
|
628 Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"; |
|
629 by (Clarify_tac 1); |
|
630 by (res_inst_tac [("x","k*ka")] exI 1); |
|
631 by (asm_simp_tac (simpset() addsimps mult_ac) 1); |
|
632 qed "mult_dvd_mono"; |
|
633 |
|
634 Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k"; |
|
635 by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); |
|
636 by (Blast_tac 1); |
|
637 qed "dvd_mult_left"; |
|
638 |
|
639 Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k"; |
|
640 by (Clarify_tac 1); |
|
641 by (res_inst_tac [("x","i*k")] exI 1); |
|
642 by (simp_tac (simpset() addsimps mult_ac) 1); |
|
643 qed "dvd_mult_right"; |
|
644 |
|
645 Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)"; |
|
646 by (Clarify_tac 1); |
|
647 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); |
|
648 by (etac conjE 1); |
|
649 by (rtac le_trans 1); |
|
650 by (rtac (le_refl RS mult_le_mono) 2); |
|
651 by (etac Suc_leI 2); |
|
652 by (Simp_tac 1); |
|
653 qed "dvd_imp_le"; |
|
654 |
|
655 Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)"; |
|
656 by (div_undefined_case_tac "k=0" 1); |
|
657 by Safe_tac; |
|
658 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); |
|
659 by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1); |
|
660 by (stac mult_commute 1); |
|
661 by (Asm_simp_tac 1); |
|
662 qed "dvd_eq_mod_eq_0"; |
|
663 |
|
664 Goal "n dvd m ==> n * (m div n) = (m::nat)"; |
|
665 by (subgoal_tac "m mod n = 0" 1); |
|
666 by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1); |
|
667 by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1); |
|
668 qed "dvd_mult_div_cancel"; |
|
669 |
|
670 Goal "(m mod d = 0) = (EX q::nat. m = d*q)"; |
|
671 by (auto_tac (claset(), |
|
672 simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def])); |
|
673 qed "mod_eq_0_iff"; |
|
674 AddSDs [mod_eq_0_iff RS iffD1]; |
|
675 |
|
676 (*Loses information, namely we also have r<d provided d is nonzero*) |
|
677 Goal "(m mod d = r) ==> EX q::nat. m = r + q*d"; |
|
678 by (cut_inst_tac [("m","m")] mod_div_equality 1); |
|
679 by (full_simp_tac (simpset() addsimps add_ac) 1); |
|
680 by (blast_tac (claset() addIs [sym]) 1); |
|
681 qed "mod_eqD"; |
|
682 |
|