updated doc

--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Thu Apr 26 13:32:55 2007 +0200
@@ -168,7 +168,7 @@
   \emph{type classes}. A defining equation as a first approximation
   is a theorem of the form @{text "f t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n \<equiv> t"}
   (an equation headed by a constant @{text f} with arguments
-  @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}.
+  @{text "t\<^isub>1 t\<^isub>2 \<dots> t\<^isub>n"} and right hand side @{text t}).
   Code generation aims to turn defining equations
   into a functional program by running through
   a process (see figure \ref{fig:process}):
@@ -245,15 +245,12 @@
   a defining equation (e.g.~the Hilbert choice
   operation @{text "SOME"}):
 *}
-
 (*<*)
 setup {* Sign.add_path "foo" *}
 (*>*)
-
 definition
   pick_some :: "'a list \<Rightarrow> 'a" where
   "pick_some xs = (SOME x. x \<in> set xs)"
-
 (*<*)
 hide const pick_some
 
@@ -263,7 +260,6 @@
   pick_some :: "'a list \<Rightarrow> 'a" where
   "pick_some = hd"
 (*>*)
-
 code_gen pick_some (SML "examples/fail_const.ML")
 
 text {* \noindent will fail. *}
@@ -285,7 +281,7 @@
   The typical HOL tools are already set up in a way that
   function definitions introduced by @{text "\<DEFINITION>"},
   @{text "\<FUN>"},
-  @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"}
+  @{text "\<FUNCTION>"}, @{text "\<PRIMREC>"},
   @{text "\<RECDEF>"} are implicitly propagated
   to this defining equation table. Specific theorems may be
   selected using an attribute: \emph{code func}. As example,
@@ -300,7 +296,7 @@
     if n < k then v else pick xs (n - k))"
 
 text {*
-  We want to eliminate the explicit destruction
+  \noindent We want to eliminate the explicit destruction
   of @{term x} to @{term "(k, v)"}:
 *}
 
@@ -311,11 +307,11 @@
 code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
 
 text {*
-  This theorem is now added to the defining equation table:
+  \noindent This theorem now is used for generating code:
 
   \lstsml{Thy/examples/pick1.ML}
 
-  It might be convenient to remove the pointless original
+  \noindent It might be convenient to remove the pointless original
   equation, using the \emph{nofunc} attribute:
 *}
 
@@ -326,7 +322,7 @@
 text {*
   \lstsml{Thy/examples/pick2.ML}
 
-  Syntactic redundancies are implicitly dropped. For example,
+  \noindent Syntactic redundancies are implicitly dropped. For example,
   using a modified version of the @{const fac} function
   as defining equation, the then redundant (since
   syntactically subsumed) original defining equations
@@ -358,7 +354,7 @@
   here we just illustrate its impact on code generation.
 
   In a target language, type classes may be represented
-  natively (as in the case of Haskell). For languages
+  natively (as in the case of Haskell).  For languages
   like SML, they are implemented using \emph{dictionaries}.
   Our following example specifies a class \qt{null},
   assigning to each of its inhabitants a \qt{null} value:
@@ -367,12 +363,11 @@
 class null = type +
   fixes null :: 'a
 
-consts
+fun
   head :: "'a\<Colon>null list \<Rightarrow> 'a"
-
-primrec
+where
   "head [] = null"
-  "head (x#xs) = x"
+  | "head (x#xs) = x"
 
 text {*
   We provide some instances for our @{text null}:
@@ -406,8 +401,9 @@
 
 text {*
   \lsthaskell{Thy/examples/Codegen.hs}
+  \noindent (we have left out all other modules).
 
-  (we have left out all other modules).
+  \medskip
 
   The whole code in SML with explicit dictionary passing:
 *}
@@ -416,51 +412,21 @@
 
 text {*
   \lstsml{Thy/examples/class.ML}
-*}
 
-text {*
-  or in OCaml:
+  \medskip
+
+  \noindent or in OCaml:
 *}
 
 code_gen dummy (OCaml "examples/class.ocaml")
 
 text {*
   \lstsml{Thy/examples/class.ocaml}
+
+  \medskip The explicit association of constants
+  to classes can be inspected using the @{text "\<PRINTCLASSES>"}
 *}
 
-subsection {* Incremental code generation *}
-
-text {*
-  Code generation is \emph{incremental}: theorems
-  and abstract intermediate code are cached and extended on demand.
-  The cache may be partially or fully dropped if the underlying
-  executable content of the theory changes.
-  Implementation of caching is supposed to transparently
-  hid away the details from the user.  Anyway, caching
-  reaches the surface by using a slightly more general form
-  of the @{text "\<CODEGEN>"}: either the list of constants or the
-  list of serialization expressions may be dropped.  If no
-  serialization expressions are given, only abstract code
-  is generated and cached; if no constants are given, the
-  current cache is serialized.
-
-  For explorative purpose, the
-  @{text "\<CODETHMS>"} command may prove useful:
-*}
-
-code_thms
-
-text {*
-  \noindent print all cached defining equations (i.e.~\emph{after}
-  any applied transformation).  A
-  list of constants may be given; their function
-  equations are added to the cache if not already present.
-
-  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
-  visualizing dependencies between defining equations.
-*}
-
-
 
 section {* Recipes and advanced topics \label{sec:advanced} *}
 
@@ -481,7 +447,7 @@
   \end{itemize}
 *}
 
-subsection {* Library theories *}
+subsection {* Library theories \label{sec:library} *}
 
 text {*
   The HOL \emph{Main} theory already provides a code generator setup
@@ -492,6 +458,13 @@
 
   \begin{description}
 
+    \item[@{text "Pretty_Int"}] represents HOL integers by big
+       integer literals in target languages.
+    \item[@{text "Pretty_Char"}] represents HOL characters by 
+       character literals in target languages.
+    \item[@{text "Pretty_Char_chr"}] like @{text "Pretty_Char_chr"},
+       but also offers treatment of character codes; includes
+       @{text "Pretty_Int"}.
     \item[@{text "ExecutableSet"}] allows to generate code
        for finite sets using lists.
     \item[@{text "ExecutableRat"}] \label{exec_rat} implements rational
@@ -499,10 +472,10 @@
     \item[@{text "EfficientNat"}] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
        matching with @{const "0\<Colon>nat"} / @{const "Suc"}
-       is eliminated.
+       is eliminated;  includes @{text "Pretty_Int"}.
     \item[@{text "MLString"}] provides an additional datatype @{text "mlstring"};
        in the HOL default setup, strings in HOL are mapped to list
-       of chars in SML; values of type @{text "mlstring"} are
+       of HOL characters in SML; values of type @{text "mlstring"} are
        mapped to strings in SML.
 
   \end{description}
@@ -524,7 +497,6 @@
   equation, but never to the constant heading the left hand side.
   Inline theorems may be declared an undeclared using the
   \emph{code inline} or \emph{code noinline} attribute respectively.
-
   Some common applications:
 *}
 
@@ -585,8 +557,148 @@
   \end{warn}
 *}
 
