# HG changeset patch
# User wenzelm
# Date 1282055925 -7200
# Node ID e0b8b173368995f80c4802964065499f04723970
# Parent  0e4565062017171717a2a4e19671234e82d542f5# Parent  2eb6bad282b1e5d99dc65e67ba4e9579a42dc7b0
merged

diff -r 2eb6bad282b1 -r e0b8b1733689 CONTRIBUTORS
--- a/CONTRIBUTORS	Tue Aug 17 15:54:04 2010 +0200
+++ b/CONTRIBUTORS	Tue Aug 17 16:38:45 2010 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* July 2010: Florian Haftmann, TUM
+  Reworking and extension of the Isabelle/HOL framework.
+
 
 Contributions to Isabelle2009-2
 --------------------------------------
diff -r 2eb6bad282b1 -r e0b8b1733689 NEWS
--- a/NEWS	Tue Aug 17 15:54:04 2010 +0200
+++ b/NEWS	Tue Aug 17 16:38:45 2010 +0200
@@ -35,11 +35,17 @@
 
 *** HOL ***
 
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
 * Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
 in Library/State_Monad has been changed to avoid ambiguities.
 INCOMPATIBILITY.
 
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
 to standard output.  INCOMPATIBILITY.
 
 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
 INCOMPATIBILITY.
 
 * Inductive package: offers new command "inductive_simps" to automatically
-  derive instantiated and simplified equations for inductive predicates,
-  similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
 
 
 *** ML ***
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Tue Aug 17 16:38:45 2010 +0200
@@ -13,18 +13,21 @@
   in common:
 
   \begin{itemize}
-    \item They act uniformly, without reference to a specific
-       target language.
+
+    \item They act uniformly, without reference to a specific target
+       language.
+
     \item They are \emph{safe} in the sense that as long as you trust
        the code generator meta theory and implementation, you cannot
-       produce programs that yield results which are not derivable
-       in the logic.
+       produce programs that yield results which are not derivable in
+       the logic.
+
   \end{itemize}
 
-  \noindent In this section we will introduce means to \emph{adapt} the serialiser
-  to a specific target language, i.e.~to print program fragments
-  in a way which accommodates \qt{already existing} ingredients of
-  a target language environment, for three reasons:
+  \noindent In this section we will introduce means to \emph{adapt}
+  the serialiser to a specific target language, i.e.~to print program
+  fragments in a way which accommodates \qt{already existing}
+  ingredients of a target language environment, for three reasons:
 
   \begin{itemize}
     \item improving readability and aesthetics of generated code
@@ -37,26 +40,34 @@
   \emph{at any cost}:
 
   \begin{itemize}
-    \item The safe configuration methods act uniformly on every target language,
-      whereas for adaptation you have to treat each target language separately.
-    \item Application is extremely tedious since there is no abstraction
-      which would allow for a static check, making it easy to produce garbage.
+
+    \item The safe configuration methods act uniformly on every target
+      language, whereas for adaptation you have to treat each target
+      language separately.
+
+    \item Application is extremely tedious since there is no
+      abstraction which would allow for a static check, making it easy
+      to produce garbage.
+
     \item Subtle errors can be introduced unconsciously.
+
   \end{itemize}
 
-  \noindent However, even if you ought refrain from setting up adaptation
-  yourself, already the @{text "HOL"} comes with some reasonable default
-  adaptations (say, using target language list syntax).  There also some
-  common adaptation cases which you can setup by importing particular
-  library theories.  In order to understand these, we provide some clues here;
-  these however are not supposed to replace a careful study of the sources.
+  \noindent However, even if you ought refrain from setting up
+  adaptation yourself, already the @{text "HOL"} comes with some
+  reasonable default adaptations (say, using target language list
+  syntax).  There also some common adaptation cases which you can
+  setup by importing particular library theories.  In order to
+  understand these, we provide some clues here; these however are not
+  supposed to replace a careful study of the sources.
 *}
 
