doc-src/IsarImplementation/Thy/document/tactic.tex

 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Tactical theorem proving%
-}
-\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.%
+\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.  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%
 %
 \isamarkupsection{Goals \label{sec:tactical-goals}%
 }
 \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.
-
-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 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:
+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 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.
+
+  \medskip Basic goal management is performed via the following
+  Isabelle/Pure rules:
 
   \[
   \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
   \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
   \]

   \indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
   \end{mldecls}
 
   \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
   for any number of pending subgoals.
 

   \secref{sec:tactical-goals}.  Further checks are required to ensure
   that the result is actually an instance of the original claim --
   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
   operation, such that the user merely needs to provide the statement
   and tactic to be applied.%