src/HOL/Library/ExecutableSet.thy

 
 theory ExecutableSet
 imports Main
 begin
 
-section {* Definitional rewrites *}
+section {* Definitional equality rewrites *}
+
+instance set :: (eq) eq ..
 
 lemma [code target: Set]:
   "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
   by blast
 
+lemma [code func]:
+  "OperationalEquality.eq A B = (A \<subseteq> B \<and> B \<subseteq> A)"
+  unfolding eq_def 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 :: "'a list \<Rightarrow> 'a\<Colon>eq \<Rightarrow> bool"
   "member xs x = (x \<in> set xs)"
-  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  insertl :: "'a\<Colon>eq\<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)"

   "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]
+ML {* reset CodegenData.strict_functyp *}
 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
+ML {* set CodegenData.strict_functyp *}
 
 lemma member_nil [simp]:
   "member [] = (\<lambda>x. False)"
 proof
   fix x

   by (induct xs) simp_all
 
 
 subsection {* Derived definitions *}
 
-
-function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function unionl :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "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)
 declare unionl.simps[code]
 
-function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function intersect :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "intersect [] ys = []"
 | "intersect xs [] = []"
 | "intersect xs ys = filter (member xs) ys"
   by pat_completeness auto
 termination intersect by (auto_term "{}")
 lemmas intersect_def = intersect.simps(3)
 declare intersect.simps[code]
 
-function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function subtract :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "subtract [] ys = ys"
 | "subtract xs [] = []"
 | "subtract xs ys = foldr remove1 xs ys"
   by pat_completeness auto
 termination subtract by (auto_term "{}")
 lemmas subtract_def = subtract.simps(3)
 declare subtract.simps[code]
 
-function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+function map_distinct :: "('a \<Rightarrow> 'b\<Colon>eq) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 where
   "map_distinct f [] = []"
 | "map_distinct f xs = foldr (insertl o f) xs []"
   by pat_completeness auto
 termination map_distinct by (auto_term "{}")
 lemmas map_distinct_def = map_distinct.simps(2)
 declare map_distinct.simps[code]
 
-function unions :: "'a list list \<Rightarrow> 'a list"
+function unions :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
 where
   "unions [] = []"
   "unions xs = foldr unionl xs []"
   by pat_completeness auto
 termination unions by (auto_term "{}")
 lemmas unions_def = unions.simps(2)
 declare unions.simps[code]
 
-consts intersects :: "'a list list \<Rightarrow> 'a list"
+consts intersects :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
 primrec
   "intersects (x#xs) = foldr intersect xs x"
 
 definition
-  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
+  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq 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 :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
   "map_inter xs f = intersects (map f xs)"
 
 
 section {* Isomorphism proofs *}
 

 code_constname
   "ExecutableSet.member" "List.member"
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
 
-code_gen
-  insertl unionl intersect flip subtract map_distinct
-  unions intersects map_union map_inter Blall Blex
-  (SML) (Haskell) 
-
 code_const "{}"
   (SML target_atom "[]")
   (Haskell target_atom "[]")
 
 code_const insert

 
 code_const Bex
   (SML "{*Blex*}")
   (Haskell "{*Blex*}")
 
+code_gen (SML -) (SML _)
+
 end