+
 subsection {* The adaptation principle *}
 
 text {*
-  Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
-  supposed to be:
+  Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
+  conceptually supposed to be:
 
   \begin{figure}[here]
     \includegraphics{adaptation}
@@ -65,79 +76,87 @@
   \end{figure}
 
   \noindent In the tame view, code generation acts as broker between
-  @{text logic}, @{text "intermediate language"} and
-  @{text "target language"} by means of @{text translation} and
-  @{text serialisation};  for the latter, the serialiser has to observe
-  the structure of the @{text language} itself plus some @{text reserved}
-  keywords which have to be avoided for generated code.
-  However, if you consider @{text adaptation} mechanisms, the code generated
-  by the serializer is just the tip of the iceberg:
+  @{text logic}, @{text "intermediate language"} and @{text "target
+  language"} by means of @{text translation} and @{text
+  serialisation}; for the latter, the serialiser has to observe the
+  structure of the @{text language} itself plus some @{text reserved}
+  keywords which have to be avoided for generated code.  However, if
+  you consider @{text adaptation} mechanisms, the code generated by
+  the serializer is just the tip of the iceberg:
 
   \begin{itemize}
+
     \item @{text serialisation} can be \emph{parametrised} such that
       logical entities are mapped to target-specific ones
-      (e.g. target-specific list syntax,
-        see also \secref{sec:adaptation_mechanisms})
+      (e.g. target-specific list syntax, see also
+      \secref{sec:adaptation_mechanisms})
+
     \item Such parametrisations can involve references to a
-      target-specific standard @{text library} (e.g. using
-      the @{text Haskell} @{verbatim Maybe} type instead
-      of the @{text HOL} @{type "option"} type);
-      if such are used, the corresponding identifiers
-      (in our example, @{verbatim Maybe}, @{verbatim Nothing}
-      and @{verbatim Just}) also have to be considered @{text reserved}.
+      target-specific standard @{text library} (e.g. using the @{text
+      Haskell} @{verbatim Maybe} type instead of the @{text HOL}
+      @{type "option"} type); if such are used, the corresponding
+      identifiers (in our example, @{verbatim Maybe}, @{verbatim
+      Nothing} and @{verbatim Just}) also have to be considered @{text
+      reserved}.
+
     \item Even more, the user can enrich the library of the
-      target-language by providing code snippets
-      (\qt{@{text "includes"}}) which are prepended to
-      any generated code (see \secref{sec:include});  this typically
-      also involves further @{text reserved} identifiers.
+      target-language by providing code snippets (\qt{@{text
+      "includes"}}) which are prepended to any generated code (see
+      \secref{sec:include}); this typically also involves further
+      @{text reserved} identifiers.
+
   \end{itemize}
 
-  \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
-  have to act consistently;  it is at the discretion of the user
-  to take care for this.
+  \noindent As figure \ref{fig:adaptation} illustrates, all these
+  adaptation mechanisms have to act consistently; it is at the
+  discretion of the user to take care for this.
 *}
 
 subsection {* Common adaptation patterns *}
 
 text {*
   The @{theory HOL} @{theory Main} theory already provides a code
-  generator setup
-  which should be suitable for most applications.  Common extensions
-  and modifications are available by certain theories of the @{text HOL}
-  library; beside being useful in applications, they may serve
-  as a tutorial for customising the code generator setup (see below
-  \secref{sec:adaptation_mechanisms}).
+  generator setup which should be suitable for most applications.
+  Common extensions and modifications are available by certain
+  theories of the @{text HOL} library; beside being useful in
+  applications, they may serve as a tutorial for customising the code
+  generator setup (see below \secref{sec:adaptation_mechanisms}).
 
   \begin{description}
 
-    \item[@{theory "Code_Integer"}] represents @{text HOL} integers by big
-       integer literals in target languages.
-    \item[@{theory "Code_Char"}] represents @{text HOL} characters by 
+    \item[@{theory "Code_Integer"}] represents @{text HOL} integers by
+       big integer literals in target languages.
+
+    \item[@{theory "Code_Char"}] represents @{text HOL} characters by
        character literals in target languages.
-    \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"},
-       but also offers treatment of character codes; includes
-       @{theory "Code_Char"}.
-    \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
-       which in general will result in higher efficiency; pattern
-       matching with @{term "0\<Colon>nat"} / @{const "Suc"}
-       is eliminated;  includes @{theory "Code_Integer"}
+
+    \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but
+       also offers treatment of character codes; includes @{theory
+       "Code_Char"}.
+
+    \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements
+       natural numbers by integers, which in general will result in
+       higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
+       @{const "Suc"} is eliminated; includes @{theory "Code_Integer"}
        and @{theory "Code_Numeral"}.
+
     \item[@{theory "Code_Numeral"}] provides an additional datatype
-       @{typ index} which is mapped to target-language built-in integers.
-       Useful for code setups which involve e.g. indexing of
-       target-language arrays.
-    \item[@{theory "String"}] provides an additional datatype
-       @{typ String.literal} which is isomorphic to strings;
-       @{typ String.literal}s are mapped to target-language strings.
-       Useful for code setups which involve e.g. printing (error) messages.
+       @{typ index} which is mapped to target-language built-in
+       integers.  Useful for code setups which involve e.g.~indexing
+       of target-language arrays.
+
+    \item[@{theory "String"}] provides an additional datatype @{typ
+       String.literal} which is isomorphic to strings; @{typ
+       String.literal}s are mapped to target-language strings.  Useful
+       for code setups which involve e.g.~printing (error) messages.
 
   \end{description}
 
   \begin{warn}
     When importing any of these theories, they should form the last
-    items in an import list.  Since these theories adapt the
-    code generator setup in a non-conservative fashion,
-    strange effects may occur otherwise.
+    items in an import list.  Since these theories adapt the code
+    generator setup in a non-conservative fashion, strange effects may
+    occur otherwise.
   \end{warn}
 *}
 
@@ -145,8 +164,7 @@
 subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
 
 text {*
-  Consider the following function and its corresponding
-  SML code:
+  Consider the following function and its corresponding SML code:
 *}
 
 primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -160,15 +178,14 @@
 text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
-  \noindent Though this is correct code, it is a little bit unsatisfactory:
-  boolean values and operators are materialised as distinguished
-  entities with have nothing to do with the SML-built-in notion
-  of \qt{bool}.  This results in less readable code;
-  additionally, eager evaluation may cause programs to
-  loop or break which would perfectly terminate when
-  the existing SML @{verbatim "bool"} would be used.  To map
-  the HOL @{typ bool} on SML @{verbatim "bool"}, we may use
-  \qn{custom serialisations}:
+  \noindent Though this is correct code, it is a little bit
+  unsatisfactory: boolean values and operators are materialised as
+  distinguished entities with have nothing to do with the SML-built-in
+  notion of \qt{bool}.  This results in less readable code;
+  additionally, eager evaluation may cause programs to loop or break
+  which would perfectly terminate when the existing SML @{verbatim
+  "bool"} would be used.  To map the HOL @{typ bool} on SML @{verbatim
+  "bool"}, we may use \qn{custom serialisations}:
 *}
 
 code_type %quotett bool
@@ -178,25 +195,23 @@
 
 text {*
   \noindent The @{command code_type} command takes a type constructor
-  as arguments together with a list of custom serialisations.
-  Each custom serialisation starts with a target language
-  identifier followed by an expression, which during
-  code serialisation is inserted whenever the type constructor
-  would occur.  For constants, @{command code_const} implements
-  the corresponding mechanism.  Each ``@{verbatim "_"}'' in
-  a serialisation expression is treated as a placeholder
-  for the type constructor's (the constant's) arguments.
+  as arguments together with a list of custom serialisations.  Each
+  custom serialisation starts with a target language identifier
+  followed by an expression, which during code serialisation is
+  inserted whenever the type constructor would occur.  For constants,
+  @{command code_const} implements the corresponding mechanism.  Each
+  ``@{verbatim "_"}'' in a serialisation expression is treated as a
+  placeholder for the type constructor's (the constant's) arguments.
 *}
 
 text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
-  \noindent This still is not perfect: the parentheses
-  around the \qt{andalso} expression are superfluous.
-  Though the serialiser
-  by no means attempts to imitate the rich Isabelle syntax
-  framework, it provides some common idioms, notably
-  associative infixes with precedences which may be used here:
+  \noindent This still is not perfect: the parentheses around the
+  \qt{andalso} expression are superfluous.  Though the serialiser by
+  no means attempts to imitate the rich Isabelle syntax framework, it
+  provides some common idioms, notably associative infixes with
+  precedences which may be used here:
 *}
 
 code_const %quotett "op \<and>"
