providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
authorbulwahn
Sun Dec 16 18:07:29 2012 +0100 (2012-12-16)
changeset 50567768a3fbe4149
parent 50563 3a4785d64ecb
child 50568 ee090b5712f3
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
src/HOL/Enum.thy
     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)"