# HG changeset patch
# User chaieb
# Date 1233747155 0
# Node ID 67266b31cd46a15180a70007e215c18b703f1bb8
# Parent  7c7f759c438ead74e8f3cae85eb9afe2260d9ac7# Parent  f73a68c9d810e1aa0cafb99242ec54010902c55f
merged

diff -r f73a68c9d810 -r 67266b31cd46 NEWS
--- a/NEWS	Wed Feb 04 11:31:05 2009 +0000
+++ b/NEWS	Wed Feb 04 11:32:35 2009 +0000
@@ -193,6 +193,9 @@
 
 *** HOL ***
 
+* Auxiliary class "itself" has disappeared -- classes without any parameter
+are treated as expected by the 'class' command.
+
 * Theory "Reflection" now resides in HOL/Library.  Common reflection examples
 (Cooper, MIR, Ferrack) now in distinct session directory HOL/Reflection.
 
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/Further.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Further.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -96,7 +96,7 @@
   allows to use pattern matching on constructors stemming from compiled
   @{text datatypes}.
 
-  For a less simplistic example, theory @{theory ReflectedFerrack} is
+  For a less simplistic example, theory @{theory Ferrack} is
   a good reference.
 *}
 
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Introduction.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -65,19 +65,19 @@
   For example, here a simple \qt{implementation} of amortised queues:
 *}
 
-datatype %quote 'a queue = Queue "'a list" "'a list"
+datatype %quote 'a queue = AQueue "'a list" "'a list"
 
 definition %quote empty :: "'a queue" where
-  "empty = Queue [] []"
+  "empty = AQueue [] []"
 
 primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
-  "enqueue x (Queue xs ys) = Queue (x # xs) ys"
+  "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
 
 fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
-    "dequeue (Queue [] []) = (None, Queue [] [])"
-  | "dequeue (Queue xs (y # ys)) = (Some y, Queue xs ys)"
-  | "dequeue (Queue xs []) =
-      (case rev xs of y # ys \<Rightarrow> (Some y, Queue [] ys))"
+    "dequeue (AQueue [] []) = (None, AQueue [] [])"
+  | "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
+  | "dequeue (AQueue xs []) =
+      (case rev xs of y # ys \<Rightarrow> (Some y, AQueue [] ys))"
 
 text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
 
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/Program.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -26,11 +26,11 @@
 *}
 
 lemma %quote [code]:
-  "dequeue (Queue xs []) =
-     (if xs = [] then (None, Queue [] [])
-       else dequeue (Queue [] (rev xs)))"
-  "dequeue (Queue xs (y # ys)) =
-     (Some y, Queue xs ys)"
+  "dequeue (AQueue xs []) =
+     (if xs = [] then (None, AQueue [] [])
+       else dequeue (AQueue [] (rev xs)))"
+  "dequeue (AQueue xs (y # ys)) =
+     (Some y, AQueue xs ys)"
   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
 text {*
@@ -48,7 +48,7 @@
   setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
 
   Changing the default constructor set of datatypes is also
-  possible but rarely desired in practice.  See \secref{sec:datatypes} for an example.
+  possible.  See \secref{sec:datatypes} for an example.
 
   As told in \secref{sec:concept}, code generation is based
   on a structured collection of code theorems.
@@ -75,7 +75,7 @@
   from abstract algebra:
 *}
 
-class %quote semigroup = type +
+class %quote semigroup =
   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70)
   assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
 
@@ -221,106 +221,115 @@
 
 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.
+  \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.
 
-  In some cases, it may be convenient to alter or
-  extend this table;  as an example, we will develop an alternative
-  representation of natural numbers as binary digits, whose
-  size does increase logarithmically with its value, not linear
-  \footnote{Indeed, the @{theory Efficient_Nat} theory (see \ref{eff_nat})
-    does something similar}.  First, the digit representation:
+  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:intro}.  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 a simple, straightforward
+  representation of queues:
 *}
 
-definition %quote Dig0 :: "nat \<Rightarrow> nat" where
-  "Dig0 n = 2 * n"
+datatype %quote 'a queue = Queue "'a list"
+
+definition %quote empty :: "'a queue" where
+  "empty = Queue []"
 
