added code_abstype

--- a/src/HOL/Library/ExecutableRat.thy	Tue Oct 10 09:17:19 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Tue Oct 10 09:17:20 2006 +0200
@@ -81,11 +81,14 @@
 
 section {* code lemmas *}
 
-lemma
-  number_of_rat [code unfold]: "(number_of k \<Colon> rat) \<equiv> Fract k 1"
+lemma number_of_rat [code unfold]:
+  "(number_of k \<Colon> rat) \<equiv> Fract k 1"
   unfolding Fract_of_int_eq rat_number_of_def by simp
 
+declare divide_inverse [where ?'a = rat, code func]
+
 instance rat :: eq ..
+instance erat :: eq ..
 
 
 section {* code names *}
@@ -113,18 +116,41 @@
   "OperationalEquality.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
 
 
+section {* rat as abstype *}
+
+code_abstype rat erat where
+  Fract \<equiv> of_quotient
+  "0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
+  "1 \<Colon> rat" \<equiv> "1 \<Colon> erat"
+  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
+  "uminus \<Colon> rat \<Rightarrow> rat" \<equiv> "uminus \<Colon> erat \<Rightarrow> erat"
+  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
+  "inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
+  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv>  "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
+   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
+
+code_const div_zero
+  (SML "raise/ (Fail/ \"Division by zero\")")
+  (Haskell "error/ \"Division by zero\"")
+
+code_gen
+  Fract
+  "0 \<Colon> rat"
+  "1 \<Colon> rat"
+  "op + \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
+  "uminus \<Colon> rat \<Rightarrow> rat"
+  "op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat"
+  "inverse \<Colon> rat \<Rightarrow> rat"
+  "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
+   "OperationalEquality.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
+  (SML -)
+
+
 section {* type serializations *}
 
 types_code
   rat ("{*erat*}")
 
-code_gen Rat
-  (SML) (Haskell)
-
-code_type rat
-  (SML "{*erat*}")
-  (Haskell "{*erat*}")
-
 
 section {* const serializations *}
 
@@ -139,64 +165,12 @@
   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_const div_zero
-  (SML "raise/ (Fail/ \"Division by zero\")")
-  (Haskell "error/ \"Division by zero\"")
+  "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_erat*}")
 
 code_gen
   of_quotient
   "0::erat"
   "1::erat"
   "op + :: erat \<Rightarrow> erat \<Rightarrow> erat"
-  "uminus :: erat \<Rightarrow> erat"
-  "op * :: erat \<Rightarrow> erat \<Rightarrow> erat"
-  "inverse :: erat \<Rightarrow> erat"
-  "op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
-  eq_erat
-  (SML) (Haskell)
-
-code_const Fract
-  (SML "{*of_quotient*}")
-  (Haskell "{*of_quotient*}")
-
-code_const "0 :: rat"
-  (SML "{*0::erat*}")
-  (Haskell "{*1::erat*}")
-
-code_const "1 :: rat"
-  (SML "{*1::erat*}")
-  (Haskell "{*1::erat*}")
-
-code_const "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
-  (SML "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  (Haskell "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-
-code_const "uminus :: rat \<Rightarrow> rat"
-  (SML "{*uminus :: erat \<Rightarrow> erat*}")
-  (Haskell "{*uminus :: erat \<Rightarrow> erat*}")
-
-code_const "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
-  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-
-code_const "inverse :: rat \<Rightarrow> rat"
-  (SML "{*inverse :: erat \<Rightarrow> erat*}")
-  (Haskell "{*inverse :: erat \<Rightarrow> erat*}")
-
-code_const "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
-  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
-  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
-
-code_const "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
-  (SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
-  (Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
-
-code_const "OperationalEquality.eq :: rat \<Rightarrow> rat \<Rightarrow> bool"
-  (SML "{*eq_erat*}")
-  (Haskell "{*eq_erat*}")
-
-code_gen (SML -)
 
 end

--- a/src/HOL/Library/ExecutableSet.thy	Tue Oct 10 09:17:19 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Oct 10 09:17:20 2006 +0200
@@ -31,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\<Colon>eq \<Rightarrow> bool"
+  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
   "member xs x = (x \<in> set xs)"
-  insertl :: "'a\<Colon>eq\<Rightarrow> 'a list \<Rightarrow> 'a list"
+  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
   "insertl x xs = (if member xs x then xs else x#xs)"
 
 lemma
@@ -51,7 +51,6 @@
 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")
@@ -61,7 +60,6 @@
   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)"
@@ -93,7 +91,7 @@
 
 subsection {* Derived definitions *}
 
-function unionl :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "unionl [] ys = ys"
 | "unionl xs ys = foldr insertl xs ys"
@@ -102,7 +100,7 @@
 lemmas unionl_def = unionl.simps(2)
 declare unionl.simps[code]
 
-function intersect :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "intersect [] ys = []"
 | "intersect xs [] = []"
@@ -112,7 +110,7 @@
 lemmas intersect_def = intersect.simps(3)
 declare intersect.simps[code]
 
-function subtract :: "'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "subtract [] ys = ys"
 | "subtract xs [] = []"
@@ -122,7 +120,7 @@
 lemmas subtract_def = subtract.simps(3)
 declare subtract.simps[code]
 
-function map_distinct :: "('a \<Rightarrow> 'b\<Colon>eq) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 where
   "map_distinct f [] = []"
 | "map_distinct f xs = foldr (insertl o f) xs []"
@@ -131,7 +129,7 @@
 lemmas map_distinct_def = map_distinct.simps(2)
 declare map_distinct.simps[code]
 
-function unions :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
+function unions :: "'a list list \<Rightarrow> 'a list"
 where
   "unions [] = []"
   "unions xs = foldr unionl xs []"
@@ -140,14 +138,14 @@
 lemmas unions_def = unions.simps(2)
 declare unions.simps[code]
 
-consts intersects :: "'a\<Colon>eq list list \<Rightarrow> 'a list"
+consts intersects :: "'a list list \<Rightarrow> 'a list"
 primrec
   "intersects (x#xs) = foldr intersect xs x"
 
 definition
-  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b\<Colon>eq list) \<Rightarrow> 'b list"
+  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\<Colon>eq list) \<Rightarrow> 'b list"
+  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list"
   "map_inter xs f = intersects (map f xs)"
 
 
