--- a/CONTRIBUTORS Tue Aug 17 15:54:04 2010 +0200
+++ b/CONTRIBUTORS Tue Aug 17 16:38:45 2010 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* July 2010: Florian Haftmann, TUM
+ Reworking and extension of the Isabelle/HOL framework.
+
Contributions to Isabelle2009-2
--------------------------------------
--- a/NEWS Tue Aug 17 15:54:04 2010 +0200
+++ b/NEWS Tue Aug 17 16:38:45 2010 +0200
@@ -35,11 +35,17 @@
*** HOL ***
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Quickcheck in locales considers interpretations of that locale for
+counter example search.
+
* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
in Library/State_Monad has been changed to avoid ambiguities.
INCOMPATIBILITY.
-* code generator: export_code without explicit file declaration prints
+* Code generator: export_code without explicit file declaration prints
to standard output. INCOMPATIBILITY.
* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
@@ -121,8 +127,8 @@
INCOMPATIBILITY.
* Inductive package: offers new command "inductive_simps" to automatically
- derive instantiated and simplified equations for inductive predicates,
- similar to inductive_cases.
+derive instantiated and simplified equations for inductive predicates,
+similar to inductive_cases.
*** ML ***
--- a/doc-src/Codegen/Thy/Adaptation.thy Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Tue Aug 17 16:38:45 2010 +0200
@@ -13,18 +13,21 @@
in common:
\begin{itemize}
- \item They act uniformly, without reference to a specific
- target language.
+
+ \item They act uniformly, without reference to a specific target
+ language.
+
\item They are \emph{safe} in the sense that as long as you trust
the code generator meta theory and implementation, you cannot
- produce programs that yield results which are not derivable
- in the logic.
+ produce programs that yield results which are not derivable in
+ the logic.
+
\end{itemize}
- \noindent In this section we will introduce means to \emph{adapt} the serialiser
- to a specific target language, i.e.~to print program fragments
- in a way which accommodates \qt{already existing} ingredients of
- a target language environment, for three reasons:
+ \noindent In this section we will introduce means to \emph{adapt}
+ the serialiser to a specific target language, i.e.~to print program
+ fragments in a way which accommodates \qt{already existing}
+ ingredients of a target language environment, for three reasons:
\begin{itemize}
\item improving readability and aesthetics of generated code
@@ -37,26 +40,34 @@
\emph{at any cost}:
\begin{itemize}
- \item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separately.
- \item Application is extremely tedious since there is no abstraction
- which would allow for a static check, making it easy to produce garbage.
+
+ \item The safe configuration methods act uniformly on every target
+ language, whereas for adaptation you have to treat each target
+ language separately.
+
+ \item Application is extremely tedious since there is no
+ abstraction which would allow for a static check, making it easy
+ to produce garbage.
+
\item Subtle errors can be introduced unconsciously.
+
\end{itemize}
- \noindent However, even if you ought refrain from setting up adaptation
- yourself, already the @{text "HOL"} comes with some reasonable default
- adaptations (say, using target language list syntax). There also some
- common adaptation cases which you can setup by importing particular
- library theories. In order to understand these, we provide some clues here;
- these however are not supposed to replace a careful study of the sources.
+ \noindent However, even if you ought refrain from setting up
+ adaptation yourself, already the @{text "HOL"} comes with some
+ reasonable default adaptations (say, using target language list
+ syntax). There also some common adaptation cases which you can
+ setup by importing particular library theories. In order to
+ understand these, we provide some clues here; these however are not
+ supposed to replace a careful study of the sources.
*}
+
subsection {* The adaptation principle *}
text {*
- Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
- supposed to be:
+ Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
+ conceptually supposed to be:
\begin{figure}[here]
\includegraphics{adaptation}
@@ -65,79 +76,87 @@
\end{figure}
\noindent In the tame view, code generation acts as broker between
- @{text logic}, @{text "intermediate language"} and
- @{text "target language"} by means of @{text translation} and
- @{text serialisation}; for the latter, the serialiser has to observe
- the structure of the @{text language} itself plus some @{text reserved}
- keywords which have to be avoided for generated code.
- However, if you consider @{text adaptation} mechanisms, the code generated
- by the serializer is just the tip of the iceberg:
+ @{text logic}, @{text "intermediate language"} and @{text "target
+ language"} by means of @{text translation} and @{text
+ serialisation}; for the latter, the serialiser has to observe the
+ structure of the @{text language} itself plus some @{text reserved}
+ keywords which have to be avoided for generated code. However, if
+ you consider @{text adaptation} mechanisms, the code generated by
+ the serializer is just the tip of the iceberg:
\begin{itemize}
+
\item @{text serialisation} can be \emph{parametrised} such that
logical entities are mapped to target-specific ones
- (e.g. target-specific list syntax,
- see also \secref{sec:adaptation_mechanisms})
+ (e.g. target-specific list syntax, see also
+ \secref{sec:adaptation_mechanisms})
+
\item Such parametrisations can involve references to a
- target-specific standard @{text library} (e.g. using
- the @{text Haskell} @{verbatim Maybe} type instead
- of the @{text HOL} @{type "option"} type);
- if such are used, the corresponding identifiers
- (in our example, @{verbatim Maybe}, @{verbatim Nothing}
- and @{verbatim Just}) also have to be considered @{text reserved}.
+ target-specific standard @{text library} (e.g. using the @{text
+ Haskell} @{verbatim Maybe} type instead of the @{text HOL}
+ @{type "option"} type); if such are used, the corresponding
+ identifiers (in our example, @{verbatim Maybe}, @{verbatim
+ Nothing} and @{verbatim Just}) also have to be considered @{text
+ reserved}.
+
\item Even more, the user can enrich the library of the
- target-language by providing code snippets
- (\qt{@{text "includes"}}) which are prepended to
- any generated code (see \secref{sec:include}); this typically
- also involves further @{text reserved} identifiers.
+ target-language by providing code snippets (\qt{@{text
+ "includes"}}) which are prepended to any generated code (see
+ \secref{sec:include}); this typically also involves further
+ @{text reserved} identifiers.
+
\end{itemize}
- \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
- have to act consistently; it is at the discretion of the user
- to take care for this.
+ \noindent As figure \ref{fig:adaptation} illustrates, all these
+ adaptation mechanisms have to act consistently; it is at the
+ discretion of the user to take care for this.
*}
subsection {* Common adaptation patterns *}
text {*
The @{theory HOL} @{theory Main} theory already provides a code
- generator setup
- which should be suitable for most applications. Common extensions
- and modifications are available by certain theories of the @{text HOL}
- library; beside being useful in applications, they may serve
- as a tutorial for customising the code generator setup (see below
- \secref{sec:adaptation_mechanisms}).
+ generator setup which should be suitable for most applications.
+ Common extensions and modifications are available by certain
+ theories of the @{text HOL} library; beside being useful in
+ applications, they may serve as a tutorial for customising the code
+ generator setup (see below \secref{sec:adaptation_mechanisms}).
\begin{description}
- \item[@{theory "Code_Integer"}] represents @{text HOL} integers by big
- integer literals in target languages.
- \item[@{theory "Code_Char"}] represents @{text HOL} characters by
+ \item[@{theory "Code_Integer"}] represents @{text HOL} integers by
+ big integer literals in target languages.
+
+ \item[@{theory "Code_Char"}] represents @{text HOL} characters by
character literals in target languages.
- \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"},
- but also offers treatment of character codes; includes
- @{theory "Code_Char"}.
- \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements natural numbers by integers,
- which in general will result in higher efficiency; pattern
- matching with @{term "0\<Colon>nat"} / @{const "Suc"}
- is eliminated; includes @{theory "Code_Integer"}
+
+ \item[@{theory "Code_Char_chr"}] like @{text "Code_Char"}, but
+ also offers treatment of character codes; includes @{theory
+ "Code_Char"}.
+
+ \item[@{theory "Efficient_Nat"}] \label{eff_nat} implements
+ natural numbers by integers, which in general will result in
+ higher efficiency; pattern matching with @{term "0\<Colon>nat"} /
+ @{const "Suc"} is eliminated; includes @{theory "Code_Integer"}
and @{theory "Code_Numeral"}.
+
\item[@{theory "Code_Numeral"}] provides an additional datatype
- @{typ index} which is mapped to target-language built-in integers.
- Useful for code setups which involve e.g. indexing of
- target-language arrays.
- \item[@{theory "String"}] provides an additional datatype
- @{typ String.literal} which is isomorphic to strings;
- @{typ String.literal}s are mapped to target-language strings.
- Useful for code setups which involve e.g. printing (error) messages.
+ @{typ index} which is mapped to target-language built-in
+ integers. Useful for code setups which involve e.g.~indexing
+ of target-language arrays.
+
+ \item[@{theory "String"}] provides an additional datatype @{typ
+ String.literal} which is isomorphic to strings; @{typ
+ String.literal}s are mapped to target-language strings. Useful
+ for code setups which involve e.g.~printing (error) messages.
\end{description}
\begin{warn}
When importing any of these theories, they should form the last
- items in an import list. Since these theories adapt the
- code generator setup in a non-conservative fashion,
- strange effects may occur otherwise.
+ items in an import list. Since these theories adapt the code
+ generator setup in a non-conservative fashion, strange effects may
+ occur otherwise.
\end{warn}
*}
@@ -145,8 +164,7 @@
subsection {* Parametrising serialisation \label{sec:adaptation_mechanisms} *}
text {*
- Consider the following function and its corresponding
- SML code:
+ Consider the following function and its corresponding SML code:
*}
primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
@@ -160,15 +178,14 @@
text %quote {*@{code_stmts in_interval (SML)}*}
text {*
- \noindent Though this is correct code, it is a little bit unsatisfactory:
- boolean values and operators are materialised as distinguished
- entities with have nothing to do with the SML-built-in notion
- of \qt{bool}. This results in less readable code;
- additionally, eager evaluation may cause programs to
- loop or break which would perfectly terminate when
- the existing SML @{verbatim "bool"} would be used. To map
- the HOL @{typ bool} on SML @{verbatim "bool"}, we may use
- \qn{custom serialisations}:
+ \noindent Though this is correct code, it is a little bit
+ unsatisfactory: boolean values and operators are materialised as
+ distinguished entities with have nothing to do with the SML-built-in
+ notion of \qt{bool}. This results in less readable code;
+ additionally, eager evaluation may cause programs to loop or break
+ which would perfectly terminate when the existing SML @{verbatim
+ "bool"} would be used. To map the HOL @{typ bool} on SML @{verbatim
+ "bool"}, we may use \qn{custom serialisations}:
*}
code_type %quotett bool
@@ -178,25 +195,23 @@
text {*
\noindent The @{command code_type} command takes a type constructor
- as arguments together with a list of custom serialisations.
- Each custom serialisation starts with a target language
- identifier followed by an expression, which during
- code serialisation is inserted whenever the type constructor
- would occur. For constants, @{command code_const} implements
- the corresponding mechanism. Each ``@{verbatim "_"}'' in
- a serialisation expression is treated as a placeholder
- for the type constructor's (the constant's) arguments.
+ as arguments together with a list of custom serialisations. Each
+ custom serialisation starts with a target language identifier
+ followed by an expression, which during code serialisation is
+ inserted whenever the type constructor would occur. For constants,
+ @{command code_const} implements the corresponding mechanism. Each
+ ``@{verbatim "_"}'' in a serialisation expression is treated as a
+ placeholder for the type constructor's (the constant's) arguments.
*}
text %quote {*@{code_stmts in_interval (SML)}*}
text {*
- \noindent This still is not perfect: the parentheses
- around the \qt{andalso} expression are superfluous.
- Though the serialiser
- by no means attempts to imitate the rich Isabelle syntax
- framework, it provides some common idioms, notably
- associative infixes with precedences which may be used here:
+ \noindent This still is not perfect: the parentheses around the
+ \qt{andalso} expression are superfluous. Though the serialiser by
+ no means attempts to imitate the rich Isabelle syntax framework, it
+ provides some common idioms, notably associative infixes with
+ precedences which may be used here:
*}
code_const %quotett "op \<and>"
@@ -205,12 +220,13 @@
text %quote {*@{code_stmts in_interval (SML)}*}
text {*
- \noindent The attentive reader may ask how we assert that no generated
- code will accidentally overwrite. For this reason the serialiser has
- an internal table of identifiers which have to be avoided to be used
- for new declarations. Initially, this table typically contains the
- keywords of the target language. It can be extended manually, thus avoiding
- accidental overwrites, using the @{command "code_reserved"} command:
+ \noindent The attentive reader may ask how we assert that no
+ generated code will accidentally overwrite. For this reason the
+ serialiser has an internal table of identifiers which have to be
+ avoided to be used for new declarations. Initially, this table
+ typically contains the keywords of the target language. It can be
+ extended manually, thus avoiding accidental overwrites, using the
+ @{command "code_reserved"} command:
*}
code_reserved %quote "\<SML>" bool true false andalso
@@ -232,37 +248,33 @@
text {*
\noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
- never to put
- parentheses around the whole expression (they are already present),
- while the parentheses around argument place holders
- tell not to put parentheses around the arguments.
- The slash ``@{verbatim "/"}'' (followed by arbitrary white space)
- inserts a space which may be used as a break if necessary
- during pretty printing.
+ never to put parentheses around the whole expression (they are
+ already present), while the parentheses around argument place
+ holders tell not to put parentheses around the arguments. The slash
+ ``@{verbatim "/"}'' (followed by arbitrary white space) inserts a
+ space which may be used as a break if necessary during pretty
+ printing.
- These examples give a glimpse what mechanisms
- custom serialisations provide; however their usage
- requires careful thinking in order not to introduce
- inconsistencies -- or, in other words:
- custom serialisations are completely axiomatic.
+ These examples give a glimpse what mechanisms custom serialisations
+ provide; however their usage requires careful thinking in order not
+ to introduce inconsistencies -- or, in other words: custom
+ serialisations are completely axiomatic.
- A further noteworthy details is that any special
- character in a custom serialisation may be quoted
- using ``@{verbatim "'"}''; thus, in
- ``@{verbatim "fn '_ => _"}'' the first
- ``@{verbatim "_"}'' is a proper underscore while the
- second ``@{verbatim "_"}'' is a placeholder.
+ A further noteworthy details is that any special character in a
+ custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
+ in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
+ proper underscore while the second ``@{verbatim "_"}'' is a
+ placeholder.
*}
subsection {* @{text Haskell} serialisation *}
text {*
- For convenience, the default
- @{text HOL} setup for @{text Haskell} maps the @{class eq} class to
- its counterpart in @{text Haskell}, giving custom serialisations
- for the class @{class eq} (by command @{command code_class}) and its operation
- @{const HOL.eq}
+ For convenience, the default @{text HOL} setup for @{text Haskell}
+ maps the @{class eq} class to its counterpart in @{text Haskell},
+ giving custom serialisations for the class @{class eq} (by command
+ @{command code_class}) and its operation @{const HOL.eq}
*}
code_class %quotett eq
@@ -272,10 +284,10 @@
(Haskell infixl 4 "==")
text {*
- \noindent A problem now occurs whenever a type which
- is an instance of @{class eq} in @{text HOL} is mapped
- on a @{text Haskell}-built-in type which is also an instance
- of @{text Haskell} @{text Eq}:
+ \noindent A problem now occurs whenever a type which is an instance
+ of @{class eq} in @{text HOL} is mapped on a @{text
+ Haskell}-built-in type which is also an instance of @{text Haskell}
+ @{text Eq}:
*}
typedecl %quote bar
@@ -293,11 +305,9 @@
(Haskell "Integer")
text {*
- \noindent The code generator would produce
- an additional instance, which of course is rejected by the @{text Haskell}
- compiler.
- To suppress this additional instance, use
- @{text "code_instance"}:
+ \noindent The code generator would produce an additional instance,
+ which of course is rejected by the @{text Haskell} compiler. To
+ suppress this additional instance, use @{text "code_instance"}:
*}
code_instance %quotett bar :: eq
@@ -308,8 +318,8 @@
text {*
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command "code_include"}
- command:
+ target language; this is accomplished using the @{command
+ "code_include"} command:
*}
code_include %quotett Haskell "Errno"
@@ -318,9 +328,10 @@
code_reserved %quotett Haskell Errno
text {*
- \noindent Such named @{text include}s are then prepended to every generated code.
- Inspect such code in order to find out how @{command "code_include"} behaves
- with respect to a particular target language.
+ \noindent Such named @{text include}s are then prepended to every
+ generated code. Inspect such code in order to find out how
+ @{command "code_include"} behaves with respect to a particular
+ target language.
*}
end
--- a/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Tue Aug 17 16:38:45 2010 +0200
@@ -7,7 +7,6 @@
subsection {* Code generator architecture \label{sec:architecture} *}
text {*
-
The code generator is actually a framework consisting of different
components which can be customised individually.
--- a/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Tue Aug 17 16:38:45 2010 +0200
@@ -4,23 +4,83 @@
section {* Program and datatype refinement \label{sec:refinement} *}
-subsection {* Datatypes \label{sec:datatypes} *}
+text {*
+ Code generation by shallow embedding (cf.~\secref{sec:principle})
+ allows to choose code equations and datatype constructors freely,
+ given that some very basic syntactic properties are met; this
+ flexibility opens up mechanisms for refinement which allow to extend
+ the scope and quality of generated code dramatically.
+*}
+
+
+subsection {* Program refinement *}
+
+text {*
+ Program refinement works by choosing appropriate code equations
+ explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ numbers:
+*}
+
+fun %quote fib :: "nat \<Rightarrow> nat" where
+ "fib 0 = 0"
+ | "fib (Suc 0) = Suc 0"
+ | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
+text {*
+ \noindent The runtime of the corresponding code grows exponential due
+ to two recursive calls:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib (Haskell)}*}
text {*
- Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
- "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
- @{text "\<tau>"}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- @{command print_codesetup} command.
+ \noindent A more efficient implementation would use dynamic
+ programming, e.g.~sharing of common intermediate results between
+ recursive calls. This idea is expressed by an auxiliary operation
+ which computes a Fibonacci number and its successor simultaneously:
+*}
+
+definition %quote fib_step :: "nat \<Rightarrow> nat \<times> nat" where
+ "fib_step n = (fib (Suc n), fib n)"
+
+text {*
+ \noindent This operation can be implemented by recursion using
+ dynamic programming:
+*}
+
+lemma %quote [code]:
+ "fib_step 0 = (Suc 0, 0)"
+ "fib_step (Suc n) = (let (m, q) = fib_step n in (m + q, m))"
+ by (simp_all add: fib_step_def)
+
+text {*
+ \noindent What remains is to implement @{const fib} by @{const
+ fib_step} as follows:
+*}
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:queue_example}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:
+lemma %quote [code]:
+ "fib 0 = 0"
+ "fib (Suc n) = fst (fib_step n)"
+ by (simp_all add: fib_step_def)
+
+text {*
+ \noindent The resulting code shows only linear growth of runtime:
+*}
+
+text %quote {*@{code_stmts fib (consts) fib fib_step (Haskell)}*}
+
+
+subsection {* Datatype refinement *}
+
+text {*
+ Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. As an example, we will develop an
+ alternative representation of the queue example given in
+ \secref{sec:queue_example}. The amortised representation is
+ convenient for generating code but exposes its \qt{implementation}
+ details, which may be cumbersome when proving theorems about it.
+ Therefore, here is a simple, straightforward representation of
+ queues:
*}
datatype %quote 'a queue = Queue "'a list"
@@ -49,7 +109,18 @@
\noindent Here we define a \qt{constructor} @{const "AQueue"} which
is defined in terms of @{text "Queue"} and interprets its arguments
according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ constructor must be of type @{text "\<tau> = \<dots> \<Rightarrow> \<kappa> \<alpha>\<^isub>1 \<dots> \<alpha>\<^isub>n"} where @{text
+ "{\<alpha>\<^isub>1, \<dots>, \<alpha>\<^isub>n}"} is exactly the set of \emph{all} type variables in
+ @{text "\<tau>"}; then @{text "\<kappa>"} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using @{command
+ code_datatype}; the currently chosen constructors can be inspected
+ using the @{command print_codesetup} command.
+
+ Equipped with this, we are able to prove the following equations
for our primitive queue operations which \qt{implement} the simple
queues in an amortised fashion:
*}
@@ -85,28 +156,21 @@
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
text {*
- \noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
-
- \begin{itemize}
-
- \item When changing the constructor set for datatypes, take care
- to provide alternative equations for the @{text case} combinator.
+ The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type @{typ int} is originally specified
+ as quotient type by means of @{command typedef}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for @{typ int}.
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.
+*}
+
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
+subsection {* Datatype refinement involving invariants *}
- \end{itemize}
+text {*
+ FIXME
*}
end
--- a/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Tue Aug 17 16:38:45 2010 +0200
@@ -1,5 +1,5 @@
theory Setup
-imports Complex_Main
+imports Complex_Main More_List
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Tue Aug 17 16:38:45 2010 +0200
@@ -47,18 +47,21 @@
in common:
\begin{itemize}
- \item They act uniformly, without reference to a specific
- target language.
+
+ \item They act uniformly, without reference to a specific target
+ language.
+
\item They are \emph{safe} in the sense that as long as you trust
the code generator meta theory and implementation, you cannot
- produce programs that yield results which are not derivable
- in the logic.
+ produce programs that yield results which are not derivable in
+ the logic.
+
\end{itemize}
- \noindent In this section we will introduce means to \emph{adapt} the serialiser
- to a specific target language, i.e.~to print program fragments
- in a way which accommodates \qt{already existing} ingredients of
- a target language environment, for three reasons:
+ \noindent In this section we will introduce means to \emph{adapt}
+ the serialiser to a specific target language, i.e.~to print program
+ fragments in a way which accommodates \qt{already existing}
+ ingredients of a target language environment, for three reasons:
\begin{itemize}
\item improving readability and aesthetics of generated code
@@ -71,19 +74,26 @@
\emph{at any cost}:
\begin{itemize}
- \item The safe configuration methods act uniformly on every target language,
- whereas for adaptation you have to treat each target language separately.
- \item Application is extremely tedious since there is no abstraction
- which would allow for a static check, making it easy to produce garbage.
+
+ \item The safe configuration methods act uniformly on every target
+ language, whereas for adaptation you have to treat each target
+ language separately.
+
+ \item Application is extremely tedious since there is no
+ abstraction which would allow for a static check, making it easy
+ to produce garbage.
+
\item Subtle errors can be introduced unconsciously.
+
\end{itemize}
- \noindent However, even if you ought refrain from setting up adaptation
- yourself, already the \isa{HOL} comes with some reasonable default
- adaptations (say, using target language list syntax). There also some
- common adaptation cases which you can setup by importing particular
- library theories. In order to understand these, we provide some clues here;
- these however are not supposed to replace a careful study of the sources.%
+ \noindent However, even if you ought refrain from setting up
+ adaptation yourself, already the \isa{HOL} comes with some
+ reasonable default adaptations (say, using target language list
+ syntax). There also some common adaptation cases which you can
+ setup by importing particular library theories. In order to
+ understand these, we provide some clues here; these however are not
+ supposed to replace a careful study of the sources.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -92,8 +102,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is conceptually
- supposed to be:
+Figure \ref{fig:adaptation} illustrates what \qt{adaptation} is
+ conceptually supposed to be:
\begin{figure}[here]
\includegraphics{adaptation}
@@ -102,36 +112,34 @@
\end{figure}
\noindent In the tame view, code generation acts as broker between
- \isa{logic}, \isa{intermediate\ language} and
- \isa{target\ language} by means of \isa{translation} and
- \isa{serialisation}; for the latter, the serialiser has to observe
- the structure of the \isa{language} itself plus some \isa{reserved}
- keywords which have to be avoided for generated code.
- However, if you consider \isa{adaptation} mechanisms, the code generated
- by the serializer is just the tip of the iceberg:
+ \isa{logic}, \isa{intermediate\ language} and \isa{target\ language} by means of \isa{translation} and \isa{serialisation}; for the latter, the serialiser has to observe the
+ structure of the \isa{language} itself plus some \isa{reserved}
+ keywords which have to be avoided for generated code. However, if
+ you consider \isa{adaptation} mechanisms, the code generated by
+ the serializer is just the tip of the iceberg:
\begin{itemize}
+
\item \isa{serialisation} can be \emph{parametrised} such that
logical entities are mapped to target-specific ones
- (e.g. target-specific list syntax,
- see also \secref{sec:adaptation_mechanisms})
+ (e.g. target-specific list syntax, see also
+ \secref{sec:adaptation_mechanisms})
+
\item Such parametrisations can involve references to a
- target-specific standard \isa{library} (e.g. using
- the \isa{Haskell} \verb|Maybe| type instead
- of the \isa{HOL} \isa{option} type);
- if such are used, the corresponding identifiers
- (in our example, \verb|Maybe|, \verb|Nothing|
- and \verb|Just|) also have to be considered \isa{reserved}.
+ target-specific standard \isa{library} (e.g. using the \isa{Haskell} \verb|Maybe| type instead of the \isa{HOL}
+ \isa{option} type); if such are used, the corresponding
+ identifiers (in our example, \verb|Maybe|, \verb|Nothing| and \verb|Just|) also have to be considered \isa{reserved}.
+
\item Even more, the user can enrich the library of the
- target-language by providing code snippets
- (\qt{\isa{includes}}) which are prepended to
- any generated code (see \secref{sec:include}); this typically
- also involves further \isa{reserved} identifiers.
+ target-language by providing code snippets (\qt{\isa{includes}}) which are prepended to any generated code (see
+ \secref{sec:include}); this typically also involves further
+ \isa{reserved} identifiers.
+
\end{itemize}
- \noindent As figure \ref{fig:adaptation} illustrates, all these adaptation mechanisms
- have to act consistently; it is at the discretion of the user
- to take care for this.%
+ \noindent As figure \ref{fig:adaptation} illustrates, all these
+ adaptation mechanisms have to act consistently; it is at the
+ discretion of the user to take care for this.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -141,43 +149,44 @@
%
\begin{isamarkuptext}%
The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code
- generator setup
- which should be suitable for most applications. Common extensions
- and modifications are available by certain theories of the \isa{HOL}
- library; beside being useful in applications, they may serve
- as a tutorial for customising the code generator setup (see below
- \secref{sec:adaptation_mechanisms}).
+ generator setup which should be suitable for most applications.
+ Common extensions and modifications are available by certain
+ theories of the \isa{HOL} library; beside being useful in
+ applications, they may serve as a tutorial for customising the code
+ generator setup (see below \secref{sec:adaptation_mechanisms}).
\begin{description}
- \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by big
- integer literals in target languages.
- \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
+ \item[\hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}] represents \isa{HOL} integers by
+ big integer literals in target languages.
+
+ \item[\hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}] represents \isa{HOL} characters by
character literals in target languages.
- \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char},
- but also offers treatment of character codes; includes
- \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
- \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements natural numbers by integers,
- which in general will result in higher efficiency; pattern
- matching with \isa{{\isadigit{0}}} / \isa{Suc}
- is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
+
+ \item[\hyperlink{theory.Code-Char-chr}{\mbox{\isa{Code{\isacharunderscore}Char{\isacharunderscore}chr}}}] like \isa{Code{\isacharunderscore}Char}, but
+ also offers treatment of character codes; includes \hyperlink{theory.Code-Char}{\mbox{\isa{Code{\isacharunderscore}Char}}}.
+
+ \item[\hyperlink{theory.Efficient-Nat}{\mbox{\isa{Efficient{\isacharunderscore}Nat}}}] \label{eff_nat} implements
+ natural numbers by integers, which in general will result in
+ higher efficiency; pattern matching with \isa{{\isadigit{0}}} /
+ \isa{Suc} is eliminated; includes \hyperlink{theory.Code-Integer}{\mbox{\isa{Code{\isacharunderscore}Integer}}}
and \hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}.
+
\item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isacharunderscore}Numeral}}}] provides an additional datatype
- \isa{index} which is mapped to target-language built-in integers.
- Useful for code setups which involve e.g. indexing of
- target-language arrays.
- \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype
- \isa{String{\isachardot}literal} which is isomorphic to strings;
- \isa{String{\isachardot}literal}s are mapped to target-language strings.
- Useful for code setups which involve e.g. printing (error) messages.
+ \isa{index} which is mapped to target-language built-in
+ integers. Useful for code setups which involve e.g.~indexing
+ of target-language arrays.
+
+ \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isachardot}literal} which is isomorphic to strings; \isa{String{\isachardot}literal}s are mapped to target-language strings. Useful
+ for code setups which involve e.g.~printing (error) messages.
\end{description}
\begin{warn}
When importing any of these theories, they should form the last
- items in an import list. Since these theories adapt the
- code generator setup in a non-conservative fashion,
- strange effects may occur otherwise.
+ items in an import list. Since these theories adapt the code
+ generator setup in a non-conservative fashion, strange effects may
+ occur otherwise.
\end{warn}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -187,8 +196,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Consider the following function and its corresponding
- SML code:%
+Consider the following function and its corresponding SML code:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -266,15 +274,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Though this is correct code, it is a little bit unsatisfactory:
- boolean values and operators are materialised as distinguished
- entities with have nothing to do with the SML-built-in notion
- of \qt{bool}. This results in less readable code;
- additionally, eager evaluation may cause programs to
- loop or break which would perfectly terminate when
- the existing SML \verb|bool| would be used. To map
- the HOL \isa{bool} on SML \verb|bool|, we may use
- \qn{custom serialisations}:%
+\noindent Though this is correct code, it is a little bit
+ unsatisfactory: boolean values and operators are materialised as
+ distinguished entities with have nothing to do with the SML-built-in
+ notion of \qt{bool}. This results in less readable code;
+ additionally, eager evaluation may cause programs to loop or break
+ which would perfectly terminate when the existing SML \verb|bool| would be used. To map the HOL \isa{bool} on SML \verb|bool|, we may use \qn{custom serialisations}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -298,14 +303,13 @@
%
\begin{isamarkuptext}%
\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
- as arguments together with a list of custom serialisations.
- Each custom serialisation starts with a target language
- identifier followed by an expression, which during
- code serialisation is inserted whenever the type constructor
- would occur. For constants, \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements
- the corresponding mechanism. Each ``\verb|_|'' in
- a serialisation expression is treated as a placeholder
- for the type constructor's (the constant's) arguments.%
+ as arguments together with a list of custom serialisations. Each
+ custom serialisation starts with a target language identifier
+ followed by an expression, which during code serialisation is
+ inserted whenever the type constructor would occur. For constants,
+ \hyperlink{command.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} implements the corresponding mechanism. Each
+ ``\verb|_|'' in a serialisation expression is treated as a
+ placeholder for the type constructor's (the constant's) arguments.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -346,12 +350,11 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent This still is not perfect: the parentheses
- around the \qt{andalso} expression are superfluous.
- Though the serialiser
- by no means attempts to imitate the rich Isabelle syntax
- framework, it provides some common idioms, notably
- associative infixes with precedences which may be used here:%
+\noindent This still is not perfect: the parentheses around the
+ \qt{andalso} expression are superfluous. Though the serialiser by
+ no means attempts to imitate the rich Isabelle syntax framework, it
+ provides some common idioms, notably associative infixes with
+ precedences which may be used here:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -407,12 +410,13 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The attentive reader may ask how we assert that no generated
- code will accidentally overwrite. For this reason the serialiser has
- an internal table of identifiers which have to be avoided to be used
- for new declarations. Initially, this table typically contains the
- keywords of the target language. It can be extended manually, thus avoiding
- accidental overwrites, using the \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
+\noindent The attentive reader may ask how we assert that no
+ generated code will accidentally overwrite. For this reason the
+ serialiser has an internal table of identifiers which have to be
+ avoided to be used for new declarations. Initially, this table
+ typically contains the keywords of the target language. It can be
+ extended manually, thus avoiding accidental overwrites, using the
+ \hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -469,26 +473,23 @@
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serialiser
- never to put
- parentheses around the whole expression (they are already present),
- while the parentheses around argument place holders
- tell not to put parentheses around the arguments.
- The slash ``\verb|/|'' (followed by arbitrary white space)
- inserts a space which may be used as a break if necessary
- during pretty printing.
+ never to put parentheses around the whole expression (they are
+ already present), while the parentheses around argument place
+ holders tell not to put parentheses around the arguments. The slash
+ ``\verb|/|'' (followed by arbitrary white space) inserts a
+ space which may be used as a break if necessary during pretty
+ printing.
- These examples give a glimpse what mechanisms
- custom serialisations provide; however their usage
- requires careful thinking in order not to introduce
- inconsistencies -- or, in other words:
- custom serialisations are completely axiomatic.
+ These examples give a glimpse what mechanisms custom serialisations
+ provide; however their usage requires careful thinking in order not
+ to introduce inconsistencies -- or, in other words: custom
+ serialisations are completely axiomatic.
- A further noteworthy details is that any special
- character in a custom serialisation may be quoted
- using ``\verb|'|''; thus, in
- ``\verb|fn '_ => _|'' the first
- ``\verb|_|'' is a proper underscore while the
- second ``\verb|_|'' is a placeholder.%
+ A further noteworthy details is that any special character in a
+ custom serialisation may be quoted using ``\verb|'|''; thus,
+ in ``\verb|fn '_ => _|'' the first ``\verb|_|'' is a
+ proper underscore while the second ``\verb|_|'' is a
+ placeholder.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -497,11 +498,10 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-For convenience, the default
- \isa{HOL} setup for \isa{Haskell} maps the \isa{eq} class to
- its counterpart in \isa{Haskell}, giving custom serialisations
- for the class \isa{eq} (by command \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation
- \isa{eq{\isacharunderscore}class{\isachardot}eq}%
+For convenience, the default \isa{HOL} setup for \isa{Haskell}
+ maps the \isa{eq} class to its counterpart in \isa{Haskell},
+ giving custom serialisations for the class \isa{eq} (by command
+ \hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -525,10 +525,9 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent A problem now occurs whenever a type which
- is an instance of \isa{eq} in \isa{HOL} is mapped
- on a \isa{Haskell}-built-in type which is also an instance
- of \isa{Haskell} \isa{Eq}:%
+\noindent A problem now occurs whenever a type which is an instance
+ of \isa{eq} in \isa{HOL} is mapped on a \isa{Haskell}-built-in type which is also an instance of \isa{Haskell}
+ \isa{Eq}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -576,11 +575,9 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent The code generator would produce
- an additional instance, which of course is rejected by the \isa{Haskell}
- compiler.
- To suppress this additional instance, use
- \isa{code{\isacharunderscore}instance}:%
+\noindent The code generator would produce an additional instance,
+ which of course is rejected by the \isa{Haskell} compiler. To
+ suppress this additional instance, use \isa{code{\isacharunderscore}instance}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -605,8 +602,7 @@
%
\begin{isamarkuptext}%
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}
- command:%
+ target language; this is accomplished using the \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -629,9 +625,10 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent Such named \isa{include}s are then prepended to every generated code.
- Inspect such code in order to find out how \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves
- with respect to a particular target language.%
+\noindent Such named \isa{include}s are then prepended to every
+ generated code. Inspect such code in order to find out how
+ \hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} behaves with respect to a particular
+ target language.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Aug 17 16:38:45 2010 +0200
@@ -141,7 +141,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
\hspace*{0pt} ~val empty :~'a queue\\
@@ -149,10 +150,12 @@
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
\hspace*{0pt}\\
--- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Aug 17 16:38:45 2010 +0200
@@ -22,24 +22,188 @@
}
\isamarkuptrue%
%
-\isamarkupsubsection{Datatypes \label{sec:datatypes}%
+\begin{isamarkuptext}%
+Code generation by shallow embedding (cf.~\secref{sec:principle})
+ allows to choose code equations and datatype constructors freely,
+ given that some very basic syntactic properties are met; this
+ flexibility opens up mechanisms for refinement which allow to extend
+ the scope and quality of generated code dramatically.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Program refinement%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Conceptually, any datatype is spanned by a set of
- \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
- \isa{{\isasymtau}}. The HOL datatype package by default registers any new
- datatype in the table of datatypes, which may be inspected using the
- \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
-
- In some cases, it is appropriate to alter or extend this table. As
- an example, we will develop an alternative representation of the
- queue example given in \secref{sec:queue_example}. The amortised
- representation is convenient for generating code but exposes its
- \qt{implementation} details, which may be cumbersome when proving
- theorems about it. Therefore, here is a simple, straightforward
- representation of queues:%
+Program refinement works by choosing appropriate code equations
+ explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ numbers:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{fun}\isamarkupfalse%
+\ fib\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The runtime of the corresponding code grows exponential due
+ to two recursive calls:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc Zero{\char95}nat) = Suc Zero{\char95}nat;\\
+\hspace*{0pt}fib (Suc (Suc n)) = plus{\char95}nat (fib n) (fib (Suc n));%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent A more efficient implementation would use dynamic
+ programming, e.g.~sharing of common intermediate results between
+ recursive calls. This idea is expressed by an auxiliary operation
+ which computes a Fibonacci number and its successor simultaneously:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{definition}\isamarkupfalse%
+\ fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymtimes}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ n\ {\isacharequal}\ {\isacharparenleft}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharcomma}\ fib\ n{\isacharparenright}{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This operation can be implemented by recursion using
+ dynamic programming:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib{\isacharunderscore}step\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}let\ {\isacharparenleft}m{\isacharcomma}\ q{\isacharparenright}\ {\isacharequal}\ fib{\isacharunderscore}step\ n\ in\ {\isacharparenleft}m\ {\isacharplus}\ q{\isacharcomma}\ m{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent What remains is to implement \isa{fib} by \isa{fib{\isacharunderscore}step} as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ fst\ {\isacharparenleft}fib{\isacharunderscore}step\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ fib{\isacharunderscore}step{\isacharunderscore}def{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent The resulting code shows only linear growth of runtime:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}fib{\char95}step ::~Nat -> (Nat,~Nat);\\
+\hspace*{0pt}fib{\char95}step (Suc n) = let {\char123}\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~~~(m,~q) = fib{\char95}step n;\\
+\hspace*{0pt} ~~~~~~~~~~~~~~~~~~{\char125}~in (plus{\char95}nat m q,~m);\\
+\hspace*{0pt}fib{\char95}step Zero{\char95}nat = (Suc Zero{\char95}nat,~Zero{\char95}nat);\\
+\hspace*{0pt}\\
+\hspace*{0pt}fib ::~Nat -> Nat;\\
+\hspace*{0pt}fib (Suc n) = fst (fib{\char95}step n);\\
+\hspace*{0pt}fib Zero{\char95}nat = Zero{\char95}nat;%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isamarkupsubsection{Datatype refinement%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Selecting specific code equations \emph{and} datatype constructors
+ leads to datatype refinement. As an example, we will develop an
+ alternative representation of the queue example given in
+ \secref{sec:queue_example}. The amortised representation is
+ convenient for generating code but exposes its \qt{implementation}
+ details, which may be cumbersome when proving theorems about it.
+ Therefore, here is a simple, straightforward representation of
+ queues:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -98,7 +262,16 @@
\noindent Here we define a \qt{constructor} \isa{AQueue} which
is defined in terms of \isa{Queue} and interprets its arguments
according to what the \emph{content} of an amortised queue is supposed
- to be. Equipped with this, we are able to prove the following equations
+ to be.
+
+ The prerequisite for datatype constructors is only syntactical: a
+ constructor must be of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
+ \isa{{\isasymtau}}; then \isa{{\isasymkappa}} is its corresponding datatype. The
+ HOL datatype package by default registers any new datatype with its
+ constructors, but this may be changed using \hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}; the currently chosen constructors can be inspected
+ using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
+
+ Equipped with this, we are able to prove the following equations
for our primitive queue operations which \qt{implement} the simple
queues in an amortised fashion:%
\end{isamarkuptext}%
@@ -178,7 +351,8 @@
\isatypewriter%
\noindent%
\hspace*{0pt}structure Example :~sig\\
-\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
+\hspace*{0pt} ~val id :~'a -> 'a\\
+\hspace*{0pt} ~val fold :~('a -> 'b -> 'b) -> 'a list -> 'b -> 'b\\
\hspace*{0pt} ~val rev :~'a list -> 'a list\\
\hspace*{0pt} ~val null :~'a list -> bool\\
\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
@@ -187,10 +361,12 @@
\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
\hspace*{0pt}end = struct\\
\hspace*{0pt}\\
-\hspace*{0pt}fun foldl f a [] = a\\
-\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
+\hspace*{0pt}fun id x = (fn xa => xa) x;\\
\hspace*{0pt}\\
-\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
+\hspace*{0pt}fun fold f [] = id\\
+\hspace*{0pt} ~| fold f (x ::~xs) = fold f xs o f x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}fun rev xs = fold (fn a => fn b => a ::~b) xs [];\\
\hspace*{0pt}\\
\hspace*{0pt}fun null [] = true\\
\hspace*{0pt} ~| null (x ::~xs) = false;\\
@@ -218,28 +394,23 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent From this example, it can be glimpsed that using own
- constructor sets is a little delicate since it changes the set of
- valid patterns for values of that type. Without going into much
- detail, here some practical hints:
-
- \begin{itemize}
-
- \item When changing the constructor set for datatypes, take care
- to provide alternative equations for the \isa{case} combinator.
+The same techniques can also be applied to types which are not
+ specified as datatypes, e.g.~type \isa{int} is originally specified
+ as quotient type by means of \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}, but for code
+ generation constants allowing construction of binary numeral values
+ are used as constructors for \isa{int}.
- \item Values in the target language need not to be normalised --
- different values in the target language may represent the same
- value in the logic.
-
- \item Usually, a good methodology to deal with the subtleties of
- pattern matching is to see the type as an abstract type: provide
- a set of operations which operate on the concrete representation
- of the type, and derive further operations by combinations of
- these primitive ones, without relying on a particular
- representation.
-
- \end{itemize}%
+ This approach however fails if the representation of a type demands
+ invariants; this issue is discussed in the next section.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Datatype refinement involving invariants%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/Codegen/Thy/examples/example.ML Tue Aug 17 16:38:45 2010 +0200
@@ -1,5 +1,6 @@
structure Example : sig
- val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
+ val id : 'a -> 'a
+ val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val rev : 'a list -> 'a list
datatype 'a queue = AQueue of 'a list * 'a list
val empty : 'a queue
@@ -7,10 +8,12 @@
val enqueue : 'a -> 'a queue -> 'a queue
end = struct
-fun foldl f a [] = a
- | foldl f a (x :: xs) = foldl f (f a x) xs;
+fun id x = (fn xa => xa) x;
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
+fun fold f [] = id
+ | fold f (x :: xs) = fold f xs o f x;
+
+fun rev xs = fold (fn a => fn b => a :: b) xs [];
datatype 'a queue = AQueue of 'a list * 'a list;
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 16:38:45 2010 +0200
@@ -1018,7 +1018,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
declaration.
\item @{attribute (HOL) code} explicitly selects (or with option
- ``@{text "del"}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``@{text "del"}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants @{text "code abstype"} and
+ @{text "code abstract"} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item @{command (HOL) "code_abort"} declares constants which are not
required to have a definition by means of code equations; if
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 15:54:04 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 16:38:45 2010 +0200
@@ -1034,7 +1034,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
declaration.
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
- ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+ \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
required to have a definition by means of code equations; if
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 15:54:04 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 16:38:45 2010 +0200
@@ -8,9 +8,7 @@
signature ATP_SYSTEMS =
sig
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -39,9 +37,9 @@
(* prover configuration *)
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -72,6 +70,10 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
+ | string_for_failure OldVampire =
+ "Isabelle requires a more recent version of Vampire. To install it, follow \
+ \the instructions from the Sledgehammer manual (\"isabelle doc\
+ \ sledgehammer\")."
| string_for_failure NoPerl = "Perl" ^ missing_message_tail
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
@@ -143,6 +145,7 @@
max_new_relevant_facts_per_iter = 60 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
+
val e = ("e", e_config)
@@ -169,8 +172,10 @@
max_new_relevant_facts_per_iter = 35 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
+
val spass = ("spass", spass_config)
+
(* Vampire *)
val vampire_config : prover_config =
@@ -189,12 +194,15 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found")],
+ (OutOfResources, "Refutation not found"),
+ (OldVampire, "input_file")],
max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
+
val vampire = ("vampire", vampire_config)
+
(* Remote prover invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -236,13 +244,15 @@
explicit_forall = true}
val remote_name = prefix "remote_"
-
fun remote_prover (name, config) atp_prefix =
(remote_name name, remote_config atp_prefix config)
val remote_e = remote_prover e "EP---"
val remote_vampire = remote_prover vampire "Vampire---9"
+
+(* Setup *)
+
fun is_installed ({exec, required_execs, ...} : prover_config) =
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 17 15:54:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 17 16:38:45 2010 +0200
@@ -206,27 +206,37 @@
(* generic TPTP-based provers *)
-fun prover_fun name
+fun prover_fun atp_name
{exec, required_execs, arguments, proof_delims, known_failures,
max_new_relevant_facts_per_iter, prefers_theory_relevant,
explicit_forall}
- ({debug, overlord, full_types, explicit_apply, relevance_threshold,
- relevance_convergence, theory_relevant, defs_relevant, isar_proof,
- isar_shrink_factor, timeout, ...} : params)
+ ({debug, verbose, overlord, full_types, explicit_apply,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
let
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
+
+ fun print s = (priority s; if debug then tracing s else ())
+ fun print_v f = () |> verbose ? print o f
+ fun print_d f = () |> debug ? print o f
+
val the_axioms =
case axioms of
SOME axioms => axioms
- | NONE => relevant_facts full_types relevance_threshold
- relevance_convergence defs_relevant
- max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
+ | NONE =>
+ (print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
+ ".");
+ relevant_facts full_types relevance_threshold relevance_convergence
+ defs_relevant max_new_relevant_facts_per_iter
+ (the_default prefers_theory_relevant theory_relevant)
+ relevance_override goal hyp_ts concl_t
+ |> tap ((fn n => print_v (fn () =>
+ "Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
+ " for " ^ quote atp_name ^ ".")) o length))
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -235,7 +245,7 @@
fun prob_pathname nr =
let
val probfile =
- Path.basic ((if overlord then "prob_" ^ name
+ Path.basic ((if overlord then "prob_" ^ atp_name
else the_problem_prefix ^ serial_string ())
^ "_" ^ string_of_int nr)
in
@@ -290,6 +300,8 @@
extract_proof_and_outcome complete res_code proof_delims
known_failures output
in (output, msecs, proof, outcome) end
+ val _ = print_d (fn () => "Preparing problem for " ^
+ quote atp_name ^ "...")
val readable_names = debug andalso overlord
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
@@ -298,6 +310,7 @@
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
+ val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
val result =
do_run false
|> (fn (_, msecs0, _, SOME _) =>
@@ -343,15 +356,16 @@
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
- relevance_override minimize_command proof_state name =
+ relevance_override minimize_command proof_state
+ atp_name =
let
val thy = Proof.theory_of proof_state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val prover = get_prover_fun thy name
+ val prover = get_prover_fun thy atp_name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
- "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
in
Async_Manager.launch das_Tool verbose birth_time death_time desc
@@ -361,7 +375,7 @@
{subgoal = i, goal = (ctxt, (facts, goal)),
relevance_override = relevance_override, axioms = NONE}
in
- prover params (minimize_command name) problem |> #message
+ prover params (minimize_command atp_name) problem |> #message
handle ERROR message => "Error: " ^ message ^ "\n"
| exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
"\n"
--- a/src/Provers/quantifier1.ML Tue Aug 17 15:54:04 2010 +0200
+++ b/src/Provers/quantifier1.ML Tue Aug 17 16:38:45 2010 +0200
@@ -17,7 +17,7 @@
And analogously for t=x, but the eqn is not turned around!
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
- "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
+ "!x. x=t --> P(x)" is covered by the congruence rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
As must be "? x. t=x & P(x)".
@@ -26,7 +26,7 @@
Gries etc call this the "1 point rules"
The above also works for !x1..xn. and ?x1..xn by moving the defined
-qunatifier inside first, but not for nested bounded quantifiers.
+quantifier inside first, but not for nested bounded quantifiers.
For set comprehensions the basic permutations
... & x = t & ... -> x = t & (... & ...)
@@ -113,8 +113,13 @@
in exqu [] end;
fun prove_conv tac thy tu =
- Goal.prove (ProofContext.init_global thy) [] [] (Logic.mk_equals tu)
- (K (rtac iff_reflection 1 THEN tac));
+ let val ctxt = ProofContext.init_global thy;
+ val eq_tu = Logic.mk_equals tu;
+ val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
+ val thm = Goal.prove ctxt' [] [] fixed_goal
+ (K (rtac iff_reflection 1 THEN tac));
+ val [gen_thm] = Variable.export ctxt' ctxt [thm];
+ in gen_thm end;
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)