--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Mon Feb 16 21:39:52 2009 +0100
@@ -158,7 +158,7 @@
Internally, Isar commands are put together from an empty transition
extended by name and source position (and optional source text). It
is then left to the individual command parser to turn the given
- concrete syntax into a suitable transition transformer that adjoin
+ concrete syntax into a suitable transition transformer that adjoins
actual operations on a theory or proof state etc.%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Mon Feb 16 21:39:52 2009 +0100
@@ -18,11 +18,27 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Isar proof texts%
+\isamarkupchapter{Isar language elements%
}
\isamarkuptrue%
%
-\isamarkupsection{Proof context%
+\begin{isamarkuptext}%
+The primary Isar language consists of three main categories of
+ language elements:
+
+ \begin{enumerate}
+
+ \item Proof commands
+
+ \item Proof methods
+
+ \item Attributes
+
+ \end{enumerate}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof commands%
}
\isamarkuptrue%
%
@@ -31,26 +47,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Proof state \label{sec:isar-proof-state}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-\glossary{Proof state}{The whole configuration of a structured proof,
-consisting of a \seeglossary{proof context} and an optional
-\seeglossary{structured goal}. Internally, an Isar proof state is
-organized as a stack to accomodate block structure of proof texts.
-For historical reasons, a low-level \seeglossary{tactical goal} is
-occasionally called ``proof state'' as well.}
-
-\glossary{Structured goal}{FIXME}
-
-\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Proof methods%
}
\isamarkuptrue%
@@ -65,7 +61,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME ?!%
+FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Mon Feb 16 21:39:52 2009 +0100
@@ -18,11 +18,11 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Structured specifications%
+\isamarkupchapter{Local theory specifications%
}
\isamarkuptrue%
%
-\isamarkupsection{Specification elements%
+\isamarkupsection{Definitional elements%
}
\isamarkuptrue%
%
@@ -31,7 +31,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Type-inference%
+\isamarkupsection{Morphisms and declarations%
}
\isamarkuptrue%
%
@@ -40,17 +40,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Local theories%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
- \glossary{Local theory}{FIXME}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Feb 16 21:39:52 2009 +0100
@@ -203,13 +203,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\glossary{Term}{FIXME}
-
- The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
+The language of terms is that of simply-typed \isa{{\isasymlambda}}-calculus
with de-Bruijn indices for bound variables (cf.\ \cite{debruijn72}
- or \cite{paulson-ml2}), with the types being determined determined
- by the corresponding binders. In contrast, free variables and
- constants are have an explicit name and type in each occurrence.
+ or \cite{paulson-ml2}), with the types being determined by the
+ corresponding binders. In contrast, free variables and constants
+ are have an explicit name and type in each occurrence.
\medskip A \emph{bound variable} is a natural number \isa{b},
which accounts for the number of intermediate binders between the
@@ -394,42 +392,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\glossary{Proposition}{FIXME A \seeglossary{term} of
- \seeglossary{type} \isa{prop}. Internally, there is nothing
- special about propositions apart from their type, but the concrete
- syntax enforces a clear distinction. Propositions are structured
- via implication \isa{A\ {\isasymLongrightarrow}\ B} or universal quantification \isa{{\isasymAnd}x{\isachardot}\ B\ x} --- anything else is considered atomic. The canonical
- form for propositions is that of a \seeglossary{Hereditary Harrop
- Formula}. FIXME}
-
- \glossary{Theorem}{A proven proposition within a certain theory and
- proof context, formally \isa{{\isasymGamma}\ {\isasymturnstile}\isactrlsub {\isasymTheta}\ {\isasymphi}}; both contexts are
- rarely spelled out explicitly. Theorems are usually normalized
- according to the \seeglossary{HHF} format. FIXME}
-
- \glossary{Fact}{Sometimes used interchangeably for
- \seeglossary{theorem}. Strictly speaking, a list of theorems,
- essentially an extra-logical conjunction. Facts emerge either as
- local assumptions, or as results of local goal statements --- both
- may be simultaneous, hence the list representation. FIXME}
-
- \glossary{Schematic variable}{FIXME}
-
- \glossary{Fixed variable}{A variable that is bound within a certain
- proof context; an arbitrary-but-fixed entity within a portion of
- proof text. FIXME}
-
- \glossary{Free variable}{Synonymous for \seeglossary{fixed
- variable}. FIXME}
-
- \glossary{Bound variable}{FIXME}
-
- \glossary{Variable}{See \seeglossary{schematic variable},
- \seeglossary{fixed variable}, \seeglossary{bound variable}, or
- \seeglossary{type variable}. The distinguishing feature of
- different variables is their binding scope. FIXME}
-
- A \emph{proposition} is a well-typed term of type \isa{prop}, a
+A \emph{proposition} is a well-typed term of type \isa{prop}, a
\emph{theorem} is a proven proposition (depending on a context of
hypotheses and the background theory). Primitive inferences include
plain natural deduction rules for the primary connectives \isa{{\isasymAnd}} and \isa{{\isasymLongrightarrow}} of the framework. There is also a builtin
@@ -812,15 +775,12 @@
expect a normal form: quantifiers \isa{{\isasymAnd}} before implications
\isa{{\isasymLongrightarrow}} at each level of nesting.
-\glossary{Hereditary Harrop Formula}{The set of propositions in HHF
-format is defined inductively as \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x} and atomic propositions \isa{A}.
-Any proposition may be put into HHF form by normalizing with the rule
-\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. In Isabelle, the outermost
-quantifier prefix is represented via \seeglossary{schematic
-variables}, such that the top-level structure is merely that of a
-\seeglossary{Horn Clause}}.
-
-\glossary{HHF}{See \seeglossary{Hereditary Harrop Formula}.}
+ The set of propositions in HHF format is defined inductively as
+ \isa{H\ {\isacharequal}\ {\isacharparenleft}{\isasymAnd}x\isactrlsup {\isacharasterisk}{\isachardot}\ H\isactrlsup {\isacharasterisk}\ {\isasymLongrightarrow}\ A{\isacharparenright}}, for variables \isa{x}
+ and atomic propositions \isa{A}. Any proposition may be put
+ into HHF form by normalizing with the rule \isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x{\isacharparenright}{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ A\ {\isasymLongrightarrow}\ B\ x{\isacharparenright}}. In Isabelle, the outermost quantifier prefix is
+ represented via schematic variables, such that the top-level
+ structure is merely that of a Horn Clause.
\[
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Feb 16 21:39:52 2009 +0100
@@ -93,9 +93,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\glossary{Theory}{FIXME}
-
- A \emph{theory} is a data container with explicit named and unique
+A \emph{theory} is a data container with explicit name and unique
identifier. Theories are related by a (nominal) sub-theory
relation, which corresponds to the dependency graph of the original
construction; each theory is derived from a certain sub-graph of
@@ -204,7 +202,7 @@
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 result is not
- related to the original; the original is unchanched.
+ related to the original; the original is unchanged.
\item \verb|theory_ref| represents a sliding reference to an
always valid theory; updates on the original are propagated
@@ -231,14 +229,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\glossary{Proof context}{The static context of a structured proof,
- acts like a local ``theory'' of the current portion of Isar proof
- text, generalizes the idea of local hypotheses \isa{{\isasymGamma}} in
- judgments \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}} of natural deduction calculi. There is a
- generic notion of introducing and discharging hypotheses.
- Arbritrary auxiliary context data may be adjoined.}
-
- A proof context is a container for pure data with a back-reference
+A proof context is a container for pure data with a back-reference
to the theory it belongs to. The \isa{init} operation creates a
proof context from a given theory. Modifications to draft theories
are propagated to the proof context as usual, but there is also an
@@ -252,7 +243,7 @@
identification as for theories. For example, hypotheses used in
primitive derivations (cf.\ \secref{sec:thms}) are recorded
separately within the sequent \isa{{\isasymGamma}\ {\isasymturnstile}\ {\isasymphi}}, just to make double
- sure. Results could still leak into an alien proof context do to
+ sure. Results could still leak into an alien proof context due to
programming errors, but Isabelle/Isar includes some extra validity
checks in critical positions, notably at the end of a sub-proof.
@@ -261,7 +252,7 @@
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}.%
+ contexts internally.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -418,7 +409,7 @@
\medskip
\begin{tabular}{ll}
- \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ theory} \\
+ \isa{init{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
\isa{get{\isacharcolon}\ context\ {\isasymrightarrow}\ T} \\
\isa{put{\isacharcolon}\ T\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
\isa{map{\isacharcolon}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ context\ {\isasymrightarrow}\ context} \\
@@ -491,11 +482,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-\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.).}
-
- A \emph{symbol} constitutes the smallest textual unit in Isabelle
+A \emph{symbol} constitutes the smallest textual unit in Isabelle
--- raw characters are normally not encountered at all. Isabelle
strings consist of a sequence of symbols, represented as a packed
string or a list of strings. Each symbol is in itself a small
@@ -535,8 +522,8 @@
link to the standard collection of Isabelle.
\medskip Output of Isabelle symbols depends on the print mode
- (\secref{FIXME}). For example, the standard {\LaTeX} setup of the
- Isabelle document preparation system would present
+ (\secref{print-mode}). For example, the standard {\LaTeX} setup of
+ the Isabelle document preparation system would present
``\verb,\,\verb,<alpha>,'' as \isa{{\isasymalpha}}, and
``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as \isa{\isactrlbold {\isasymalpha}}.%
\end{isamarkuptext}%
@@ -599,10 +586,9 @@
\begin{isamarkuptext}%
A \emph{basic name} essentially consists of a single Isabelle
identifier. There are conventions to mark separate classes of basic
- names, by attaching a suffix of underscores (\isa{{\isacharunderscore}}): one
- underscore means \emph{internal name}, two underscores means
- \emph{Skolem name}, three underscores means \emph{internal Skolem
- name}.
+ names, by attaching a suffix of underscores: one underscore means
+ \emph{internal name}, two underscores means \emph{Skolem name},
+ three underscores means \emph{internal Skolem name}.
For example, the basic name \isa{foo} has the internal version
\isa{foo{\isacharunderscore}}, with Skolem versions \isa{foo{\isacharunderscore}{\isacharunderscore}} and \isa{foo{\isacharunderscore}{\isacharunderscore}{\isacharunderscore}}, respectively.
@@ -663,7 +649,7 @@
\item \verb|Name.invents|~\isa{context\ name\ n} produces \isa{n} fresh names derived from \isa{name}.
\item \verb|Name.variants|~\isa{names\ context} produces fresh
- varians of \isa{names}; the result is entered into the context.
+ variants of \isa{names}; the result is entered into the context.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Feb 16 21:39:52 2009 +0100
@@ -194,8 +194,7 @@
rules. Note that the discharged portion is determined by the
difference contexts, not the facts being exported! There is a
separate flag to indicate a goal context, where the result is meant
- to refine an enclosing sub-goal of a structured proof state (cf.\
- \secref{sec:isar-proof-state}).
+ to refine an enclosing sub-goal of a structured proof state.
\medskip The most basic export rule discharges assumptions directly
by means of the \isa{{\isasymLongrightarrow}} introduction rule:
@@ -342,11 +341,11 @@
\begin{description}
- \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
- particular sub-goal, producing an extended context and a reduced
- goal, which needs to be solved by the given tactic. All schematic
- parameters of the goal are imported into the context as fixed ones,
- which may not be instantiated in the sub-proof.
+ \item \verb|SUBPROOF|~\isa{tac\ ctxt\ i} decomposes the structure
+ of the specified sub-goal, producing an extended context and a
+ reduced goal, which needs to be solved by the given tactic. All
+ schematic parameters of the goal are imported into the context as
+ fixed ones, which may not be instantiated in the sub-proof.
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
assumptions \isa{As}, and applies tactic \isa{tac} to solve
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Mon Feb 16 21:39:52 2009 +0100
@@ -37,38 +37,25 @@
\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).}: 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''.
+Isabelle/Pure represents a goal 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: 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
- 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} in
- normal form. 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
- Hereditary 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}. 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 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 represented explicitly by the notation \isa{{\isacharhash}C}. This
- ensures that the decomposition into subgoals and main conclusion is
- well-defined for arbitrarily structured claims.
+ proposition, which is represented explicitly by the notation \isa{{\isacharhash}C}. 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:
@@ -480,12 +467,12 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-FIXME
+A \emph{tactical} is a functional combinator for building up complex
+ tactics from simpler ones. Typical tactical perform sequential
+ composition, disjunction (choice), iteration, or goal addressing.
+ Various search strategies may be expressed via tacticals.
-\glossary{Tactical}{A functional combinator for building up complex
-tactics from simpler ones. Typical tactical perform sequential
-composition, disjunction (choice), iteration, or goal addressing.
-Various search strategies may be expressed via tacticals.}%
+ \medskip FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%