# HG changeset patch
# User haftmann
# Date 1150280053 -7200
# Node ID 2202a56488974e1ea66c8444578b748bc1d01077
# Parent  2b4c09941e0466395d4319bd19030af8e80785fa
slight adaptions for code generator

diff -r 2b4c09941e04 -r 2202a5648897 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Wed Jun 14 12:13:12 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Wed Jun 14 12:14:13 2006 +0200
@@ -51,17 +51,20 @@
 *}
   int ("(_)")
 
-code_syntax_tyco nat
-  ml (target_atom "{* int *}")
-  haskell (target_atom "{* int *}")
+code_typapp nat
+  ml (target_atom "IntInf.int")
+  haskell (target_atom "Integer")
+
+definition
+  "nat_of_int (k::int) = (if k < 0 then - k else k)"
 
-code_syntax_const
-  "0 :: nat"
-    ml (target_atom "{* 0 :: int *}")
-    haskell (target_atom "{* 0 :: int *}")
-  Suc
-    ml (target_atom "(__ + 1)")
-    haskell (target_atom "(__ + 1)")
+lemma
+  "nat_of_int = abs"
+by (simp add: expand_fun_eq nat_of_int_def zabs_def)
+
+code_generate (ml, haskell) "abs :: int \<Rightarrow> int"
+
+code_constapp
   nat
     ml ("{* abs :: int \<Rightarrow> int *}")
     haskell ("{* abs :: int \<Rightarrow> int *}")
@@ -70,6 +73,18 @@
     haskell ("_")
 
 text {*
+  Eliminate @{const "0::nat"} and @{const "Suc"}
+  by unfolding in place.
+*}
+
+lemma [code unfolt]:
+  "0 = nat 0"
+  "Suc = (op +) 1"
+by (simp_all add: expand_fun_eq)
+
+declare elim_one_nat [code nofold]
+
+text {*
 Case analysis on natural numbers is rephrased using a conditional
 expression:
 *}
@@ -98,9 +113,8 @@
 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
+  by simp
 
 subsection {* Preprocessors *}
 
diff -r 2b4c09941e04 -r 2202a5648897 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Wed Jun 14 12:13:12 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Wed Jun 14 12:14:13 2006 +0200
@@ -81,9 +81,11 @@
 types_code
   rat ("{*erat*}")
 
-code_syntax_tyco rat
-  ml (target_atom "{*erat*}")
-  haskell (target_atom "{*erat*}")
+code_generate (ml, haskell) Rat
+
+code_typapp rat
+  ml ("{*erat*}")
+  haskell ("{*erat*}")
 
 
 section {* const serializations *}
@@ -101,10 +103,23 @@
   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
+code_constapp
   "arbitrary :: erat"
     ml ("raise/ (Fail/ \"non-defined rational number\")")
     haskell ("error/ \"non-defined rational number\"")
+
+code_generate (ml, haskell)
+  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_rat
+
+code_constapp
   Fract
     ml ("{*of_quotient*}")
     haskell ("{*of_quotient*}")
@@ -137,4 +152,3 @@
     haskell ("{*eq_rat*}")
 
 end
-
diff -r 2b4c09941e04 -r 2202a5648897 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Wed Jun 14 12:13:12 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Wed Jun 14 12:14:13 2006 +0200
@@ -234,7 +234,7 @@
 and gen_set aG i = gen_set' aG i i;
 *}
 
-code_syntax_tyco set
+code_typapp set
   ml ("_ list")
   haskell (target_atom "[_]")
 
@@ -261,7 +261,11 @@
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
 
-code_syntax_const
+code_generate (ml, haskell) 
+  insertl unionl intersect flip subtract map_distinct
+  unions intersects map_union map_inter Blall Blex
+
+code_constapp
   "{}"
     ml (target_atom "[]")
     haskell (target_atom "[]")