
diff -r 640b7f8f9cad -r 6ec603695aaf doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Oct 02 17:18:22 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Thu Oct 02 17:18:36 2008 +0200
@@ -784,7 +784,7 @@
 \newline%
 \verb|fun eqop A_ a b = eq A_ a b;|\newline%
 \newline%
-\verb|fun member A_ x (y :: ys) = (if eqop A_ y x then true else member A_ x ys)|\newline%
+\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
 \verb|  |\verb,|,\verb| member A_ x [] = false;|\newline%
 \newline%
 \verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
@@ -987,12 +987,12 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Then code generation for SML would fail with a message
+\noindent Then code generation for SML would fail with a message
   that the generated code contains illegal mutual dependencies:
-  the theorem \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}} already requires the
+  the theorem \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}} already requires the
   instance \isa{monotype\ {\isasymColon}\ eq}, which itself requires
-  \isa{Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}\ {\isacharequal}\ Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}\ {\isasymequiv}\ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ typargs{\isadigit{1}}\ {\isacharequal}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually
-  recursive \isa{inst} and \isa{fun} definitions,
+  \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymequiv}\ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}};  Haskell has no problem with mutually
+  recursive \isa{instance} and \isa{function} definitions,
   but the SML serializer does not support this.
 
   In such cases, you have to provide your own equality equations
@@ -1009,7 +1009,7 @@
 \isacommand{lemma}\isamarkupfalse%
 \ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
-\ \ \ \ \ tyco{\isadigit{1}}\ {\isacharequal}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}simp\ add{\isacharcolon}\ eq\ list{\isacharunderscore}all{\isadigit{2}}{\isacharunderscore}eq\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}%
 \endisatagquoteme
@@ -1036,13 +1036,8 @@
 \verb|structure Example = |\newline%
 \verb|struct|\newline%
 \newline%
-\verb|type 'a eq = {eq : 'a -> 'a -> bool};|\newline%
-\verb|fun eq (A_:'a eq) = #eq A_;|\newline%
-\newline%
 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
 \newline%
-\verb|fun eqop A_ a b = eq A_ a b;|\newline%
-\newline%
 \verb|fun null (x :: xs) = false|\newline%
 \verb|  |\verb,|,\verb| null [] = true;|\newline%
 \newline%
@@ -1051,8 +1046,6 @@
 \verb|  |\verb,|,\verb| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'|\newline%
 \verb|  |\verb,|,\verb| eq_nat Zero_nat Zero_nat = true;|\newline%
 \newline%
-\verb|val eq_nata = {eq = eq_nat} : nat eq;|\newline%
-\newline%
 \verb|datatype monotype = Mono of nat * monotype list;|\newline%
 \newline%
 \verb|fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys|\newline%
@@ -1060,8 +1053,7 @@
 \verb|  |\verb,|,\verb| list_all2 p [] ys = null ys;|\newline%
 \newline%
 \verb|fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =|\newline%
-\verb|  eqop eq_nata tyco1 tyco2 andalso|\newline%
-\verb|    list_all2 eq_monotype typargs1 typargs2;|\newline%
+\verb|  eq_nat tyco1 tyco2 andalso list_all2 eq_monotype typargs1 typargs2;|\newline%
 \newline%
 \verb|end; (*struct Example*)|%
 \end{isamarkuptext}%
@@ -1074,12 +1066,166 @@
 %
 \endisadelimquoteme
 %
-\isamarkupsubsection{Partiality%
+\isamarkupsubsection{Explicit partiality%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, examples: maps%
+Partiality usually enters the game by partial patterns, as
+  in the following example, again for amortised queues:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{fun}\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}%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent In the corresponding code, there is no equation
+  for the pattern \isa{Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|strict_dequeue :: forall a. Queue a -> (a, Queue a);|\newline%
+\verb|strict_dequeue (Queue xs (y : ys)) = (y, Queue xs ys);|\newline%
+\verb|strict_dequeue (Queue xs []) =|\newline%
+\verb|  let {|\newline%
+\verb|    (y : ys) = rev xs;|\newline%
+\verb|  } in (y, Queue [] ys);|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent In some cases it is desirable to have this
+  pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{axiomatization}\isamarkupfalse%
+\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
+\isanewline
+\isacommand{function}\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
+\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%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\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.
+
+  Normally, if constants without any defining 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 categorize a constant into
+  that category explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
+\ empty{\isacharunderscore}queue%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent Then the code generator will just insert an error or
+  exception at the appropriate position:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|empty_queue :: forall a. a;|\newline%
+\verb|empty_queue = error "empty_queue";|\newline%
+\newline%
+\verb|strict_dequeue' :: forall a. Queue a -> (a, Queue a);|\newline%
+\verb|strict_dequeue' (Queue xs []) =|\newline%
+\verb|  (if nulla xs then empty_queue else strict_dequeue' (Queue [] (rev xs)));|\newline%
+\verb|strict_dequeue' (Queue xs (y : ys)) = (y, Queue xs ys);|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\begin{isamarkuptext}%
+\noindent This feature however is rarely needed in practice.
+  Note also that the \isa{HOL} default setup already declares
+  \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
+  likely to be used in such situations.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -1097,7 +1243,7 @@
 %
 \endisadelimtheory
 \isanewline
-\end{isabellebody}%
+\ \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"




