# HG changeset patch
# User haftmann
# Date 1149598975 -7200
# Node ID ab326de16ad5d7be2fa74847cc05966f57866d38
# Parent  1c788c6974e8b962dc8fecdb70fcf7ffcd7f201e
refined code generation

diff -r 1c788c6974e8 -r ab326de16ad5 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Jun 06 15:02:09 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jun 06 15:02:55 2006 +0200
@@ -51,25 +51,23 @@
 *}
   int ("(_)")
 
-code_primconst nat
-ml {*
-fun nat i = if i < 0 then 0 : IntInf.int else i;
-*}
-haskell {*
-nat i = if i < 0 then 0 else i
-*}
+code_syntax_tyco nat
+  ml (target_atom "{* int *}")
+  haskell (target_atom "{* int *}")
 
-code_syntax_tyco nat
-  ml (target_atom "IntInf.int")
-  haskell (target_atom "Integer")
-
-code_syntax_const "0 :: nat"
-  ml (target_atom "(0:IntInf.int)")
-  haskell (target_atom "0")
-
-code_syntax_const Suc
-  ml (target_atom "(__ + 1)")
-  haskell (target_atom "(__ + 1)")
+code_syntax_const
+  "0 :: nat"
+    ml (target_atom "{* 0 :: int *}")
+    haskell (target_atom "{* 0 :: int *}")
+  Suc
+    ml (target_atom "(__ + 1)")
+    haskell (target_atom "(__ + 1)")
+  nat
+    ml ("{* abs :: int \<Rightarrow> int *}")
+    haskell ("{* abs :: int \<Rightarrow> int *}")
+  int
+    ml ("_")
+    haskell ("_")
 
 text {*
 Case analysis on natural numbers is rephrased using a conditional
@@ -87,8 +85,17 @@
 using their counterparts on the integers:
 *}
 
-lemma [code]: "m - n = nat (int m - int n)" by arith
-lemma [code]: "m + n = nat (int m + int n)" by arith
+declare
+  Nat.plus.simps [code del]
+  Nat.minus.simps [code del]
+  diff_0_eq_0 [code del]
+  diff_Suc_Suc [code del]
+  Nat.times.simps [code del]
+
+lemma [code]: "m + n = nat (int m + int n)"
+  by arith
+lemma [code]: "m - n = nat (int m - int n)"
+  by arith
 lemma [code]: "m * n = nat (int m * int n)"
   by (simp add: zmult_int)
 lemma [code]: "m div n = nat (int m div int n)"
@@ -97,6 +104,10 @@
   by (simp add: zmod_int [symmetric])
 lemma [code]: "(m < n) = (int m < int n)"
   by simp
+lemma [code fun]:
+  "((0::nat) = 0) = True"
+  "(m = n) = (int m = int n)"
+  by simp_all
 
 subsection {* Preprocessors *}
 
@@ -124,8 +135,13 @@
 *}
 
 (*<*)
+
 ML {*
-val Suc_if_eq = thm "Suc_if_eq";
+local
+  val Suc_if_eq = thm "Suc_if_eq";
+  val Suc_clause = thm "Suc_clause";
+  fun contains_suc t = member (op =) (term_consts t) "Suc";
+in
 
 fun remove_suc thy thms =
   let
@@ -162,25 +178,24 @@
           handle THM _ => NONE) thms of
             [] => NONE
           | thps =>
-              let val (ths1, ths2) = ListPair.unzip thps
+              let val (ths1, ths2) = split_list thps
               in SOME (gen_rems eq_thm (thms, th :: ths1) @ ths2) end
       end
   in
-    case Library.get_first mk_thms eqs of
+    case get_first mk_thms eqs of
       NONE => thms
     | SOME x => remove_suc thy x
   end;
 
 fun eqn_suc_preproc thy ths =
-  let val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
+  let
+    val dest = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of
   in
     if forall (can dest) ths andalso
-      exists (fn th => "Suc" mem term_consts (dest th)) ths
+      exists (contains_suc o dest) ths
     then remove_suc thy ths else ths
   end;
 
-val Suc_clause = thm "Suc_clause";
-
 fun remove_suc_clause thy thms =
   let
     val Suc_clause' = Thm.transfer thy Suc_clause;