-definition %quote  Dig1 :: "nat \<Rightarrow> nat" where
-  "Dig1 n = Suc (2 * n)"
+primrec %quote enqueue :: "'a \<Rightarrow> 'a queue \<Rightarrow> 'a queue" where
+  "enqueue x (Queue xs) = Queue (xs @ [x])"
+
+fun %quote dequeue :: "'a queue \<Rightarrow> 'a option \<times> 'a queue" where
+    "dequeue (Queue []) = (None, Queue [])"
+  | "dequeue (Queue (x # xs)) = (Some x, Queue xs)"
 
 text {*
-  \noindent We will use these two \qt{digits} to represent natural numbers
-  in binary digits, e.g.:
-*}
-
-lemma %quote 42: "42 = Dig0 (Dig1 (Dig0 (Dig1 (Dig0 1))))"
-  by (simp add: Dig0_def Dig1_def)
-
-text {*
-  \noindent Of course we also have to provide proper code equations for
-  the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
+  \noindent This we can use directly for proving;  for executing,
+  we provide an alternative characterisation:
 *}
 
-lemma %quote plus_Dig [code]:
-  "0 + n = n"
-  "m + 0 = m"
-  "1 + Dig0 n = Dig1 n"
-  "Dig0 m + 1 = Dig1 m"
-  "1 + Dig1 n = Dig0 (n + 1)"
-  "Dig1 m + 1 = Dig0 (m + 1)"
-  "Dig0 m + Dig0 n = Dig0 (m + n)"
-  "Dig0 m + Dig1 n = Dig1 (m + n)"
-  "Dig1 m + Dig0 n = Dig1 (m + n)"
-  "Dig1 m + Dig1 n = Dig0 (m + n + 1)"
-  by (simp_all add: Dig0_def Dig1_def)
+definition %quote AQueue :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a queue" where
+  "AQueue xs ys = Queue (ys @ rev xs)"
+
+code_datatype %quote AQueue
 
 text {*
-  \noindent We then instruct the code generator to view @{term "0\<Colon>nat"},
-  @{term "1\<Colon>nat"}, @{term Dig0} and @{term Dig1} as
-  datatype constructors:
+  \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
+  for our primitive queue operations which \qt{implement} the simple
+  queues in an amortised fashion:
 *}
 
-code_datatype %quote "0\<Colon>nat" "1\<Colon>nat" Dig0 Dig1
+lemma %quote empty_AQueue [code]:
+  "empty = AQueue [] []"
+  unfolding AQueue_def empty_def by simp
+
+lemma %quote enqueue_AQueue [code]:
+  "enqueue x (AQueue xs ys) = AQueue (x # xs) ys"
+  unfolding AQueue_def by simp
+
+lemma %quote dequeue_AQueue [code]:
+  "dequeue (AQueue xs []) =
+    (if xs = [] then (None, AQueue [] [])
+    else dequeue (AQueue [] (rev xs)))"
+  "dequeue (AQueue xs (y # ys)) = (Some y, AQueue xs ys)"
+  unfolding AQueue_def by simp_all
 
 text {*
-  \noindent For the former constructor @{term Suc}, we provide a code
-  equation and remove some parts of the default code generator setup
-  which are an obstacle here:
-*}
-
-lemma %quote Suc_Dig [code]:
-  "Suc n = n + 1"
-  by simp
-
-declare %quote One_nat_def [code inline del]
-declare %quote add_Suc_shift [code del] 
-
-text {*
-  \noindent This yields the following code:
+  \noindent For completeness, we provide a substitute for the
+  @{text case} combinator on queues:
 *}
 
-text %quote {*@{code_stmts "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" (SML)}*}
+definition %quote
+  aqueue_case_def: "aqueue_case = queue_case"
+
+lemma %quote aqueue_case [code, code inline]:
+  "queue_case = aqueue_case"
+  unfolding aqueue_case_def ..
+
+lemma %quote case_AQueue [code]:
+  "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
+  unfolding aqueue_case_def AQueue_def by simp
 
 text {*
-  \noindent From this example, it can be easily 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:
+  \noindent The resulting code looks as expected:
+*}
+
+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 an alternative for the @{text case} combinator (e.g.~by replacing
-      it using the preprocessor).
-    \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 (e.g. @{term "Dig1 0 = 1"}).
-    \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.
+
+    \item When changing the constructor set for datatypes, take care
+      to provide an alternative for the @{text case} combinator
+      (e.g.~by replacing it using the preprocessor).
+
+    \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}
 *}
 
-code_datatype %invisible "0::nat" Suc
-declare %invisible plus_Dig [code del]
-declare %invisible One_nat_def [code inline]
-declare %invisible add_Suc_shift [code] 
-lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
-
 
 subsection {* Equality and wellsortedness *}
 
@@ -457,14 +466,19 @@
   in the following example, again for amortised queues:
 *}
 
