src/HOL/Library/ExecutableSet.thy

--- a/src/HOL/Library/ExecutableSet.thy	Tue Sep 19 15:22:03 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Sep 19 15:22:05 2006 +0200
@@ -9,14 +9,21 @@
 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 *}
@@ -24,9 +31,9 @@
 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
@@ -44,6 +51,7 @@
 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")
@@ -53,6 +61,7 @@
   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)"
@@ -84,8 +93,7 @@
 
 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"
@@ -94,7 +102,7 @@
 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 [] = []"
@@ -104,7 +112,7 @@
 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 [] = []"
@@ -114,7 +122,7 @@
 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 []"
@@ -123,7 +131,7 @@
 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 []"
@@ -132,14 +140,14 @@
 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)"
 
 
@@ -266,11 +274,6 @@
   "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 "[]")
@@ -319,4 +322,6 @@
   (SML "{*Blex*}")
   (Haskell "{*Blex*}")
 
+code_gen (SML -) (SML _)
+
 end