src/HOL/Enum.thy
changeset 48123 104e5fccea12
parent 47231 3ff8c79a9e2f
child 49948 744934b818c7
equal deleted inserted replaced
48122:f479f36ed2ff 48123:104e5fccea12
   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