-fun %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
-  "strict_dequeue (Queue xs (y # ys)) = (y, Queue xs ys)"
-  | "strict_dequeue (Queue xs []) =
-      (case rev xs of y # ys \<Rightarrow> (y, Queue [] ys))"
+definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+  "strict_dequeue q = (case dequeue q
+    of (Some x, q') \<Rightarrow> (x, q'))"
+
+lemma %quote strict_dequeue_AQueue [code]:
+  "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
+  "strict_dequeue (AQueue xs []) =
+    (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
+  by (simp_all add: strict_dequeue_def dequeue_AQueue split: list.splits)
 
 text {*
   \noindent In the corresponding code, there is no equation
-  for the pattern @{term "Queue [] []"}:
+  for the pattern @{term "AQueue [] []"}:
 *}
 
 text %quote {*@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}*}
@@ -476,30 +490,28 @@
 
 axiomatization %quote empty_queue :: 'a
 
-function %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
-  "strict_dequeue' (Queue xs []) = (if xs = [] then empty_queue
-     else strict_dequeue' (Queue [] (rev xs)))"
-  | "strict_dequeue' (Queue xs (y # ys)) =
-       (y, Queue xs ys)"
-by pat_completeness auto
+definition %quote strict_dequeue' :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
+  "strict_dequeue' q = (case dequeue q of (Some x, q') \<Rightarrow> (x, q') | _ \<Rightarrow> empty_queue)"
 
-termination %quote strict_dequeue'
-by (relation "measure (\<lambda>q::'a queue. case q of Queue xs ys \<Rightarrow> length xs)") simp_all
+lemma %quote strict_dequeue'_AQueue [code]:
+  "strict_dequeue' (AQueue xs []) = (if xs = [] then empty_queue
+     else strict_dequeue' (AQueue [] (rev xs)))"
+  "strict_dequeue' (AQueue xs (y # ys)) =
+     (y, AQueue xs ys)"
+  by (simp_all add: strict_dequeue'_def dequeue_AQueue split: list.splits)
 
 text {*
-  \noindent For technical reasons the definition of
-  @{const strict_dequeue'} is more involved since it requires
-  a manual termination proof.  Apart from that observe that
-  on the right hand side of its first equation the constant
-  @{const empty_queue} occurs which is unspecified.
+  Observe that on the right hand side of the definition of @{const
+  "strict_dequeue'"} the constant @{const empty_queue} occurs
+  which is unspecified.
 
-  Normally, if constants without any code equations occur in
-  a program, the code generator complains (since in most cases
-  this is not what the user expects).  But such constants can also
-  be thought of as function definitions with no equations which
-  always fail, since there is never a successful pattern match
-  on the left hand side.  In order to categorise a constant into
-  that category explicitly, use @{command "code_abort"}:
+  Normally, if constants without any code equations occur in a
+  program, the code generator complains (since in most cases this is
+  not what the user expects).  But such constants can also be thought
+  of as function definitions with no equations which always fail,
+  since there is never a successful pattern match on the left hand
+  side.  In order to categorise a constant into that category
+  explicitly, use @{command "code_abort"}:
 *}
 
 code_abort %quote empty_queue
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/Setup.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Setup.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -5,7 +5,7 @@
 
 ML {* no_document use_thys
   ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
-   "~~/src/HOL/ex/ReflectedFerrack"] *}
+   "~~/src/HOL/Reflection/Ferrack"] *}
 
 ML_val {* Code_Target.code_width := 74 *}
 
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Further.tex	Wed Feb 04 11:32:35 2009 +0000
@@ -195,7 +195,7 @@
   allows to use pattern matching on constructors stemming from compiled
   \isa{datatypes}.
 
-  For a less simplistic example, theory \hyperlink{theory.ReflectedFerrack}{\mbox{\isa{ReflectedFerrack}}} is
+  For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is
   a good reference.%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Introduction.tex	Wed Feb 04 11:32:35 2009 +0000
@@ -94,22 +94,22 @@
 %
 \isatagquote
 \isacommand{datatype}\isamarkupfalse%
-\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\ {\isacharprime}a\ queue\ {\isacharequal}\ AQueue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
 \ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{primrec}\isamarkupfalse%
 \ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{fun}\isamarkupfalse%
 \ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -162,20 +162,20 @@
 \hspace*{0pt}fun list{\char95}case f1 f2 (a ::~lista) = f2 a lista\\
 \hspace*{0pt} ~| list{\char95}case f1 f2 [] = f1;\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype 'a queue = Queue of 'a list * 'a list;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = Queue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun dequeue (Queue ([],~[])) = (NONE,~Queue ([],~[]))\\
-\hspace*{0pt} ~| dequeue (Queue (xs,~y ::~ys)) = (SOME y,~Queue (xs,~ys))\\
-\hspace*{0pt} ~| dequeue (Queue (v ::~va,~[])) =\\
+\hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (v ::~va,~[])) =\\
 \hspace*{0pt} ~~~let\\
 \hspace*{0pt} ~~~~~val y ::~ys = rev (v ::~va);\\
 \hspace*{0pt} ~~~in\\