@@ -203,7 +218,7 @@
               (Drule.instantiate' []
                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
                    abstract_over (Sucv,
-                     HOLogic.dest_Trueprop (prop_of th')))))),
+                     (HOLogic.dest_Trueprop o prop_of) th'))))),
                  SOME (cert v)] Suc_clause'))
             (Thm.forall_intr (cert v) th'))
         in
@@ -213,22 +228,29 @@
   end;
 
 fun clause_suc_preproc thy ths =
-  let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
+  let
+    val dest = fst o HOLogic.dest_mem o ObjectLogic.drop_judgment thy
   in
     if forall (can (dest o concl_of)) ths andalso
-      exists (fn th => "Suc" mem foldr add_term_consts
-        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
+      exists (fn th => member (op =) (foldr add_term_consts
+        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) "Suc") ths
     then remove_suc_clause thy ths else ths
   end;
 
-val suc_preproc_setup =
+end; (*local*)
+
+fun lift_obj_eq f thy =
+  map (fn thm => thm RS meta_eq_to_obj_eq)
+  #> f thy
+  #> map (fn thm => thm RS HOL.eq_reflection)
+*}
+
+setup {*
   Codegen.add_preprocessor eqn_suc_preproc
   #> Codegen.add_preprocessor clause_suc_preproc
-  #> Codegen.add_preprocessor eqn_suc_preproc
-  #> Codegen.add_preprocessor clause_suc_preproc
+  #> CodegenTheorems.add_preproc (lift_obj_eq eqn_suc_preproc)
+  #> CodegenTheorems.add_preproc (lift_obj_eq clause_suc_preproc)
 *}
-
-setup suc_preproc_setup
 (*>*)
 
 end
diff -r 1c788c6974e8 -r ab326de16ad5 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Tue Jun 06 15:02:09 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Tue Jun 06 15:02:55 2006 +0200
@@ -13,6 +13,9 @@
   Actually nothing is proved about the implementation.
 *}
 
+
+section {* HOL definitions *}
+
 datatype erat = Rat bool int int
 
 instance erat :: zero ..
@@ -25,7 +28,7 @@
 
 definition
   norm :: "erat \<Rightarrow> erat"
-  norm_def [simp]: "norm r = (case r of (Rat a p q) \<Rightarrow>
+  norm_def: "norm r = (case r of (Rat a p q) \<Rightarrow>
      if p = 0 then Rat True 0 1
      else
        let
@@ -34,46 +37,70 @@
          m = zgcd (absp, q)
        in Rat (a = (0 <= p)) (absp div m) (q div m))"
   common :: "(int * int) * (int * int) \<Rightarrow> (int * int) * int"
-  common_def [simp]: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
+  common_def: "common r = (case r of ((p1, q1), (p2, q2)) \<Rightarrow>
        let q' = q1 * q2 div int (gcd (nat q1, nat q2))
        in ((p1 * (q' div q1), p2 * (q' div q2)), q'))"
   of_quotient :: "int * int \<Rightarrow> erat"
-  of_quotient_def [simp]: "of_quotient r = (case r of (a, b) \<Rightarrow>
+  of_quotient_def: "of_quotient r = (case r of (a, b) \<Rightarrow>
        norm (Rat True a b))"
   of_rat :: "rat \<Rightarrow> erat"
-  of_rat_def [simp]: "of_rat r = of_quotient (THE s. s : Rep_Rat r)"
+  of_rat_def: "of_rat r = of_quotient (SOME s. s : Rep_Rat r)"
   to_rat :: "erat \<Rightarrow> rat"
-  to_rat_def [simp]: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
+  to_rat_def: "to_rat r = (case r of (Rat a p q) \<Rightarrow>
        if a then Fract p q else Fract (uminus p) q)"
+  eq_rat :: "erat \<Rightarrow> erat \<Rightarrow> bool"
+  "eq_rat r s = (norm r = norm s)"
 
 defs (overloaded)
-  zero_rat_def [simp]: "0 == Rat False 0 1"
-  one_rat_def [simp]: "1 == Rat False 1 1"
-  add_rat_def [simp]: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
+  zero_rat_def: "0 == Rat True 0 1"
+  one_rat_def: "1 == Rat True 1 1"
+  add_rat_def: "r + s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
         let
           ((r1, r2), den) = common ((p1, q1), (p2, q2))
         in let
           num = (if a1 then r1 else -r1) + (if a2 then r2 else -r2)
         in norm (Rat True num den)"
-  uminus_rat_def [simp]: "- r == case r of Rat a p q \<Rightarrow>
+  uminus_rat_def: "- r == case r of Rat a p q \<Rightarrow>
         if p = 0 then Rat a p q
         else Rat (\<not> a) p q"
