some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
authorbulwahn
Mon Jun 25 16:03:21 2012 +0200 (2012-06-25)
changeset 48123104e5fccea12
parent 48122 f479f36ed2ff
child 48128 bf172a5929bb
some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
src/HOL/Enum.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Jun 25 16:03:14 2012 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Jun 25 16:03:21 2012 +0200
     1.3 @@ -784,10 +784,14 @@
     1.4  
     1.5  subsection {* Further operations on finite types *}
     1.6  
     1.7 -lemma [code]:
     1.8 +lemma Collect_code[code]:
     1.9    "Collect P = set (filter P enum)"
    1.10  by (auto simp add: enum_UNIV)
    1.11  
    1.12 +lemma [code]:
    1.13 +  "Id = image (%x. (x, x)) (set Enum.enum)"
    1.14 +by (auto intro: imageI in_enum)
    1.15 +
    1.16  lemma tranclp_unfold [code, no_atp]:
    1.17    "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
    1.18  by (simp add: trancl_def)