-\hspace*{0pt} ~~~~~(SOME y,~Queue ([],~ys))\\
+\hspace*{0pt} ~~~~~(SOME y,~AQueue ([],~ys))\\
 \hspace*{0pt} ~~~end;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun enqueue x (Queue (xs,~ys)) = Queue (x ::~xs,~ys);\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%
@@ -244,21 +244,21 @@
 \hspace*{0pt}list{\char95}case f1 f2 (a :~list) = f2 a list;\\
 \hspace*{0pt}list{\char95}case f1 f2 [] = f1;\\
 \hspace*{0pt}\\
-\hspace*{0pt}data Queue a = Queue [a] [a];\\
+\hspace*{0pt}data Queue a = AQueue [a] [a];\\
 \hspace*{0pt}\\
 \hspace*{0pt}empty ::~forall a.~Queue a;\\
-\hspace*{0pt}empty = Queue [] [];\\
+\hspace*{0pt}empty = AQueue [] [];\\
 \hspace*{0pt}\\
 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (Queue [] []) = (Nothing,~Queue [] []);\\
-\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\
-\hspace*{0pt}dequeue (Queue (v :~va) []) =\\
+\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~Queue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
 \hspace*{0pt}\\
 \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
-\hspace*{0pt}enqueue x (Queue xs ys) = Queue (x :~xs) ys;\\
+\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
 \hspace*{0pt}\\
 \hspace*{0pt}{\char125}%
 \end{isamarkuptext}%
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Wed Feb 04 11:32:35 2009 +0000
@@ -56,11 +56,11 @@
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
-\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
 \endisatagquote
@@ -88,10 +88,10 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
-\hspace*{0pt}dequeue (Queue xs (y :~ys)) = (Just y,~Queue xs ys);\\
-\hspace*{0pt}dequeue (Queue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then (Nothing,~Queue [] [])\\
-\hspace*{0pt} ~~~else dequeue (Queue [] (rev xs)));%
+\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
+\hspace*{0pt}dequeue (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then (Nothing,~AQueue [] [])\\
+\hspace*{0pt} ~~~else dequeue (AQueue [] (rev xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -108,7 +108,7 @@
   setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
 
   Changing the default constructor set of datatypes is also
-  possible but rarely desired in practice.  See \secref{sec:datatypes} for an example.
+  possible.  See \secref{sec:datatypes} for an example.
 
   As told in \secref{sec:concept}, code generation is based
   on a structured collection of code theorems.
@@ -158,7 +158,7 @@
 %
 \isatagquote
 \isacommand{class}\isamarkupfalse%
-\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
+\ semigroup\ {\isacharequal}\isanewline
 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
@@ -506,19 +506,51 @@
 %
 \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.
+  \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 may be convenient to alter or
-  extend this table;  as an example, we will develop an alternative
-  representation of natural numbers as binary digits, whose
-  size does increase logarithmically with its value, not linear
-  \footnote{Indeed, the \hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}} theory (see \ref{eff_nat})
-    does something similar}.  First, the digit representation:%
+  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:intro}.  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 a simple, straightforward
+  representation of queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{datatype}\isamarkupfalse%
+\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{definition}\isamarkupfalse%
+\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{primrec}\isamarkupfalse%
+\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we can use directly for proving;  for executing,
+  we provide an alternative characterisation:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -528,12 +560,11 @@
 %
 \isatagquote
 \isacommand{definition}\isamarkupfalse%
-\ Dig{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ n{\isachardoublequoteclose}\isanewline
+\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\isacommand{definition}\isamarkupfalse%
-\ \ Dig{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ n{\isacharparenright}{\isachardoublequoteclose}%
+\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
+\ AQueue%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -542,30 +573,12 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent We will use these two \qt{digits} to represent natural numbers
-  in binary digits, e.g.:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isadigit{4}}{\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isacharparenleft}Dig{\isadigit{1}}\ {\isacharparenleft}Dig{\isadigit{0}}\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent Of course we also have to provide proper code equations for
-  the operations, e.g. \isa{op\ {\isacharplus}}:%
+\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}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
+  for our primitive queue operations which \qt{implement} the simple
+  queues in an amortised fashion:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -575,19 +588,28 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{1}}\ m{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ {\isadigit{1}}\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{0}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}Dig{\isadigit{1}}\ m\ {\isacharplus}\ Dig{\isadigit{1}}\ n\ {\isacharequal}\ Dig{\isadigit{0}}\ {\isacharparenleft}m\ {\isacharplus}\ n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Dig{\isadigit{0}}{\isacharunderscore}def\ Dig{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
+\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp{\isacharunderscore}all%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -596,9 +618,8 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent We then instruct the code generator to view \isa{{\isadigit{0}}},
-  \isa{{\isadigit{1}}}, \isa{Dig{\isadigit{0}}} and \isa{Dig{\isadigit{1}}} as
-  datatype constructors:%
+\noindent For completeness, we provide a substitute for the
+  \isa{case} combinator on queues:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -607,8 +628,23 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{0}}{\isasymColon}nat{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isadigit{1}}{\isasymColon}nat{\isachardoublequoteclose}\ Dig{\isadigit{0}}\ Dig{\isadigit{1}}%
+\isacommand{definition}\isamarkupfalse%
+\isanewline
+\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{unfolding}\isamarkupfalse%
+\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ simp%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -617,36 +653,7 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent For the former constructor \isa{Suc}, we provide a code
-  equation and remove some parts of the default code generator setup
-  which are an obstacle here:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
-\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent This yields the following code:%
+\noindent The resulting code looks as expected:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -662,18 +669,24 @@
 \hspace*{0pt}structure Example = \\
 \hspace*{0pt}struct\\
 \hspace*{0pt}\\
