--- a/doc-src/IsarImplementation/Thy/tactic.thy Thu Feb 26 11:21:29 2009 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,420 +0,0 @@
-
-(* $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. 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 {* A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
- maps a given goal state (represented as a theorem, cf.\
- \secref{sec:tactical-goals}) to a lazy sequence of potential
- successor states. The underlying sequence implementation is lazy
- both in head and tail, and is purely functional in \emph{not}
- supporting memoing.\footnote{The lack of memoing and the strict
- nature of SML requires some care when working with low-level
- sequence operations, to avoid duplicate or premature evaluation of
- results.}
-
- An \emph{empty result sequence} means that the tactic has failed: in
- a compound tactic expressions other tactics might be tried instead,
- or the whole refinement step might fail outright, producing a
- toplevel error message. When implementing tactics from scratch, one
- should take care to observe the basic protocol of mapping regular
- error conditions to an empty result; only serious faults should
- emerge as exceptions.
-
- By enumerating \emph{multiple results}, a tactic can easily express
- the potential outcome of an internal search process. There are also
- combinators for building proof tools that involve search
- systematically, see also \secref{sec:tacticals}.
-
- \medskip As explained in \secref{sec:tactical-goals}, a goal state
- essentially consists of a list of subgoals that imply the main goal
- (conclusion). Tactics may operate on all subgoals or on a
- particularly specified subgoal, but must not change the main
- conclusion (apart from instantiating schematic goal variables).
-
- Tactics with explicit \emph{subgoal addressing} are of the form
- @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
- (counting from 1). If the subgoal number is out of range, the
- tactic should fail with an empty result sequence, but must not raise
- an exception!
-
- Operating on a particular subgoal means to replace it by an interval
- of zero or more subgoals in the same place; other subgoals must not
- be affected, apart from instantiating schematic variables ranging
- over the whole goal state.
-
- A common pattern of composing tactics with subgoal addressing is to
- try the first one, and then the second one only if the subgoal has
- not been solved yet. Special care is required here to avoid bumping
- into unrelated subgoals that happen to come after the original
- subgoal. Assuming that there is only a single initial subgoal is a
- very common error when implementing tactics!
-
- Tactics with internal subgoal addressing should expose the subgoal
- index as @{text "int"} argument in full generality; a hardwired
- subgoal 1 inappropriate.
-
- \medskip The main well-formedness conditions for proper tactics are
- summarized as follows.
-
- \begin{itemize}
-
- \item General tactic failure is indicated by an empty result, only
- serious faults may produce an exception.
-
- \item The main conclusion must not be changed, apart from
- instantiating schematic variables.
-
- \item A tactic operates either uniformly on all subgoals, or
- specifically on a selected subgoal (without bumping into unrelated
- subgoals).
-
- \item Range errors in subgoal addressing produce an empty result.
-
- \end{itemize}
-
- Some of these conditions are checked by higher-level goal
- infrastructure (\secref{sec:results}); others are not checked
- explicitly, and violating them merely results in ill-behaved tactics
- experienced by the user (e.g.\ tactics that insist in being
- applicable only to singleton goals, or disallow composition with
- basic tacticals).
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
- @{index_ML no_tac: tactic} \\
- @{index_ML all_tac: tactic} \\
- @{index_ML print_tac: "string -> tactic"} \\[1ex]
- @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
- @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
- @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML_type tactic} represents tactics. The well-formedness
- conditions described above need to be observed. See also @{"file"
- "~~/src/Pure/General/seq.ML"} for the underlying implementation of
- lazy sequences.
-
- \item @{ML_type "int -> tactic"} represents tactics with explicit
- subgoal addressing, with well-formedness conditions as described
- above.
-
- \item @{ML no_tac} is a tactic that always fails, returning the
- empty sequence.
-
- \item @{ML all_tac} is a tactic that always succeeds, returning a
- singleton sequence with unchanged goal state.
-
- \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but
- prints a message together with the goal state on the tracing
- channel.
-
- \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
- into a tactic with unique result. Exception @{ML THM} is considered
- a regular tactic failure and produces an empty result; other
- exceptions are passed through.
-
- \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
- most basic form to produce a tactic with subgoal addressing. The
- given abstraction over the subgoal term and subgoal number allows to
- peek at the relevant information of the full goal state. The
- subgoal range is checked as required above.
-
- \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
- subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This
- avoids expensive re-certification in situations where the subgoal is
- used directly for primitive inferences.
-
- \end{description}
-*}
-
-
-subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *}
-
-text {* \emph{Resolution} is the most basic mechanism for refining a
- subgoal using a theorem as object-level rule.
- \emph{Elim-resolution} is particularly suited for elimination rules:
- it resolves with a rule, proves its first premise by assumption, and
- finally deletes that assumption from any new subgoals.
- \emph{Destruct-resolution} is like elim-resolution, but the given
- destruction rules are first turned into canonical elimination
- format. \emph{Forward-resolution} is like destruct-resolution, but
- without deleting the selected assumption. The @{text "r/e/d/f"}
- naming convention is maintained for several different kinds of
- resolution rules and tactics.
-
- Assumption tactics close a subgoal by unifying some of its premises
- against its conclusion.
-
- \medskip All the tactics in this section operate on a subgoal
- designated by a positive integer. Other subgoals might be affected
- indirectly, due to instantiation of schematic variables.
-
- There are various sources of non-determinism, the tactic result
- sequence enumerates all possibilities of the following choices (if
- applicable):
-
- \begin{enumerate}
-
- \item selecting one of the rules given as argument to the tactic;
-
- \item selecting a subgoal premise to eliminate, unifying it against
- the first premise of the rule;
-
- \item unifying the conclusion of the subgoal to the conclusion of
- the rule.
-
- \end{enumerate}
-
- Recall that higher-order unification may produce multiple results
- that are enumerated here.
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
- @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
- @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
- @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
- @{index_ML assume_tac: "int -> tactic"} \\
- @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
- @{index_ML match_tac: "thm list -> int -> tactic"} \\
- @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
- @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
- using the given theorems, which should normally be introduction
- rules. The tactic resolves a rule's conclusion with subgoal @{text
- i}, replacing it by the corresponding versions of the rule's
- premises.
-
- \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
- with the given theorems, which should normally be elimination rules.
-
- \item @{ML dresolve_tac}~@{text "thms i"} performs
- destruct-resolution with the given theorems, which should normally
- be destruction rules. This replaces an assumption by the result of
- applying one of the rules.
-
- \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
- selected assumption is not deleted. It applies a rule to an
- assumption, adding the result as a new assumption.
-
- \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
- by assumption (modulo higher-order unification).
-
- \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
- only for immediate @{text "\<alpha>"}-convertibility instead of using
- unification. It succeeds (with a unique next state) if one of the
- assumptions is equal to the subgoal's conclusion. Since it does not
- instantiate variables, it cannot make other subgoals unprovable.
-
- \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
- similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
- dresolve_tac}, respectively, but do not instantiate schematic
- variables in the goal state.
-
- Flexible subgoals are not updated at will, but are left alone.
- Strictly speaking, matching means to treat the unknowns in the goal
- state as constants; these tactics merely discard unifiers that would
- update the goal state.
-
- \end{description}
-*}
-
-
-subsection {* Explicit instantiation within a subgoal context *}
-
-text {* The main resolution tactics (\secref{sec:resolve-assume-tac})
- use higher-order unification, which works well in many practical
- situations despite its daunting theoretical properties.
- Nonetheless, there are important problem classes where unguided
- higher-order unification is not so useful. This typically involves
- rules like universal elimination, existential introduction, or
- equational substitution. Here the unification problem involves
- fully flexible @{text "?P ?x"} schemes, which are hard to manage
- without further hints.
-
- By providing a (small) rigid term for @{text "?x"} explicitly, the
- remaining unification problem is to assign a (large) term to @{text
- "?P"}, according to the shape of the given subgoal. This is
- sufficiently well-behaved in most practical situations.
-
- \medskip Isabelle provides separate versions of the standard @{text
- "r/e/d/f"} resolution tactics that allow to provide explicit
- instantiations of unknowns of the given rule, wrt.\ terms that refer
- to the implicit context of the selected subgoal.
-
- An instantiation consists of a list of pairs of the form @{text
- "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
- the given rule, and @{text t} is a term from the current proof
- context, augmented by the local goal parameters of the selected
- subgoal; cf.\ the @{text "focus"} operation described in
- \secref{sec:variables}.
-
- Entering the syntactic context of a subgoal is a brittle operation,
- because its exact form is somewhat accidental, and the choice of
- bound variable names depends on the presence of other local and
- global names. Explicit renaming of subgoal parameters prior to
- explicit instantiation might help to achieve a bit more robustness.
-
- Type instantiations may be given as well, via pairs like @{text
- "(?'a, \<tau>)"}. Type instantiations are distinguished from term
- instantiations by the syntactic form of the schematic variable.
- Types are instantiated before terms are. Since term instantiation
- already performs type-inference as expected, explicit type
- instantiations are seldom necessary.
-*}
-
-text %mlref {*
- \begin{mldecls}
- @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
- @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex]
- @{index_ML rename_tac: "string list -> int -> tactic"} \\
- \end{mldecls}
-
- \begin{description}
-
- \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
- rule @{text thm} with the instantiations @{text insts}, as described
- above, and then performs resolution on subgoal @{text i}.
-
- \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
- elim-resolution.
-
- \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
- destruct-resolution.
-
- \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
- the selected assumption is not deleted.
-
- \item @{ML rename_tac}~@{text "names i"} renames the innermost
- parameters of subgoal @{text i} according to the provided @{text
- names} (which need to be distinct indentifiers).
-
- \end{description}
-*}
-
-
-section {* Tacticals \label{sec: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
-