--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Fri Feb 05 14:39:02 2010 +0100
@@ -106,8 +106,9 @@
\item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
toplevel state.
- \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
- a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
+ \item \verb|Toplevel.theory_of|~\isa{state} selects the
+ background theory of \isa{state}, raises \verb|Toplevel.UNDEF|
+ for an empty toplevel state.
\item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
state if available, otherwise raises \verb|Toplevel.UNDEF|.
@@ -150,16 +151,16 @@
The operational part is represented as the sequential union of a
list of partial functions, which are tried in turn until the first
one succeeds. This acts like an outer case-expression for various
- alternative state transitions. For example, \isakeyword{qed} acts
+ alternative state transitions. For example, \isakeyword{qed} works
differently for a local proofs vs.\ the global ending of the main
proof.
Toplevel transitions are composed via transition transformers.
Internally, Isar commands are put together from an empty transition
- extended by name and source position (and optional source text). It
- is then left to the individual command parser to turn the given
- concrete syntax into a suitable transition transformer that adjoins
- actual operations on a theory or proof state etc.%
+ extended by name and source position. It is then left to the
+ individual command parser to turn the given concrete syntax into a
+ suitable transition transformer that adjoins actual operations on a
+ theory or proof state etc.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -240,7 +241,7 @@
the toplevel itself, and only make sense in interactive mode. Under
normal circumstances, the user encounters these only implicitly as
part of the protocol between the Isabelle/Isar system and a
- user-interface such as ProofGeneral.
+ user-interface such as Proof~General.
\begin{description}
@@ -391,9 +392,7 @@
associated with each theory, by declaring these dependencies in the
theory header as \isa{{\isasymUSES}}, and loading them consecutively
within the theory context. The system keeps track of incoming {\ML}
- sources and associates them with the current theory. The file
- \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
- order to support legacy proof {\ML} proof scripts.
+ sources and associates them with the current theory.
The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
@@ -458,12 +457,14 @@
\item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
up-to-date wrt.\ the external file store, reloading outdated
- ancestors as required.
+ ancestors as required. In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
\item \verb|use_thys| is similar to \verb|use_thy|, but handles
several theories simultaneously. Thus it acts like processing the
import header of a theory, without performing the merge of the
- result, though.
+ result. By loading a whole sub-graph of theories like that, the
+ intrinsic parallelism can be exploited by the system, to speedup
+ loading.
\item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
on theory \isa{A} and all descendants.
@@ -472,7 +473,7 @@
descendants from the theory database.
\item \verb|ThyInfo.begin_theory| is the basic operation behind a
- \isa{{\isasymTHEORY}} header declaration. This is {\ML} functions is
+ \isa{{\isasymTHEORY}} header declaration. This {\ML} function is
normally not invoked directly.
\item \verb|ThyInfo.end_theory| concludes the loading of a theory
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Fri Feb 05 14:39:02 2010 +0100
@@ -18,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Local theory specifications%
+\isamarkupchapter{Local theory specifications \label{ch:local-theory}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Fri Feb 05 14:39:02 2010 +0100
@@ -39,7 +39,9 @@
schematic polymorphism, which is strictly speaking outside the
logic.\footnote{This is the deeper logical reason, why the theory
context \isa{{\isasymTheta}} is separate from the proof context \isa{{\isasymGamma}}
- of the core calculus.}%
+ of the core calculus: type constructors, term constants, and facts
+ (proof constants) may involve arbitrary type schemes, but the type
+ of a locally fixed term parameter is also fixed!}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -57,16 +59,15 @@
internally. The resulting relation is an ordering: reflexive,
transitive, and antisymmetric.
- A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, which represents symbolic
- intersection. Notationally, the curly braces are omitted for
- singleton intersections, i.e.\ any class \isa{c} may be read as
- a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering on type classes is extended to
- sorts according to the meaning of intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff
- \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection
- \isa{{\isacharbraceleft}{\isacharbraceright}} refers to the universal sort, which is the largest
- element wrt.\ the sort order. The intersections of all (finitely
- many) classes declared in the current theory are the minimal
- elements wrt.\ the sort order.
+ A \emph{sort} is a list of type classes written as \isa{s\ {\isacharequal}\ {\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlisub m{\isacharbraceright}}, it represents symbolic intersection. Notationally, the
+ curly braces are omitted for singleton intersections, i.e.\ any
+ class \isa{c} may be read as a sort \isa{{\isacharbraceleft}c{\isacharbraceright}}. The ordering
+ on type classes is extended to sorts according to the meaning of
+ intersections: \isa{{\isacharbraceleft}c\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ c\isactrlisub m{\isacharbraceright}\ {\isasymsubseteq}\ {\isacharbraceleft}d\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ d\isactrlisub n{\isacharbraceright}} iff \isa{{\isasymforall}j{\isachardot}\ {\isasymexists}i{\isachardot}\ c\isactrlisub i\ {\isasymsubseteq}\ d\isactrlisub j}. The empty intersection \isa{{\isacharbraceleft}{\isacharbraceright}} refers to
+ the universal sort, which is the largest element wrt.\ the sort
+ order. Thus \isa{{\isacharbraceleft}{\isacharbraceright}} represents the ``full sort'', not the
+ empty one! The intersection of all (finitely many) classes declared
+ in the current theory is the least element wrt.\ the sort ordering.
\medskip A \emph{fixed type variable} is a pair of a basic name
(starting with a \isa{{\isacharprime}} character) and a sort constraint, e.g.\
@@ -76,10 +77,10 @@
printed as \isa{{\isacharquery}{\isasymalpha}\isactrlisub s}.
Note that \emph{all} syntactic components contribute to the identity
- of type variables, including the sort constraint. The core logic
- handles type variables with the same name but different sorts as
- different, although some outer layers of the system make it hard to
- produce anything like this.
+ of type variables: basic name, index, and sort constraint. The core
+ logic handles type variables with the same name but different sorts
+ as different, although the type-inference layer (which is outside
+ the core) rejects anything like that.
A \emph{type constructor} \isa{{\isasymkappa}} is a \isa{k}-ary operator
on types declared in the theory. Type constructor application is
@@ -90,8 +91,8 @@
Further notation is provided for specific constructors, notably the
right-associative infix \isa{{\isasymalpha}\ {\isasymRightarrow}\ {\isasymbeta}} instead of \isa{{\isacharparenleft}{\isasymalpha}{\isacharcomma}\ {\isasymbeta}{\isacharparenright}fun}.
- A \emph{type} is defined inductively over type variables and type
- constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}{\isasymkappa}}.
+ The logical category \emph{type} is defined inductively over type
+ variables and type constructors as follows: \isa{{\isasymtau}\ {\isacharequal}\ {\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharquery}{\isasymalpha}\isactrlisub s\ {\isacharbar}\ {\isacharparenleft}{\isasymtau}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlsub k{\isacharparenright}{\isasymkappa}}.
A \emph{type abbreviation} is a syntactic definition \isa{{\isacharparenleft}\isactrlvec {\isasymalpha}{\isacharparenright}{\isasymkappa}\ {\isacharequal}\ {\isasymtau}} of an arbitrary type expression \isa{{\isasymtau}} over
variables \isa{\isactrlvec {\isasymalpha}}. Type abbreviations appear as type
@@ -127,9 +128,9 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML type}{class}\verb|type class| \\
- \indexdef{}{ML type}{sort}\verb|type sort| \\
- \indexdef{}{ML type}{arity}\verb|type arity| \\
+ \indexdef{}{ML type}{class}\verb|type class = string| \\
+ \indexdef{}{ML type}{sort}\verb|type sort = class list| \\
+ \indexdef{}{ML type}{arity}\verb|type arity = string * sort list * sort| \\
\indexdef{}{ML type}{typ}\verb|type typ| \\
\indexdef{}{ML}{map\_atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
\indexdef{}{ML}{fold\_atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
@@ -147,14 +148,14 @@
\begin{description}
- \item \verb|class| represents type classes; this is an alias for
- \verb|string|.
+ \item \verb|class| represents type classes.
- \item \verb|sort| represents sorts; this is an alias for
- \verb|class list|.
+ \item \verb|sort| represents sorts, i.e.\ finite intersections
+ of classes. The empty list \verb|[]: sort| refers to the empty
+ class intersection, i.e.\ the ``full sort''.
- \item \verb|arity| represents type arities; this is an alias for
- triples of the form \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}} for \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} described above.
+ \item \verb|arity| represents type arities. A triple \isa{{\isacharparenleft}{\isasymkappa}{\isacharcomma}\ \isactrlvec s{\isacharcomma}\ s{\isacharparenright}\ {\isacharcolon}\ arity} represents \isa{{\isasymkappa}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}s} as
+ described above.
\item \verb|typ| represents types; this is a datatype with
constructors \verb|TFree|, \verb|TVar|, \verb|Type|.
@@ -207,13 +208,13 @@
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
or \cite{paulson-ml2}), with the types being determined by the
corresponding binders. In contrast, free variables and constants
- are have an explicit name and type in each occurrence.
+ have an explicit name and type in each occurrence.
\medskip A \emph{bound variable} is a natural number \isa{b},
which accounts for the number of intermediate binders between the
variable occurrence in the body and its binding position. For
- example, the de-Bruijn term \isa{{\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub nat\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isacharplus}\ {\isadigit{0}}} would
- correspond to \isa{{\isasymlambda}x\isactrlbsub nat\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub nat\isactrlesub {\isachardot}\ x\ {\isacharplus}\ y} in a named
+ example, the de-Bruijn term \isa{{\isasymlambda}\isactrlbsub bool\isactrlesub {\isachardot}\ {\isasymlambda}\isactrlbsub bool\isactrlesub {\isachardot}\ {\isadigit{1}}\ {\isasymand}\ {\isadigit{0}}} would
+ correspond to \isa{{\isasymlambda}x\isactrlbsub bool\isactrlesub {\isachardot}\ {\isasymlambda}y\isactrlbsub bool\isactrlesub {\isachardot}\ x\ {\isasymand}\ y} in a named
representation. Note that a bound variable may be represented by
different de-Bruijn indices at different occurrences, depending on
the nesting of abstractions.
@@ -225,19 +226,23 @@
without any loose variables.
A \emph{fixed variable} is a pair of a basic name and a type, e.g.\
- \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}}. A
+ \isa{{\isacharparenleft}x{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed \isa{x\isactrlisub {\isasymtau}} here. A
\emph{schematic variable} is a pair of an indexname and a type,
- e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.
+ e.g.\ \isa{{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is likewise printed as \isa{{\isacharquery}x\isactrlisub {\isasymtau}}.
\medskip A \emph{constant} is a pair of a basic name and a type,
- e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}. Constants are declared in the context as polymorphic
- families \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances
- \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.
+ e.g.\ \isa{{\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} which is usually printed as \isa{c\isactrlisub {\isasymtau}}
+ here. Constants are declared in the context as polymorphic families
+ \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}, meaning that all substitution instances \isa{c\isactrlisub {\isasymtau}} for \isa{{\isasymtau}\ {\isacharequal}\ {\isasymsigma}{\isasymvartheta}} are valid.
- The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}}
- wrt.\ the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of
- the matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}. Within a given theory context,
- there is a one-to-one correspondence between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments. For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to \isa{plus{\isacharparenleft}nat{\isacharparenright}}.
+ The vector of \emph{type arguments} of constant \isa{c\isactrlisub {\isasymtau}} wrt.\
+ the declaration \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} is defined as the codomain of the
+ matcher \isa{{\isasymvartheta}\ {\isacharequal}\ {\isacharbraceleft}{\isacharquery}{\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymmapsto}\ {\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isacharquery}{\isasymalpha}\isactrlisub n\ {\isasymmapsto}\ {\isasymtau}\isactrlisub n{\isacharbraceright}} presented in
+ canonical order \isa{{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}}, corresponding to the
+ left-to-right occurrences of the \isa{{\isasymalpha}\isactrlisub i} in \isa{{\isasymsigma}}.
+ Within a given theory context, there is a one-to-one correspondence
+ between any constant \isa{c\isactrlisub {\isasymtau}} and the application \isa{c{\isacharparenleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharparenright}} of its type arguments. For example, with \isa{plus\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}}, the instance \isa{plus\isactrlbsub nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat\isactrlesub } corresponds to
+ \isa{plus{\isacharparenleft}nat{\isacharparenright}}.
Constant declarations \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} may contain sort constraints
for type variables in \isa{{\isasymsigma}}. These are observed by
@@ -246,13 +251,12 @@
polymorphic constants that the user-level type-checker would reject
due to violation of type class restrictions.
- \medskip An \emph{atomic} term is either a variable or constant. A
- \emph{term} is defined inductively over atomic terms, with
- abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}.
- Parsing and printing takes care of converting between an external
- representation with named bound variables. Subsequently, we shall
- use the latter notation instead of internal de-Bruijn
- representation.
+ \medskip An \emph{atomic} term is either a variable or constant.
+ The logical category \emph{term} is defined inductively over atomic
+ terms, with abstraction and application as follows: \isa{t\ {\isacharequal}\ b\ {\isacharbar}\ x\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isacharquery}x\isactrlisub {\isasymtau}\ {\isacharbar}\ c\isactrlisub {\isasymtau}\ {\isacharbar}\ {\isasymlambda}\isactrlisub {\isasymtau}{\isachardot}\ t\ {\isacharbar}\ t\isactrlisub {\isadigit{1}}\ t\isactrlisub {\isadigit{2}}}. Parsing and printing takes care of
+ converting between an external representation with named bound
+ variables. Subsequently, we shall use the latter notation instead
+ of internal de-Bruijn representation.
The inductive relation \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} assigns a (unique) type to a
term according to the structure of atomic terms, abstractions, and
@@ -273,16 +277,17 @@
variables, and declarations for polymorphic constants.
The identity of atomic terms consists both of the name and the type
- component. This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after type
- instantiation. Some outer layers of the system make it hard to
- produce variables of the same name, but different types. In
- contrast, mixed instances of polymorphic constants occur frequently.
+ component. This means that different variables \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{1}}\isactrlesub } and \isa{x\isactrlbsub {\isasymtau}\isactrlisub {\isadigit{2}}\isactrlesub } may become the same after
+ type instantiation. Type-inference rejects variables of the same
+ name, but different types. In contrast, mixed instances of
+ polymorphic constants occur routinely.
\medskip The \emph{hidden polymorphism} of a term \isa{t\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}
is the set of type variables occurring in \isa{t}, but not in
- \isa{{\isasymsigma}}. This means that the term implicitly depends on type
- arguments that are not accounted in the result type, i.e.\ there are
- different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This slightly
+ its type \isa{{\isasymsigma}}. This means that the term implicitly depends
+ on type arguments that are not accounted in the result type, i.e.\
+ there are different type instances \isa{t{\isasymvartheta}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} and
+ \isa{t{\isasymvartheta}{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with the same type. This slightly
pathological situation notoriously demands additional care.
\medskip A \emph{term abbreviation} is a syntactic definition \isa{c\isactrlisub {\isasymsigma}\ {\isasymequiv}\ t} of a closed term \isa{t} of type \isa{{\isasymsigma}},
@@ -435,14 +440,14 @@
\infer[\isa{{\isacharparenleft}assume{\isacharparenright}}]{\isa{A\ {\isasymturnstile}\ A}}{}
\]
\[
- \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}
+ \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}x{\isacharbrackright}} & \isa{x\ {\isasymnotin}\ {\isasymGamma}}}
\qquad
- \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}
+ \infer[\isa{{\isacharparenleft}{\isasymAnd}{\isasymdash}elim{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isasymturnstile}\ b{\isacharbrackleft}a{\isacharbrackright}}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ b{\isacharbrackleft}x{\isacharbrackright}}}
\]
\[
- \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+ \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}intro{\isacharparenright}}]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
\qquad
- \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isacharunderscore}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}}
+ \infer[\isa{{\isacharparenleft}{\isasymLongrightarrow}{\isasymdash}elim{\isacharparenright}}]{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymunion}\ {\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ B}}{\isa{{\isasymGamma}\isactrlsub {\isadigit{1}}\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B} & \isa{{\isasymGamma}\isactrlsub {\isadigit{2}}\ {\isasymturnstile}\ A}}
\]
\caption{Primitive inferences of Pure}\label{fig:prim-rules}
\end{center}
@@ -469,17 +474,18 @@
terms, and \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} for proofs (cf.\
\cite{Berghofer-Nipkow:2000:TPHOL}).
- Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isacharunderscore}intro}) need
- not be recorded in the hypotheses, because the simple syntactic
- types of Pure are always inhabitable. ``Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for type-membership are only present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement body.\footnote{This is the key
- difference to ``\isa{{\isasymlambda}HOL}'' in the PTS framework
- \cite{Barendregt-Geuvers:2001}, where hypotheses \isa{x\ {\isacharcolon}\ A} are
- treated uniformly for propositions and types.}
+ Observe that locally fixed parameters (as in \isa{{\isasymAnd}{\isasymdash}intro}) need not be recorded in the hypotheses, because
+ the simple syntactic types of Pure are always inhabitable.
+ ``Assumptions'' \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} for type-membership are only
+ present as long as some \isa{x\isactrlisub {\isasymtau}} occurs in the statement
+ body.\footnote{This is the key difference to ``\isa{{\isasymlambda}HOL}'' in
+ the PTS framework \cite{Barendregt-Geuvers:2001}, where hypotheses
+ \isa{x\ {\isacharcolon}\ A} are treated uniformly for propositions and types.}
\medskip The axiomatization of a theory is implicitly closed by
forming all instances of type and term variables: \isa{{\isasymturnstile}\ A{\isasymvartheta}} holds for any substitution instance of an axiom
\isa{{\isasymturnstile}\ A}. By pushing substitutions through derivations
- inductively, we also get admissible \isa{generalize} and \isa{instance} rules as shown in \figref{fig:subst-rules}.
+ inductively, we also get admissible \isa{generalize} and \isa{instantiate} rules as shown in \figref{fig:subst-rules}.
\begin{figure}[htb]
\begin{center}
@@ -586,11 +592,11 @@
Every \verb|thm| value contains a sliding back-reference to the
enclosing theory, cf.\ \secref{sec:context-theory}.
- \item \verb|proofs| determines the detail of proof recording within
+ \item \verb|proofs| specifies the detail of proof recording within
\verb|thm| values: \verb|0| records only the names of oracles,
\verb|1| records oracle names and propositions, \verb|2| additionally
records full proof terms. Officially named theorems that contribute
- to a result are always recorded.
+ to a result are recorded in any case.
\item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|
correspond to the primitive inferences of \figref{fig:prim-rules}.
@@ -646,8 +652,8 @@
\begin{figure}[htb]
\begin{center}
\begin{tabular}{ll}
- \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}}) \\
- \isa{{\isasymturnstile}\ A\ {\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]
+ \isa{conjunction\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop\ {\isasymRightarrow}\ prop} & (infix \isa{{\isacharampersand}{\isacharampersand}{\isacharampersand}}) \\
+ \isa{{\isasymturnstile}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}C{\isachardot}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isacharparenright}} \\[1ex]
\isa{prop\ {\isacharcolon}{\isacharcolon}\ prop\ {\isasymRightarrow}\ prop} & (prefix \isa{{\isacharhash}}, suppressed) \\
\isa{{\isacharhash}A\ {\isasymequiv}\ A} \\[1ex]
\isa{term\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymRightarrow}\ prop} & (prefix \isa{TERM}) \\
@@ -659,12 +665,15 @@
\end{center}
\end{figure}
- Derived conjunction rules include introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}\ B}, and destructions \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}\ B\ {\isasymLongrightarrow}\ B}.
- Conjunction allows to treat simultaneous assumptions and conclusions
- uniformly. For example, multiple claims are intermediately
- represented as explicit conjunction, but this is refined into
- separate sub-goals before the user continues the proof; the final
- result is projected into a list of theorems (cf.\
+ The introduction \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B}, and eliminations
+ (projections) \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ A} and \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B\ {\isasymLongrightarrow}\ B} are
+ available as derived rules. Conjunction allows to treat
+ simultaneous assumptions and conclusions uniformly, e.g.\ consider
+ \isa{A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ D}. In particular, the goal mechanism
+ represents multiple claims as explicit conjunction internally, but
+ this is refined (via backwards introduction) into separate sub-goals
+ before the user commences the proof; the final result is projected
+ into a list of theorems using eliminations (cf.\
\secref{sec:tactical-goals}).
The \isa{prop} marker (\isa{{\isacharhash}}) makes arbitrarily complex
@@ -680,7 +689,7 @@
the unspecified type \isa{{\isasymalpha}\ itself}; it essentially injects the
language of types into that of terms. There is specific notation
\isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} for \isa{TYPE\isactrlbsub {\isasymtau}\ itself\isactrlesub }.
- Although being devoid of any particular meaning, the \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term
+ Although being devoid of any particular meaning, the term \isa{TYPE{\isacharparenleft}{\isasymtau}{\isacharparenright}} accounts for the type \isa{{\isasymtau}} within the term
language. In particular, \isa{TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}} may be used as formal
argument in primitive definitions, in order to circumvent hidden
polymorphism (cf.\ \secref{sec:terms}). For example, \isa{c\ TYPE{\isacharparenleft}{\isasymalpha}{\isacharparenright}\ {\isasymequiv}\ A{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}} defines \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ itself\ {\isasymRightarrow}\ prop} in terms of
@@ -707,10 +716,10 @@
\begin{description}
- \item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}\ B} from \isa{A} and \isa{B}.
+ \item \verb|Conjunction.intr| derives \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B} from \isa{A} and \isa{B}.
\item \verb|Conjunction.elim| derives \isa{A} and \isa{B}
- from \isa{A\ {\isacharampersand}\ B}.
+ from \isa{A\ {\isacharampersand}{\isacharampersand}{\isacharampersand}\ B}.
\item \verb|Drule.mk_term| derives \isa{TERM\ t}.
@@ -792,7 +801,8 @@
prefix of parameters and compound premises, concluding an atomic
proposition. Typical examples are \isa{{\isasymlongrightarrow}}-introduction \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B} or mathematical induction \isa{P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n}. Even deeper nesting occurs in well-founded
induction \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymprec}\ x\ {\isasymLongrightarrow}\ P\ y{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x}, but this
- already marks the limit of rule complexity seen in practice.
+ already marks the limit of rule complexity that is usually seen in
+ practice.
\medskip Regular user-level inferences in Isabelle/Pure always
maintain the following canonical form of results:
@@ -917,9 +927,9 @@
\begin{description}
- \item \isa{rule\isactrlsub {\isadigit{1}}\ RS\ rule\isactrlsub {\isadigit{2}}} resolves \isa{rule\isactrlsub {\isadigit{1}}} with \isa{rule\isactrlsub {\isadigit{2}}} according to the
- \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle explained above. Note that the
- corresponding attribute in the Isar language is called \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}.
+ \item \isa{rule\isactrlsub {\isadigit{1}}\ RS\ rule\isactrlsub {\isadigit{2}}} resolves \isa{rule\isactrlsub {\isadigit{1}}} with \isa{rule\isactrlsub {\isadigit{2}}} according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle
+ explained above. Note that the corresponding rule attribute in the
+ Isar language is called \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}.
\item \isa{rule\ OF\ rules} resolves a list of rules with the
first rule, addressing its premises \isa{{\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ length\ rules}
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Fri Feb 05 14:39:02 2010 +0100
@@ -93,39 +93,46 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{theory} is a data container with explicit name and unique
- identifier. Theories are related by a (nominal) sub-theory
+A \emph{theory} is a data container with explicit name and
+ unique identifier. Theories are related by a (nominal) sub-theory
relation, which corresponds to the dependency graph of the original
construction; each theory is derived from a certain sub-graph of
- ancestor theories.
-
- The \isa{merge} operation produces the least upper bound of two
- theories, which actually degenerates into absorption of one theory
- into the other (due to the nominal sub-theory relation).
+ ancestor theories. To this end, the system maintains a set of
+ symbolic ``identification stamps'' within each theory.
- The \isa{begin} operation starts a new theory by importing
- several parent theories and entering a special \isa{draft} mode,
- which is sustained until the final \isa{end} operation. A draft
- theory acts like a linear type, where updates invalidate earlier
- versions. An invalidated draft is called ``stale''.
+ In order to avoid the full-scale overhead of explicit sub-theory
+ identification of arbitrary intermediate stages, a theory is
+ switched into \isa{draft} mode under certain circumstances. A
+ draft theory acts like a linear type, where updates invalidate
+ earlier versions. An invalidated draft is called \emph{stale}.
- The \isa{checkpoint} operation produces an intermediate stepping
- stone that will survive the next update: both the original and the
- changed theory remain valid and are related by the sub-theory
- relation. Checkpointing essentially recovers purely functional
- theory values, at the expense of some extra internal bookkeeping.
+ The \isa{checkpoint} operation produces a safe stepping stone
+ that will survive the next update without becoming stale: both the
+ old and the new theory remain valid and are related by the
+ sub-theory relation. Checkpointing essentially recovers purely
+ functional theory values, at the expense of some extra internal
+ bookkeeping.
The \isa{copy} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
the copy do not affect the original, neither does the sub-theory
relation hold.
+ The \isa{merge} operation produces the least upper bound of two
+ theories, which actually degenerates into absorption of one theory
+ into the other (according to the nominal sub-theory relation).
+
+ The \isa{begin} operation starts a new theory by importing
+ several parent theories and entering a special mode of nameless
+ incremental updates, until the final \isa{end} operation is
+ performed.
+
\medskip The example in \figref{fig:ex-theory} below shows a theory
graph derived from \isa{Pure}, with theory \isa{Length}
importing \isa{Nat} and \isa{List}. The body of \isa{Length} consists of a sequence of updates, working mostly on
- drafts. Intermediate checkpoints may occur as well, due to the
- history mechanism provided by the Isar top-level, cf.\
- \secref{sec:isar-toplevel}.
+ drafts internally, while transaction boundaries of Isar top-level
+ commands (\secref{sec:isar-toplevel}) are guaranteed to be safe
+ checkpoints.
\begin{figure}[htb]
\begin{center}
@@ -172,9 +179,10 @@
\begin{mldecls}
\indexdef{}{ML type}{theory}\verb|type theory| \\
\indexdef{}{ML}{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
- \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
\indexdef{}{ML}{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
\indexdef{}{ML}{Theory.copy}\verb|Theory.copy: theory -> theory| \\
+ \indexdef{}{ML}{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
+ \indexdef{}{ML}{Theory.begin\_theory}\verb|Theory.begin_theory: string -> theory list -> theory| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{theory\_ref}\verb|type theory_ref| \\
@@ -185,24 +193,31 @@
\begin{description}
\item \verb|theory| represents theory contexts. This is
- essentially a linear type! Most operations destroy the original
- version, which then becomes ``stale''.
+ essentially a linear type, with explicit runtime checking! Most
+ internal theory operations destroy the original version, which then
+ becomes ``stale''.
- \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
- compares theories according to the inherent graph structure of the
- construction. This sub-theory relation is a nominal approximation
- of inclusion (\isa{{\isasymsubseteq}}) of the corresponding content.
-
- \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}}
- absorbs one theory into the other. This fails for unrelated
- theories!
+ \item \verb|Theory.subthy|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} compares theories
+ according to the intrinsic graph structure of the construction.
+ This sub-theory relation is a nominal approximation of inclusion
+ (\isa{{\isasymsubseteq}}) of the corresponding content (according to the
+ semantics of the ML modules that implement the data).
\item \verb|Theory.checkpoint|~\isa{thy} produces a safe
- stepping stone in the linear development of \isa{thy}. The next
- update will result in two related, valid theories.
+ stepping stone in the linear development of \isa{thy}. This
+ changes the old theory, but the next update will result in two
+ related, valid theories.
+
+ \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data. The copy is not related to the original,
+ but the original is unchanged.
- \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} with the same data. The result is not related to the
- original; the original is unchanged.
+ \item \verb|Theory.merge|~\isa{{\isacharparenleft}thy\isactrlsub {\isadigit{1}}{\isacharcomma}\ thy\isactrlsub {\isadigit{2}}{\isacharparenright}} absorbs one theory
+ into the other, without changing \isa{thy\isactrlsub {\isadigit{1}}} or \isa{thy\isactrlsub {\isadigit{2}}}.
+ This version of ad-hoc theory merge fails for unrelated theories!
+
+ \item \verb|Theory.begin_theory|~\isa{name\ parents} constructs
+ a new theory based on the given parents. This {\ML} function is
+ normally not invoked directly.
\item \verb|theory_ref| represents a sliding reference to an
always valid theory; updates on the original are propagated
@@ -229,30 +244,32 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A proof context is a container for pure data with a back-reference
- to the theory it belongs to. The \isa{init} operation creates a
- proof context from a given theory. Modifications to draft theories
- are propagated to the proof context as usual, but there is also an
- explicit \isa{transfer} operation to force resynchronization
- with more substantial updates to the underlying theory. The actual
- context data does not require any special bookkeeping, thanks to the
- lack of destructive features.
+A proof context is a container for pure data with a
+ back-reference to the theory it belongs to. The \isa{init}
+ operation creates a proof context from a given theory.
+ Modifications to draft theories are propagated to the proof context
+ as usual, but there is also an explicit \isa{transfer} operation
+ to force resynchronization with more substantial updates to the
+ underlying theory.
- Entities derived in a proof context need to record inherent logical
+ Entities derived in a proof context need to record logical
requirements explicitly, since there is no separate context
- identification as for theories. For example, hypotheses used in
- primitive derivations (cf.\ \secref{sec:thms}) are recorded
- separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
- sure. Results could still leak into an alien proof context due to
- programming errors, but Isabelle/Isar includes some extra validity
- checks in critical positions, notably at the end of a sub-proof.
+ identification or symbolic inclusion as for theories. For example,
+ hypotheses used in primitive derivations (cf.\ \secref{sec:thms})
+ are recorded separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to
+ make double sure. Results could still leak into an alien proof
+ context due to programming errors, but Isabelle/Isar includes some
+ extra validity checks in critical positions, notably at the end of a
+ sub-proof.
Proof contexts may be manipulated arbitrarily, although the common
discipline is to follow block structure as a mental model: a given
context is extended consecutively, and results are exported back
- into the original context. Note that the Isar proof states model
+ into the original context. Note that an Isar proof state models
block-structured reasoning explicitly, using a stack of proof
- contexts internally.%
+ contexts internally. For various technical reasons, the background
+ theory of an Isar proof state must not be changed while the proof is
+ still under construction!%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -311,7 +328,8 @@
Moreover, there are total operations \isa{theory{\isacharunderscore}of} and \isa{proof{\isacharunderscore}of} to convert a generic context into either kind: a theory
can always be selected from the sum, while a proof context might
- have to be constructed by an ad-hoc \isa{init} operation.%
+ have to be constructed by an ad-hoc \isa{init} operation, which
+ incurs a small runtime overhead.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -376,6 +394,15 @@
\noindent The \isa{empty} value acts as initial default for
\emph{any} theory that does not declare actual data content; \isa{extend} is acts like a unitary version of \isa{merge}.
+ Implementing \isa{merge} can be tricky. The general idea is
+ that \isa{merge\ {\isacharparenleft}data\isactrlsub {\isadigit{1}}{\isacharcomma}\ data\isactrlsub {\isadigit{2}}{\isacharparenright}} inserts those parts of \isa{data\isactrlsub {\isadigit{2}}} into \isa{data\isactrlsub {\isadigit{1}}} that are not yet present, while
+ keeping the general order of things. The \verb|Library.merge|
+ function on plain lists may serve as canonical template.
+
+ Particularly note that shared parts of the data must not be
+ duplicated by naive concatenation, or a theory graph that is like a
+ chain of diamonds would cause an exponential blowup!
+
\paragraph{Proof context data} declarations need to implement the
following SML signature:
@@ -387,15 +414,18 @@
\medskip
\noindent The \isa{init} operation is supposed to produce a pure
- value from the given background theory.
+ value from the given background theory and should be somehow
+ ``immediate''. Whenever a proof context is initialized, which
+ happens frequently, the the system invokes the \isa{init}
+ operation of \emph{all} theory data slots ever declared.
\paragraph{Generic data} provides a hybrid interface for both theory
and proof data. The \isa{init} operation for proof contexts is
predefined to select the current data value from the background
theory.
- \bigskip A data declaration of type \isa{T} results in the
- following interface:
+ \bigskip Any of these data declaration over type \isa{T} result
+ in an ML structure with the following signature:
\medskip
\begin{tabular}{ll}
@@ -405,12 +435,12 @@
\end{tabular}
\medskip
- \noindent These other operations provide access for the particular
- kind of context (theory, proof, or generic context). Note that this
- is a safe interface: there is no other way to access the
- corresponding data slot of a context. By keeping these operations
- private, a component may maintain abstract values authentically,
- without other components interfering.%
+ \noindent These other operations provide exclusive access for the
+ particular kind of context (theory, proof, or generic context).
+ This interface fully observes the ML discipline for types and
+ scopes: there is no other way to access the corresponding data slot
+ of a context. By keeping these operations private, an Isabelle/ML
+ module may maintain abstract values authentically.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -451,16 +481,157 @@
%
\endisadelimmlref
%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example demonstrates theory
+ data: we maintain a set of terms that are supposed to be wellformed
+ wrt.\ the enclosing theory. The public interface is as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ signature\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline
+\ \ sig\isanewline
+\ \ \ \ val\ get{\isacharcolon}\ theory\ {\isacharminus}{\isachargreater}\ term\ list\isanewline
+\ \ \ \ val\ add{\isacharcolon}\ term\ {\isacharminus}{\isachargreater}\ theory\ {\isacharminus}{\isachargreater}\ theory\isanewline
+\ \ end{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent The implementation uses private theory data
+ internally, and only exposes an operation that involves explicit
+ argument checking wrt.\ the given theory.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ structure\ Wellformed{\isacharunderscore}Terms{\isacharcolon}\ WELLFORMED{\isacharunderscore}TERMS\ {\isacharequal}\isanewline
+\ \ struct\isanewline
+\isanewline
+\ \ structure\ Terms\ {\isacharequal}\ Theory{\isacharunderscore}Data\isanewline
+\ \ {\isacharparenleft}\isanewline
+\ \ \ \ type\ T\ {\isacharequal}\ term\ OrdList{\isachardot}T{\isacharsemicolon}\isanewline
+\ \ \ \ val\ empty\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ \ \ val\ extend\ {\isacharequal}\ I{\isacharsemicolon}\isanewline
+\ \ \ \ fun\ merge\ {\isacharparenleft}ts{\isadigit{1}}{\isacharcomma}\ ts{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ OrdList{\isachardot}union\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ ts{\isadigit{1}}\ ts{\isadigit{2}}{\isacharsemicolon}\isanewline
+\ \ {\isacharparenright}\isanewline
+\isanewline
+\ \ val\ get\ {\isacharequal}\ Terms{\isachardot}get{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ add\ raw{\isacharunderscore}t\ thy\ {\isacharequal}\isanewline
+\ \ \ \ let\ val\ t\ {\isacharequal}\ Sign{\isachardot}cert{\isacharunderscore}term\ thy\ raw{\isacharunderscore}t\isanewline
+\ \ \ \ in\ Terms{\isachardot}map\ {\isacharparenleft}OrdList{\isachardot}insert\ TermOrd{\isachardot}fast{\isacharunderscore}term{\isacharunderscore}ord\ t{\isacharparenright}\ thy\ end{\isacharsemicolon}\isanewline
+\isanewline
+\ \ end{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+We use \verb|term OrdList.T| for reasonably efficient
+ representation of a set of terms: all operations are linear in the
+ number of stored elements. Here we assume that our users do not
+ care about the declaration order, since that data structure forces
+ its own arrangement of elements.
+
+ Observe how the \verb|merge| operation joins the data slots of
+ the two constituents: \verb|OrdList.union| prevents duplication of
+ common data from different branches, thus avoiding the danger of
+ exponential blowup. (Plain list append etc.\ must never be used for
+ theory data merges.)
+
+ \medskip Our intended invariant is achieved as follows:
+ \begin{enumerate}
+
+ \item \verb|Wellformed_Terms.add| only admits terms that have passed
+ the \verb|Sign.cert_term| check of the given theory at that point.
+
+ \item Wellformedness in the sense of \verb|Sign.cert_term| is
+ monotonic wrt.\ the sub-theory relation. So our data can move
+ upwards in the hierarchy (via extension or merges), and maintain
+ wellformedness without further checks.
+
+ \end{enumerate}
+
+ Note that all basic operations of the inference kernel (which
+ includes \verb|Sign.cert_term|) observe this monotonicity principle,
+ but other user-space tools don't. For example, fully-featured
+ type-inference via \verb|Syntax.check_term| (cf.\
+ \secref{sec:term-check}) is not necessarily monotonic wrt.\ the
+ background theory, since constraints of term constants can be
+ strengthened by later declarations, for example.
+
+ In most cases, user-space context data does not have to take such
+ invariants too seriously. The situation is different in the
+ implementation of the inference kernel itself, which uses the very
+ same data mechanisms for types, constants, axioms etc.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Names \label{sec:names}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
In principle, a name is just a string, but there are various
- convention for encoding additional structure. For example, ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a qualified name consisting of
- three basic name components. The individual constituents of a name
- may have further substructure, e.g.\ the string
- ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.%
+ conventions for representing additional structure. For example,
+ ``\isa{Foo{\isachardot}bar{\isachardot}baz}'' is considered as a long name consisting of
+ qualifier \isa{Foo{\isachardot}bar} and base name \isa{baz}. The
+ individual constituents of a name may have further substructure,
+ e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single
+ symbol.
+
+ \medskip Subsequently, we shall introduce specific categories of
+ names. Roughly speaking these correspond to logical entities as
+ follows:
+ \begin{itemize}
+
+ \item Basic names (\secref{sec:basic-name}): free and bound
+ variables.
+
+ \item Indexed names (\secref{sec:indexname}): schematic variables.
+
+ \item Long names (\secref{sec:long-name}): constants of any kind
+ (type constructors, term constants, other concepts defined in user
+ space). Such entities are typically managed via name spaces
+ (\secref{sec:name-space}).
+
+ \end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -469,16 +640,16 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{symbol} constitutes the smallest textual unit in Isabelle
- --- raw characters are normally not encountered at all. Isabelle
- strings consist of a sequence of symbols, represented as a packed
- string or a list of strings. Each symbol is in itself a small
- string, which has either one of the following forms:
+A \emph{symbol} constitutes the smallest textual unit in
+ Isabelle --- raw ML characters are normally not encountered at all!
+ Isabelle strings consist of a sequence of symbols, represented as a
+ packed string or an exploded list of strings. Each symbol is in
+ itself a small string, which has either one of the following forms:
\begin{enumerate}
- \item a single ASCII character ``\isa{c}'', for example
- ``\verb,a,'',
+ \item a single ASCII character ``\isa{c}'' or raw byte in the
+ range of 128\dots 255, for example ``\verb,a,'',
\item a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
for example ``\verb,\,\verb,<alpha>,'',
@@ -487,7 +658,7 @@
for example ``\verb,\,\verb,<^bold>,'',
\item a raw symbol ``\verb,\,\verb,<^raw:,\isa{text}\verb,>,''
- where \isa{text} constists of printable characters excluding
+ where \isa{text} consists of printable characters excluding
``\verb,.,'' and ``\verb,>,'', for example
``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
@@ -503,16 +674,25 @@
may occur within regular Isabelle identifiers.
Since the character set underlying Isabelle symbols is 7-bit ASCII
- and 8-bit characters are passed through transparently, Isabelle may
- also process Unicode/UCS data in UTF-8 encoding. Unicode provides
- its own collection of mathematical symbols, but there is no built-in
- link to the standard collection of Isabelle.
+ and 8-bit characters are passed through transparently, Isabelle can
+ also process Unicode/UCS data in UTF-8 encoding.\footnote{When
+ counting precise source positions internally, bytes in the range of
+ 128\dots 191 are ignored. In UTF-8 encoding, this interval covers
+ the additional trailer bytes, so Isabelle happens to count Unicode
+ characters here, not bytes in memory. In ISO-Latin encoding, the
+ ignored range merely includes some extra punctuation characters that
+ even have replacements within the standard collection of Isabelle
+ symbols; the accented letters range is counted properly.} Unicode
+ provides its own collection of mathematical symbols, but within the
+ core Isabelle/ML world there is no link to the standard collection
+ of Isabelle regular symbols.
\medskip Output of Isabelle symbols depends on the print mode
(\secref{print-mode}). For example, the standard {\LaTeX} setup of
the Isabelle document preparation system would present
``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
- ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
+ ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}. On-screen rendering usually works by mapping a finite
+ subset of Isabelle symbols to suitable Unicode characters.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -524,7 +704,7 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol| \\
+ \indexdef{}{ML type}{Symbol.symbol}\verb|type Symbol.symbol = string| \\
\indexdef{}{ML}{Symbol.explode}\verb|Symbol.explode: string -> Symbol.symbol list| \\
\indexdef{}{ML}{Symbol.is\_letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexdef{}{ML}{Symbol.is\_digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
@@ -539,11 +719,14 @@
\begin{description}
\item \verb|Symbol.symbol| represents individual Isabelle
- symbols; this is an alias for \verb|string|.
+ symbols.
\item \verb|Symbol.explode|~\isa{str} produces a symbol list
from the packed form. This function supercedes \verb|String.explode| for virtually all purposes of manipulating text in
- Isabelle!
+ Isabelle!\footnote{The runtime overhead for exploded strings is
+ mainly that of the list structure: individual symbols that happen to
+ be a singleton string --- which is the most common case --- do not
+ require extra memory in Poly/ML.}
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify standard
symbols according to fixed syntactic conventions of Isabelle, cf.\
@@ -555,7 +738,16 @@
\item \verb|Symbol.decode| converts the string representation of a
symbol into the datatype version.
- \end{description}%
+ \end{description}
+
+ \paragraph{Historical note.} In the original SML90 standard the
+ primitive ML type \verb|char| did not exists, and the basic \verb|explode: string -> string list| operation would produce a list of
+ singleton strings as in Isabelle/ML today. When SML97 came out,
+ Isabelle did not adopt its slightly anachronistic 8-bit characters,
+ but the idea of exploding a string into a list of small strings was
+ extended to ``symbols'' as explained above. Thus Isabelle sources
+ can refer to an infinite store of user-defined symbols, without
+ having to worry about the multitude of Unicode encodings.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -566,7 +758,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Basic names \label{sec:basic-names}%
+\isamarkupsubsection{Basic names \label{sec:basic-name}%
}
\isamarkuptrue%
%
@@ -583,7 +775,8 @@
These special versions provide copies of the basic name space, apart
from anything that normally appears in the user text. For example,
system generated variables in Isar proof contexts are usually marked
- as internal, which prevents mysterious name references like \isa{xaa} to appear in the text.
+ as internal, which prevents mysterious names like \isa{xaa} to
+ appear in human-readable text.
\medskip Manipulating binding scopes often requires on-the-fly
renamings. A \emph{name context} contains a collection of already
@@ -618,6 +811,9 @@
\indexdef{}{ML}{Name.invents}\verb|Name.invents: Name.context -> string -> int -> string list| \\
\indexdef{}{ML}{Name.variants}\verb|Name.variants: string list -> Name.context -> string list * Name.context| \\
\end{mldecls}
+ \begin{mldecls}
+ \indexdef{}{ML}{Variable.names\_of}\verb|Variable.names_of: Proof.context -> Name.context| \\
+ \end{mldecls}
\begin{description}
@@ -638,6 +834,14 @@
\item \verb|Name.variants|~\isa{names\ context} produces fresh
variants of \isa{names}; the result is entered into the context.
+ \item \verb|Variable.names_of|~\isa{ctxt} retrieves the context
+ of declared type and term variable names. Projecting a proof
+ context down to a primitive name context is occasionally useful when
+ invoking lower-level operations. Regular management of ``fresh
+ variables'' is done by suitable operations of structure \verb|Variable|, which is also able to provide an official status of
+ ``locally fixed variable'' within the logical environment (cf.\
+ \secref{sec:variables}).
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -649,7 +853,7 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Indexed names%
+\isamarkupsubsection{Indexed names \label{sec:indexname}%
}
\isamarkuptrue%
%
@@ -663,9 +867,9 @@
\isa{maxidx\ {\isacharplus}\ {\isadigit{1}}}; the maximum index of an empty collection is
\isa{{\isacharminus}{\isadigit{1}}}.
- Occasionally, basic names and indexed names are injected into the
- same pair type: the (improper) indexname \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used
- to encode basic names.
+ Occasionally, basic names are injected into the same pair type of
+ indexed names: then \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}} is used to encode the basic
+ name \isa{x}.
\medskip Isabelle syntax observes the following rules for
representing an indexname \isa{{\isacharparenleft}x{\isacharcomma}\ i{\isacharparenright}} as a packed string:
@@ -680,11 +884,12 @@
\end{itemize}
- Indexnames may acquire large index numbers over time. Results are
- normalized towards \isa{{\isadigit{0}}} at certain checkpoints, notably at
- the end of a proof. This works by producing variants of the
- corresponding basic name components. For example, the collection
- \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}} becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
+ Indexnames may acquire large index numbers after several maxidx
+ shifts have been applied. Results are usually normalized towards
+ \isa{{\isadigit{0}}} at certain checkpoints, notably at the end of a proof.
+ This works by producing variants of the corresponding basic name
+ components. For example, the collection \isa{{\isacharquery}x{\isadigit{1}}{\isacharcomma}\ {\isacharquery}x{\isadigit{7}}{\isacharcomma}\ {\isacharquery}x{\isadigit{4}}{\isadigit{2}}}
+ becomes \isa{{\isacharquery}x{\isacharcomma}\ {\isacharquery}xa{\isacharcomma}\ {\isacharquery}xb}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -704,7 +909,8 @@
\item \verb|indexname| represents indexed names. This is an
abbreviation for \verb|string * int|. The second component is
usually non-negative, except for situations where \isa{{\isacharparenleft}x{\isacharcomma}\ {\isacharminus}{\isadigit{1}}{\isacharparenright}}
- is used to embed basic names into this type.
+ is used to inject basic names into this type. Other negative
+ indexes should not be used.
\end{description}%
\end{isamarkuptext}%
@@ -717,56 +923,31 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Qualified names and name spaces%
+\isamarkupsubsection{Long names \label{sec:long-name}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A \emph{qualified name} consists of a non-empty sequence of basic
- name components. The packed representation uses a dot as separator,
- as in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base}
- name, the remaining prefix \emph{qualifier} (which may be empty).
- The idea of qualified names is to encode nested structures by
- recording the access paths as qualifiers. For example, an item
- named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as a local entity \isa{c}, within a local structure \isa{b}, within a global
- structure \isa{A}. Typically, name space hierarchies consist of
- 1--2 levels of qualification, but this need not be always so.
+A \emph{long name} consists of a sequence of non-empty name
+ components. The packed representation uses a dot as separator, as
+ in ``\isa{A{\isachardot}b{\isachardot}c}''. The last component is called \emph{base
+ name}, the remaining prefix is called \emph{qualifier} (which may be
+ empty). The qualifier can be understood as the access path to the
+ named entity while passing through some nested block-structure,
+ although our free-form long names do not really enforce any strict
+ discipline.
+
+ For example, an item named ``\isa{A{\isachardot}b{\isachardot}c}'' may be understood as
+ a local entity \isa{c}, within a local structure \isa{b},
+ within a global structure \isa{A}. In practice, long names
+ usually represent 1--3 levels of qualification. User ML code should
+ not make any assumptions about the particular structure of long
+ names!
The empty name is commonly used as an indication of unnamed
- entities, whenever this makes any sense. The basic operations on
- qualified names are smart enough to pass through such improper names
- unchanged.
-
- \medskip A \isa{naming} policy tells how to turn a name
- specification into a fully qualified internal name (by the \isa{full} operation), and how fully qualified names may be accessed
- externally. For example, the default naming policy is to prefix an
- implicit path: \isa{full\ x} produces \isa{path{\isachardot}x}, and the
- standard accesses for \isa{path{\isachardot}x} include both \isa{x} and
- \isa{path{\isachardot}x}. Normally, the naming is implicit in the theory or
- proof context; there are separate versions of the corresponding.
-
- \medskip A \isa{name\ space} manages a collection of fully
- internalized names, together with a mapping between external names
- and internal names (in both directions). The corresponding \isa{intern} and \isa{extern} operations are mostly used for
- parsing and printing only! The \isa{declare} operation augments
- a name space according to the accesses determined by the naming
- policy.
-
- \medskip As a general principle, there is a separate name space for
- each kind of formal entity, e.g.\ logical constant, type
- constructor, type class, theorem. It is usually clear from the
- occurrence in concrete syntax (or from the scope) which kind of
- entity a name refers to. For example, the very same name \isa{c} may be used uniformly for a constant, type constructor, and
- type class.
-
- There are common schemes to name theorems systematically, according
- to the name of the main logical entity involved, e.g.\ \isa{c{\isachardot}intro} for a canonical theorem related to constant \isa{c}.
- This technique of mapping names from one space into another requires
- some care in order to avoid conflicts. In particular, theorem names
- derived from a type constructor or type class are better suffixed in
- addition to the usual qualification, e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro}
- and \isa{c{\isacharunderscore}class{\isachardot}intro} for theorems related to type \isa{c}
- and class \isa{c}, respectively.%
+ entities, or entities that are not entered into the corresponding
+ name space, whenever this makes any sense. The basic operations on
+ long names map empty names again to empty names.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -784,6 +965,100 @@
\indexdef{}{ML}{Long\_Name.implode}\verb|Long_Name.implode: string list -> string| \\
\indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
\end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Long_Name.base_name|~\isa{name} returns the base name
+ of a long name.
+
+ \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
+ of a long name.
+
+ \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}} appends two long
+ names.
+
+ \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
+ representation and the explicit list form of long names.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Name spaces \label{sec:name-space}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A \isa{name\ space} manages a collection of long names,
+ together with a mapping between partially qualified external names
+ and fully qualified internal names (in both directions). Note that
+ the corresponding \isa{intern} and \isa{extern} operations
+ are mostly used for parsing and printing only! The \isa{declare} operation augments a name space according to the accesses
+ determined by a given binding, and a naming policy from the context.
+
+ \medskip A \isa{binding} specifies details about the prospective
+ long name of a newly introduced formal entity. It consists of a
+ base name, prefixes for qualification (separate ones for system
+ infrastructure and user-space mechanisms), a slot for the original
+ source position, and some additional flags.
+
+ \medskip A \isa{naming} provides some additional details for
+ producing a long name from a binding. Normally, the naming is
+ implicit in the theory or proof context. The \isa{full}
+ operation (and its variants for different context types) produces a
+ fully qualified internal name to be entered into a name space. The
+ main equation of this ``chemical reaction'' when binding new
+ entities in a context is as follows:
+
+ \smallskip
+ \begin{tabular}{l}
+ \isa{binding\ {\isacharplus}\ naming\ {\isasymlongrightarrow}\ long\ name\ {\isacharplus}\ name\ space\ accesses}
+ \end{tabular}
+ \smallskip
+
+ \medskip As a general principle, there is a separate name space for
+ each kind of formal entity, e.g.\ fact, logical constant, type
+ constructor, type class. It is usually clear from the occurrence in
+ concrete syntax (or from the scope) which kind of entity a name
+ refers to. For example, the very same name \isa{c} may be used
+ uniformly for a constant, type constructor, and type class.
+
+ There are common schemes to name derived entities systematically
+ according to the name of the main logical entity involved, e.g.\
+ fact \isa{c{\isachardot}intro} for a canonical introduction rule related to
+ constant \isa{c}. This technique of mapping names from one
+ space into another requires some care in order to avoid conflicts.
+ In particular, theorem names derived from a type constructor or type
+ class are better suffixed in addition to the usual qualification,
+ e.g.\ \isa{c{\isacharunderscore}type{\isachardot}intro} and \isa{c{\isacharunderscore}class{\isachardot}intro} for
+ theorems related to type \isa{c} and class \isa{c},
+ respectively.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexdef{}{ML type}{binding}\verb|type binding| \\
+ \indexdef{}{ML}{Binding.empty}\verb|Binding.empty: binding| \\
+ \indexdef{}{ML}{Binding.name}\verb|Binding.name: string -> binding| \\
+ \indexdef{}{ML}{Binding.qualify}\verb|Binding.qualify: bool -> string -> binding -> binding| \\
+ \indexdef{}{ML}{Binding.prefix}\verb|Binding.prefix: bool -> string -> binding -> binding| \\
+ \indexdef{}{ML}{Binding.conceal}\verb|Binding.conceal: binding -> binding| \\
+ \indexdef{}{ML}{Binding.str\_of}\verb|Binding.str_of: binding -> string| \\
+ \end{mldecls}
\begin{mldecls}
\indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
\indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\
@@ -798,21 +1073,39 @@
\verb| string * Name_Space.T| \\
\indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
\indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\
+ \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
\end{mldecls}
\begin{description}
- \item \verb|Long_Name.base_name|~\isa{name} returns the base name of a
- qualified name.
+ \item \verb|binding| represents the abstract concept of name
+ bindings.
+
+ \item \verb|Binding.empty| is the empty binding.
- \item \verb|Long_Name.qualifier|~\isa{name} returns the qualifier
- of a qualified name.
+ \item \verb|Binding.name|~\isa{name} produces a binding with base
+ name \isa{name}.
+
+ \item \verb|Binding.qualify|~\isa{mandatory\ name\ binding}
+ prefixes qualifier \isa{name} to \isa{binding}. The \isa{mandatory} flag tells if this name component always needs to be
+ given in name space accesses --- this is mostly \isa{false} in
+ practice. Note that this part of qualification is typically used in
+ derived specification mechanisms.
- \item \verb|Long_Name.append|~\isa{name\isactrlisub {\isadigit{1}}\ name\isactrlisub {\isadigit{2}}}
- appends two qualified names.
+ \item \verb|Binding.prefix| is similar to \verb|Binding.qualify|, but
+ affects the system prefix. This part of extra qualification is
+ typically used in the infrastructure for modular specifications,
+ notably ``local theory targets'' (see also \chref{ch:local-theory}).
- \item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
- representation and the explicit list form of qualified names.
+ \item \verb|Binding.conceal|~\isa{binding} indicates that the
+ binding shall refer to an entity that serves foundational purposes
+ only. This flag helps to mark implementation details of
+ specification mechanism etc. Other tools should not depend on the
+ particulars of concealed entities (cf.\ \verb|Name_Space.is_concealed|).
+
+ \item \verb|Binding.str_of|~\isa{binding} produces a string
+ representation for human-readable output, together with some formal
+ markup that might get used in GUI front-ends, for example.
\item \verb|Name_Space.naming| represents the abstract concept of
a naming policy.
@@ -853,6 +1146,10 @@
This operation is mostly for printing! User code should not rely on
the precise result too much.
+ \item \verb|Name_Space.is_concealed|~\isa{space\ name} indicates
+ whether \isa{name} refers to a strictly private entity that
+ other tools are supposed to ignore!
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Fri Feb 05 14:39:02 2010 +0100
@@ -42,9 +42,10 @@
or outside the current scope by providing separate syntactic
categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
\emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}). Incidently, a
- universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring
- an explicit quantifier. The same principle works for type
- variables: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' without demanding a truly polymorphic framework.
+ universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality without requiring an
+ explicit quantifier. The same principle works for type variables:
+ \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}''
+ without demanding a truly polymorphic framework.
\medskip Additional care is required to treat type variables in a
way that facilitates type-inference. In principle, term variables
@@ -113,7 +114,8 @@
\indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
\indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
\verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
- \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\
+ \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline%
+\verb| ((string * cterm) list * cterm) * Proof.context| \\
\end{mldecls}
\begin{description}
@@ -167,6 +169,160 @@
%
\endisadelimmlref
%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example (in theory \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}) shows
+ how to work with fixed term and type parameters work with
+ type-inference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+\isacommand{typedecl}\isamarkupfalse%
+\ foo\ \ %
+\isamarkupcmt{some basic type for testing purposes%
+}
+\isanewline
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}locally\ fixed\ parameters\ {\isacharminus}{\isacharminus}\ no\ type\ assignment\ yet{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isacharcomma}\ y{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}t{\isadigit{1}}{\isacharcolon}\ most\ general\ fixed\ type{\isacharsemicolon}\ t{\isadigit{1}}{\isacharprime}{\isacharcolon}\ most\ general\ arbitrary\ type{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ t{\isadigit{1}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\isanewline
+\ \ val\ t{\isadigit{1}}{\isacharprime}\ {\isacharequal}\ singleton\ {\isacharparenleft}Variable{\isachardot}polymorphic\ ctxt{\isadigit{1}}{\isacharparenright}\ t{\isadigit{1}}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}term\ u\ enforces\ specific\ type\ assignment{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ u\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}foo{\isacharparenright}\ {\isasymequiv}\ y{\isachardoublequote}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}official\ declaration\ of\ u\ {\isacharminus}{\isacharminus}\ propagates\ constraints\ etc{\isachardot}{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{2}}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}declare{\isacharunderscore}term\ u{\isacharsemicolon}\isanewline
+\ \ val\ t{\isadigit{2}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{2}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\ \ {\isacharparenleft}{\isacharasterisk}x{\isacharcolon}{\isacharcolon}foo\ is\ enforced{\isacharasterisk}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+In the above example, the starting context had been derived
+ from the toplevel theory, which means that fixed variables are
+ internalized literally: \verb|x| is mapped again to
+ \verb|x|, and attempting to fix it again in the subsequent
+ context is an error. Alternatively, fixed parameters can be renamed
+ explicitly as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}\ x{\isadigit{2}}{\isacharcomma}\ x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent Subsequent ML code can now work with the invented
+ names of \verb|x1|, \verb|x2|, \verb|x3|, without
+ depending on the details on the system policy for introducing these
+ variants. Recall that within a proof body the system always invents
+ fresh ``skolem constants'', e.g.\ as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}PROP\ XXX{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{3}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{2}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}y{\isadigit{1}}{\isacharcomma}\ y{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{4}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ ctxt{\isadigit{3}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}y{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{oops}\isamarkupfalse%
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent In this situation \verb|Variable.add_fixes| and \verb|Variable.variant_fixes| are very similar, but identical name
+ proposals given in a row are only accepted by the second version.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Assumptions \label{sec:assumptions}%
}
\isamarkuptrue%
@@ -192,21 +348,21 @@
context into a (smaller) outer context, by discharging the
difference of the assumptions as specified by the associated export
rules. Note that the discharged portion is determined by the
- difference contexts, not the facts being exported! There is a
+ difference of contexts, not the facts being exported! There is a
separate flag to indicate a goal context, where the result is meant
to refine an enclosing sub-goal of a structured proof state.
\medskip The most basic export rule discharges assumptions directly
by means of the \isa{{\isasymLongrightarrow}} introduction rule:
\[
- \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+ \infer[(\isa{{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
\]
The variant for goal refinements marks the newly introduced
premises, which causes the canonical Isar goal refinement scheme to
enforce unification with local premises within the goal:
\[
- \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+ \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
\]
\medskip Alternative versions of assumptions may perform arbitrary
@@ -215,7 +371,7 @@
definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
with the following export rule to reverse the effect:
\[
- \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
+ \infer[(\isa{{\isasymequiv}{\isasymdash}expand})]{\isa{{\isasymGamma}\ {\isacharminus}\ {\isacharparenleft}x\ {\isasymequiv}\ t{\isacharparenright}\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
\]
This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
a context with \isa{x} being fresh, so \isa{x} does not
@@ -247,8 +403,8 @@
where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
simultaneously.
- \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
- \isa{A{\isacharprime}} is in HHF normal form.
+ \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a primitive assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the
+ conclusion \isa{A{\isacharprime}} is in HHF normal form.
\item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
by assumptions \isa{As} with export rule \isa{r}. The
@@ -256,7 +412,8 @@
\verb|Assumption.assume|.
\item \verb|Assumption.add_assumes|~\isa{As} is a special case of
- \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.
+ \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isasymdash}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro}, depending on goal
+ mode.
\item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm}
exports result \isa{thm} from the the \isa{inner} context
@@ -276,7 +433,68 @@
%
\endisadelimmlref
%
-\isamarkupsection{Results \label{sec:results}%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example demonstrates how rules can be
+ derived by building up a context of assumptions first, and exporting
+ some local fact afterwards. We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
+ here for testing purposes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}eq{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Assumption{\isachardot}add{\isacharunderscore}assumes\ {\isacharbrackleft}%
+\isaantiq
+cprop\ {\isachardoublequote}x\ {\isasymequiv}\ y{\isachardoublequote}%
+\endisaantiq
+{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ val\ eq{\isacharprime}\ {\isacharequal}\ Thm{\isachardot}symmetric\ eq{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}back\ to\ original\ context\ {\isacharminus}{\isacharminus}\ discharges\ assumption{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ r\ {\isacharequal}\ Assumption{\isachardot}export\ false\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ eq{\isacharprime}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent Note that the variables of the resulting rule are
+ not generalized. This would have required to fix them properly in
+ the context beforehand, and export wrt.\ variables afterwards (cf.\
+ \verb|Variable.export| or the combined \verb|ProofContext.export|).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structured goals and results \label{sec:struct-goals}%
}
\isamarkuptrue%
%
@@ -296,6 +514,9 @@
the tactic needs to solve the conclusion, but may use the premise as
a local fact, for locally fixed variables.
+ The family of \isa{FOCUS} combinators is similar to \isa{SUBPROOF}, but allows to retain schematic variables and pending
+ subgoals in the resulting goal state.
+
The \isa{prove} operation provides an interface for structured
backwards reasoning under program control, with some explicit sanity
checks of the result. The goal context can be augmented by
@@ -308,7 +529,8 @@
The \isa{obtain} operation produces results by eliminating
existing facts by means of a given tactic. This acts like a dual
conclusion: the proof demonstrates that the context may be augmented
- by certain fixed variables and assumptions. See also
+ by parameters and assumptions, without affecting any conclusions
+ that do not mention these parameters. See also
\cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
\isa{{\isasymGUESS}} elements. Final results, which may not refer to
the parameters in the conclusion, need to exported explicitly into
@@ -325,7 +547,11 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{Subgoal.FOCUS\_PARAMS}\verb|Subgoal.FOCUS_PARAMS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
\end{mldecls}
+
\begin{mldecls}
\indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
@@ -345,6 +571,11 @@
schematic parameters of the goal are imported into the context as
fixed ones, which may not be instantiated in the sub-proof.
+ \item \verb|Subgoal.FOCUS|, \verb|Subgoal.FOCUS_PREMS|, and \verb|Subgoal.FOCUS_PARAMS| are similar to \verb|SUBPROOF|, but are
+ slightly more flexible: only the specified parts of the subgoal are
+ imported into the context, and the body tactic may introduce new
+ subgoals and schematic variables.
+
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
assumptions \isa{As}, and applies tactic \isa{tac} to solve
it. The latter may depend on the local assumptions being presented
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex Fri Feb 05 14:39:02 2010 +0100
@@ -18,7 +18,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Syntax and type-checking%
+\isamarkupchapter{Concrete syntax and type-checking%
}
\isamarkuptrue%
%
@@ -27,6 +27,19 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Parsing and printing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Checking and unchecking \label{sec:term-check}%
+}
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Fri Feb 05 14:39:02 2010 +0100
@@ -23,7 +23,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Tactical reasoning works by refining the initial claim in a
+Tactical reasoning works by refining an initial claim in a
backwards fashion, until a solved form is reached. A \isa{goal}
consists of several subgoals that need to be solved in order to
achieve the main statement; zero subgoals means that the proof may
@@ -54,8 +54,8 @@
nesting rarely exceeds 1--2 in practice.
The main conclusion \isa{C} is internally marked as a protected
- proposition, which is represented explicitly by the notation \isa{{\isacharhash}C}. This ensures that the decomposition into subgoals and main
- conclusion is well-defined for arbitrarily structured claims.
+ proposition, which is represented explicitly by the notation \isa{{\isacharhash}C} here. This ensures that the decomposition into subgoals and
+ main conclusion is well-defined for arbitrarily structured claims.
\medskip Basic goal management is performed via the following
Isabelle/Pure rules:
@@ -129,26 +129,27 @@
supporting memoing.\footnote{The lack of memoing and the strict
nature of SML requires some care when working with low-level
sequence operations, to avoid duplicate or premature evaluation of
- results.}
+ results. It also means that modified runtime behavior, such as
+ timeout, is very hard to achieve for general tactics.}
An \emph{empty result sequence} means that the tactic has failed: in
- a compound tactic expressions other tactics might be tried instead,
+ a compound tactic expression other tactics might be tried instead,
or the whole refinement step might fail outright, producing a
- toplevel error message. When implementing tactics from scratch, one
- should take care to observe the basic protocol of mapping regular
- error conditions to an empty result; only serious faults should
- emerge as exceptions.
+ toplevel error message in the end. When implementing tactics from
+ scratch, one should take care to observe the basic protocol of
+ mapping regular error conditions to an empty result; only serious
+ faults should emerge as exceptions.
By enumerating \emph{multiple results}, a tactic can easily express
the potential outcome of an internal search process. There are also
combinators for building proof tools that involve search
systematically, see also \secref{sec:tacticals}.
- \medskip As explained in \secref{sec:tactical-goals}, a goal state
- essentially consists of a list of subgoals that imply the main goal
- (conclusion). Tactics may operate on all subgoals or on a
- particularly specified subgoal, but must not change the main
- conclusion (apart from instantiating schematic goal variables).
+ \medskip As explained before, a goal state essentially consists of a
+ list of subgoals that imply the main goal (conclusion). Tactics may
+ operate on all subgoals or on a particularly specified subgoal, but
+ must not change the main conclusion (apart from instantiating
+ schematic goal variables).
Tactics with explicit \emph{subgoal addressing} are of the form
\isa{int\ {\isasymrightarrow}\ tactic} and may be applied to a particular subgoal
@@ -170,7 +171,7 @@
Tactics with internal subgoal addressing should expose the subgoal
index as \isa{int} argument in full generality; a hardwired
- subgoal 1 inappropriate.
+ subgoal 1 is not acceptable.
\medskip The main well-formedness conditions for proper tactics are
summarized as follows.
@@ -192,11 +193,11 @@
\end{itemize}
Some of these conditions are checked by higher-level goal
- infrastructure (\secref{sec:results}); others are not checked
+ infrastructure (\secref{sec:struct-goals}); others are not checked
explicitly, and violating them merely results in ill-behaved tactics
experienced by the user (e.g.\ tactics that insist in being
- applicable only to singleton goals, or disallow composition with
- basic tacticals).%
+ applicable only to singleton goals, or prevent composition via
+ standard tacticals).%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -414,7 +415,7 @@
Type instantiations may be given as well, via pairs like \isa{{\isacharparenleft}{\isacharquery}{\isacharprime}a{\isacharcomma}\ {\isasymtau}{\isacharparenright}}. Type instantiations are distinguished from term
instantiations by the syntactic form of the schematic variable.
Types are instantiated before terms are. Since term instantiation
- already performs type-inference as expected, explicit type
+ already performs simple type-inference, so explicit type
instantiations are seldom necessary.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -452,7 +453,13 @@
\item \verb|rename_tac|~\isa{names\ i} renames the innermost
parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers).
- \end{description}%
+ \end{description}
+
+ For historical reasons, the above instantiation tactics take
+ unparsed string arguments, which makes them hard to use in general
+ ML code. The slightly more advanced \verb|Subgoal.FOCUS| combinator
+ of \secref{sec:struct-goals} allows to refer to internal goal
+ structure with explicit context management.%
\end{isamarkuptext}%
\isamarkuptrue%
%