+
+subsection {* Concerning operational equality *}
+
+text {*
+  Surely you have already noticed how equality is treated
+  by the code generator:
+*}
+
+fun
+  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+    "collect_duplicates xs ys [] = xs"
+  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
+      then if z \<in> set ys
+        then collect_duplicates xs ys zs
+        else collect_duplicates xs (z#ys) zs
+      else collect_duplicates (z#xs) (z#ys) zs)"
+
+text {*
+  The membership test during preprocessing is rewritten,
+  resulting in @{const List.memberl}, which itself
+  performs an explicit equality check.
+*}
+
+code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
+
+text {*
+  \lstsml{Thy/examples/collect_duplicates.ML}
+*}
+
+text {*
+  Obviously, polymorphic equality is implemented the Haskell
+  way using a type class.  How is this achieved?  By an
+  almost trivial definition in the HOL setup:
+*}
+(*<*)
+setup {* Sign.add_path "foo" *}
+consts "op =" :: "'a"
+(*>*)
+class eq (attach "op =") = type
+
+text {*
+  This merely introduces a class @{text eq} with corresponding
+  operation @{text "op ="};
+  the preprocessing framework does the rest.
+  For datatypes, instances of @{text eq} are implicitly derived
+  when possible.
+
+  Though this @{text eq} class is designed to get rarely in
+  the way, a subtlety
+  enters the stage when definitions of overloaded constants
+  are dependent on operational equality.  For example, let
+  us define a lexicographic ordering on tuples:
+*}
+(*<*)
+hide (open) "class" eq
+hide (open) const "op ="
+setup {* Sign.parent_path *}
+(*>*)
+instance * :: (ord, ord) ord
+  less_prod_def:
+    "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
+    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
+  less_eq_prod_def:
+    "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
+    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
+
+lemmas [code nofunc] = less_prod_def less_eq_prod_def
+
+lemma ord_prod [code func(*<*), code nofunc(*>*)]:
+  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
+  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
+  unfolding less_prod_def less_eq_prod_def by simp_all
+
+text {*
+  Then code generation will fail.  Why?  The definition
+  of @{const "op \<le>"} depends on equality on both arguments,
+  which are polymorphic and impose an additional @{text eq}
+  class constraint, thus violating the type discipline
+  for class operations.
+
+  The solution is to add @{text eq} explicitly to the first sort arguments in the
+  code theorems:
+*}
+
+lemma ord_prod_code [code func]:
+  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow>
+    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
+  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow>
+    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
+  unfolding ord_prod by rule+
+
+text {*
+  \noindent Then code generation succeeds:
+*}
+
+code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
+
+text {*
+  \lstsml{Thy/examples/lexicographic.ML}
+*}
+
+text {*
+  In general, code theorems for overloaded constants may have more
+  restrictive sort constraints than the underlying instance relation
+  between class and type constructor as long as the whole system of
+  constraints is coregular; code theorems violating coregularity
+  are rejected immediately.  Consequently, it might be necessary
+  to delete disturbing theorems in the code theorem table,
+  as we have done here with the original definitions @{text less_prod_def}
+  and @{text less_eq_prod_def}.
+*}
+
+
+subsection {* Programs as sets of theorems *}
+
+text {*
+  As told in \secref{sec:concept}, code generation is based
+  on a structured collection of code theorems.
+  For explorative purpose, this collection
+  may be inspected using the @{text "\<CODETHMS>"} command:
+*}
+
+code_thms "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"
+
+text {*
+  \noindent prints a table with \emph{all} defining equations
+  for @{const "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}, including
+  \emph{all} defining equations those equations depend
+  on recursivly.  @{text "\<CODETHMS>"} provides a convenient
+  mechanism to inspect the impact of a preprocessor setup
+  on defining equations.
+  
+  Similarly, the @{text "\<CODEDEPS>"} command shows a graph
+  visualizing dependencies between defining equations.
+*}
+
+
 subsection {* Customizing serialization  *}
 
+subsubsection {* Basics *}
+
 text {*
   Consider the following function and its corresponding
   SML code:
@@ -595,20 +707,18 @@
 fun
   in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-
 (*<*)
 code_type %tt bool
   (SML)
 code_const %tt True and False and "op \<and>" and Not
   (SML and and and)
 (*>*)
-
 code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
 
 text {*
   \lstsml{Thy/examples/bool_literal.ML}
 
-  Though this is correct code, it is a little bit unsatisfactory:
+  \noindent Though this is correct code, it is a little bit unsatisfactory:
   boolean values and operators are materialized as distinguished
   entities with have nothing to do with the SML-builtin notion
   of \qt{bool}.  This results in less readable code;
@@ -651,7 +761,7 @@
 text {*
   \lstsml{Thy/examples/bool_mlbool.ML}
 
-  This still is not perfect: the parentheses
+  \noindent This still is not perfect: the parentheses
   around the \qt{andalso} expression are superfluous.
   Though the serializer
   by no means attempts to imitate the rich Isabelle syntax
@@ -667,20 +777,19 @@
 text {*
   \lstsml{Thy/examples/bool_infix.ML}
 
+  \medskip
+
   Next, we try to map HOL pairs to SML pairs, using the
   infix ``@{verbatim "*"}'' type constructor and parentheses:
 *}
-
 (*<*)
 code_type *
   (SML)
 code_const Pair
   (SML)
 (*>*)
-
 code_type %tt *
   (SML infix 2 "*")
-
 code_const %tt Pair
   (SML "!((_),/ (_))")
 
@@ -693,44 +802,7 @@
   inserts a space which may be used as a break if necessary
   during pretty printing.
 
-  So far, we did only provide more idiomatic serializations for
-  constructs which would be executable on their own.  Target-specific
-  serializations may also be used to \emph{implement} constructs
-  which have no explicit notion of executability.  For example,
-  take the HOL integers:
-*}
-
-definition
-  double_inc :: "int \<Rightarrow> int" where
-  "double_inc k = 2 * k + 1"
-
-code_gen double_inc (SML "examples/integers.ML")
-
-text {*
-  will fail: @{typ int} in HOL is implemented using a quotient
-  type, which does not provide any notion of executability.
-  \footnote{Eventually, we also want to provide executability
-  for quotients.}.  However, we could use the SML builtin
-  integers:
-*}
-
-code_type %tt int
-  (SML "IntInf.int")
-
-code_const %tt "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-    and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
-  (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
-
-code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML")
-
-text {*
-  resulting in:
-
-  \lstsml{Thy/examples/integers.ML}
-*}
-
-text {*
-  These examples give a glimpse what powerful mechanisms
+  These examples give a glimpse what mechanisms
   custom serializations provide; however their usage
   requires careful thinking in order not to introduce
   inconsistencies -- or, in other words:
@@ -748,169 +820,6 @@
   a recommended tutorial on how to use them properly.
 *}
 
-subsection {* Concerning operational equality *}
-
-text {*
-  Surely you have already noticed how equality is treated
-  by the code generator:
-*}
-
-fun
-  collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-    "collect_duplicates xs ys [] = xs"
-  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
-      then if z \<in> set ys
-        then collect_duplicates xs ys zs
-        else collect_duplicates xs (z#ys) zs
-      else collect_duplicates (z#xs) (z#ys) zs)"
-
-text {*
-  The membership test during preprocessing is rewritten,
-  resulting in @{const List.memberl}, which itself
-  performs an explicit equality check.
-*}
-
-code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
-
-text {*
-  \lstsml{Thy/examples/collect_duplicates.ML}
-*}
-
-text {*
-  Obviously, polymorphic equality is implemented the Haskell
-  way using a type class.  How is this achieved?  By an
-  almost trivial definition in the HOL setup:
-*}
-
-(*<*)
-setup {* Sign.add_path "foo" *}
-consts "op =" :: "'a"
-(*>*)
-
-class eq (attach "op =") = type
-
-text {*
-  This merely introduces a class @{text eq} with corresponding
-  operation @{text "op ="};
-  the preprocessing framework does the rest.
-*}
-
-(*<*)
-hide (open) "class" eq
-hide (open) const "op ="
-setup {* Sign.parent_path *}
-(*>*)
-
-text {*
-  For datatypes, instances of @{text eq} are implicitly derived
-  when possible.
-
-  Though this class is designed to get rarely in the way, there
-  are some cases when it suddenly comes to surface:
-*}
-
-subsubsection {* typedecls interpreted by customary serializations *}
-
-text {*
-  A common idiom is to use unspecified types for formalizations
-  and interpret them for a specific target language:
-*}
-
-typedecl key
-
-fun
-  lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
-    "lookup [] l = None"
-  | "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
-
-code_type %tt key
-  (SML "string")
-
-text {*
-  This, though, is not sufficient: @{typ key} is no instance
-  of @{text eq} since @{typ key} is no datatype; the instance
-  has to be declared manually, including a serialization
-  for the particular instance of @{const "op ="}:
-*}
-
-instance key :: eq ..
-
-code_const %tt "op = \<Colon> key \<Rightarrow> key \<Rightarrow> bool"
-  (SML "!((_ : string) = _)")
-
-text {*
-  Then everything goes fine:
-*}
-
-code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML")
-
-text {*
-  \lstsml{Thy/examples/lookup.ML}
-*}
-
-subsubsection {* lexicographic orderings *}
-
-text {*
-  Another subtlety
-  enters the stage when definitions of overloaded constants
-  are dependent on operational equality.  For example, let
-  us define a lexicographic ordering on tuples:
-*}
-
-instance * :: (ord, ord) ord
-  less_prod_def: "p1 < p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
-    x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
-  less_eq_prod_def: "p1 \<le> p2 \<equiv> let (x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) = p1; (x2, y2) = p2 in
-    x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)" ..
-
-lemmas [code nofunc] = less_prod_def less_eq_prod_def
-
-lemma ord_prod [code func]:
-  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
-  "(x1 \<Colon> 'a\<Colon>ord, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
-  unfolding less_prod_def less_eq_prod_def by simp_all
-
-text {*
-  Then code generation will fail.  Why?  The definition
-  of @{const "op \<le>"} depends on equality on both arguments,
-  which are polymorphic and impose an additional @{text eq}
-  class constraint, thus violating the type discipline
-  for class operations.
-
-  The solution is to add @{text eq} explicitly to the first sort arguments in the
-  code theorems:
-*}
-
-(*<*)
-lemmas [code nofunc] = ord_prod
-(*>*)
-
-lemma ord_prod_code [code func]:
-  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 < y2)"
-  "(x1 \<Colon> 'a\<Colon>{ord, eq}, y1 \<Colon> 'b\<Colon>ord) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> (x1 = x2 \<and> y1 \<le> y2)"
-  unfolding ord_prod by rule+
-
-text {*
-  Then code generation succeeds:
-*}
-
-code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>ord \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
-
-text {*
-  \lstsml{Thy/examples/lexicographic.ML}
-*}
-
-text {*
-  In general, code theorems for overloaded constants may have more
-  restrictive sort constraints than the underlying instance relation
-  between class and type constructor as long as the whole system of
-  constraints is coregular; code theorems violating coregularity
-  are rejected immediately.  Consequently, it might be necessary
-  to delete disturbing theorems in the code theorem table,
-  as we have done here with the original definitions @{text less_prod_def}
-  and @{text less_eq_prod_def}.
-*}
 
 subsubsection {* Haskell serialization *}
 
@@ -921,23 +830,12 @@
   for the class (@{text "\<CODECLASS>"}) and its operation:
 *}
 
-(*<*)
-setup {* Sign.add_path "bar" *}
-class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-(*>*)
-
 code_class %tt eq
-  (Haskell "Eq" where eq \<equiv> "(==)")
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
 
-code_const %tt eq
+code_const %tt "op ="
   (Haskell infixl 4 "==")
 
-(*<*)
-hide "class" eq
-hide const eq
-setup {* Sign.parent_path *}
-(*>*)
-
 text {*
   A problem now occurs whenever a type which
   is an instance of @{text eq} in HOL is mapped
@@ -962,86 +860,57 @@
 code_instance %tt bar :: eq
   (Haskell -)
 
-subsection {* Types matter *}
 
-text {*
-  Imagine the following quick-and-dirty setup for implementing
-  some kind of sets as lists in SML:
-*}
-
-code_type %tt set
-  (SML "_ list")
-
-code_const %tt "{}" and insert
-  (SML "![]" and infixl 7 "::")
-
-definition
-  dummy_set :: "(nat \<Rightarrow> nat) set" where
-  "dummy_set = {Suc}"
-
-text {*
-  Then code generation for @{const dummy_set} will fail.
-  Why? A glimpse at the defining equations will offer:
-*}
-
-code_thms insert
+subsubsection {* Pretty printing *}
 
 text {*
-  This reveals the defining equation @{thm insert_def}
-  for @{const insert}, which is operationally meaningless
-  but forces an equality constraint on the set members
-  (which is not satisfiable if the set members are functions).
-  Even when using set of natural numbers (which are an instance
-  of \emph{eq}), we run into a problem:
-*}
-
-definition
-  foobar_set :: "nat set" where
-  "foobar_set = {0, 1, 2}"
-
-text {*
-  In this case the serializer would complain that @{const insert}
-  expects dictionaries (namely an \emph{eq} dictionary) but
-  has also been given a customary serialization.
-
-  \fixme[needs rewrite] The solution to this dilemma:
+  The serializer provides ML interfaces to set up
+  pretty serializations for expressions like lists, numerals
+  and characters;  these are
+  monolithic stubs and should only be used with the
+  theories introduces in \secref{sec:library}.
 *}
 
-lemma [code func]:
-  "insert = insert" ..
-
-code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML")
-
-text {*
-  \lstsml{Thy/examples/dirty_set.ML}
-
-  Reflexive defining equations by convention are dropped:
-*}
-
-code_thms insert
-
-text {*
-  will show \emph{no} defining equations for insert.
-
-  Note that the sort constraints of reflexive equations
-  are considered; so
-*}
-
-lemma [code func]:
-  "(insert \<Colon> 'a\<Colon>eq \<Rightarrow> 'a set \<Rightarrow> 'a set) = insert" ..
-
-text {*
-  would mean nothing else than to introduce the evil
-  sort constraint by hand.
-*}
-
-
 subsection {* Constructor sets for datatypes *}
 
 text {*
-  \fixme
+  Conceptually, any datatype is spanned by a set of
+  \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"}
+  where @{text "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is excactly the set of \emph{all}
+  type variables in @{text "\<tau>"}.  The HOL datatype package
+  by default registers any new datatype in the table
+  of datatypes, which may be inspected using
+  the @{text "\<PRINTCODESETUP>"} command.
+
+  In some cases, it may be convenient to alter or
+  extend this table;  as an example, we show
+  how to implement finite sets by lists
+  using the conversion @{term [source] "set \<Colon> 'a list \<Rightarrow> 'a set"}
+  as constructor:
 *}
 
+code_datatype set
+
+lemma [code func]: "{} = set []" by simp
+
+lemma [code func]: "insert x (set xs) = set (x#xs)" by simp
+
+lemma [code func]: "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
+
+lemma [code func]: "xs \<union> set ys = foldr insert ys xs" by (induct ys) simp_all
+
+lemma [code func]: "\<Union>set xs = foldr (op \<union>) xs {}" by (induct xs) simp_all
+
+code_gen "{}" insert "op \<in>" "op \<union>" "Union" (*<*)(SML #)(*>*)(SML "examples/set_list.ML")
+
+text {*
+  \lstsml{Thy/examples/set_list.ML}
+
+  \medskip
+
+  Changing the representation of existing datatypes requires
+  some care with respect to pattern matching and such.
+*}
 
 subsection {* Cyclic module dependencies *}
 
@@ -1069,6 +938,22 @@
   at serialization time.
 *}
 
+subsection {* Incremental code generation *}
+
+text {*
+  Code generation is \emph{incremental}: theorems
+  and abstract intermediate code are cached and extended on demand.
+  The cache may be partially or fully dropped if the underlying
+  executable content of the theory changes.
+  Implementation of caching is supposed to transparently
+  hid away the details from the user.  Anyway, caching
+  reaches the surface by using a slightly more general form
+  of the @{text "\<CODETHMS>"}, @{text "\<CODEDEPS>"}
+  and @{text "\<CODEGEN>"} commands: the list of constants
+  may be omitted.  Then, all constants with code theorems
+  in the current cache are referred to.
+*}
+
 subsection {* Axiomatic extensions *}
 
 text {*
@@ -1145,6 +1030,8 @@
 text {*
   \lstsml{Thy/examples/arbitrary.ML}
 
+  \medskip
+
   Another axiomatic extension is code generation
   for abstracted types.  For this, the  
   @{text "ExecutableRat"} (see \secref{exec_rat})
@@ -1370,13 +1257,13 @@
 
   \item @{text merge} merging two data slots.
 
-  \item @{text purge}~@{text thy}~@{text cs} propagates changes in executable content;
+  \item @{text purge}~@{text thy}~@{text consts} propagates changes in executable content;
     if possible, the current theory context is handed over
     as argument @{text thy} (if there is no current theory context (e.g.~during
-    theory merge, @{ML NONE}); @{text cs} indicates the kind
+    theory merge, @{ML NONE}); @{text consts} indicates the kind
     of change: @{ML NONE} stands for a fundamental change
-    which invalidates any existing code, @{text "SOME cs"}
-    hints that executable content for constants @{text cs}
+    which invalidates any existing code, @{text "SOME consts"}
+    hints that executable content for constants @{text consts}
     has changed.
 
   \end{description}
@@ -1406,19 +1293,61 @@
   \end{description}
 *}
 
-(* subsubsection {* Building implementable systems fo defining equations *}
+subsubsection {* Building implementable systems fo defining equations *}
 
 text {*
   Out of the executable content of a theory, a normalized
   defining equation systems may be constructed containing
   function definitions for constants.  The system is cached
   until its underlying executable content changes.
+
+  Defining equations are retrieved by instantiation
+  of the functor @{ML_functor CodegenFuncgrRetrieval}
+  which takes two arguments:
+
+  \medskip
+  \begin{tabular}{l}
+  @{text "val name: string"} \\
+  @{text "val rewrites: theory \<rightarrow> thm list"}
+  \end{tabular}
+
+  \begin{description}
+
+  \item @{text name} is a system-wide unique name identifying
+    this particular system of defining equations.
+
+  \item @{text rewrites} specifies a set of theory-dependent
+    rewrite rules which are added to the preprocessor setup;
+    if no additional preprocessing is required, pass
+    a function returning an empty list.
+
+  \end{description}
+
+  An instance of @{ML_functor CodegenFuncgrRetrieval} in essence
+  provides the following interface:
+
+  \medskip
+  \begin{tabular}{l}
+  @{text "make: theory \<rightarrow> CodegenConsts.const list \<rightarrow> CodegenFuncgr.T"} \\
+  \end{tabular}
+
+  \begin{description}
+
+  \item @{text make}~@{text thy}~@{text consts} returns
+    a system of defining equations which is guaranteed
+    to contain all defining equations for constants @{text consts}
+    including all defining equations any defining equation
+    for any constant in @{text consts} depends on.
+
+  \end{description}
+
+  Systems of defining equations are graphs accesible by the
+  following operations:
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type CodegenFuncgr.T} \\
-  @{index_ML CodegenFuncgr.make: "theory -> CodegenConsts.const list -> CodegenFuncgr.T"} \\
   @{index_ML CodegenFuncgr.funcs: "CodegenFuncgr.T -> CodegenConsts.const -> thm list"} \\
   @{index_ML CodegenFuncgr.typ: "CodegenFuncgr.T -> CodegenConsts.const -> typ"} \\
   @{index_ML CodegenFuncgr.deps: "CodegenFuncgr.T
@@ -1431,20 +1360,15 @@
   \item @{ML_type CodegenFuncgr.T} represents
     a normalized defining equation system.
 
-  \item @{ML CodegenFuncgr.make}~@{text thy}~@{text cs}
-    returns a normalized defining equation system,
-    with the assertion that it contains any function
-    definition for constants @{text cs} (if existing).
+  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text const}
+    retrieves defining equiations for constant @{text const}.
 
-  \item @{ML CodegenFuncgr.funcs}~@{text funcgr}~@{text c}
-    retrieves function definition for constant @{text c}.
+  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text const}
+    retrieves function type for constant @{text const}.
 
-  \item @{ML CodegenFuncgr.typ}~@{text funcgr}~@{text c}
-    retrieves function type for constant @{text c}.
-
-  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text cs}
+  \item @{ML CodegenFuncgr.deps}~@{text funcgr}~@{text consts}
     returns the transitive closure of dependencies for
-    constants @{text cs} as a partitioning where each partition
+    constants @{text consts} as a partitioning where each partition
     corresponds to a strongly connected component of
     dependencies and any partition does \emph{not}
     depend on partitions further left.
@@ -1453,7 +1377,7 @@
     returns all currently represented constants.
 
   \end{description}
-*} *)
+*}
 
 subsubsection {* Datatype hooks *}
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex	Thu Apr 26 13:32:55 2007 +0200
@@ -198,7 +198,7 @@
   \emph{type classes}. A defining equation as a first approximation
   is a theorem of the form \isa{f\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n\ {\isasymequiv}\ t}
   (an equation headed by a constant \isa{f} with arguments
-  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}.
+  \isa{t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}\ {\isasymdots}\ t\isactrlisub n} and right hand side \isa{t}).
   Code generation aims to turn defining equations
   into a functional program by running through
   a process (see figure \ref{fig:process}):
@@ -290,14 +290,12 @@
 {\isafoldML}%
 %
 \isadelimML
-\isanewline
 %
 \endisadelimML
 \isacommand{definition}\isamarkupfalse%
 \isanewline
 \ \ pick{\isacharunderscore}some\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
+\ \ {\isachardoublequoteopen}pick{\isacharunderscore}some\ xs\ {\isacharequal}\ {\isacharparenleft}SOME\ x{\isachardot}\ x\ {\isasymin}\ set\ xs{\isacharparenright}{\isachardoublequoteclose}%
 \isadelimML
 %
 \endisadelimML
@@ -310,7 +308,6 @@
 \isadelimML
 %
 \endisadelimML
-\isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ pick{\isacharunderscore}some\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}fail{\isacharunderscore}const{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
@@ -337,7 +334,7 @@
   The typical HOL tools are already set up in a way that
   function definitions introduced by \isa{{\isasymDEFINITION}},
   \isa{{\isasymFUN}},
-  \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}}
+  \isa{{\isasymFUNCTION}}, \isa{{\isasymPRIMREC}},
   \isa{{\isasymRECDEF}} are implicitly propagated
   to this defining equation table. Specific theorems may be
   selected using an attribute: \emph{code func}. As example,
