--- a/doc-src/Codegen/IsaMakefile Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile Wed Aug 18 12:05:44 2010 +0200
@@ -24,7 +24,7 @@
Thy: $(THY)
$(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
- @$(USEDIR) -m no_brackets -m iff HOL Thy
+ @$(USEDIR) -m no_brackets -m iff HOL-Library Thy
@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
Thy/document/pdfsetup.sty Thy/document/session.tex
--- a/doc-src/Codegen/Thy/Adaptation.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Aug 18 12:05:44 2010 +0200
@@ -194,12 +194,12 @@
(SML "true" and "false" and "_ andalso _")
text {*
- \noindent The @{command code_type} command takes a type constructor
+ \noindent The @{command_def 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
+ @{command_def 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.
*}
@@ -226,7 +226,7 @@
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:
+ @{command_def "code_reserved"} command:
*}
code_reserved %quote "\<SML>" bool true false andalso
@@ -274,7 +274,7 @@
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}
+ @{command_def code_class}) and its operation @{const HOL.eq}
*}
code_class %quotett eq
@@ -307,7 +307,7 @@
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"}:
+ suppress this additional instance, use @{command_def "code_instance"}:
*}
code_instance %quotett bar :: eq
@@ -318,7 +318,7 @@
text {*
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command
+ target language; this is accomplished using the @{command_def
"code_include"} command:
*}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/Evaluation.thy Wed Aug 18 12:05:44 2010 +0200
@@ -0,0 +1,104 @@
+theory Evaluation
+imports Setup
+begin
+
+section {* Evaluation *}
+
+text {* Introduction *}
+
+
+subsection {* Evaluation techniques *}
+
+text {* simplifier *}
+
+text {* nbe *}
+
+text {* eval target: SML standalone vs. Isabelle/SML, example, soundness *}
+
+
+subsection {* Dynamic evaluation *}
+
+text {* value (three variants) *}
+
+text {* methods (three variants) *}
+
+text {* corresponding ML interfaces *}
+
+
+subsection {* Static evaluation *}
+
+text {* code_simp, nbe (tbd), Eval (tbd, in simple fashion) *}
+
+text {* hand-written: code antiquotation *}
+
+
+subsection {* Hybrid techniques *}
+
+text {* code reflect runtime *}
+
+text {* code reflect external *}
+
+
+text {* FIXME here the old sections follow *}
+
+subsection {* Evaluation oracle *}
+
+text {*
+ Code generation may also be used to \emph{evaluate} expressions
+ (using @{text SML} as target language of course).
+ For instance, the @{command_def value} reduces an expression to a
+ normal form with respect to the underlying code equations:
+*}
+
+value %quote "42 / (12 :: rat)"
+
+text {*
+ \noindent will display @{term "7 / (2 :: rat)"}.
+
+ The @{method eval} method tries to reduce a goal by code generation to @{term True}
+ and solves it in that case, but fails otherwise:
+*}
+
+lemma %quote "42 / (12 :: rat) = 7 / 2"
+ by %quote eval
+
+text {*
+ \noindent The soundness of the @{method eval} method depends crucially
+ on the correctness of the code generator; this is one of the reasons
+ why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
+*}
+
+
+subsubsection {* Code antiquotation *}
+
+text {*
+ In scenarios involving techniques like reflection it is quite common
+ that code generated from a theory forms the basis for implementing
+ a proof procedure in @{text SML}. To facilitate interfacing of generated code
+ with system code, the code generator provides a @{text code} antiquotation:
+*}
+
+datatype %quote form = T | F | And form form | Or form form (*<*)
+
+(*>*) ML %quotett {*
+ fun eval_form @{code T} = true
+ | eval_form @{code F} = false
+ | eval_form (@{code And} (p, q)) =
+ eval_form p andalso eval_form q
+ | eval_form (@{code Or} (p, q)) =
+ eval_form p orelse eval_form q;
+*}
+
+text {*
+ \noindent @{text code} takes as argument the name of a constant; after the
+ whole @{text SML} is read, the necessary code is generated transparently
+ and the corresponding constant names are inserted. This technique also
+ allows to use pattern matching on constructors stemming from compiled
+ @{text "datatypes"}.
+
+ For a less simplistic example, theory @{theory Ferrack} is
+ a good reference.
+*}
+
+
+end
--- a/doc-src/Codegen/Thy/Foundations.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Wed Aug 18 12:05:44 2010 +0200
@@ -121,9 +121,10 @@
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
- using the @{command print_codeproc} command. @{command code_thms}
- (see \secref{sec:equations}) provides a convenient mechanism to
- inspect the impact of a preprocessor setup on code equations.
+ using the @{command_def print_codeproc} command. @{command_def
+ code_thms} (see \secref{sec:equations}) provides a convenient
+ mechanism to inspect the impact of a preprocessor setup on code
+ equations.
\begin{warn}
Attribute @{attribute code_unfold} also applies to the
@@ -175,9 +176,8 @@
equations (before preprocessing) and code equations (after
preprocessing).
- The first can be listed (among other data) using the @{command
- print_codesetup} command (later on in \secref{sec:refinement}
- it will be shown how these code equations can be changed).
+ The first can be listed (among other data) using the @{command_def
+ print_codesetup} command.
The code equations after preprocessing are already are blueprint of
the generated program and can be inspected using the @{command
@@ -190,7 +190,7 @@
\noindent This prints a table with the code equations for @{const
dequeue}, including \emph{all} code equations those equations depend
on recursively. These dependencies themselves can be visualized using
- the @{command code_deps} command.
+ the @{command_def code_deps} command.
*}
@@ -280,7 +280,7 @@
of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
- explicitly, use @{command "code_abort"}:
+ explicitly, use @{command_def "code_abort"}:
*}
code_abort %quote empty_queue
--- a/doc-src/Codegen/Thy/Further.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Wed Aug 18 12:05:44 2010 +0200
@@ -75,7 +75,7 @@
end %quote
text {*
- After an interpretation of this locale (say, @{command
+ After an interpretation of this locale (say, @{command_def
interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f ::
'a \<Rightarrow> 'a). f ^^ n)"}), one would expect to have a constant @{text
"fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
@@ -126,91 +126,27 @@
*}
-subsection {* Evaluation oracle *}
-
-text {*
- Code generation may also be used to \emph{evaluate} expressions
- (using @{text SML} as target language of course).
- For instance, the @{command value} reduces an expression to a
- normal form with respect to the underlying code equations:
-*}
-
-value %quote "42 / (12 :: rat)"
-
-text {*
- \noindent will display @{term "7 / (2 :: rat)"}.
-
- The @{method eval} method tries to reduce a goal by code generation to @{term True}
- and solves it in that case, but fails otherwise:
-*}
-
-lemma %quote "42 / (12 :: rat) = 7 / 2"
- by %quote eval
-
-text {*
- \noindent The soundness of the @{method eval} method depends crucially
- on the correctness of the code generator; this is one of the reasons
- why you should not use adaptation (see \secref{sec:adaptation}) frivolously.
-*}
-
-
-subsection {* Building evaluators *}
-
-text {*
- FIXME
-*}
-
-subsubsection {* Code antiquotation *}
-
-text {*
- In scenarios involving techniques like reflection it is quite common
- that code generated from a theory forms the basis for implementing
- a proof procedure in @{text SML}. To facilitate interfacing of generated code
- with system code, the code generator provides a @{text code} antiquotation:
-*}
-
-datatype %quote form = T | F | And form form | Or form form (*<*)
-
-(*>*) ML %quotett {*
- fun eval_form @{code T} = true
- | eval_form @{code F} = false
- | eval_form (@{code And} (p, q)) =
- eval_form p andalso eval_form q
- | eval_form (@{code Or} (p, q)) =
- eval_form p orelse eval_form q;
-*}
-
-text {*
- \noindent @{text code} takes as argument the name of a constant; after the
- whole @{text SML} is read, the necessary code is generated transparently
- and the corresponding constant names are inserted. This technique also
- allows to use pattern matching on constructors stemming from compiled
- @{text "datatypes"}.
-
- For a less simplistic example, theory @{theory Ferrack} is
- a good reference.
-*}
-
-
subsection {* ML system interfaces \label{sec:ml} *}
text {*
- Since the code generator framework not only aims to provide
- a nice Isar interface but also to form a base for
- code-generation-based applications, here a short
- description of the most important ML interfaces.
+ Since the code generator framework not only aims to provide a nice
+ Isar interface but also to form a base for code-generation-based
+ applications, here a short description of the most fundamental ML
+ interfaces.
*}
subsubsection {* Managing executable content *}
text %mlref {*
\begin{mldecls}
+ @{index_ML Code.read_const: "theory -> string -> string"} \\
@{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
@{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
@{index_ML Code_Preproc.map_pre: "(simpset -> simpset) -> theory -> theory"} \\
@{index_ML Code_Preproc.map_post: "(simpset -> simpset) -> theory -> theory"} \\
- @{index_ML Code_Preproc.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
- -> theory -> theory"} \\
+ @{index_ML Code_Preproc.add_functrans: "
+ string * (theory -> (thm * bool) list -> (thm * bool) list option)
+ -> theory -> theory"} \\
@{index_ML Code_Preproc.del_functrans: "string -> theory -> theory"} \\
@{index_ML Code.add_datatype: "(string * typ) list -> theory -> theory"} \\
@{index_ML Code.get_type: "theory -> string
@@ -220,6 +156,9 @@
\begin{description}
+ \item @{ML Code.read_const}~@{text thy}~@{text s}
+ reads a constant as a concrete term expression @{text s}.
+
\item @{ML Code.add_eqn}~@{text "thm"}~@{text "thy"} adds function
theorem @{text "thm"} to executable content.
@@ -252,21 +191,6 @@
\end{description}
*}
-subsubsection {* Auxiliary *}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML Code.read_const: "theory -> string -> string"}
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML Code.read_const}~@{text thy}~@{text s}
- reads a constant as a concrete term expression @{text s}.
-
- \end{description}
-
-*}
subsubsection {* Data depending on the theory's executable content *}
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Wed Aug 18 12:05:44 2010 +0200
@@ -16,7 +16,7 @@
section {* Inductive Predicates \label{sec:inductive} *}
text {*
- The @{text predicate_compiler} is an extension of the code generator
+ The @{text "predicate compiler"} is an extension of the code generator
which turns inductive specifications into equational ones, from
which in turn executable code can be generated. The mechanisms of
this compiler are described in detail in
--- a/doc-src/Codegen/Thy/Introduction.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Aug 18 12:05:44 2010 +0200
@@ -34,11 +34,12 @@
subsection {* A quick start with the Isabelle/HOL toolbox \label{sec:queue_example} *}
text {*
- In a HOL theory, the @{command datatype} and @{command
- definition}/@{command primrec}/@{command fun} declarations form the
- core of a functional programming language. By default equational
- theorems stemming from those are used for generated code, therefore
- \qt{naive} code generation can proceed without further ado.
+ In a HOL theory, the @{command_def datatype} and @{command_def
+ definition}/@{command_def primrec}/@{command_def fun} declarations
+ form the core of a functional programming language. By default
+ equational theorems stemming from those are used for generated code,
+ therefore \qt{naive} code generation can proceed without further
+ ado.
For example, here a simple \qt{implementation} of amortised queues:
*}
@@ -71,12 +72,12 @@
text %quote {*@{code_stmts empty enqueue dequeue (SML)}*}
text {*
- \noindent The @{command export_code} command takes a space-separated
- list of constants for which code shall be generated; anything else
- needed for those is added implicitly. Then follows a target
- language identifier and a freely chosen module name. A file name
- denotes the destination to store the generated code. Note that the
- semantics of the destination depends on the target language: for
+ \noindent The @{command_def export_code} command takes a
+ space-separated list of constants for which code shall be generated;
+ anything else needed for those is added implicitly. Then follows a
+ target language identifier and a freely chosen module name. A file
+ name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
@{text SML} and @{text OCaml} it denotes a \emph{file}, for @{text
Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension @{text ".hs"}) is written:
--- a/doc-src/Codegen/Thy/ROOT.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/ROOT.ML Wed Aug 18 12:05:44 2010 +0200
@@ -5,5 +5,6 @@
use_thy "Foundations";
use_thy "Refinement";
use_thy "Inductive_Predicate";
+use_thy "Evaluation";
use_thy "Adaptation";
use_thy "Further";
--- a/doc-src/Codegen/Thy/Refinement.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Aug 18 12:05:44 2010 +0200
@@ -116,7 +116,7 @@
"{\<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
+ constructors, but this may be changed using @{command_def
code_datatype}; the currently chosen constructors can be inspected
using the @{command print_codesetup} command.
@@ -158,7 +158,7 @@
text {*
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
+ as quotient type by means of @{command_def typedef}, but for code
generation constants allowing construction of binary numeral values
are used as constructors for @{typ int}.
@@ -170,7 +170,95 @@
subsection {* Datatype refinement involving invariants *}
text {*
- FIXME
+ Datatype representation involving invariants require a dedicated
+ setup for the type and its primitive operations. As a running
+ example, we implement a type @{text "'a dlist"} of list consisting
+ of distinct elements.
+
+ The first step is to decide on which representation the abstract
+ type (in our example @{text "'a dlist"}) should be implemented.
+ Here we choose @{text "'a list"}. Then a conversion from the concrete
+ type to the abstract type must be specified, here:
+*}
+
+text %quote {*
+ @{term_type Dlist}
+*}
+
+text {*
+ \noindent Next follows the specification of a suitable \emph{projection},
+ i.e.~a conversion from abstract to concrete type:
+*}
+
+text %quote {*
+ @{term_type list_of_dlist}
+*}
+
+text {*
+ \noindent This projection must be specified such that the following
+ \emph{abstract datatype certificate} can be proven:
+*}
+
+lemma %quote [code abstype]:
+ "Dlist (list_of_dlist dxs) = dxs"
+ by (fact Dlist_list_of_dlist)
+
+text {*
+ \noindent Note that so far the invariant on representations
+ (@{term_type distinct}) has never been mentioned explicitly:
+ the invariant is only referred to implicitly: all values in
+ set @{term "{xs. list_of_dlist (Dlist xs) = xs}"} are invariant,
+ and in our example this is exactly @{term "{xs. distinct xs}"}.
+
+ The primitive operations on @{typ "'a dlist"} are specified
+ indirectly using the projection @{const list_of_dlist}. For
+ the empty @{text "dlist"}, @{const Dlist.empty}, we finally want
+ the code equation
+*}
+
+text %quote {*
+ @{term "Dlist.empty = Dlist []"}
+*}
+
+text {*
+ \noindent This we have to prove indirectly as follows:
+*}
+
+lemma %quote [code abstract]:
+ "list_of_dlist Dlist.empty = []"
+ by (fact list_of_dlist_empty)
+
+text {*
+ \noindent This equation logically encodes both the desired code
+ equation and that the expression @{const Dlist} is applied to obeys
+ the implicit invariant. Equations for insertion and removal are
+ similar:
+*}
+
+lemma %quote [code abstract]:
+ "list_of_dlist (Dlist.insert x dxs) = List.insert x (list_of_dlist dxs)"
+ by (fact list_of_dlist_insert)
+
+lemma %quote [code abstract]:
+ "list_of_dlist (Dlist.remove x dxs) = remove1 x (list_of_dlist dxs)"
+ by (fact list_of_dlist_remove)
+
+text {*
+ \noindent Then the corresponding code is as follows:
+*}
+
+text %quote {*
+ @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
+*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
+
+text {*
+ Typical data structures implemented by representations involving
+ invariants are available in the library, e.g.~theories @{theory
+ Fset} and @{theory Mapping} specify sets (type @{typ "'a fset"}) and
+ key-value-mappings (type @{typ "('a, 'b) mapping"}) respectively;
+ these can be implemented by distinct lists as presented here as
+ example (theory @{theory Dlist}) and red-black-trees respectively
+ (theory @{theory RBT}).
*}
end
--- a/doc-src/Codegen/Thy/Setup.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Wed Aug 18 12:05:44 2010 +0200
@@ -1,14 +1,30 @@
theory Setup
-imports Complex_Main More_List
+imports Complex_Main More_List RBT Dlist Mapping
uses
"../../antiquote_setup.ML"
"../../more_antiquote.ML"
begin
ML {* no_document use_thys
- ["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
+ ["Efficient_Nat", "Code_Char_chr", "Product_ord",
+ "~~/src/HOL/Imperative_HOL/Imperative_HOL",
"~~/src/HOL/Decision_Procs/Ferrack"] *}
+setup {*
+let
+ val typ = Simple_Syntax.read_typ;
+ val typeT = Syntax.typeT;
+ val spropT = Syntax.spropT;
+in
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
+ #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+end
+*}
+
setup {* Code_Target.set_default_code_width 74 *}
ML_command {* Unsynchronized.reset unique_names *}
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 12:05:44 2010 +0200
@@ -302,12 +302,12 @@
\endisadelimquotett
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} command takes a type constructor
+\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\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
+ \indexdef{}{command}{code\_const}\hypertarget{command.code-const}{\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}%
@@ -416,7 +416,7 @@
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:%
+ \indexdef{}{command}{code\_reserved}\hypertarget{command.code-reserved}{\hyperlink{command.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -501,7 +501,7 @@
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}%
+ \indexdef{}{command}{code\_class}\hypertarget{command.code-class}{\hyperlink{command.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}}) and its operation \isa{eq{\isacharunderscore}class{\isachardot}eq}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -577,7 +577,7 @@
\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}:%
+ suppress this additional instance, use \indexdef{}{command}{code\_instance}\hypertarget{command.code-instance}{\hyperlink{command.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -602,7 +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 \indexdef{}{command}{code\_include}\hypertarget{command.code-include}{\hyperlink{command.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} command:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Foundations.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Wed Aug 18 12:05:44 2010 +0200
@@ -182,9 +182,9 @@
\secref{eff_nat}) uses this interface.
\noindent The current setup of the preprocessor may be inspected
- using the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command. \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}
- (see \secref{sec:equations}) provides a convenient mechanism to
- inspect the impact of a preprocessor setup on code equations.
+ using the \indexdef{}{command}{print\_codeproc}\hypertarget{command.print-codeproc}{\hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}} command. \indexdef{}{command}{code\_thms}\hypertarget{command.code-thms}{\hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}} (see \secref{sec:equations}) provides a convenient
+ mechanism to inspect the impact of a preprocessor setup on code
+ equations.
\begin{warn}
Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
@@ -275,8 +275,7 @@
equations (before preprocessing) and code equations (after
preprocessing).
- The first can be listed (among other data) using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command (later on in \secref{sec:refinement}
- it will be shown how these code equations can be changed).
+ The first can be listed (among other data) using the \indexdef{}{command}{print\_codesetup}\hypertarget{command.print-codesetup}{\hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}} command.
The code equations after preprocessing are already are blueprint of
the generated program and can be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
@@ -300,7 +299,7 @@
\begin{isamarkuptext}%
\noindent This prints a table with the code equations for \isa{dequeue}, including \emph{all} code equations those equations depend
on recursively. These dependencies themselves can be visualized using
- the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command.%
+ the \indexdef{}{command}{code\_deps}\hypertarget{command.code-deps}{\hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}} command.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -503,7 +502,7 @@
of as function definitions which always fail,
since there is never a successful pattern match on the left hand
side. In order to categorise a constant into that category
- explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
+ explicitly, use \indexdef{}{command}{code\_abort}\hypertarget{command.code-abort}{\hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 12:05:44 2010 +0200
@@ -145,7 +145,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-After an interpretation of this locale (say, \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
+After an interpretation of this locale (say, \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} \isa{fun{\isacharunderscore}power{\isacharcolon}} \isa{{\isachardoublequote}power\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}), one would expect to have a constant \isa{fun{\isacharunderscore}power{\isachardot}powers\ {\isacharcolon}{\isacharcolon}\ nat\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} for which code
can be generated. But this not the case: internally, the term
\isa{fun{\isacharunderscore}power{\isachardot}powers} is an abbreviation for the foundational
term \isa{{\isachardoublequote}power{\isachardot}powers\ {\isacharparenleft}{\isasymlambda}n\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}{\isachardot}\ f\ {\isacharcircum}{\isacharcircum}\ n{\isacharparenright}{\isachardoublequote}}
@@ -246,156 +246,15 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Evaluation oracle%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Code generation may also be used to \emph{evaluate} expressions
- (using \isa{SML} as target language of course).
- For instance, the \hyperlink{command.value}{\mbox{\isa{\isacommand{value}}}} reduces an expression to a
- normal form with respect to the underlying code equations:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{value}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}{\isachardoublequoteclose}%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent will display \isa{{\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}}.
-
- The \hyperlink{method.eval}{\mbox{\isa{eval}}} method tries to reduce a goal by code generation to \isa{True}
- and solves it in that case, but fails otherwise:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isadigit{4}}{\isadigit{2}}\ {\isacharslash}\ {\isacharparenleft}{\isadigit{1}}{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ rat{\isacharparenright}\ {\isacharequal}\ {\isadigit{7}}\ {\isacharslash}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{by}\isamarkupfalse%
-\ eval%
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\begin{isamarkuptext}%
-\noindent The soundness of the \hyperlink{method.eval}{\mbox{\isa{eval}}} method depends crucially
- on the correctness of the code generator; this is one of the reasons
- why you should not use adaptation (see \secref{sec:adaptation}) frivolously.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Building evaluators%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Code antiquotation%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In scenarios involving techniques like reflection it is quite common
- that code generated from a theory forms the basis for implementing
- a proof procedure in \isa{SML}. To facilitate interfacing of generated code
- with system code, the code generator provides a \isa{code} antiquotation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isatagquote
-\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{ML}\isamarkupfalse%
-\ {\isacharverbatimopen}\isanewline
-\ \ fun\ eval{\isacharunderscore}form\ %
-\isaantiq
-code\ T%
-\endisaantiq
-\ {\isacharequal}\ true\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ %
-\isaantiq
-code\ F%
-\endisaantiq
-\ {\isacharequal}\ false\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
-\isaantiq
-code\ And%
-\endisaantiq
-\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ andalso\ eval{\isacharunderscore}form\ q\isanewline
-\ \ \ \ {\isacharbar}\ eval{\isacharunderscore}form\ {\isacharparenleft}%
-\isaantiq
-code\ Or%
-\endisaantiq
-\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
-\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
-{\isacharverbatimclose}%
-\endisatagquotett
-{\isafoldquotett}%
-%
-\isadelimquotett
-%
-\endisadelimquotett
-%
-\begin{isamarkuptext}%
-\noindent \isa{code} takes as argument the name of a constant; after the
- whole \isa{SML} is read, the necessary code is generated transparently
- and the corresponding constant names are inserted. This technique also
- allows to use pattern matching on constructors stemming from compiled
- \isa{datatypes}.
-
- For a less simplistic example, theory \hyperlink{theory.Ferrack}{\mbox{\isa{Ferrack}}} is
- a good reference.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsubsection{ML system interfaces \label{sec:ml}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Since the code generator framework not only aims to provide
- a nice Isar interface but also to form a base for
- code-generation-based applications, here a short
- description of the most important ML interfaces.%
+Since the code generator framework not only aims to provide a nice
+ Isar interface but also to form a base for code-generation-based
+ applications, here a short description of the most fundamental ML
+ interfaces.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -411,12 +270,14 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
+ \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
\indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
- \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
-\verb| -> theory -> theory| \\
+ \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: |\isasep\isanewline%
+\verb| string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
+\verb| -> theory -> theory| \\
\indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
\indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
\indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
@@ -426,6 +287,9 @@
\begin{description}
+ \item \verb|Code.read_const|~\isa{thy}~\isa{s}
+ reads a constant as a concrete term expression \isa{s}.
+
\item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
theorem \isa{thm} to executable content.
@@ -466,37 +330,6 @@
%
\endisadelimmlref
%
-\isamarkupsubsubsection{Auxiliary%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
- \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
- \end{mldecls}
-
- \begin{description}
-
- \item \verb|Code.read_const|~\isa{thy}~\isa{s}
- reads a constant as a concrete term expression \isa{s}.
-
- \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
\isamarkupsubsubsection{Data depending on the theory's executable content%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Wed Aug 18 12:05:44 2010 +0200
@@ -37,7 +37,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The \isa{predicate{\isacharunderscore}compiler} is an extension of the code generator
+The \isa{predicate\ compiler} is an extension of the code generator
which turns inductive specifications into equational ones, from
which in turn executable code can be generated. The mechanisms of
this compiler are described in detail in
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 12:05:44 2010 +0200
@@ -55,10 +55,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-In a HOL theory, the \hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}} and \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}/\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}/\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}} declarations form the
- core of a functional programming language. By default equational
- theorems stemming from those are used for generated code, therefore
- \qt{naive} code generation can proceed without further ado.
+In a HOL theory, the \indexdef{}{command}{datatype}\hypertarget{command.datatype}{\hyperlink{command.datatype}{\mbox{\isa{\isacommand{datatype}}}}} and \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}}/\indexdef{}{command}{primrec}\hypertarget{command.primrec}{\hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}}}/\indexdef{}{command}{fun}\hypertarget{command.fun}{\hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}} declarations
+ form the core of a functional programming language. By default
+ equational theorems stemming from those are used for generated code,
+ therefore \qt{naive} code generation can proceed without further
+ ado.
For example, here a simple \qt{implementation} of amortised queues:%
\end{isamarkuptext}%
@@ -184,12 +185,12 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} command takes a space-separated
- list of constants for which code shall be generated; anything else
- needed for those is added implicitly. Then follows a target
- language identifier and a freely chosen module name. A file name
- denotes the destination to store the generated code. Note that the
- semantics of the destination depends on the target language: for
+\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
+ space-separated list of constants for which code shall be generated;
+ anything else needed for those is added implicitly. Then follows a
+ target language identifier and a freely chosen module name. A file
+ name denotes the destination to store the generated code. Note that
+ the semantics of the destination depends on the target language: for
\isa{SML} and \isa{OCaml} it denotes a \emph{file}, for \isa{Haskell} it denotes a \emph{directory} where a file named as the
module name (with extension \isa{{\isachardot}hs}) is written:%
\end{isamarkuptext}%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Aug 18 12:05:44 2010 +0200
@@ -268,7 +268,7 @@
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
+ constructors, but this may be changed using \indexdef{}{command}{code\_datatype}\hypertarget{command.code-datatype}{\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
@@ -396,7 +396,7 @@
\begin{isamarkuptext}%
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
+ as quotient type by means of \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\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}.
@@ -410,7 +410,227 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+Datatype representation involving invariants require a dedicated
+ setup for the type and its primitive operations. As a running
+ example, we implement a type \isa{{\isacharprime}a\ dlist} of list consisting
+ of distinct elements.
+
+ The first step is to decide on which representation the abstract
+ type (in our example \isa{{\isacharprime}a\ dlist}) should be implemented.
+ Here we choose \isa{{\isacharprime}a\ list}. Then a conversion from the concrete
+ type to the abstract type must be specified, here:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{Dlist\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ dlist}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Next follows the specification of a suitable \emph{projection},
+ i.e.~a conversion from abstract to concrete type:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isasymColon}\ {\isacharprime}a\ dlist\ {\isasymRightarrow}\ {\isacharprime}a\ list}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This projection must be specified such that the following
+ \emph{abstract datatype certificate} can be proven:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ abstype{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}Dlist\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}\ {\isacharequal}\ dxs{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ Dlist{\isacharunderscore}list{\isacharunderscore}of{\isacharunderscore}dlist{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Note that so far the invariant on representations
+ (\isa{distinct\ {\isasymColon}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ bool}) has never been mentioned explicitly:
+ the invariant is only referred to implicitly: all values in
+ set \isa{{\isacharbraceleft}xs{\isachardot}\ list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isacharbraceright}} are invariant,
+ and in our example this is exactly \isa{{\isacharbraceleft}xs{\isachardot}\ distinct\ xs{\isacharbraceright}}.
+
+ The primitive operations on \isa{{\isacharprime}a\ dlist} are specified
+ indirectly using the projection \isa{list{\isacharunderscore}of{\isacharunderscore}dlist}. For
+ the empty \isa{dlist}, \isa{Dlist{\isachardot}empty}, we finally want
+ the code equation%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isa{Dlist{\isachardot}empty\ {\isacharequal}\ Dlist\ {\isacharbrackleft}{\isacharbrackright}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This we have to prove indirectly as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ abstract{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}list{\isacharunderscore}of{\isacharunderscore}dlist\ Dlist{\isachardot}empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ list{\isacharunderscore}of{\isacharunderscore}dlist{\isacharunderscore}empty{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This equation logically encodes both the desired code
+ equation and that the expression \isa{Dlist} is applied to obeys
+ the implicit invariant. Equations for insertion and removal are
+ similar:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ abstract{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist{\isachardot}insert\ x\ dxs{\isacharparenright}\ {\isacharequal}\ List{\isachardot}insert\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ list{\isacharunderscore}of{\isacharunderscore}dlist{\isacharunderscore}insert{\isacharparenright}\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\ {\isacharbrackleft}code\ abstract{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}list{\isacharunderscore}of{\isacharunderscore}dlist\ {\isacharparenleft}Dlist{\isachardot}remove\ x\ dxs{\isacharparenright}\ {\isacharequal}\ remove{\isadigit{1}}\ x\ {\isacharparenleft}list{\isacharunderscore}of{\isacharunderscore}dlist\ dxs{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}fact\ list{\isacharunderscore}of{\isacharunderscore}dlist{\isacharunderscore}remove{\isacharparenright}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent Then the corresponding code is as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+%
+\begin{isamarkuptext}%
+\isatypewriter%
+\noindent%
+\hspace*{0pt}module Example where {\char123}\\
+\hspace*{0pt}\\
+\hspace*{0pt}newtype Dlist a = Dlist [a];\\
+\hspace*{0pt}\\
+\hspace*{0pt}empty ::~forall a.~Dlist a;\\
+\hspace*{0pt}empty = Dlist [];\\
+\hspace*{0pt}\\
+\hspace*{0pt}member ::~forall a.~(Eq a) => [a] -> a -> Bool;\\
+\hspace*{0pt}member [] y = False;\\
+\hspace*{0pt}member (x :~xs) y = x == y || member xs y;\\
+\hspace*{0pt}\\
+\hspace*{0pt}inserta ::~forall a.~(Eq a) => a -> [a] -> [a];\\
+\hspace*{0pt}inserta x xs = (if member xs x then xs else x :~xs);\\
+\hspace*{0pt}\\
+\hspace*{0pt}list{\char95}of{\char95}dlist ::~forall a.~Dlist a -> [a];\\
+\hspace*{0pt}list{\char95}of{\char95}dlist (Dlist x) = x;\\
+\hspace*{0pt}\\
+\hspace*{0pt}insert ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
+\hspace*{0pt}insert x dxs = Dlist (inserta x (list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}\\
+\hspace*{0pt}remove1 ::~forall a.~(Eq a) => a -> [a] -> [a];\\
+\hspace*{0pt}remove1 x [] = [];\\
+\hspace*{0pt}remove1 x (y :~xs) = (if x == y then xs else y :~remove1 x xs);\\
+\hspace*{0pt}\\
+\hspace*{0pt}remove ::~forall a.~(Eq a) => a -> Dlist a -> Dlist a;\\
+\hspace*{0pt}remove x dxs = Dlist (remove1 x (list{\char95}of{\char95}dlist dxs));\\
+\hspace*{0pt}\\
+\hspace*{0pt}{\char125}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+Typical data structures implemented by representations involving
+ invariants are available in the library, e.g.~theories \hyperlink{theory.Fset}{\mbox{\isa{Fset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isacharprime}a\ fset}) and
+ key-value-mappings (type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ mapping}) respectively;
+ these can be implemented by distinct lists as presented here as
+ example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively
+ (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/codegen.tex Wed Aug 18 12:04:00 2010 +0200
+++ b/doc-src/Codegen/codegen.tex Wed Aug 18 12:05:44 2010 +0200
@@ -35,6 +35,7 @@
\input{Thy/document/Refinement.tex}
\input{Thy/document/Inductive_Predicate.tex}
\input{Thy/document/Adaptation.tex}
+\input{Thy/document/Evaluation.tex}
\input{Thy/document/Further.tex}
\begingroup
--- a/src/CCL/Set.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/src/CCL/Set.thy Wed Aug 18 12:05:44 2010 +0200
@@ -4,8 +4,6 @@
imports FOL
begin
-global
-
typedecl 'a set
arities set :: ("term") "term"
@@ -46,8 +44,6 @@
"ALL x:A. P" == "CONST Ball(A, %x. P)"
"EX x:A. P" == "CONST Bex(A, %x. P)"
-local
-
axioms
mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)"
set_extension: "A=B <-> (ALL x. x:A <-> x:B)"
--- a/src/CCL/Wfd.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/src/CCL/Wfd.thy Wed Aug 18 12:05:44 2010 +0200
@@ -423,13 +423,13 @@
@{thms canTs} @ @{thms icanTs} @ @{thms applyT2} @ @{thms ncanTs} @ @{thms incanTs} @
@{thms precTs} @ @{thms letrecTs} @ @{thms letT} @ @{thms Subtype_canTs};
-fun bvars (Const("all",_) $ Abs(s,_,t)) l = bvars t (s::l)
+fun bvars (Const(@{const_name all},_) $ Abs(s,_,t)) l = bvars t (s::l)
| bvars _ l = l
-fun get_bno l n (Const("all",_) $ Abs(s,_,t)) = get_bno (s::l) n t
- | get_bno l n (Const("Trueprop",_) $ t) = get_bno l n t
- | get_bno l n (Const("Ball",_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
- | get_bno l n (Const("mem",_) $ t $ _) = get_bno l n t
+fun get_bno l n (Const(@{const_name all},_) $ Abs(s,_,t)) = get_bno (s::l) n t
+ | get_bno l n (Const(@{const_name Trueprop},_) $ t) = get_bno l n t
+ | get_bno l n (Const(@{const_name Ball},_) $ _ $ Abs(s,_,t)) = get_bno (s::l) (n+1) t
+ | get_bno l n (Const(@{const_name mem},_) $ t $ _) = get_bno l n t
| get_bno l n (t $ s) = get_bno l n t
| get_bno l n (Bound m) = (m-length(l),n)
@@ -450,7 +450,7 @@
fun is_rigid_prog t =
case (Logic.strip_assums_concl t) of
- (Const("Trueprop",_) $ (Const("mem",_) $ a $ _)) => null (Term.add_vars a [])
+ (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) => null (Term.add_vars a [])
| _ => false
in
--- a/src/FOL/fologic.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/FOL/fologic.ML Wed Aug 18 12:05:44 2010 +0200
@@ -37,48 +37,48 @@
structure FOLogic: FOLOGIC =
struct
-val oT = Type("o",[]);
+val oT = Type(@{type_name o},[]);
-val Trueprop = Const("Trueprop", oT-->propT);
+val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
(* Logical constants *)
-val not = Const ("Not", oT --> oT);
-val conj = Const("op &", [oT,oT]--->oT);
-val disj = Const("op |", [oT,oT]--->oT);
-val imp = Const("op -->", [oT,oT]--->oT)
-val iff = Const("op <->", [oT,oT]--->oT);
+val not = Const (@{const_name Not}, oT --> oT);
+val conj = Const(@{const_name "op &"}, [oT,oT]--->oT);
+val disj = Const(@{const_name "op |"}, [oT,oT]--->oT);
+val imp = Const(@{const_name "op -->"}, [oT,oT]--->oT)
+val iff = Const(@{const_name "op <->"}, [oT,oT]--->oT);
fun mk_conj (t1, t2) = conj $ t1 $ t2
and mk_disj (t1, t2) = disj $ t1 $ t2
and mk_imp (t1, t2) = imp $ t1 $ t2
and mk_iff (t1, t2) = iff $ t1 $ t2;
-fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
+fun dest_imp (Const(@{const_name "op -->"},_) $ A $ B) = (A, B)
| dest_imp t = raise TERM ("dest_imp", [t]);
-fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
+fun dest_conj (Const (@{const_name "op &"}, _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
+fun dest_iff (Const(@{const_name "op <->"},_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);
-fun eq_const T = Const ("op =", [T, T] ---> oT);
+fun eq_const T = Const (@{const_name "op ="}, [T, T] ---> oT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
-fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+fun dest_eq (Const (@{const_name "op ="}, _) $ lhs $ rhs) = (lhs, rhs)
| dest_eq t = raise TERM ("dest_eq", [t])
-fun all_const T = Const ("All", [T --> oT] ---> oT);
+fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
-fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
+fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
--- a/src/FOL/intprover.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/FOL/intprover.ML Wed Aug 18 12:05:44 2010 +0200
@@ -40,22 +40,22 @@
step of an intuitionistic proof.
*)
val safe_brls = sort (make_ord lessb)
- [ (true, thm "FalseE"), (false, thm "TrueI"), (false, thm "refl"),
- (false, thm "impI"), (false, thm "notI"), (false, thm "allI"),
- (true, thm "conjE"), (true, thm "exE"),
- (false, thm "conjI"), (true, thm "conj_impE"),
- (true, thm "disj_impE"), (true, thm "disjE"),
- (false, thm "iffI"), (true, thm "iffE"), (true, thm "not_to_imp") ];
+ [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
+ (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
+ (true, @{thm conjE}), (true, @{thm exE}),
+ (false, @{thm conjI}), (true, @{thm conj_impE}),
+ (true, @{thm disj_impE}), (true, @{thm disjE}),
+ (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
val haz_brls =
- [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"),
- (true, thm "allE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"),
- (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ];
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
+ (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
val haz_dup_brls =
- [ (false, thm "disjI1"), (false, thm "disjI2"), (false, thm "exI"),
- (true, thm "all_dupE"), (true, thm "not_impE"), (true, thm "imp_impE"), (true, thm "iff_impE"),
- (true, thm "all_impE"), (true, thm "ex_impE"), (true, thm "impE") ];
+ [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}),
+ (true, @{thm all_dupE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
+ (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
(*0 subgoals vs 1 or more: the p in safep is for positive*)
val (safe0_brls, safep_brls) =
--- a/src/FOL/simpdata.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/FOL/simpdata.ML Wed Aug 18 12:05:44 2010 +0200
@@ -8,16 +8,16 @@
(*Make meta-equalities. The operator below is Trueprop*)
fun mk_meta_eq th = case concl_of th of
- _ $ (Const("op =",_)$_$_) => th RS @{thm eq_reflection}
- | _ $ (Const("op <->",_)$_$_) => th RS @{thm iff_reflection}
+ _ $ (Const(@{const_name "op ="},_)$_$_) => th RS @{thm eq_reflection}
+ | _ $ (Const(@{const_name "op <->"},_)$_$_) => th RS @{thm iff_reflection}
| _ =>
error("conclusion must be a =-equality or <->");;
fun mk_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | _ $ (Const("op =",_)$_$_) => mk_meta_eq th
- | _ $ (Const("op <->",_)$_$_) => mk_meta_eq th
- | _ $ (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
+ | _ $ (Const(@{const_name "op ="},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name "op <->"},_)$_$_) => mk_meta_eq th
+ | _ $ (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T};
(*Replace premises x=y, X<->Y by X==Y*)
@@ -32,13 +32,13 @@
error("Premises and conclusion of congruence rules must use =-equality or <->");
val mksimps_pairs =
- [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
- ("All", [@{thm spec}]), ("True", []), ("False", [])];
+ [(@{const_name "op -->"}, [@{thm mp}]), (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
+ (@{const_name All}, [@{thm spec}]), (@{const_name True}, []), (@{const_name False}, [])];
fun mk_atomize pairs =
let fun atoms th =
(case concl_of th of
- Const("Trueprop",_) $ p =>
+ Const(@{const_name Trueprop},_) $ p =>
(case head_of p of
Const(a,_) =>
(case AList.lookup (op =) pairs a of
@@ -55,11 +55,11 @@
structure Quantifier1 = Quantifier1Fun(
struct
(*abstract syntax*)
- fun dest_eq((c as Const("op =",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_eq((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME(c,s,t)
| dest_eq _ = NONE;
- fun dest_conj((c as Const("op &",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_conj((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME(c,s,t)
| dest_conj _ = NONE;
- fun dest_imp((c as Const("op -->",_)) $ s $ t) = SOME(c,s,t)
+ fun dest_imp((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME(c,s,t)
| dest_imp _ = NONE;
val conj = FOLogic.conj
val imp = FOLogic.imp
--- a/src/HOL/Library/ROOT.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/HOL/Library/ROOT.ML Wed Aug 18 12:05:44 2010 +0200
@@ -2,4 +2,4 @@
(* Classical Higher-order Logic -- batteries included *)
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order",
- "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set", "Code_Prolog"];
+ "Code_Char_chr", "Code_Integer", "Efficient_Nat", "Executable_Set"(*, "Code_Prolog"*)];
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 12:05:44 2010 +0200
@@ -414,6 +414,6 @@
val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
>> (fn ((print_modes, soln), t) => Toplevel.keep
- (values_cmd print_modes soln t)));
+ (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
end;
--- a/src/HOL/ex/SAT_Examples.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Wed Aug 18 12:05:44 2010 +0200
@@ -273,16 +273,7 @@
and 183: "~x29 | ~x58"
and 184: "~x28 | ~x58"
shows "False"
-using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
-20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
-40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
-60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
-80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
-100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
-120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
-140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
-160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
-180 181 182 183 184
+using assms
(*
by sat
*)
@@ -495,17 +486,7 @@
and 203: "~x41 | ~x55"
and 204: "~x48 | ~x55"
shows "False"
-using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
-20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
-40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
-60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
-80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
-100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
-120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
-140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159
-160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
-180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
-200 201 202 203 204
+using assms
(*
by sat
*)
--- a/src/Sequents/LK0.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/src/Sequents/LK0.thy Wed Aug 18 12:05:44 2010 +0200
@@ -12,8 +12,6 @@
imports Sequents
begin
-global
-
classes "term"
default_sort "term"
@@ -61,8 +59,6 @@
Ex (binder "\<exists>" 10) and
not_equal (infixl "\<noteq>" 50)
-local
-
axioms
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
--- a/src/Sequents/Sequents.thy Wed Aug 18 12:04:00 2010 +0200
+++ b/src/Sequents/Sequents.thy Wed Aug 18 12:05:44 2010 +0200
@@ -14,8 +14,6 @@
declare [[unify_trace_bound = 20, unify_search_bound = 40]]
-global
-
typedecl o
(* Sequences *)
--- a/src/Sequents/modal.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/Sequents/modal.ML Wed Aug 18 12:05:44 2010 +0200
@@ -29,7 +29,7 @@
in
(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("SeqO",_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq (Const(@{const_name SeqO'},_) $ P $ u) = P :: forms_of_seq u
| forms_of_seq (H $ u) = forms_of_seq u
| forms_of_seq _ = [];
--- a/src/Sequents/prover.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/Sequents/prover.ML Wed Aug 18 12:05:44 2010 +0200
@@ -55,7 +55,7 @@
["Unsafe rules:"] @ map Display.string_of_thm_without_context unsafes));
(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("SeqO'",_) $ P $ u) = P :: forms_of_seq u
+fun forms_of_seq (Const(@{const_name "SeqO'"},_) $ P $ u) = P :: forms_of_seq u
| forms_of_seq (H $ u) = forms_of_seq u
| forms_of_seq _ = [];
--- a/src/Sequents/simpdata.ML Wed Aug 18 12:04:00 2010 +0200
+++ b/src/Sequents/simpdata.ML Wed Aug 18 12:05:44 2010 +0200
@@ -13,16 +13,16 @@
(*Make atomic rewrite rules*)
fun atomize r =
case concl_of r of
- Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+ Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- Const("imp",_)$_$_ => atomize(r RS @{thm mp_R})
- | Const("conj",_)$_$_ => atomize(r RS @{thm conjunct1}) @
+ Const(@{const_name imp},_)$_$_ => atomize(r RS @{thm mp_R})
+ | Const(@{const_name conj},_)$_$_ => atomize(r RS @{thm conjunct1}) @
atomize(r RS @{thm conjunct2})
- | Const("All",_)$_ => atomize(r RS @{thm spec})
- | Const("True",_) => [] (*True is DELETED*)
- | Const("False",_) => [] (*should False do something?*)
+ | Const(@{const_name All},_)$_ => atomize(r RS @{thm spec})
+ | Const(@{const_name True},_) => [] (*True is DELETED*)
+ | Const(@{const_name False},_) => [] (*should False do something?*)
| _ => [r])
| _ => []) (*ignore theorem unless it has precisely one conclusion*)
| _ => [r];
@@ -30,13 +30,13 @@
(*Make meta-equalities.*)
fun mk_meta_eq th = case concl_of th of
Const("==",_)$_$_ => th
- | Const("Trueprop",_) $ Abs(_,_,a) $ Abs(_,_,c) =>
+ | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) =>
(case (forms_of_seq a, forms_of_seq c) of
([], [p]) =>
(case p of
- (Const("equal",_)$_$_) => th RS @{thm eq_reflection}
- | (Const("iff",_)$_$_) => th RS @{thm iff_reflection}
- | (Const("Not",_)$_) => th RS @{thm iff_reflection_F}
+ (Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection}
+ | (Const(@{const_name iff},_)$_$_) => th RS @{thm iff_reflection}
+ | (Const(@{const_name Not},_)$_) => th RS @{thm iff_reflection_F}
| _ => th RS @{thm iff_reflection_T})
| _ => error ("addsimps: unable to use theorem\n" ^
Display.string_of_thm_without_context th));