doc-src/IsarImplementation/Thy/tactic.thy

tuned;

(* $Id$ *)

theory tactic imports base begin

chapter {* Tactical reasoning *}

text {*
  Tactical reasoning works by refining the initial claim in a
  backwards fashion, until a solved form is reached.  A @{text "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"} in normal form where.
  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 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 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 C} initializes a tactical goal from
  the well-formed proposition @{text C}.

  \item @{ML "Goal.finish"}~@{text "thm"} checks whether theorem
  @{text "thm"} is a solved goal (no subgoals), and concludes the
  result by removing the goal protection.

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

  \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
  protection, even if there are 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.}

*}

end