@@ -353,7 +350,7 @@
 \ \ {\isachardoublequoteopen}pick\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ n\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharequal}\ x\ in\isanewline
 \ \ \ \ if\ n\ {\isacharless}\ k\ then\ v\ else\ pick\ xs\ {\isacharparenleft}n\ {\isacharminus}\ k{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
-We want to eliminate the explicit destruction
+\noindent We want to eliminate the explicit destruction
   of \isa{x} to \isa{{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -379,11 +376,11 @@
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ pick\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}pick{\isadigit{1}}{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-This theorem is now added to the defining equation table:
+\noindent This theorem now is used for generating code:
 
   \lstsml{Thy/examples/pick1.ML}
 
-  It might be convenient to remove the pointless original
+  \noindent It might be convenient to remove the pointless original
   equation, using the \emph{nofunc} attribute:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -395,7 +392,7 @@
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/pick2.ML}
 
-  Syntactic redundancies are implicitly dropped. For example,
+  \noindent Syntactic redundancies are implicitly dropped. For example,
   using a modified version of the \isa{fac} function
   as defining equation, the then redundant (since
   syntactically subsumed) original defining equations
@@ -445,7 +442,7 @@
   here we just illustrate its impact on code generation.
 
   In a target language, type classes may be represented
-  natively (as in the case of Haskell). For languages
+  natively (as in the case of Haskell).  For languages
   like SML, they are implemented using \emph{dictionaries}.
   Our following example specifies a class \qt{null},
   assigning to each of its inhabitants a \qt{null} value:%
@@ -455,14 +452,12 @@
 \ null\ {\isacharequal}\ type\ {\isacharplus}\isanewline
 \ \ \isakeyword{fixes}\ null\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
 \isanewline
-\isacommand{consts}\isamarkupfalse%
+\isacommand{fun}\isamarkupfalse%
 \isanewline
 \ \ head\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}null\ list\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\isanewline
+\isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}head\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ null{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\ \ {\isacharbar}\ {\isachardoublequoteopen}head\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 We provide some instances for our \isa{null}:%
 \end{isamarkuptext}%
@@ -522,8 +517,9 @@
 \ dummy\ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}examples{\isacharslash}{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
 \lsthaskell{Thy/examples/Codegen.hs}
+  \noindent (we have left out all other modules).
 
-  (we have left out all other modules).
+  \medskip
 
   The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
@@ -531,53 +527,20 @@
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ dummy\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/class.ML}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-or in OCaml:%
+\lstsml{Thy/examples/class.ML}
+
+  \medskip
+
+  \noindent or in OCaml:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
 \ dummy\ {\isacharparenleft}OCaml\ {\isachardoublequoteopen}examples{\isacharslash}class{\isachardot}ocaml{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/class.ocaml}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Incremental code generation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Code generation is \emph{incremental}: theorems
