--- a/doc-src/IsarImplementation/Thy/document/integration.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Thu Aug 31 22:55:49 2006 +0200
@@ -30,19 +30,18 @@
\begin{isamarkuptext}%
The Isar toplevel may be considered the centeral hub of the
Isabelle/Isar system, where all key components and sub-systems are
- integrated into a single read-eval-print loop of Isar commands.
- Here we even incorporate the existing {\ML} toplevel of the compiler
+ integrated into a single read-eval-print loop of Isar commands. We
+ shall even incorporate the existing {\ML} toplevel of the compiler
and run-time system (cf.\ \secref{sec:ML-toplevel}).
- Isabelle/Isar departs from original ``LCF system architecture''
+ Isabelle/Isar departs from the original ``LCF system architecture''
where {\ML} was really The Meta Language for defining theories and
- conducting proofs. Instead, {\ML} merely serves as the
+ conducting proofs. Instead, {\ML} now only serves as the
implementation language for the system (and user extensions), while
- our specific Isar toplevel supports particular notions of
- incremental theory and proof development more directly. This
- includes the graph structure of theories and the block structure of
- proofs, support for unlimited undo, facilities for tracing,
- debugging, timing, profiling.
+ the specific Isar toplevel supports the concepts of theory and proof
+ development natively. This includes the graph structure of theories
+ and the block structure of proofs, support for unlimited undo,
+ facilities for tracing, debugging, timing, profiling etc.
\medskip The toplevel maintains an implicit state, which is
transformed by a sequence of transitions -- either interactively or
@@ -50,9 +49,9 @@
encapsulated as safe transactions, such that both failure and undo
are handled conveniently without destroying the underlying draft
theory (cf.~\secref{sec:context-theory}). In batch mode,
- transitions operate in a strictly linear (destructive) fashion, such
- that error conditions abort the present attempt to construct a
- theory altogether.
+ transitions operate in a linear (destructive) fashion, such that
+ error conditions abort the present attempt to construct a theory or
+ proof altogether.
The toplevel state is a disjoint sum of empty \isa{toplevel}, or
\isa{theory}, or \isa{proof}. On entering the main Isar loop we
@@ -96,22 +95,23 @@
\begin{description}
\item \verb|Toplevel.state| represents Isar toplevel states,
- which are normally only manipulated through the toplevel transition
- concept (\secref{sec:toplevel-transition}). Also note that a
- toplevel state is subject to the same linerarity restrictions as a
- theory context (cf.~\secref{sec:context-theory}).
+ which are normally manipulated through the concept of toplevel
+ transitions only (\secref{sec:toplevel-transition}). Also note that
+ a raw toplevel state is subject to the same linearity restrictions
+ as a theory context (cf.~\secref{sec:context-theory}).
\item \verb|Toplevel.UNDEF| is raised for undefined toplevel
- operations: \verb|Toplevel.state| is a sum type, many operations
- work only partially for certain cases.
+ operations. Many operations work only partially for certain cases,
+ since \verb|Toplevel.state| is a sum type.
- \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
+ \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
+ toplevel state.
- \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
- (!), otherwise raises \verb|Toplevel.UNDEF|.
+ \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
+ a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
- \item \verb|Toplevel.proof_of| gets the Isar proof state if
- available, otherwise raises \verb|Toplevel.UNDEF|.
+ \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
+ state if available, otherwise raises \verb|Toplevel.UNDEF|.
\item \verb|set Toplevel.debug| makes the toplevel print further
details about internal error conditions, exceptions being raised
@@ -120,9 +120,10 @@
\item \verb|set Toplevel.timing| makes the toplevel print timing
information for each Isar command being executed.
- \item \verb|Toplevel.profiling| controls low-level profiling of the
- underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
- and 2 space profiling.}
+ \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
+ low-level profiling of the underlying {\ML} runtime system. For
+ Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
+ profiling.
\end{description}%
\end{isamarkuptext}%
@@ -135,31 +136,30 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Toplevel transitions%
+\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-An Isar toplevel transition consists of a partial
- function on the toplevel state, with additional information for
- diagnostics and error reporting: there are fields for command name,
- source position, optional source text, as well as flags for
- interactive-only commands (which issue a warning in batch-mode),
- printing of result state, etc.
+An Isar toplevel transition consists of a partial function on the
+ toplevel state, with additional information for diagnostics and
+ error reporting: there are fields for command name, source position,
+ optional source text, as well as flags for interactive-only commands
+ (which issue a warning in batch-mode), printing of result state,
+ etc.
- The operational part is represented as a sequential union of a list
- of partial functions, which are tried in turn until the first one
- succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|). For example,
- a single Isar command like \isacommand{qed} consists of the union of
- some function \verb|Proof.state -> Proof.state| for proofs
- within proofs, plus \verb|Proof.state -> theory| for proofs at
- the outer theory level.
+ 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 (i.e.\ does not raise \verb|Toplevel.UNDEF|). This acts
+ like an outer case-expression for various alternative state
+ transitions. For example, \isakeyword{qed} acts 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
- syntax body into a suitable transition transformer that adjoin
+ concrete syntax into a suitable transition transformer that adjoin
actual operations on a theory or proof state etc.%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -190,32 +190,36 @@
\begin{description}
- \item \verb|Toplevel.print| sets the print flag, which causes the
- resulting state of the transition to be echoed in interactive mode.
+ \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
+ causes the toplevel loop to echo the result state (in interactive
+ mode).
- \item \verb|Toplevel.no_timing| indicates that the transition should
- never show timing information, e.g.\ because it is merely a
- diagnostic command.
+ \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
+ transition should never show timing information, e.g.\ because it is
+ a diagnostic command.
- \item \verb|Toplevel.keep| adjoins a diagnostic function.
+ \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
+ function.
- \item \verb|Toplevel.theory| adjoins a theory transformer.
+ \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
+ transformer.
- \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
- which turns a theory into a proof state. The theory may be changed
- before entering the proof; the generic Isar goal setup includes an
- argument that specifies how to apply the proven result to the
- theory, when the proof is finished.
+ \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
+ goal function, which turns a theory into a proof state. The theory
+ may be changed before entering the proof; the generic Isar goal
+ setup includes an argument that specifies how to apply the proven
+ result to the theory, when the proof is finished.
- \item \verb|Toplevel.proof| adjoins a deterministic proof command,
- with a singleton result state.
+ \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
+ proof command, with a singleton result.
- \item \verb|Toplevel.proofs| adjoins a general proof command, with
- zero or more result states (represented as a lazy list).
+ \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
+ command, with zero or more result states (represented as a lazy
+ list).
- \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
- command, that returns the resulting theory, after storing the
- resulting facts etc.
+ \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
+ concluding proof command, that returns the resulting theory, after
+ storing the resulting facts etc.
\end{description}%
\end{isamarkuptext}%
@@ -233,12 +237,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Apart from regular toplevel transactions there are a few
- special control commands that modify the behavior 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.
+There are a few special control commands that modify the behavior
+ 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.
\begin{description}
@@ -278,14 +281,15 @@
no clean way to undo {\ML} declarations, except for reverting to a
previously saved state of the whole Isabelle process. {\ML} input
is either read interactively from a TTY, or from a string (usually
- within a theory text), or from a source file (usually associated
- with a theory).
+ within a theory text), or from a source file (usually loaded from a
+ theory).
Whenever the {\ML} toplevel is active, the current Isabelle theory
context is passed as an internal reference variable. Thus {\ML}
code may access the theory context during compilation, it may even
- change the value of a theory being under construction --- following
- the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
+ change the value of a theory being under construction --- while
+ observing the usual linearity restrictions
+ (cf.~\secref{sec:context-theory}).%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -311,28 +315,28 @@
\item \verb|the_context ()| refers to the theory context of the
{\ML} toplevel --- at compile time! {\ML} code needs to take care
- to refer to \verb|the_context ()| correctly, recall that evaluation
- of a function body is delayed until actual runtime. Moreover,
- persistent {\ML} toplevel bindings to an unfinished theory should be
- avoided: code should either project out the desired information
- immediately, or produce an explicit \verb|theory_ref| (cf.\
- \secref{sec:context-theory}).
+ to refer to \verb|the_context ()| correctly. Recall that
+ evaluation of a function body is delayed until actual runtime.
+ Moreover, persistent {\ML} toplevel bindings to an unfinished theory
+ should be avoided: code should either project out the desired
+ information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
\item \verb|Context.>>|~\isa{f} applies theory transformation
\isa{f} to the current theory of the {\ML} toplevel. In order to
work as expected, the theory should be still under construction, and
the Isar language element that invoked the {\ML} compiler in the
- first place shoule be ready to accept the changed theory value
+ first place should be ready to accept the changed theory value
(e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
- Otherwise the theory may get destroyed!
+ Otherwise the theory becomes stale!
\end{description}
It is very important to note that the above functions are really
restricted to the compile time, even though the {\ML} compiler is
invoked at runtime! The majority of {\ML} code uses explicit
- functional arguments of a theory or proof context, as required.
- Thus it may get run in an arbitrary context later on.
+ functional arguments of a theory or proof context instead. Thus it
+ may be invoked for an arbitrary context later on, without having to
+ worry about any operational details.
\bigskip
@@ -347,16 +351,17 @@
\begin{description}
\item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
- initializing the state to empty toplevel state.
+ initializing an empty toplevel state.
\item \verb|Isar.loop ()| continues the Isar toplevel with the
- current state, after dropping out of the Isar toplevel loop.
+ current state, after having dropped out of the Isar toplevel loop.
\item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
- toplevel state and optional error condition, respectively. This
- only works after dropping out of the Isar toplevel loop.
+ toplevel state and error condition, respectively. This only works
+ after having dropped out of the Isar toplevel loop.
- \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
+ \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
+ (\secref{sec:generic-context}).
\end{description}%
\end{isamarkuptext}%
@@ -369,32 +374,30 @@
%
\endisadelimmlref
%
-\isamarkupsection{Theory database%
+\isamarkupsection{Theory database \label{sec:theory-database}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The theory database maintains a collection of theories,
- together with some administrative information about the original
- sources, which are held in an external store (i.e.\ a collection of
- directories within the regular file system of the underlying
- platform).
+The theory database maintains a collection of theories, together
+ with some administrative information about their original sources,
+ which are held in an external store (i.e.\ some directory within the
+ regular file system).
- The theory database is organized as a directed acyclic graph, with
- entries referenced by theory name. Although some external
- interfaces allow to include a directory specification, this is only
- a hint to the underlying theory loader mechanism: the internal
- theory name space is flat.
+ The theory database is organized as a directed acyclic graph;
+ entries are referenced by theory name. Although some additional
+ interfaces allow to include a directory specification as well, this
+ is only a hint to the underlying theory loader. The internal theory
+ name space is flat!
Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
- loader path. A number of optional {\ML} source files may be
+ loader path. Any number of additional {\ML} source files may be
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 special
- theory {\ML} 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 file
+ \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
+ order to support legacy proof {\ML} proof scripts.
The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
@@ -402,29 +405,29 @@
\item \isa{update\ A} introduces a link of \isa{A} with a
\isa{theory} value of the same name; it asserts that the theory
- sources are consistent with that value.
+ sources are now consistent with that value;
\item \isa{outdate\ A} invalidates the link of a theory database
- entry to its sources, but retains the present theory value.
+ entry to its sources, but retains the present theory value;
- \item \isa{remove\ A} removes entry \isa{A} from the theory
+ \item \isa{remove\ A} deletes entry \isa{A} from the theory
database.
\end{itemize}
These actions are propagated to sub- or super-graphs of a theory
- entry in the usual way, in order to preserve global consistency of
- the state of all loaded theories with the sources of the external
- store. This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
- all descendants; \isa{remove} will \isa{remove} all
- descendants.
+ entry as expected, in order to preserve global consistency of the
+ state of all loaded theories with the sources of the external store.
+ This implies certain causalities between actions: \isa{update}
+ or \isa{outdate} of an entry will \isa{outdate} all
+ descendants; \isa{remove} will \isa{remove} all descendants.
\medskip There are separate user-level interfaces to operate on the
theory database directly or indirectly. The primitive actions then
just happen automatically while working with the system. In
- particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
+ particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
- is up-to-date. Earlier theories are reloaded as required, with
+ is up-to-date, too. Earlier theories are reloaded as required, with
\isa{update} actions proceeding in topological order according to
theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
is achieved eventually.%
@@ -442,8 +445,6 @@
\indexml{theory}\verb|theory: string -> theory| \\
\indexml{use-thy}\verb|use_thy: string -> unit| \\
\indexml{update-thy}\verb|update_thy: string -> unit| \\
- \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
- \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
\indexml{touch-thy}\verb|touch_thy: string -> unit| \\
\indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
\indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
@@ -456,8 +457,8 @@
\begin{description}
\item \verb|theory|~\isa{A} retrieves the theory value presently
- associated with \isa{A}. The result is not necessarily
- up-to-date!
+ associated with name \isa{A}. Note that the result might be
+ outdated.
\item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
or out-of-date. It ensures that all parent theories are available
@@ -465,20 +466,12 @@
present.
\item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
- the \isa{A} and all of its ancestors are fully up-to-date.
+ theory \isa{A} and all ancestors are fully up-to-date.
- \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
- but refrains from loading the attached \isa{A}\verb,.ML, file.
- This is occasionally useful in replaying legacy {\ML} proof scripts
- by hand.
-
- \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
- proceeds like \verb|update_thy| for ancestors.
+ \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
+ on theory \isa{A} and all descendants.
- \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
- theory \isa{A} and all of its descendants.
-
- \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
+ \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
descendants from the theory database.
\item \verb|ThyInfo.begin_theory| is the basic operation behind a
@@ -489,22 +482,22 @@
normally not invoked directly.
\item \verb|ThyInfo.end_theory| concludes the loading of a theory
- proper; an attached theory {\ML} file may be still loaded later on.
- This is {\ML} functions is normally not invoked directly.
+ proper. An attached theory {\ML} file may be still loaded later on.
+ This is function is normally not invoked directly.
- \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
- theory value with the theory loader database. There is no
- management of associated sources; this is mainly for bootstrapping.
+ \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
+ existing theory value with the theory loader database. There is no
+ management of associated sources.
\item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
invoked with the action and theory name being involved; thus derived
actions may be performed in associated system components, e.g.\
- maintaining the state of an editor for theory sources.
+ maintaining the state of an editor for the theory sources.
The kind and order of actions occurring in practice depends both on
user interactions and the internal process of resolving theory
imports. Hooks should not rely on a particular policy here! Any
- exceptions raised by the hook are ignored by the theory database.
+ exceptions raised by the hook are ignored.
\end{description}%
\end{isamarkuptext}%
@@ -517,6 +510,15 @@
%
\endisadelimmlref
%
+\isamarkupsection{Sessions and document preparation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/document/locale.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/locale.tex Thu Aug 31 22:55:49 2006 +0200
@@ -32,7 +32,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Locales%
+\isamarkupsection{Type-checking specifications%
}
\isamarkuptrue%
%
@@ -41,6 +41,17 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Localized theory specifications%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+ \glossary{Local theory}{FIXME}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu Aug 31 22:55:49 2006 +0200
@@ -23,11 +23,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Syntax%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Variable names%
+\isamarkupsection{Variable names%
}
\isamarkuptrue%
%
@@ -36,39 +32,41 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Simply-typed lambda calculus%
+\isamarkupsection{Types \label{sec:types}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
+\glossary{Type class}{FIXME}
+
+ \glossary{Type arity}{FIXME}
+
+ \glossary{Sort}{FIXME}
+
+ FIXME classes and sorts
-\glossary{Type}{FIXME}
-\glossary{Term}{FIXME}%
+
+ \glossary{Type}{FIXME}
+
+ \glossary{Type constructor}{FIXME}
+
+ \glossary{Type variable}{FIXME}
+
+ FIXME simple types%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{The order-sorted algebra of types%
+\isamarkupsection{Terms \label{sec:terms}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
-
-\glossary{Type constructor}{FIXME}
-
-\glossary{Type class}{FIXME}
+\glossary{Term}{FIXME}
-\glossary{Type arity}{FIXME}
-
-\glossary{Sort}{FIXME}%
+ FIXME de-Bruijn representation of lambda terms%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Type-inference and schematic polymorphism%
-}
-\isamarkuptrue%
-%
\begin{isamarkuptext}%
FIXME
@@ -78,21 +76,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Theory%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
-theory context, but slightly more flexible since it may be used at
-different type-instances, due to \seeglossary{schematic
-polymorphism.}}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Deduction%
+\isamarkupsection{Theorems \label{sec:thms}%
}
\isamarkuptrue%
%
@@ -171,12 +155,21 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof terms%
+\isamarkupsection{Low-level specifications%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+FIXME
+
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}
+
+\glossary{Axiom}{FIXME}
+
+\glossary{Primitive definition}{FIXME}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Thu Aug 31 22:55:49 2006 +0200
@@ -28,19 +28,20 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A logical context represents the background that is taken for
- granted when formulating statements and composing proofs. It acts
- as a medium to produce formal content, depending on earlier material
- (declarations, results etc.).
+A logical context represents the background that is required for
+ formulating statements and composing proofs. It acts as a medium to
+ produce formal content, depending on earlier material (declarations,
+ results etc.).
- In particular, derivations within the primitive Pure logic can be
- described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, meaning that a
+ For example, derivations within the Isabelle/Pure logic can be
+ described as a judgment \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}, which means that a
proposition \isa{{\isasymphi}} is derivable from hypotheses \isa{{\isasymGamma}}
within the theory \isa{{\isasymTheta}}. There are logical reasons for
- keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories support type
- constructors and schematic polymorphism of constants and axioms,
- while the inner calculus of \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is limited to Simple
- Type Theory (with fixed type variables in the assumptions).
+ keeping \isa{{\isasymTheta}} and \isa{{\isasymGamma}} separate: theories can be
+ liberal about supporting type constructors and schematic
+ polymorphism of constants and axioms, while the inner calculus of
+ \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} is strictly limited to Simple Type Theory (with
+ fixed type variables in the assumptions).
\medskip Contexts and derivations are linked by the following key
principles:
@@ -48,43 +49,43 @@
\begin{itemize}
\item Transfer: monotonicity of derivations admits results to be
- transferred into a larger context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
- implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
+ transferred into a \emph{larger} context, i.e.\ \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\isactrlsub {\isacharprime}\ {\isasymphi}} for contexts \isa{{\isasymTheta}{\isacharprime}\ {\isasymsupseteq}\ {\isasymTheta}} and \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}}.
\item Export: discharge of hypotheses admits results to be exported
- into a smaller context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}} implies
- \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here, only the
- \isa{{\isasymGamma}} part is affected.
+ into a \emph{smaller} context, i.e.\ \isa{{\isasymGamma}{\isacharprime}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}
+ implies \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymDelta}\ {\isasymLongrightarrow}\ {\isasymphi}} where \isa{{\isasymGamma}{\isacharprime}\ {\isasymsupseteq}\ {\isasymGamma}} and
+ \isa{{\isasymDelta}\ {\isacharequal}\ {\isasymGamma}{\isacharprime}\ {\isacharminus}\ {\isasymGamma}}. Note that \isa{{\isasymTheta}} remains unchanged here,
+ only the \isa{{\isasymGamma}} part is affected.
\end{itemize}
- \medskip Isabelle/Isar provides two different notions of abstract
- containers called \emph{theory context} and \emph{proof context},
- respectively. These model the main characteristics of the primitive
- \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, without subscribing to any
- particular kind of content yet. Instead, contexts merely impose a
- certain policy of managing arbitrary \emph{context data}. The
- system provides strongly typed mechanisms to declare new kinds of
+ \medskip By modeling the main characteristics of the primitive
+ \isa{{\isasymTheta}} and \isa{{\isasymGamma}} above, and abstracting over any
+ particular logical content, we arrive at the fundamental notions of
+ \emph{theory context} and \emph{proof context} in Isabelle/Isar.
+ These implement a certain policy to manage arbitrary \emph{context
+ data}. There is a strongly-typed mechanism to declare new kinds of
data at compile time.
- Thus the internal bootstrap process of Isabelle/Pure eventually
- reaches a stage where certain data slots provide the logical content
- of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not
- stop there! Various additional data slots support all kinds of
- mechanisms that are not necessarily part of the core logic.
+ The internal bootstrap process of Isabelle/Pure eventually reaches a
+ stage where certain data slots provide the logical content of \isa{{\isasymTheta}} and \isa{{\isasymGamma}} sketched above, but this does not stop there!
+ Various additional data slots support all kinds of mechanisms that
+ are not necessarily part of the core logic.
For example, there would be data for canonical introduction and
elimination rules for arbitrary operators (depending on the
object-logic and application), which enables users to perform
- standard proof steps implicitly (cf.\ the \isa{rule} method).
+ standard proof steps implicitly (cf.\ the \isa{rule} method
+ \cite{isabelle-isar-ref}).
- Isabelle is able to bring forth more and more concepts successively.
- In particular, an object-logic like Isabelle/HOL continues the
- Isabelle/Pure setup by adding specific components for automated
- reasoning (classical reasoner, tableau prover, structured induction
- etc.) and derived specification mechanisms (inductive predicates,
- recursive functions etc.). All of this is based on the generic data
- management by theory and proof contexts.%
+ \medskip Thus Isabelle/Isar is able to bring forth more and more
+ concepts successively. In particular, an object-logic like
+ Isabelle/HOL continues the Isabelle/Pure setup by adding specific
+ components for automated reasoning (classical reasoner, tableau
+ prover, structured induction etc.) and derived specification
+ mechanisms (inductive predicates, recursive functions etc.). All of
+ this is ultimately based on the generic data management by theory
+ and proof contexts introduced here.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -95,31 +96,27 @@
\begin{isamarkuptext}%
\glossary{Theory}{FIXME}
- Each theory is explicitly named and holds a unique identifier.
- There is a separate \emph{theory reference} for pointing backwards
- to the enclosing theory context of derived entities. Theories are
- related by a (nominal) sub-theory relation, which corresponds to the
- canonical dependency graph: each theory is derived from a certain
- sub-graph of ancestor theories. The \isa{merge} of two theories
- refers to the least upper bound, which actually degenerates into
- absorption of one theory into the other, due to the nominal
- sub-theory relation this.
+ A \emph{theory} is a data container with explicit named 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).
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
- mode theory acts like a linear type, where updates invalidate
- earlier drafts, but theory reference values will be propagated
- automatically. Thus derived entities that ``belong'' to a draft
- might be transferred spontaneously to a larger context. An
- invalidated draft is called ``stale''.
+ theory acts like a linear type, where updates invalidate earlier
+ versions. An invalidated draft is called ``stale''.
The \isa{checkpoint} operation produces an intermediate stepping
- stone that will survive the next update unscathed: 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.
+ 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{copy} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
@@ -127,11 +124,11 @@
relation hold.
\medskip The example in \figref{fig:ex-theory} below shows a theory
- graph derived from \isa{Pure}. Theory \isa{Length} imports
- \isa{Nat} and \isa{List}. The theory body 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}.
+ 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}.
\begin{figure}[htb]
\begin{center}
@@ -152,9 +149,19 @@
& & $\vdots$~~ \\
& & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
\end{tabular}
- \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
+ \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
\end{center}
- \end{figure}%
+ \end{figure}
+
+ \medskip There is a separate notion of \emph{theory reference} for
+ maintaining a live link to an evolving theory context: updates on
+ drafts are propagated automatically. The dynamic stops after an
+ explicit \isa{end} only.
+
+ Derived entities may store a theory reference in order to indicate
+ the context they belong to. This implicitly assumes monotonic
+ reasoning, because the referenced context may become larger without
+ further notice.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -178,9 +185,9 @@
\begin{description}
- \item \verb|theory| represents theory contexts. This is a
- linear type! Most operations destroy the old version, which then
- becomes ``stale''.
+ \item \verb|theory| represents theory contexts. This is
+ essentially a linear type! Most 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
@@ -195,15 +202,15 @@
stepping stone in the linear development of \isa{thy}. The next
update will result in two related, valid theories.
- \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The copy is not related
- to the original, which is not touched at all.
+ \item \verb|Theory.copy|~\isa{thy} produces a variant of \isa{thy} that holds a copy of the same data. The result is not
+ related to the original; the original is unchanched.
- \item \verb|theory_ref| represents a sliding reference to a
- valid theory --- updates on the original are propagated
+ \item \verb|theory_ref| represents a sliding reference to an
+ always valid theory; updates on the original are propagated
automatically.
\item \verb|Theory.self_ref|~\isa{thy} and \verb|Theory.deref|~\isa{thy{\isacharunderscore}ref} convert between \verb|theory| and \verb|theory_ref|. As the referenced theory
- evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to larger contexts.
+ evolves monotonically over time, later invocations of \verb|Theory.deref| may refer to a larger context.
\end{description}%
\end{isamarkuptext}%
@@ -230,28 +237,28 @@
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 derived 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.
+ 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.
Entities derived in a proof context need to record inherent logical
requirements explicitly, since there is no separate context
identification as for theories. For example, hypotheses used in
- primitive derivations (cf.\ \secref{sec:thm}) are recorded
+ 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 do to
programming errors, but Isabelle/Isar includes some extra validity
checks in critical positions, notably at the end of sub-proof.
- Proof contexts may be produced in arbitrary ways, 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 block-structured reasoning explicitly, using a stack of proof
- contexts, cf.\ \secref{isar-proof-state}.%
+ 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
+ block-structured reasoning explicitly, using a stack of proof
+ contexts internally, cf.\ \secref{sec:isar-proof-state}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -279,7 +286,8 @@
derived from \isa{thy}, initializing all data.
\item \verb|ProofContext.theory_of|~\isa{ctxt} selects the
- background theory from \isa{ctxt}.
+ background theory from \isa{ctxt}, dereferencing its internal
+ \verb|theory_ref|.
\item \verb|ProofContext.transfer|~\isa{thy\ ctxt} promotes the
background theory of \isa{ctxt} to the super theory \isa{thy}.
@@ -295,21 +303,21 @@
%
\endisadelimmlref
%
-\isamarkupsubsection{Generic contexts%
+\isamarkupsubsection{Generic contexts \label{sec:generic-context}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
A generic context is the disjoint sum of either a theory or proof
- context. Occasionally, this simplifies uniform treatment of generic
+ context. Occasionally, this enables uniform treatment of generic
context data, typically extra-logical information. Operations on
generic contexts include the usual injections, partial selections,
and combinators for lifting operations on either component of the
disjoint sum.
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, while a proof context may have to be
- constructed by an ad-hoc \isa{init} operation.%
+ can always be selected from the sum, while a proof context might
+ have to be constructed by an ad-hoc \isa{init} operation.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -328,15 +336,15 @@
\begin{description}
- \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with datatype constructors
- \verb|Context.Theory| and \verb|Context.Proof|.
+ \item \verb|Context.generic| is the direct sum of \verb|theory| and \verb|Proof.context|, with the datatype
+ constructors \verb|Context.Theory| and \verb|Context.Proof|.
\item \verb|Context.theory_of|~\isa{context} always produces a
theory from the generic \isa{context}, using \verb|ProofContext.theory_of| as required.
\item \verb|Context.proof_of|~\isa{context} always produces a
- proof context from the generic \isa{context}, using \verb|ProofContext.init| as required. Note that this re-initializes the
- context data with each invocation.
+ proof context from the generic \isa{context}, using \verb|ProofContext.init| as required (note that this re-initializes the
+ context data with each invocation).
\end{description}%
\end{isamarkuptext}%
@@ -354,23 +362,23 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Both theory and proof contexts manage arbitrary data, which is the
- main purpose of contexts in the first place. Data can be declared
- incrementally at compile --- Isabelle/Pure and major object-logics
- are bootstrapped that way.
+The main purpose of theory and proof contexts is to manage arbitrary
+ data. New data types can be declared incrementally at compile time.
+ There are separate declaration mechanisms for any of the three kinds
+ of contexts: theory, proof, generic.
\paragraph{Theory data} may refer to destructive entities, which are
- maintained in correspondence to the linear evolution of theory
- values, or explicit copies.\footnote{Most existing instances of
- destructive theory data are merely historical relics (e.g.\ the
- destructive theorem storage, and destructive hints for the
- Simplifier and Classical rules).} A theory data declaration needs
- to implement the following specification:
+ maintained in direct correspondence to the linear evolution of
+ theory values, including explicit copies.\footnote{Most existing
+ instances of destructive theory data are merely historical relics
+ (e.g.\ the destructive theorem storage, and destructive hints for
+ the Simplifier and Classical rules).} A theory data declaration
+ needs to implement the following specification (depending on type
+ \isa{T}):
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
- \isa{T} & the ML type \\
\isa{empty{\isacharcolon}\ T} & initial value \\
\isa{copy{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & refresh impure data \\
\isa{extend{\isacharcolon}\ T\ {\isasymrightarrow}\ T} & re-initialize on import \\
@@ -384,26 +392,25 @@
should also include the functionality of \isa{copy} for impure
data.
- \paragraph{Proof context data} is purely functional. It is declared
- by implementing the following specification:
+ \paragraph{Proof context data} is purely functional. A declaration
+ needs to implement the following specification:
\medskip
\begin{tabular}{ll}
\isa{name{\isacharcolon}\ string} \\
- \isa{T} & the ML type \\
\isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} & produce initial value \\
\isa{print{\isacharcolon}\ T\ {\isasymrightarrow}\ unit} & diagnostic output \\
\end{tabular}
\medskip
\noindent The \isa{init} operation is supposed to produce a pure
- value from the given background theory. The rest is analogous to
- (pure) theory data.
+ value from the given background theory. The remainder is analogous
+ to theory data.
- \paragraph{Generic data} provides a hybrid interface for both kinds.
- The declaration is essentially the same as for pure theory data,
- without \isa{copy} (it is always the identity). The \isa{init} operation for proof contexts selects the current data value
- from the background theory.
+ \paragraph{Generic data} provides a hybrid interface for both theory
+ and proof data. The declaration is essentially the same as for
+ (pure) theory data, without \isa{copy}, though. The \isa{init} operation for proof contexts merely selects the current data
+ value from the background theory.
\bigskip In any case, a data declaration of type \isa{T} results
in the following interface:
@@ -423,9 +430,9 @@
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 within a context. By keeping these operations private, a
- component may maintain abstract values authentically, without other
- components interfering.%
+ slot of a context. By keeping these operations private, a component
+ may maintain abstract values authentically, without other components
+ interfering.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -446,8 +453,8 @@
\item \verb|TheoryDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} declares data for
type \verb|theory| according to the specification provided as
- argument structure. The result structure provides init and access
- operations as described above.
+ argument structure. The resulting structure provides data init and
+ access operations as described above.
\item \verb|ProofDataFun|\isa{{\isacharparenleft}spec{\isacharparenright}} is analogous for
type \verb|Proof.context|.
@@ -471,23 +478,34 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Named entities of different kinds (logical constant, type,
-type class, theorem, method etc.) live in separate name spaces. It is
-usually clear from the occurrence of a name which kind of entity it
-refers to. For example, proof method \isa{foo} vs.\ theorem
-\isa{foo} vs.\ logical constant \isa{foo} are easily
-distinguished by means of the syntactic context. A notable exception
-are logical identifiers within a term (\secref{sec:terms}): constants,
-fixed variables, and bound variables all share the same identifier
-syntax, but are distinguished by their scope.
+By general convention, each kind of formal entities (logical
+ constant, type, type class, theorem, method etc.) lives in a
+ separate name space. It is usually clear from the syntactic context
+ of a name, which kind of entity it refers to. For example, proof
+ method \isa{foo} vs.\ theorem \isa{foo} vs.\ logical
+ constant \isa{foo} are easily distinguished thanks to the design
+ of the concrete outer syntax. A notable exception are logical
+ identifiers within a term (\secref{sec:terms}): constants, fixed
+ variables, and bound variables all share the same identifier syntax,
+ but are distinguished by their scope.
-Each name space is organized as a collection of \emph{qualified
-names}, which consist of a sequence of basic name components separated
-by dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
-are examples for valid qualified names. Name components are
-subdivided into \emph{symbols}, which constitute the smallest textual
-unit in Isabelle --- raw characters are normally not encountered
-directly.%
+ Name spaces are organized uniformly, as a collection of qualified
+ names consisting of a sequence of basic name components separated by
+ dots: \isa{Bar{\isachardot}bar{\isachardot}foo}, \isa{Bar{\isachardot}foo}, and \isa{foo}
+ are examples for qualified names.
+
+ Despite the independence of names of different kinds, certain naming
+ conventions may relate them to each other. For example, a constant
+ \isa{foo} could be accompanied with theorems \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc. The same
+ could happen for a type \isa{foo}, but this is apt to cause
+ clashes in the theorem name space! To avoid this, there is an
+ additional convention to add a suffix that determines the original
+ kind. For example, constant \isa{foo} could associated with
+ theorem \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.
+
+ \medskip Name components are subdivided into \emph{symbols}, which
+ constitute the smallest textual unit in Isabelle --- raw characters
+ are normally not encountered.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -497,48 +515,49 @@
%
\begin{isamarkuptext}%
Isabelle strings consist of a sequence of
-symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
-subsumes plain ASCII characters as well as an infinite collection of
-named symbols (for greek, math etc.).}, which are either packed as an
-actual \isa{string}, or represented as a list. Each symbol is in
-itself a small string of the following form:
+ symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
+ subsumes plain ASCII characters as well as an infinite collection of
+ named symbols (for greek, math etc.).}, which are either packed as
+ an actual \isa{string}, or represented as a list. Each symbol
+ is in itself a small string of the following form:
-\begin{enumerate}
+ \begin{enumerate}
+
+ \item either a singleton ASCII character ``\isa{c}'' (with
+ character code 0--127), for example ``\verb,a,'',
-\item either a singleton ASCII character ``\isa{c}'' (with
-character code 0--127), for example ``\verb,a,'',
+ \item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
-\item or a regular symbol ``\verb,\,\verb,<,\isa{ident}\verb,>,'',
-for example ``\verb,\,\verb,<alpha>,'',
+ \item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
-\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+ \item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
+ character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
+ character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
-\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
-printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
-non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+ \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
+ ``\verb,\,\verb,<^raw42>,''.
-\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
-``\verb,\,\verb,<^raw42>,''.
-
-\end{enumerate}
+ \end{enumerate}
-The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}Z} and \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols and
-control symbols available, but a certain collection of standard
-symbols is treated specifically. For example,
-``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
-which means it may occur within regular Isabelle identifier syntax.
+ The \isa{ident} syntax for symbol names is \isa{letter\ {\isacharparenleft}letter\ {\isacharbar}\ digit{\isacharparenright}\isactrlsup {\isacharasterisk}}, where \isa{letter\ {\isacharequal}\ A{\isachardot}{\isachardot}Za{\isachardot}{\isachardot}z} and
+ \isa{digit\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isadigit{9}}}. There are infinitely many regular symbols
+ and control symbols available, but a certain collection of standard
+ symbols is treated specifically. For example,
+ ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
+ which means it may occur within regular Isabelle identifier syntax.
-Output of symbols depends on the print mode (\secref{sec: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}}.
+ Output of symbols depends on the print mode
+ (\secref{sec: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}}.
-\medskip It is important to note that the character set underlying
-Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
-passed through transparently, Isabelle may easily process actual
-Unicode/UCS data (using the well-known UTF-8 encoding, for example).
-Unicode provides its own collection of mathematical symbols, but there
-is presently no link to Isabelle's named ones; both kinds of symbols
-coexist independently.%
+ \medskip It is important to note that the character set underlying
+ Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
+ passed through transparently, Isabelle may easily process
+ Unicode/UCS data as well (using UTF-8 encoding). Unicode provides
+ its own collection of mathematical symbols, but there is no built-in
+ link to the ones of Isabelle.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -555,33 +574,32 @@
\indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
\indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
\indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
- \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+ \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
\indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
\indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
\end{mldecls}
\begin{description}
- \item \verb|Symbol.symbol| represents Isabelle symbols; this type
- is merely an alias for \verb|string|, but emphasizes the
+ \item \verb|Symbol.symbol| represents Isabelle symbols. This
+ type is an alias for \verb|string|, but emphasizes the
specific format encountered here.
\item \verb|Symbol.explode|~\isa{s} produces a symbol list from
- the packed form usually encountered as user input. This function
- replaces \verb|String.explode| for virtually all purposes of
- manipulating text in Isabelle! Plain \verb|implode| may be used
- for the reverse operation.
+ the packed form that is encountered in most practical situations.
+ This function supercedes \verb|String.explode| for virtually all
+ purposes of manipulating text in Isabelle! Plain \verb|implode|
+ may still be used for the reverse operation.
\item \verb|Symbol.is_letter|, \verb|Symbol.is_digit|, \verb|Symbol.is_quasi|, \verb|Symbol.is_blank| classify certain symbols
(both ASCII and several named ones) according to fixed syntactic
- convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+ conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
\item \verb|Symbol.sym| is a concrete datatype that represents
- the different kinds of symbols explicitly as \verb|Symbol.Char|,
- \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
+ the different kinds of symbols explicitly with constructors \verb|Symbol.Char|, \verb|Symbol.Sym|, \verb|Symbol.Ctrl|, or \verb|Symbol.Raw|.
\item \verb|Symbol.decode| converts the string representation of a
- symbol into the explicit datatype version.
+ symbol into the datatype version.
\end{description}%
\end{isamarkuptext}%
@@ -599,49 +617,43 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
-
- Qualified names are constructed according to implicit naming
- principles of the present context.
-
-
- The last component is called \emph{base name}; the remaining prefix
- of qualification may be empty.
-
- Some practical conventions help to organize named entities more
- systematically:
-
- \begin{itemize}
-
- \item Names are qualified first by the theory name, second by an
- optional ``structure''. For example, a constant \isa{c}
- declared as part of a certain structure \isa{b} (say a type
- definition) in theory \isa{A} will be named \isa{A{\isachardot}b{\isachardot}c}
- internally.
+A \emph{qualified name} essentially consists of a non-empty list of
+ basic name components. The packad notation uses a dot as separator,
+ as in \isa{A{\isachardot}b}, for example. The very last component is called
+ \emph{base} name, the remaining prefix \emph{qualifier} (which may
+ be empty).
- \item
-
- \item
-
- \item
-
- \item
-
- \end{itemize}
+ A \isa{naming} policy tells how to produce fully qualified names
+ from a given specification. The \isa{full} operation applies
+ performs naming of a name; the policy is usually taken from the
+ context. For example, a common policy is to attach an implicit
+ prefix.
- Names of different kinds of entities are basically independent, but
- some practical naming conventions relate them to each other. For
- example, a constant \isa{foo} may be accompanied with theorems
- \isa{foo{\isachardot}intro}, \isa{foo{\isachardot}elim}, \isa{foo{\isachardot}simps} etc.
- The same may happen for a type \isa{foo}, which is then apt to
- cause clashes in the theorem name space! To avoid this, we
- occasionally follow an additional convention of suffixes that
- determine the original kind of entity that a name has been derived.
- For example, constant \isa{foo} is associated with theorem
- \isa{foo{\isachardot}intro}, type \isa{foo} with theorem \isa{foo{\isacharunderscore}type{\isachardot}intro}, and type class \isa{foo} with \isa{foo{\isacharunderscore}class{\isachardot}intro}.%
+ A \isa{name\ space} manages declarations of fully qualified
+ names. There are separate operations to \isa{declare}, \isa{intern}, and \isa{extern} names.
+
+ FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\isamarkupsection{Structured output%
}
\isamarkuptrue%
@@ -664,7 +676,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Print modes%
+\isamarkupsubsection{Print modes \label{sec:print-mode}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Aug 31 22:55:49 2006 +0200
@@ -19,15 +19,11 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Structured reasoning%
+\isamarkupchapter{Structured proofs%
}
\isamarkuptrue%
%
-\isamarkupsection{Proof context%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Local variables%
+\isamarkupsection{Local variables%
}
\isamarkuptrue%
%
@@ -105,7 +101,34 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof state%
+\isamarkupsection{Schematic polymorphism%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Assumptions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conclusions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
}
\isamarkuptrue%
%
@@ -125,7 +148,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Methods%
+\isamarkupsection{Proof methods%
}
\isamarkuptrue%
%
@@ -139,7 +162,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME%
+FIXME ?!%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex Thu Aug 31 22:55:49 2006 +0200
@@ -19,17 +19,19 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Tactical theorem proving%
+\isamarkupchapter{Goal-directed reasoning%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The basic idea of tactical theorem proving is to refine the
-initial claim in a backwards fashion, until a solved form is reached.
-An intermediate goal consists of several subgoals that need to be
-solved in order to achieve the main statement; zero subgoals means
-that the proof may be finished. Goal refinement operations are called
-tactics; combinators for composing tactics are called tacticals.%
+The basic idea of tactical theorem proving is to refine the initial
+ claim in a backwards fashion, until a solved form is reached. An
+ intermediate goal consists of several subgoals that need to be
+ solved in order to achieve the main statement; zero subgoals means
+ that the proof may be finished. A \isa{tactic} is a refinement
+ operation that maps a goal to a lazy sequence of potential
+ successors. A \isa{tactical} is a combinator for composing
+ tactics.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -38,40 +40,41 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Isabelle/Pure represents a goal\glossary{Tactical goal}{A
-theorem of \seeglossary{Horn Clause} form stating that a number of
-subgoals imply the main conclusion, which is marked as a protected
-proposition.} as a theorem stating that the subgoals imply the main
-goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal
-structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
-implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
-outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
-arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
-connectives).}: an iterated implication without any
-quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
-always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These may get instantiated during the course of
-reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is solved.
+Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
+ \seeglossary{Horn Clause} form stating that a number of subgoals
+ imply the main conclusion, which is marked as a protected
+ proposition.} as a theorem stating that the subgoals imply the main
+ goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal
+ structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
+ implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
+ outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
+ arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
+ connectives).}: i.e.\ an iterated implication without any
+ quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
+ always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These variables may get instantiated during the course of
+ reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is called ``solved''.
-The structure of each subgoal \isa{A\isactrlsub i} is that of a general
-Heriditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal form where any local
-\isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}. Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ arbitrary-but-fixed entities of
-certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal
-hypotheses, i.e.\ facts that may be assumed locally. Together, this
-forms the goal context of the conclusion \isa{B} to be established.
-The goal hypotheses may be again arbitrary Harrop Formulas, although
-the level of nesting rarely exceeds 1--2 in practice.
+ The structure of each subgoal \isa{A\isactrlsub i} is that of a
+ general Hereditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal
+ form where any local \isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}. Here
+ \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\
+ arbitrary-but-fixed entities of certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal hypotheses, i.e.\ facts that may
+ be assumed locally. Together, this forms the goal context of the
+ conclusion \isa{B} to be established. The goal hypotheses may be
+ again Hereditary Harrop Formulas, although the level of nesting
+ rarely exceeds 1--2 in practice.
-The main conclusion \isa{C} is internally marked as a protected
-proposition\glossary{Protected proposition}{An arbitrarily structured
-proposition \isa{C} which is forced to appear as atomic by
-wrapping it into a propositional identity operator; notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic inferences from
-entering into that structure for the time being.}, which is
-occasionally 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.
+ The main conclusion \isa{C} is internally marked as a protected
+ proposition\glossary{Protected proposition}{An arbitrarily
+ structured proposition \isa{C} which is forced to appear as
+ atomic by wrapping it into a propositional identity operator;
+ notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic
+ inferences from entering into that structure for the time being.},
+ which is occasionally 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.
-\medskip Basic goal management is performed via the following
-Isabelle/Pure rules:
+ \medskip Basic goal management is performed via the following
+ Isabelle/Pure rules:
\[
\infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
@@ -104,13 +107,13 @@
\begin{description}
- \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal with
+ \item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal from
the type-checked proposition \isa{{\isasymphi}}.
- \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (zero subgoals), and concludes
+ \item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (no subgoals), and concludes
the result by removing the goal protection.
- \item \verb|Goal.protect|~\isa{th} protects the whole statement
+ \item \verb|Goal.protect|~\isa{th} protects the full statement
of theorem \isa{th}.
\item \verb|Goal.conclude|~\isa{th} removes the goal protection
@@ -173,12 +176,10 @@
ill-behaved tactics could have destroyed that information.
Several simultaneous claims may be handled within a single goal
- statement by using meta-level conjunction internally.\footnote{This
- is merely syntax for certain derived statements within
- Isabelle/Pure, there is no need to introduce a separate conjunction
- operator.} The whole configuration may be considered within a
- context of arbitrary-but-fixed parameters and hypotheses, which will
- be available as local facts during the proof and discharged into
+ statement by using meta-level conjunction internally. The whole
+ configuration may be considered within a context of
+ arbitrary-but-fixed parameters and hypotheses, which will be
+ available as local facts during the proof and discharged into
implications in the result.
All of these administrative tasks are packaged into a separate
--- a/doc-src/IsarImplementation/Thy/integration.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy Thu Aug 31 22:55:49 2006 +0200
@@ -9,19 +9,18 @@
text {* The Isar toplevel may be considered the centeral hub of the
Isabelle/Isar system, where all key components and sub-systems are
- integrated into a single read-eval-print loop of Isar commands.
- Here we even incorporate the existing {\ML} toplevel of the compiler
+ integrated into a single read-eval-print loop of Isar commands. We
+ shall even incorporate the existing {\ML} toplevel of the compiler
and run-time system (cf.\ \secref{sec:ML-toplevel}).
- Isabelle/Isar departs from original ``LCF system architecture''
+ Isabelle/Isar departs from the original ``LCF system architecture''
where {\ML} was really The Meta Language for defining theories and
- conducting proofs. Instead, {\ML} merely serves as the
+ conducting proofs. Instead, {\ML} now only serves as the
implementation language for the system (and user extensions), while
- our specific Isar toplevel supports particular notions of
- incremental theory and proof development more directly. This
- includes the graph structure of theories and the block structure of
- proofs, support for unlimited undo, facilities for tracing,
- debugging, timing, profiling.
+ the specific Isar toplevel supports the concepts of theory and proof
+ development natively. This includes the graph structure of theories
+ and the block structure of proofs, support for unlimited undo,
+ facilities for tracing, debugging, timing, profiling etc.
\medskip The toplevel maintains an implicit state, which is
transformed by a sequence of transitions -- either interactively or
@@ -29,9 +28,9 @@
encapsulated as safe transactions, such that both failure and undo
are handled conveniently without destroying the underlying draft
theory (cf.~\secref{sec:context-theory}). In batch mode,
- transitions operate in a strictly linear (destructive) fashion, such
- that error conditions abort the present attempt to construct a
- theory altogether.
+ transitions operate in a linear (destructive) fashion, such that
+ error conditions abort the present attempt to construct a theory or
+ proof altogether.
The toplevel state is a disjoint sum of empty @{text toplevel}, or
@{text theory}, or @{text proof}. On entering the main Isar loop we
@@ -69,22 +68,23 @@
\begin{description}
\item @{ML_type Toplevel.state} represents Isar toplevel states,
- which are normally only manipulated through the toplevel transition
- concept (\secref{sec:toplevel-transition}). Also note that a
- toplevel state is subject to the same linerarity restrictions as a
- theory context (cf.~\secref{sec:context-theory}).
+ which are normally manipulated through the concept of toplevel
+ transitions only (\secref{sec:toplevel-transition}). Also note that
+ a raw toplevel state is subject to the same linearity restrictions
+ as a theory context (cf.~\secref{sec:context-theory}).
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel
- operations: @{ML_type Toplevel.state} is a sum type, many operations
- work only partially for certain cases.
+ operations. Many operations work only partially for certain cases,
+ since @{ML_type Toplevel.state} is a sum type.
- \item @{ML Toplevel.is_toplevel} checks for an empty toplevel state.
+ \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
+ toplevel state.
- \item @{ML Toplevel.theory_of} gets the theory of a theory or proof
- (!), otherwise raises @{ML Toplevel.UNDEF}.
+ \item @{ML Toplevel.theory_of}~@{text "state"} selects the theory of
+ a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
- \item @{ML Toplevel.proof_of} gets the Isar proof state if
- available, otherwise raises @{ML Toplevel.UNDEF}.
+ \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
+ state if available, otherwise raises @{ML Toplevel.UNDEF}.
\item @{ML "set Toplevel.debug"} makes the toplevel print further
details about internal error conditions, exceptions being raised
@@ -93,36 +93,37 @@
\item @{ML "set Toplevel.timing"} makes the toplevel print timing
information for each Isar command being executed.
- \item @{ML Toplevel.profiling} controls low-level profiling of the
- underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
- and 2 space profiling.}
+ \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
+ low-level profiling of the underlying {\ML} runtime system. For
+ Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
+ profiling.
\end{description}
*}
-subsection {* Toplevel transitions *}
+subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
-text {* An Isar toplevel transition consists of a partial
- function on the toplevel state, with additional information for
- diagnostics and error reporting: there are fields for command name,
- source position, optional source text, as well as flags for
- interactive-only commands (which issue a warning in batch-mode),
- printing of result state, etc.
+text {*
+ An Isar toplevel transition consists of a partial function on the
+ toplevel state, with additional information for diagnostics and
+ error reporting: there are fields for command name, source position,
+ optional source text, as well as flags for interactive-only commands
+ (which issue a warning in batch-mode), printing of result state,
+ etc.
- The operational part is represented as a sequential union of a list
- of partial functions, which are tried in turn until the first one
- succeeds (i.e.\ does not raise @{ML Toplevel.UNDEF}). For example,
- a single Isar command like \isacommand{qed} consists of the union of
- some function @{ML_type "Proof.state -> Proof.state"} for proofs
- within proofs, plus @{ML_type "Proof.state -> theory"} for proofs at
- the outer theory level.
+ 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 (i.e.\ does not raise @{ML Toplevel.UNDEF}). This acts
+ like an outer case-expression for various alternative state
+ transitions. For example, \isakeyword{qed} acts 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
- syntax body into a suitable transition transformer that adjoin
+ concrete syntax into a suitable transition transformer that adjoin
actual operations on a theory or proof state etc.
*}
@@ -146,32 +147,36 @@
\begin{description}
- \item @{ML Toplevel.print} sets the print flag, which causes the
- resulting state of the transition to be echoed in interactive mode.
+ \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
+ causes the toplevel loop to echo the result state (in interactive
+ mode).
- \item @{ML Toplevel.no_timing} indicates that the transition should
- never show timing information, e.g.\ because it is merely a
- diagnostic command.
+ \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
+ transition should never show timing information, e.g.\ because it is
+ a diagnostic command.
- \item @{ML Toplevel.keep} adjoins a diagnostic function.
+ \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
+ function.
- \item @{ML Toplevel.theory} adjoins a theory transformer.
+ \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
+ transformer.
- \item @{ML Toplevel.theory_to_proof} adjoins a global goal function,
- which turns a theory into a proof state. The theory may be changed
- before entering the proof; the generic Isar goal setup includes an
- argument that specifies how to apply the proven result to the
- theory, when the proof is finished.
+ \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
+ goal function, which turns a theory into a proof state. The theory
+ may be changed before entering the proof; the generic Isar goal
+ setup includes an argument that specifies how to apply the proven
+ result to the theory, when the proof is finished.
- \item @{ML Toplevel.proof} adjoins a deterministic proof command,
- with a singleton result state.
+ \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
+ proof command, with a singleton result.
- \item @{ML Toplevel.proofs} adjoins a general proof command, with
- zero or more result states (represented as a lazy list).
+ \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
+ command, with zero or more result states (represented as a lazy
+ list).
- \item @{ML Toplevel.proof_to_theory} adjoins a concluding proof
- command, that returns the resulting theory, after storing the
- resulting facts etc.
+ \item @{ML Toplevel.proof_to_theory}~@{text "tr"} adjoins a
+ concluding proof command, that returns the resulting theory, after
+ storing the resulting facts etc.
\end{description}
*}
@@ -179,12 +184,12 @@
subsection {* Toplevel control *}
-text {* Apart from regular toplevel transactions there are a few
- special control commands that modify the behavior 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.
+text {*
+ There are a few special control commands that modify the behavior
+ 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.
\begin{description}
@@ -221,14 +226,15 @@
no clean way to undo {\ML} declarations, except for reverting to a
previously saved state of the whole Isabelle process. {\ML} input
is either read interactively from a TTY, or from a string (usually
- within a theory text), or from a source file (usually associated
- with a theory).
+ within a theory text), or from a source file (usually loaded from a
+ theory).
Whenever the {\ML} toplevel is active, the current Isabelle theory
context is passed as an internal reference variable. Thus {\ML}
code may access the theory context during compilation, it may even
- change the value of a theory being under construction --- following
- the usual linearity restrictions (cf.~\secref{sec:context-theory}).
+ change the value of a theory being under construction --- while
+ observing the usual linearity restrictions
+ (cf.~\secref{sec:context-theory}).
*}
text %mlref {*
@@ -247,28 +253,29 @@
\item @{ML "the_context ()"} refers to the theory context of the
{\ML} toplevel --- at compile time! {\ML} code needs to take care
- to refer to @{ML "the_context ()"} correctly, recall that evaluation
- of a function body is delayed until actual runtime. Moreover,
- persistent {\ML} toplevel bindings to an unfinished theory should be
- avoided: code should either project out the desired information
- immediately, or produce an explicit @{ML_type theory_ref} (cf.\
- \secref{sec:context-theory}).
+ to refer to @{ML "the_context ()"} correctly. Recall that
+ evaluation of a function body is delayed until actual runtime.
+ Moreover, persistent {\ML} toplevel bindings to an unfinished theory
+ should be avoided: code should either project out the desired
+ information immediately, or produce an explicit @{ML_type
+ theory_ref} (cf.\ \secref{sec:context-theory}).
\item @{ML "Context.>>"}~@{text f} applies theory transformation
@{text f} to the current theory of the {\ML} toplevel. In order to
work as expected, the theory should be still under construction, and
the Isar language element that invoked the {\ML} compiler in the
- first place shoule be ready to accept the changed theory value
+ first place should be ready to accept the changed theory value
(e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
- Otherwise the theory may get destroyed!
+ Otherwise the theory becomes stale!
\end{description}
It is very important to note that the above functions are really
restricted to the compile time, even though the {\ML} compiler is
invoked at runtime! The majority of {\ML} code uses explicit
- functional arguments of a theory or proof context, as required.
- Thus it may get run in an arbitrary context later on.
+ functional arguments of a theory or proof context instead. Thus it
+ may be invoked for an arbitrary context later on, without having to
+ worry about any operational details.
\bigskip
@@ -283,46 +290,46 @@
\begin{description}
\item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
- initializing the state to empty toplevel state.
+ initializing an empty toplevel state.
\item @{ML "Isar.loop ()"} continues the Isar toplevel with the
- current state, after dropping out of the Isar toplevel loop.
+ current state, after having dropped out of the Isar toplevel loop.
\item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
- toplevel state and optional error condition, respectively. This
- only works after dropping out of the Isar toplevel loop.
+ toplevel state and error condition, respectively. This only works
+ after having dropped out of the Isar toplevel loop.
\item @{ML "Isar.context ()"} produces the proof context from @{ML
- "Isar.state ()"}.
+ "Isar.state ()"}, analogous to @{ML Context.proof_of}
+ (\secref{sec:generic-context}).
\end{description}
*}
-section {* Theory database *}
+section {* Theory database \label{sec:theory-database} *}
-text {* The theory database maintains a collection of theories,
- together with some administrative information about the original
- sources, which are held in an external store (i.e.\ a collection of
- directories within the regular file system of the underlying
- platform).
+text {*
+ The theory database maintains a collection of theories, together
+ with some administrative information about their original sources,
+ which are held in an external store (i.e.\ some directory within the
+ regular file system).
- The theory database is organized as a directed acyclic graph, with
- entries referenced by theory name. Although some external
- interfaces allow to include a directory specification, this is only
- a hint to the underlying theory loader mechanism: the internal
- theory name space is flat.
+ The theory database is organized as a directed acyclic graph;
+ entries are referenced by theory name. Although some additional
+ interfaces allow to include a directory specification as well, this
+ is only a hint to the underlying theory loader. The internal theory
+ name space is flat!
Theory @{text A} is associated with the main theory file @{text
A}\verb,.thy,, which needs to be accessible through the theory
- loader path. A number of optional {\ML} source files may be
+ loader path. Any number of additional {\ML} source files may be
associated with each theory, by declaring these dependencies in the
theory header as @{text \<USES>}, and loading them consecutively
within the theory context. The system keeps track of incoming {\ML}
- sources and associates them with the current theory. The special
- theory {\ML} file @{text 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 file
+ @{text A}\verb,.ML, is loaded after a theory has been concluded, in
+ order to support legacy proof {\ML} proof scripts.
The basic internal actions of the theory database are @{text
"update"}, @{text "outdate"}, and @{text "remove"}:
@@ -331,31 +338,30 @@
\item @{text "update A"} introduces a link of @{text "A"} with a
@{text "theory"} value of the same name; it asserts that the theory
- sources are consistent with that value.
+ sources are now consistent with that value;
\item @{text "outdate A"} invalidates the link of a theory database
- entry to its sources, but retains the present theory value.
+ entry to its sources, but retains the present theory value;
- \item @{text "remove A"} removes entry @{text "A"} from the theory
+ \item @{text "remove A"} deletes entry @{text "A"} from the theory
database.
\end{itemize}
These actions are propagated to sub- or super-graphs of a theory
- entry in the usual way, in order to preserve global consistency of
- the state of all loaded theories with the sources of the external
- store. This implies causal dependencies of certain actions: @{text
- "update"} or @{text "outdate"} of an entry will @{text "outdate"}
- all descendants; @{text "remove"} will @{text "remove"} all
- descendants.
+ entry as expected, in order to preserve global consistency of the
+ state of all loaded theories with the sources of the external store.
+ This implies certain causalities between actions: @{text "update"}
+ or @{text "outdate"} of an entry will @{text "outdate"} all
+ descendants; @{text "remove"} will @{text "remove"} all descendants.
\medskip There are separate user-level interfaces to operate on the
theory database directly or indirectly. The primitive actions then
just happen automatically while working with the system. In
particular, processing a theory header @{text "\<THEORY> A
- \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensure that the
+ \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
- is up-to-date. Earlier theories are reloaded as required, with
+ is up-to-date, too. Earlier theories are reloaded as required, with
@{text update} actions proceeding in topological order according to
theory dependencies. There may be also a wave of implied @{text
outdate} actions for derived theory nodes until a stable situation
@@ -367,8 +373,6 @@
@{index_ML theory: "string -> theory"} \\
@{index_ML use_thy: "string -> unit"} \\
@{index_ML update_thy: "string -> unit"} \\
- @{index_ML use_thy_only: "string -> unit"} \\
- @{index_ML update_thy_only: "string -> unit"} \\
@{index_ML touch_thy: "string -> unit"} \\
@{index_ML remove_thy: "string -> unit"} \\[1ex]
@{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
@@ -381,8 +385,8 @@
\begin{description}
\item @{ML theory}~@{text A} retrieves the theory value presently
- associated with @{text A}. The result is not necessarily
- up-to-date!
+ associated with name @{text A}. Note that the result might be
+ outdated.
\item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
or out-of-date. It ensures that all parent theories are available
@@ -390,20 +394,12 @@
present.
\item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
- the @{text A} and all of its ancestors are fully up-to-date.
+ theory @{text A} and all ancestors are fully up-to-date.
- \item @{ML use_thy_only}~@{text A} is like @{ML use_thy}~@{text A},
- but refrains from loading the attached @{text A}\verb,.ML, file.
- This is occasionally useful in replaying legacy {\ML} proof scripts
- by hand.
-
- \item @{ML update_thy_only} is analogous to @{ML use_thy_only}, but
- proceeds like @{ML update_thy} for ancestors.
+ \item @{ML touch_thy}~@{text A} performs and @{text outdate} action
+ on theory @{text A} and all descendants.
- \item @{ML touch_thy}~@{text A} performs @{text outdate} action on
- theory @{text A} and all of its descendants.
-
- \item @{ML remove_thy}~@{text A} removes @{text A} and all of its
+ \item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
descendants from the theory database.
\item @{ML ThyInfo.begin_theory} is the basic operation behind a
@@ -414,28 +410,30 @@
normally not invoked directly.
\item @{ML ThyInfo.end_theory} concludes the loading of a theory
- proper; an attached theory {\ML} file may be still loaded later on.
- This is {\ML} functions is normally not invoked directly.
+ proper. An attached theory {\ML} file may be still loaded later on.
+ This is function is normally not invoked directly.
- \item @{ML ThyInfo.register_theory}~{text thy} registers an existing
- theory value with the theory loader database. There is no
- management of associated sources; this is mainly for bootstrapping.
+ \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
+ existing theory value with the theory loader database. There is no
+ management of associated sources.
\item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
f} as a hook for theory database actions. The function will be
invoked with the action and theory name being involved; thus derived
actions may be performed in associated system components, e.g.\
- maintaining the state of an editor for theory sources.
+ maintaining the state of an editor for the theory sources.
The kind and order of actions occurring in practice depends both on
user interactions and the internal process of resolving theory
imports. Hooks should not rely on a particular policy here! Any
- exceptions raised by the hook are ignored by the theory database.
+ exceptions raised by the hook are ignored.
\end{description}
*}
-(* FIXME section {* Sessions and document preparation *} *)
+section {* Sessions and document preparation *}
+
+text FIXME
end
--- a/doc-src/IsarImplementation/Thy/locale.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/locale.thy Thu Aug 31 22:55:49 2006 +0200
@@ -9,8 +9,18 @@
text FIXME
-section {* Locales *}
+
+section {* Type-checking specifications *}
text FIXME
+
+section {* Localized theory specifications *}
+
+text {*
+ FIXME
+
+ \glossary{Local theory}{FIXME}
+*}
+
end
--- a/doc-src/IsarImplementation/Thy/logic.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy Thu Aug 31 22:55:49 2006 +0200
@@ -5,45 +5,42 @@
chapter {* Primitive logic *}
-section {* Syntax *}
+section {* Variable names *}
-subsection {* Variable names *}
+text FIXME
+
+
+section {* Types \label{sec:types} *}
text {*
- FIXME
+ \glossary{Type class}{FIXME}
+
+ \glossary{Type arity}{FIXME}
+
+ \glossary{Sort}{FIXME}
+
+ FIXME classes and sorts
+
+
+ \glossary{Type}{FIXME}
+
+ \glossary{Type constructor}{FIXME}
+
+ \glossary{Type variable}{FIXME}
+
+ FIXME simple types
*}
-subsection {* Simply-typed lambda calculus *}
-
-text {*
-
-FIXME
-
-\glossary{Type}{FIXME}
-\glossary{Term}{FIXME}
-
-*}
-
-subsection {* The order-sorted algebra of types *}
+section {* Terms \label{sec:terms} *}
text {*
-
-FIXME
-
-\glossary{Type constructor}{FIXME}
+ \glossary{Term}{FIXME}
-\glossary{Type class}{FIXME}
-
-\glossary{Type arity}{FIXME}
-
-\glossary{Sort}{FIXME}
-
+ FIXME de-Bruijn representation of lambda terms
*}
-subsection {* Type-inference and schematic polymorphism *}
-
text {*
FIXME
@@ -55,21 +52,7 @@
*}
-section {* Theory *}
-
-text {*
-
-FIXME
-
-\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
-theory context, but slightly more flexible since it may be used at
-different type-instances, due to \seeglossary{schematic
-polymorphism.}}
-
-*}
-
-
-section {* Deduction *}
+section {* Theorems \label{sec:thms} *}
text {*
@@ -139,8 +122,21 @@
text FIXME
-section {* Proof terms *}
+section {* Low-level specifications *}
+
+text {*
+
+FIXME
-text FIXME
+\glossary{Constant}{Essentially a \seeglossary{fixed variable} of the
+theory context, but slightly more flexible since it may be used at
+different type-instances, due to \seeglossary{schematic
+polymorphism.}}
+
+\glossary{Axiom}{FIXME}
+
+\glossary{Primitive definition}{FIXME}
+
+*}
end
--- a/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Thu Aug 31 22:55:49 2006 +0200
@@ -8,19 +8,20 @@
section {* Contexts \label{sec:context} *}
text {*
- A logical context represents the background that is taken for
- granted when formulating statements and composing proofs. It acts
- as a medium to produce formal content, depending on earlier material
- (declarations, results etc.).
+ A logical context represents the background that is required for
+ formulating statements and composing proofs. It acts as a medium to
+ produce formal content, depending on earlier material (declarations,
+ results etc.).
- In particular, derivations within the primitive Pure logic can be
- described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, meaning that a
+ For example, derivations within the Isabelle/Pure logic can be
+ described as a judgment @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}, which means that a
proposition @{text "\<phi>"} is derivable from hypotheses @{text "\<Gamma>"}
within the theory @{text "\<Theta>"}. There are logical reasons for
- keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories support type
- constructors and schematic polymorphism of constants and axioms,
- while the inner calculus of @{text "\<Gamma> \<turnstile> \<phi>"} is limited to Simple
- Type Theory (with fixed type variables in the assumptions).
+ keeping @{text "\<Theta>"} and @{text "\<Gamma>"} separate: theories can be
+ liberal about supporting type constructors and schematic
+ polymorphism of constants and axioms, while the inner calculus of
+ @{text "\<Gamma> \<turnstile> \<phi>"} is strictly limited to Simple Type Theory (with
+ fixed type variables in the assumptions).
\medskip Contexts and derivations are linked by the following key
principles:
@@ -28,45 +29,46 @@
\begin{itemize}
\item Transfer: monotonicity of derivations admits results to be
- transferred into a larger context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<phi>"}
- implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>' \<supseteq>
- \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
+ transferred into a \emph{larger} context, i.e.\ @{text "\<Gamma> \<turnstile>\<^sub>\<Theta>
+ \<phi>"} implies @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta>\<^sub>' \<phi>"} for contexts @{text "\<Theta>'
+ \<supseteq> \<Theta>"} and @{text "\<Gamma>' \<supseteq> \<Gamma>"}.
\item Export: discharge of hypotheses admits results to be exported
- into a smaller context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"} implies
- @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and @{text "\<Delta> =
- \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here, only the
- @{text "\<Gamma>"} part is affected.
+ into a \emph{smaller} context, i.e.\ @{text "\<Gamma>' \<turnstile>\<^sub>\<Theta> \<phi>"}
+ implies @{text "\<Gamma> \<turnstile>\<^sub>\<Theta> \<Delta> \<Longrightarrow> \<phi>"} where @{text "\<Gamma>' \<supseteq> \<Gamma>"} and
+ @{text "\<Delta> = \<Gamma>' - \<Gamma>"}. Note that @{text "\<Theta>"} remains unchanged here,
+ only the @{text "\<Gamma>"} part is affected.
\end{itemize}
- \medskip Isabelle/Isar provides two different notions of abstract
- containers called \emph{theory context} and \emph{proof context},
- respectively. These model the main characteristics of the primitive
- @{text "\<Theta>"} and @{text "\<Gamma>"} above, without subscribing to any
- particular kind of content yet. Instead, contexts merely impose a
- certain policy of managing arbitrary \emph{context data}. The
- system provides strongly typed mechanisms to declare new kinds of
+ \medskip By modeling the main characteristics of the primitive
+ @{text "\<Theta>"} and @{text "\<Gamma>"} above, and abstracting over any
+ particular logical content, we arrive at the fundamental notions of
+ \emph{theory context} and \emph{proof context} in Isabelle/Isar.
+ These implement a certain policy to manage arbitrary \emph{context
+ data}. There is a strongly-typed mechanism to declare new kinds of
data at compile time.
- Thus the internal bootstrap process of Isabelle/Pure eventually
- reaches a stage where certain data slots provide the logical content
- of @{text "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not
- stop there! Various additional data slots support all kinds of
- mechanisms that are not necessarily part of the core logic.
+ The internal bootstrap process of Isabelle/Pure eventually reaches a
+ stage where certain data slots provide the logical content of @{text
+ "\<Theta>"} and @{text "\<Gamma>"} sketched above, but this does not stop there!
+ Various additional data slots support all kinds of mechanisms that
+ are not necessarily part of the core logic.
For example, there would be data for canonical introduction and
elimination rules for arbitrary operators (depending on the
object-logic and application), which enables users to perform
- standard proof steps implicitly (cf.\ the @{text "rule"} method).
+ standard proof steps implicitly (cf.\ the @{text "rule"} method
+ \cite{isabelle-isar-ref}).
- Isabelle is able to bring forth more and more concepts successively.
- In particular, an object-logic like Isabelle/HOL continues the
- Isabelle/Pure setup by adding specific components for automated
- reasoning (classical reasoner, tableau prover, structured induction
- etc.) and derived specification mechanisms (inductive predicates,
- recursive functions etc.). All of this is based on the generic data
- management by theory and proof contexts.
+ \medskip Thus Isabelle/Isar is able to bring forth more and more
+ concepts successively. In particular, an object-logic like
+ Isabelle/HOL continues the Isabelle/Pure setup by adding specific
+ components for automated reasoning (classical reasoner, tableau
+ prover, structured induction etc.) and derived specification
+ mechanisms (inductive predicates, recursive functions etc.). All of
+ this is ultimately based on the generic data management by theory
+ and proof contexts introduced here.
*}
@@ -75,31 +77,27 @@
text {*
\glossary{Theory}{FIXME}
- Each theory is explicitly named and holds a unique identifier.
- There is a separate \emph{theory reference} for pointing backwards
- to the enclosing theory context of derived entities. Theories are
- related by a (nominal) sub-theory relation, which corresponds to the
- canonical dependency graph: each theory is derived from a certain
- sub-graph of ancestor theories. The @{text "merge"} of two theories
- refers to the least upper bound, which actually degenerates into
- absorption of one theory into the other, due to the nominal
- sub-theory relation this.
+ A \emph{theory} is a data container with explicit named 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 @{text "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).
The @{text "begin"} operation starts a new theory by importing
several parent theories and entering a special @{text "draft"} mode,
which is sustained until the final @{text "end"} operation. A draft
- mode theory acts like a linear type, where updates invalidate
- earlier drafts, but theory reference values will be propagated
- automatically. Thus derived entities that ``belong'' to a draft
- might be transferred spontaneously to a larger context. An
- invalidated draft is called ``stale''.
+ theory acts like a linear type, where updates invalidate earlier
+ versions. An invalidated draft is called ``stale''.
The @{text "checkpoint"} operation produces an intermediate stepping
- stone that will survive the next update unscathed: 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.
+ 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 @{text "copy"} operation produces an auxiliary version that has
the same data content, but is unrelated to the original: updates of
@@ -107,11 +105,12 @@
relation hold.
\medskip The example in \figref{fig:ex-theory} below shows a theory
- graph derived from @{text "Pure"}. Theory @{text "Length"} imports
- @{text "Nat"} and @{text "List"}. The theory body 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}.
+ graph derived from @{text "Pure"}, with theory @{text "Length"}
+ importing @{text "Nat"} and @{text "List"}. The body of @{text
+ "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}.
\begin{figure}[htb]
\begin{center}
@@ -132,9 +131,19 @@
& & $\vdots$~~ \\
& & \multicolumn{3}{l}{~~$\isarkeyword{end}$} \\
\end{tabular}
- \caption{Theory definition depending on ancestors}\label{fig:ex-theory}
+ \caption{A theory definition depending on ancestors}\label{fig:ex-theory}
\end{center}
\end{figure}
+
+ \medskip There is a separate notion of \emph{theory reference} for
+ maintaining a live link to an evolving theory context: updates on
+ drafts are propagated automatically. The dynamic stops after an
+ explicit @{text "end"} only.
+
+ Derived entities may store a theory reference in order to indicate
+ the context they belong to. This implicitly assumes monotonic
+ reasoning, because the referenced context may become larger without
+ further notice.
*}
text %mlref {*
@@ -151,9 +160,9 @@
\begin{description}
- \item @{ML_type theory} represents theory contexts. This is a
- linear type! Most operations destroy the old version, which then
- becomes ``stale''.
+ \item @{ML_type theory} represents theory contexts. This is
+ essentially a linear type! Most operations destroy the original
+ version, which then becomes ``stale''.
\item @{ML "Theory.subthy"}~@{text "(thy\<^sub>1, thy\<^sub>2)"}
compares theories according to the inherent graph structure of the
@@ -169,18 +178,18 @@
update will result in two related, valid theories.
\item @{ML "Theory.copy"}~@{text "thy"} produces a variant of @{text
- "thy"} that holds a copy of the same data. The copy is not related
- to the original, which is not touched at all.
+ "thy"} that holds a copy of the same data. The result is not
+ related to the original; the original is unchanched.
- \item @{ML_type theory_ref} represents a sliding reference to a
- valid theory --- updates on the original are propagated
+ \item @{ML_type theory_ref} represents a sliding reference to an
+ always valid theory; updates on the original are propagated
automatically.
\item @{ML "Theory.self_ref"}~@{text "thy"} and @{ML
"Theory.deref"}~@{text "thy_ref"} convert between @{ML_type
"theory"} and @{ML_type "theory_ref"}. As the referenced theory
evolves monotonically over time, later invocations of @{ML
- "Theory.deref"} may refer to larger contexts.
+ "Theory.deref"} may refer to a larger context.
\end{description}
*}
@@ -198,28 +207,28 @@
A proof context is a container for pure data with a back-reference
to the theory it belongs to. The @{text "init"} operation creates a
- proof context derived from a given theory. Modifications to draft
- theories are propagated to the proof context as usual, but there is
- also an explicit @{text "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.
+ proof context from a given theory. Modifications to draft theories
+ are propagated to the proof context as usual, but there is also an
+ explicit @{text "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.
Entities derived in a proof context need to record inherent logical
requirements explicitly, since there is no separate context
identification as for theories. For example, hypotheses used in
- primitive derivations (cf.\ \secref{sec:thm}) are recorded
+ primitive derivations (cf.\ \secref{sec:thms}) are recorded
separately within the sequent @{text "\<Gamma> \<turnstile> \<phi>"}, just to make double
sure. Results could still leak into an alien proof context do to
programming errors, but Isabelle/Isar includes some extra validity
checks in critical positions, notably at the end of sub-proof.
- Proof contexts may be produced in arbitrary ways, 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 block-structured reasoning explicitly, using a stack of proof
- contexts, cf.\ \secref{isar-proof-state}.
+ 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
+ block-structured reasoning explicitly, using a stack of proof
+ contexts internally, cf.\ \secref{sec:isar-proof-state}.
*}
text %mlref {*
@@ -240,7 +249,8 @@
derived from @{text "thy"}, initializing all data.
\item @{ML ProofContext.theory_of}~@{text "ctxt"} selects the
- background theory from @{text "ctxt"}.
+ background theory from @{text "ctxt"}, dereferencing its internal
+ @{ML_type theory_ref}.
\item @{ML ProofContext.transfer}~@{text "thy ctxt"} promotes the
background theory of @{text "ctxt"} to the super theory @{text
@@ -250,12 +260,11 @@
*}
-
-subsection {* Generic contexts *}
+subsection {* Generic contexts \label{sec:generic-context} *}
text {*
A generic context is the disjoint sum of either a theory or proof
- context. Occasionally, this simplifies uniform treatment of generic
+ context. Occasionally, this enables uniform treatment of generic
context data, typically extra-logical information. Operations on
generic contexts include the usual injections, partial selections,
and combinators for lifting operations on either component of the
@@ -263,8 +272,8 @@
Moreover, there are total operations @{text "theory_of"} and @{text
"proof_of"} to convert a generic context into either kind: a theory
- can always be selected, while a proof context may have to be
- constructed by an ad-hoc @{text "init"} operation.
+ can always be selected from the sum, while a proof context might
+ have to be constructed by an ad-hoc @{text "init"} operation.
*}
text %mlref {*
@@ -277,8 +286,8 @@
\begin{description}
\item @{ML_type Context.generic} is the direct sum of @{ML_type
- "theory"} and @{ML_type "Proof.context"}, with datatype constructors
- @{ML "Context.Theory"} and @{ML "Context.Proof"}.
+ "theory"} and @{ML_type "Proof.context"}, with the datatype
+ constructors @{ML "Context.Theory"} and @{ML "Context.Proof"}.
\item @{ML Context.theory_of}~@{text "context"} always produces a
theory from the generic @{text "context"}, using @{ML
@@ -286,8 +295,8 @@
\item @{ML Context.proof_of}~@{text "context"} always produces a
proof context from the generic @{text "context"}, using @{ML
- "ProofContext.init"} as required. Note that this re-initializes the
- context data with each invocation.
+ "ProofContext.init"} as required (note that this re-initializes the
+ context data with each invocation).
\end{description}
*}
@@ -295,23 +304,23 @@
subsection {* Context data *}
text {*
- Both theory and proof contexts manage arbitrary data, which is the
- main purpose of contexts in the first place. Data can be declared
- incrementally at compile --- Isabelle/Pure and major object-logics
- are bootstrapped that way.
+ The main purpose of theory and proof contexts is to manage arbitrary
+ data. New data types can be declared incrementally at compile time.
+ There are separate declaration mechanisms for any of the three kinds
+ of contexts: theory, proof, generic.
\paragraph{Theory data} may refer to destructive entities, which are
- maintained in correspondence to the linear evolution of theory
- values, or explicit copies.\footnote{Most existing instances of
- destructive theory data are merely historical relics (e.g.\ the
- destructive theorem storage, and destructive hints for the
- Simplifier and Classical rules).} A theory data declaration needs
- to implement the following specification:
+ maintained in direct correspondence to the linear evolution of
+ theory values, including explicit copies.\footnote{Most existing
+ instances of destructive theory data are merely historical relics
+ (e.g.\ the destructive theorem storage, and destructive hints for
+ the Simplifier and Classical rules).} A theory data declaration
+ needs to implement the following specification (depending on type
+ @{text "T"}):
\medskip
\begin{tabular}{ll}
@{text "name: string"} \\
- @{text "T"} & the ML type \\
@{text "empty: T"} & initial value \\
@{text "copy: T \<rightarrow> T"} & refresh impure data \\
@{text "extend: T \<rightarrow> T"} & re-initialize on import \\
@@ -326,27 +335,26 @@
should also include the functionality of @{text "copy"} for impure
data.
- \paragraph{Proof context data} is purely functional. It is declared
- by implementing the following specification:
+ \paragraph{Proof context data} is purely functional. A declaration
+ needs to implement the following specification:
\medskip
\begin{tabular}{ll}
@{text "name: string"} \\
- @{text "T"} & the ML type \\
@{text "init: theory \<rightarrow> T"} & produce initial value \\
@{text "print: T \<rightarrow> unit"} & diagnostic output \\
\end{tabular}
\medskip
\noindent The @{text "init"} operation is supposed to produce a pure
- value from the given background theory. The rest is analogous to
- (pure) theory data.
+ value from the given background theory. The remainder is analogous
+ to theory data.
- \paragraph{Generic data} provides a hybrid interface for both kinds.
- The declaration is essentially the same as for pure theory data,
- without @{text "copy"} (it is always the identity). The @{text
- "init"} operation for proof contexts selects the current data value
- from the background theory.
+ \paragraph{Generic data} provides a hybrid interface for both theory
+ and proof data. The declaration is essentially the same as for
+ (pure) theory data, without @{text "copy"}, though. The @{text
+ "init"} operation for proof contexts merely selects the current data
+ value from the background theory.
\bigskip In any case, a data declaration of type @{text "T"} results
in the following interface:
@@ -366,9 +374,9 @@
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 within a context. By keeping these operations private, a
- component may maintain abstract values authentically, without other
- components interfering.
+ slot of a context. By keeping these operations private, a component
+ may maintain abstract values authentically, without other components
+ interfering.
*}
text %mlref {*
@@ -382,8 +390,8 @@
\item @{ML_functor TheoryDataFun}@{text "(spec)"} declares data for
type @{ML_type theory} according to the specification provided as
- argument structure. The result structure provides init and access
- operations as described above.
+ argument structure. The resulting structure provides data init and
+ access operations as described above.
\item @{ML_functor ProofDataFun}@{text "(spec)"} is analogous for
type @{ML_type Proof.context}.
@@ -397,77 +405,95 @@
section {* Named entities *}
-text {* Named entities of different kinds (logical constant, type,
-type class, theorem, method etc.) live in separate name spaces. It is
-usually clear from the occurrence of a name which kind of entity it
-refers to. For example, proof method @{text "foo"} vs.\ theorem
-@{text "foo"} vs.\ logical constant @{text "foo"} are easily
-distinguished by means of the syntactic context. A notable exception
-are logical identifiers within a term (\secref{sec:terms}): constants,
-fixed variables, and bound variables all share the same identifier
-syntax, but are distinguished by their scope.
+text {*
+ By general convention, each kind of formal entities (logical
+ constant, type, type class, theorem, method etc.) lives in a
+ separate name space. It is usually clear from the syntactic context
+ of a name, which kind of entity it refers to. For example, proof
+ method @{text "foo"} vs.\ theorem @{text "foo"} vs.\ logical
+ constant @{text "foo"} are easily distinguished thanks to the design
+ of the concrete outer syntax. A notable exception are logical
+ identifiers within a term (\secref{sec:terms}): constants, fixed
+ variables, and bound variables all share the same identifier syntax,
+ but are distinguished by their scope.
+
+ Name spaces are organized uniformly, as a collection of qualified
+ names consisting of a sequence of basic name components separated by
+ dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
+ are examples for qualified names.
-Each name space is organized as a collection of \emph{qualified
-names}, which consist of a sequence of basic name components separated
-by dots: @{text "Bar.bar.foo"}, @{text "Bar.foo"}, and @{text "foo"}
-are examples for valid qualified names. Name components are
-subdivided into \emph{symbols}, which constitute the smallest textual
-unit in Isabelle --- raw characters are normally not encountered
-directly. *}
+ Despite the independence of names of different kinds, certain naming
+ conventions may relate them to each other. For example, a constant
+ @{text "foo"} could be accompanied with theorems @{text
+ "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc. The same
+ could happen for a type @{text "foo"}, but this is apt to cause
+ clashes in the theorem name space! To avoid this, there is an
+ additional convention to add a suffix that determines the original
+ kind. For example, constant @{text "foo"} could associated with
+ theorem @{text "foo.intro"}, type @{text "foo"} with theorem @{text
+ "foo_type.intro"}, and type class @{text "foo"} with @{text
+ "foo_class.intro"}.
+
+ \medskip Name components are subdivided into \emph{symbols}, which
+ constitute the smallest textual unit in Isabelle --- raw characters
+ are normally not encountered.
+*}
subsection {* Strings of symbols *}
-text {* Isabelle strings consist of a sequence of
-symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
-subsumes plain ASCII characters as well as an infinite collection of
-named symbols (for greek, math etc.).}, which are either packed as an
-actual @{text "string"}, or represented as a list. Each symbol is in
-itself a small string of the following form:
+text {*
+ Isabelle strings consist of a sequence of
+ symbols\glossary{Symbol}{The smallest unit of text in Isabelle,
+ subsumes plain ASCII characters as well as an infinite collection of
+ named symbols (for greek, math etc.).}, which are either packed as
+ an actual @{text "string"}, or represented as a list. Each symbol
+ is in itself a small string of the following form:
-\begin{enumerate}
+ \begin{enumerate}
-\item either a singleton ASCII character ``@{text "c"}'' (with
-character code 0--127), for example ``\verb,a,'',
+ \item either a singleton ASCII character ``@{text "c"}'' (with
+ character code 0--127), for example ``\verb,a,'',
-\item or a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
-for example ``\verb,\,\verb,<alpha>,'',
+ \item or a regular symbol ``\verb,\,\verb,<,@{text
+ "ident"}\verb,>,'', for example ``\verb,\,\verb,<alpha>,'',
-\item or a control symbol ``\verb,\,\verb,<^,@{text
-"ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
+ \item or a control symbol ``\verb,\,\verb,<^,@{text
+ "ident"}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
-\item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
-"\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any
-printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
-non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+ \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
+ "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' refers to any printable ASCII
+ character (excluding ``\verb,.,'' and ``\verb,>,'') or non-ASCII
+ character, for example ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
-\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
-"nnn"}\verb,>, where @{text "nnn"} are digits, for example
-``\verb,\,\verb,<^raw42>,''.
+ \item or a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
+ "nnn"}\verb,>, where @{text "nnn"} are digits, for example
+ ``\verb,\,\verb,<^raw42>,''.
-\end{enumerate}
+ \end{enumerate}
-The @{text "ident"} syntax for symbol names is @{text "letter (letter
-| digit)\<^sup>*"}, where @{text "letter = A..Za..Z"} and @{text
-"digit = 0..9"}. There are infinitely many regular symbols and
-control symbols available, but a certain collection of standard
-symbols is treated specifically. For example,
-``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
-which means it may occur within regular Isabelle identifier syntax.
+ The @{text "ident"} syntax for symbol names is @{text "letter
+ (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and
+ @{text "digit = 0..9"}. There are infinitely many regular symbols
+ and control symbols available, but a certain collection of standard
+ symbols is treated specifically. For example,
+ ``\verb,\,\verb,<alpha>,'' is classified as a (non-ASCII) letter,
+ which means it may occur within regular Isabelle identifier syntax.
-Output of symbols depends on the print mode (\secref{sec:print-mode}).
-For example, the standard {\LaTeX} setup of the Isabelle document
-preparation system would present ``\verb,\,\verb,<alpha>,'' as @{text
-"\<alpha>"}, and ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
-"\<^bold>\<alpha>"}.
+ Output of symbols depends on the print mode
+ (\secref{sec:print-mode}). For example, the standard {\LaTeX} setup
+ of the Isabelle document preparation system would present
+ ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
+ ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text
+ "\<^bold>\<alpha>"}.
-\medskip It is important to note that the character set underlying
-Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
-passed through transparently, Isabelle may easily process actual
-Unicode/UCS data (using the well-known UTF-8 encoding, for example).
-Unicode provides its own collection of mathematical symbols, but there
-is presently no link to Isabelle's named ones; both kinds of symbols
-coexist independently. *}
+ \medskip It is important to note that the character set underlying
+ Isabelle symbols is plain 7-bit ASCII. Since 8-bit characters are
+ passed through transparently, Isabelle may easily process
+ Unicode/UCS data as well (using UTF-8 encoding). Unicode provides
+ its own collection of mathematical symbols, but there is no built-in
+ link to the ones of Isabelle.
+*}
text %mlref {*
\begin{mldecls}
@@ -476,34 +502,35 @@
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
- @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+ @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
@{index_ML_type "Symbol.sym"} \\
@{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
\end{mldecls}
\begin{description}
- \item @{ML_type "Symbol.symbol"} represents Isabelle symbols; this type
- is merely an alias for @{ML_type "string"}, but emphasizes the
+ \item @{ML_type "Symbol.symbol"} represents Isabelle symbols. This
+ type is an alias for @{ML_type "string"}, but emphasizes the
specific format encountered here.
\item @{ML "Symbol.explode"}~@{text "s"} produces a symbol list from
- the packed form usually encountered as user input. This function
- replaces @{ML "String.explode"} for virtually all purposes of
- manipulating text in Isabelle! Plain @{ML "implode"} may be used
- for the reverse operation.
+ the packed form that is encountered in most practical situations.
+ This function supercedes @{ML "String.explode"} for virtually all
+ purposes of manipulating text in Isabelle! Plain @{ML "implode"}
+ may still be used for the reverse operation.
\item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
"Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify certain symbols
(both ASCII and several named ones) according to fixed syntactic
- convections of Isabelle, e.g.\ see \cite{isabelle-isar-ref}.
+ conventions of Isabelle, cf.\ \cite{isabelle-isar-ref}.
\item @{ML_type "Symbol.sym"} is a concrete datatype that represents
- the different kinds of symbols explicitly as @{ML "Symbol.Char"},
- @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML "Symbol.Raw"}.
+ the different kinds of symbols explicitly with constructors @{ML
+ "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, or @{ML
+ "Symbol.Raw"}.
\item @{ML "Symbol.decode"} converts the string representation of a
- symbol into the explicit datatype version.
+ symbol into the datatype version.
\end{description}
*}
@@ -512,50 +539,27 @@
subsection {* Qualified names and name spaces *}
text {*
- FIXME
-
- Qualified names are constructed according to implicit naming
- principles of the present context.
-
-
- The last component is called \emph{base name}; the remaining prefix
- of qualification may be empty.
-
- Some practical conventions help to organize named entities more
- systematically:
-
- \begin{itemize}
-
- \item Names are qualified first by the theory name, second by an
- optional ``structure''. For example, a constant @{text "c"}
- declared as part of a certain structure @{text "b"} (say a type
- definition) in theory @{text "A"} will be named @{text "A.b.c"}
- internally.
-
- \item
+ A \emph{qualified name} essentially consists of a non-empty list of
+ basic name components. The packad notation uses a dot as separator,
+ as in @{text "A.b"}, for example. The very last component is called
+ \emph{base} name, the remaining prefix \emph{qualifier} (which may
+ be empty).
- \item
-
- \item
-
- \item
-
- \end{itemize}
+ A @{text "naming"} policy tells how to produce fully qualified names
+ from a given specification. The @{text "full"} operation applies
+ performs naming of a name; the policy is usually taken from the
+ context. For example, a common policy is to attach an implicit
+ prefix.
- Names of different kinds of entities are basically independent, but
- some practical naming conventions relate them to each other. For
- example, a constant @{text "foo"} may be accompanied with theorems
- @{text "foo.intro"}, @{text "foo.elim"}, @{text "foo.simps"} etc.
- The same may happen for a type @{text "foo"}, which is then apt to
- cause clashes in the theorem name space! To avoid this, we
- occasionally follow an additional convention of suffixes that
- determine the original kind of entity that a name has been derived.
- For example, constant @{text "foo"} is associated with theorem
- @{text "foo.intro"}, type @{text "foo"} with theorem @{text
- "foo_type.intro"}, and type class @{text "foo"} with @{text
- "foo_class.intro"}.
+ A @{text "name space"} manages declarations of fully qualified
+ names. There are separate operations to @{text "declare"}, @{text
+ "intern"}, and @{text "extern"} names.
+
+ FIXME
*}
+text %mlref FIXME
+
section {* Structured output *}
@@ -567,7 +571,7 @@
text FIXME
-subsection {* Print modes *}
+subsection {* Print modes \label{sec:print-mode} *}
text FIXME
--- a/doc-src/IsarImplementation/Thy/proof.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Thu Aug 31 22:55:49 2006 +0200
@@ -3,11 +3,9 @@
theory "proof" imports base begin
-chapter {* Structured reasoning *}
+chapter {* Structured proofs *}
-section {* Proof context *}
-
-subsection {* Local variables *}
+section {* Local variables *}
text FIXME
@@ -66,7 +64,23 @@
text FIXME
-section {* Proof state *}
+
+section {* Schematic polymorphism *}
+
+text FIXME
+
+
+section {* Assumptions *}
+
+text FIXME
+
+
+section {* Conclusions *}
+
+text FIXME
+
+
+section {* Structured proofs \label{sec:isar-proof-state} *}
text {*
FIXME
@@ -85,12 +99,12 @@
*}
-section {* Methods *}
+section {* Proof methods *}
text FIXME
section {* Attributes *}
-text FIXME
+text "FIXME ?!"
end
--- a/doc-src/IsarImplementation/Thy/tactic.thy Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy Thu Aug 31 22:55:49 2006 +0200
@@ -3,57 +3,63 @@
theory tactic imports base begin
-chapter {* Tactical theorem proving *}
+chapter {* Goal-directed reasoning *}
-text {* The basic idea of tactical theorem proving is to refine the
-initial claim in a backwards fashion, until a solved form is reached.
-An intermediate goal consists of several subgoals that need to be
-solved in order to achieve the main statement; zero subgoals means
-that the proof may be finished. Goal refinement operations are called
-tactics; combinators for composing tactics are called tacticals. *}
+text {*
+ The basic idea of tactical theorem proving is to refine the initial
+ claim in a backwards fashion, until a solved form is reached. An
+ intermediate goal consists of several subgoals that need to be
+ solved in order to achieve the main statement; zero subgoals means
+ that the proof may be finished. A @{text "tactic"} is a refinement
+ operation that maps a goal to a lazy sequence of potential
+ successors. A @{text "tactical"} is a combinator for composing
+ tactics.
+*}
section {* Goals \label{sec:tactical-goals} *}
-text {* Isabelle/Pure represents a goal\glossary{Tactical goal}{A
-theorem of \seeglossary{Horn Clause} form stating that a number of
-subgoals imply the main conclusion, which is marked as a protected
-proposition.} as a theorem stating that the subgoals imply the main
-goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal
-structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
-implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
-outermost quantifiers. Strictly speaking, propositions @{text
-"A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
-arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
-connectives).}: an iterated implication without any
-quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
-always represented via schematic variables in the body: @{text
-"\<phi>[?x]"}. These may get instantiated during the course of
-reasoning.}. For @{text "n = 0"} a goal is solved.
+text {*
+ Isabelle/Pure represents a goal\glossary{Tactical goal}{A theorem of
+ \seeglossary{Horn Clause} form stating that a number of subgoals
+ imply the main conclusion, which is marked as a protected
+ proposition.} as a theorem stating that the subgoals imply the main
+ goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}. The outermost goal
+ structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
+ implication @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}, without any
+ outermost quantifiers. Strictly speaking, propositions @{text
+ "A\<^sub>i"} need to be atomic in Horn Clauses, but Isabelle admits
+ arbitrary substructure here (nested @{text "\<Longrightarrow>"} and @{text "\<And>"}
+ connectives).}: i.e.\ an iterated implication without any
+ quantifiers\footnote{Recall that outermost @{text "\<And>x. \<phi>[x]"} is
+ always represented via schematic variables in the body: @{text
+ "\<phi>[?x]"}. These variables may get instantiated during the course of
+ reasoning.}. For @{text "n = 0"} a goal is called ``solved''.
-The structure of each subgoal @{text "A\<^sub>i"} is that of a general
-Heriditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots> \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow>
-\<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal form where any local
-@{text \<And>} is pulled before @{text \<Longrightarrow>}. Here @{text "x\<^sub>1, \<dots>,
-x\<^sub>k"} are goal parameters, i.e.\ arbitrary-but-fixed entities of
-certain types, and @{text "H\<^sub>1, \<dots>, H\<^sub>m"} are goal
-hypotheses, i.e.\ facts that may be assumed locally. Together, this
-forms the goal context of the conclusion @{text B} to be established.
-The goal hypotheses may be again arbitrary Harrop Formulas, although
-the level of nesting rarely exceeds 1--2 in practice.
+ The structure of each subgoal @{text "A\<^sub>i"} is that of a
+ general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
+ \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"} according to the normal
+ form where any local @{text \<And>} is pulled before @{text \<Longrightarrow>}. Here
+ @{text "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
+ arbitrary-but-fixed entities of certain types, and @{text
+ "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
+ be assumed locally. Together, this forms the goal context of the
+ conclusion @{text B} to be established. The goal hypotheses may be
+ again Hereditary Harrop Formulas, although the level of nesting
+ rarely exceeds 1--2 in practice.
-The main conclusion @{text C} is internally marked as a protected
-proposition\glossary{Protected proposition}{An arbitrarily structured
-proposition @{text "C"} which is forced to appear as atomic by
-wrapping it into a propositional identity operator; notation @{text
-"#C"}. Protecting a proposition prevents basic inferences from
-entering into that structure for the time being.}, which is
-occasionally represented explicitly by the notation @{text "#C"}.
-This ensures that the decomposition into subgoals and main conclusion
-is well-defined for arbitrarily structured claims.
+ The main conclusion @{text C} is internally marked as a protected
+ proposition\glossary{Protected proposition}{An arbitrarily
+ structured proposition @{text "C"} which is forced to appear as
+ atomic by wrapping it into a propositional identity operator;
+ notation @{text "#C"}. Protecting a proposition prevents basic
+ inferences from entering into that structure for the time being.},
+ which is occasionally represented explicitly by the notation @{text
+ "#C"}. 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:
+ \medskip Basic goal management is performed via the following
+ Isabelle/Pure rules:
\[
\infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
@@ -79,14 +85,14 @@
\begin{description}
- \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal with
+ \item @{ML "Goal.init"}~@{text "\<phi>"} initializes a tactical goal from
the type-checked proposition @{text \<phi>}.
\item @{ML "Goal.finish"}~@{text "th"} checks whether theorem @{text
- "th"} is a solved goal configuration (zero subgoals), and concludes
+ "th"} is a solved goal configuration (no subgoals), and concludes
the result by removing the goal protection.
- \item @{ML "Goal.protect"}~@{text "th"} protects the whole statement
+ \item @{ML "Goal.protect"}~@{text "th"} protects the full statement
of theorem @{text "th"}.
\item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
@@ -139,12 +145,10 @@
ill-behaved tactics could have destroyed that information.
Several simultaneous claims may be handled within a single goal
- statement by using meta-level conjunction internally.\footnote{This
- is merely syntax for certain derived statements within
- Isabelle/Pure, there is no need to introduce a separate conjunction
- operator.} The whole configuration may be considered within a
- context of arbitrary-but-fixed parameters and hypotheses, which will
- be available as local facts during the proof and discharged into
+ statement by using meta-level conjunction internally. The whole
+ configuration may be considered within a context of
+ arbitrary-but-fixed parameters and hypotheses, which will be
+ available as local facts during the proof and discharged into
implications in the result.
All of these administrative tasks are packaged into a separate
--- a/doc-src/IsarImplementation/implementation.tex Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Thu Aug 31 22:55:49 2006 +0200
@@ -29,7 +29,7 @@
\begin{abstract}
We describe the key concepts underlying the Isabelle/Isar
implementation, including ML references for the most important
- elements. The aim is to give some insight into the overall system
+ functions. The aim is to give some insight into the overall system
architecture, and provide clues on implementing user extensions.
\end{abstract}
--- a/doc-src/IsarImplementation/style.sty Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/style.sty Thu Aug 31 22:55:49 2006 +0200
@@ -38,6 +38,8 @@
\binperiod
\underscoreon
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
\isafoldtag{FIXME}