-\hspace*{0pt}datatype nat = Dig1 of nat | Dig0 of nat | One{\char95}nat | Zero{\char95}nat;\\
+\hspace*{0pt}fun foldl f a [] = a\\
+\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun null [] = true\\
+\hspace*{0pt} ~| null (x ::~xs) = false;\\
 \hspace*{0pt}\\
-\hspace*{0pt}fun plus{\char95}nat (Dig1 m) (Dig1 n) = Dig0 (plus{\char95}nat (plus{\char95}nat m n) One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) (Dig0 n) = Dig1 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig1 n) = Dig1 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) (Dig0 n) = Dig0 (plus{\char95}nat m n)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig1 m) One{\char95}nat = Dig0 (plus{\char95}nat m One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig1 n) = Dig0 (plus{\char95}nat n One{\char95}nat)\\
-\hspace*{0pt} ~| plus{\char95}nat (Dig0 m) One{\char95}nat = Dig1 m\\
-\hspace*{0pt} ~| plus{\char95}nat One{\char95}nat (Dig0 n) = Dig1 n\\
-\hspace*{0pt} ~| plus{\char95}nat m Zero{\char95}nat = m\\
-\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
+\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
+\hspace*{0pt}\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
+\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
+\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
+\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
 \hspace*{0pt}\\
 \hspace*{0pt}end;~(*struct Example*)%
 \end{isamarkuptext}%
@@ -687,49 +700,32 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent From this example, it can be easily 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:
+\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 an alternative for the \isa{case} combinator (e.g.~by replacing
-      it using the preprocessor).
-    \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 (e.g. \isa{Dig{\isadigit{1}}\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}}).
-    \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.
+
+    \item When changing the constructor set for datatypes, take care
+      to provide an alternative for the \isa{case} combinator
+      (e.g.~by replacing it using the preprocessor).
+
+    \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}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
-\isataginvisible
-\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
-\isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-\ simp%
-\endisataginvisible
-{\isafoldinvisible}%
-%
-\isadeliminvisible
-%
-\endisadeliminvisible
-%
 \isamarkupsubsection{Equality and wellsortedness%
 }
 \isamarkuptrue%
@@ -1081,11 +1077,18 @@
 \endisadelimquote
 %
 \isatagquote
-\isacommand{fun}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
 \ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
+\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -1095,7 +1098,7 @@
 %
 \begin{isamarkuptext}%
 \noindent In the corresponding code, there is no equation
-  for the pattern \isa{Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+  for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1109,11 +1112,11 @@
 \isatypewriter%
 \noindent%
 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue (Queue xs (y :~ys)) = (y,~Queue xs ys);\\
-\hspace*{0pt}strict{\char95}dequeue (Queue xs []) =\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
 \hspace*{0pt} ~let {\char123}\\
 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~Queue [] ys);%
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1138,19 +1141,18 @@
 \isacommand{axiomatization}\isamarkupfalse%
 \ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
 \isanewline
-\isacommand{function}\isamarkupfalse%
+\isacommand{definition}\isamarkupfalse%
 \ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