-  and abstract intermediate code are cached and extended on demand.
-  The cache may be partially or fully dropped if the underlying
-  executable content of the theory changes.
-  Implementation of caching is supposed to transparently
-  hid away the details from the user.  Anyway, caching
-  reaches the surface by using a slightly more general form
-  of the \isa{{\isasymCODEGEN}}: either the list of constants or the
-  list of serialization expressions may be dropped.  If no
-  serialization expressions are given, only abstract code
-  is generated and cached; if no constants are given, the
-  current cache is serialized.
+\lstsml{Thy/examples/class.ocaml}
 
-  For explorative purpose, the
-  \isa{{\isasymCODETHMS}} command may prove useful:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-\noindent print all cached defining equations (i.e.~\emph{after}
-  any applied transformation).  A
-  list of constants may be given; their function
-  equations are added to the cache if not already present.
-
-  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
-  visualizing dependencies between defining equations.%
+  \medskip The explicit association of constants
+  to classes can be inspected using the \isa{{\isasymPRINTCLASSES}}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -603,7 +566,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Library theories%
+\isamarkupsubsection{Library theories \label{sec:library}%
 }
 \isamarkuptrue%
 %
@@ -616,6 +579,13 @@
 
   \begin{description}
 
+    \item[\isa{Pretty{\isacharunderscore}Int}] represents HOL integers by big
+       integer literals in target languages.
+    \item[\isa{Pretty{\isacharunderscore}Char}] represents HOL characters by 
+       character literals in target languages.
+    \item[\isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr}] like \isa{Pretty{\isacharunderscore}Char{\isacharunderscore}chr},
+       but also offers treatment of character codes; includes
+       \isa{Pretty{\isacharunderscore}Int}.
     \item[\isa{ExecutableSet}] allows to generate code
        for finite sets using lists.
     \item[\isa{ExecutableRat}] \label{exec_rat} implements rational
