170 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); |
171 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); |
171 by (full_simp_tac (simpset() addsimps mult_ac) 1); |
172 by (full_simp_tac (simpset() addsimps mult_ac) 1); |
172 by (arith_tac 1); |
173 by (arith_tac 1); |
173 qed "mult_div_cancel"; |
174 qed "mult_div_cancel"; |
174 |
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 @ [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 [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@[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 (** proving (a*b) div c = a * (b div c) + a * (b mod c) **) |
|
244 |
|
245 Goal "[| quorem((b,c),(q,r)); 0 < c |] \ |
|
246 \ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; |
|
247 by (cut_inst_tac [("m", "a*r"), ("n","c")] mod_div_equality 1); |
|
248 by (auto_tac |
|
249 (claset(), |
|
250 simpset() addsimps split_ifs@mult_ac@ |
|
251 [quorem_def, add_mult_distrib2])); |
|
252 val lemma = result(); |
|
253 |
|
254 Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"; |
|
255 by (div_undefined_case_tac "c = 0" 1); |
|
256 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
|
257 qed "div_mult1_eq"; |
|
258 |
|
259 Goal "(a*b) mod c = a*(b mod c) mod (c::nat)"; |
|
260 by (div_undefined_case_tac "c = 0" 1); |
|
261 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
|
262 qed "mod_mult1_eq"; |
|
263 |
|
264 Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c"; |
|
265 by (rtac trans 1); |
|
266 by (res_inst_tac [("s","b*a mod c")] trans 1); |
|
267 by (rtac mod_mult1_eq 2); |
|
268 by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute]))); |
|
269 qed "mod_mult1_eq'"; |
|
270 |
|
271 Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"; |
|
272 by (rtac (mod_mult1_eq' RS trans) 1); |
|
273 by (rtac mod_mult1_eq 1); |
|
274 qed "mod_mult_distrib_mod"; |
|
275 |
|
276 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
|
277 |
|
278 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); 0 < c |] \ |
|
279 \ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; |
|
280 by (cut_inst_tac [("m", "ar+br"), ("n","c")] mod_div_equality 1); |
|
281 by (auto_tac |
|
282 (claset(), |
|
283 simpset() addsimps split_ifs@mult_ac@ |
|
284 [quorem_def, add_mult_distrib2])); |
|
285 val lemma = result(); |
|
286 |
|
287 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
|
288 Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"; |
|
289 by (div_undefined_case_tac "c = 0" 1); |
|
290 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
|
291 MRS lemma RS quorem_div]) 1); |
|
292 qed "div_add1_eq"; |
|
293 |
|
294 Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"; |
|
295 by (div_undefined_case_tac "c = 0" 1); |
|
296 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
|
297 MRS lemma RS quorem_mod]) 1); |
|
298 qed "mod_add1_eq"; |
|
299 |
|
300 |
|
301 (*** proving a div (b*c) = (a div b) div c ***) |
|
302 |
|
303 (** first, two lemmas to bound the remainder for the cases b<0 and b>0 **) |
|
304 |
|
305 Goal "[| (0::nat) < c; r < b |] ==> 0 <= b * (q mod c) + r"; |
|
306 by (subgoal_tac "0 <= b * (q mod c)" 1); |
|
307 by Auto_tac; |
|
308 val lemma3 = result(); |
|
309 |
|
310 Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"; |
|
311 by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1); |
|
312 by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); |
|
313 by Auto_tac; |
|
314 by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); |
|
315 by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1); |
|
316 val lemma4 = result(); |
|
317 |
|
318 Goal "[| quorem ((a,b), (q,r)); 0 < b; 0 < c |] \ |
|
319 \ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; |
|
320 by (cut_inst_tac [("m", "q"), ("n","c")] mod_div_equality 1); |
|
321 by (auto_tac |
|
322 (claset(), |
|
323 simpset() addsimps mult_ac@ |
|
324 [quorem_def, add_mult_distrib2 RS sym, |
|
325 lemma3, lemma4])); |
|
326 val lemma = result(); |
|
327 |
|
328 Goal "(0::nat) < c ==> a div (b*c) = (a div b) div c"; |
|
329 by (div_undefined_case_tac "b = 0" 1); |
|
330 by (force_tac (claset(), |
|
331 simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1); |
|
332 qed "div_mult2_eq"; |
|
333 |
|
334 Goal "(0::nat) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; |
|
335 by (div_undefined_case_tac "b = 0" 1); |
|
336 by (force_tac (claset(), |
|
337 simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod]) 1); |
|
338 qed "mod_mult2_eq"; |
|
339 |
|
340 |
|
341 (*** Cancellation of common factors in "div" ***) |
|
342 |
|
343 Goal "[| (0::nat) < b; 0 < c |] ==> (c*a) div (c*b) = a div b"; |
|
344 by (stac div_mult2_eq 1); |
|
345 by Auto_tac; |
|
346 val lemma1 = result(); |
|
347 |
|
348 Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b"; |
|
349 by (div_undefined_case_tac "b = 0" 1); |
|
350 by (auto_tac |
|
351 (claset(), |
|
352 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
|
353 lemma1, lemma2])); |
|
354 qed "div_mult_mult1"; |
|
355 |
|
356 Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b"; |
|
357 by (dtac div_mult_mult1 1); |
|
358 by (auto_tac (claset(), simpset() addsimps [mult_commute])); |
|
359 qed "div_mult_mult2"; |
|
360 |
|
361 Addsimps [div_mult_mult1, div_mult_mult2]; |
|
362 |
|
363 |
|
364 (*** Distribution of factors over "mod" |
|
365 |
|
366 Could prove these as in Integ/IntDiv.ML, but we already have |
|
367 mod_mult_distrib and mod_mult_distrib2 above! |
|
368 |
|
369 Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"; |
|
370 qed "mod_mult_mult1"; |
|
371 |
|
372 Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)"; |
|
373 qed "mod_mult_mult2"; |
|
374 ***) |
|
375 |
|
376 (*** Further facts about div and mod ***) |
|
377 |
175 Goal "m div 1 = m"; |
378 Goal "m div 1 = m"; |
176 by (induct_tac "m" 1); |
379 by (induct_tac "m" 1); |
177 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); |
380 by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); |
178 qed "div_1"; |
381 qed "div_1"; |
179 Addsimps [div_1]; |
382 Addsimps [div_1]; |
180 |
383 |
181 Goal "0<n ==> n div n = (1::nat)"; |
384 Goal "0<n ==> n div n = (1::nat)"; |
182 by (asm_simp_tac (simpset() addsimps [div_geq]) 1); |
385 by (asm_simp_tac (simpset() addsimps [div_geq]) 1); |
183 qed "div_self"; |
386 qed "div_self"; |
184 |
387 Addsimps [div_self]; |
185 |
388 |
186 Goal "0<n ==> (m+n) div n = Suc (m div n)"; |
389 Goal "0<n ==> (m+n) div n = Suc (m div n)"; |
187 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1); |
390 by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1); |
188 by (stac (div_geq RS sym) 2); |
391 by (stac (div_geq RS sym) 2); |
189 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
392 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); |
294 mod_geq]) 1); |
498 mod_geq]) 1); |
295 by (auto_tac (claset(), |
499 by (auto_tac (claset(), |
296 simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq])); |
500 simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq])); |
297 qed "mod_Suc"; |
501 qed "mod_Suc"; |
298 |
502 |
299 Goal "0<n ==> m mod n < (n::nat)"; |
|
300 by (induct_thm_tac nat_less_induct "m" 1); |
|
301 by (case_tac "na<n" 1); |
|
302 (*case n le na*) |
|
303 by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2); |
|
304 (*case na<n*) |
|
305 by (Asm_simp_tac 1); |
|
306 qed "mod_less_divisor"; |
|
307 Addsimps [mod_less_divisor]; |
|
308 |
|
309 (*** More division laws ***) |
|
310 |
|
311 Goal "0<n ==> (m*n) div n = (m::nat)"; |
|
312 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1); |
|
313 by Auto_tac; |
|
314 qed "div_mult_self_is_m"; |
|
315 |
|
316 Goal "0<n ==> (n*m) div n = (m::nat)"; |
|
317 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1); |
|
318 qed "div_mult_self1_is_m"; |
|
319 Addsimps [div_mult_self_is_m, div_mult_self1_is_m]; |
|
320 |
|
321 (*Cancellation law for division*) |
|
322 Goal "0<k ==> (k*m) div (k*n) = m div (n::nat)"; |
|
323 by (div_undefined_case_tac "n=0" 1); |
|
324 by (induct_thm_tac nat_less_induct "m" 1); |
|
325 by (case_tac "na<n" 1); |
|
326 by (asm_simp_tac (simpset() addsimps [zero_less_mult_iff, mult_less_mono2]) 1); |
|
327 by (subgoal_tac "~ k*na < k*n" 1); |
|
328 by (asm_simp_tac |
|
329 (simpset() addsimps [zero_less_mult_iff, div_geq, |
|
330 diff_mult_distrib2 RS sym, diff_less]) 1); |
|
331 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, |
|
332 le_refl RS mult_le_mono]) 1); |
|
333 qed "div_cancel"; |
|
334 Addsimps [div_cancel]; |
|
335 |
|
336 (*mod_mult_distrib2 above is the counterpart for remainder*) |
|
337 |
|
338 |
503 |
339 (************************************************) |
504 (************************************************) |
340 (** Divides Relation **) |
505 (** Divides Relation **) |
341 (************************************************) |
506 (************************************************) |
342 |
507 |