-\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ {\isacharbar}\ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}Queue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ Queue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\isacommand{by}\isamarkupfalse%
-\ pat{\isacharunderscore}completeness\ auto\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
-\isacommand{termination}\isamarkupfalse%
-\ strict{\isacharunderscore}dequeue{\isacharprime}\isanewline
-\isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}q{\isacharcolon}{\isacharcolon}{\isacharprime}a\ queue{\isachardot}\ case\ q\ of\ Queue\ xs\ ys\ {\isasymRightarrow}\ length\ xs{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ simp{\isacharunderscore}all%
+\isacommand{lemma}\isamarkupfalse%
+\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
+\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
 \endisatagquote
 {\isafoldquote}%
 %
@@ -1159,19 +1161,16 @@
 \endisadelimquote
 %
 \begin{isamarkuptext}%
-\noindent For technical reasons the definition of
-  \isa{strict{\isacharunderscore}dequeue{\isacharprime}} is more involved since it requires
-  a manual termination proof.  Apart from that observe that
-  on the right hand side of its first equation the constant
-  \isa{empty{\isacharunderscore}queue} occurs which is unspecified.
+Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}} the constant \isa{empty{\isacharunderscore}queue} occurs
+  which is unspecified.
 
-  Normally, if constants without any code equations occur in
-  a program, the code generator complains (since in most cases
-  this is not what the user expects).  But such constants can also
-  be thought of as function definitions with no equations which
-  always fail, since there is never a successful pattern match
-  on the left hand side.  In order to categorise a constant into
-  that category explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+  Normally, if constants without any code equations occur in a
+  program, the code generator complains (since in most cases this is
+  not what the user expects).  But such constants can also be thought
+  of as function definitions with no equations which always fail,
+  since there is never a successful pattern match on the left hand
+  side.  In order to categorise a constant into that category
+  explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1208,9 +1207,10 @@
 \hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
 \hspace*{0pt}\\
 \hspace*{0pt}strict{\char95}dequeue' ::~forall a.~Queue a -> (a,~Queue a);\\
-\hspace*{0pt}strict{\char95}dequeue' (Queue xs []) =\\
-\hspace*{0pt} ~(if nulla xs then empty{\char95}queue else strict{\char95}dequeue' (Queue [] (rev xs)));\\
-\hspace*{0pt}strict{\char95}dequeue' (Queue xs (y :~ys)) = (y,~Queue xs ys);%
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
+\hspace*{0pt}strict{\char95}dequeue' (AQueue xs []) =\\
+\hspace*{0pt} ~(if nulla xs then empty{\char95}queue\\
+\hspace*{0pt} ~~~else strict{\char95}dequeue' (AQueue [] (rev xs)));%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs	Wed Feb 04 11:32:35 2009 +0000
@@ -14,20 +14,20 @@
 list_case f1 f2 (a : list) = f2 a list;
 list_case f1 f2 [] = f1;
 
-data Queue a = Queue [a] [a];
+data Queue a = AQueue [a] [a];
 
 empty :: forall a. Queue a;
-empty = Queue [] [];
+empty = AQueue [] [];
 
 dequeue :: forall a. Queue a -> (Maybe a, Queue a);
-dequeue (Queue [] []) = (Nothing, Queue [] []);
-dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);
-dequeue (Queue (v : va) []) =
+dequeue (AQueue [] []) = (Nothing, AQueue [] []);
+dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
+dequeue (AQueue (v : va) []) =
   let {
     (y : ys) = rev (v : va);
-  } in (Just y, Queue [] ys);
+  } in (Just y, AQueue [] ys);
 
 enqueue :: forall a. a -> Queue a -> Queue a;
-enqueue x (Queue xs ys) = Queue (x : xs) ys;
+enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
 
 }
diff -r f73a68c9d810 -r 67266b31cd46 doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML	Wed Feb 04 11:31:05 2009 +0000
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML	Wed Feb 04 11:32:35 2009 +0000
@@ -9,19 +9,19 @@
 fun list_case f1 f2 (a :: lista) = f2 a lista
   | list_case f1 f2 [] = f1;
 
-datatype 'a queue = Queue of 'a list * 'a list;
+datatype 'a queue = AQueue of 'a list * 'a list;
 
-val empty : 'a queue = Queue ([], [])
+val empty : 'a queue = AQueue ([], [])
 
-fun dequeue (Queue ([], [])) = (NONE, Queue ([], []))
-  | dequeue (Queue (xs, y :: ys)) = (SOME y, Queue (xs, ys))
-  | dequeue (Queue (v :: va, [])) =
+fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
+  | dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
+  | dequeue (AQueue (v :: va, [])) =
     let
       val y :: ys = rev (v :: va);
     in
-      (SOME y, Queue ([], ys))
+      (SOME y, AQueue ([], ys))
     end;
 
-fun enqueue x (Queue (xs, ys)) = Queue (x :: xs, ys);
+fun enqueue x (AQueue (xs, ys)) = AQueue (x :: xs, ys);
 
 end; (*struct Example*)
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Finite_Set.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -383,7 +383,7 @@
 subsection {* Class @{text finite}  *}
 
 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
