--- a/NEWS Wed Aug 18 17:01:12 2010 +0200
+++ b/NEWS Wed Aug 18 17:03:09 2010 +0200
@@ -89,6 +89,8 @@
nat ~> Nat.nat
constants
+ Let ~> HOL.Let
+ If ~> HOL.If
Ball ~> Set.Ball
Bex ~> Set.Bex
Suc ~> Nat.Suc
@@ -102,7 +104,7 @@
INCOMPATIBILITY.
* Removed simplifier congruence rule of "prod_case", as has for long
-been the case with "split".
+been the case with "split". INCOMPATIBILITY.
* Datatype package: theorems generated for executable equality
(class eq) carry proper names and are treated as default code
@@ -111,8 +113,8 @@
* List.thy: use various operations from the Haskell prelude when
generating Haskell code.
-* code_simp.ML: simplification with rules determined by
-code generator.
+* code_simp.ML and method code_simp: simplification with rules determined
+by code generator.
* code generator: do not print function definitions for case
combinators any longer.
@@ -143,6 +145,16 @@
similar to inductive_cases.
+*** FOL ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
+*** ZF ***
+
+* All constant names are now qualified. INCOMPATIBILITY.
+
+
*** ML ***
* ML antiquotations @{theory} and @{theory_ref} refer to named
--- a/doc-src/Codegen/IsaMakefile Wed Aug 18 17:01:12 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Wed Aug 18 17:03:09 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 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/ROOT.ML Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/doc-src/Codegen/codegen.tex Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/CCL/Set.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/CCL/Wfd.thy Wed Aug 18 17:03:09 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/IFOL.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/FOL/IFOL.thy Wed Aug 18 17:03:09 2010 +0200
@@ -28,8 +28,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -87,8 +85,6 @@
Ex (binder "\<exists>" 10) and
Ex1 (binder "\<exists>!" 10)
-local
-
finalconsts
False All Ex
"op ="
--- a/src/FOL/fologic.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/FOL/fologic.ML Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/FOL/intprover.ML Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/FOL/simpdata.ML Wed Aug 18 17:03:09 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/FOLP/IFOLP.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/FOLP/IFOLP.thy Wed Aug 18 17:03:09 2010 +0200
@@ -12,8 +12,6 @@
setup PureThy.old_appl_syntax_setup
-global
-
classes "term"
default_sort "term"
@@ -63,8 +61,6 @@
nrm :: p
NRM :: p
-local
-
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5)
ML {*
--- a/src/HOL/HOL.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/HOL.thy Wed Aug 18 17:03:09 2010 +0200
@@ -63,7 +63,6 @@
All :: "('a => bool) => bool" (binder "ALL " 10)
Ex :: "('a => bool) => bool" (binder "EX " 10)
Ex1 :: "('a => bool) => bool" (binder "EX! " 10)
- Let :: "['a, 'a => 'b] => 'b"
"op =" :: "['a, 'a] => bool" (infixl "=" 50)
"op &" :: "[bool, bool] => bool" (infixr "&" 35)
@@ -72,9 +71,6 @@
local
-consts
- If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
-
subsubsection {* Additional concrete syntax *}
@@ -127,8 +123,6 @@
translations
"THE x. P" == "CONST The (%x. P)"
- "_Let (_binds b bs) e" == "_Let b (_Let bs e)"
- "let x = a in e" == "CONST Let a (%x. e)"
print_translation {*
[(@{const_syntax The}, fn [Abs abs] =>
@@ -185,15 +179,21 @@
iff: "(P-->Q) --> (Q-->P) --> (P=Q)"
True_or_False: "(P=True) | (P=False)"
-defs
- Let_def [code]: "Let s f == f(s)"
- if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
-
finalconsts
"op ="
"op -->"
The
+definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10) where
+ "If P x y \<equiv> (THE z::'a. (P=True --> z=x) & (P=False --> z=y))"
+
+definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" where
+ "Let s f \<equiv> f s"
+
+translations
+ "_Let (_binds b bs) e" == "_Let b (_Let bs e)"
+ "let x = a in e" == "CONST Let a (%x. e)"
+
axiomatization
undefined :: 'a
@@ -1084,16 +1084,16 @@
text {* \medskip if-then-else rules *}
lemma if_True [code]: "(if True then x else y) = x"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_False [code]: "(if False then x else y) = y"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_P: "P ==> (if P then x else y) = x"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma if_not_P: "~P ==> (if P then x else y) = y"
- by (unfold if_def) blast
+ by (unfold If_def) blast
lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
apply (rule case_split [of Q])
@@ -1365,7 +1365,7 @@
and "c \<Longrightarrow> x = u"
and "\<not> c \<Longrightarrow> y = v"
shows "(if b then x else y) = (if c then u else v)"
- unfolding if_def using assms by simp
+ using assms by simp
text {* Prevents simplification of x and y:
faster and allows the execution of functional programs. *}
@@ -1390,13 +1390,6 @@
"f (if c then x else y) = (if c then f x else f y)"
by simp
-text {* This lemma restricts the effect of the rewrite rule u=v to the left-hand
- side of an equality. Used in @{text "{Integ,Real}/simproc.ML"} *}
-lemma restrict_to_left:
- assumes "x = y"
- shows "(x = z) = (y = z)"
- using assms by simp
-
subsubsection {* Generic cases and induction *}
--- a/src/HOL/Library/Dlist.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Wed Aug 18 17:03:09 2010 +0200
@@ -15,8 +15,8 @@
qed
lemma dlist_ext:
- assumes "list_of_dlist xs = list_of_dlist ys"
- shows "xs = ys"
+ assumes "list_of_dlist dxs = list_of_dlist dys"
+ shows "dxs = dys"
using assms by (simp add: list_of_dlist_inject)
@@ -107,6 +107,19 @@
by simp
+text {* Equality *}
+
+instantiation dlist :: (eq) eq
+begin
+
+definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+
+instance proof
+qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+
+end
+
+
section {* Induction principle and case distinction *}
lemma dlist_induct [case_names empty insert, induct type: dlist]:
@@ -283,6 +296,7 @@
end
+
hide_const (open) member fold foldr empty insert remove map filter null member length fold
end
--- a/src/HOL/Library/ROOT.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Library/ROOT.ML Wed Aug 18 17:03:09 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/Matrix/Matrix.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy Wed Aug 18 17:03:09 2010 +0200
@@ -528,12 +528,12 @@
show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
apply (simp add: subd)
- apply (case_tac "m=0")
+ apply (cases "m = 0")
apply (simp)
apply (drule sube)
apply (auto)
apply (rule a)
- by (simp add: subc if_def)
+ by (simp add: subc cong del: if_cong)
qed
then show ?thesis using assms by simp
qed
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Aug 18 17:03:09 2010 +0200
@@ -63,12 +63,12 @@
| string_for_connective AIff = "<=>"
| string_for_connective ANotIff = "<~>"
fun string_for_formula (AQuant (q, xs, phi)) =
- string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
- string_for_formula phi
+ "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+ string_for_formula phi ^ ")"
| string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
space_implode " != " (map string_for_term ts)
| string_for_formula (AConn (c, [phi])) =
- string_for_connective c ^ " " ^ string_for_formula phi
+ "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
| string_for_formula (AConn (c, phis)) =
"(" ^ space_implode (" " ^ string_for_connective c ^ " ")
(map string_for_formula phis) ^ ")"
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 17:03:09 2010 +0200
@@ -8,7 +8,9 @@
signature ATP_SYSTEMS =
sig
datatype failure =
- Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+ MalformedInput | MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -38,7 +40,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+ SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
MalformedOutput | UnknownError
type prover_config =
@@ -61,7 +63,7 @@
| string_for_failure CantConnect = "Can't connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure OldSpass =
+ | string_for_failure SpassTooOld =
"Isabelle requires a more recent version of SPASS with support for the \
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -70,7 +72,7 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
- | string_for_failure OldVampire =
+ | string_for_failure VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
\the instructions from the Sledgehammer manual (\"isabelle doc\
\ sledgehammer\")."
@@ -142,7 +144,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 60 (* FIXME *),
+ max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
@@ -168,7 +170,7 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
- (OldSpass, "tptp2dfg")],
+ (SpassTooOld, "tptp2dfg")],
max_new_relevant_facts_per_iter = 35 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
@@ -183,7 +185,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --input_file ",
+ " --input_file",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -195,8 +197,8 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found"),
- (OldVampire, "input_file")],
- max_new_relevant_facts_per_iter = 50 (* FIXME *),
+ (VampireTooOld, "not a valid option")],
+ max_new_relevant_facts_per_iter = 45 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 17:03:09 2010 +0200
@@ -156,6 +156,7 @@
datatype outcome =
JavaNotInstalled |
+ JavaTooOld |
KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
@@ -303,6 +304,7 @@
datatype outcome =
JavaNotInstalled |
+ JavaTooOld |
KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
@@ -1063,19 +1065,20 @@
|> perhaps (try (unsuffix "."))
|> perhaps (try (unprefix "Solve error: "))
|> perhaps (try (unprefix "Error: "))
+ fun has_error s =
+ first_error |> Substring.full |> Substring.position s |> snd
+ |> Substring.isEmpty |> not
in
if null ps then
if code = 2 then
TimedOut js
else if code = 0 then
Normal ([], js, first_error)
- else if first_error |> Substring.full
- |> Substring.position "exec: java" |> snd
- |> Substring.isEmpty |> not then
+ else if has_error "exec: java" then
JavaNotInstalled
- else if first_error |> Substring.full
- |> Substring.position "NoClassDefFoundError" |> snd
- |> Substring.isEmpty |> not then
+ else if has_error "UnsupportedClassVersionError" then
+ JavaTooOld
+ else if has_error "NoClassDefFoundError" then
KodkodiNotInstalled
else if first_error <> "" then
Error (first_error, js)
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 17:03:09 2010 +0200
@@ -315,6 +315,7 @@
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
JavaNotInstalled => "unknown"
+ | JavaTooOld => "unknown"
| KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 17:03:09 2010 +0200
@@ -740,6 +740,9 @@
KK.JavaNotInstalled =>
(print_m install_java_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
+ | KK.JavaTooOld =>
+ (print_m install_java_message;
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.KodkodiNotInstalled =>
(print_m install_kodkodi_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Aug 18 17:03:09 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/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:03:09 2010 +0200
@@ -167,8 +167,8 @@
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
- --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
+ $$ "(" |-- scan_integer --| $$ ","
+ -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
--| Scan.option ($$ ",")
val parse_clause_formula_relation =
Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
@@ -183,21 +183,21 @@
thm_names =
if String.isSubstring set_ClauseFormulaRelationN output then
(* This is a hack required for keeping track of axioms after they have been
- clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
- of this hack. *)
+ clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
+ part of this hack. *)
let
val j0 = hd (hd conjecture_shape)
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
fun renumber_conjecture j =
- AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
+ conjecture_prefix ^ Int.toString (j - j0)
+ |> AList.find (fn (s, ss) => member (op =) ss s) name_map
|> map (fn s => find_index (curry (op =) s) seq + 1)
in
(conjecture_shape |> map (maps renumber_conjecture),
- seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
- |> try (unprefix axiom_prefix) of
- SOME s' => undo_ascii_of s'
- | NONE => "")
+ seq |> map (AList.lookup (op =) name_map #> these
+ #> map_filter (try (unprefix axiom_prefix))
+ #> map undo_ascii_of #> space_implode " ")
|> Vector.fromList)
end
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:03:09 2010 +0200
@@ -85,8 +85,7 @@
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, proof, used_thm_names, ...}
- : prover_result =>
+ result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
sublinear_minimize test (filter_used_facts used_thm_names xs)
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Aug 18 17:03:09 2010 +0200
@@ -279,10 +279,10 @@
| add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ = I
-fun fix_atp_variable_name s =
+fun repair_atp_variable_name f s =
let
fun subscript_name s n = s ^ nat_subscript n
- val s = String.map Char.toLower s
+ val s = String.map f s
in
case space_explode "_" s of
[_] => (case take_suffix Char.isDigit (String.explode s) of
@@ -349,9 +349,10 @@
SOME b => Var ((b, 0), T)
| NONE =>
if is_tptp_variable a then
- Var ((fix_atp_variable_name a, 0), T)
+ Var ((repair_atp_variable_name Char.toLower a, 0), T)
else
- raise Fail ("Unexpected constant: " ^ quote a)
+ (* Skolem constants? *)
+ Var ((repair_atp_variable_name Char.toUpper a, 0), T)
in list_comb (t, ts) end
in aux (SOME HOLogic.boolT) [] end
@@ -410,7 +411,8 @@
do_formula pos (AQuant (q, xs, phi'))
#>> quantify_over_free (case q of
AForall => @{const_name All}
- | AExists => @{const_name Ex}) x
+ | AExists => @{const_name Ex})
+ (repair_atp_variable_name Char.toLower x)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -834,6 +836,7 @@
second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
in proof_top @ proof_bottom end
+(* FIXME: Still needed? Probably not. *)
val kill_duplicate_assumptions_in_proof =
let
fun relabel_facts subst =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 17:03:09 2010 +0200
@@ -55,8 +55,10 @@
let
val do_term = combterm_from_term thy
fun do_quant bs q s T t' =
- do_formula ((s, T) :: bs) t'
- #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ let val s = Name.variant (map fst bs) s in
+ do_formula ((s, T) :: bs) t'
+ #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ end
and do_conn bs c t1 t2 =
do_formula bs t1 ##>> do_formula bs t2
#>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
@@ -102,41 +104,41 @@
(0 upto length Ts - 1 ~~ Ts))
fun introduce_combinators_in_term ctxt kind t =
- let
- val thy = ProofContext.theory_of ctxt
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- let
- val t = t |> conceal_bounds Ts
- |> Envir.eta_contract
- val ([t], ctxt') = Variable.import_terms true [t] ctxt
- in
- t |> cterm_of thy
- |> Clausifier.introduce_combinators_in_cterm
- |> singleton (Variable.export ctxt' ctxt)
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- end
- in t |> not (Meson.is_fol_term thy t) ? aux [] end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
+ let val thy = ProofContext.theory_of ctxt in
+ if Meson.is_fol_term thy t then
+ t
+ else
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ |> cterm_of thy
+ |> Clausifier.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ val ([t], ctxt') = Variable.import_terms true [t] ctxt
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ case kind of
+ Axiom => HOLogic.true_const
+ | Conjecture => HOLogic.false_const
+ end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
same in Sledgehammer to prevent the discovery of unreplable proofs. *)
@@ -267,16 +269,18 @@
val (x, ty_args) =
case head of
CombConst (name as (s, s'), _, ty_args) =>
- if s = "equal" then
- (if top_level andalso length args = 2 then name
- else ("c_fequal", @{const_name fequal}), [])
- else if top_level then
- case s of
- "c_False" => (("$false", s'), [])
- | "c_True" => (("$true", s'), [])
- | _ => (name, if full_types then [] else ty_args)
- else
- (name, if full_types then [] else ty_args)
+ let val ty_args = if full_types then [] else ty_args in
+ if s = "equal" then
+ if top_level andalso length args = 2 then (name, [])
+ else (("c_fequal", @{const_name fequal}), ty_args)
+ else if top_level then
+ case s of
+ "c_False" => (("$false", s'), [])
+ | "c_True" => (("$true", s'), [])
+ | _ => (name, ty_args)
+ else
+ (name, ty_args)
+ end
| CombVar (name, _) => (name, [])
| CombApp _ => raise Fail "impossible \"CombApp\""
val t = ATerm (x, map fo_term_for_combtyp ty_args @
--- a/src/HOL/Word/Word.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/Word/Word.thy Wed Aug 18 17:03:09 2010 +0200
@@ -4034,6 +4034,11 @@
"length (rotater n xs) = length xs"
by (simp add : rotater_rev)
+lemma restrict_to_left:
+ assumes "x = y"
+ shows "(x = z) = (y = z)"
+ using assms by simp
+
lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
--- a/src/HOL/ex/SAT_Examples.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Wed Aug 18 17:03:09 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
*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/linear_set.ML Wed Aug 18 17:03:09 2010 +0200
@@ -0,0 +1,142 @@
+(* Title: Pure/General/linear_set.ML
+ Author: Makarius
+
+Sets with canonical linear order, or immutable linked-lists.
+*)
+
+signature LINEAR_SET =
+sig
+ type key
+ type 'a T
+ exception DUPLICATE of key
+ exception UNDEFINED of key
+ exception NEXT_UNDEFINED of key option
+ val empty: 'a T
+ val is_empty: 'a T -> bool
+ val defined: 'a T -> key -> bool
+ val lookup: 'a T -> key -> 'a option
+ val update: key * 'a -> 'a T -> 'a T
+ val fold: key option ->
+ ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
+ val get_first: key option ->
+ ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+ val get_after: 'a T -> key option -> key option
+ val insert_after: key option -> key * 'a -> 'a T -> 'a T
+ val delete_after: key option -> 'a T -> 'a T
+end;
+
+functor Linear_Set(Key: KEY): LINEAR_SET =
+struct
+
+(* type key *)
+
+type key = Key.key;
+structure Table = Table(Key);
+
+exception DUPLICATE of key;
+exception UNDEFINED of key;
+exception NEXT_UNDEFINED of key option;
+
+
+(* raw entries *)
+
+fun the_entry entries key =
+ (case Table.lookup entries key of
+ NONE => raise UNDEFINED key
+ | SOME entry => entry);
+
+fun next_entry entries key = snd (the_entry entries key);
+
+fun put_entry entry entries = Table.update entry entries;
+
+fun new_entry entry entries = Table.update_new entry entries
+ handle Table.DUP key => raise DUPLICATE key;
+
+fun del_entry key entries = Table.delete_safe key entries;
+
+
+(* set representation and basic operations *)
+
+datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table};
+
+fun make_set (start, entries) = Set {start = start, entries = entries};
+fun map_set f (Set {start, entries}) = make_set (f (start, entries));
+
+fun start_of (Set {start, ...}) = start;
+fun entries_of (Set {entries, ...}) = entries;
+
+val empty = Set {start = NONE, entries = Table.empty};
+fun is_empty set = is_none (start_of set);
+
+fun defined set key = Table.defined (entries_of set) key;
+
+fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+
+fun update (key, x) = map_set (fn (start, entries) =>
+ (start, put_entry (key, (x, next_entry entries key)) entries));
+
+
+(* iterate entries *)
+
+fun optional_start set NONE = start_of set
+ | optional_start _ some = some;
+
+fun fold opt_start f set =
+ let
+ val entries = entries_of set;
+ fun apply _ NONE y = y
+ | apply prev (SOME key) y =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in apply (SOME key) next (f item y) end;
+ in apply NONE (optional_start set opt_start) end;
+
+fun get_first opt_start P set =
+ let
+ val entries = entries_of set;
+ fun first _ NONE = NONE
+ | first prev (SOME key) =
+ let
+ val (x, next) = the_entry entries key;
+ val item = ((prev, key), x);
+ in if P item then SOME item else first (SOME key) next end;
+ in first NONE (optional_start set opt_start) end;
+
+
+(* relative addressing *)
+
+fun get_after set hook =
+ (case hook of
+ NONE => start_of set
+ | SOME key => next_entry (entries_of set) key);
+
+fun insert_after hook (key, x) = map_set (fn (start, entries) =>
+ (case hook of
+ NONE => (SOME key, new_entry (key, (x, start)) entries)
+ | SOME key1 =>
+ let
+ val (x1, next) = the_entry entries key1;
+ val entries' = entries
+ |> put_entry (key1, (x1, SOME key))
+ |> new_entry (key, (x, next));
+ in (start, entries') end));
+
+fun delete_after hook set = set |> map_set (fn (start, entries) =>
+ (case hook of
+ NONE =>
+ (case start of
+ NONE => raise NEXT_UNDEFINED NONE
+ | SOME key1 => (next_entry entries key1, del_entry key1 entries))
+ | SOME key1 =>
+ (case the_entry entries key1 of
+ (_, NONE) => raise NEXT_UNDEFINED (SOME key1)
+ | (x1, SOME key2) =>
+ let
+ val entries' = entries
+ |> put_entry (key1, (x1, next_entry entries key2))
+ |> del_entry key2;
+ in (start, entries') end)));
+
+end;
+
--- a/src/Pure/General/linear_set.scala Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/General/linear_set.scala Wed Aug 18 17:03:09 2010 +0200
@@ -25,8 +25,9 @@
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
override def empty[A] = new Linear_Set[A]
- class Duplicate(s: String) extends Exception(s)
- class Undefined(s: String) extends Exception(s)
+ class Duplicate[A](x: A) extends Exception
+ class Undefined[A](x: A) extends Exception
+ class Next_Undefined[A](x: Option[A]) extends Exception
}
@@ -43,19 +44,22 @@
protected val rep = Linear_Set.empty_rep[A]
- /* auxiliary operations */
+ /* relative addressing */
+ // FIXME check definedness??
def next(elem: A): Option[A] = rep.nexts.get(elem)
def prev(elem: A): Option[A] = rep.prevs.get(elem)
def get_after(hook: Option[A]): Option[A] =
hook match {
case None => rep.start
- case Some(elem) => next(elem)
+ case Some(elem) =>
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
+ next(elem)
}
def insert_after(hook: Option[A], elem: A): Linear_Set[A] =
- if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString)
+ if (contains(elem)) throw new Linear_Set.Duplicate(elem)
else
hook match {
case None =>
@@ -66,7 +70,7 @@
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
case None =>
@@ -83,7 +87,7 @@
hook match {
case None =>
rep.start match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined[A](None)
case Some(elem1) =>
rep.nexts.get(elem1) match {
case None => empty
@@ -92,10 +96,10 @@
}
}
case Some(elem1) =>
- if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString)
+ if (!contains(elem1)) throw new Linear_Set.Undefined(elem1)
else
rep.nexts.get(elem1) match {
- case None => throw new Linear_Set.Undefined("")
+ case None => throw new Linear_Set.Next_Undefined(Some(elem1))
case Some(elem2) =>
rep.nexts.get(elem2) match {
case None =>
@@ -153,15 +157,15 @@
def iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.nexts)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def reverse_iterator(elem: A): Iterator[A] =
if (contains(elem)) make_iterator(Some(elem), rep.prevs)
- else throw new Linear_Set.Undefined(elem.toString)
+ else throw new Linear_Set.Undefined(elem)
def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
def - (elem: A): Linear_Set[A] =
- if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
+ if (!contains(elem)) throw new Linear_Set.Undefined(elem)
else delete_after(prev(elem))
}
\ No newline at end of file
--- a/src/Pure/IsaMakefile Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/IsaMakefile Wed Aug 18 17:03:09 2010 +0200
@@ -80,6 +80,7 @@
General/graph.ML \
General/heap.ML \
General/integer.ML \
+ General/linear_set.ML \
General/long_name.ML \
General/markup.ML \
General/name_space.ML \
--- a/src/Pure/Isar/class_declaration.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Aug 18 17:03:09 2010 +0200
@@ -129,18 +129,22 @@
^ Syntax.string_of_sort_global thy a_sort ^ ".")
| _ => error "Multiple type variables in class specification.";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
+ val after_infer_fixate = (map o map_atyps)
+ (fn T as TFree _ => T | T as TVar (vi, sort) =>
+ if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort) else T);
fun add_typ_check level name f = Context.proof_map
(Syntax.add_typ_check level name (fn Ts => fn ctxt =>
let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end));
(* preprocessing elements, retrieving base sort from type-checked elements *)
+ val raw_supexpr = (map (fn sup => (sup, (("", false),
+ Expression.Positional []))) sups, []);
val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
#> Class.redeclare_operations thy sups
#> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
#> add_typ_check ~10 "singleton_fixate" singleton_fixate;
- val raw_supexpr = (map (fn sup => (sup, (("", false),
- Expression.Positional []))) sups, []);
val ((raw_supparams, _, raw_inferred_elems), _) = ProofContext.init_global thy
+ |> add_typ_check 5 "after_infer_fixate" after_infer_fixate
|> prep_decl raw_supexpr init_class_body raw_elems;
fun filter_element (Element.Fixes []) = NONE
| filter_element (e as Element.Fixes _) = SOME e
--- a/src/Pure/PIDE/document.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/PIDE/document.ML Wed Aug 18 17:03:09 2010 +0200
@@ -15,7 +15,7 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type edit = string * ((command_id * command_id option) list) option
+ type edit = string * ((command_id option * command_id option) list) option
type state
val init_state: state
val define_command: command_id -> string -> state -> state
@@ -55,82 +55,43 @@
(** document structure **)
-abstype entry = Entry of {next: command_id option, exec: exec_id option}
- and node = Node of entry Inttab.table (*unique entries indexed by command_id, start with no_id*)
+structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+
+abstype node = Node of exec_id option Entries.T (*command entries with excecutions*)
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-
-(* command entries *)
-
-fun make_entry next exec = Entry {next = next, exec = exec};
-
-fun the_entry (Node entries) (id: command_id) =
- (case Inttab.lookup entries id of
- NONE => err_undef "command entry" id
- | SOME (Entry entry) => entry);
+val empty_node = Node Entries.empty;
+val empty_version = Version Graph.empty;
-fun put_entry (id: command_id, entry: entry) (Node entries) =
- Node (Inttab.update (id, entry) entries);
-
-fun put_entry_exec (id: command_id) exec node =
- let val {next, ...} = the_entry node id
- in put_entry (id, make_entry next exec) node end;
-
-fun reset_entry_exec id = put_entry_exec id NONE;
-fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
+fun fold_entries start f (Node entries) = Entries.fold start f entries;
+fun first_entry start P (Node entries) = Entries.get_first start P entries;
-(* iterate entries *)
-
-fun fold_entries id0 f (node as Node entries) =
- let
- fun apply NONE x = x
- | apply (SOME id) x =
- let val entry = the_entry node id
- in apply (#next entry) (f (id, entry) x) end;
- in if Inttab.defined entries id0 then apply (SOME id0) else I end;
-
-fun first_entry P node =
- let
- fun first _ NONE = NONE
- | first prev (SOME id) =
- let val entry = the_entry node id
- in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
- in first NONE (SOME no_id) end;
-
-
-(* modify entries *)
-
-fun insert_after (id: command_id) (id2: command_id) node =
- let val {next, exec} = the_entry node id in
- node
- |> put_entry (id, make_entry (SOME id2) exec)
- |> put_entry (id2, make_entry next NONE)
- end;
-
-fun delete_after (id: command_id) node =
- let val {next, exec} = the_entry node id in
- (case next of
- NONE => error ("No next entry to delete: " ^ print_id id)
- | SOME id2 =>
- node |>
- (case #next (the_entry node id2) of
- NONE => put_entry (id, make_entry NONE exec)
- | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
- end;
-
-
-(* node edits *)
+(* node edits and associated executions *)
type edit =
- string * (*node name*)
- ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
+ string *
+ (*NONE: remove node, SOME: insert/remove commands*)
+ ((command_id option * command_id option) list) option;
+
+fun the_entry (Node entries) id =
+ (case Entries.lookup entries id of
+ NONE => err_undef "command entry" id
+ | SOME entry => entry);
-val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]);
+fun update_entry (id, exec_id) (Node entries) =
+ Node (Entries.update (id, SOME exec_id) entries);
-fun edit_node (id, SOME id2) = insert_after id id2
- | edit_node (id, NONE) = delete_after id;
+fun reset_after id entries =
+ (case Entries.get_after entries id of
+ NONE => entries
+ | SOME next => Entries.update (next, NONE) entries);
+
+fun edit_node (hook, SOME id2) (Node entries) =
+ Node (Entries.insert_after hook (id2, NONE) entries)
+ | edit_node (hook, NONE) (Node entries) =
+ Node (entries |> Entries.delete_after hook |> reset_after hook);
(* version operations *)
@@ -138,19 +99,18 @@
fun nodes_of (Version nodes) = nodes;
val node_names_of = Graph.keys o nodes_of;
+fun get_node version name = Graph.get_node (nodes_of version) name
+ handle Graph.UNDEF _ => empty_node;
+
fun edit_nodes (name, SOME edits) (Version nodes) =
Version (nodes
|> Graph.default_node (name, empty_node)
|> Graph.map_node name (fold edit_node edits))
- | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes);
-
-val empty_version = Version Graph.empty;
-
-fun the_node version name =
- Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node;
+ | edit_nodes (name, NONE) (Version nodes) =
+ Version (Graph.del_node name nodes);
fun put_node name node (Version nodes) =
- Version (Graph.map_node name (K node) nodes); (* FIXME Graph.UNDEF !? *)
+ Version (Graph.map_node name (K node) nodes);
end;
@@ -238,22 +198,22 @@
local
-fun is_changed node' (id, {next = _, exec}) =
+fun is_changed node' ((_, id), exec) =
(case try (the_entry node') id of
NONE => true
- | SOME {next = _, exec = exec'} => exec' <> exec);
+ | SOME exec' => exec' <> exec);
fun new_exec name (id: command_id) (exec_id, updates, state) =
let
val exec = the_exec state exec_id;
val exec_id' = new_id ();
- val tr = the_command state id;
+ val future_tr = the_command state id;
val exec' =
Lazy.lazy (fn () =>
(case Lazy.force exec of
NONE => NONE
| SOME st =>
- let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join tr)
+ let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
in Toplevel.run_command name exec_tr st end));
val state' = define_exec exec_id' exec' state;
in (exec_id', (id, exec_id') :: updates, state') end;
@@ -266,15 +226,18 @@
val new_version = fold edit_nodes edits old_version;
fun update_node name (rev_updates, version, st) =
- let val node = the_node version name in
- (case first_entry (is_changed (the_node old_version name)) node of
+ let val node = get_node version name in
+ (case first_entry NONE (is_changed (get_node old_version name)) node of
NONE => (rev_updates, version, st)
- | SOME (prev, id, _) =>
+ | SOME ((prev, id), _) =>
let
- val prev_exec = the (#exec (the_entry node (the prev)));
+ val prev_exec =
+ (case prev of
+ NONE => no_id
+ | SOME prev_id => the_default no_id (the_entry node prev_id));
val (_, rev_upds, st') =
- fold_entries id (new_exec name o #1) node (prev_exec, [], st);
- val node' = fold set_entry_exec rev_upds node;
+ fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
+ val node' = fold update_entry rev_upds node;
in (rev_upds @ rev_updates, put_node name node' version, st') end)
end;
@@ -306,8 +269,8 @@
node_names_of version |> map (fn name =>
Future.fork_pri 1 (fn () =>
(await_cancellation ();
- fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
- (the_node version name) ())));
+ fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
+ (get_node version name) ())));
in (versions, commands, execs, execution') end);
end;
--- a/src/Pure/ROOT.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Aug 18 17:03:09 2010 +0200
@@ -42,6 +42,7 @@
use "General/ord_list.ML";
use "General/balanced_tree.ML";
use "General/graph.ML";
+use "General/linear_set.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/name_space.ML";
--- a/src/Pure/System/isar_document.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/System/isar_document.ML Wed Aug 18 17:03:09 2010 +0200
@@ -21,10 +21,14 @@
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
val edits =
- XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_option (XML_Data.dest_list
- (XML_Data.dest_pair XML_Data.dest_int
- (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+ XML_Data.dest_list
+ (XML_Data.dest_pair
+ XML_Data.dest_string
+ (XML_Data.dest_option
+ (XML_Data.dest_list
+ (XML_Data.dest_pair
+ (XML_Data.dest_option XML_Data.dest_int)
+ (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
val (updates, state') = Document.edit old_id new_id edits state;
val _ =
--- a/src/Pure/System/isar_document.scala Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Pure/System/isar_document.scala Wed Aug 18 17:03:09 2010 +0200
@@ -51,14 +51,13 @@
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit[Document.Command_ID]])
{
- def make_id1(id1: Option[Document.Command_ID]): XML.Body =
- XML_Data.make_long(id1 getOrElse Document.NO_ID)
-
val arg =
XML_Data.make_list(
XML_Data.make_pair(XML_Data.make_string)(
XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
+ XML_Data.make_pair(
+ XML_Data.make_option(XML_Data.make_long))(
+ XML_Data.make_option(XML_Data.make_long))))))(edits)
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
--- a/src/Sequents/LK0.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/Sequents/LK0.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/Sequents/Sequents.thy Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/Sequents/modal.ML Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/Sequents/prover.ML Wed Aug 18 17:03:09 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 17:01:12 2010 +0200
+++ b/src/Sequents/simpdata.ML Wed Aug 18 17:03:09 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));
--- a/src/ZF/Datatype_ZF.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Datatype_ZF.thy Wed Aug 18 17:03:09 2010 +0200
@@ -61,7 +61,7 @@
struct
val trace = Unsynchronized.ref false;
- fun mk_new ([],[]) = Const("True",FOLogic.oT)
+ fun mk_new ([],[]) = Const(@{const_name True},FOLogic.oT)
| mk_new (largs,rargs) =
Balanced_Tree.make FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -85,7 +85,7 @@
if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
- else Const("False",FOLogic.oT)
+ else Const(@{const_name False},FOLogic.oT)
else raise Match
val _ =
if !trace then writeln ("NEW = " ^ Syntax.string_of_term_global sg new)
--- a/src/ZF/Inductive_ZF.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Inductive_ZF.thy Wed Aug 18 17:03:09 2010 +0200
@@ -31,8 +31,8 @@
lemma refl_thin: "!!P. a = a ==> P ==> P" .
use "ind_syntax.ML"
+use "Tools/ind_cases.ML"
use "Tools/cartprod.ML"
-use "Tools/ind_cases.ML"
use "Tools/inductive_package.ML"
use "Tools/induct_tacs.ML"
use "Tools/primrec_package.ML"
--- a/src/ZF/Sum.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Sum.thy Wed Aug 18 17:03:09 2010 +0200
@@ -9,8 +9,6 @@
text{*And the "Part" primitive for simultaneous recursive type definitions*}
-global
-
definition sum :: "[i,i]=>i" (infixr "+" 65) where
"A+B == {0}*A Un {1}*B"
@@ -27,8 +25,6 @@
definition Part :: "[i,i=>i] => i" where
"Part(A,h) == {x: A. EX z. x = h(z)}"
-local
-
subsection{*Rules for the @{term Part} Primitive*}
lemma Part_iff:
--- a/src/ZF/Tools/induct_tacs.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Wed Aug 18 17:03:09 2010 +0200
@@ -118,7 +118,7 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
+ fun const_of (Const(@{const_name "op ="}, _) $ (_ $ c) $ _) = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
--- a/src/ZF/Tools/inductive_package.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Wed Aug 18 17:03:09 2010 +0200
@@ -102,7 +102,7 @@
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
- fun dest_tprop (Const("Trueprop",_) $ P) = P
+ fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
Syntax.string_of_term ctxt Q);
--- a/src/ZF/Tools/primrec_package.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Tools/primrec_package.ML Wed Aug 18 17:03:09 2010 +0200
@@ -115,8 +115,8 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const ("0", Ind_Syntax.iT),
- #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+ (Const (@{const_name 0}, Ind_Syntax.iT),
+ #2 recursor_pair, Const (@{const_name 0}, Ind_Syntax.iT)))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/Tools/typechk.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Aug 18 17:03:09 2010 +0200
@@ -75,7 +75,7 @@
if length rls <= maxr then resolve_tac rls i else no_tac
end);
-fun is_rigid_elem (Const("Trueprop",_) $ (Const(@{const_name mem},_) $ a $ _)) =
+fun is_rigid_elem (Const(@{const_name Trueprop},_) $ (Const(@{const_name mem},_) $ a $ _)) =
not (is_Var (head_of a))
| is_rigid_elem _ = false;
--- a/src/ZF/ZF.thy Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/ZF.thy Wed Aug 18 17:03:09 2010 +0200
@@ -12,8 +12,6 @@
ML {* Unsynchronized.reset eta_contract *}
-global
-
typedecl i
arities i :: "term"
@@ -209,8 +207,6 @@
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
-local
-
axioms
(* ZF axioms -- see Suppes p.238
--- a/src/ZF/arith_data.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/arith_data.ML Wed Aug 18 17:03:09 2010 +0200
@@ -24,12 +24,12 @@
val iT = Ind_Syntax.iT;
-val zero = Const("0", iT);
-val succ = Const("succ", iT --> iT);
+val zero = Const(@{const_name 0}, iT);
+val succ = Const(@{const_name succ}, iT --> iT);
fun mk_succ t = succ $ t;
val one = mk_succ zero;
-val mk_plus = FOLogic.mk_binop "Arith.add";
+val mk_plus = FOLogic.mk_binop @{const_name Arith.add};
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -40,13 +40,13 @@
fun long_mk_sum [] = zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = FOLogic.dest_bin "Arith.add" iT;
+val dest_plus = FOLogic.dest_bin @{const_name Arith.add} iT;
(* dest_sum *)
-fun dest_sum (Const("0",_)) = []
- | dest_sum (Const("succ",_) $ t) = one :: dest_sum t
- | dest_sum (Const("Arith.add",_) $ t $ u) = dest_sum t @ dest_sum u
+fun dest_sum (Const(@{const_name 0},_)) = []
+ | dest_sum (Const(@{const_name succ},_) $ t) = one :: dest_sum t
+ | dest_sum (Const(@{const_name Arith.add},_) $ t $ u) = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
(*Apply the given rewrite (if present) just once*)
@@ -83,14 +83,14 @@
(*** Use CancelNumerals simproc without binary numerals,
just for cancellation ***)
-val mk_times = FOLogic.mk_binop "Arith.mult";
+val mk_times = FOLogic.mk_binop @{const_name Arith.mult};
fun mk_prod [] = one
| mk_prod [t] = t
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = FOLogic.dest_bin "Arith.mult" iT;
+val dest_times = FOLogic.dest_bin @{const_name Arith.mult} iT;
fun dest_prod t =
let val (t,u) = dest_times t
@@ -174,8 +174,8 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
- val mk_bal = FOLogic.mk_binrel "Ordinal.lt"
- val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
+ val mk_bal = FOLogic.mk_binrel @{const_name Ordinal.lt}
+ val dest_bal = FOLogic.dest_bin @{const_name Ordinal.lt} iT
val bal_add1 = @{thm less_add_iff} RS @{thm iff_trans}
val bal_add2 = @{thm less_add_iff} RS @{thm iff_trans}
fun trans_tac _ = gen_trans_tac @{thm iff_trans}
@@ -187,8 +187,8 @@
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
- val mk_bal = FOLogic.mk_binop "Arith.diff"
- val dest_bal = FOLogic.dest_bin "Arith.diff" iT
+ val mk_bal = FOLogic.mk_binop @{const_name Arith.diff}
+ val dest_bal = FOLogic.dest_bin @{const_name Arith.diff} iT
val bal_add1 = @{thm diff_add_eq} RS @{thm trans}
val bal_add2 = @{thm diff_add_eq} RS @{thm trans}
fun trans_tac _ = gen_trans_tac @{thm trans}
--- a/src/ZF/ind_syntax.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/ind_syntax.ML Wed Aug 18 17:03:09 2010 +0200
@@ -18,7 +18,7 @@
(** Abstract syntax definitions for ZF **)
-val iT = Type("i",[]);
+val iT = Type(@{type_name i}, []);
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
--- a/src/ZF/simpdata.ML Wed Aug 18 17:01:12 2010 +0200
+++ b/src/ZF/simpdata.ML Wed Aug 18 17:03:09 2010 +0200
@@ -19,27 +19,27 @@
| NONE => [th])
| _ => [th]
in case concl_of th of
- Const("Trueprop",_) $ P =>
+ Const(@{const_name Trueprop},_) $ P =>
(case P of
Const(@{const_name mem},_) $ a $ b => tryrules mem_pairs b
- | Const("True",_) => []
- | Const("False",_) => []
+ | Const(@{const_name True},_) => []
+ | Const(@{const_name False},_) => []
| A => tryrules conn_pairs A)
| _ => [th]
end;
(*Analyse a rigid formula*)
val ZF_conn_pairs =
- [("Ball", [@{thm bspec}]),
- ("All", [@{thm spec}]),
- ("op -->", [@{thm mp}]),
- ("op &", [@{thm conjunct1}, @{thm conjunct2}])];
+ [(@{const_name Ball}, [@{thm bspec}]),
+ (@{const_name All}, [@{thm spec}]),
+ (@{const_name "op -->"}, [@{thm mp}]),
+ (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
(*Analyse a:b, where b is rigid*)
val ZF_mem_pairs =
- [("Collect", [@{thm CollectD1}, @{thm CollectD2}]),
- (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
- (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
+ [(@{const_name Collect}, [@{thm CollectD1}, @{thm CollectD2}]),
+ (@{const_name Diff}, [@{thm DiffD1}, @{thm DiffD2}]),
+ (@{const_name Int}, [@{thm IntD1}, @{thm IntD2}])];
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);