# HG changeset patch
# User bulwahn
# Date 1340633001 -7200
# Node ID 104e5fccea1290131bfaac6e37ca32b2f98000d2
# Parent  f479f36ed2fff30af5666a81d3632a91c8e0aa53
some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing

diff -r f479f36ed2ff -r 104e5fccea12 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Jun 25 16:03:14 2012 +0200
+++ b/src/HOL/Enum.thy	Mon Jun 25 16:03:21 2012 +0200
@@ -784,10 +784,14 @@
 
 subsection {* Further operations on finite types *}
 
-lemma [code]:
+lemma Collect_code[code]:
   "Collect P = set (filter P enum)"
 by (auto simp add: enum_UNIV)
 
+lemma [code]:
+  "Id = image (%x. (x, x)) (set Enum.enum)"
+by (auto intro: imageI in_enum)
+
 lemma tranclp_unfold [code, no_atp]:
   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
 by (simp add: trancl_def)