--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 19 09:11:21 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 19 14:21:29 2011 +0200
@@ -2523,20 +2523,12 @@
A more efficient way of executing specifications is to translate
them into a functional programming language such as ML.
- Isabelle provides two generic frameworks to support code generation
+ Isabelle provides a generic framework 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
+ mechanisms in a way that is amenable to end-user applications. Code
+ can be generated for functional programs (including overloading
+ using type classes) targeting 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
@@ -2989,388 +2981,6 @@
\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{}{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}{}
-\rail@bar
-\rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{modespec}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
-\rail@nextbar{4}
-\rail@term{\isa{\isakeyword{file}}}[]
-\rail@nont{\isa{name}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{4}
-\rail@term{\isa{\isakeyword{imports}}}[]
-\rail@plus
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextplus{5}
-\rail@endplus
-\rail@endbar
-\rail@cr{7}
-\rail@term{\isa{\isakeyword{contains}}}[]
-\rail@bar
-\rail@plus
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{8}
-\rail@endplus
-\rail@nextbar{9}
-\rail@plus
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@nextplus{10}
-\rail@endplus
-\rail@endbar
-\rail@end
-\rail@begin{2}{\isa{modespec}}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@plus
-\rail@nextplus{1}
-\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@endplus
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
-\rail@plus
-\rail@nont{\isa{codespec}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{codespec}}
-\rail@nont{\isa{const}}[]
-\rail@nont{\isa{template}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{attachment}}[]
-\rail@endbar
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
-\rail@plus
-\rail@nont{\isa{tycodespec}}[]
-\rail@nextplus{1}
-\rail@endplus
-\rail@end
-\rail@begin{2}{\isa{tycodespec}}
-\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nont{\isa{template}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{attachment}}[]
-\rail@endbar
-\rail@end
-\rail@begin{1}{\isa{const}}
-\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
-\rail@end
-\rail@begin{1}{\isa{template}}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@end
-\rail@begin{2}{\isa{attachment}}
-\rail@term{\isa{attach}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{modespec}}[]
-\rail@endbar
-\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
-\rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
-\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
-\rail@end
-\rail@begin{2}{}
-\rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\isa{name}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}%
-\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.
-
- The following example demonstrates this for beta-reduction on lambda
- terms (see also \verb|~~/src/HOL/Proofs/Lambda/Lambda.thy|).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ dB\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ Var\ nat\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ App\ dB\ dB\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6465677265653E}{\isasymdegree}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{2}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ Abs\ dB\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ lift\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3C}{\isacharless}}\ k\ then\ Var\ i\ else\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ lift\ s\ k\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ lift\ t\ k{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}lift\ {\isaliteral{28}{\isacharparenleft}}Abs\ s{\isaliteral{29}{\isacharparenright}}\ k\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}lift\ s\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{primrec}\isamarkupfalse%
-\ subst\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{27}{\isacharprime}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}\ {\isadigit{3}}{\isadigit{0}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ k\ {\isaliteral{3C}{\isacharless}}\ i\ then\ Var\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ else\ if\ i\ {\isaliteral{3D}{\isacharequal}}\ k\ then\ s\ else\ Var\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Abs\ t{\isaliteral{29}{\isacharparenright}}{\isaliteral{5B}{\isacharbrackleft}}s{\isaliteral{2F}{\isacharslash}}k{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ Abs\ {\isaliteral{28}{\isacharparenleft}}t{\isaliteral{5B}{\isacharbrackleft}}lift\ s\ {\isadigit{0}}\ {\isaliteral{2F}{\isacharslash}}\ k{\isaliteral{2B}{\isacharplus}}{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{inductive}\isamarkupfalse%
-\ beta\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ dB\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isakeyword{where}\isanewline
-\ \ \ \ beta{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ s{\isaliteral{5B}{\isacharbrackleft}}t{\isaliteral{2F}{\isacharslash}}{\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ appL{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ s\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ u{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ appR{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ u\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ abs{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ t\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Abs\ s\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Abs\ t{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isanewline
-\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
-\ Test\isanewline
-\isakeyword{contains}\isanewline
-\ \ test{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ Var\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ test{\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}Abs\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ {\isaliteral{28}{\isacharparenleft}}Abs\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6465677265653E}{\isasymdegree}}\ Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isaliteral{5C3C626574613E}{\isasymbeta}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-In the above example, \verb|Test.test1| evaluates to a boolean,
- whereas \verb|Test.test2| is a lazy sequence whose elements can be
- inspected separately.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
-\isaantiq
-assert{}%
-\endisaantiq
-\ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{1}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ val\ results\ {\isaliteral{3D}{\isacharequal}}\ DSeq{\isaliteral{2E}{\isachardot}}list{\isaliteral{5F}{\isacharunderscore}}of\ Test{\isaliteral{2E}{\isachardot}}test{\isadigit{2}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
-\isaantiq
-assert{}%
-\endisaantiq
-\ {\isaliteral{28}{\isacharparenleft}}length\ results\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\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%