@@ -623,10 +593,10 @@
     \item[\isa{EfficientNat}] \label{eff_nat} implements natural numbers by integers,
        which in general will result in higher efficency; pattern
        matching with \isa{{\isadigit{0}}} / \isa{Suc}
-       is eliminated.
+       is eliminated;  includes \isa{Pretty{\isacharunderscore}Int}.
     \item[\isa{MLString}] provides an additional datatype \isa{mlstring};
        in the HOL default setup, strings in HOL are mapped to list
-       of chars in SML; values of type \isa{mlstring} are
+       of HOL characters in SML; values of type \isa{mlstring} are
        mapped to strings in SML.
 
   \end{description}%
@@ -651,7 +621,6 @@
   equation, but never to the constant heading the left hand side.
   Inline theorems may be declared an undeclared using the
   \emph{code inline} or \emph{code noinline} attribute respectively.
-
   Some common applications:%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -745,10 +714,222 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Concerning operational equality%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Surely you have already noticed how equality is treated
+  by the code generator:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{fun}\isamarkupfalse%
+\isanewline
+\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
+\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
+\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
+\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
+\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+The membership test during preprocessing is rewritten,
+  resulting in \isa{op\ mem}, which itself
+  performs an explicit equality check.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/collect_duplicates.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Obviously, polymorphic equality is implemented the Haskell
+  way using a type class.  How is this achieved?  By an
+  almost trivial definition in the HOL setup:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isacommand{class}\isamarkupfalse%
+\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
+\begin{isamarkuptext}%
+This merely introduces a class \isa{eq} with corresponding
+  operation \isa{op\ {\isacharequal}};
+  the preprocessing framework does the rest.
+  For datatypes, instances of \isa{eq} are implicitly derived
+  when possible.
+
+  Though this \isa{eq} class is designed to get rarely in
+  the way, a subtlety
+  enters the stage when definitions of overloaded constants
+  are dependent on operational equality.  For example, let
+  us define a lexicographic ordering on tuples:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isacommand{instance}\isamarkupfalse%
+\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
+\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\isanewline
+\ \ \ \ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemmas}\isamarkupfalse%
+\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+Then code generation will fail.  Why?  The definition
+  of \isa{op\ {\isasymle}} depends on equality on both arguments,
+  which are polymorphic and impose an additional \isa{eq}
+  class constraint, thus violating the type discipline
+  for class operations.
+
+  The solution is to add \isa{eq} explicitly to the first sort arguments in the
+  code theorems:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
+\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{unfolding}\isamarkupfalse%
+\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
+\ rule{\isacharplus}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Then code generation succeeds:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\begin{isamarkuptext}%
+\lstsml{Thy/examples/lexicographic.ML}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In general, code theorems for overloaded constants may have more
+  restrictive sort constraints than the underlying instance relation
+  between class and type constructor as long as the whole system of
+  constraints is coregular; code theorems violating coregularity
+  are rejected immediately.  Consequently, it might be necessary
+  to delete disturbing theorems in the code theorem table,
+  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
+  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Programs as sets of theorems%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As told in \secref{sec:concept}, code generation is based
+  on a structured collection of code theorems.
+  For explorative purpose, this collection
+  may be inspected using the \isa{{\isasymCODETHMS}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
+\ {\isachardoublequoteopen}op\ mod\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}%
+\begin{isamarkuptext}%
+\noindent prints a table with \emph{all} defining equations
+  for \isa{op\ mod}, including
+  \emph{all} defining equations those equations depend
+  on recursivly.  \isa{{\isasymCODETHMS}} provides a convenient
+  mechanism to inspect the impact of a preprocessor setup
+  on defining equations.
+  
+  Similarly, the \isa{{\isasymCODEDEPS}} command shows a graph
+  visualizing dependencies between defining equations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Customizing serialization%
 }
 \isamarkuptrue%
 %
+\isamarkupsubsubsection{Basics%
+}
+\isamarkuptrue%
+%
 \begin{isamarkuptext}%
 Consider the following function and its corresponding
   SML code:%
@@ -757,8 +938,7 @@
 \isacommand{fun}\isamarkupfalse%
 \isanewline
 \ \ in{\isacharunderscore}interval\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}\isanewline
-%
+\ \ {\isachardoublequoteopen}in{\isacharunderscore}interval\ {\isacharparenleft}k{\isacharcomma}\ l{\isacharparenright}\ n\ {\isasymlongleftrightarrow}\ k\ {\isasymle}\ n\ {\isasymand}\ n\ {\isasymle}\ l{\isachardoublequoteclose}%
 \isadelimtt
 %
 \endisadelimtt
@@ -769,7 +949,6 @@
 {\isafoldtt}%
 %
 \isadelimtt
-\isanewline
 %
 \endisadelimtt
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
@@ -777,7 +956,7 @@
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_literal.ML}
 
-  Though this is correct code, it is a little bit unsatisfactory:
+  \noindent Though this is correct code, it is a little bit unsatisfactory:
   boolean values and operators are materialized as distinguished
   entities with have nothing to do with the SML-builtin notion
   of \qt{bool}.  This results in less readable code;
@@ -834,7 +1013,7 @@
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_mlbool.ML}
 
-  This still is not perfect: the parentheses
+  \noindent This still is not perfect: the parentheses
   around the \qt{andalso} expression are superfluous.
   Though the serializer
   by no means attempts to imitate the rich Isabelle syntax
@@ -864,11 +1043,12 @@
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/bool_infix.ML}
 
+  \medskip
+
   Next, we try to map HOL pairs to SML pairs, using the
   infix ``\verb|*|'' type constructor and parentheses:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isanewline
 %
 \isadelimtt
 %
@@ -878,7 +1058,6 @@
 \isacommand{code{\isacharunderscore}type}\isamarkupfalse%
 \ {\isacharasterisk}\isanewline
 \ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
 \ Pair\isanewline
 \ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
@@ -898,61 +1077,7 @@
   inserts a space which may be used as a break if necessary
   during pretty printing.
 
