src/HOL/Library/ExecutableSet.thy

--- a/src/HOL/Library/ExecutableSet.thy	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Jan 17 16:36:57 2006 +0100
@@ -27,6 +27,14 @@
 and gen_set aG i = gen_set' aG i i;
 *}
 
+code_syntax_tyco set
+  ml ("_ list")
+  haskell (atom "[_]")
+
+code_syntax_const "{}"
+  ml (atom "[]")
+  haskell (atom "[]")
+
 consts_code
   "{}"      ("[]")
   "insert"  ("(_ ins _)")
@@ -54,4 +62,121 @@
 fun Ball S P = Library.forall P S;
 *}
 
+code_generate "op mem"
+
+code_primconst "insert"
+  depending_on ("List.const.member")
+ml {*
+fun insert x xs =
+  if List.member x xs then xs
+  else x::xs;
+*}
+haskell {*
+insert x xs =
+  if elem x xs then xs else x:xs
+*}
+
+code_primconst "op Un"
+  depending_on ("List.const.insert")
+ml {*
+fun union xs [] = xs
+  | union [] ys = ys
+  | union (x::xs) ys = union xs (insert x ys);
+*}
+haskell {*
+union xs [] = xs
+union [] ys = ys
+union (x:xs) ys = union xs (insert x ys)
+*}
+
+code_primconst "op Int"
+  depending_on ("List.const.member")
+ml {*
+fun inter [] ys = []
+  | inter (x::xs) ys =
+      if List.member x ys
+      then x :: inter xs ys
+      else inter xs ys;
+*}
+haskell {*
+inter [] ys = []
+inter (x:xs) ys =
+  if elem x ys
+  then x : inter xs ys
+  else inter xs ys
+*}
+
+code_primconst  "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ml {*
+fun op_minus ys [] = ys
+  | op_minus ys (x::xs) =
+      let
+        fun minus [] x = []
+          | minus (y::ys) x = if x = y then ys else y :: minus ys x
+      in
+        op_minus (minus ys x) xs
+      end;
+*}
+haskell {*
+op_minus ys [] = ys
+op_minus ys (x:xs) = op_minus (minus ys x) xs where
+  minus [] x = []
+  minus (y:ys) x = if x = y then ys else y : minus ys x
+*}
+
+code_primconst "image"
+  depending_on ("List.const.insert")
+ml {*
+fun image f =
+  let
+    fun img xs [] = xs
+      | img xs (y::ys) = img (insert (f y) xs) ys;
+  in img [] end;;
+*}
+haskell {*
+image f = img [] where
+  img xs [] = xs
+  img xs (y:ys) = img (insert (f y) xs) ys;
+*}
+
+code_primconst "UNION"
+  depending_on ("List.const.union")
+ml {*
+fun UNION [] f = []
+  | UNION (x::xs) f = union (f x) (UNION xs);
+*}
+haskell {*
+UNION [] f = []
+UNION (x:xs) f = union (f x) (UNION xs);
+*}
+
+code_primconst "INTER"
+  depending_on ("List.const.inter")
+ml {*
+fun INTER [] f = []
+  | INTER (x::xs) f = inter (f x) (INTER xs);
+*}
+haskell {*
+INTER [] f = []
+INTER (x:xs) f = inter (f x) (INTER xs);
+*}
+
+code_primconst "Ball"
+ml {*
+fun Ball [] f = true
+  | Ball (x::xs) f = f x andalso Ball f xs;
+*}
+haskell {*
+Ball = all . flip
+*}
+
+code_primconst "Bex"
+ml {*
+fun Bex [] f = false
+  | Bex (x::xs) f = f x orelse Bex f xs;
+*}
+haskell {*
+Ball = any . flip
+*}
+
 end