-  times_rat_def [simp]: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
+  times_rat_def: "r * s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
         norm (Rat (a1 = a2) (p1 * p2) (q1 * q2))"
-  inverse_rat_def [simp]: "inverse r == case r of Rat a p q \<Rightarrow>
+  inverse_rat_def: "inverse r == case r of Rat a p q \<Rightarrow>
         if p = 0 then arbitrary
         else Rat a q p"
-  le_rat_def [simp]: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
+  le_rat_def: "r <= s == case r of Rat a1 p1 q1 \<Rightarrow> case s of Rat a2 p2 q2 \<Rightarrow>
         (\<not> a1 \<and> a2) \<or>
         (\<not> (a1 \<and> \<not> a2) \<and>
           (let
             ((r1, r2), dummy) = common ((p1, q1), (p2, q2))
           in if a1 then r1 <= r2 else r2 <= r1))"
 
+
+section {* type serializations *}
+
+types_code
+  rat ("{*erat*}")
+
 code_syntax_tyco rat
   ml (target_atom "{*erat*}")
   haskell (target_atom "{*erat*}")
 
+
+section {* const serializations *}
+
+consts_code
+  arbitrary :: erat ("raise/ (Fail/ \"non-defined rational number\")")
+  Fract ("{*of_quotient*}")
+  0 :: rat ("{*0::erat*}")
+  1 :: rat ("{*1::erat*}")
+  HOL.plus :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+  uminus :: "rat \<Rightarrow> rat" ("{*uminus :: erat \<Rightarrow> erat*}")
+  HOL.times :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+  inverse :: "rat \<Rightarrow> rat" ("{*inverse :: erat \<Rightarrow> erat*}")
+  divide :: "rat \<Rightarrow> rat \<Rightarrow> rat" ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
+  Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}")
+
 code_syntax_const
   "arbitrary :: erat"
     ml ("raise/ (Fail/ \"non-defined rational number\")")