-  So far, we did only provide more idiomatic serializations for
-  constructs which would be executable on their own.  Target-specific
-  serializations may also be used to \emph{implement} constructs
-  which have no explicit notion of executability.  For example,
-  take the HOL integers:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ double{\isacharunderscore}inc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}double{\isacharunderscore}inc\ k\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-will fail: \isa{int} in HOL is implemented using a quotient
-  type, which does not provide any notion of executability.
-  \footnote{Eventually, we also want to provide executability
-  for quotients.}.  However, we could use the SML builtin
-  integers:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ int\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}int{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharplus}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isacharasterisk}\ {\isasymColon}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharplus}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}IntInf{\isachardot}{\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}{\isacharcomma}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ double{\isacharunderscore}inc\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}integers{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-resulting in:
-
-  \lstsml{Thy/examples/integers.ML}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-These examples give a glimpse what powerful mechanisms
+  These examples give a glimpse what mechanisms
   custom serializations provide; however their usage
   requires careful thinking in order not to introduce
   inconsistencies -- or, in other words:
@@ -971,284 +1096,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Concerning operational equality%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Surely you have already noticed how equality is treated
-  by the code generator:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\isanewline
-\ \ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
-\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
-\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
-\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
-\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-The membership test during preprocessing is rewritten,
-  resulting in \isa{op\ mem}, which itself
-  performs an explicit equality check.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}collect{\isacharunderscore}duplicates{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\lstsml{Thy/examples/collect_duplicates.ML}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Obviously, polymorphic equality is implemented the Haskell
-  way using a type class.  How is this achieved?  By an
-  almost trivial definition in the HOL setup:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
-\isacommand{class}\isamarkupfalse%
-\ eq\ {\isacharparenleft}\isakeyword{attach}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\ {\isacharequal}\ type%
-\begin{isamarkuptext}%
-This merely introduces a class \isa{eq} with corresponding
-  operation \isa{op\ {\isacharequal}};
-  the preprocessing framework does the rest.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-For datatypes, instances of \isa{eq} are implicitly derived
-  when possible.
-
-  Though this class is designed to get rarely in the way, there
-  are some cases when it suddenly comes to surface:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{typedecls interpreted by customary serializations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A common idiom is to use unspecified types for formalizations
-  and interpret them for a specific target language:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{typedecl}\isamarkupfalse%
-\ key\isanewline
-\isanewline
-\isacommand{fun}\isamarkupfalse%
-\isanewline
-\ \ lookup\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}key\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ list\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ {\isacharprime}a\ option{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}lookup\ {\isacharbrackleft}{\isacharbrackright}\ l\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}lookup\ {\isacharparenleft}{\isacharparenleft}k{\isacharcomma}\ v{\isacharparenright}\ {\isacharhash}\ xs{\isacharparenright}\ l\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isacharequal}\ l\ then\ Some\ v\ else\ lookup\ xs\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimtt
-\isanewline
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
-\ key\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}string{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\begin{isamarkuptext}%
-This, though, is not sufficient: \isa{key} is no instance
-  of \isa{eq} since \isa{key} is no datatype; the instance
-  has to be declared manually, including a serialization
-  for the particular instance of \isa{op\ {\isacharequal}}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ key\ {\isacharcolon}{\isacharcolon}\ eq%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-%
-\isadelimtt
-\isanewline
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isacharequal}\ {\isasymColon}\ key\ {\isasymRightarrow}\ key\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}\ {\isacharcolon}\ string{\isacharparenright}\ {\isacharequal}\ {\isacharunderscore}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\begin{isamarkuptext}%
-Then everything goes fine:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ lookup\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lookup{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\lstsml{Thy/examples/lookup.ML}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{lexicographic orderings%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Another subtlety
-  enters the stage when definitions of overloaded constants
-  are dependent on operational equality.  For example, let
-  us define a lexicographic ordering on tuples:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ord{\isacharcomma}\ ord{\isacharparenright}\ ord\isanewline
-\ \ less{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isacharless}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
-\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p{\isadigit{1}}\ {\isasymle}\ p{\isadigit{2}}\ {\isasymequiv}\ let\ {\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharequal}\ p{\isadigit{1}}{\isacharsemicolon}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ p{\isadigit{2}}\ in\isanewline
-\ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{lemmas}\isamarkupfalse%
-\ {\isacharbrackleft}code\ nofunc{\isacharbrackright}\ {\isacharequal}\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ ord{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}ord{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{unfolding}\isamarkupfalse%
-\ less{\isacharunderscore}prod{\isacharunderscore}def\ less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp{\isacharunderscore}all%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Then code generation will fail.  Why?  The definition
-  of \isa{op\ {\isasymle}} depends on equality on both arguments,
-  which are polymorphic and impose an additional \isa{eq}
-  class constraint, thus violating the type discipline
-  for class operations.
-
-  The solution is to add \isa{eq} explicitly to the first sort arguments in the
-  code theorems:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ ord{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}ord{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}ord{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ {\isacharparenleft}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isasymle}\ y{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-\ \ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{unfolding}\isamarkupfalse%
-\ ord{\isacharunderscore}prod\ \isacommand{by}\isamarkupfalse%
-\ rule{\isacharplus}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-Then code generation succeeds:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ {\isachardoublequoteopen}op\ {\isasymle}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}eq{\isacharcomma}\ ord{\isacharbraceright}\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}ord\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}lexicographic{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
-\begin{isamarkuptext}%
-\lstsml{Thy/examples/lexicographic.ML}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In general, code theorems for overloaded constants may have more
-  restrictive sort constraints than the underlying instance relation
-  between class and type constructor as long as the whole system of
-  constraints is coregular; code theorems violating coregularity
-  are rejected immediately.  Consequently, it might be necessary
-  to delete disturbing theorems in the code theorem table,
-  as we have done here with the original definitions \isa{less{\isacharunderscore}prod{\isacharunderscore}def}
-  and \isa{less{\isacharunderscore}eq{\isacharunderscore}prod{\isacharunderscore}def}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsubsubsection{Haskell serialization%
 }
 \isamarkuptrue%
@@ -1261,20 +1108,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-\isanewline
-%
 \isadelimtt
 %
 \endisadelimtt
@@ -1282,12 +1115,11 @@
 \isatagtt
 \isacommand{code{\isacharunderscore}class}\isamarkupfalse%
 \ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ eq\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\ {\isasymequiv}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharequal}{\isacharequal}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ eq\isanewline
-\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}\isanewline
-%
+\ {\isachardoublequoteopen}op\ {\isacharequal}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
 \endisatagtt
 {\isafoldtt}%
 %
@@ -1295,19 +1127,6 @@
 %
 \endisadelimtt
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \begin{isamarkuptext}%
 A problem now occurs whenever a type which
   is an instance of \isa{eq} in HOL is mapped
@@ -1374,78 +1193,119 @@
 %
 \endisadelimtt
 %
-\isamarkupsubsection{Types matter%
+\isamarkupsubsubsection{Pretty printing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The serializer provides ML interfaces to set up
+  pretty serializations for expressions like lists, numerals
+  and characters;  these are
+  monolithic stubs and should only be used with the
+  theories introduces in \secref{sec:library}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Constructor sets for datatypes%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Imagine the following quick-and-dirty setup for implementing
-  some kind of sets as lists in SML:%
+Conceptually, any datatype is spanned by a set of
+  \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n}
+  where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is excactly the set of \emph{all}
+  type variables in \isa{{\isasymtau}}.  The HOL datatype package
+  by default registers any new datatype in the table
+  of datatypes, which may be inspected using
+  the \isa{{\isasymPRINTCODESETUP}} command.
+
+  In some cases, it may be convenient to alter or
+  extend this table;  as an example, we show
+  how to implement finite sets by lists
+  using the conversion \isa{{\isachardoublequote}set\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequote}}
+  as constructor:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-%
-\isadelimtt
-%
-\endisadelimtt
-%
-\isatagtt
-\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
 \ set\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharunderscore}\ list{\isachardoublequoteclose}{\isacharparenright}\isanewline
-\isanewline
-\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ \isakeyword{and}\ insert\isanewline
-\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{and}\ \isakeyword{infixl}\ {\isadigit{7}}\ {\isachardoublequoteopen}{\isacharcolon}{\isacharcolon}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
-%
-\isadelimtt
-%
-\endisadelimtt
-\isanewline
-\isanewline
-\isacommand{definition}\isamarkupfalse%
 \isanewline
