equal
deleted
inserted
replaced
782 code_abort enum_the |
782 code_abort enum_the |
783 code_const enum_the (Eval "(fn p => raise Match)") |
783 code_const enum_the (Eval "(fn p => raise Match)") |
784 |
784 |
785 subsection {* Further operations on finite types *} |
785 subsection {* Further operations on finite types *} |
786 |
786 |
787 lemma [code]: |
787 lemma Collect_code[code]: |
788 "Collect P = set (filter P enum)" |
788 "Collect P = set (filter P enum)" |
789 by (auto simp add: enum_UNIV) |
789 by (auto simp add: enum_UNIV) |
|
790 |
|
791 lemma [code]: |
|
792 "Id = image (%x. (x, x)) (set Enum.enum)" |
|
793 by (auto intro: imageI in_enum) |
790 |
794 |
791 lemma tranclp_unfold [code, no_atp]: |
795 lemma tranclp_unfold [code, no_atp]: |
792 "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" |
796 "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}" |
793 by (simp add: trancl_def) |
797 by (simp add: trancl_def) |
794 |
798 |