-class finite = itself +
+class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
 setup {* Sign.parent_path *}
 hide const finite
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Array.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -198,12 +198,12 @@
 
 subsubsection {* Haskell *}
 
-code_type array (Haskell "STArray/ RealWorld/ _")
+code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
 code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "newArray/ (0,/ _)")
-code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
-code_const Array.length' (Haskell "lengthArray")
-code_const Array.nth' (Haskell "readArray")
-code_const Array.upd' (Haskell "writeArray")
+code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
+code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
+code_const Array.length' (Haskell "Heap.lengthArray")
+code_const Array.nth' (Haskell "Heap.readArray")
+code_const Array.upd' (Haskell "Heap.writeArray")
 
 end
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Heap_Monad.thy
-    ID:         $Id$
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
@@ -375,7 +374,7 @@
 
 text {* Adaption layer *}
 
-code_include Haskell "STMonad"
+code_include Haskell "Heap"
 {*import qualified Control.Monad;
 import qualified Control.Monad.ST;
 import qualified Data.STRef;
@@ -386,9 +385,6 @@
 type STRef s a = Data.STRef.STRef s a;
 type STArray s a = Data.Array.ST.STArray s Int a;
 
-runST :: (forall s. ST s a) -> a;
-runST s = Control.Monad.ST.runST s;
-
 newSTRef = Data.STRef.newSTRef;
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
@@ -408,14 +404,11 @@
 writeArray :: STArray s a -> Int -> a -> ST s ();
 writeArray = Data.Array.ST.writeArray;*}
 
-code_reserved Haskell RealWorld ST STRef Array
-  runST
-  newSTRef reasSTRef writeSTRef
-  newArray newListArray lengthArray readArray writeArray
+code_reserved Haskell Heap
 
 text {* Monad *}
 
-code_type Heap (Haskell "ST/ RealWorld/ _")
+code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
 code_const Heap (Haskell "error/ \"bare Heap\"")
 code_monad "op \<guillemotright>=" Haskell
 code_const return (Haskell "return")
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -82,10 +82,10 @@
 
 subsubsection {* Haskell *}
 
-code_type ref (Haskell "STRef/ RealWorld/ _")
+code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
 code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const Ref.new (Haskell "newSTRef")
-code_const Ref.lookup (Haskell "readSTRef")
-code_const Ref.update (Haskell "writeSTRef")
+code_const Ref.new (Haskell "Heap.newSTRef")
+code_const Ref.lookup (Haskell "Heap.readSTRef")
+code_const Ref.update (Haskell "Heap.writeSTRef")
 
 end
\ No newline at end of file
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Countable.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -10,7 +10,7 @@
 
 subsection {* The class of countable types *}
 
-class countable = itself +
+class countable =
   assumes ex_inj: "\<exists>to_nat \<Colon> 'a \<Rightarrow> nat. inj to_nat"
 
 lemma countable_classI:
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Efficient_Nat.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -308,7 +308,7 @@
 code_reserved Haskell Nat
 
 code_type nat
-  (Haskell "Nat")
+  (Haskell "Nat.Nat")
 
 code_instance nat :: eq
   (Haskell -)
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/Enum.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -11,14 +11,14 @@
 
 subsection {* Class @{text enum} *}
 
-class enum = itself +
+class enum =
   fixes enum :: "'a list"
   assumes UNIV_enum [code]: "UNIV = set enum"
     and enum_distinct: "distinct enum"
 begin
 
-lemma finite_enum: "finite (UNIV \<Colon> 'a set)"
-  unfolding UNIV_enum ..
+subclass finite proof
+qed (simp add: UNIV_enum)
 
 lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
 
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Library/State_Monad.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/State_Monad.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/Typedef.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -119,52 +119,4 @@
 use "Tools/typecopy_package.ML" setup TypecopyPackage.setup
 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
 
-
-text {* This class is just a workaround for classes without parameters;
-  it shall disappear as soon as possible. *}
-
-class itself = 
-  fixes itself :: "'a itself"
-
-setup {*
-let fun add_itself tyco thy =
-  let
-    val vs = Name.names Name.context "'a"
-      (replicate (Sign.arity_number thy tyco) @{sort type});
-    val ty = Type (tyco, map TFree vs);
-    val lhs = Const (@{const_name itself}, Term.itselfT ty);
-    val rhs = Logic.mk_type ty;
-    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
-  in
-    thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
-    |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
-    |> snd
-    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-    |> LocalTheory.exit_global
-  end
-in TypedefPackage.interpretation add_itself end
-*}
-
-instantiation bool :: itself
-begin
-
-definition "itself = TYPE(bool)"
-
-instance ..
-
 end