@@ -205,12 +220,13 @@
 text %quote {*@{code_stmts in_interval (SML)}*}
 
 text {*
-  \noindent The attentive reader may ask how we assert that no generated
-  code will accidentally overwrite.  For this reason the serialiser has
-  an internal table of identifiers which have to be avoided to be used
-  for new declarations.  Initially, this table typically contains the
-  keywords of the target language.  It can be extended manually, thus avoiding
-  accidental overwrites, using the @{command "code_reserved"} command:
+  \noindent The attentive reader may ask how we assert that no
+  generated code will accidentally overwrite.  For this reason the
+  serialiser has an internal table of identifiers which have to be
+  avoided to be used for new declarations.  Initially, this table
+  typically contains the keywords of the target language.  It can be
+  extended manually, thus avoiding accidental overwrites, using the
+  @{command "code_reserved"} command:
 *}
 
 code_reserved %quote "\<SML>" bool true false andalso
@@ -232,37 +248,33 @@
 
 text {*
   \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
-  never to put
-  parentheses around the whole expression (they are already present),
-  while the parentheses around argument place holders
-  tell not to put parentheses around the arguments.
-  The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
-  inserts a space which may be used as a break if necessary
-  during pretty printing.
+  never to put parentheses around the whole expression (they are
+  already present), while the parentheses around argument place
+  holders tell not to put parentheses around the arguments.  The slash
+  ``@{verbatim "/"}'' (followed by arbitrary white space) inserts a
+  space which may be used as a break if necessary during pretty
+  printing.
 
-  These examples give a glimpse what mechanisms
-  custom serialisations provide; however their usage
-  requires careful thinking in order not to introduce
-  inconsistencies -- or, in other words:
-  custom serialisations are completely axiomatic.
+  These examples give a glimpse what mechanisms custom serialisations
+  provide; however their usage requires careful thinking in order not
+  to introduce inconsistencies -- or, in other words: custom
+  serialisations are completely axiomatic.
 
-  A further noteworthy details is that any special
-  character in a custom serialisation may be quoted
-  using ``@{verbatim "'"}''; thus, in
-  ``@{verbatim "fn '_ => _"}'' the first
-  ``@{verbatim "_"}'' is a proper underscore while the
-  second ``@{verbatim "_"}'' is a placeholder.
+  A further noteworthy details is that any special character in a
+  custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
+  in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
+  proper underscore while the second ``@{verbatim "_"}'' is a
+  placeholder.
 *}
 
 
 subsection {* @{text Haskell} serialisation *}
 
 text {*
-  For convenience, the default
-  @{text HOL} setup for @{text Haskell} maps the @{class eq} class to
-  its counterpart in @{text Haskell}, giving custom serialisations
-  for the class @{class eq} (by command @{command code_class}) and its operation
-  @{const HOL.eq}
+  For convenience, the default @{text HOL} setup for @{text Haskell}
+  maps the @{class eq} class to its counterpart in @{text Haskell},
+  giving custom serialisations for the class @{class eq} (by command
+  @{command code_class}) and its operation @{const HOL.eq}
 *}
 
 code_class %quotett eq
@@ -272,10 +284,10 @@
   (Haskell infixl 4 "==")
 
 text {*
-  \noindent A problem now occurs whenever a type which
-  is an instance of @{class eq} in @{text HOL} is mapped
-  on a @{text Haskell}-built-in type which is also an instance
-  of @{text Haskell} @{text Eq}:
+  \noindent A problem now occurs whenever a type which is an instance
+  of @{class eq} in @{text HOL} is mapped on a @{text
+  Haskell}-built-in type which is also an instance of @{text Haskell}
+  @{text Eq}:
 *}
 
 typedecl %quote bar
@@ -293,11 +305,9 @@
   (Haskell "Integer")
 
 text {*
-  \noindent The code generator would produce
-  an additional instance, which of course is rejected by the @{text Haskell}
-  compiler.
-  To suppress this additional instance, use
-  @{text "code_instance"}:
+  \noindent The code generator would produce an additional instance,
+  which of course is rejected by the @{text Haskell} compiler.  To
+  suppress this additional instance, use @{text "code_instance"}:
 *}
 
 code_instance %quotett bar :: eq
@@ -308,8 +318,8 @@
 
 text {*
   In rare cases it is necessary to \emph{enrich} the context of a
-  target language;  this is accomplished using the @{command "code_include"}
-  command:
+  target language; this is accomplished using the @{command
+  "code_include"} command:
 *}
 
 code_include %quotett Haskell "Errno"
@@ -318,9 +328,10 @@
 code_reserved %quotett Haskell Errno
 
 text {*
-  \noindent Such named @{text include}s are then prepended to every generated code.
-  Inspect such code in order to find out how @{command "code_include"} behaves
-  with respect to a particular target language.
+  \noindent Such named @{text include}s are then prepended to every
+  generated code.  Inspect such code in order to find out how
+  @{command "code_include"} behaves with respect to a particular
+  target language.
 *}
 
 end
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/Foundations.thy
--- a/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy	Tue Aug 17 16:38:45 2010 +0200
@@ -7,7 +7,6 @@
 subsection {* Code generator architecture \label{sec:architecture} *}
 
 text {*
-
   The code generator is actually a framework consisting of different
   components which can be customised individually.
 
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy	Tue Aug 17 16:38:45 2010 +0200
@@ -4,23 +4,83 @@
 
 section {* Program and datatype refinement \label{sec:refinement} *}
 
-subsection {* Datatypes \label{sec:datatypes} *}
+text {*
+  Code generation by shallow embedding (cf.~\secref{sec:principle})
+  allows to choose code equations and datatype constructors freely,
+  given that some very basic syntactic properties are met; this
+  flexibility opens up mechanisms for refinement which allow to extend
+  the scope and quality of generated code dramatically.
+*}
+
+
+subsection {* Program refinement *}
+
+text {*
+  Program refinement works by choosing appropriate code equations
+  explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+  numbers:
+*}
+
+fun %quote fib :: "nat \<Rightarrow> nat" where
+    "fib 0 = 0"
+  | "fib (Suc 0) = Suc 0"
+  | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+text {*
+  \noindent The runtime of the corresponding code grows exponential due
+  to two recursive calls:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib (Haskell)}*}
 
 text {*
-  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 exactly 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
-  @{command print_codesetup} command.
+  \noindent A more efficient implementation would use dynamic
+  programming, e.g.~sharing of common intermediate results between
+  recursive calls.  This idea is expressed by an auxiliary operation
+  which computes a Fibonacci number and its successor simultaneously:
+*}
+
+definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
+  "fib_step n = (fib (Suc n), fib n)"
+
+text {*
+  \noindent This operation can be implemented by recursion using
+  dynamic programming:
+*}
+
+lemma %quote [code]:
+  "fib_step 0 = (Suc 0, 0)"
+  "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
+  by (simp_all add: fib_step_def)
+
+text {*
+  \noindent What remains is to implement @{const fib} by @{const
+  fib_step} as follows:
+*}
 
