32 |
32 |
33 Addsimps [zless_nat_conj]; |
33 Addsimps [zless_nat_conj]; |
34 |
34 |
35 (*** Uniqueness and monotonicity of quotients and remainders ***) |
35 (*** Uniqueness and monotonicity of quotients and remainders ***) |
36 |
36 |
37 Goal "[| b*q' + r' <= b*q + r; #0 <= r'; #0 < b; r < b |] \ |
37 Goal "[| b*q' + r' <= b*q + r; Numeral0 <= r'; Numeral0 < b; r < b |] \ |
38 \ ==> q' <= (q::int)"; |
38 \ ==> q' <= (q::int)"; |
39 by (subgoal_tac "r' + b * (q'-q) <= r" 1); |
39 by (subgoal_tac "r' + b * (q'-q) <= r" 1); |
40 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
40 by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
41 by (subgoal_tac "#0 < b * (#1 + q - q')" 1); |
41 by (subgoal_tac "Numeral0 < b * (Numeral1 + q - q')" 1); |
42 by (etac order_le_less_trans 2); |
42 by (etac order_le_less_trans 2); |
43 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
43 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
44 zadd_zmult_distrib2]) 2); |
44 zadd_zmult_distrib2]) 2); |
45 by (subgoal_tac "b * q' < b * (#1 + q)" 1); |
45 by (subgoal_tac "b * q' < b * (Numeral1 + q)" 1); |
46 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
46 by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, |
47 zadd_zmult_distrib2]) 2); |
47 zadd_zmult_distrib2]) 2); |
48 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
48 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
49 qed "unique_quotient_lemma"; |
49 qed "unique_quotient_lemma"; |
50 |
50 |
51 Goal "[| b*q' + r' <= b*q + r; r <= #0; b < #0; b < r' |] \ |
51 Goal "[| b*q' + r' <= b*q + r; r <= Numeral0; b < Numeral0; b < r' |] \ |
52 \ ==> q <= (q'::int)"; |
52 \ ==> q <= (q'::int)"; |
53 by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] |
53 by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] |
54 unique_quotient_lemma 1); |
54 unique_quotient_lemma 1); |
55 by (auto_tac (claset(), |
55 by (auto_tac (claset(), |
56 simpset() addsimps [zmult_zminus, zmult_zminus_right])); |
56 simpset() addsimps [zmult_zminus, zmult_zminus_right])); |
57 qed "unique_quotient_lemma_neg"; |
57 qed "unique_quotient_lemma_neg"; |
58 |
58 |
59 |
59 |
60 Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= #0 |] \ |
60 Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= Numeral0 |] \ |
61 \ ==> q = q'"; |
61 \ ==> q = q'"; |
62 by (asm_full_simp_tac |
62 by (asm_full_simp_tac |
63 (simpset() addsimps split_ifs@ |
63 (simpset() addsimps split_ifs@ |
64 [quorem_def, linorder_neq_iff]) 1); |
64 [quorem_def, linorder_neq_iff]) 1); |
65 by Safe_tac; |
65 by Safe_tac; |
220 DIVISION_BY_ZERO_ZMOD]) i; |
220 DIVISION_BY_ZERO_ZMOD]) i; |
221 |
221 |
222 (** Basic laws about division and remainder **) |
222 (** Basic laws about division and remainder **) |
223 |
223 |
224 Goal "(a::int) = b * (a div b) + (a mod b)"; |
224 Goal "(a::int) = b * (a div b) + (a mod b)"; |
225 by (zdiv_undefined_case_tac "b = #0" 1); |
225 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
226 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
226 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
227 by (auto_tac (claset(), |
227 by (auto_tac (claset(), |
228 simpset() addsimps [quorem_def, div_def, mod_def])); |
228 simpset() addsimps [quorem_def, div_def, mod_def])); |
229 qed "zmod_zdiv_equality"; |
229 qed "zmod_zdiv_equality"; |
230 |
230 |
231 Goal "(#0::int) < b ==> #0 <= a mod b & a mod b < b"; |
231 Goal "(Numeral0::int) < b ==> Numeral0 <= a mod b & a mod b < b"; |
232 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
232 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
233 by (auto_tac (claset(), |
233 by (auto_tac (claset(), |
234 simpset() addsimps [quorem_def, mod_def])); |
234 simpset() addsimps [quorem_def, mod_def])); |
235 bind_thm ("pos_mod_sign", result() RS conjunct1); |
235 bind_thm ("pos_mod_sign", result() RS conjunct1); |
236 bind_thm ("pos_mod_bound", result() RS conjunct2); |
236 bind_thm ("pos_mod_bound", result() RS conjunct2); |
237 |
237 |
238 Goal "b < (#0::int) ==> a mod b <= #0 & b < a mod b"; |
238 Goal "b < (Numeral0::int) ==> a mod b <= Numeral0 & b < a mod b"; |
239 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
239 by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
240 by (auto_tac (claset(), |
240 by (auto_tac (claset(), |
241 simpset() addsimps [quorem_def, div_def, mod_def])); |
241 simpset() addsimps [quorem_def, div_def, mod_def])); |
242 bind_thm ("neg_mod_sign", result() RS conjunct1); |
242 bind_thm ("neg_mod_sign", result() RS conjunct1); |
243 bind_thm ("neg_mod_bound", result() RS conjunct2); |
243 bind_thm ("neg_mod_bound", result() RS conjunct2); |
244 |
244 |
245 |
245 |
246 (** proving general properties of div and mod **) |
246 (** proving general properties of div and mod **) |
247 |
247 |
248 Goal "b ~= #0 ==> quorem ((a, b), (a div b, a mod b))"; |
248 Goal "b ~= Numeral0 ==> quorem ((a, b), (a div b, a mod b))"; |
249 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
249 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
250 by (auto_tac |
250 by (auto_tac |
251 (claset(), |
251 (claset(), |
252 simpset() addsimps [quorem_def, linorder_neq_iff, |
252 simpset() addsimps [quorem_def, linorder_neq_iff, |
253 pos_mod_sign,pos_mod_bound, |
253 pos_mod_sign,pos_mod_bound, |
254 neg_mod_sign, neg_mod_bound])); |
254 neg_mod_sign, neg_mod_bound])); |
255 qed "quorem_div_mod"; |
255 qed "quorem_div_mod"; |
256 |
256 |
257 Goal "[| quorem((a,b),(q,r)); b ~= #0 |] ==> a div b = q"; |
257 Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a div b = q"; |
258 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); |
258 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); |
259 qed "quorem_div"; |
259 qed "quorem_div"; |
260 |
260 |
261 Goal "[| quorem((a,b),(q,r)); b ~= #0 |] ==> a mod b = r"; |
261 Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a mod b = r"; |
262 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); |
262 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); |
263 qed "quorem_mod"; |
263 qed "quorem_mod"; |
264 |
264 |
265 Goal "[| (#0::int) <= a; a < b |] ==> a div b = #0"; |
265 Goal "[| (Numeral0::int) <= a; a < b |] ==> a div b = Numeral0"; |
266 by (rtac quorem_div 1); |
266 by (rtac quorem_div 1); |
267 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
267 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
268 qed "div_pos_pos_trivial"; |
268 qed "div_pos_pos_trivial"; |
269 |
269 |
270 Goal "[| a <= (#0::int); b < a |] ==> a div b = #0"; |
270 Goal "[| a <= (Numeral0::int); b < a |] ==> a div b = Numeral0"; |
271 by (rtac quorem_div 1); |
271 by (rtac quorem_div 1); |
272 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
272 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
273 qed "div_neg_neg_trivial"; |
273 qed "div_neg_neg_trivial"; |
274 |
274 |
275 Goal "[| (#0::int) < a; a+b <= #0 |] ==> a div b = #-1"; |
275 Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = # -1"; |
276 by (rtac quorem_div 1); |
276 by (rtac quorem_div 1); |
277 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
277 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
278 qed "div_pos_neg_trivial"; |
278 qed "div_pos_neg_trivial"; |
279 |
279 |
280 (*There is no div_neg_pos_trivial because #0 div b = #0 would supersede it*) |
280 (*There is no div_neg_pos_trivial because Numeral0 div b = Numeral0 would supersede it*) |
281 |
281 |
282 Goal "[| (#0::int) <= a; a < b |] ==> a mod b = a"; |
282 Goal "[| (Numeral0::int) <= a; a < b |] ==> a mod b = a"; |
283 by (res_inst_tac [("q","#0")] quorem_mod 1); |
283 by (res_inst_tac [("q","Numeral0")] quorem_mod 1); |
284 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
284 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
285 qed "mod_pos_pos_trivial"; |
285 qed "mod_pos_pos_trivial"; |
286 |
286 |
287 Goal "[| a <= (#0::int); b < a |] ==> a mod b = a"; |
287 Goal "[| a <= (Numeral0::int); b < a |] ==> a mod b = a"; |
288 by (res_inst_tac [("q","#0")] quorem_mod 1); |
288 by (res_inst_tac [("q","Numeral0")] quorem_mod 1); |
289 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
289 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
290 qed "mod_neg_neg_trivial"; |
290 qed "mod_neg_neg_trivial"; |
291 |
291 |
292 Goal "[| (#0::int) < a; a+b <= #0 |] ==> a mod b = a+b"; |
292 Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a mod b = a+b"; |
293 by (res_inst_tac [("q","#-1")] quorem_mod 1); |
293 by (res_inst_tac [("q","# -1")] quorem_mod 1); |
294 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
294 by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
295 qed "mod_pos_neg_trivial"; |
295 qed "mod_pos_neg_trivial"; |
296 |
296 |
297 (*There is no mod_neg_pos_trivial...*) |
297 (*There is no mod_neg_pos_trivial...*) |
298 |
298 |
299 |
299 |
300 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
300 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) |
301 Goal "(-a) div (-b) = a div (b::int)"; |
301 Goal "(-a) div (-b) = a div (b::int)"; |
302 by (zdiv_undefined_case_tac "b = #0" 1); |
302 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
303 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
303 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
304 RS quorem_div) 1); |
304 RS quorem_div) 1); |
305 by Auto_tac; |
305 by Auto_tac; |
306 qed "zdiv_zminus_zminus"; |
306 qed "zdiv_zminus_zminus"; |
307 Addsimps [zdiv_zminus_zminus]; |
307 Addsimps [zdiv_zminus_zminus]; |
308 |
308 |
309 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
309 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) |
310 Goal "(-a) mod (-b) = - (a mod (b::int))"; |
310 Goal "(-a) mod (-b) = - (a mod (b::int))"; |
311 by (zdiv_undefined_case_tac "b = #0" 1); |
311 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
312 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
312 by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
313 RS quorem_mod) 1); |
313 RS quorem_mod) 1); |
314 by Auto_tac; |
314 by Auto_tac; |
315 qed "zmod_zminus_zminus"; |
315 qed "zmod_zminus_zminus"; |
316 Addsimps [zmod_zminus_zminus]; |
316 Addsimps [zmod_zminus_zminus]; |
317 |
317 |
318 |
318 |
319 (*** div, mod and unary minus ***) |
319 (*** div, mod and unary minus ***) |
320 |
320 |
321 Goal "quorem((a,b),(q,r)) \ |
321 Goal "quorem((a,b),(q,r)) \ |
322 \ ==> quorem ((-a,b), (if r=#0 then -q else -q-#1), \ |
322 \ ==> quorem ((-a,b), (if r=Numeral0 then -q else -q-Numeral1), \ |
323 \ (if r=#0 then #0 else b-r))"; |
323 \ (if r=Numeral0 then Numeral0 else b-r))"; |
324 by (auto_tac |
324 by (auto_tac |
325 (claset(), |
325 (claset(), |
326 simpset() addsimps split_ifs@ |
326 simpset() addsimps split_ifs@ |
327 [quorem_def, linorder_neq_iff, |
327 [quorem_def, linorder_neq_iff, |
328 zdiff_zmult_distrib2])); |
328 zdiff_zmult_distrib2])); |
329 val lemma = result(); |
329 val lemma = result(); |
330 |
330 |
331 Goal "b ~= (#0::int) \ |
331 Goal "b ~= (Numeral0::int) \ |
332 \ ==> (-a) div b = \ |
332 \ ==> (-a) div b = \ |
333 \ (if a mod b = #0 then - (a div b) else - (a div b) - #1)"; |
333 \ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; |
334 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
334 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
335 qed "zdiv_zminus1_eq_if"; |
335 qed "zdiv_zminus1_eq_if"; |
336 |
336 |
337 Goal "(-a::int) mod b = (if a mod b = #0 then #0 else b - (a mod b))"; |
337 Goal "(-a::int) mod b = (if a mod b = Numeral0 then Numeral0 else b - (a mod b))"; |
338 by (zdiv_undefined_case_tac "b = #0" 1); |
338 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
339 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
339 by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
340 qed "zmod_zminus1_eq_if"; |
340 qed "zmod_zminus1_eq_if"; |
341 |
341 |
342 Goal "a div (-b) = (-a::int) div b"; |
342 Goal "a div (-b) = (-a::int) div b"; |
343 by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1); |
343 by (cut_inst_tac [("a","-a")] zdiv_zminus_zminus 1); |
347 Goal "a mod (-b) = - ((-a::int) mod b)"; |
347 Goal "a mod (-b) = - ((-a::int) mod b)"; |
348 by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1); |
348 by (cut_inst_tac [("a","-a"),("b","b")] zmod_zminus_zminus 1); |
349 by Auto_tac; |
349 by Auto_tac; |
350 qed "zmod_zminus2"; |
350 qed "zmod_zminus2"; |
351 |
351 |
352 Goal "b ~= (#0::int) \ |
352 Goal "b ~= (Numeral0::int) \ |
353 \ ==> a div (-b) = \ |
353 \ ==> a div (-b) = \ |
354 \ (if a mod b = #0 then - (a div b) else - (a div b) - #1)"; |
354 \ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; |
355 by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); |
355 by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); |
356 qed "zdiv_zminus2_eq_if"; |
356 qed "zdiv_zminus2_eq_if"; |
357 |
357 |
358 Goal "a mod (-b::int) = (if a mod b = #0 then #0 else (a mod b) - b)"; |
358 Goal "a mod (-b::int) = (if a mod b = Numeral0 then Numeral0 else (a mod b) - b)"; |
359 by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); |
359 by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); |
360 qed "zmod_zminus2_eq_if"; |
360 qed "zmod_zminus2_eq_if"; |
361 |
361 |
362 |
362 |
363 (*** division of a number by itself ***) |
363 (*** division of a number by itself ***) |
364 |
364 |
365 Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q"; |
365 Goal "[| (Numeral0::int) < a; a = r + a*q; r < a |] ==> Numeral1 <= q"; |
366 by (subgoal_tac "#0 < a*q" 1); |
366 by (subgoal_tac "Numeral0 < a*q" 1); |
367 by (arith_tac 2); |
367 by (arith_tac 2); |
368 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
368 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
369 val lemma1 = result(); |
369 val lemma1 = result(); |
370 |
370 |
371 Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1"; |
371 Goal "[| (Numeral0::int) < a; a = r + a*q; Numeral0 <= r |] ==> q <= Numeral1"; |
372 by (subgoal_tac "#0 <= a*(#1-q)" 1); |
372 by (subgoal_tac "Numeral0 <= a*(Numeral1-q)" 1); |
373 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
373 by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
374 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
374 by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
375 val lemma2 = result(); |
375 val lemma2 = result(); |
376 |
376 |
377 Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> q = #1"; |
377 Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> q = Numeral1"; |
378 by (asm_full_simp_tac |
378 by (asm_full_simp_tac |
379 (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1); |
379 (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1); |
380 by (rtac order_antisym 1); |
380 by (rtac order_antisym 1); |
381 by Safe_tac; |
381 by Safe_tac; |
382 by Auto_tac; |
382 by Auto_tac; |
384 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1); |
384 by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1); |
385 by (REPEAT (force_tac (claset() addIs [lemma1,lemma2], |
385 by (REPEAT (force_tac (claset() addIs [lemma1,lemma2], |
386 simpset() addsimps [zadd_commute, zmult_zminus]) 1)); |
386 simpset() addsimps [zadd_commute, zmult_zminus]) 1)); |
387 qed "self_quotient"; |
387 qed "self_quotient"; |
388 |
388 |
389 Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> r = #0"; |
389 Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> r = Numeral0"; |
390 by (ftac self_quotient 1); |
390 by (ftac self_quotient 1); |
391 by (assume_tac 1); |
391 by (assume_tac 1); |
392 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); |
392 by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); |
393 qed "self_remainder"; |
393 qed "self_remainder"; |
394 |
394 |
395 Goal "a ~= #0 ==> a div a = (#1::int)"; |
395 Goal "a ~= Numeral0 ==> a div a = (Numeral1::int)"; |
396 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); |
396 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); |
397 qed "zdiv_self"; |
397 qed "zdiv_self"; |
398 Addsimps [zdiv_self]; |
398 Addsimps [zdiv_self]; |
399 |
399 |
400 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
400 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
401 Goal "a mod a = (#0::int)"; |
401 Goal "a mod a = (Numeral0::int)"; |
402 by (zdiv_undefined_case_tac "a = #0" 1); |
402 by (zdiv_undefined_case_tac "a = Numeral0" 1); |
403 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); |
403 by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); |
404 qed "zmod_self"; |
404 qed "zmod_self"; |
405 Addsimps [zmod_self]; |
405 Addsimps [zmod_self]; |
406 |
406 |
407 |
407 |
408 (*** Computation of division and remainder ***) |
408 (*** Computation of division and remainder ***) |
409 |
409 |
410 Goal "(#0::int) div b = #0"; |
410 Goal "(Numeral0::int) div b = Numeral0"; |
411 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
411 by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
412 qed "zdiv_zero"; |
412 qed "zdiv_zero"; |
413 |
413 |
414 Goal "(#0::int) < b ==> #-1 div b = #-1"; |
414 Goal "(Numeral0::int) < b ==> # -1 div b = # -1"; |
415 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
415 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
416 qed "div_eq_minus1"; |
416 qed "div_eq_minus1"; |
417 |
417 |
418 Goal "(#0::int) mod b = #0"; |
418 Goal "(Numeral0::int) mod b = Numeral0"; |
419 by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
419 by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
420 qed "zmod_zero"; |
420 qed "zmod_zero"; |
421 |
421 |
422 Addsimps [zdiv_zero, zmod_zero]; |
422 Addsimps [zdiv_zero, zmod_zero]; |
423 |
423 |
424 Goal "(#0::int) < b ==> #-1 div b = #-1"; |
424 Goal "(Numeral0::int) < b ==> # -1 div b = # -1"; |
425 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
425 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
426 qed "zdiv_minus1"; |
426 qed "zdiv_minus1"; |
427 |
427 |
428 Goal "(#0::int) < b ==> #-1 mod b = b-#1"; |
428 Goal "(Numeral0::int) < b ==> # -1 mod b = b-Numeral1"; |
429 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
429 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
430 qed "zmod_minus1"; |
430 qed "zmod_minus1"; |
431 |
431 |
432 (** a positive, b positive **) |
432 (** a positive, b positive **) |
433 |
433 |
434 Goal "[| #0 < a; #0 <= b |] ==> a div b = fst (posDivAlg(a,b))"; |
434 Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a div b = fst (posDivAlg(a,b))"; |
435 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
435 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
436 qed "div_pos_pos"; |
436 qed "div_pos_pos"; |
437 |
437 |
438 Goal "[| #0 < a; #0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"; |
438 Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"; |
439 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
439 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
440 qed "mod_pos_pos"; |
440 qed "mod_pos_pos"; |
441 |
441 |
442 (** a negative, b positive **) |
442 (** a negative, b positive **) |
443 |
443 |
444 Goal "[| a < #0; #0 < b |] ==> a div b = fst (negDivAlg(a,b))"; |
444 Goal "[| a < Numeral0; Numeral0 < b |] ==> a div b = fst (negDivAlg(a,b))"; |
445 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
445 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
446 qed "div_neg_pos"; |
446 qed "div_neg_pos"; |
447 |
447 |
448 Goal "[| a < #0; #0 < b |] ==> a mod b = snd (negDivAlg(a,b))"; |
448 Goal "[| a < Numeral0; Numeral0 < b |] ==> a mod b = snd (negDivAlg(a,b))"; |
449 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
449 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
450 qed "mod_neg_pos"; |
450 qed "mod_neg_pos"; |
451 |
451 |
452 (** a positive, b negative **) |
452 (** a positive, b negative **) |
453 |
453 |
454 Goal "[| #0 < a; b < #0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"; |
454 Goal "[| Numeral0 < a; b < Numeral0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"; |
455 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
455 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
456 qed "div_pos_neg"; |
456 qed "div_pos_neg"; |
457 |
457 |
458 Goal "[| #0 < a; b < #0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"; |
458 Goal "[| Numeral0 < a; b < Numeral0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"; |
459 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
459 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
460 qed "mod_pos_neg"; |
460 qed "mod_pos_neg"; |
461 |
461 |
462 (** a negative, b negative **) |
462 (** a negative, b negative **) |
463 |
463 |
464 Goal "[| a < #0; b <= #0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; |
464 Goal "[| a < Numeral0; b <= Numeral0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; |
465 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
465 by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
466 qed "div_neg_neg"; |
466 qed "div_neg_neg"; |
467 |
467 |
468 Goal "[| a < #0; b <= #0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"; |
468 Goal "[| a < Numeral0; b <= Numeral0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"; |
469 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
469 by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
470 qed "mod_neg_neg"; |
470 qed "mod_neg_neg"; |
471 |
471 |
472 Addsimps (map (read_instantiate_sg (sign_of (the_context ())) |
472 Addsimps (map (read_instantiate_sg (sign_of (the_context ())) |
473 [("a", "number_of ?v"), ("b", "number_of ?w")]) |
473 [("a", "number_of ?v"), ("b", "number_of ?w")]) |
476 posDivAlg_eqn, negDivAlg_eqn]); |
476 posDivAlg_eqn, negDivAlg_eqn]); |
477 |
477 |
478 |
478 |
479 (** Special-case simplification **) |
479 (** Special-case simplification **) |
480 |
480 |
481 Goal "a mod (#1::int) = #0"; |
481 Goal "a mod (Numeral1::int) = Numeral0"; |
482 by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1); |
482 by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_sign 1); |
483 by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2); |
483 by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_bound 2); |
484 by Auto_tac; |
484 by Auto_tac; |
485 qed "zmod_1"; |
485 qed "zmod_1"; |
486 Addsimps [zmod_1]; |
486 Addsimps [zmod_1]; |
487 |
487 |
488 Goal "a div (#1::int) = a"; |
488 Goal "a div (Numeral1::int) = a"; |
489 by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1); |
489 by (cut_inst_tac [("a","a"),("b","Numeral1")] zmod_zdiv_equality 1); |
490 by Auto_tac; |
490 by Auto_tac; |
491 qed "zdiv_1"; |
491 qed "zdiv_1"; |
492 Addsimps [zdiv_1]; |
492 Addsimps [zdiv_1]; |
493 |
493 |
494 Goal "a mod (#-1::int) = #0"; |
494 Goal "a mod (# -1::int) = Numeral0"; |
495 by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1); |
495 by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_sign 1); |
496 by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2); |
496 by (cut_inst_tac [("a","a"),("b","# -1")] neg_mod_bound 2); |
497 by Auto_tac; |
497 by Auto_tac; |
498 qed "zmod_minus1_right"; |
498 qed "zmod_minus1_right"; |
499 Addsimps [zmod_minus1_right]; |
499 Addsimps [zmod_minus1_right]; |
500 |
500 |
501 Goal "a div (#-1::int) = -a"; |
501 Goal "a div (# -1::int) = -a"; |
502 by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1); |
502 by (cut_inst_tac [("a","a"),("b","# -1")] zmod_zdiv_equality 1); |
503 by Auto_tac; |
503 by Auto_tac; |
504 qed "zdiv_minus1_right"; |
504 qed "zdiv_minus1_right"; |
505 Addsimps [zdiv_minus1_right]; |
505 Addsimps [zdiv_minus1_right]; |
506 |
506 |
507 |
507 |
508 (*** Monotonicity in the first argument (divisor) ***) |
508 (*** Monotonicity in the first argument (divisor) ***) |
509 |
509 |
510 Goal "[| a <= a'; #0 < (b::int) |] ==> a div b <= a' div b"; |
510 Goal "[| a <= a'; Numeral0 < (b::int) |] ==> a div b <= a' div b"; |
511 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
511 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
512 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
512 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
513 by (rtac unique_quotient_lemma 1); |
513 by (rtac unique_quotient_lemma 1); |
514 by (etac subst 1); |
514 by (etac subst 1); |
515 by (etac subst 1); |
515 by (etac subst 1); |
516 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
516 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
517 qed "zdiv_mono1"; |
517 qed "zdiv_mono1"; |
518 |
518 |
519 Goal "[| a <= a'; (b::int) < #0 |] ==> a' div b <= a div b"; |
519 Goal "[| a <= a'; (b::int) < Numeral0 |] ==> a' div b <= a div b"; |
520 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
520 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
521 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
521 by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
522 by (rtac unique_quotient_lemma_neg 1); |
522 by (rtac unique_quotient_lemma_neg 1); |
523 by (etac subst 1); |
523 by (etac subst 1); |
524 by (etac subst 1); |
524 by (etac subst 1); |
526 qed "zdiv_mono1_neg"; |
526 qed "zdiv_mono1_neg"; |
527 |
527 |
528 |
528 |
529 (*** Monotonicity in the second argument (dividend) ***) |
529 (*** Monotonicity in the second argument (dividend) ***) |
530 |
530 |
531 Goal "[| b*q + r = b'*q' + r'; #0 <= b'*q' + r'; \ |
531 Goal "[| b*q + r = b'*q' + r'; Numeral0 <= b'*q' + r'; \ |
532 \ r' < b'; #0 <= r; #0 < b'; b' <= b |] \ |
532 \ r' < b'; Numeral0 <= r; Numeral0 < b'; b' <= b |] \ |
533 \ ==> q <= (q'::int)"; |
533 \ ==> q <= (q'::int)"; |
534 by (subgoal_tac "#0 <= q'" 1); |
534 by (subgoal_tac "Numeral0 <= q'" 1); |
535 by (subgoal_tac "#0 < b'*(q' + #1)" 2); |
535 by (subgoal_tac "Numeral0 < b'*(q' + Numeral1)" 2); |
536 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3); |
536 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3); |
537 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2); |
537 by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2); |
538 by (subgoal_tac "b*q < b*(q' + #1)" 1); |
538 by (subgoal_tac "b*q < b*(q' + Numeral1)" 1); |
539 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
539 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
540 by (subgoal_tac "b*q = r' - r + b'*q'" 1); |
540 by (subgoal_tac "b*q = r' - r + b'*q'" 1); |
541 by (Simp_tac 2); |
541 by (Simp_tac 2); |
542 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
542 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
543 by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1); |
543 by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1); |
544 by (rtac zmult_zle_mono1 1); |
544 by (rtac zmult_zle_mono1 1); |
545 by Auto_tac; |
545 by Auto_tac; |
546 qed "zdiv_mono2_lemma"; |
546 qed "zdiv_mono2_lemma"; |
547 |
547 |
548 Goal "[| (#0::int) <= a; #0 < b'; b' <= b |] \ |
548 Goal "[| (Numeral0::int) <= a; Numeral0 < b'; b' <= b |] \ |
549 \ ==> a div b <= a div b'"; |
549 \ ==> a div b <= a div b'"; |
550 by (subgoal_tac "b ~= #0" 1); |
550 by (subgoal_tac "b ~= Numeral0" 1); |
551 by (arith_tac 2); |
551 by (arith_tac 2); |
552 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
552 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
553 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
553 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
554 by (rtac zdiv_mono2_lemma 1); |
554 by (rtac zdiv_mono2_lemma 1); |
555 by (etac subst 1); |
555 by (etac subst 1); |
556 by (etac subst 1); |
556 by (etac subst 1); |
557 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
557 by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
558 qed "zdiv_mono2"; |
558 qed "zdiv_mono2"; |
559 |
559 |
560 Goal "[| b*q + r = b'*q' + r'; b'*q' + r' < #0; \ |
560 Goal "[| b*q + r = b'*q' + r'; b'*q' + r' < Numeral0; \ |
561 \ r < b; #0 <= r'; #0 < b'; b' <= b |] \ |
561 \ r < b; Numeral0 <= r'; Numeral0 < b'; b' <= b |] \ |
562 \ ==> q' <= (q::int)"; |
562 \ ==> q' <= (q::int)"; |
563 by (subgoal_tac "q' < #0" 1); |
563 by (subgoal_tac "q' < Numeral0" 1); |
564 by (subgoal_tac "b'*q' < #0" 2); |
564 by (subgoal_tac "b'*q' < Numeral0" 2); |
565 by (arith_tac 3); |
565 by (arith_tac 3); |
566 by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2); |
566 by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2); |
567 by (subgoal_tac "b*q' < b*(q + #1)" 1); |
567 by (subgoal_tac "b*q' < b*(q + Numeral1)" 1); |
568 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
568 by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); |
569 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
569 by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
570 by (subgoal_tac "b*q' <= b'*q'" 1); |
570 by (subgoal_tac "b*q' <= b'*q'" 1); |
571 by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2); |
571 by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2); |
572 by (subgoal_tac "b'*q' < b + b*q" 1); |
572 by (subgoal_tac "b'*q' < b + b*q" 1); |
573 by (Asm_simp_tac 2); |
573 by (Asm_simp_tac 2); |
574 by (arith_tac 1); |
574 by (arith_tac 1); |
575 qed "zdiv_mono2_neg_lemma"; |
575 qed "zdiv_mono2_neg_lemma"; |
576 |
576 |
577 Goal "[| a < (#0::int); #0 < b'; b' <= b |] \ |
577 Goal "[| a < (Numeral0::int); Numeral0 < b'; b' <= b |] \ |
578 \ ==> a div b' <= a div b"; |
578 \ ==> a div b' <= a div b"; |
579 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
579 by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
580 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
580 by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
581 by (rtac zdiv_mono2_neg_lemma 1); |
581 by (rtac zdiv_mono2_neg_lemma 1); |
582 by (etac subst 1); |
582 by (etac subst 1); |
621 Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"; |
621 Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"; |
622 by (rtac (zmod_zmult1_eq' RS trans) 1); |
622 by (rtac (zmod_zmult1_eq' RS trans) 1); |
623 by (rtac zmod_zmult1_eq 1); |
623 by (rtac zmod_zmult1_eq 1); |
624 qed "zmod_zmult_distrib"; |
624 qed "zmod_zmult_distrib"; |
625 |
625 |
626 Goal "b ~= (#0::int) ==> (a*b) div b = a"; |
626 Goal "b ~= (Numeral0::int) ==> (a*b) div b = a"; |
627 by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); |
627 by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); |
628 qed "zdiv_zmult_self1"; |
628 qed "zdiv_zmult_self1"; |
629 |
629 |
630 Goal "b ~= (#0::int) ==> (b*a) div b = a"; |
630 Goal "b ~= (Numeral0::int) ==> (b*a) div b = a"; |
631 by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1); |
631 by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1); |
632 qed "zdiv_zmult_self2"; |
632 qed "zdiv_zmult_self2"; |
633 |
633 |
634 Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; |
634 Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; |
635 |
635 |
636 Goal "(a*b) mod b = (#0::int)"; |
636 Goal "(a*b) mod b = (Numeral0::int)"; |
637 by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); |
637 by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); |
638 qed "zmod_zmult_self1"; |
638 qed "zmod_zmult_self1"; |
639 |
639 |
640 Goal "(b*a) mod b = (#0::int)"; |
640 Goal "(b*a) mod b = (Numeral0::int)"; |
641 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
641 by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
642 qed "zmod_zmult_self2"; |
642 qed "zmod_zmult_self2"; |
643 |
643 |
644 Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
644 Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
645 |
645 |
646 Goal "(m mod d = #0) = (EX q::int. m = d*q)"; |
646 Goal "(m mod d = Numeral0) = (EX q::int. m = d*q)"; |
647 by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1); |
647 by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1); |
648 by Auto_tac; |
648 by Auto_tac; |
649 qed "zmod_eq_0_iff"; |
649 qed "zmod_eq_0_iff"; |
650 AddSDs [zmod_eq_0_iff RS iffD1]; |
650 AddSDs [zmod_eq_0_iff RS iffD1]; |
651 |
651 |
652 |
652 |
653 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
653 (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) |
654 |
654 |
655 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= #0 |] \ |
655 Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= Numeral0 |] \ |
656 \ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; |
656 \ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; |
657 by (auto_tac |
657 by (auto_tac |
658 (claset(), |
658 (claset(), |
659 simpset() addsimps split_ifs@ |
659 simpset() addsimps split_ifs@ |
660 [quorem_def, linorder_neq_iff, |
660 [quorem_def, linorder_neq_iff, |
664 by (ALLGOALS(rtac zmod_zdiv_equality)); |
664 by (ALLGOALS(rtac zmod_zdiv_equality)); |
665 val lemma = result(); |
665 val lemma = result(); |
666 |
666 |
667 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
667 (*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
668 Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"; |
668 Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"; |
669 by (zdiv_undefined_case_tac "c = #0" 1); |
669 by (zdiv_undefined_case_tac "c = Numeral0" 1); |
670 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
670 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
671 MRS lemma RS quorem_div]) 1); |
671 MRS lemma RS quorem_div]) 1); |
672 qed "zdiv_zadd1_eq"; |
672 qed "zdiv_zadd1_eq"; |
673 |
673 |
674 Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c"; |
674 Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c"; |
675 by (zdiv_undefined_case_tac "c = #0" 1); |
675 by (zdiv_undefined_case_tac "c = Numeral0" 1); |
676 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
676 by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
677 MRS lemma RS quorem_mod]) 1); |
677 MRS lemma RS quorem_mod]) 1); |
678 qed "zmod_zadd1_eq"; |
678 qed "zmod_zadd1_eq"; |
679 |
679 |
680 Goal "(a mod b) div b = (#0::int)"; |
680 Goal "(a mod b) div b = (Numeral0::int)"; |
681 by (zdiv_undefined_case_tac "b = #0" 1); |
681 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
682 by (auto_tac (claset(), |
682 by (auto_tac (claset(), |
683 simpset() addsimps [linorder_neq_iff, |
683 simpset() addsimps [linorder_neq_iff, |
684 pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, |
684 pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, |
685 neg_mod_sign, neg_mod_bound, div_neg_neg_trivial])); |
685 neg_mod_sign, neg_mod_bound, div_neg_neg_trivial])); |
686 qed "mod_div_trivial"; |
686 qed "mod_div_trivial"; |
687 Addsimps [mod_div_trivial]; |
687 Addsimps [mod_div_trivial]; |
688 |
688 |
689 Goal "(a mod b) mod b = a mod (b::int)"; |
689 Goal "(a mod b) mod b = a mod (b::int)"; |
690 by (zdiv_undefined_case_tac "b = #0" 1); |
690 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
691 by (auto_tac (claset(), |
691 by (auto_tac (claset(), |
692 simpset() addsimps [linorder_neq_iff, |
692 simpset() addsimps [linorder_neq_iff, |
693 pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, |
693 pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, |
694 neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial])); |
694 neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial])); |
695 qed "mod_mod_trivial"; |
695 qed "mod_mod_trivial"; |
737 7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
737 7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
738 to cause particular problems.*) |
738 to cause particular problems.*) |
739 |
739 |
740 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
740 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
741 |
741 |
742 Goal "[| (#0::int) < c; b < r; r <= #0 |] ==> b*c < b*(q mod c) + r"; |
742 Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b*c < b*(q mod c) + r"; |
743 by (subgoal_tac "b * (c - q mod c) < r * #1" 1); |
743 by (subgoal_tac "b * (c - q mod c) < r * Numeral1" 1); |
744 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
744 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
745 by (rtac order_le_less_trans 1); |
745 by (rtac order_le_less_trans 1); |
746 by (etac zmult_zless_mono1 2); |
746 by (etac zmult_zless_mono1 2); |
747 by (rtac zmult_zle_mono2_neg 1); |
747 by (rtac zmult_zle_mono2_neg 1); |
748 by (auto_tac |
748 by (auto_tac |
749 (claset(), |
749 (claset(), |
750 simpset() addsimps zcompare_rls@ |
750 simpset() addsimps zcompare_rls@ |
751 [zadd_commute, add1_zle_eq, pos_mod_bound])); |
751 [zadd_commute, add1_zle_eq, pos_mod_bound])); |
752 val lemma1 = result(); |
752 val lemma1 = result(); |
753 |
753 |
754 Goal "[| (#0::int) < c; b < r; r <= #0 |] ==> b * (q mod c) + r <= #0"; |
754 Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b * (q mod c) + r <= Numeral0"; |
755 by (subgoal_tac "b * (q mod c) <= #0" 1); |
755 by (subgoal_tac "b * (q mod c) <= Numeral0" 1); |
756 by (arith_tac 1); |
756 by (arith_tac 1); |
757 by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1); |
757 by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1); |
758 val lemma2 = result(); |
758 val lemma2 = result(); |
759 |
759 |
760 Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> #0 <= b * (q mod c) + r"; |
760 Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> Numeral0 <= b * (q mod c) + r"; |
761 by (subgoal_tac "#0 <= b * (q mod c)" 1); |
761 by (subgoal_tac "Numeral0 <= b * (q mod c)" 1); |
762 by (arith_tac 1); |
762 by (arith_tac 1); |
763 by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1); |
763 by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1); |
764 val lemma3 = result(); |
764 val lemma3 = result(); |
765 |
765 |
766 Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> b * (q mod c) + r < b * c"; |
766 Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> b * (q mod c) + r < b * c"; |
767 by (subgoal_tac "r * #1 < b * (c - q mod c)" 1); |
767 by (subgoal_tac "r * Numeral1 < b * (c - q mod c)" 1); |
768 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
768 by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
769 by (rtac order_less_le_trans 1); |
769 by (rtac order_less_le_trans 1); |
770 by (etac zmult_zless_mono1 1); |
770 by (etac zmult_zless_mono1 1); |
771 by (rtac zmult_zle_mono2 2); |
771 by (rtac zmult_zle_mono2 2); |
772 by (auto_tac |
772 by (auto_tac |
773 (claset(), |
773 (claset(), |
774 simpset() addsimps zcompare_rls@ |
774 simpset() addsimps zcompare_rls@ |
775 [zadd_commute, add1_zle_eq, pos_mod_bound])); |
775 [zadd_commute, add1_zle_eq, pos_mod_bound])); |
776 val lemma4 = result(); |
776 val lemma4 = result(); |
777 |
777 |
778 Goal "[| quorem ((a,b), (q,r)); b ~= #0; #0 < c |] \ |
778 Goal "[| quorem ((a,b), (q,r)); b ~= Numeral0; Numeral0 < c |] \ |
779 \ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; |
779 \ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; |
780 by (auto_tac |
780 by (auto_tac |
781 (claset(), |
781 (claset(), |
782 simpset() addsimps zmult_ac@ |
782 simpset() addsimps zmult_ac@ |
783 [zmod_zdiv_equality, quorem_def, linorder_neq_iff, |
783 [zmod_zdiv_equality, quorem_def, linorder_neq_iff, |
784 int_0_less_mult_iff, |
784 int_0_less_mult_iff, |
785 zadd_zmult_distrib2 RS sym, |
785 zadd_zmult_distrib2 RS sym, |
786 lemma1, lemma2, lemma3, lemma4])); |
786 lemma1, lemma2, lemma3, lemma4])); |
787 val lemma = result(); |
787 val lemma = result(); |
788 |
788 |
789 Goal "(#0::int) < c ==> a div (b*c) = (a div b) div c"; |
789 Goal "(Numeral0::int) < c ==> a div (b*c) = (a div b) div c"; |
790 by (zdiv_undefined_case_tac "b = #0" 1); |
790 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
791 by (force_tac (claset(), |
791 by (force_tac (claset(), |
792 simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, |
792 simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, |
793 zmult_eq_0_iff]) 1); |
793 zmult_eq_0_iff]) 1); |
794 qed "zdiv_zmult2_eq"; |
794 qed "zdiv_zmult2_eq"; |
795 |
795 |
796 Goal "(#0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; |
796 Goal "(Numeral0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; |
797 by (zdiv_undefined_case_tac "b = #0" 1); |
797 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
798 by (force_tac (claset(), |
798 by (force_tac (claset(), |
799 simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, |
799 simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, |
800 zmult_eq_0_iff]) 1); |
800 zmult_eq_0_iff]) 1); |
801 qed "zmod_zmult2_eq"; |
801 qed "zmod_zmult2_eq"; |
802 |
802 |
803 |
803 |
804 (*** Cancellation of common factors in "div" ***) |
804 (*** Cancellation of common factors in "div" ***) |
805 |
805 |
806 Goal "[| (#0::int) < b; c ~= #0 |] ==> (c*a) div (c*b) = a div b"; |
806 Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; |
807 by (stac zdiv_zmult2_eq 1); |
807 by (stac zdiv_zmult2_eq 1); |
808 by Auto_tac; |
808 by Auto_tac; |
809 val lemma1 = result(); |
809 val lemma1 = result(); |
810 |
810 |
811 Goal "[| b < (#0::int); c ~= #0 |] ==> (c*a) div (c*b) = a div b"; |
811 Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; |
812 by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1); |
812 by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1); |
813 by (rtac lemma1 2); |
813 by (rtac lemma1 2); |
814 by Auto_tac; |
814 by Auto_tac; |
815 val lemma2 = result(); |
815 val lemma2 = result(); |
816 |
816 |
817 Goal "c ~= (#0::int) ==> (c*a) div (c*b) = a div b"; |
817 Goal "c ~= (Numeral0::int) ==> (c*a) div (c*b) = a div b"; |
818 by (zdiv_undefined_case_tac "b = #0" 1); |
818 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
819 by (auto_tac |
819 by (auto_tac |
820 (claset(), |
820 (claset(), |
821 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
821 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
822 lemma1, lemma2])); |
822 lemma1, lemma2])); |
823 qed "zdiv_zmult_zmult1"; |
823 qed "zdiv_zmult_zmult1"; |
824 |
824 |
825 Goal "c ~= (#0::int) ==> (a*c) div (b*c) = a div b"; |
825 Goal "c ~= (Numeral0::int) ==> (a*c) div (b*c) = a div b"; |
826 by (dtac zdiv_zmult_zmult1 1); |
826 by (dtac zdiv_zmult_zmult1 1); |
827 by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
827 by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
828 qed "zdiv_zmult_zmult2"; |
828 qed "zdiv_zmult_zmult2"; |
829 |
829 |
830 |
830 |
831 |
831 |
832 (*** Distribution of factors over "mod" ***) |
832 (*** Distribution of factors over "mod" ***) |
833 |
833 |
834 Goal "[| (#0::int) < b; c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
834 Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
835 by (stac zmod_zmult2_eq 1); |
835 by (stac zmod_zmult2_eq 1); |
836 by Auto_tac; |
836 by Auto_tac; |
837 val lemma1 = result(); |
837 val lemma1 = result(); |
838 |
838 |
839 Goal "[| b < (#0::int); c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
839 Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; |
840 by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1); |
840 by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1); |
841 by (rtac lemma1 2); |
841 by (rtac lemma1 2); |
842 by Auto_tac; |
842 by Auto_tac; |
843 val lemma2 = result(); |
843 val lemma2 = result(); |
844 |
844 |
845 Goal "(c*a) mod (c*b) = (c::int) * (a mod b)"; |
845 Goal "(c*a) mod (c*b) = (c::int) * (a mod b)"; |
846 by (zdiv_undefined_case_tac "b = #0" 1); |
846 by (zdiv_undefined_case_tac "b = Numeral0" 1); |
847 by (zdiv_undefined_case_tac "c = #0" 1); |
847 by (zdiv_undefined_case_tac "c = Numeral0" 1); |
848 by (auto_tac |
848 by (auto_tac |
849 (claset(), |
849 (claset(), |
850 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
850 simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, |
851 lemma1, lemma2])); |
851 lemma1, lemma2])); |
852 qed "zmod_zmult_zmult1"; |
852 qed "zmod_zmult_zmult1"; |
879 by (asm_simp_tac (simpset() |
879 by (asm_simp_tac (simpset() |
880 addsimps [mod_pos_pos_trivial, |
880 addsimps [mod_pos_pos_trivial, |
881 pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
881 pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
882 by (auto_tac (claset(), |
882 by (auto_tac (claset(), |
883 simpset() addsimps [mod_pos_pos_trivial])); |
883 simpset() addsimps [mod_pos_pos_trivial])); |
884 by (subgoal_tac "#0 <= b mod a" 1); |
884 by (subgoal_tac "Numeral0 <= b mod a" 1); |
885 by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
885 by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
886 by (arith_tac 1); |
886 by (arith_tac 1); |
887 qed "pos_zdiv_mult_2"; |
887 qed "pos_zdiv_mult_2"; |
888 |
888 |
889 |
889 |
890 Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a"; |
890 Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) div (# 2*a) = (b+Numeral1) div a"; |
891 by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1); |
891 by (subgoal_tac "(Numeral1 + # 2*(-b-Numeral1)) div (# 2 * (-a)) = (-b-Numeral1) div (-a)" 1); |
892 by (rtac pos_zdiv_mult_2 2); |
892 by (rtac pos_zdiv_mult_2 2); |
893 by (auto_tac (claset(), |
893 by (auto_tac (claset(), |
894 simpset() addsimps [zmult_zminus_right])); |
894 simpset() addsimps [zmult_zminus_right])); |
895 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1); |
895 by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1); |
896 by (Simp_tac 2); |
896 by (Simp_tac 2); |
897 by (asm_full_simp_tac (HOL_ss |
897 by (asm_full_simp_tac (HOL_ss |
898 addsimps [zdiv_zminus_zminus, zdiff_def, |
898 addsimps [zdiv_zminus_zminus, zdiff_def, |
899 zminus_zadd_distrib RS sym]) 1); |
899 zminus_zadd_distrib RS sym]) 1); |
900 qed "neg_zdiv_mult_2"; |
900 qed "neg_zdiv_mult_2"; |
901 |
901 |
902 |
902 |
903 (*Not clear why this must be proved separately; probably number_of causes |
903 (*Not clear why this must be proved separately; probably number_of causes |
904 simplification problems*) |
904 simplification problems*) |
905 Goal "~ #0 <= x ==> x <= (#0::int)"; |
905 Goal "~ Numeral0 <= x ==> x <= (Numeral0::int)"; |
906 by Auto_tac; |
906 by Auto_tac; |
907 val lemma = result(); |
907 val lemma = result(); |
908 |
908 |
909 Goal "number_of (v BIT b) div number_of (w BIT False) = \ |
909 Goal "number_of (v BIT b) div number_of (w BIT False) = \ |
910 \ (if ~b | (#0::int) <= number_of w \ |
910 \ (if ~b | (Numeral0::int) <= number_of w \ |
911 \ then number_of v div (number_of w) \ |
911 \ then number_of v div (number_of w) \ |
912 \ else (number_of v + (#1::int)) div (number_of w))"; |
912 \ else (number_of v + (Numeral1::int)) div (number_of w))"; |
913 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
913 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
914 by (asm_simp_tac (simpset() |
914 by (asm_simp_tac (simpset() |
915 delsimps [number_of_reorient]@bin_arith_extra_simps@bin_rel_simps |
915 delsimps [thm "number_of_reorient"]@bin_arith_extra_simps@bin_rel_simps |
916 addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, |
916 addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, |
917 neg_zdiv_mult_2]) 1); |
917 neg_zdiv_mult_2]) 1); |
918 qed "zdiv_number_of_BIT"; |
918 qed "zdiv_number_of_BIT"; |
919 Addsimps [zdiv_number_of_BIT]; |
919 Addsimps [zdiv_number_of_BIT]; |
920 |
920 |
921 |
921 |
922 (** computing "mod" by shifting (proofs resemble those for "div") **) |
922 (** computing "mod" by shifting (proofs resemble those for "div") **) |
923 |
923 |
924 Goal "(#0::int) <= a ==> (#1 + #2*b) mod (#2*a) = #1 + #2 * (b mod a)"; |
924 Goal "(Numeral0::int) <= a ==> (Numeral1 + # 2*b) mod (# 2*a) = Numeral1 + # 2 * (b mod a)"; |
925 by (zdiv_undefined_case_tac "a = #0" 1); |
925 by (zdiv_undefined_case_tac "a = Numeral0" 1); |
926 by (subgoal_tac "#1 <= a" 1); |
926 by (subgoal_tac "Numeral1 <= a" 1); |
927 by (arith_tac 2); |
927 by (arith_tac 2); |
928 by (subgoal_tac "#1 < a * #2" 1); |
928 by (subgoal_tac "Numeral1 < a * # 2" 1); |
929 by (arith_tac 2); |
929 by (arith_tac 2); |
930 by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1); |
930 by (subgoal_tac "# 2*(Numeral1 + b mod a) <= # 2*a" 1); |
931 by (rtac zmult_zle_mono2 2); |
931 by (rtac zmult_zle_mono2 2); |
932 by (auto_tac (claset(), |
932 by (auto_tac (claset(), |
933 simpset() addsimps [zadd_commute, zmult_commute, |
933 simpset() addsimps [zadd_commute, zmult_commute, |
934 add1_zle_eq, pos_mod_bound])); |
934 add1_zle_eq, pos_mod_bound])); |
935 by (stac zmod_zadd1_eq 1); |
935 by (stac zmod_zadd1_eq 1); |
939 by (asm_simp_tac (simpset() |
939 by (asm_simp_tac (simpset() |
940 addsimps [mod_pos_pos_trivial, |
940 addsimps [mod_pos_pos_trivial, |
941 pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
941 pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
942 by (auto_tac (claset(), |
942 by (auto_tac (claset(), |
943 simpset() addsimps [mod_pos_pos_trivial])); |
943 simpset() addsimps [mod_pos_pos_trivial])); |
944 by (subgoal_tac "#0 <= b mod a" 1); |
944 by (subgoal_tac "Numeral0 <= b mod a" 1); |
945 by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
945 by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
946 by (arith_tac 1); |
946 by (arith_tac 1); |
947 qed "pos_zmod_mult_2"; |
947 qed "pos_zmod_mult_2"; |
948 |
948 |
949 |
949 |
950 Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1"; |
950 Goal "a <= (Numeral0::int) ==> (Numeral1 + # 2*b) mod (# 2*a) = # 2 * ((b+Numeral1) mod a) - Numeral1"; |
951 by (subgoal_tac |
951 by (subgoal_tac |
952 "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1); |
952 "(Numeral1 + # 2*(-b-Numeral1)) mod (# 2*(-a)) = Numeral1 + # 2*((-b-Numeral1) mod (-a))" 1); |
953 by (rtac pos_zmod_mult_2 2); |
953 by (rtac pos_zmod_mult_2 2); |
954 by (auto_tac (claset(), |
954 by (auto_tac (claset(), |
955 simpset() addsimps [zmult_zminus_right])); |
955 simpset() addsimps [zmult_zminus_right])); |
956 by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1); |
956 by (subgoal_tac "(# -1 - (# 2 * b)) = - (Numeral1 + (# 2 * b))" 1); |
957 by (Simp_tac 2); |
957 by (Simp_tac 2); |
958 by (asm_full_simp_tac (HOL_ss |
958 by (asm_full_simp_tac (HOL_ss |
959 addsimps [zmod_zminus_zminus, zdiff_def, |
959 addsimps [zmod_zminus_zminus, zdiff_def, |
960 zminus_zadd_distrib RS sym]) 1); |
960 zminus_zadd_distrib RS sym]) 1); |
961 by (dtac (zminus_equation RS iffD1 RS sym) 1); |
961 by (dtac (zminus_equation RS iffD1 RS sym) 1); |
962 by Auto_tac; |
962 by Auto_tac; |
963 qed "neg_zmod_mult_2"; |
963 qed "neg_zmod_mult_2"; |
964 |
964 |
965 Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |
965 Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |
966 \ (if b then \ |
966 \ (if b then \ |
967 \ if (#0::int) <= number_of w \ |
967 \ if (Numeral0::int) <= number_of w \ |
968 \ then #2 * (number_of v mod number_of w) + #1 \ |
968 \ then # 2 * (number_of v mod number_of w) + Numeral1 \ |
969 \ else #2 * ((number_of v + (#1::int)) mod number_of w) - #1 \ |
969 \ else # 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \ |
970 \ else #2 * (number_of v mod number_of w))"; |
970 \ else # 2 * (number_of v mod number_of w))"; |
971 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
971 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
972 by (asm_simp_tac (simpset() |
972 by (asm_simp_tac (simpset() |
973 delsimps bin_arith_extra_simps@bin_rel_simps |
973 delsimps bin_arith_extra_simps@bin_rel_simps |
974 addsimps [zmod_zmult_zmult1, |
974 addsimps [zmod_zmult_zmult1, |
975 pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1); |
975 pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1); |
978 Addsimps [zmod_number_of_BIT]; |
978 Addsimps [zmod_number_of_BIT]; |
979 |
979 |
980 |
980 |
981 (** Quotients of signs **) |
981 (** Quotients of signs **) |
982 |
982 |
983 Goal "[| a < (#0::int); #0 < b |] ==> a div b < #0"; |
983 Goal "[| a < (Numeral0::int); Numeral0 < b |] ==> a div b < Numeral0"; |
984 by (subgoal_tac "a div b <= #-1" 1); |
984 by (subgoal_tac "a div b <= # -1" 1); |
985 by (Force_tac 1); |
985 by (Force_tac 1); |
986 by (rtac order_trans 1); |
986 by (rtac order_trans 1); |
987 by (res_inst_tac [("a'","#-1")] zdiv_mono1 1); |
987 by (res_inst_tac [("a'","# -1")] zdiv_mono1 1); |
988 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); |
988 by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); |
989 qed "div_neg_pos_less0"; |
989 qed "div_neg_pos_less0"; |
990 |
990 |
991 Goal "[| (#0::int) <= a; b < #0 |] ==> a div b <= #0"; |
991 Goal "[| (Numeral0::int) <= a; b < Numeral0 |] ==> a div b <= Numeral0"; |
992 by (dtac zdiv_mono1_neg 1); |
992 by (dtac zdiv_mono1_neg 1); |
993 by Auto_tac; |
993 by Auto_tac; |
994 qed "div_nonneg_neg_le0"; |
994 qed "div_nonneg_neg_le0"; |
995 |
995 |
996 Goal "(#0::int) < b ==> (#0 <= a div b) = (#0 <= a)"; |
996 Goal "(Numeral0::int) < b ==> (Numeral0 <= a div b) = (Numeral0 <= a)"; |
997 by Auto_tac; |
997 by Auto_tac; |
998 by (dtac zdiv_mono1 2); |
998 by (dtac zdiv_mono1 2); |
999 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); |
999 by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); |
1000 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
1000 by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
1001 by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); |
1001 by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); |
1002 qed "pos_imp_zdiv_nonneg_iff"; |
1002 qed "pos_imp_zdiv_nonneg_iff"; |
1003 |
1003 |
1004 Goal "b < (#0::int) ==> (#0 <= a div b) = (a <= (#0::int))"; |
1004 Goal "b < (Numeral0::int) ==> (Numeral0 <= a div b) = (a <= (Numeral0::int))"; |
1005 by (stac (zdiv_zminus_zminus RS sym) 1); |
1005 by (stac (zdiv_zminus_zminus RS sym) 1); |
1006 by (stac pos_imp_zdiv_nonneg_iff 1); |
1006 by (stac pos_imp_zdiv_nonneg_iff 1); |
1007 by Auto_tac; |
1007 by Auto_tac; |
1008 qed "neg_imp_zdiv_nonneg_iff"; |
1008 qed "neg_imp_zdiv_nonneg_iff"; |
1009 |
1009 |
1010 (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) |
1010 (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) |
1011 Goal "(#0::int) < b ==> (a div b < #0) = (a < #0)"; |
1011 Goal "(Numeral0::int) < b ==> (a div b < Numeral0) = (a < Numeral0)"; |
1012 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1012 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1013 pos_imp_zdiv_nonneg_iff]) 1); |
1013 pos_imp_zdiv_nonneg_iff]) 1); |
1014 qed "pos_imp_zdiv_neg_iff"; |
1014 qed "pos_imp_zdiv_neg_iff"; |
1015 |
1015 |
1016 (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*) |
1016 (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*) |
1017 Goal "b < (#0::int) ==> (a div b < #0) = (#0 < a)"; |
1017 Goal "b < (Numeral0::int) ==> (a div b < Numeral0) = (Numeral0 < a)"; |
1018 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1018 by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
1019 neg_imp_zdiv_nonneg_iff]) 1); |
1019 neg_imp_zdiv_nonneg_iff]) 1); |
1020 qed "neg_imp_zdiv_neg_iff"; |
1020 qed "neg_imp_zdiv_neg_iff"; |