-\ \ dummy{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}nat\ {\isasymRightarrow}\ nat{\isacharparenright}\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}dummy{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}Suc{\isacharbraceright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-Then code generation for \isa{dummy{\isacharunderscore}set} will fail.
-  Why? A glimpse at the defining equations will offer:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
-\ insert%
-\begin{isamarkuptext}%
-This reveals the defining equation \isa{insert\ {\isacharquery}a\ {\isacharquery}B\ {\isasymequiv}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isacharequal}\ {\isacharquery}a{\isacharbraceright}\ {\isasymunion}\ {\isacharquery}B}
-  for \isa{insert}, which is operationally meaningless
-  but forces an equality constraint on the set members
-  (which is not satisfiable if the set members are functions).
-  Even when using set of natural numbers (which are an instance
-  of \emph{eq}), we run into a problem:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ foobar{\isacharunderscore}set\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}foobar{\isacharunderscore}set\ {\isacharequal}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequoteclose}%
-\begin{isamarkuptext}%
-In this case the serializer would complain that \isa{insert}
-  expects dictionaries (namely an \emph{eq} dictionary) but
-  has also been given a customary serialization.
-
-  \fixme[needs rewrite] The solution to this dilemma:%
-\end{isamarkuptext}%
-\isamarkuptrue%
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}insert\ {\isacharequal}\ insert{\isachardoublequoteclose}%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}\ {\isacharequal}\ set\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}%
 \isadelimproof
 \ %
 \endisadelimproof
 %
 \isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}insert\ x\ {\isacharparenleft}set\ xs{\isacharparenright}\ {\isacharequal}\ set\ {\isacharparenleft}x{\isacharhash}xs{\isacharparenright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
 %
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymunion}\ set\ ys\ {\isacharequal}\ foldr\ insert\ ys\ xs{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ ys{\isacharparenright}\ simp{\isacharunderscore}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymUnion}set\ xs\ {\isacharequal}\ foldr\ {\isacharparenleft}op\ {\isasymunion}{\isacharparenright}\ xs\ {\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -1455,51 +1315,14 @@
 \isanewline
 \isanewline
 \isacommand{code{\isacharunderscore}gen}\isamarkupfalse%
-\ dummy{\isacharunderscore}set\ foobar{\isacharunderscore}set\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}dirty{\isacharunderscore}set{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\ insert\ {\isachardoublequoteopen}op\ {\isasymin}{\isachardoublequoteclose}\ {\isachardoublequoteopen}op\ {\isasymunion}{\isachardoublequoteclose}\ {\isachardoublequoteopen}Union{\isachardoublequoteclose}\ {\isacharparenleft}SML\ {\isachardoublequoteopen}examples{\isacharslash}set{\isacharunderscore}list{\isachardot}ML{\isachardoublequoteclose}{\isacharparenright}%
 \begin{isamarkuptext}%
-\lstsml{Thy/examples/dirty_set.ML}
-
-  Reflexive defining equations by convention are dropped:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
-\ insert%
-\begin{isamarkuptext}%
-will show \emph{no} defining equations for insert.
+\lstsml{Thy/examples/set_list.ML}
 
-  Note that the sort constraints of reflexive equations
-  are considered; so%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isacharparenleft}insert\ {\isasymColon}\ {\isacharprime}a{\isasymColon}eq\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}\ {\isacharequal}\ insert{\isachardoublequoteclose}%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-would mean nothing else than to introduce the evil
-  sort constraint by hand.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Constructor sets for datatypes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\fixme%
+  \medskip
+
+  Changing the representation of existing datatypes requires
+  some care with respect to pattern matching and such.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1532,6 +1355,25 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsection{Incremental code generation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Code generation is \emph{incremental}: theorems
+  and abstract intermediate code are cached and extended on demand.
+  The cache may be partially or fully dropped if the underlying
+  executable content of the theory changes.
+  Implementation of caching is supposed to transparently
+  hid away the details from the user.  Anyway, caching
+  reaches the surface by using a slightly more general form
+  of the \isa{{\isasymCODETHMS}}, \isa{{\isasymCODEDEPS}}
+  and \isa{{\isasymCODEGEN}} commands: the list of constants
+  may be omitted.  Then, all constants with code theorems
+  in the current cache are referred to.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Axiomatic extensions%
 }
 \isamarkuptrue%
@@ -1611,6 +1453,8 @@
 \begin{isamarkuptext}%
 \lstsml{Thy/examples/arbitrary.ML}
 
+  \medskip
+
   Another axiomatic extension is code generation
   for abstracted types.  For this, the  
   \isa{ExecutableRat} (see \secref{exec_rat})
@@ -1911,13 +1755,13 @@
 
   \item \isa{merge} merging two data slots.
 
-  \item \isa{purge}~\isa{thy}~\isa{cs} propagates changes in executable content;
+  \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
     if possible, the current theory context is handed over
     as argument \isa{thy} (if there is no current theory context (e.g.~during
-    theory merge, \verb|NONE|); \isa{cs} indicates the kind
+    theory merge, \verb|NONE|); \isa{consts} indicates the kind
     of change: \verb|NONE| stands for a fundamental change
-    which invalidates any existing code, \isa{SOME\ cs}
-    hints that executable content for constants \isa{cs}
+    which invalidates any existing code, \isa{SOME\ consts}
+    hints that executable content for constants \isa{consts}
     has changed.
 
   \end{description}
@@ -1948,6 +1792,109 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsubsubsection{Building implementable systems fo defining equations%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Out of the executable content of a theory, a normalized
+  defining equation systems may be constructed containing
+  function definitions for constants.  The system is cached
+  until its underlying executable content changes.
+
+  Defining equations are retrieved by instantiation
+  of the functor \verb|CodegenFuncgrRetrieval|
+  which takes two arguments:
+
+  \medskip
+  \begin{tabular}{l}
+  \isa{val\ name{\isacharcolon}\ string} \\
+  \isa{val\ rewrites{\isacharcolon}\ theory\ {\isasymrightarrow}\ thm\ list}
+  \end{tabular}
+
+  \begin{description}
+
+  \item \isa{name} is a system-wide unique name identifying
+    this particular system of defining equations.
+
+  \item \isa{rewrites} specifies a set of theory-dependent
+    rewrite rules which are added to the preprocessor setup;
+    if no additional preprocessing is required, pass
+    a function returning an empty list.
+
+  \end{description}
+
+  An instance of \verb|CodegenFuncgrRetrieval| in essence
+  provides the following interface:
+
+  \medskip
+  \begin{tabular}{l}
+  \isa{make{\isacharcolon}\ theory\ {\isasymrightarrow}\ CodegenConsts{\isachardot}const\ list\ {\isasymrightarrow}\ CodegenFuncgr{\isachardot}T} \\
+  \end{tabular}
+
+  \begin{description}
+
+  \item \isa{make}~\isa{thy}~\isa{consts} returns
+    a system of defining equations which is guaranteed
+    to contain all defining equations for constants \isa{consts}
+    including all defining equations any defining equation
+    for any constant in \isa{consts} depends on.
+
+  \end{description}
+
+  Systems of defining equations are graphs accesible by the
+  following operations:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{CodegenFuncgr.T}\verb|type CodegenFuncgr.T| \\
+  \indexml{CodegenFuncgr.funcs}\verb|CodegenFuncgr.funcs: CodegenFuncgr.T -> CodegenConsts.const -> thm list| \\
+  \indexml{CodegenFuncgr.typ}\verb|CodegenFuncgr.typ: CodegenFuncgr.T -> CodegenConsts.const -> typ| \\
+  \indexml{CodegenFuncgr.deps}\verb|CodegenFuncgr.deps: CodegenFuncgr.T|\isasep\isanewline%
+\verb|    -> CodegenConsts.const list -> CodegenConsts.const list list| \\
+  \indexml{CodegenFuncgr.all}\verb|CodegenFuncgr.all: CodegenFuncgr.T -> CodegenConsts.const list|
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|CodegenFuncgr.T| represents
+    a normalized defining equation system.
+
+  \item \verb|CodegenFuncgr.funcs|~\isa{funcgr}~\isa{const}
+    retrieves defining equiations for constant \isa{const}.
+
+  \item \verb|CodegenFuncgr.typ|~\isa{funcgr}~\isa{const}
+    retrieves function type for constant \isa{const}.
+
+  \item \verb|CodegenFuncgr.deps|~\isa{funcgr}~\isa{consts}
+    returns the transitive closure of dependencies for
+    constants \isa{consts} as a partitioning where each partition
+    corresponds to a strongly connected component of
+    dependencies and any partition does \emph{not}
+    depend on partitions further left.
+
+  \item \verb|CodegenFuncgr.all|~\isa{funcgr}
+    returns all currently represented constants.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
 \isamarkupsubsubsection{Datatype hooks%
 }
 \isamarkuptrue%

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Thu Apr 26 13:32:55 2007 +0200
@@ -6,7 +6,7 @@
   nulla :: a;
 };
 
-heada :: (Codegen.Null a) => [a] -> a;
+heada :: (Codegen.Null b) => [b] -> b;
 heada (x : xs) = x;
 heada [] = Codegen.nulla;
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -14,8 +14,8 @@
 type 'a null = {null : 'a};
 fun null (A_:'a null) = #null A_;
 
-fun head A_ (x :: xs) = x
-  | head A_ [] = null A_;
+fun head B_ (x :: xs) = x
+  | head B_ [] = null B_;
 
 val null_option : 'a option = NONE;
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/class.ocaml	Thu Apr 26 13:32:55 2007 +0200
@@ -14,8 +14,8 @@
 type 'a null = {null : 'a};;
 let null _A = _A.null;;
 
-let rec head _A = function x :: xs -> x
-                  | [] -> null _A;;
+let rec head _B = function x :: xs -> x
+                  | [] -> null _B;;
 
 let rec null_option = None;;
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -21,12 +21,12 @@
 structure Codegen = 
 struct
 