-  In some cases, it is appropriate to alter or extend this table.  As
-  an example, we will develop an alternative representation of the
-  queue example given in \secref{sec:queue_example}.  The amortised
-  representation is convenient for generating code but exposes its
-  \qt{implementation} details, which may be cumbersome when proving
-  theorems about it.  Therefore, here is a simple, straightforward
-  representation of queues:
+lemma %quote [code]:
+  "fib 0 = 0"
+  "fib (Suc n) = fst (fib_step n)"
+  by (simp_all add: fib_step_def)
+
+text {*
+  \noindent The resulting code shows only linear growth of runtime:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
+
+
+subsection {* Datatype refinement *}
+
+text {*
+  Selecting specific code equations \emph{and} datatype constructors
+  leads to datatype refinement.  As an example, we will develop an
+  alternative representation of the queue example given in
+  \secref{sec:queue_example}.  The amortised representation is
+  convenient for generating code but exposes its \qt{implementation}
+  details, which may be cumbersome when proving theorems about it.
+  Therefore, here is a simple, straightforward representation of
+  queues:
 *}
 
 datatype %quote 'a queue = Queue "'a list"
@@ -49,7 +109,18 @@
   \noindent Here we define a \qt{constructor} @{const "AQueue"} which
   is defined in terms of @{text "Queue"} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
-  to be.  Equipped with this, we are able to prove the following equations
+  to be.
+
+  The prerequisite for datatype constructors is only syntactical: a
+  constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+  "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+  @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype.  The
+  HOL datatype package by default registers any new datatype with its
+  constructors, but this may be changed using @{command
+  code_datatype}; the currently chosen constructors can be inspected
+  using the @{command print_codesetup} command.
+
+  Equipped with this, we are able to prove the following equations
   for our primitive queue operations which \qt{implement} the simple
   queues in an amortised fashion:
 *}
@@ -85,28 +156,21 @@
 text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
 
 text {*
-  \noindent From this example, it can be glimpsed that using own
-  constructor sets is a little delicate since it changes the set of
-  valid patterns for values of that type.  Without going into much
-  detail, here some practical hints:
-
-  \begin{itemize}
-
-    \item When changing the constructor set for datatypes, take care
-      to provide alternative equations for the @{text case} combinator.
+  The same techniques can also be applied to types which are not
+  specified as datatypes, e.g.~type @{typ int} is originally specified
+  as quotient type by means of @{command typedef}, but for code
+  generation constants allowing construction of binary numeral values
+  are used as constructors for @{typ int}.
 
-    \item Values in the target language need not to be normalised --
-      different values in the target language may represent the same
-      value in the logic.
+  This approach however fails if the representation of a type demands
+  invariants; this issue is discussed in the next section.
+*}
+
 
-    \item Usually, a good methodology to deal with the subtleties of
-      pattern matching is to see the type as an abstract type: provide
-      a set of operations which operate on the concrete representation
-      of the type, and derive further operations by combinations of
-      these primitive ones, without relying on a particular
-      representation.
+subsection {* Datatype refinement involving invariants *}
 
-  \end{itemize}
+text {*
+  FIXME
 *}
 
 end
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Tue Aug 17 16:38:45 2010 +0200
@@ -1,5 +1,5 @@
 theory Setup
-imports Complex_Main
+imports Complex_Main More_List
 uses
   "../../antiquote_setup.ML"
   "../../more_antiquote.ML"
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Tue Aug 17 16:38:45 2010 +0200
@@ -47,18 +47,21 @@
   in common:
 
   \begin{itemize}
-    \item They act uniformly, without reference to a specific
-       target language.
+
+    \item They act uniformly, without reference to a specific target
+       language.
+
     \item They are \emph{safe} in the sense that as long as you trust
        the code generator meta theory and implementation, you cannot
-       produce programs that yield results which are not derivable
-       in the logic.
+       produce programs that yield results which are not derivable in
+       the logic.
+
   \end{itemize}
 
-  \noindent In this section we will introduce means to \emph{adapt} the serialiser
-  to a specific target language, i.e.~to print program fragments
-  in a way which accommodates \qt{already existing} ingredients of
-  a target language environment, for three reasons:
+  \noindent In this section we will introduce means to \emph{adapt}
+  the serialiser to a specific target language, i.e.~to print program
+  fragments in a way which accommodates \qt{already existing}
+  ingredients of a target language environment, for three reasons:
 
   \begin{itemize}
     \item improving readability and aesthetics of generated code
@@ -71,19 +74,26 @@
   \emph{at any cost}:
 
   \begin{itemize}
-    \item The safe configuration methods act uniformly on every target language,
-      whereas for adaptation you have to treat each target language separately.
-    \item Application is extremely tedious since there is no abstraction
-      which would allow for a static check, making it easy to produce garbage.
+
+    \item The safe configuration methods act uniformly on every target
+      language, whereas for adaptation you have to treat each target
+      language separately.
+
+    \item Application is extremely tedious since there is no
+      abstraction which would allow for a static check, making it easy
+      to produce garbage.
+
     \item Subtle errors can be introduced unconsciously.
+
   \end{itemize}
 
-  \noindent However, even if you ought refrain from setting up adaptation
-  yourself, already the \isa{HOL} comes with some reasonable default
-  adaptations (say, using target language list syntax).  There also some
-  common adaptation cases which you can setup by importing particular
-  library theories.  In order to understand these, we provide some clues here;
-  these however are not supposed to replace a careful study of the sources.%
+  \noindent However, even if you ought refrain from setting up
+  adaptation yourself, already the \isa{HOL} comes with some
+  reasonable default adaptations (say, using target language list
+  syntax).  There also some common adaptation cases which you can
+  setup by importing particular library theories.  In order to
+  understand these, we provide some clues here; these however are not
+  supposed to replace a careful study of the sources.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -92,8 +102,8 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
-  supposed to be:
+Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
+  conceptually supposed to be:
 
   \begin{figure}[here]
     \includegraphics{adaptation}
