--- 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"
--- 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
--- 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
--- 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%
--- 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
--- 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]
--- 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;
--- 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