--- 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