-
-instantiation "fun" :: ("type", "type") itself
-begin
-
-definition "itself = TYPE('a \<Rightarrow> 'b)"
-
-instance ..
-
-end
-
-hide (open) const itself
-
-end
diff -r f73a68c9d810 -r 67266b31cd46 src/HOL/ex/ImperativeQuicksort.thy
--- a/src/HOL/ex/ImperativeQuicksort.thy	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/HOL/ex/ImperativeQuicksort.thy	Wed Feb 04 11:32:35 2009 +0000
@@ -629,9 +629,9 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort in SML_imp module_name Arr
-export_code qsort in OCaml module_name Arr file -
-export_code qsort in OCaml_imp module_name Arr file -
-export_code qsort in Haskell module_name Arr file -
+export_code qsort in SML_imp module_name QSort
+export_code qsort in OCaml module_name QSort file -
+export_code qsort in OCaml_imp module_name QSort file -
+export_code qsort in Haskell module_name QSort file -
 
 end
\ No newline at end of file
diff -r f73a68c9d810 -r 67266b31cd46 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Pure/Isar/class.ML	Wed Feb 04 11:32:35 2009 +0000
@@ -41,9 +41,16 @@
       (Const o apsnd (map_atyps (K aT))) param_map;
     val const_morph = Element.inst_morphism thy
       (Symtab.empty, Symtab.make param_map_inst);
-    val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
+    val typ_morph = Element.inst_morphism thy
+      (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
+    val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
            Expression.Named param_map_const))], []);
+    val (props, inst_morph) = if null param_map
+      then (raw_props |> map (Morphism.term typ_morph),
+        raw_inst_morph $> typ_morph)
+      else (raw_props, raw_inst_morph); (*FIXME proper handling in
+        locale.ML / expression.ML would be desirable*)
 
     (* witness for canonical interpretation *)
     val prop = try the_single props;
@@ -162,7 +169,7 @@
       |> Sign.minimize_sort thy;
     val _ = case filter_out (is_class thy) sups
      of [] => ()
-      | no_classes => error ("No proper classes: " ^ commas (map quote no_classes));
+      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
           val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
     val supparam_names = map fst supparams;
     val _ = if has_duplicates (op =) supparam_names
diff -r f73a68c9d810 -r 67266b31cd46 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Pure/Isar/expression.ML	Wed Feb 04 11:32:35 2009 +0000
@@ -100,7 +100,7 @@
       (* FIXME: cannot compare bindings for equality. *)
 
     fun params_loc loc =
-          (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =
           let
             val (ps, loc') = params_loc loc;
@@ -150,14 +150,14 @@
 
 local
 
-fun prep_inst parse_term ctxt parms (Positional insts) =
+fun prep_inst prep_term ctxt parms (Positional insts) =
       (insts ~~ parms) |> map (fn
-        (NONE, p) => Free (p, the (Variable.default_type ctxt p)) |
-        (SOME t, _) => parse_term ctxt t)
-  | prep_inst parse_term ctxt parms (Named insts) =
+        (NONE, p) => Free (p, dummyT) |
+        (SOME t, _) => prep_term ctxt t)
+  | prep_inst prep_term ctxt parms (Named insts) =
       parms |> map (fn p => case AList.lookup (op =) insts p of
-        SOME t => parse_term ctxt t |
-        NONE => Free (p, the (Variable.default_type ctxt p)));
+        SOME t => prep_term ctxt t |
+        NONE => Free (p, dummyT));
 
 in
 
@@ -350,19 +350,19 @@
 
 local
 
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem parse_inst prep_vars_inst prep_expr
+fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
     strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
   let
     val thy = ProofContext.theory_of ctxt1;
 
     val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
 
-    fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
+    fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |>
           map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
             (*FIXME return value of Locale.params_of has strange type*)
-        val inst' = parse_inst ctxt parm_names inst;
+        val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
         val inst'' = map2 TypeInfer.constrain parm_types' inst';
@@ -387,7 +387,7 @@
 
     val fors = prep_vars_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
-    val (_, insts', ctxt3) = fold prep_inst raw_insts (0, [], ctxt2);
+    val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
     val ctxt4 = init_body ctxt3;
     val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
     val (insts, elems', concl, ctxt6) =
diff -r f73a68c9d810 -r 67266b31cd46 src/Tools/code/code_haskell.ML
--- a/src/Tools/code/code_haskell.ML	Wed Feb 04 11:31:05 2009 +0000
+++ b/src/Tools/code/code_haskell.ML	Wed Feb 04 11:32:35 2009 +0000
@@ -385,7 +385,7 @@
         val imports = deps'
           |> map NameSpace.qualifier
           |> distinct (op =);
-        fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
+        fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
         val pr_import_module = str o (if qualified
           then prefix "import qualified "
           else prefix "import ") o suffix ";";