equal
deleted
inserted
replaced
484 lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True" |
484 lemma finite_code [code]: "finite (A \<Colon> 'a set) \<longleftrightarrow> True" |
485 by simp |
485 by simp |
486 |
486 |
487 end |
487 end |
488 |
488 |
489 instance unit :: finite proof |
|
490 qed (simp add: UNIV_unit) |
|
491 |
|
492 instance bool :: finite proof |
|
493 qed (simp add: UNIV_bool) |
|
494 |
|
495 instance prod :: (finite, finite) finite proof |
489 instance prod :: (finite, finite) finite proof |
496 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) |
490 qed (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) |
497 |
|
498 lemma finite_option_UNIV [simp]: |
|
499 "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" |
|
500 by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) |
|
501 |
|
502 instance option :: (finite) finite proof |
|
503 qed (simp add: UNIV_option_conv) |
|
504 |
491 |
505 lemma inj_graph: "inj (%f. {(x, y). y = f x})" |
492 lemma inj_graph: "inj (%f. {(x, y). y = f x})" |
506 by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff) |
493 by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff) |
507 |
494 |
508 instance "fun" :: (finite, finite) finite |
495 instance "fun" :: (finite, finite) finite |
517 by (rule finite_subset) |
504 by (rule finite_subset) |
518 show "inj ?graph" by (rule inj_graph) |
505 show "inj ?graph" by (rule inj_graph) |
519 qed |
506 qed |
520 qed |
507 qed |
521 |
508 |
|
509 instance bool :: finite proof |
|
510 qed (simp add: UNIV_bool) |
|
511 |
|
512 instance unit :: finite proof |
|
513 qed (simp add: UNIV_unit) |
|
514 |
522 instance sum :: (finite, finite) finite proof |
515 instance sum :: (finite, finite) finite proof |
523 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) |
516 qed (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) |
|
517 |
|
518 lemma finite_option_UNIV [simp]: |
|
519 "finite (UNIV :: 'a option set) = finite (UNIV :: 'a set)" |
|
520 by (auto simp add: UNIV_option_conv elim: finite_imageD intro: inj_Some) |
|
521 |
|
522 instance option :: (finite) finite proof |
|
523 qed (simp add: UNIV_option_conv) |
524 |
524 |
525 |
525 |
526 subsection {* A basic fold functional for finite sets *} |
526 subsection {* A basic fold functional for finite sets *} |
527 |
527 |
528 text {* The intended behaviour is |
528 text {* The intended behaviour is |