# HG changeset patch # User nipkow # Date 1319034750 -7200 # Node ID 154242732ef87d1f69a9bf9f3f14772181cf5de2 # Parent 78478d938cb8c269cbe5d434dc9dbdfa5f2d7de6# Parent 1f1897ac78771e5b49633c2edcf0de58b20d8ba1 merged diff -r 1f1897ac7877 -r 154242732ef8 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Wed Oct 19 16:32:12 2011 +0200 +++ b/Admin/isatest/isatest-stats Wed Oct 19 16:32:30 2011 +0200 @@ -8,161 +8,177 @@ PLATFORMS="at-poly at-poly-test afp at64-poly cygwin-poly-e mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at64-poly-5.1-para at-mac-poly-5.1-para at-sml-dev" -ISABELLE_SESSIONS="\ - HOL-Auth \ - HOL-Bali \ - HOL-Boogie-Examples \ - HOL-Decision_Procs \ - HOL-Hahn_Banach \ - HOL-Hoare \ - HOL-Hoare_Parallel \ - HOL-IMPP \ - HOL-IOA \ - HOL-Imperative_HOL \ - HOL-Import \ - HOL-Induct \ - HOL-Isar_Examples \ - HOL-Lattice \ - HOL-Library-Codegenerator_Test \ - HOL-Matrix \ - HOL-Metis_Examples \ - HOL-MicroJava \ - HOL-Mirabelle \ - HOL-Mutabelle \ - HOL-NanoJava \ - HOL-Nitpick_Examples \ +ISABELLE_SESSIONS=" + HOL + HOL-Main + HOL-Plain + HOL-Base + HOL-Library + HOL-Algebra + HOL-Auth + HOL-Bali + HOL-Boogie + HOL-Boogie-Examples + HOL-Decision_Procs + HOL-Hahn_Banach + HOL-Hoare + HOL-Hoare_Parallel + HOL-IMP + HOL-IMPP + HOL-IOA + HOL-Imperative_HOL + HOL-Import + HOL-Induct + HOL-Isar_Examples + HOL-Lattice + HOL-Library-Codegenerator_Test + HOL-Matrix + HOL-Metis_Examples + HOL-MicroJava + HOL-Mirabelle + HOL-Multivariate_Analysis + HOL-Mutabelle + HOL-NSA + HOL-NanoJava + HOL-Nitpick_Examples + HOL-Nominal HOL-Nominal-Examples - HOL-Number_Theory \ - HOL-Old_Number_Theory \ - HOL-Predicate_Compile_Examples \ + HOL-Number_Theory + HOL-Old_Number_Theory + HOL-Predicate_Compile_Examples HOL-Probability - HOL-Prolog \ - HOL-Proofs-Extraction \ - HOL-Proofs-Lambda \ - HOL-Proofs-ex \ - HOL-Quotient_Examples \ - HOL-SET_Protocol \ - HOL-SPARK-Examples \ - HOL-SPARK-Manual \ - HOL-Statespace \ - HOL-TPTP \ - HOL-UNITY \ - HOL-Unix \ - HOL-Word-Examples \ - HOL-Word-SMT_Examples \ + HOL-Prolog + HOL-Proofs + HOL-Proofs-Extraction + HOL-Proofs-Lambda + HOL-Proofs-ex + HOL-Quotient_Examples + HOL-SET_Protocol + HOL-SPARK + HOL-SPARK-Examples + HOL-SPARK-Manual + HOL-Statespace + HOL-TPTP + HOL-UNITY + HOL-Unix + HOL-Word + HOL-Word-Examples + HOL-Word-SMT_Examples HOL-ZF - HOL-ex \ - HOLCF-FOCUS \ - HOLCF-IMP \ - HOLCF-Library \ - HOLCF-Tutorial \ - HOLCF-ex \ - IOA-ABP \ - IOA-NTP \ - IOA-Storage \ - IOA-ex \ - TLA-Buffer \ - TLA-Inc \ + HOL-ex + HOL4 + HOLCF + HOLCF-FOCUS + HOLCF-IMP + HOLCF-Library + HOLCF-Tutorial + HOLCF-ex + IOA + IOA-ABP + IOA-NTP + IOA-Storage + IOA-ex + TLA + TLA-Buffer + TLA-Inc TLA-Memory" -AFP_SESSIONS="\ - ArrowImpossibilityGS \ - Coinductive \ - CoreC++ \ - HOL-AVL-Trees \ - HOL-Abstract-Hoare-Logics \ - HOL-Abstract-Rewriting \ - HOL-BinarySearchTree \ - HOL-Binomial-Heaps \ - HOL-Binomial-Queues \ - HOL-BytecodeLogicJmlTypes \ - HOL-Category \ - HOL-Category2 \ - HOL-Cauchy \ - HOL-ClockSynchInst \ - HOL-CofGroups \ - HOL-Collections \ - HOL-Compiling-Exceptions-Correctly \ - HOL-Completeness \ - HOL-DPT-SAT-Solver \ - HOL-DataRefinementIBP \ - HOL-Depth-First-Search \ - HOL-DiskPaxos \ - HOL-Example-Submission \ - HOL-FFT \ - HOL-FOL-Fitting \ - HOL-FeatherweightJava \ - HOL-FileRefinement \ - HOL-FinFun \ - HOL-Finger-Trees \ - HOL-Flyspeck-Tame \ - HOL-Free-Boolean-Algebra \ - HOL-Free-Groups \ - HOL-FunWithFunctions \ - HOL-FunWithTilings \ - HOL-Functional-Automata \ - HOL-Gauss-Jordan-Elim-Fun \ - HOL-GenClock \ - HOL-General-Triangle \ - HOL-GraphMarkingIBP \ - HOL-HotelKeyCards \ - HOL-Huffman \ - HOL-Integration \ - HOL-JiveDataStoreModel \ - HOL-KBPs \ - HOL-Lazy-Lists-II \ - HOL-LightweightJava \ - HOL-List-Index \ - HOL-Locally-Nameless-Sigma \ - HOL-Marriage \ - HOL-Matrix \ - HOL-Max-Card-Matching \ - HOL-MiniML \ - HOL-MuchAdoAboutTwo \ - HOL-Multivariate_Analysis \ - HOL-Myhill-Nerode \ - HOL-Nominal \ - HOL-Nominal-Lam-ml-Normalization \ - HOL-Nominal-SequentInvertibility \ - HOL-Ordinal \ - HOL-Ordinals_and_Cardinals \ - HOL-POPLmark-deBruijn \ - HOL-Perfect-Number-Thm \ - HOL-Polynomials \ - HOL-Presburger-Automata \ - HOL-Program-Conflict-Analysis \ - HOL-Ramsey-Infinite \ - HOL-Recursion-Theory-I \ - HOL-Regular-Sets \ - HOL-Robbins-Conjecture \ - HOL-SATSolverVerification \ - HOL-SIFPL \ - HOL-SenSocialChoice \ - HOL-Statecharts \ - HOL-Topology \ - HOL-Transitive-Closure \ - HOL-Tree-Automata \ - HOL-Verified-Prover \ - HOL-Word \ - HOL-Word-RIPEMD-160-SPARK \ - HOLCF \ - HOLCF-Shivers-CFA \ - HOLCF-Stream-Fusion \ - HOLCF-WorkerWrapper \ - HRB-Slicing \ - HRB-Slicing-InformationFlowSlicing \ - Jinja \ - Jinja \ - LatticeProperties \ - LatticeProperties-MonoBoolTranAlgebra \ - LatticeProperties-PseudoHoops \ - Lower_Semicontinuous \ - NormByEval \ - Simpl \ - Simpl-BDD \ - Slicing \ - Slicing \ - Slicing-InformationFlowSlicing \ +AFP_SESSIONS=" + ArrowImpossibilityGS + Coinductive + CoreC++ + HOL-AVL-Trees + HOL-Abstract-Hoare-Logics + HOL-Abstract-Rewriting + HOL-BinarySearchTree + HOL-Binomial-Heaps + HOL-Binomial-Queues + HOL-BytecodeLogicJmlTypes + HOL-Category + HOL-Category2 + HOL-Cauchy + HOL-ClockSynchInst + HOL-CofGroups + HOL-Collections + HOL-Compiling-Exceptions-Correctly + HOL-Completeness + HOL-DPT-SAT-Solver + HOL-DataRefinementIBP + HOL-Depth-First-Search + HOL-DiskPaxos + HOL-Example-Submission + HOL-FFT + HOL-FOL-Fitting + HOL-FeatherweightJava + HOL-FileRefinement + HOL-FinFun + HOL-Finger-Trees + HOL-Flyspeck-Tame + HOL-Free-Boolean-Algebra + HOL-Free-Groups + HOL-FunWithFunctions + HOL-FunWithTilings + HOL-Functional-Automata + HOL-Gauss-Jordan-Elim-Fun + HOL-GenClock + HOL-General-Triangle + HOL-GraphMarkingIBP + HOL-HotelKeyCards + HOL-Huffman + HOL-Integration + HOL-JiveDataStoreModel + HOL-KBPs + HOL-Lazy-Lists-II + HOL-LightweightJava + HOL-List-Index + HOL-Locally-Nameless-Sigma + HOL-Marriage + HOL-Matrix + HOL-Max-Card-Matching + HOL-MiniML + HOL-MuchAdoAboutTwo + HOL-Multivariate_Analysis + HOL-Myhill-Nerode + HOL-Nominal + HOL-Nominal-Lam-ml-Normalization + HOL-Nominal-SequentInvertibility + HOL-Ordinal + HOL-Ordinals_and_Cardinals + HOL-POPLmark-deBruijn + HOL-Perfect-Number-Thm + HOL-Polynomials + HOL-Presburger-Automata + HOL-Program-Conflict-Analysis + HOL-Ramsey-Infinite + HOL-Recursion-Theory-I + HOL-Regular-Sets + HOL-Robbins-Conjecture + HOL-SATSolverVerification + HOL-SIFPL + HOL-SenSocialChoice + HOL-Statecharts + HOL-Topology + HOL-Transitive-Closure + HOL-Tree-Automata + HOL-Verified-Prover + HOL-Word + HOL-Word-RIPEMD-160-SPARK + HOLCF + HOLCF-Shivers-CFA + HOLCF-Stream-Fusion + HOLCF-WorkerWrapper + HRB-Slicing + HRB-Slicing-InformationFlowSlicing + Jinja + LatticeProperties + LatticeProperties-MonoBoolTranAlgebra + LatticeProperties-PseudoHoops + Lower_Semicontinuous + NormByEval + Simpl + Simpl-BDD + Slicing + Slicing-InformationFlowSlicing VolpanoSmith" diff -r 1f1897ac7877 -r 154242732ef8 NEWS --- a/NEWS Wed Oct 19 16:32:12 2011 +0200 +++ b/NEWS Wed Oct 19 16:32:30 2011 +0200 @@ -28,6 +28,7 @@ zadd_commute ~> add_commute zadd_assoc ~> add_assoc zadd_left_commute ~> add_left_commute + zadd_ac ~> add_ac zmult_ac ~> mult_ac zadd_0 ~> add_0_left zadd_0_right ~> add_0_right diff -r 1f1897ac7877 -r 154242732ef8 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 16:32:12 2011 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Oct 19 16:32:30 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 1f1897ac7877 -r 154242732ef8 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 19 16:32:12 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Oct 19 16:32:30 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% diff -r 1f1897ac7877 -r 154242732ef8 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Oct 19 16:32:12 2011 +0200 +++ b/etc/isar-keywords.el Wed Oct 19 16:32:30 2011 +0200 @@ -51,8 +51,6 @@ "code_deps" "code_include" "code_instance" - "code_library" - "code_module" "code_modulename" "code_monad" "code_pred" @@ -64,7 +62,6 @@ "coinductive_set" "commit" "consts" - "consts_code" "context" "corollary" "cpodef" @@ -264,7 +261,6 @@ "typed_print_translation" "typedecl" "typedef" - "types_code" "ultimately" "undo" "undos_proof" @@ -292,7 +288,6 @@ "checking" "congs" "constrains" - "contains" "datatypes" "defines" "file" @@ -456,8 +451,6 @@ "code_datatype" "code_include" "code_instance" - "code_library" - "code_module" "code_modulename" "code_monad" "code_reflect" @@ -466,7 +459,6 @@ "coinductive" "coinductive_set" "consts" - "consts_code" "context" "datatype" "declaration" @@ -538,7 +530,6 @@ "type_synonym" "typed_print_translation" "typedecl" - "types_code" "use")) (defconst isar-keywords-theory-script diff -r 1f1897ac7877 -r 154242732ef8 src/HOL/Int.thy --- a/src/HOL/Int.thy Wed Oct 19 16:32:12 2011 +0200 +++ b/src/HOL/Int.thy Wed Oct 19 16:32:30 2011 +0200 @@ -2390,9 +2390,6 @@ subsection {* Legacy theorems *} -(* used by Tools/Qelim/cooper.ML *) -lemmas zadd_ac = add_ac [where 'a=int] - lemmas inj_int = inj_of_nat [where 'a=int] lemmas zadd_int = of_nat_add [where 'a=int, symmetric] lemmas int_mult = of_nat_mult [where 'a=int] diff -r 1f1897ac7877 -r 154242732ef8 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 19 16:32:12 2011 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 19 16:32:30 2011 +0200 @@ -74,7 +74,8 @@ val false_tm = @{cterm "False"}; val zdvd1_eq = @{thm "zdvd1_eq"}; val presburger_ss = @{simpset} addsimps [zdvd1_eq]; -val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac}); +val lin_ss = + presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms add_ac [where 'a=int]}); val iT = HOLogic.intT val bT = HOLogic.boolT; diff -r 1f1897ac7877 -r 154242732ef8 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Wed Oct 19 16:32:12 2011 +0200 +++ b/src/Tools/misc_legacy.ML Wed Oct 19 16:32:30 2011 +0200 @@ -5,7 +5,6 @@ signature MISC_LEGACY = sig - val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a val add_term_names: term * string list -> string list val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list val add_typ_tfree_names: typ * string list -> string list