wenzelm@30081: theory Tactic wenzelm@30081: imports Base wenzelm@30081: begin wenzelm@18537: wenzelm@20452: chapter {* Tactical reasoning *} wenzelm@18537: wenzelm@34997: text {* Tactical reasoning works by refining an initial claim in a wenzelm@20474: backwards fashion, until a solved form is reached. A @{text "goal"} wenzelm@20474: consists of several subgoals that need to be solved in order to wenzelm@20474: achieve the main statement; zero subgoals means that the proof may wenzelm@20474: be finished. A @{text "tactic"} is a refinement operation that maps wenzelm@20474: a goal to a lazy sequence of potential successors. A @{text wenzelm@34997: "tactical"} is a combinator for composing tactics. *} wenzelm@18537: wenzelm@18537: wenzelm@18537: section {* Goals \label{sec:tactical-goals} *} wenzelm@18537: wenzelm@20451: text {* wenzelm@30084: Isabelle/Pure represents a goal as a theorem stating that the wenzelm@30084: subgoals imply the main goal: @{text "A\<^sub>1 \ \ \ A\<^sub>n \ wenzelm@30084: C"}. The outermost goal structure is that of a Horn Clause: i.e.\ wenzelm@30084: an iterated implication without any quantifiers\footnote{Recall that wenzelm@30084: outermost @{text "\x. \[x]"} is always represented via schematic wenzelm@30084: variables in the body: @{text "\[?x]"}. These variables may get wenzelm@30084: instantiated during the course of reasoning.}. For @{text "n = 0"} wenzelm@30084: a goal is called ``solved''. wenzelm@18537: wenzelm@30087: The structure of each subgoal @{text "A\<^sub>i"} is that of a wenzelm@30087: general Hereditary Harrop Formula @{text "\x\<^sub>1 \ wenzelm@30087: \x\<^sub>k. H\<^sub>1 \ \ \ H\<^sub>m \ B"}. Here @{text wenzelm@30087: "x\<^sub>1, \, x\<^sub>k"} are goal parameters, i.e.\ wenzelm@30087: arbitrary-but-fixed entities of certain types, and @{text wenzelm@30087: "H\<^sub>1, \, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may wenzelm@30087: be assumed locally. Together, this forms the goal context of the wenzelm@30087: conclusion @{text B} to be established. The goal hypotheses may be wenzelm@30087: again arbitrary Hereditary Harrop Formulas, although the level of wenzelm@30087: nesting rarely exceeds 1--2 in practice. wenzelm@18537: wenzelm@20451: The main conclusion @{text C} is internally marked as a protected wenzelm@30084: proposition, which is represented explicitly by the notation @{text wenzelm@34997: "#C"} here. This ensures that the decomposition into subgoals and wenzelm@34997: main conclusion is well-defined for arbitrarily structured claims. wenzelm@18537: wenzelm@20451: \medskip Basic goal management is performed via the following wenzelm@20451: Isabelle/Pure rules: wenzelm@18537: wenzelm@18537: \[ wenzelm@18537: \infer[@{text "(init)"}]{@{text "C \ #C"}}{} \qquad wenzelm@20547: \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}} wenzelm@18537: \] wenzelm@18537: wenzelm@18537: \medskip The following low-level variants admit general reasoning wenzelm@18537: with protected propositions: wenzelm@18537: wenzelm@18537: \[ wenzelm@18537: \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad wenzelm@18537: \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ C"}}{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ #C"}} wenzelm@18537: \] wenzelm@18537: *} wenzelm@18537: wenzelm@18537: text %mlref {* wenzelm@18537: \begin{mldecls} wenzelm@18537: @{index_ML Goal.init: "cterm -> thm"} \\ wenzelm@32207: @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\ wenzelm@18537: @{index_ML Goal.protect: "thm -> thm"} \\ wenzelm@18537: @{index_ML Goal.conclude: "thm -> thm"} \\ wenzelm@18537: \end{mldecls} wenzelm@18537: wenzelm@18537: \begin{description} wenzelm@18537: wenzelm@20474: \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from wenzelm@20474: the well-formed proposition @{text C}. wenzelm@18537: wenzelm@32207: \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem wenzelm@20474: @{text "thm"} is a solved goal (no subgoals), and concludes the wenzelm@32207: result by removing the goal protection. The context is only wenzelm@32207: required for printing error messages. wenzelm@18537: wenzelm@20474: \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement wenzelm@20474: of theorem @{text "thm"}. wenzelm@18537: wenzelm@20474: \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal wenzelm@20474: protection, even if there are pending subgoals. wenzelm@18537: wenzelm@18537: \end{description} wenzelm@18537: *} wenzelm@18537: wenzelm@18537: wenzelm@18537: section {* Tactics *} wenzelm@18537: wenzelm@28781: text {* A @{text "tactic"} is a function @{text "goal \ goal\<^sup>*\<^sup>*"} that wenzelm@28781: maps a given goal state (represented as a theorem, cf.\ wenzelm@28781: \secref{sec:tactical-goals}) to a lazy sequence of potential wenzelm@28781: successor states. The underlying sequence implementation is lazy wenzelm@28781: both in head and tail, and is purely functional in \emph{not} wenzelm@28781: supporting memoing.\footnote{The lack of memoing and the strict wenzelm@28781: nature of SML requires some care when working with low-level wenzelm@28781: sequence operations, to avoid duplicate or premature evaluation of wenzelm@34997: results. It also means that modified runtime behavior, such as wenzelm@34997: timeout, is very hard to achieve for general tactics.} wenzelm@18537: wenzelm@28781: An \emph{empty result sequence} means that the tactic has failed: in wenzelm@34997: a compound tactic expression other tactics might be tried instead, wenzelm@28781: or the whole refinement step might fail outright, producing a wenzelm@34997: toplevel error message in the end. When implementing tactics from wenzelm@34997: scratch, one should take care to observe the basic protocol of wenzelm@34997: mapping regular error conditions to an empty result; only serious wenzelm@34997: faults should emerge as exceptions. wenzelm@18537: wenzelm@28781: By enumerating \emph{multiple results}, a tactic can easily express wenzelm@28781: the potential outcome of an internal search process. There are also wenzelm@28781: combinators for building proof tools that involve search wenzelm@28781: systematically, see also \secref{sec:tacticals}. wenzelm@18537: wenzelm@34997: \medskip As explained before, a goal state essentially consists of a wenzelm@34997: list of subgoals that imply the main goal (conclusion). Tactics may wenzelm@34997: operate on all subgoals or on a particularly specified subgoal, but wenzelm@34997: must not change the main conclusion (apart from instantiating wenzelm@34997: schematic goal variables). wenzelm@18537: wenzelm@28781: Tactics with explicit \emph{subgoal addressing} are of the form wenzelm@28781: @{text "int \ tactic"} and may be applied to a particular subgoal wenzelm@28781: (counting from 1). If the subgoal number is out of range, the wenzelm@28781: tactic should fail with an empty result sequence, but must not raise wenzelm@28781: an exception! wenzelm@28781: wenzelm@28781: Operating on a particular subgoal means to replace it by an interval wenzelm@28781: of zero or more subgoals in the same place; other subgoals must not wenzelm@28781: be affected, apart from instantiating schematic variables ranging wenzelm@28781: over the whole goal state. wenzelm@28781: wenzelm@28781: A common pattern of composing tactics with subgoal addressing is to wenzelm@28781: try the first one, and then the second one only if the subgoal has wenzelm@28781: not been solved yet. Special care is required here to avoid bumping wenzelm@28782: into unrelated subgoals that happen to come after the original wenzelm@28782: subgoal. Assuming that there is only a single initial subgoal is a wenzelm@28782: very common error when implementing tactics! wenzelm@28782: wenzelm@28782: Tactics with internal subgoal addressing should expose the subgoal wenzelm@28782: index as @{text "int"} argument in full generality; a hardwired wenzelm@34997: subgoal 1 is not acceptable. wenzelm@28781: wenzelm@28781: \medskip The main well-formedness conditions for proper tactics are wenzelm@28781: summarized as follows. wenzelm@28781: wenzelm@28781: \begin{itemize} wenzelm@28781: wenzelm@28781: \item General tactic failure is indicated by an empty result, only wenzelm@28781: serious faults may produce an exception. wenzelm@28781: wenzelm@28781: \item The main conclusion must not be changed, apart from wenzelm@28781: instantiating schematic variables. wenzelm@28781: wenzelm@28781: \item A tactic operates either uniformly on all subgoals, or wenzelm@28781: specifically on a selected subgoal (without bumping into unrelated wenzelm@28781: subgoals). wenzelm@28781: wenzelm@28781: \item Range errors in subgoal addressing produce an empty result. wenzelm@28781: wenzelm@28781: \end{itemize} wenzelm@28782: wenzelm@28782: Some of these conditions are checked by higher-level goal wenzelm@34997: infrastructure (\secref{sec:struct-goals}); others are not checked wenzelm@28782: explicitly, and violating them merely results in ill-behaved tactics wenzelm@28782: experienced by the user (e.g.\ tactics that insist in being wenzelm@34997: applicable only to singleton goals, or prevent composition via wenzelm@34997: standard tacticals). wenzelm@28782: *} wenzelm@28782: wenzelm@28782: text %mlref {* wenzelm@28782: \begin{mldecls} wenzelm@28782: @{index_ML_type tactic: "thm -> thm Seq.seq"} \\ wenzelm@28783: @{index_ML no_tac: tactic} \\ wenzelm@28783: @{index_ML all_tac: tactic} \\ wenzelm@28783: @{index_ML print_tac: "string -> tactic"} \\[1ex] wenzelm@28783: @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex] wenzelm@28782: @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\ wenzelm@28782: @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\ wenzelm@28782: \end{mldecls} wenzelm@28782: wenzelm@28782: \begin{description} wenzelm@28782: wenzelm@28782: \item @{ML_type tactic} represents tactics. The well-formedness wenzelm@28782: conditions described above need to be observed. See also @{"file" wenzelm@28782: "~~/src/Pure/General/seq.ML"} for the underlying implementation of wenzelm@28782: lazy sequences. wenzelm@28782: wenzelm@28782: \item @{ML_type "int -> tactic"} represents tactics with explicit wenzelm@28782: subgoal addressing, with well-formedness conditions as described wenzelm@28782: above. wenzelm@28782: wenzelm@28783: \item @{ML no_tac} is a tactic that always fails, returning the wenzelm@28783: empty sequence. wenzelm@28783: wenzelm@28783: \item @{ML all_tac} is a tactic that always succeeds, returning a wenzelm@28783: singleton sequence with unchanged goal state. wenzelm@28783: wenzelm@28783: \item @{ML print_tac}~@{text "message"} is like @{ML all_tac}, but wenzelm@28783: prints a message together with the goal state on the tracing wenzelm@28783: channel. wenzelm@28783: wenzelm@28782: \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule wenzelm@28782: into a tactic with unique result. Exception @{ML THM} is considered wenzelm@28782: a regular tactic failure and produces an empty result; other wenzelm@28782: exceptions are passed through. wenzelm@28782: wenzelm@28782: \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the wenzelm@28783: most basic form to produce a tactic with subgoal addressing. The wenzelm@28782: given abstraction over the subgoal term and subgoal number allows to wenzelm@28782: peek at the relevant information of the full goal state. The wenzelm@28782: subgoal range is checked as required above. wenzelm@28782: wenzelm@28782: \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the wenzelm@28783: subgoal as @{ML_type cterm} instead of raw @{ML_type term}. This wenzelm@28782: avoids expensive re-certification in situations where the subgoal is wenzelm@28782: used directly for primitive inferences. wenzelm@28782: wenzelm@28782: \end{description} wenzelm@18537: *} wenzelm@18537: wenzelm@28781: wenzelm@28785: subsection {* Resolution and assumption tactics \label{sec:resolve-assume-tac} *} wenzelm@28783: wenzelm@28783: text {* \emph{Resolution} is the most basic mechanism for refining a wenzelm@28783: subgoal using a theorem as object-level rule. wenzelm@28783: \emph{Elim-resolution} is particularly suited for elimination rules: wenzelm@28783: it resolves with a rule, proves its first premise by assumption, and wenzelm@28783: finally deletes that assumption from any new subgoals. wenzelm@28783: \emph{Destruct-resolution} is like elim-resolution, but the given wenzelm@28783: destruction rules are first turned into canonical elimination wenzelm@28783: format. \emph{Forward-resolution} is like destruct-resolution, but wenzelm@28785: without deleting the selected assumption. The @{text "r/e/d/f"} wenzelm@28785: naming convention is maintained for several different kinds of wenzelm@28785: resolution rules and tactics. wenzelm@28783: wenzelm@28783: Assumption tactics close a subgoal by unifying some of its premises wenzelm@28783: against its conclusion. wenzelm@28783: wenzelm@28783: \medskip All the tactics in this section operate on a subgoal wenzelm@28783: designated by a positive integer. Other subgoals might be affected wenzelm@28783: indirectly, due to instantiation of schematic variables. wenzelm@28783: wenzelm@28783: There are various sources of non-determinism, the tactic result wenzelm@28783: sequence enumerates all possibilities of the following choices (if wenzelm@28783: applicable): wenzelm@28783: wenzelm@28783: \begin{enumerate} wenzelm@28783: wenzelm@28783: \item selecting one of the rules given as argument to the tactic; wenzelm@28783: wenzelm@28783: \item selecting a subgoal premise to eliminate, unifying it against wenzelm@28783: the first premise of the rule; wenzelm@28783: wenzelm@28783: \item unifying the conclusion of the subgoal to the conclusion of wenzelm@28783: the rule. wenzelm@28783: wenzelm@28783: \end{enumerate} wenzelm@28783: wenzelm@28783: Recall that higher-order unification may produce multiple results wenzelm@28783: that are enumerated here. wenzelm@28783: *} wenzelm@28783: wenzelm@28783: text %mlref {* wenzelm@28783: \begin{mldecls} wenzelm@28783: @{index_ML resolve_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex] wenzelm@28783: @{index_ML assume_tac: "int -> tactic"} \\ wenzelm@28783: @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex] wenzelm@28783: @{index_ML match_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: @{index_ML ematch_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\ wenzelm@28783: \end{mldecls} wenzelm@28783: wenzelm@28783: \begin{description} wenzelm@28783: wenzelm@28783: \item @{ML resolve_tac}~@{text "thms i"} refines the goal state wenzelm@28783: using the given theorems, which should normally be introduction wenzelm@28783: rules. The tactic resolves a rule's conclusion with subgoal @{text wenzelm@28783: i}, replacing it by the corresponding versions of the rule's wenzelm@28783: premises. wenzelm@28783: wenzelm@28783: \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution wenzelm@28783: with the given theorems, which should normally be elimination rules. wenzelm@28783: wenzelm@28783: \item @{ML dresolve_tac}~@{text "thms i"} performs wenzelm@28783: destruct-resolution with the given theorems, which should normally wenzelm@28783: be destruction rules. This replaces an assumption by the result of wenzelm@28783: applying one of the rules. wenzelm@28783: wenzelm@28783: \item @{ML forward_tac} is like @{ML dresolve_tac} except that the wenzelm@28783: selected assumption is not deleted. It applies a rule to an wenzelm@28783: assumption, adding the result as a new assumption. wenzelm@28783: wenzelm@28783: \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i} wenzelm@28783: by assumption (modulo higher-order unification). wenzelm@28783: wenzelm@28783: \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks wenzelm@28783: only for immediate @{text "\"}-convertibility instead of using wenzelm@28783: unification. It succeeds (with a unique next state) if one of the wenzelm@28783: assumptions is equal to the subgoal's conclusion. Since it does not wenzelm@28783: instantiate variables, it cannot make other subgoals unprovable. wenzelm@28783: wenzelm@28783: \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are wenzelm@28783: similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML wenzelm@28783: dresolve_tac}, respectively, but do not instantiate schematic wenzelm@28783: variables in the goal state. wenzelm@28783: wenzelm@28783: Flexible subgoals are not updated at will, but are left alone. wenzelm@28783: Strictly speaking, matching means to treat the unknowns in the goal wenzelm@28783: state as constants; these tactics merely discard unifiers that would wenzelm@28783: update the goal state. wenzelm@28783: wenzelm@28783: \end{description} wenzelm@28783: *} wenzelm@28783: wenzelm@28783: wenzelm@28785: subsection {* Explicit instantiation within a subgoal context *} wenzelm@28785: wenzelm@28785: text {* The main resolution tactics (\secref{sec:resolve-assume-tac}) wenzelm@28785: use higher-order unification, which works well in many practical wenzelm@28785: situations despite its daunting theoretical properties. wenzelm@28785: Nonetheless, there are important problem classes where unguided wenzelm@28785: higher-order unification is not so useful. This typically involves wenzelm@28785: rules like universal elimination, existential introduction, or wenzelm@28785: equational substitution. Here the unification problem involves wenzelm@28785: fully flexible @{text "?P ?x"} schemes, which are hard to manage wenzelm@28785: without further hints. wenzelm@28785: wenzelm@28785: By providing a (small) rigid term for @{text "?x"} explicitly, the wenzelm@28785: remaining unification problem is to assign a (large) term to @{text wenzelm@28785: "?P"}, according to the shape of the given subgoal. This is wenzelm@28785: sufficiently well-behaved in most practical situations. wenzelm@28785: wenzelm@28785: \medskip Isabelle provides separate versions of the standard @{text wenzelm@28785: "r/e/d/f"} resolution tactics that allow to provide explicit wenzelm@28785: instantiations of unknowns of the given rule, wrt.\ terms that refer wenzelm@28785: to the implicit context of the selected subgoal. wenzelm@28785: wenzelm@28785: An instantiation consists of a list of pairs of the form @{text wenzelm@28785: "(?x, t)"}, where @{text ?x} is a schematic variable occurring in wenzelm@28785: the given rule, and @{text t} is a term from the current proof wenzelm@28785: context, augmented by the local goal parameters of the selected wenzelm@28785: subgoal; cf.\ the @{text "focus"} operation described in wenzelm@28785: \secref{sec:variables}. wenzelm@28785: wenzelm@28785: Entering the syntactic context of a subgoal is a brittle operation, wenzelm@28785: because its exact form is somewhat accidental, and the choice of wenzelm@28785: bound variable names depends on the presence of other local and wenzelm@28785: global names. Explicit renaming of subgoal parameters prior to wenzelm@28785: explicit instantiation might help to achieve a bit more robustness. wenzelm@28785: wenzelm@28785: Type instantiations may be given as well, via pairs like @{text wenzelm@28785: "(?'a, \)"}. Type instantiations are distinguished from term wenzelm@28785: instantiations by the syntactic form of the schematic variable. wenzelm@28785: Types are instantiated before terms are. Since term instantiation wenzelm@34997: already performs simple type-inference, so explicit type wenzelm@28785: instantiations are seldom necessary. wenzelm@28785: *} wenzelm@28785: wenzelm@28785: text %mlref {* wenzelm@28785: \begin{mldecls} wenzelm@28785: @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ wenzelm@28785: @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ wenzelm@28785: @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ wenzelm@28785: @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\[1ex] wenzelm@28785: @{index_ML rename_tac: "string list -> int -> tactic"} \\ wenzelm@28785: \end{mldecls} wenzelm@28785: wenzelm@28785: \begin{description} wenzelm@28785: wenzelm@28785: \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the wenzelm@28785: rule @{text thm} with the instantiations @{text insts}, as described wenzelm@28785: above, and then performs resolution on subgoal @{text i}. wenzelm@28785: wenzelm@28785: \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs wenzelm@28785: elim-resolution. wenzelm@28785: wenzelm@28785: \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs wenzelm@28785: destruct-resolution. wenzelm@28785: wenzelm@28785: \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that wenzelm@28785: the selected assumption is not deleted. wenzelm@28785: wenzelm@28785: \item @{ML rename_tac}~@{text "names i"} renames the innermost wenzelm@28785: parameters of subgoal @{text i} according to the provided @{text wenzelm@28785: names} (which need to be distinct indentifiers). wenzelm@28785: wenzelm@28785: \end{description} wenzelm@34997: wenzelm@34997: For historical reasons, the above instantiation tactics take wenzelm@34997: unparsed string arguments, which makes them hard to use in general wenzelm@34997: ML code. The slightly more advanced @{ML Subgoal.FOCUS} combinator wenzelm@34997: of \secref{sec:struct-goals} allows to refer to internal goal wenzelm@34997: structure with explicit context management. wenzelm@28785: *} wenzelm@28785: wenzelm@28785: wenzelm@28781: section {* Tacticals \label{sec:tacticals} *} wenzelm@18537: wenzelm@18537: text {* wenzelm@30084: A \emph{tactical} is a functional combinator for building up complex wenzelm@30084: tactics from simpler ones. Typical tactical perform sequential wenzelm@30084: composition, disjunction (choice), iteration, or goal addressing. wenzelm@30084: Various search strategies may be expressed via tacticals. wenzelm@18537: wenzelm@30084: \medskip FIXME wenzelm@18537: *} wenzelm@30273: wenzelm@18537: end