@@ -232,6 +230,61 @@
 
 section {* code generator setup *}
 
+code_constname
+  "ExecutableSet.member" "List.member"
+  "ExecutableSet.insertl" "List.insertl"
+  "ExecutableSet.drop_first" "List.drop_first"
+
+definition
+  "empty_list = []"
+
+declare empty_list_def [code inline]
+
+lemma [code func]:
+  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
+
+lemma [code func]:
+  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
+
+lemma [code func]:
+  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
+
+definition
+  "subtract' = flip subtract"
+
+lemma [code func]:
+  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
+
+lemma [code func]:
+  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
+
+lemma [code func]:
+  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
+
+lemma [code func]:
+  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
+
+lemma [code func]:
+  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex 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'
+  image \<equiv> map_distinct
+  Union \<equiv> unions
+  Inter \<equiv> intersects
+  UNION \<equiv> map_union
+  INTER \<equiv> map_inter
+  Ball \<equiv> Blall
+  Bex \<equiv> Blex
+
+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 -)
+
+
 subsection {* type serializations *}
 
 types_code
@@ -247,10 +300,6 @@
 and gen_set aG i = gen_set' aG i i;
 *}
 
-code_type set
-  (SML "_ list")
-  (Haskell target_atom "[_]")
-
 
 subsection {* const serializations *}
 
@@ -269,63 +318,4 @@
   "Ball"    ("{*Blall*}")
   "Bex"     ("{*Blex*}")
 
-code_constname
-  "ExecutableSet.member" "List.member"
-  "ExecutableSet.insertl" "List.insertl"
-  "ExecutableSet.drop_first" "List.drop_first"
-
-code_const "{}"
-  (SML target_atom "[]")
-  (Haskell target_atom "[]")
-
-code_const insert
-  (SML "{*insertl*}")
-  (Haskell "{*insertl*}")
-
-code_const insert
-  (SML "{*insertl*}")
-  (Haskell "{*insertl*}")
-
-code_const "op \<union>"
-  (SML "{*unionl*}")
-  (Haskell "{*unionl*}")
-
-code_const "op \<inter>"
-  (SML "{*intersect*}")
-  (Haskell "{*intersect*}")
-
-code_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  (SML "{*flip subtract*}")
-  (Haskell "{*flip subtract*}")
-
-code_const image
-  (SML "{*map_distinct*}")
-  (Haskell "{*map_distinct*}")
-
-code_const "Union"
-  (SML "{*unions*}")
-  (Haskell "{*unions*}")
-
-code_const "Inter"
-  (SML "{*intersects*}")
-  (Haskell "{*intersects*}")
-
-code_const UNION
-  (SML "{*map_union*}")
-  (Haskell "{*map_union*}")
-
-code_const INTER
-  (SML "{*map_inter*}")
-  (Haskell "{*map_inter*}")
-
-code_const Ball
-  (SML "{*Blall*}")
-  (Haskell "{*Blall*}")
-
-code_const Bex
-  (SML "{*Blex*}")
-  (Haskell "{*Blex*}")
-
-code_gen (SML -) (SML _)
-
 end