-fun collect_duplicates A_ xs ys (z :: zs) =
-  (if List.memberl A_ z xs
-    then (if List.memberl A_ z ys then collect_duplicates A_ xs ys zs
-           else collect_duplicates A_ xs (z :: ys) zs)
-    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
-  | collect_duplicates A_ xs ys [] = xs;
+fun collect_duplicates B_ xs ys (z :: zs) =
+  (if List.memberl B_ z xs
+    then (if List.memberl B_ z ys then collect_duplicates B_ xs ys zs
+           else collect_duplicates B_ xs (z :: ys) zs)
+    else collect_duplicates B_ (z :: xs) (z :: ys) zs)
+  | collect_duplicates B_ xs ys [] = xs;
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -11,9 +11,73 @@
 structure Integer = 
 struct
 
+datatype bit = B0 | B1;
+
+datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
+
+fun pred (Bit (k, B0)) = Bit (pred k, B1)
+  | pred (Bit (k, B1)) = Bit (k, B0)
+  | pred Min = Bit (Min, B0)
+  | pred Pls = Min;
+
+fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
+  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
+  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
+  | uminus_int Min = Bit (Pls, B1)
+  | uminus_int Pls = Pls;
+
+fun succ (Bit (k, B0)) = Bit (k, B1)
+  | succ (Bit (k, B1)) = Bit (succ k, B0)
+  | succ Min = Pls
+  | succ Pls = Bit (Pls, B1);
+
+fun plus_int (Number_of_int v) (Number_of_int w) =
+  Number_of_int (plus_int v w)
+  | plus_int k Min = pred k
+  | plus_int k Pls = k
+  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
+  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
+  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
+  | plus_int Min k = pred k
+  | plus_int Pls k = k;
+
+fun minus_int (Number_of_int v) (Number_of_int w) =
+  Number_of_int (plus_int v (uminus_int w))
+  | minus_int z w = plus_int z (uminus_int w);
+
+fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l
+  | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2
+  | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2
+  | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2
+  | less_eq_int (Bit (k, v)) Min = less_eq_int k Min
+  | less_eq_int (Bit (k, B1)) Pls = less_int k Pls
+  | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls
+  | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k
+  | less_eq_int Min (Bit (k, B0)) = less_int Min k
+  | less_eq_int Min Min = true
+  | less_eq_int Min Pls = true
+  | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k
+  | less_eq_int Pls Min = false
+  | less_eq_int Pls Pls = true
+and less_int (Number_of_int k) (Number_of_int l) = less_int k l
+  | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2
+  | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2
+  | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2
+  | less_int (Bit (k, B1)) Min = less_int k Min
+  | less_int (Bit (k, B0)) Min = less_eq_int k Min
+  | less_int (Bit (k, v)) Pls = less_int k Pls
+  | less_int Min (Bit (k, v)) = less_int Min k
+  | less_int Min Min = false
+  | less_int Min Pls = true
+  | less_int Pls (Bit (k, B1)) = less_eq_int Pls k
+  | less_int Pls (Bit (k, B0)) = less_int Pls k
+  | less_int Pls Min = false
+  | less_int Pls Pls = false;
+
 fun nat_aux n i =
-  (if IntInf.<= (i, (0 : IntInf.int)) then n
-    else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
+  (if less_eq_int i (Number_of_int Pls) then n
+    else nat_aux (Nat.Suc n)
+           (minus_int i (Number_of_int (Bit (Pls, B1)))));
 
 fun nat i = nat_aux Nat.Zero_nat i;
 
@@ -26,7 +90,12 @@
 
 val foobar_set : Nat.nat list =
   Nat.Zero_nat ::
-    (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
+    (Nat.Suc Nat.Zero_nat ::
+      (Integer.nat
+         (Integer.Number_of_int
+           (Integer.Bit
+             (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
+        :: []));
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -1,11 +1,58 @@
 structure ROOT = 
 struct
 
+structure Integer = 
+struct
+
+datatype bit = B0 | B1;
+
+datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
+
+fun pred (Bit (k, B0)) = Bit (pred k, B1)
+  | pred (Bit (k, B1)) = Bit (k, B0)
+  | pred Min = Bit (Min, B0)
+  | pred Pls = Min;
+
+fun succ (Bit (k, B0)) = Bit (k, B1)
+  | succ (Bit (k, B1)) = Bit (succ k, B0)
+  | succ Min = Pls
+  | succ Pls = Bit (Pls, B1);
+
+fun plus_int (Number_of_int v) (Number_of_int w) =
+  Number_of_int (plus_int v w)
+  | plus_int k Min = pred k
+  | plus_int k Pls = k
+  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
+  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
+  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
+  | plus_int Min k = pred k
+  | plus_int Pls k = k;
+
+fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
+  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
+  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
+  | uminus_int Min = Bit (Pls, B1)
+  | uminus_int Pls = Pls;
+
+fun times_int (Number_of_int v) (Number_of_int w) =
+  Number_of_int (times_int v w)
+  | times_int (Bit (k, B0)) l = Bit (times_int k l, B0)
+  | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l
+  | times_int Min k = uminus_int k
+  | times_int Pls w = Pls;
+
+end; (*struct Integer*)
+
 structure Codegen = 
 struct
 
 fun double_inc k =
-  IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int));
+  Integer.plus_int
+    (Integer.times_int
+      (Integer.Number_of_int
+        (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
+      k)
+    (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1)));
 
 end; (*struct Codegen*)
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -0,0 +1,41 @@
+structure ROOT = 
+struct
+
+structure Code_Generator = 
+struct
+
+type 'a eq = {op_eq : 'a -> 'a -> bool};
+fun op_eq (A_:'a eq) = #op_eq A_;
+
+end; (*struct Code_Generator*)
+
+structure List = 
+struct
+
+fun foldr f (x :: xs) a = f x (foldr f xs a)
+  | foldr f [] a = a;
+
+fun memberl A_ x (y :: ys) =
+  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
+  | memberl A_ x [] = false;
+
+end; (*struct List*)
+
+structure Set = 
+struct
+
+datatype 'a set = Set of 'a list;
+
+fun opa A_ x (Set xs) = List.memberl A_ x xs;
+
+val empty : 'a set = Set [];
+
+fun insert x (Set xs) = Set (x :: xs);
+
+fun op_Un xs (Set ys) = List.foldr insert ys xs;
+
+fun union (Set xs) = List.foldr op_Un xs empty;
+
+end; (*struct Set*)
+
+end; (*struct ROOT*)

--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Thu Apr 26 13:32:55 2007 +0200
@@ -47,6 +47,8 @@
   Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
   NibbleC | NibbleD | NibbleE | NibbleF;
 
+datatype char = Char of nibble * nibble;
+
 end; (*struct List*)
 
 structure Codegen = 
@@ -55,19 +57,26 @@
 datatype ('a, 'b) searchtree = Leaf of 'a * 'b |
   Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
 
-fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
-  (if Orderings.less_eq A2_ it key
-    then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
-    else Branch (t1, key, update (A1_, A2_) (it, entry) t2))
-  | update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
-    (if Code_Generator.op_eq A1_ it key then Leaf (key, entry)
-      else (if Orderings.less_eq A2_ it key
+fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
+  (if Orderings.less_eq C2_ it key
+    then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
+    else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
+  | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
+    (if Code_Generator.op_eq C1_ it key then Leaf (key, entry)
+      else (if Orderings.less_eq C2_ it key
              then Branch (Leaf (it, entry), it, Leaf (key, vala))
              else Branch (Leaf (key, vala), it, Leaf (it, entry))));
 
 fun example n =
-  update (Nat.eq_nat, Nat.ord_nat) (n, [#"b", #"a", #"r"])
-    (Leaf (Nat.Zero_nat, [#"f", #"o", #"o"]));
+  update (Nat.eq_nat, Nat.ord_nat)
+    (n, [List.Char (List.Nibble6, List.Nibble2),
+          List.Char (List.Nibble6, List.Nibble1),
+          List.Char (List.Nibble7, List.Nibble2)])
+    (Leaf
+      (Nat.Zero_nat,
+        [List.Char (List.Nibble6, List.Nibble6),
+          List.Char (List.Nibble6, List.NibbleF),
+          List.Char (List.Nibble6, List.NibbleF)]));
 
 end; (*struct Codegen*)
 

--- a/doc-src/IsarAdvanced/Codegen/codegen.tex	Thu Apr 26 12:00:12 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex	Thu Apr 26 13:32:55 2007 +0200
@@ -44,6 +44,7 @@
 \newcommand{\isasymCODEAXIOMS}{\cmd{code\_axioms}}
 \newcommand{\isasymCODEABSTYPE}{\cmd{code\_abstype}}
 \newcommand{\isasymPRINTCODESETUP}{\cmd{print\_codesetup}}
+\newcommand{\isasymPRINTCLASSES}{\cmd{print\_classes}}
 \newcommand{\isasymCODETHMS}{\cmd{code\_thms}}
 \newcommand{\isasymCODEDEPS}{\cmd{code\_deps}}
 \newcommand{\isasymFUN}{\cmd{fun}}