@@ -102,36 +112,34 @@
   \end{figure}
 
   \noindent In the tame view, code generation acts as broker between
-  \isa{logic}, \isa{intermediate\ language} and
-  \isa{target\ language} by means of \isa{translation} and
-  \isa{serialisation};  for the latter, the serialiser has to observe
-  the structure of the \isa{language} itself plus some \isa{reserved}
-  keywords which have to be avoided for generated code.
-  However, if you consider \isa{adaptation} mechanisms, the code generated
-  by the serializer is just the tip of the iceberg:
+  \isa{logic}, \isa{intermediate\ language} and \isa{target\ language} by means of \isa{translation} and \isa{serialisation}; for the latter, the serialiser has to observe the
+  structure of the \isa{language} itself plus some \isa{reserved}
+  keywords which have to be avoided for generated code.  However, if
+  you consider \isa{adaptation} mechanisms, the code generated by
+  the serializer is just the tip of the iceberg:
 
   \begin{itemize}
+
     \item \isa{serialisation} can be \emph{parametrised} such that
       logical entities are mapped to target-specific ones
-      (e.g. target-specific list syntax,
-        see also \secref{sec:adaptation_mechanisms})
+      (e.g. target-specific list syntax, see also
+      \secref{sec:adaptation_mechanisms})
+
     \item Such parametrisations can involve references to a
-      target-specific standard \isa{library} (e.g. using
-      the \isa{Haskell} \verb|Maybe| type instead
-      of the \isa{HOL} \isa{option} type);
-      if such are used, the corresponding identifiers
-      (in our example, \verb|Maybe|, \verb|Nothing|
-      and \verb|Just|) also have to be considered \isa{reserved}.
+      target-specific standard \isa{library} (e.g. using the \isa{Haskell} \verb|Maybe| type instead of the \isa{HOL}
+      \isa{option} type); if such are used, the corresponding
+      identifiers (in our example, \verb|Maybe|, \verb|Nothing| and \verb|Just|) also have to be considered \isa{reserved}.
+
     \item Even more, the user can enrich the library of the
-      target-language by providing code snippets
-      (\qt{\isa{includes}}) which are prepended to
-      any generated code (see \secref{sec:include});  this typically
-      also involves further \isa{reserved} identifiers.
+      target-language by providing code snippets (\qt{\isa{includes}}) which are prepended to any generated code (see
+      \secref{sec:include}); this typically also involves further
+      \isa{reserved} identifiers.
+
   \end{itemize}
 
-  \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
-  have to act consistently;  it is at the discretion of the user
-  to take care for this.%
+  \noindent As figure \ref{fig:adaptation} illustrates, all these
+  adaptation mechanisms have to act consistently; it is at the
+  discretion of the user to take care for this.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -141,43 +149,44 @@
 %
 \begin{isamarkuptext}%
 The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
-  generator setup
-  which should be suitable for most applications.  Common extensions
-  and modifications are available by certain theories of the \isa{HOL}
-  library; beside being useful in applications, they may serve
-  as a tutorial for customising the code generator setup (see below
-  \secref{sec:adaptation_mechanisms}).
+  generator setup which should be suitable for most applications.
+  Common extensions and modifications are available by certain
+  theories of the \isa{HOL} library; beside being useful in
+  applications, they may serve as a tutorial for customising the code
+  generator setup (see below \secref{sec:adaptation_mechanisms}).
 
   \begin{description}
 
-    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
-       integer literals in target languages.
-    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by 
+    \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by
+       big integer literals in target languages.
+
+    \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
        character literals in target languages.
-    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
-       but also offers treatment of character codes; includes
-       \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
-    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
-       which in general will result in higher efficiency; pattern
-       matching with \isa{{\isadigit{0}}} / \isa{Suc}
-       is eliminated;  includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
+
+    \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, but
+       also offers treatment of character codes; includes \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
+
+    \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements
+       natural numbers by integers, which in general will result in
+       higher efficiency; pattern matching with \isa{{\isadigit{0}}} /
+       \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
        and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}.
+
     \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype
-       \isa{index} which is mapped to target-language built-in integers.
-       Useful for code setups which involve e.g. indexing of
-       target-language arrays.
-    \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype
-       \isa{String{\isachardot}literal} which is isomorphic to strings;
-       \isa{String{\isachardot}literal}s are mapped to target-language strings.
-       Useful for code setups which involve e.g. printing (error) messages.
+       \isa{index} which is mapped to target-language built-in
+       integers.  Useful for code setups which involve e.g.~indexing
+       of target-language arrays.
+
+    \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isachardot}literal} which is isomorphic to strings; \isa{String{\isachardot}literal}s are mapped to target-language strings.  Useful
+       for code setups which involve e.g.~printing (error) messages.
 
   \end{description}
 
   \begin{warn}
     When importing any of these theories, they should form the last
-    items in an import list.  Since these theories adapt the
-    code generator setup in a non-conservative fashion,
-    strange effects may occur otherwise.
+    items in an import list.  Since these theories adapt the code
+    generator setup in a non-conservative fashion, strange effects may
+    occur otherwise.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -187,8 +196,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Consider the following function and its corresponding
-  SML code:%
+Consider the following function and its corresponding SML code:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -266,15 +274,12 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent Though this is correct code, it is a little bit unsatisfactory:
-  boolean values and operators are materialised as distinguished
-  entities with have nothing to do with the SML-built-in notion
-  of \qt{bool}.  This results in less readable code;
-  additionally, eager evaluation may cause programs to
-  loop or break which would perfectly terminate when
-  the existing SML \verb|bool| would be used.  To map
-  the HOL \isa{bool} on SML \verb|bool|, we may use
-  \qn{custom serialisations}:%
+\noindent Though this is correct code, it is a little bit
+  unsatisfactory: boolean values and operators are materialised as
+  distinguished entities with have nothing to do with the SML-built-in
+  notion of \qt{bool}.  This results in less readable code;
+  additionally, eager evaluation may cause programs to loop or break
+  which would perfectly terminate when the existing SML \verb|bool| would be used.  To map the HOL \isa{bool} on SML \verb|bool|, we may use \qn{custom serialisations}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -298,14 +303,13 @@
 %
 \begin{isamarkuptext}%
 \noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
