diff -r 2b58b308300c -r cf398bb8a8be src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Nov 15 17:05:43 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Nov 15 17:05:44 2006 +0100
@@ -13,20 +13,44 @@
 
 instance set :: (eq) eq ..
 
+definition
+  minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  "minus_set xs ys = ys - xs"
+
+lemma [code inline]:
+  "op - = (\<lambda>xs ys. minus_set ys xs)"
+  unfolding minus_set_def ..
+
+definition
+  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  subset_def: "subset = op \<subseteq>"
+
+lemmas [symmetric, code inline] = subset_def
+
 lemma [code target: Set]:
-  "(A = B) \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)"
+  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   by blast
 
 lemma [code func]:
-  "Code_Generator.eq A B \<longleftrightarrow> (A \<subseteq> B \<and> B \<subseteq> A)"
-  unfolding eq_def by blast
+  "Code_Generator.eq A B \<longleftrightarrow> subset A B \<and> subset B A"
+  unfolding eq_def subset_def by blast
+
+lemma [code func]:
+  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+  unfolding subset_def Set.subset_def ..
 
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
 
+definition
+  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  filter_set_def: "filter_set P xs = {x\<in>xs. P x}"
 
-section {* HOL definitions *}
+lemmas [symmetric, code inline] = filter_set_def
+
+
+section {* Operations on lists *}
 
 subsection {* Basic definitions *}
 
@@ -169,12 +193,12 @@
 lemma iso_remove1:
   assumes distnct: "distinct xs"
   shows "set (remove1 x xs) = set xs - {x}"
-using distnct set_remove1_eq by auto
+  using distnct set_remove1_eq by auto
 
 lemma iso_union:
   "set (unionl xs ys) = set xs \<union> set ys"
   unfolding unionl_def
- by (induct xs arbitrary: ys) (simp_all add: iso_insert)
+  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
 
 lemma iso_intersect:
   "set (intersect xs ys) = set xs \<inter> set ys"
@@ -183,18 +207,10 @@
 lemma iso_subtract:
   fixes ys
   assumes distnct: "distinct ys"
-  shows "set (subtract xs ys) = set ys - set xs"
+  shows "set (subtract xs ys) = minus_set (set xs) (set ys)"
   and "distinct (subtract xs ys)"
-unfolding subtract_def using distnct by (induct xs arbitrary: ys) (simp_all, auto)
-
-corollary iso_subtract':
-  fixes xs ys
-  assumes distnct: "distinct xs"
-  shows "set ((flip subtract) xs ys) = set xs - set ys"
-proof -
-  from distnct iso_subtract have "set (subtract ys xs) = set xs - set ys" by auto
-  thus ?thesis unfolding flip_def by auto
-qed
+  unfolding subtract_def minus_set_def
+  using distnct by (induct xs arbitrary: ys) auto
 
 lemma iso_map_distinct:
   "set (map_distinct f xs) = image f (set xs)"
@@ -234,6 +250,9 @@
   "Blex xs f = Bex (set xs) f"
   unfolding Blex_def flip_def by (induct xs) simp_all
 
+lemma iso_filter:
+  "set (filter P xs) = filter_set P (set xs)"
+  unfolding filter_set_def by (induct xs) auto
 
 section {* code generator setup *}
 
@@ -244,6 +263,11 @@
 
 code_modulename SML
   ExecutableSet List
+  Set List
+
+code_modulename Haskell
+  ExecutableSet List
+  Set List
 
 definition [code inline]:
   "empty_list = []"
@@ -257,8 +281,8 @@
 lemma [code func]:
   "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
 
-definition
-  "subtract' = flip subtract"
+lemma [code func]:
+  "minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" ..
 
 lemma [code func]:
   "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
@@ -275,12 +299,15 @@
 lemma [code func]:
   "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
 
+lemma [code func]:
+  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
+
 code_abstype "'a set" "'a list" where
   "{}" \<equiv> empty_list
   insert \<equiv> insertl
   "op \<union>" \<equiv> unionl
   "op \<inter>" \<equiv> intersect
-  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
+  minus_set \<equiv> subtract
   image \<equiv> map_distinct
   Union \<equiv> unions
   Inter \<equiv> intersects
@@ -288,9 +315,10 @@
   INTER \<equiv> map_inter
   Ball \<equiv> Blall
   Bex \<equiv> Blex
+  filter_set \<equiv> filter
 
-code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  image Union Inter UNION INTER Ball Bex (SML -)
+code_gen "{}" insert "op \<union>" "op \<inter>" minus_set
+  image Union Inter UNION INTER Ball Bex filter_set (SML -)
 
 
 subsection {* type serializations *}
@@ -325,5 +353,6 @@
   "INTER"   ("{*map_inter*}")
   "Ball"    ("{*Blall*}")
   "Bex"     ("{*Blex*}")
+  "filter_set" ("{*filter*}")
 
 end