--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 20:34:34 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon May 02 21:33:21 2011 +0200
@@ -10,6 +10,7 @@
\isacommand{theory}\isamarkupfalse%
\ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
\isakeyword{imports}\ Main\isanewline
+\isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
@@ -1699,21 +1700,34 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle/Pure provides two generic frameworks to support code
- generation from executable specifications. Isabelle/HOL
- instantiates these mechanisms in a way that is amenable to end-user
- applications.
+For validation purposes, it is often useful to \emph{execute}
+ specifications. In principle, execution could be simulated by
+ Isabelle's inference kernel, i.e. by a combination of resolution and
+ simplification. Unfortunately, this approach is rather inefficient.
+ A more efficient way of executing specifications is to translate
+ them into a functional programming language such as ML.
- \medskip One framework generates code from functional programs
+ Isabelle provides two generic frameworks to support code generation
+ from executable specifications. Isabelle/HOL instantiates these
+ mechanisms in a way that is amenable to end-user applications.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The new code generator (F. Haftmann)%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This framework generates code from functional programs
(including overloading using type classes) to SML \cite{SML}, OCaml
\cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
- \cite{scala-overview-tech-report}.
- Conceptually, code generation is split up in three steps:
- \emph{selection} of code theorems, \emph{translation} into an
- abstract executable view and \emph{serialization} to a specific
- \emph{target language}. Inductive specifications can be executed
- using the predicate compiler which operates within HOL.
- See \cite{isabelle-codegen} for an introduction.
+ \cite{scala-overview-tech-report}. Conceptually, code generation is
+ split up in three steps: \emph{selection} of code theorems,
+ \emph{translation} into an abstract executable view and
+ \emph{serialization} to a specific \emph{target language}.
+ Inductive specifications can be executed using the predicate
+ compiler which operates within HOL. See \cite{isabelle-codegen} for
+ an introduction.
\begin{matharray}{rcl}
\indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -2155,27 +2169,32 @@
is generated into that specified file without modifying the code
generator setup.
- \end{description}
-
- The other framework generates code from both functional and
- relational programs to SML. See \cite{isabelle-HOL} for further
- information (this actually covers the new-style theory format as
- well).
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The old code generator (S. Berghofer)%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+This framework generates code from both functional and
+ relational programs to SML, as explained below.
\begin{matharray}{rcl}
- \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
- \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{code\_module}\hypertarget{command.code-module}{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{code\_library}\hypertarget{command.code-library}{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{consts\_code}\hypertarget{command.consts-code}{\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{}{command}{types\_code}\hypertarget{command.types-code}{\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
\indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
\end{matharray}
\begin{railoutput}
\rail@begin{11}{\isa{}}
\rail@bar
-\rail@term{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
+\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
\rail@nextbar{1}
-\rail@term{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
+\rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
@@ -2282,6 +2301,205 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsubsection{Invoking the code generator%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}
+ and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to
+ \emph{incremental} and \emph{modular} code generation, respectively.
+
+ \begin{description}
+
+ \item [Modular] For each theory, an ML structure is generated,
+ containing the code generated from the constants defined in this
+ theory.
+
+ \item [Incremental] All the generated code is emitted into the same
+ structure. This structure may import code from previously generated
+ structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.
+ Moreover, the generated structure may also be referred to in later
+ invocations of the code generator.
+
+ \end{description}
+
+ After the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}} and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}
+ keywords, the user may specify an optional list of ``modes'' in
+ parentheses. These can be used to instruct the code generator to
+ emit additional code for special purposes, e.g.\ functions for
+ converting elements of generated datatypes to Isabelle terms, or
+ test data generators. The list of modes is followed by a module
+ name. The module name is optional for modular code generation, but
+ must be specified for incremental code generation.
+
+ The code can either be written to a file, in which case a file name
+ has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded
+ directly into Isabelle's ML environment. In the latter case, the
+ \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results
+ interactively, for example.
+
+ The terms from which to generate code can be specified after the
+ \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just
+ as a list of terms. In the latter case, the code generator just
+ produces code for all constants and types occuring in the term, but
+ does not bind the compiled terms to ML identifiers.
+
+ Here is an example:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
+\ Test\isanewline
+\ \ \isakeyword{contains}\ test\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}foldl\ op\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
+\begin{isamarkuptext}%
+\noindent This binds the result of compiling the given term to
+ the ML identifier \verb|Test.test|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
+\isaantiq
+assert{}%
+\endisaantiq
+\ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsubsubsection{Configuring the code generator%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+When generating code for a complex term, the code generator
+ recursively calls itself for all subterms. When it arrives at a
+ constant, the default strategy of the code generator is to look up
+ its definition and try to generate code for it. Constants which
+ have no definitions that are immediately executable, may be
+ associated with a piece of ML code manually using the \indexref{}{command}{consts\_code}\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}} command. It takes a list whose elements consist of a
+ constant (given in usual term syntax -- an explicit type constraint
+ accounts for overloading), and a mixfix template describing the ML
+ code. The latter is very much the same as the mixfix templates used
+ when declaring new constants. The most notable difference is that
+ terms may be included in the ML template using antiquotation
+ brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.
+
+ A similar mechanism is available for types: \indexref{}{command}{types\_code}\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}} associates type constructors with specific ML code.
+
+ For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of
+ Isabelle/HOL should be compiled to ML.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{typedecl}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline
+\isacommand{consts}\isamarkupfalse%
+\ Pair\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ prod\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ Pair\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
+\begin{isamarkuptext}%
+Sometimes, the code associated with a constant or type may
+ need to refer to auxiliary functions, which have to be emitted when
+ the constant is used. Code for such auxiliary functions can be
+ declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}
+ function can be implemented as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
+\ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline
+\ \ \isakeyword{attach}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ fun\ wfrec\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}wfrec\ f{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
+\begin{isamarkuptext}%
+If the code containing a call to \isa{wfrec} resides in an
+ ML structure different from the one containing the function
+ definition attached to \isa{wfrec}, the name of the ML structure
+ (followed by a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}'') is inserted in place of ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}{\isaliteral{22}{\isachardoublequote}}}'' in the above template. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' means that
+ the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not
+ executable.
+
+ \medskip Another possibility of configuring the code generator is to
+ register theorems to be used for code generation. Theorems can be
+ registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional
+ name as an argument, which indicates the format of the
+ theorem. Currently supported formats are equations (this is the
+ default when no name is specified) and horn clauses (this is
+ indicated by the name \texttt{ind}). The left-hand sides of
+ equations may only contain constructors and distinct variables,
+ whereas horn clauses must have the same format as introduction rules
+ of inductive definitions.
+
+ The following example specifies three equations from which to
+ generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also
+ \verb|~~/src/HOL/Nat.thy|).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Suc\ m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}%
+\isadelimproof
+\ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ simp{\isaliteral{5F}{\isacharunderscore}}all%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsubsection{Specific HOL code generators%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basic code generator framework offered by Isabelle/Pure
+ has already been extended with additional code generators for
+ specific HOL constructs. These include datatypes, recursive
+ functions and inductive relations. The code generator for inductive
+ relations can handle expressions of the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{22}{\isachardoublequote}}} is an inductively defined relation. If at
+ least one of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is a dummy pattern ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'',
+ the above expression evaluates to a sequence of possible answers. If
+ all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates
+ to a boolean value.
+
+ %FIXME
+ %\begin{ttbox}
+ % theory Test = Lambda:
+ %
+ % code_module Test
+ % contains
+ % test1 = "Abs (Var 0) \(\circ\) Var 0 -> Var 0"
+ % test2 = "Abs (Abs (Var 0 \(\circ\) Var 0) \(\circ\) (Abs (Var 0) \(\circ\) Var 0)) -> _"
+ %\end{ttbox}
+ %In the above example, \texttt{Test.test1} evaluates to the boolean
+ %value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose
+ %elements can be inspected using \texttt{Seq.pull} or similar functions.
+ %\begin{ttbox}
+ %ML \{* Seq.pull Test.test2 *\} -- \{* This is the first answer *\}
+ %ML \{* Seq.pull (snd (the it)) *\} -- \{* This is the second answer *\}
+ %\end{ttbox}
+
+ \medskip The theory underlying the HOL code generator is described
+ more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
+ illustrate the usage of the code generator can be found e.g.\ in
+ \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Definition by specification \label{sec:hol-specification}%
}
\isamarkuptrue%