-  as arguments together with a list of custom serialisations.
-  Each custom serialisation starts with a target language
-  identifier followed by an expression, which during
-  code serialisation is inserted whenever the type constructor
-  would occur.  For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
-  the corresponding mechanism.  Each ``\verb|_|'' in
-  a serialisation expression is treated as a placeholder
-  for the type constructor's (the constant's) arguments.%
+  as arguments together with a list of custom serialisations.  Each
+  custom serialisation starts with a target language identifier
+  followed by an expression, which during code serialisation is
+  inserted whenever the type constructor would occur.  For constants,
+  \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements the corresponding mechanism.  Each
+  ``\verb|_|'' in a serialisation expression is treated as a
+  placeholder for the type constructor's (the constant's) arguments.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -346,12 +350,11 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent This still is not perfect: the parentheses
-  around the \qt{andalso} expression are superfluous.
-  Though the serialiser
-  by no means attempts to imitate the rich Isabelle syntax
-  framework, it provides some common idioms, notably
-  associative infixes with precedences which may be used here:%
+\noindent This still is not perfect: the parentheses around the
+  \qt{andalso} expression are superfluous.  Though the serialiser by
+  no means attempts to imitate the rich Isabelle syntax framework, it
+  provides some common idioms, notably associative infixes with
+  precedences which may be used here:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -407,12 +410,13 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent The attentive reader may ask how we assert that no generated
-  code will accidentally overwrite.  For this reason the serialiser has
-  an internal table of identifiers which have to be avoided to be used
-  for new declarations.  Initially, this table typically contains the
-  keywords of the target language.  It can be extended manually, thus avoiding
-  accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
+\noindent The attentive reader may ask how we assert that no
+  generated code will accidentally overwrite.  For this reason the
+  serialiser has an internal table of identifiers which have to be
+  avoided to be used for new declarations.  Initially, this table
+  typically contains the keywords of the target language.  It can be
+  extended manually, thus avoiding accidental overwrites, using the
+  \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -469,26 +473,23 @@
 %
 \begin{isamarkuptext}%
 \noindent The initial bang ``\verb|!|'' tells the serialiser
-  never to put
-  parentheses around the whole expression (they are already present),
-  while the parentheses around argument place holders
-  tell not to put parentheses around the arguments.
-  The slash ``\verb|/|'' (followed by arbitrary white space)
-  inserts a space which may be used as a break if necessary
-  during pretty printing.
+  never to put parentheses around the whole expression (they are
+  already present), while the parentheses around argument place
+  holders tell not to put parentheses around the arguments.  The slash
+  ``\verb|/|'' (followed by arbitrary white space) inserts a
+  space which may be used as a break if necessary during pretty
+  printing.
 
-  These examples give a glimpse what mechanisms
-  custom serialisations provide; however their usage
-  requires careful thinking in order not to introduce
-  inconsistencies -- or, in other words:
-  custom serialisations are completely axiomatic.
+  These examples give a glimpse what mechanisms custom serialisations
+  provide; however their usage requires careful thinking in order not
+  to introduce inconsistencies -- or, in other words: custom
+  serialisations are completely axiomatic.
 
-  A further noteworthy details is that any special
-  character in a custom serialisation may be quoted
-  using ``\verb|'|''; thus, in
-  ``\verb|fn '_ => _|'' the first
-  ``\verb|_|'' is a proper underscore while the
-  second ``\verb|_|'' is a placeholder.%
+  A further noteworthy details is that any special character in a
+  custom serialisation may be quoted using ``\verb|'|''; thus,
+  in ``\verb|fn '_ => _|'' the first ``\verb|_|'' is a
+  proper underscore while the second ``\verb|_|'' is a
+  placeholder.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -497,11 +498,10 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-For convenience, the default
-  \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
-  its counterpart in \isa{Haskell}, giving custom serialisations
-  for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
-  \isa{eq{\isacharunderscore}class{\isachardot}eq}%
+For convenience, the default \isa{HOL} setup for \isa{Haskell}
+  maps the \isa{eq} class to its counterpart in \isa{Haskell},
+  giving custom serialisations for the class \isa{eq} (by command
+  \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -525,10 +525,9 @@
 \endisadelimquotett
 %
 \begin{isamarkuptext}%
-\noindent A problem now occurs whenever a type which
-  is an instance of \isa{eq} in \isa{HOL} is mapped
-  on a \isa{Haskell}-built-in type which is also an instance
-  of \isa{Haskell} \isa{Eq}:%
+\noindent A problem now occurs whenever a type which is an instance
+  of \isa{eq} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell}
+  \isa{Eq}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -576,11 +575,9 @@
 \endisadelimquotett
 %
 \begin{isamarkuptext}%
-\noindent The code generator would produce
-  an additional instance, which of course is rejected by the \isa{Haskell}
-  compiler.
-  To suppress this additional instance, use
-  \isa{code{\isacharunderscore}instance}:%
+\noindent The code generator would produce an additional instance,
+  which of course is rejected by the \isa{Haskell} compiler.  To
+  suppress this additional instance, use \isa{code{\isacharunderscore}instance}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -605,8 +602,7 @@
 %
 \begin{isamarkuptext}%
 In rare cases it is necessary to \emph{enrich} the context of a
-  target language;  this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
-  command:%
+  target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} command:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -629,9 +625,10 @@
 \endisadelimquotett
 %
 \begin{isamarkuptext}%
