src/HOL/Enum.thy
changeset 50567 768a3fbe4149
parent 49972 f11f8905d9fd
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Enum.thy	Sun Dec 16 14:19:08 2012 +0100
     1.2 +++ b/src/HOL/Enum.thy	Sun Dec 16 18:07:29 2012 +0100
     1.3 @@ -60,6 +60,10 @@
     1.4    "Collect P = set (filter P enum)"
     1.5    by (simp add: enum_UNIV)
     1.6  
     1.7 +lemma vimage_code [code]:
     1.8 +  "f -` B = set (filter (%x. f x : B) enum_class.enum)"
     1.9 +  unfolding vimage_def Collect_code ..
    1.10 +
    1.11  definition card_UNIV :: "'a itself \<Rightarrow> nat"
    1.12  where
    1.13    [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"