54 qed "intrelE"; |
54 qed "intrelE"; |
55 |
55 |
56 AddSIs [intrelI]; |
56 AddSIs [intrelI]; |
57 AddSEs [intrelE]; |
57 AddSEs [intrelE]; |
58 |
58 |
59 goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; |
59 Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)"; |
60 by (Fast_tac 1); |
60 by (Fast_tac 1); |
61 qed "intrel_iff"; |
61 qed "intrel_iff"; |
62 |
62 |
63 goal Integ.thy "(x,x): intrel"; |
63 Goal "(x,x): intrel"; |
64 by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1); |
64 by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1); |
65 qed "intrel_refl"; |
65 qed "intrel_refl"; |
66 |
66 |
67 goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def] |
67 Goalw [equiv_def, refl_def, sym_def, trans_def] |
68 "equiv {x::(nat*nat).True} intrel"; |
68 "equiv {x::(nat*nat).True} intrel"; |
69 by (fast_tac (claset() addSIs [intrel_refl] |
69 by (fast_tac (claset() addSIs [intrel_refl] |
70 addSEs [sym, integ_trans_lemma]) 1); |
70 addSEs [sym, integ_trans_lemma]) 1); |
71 qed "equiv_intrel"; |
71 qed "equiv_intrel"; |
72 |
72 |
73 val equiv_intrel_iff = |
73 val equiv_intrel_iff = |
74 [TrueI, TrueI] MRS |
74 [TrueI, TrueI] MRS |
75 ([CollectI, CollectI] MRS |
75 ([CollectI, CollectI] MRS |
76 (equiv_intrel RS eq_equiv_class_iff)); |
76 (equiv_intrel RS eq_equiv_class_iff)); |
77 |
77 |
78 goalw Integ.thy [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; |
78 Goalw [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ"; |
79 by (Fast_tac 1); |
79 by (Fast_tac 1); |
80 qed "intrel_in_integ"; |
80 qed "intrel_in_integ"; |
81 |
81 |
82 goal Integ.thy "inj_on Abs_Integ Integ"; |
82 Goal "inj_on Abs_Integ Integ"; |
83 by (rtac inj_on_inverseI 1); |
83 by (rtac inj_on_inverseI 1); |
84 by (etac Abs_Integ_inverse 1); |
84 by (etac Abs_Integ_inverse 1); |
85 qed "inj_on_Abs_Integ"; |
85 qed "inj_on_Abs_Integ"; |
86 |
86 |
87 Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, |
87 Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff, |
88 intrel_iff, intrel_in_integ, Abs_Integ_inverse]; |
88 intrel_iff, intrel_in_integ, Abs_Integ_inverse]; |
89 |
89 |
90 goal Integ.thy "inj(Rep_Integ)"; |
90 Goal "inj(Rep_Integ)"; |
91 by (rtac inj_inverseI 1); |
91 by (rtac inj_inverseI 1); |
92 by (rtac Rep_Integ_inverse 1); |
92 by (rtac Rep_Integ_inverse 1); |
93 qed "inj_Rep_Integ"; |
93 qed "inj_Rep_Integ"; |
94 |
94 |
95 |
95 |
96 |
96 |
97 |
97 |
98 (** znat: the injection from nat to Integ **) |
98 (** znat: the injection from nat to Integ **) |
99 |
99 |
100 goal Integ.thy "inj(znat)"; |
100 Goal "inj(znat)"; |
101 by (rtac injI 1); |
101 by (rtac injI 1); |
102 by (rewtac znat_def); |
102 by (rewtac znat_def); |
103 by (dtac (inj_on_Abs_Integ RS inj_onD) 1); |
103 by (dtac (inj_on_Abs_Integ RS inj_onD) 1); |
104 by (REPEAT (rtac intrel_in_integ 1)); |
104 by (REPEAT (rtac intrel_in_integ 1)); |
105 by (dtac eq_equiv_class 1); |
105 by (dtac eq_equiv_class 1); |
233 qed "zadd_congruent2"; |
233 qed "zadd_congruent2"; |
234 |
234 |
235 (*Resolve th against the corresponding facts for zadd*) |
235 (*Resolve th against the corresponding facts for zadd*) |
236 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
236 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2]; |
237 |
237 |
238 goalw Integ.thy [zadd_def] |
238 Goalw [zadd_def] |
239 "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ |
239 "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \ |
240 \ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; |
240 \ Abs_Integ(intrel^^{(x1+x2, y1+y2)})"; |
241 by (asm_simp_tac |
241 by (asm_simp_tac |
242 (simpset() addsimps [zadd_ize UN_equiv_class2]) 1); |
242 (simpset() addsimps [zadd_ize UN_equiv_class2]) 1); |
243 qed "zadd"; |
243 qed "zadd"; |
244 |
244 |
245 goalw Integ.thy [znat_def] "$#0 + z = z"; |
245 Goalw [znat_def] "$#0 + z = z"; |
246 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
246 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
247 by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
247 by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
248 qed "zadd_0"; |
248 qed "zadd_0"; |
249 |
249 |
250 goal Integ.thy "$~ (z + w) = $~ z + $~ w"; |
250 Goal "$~ (z + w) = $~ z + $~ w"; |
251 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
251 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
252 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
252 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
253 by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
253 by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); |
254 qed "zminus_zadd_distrib"; |
254 qed "zminus_zadd_distrib"; |
255 |
255 |
256 goal Integ.thy "(z::int) + w = w + z"; |
256 Goal "(z::int) + w = w + z"; |
257 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
257 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
258 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
258 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
259 by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1); |
259 by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1); |
260 qed "zadd_commute"; |
260 qed "zadd_commute"; |
261 |
261 |
262 goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; |
262 Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)"; |
263 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
263 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
264 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
264 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
265 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
265 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
266 by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
266 by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1); |
267 qed "zadd_assoc"; |
267 qed "zadd_assoc"; |
268 |
268 |
269 (*For AC rewriting*) |
269 (*For AC rewriting*) |
270 goal Integ.thy "(x::int)+(y+z)=y+(x+z)"; |
270 Goal "(x::int)+(y+z)=y+(x+z)"; |
271 by (rtac (zadd_commute RS trans) 1); |
271 by (rtac (zadd_commute RS trans) 1); |
272 by (rtac (zadd_assoc RS trans) 1); |
272 by (rtac (zadd_assoc RS trans) 1); |
273 by (rtac (zadd_commute RS arg_cong) 1); |
273 by (rtac (zadd_commute RS arg_cong) 1); |
274 qed "zadd_left_commute"; |
274 qed "zadd_left_commute"; |
275 |
275 |
276 (*Integer addition is an AC operator*) |
276 (*Integer addition is an AC operator*) |
277 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; |
277 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; |
278 |
278 |
279 goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)"; |
279 Goalw [znat_def] "$# (m + n) = ($#m) + ($#n)"; |
280 by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
280 by (asm_simp_tac (simpset() addsimps [zadd]) 1); |
281 qed "znat_add"; |
281 qed "znat_add"; |
282 |
282 |
283 goalw Integ.thy [znat_def] "z + ($~ z) = $#0"; |
283 Goalw [znat_def] "z + ($~ z) = $#0"; |
284 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
284 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
285 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
285 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); |
286 qed "zadd_zminus_inverse"; |
286 qed "zadd_zminus_inverse"; |
287 |
287 |
288 goal Integ.thy "($~ z) + z = $#0"; |
288 Goal "($~ z) + z = $#0"; |
289 by (rtac (zadd_commute RS trans) 1); |
289 by (rtac (zadd_commute RS trans) 1); |
290 by (rtac zadd_zminus_inverse 1); |
290 by (rtac zadd_zminus_inverse 1); |
291 qed "zadd_zminus_inverse2"; |
291 qed "zadd_zminus_inverse2"; |
292 |
292 |
293 goal Integ.thy "z + $#0 = z"; |
293 Goal "z + $#0 = z"; |
294 by (rtac (zadd_commute RS trans) 1); |
294 by (rtac (zadd_commute RS trans) 1); |
295 by (rtac zadd_0 1); |
295 by (rtac zadd_0 1); |
296 qed "zadd_0_right"; |
296 qed "zadd_0_right"; |
297 |
297 |
298 |
298 |
338 qed "zmult_congruent2"; |
338 qed "zmult_congruent2"; |
339 |
339 |
340 (*Resolve th against the corresponding facts for zmult*) |
340 (*Resolve th against the corresponding facts for zmult*) |
341 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
341 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2]; |
342 |
342 |
343 goalw Integ.thy [zmult_def] |
343 Goalw [zmult_def] |
344 "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ |
344 "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = \ |
345 \ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; |
345 \ Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"; |
346 by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1); |
346 by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1); |
347 qed "zmult"; |
347 qed "zmult"; |
348 |
348 |
349 goalw Integ.thy [znat_def] "$#0 * z = $#0"; |
349 Goalw [znat_def] "$#0 * z = $#0"; |
350 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
350 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
351 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
351 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
352 qed "zmult_0"; |
352 qed "zmult_0"; |
353 |
353 |
354 goalw Integ.thy [znat_def] "$#Suc(0) * z = z"; |
354 Goalw [znat_def] "$#Suc(0) * z = z"; |
355 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
355 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
356 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
356 by (asm_simp_tac (simpset() addsimps [zmult]) 1); |
357 qed "zmult_1"; |
357 qed "zmult_1"; |
358 |
358 |
359 goal Integ.thy "($~ z) * w = $~ (z * w)"; |
359 Goal "($~ z) * w = $~ (z * w)"; |
360 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
360 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
361 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
361 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
362 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
362 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
363 qed "zmult_zminus"; |
363 qed "zmult_zminus"; |
364 |
364 |
365 |
365 |
366 goal Integ.thy "($~ z) * ($~ w) = (z * w)"; |
366 Goal "($~ z) * ($~ w) = (z * w)"; |
367 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
367 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
368 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
368 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
369 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
369 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); |
370 qed "zmult_zminus_zminus"; |
370 qed "zmult_zminus_zminus"; |
371 |
371 |
372 goal Integ.thy "(z::int) * w = w * z"; |
372 Goal "(z::int) * w = w * z"; |
373 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
373 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
374 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
374 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
375 by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); |
375 by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); |
376 qed "zmult_commute"; |
376 qed "zmult_commute"; |
377 |
377 |
378 goal Integ.thy "z * $# 0 = $#0"; |
378 Goal "z * $# 0 = $#0"; |
379 by (rtac ([zmult_commute, zmult_0] MRS trans) 1); |
379 by (rtac ([zmult_commute, zmult_0] MRS trans) 1); |
380 qed "zmult_0_right"; |
380 qed "zmult_0_right"; |
381 |
381 |
382 goal Integ.thy "z * $#Suc(0) = z"; |
382 Goal "z * $#Suc(0) = z"; |
383 by (rtac ([zmult_commute, zmult_1] MRS trans) 1); |
383 by (rtac ([zmult_commute, zmult_1] MRS trans) 1); |
384 qed "zmult_1_right"; |
384 qed "zmult_1_right"; |
385 |
385 |
386 goal Integ.thy "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; |
386 Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; |
387 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
387 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); |
388 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
388 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); |
389 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
389 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1); |
390 by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ |
390 by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ |
391 add_ac @ mult_ac)) 1); |
391 add_ac @ mult_ac)) 1); |
432 |
432 |
433 |
433 |
434 (**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****) |
434 (**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****) |
435 |
435 |
436 (* Some Theorems about zsuc and zpred *) |
436 (* Some Theorems about zsuc and zpred *) |
437 goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)"; |
437 Goalw [zsuc_def] "$#(Suc(n)) = zsuc($# n)"; |
438 by (simp_tac (simpset() addsimps [znat_add RS sym]) 1); |
438 by (simp_tac (simpset() addsimps [znat_add RS sym]) 1); |
439 qed "znat_Suc"; |
439 qed "znat_Suc"; |
440 |
440 |
441 goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)"; |
441 Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)"; |
442 by (Simp_tac 1); |
442 by (Simp_tac 1); |
443 qed "zminus_zsuc"; |
443 qed "zminus_zsuc"; |
444 |
444 |
445 goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)"; |
445 Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)"; |
446 by (Simp_tac 1); |
446 by (Simp_tac 1); |
447 qed "zminus_zpred"; |
447 qed "zminus_zpred"; |
448 |
448 |
449 goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] |
449 Goalw [zsuc_def,zpred_def,zdiff_def] |
450 "zpred(zsuc(z)) = z"; |
450 "zpred(zsuc(z)) = z"; |
451 by (simp_tac (simpset() addsimps [zadd_assoc]) 1); |
451 by (simp_tac (simpset() addsimps [zadd_assoc]) 1); |
452 qed "zpred_zsuc"; |
452 qed "zpred_zsuc"; |
453 |
453 |
454 goalw Integ.thy [zsuc_def,zpred_def,zdiff_def] |
454 Goalw [zsuc_def,zpred_def,zdiff_def] |
455 "zsuc(zpred(z)) = z"; |
455 "zsuc(zpred(z)) = z"; |
456 by (simp_tac (simpset() addsimps [zadd_assoc]) 1); |
456 by (simp_tac (simpset() addsimps [zadd_assoc]) 1); |
457 qed "zsuc_zpred"; |
457 qed "zsuc_zpred"; |
458 |
458 |
459 goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))"; |
459 Goal "(zpred(z)=w) = (z=zsuc(w))"; |
460 by Safe_tac; |
460 by Safe_tac; |
461 by (rtac (zsuc_zpred RS sym) 1); |
461 by (rtac (zsuc_zpred RS sym) 1); |
462 by (rtac zpred_zsuc 1); |
462 by (rtac zpred_zsuc 1); |
463 qed "zpred_to_zsuc"; |
463 qed "zpred_to_zsuc"; |
464 |
464 |
465 goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))"; |
465 Goal "(zsuc(z)=w)=(z=zpred(w))"; |
466 by Safe_tac; |
466 by Safe_tac; |
467 by (rtac (zpred_zsuc RS sym) 1); |
467 by (rtac (zpred_zsuc RS sym) 1); |
468 by (rtac zsuc_zpred 1); |
468 by (rtac zsuc_zpred 1); |
469 qed "zsuc_to_zpred"; |
469 qed "zsuc_to_zpred"; |
470 |
470 |
471 goal Integ.thy "($~ z = w) = (z = $~ w)"; |
471 Goal "($~ z = w) = (z = $~ w)"; |
472 by Safe_tac; |
472 by Safe_tac; |
473 by (rtac (zminus_zminus RS sym) 1); |
473 by (rtac (zminus_zminus RS sym) 1); |
474 by (rtac zminus_zminus 1); |
474 by (rtac zminus_zminus 1); |
475 qed "zminus_exchange"; |
475 qed "zminus_exchange"; |
476 |
476 |
477 goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)"; |
477 Goal"(zsuc(z)=zsuc(w)) = (z=w)"; |
478 by Safe_tac; |
478 by Safe_tac; |
479 by (dres_inst_tac [("f","zpred")] arg_cong 1); |
479 by (dres_inst_tac [("f","zpred")] arg_cong 1); |
480 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1); |
480 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1); |
481 qed "bijective_zsuc"; |
481 qed "bijective_zsuc"; |
482 |
482 |
483 goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)"; |
483 Goal"(zpred(z)=zpred(w)) = (z=w)"; |
484 by Safe_tac; |
484 by Safe_tac; |
485 by (dres_inst_tac [("f","zsuc")] arg_cong 1); |
485 by (dres_inst_tac [("f","zsuc")] arg_cong 1); |
486 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1); |
486 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1); |
487 qed "bijective_zpred"; |
487 qed "bijective_zpred"; |
488 |
488 |
489 (* Additional Theorems about zadd *) |
489 (* Additional Theorems about zadd *) |
490 |
490 |
491 goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)"; |
491 Goalw [zsuc_def] "zsuc(z) + w = zsuc(z+w)"; |
492 by (simp_tac (simpset() addsimps zadd_ac) 1); |
492 by (simp_tac (simpset() addsimps zadd_ac) 1); |
493 qed "zadd_zsuc"; |
493 qed "zadd_zsuc"; |
494 |
494 |
495 goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)"; |
495 Goalw [zsuc_def] "w + zsuc(z) = zsuc(w+z)"; |
496 by (simp_tac (simpset() addsimps zadd_ac) 1); |
496 by (simp_tac (simpset() addsimps zadd_ac) 1); |
497 qed "zadd_zsuc_right"; |
497 qed "zadd_zsuc_right"; |
498 |
498 |
499 goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)"; |
499 Goalw [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)"; |
500 by (simp_tac (simpset() addsimps zadd_ac) 1); |
500 by (simp_tac (simpset() addsimps zadd_ac) 1); |
501 qed "zadd_zpred"; |
501 qed "zadd_zpred"; |
502 |
502 |
503 goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)"; |
503 Goalw [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)"; |
504 by (simp_tac (simpset() addsimps zadd_ac) 1); |
504 by (simp_tac (simpset() addsimps zadd_ac) 1); |
505 qed "zadd_zpred_right"; |
505 qed "zadd_zpred_right"; |
506 |
506 |
507 |
507 |
508 (* Additional Theorems about zmult *) |
508 (* Additional Theorems about zmult *) |
509 |
509 |
510 goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z"; |
510 Goalw [zsuc_def] "zsuc(w) * z = z + w * z"; |
511 by (simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_commute]) 1); |
511 by (simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_commute]) 1); |
512 qed "zmult_zsuc"; |
512 qed "zmult_zsuc"; |
513 |
513 |
514 goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z"; |
514 Goalw [zsuc_def] "z * zsuc(w) = z + w * z"; |
515 by (simp_tac |
515 by (simp_tac |
516 (simpset() addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); |
516 (simpset() addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); |
517 qed "zmult_zsuc_right"; |
517 qed "zmult_zsuc_right"; |
518 |
518 |
519 goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z"; |
519 Goalw [zpred_def, zdiff_def] "zpred(w) * z = w * z - z"; |
520 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
520 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
521 qed "zmult_zpred"; |
521 qed "zmult_zpred"; |
522 |
522 |
523 goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z"; |
523 Goalw [zpred_def, zdiff_def] "z * zpred(w) = w * z - z"; |
524 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2, zmult_commute]) 1); |
524 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2, zmult_commute]) 1); |
525 qed "zmult_zpred_right"; |
525 qed "zmult_zpred_right"; |
526 |
526 |
527 (* Further Theorems about zsuc and zpred *) |
527 (* Further Theorems about zsuc and zpred *) |
528 goal Integ.thy "$#Suc(m) ~= $#0"; |
528 Goal "$#Suc(m) ~= $#0"; |
529 by (simp_tac (simpset() addsimps [inj_znat RS inj_eq]) 1); |
529 by (simp_tac (simpset() addsimps [inj_znat RS inj_eq]) 1); |
530 qed "znat_Suc_not_znat_Zero"; |
530 qed "znat_Suc_not_znat_Zero"; |
531 |
531 |
532 bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym)); |
532 bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym)); |
533 |
533 |
534 |
534 |
535 goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)"; |
535 Goalw [zsuc_def,znat_def] "w ~= zsuc(w)"; |
536 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
536 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
537 by (asm_full_simp_tac (simpset() addsimps [zadd]) 1); |
537 by (asm_full_simp_tac (simpset() addsimps [zadd]) 1); |
538 qed "n_not_zsuc_n"; |
538 qed "n_not_zsuc_n"; |
539 |
539 |
540 val zsuc_n_not_n = n_not_zsuc_n RS not_sym; |
540 val zsuc_n_not_n = n_not_zsuc_n RS not_sym; |
541 |
541 |
542 goal Integ.thy "w ~= zpred(w)"; |
542 Goal "w ~= zpred(w)"; |
543 by Safe_tac; |
543 by Safe_tac; |
544 by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); |
544 by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); |
545 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1); |
545 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1); |
546 qed "n_not_zpred_n"; |
546 qed "n_not_zpred_n"; |
547 |
547 |
548 val zpred_n_not_n = n_not_zpred_n RS not_sym; |
548 val zpred_n_not_n = n_not_zpred_n RS not_sym; |
549 |
549 |
550 |
550 |
551 (* Theorems about less and less_equal *) |
551 (* Theorems about less and less_equal *) |
552 |
552 |
553 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
553 Goalw [zless_def, znegative_def, zdiff_def, znat_def] |
554 "!!w. w<z ==> ? n. z = w + $#(Suc(n))"; |
554 "!!w. w<z ==> ? n. z = w + $#(Suc(n))"; |
555 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
555 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
556 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
556 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
557 by Safe_tac; |
557 by Safe_tac; |
558 by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); |
558 by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); |
559 by (safe_tac (claset() addSDs [less_eq_Suc_add])); |
559 by (safe_tac (claset() addSDs [less_eq_Suc_add])); |
560 by (res_inst_tac [("x","k")] exI 1); |
560 by (res_inst_tac [("x","k")] exI 1); |
561 by (asm_full_simp_tac (simpset() addsimps add_ac) 1); |
561 by (asm_full_simp_tac (simpset() addsimps add_ac) 1); |
562 qed "zless_eq_zadd_Suc"; |
562 qed "zless_eq_zadd_Suc"; |
563 |
563 |
564 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
564 Goalw [zless_def, znegative_def, zdiff_def, znat_def] |
565 "z < z + $#(Suc(n))"; |
565 "z < z + $#(Suc(n))"; |
566 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
566 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
567 by (Clarify_tac 1); |
567 by (Clarify_tac 1); |
568 by (simp_tac (simpset() addsimps [zadd, zminus]) 1); |
568 by (simp_tac (simpset() addsimps [zadd, zminus]) 1); |
569 qed "zless_zadd_Suc"; |
569 qed "zless_zadd_Suc"; |
570 |
570 |
571 goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)"; |
571 Goal "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)"; |
572 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
572 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
573 by (simp_tac |
573 by (simp_tac |
574 (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); |
574 (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); |
575 qed "zless_trans"; |
575 qed "zless_trans"; |
576 |
576 |
577 goalw Integ.thy [zsuc_def] "z<zsuc(z)"; |
577 Goalw [zsuc_def] "z<zsuc(z)"; |
578 by (rtac zless_zadd_Suc 1); |
578 by (rtac zless_zadd_Suc 1); |
579 qed "zlessI"; |
579 qed "zlessI"; |
580 |
580 |
581 val zless_zsucI = zlessI RSN (2,zless_trans); |
581 val zless_zsucI = zlessI RSN (2,zless_trans); |
582 |
582 |
583 goal Integ.thy "!!z w::int. z<w ==> ~w<z"; |
583 Goal "!!z w::int. z<w ==> ~w<z"; |
584 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
584 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
585 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
585 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
586 by Safe_tac; |
586 by Safe_tac; |
587 by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1); |
587 by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1); |
588 qed "zless_not_sym"; |
588 qed "zless_not_sym"; |
589 |
589 |
590 (* [| n<m; m<n |] ==> R *) |
590 (* [| n<m; m<n |] ==> R *) |
591 bind_thm ("zless_asym", (zless_not_sym RS notE)); |
591 bind_thm ("zless_asym", (zless_not_sym RS notE)); |
592 |
592 |
593 goal Integ.thy "!!z::int. ~ z<z"; |
593 Goal "!!z::int. ~ z<z"; |
594 by (resolve_tac [zless_asym RS notI] 1); |
594 by (resolve_tac [zless_asym RS notI] 1); |
595 by (REPEAT (assume_tac 1)); |
595 by (REPEAT (assume_tac 1)); |
596 qed "zless_not_refl"; |
596 qed "zless_not_refl"; |
597 |
597 |
598 (* z<z ==> R *) |
598 (* z<z ==> R *) |
599 bind_thm ("zless_irrefl", (zless_not_refl RS notE)); |
599 bind_thm ("zless_irrefl", (zless_not_refl RS notE)); |
600 |
600 |
601 goal Integ.thy "!!w. z<w ==> w ~= (z::int)"; |
601 Goal "!!w. z<w ==> w ~= (z::int)"; |
602 by (fast_tac (claset() addEs [zless_irrefl]) 1); |
602 by (fast_tac (claset() addEs [zless_irrefl]) 1); |
603 qed "zless_not_refl2"; |
603 qed "zless_not_refl2"; |
604 |
604 |
605 |
605 |
606 (*"Less than" is a linear ordering*) |
606 (*"Less than" is a linear ordering*) |
607 goalw Integ.thy [zless_def, znegative_def, zdiff_def] |
607 Goalw [zless_def, znegative_def, zdiff_def] |
608 "z<w | z=w | w<(z::int)"; |
608 "z<w | z=w | w<(z::int)"; |
609 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
609 by (res_inst_tac [("z","z")] eq_Abs_Integ 1); |
610 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
610 by (res_inst_tac [("z","w")] eq_Abs_Integ 1); |
611 by Safe_tac; |
611 by Safe_tac; |
612 by (asm_full_simp_tac |
612 by (asm_full_simp_tac |
616 qed "zless_linear"; |
616 qed "zless_linear"; |
617 |
617 |
618 |
618 |
619 (*** Properties of <= ***) |
619 (*** Properties of <= ***) |
620 |
620 |
621 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] |
621 Goalw [zless_def, znegative_def, zdiff_def, znat_def] |
622 "($#m < $#n) = (m<n)"; |
622 "($#m < $#n) = (m<n)"; |
623 by (simp_tac |
623 by (simp_tac |
624 (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
624 (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1); |
625 by (fast_tac (claset() addIs [add_commute] addSEs [less_add_eq_less]) 1); |
625 by (fast_tac (claset() addIs [add_commute] addSEs [less_add_eq_less]) 1); |
626 qed "zless_eq_less"; |
626 qed "zless_eq_less"; |
627 |
627 |
628 goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)"; |
628 Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)"; |
629 by (simp_tac (simpset() addsimps [zless_eq_less]) 1); |
629 by (simp_tac (simpset() addsimps [zless_eq_less]) 1); |
630 qed "zle_eq_le"; |
630 qed "zle_eq_le"; |
631 |
631 |
632 goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)"; |
632 Goalw [zle_def] "!!w. ~(w<z) ==> z<=(w::int)"; |
633 by (assume_tac 1); |
633 by (assume_tac 1); |
634 qed "zleI"; |
634 qed "zleI"; |
635 |
635 |
636 goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))"; |
636 Goalw [zle_def] "!!w. z<=w ==> ~(w<(z::int))"; |
637 by (assume_tac 1); |
637 by (assume_tac 1); |
638 qed "zleD"; |
638 qed "zleD"; |
639 |
639 |
640 val zleE = make_elim zleD; |
640 val zleE = make_elim zleD; |
641 |
641 |
642 goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)"; |
642 Goalw [zle_def] "!!z. ~ z <= w ==> w<(z::int)"; |
643 by (Fast_tac 1); |
643 by (Fast_tac 1); |
644 qed "not_zleE"; |
644 qed "not_zleE"; |
645 |
645 |
646 goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)"; |
646 Goalw [zle_def] "!!z. z < w ==> z <= (w::int)"; |
647 by (fast_tac (claset() addEs [zless_asym]) 1); |
647 by (fast_tac (claset() addEs [zless_asym]) 1); |
648 qed "zless_imp_zle"; |
648 qed "zless_imp_zle"; |
649 |
649 |
650 goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)"; |
650 Goalw [zle_def] "!!z. z <= w ==> z < w | z=(w::int)"; |
651 by (cut_facts_tac [zless_linear] 1); |
651 by (cut_facts_tac [zless_linear] 1); |
652 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); |
652 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); |
653 qed "zle_imp_zless_or_eq"; |
653 qed "zle_imp_zless_or_eq"; |
654 |
654 |
655 goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)"; |
655 Goalw [zle_def] "!!z. z<w | z=w ==> z <=(w::int)"; |
656 by (cut_facts_tac [zless_linear] 1); |
656 by (cut_facts_tac [zless_linear] 1); |
657 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); |
657 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); |
658 qed "zless_or_eq_imp_zle"; |
658 qed "zless_or_eq_imp_zle"; |
659 |
659 |
660 goal Integ.thy "(x <= (y::int)) = (x < y | x=y)"; |
660 Goal "(x <= (y::int)) = (x < y | x=y)"; |
661 by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1)); |
661 by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1)); |
662 qed "zle_eq_zless_or_eq"; |
662 qed "zle_eq_zless_or_eq"; |
663 |
663 |
664 goal Integ.thy "w <= (w::int)"; |
664 Goal "w <= (w::int)"; |
665 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1); |
665 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1); |
666 qed "zle_refl"; |
666 qed "zle_refl"; |
667 |
667 |
668 val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)"; |
668 val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)"; |
669 by (dtac zle_imp_zless_or_eq 1); |
669 by (dtac zle_imp_zless_or_eq 1); |
670 by (fast_tac (claset() addIs [zless_trans]) 1); |
670 by (fast_tac (claset() addIs [zless_trans]) 1); |
671 qed "zle_zless_trans"; |
671 qed "zle_zless_trans"; |
672 |
672 |
673 goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)"; |
673 Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::int)"; |
674 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
674 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
675 rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]); |
675 rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]); |
676 qed "zle_trans"; |
676 qed "zle_trans"; |
677 |
677 |
678 goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)"; |
678 Goal "!!z. [| z <= w; w <= z |] ==> z = (w::int)"; |
679 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
679 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, |
680 fast_tac (claset() addEs [zless_irrefl,zless_asym])]); |
680 fast_tac (claset() addEs [zless_irrefl,zless_asym])]); |
681 qed "zle_anti_sym"; |
681 qed "zle_anti_sym"; |
682 |
682 |
683 |
683 |
684 goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w"; |
684 Goal "!!w w' z::int. z + w' = z + w ==> w' = w"; |
685 by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1); |
685 by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1); |
686 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
686 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); |
687 qed "zadd_left_cancel"; |
687 qed "zadd_left_cancel"; |
688 |
688 |
689 |
689 |
690 (*** Monotonicity results ***) |
690 (*** Monotonicity results ***) |
691 |
691 |
692 goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z"; |
692 Goal "!!v w z::int. v < w ==> v + z < w + z"; |
693 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
693 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); |
694 by (simp_tac (simpset() addsimps zadd_ac) 1); |
694 by (simp_tac (simpset() addsimps zadd_ac) 1); |
695 by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); |
695 by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); |
696 qed "zadd_zless_mono1"; |
696 qed "zadd_zless_mono1"; |
697 |
697 |
698 goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)"; |
698 Goal "!!v w z::int. (v+z < w+z) = (v < w)"; |
699 by (safe_tac (claset() addSEs [zadd_zless_mono1])); |
699 by (safe_tac (claset() addSEs [zadd_zless_mono1])); |
700 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); |
700 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); |
701 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1); |
701 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1); |
702 qed "zadd_left_cancel_zless"; |
702 qed "zadd_left_cancel_zless"; |
703 |
703 |
704 goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)"; |
704 Goal "!!v w z::int. (v+z <= w+z) = (v <= w)"; |
705 by (asm_full_simp_tac |
705 by (asm_full_simp_tac |
706 (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1); |
706 (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1); |
707 qed "zadd_left_cancel_zle"; |
707 qed "zadd_left_cancel_zle"; |
708 |
708 |
709 (*"v<=w ==> v+z <= w+z"*) |
709 (*"v<=w ==> v+z <= w+z"*) |
710 bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2); |
710 bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2); |
711 |
711 |
712 |
712 |
713 goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
713 Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
714 by (etac (zadd_zle_mono1 RS zle_trans) 1); |
714 by (etac (zadd_zle_mono1 RS zle_trans) 1); |
715 by (simp_tac (simpset() addsimps [zadd_commute]) 1); |
715 by (simp_tac (simpset() addsimps [zadd_commute]) 1); |
716 (*w moves to the end because it is free while z', z are bound*) |
716 (*w moves to the end because it is free while z', z are bound*) |
717 by (etac zadd_zle_mono1 1); |
717 by (etac zadd_zle_mono1 1); |
718 qed "zadd_zle_mono"; |
718 qed "zadd_zle_mono"; |
719 |
719 |
720 goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w"; |
720 Goal "!!w z::int. z<=$#0 ==> w+z <= w"; |
721 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1); |
721 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1); |
722 by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1); |
722 by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1); |
723 qed "zadd_zle_self"; |
723 qed "zadd_zle_self"; |
724 |
724 |
725 |
725 |
734 (** Additional theorems for Integ.thy **) |
734 (** Additional theorems for Integ.thy **) |
735 |
735 |
736 Addsimps [zless_eq_less, zle_eq_le, |
736 Addsimps [zless_eq_less, zle_eq_le, |
737 znegative_zminus_znat, not_znegative_znat]; |
737 znegative_zminus_znat, not_znegative_znat]; |
738 |
738 |
739 goal Integ.thy "!! x. (x::int) = y ==> x <= y"; |
739 Goal "!! x. (x::int) = y ==> x <= y"; |
740 by (etac subst 1); by (rtac zle_refl 1); |
740 by (etac subst 1); by (rtac zle_refl 1); |
741 qed "zequalD1"; |
741 qed "zequalD1"; |
742 |
742 |
743 goal Integ.thy "($~ x < $~ y) = (y < x)"; |
743 Goal "($~ x < $~ y) = (y < x)"; |
744 by (rewrite_goals_tac [zless_def,zdiff_def]); |
744 by (rewrite_goals_tac [zless_def,zdiff_def]); |
745 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
745 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
746 qed "zminus_zless_zminus"; |
746 qed "zminus_zless_zminus"; |
747 |
747 |
748 goal Integ.thy "($~ x <= $~ y) = (y <= x)"; |
748 Goal "($~ x <= $~ y) = (y <= x)"; |
749 by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); |
749 by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); |
750 qed "zminus_zle_zminus"; |
750 qed "zminus_zle_zminus"; |
751 |
751 |
752 goal Integ.thy "(x < $~ y) = (y < $~ x)"; |
752 Goal "(x < $~ y) = (y < $~ x)"; |
753 by (rewrite_goals_tac [zless_def,zdiff_def]); |
753 by (rewrite_goals_tac [zless_def,zdiff_def]); |
754 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
754 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
755 qed "zless_zminus"; |
755 qed "zless_zminus"; |
756 |
756 |
757 goal Integ.thy "($~ x < y) = ($~ y < x)"; |
757 Goal "($~ x < y) = ($~ y < x)"; |
758 by (rewrite_goals_tac [zless_def,zdiff_def]); |
758 by (rewrite_goals_tac [zless_def,zdiff_def]); |
759 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
759 by (simp_tac (simpset() addsimps zadd_ac ) 1); |
760 qed "zminus_zless"; |
760 qed "zminus_zless"; |
761 |
761 |
762 goal Integ.thy "(x <= $~ y) = (y <= $~ x)"; |
762 Goal "(x <= $~ y) = (y <= $~ x)"; |
763 by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); |
763 by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); |
764 qed "zle_zminus"; |
764 qed "zle_zminus"; |
765 |
765 |
766 goal Integ.thy "($~ x <= y) = ($~ y <= x)"; |
766 Goal "($~ x <= y) = ($~ y <= x)"; |
767 by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); |
767 by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); |
768 qed "zminus_zle"; |
768 qed "zminus_zle"; |
769 |
769 |
770 goal Integ.thy " $#0 < $# Suc n"; |
770 Goal " $#0 < $# Suc n"; |
771 by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); |
771 by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); |
772 qed "zero_zless_Suc_pos"; |
772 qed "zero_zless_Suc_pos"; |
773 |
773 |
774 goal Integ.thy "($# n= $# m) = (n = m)"; |
774 Goal "($# n= $# m) = (n = m)"; |
775 by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); |
775 by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); |
776 qed "znat_znat_eq"; |
776 qed "znat_znat_eq"; |
777 AddIffs[znat_znat_eq]; |
777 AddIffs[znat_znat_eq]; |
778 |
778 |
779 goal Integ.thy "$~ $# Suc n < $#0"; |
779 Goal "$~ $# Suc n < $#0"; |
780 by (stac (zminus_0 RS sym) 1); |
780 by (stac (zminus_0 RS sym) 1); |
781 by (rtac (zminus_zless_zminus RS iffD2) 1); |
781 by (rtac (zminus_zless_zminus RS iffD2) 1); |
782 by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); |
782 by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); |
783 qed "negative_zless_0"; |
783 qed "negative_zless_0"; |
784 Addsimps [zero_zless_Suc_pos, negative_zless_0]; |
784 Addsimps [zero_zless_Suc_pos, negative_zless_0]; |
785 |
785 |
786 goal Integ.thy "$~ $# n <= $#0"; |
786 Goal "$~ $# n <= $#0"; |
787 by (rtac zless_or_eq_imp_zle 1); |
787 by (rtac zless_or_eq_imp_zle 1); |
788 by (nat_ind_tac "n" 1); |
788 by (nat_ind_tac "n" 1); |
789 by (ALLGOALS Asm_simp_tac); |
789 by (ALLGOALS Asm_simp_tac); |
790 qed "negative_zle_0"; |
790 qed "negative_zle_0"; |
791 Addsimps[negative_zle_0]; |
791 Addsimps[negative_zle_0]; |
792 |
792 |
793 goal Integ.thy "~($#0 <= $~ $# Suc n)"; |
793 Goal "~($#0 <= $~ $# Suc n)"; |
794 by (stac zle_zminus 1); |
794 by (stac zle_zminus 1); |
795 by (Simp_tac 1); |
795 by (Simp_tac 1); |
796 qed "not_zle_0_negative"; |
796 qed "not_zle_0_negative"; |
797 Addsimps[not_zle_0_negative]; |
797 Addsimps[not_zle_0_negative]; |
798 |
798 |
799 goal Integ.thy "($# n <= $~ $# m) = (n = 0 & m = 0)"; |
799 Goal "($# n <= $~ $# m) = (n = 0 & m = 0)"; |
800 by (safe_tac HOL_cs); |
800 by (safe_tac HOL_cs); |
801 by (Simp_tac 3); |
801 by (Simp_tac 3); |
802 by (dtac (zle_zminus RS iffD1) 2); |
802 by (dtac (zle_zminus RS iffD1) 2); |
803 by (ALLGOALS(dtac (negative_zle_0 RSN(2,zle_trans)))); |
803 by (ALLGOALS(dtac (negative_zle_0 RSN(2,zle_trans)))); |
804 by (ALLGOALS Asm_full_simp_tac); |
804 by (ALLGOALS Asm_full_simp_tac); |
805 qed "znat_zle_znegative"; |
805 qed "znat_zle_znegative"; |
806 |
806 |
807 goal Integ.thy "~($# n < $~ $# Suc m)"; |
807 Goal "~($# n < $~ $# Suc m)"; |
808 by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); |
808 by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); |
809 by (dtac (znat_zle_znegative RS iffD1) 1); |
809 by (dtac (znat_zle_znegative RS iffD1) 1); |
810 by (safe_tac HOL_cs); |
810 by (safe_tac HOL_cs); |
811 by (dtac (zless_zminus RS iffD1) 1); |
811 by (dtac (zless_zminus RS iffD1) 1); |
812 by (Asm_full_simp_tac 1); |
812 by (Asm_full_simp_tac 1); |
813 qed "not_znat_zless_negative"; |
813 qed "not_znat_zless_negative"; |
814 |
814 |
815 goal Integ.thy "($~ $# n = $# m) = (n = 0 & m = 0)"; |
815 Goal "($~ $# n = $# m) = (n = 0 & m = 0)"; |
816 by (rtac iffI 1); |
816 by (rtac iffI 1); |
817 by (rtac (znat_zle_znegative RS iffD1) 1); |
817 by (rtac (znat_zle_znegative RS iffD1) 1); |
818 by (dtac sym 1); |
818 by (dtac sym 1); |
819 by (ALLGOALS Asm_simp_tac); |
819 by (ALLGOALS Asm_simp_tac); |
820 qed "negative_eq_positive"; |
820 qed "negative_eq_positive"; |
821 |
821 |
822 Addsimps [zminus_zless_zminus, zminus_zle_zminus, |
822 Addsimps [zminus_zless_zminus, zminus_zle_zminus, |
823 negative_eq_positive, not_znat_zless_negative]; |
823 negative_eq_positive, not_znat_zless_negative]; |
824 |
824 |
825 goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)"; |
825 Goalw [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)"; |
826 by Auto_tac; |
826 by Auto_tac; |
827 qed "znegative_less_0"; |
827 qed "znegative_less_0"; |
828 |
828 |
829 goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)"; |
829 Goalw [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)"; |
830 by (stac znegative_less_0 1); |
830 by (stac znegative_less_0 1); |
831 by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); |
831 by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); |
832 qed "not_znegative_ge_0"; |
832 qed "not_znegative_ge_0"; |
833 |
833 |
834 goal Integ.thy "!! x. znegative x ==> ? n. x = $~ $# Suc n"; |
834 Goal "!! x. znegative x ==> ? n. x = $~ $# Suc n"; |
835 by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); |
835 by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); |
836 by (etac exE 1); |
836 by (etac exE 1); |
837 by (rtac exI 1); |
837 by (rtac exI 1); |
838 by (dres_inst_tac [("f","(% z. z + $~ $# Suc n )")] arg_cong 1); |
838 by (dres_inst_tac [("f","(% z. z + $~ $# Suc n )")] arg_cong 1); |
839 by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); |
839 by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); |
840 qed "znegativeD"; |
840 qed "znegativeD"; |
841 |
841 |
842 goal Integ.thy "!! x. ~znegative x ==> ? n. x = $# n"; |
842 Goal "!! x. ~znegative x ==> ? n. x = $# n"; |
843 by (dtac (not_znegative_ge_0 RS iffD1) 1); |
843 by (dtac (not_znegative_ge_0 RS iffD1) 1); |
844 by (dtac zle_imp_zless_or_eq 1); |
844 by (dtac zle_imp_zless_or_eq 1); |
845 by (etac disjE 1); |
845 by (etac disjE 1); |
846 by (dtac zless_eq_zadd_Suc 1); |
846 by (dtac zless_eq_zadd_Suc 1); |
847 by Auto_tac; |
847 by Auto_tac; |