-\noindent Such named \isa{include}s are then prepended to every generated code.
-  Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
-  with respect to a particular target language.%
+\noindent Such named \isa{include}s are then prepended to every
+  generated code.  Inspect such code in order to find out how
+  \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves with respect to a particular
+  target language.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Tue Aug 17 16:38:45 2010 +0200
@@ -141,7 +141,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
 \hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
 \hspace*{0pt}\\
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex	Tue Aug 17 16:38:45 2010 +0200
@@ -22,24 +22,188 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+\begin{isamarkuptext}%
+Code generation by shallow embedding (cf.~\secref{sec:principle})
+  allows to choose code equations and datatype constructors freely,
+  given that some very basic syntactic properties are met; this
+  flexibility opens up mechanisms for refinement which allow to extend
+  the scope and quality of generated code dramatically.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Program refinement%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-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 exactly 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
-  \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
-
-  In some cases, it is appropriate to alter or extend this table.  As
-  an example, we will develop an alternative representation of the
-  queue example given in \secref{sec:queue_example}.  The amortised
-  representation is convenient for generating code but exposes its
-  \qt{implementation} details, which may be cumbersome when proving
-  theorems about it.  Therefore, here is a simple, straightforward
-  representation of queues:%
+Program refinement works by choosing appropriate code equations
+  explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+  numbers:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{fun}\isamarkupfalse%
+\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The runtime of the corresponding code grows exponential due
+  to two recursive calls:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent A more efficient implementation would use dynamic
+  programming, e.g.~sharing of common intermediate results between
+  recursive calls.  This idea is expressed by an auxiliary operation
+  which computes a Fibonacci number and its successor simultaneously:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymtimes}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ n\ {\isacharequal}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharcomma}\ fib\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This operation can be implemented by recursion using
+  dynamic programming:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n\ in\ {\isacharparenleft}m\ {\isacharplus}\ q{\isacharcomma}\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent What remains is to implement \isa{fib} by \isa{fib{\isacharunderscore}step} as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The resulting code shows only linear growth of runtime:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
+\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
+\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsection{Datatype refinement%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Selecting specific code equations \emph{and} datatype constructors
+  leads to datatype refinement.  As an example, we will develop an
+  alternative representation of the queue example given in
+  \secref{sec:queue_example}.  The amortised representation is
+  convenient for generating code but exposes its \qt{implementation}
+  details, which may be cumbersome when proving theorems about it.
+  Therefore, here is a simple, straightforward representation of
+  queues:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -98,7 +262,16 @@
 \noindent Here we define a \qt{constructor} \isa{AQueue} which
   is defined in terms of \isa{Queue} and interprets its arguments
   according to what the \emph{content} of an amortised queue is supposed
-  to be.  Equipped with this, we are able to prove the following equations
+  to be.
+
+  The prerequisite for datatype constructors is only syntactical: a
+  constructor must be 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 exactly the set of \emph{all} type variables in
+  \isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype.  The
+  HOL datatype package by default registers any new datatype with its
+  constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+  using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+  Equipped with this, we are able to prove the following equations
   for our primitive queue operations which \qt{implement} the simple
   queues in an amortised fashion:%
 \end{isamarkuptext}%
@@ -178,7 +351,8 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
 \hspace*{0pt} ~val rev :~'a list -> 'a list\\
 \hspace*{0pt} ~val null :~'a list -> bool\\
 \hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
@@ -187,10 +361,12 @@
 \hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
 \hspace*{0pt}end = struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun null [] = true\\
 \hspace*{0pt} ~| null (x ::~xs) = false;\\
@@ -218,28 +394,23 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent From this example, it can be glimpsed that using own
-  constructor sets is a little delicate since it changes the set of
-  valid patterns for values of that type.  Without going into much
-  detail, here some practical hints:
-
-  \begin{itemize}
-
-    \item When changing the constructor set for datatypes, take care
-      to provide alternative equations for the \isa{case} combinator.
+The same techniques can also be applied to types which are not
+  specified as datatypes, e.g.~type \isa{int} is originally specified
+  as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+  generation constants allowing construction of binary numeral values
+  are used as constructors for \isa{int}.
 
-    \item Values in the target language need not to be normalised --
-      different values in the target language may represent the same
-      value in the logic.
-
-    \item Usually, a good methodology to deal with the subtleties of
-      pattern matching is to see the type as an abstract type: provide
-      a set of operations which operate on the concrete representation
-      of the type, and derive further operations by combinations of
-      these primitive ones, without relying on a particular
-      representation.
-
-  \end{itemize}%
+  This approach however fails if the representation of a type demands
+  invariants; this issue is discussed in the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatype refinement involving invariants%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/Codegen/Thy/examples/example.ML
--- a/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML	Tue Aug 17 16:38:45 2010 +0200
@@ -1,5 +1,6 @@
 structure Example : sig
-  val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+  val id : 'a -> 'a
+  val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val rev : 'a list -> 'a list
   datatype 'a queue = AQueue of 'a list * 'a list
   val empty : 'a queue
@@ -7,10 +8,12 @@
   val enqueue : 'a -> 'a queue -> 'a queue
 end = struct
 
-fun foldl f a [] = a
-  | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
 
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+  | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
 
 datatype 'a queue = AQueue of 'a list * 'a list;
 
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 16:38:45 2010 +0200
@@ -1018,7 +1018,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code' ( 'del' ) ?
+    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
     'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
   declaration.
 
   \item @{attribute (HOL) code} explicitly selects (or with option
-  ``@{text "del"}'' deselects) a code equation for code
-  generation.  Usually packages introducing code equations provide
-  a reasonable default setup for selection.
+  ``@{text "del"}'' deselects) a code equation for code generation.
+  Usually packages introducing code equations provide a reasonable
+  default setup for selection.  Variants @{text "code abstype"} and
+  @{text "code abstract"} declare abstract datatype certificates or
+  code equations on abstract datatype representations respectively.
 
   \item @{command (HOL) "code_abort"} declares constants which are not
   required to have a definition by means of code equations; if
diff -r 2eb6bad282b1 -r e0b8b1733689 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 16:38:45 2010 +0200
@@ -1034,7 +1034,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code' ( 'del' ) ?
+    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     ;
 
     'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
   declaration.
 
   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
-  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
-  generation.  Usually packages introducing code equations provide
-  a reasonable default setup for selection.
+  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+  Usually packages introducing code equations provide a reasonable
+  default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+  \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+  code equations on abstract datatype representations respectively.
 
   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
   required to have a definition by means of code equations; if
diff -r 2eb6bad282b1 -r e0b8b1733689 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 15:54:04 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 16:38:45 2010 +0200
@@ -8,9 +8,7 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
-    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -39,9 +37,9 @@
 (* prover configuration *)
 
 datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
