doc-src/IsarImplementation/Thy/tactic.thy

tuned;

(* $Id$ *)

theory tactic imports base begin

chapter {* Tactical 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.  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).}: 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 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.

  \medskip Basic goal management is performed via the following
  Isabelle/Pure rules:

  \[
  \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
  \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
  \]

  \medskip The following low-level variants admit general reasoning
  with protected propositions:

  \[
  \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad
  \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}
  \]
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML Goal.init: "cterm -> thm"} \\
  @{index_ML Goal.finish: "thm -> thm"} \\
  @{index_ML Goal.protect: "thm -> thm"} \\
  @{index_ML Goal.conclude: "thm -> thm"} \\
  \end{mldecls}

  \begin{description}

  \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 (no subgoals), and concludes
  the result by removing the goal protection.

  \item @{ML "Goal.protect"}~@{text "th"} protects the full statement
  of theorem @{text "th"}.

  \item @{ML "Goal.conclude"}~@{text "th"} removes the goal protection
  for any number of pending subgoals.

  \end{description}
*}


section {* Tactics *}

text {*

FIXME

\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
to a lazy sequence of possible sucessors.  This scheme subsumes
failure (empty result sequence), as well as lazy enumeration of proof
search results.  Error conditions are usually mapped to an empty
result, which gives further tactics a chance to try in turn.
Commonly, tactics either take an argument to address a particular
subgoal, or operate on a certain range of subgoals in a uniform
fashion.  In any case, the main conclusion is normally left untouched,
apart from instantiating \seeglossary{schematic variables}.}


*}

section {* Tacticals *}

text {*

FIXME

\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.}

*}

section {* Programmed proofs *}

text {*
  In order to perform a complete tactical proof under program control,
  one needs to set up an initial goal configuration, apply a tactic,
  and finish the result, cf.\ the rules given in
  \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.  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.
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
  ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
  @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
  ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
  @{index_ML Goal.prove_global: "theory -> string list -> term list -> term ->
  (thm list -> tactic) -> thm"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
  "C"} in the context of arbitrary-but-fixed parameters @{text "xs"}
  and hypotheses @{text "As"} and applies tactic @{text "tac"} to
  solve it.  The latter may depend on the local assumptions being
  presented as facts.  The result is essentially @{text "\<And>xs. As \<Longrightarrow>
  C"}, but is normalized by pulling @{text "\<And>"} before @{text "\<Longrightarrow>"}
  (the conclusion @{text "C"} itself may be a rule statement), turning
  the quantifier prefix into schematic variables, and generalizing
  implicit type-variables.

  \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
  states several conclusions simultaneously.  @{ML
  Tactic.conjunction_tac} may be used to split these into individual
  subgoals before commencing the actual proof.

  \item @{ML Goal.prove_global} is a degraded version of @{ML
  Goal.prove} for theory level goals; it includes a global @{ML
  Drule.standard} for the result.

  \end{description}
*}

end