@@ -89,7 +116,7 @@
     haskell ("{*1::erat*}")
   "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
     ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-    haskell ("{*HOL.plus :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+    haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   "uminus :: rat \<Rightarrow> rat"
     ml ("{*uminus :: erat \<Rightarrow> erat*}")
     haskell ("{*uminus :: erat \<Rightarrow> erat*}")
@@ -105,6 +132,9 @@
   "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
     ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
     haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+  "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
+    ml ("{*eq_rat*}")
+    haskell ("{*eq_rat*}")
 
 end
 
diff -r 1c788c6974e8 -r ab326de16ad5 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Tue Jun 06 15:02:09 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Jun 06 15:02:55 2006 +0200
@@ -9,11 +9,218 @@
 imports Main
 begin
 
-lemma [code target: Set]: "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
+section {* Definitional rewrites *}
+
+lemma [code target: Set]:
+  "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
   by blast
 
 declare bex_triv_one_point1 [symmetric, standard, code]
 
+section {* HOL definitions *}
+
+subsection {* Basic definitions *}
+
+definition
+  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
+  "flip f a b = f b a"
+  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  "member xs x = (x \<in> set xs)"
+  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  "insertl x xs = (if member xs x then xs else x#xs)"
+
+lemma
+  [code target: List]: "member [] y = False"
+  and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)"
+unfolding member_def by (induct xs) simp_all
+
+consts
+  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+primrec
+  "drop_first f [] = []"
+  "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
+declare drop_first.simps [code del]
+declare drop_first.simps [code target: List]
+
+declare remove1.simps [code del]
+lemma [code target: List]:
+  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
+proof (cases "member xs x")
+  case False thus ?thesis unfolding member_def by (induct xs) auto
+next
+  case True
+  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
+  with True show ?thesis by simp
+qed
+
+lemma member_nil [simp]:
+  "member [] = (\<lambda>x. False)"
+proof
+  fix x
+  show "member [] x = False" unfolding member_def by simp
+qed
+
+lemma member_insertl [simp]:
+  "x \<in> set (insertl x xs)"
+  unfolding insertl_def member_def mem_iff by simp
+
+lemma insertl_member [simp]:
+  fixes xs x
+  assumes member: "member xs x"
+  shows "insertl x xs = xs"
+  using member unfolding insertl_def by simp
+
+lemma insertl_not_member [simp]:
+  fixes xs x
+  assumes member: "\<not> (member xs x)"
+  shows "insertl x xs = x # xs"
+  using member unfolding insertl_def by simp
+
+lemma foldr_remove1_empty [simp]:
+  "foldr remove1 xs [] = []"
+  by (induct xs) simp_all
+
+
+subsection {* Derived definitions *}
+
+consts
+  unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+  unions :: "'a list list \<Rightarrow> 'a list"
+  intersects :: "'a list list \<Rightarrow> 'a list"
+
+function
+  "unionl [] ys = ys"
+  "unionl xs ys = foldr insertl xs ys"
+  by pat_completeness auto
+termination unionl by (auto_term "{}")
+lemmas unionl_def = unionl.simps(2)
+
+function
+  "intersect [] ys = []"
+  "intersect xs [] = []"
+  "intersect xs ys = filter (member xs) ys"
+  by pat_completeness simp_all
+termination intersect by (auto_term "{}")
+lemmas intersect_def = intersect.simps(3)
+
+function
+  "subtract [] ys = ys"
+  "subtract xs [] = []"
+  "subtract xs ys = foldr remove1 xs ys"
+  by pat_completeness simp_all
+termination subtract by (auto_term "{}")
+lemmas subtract_def = subtract.simps(3)
+
+function
+  "map_distinct f [] = []"
+  "map_distinct f xs = foldr (insertl o f) xs []"
+  by pat_completeness simp_all
+termination map_distinct by (auto_term "{}")
+lemmas map_distinct_def = map_distinct.simps(2)
+
+function
+  "unions [] = []"
+  "unions xs = foldr unionl xs []"
+  by pat_completeness simp_all
+termination unions by (auto_term "{}")
+lemmas unions_def = unions.simps(2)
+
+primrec
+  "intersects (x#xs) = foldr intersect xs x"
+
+definition
+  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
+  "map_union xs f = unions (map f xs)"
+  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
+  "map_inter xs f = intersects (map f xs)"
+
+
+section {* Isomorphism proofs *}
+
+lemma iso_member:
+  "member xs x = (x \<in> set xs)"
+  unfolding member_def mem_iff ..
+
+lemma iso_insert:
+  "set (insertl x xs) = insert x (set xs)"
+  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
+
+lemma iso_remove1:
+  assumes distnct: "distinct xs"
+  shows "set (remove1 x xs) = set xs - {x}"
+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 fixing: ys) (simp_all add: iso_insert)
+
+lemma iso_intersect:
+  "set (intersect xs ys) = set xs \<inter> set ys"
+  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
+
+lemma iso_subtract:
+  fixes ys
+  assumes distnct: "distinct ys"
+  shows "set (subtract xs ys) = set ys - set xs"
+  and "distinct (subtract xs ys)"
+unfolding subtract_def using distnct by (induct xs fixing: 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
+
+lemma iso_map_distinct:
+  "set (map_distinct f xs) = image f (set xs)"
+  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
+
+lemma iso_unions:
+  "set (unions xss) = \<Union> set (map set xss)"
+unfolding unions_def proof (induct xss)
+  case Nil show ?case by simp
+next
+  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
+qed
+
+lemma iso_intersects:
+  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
+  by (induct xss) (simp_all add: Int_def iso_member, auto)
+
+lemma iso_UNION:
+  "set (map_union xs f) = UNION (set xs) (set o f)"
+  unfolding map_union_def iso_unions by simp
+
+lemma iso_INTER:
+  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
+  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
+
+definition
+  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  "Blall = flip list_all"
+  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  "Blex = flip list_ex"
+
+lemma iso_Ball:
+  "Blall xs f = Ball (set xs) f"
+  unfolding Blall_def flip_def by (induct xs) simp_all
+
+lemma iso_Bex:
+  "Blex xs f = Bex (set xs) f"
+  unfolding Blex_def flip_def by (induct xs) simp_all
+
+
+section {* code generator setup *}
+
+subsection {* type serializations *}
+
 types_code
   set ("_ list")
 attach (term_of) {*
@@ -31,101 +238,65 @@
   ml ("_ list")
   haskell (target_atom "[_]")
 
-code_syntax_const "{}"
-  ml (target_atom "[]")
-  haskell (target_atom "[]")
+
+subsection {* const serializations *}
 
 consts_code
   "{}"      ("[]")
-  "insert"  ("(_ ins _)")
-  "op Un"   ("(_ union _)")
-  "op Int"  ("(_ inter _)")
-  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("(_ \\\\ _)")
-  "image"   ("\<module>image")
-attach {*
-fun image f S = distinct (map f S);
-*}
-  "UNION"   ("\<module>UNION")
-attach {*
-fun UNION S f = Library.foldr Library.union (map f S, []);
-*}
-  "INTER"   ("\<module>INTER")
-attach {*
-fun INTER S f = Library.foldr1 Library.inter (map f S);
-*}
-  "Bex"     ("\<module>Bex")
-attach {*
-fun Bex S P = Library.exists P S;
-*}
-  "Ball"     ("\<module>Ball")
-attach {*
-fun Ball S P = Library.forall P S;
-*}
+  "insert"  ("{*insertl*}")
+  "op Un"   ("{*unionl*}")
+  "op Int"  ("{*intersect*}")
+  "HOL.minus" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+            ("{*flip subtract*}")
+  "image"   ("{*map_distinct*}")
+  "Union"   ("{*unions*}")
+  "Inter"   ("{*intersects*}")
+  "UNION"   ("{*map_union*}")
+  "INTER"   ("{*map_inter*}")
+  "Ball"    ("{*Blall*}")
+  "Bex"     ("{*Blex*}")
 
-consts
-  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
-  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
-  insert_ :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  remove :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
-  inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-defs
-  flip_def: "flip f a b == f b a"
-  member_def: "member xs x == x mem xs"
-  insert_def: "insert_ x xs == if member xs x then xs else x#xs"
-
-primrec
-  "remove x [] = []"
-  "remove x (y#ys) = (if x = y then ys else y # remove x ys)"
-
-primrec
-  "inter [] ys = []"
-  "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
+code_alias
+  "ExecutableSet.member" "List.member"
+  "ExecutableSet.insertl" "List.insertl"
+  "ExecutableSet.drop_first" "List.drop_first"
 
-code_syntax_const insert
-  ml ("{*insert_*}")
-  haskell ("{*insert_*}")
-
-code_syntax_const "op Un"
-  ml ("{*foldr insert_*}")
-  haskell ("{*foldr insert_*}")
-
-code_syntax_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  ml ("{*(flip o foldr) remove*}")
-  haskell ("{*(flip o foldr) remove*}")
-
-code_syntax_const "op Int"
-  ml ("{*inter*}")
-  haskell ("{*inter*}")
-
-code_syntax_const image
-  ml ("{*\<lambda>f. foldr (insert_ o f)*}")
-  haskell ("{*\<lambda>f. foldr (insert_ o f)*}")
-
-code_syntax_const INTER
-  ml ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
-  haskell ("{*\<lambda>xs f.  foldr (inter o f) xs*}")
-
-code_syntax_const UNION
-  ml ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
-  haskell ("{*\<lambda>xs f.  foldr (foldr insert_ o f) xs*}")
-
-code_primconst Ball
-ml {*
-fun `_` [] f = true
-  | `_` (x::xs) f = f x andalso `_` xs f;
-*}
-haskell {*
-`_` = flip all
-*}
-
-code_primconst Bex
-ml {*
-fun `_` [] f = false
-  | `_` (x::xs) f = f x orelse `_` xs f;
-*}
-haskell {*
-`_` = flip any
-*}
+code_syntax_const
+  "{}"
+    ml (target_atom "[]")
+    haskell (target_atom "[]")
+  insert
+    ml ("{*insertl*}")
+    haskell ("{*insertl*}")
+  "op \<union>"
+    ml ("{*unionl*}")
+    haskell ("{*unionl*}")
+  "op \<inter>"
+    ml ("{*intersect*}")
+    haskell ("{*intersect*}")
+  "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+    ml ("{*flip subtract*}")
+    haskell ("{*flip subtract*}")
+  image
+    ml ("{*map_distinct*}")
+    haskell ("{*map_distinct*}")
+  "Union"
+    ml ("{*unions*}")
+    haskell ("{*unions*}")
+  "Inter"
+    ml ("{*intersects*}")
+    haskell ("{*intersects*}")
+  UNION
+    ml ("{*map_union*}")
+    haskell ("{*map_union*}")
+  INTER
+    ml ("{*map_inter*}")
+    haskell ("{*map_inter*}")
+  Ball
+    ml ("{*Blall*}")
+    haskell ("{*Blall*}")
+  Bex
+    ml ("{*Blex*}")
+    haskell ("{*Blex*}")
 
 end