-    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+  OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+  MalformedOutput | UnknownError
 
 type prover_config =
   {exec: string * string,
@@ -72,6 +70,10 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
+  | string_for_failure OldVampire =
+    "Isabelle requires a more recent version of Vampire. To install it, follow \
+    \the instructions from the Sledgehammer manual (\"isabelle doc\
+    \ sledgehammer\")."
   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   | string_for_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
@@ -143,6 +145,7 @@
    max_new_relevant_facts_per_iter = 60 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
+
 val e = ("e", e_config)
 
 
@@ -169,8 +172,10 @@
    max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
+
 val spass = ("spass", spass_config)
 
+
 (* Vampire *)
 
 val vampire_config : prover_config =
@@ -189,12 +194,15 @@
       (IncompleteUnprovable, "CANNOT PROVE"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
-      (OutOfResources, "Refutation not found")],
+      (OutOfResources, "Refutation not found"),
+      (OldVampire, "input_file")],
    max_new_relevant_facts_per_iter = 50 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
+
 val vampire = ("vampire", vampire_config)
 
+
 (* Remote prover invocation via SystemOnTPTP *)
 
 val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -236,13 +244,15 @@
    explicit_forall = true}
 
 val remote_name = prefix "remote_"
-
 fun remote_prover (name, config) atp_prefix =
   (remote_name name, remote_config atp_prefix config)
 
 val remote_e = remote_prover e "EP---"
 val remote_vampire = remote_prover vampire "Vampire---9"
 
+
+(* Setup *)
+
 fun is_installed ({exec, required_execs, ...} : prover_config) =
   forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
 fun maybe_remote (name, config) =
diff -r 2eb6bad282b1 -r e0b8b1733689 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 17 15:54:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 17 16:38:45 2010 +0200
@@ -206,27 +206,37 @@
 
 (* generic TPTP-based provers *)
 
-fun prover_fun name
+fun prover_fun atp_name
         {exec, required_execs, arguments, proof_delims, known_failures,
          max_new_relevant_facts_per_iter, prefers_theory_relevant,
          explicit_forall}
-        ({debug, overlord, full_types, explicit_apply, relevance_threshold,
-          relevance_convergence, theory_relevant, defs_relevant, isar_proof,
-          isar_shrink_factor, timeout, ...} : params)
+        ({debug, verbose, overlord, full_types, explicit_apply,
+          relevance_threshold, relevance_convergence, theory_relevant,
+          defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
         minimize_command
         ({subgoal, goal, relevance_override, axioms} : problem) =
   let
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt
     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
+
+    fun print s = (priority s; if debug then tracing s else ())
+    fun print_v f = () |> verbose ? print o f
+    fun print_d f = () |> debug ? print o f
+
     val the_axioms =
       case axioms of
         SOME axioms => axioms
-      | NONE => relevant_facts full_types relevance_threshold
-                    relevance_convergence defs_relevant
-                    max_new_relevant_facts_per_iter
-                    (the_default prefers_theory_relevant theory_relevant)
-                    relevance_override goal hyp_ts concl_t
+      | NONE =>
+        (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
+                           ".");
+         relevant_facts full_types relevance_threshold relevance_convergence
+                        defs_relevant max_new_relevant_facts_per_iter
+                        (the_default prefers_theory_relevant theory_relevant)
+                        relevance_override goal hyp_ts concl_t
+         |> tap ((fn n => print_v (fn () =>
+                      "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
+                      " for " ^ quote atp_name ^ ".")) o length))
 
     (* path to unique problem file *)
     val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -235,7 +245,7 @@
     fun prob_pathname nr =
       let
         val probfile =
-          Path.basic ((if overlord then "prob_" ^ name
+          Path.basic ((if overlord then "prob_" ^ atp_name
                        else the_problem_prefix ^ serial_string ())
                       ^ "_" ^ string_of_int nr)
       in
@@ -290,6 +300,8 @@
                   extract_proof_and_outcome complete res_code proof_delims
                                             known_failures output
               in (output, msecs, proof, outcome) end
+            val _ = print_d (fn () => "Preparing problem for " ^
+                                      quote atp_name ^ "...")
             val readable_names = debug andalso overlord
             val (problem, pool, conjecture_offset, axiom_names) =
               prepare_problem ctxt readable_names explicit_forall full_types
@@ -298,6 +310,7 @@
             val conjecture_shape =
               conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
               |> map single
+            val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
             val result =
               do_run false
               |> (fn (_, msecs0, _, SOME _) =>
@@ -343,15 +356,16 @@
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
-                        relevance_override minimize_command proof_state name =
+                        relevance_override minimize_command proof_state
+                        atp_name =
   let
     val thy = Proof.theory_of proof_state
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
-    val prover = get_prover_fun thy name
+    val prover = get_prover_fun thy atp_name
     val {context = ctxt, facts, goal} = Proof.goal proof_state;
     val desc =
-      "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+      "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
       Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
   in
     Async_Manager.launch das_Tool verbose birth_time death_time desc
@@ -361,7 +375,7 @@
                 {subgoal = i, goal = (ctxt, (facts, goal)),
                  relevance_override = relevance_override, axioms = NONE}
             in
-              prover params (minimize_command name) problem |> #message
+              prover params (minimize_command atp_name) problem |> #message
               handle ERROR message => "Error: " ^ message ^ "\n"
                    | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
                             "\n"
diff -r 2eb6bad282b1 -r e0b8b1733689 src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Tue Aug 17 15:54:04 2010 +0200
+++ b/src/Provers/quantifier1.ML	Tue Aug 17 16:38:45 2010 +0200
@@ -17,7 +17,7 @@
      And analogously for t=x, but the eqn is not turned around!
 
      NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
-        "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
+        "!x. x=t --> P(x)" is covered by the congruence rule for -->;
         "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
         As must be "? x. t=x & P(x)".
         
@@ -26,7 +26,7 @@
 Gries etc call this the "1 point rules"
 
 The above also works for !x1..xn. and ?x1..xn by moving the defined
-qunatifier inside first, but not for nested bounded quantifiers.
+quantifier inside first, but not for nested bounded quantifiers.
 
 For set comprehensions the basic permutations
       ... & x = t & ...  ->  x = t & (... & ...)
@@ -113,8 +113,13 @@
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
-    (K (rtac iff_reflection 1 THEN tac));
+  let val ctxt = ProofContext.init_global thy;
+      val eq_tu = Logic.mk_equals tu;
+      val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
+      val thm = Goal.prove ctxt' [] [] fixed_goal
+            (K (rtac iff_reflection 1 THEN tac));
+      val [gen_thm] = Variable.export ctxt' ctxt [thm];
+  in gen_thm end;
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)