src/HOL/Library/Executable_Set.thy
changeset 29107 e70b9c2bee14
parent 28939 08004ce1b167
child 29110 476c46e99ada
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Thu Dec 11 08:52:50 2008 +0100
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Thu Dec 11 08:53:53 2008 +0100
     1.3 @@ -28,6 +28,10 @@
     1.4  lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
     1.5    unfolding eq_set_def by auto
     1.6  
     1.7 +(* FIXME allow for Stefan's code generator:
     1.8 +declare set_eq_subset[code unfold]
     1.9 +*)
    1.10 +
    1.11  lemma [code]:
    1.12    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    1.13    unfolding bex_triv_one_point1 ..
    1.14 @@ -35,6 +39,8 @@
    1.15  definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.16    "filter_set P xs = {x\<in>xs. P x}"
    1.17  
    1.18 +declare filter_set_def[symmetric, code unfold] 
    1.19 +
    1.20  
    1.21  subsection {* Operations on lists *}
    1.22  
    1.23 @@ -269,5 +275,7 @@
    1.24    Ball ("{*Blall*}")
    1.25    Bex ("{*Blex*}")
    1.26    filter_set ("{*filter*}")
    1.27 +  fold ("{* foldl *}")
    1.28 +
    1.29  
    1.30  end