109 |
109 |
110 (* finite B ==> finite (B - Ba) *) |
110 (* finite B ==> finite (B - Ba) *) |
111 bind_thm ("finite_Diff", Diff_subset RS finite_subset); |
111 bind_thm ("finite_Diff", Diff_subset RS finite_subset); |
112 Addsimps [finite_Diff]; |
112 Addsimps [finite_Diff]; |
113 |
113 |
114 Goal "finite(A-{a}) = finite(A)"; |
114 Goal "finite(A - insert a B) = finite(A-B)"; |
115 by (case_tac "a:A" 1); |
115 by(stac Diff_insert 1); |
|
116 by (case_tac "a : A-B" 1); |
116 by (rtac (finite_insert RS sym RS trans) 1); |
117 by (rtac (finite_insert RS sym RS trans) 1); |
117 by (stac insert_Diff 1); |
118 by (stac insert_Diff 1); |
118 by (ALLGOALS Asm_simp_tac); |
119 by (ALLGOALS Asm_full_simp_tac); |
119 qed "finite_Diff_singleton"; |
120 qed "finite_Diff_insert"; |
120 AddIffs [finite_Diff_singleton]; |
121 AddIffs [finite_Diff_insert]; |
|
122 |
|
123 (* lemma merely for classical reasoner *) |
|
124 Goal "finite(A-{}) = finite A"; |
|
125 by (Simp_tac 1); |
|
126 val lemma = result(); |
|
127 AddSIs [lemma RS iffD2]; |
|
128 AddSDs [lemma RS iffD1]; |
121 |
129 |
122 (*Lemma for proving finite_imageD*) |
130 (*Lemma for proving finite_imageD*) |
123 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
131 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
124 by (etac finite_induct 1); |
132 by (etac finite_induct 1); |
125 by (ALLGOALS Asm_simp_tac); |
133 by (ALLGOALS Asm_simp_tac); |
311 Goalw [card_def] "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)"; |
321 Goalw [card_def] "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)"; |
312 by (etac lemma 1); |
322 by (etac lemma 1); |
313 by (assume_tac 1); |
323 by (assume_tac 1); |
314 qed "card_insert_disjoint"; |
324 qed "card_insert_disjoint"; |
315 Addsimps [card_insert_disjoint]; |
325 Addsimps [card_insert_disjoint]; |
|
326 *) |
|
327 |
|
328 val cardR_emptyE = cardR.mk_cases [] "({},n) : cardR"; |
|
329 AddSEs [cardR_emptyE]; |
|
330 val cardR_insertE = cardR.mk_cases [] "(insert a A,n) : cardR"; |
|
331 AddSIs cardR.intrs; |
|
332 |
|
333 Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)"; |
|
334 be cardR.induct 1; |
|
335 by(Blast_tac 1); |
|
336 by(Blast_tac 1); |
|
337 qed "cardR_SucD"; |
|
338 |
|
339 Goal "(A,m): cardR ==> (!n a. m = Suc n --> a:A --> (A-{a},n) : cardR)"; |
|
340 be cardR.induct 1; |
|
341 by(Auto_tac); |
|
342 by(asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1); |
|
343 by(Auto_tac); |
|
344 by(forward_tac [cardR_SucD] 1); |
|
345 by(Blast_tac 1); |
|
346 val lemma = result(); |
|
347 |
|
348 Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR"; |
|
349 bd lemma 1; |
|
350 by(Asm_full_simp_tac 1); |
|
351 val lemma = result(); |
|
352 |
|
353 Goal "(A,m): cardR ==> (!n. (A,n) : cardR --> n=m)"; |
|
354 be cardR.induct 1; |
|
355 by(safe_tac (claset() addSEs [cardR_insertE])); |
|
356 by(rename_tac "B b m" 1); |
|
357 by(case_tac "a = b" 1); |
|
358 by(subgoal_tac "A = B" 1); |
|
359 by(blast_tac (claset() addEs [equalityE]) 2); |
|
360 by(Blast_tac 1); |
|
361 by(subgoal_tac "? C. A = insert b C & B = insert a C" 1); |
|
362 by(res_inst_tac [("x","A Int B")] exI 2); |
|
363 by(blast_tac (claset() addEs [equalityE]) 2); |
|
364 by(forw_inst_tac [("A","B")] cardR_SucD 1); |
|
365 by(blast_tac (claset() addDs [lemma]) 1); |
|
366 qed_spec_mp "cardR_determ"; |
|
367 |
|
368 Goal "(A,n) : cardR ==> finite(A)"; |
|
369 by (etac cardR.induct 1); |
|
370 by Auto_tac; |
|
371 qed "cardR_imp_finite"; |
|
372 |
|
373 Goal "finite(A) ==> EX n. (A, n) : cardR"; |
|
374 by (etac finite_induct 1); |
|
375 by Auto_tac; |
|
376 qed "finite_imp_cardR"; |
|
377 |
|
378 Goalw [card_def] "(A,n) : cardR ==> card A = n"; |
|
379 by (blast_tac (claset() addIs [cardR_determ]) 1); |
|
380 qed "card_equality"; |
|
381 |
|
382 Goalw [card_def] "card {} = 0"; |
|
383 by (Blast_tac 1); |
|
384 qed "card_empty"; |
|
385 Addsimps [card_empty]; |
|
386 |
|
387 Goal "x ~: A ==> \ |
|
388 \ ((insert x A, n) : cardR) = \ |
|
389 \ (EX m. (A, m) : cardR & n = Suc m)"; |
|
390 by Auto_tac; |
|
391 by (res_inst_tac [("A1", "A")] (finite_imp_cardR RS exE) 1); |
|
392 by (force_tac (claset() addDs [cardR_imp_finite], simpset()) 1); |
|
393 by (blast_tac (claset() addIs [cardR_determ]) 1); |
|
394 val lemma = result(); |
|
395 |
|
396 Goalw [card_def] |
|
397 "[| finite A; x ~: A |] ==> card (insert x A) = Suc(card A)"; |
|
398 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
|
399 by (rtac select_equality 1); |
|
400 by (auto_tac (claset() addIs [finite_imp_cardR], |
|
401 simpset() addcongs [conj_cong] |
|
402 addsimps [symmetric card_def, |
|
403 card_equality])); |
|
404 qed "card_insert_disjoint"; |
|
405 Addsimps [card_insert_disjoint]; |
|
406 |
|
407 (* Delete rules to do with cardR relation: obsolete *) |
|
408 Delrules [cardR_emptyE]; |
|
409 Delrules cardR.intrs; |
|
410 |
|
411 Goal "finite A ==> card(insert x A) = (if x:A then card A else Suc(card(A)))"; |
|
412 by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); |
|
413 qed "card_insert_if"; |
|
414 |
|
415 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A"; |
|
416 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); |
|
417 by (assume_tac 1); |
|
418 by (Asm_simp_tac 1); |
|
419 qed "card_Suc_Diff1"; |
|
420 |
|
421 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))"; |
|
422 by (asm_simp_tac (simpset() addsimps [card_insert_if,card_Suc_Diff1]) 1); |
|
423 qed "card_insert"; |
316 |
424 |
317 Goal "finite A ==> card A <= card (insert x A)"; |
425 Goal "finite A ==> card A <= card (insert x A)"; |
318 by (case_tac "x: A" 1); |
426 by (asm_simp_tac (simpset() addsimps [card_insert_if]) 1); |
319 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]))); |
|
320 qed "card_insert_le"; |
427 qed "card_insert_le"; |
321 |
428 |
322 Goal "finite A ==> !B. B <= A --> card(B) <= card(A)"; |
429 Goal "finite A ==> !B. B <= A --> card(B) <= card(A)"; |
323 by (etac finite_induct 1); |
430 by (etac finite_induct 1); |
324 by (Simp_tac 1); |
431 by (Simp_tac 1); |
355 (asm_simp_tac |
462 (asm_simp_tac |
356 (simpset() addsimps [add_commute, not_less_iff_le, |
463 (simpset() addsimps [add_commute, not_less_iff_le, |
357 add_diff_inverse, card_mono, finite_subset]))); |
464 add_diff_inverse, card_mono, finite_subset]))); |
358 qed "card_Diff_subset"; |
465 qed "card_Diff_subset"; |
359 |
466 |
360 Goal "[| finite A; x: A |] ==> Suc(card(A-{x})) = card A"; |
|
361 by (res_inst_tac [("t", "A")] (insert_Diff RS subst) 1); |
|
362 by (assume_tac 1); |
|
363 by (Asm_simp_tac 1); |
|
364 qed "card_Suc_Diff"; |
|
365 |
|
366 Goal "[| finite A; x: A |] ==> card(A-{x}) < card A"; |
467 Goal "[| finite A; x: A |] ==> card(A-{x}) < card A"; |
367 by (rtac Suc_less_SucD 1); |
468 by (rtac Suc_less_SucD 1); |
368 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1); |
469 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); |
369 qed "card_Diff"; |
470 qed "card_Diff1_less"; |
370 |
471 |
371 Goal "finite A ==> card(A-{x}) <= card A"; |
472 Goal "finite A ==> card(A-{x}) <= card A"; |
372 by (case_tac "x: A" 1); |
473 by (case_tac "x: A" 1); |
373 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff, less_imp_le]))); |
474 by (ALLGOALS (asm_simp_tac (simpset() addsimps [card_Diff1_less, less_imp_le]))); |
374 qed "card_Diff_le"; |
475 qed "card_Diff1_le"; |
375 |
476 |
376 |
477 Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)"; |
377 (*** Cardinality of the Powerset ***) |
478 by (etac finite_induct 1); |
378 |
479 by (Simp_tac 1); |
379 Goal "finite A ==> card(insert x A) = Suc(card(A-{x}))"; |
480 by (Clarify_tac 1); |
380 by (case_tac "x:A" 1); |
481 by (case_tac "x:A" 1); |
381 by (ALLGOALS |
482 (*1*) |
382 (asm_simp_tac (simpset() addsimps [card_Suc_Diff, insert_absorb]))); |
483 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); |
383 qed "card_insert"; |
484 by (Clarify_tac 1); |
|
485 by (rotate_tac ~3 1); |
|
486 by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1); |
|
487 by (Blast_tac 1); |
|
488 (*2*) |
|
489 by (eres_inst_tac [("P","?a<?b")] notE 1); |
|
490 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1); |
|
491 by (case_tac "A=F" 1); |
|
492 by (ALLGOALS Asm_simp_tac); |
|
493 qed_spec_mp "psubset_card" ; |
|
494 |
|
495 Goal "[| finite B; A <= B; card A = card B |] ==> A = B"; |
|
496 by (case_tac "A < B" 1); |
|
497 by ((dtac psubset_card 1) THEN (atac 1)); |
|
498 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [psubset_eq]))); |
|
499 qed "card_seteq"; |
|
500 |
|
501 Goal "[| finite B; A <= B; card A < card B |] ==> A < B"; |
|
502 by (etac psubsetI 1); |
|
503 by (Blast_tac 1); |
|
504 qed "card_psubset"; |
|
505 |
|
506 (*** Cardinality of image ***) |
|
507 |
|
508 Goal "finite A ==> card (f `` A) <= card A"; |
|
509 by (etac finite_induct 1); |
|
510 by (Simp_tac 1); |
|
511 by (asm_simp_tac (simpset() addsimps [finite_imageI,card_insert_if]) 1); |
|
512 qed "card_image_le"; |
384 |
513 |
385 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A"; |
514 Goal "finite(A) ==> inj_on f A --> card (f `` A) = card A"; |
386 by (etac finite_induct 1); |
515 by (etac finite_induct 1); |
387 by (ALLGOALS Asm_simp_tac); |
516 by (ALLGOALS Asm_simp_tac); |
388 by Safe_tac; |
517 by Safe_tac; |
391 by (stac card_insert_disjoint 1); |
520 by (stac card_insert_disjoint 1); |
392 by (etac finite_imageI 1); |
521 by (etac finite_imageI 1); |
393 by (Blast_tac 1); |
522 by (Blast_tac 1); |
394 by (Blast_tac 1); |
523 by (Blast_tac 1); |
395 qed_spec_mp "card_image"; |
524 qed_spec_mp "card_image"; |
|
525 |
|
526 Goal "[| finite A; f``A <= A; inj_on f A |] ==> f``A = A"; |
|
527 by (REPEAT (ares_tac [card_seteq,card_image] 1)); |
|
528 qed "endo_inj_surj"; |
|
529 |
|
530 (*** Cardinality of the Powerset ***) |
396 |
531 |
397 Goal "finite A ==> card (Pow A) = 2 ^ card A"; |
532 Goal "finite A ==> card (Pow A) = 2 ^ card A"; |
398 by (etac finite_induct 1); |
533 by (etac finite_induct 1); |
399 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); |
534 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert]))); |
400 by (stac card_Un_disjoint 1); |
535 by (stac card_Un_disjoint 1); |
405 by (blast_tac (claset() addSEs [equalityE]) 1); |
540 by (blast_tac (claset() addSEs [equalityE]) 1); |
406 qed "card_Pow"; |
541 qed "card_Pow"; |
407 Addsimps [card_Pow]; |
542 Addsimps [card_Pow]; |
408 |
543 |
409 |
544 |
410 (*Proper subsets*) |
|
411 Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)"; |
|
412 by (etac finite_induct 1); |
|
413 by (Simp_tac 1); |
|
414 by (Clarify_tac 1); |
|
415 by (case_tac "x:A" 1); |
|
416 (*1*) |
|
417 by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); |
|
418 by (Clarify_tac 1); |
|
419 by (rotate_tac ~3 1); |
|
420 by (asm_full_simp_tac (simpset() addsimps [finite_subset]) 1); |
|
421 by (Blast_tac 1); |
|
422 (*2*) |
|
423 by (eres_inst_tac [("P","?a<?b")] notE 1); |
|
424 by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff]) 1); |
|
425 by (case_tac "A=F" 1); |
|
426 by (ALLGOALS Asm_simp_tac); |
|
427 qed_spec_mp "psubset_card" ; |
|
428 |
|
429 |
|
430 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
545 (*Relates to equivalence classes. Based on a theorem of F. Kammueller's. |
431 The "finite C" premise is redundant*) |
546 The "finite C" premise is redundant*) |
432 Goal "finite C ==> finite (Union C) --> \ |
547 Goal "finite C ==> finite (Union C) --> \ |
433 \ (! c : C. k dvd card c) --> \ |
548 \ (! c : C. k dvd card c) --> \ |
434 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
549 \ (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \ |
506 by (subgoal_tac "Aa = insert xb Ab - {xa}" 1); |
621 by (subgoal_tac "Aa = insert xb Ab - {xa}" 1); |
507 by (blast_tac (claset() addEs [equalityE]) 2); |
622 by (blast_tac (claset() addEs [equalityE]) 2); |
508 (** LEVEL 20 **) |
623 (** LEVEL 20 **) |
509 by (subgoal_tac "card Aa <= card Ab" 1); |
624 by (subgoal_tac "card Aa <= card Ab" 1); |
510 by (rtac (Suc_le_mono RS subst) 2); |
625 by (rtac (Suc_le_mono RS subst) 2); |
511 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 2); |
626 by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 2); |
512 by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] |
627 by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] |
513 (finite_imp_foldSet RS exE) 1); |
628 (finite_imp_foldSet RS exE) 1); |
514 by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1); |
629 by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1); |
515 by (forward_tac [Diff_foldSet] 1 THEN assume_tac 1); |
630 by (forward_tac [Diff1_foldSet] 1 THEN assume_tac 1); |
516 by (subgoal_tac "ya = f xb x" 1); |
631 by (subgoal_tac "ya = f xb x" 1); |
517 by (Blast_tac 2); |
632 by (Blast_tac 2); |
518 by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1); |
633 by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1); |
519 by (Asm_full_simp_tac 2); |
634 by (Asm_full_simp_tac 2); |
520 by (subgoal_tac "yb = f xa x" 1); |
635 by (subgoal_tac "yb = f xa x" 1); |
521 by (blast_tac (claset() addDs [Diff_foldSet]) 2); |
636 by (blast_tac (claset() addDs [Diff1_foldSet]) 2); |
522 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); |
637 by (asm_simp_tac (simpset() addsimps [f_lcomm]) 1); |
523 val lemma = result(); |
638 val lemma = result(); |
524 |
639 |
525 |
640 |
526 Goal "[| (A, x) : foldSet f e; (A, y) : foldSet f e |] ==> y=x"; |
641 Goal "[| (A, x) : foldSet f e; (A, y) : foldSet f e |] ==> y=x"; |
533 |
648 |
534 Goalw [fold_def] "fold f e {} = e"; |
649 Goalw [fold_def] "fold f e {} = e"; |
535 by (Blast_tac 1); |
650 by (Blast_tac 1); |
536 qed "fold_empty"; |
651 qed "fold_empty"; |
537 Addsimps [fold_empty]; |
652 Addsimps [fold_empty]; |
|
653 |
538 |
654 |
539 Goal "x ~: A ==> \ |
655 Goal "x ~: A ==> \ |
540 \ ((insert x A, v) : foldSet f e) = \ |
656 \ ((insert x A, v) : foldSet f e) = \ |
541 \ (EX y. (A, y) : foldSet f e & v = f x y)"; |
657 \ (EX y. (A, y) : foldSet f e & v = f x y)"; |
542 by Auto_tac; |
658 by Auto_tac; |
543 by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1); |
659 by (res_inst_tac [("A1", "A"), ("f1","f")] (finite_imp_foldSet RS exE) 1); |
544 by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1); |
660 by (force_tac (claset() addDs [foldSet_imp_finite], simpset()) 1); |
545 by (blast_tac (claset() addIs [foldSet_determ]) 1); |
661 by (blast_tac (claset() addIs [foldSet_determ]) 1); |
546 val lemma = result(); |
662 val lemma = result(); |
547 |
|
548 |
663 |
549 Goalw [fold_def] |
664 Goalw [fold_def] |
550 "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)"; |
665 "[| finite A; x ~: A |] ==> fold f e (insert x A) = f x (fold f e A)"; |
551 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
666 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
552 by (rtac select_equality 1); |
667 by (rtac select_equality 1); |