# HG changeset patch # User wenzelm # Date 1319026889 -7200 # Node ID 008710fff1cc572549e954c500ded2c975e7af28 # Parent d98a0388faab49ae47d3a9a810eb7d6c7fd6f833 really document just one code generator; diff -r d98a0388faab -r 008710fff1cc doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 09:11:21 2011 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 14:21:29 2011 +0200 @@ -1724,17 +1724,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. -*} - - -subsection {* The new code generator (F. Haftmann) *} - -text {* 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 diff -r d98a0388faab -r 008710fff1cc doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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%