wenzelm@26846: theory ML_Tactic wenzelm@26846: imports Main wenzelm@26846: begin wenzelm@26846: wenzelm@26852: chapter {* ML tactic expressions *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: Isar Proof methods closely resemble traditional tactics, when used wenzelm@26846: in unstructured sequences of @{command "apply"} commands. wenzelm@26846: Isabelle/Isar provides emulations for all major ML tactics of wenzelm@26846: classic Isabelle --- mostly for the sake of easy porting of existing wenzelm@26846: developments, as actual Isar proof texts would demand much less wenzelm@26846: diversity of proof methods. wenzelm@26846: wenzelm@26846: Unlike tactic expressions in ML, Isar proof methods provide proper wenzelm@26846: concrete syntax for additional arguments, options, modifiers etc. wenzelm@26846: Thus a typical method text is usually more concise than the wenzelm@26846: corresponding ML tactic. Furthermore, the Isar versions of classic wenzelm@26846: Isabelle tactics often cover several variant forms by a single wenzelm@26846: method with separate options to tune the behavior. For example, wenzelm@26846: method @{method simp} replaces all of @{ML simp_tac}~/ @{ML wenzelm@26846: asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there wenzelm@26846: is also concrete syntax for augmenting the Simplifier context (the wenzelm@26846: current ``simpset'') in a convenient way. wenzelm@26846: *} wenzelm@26846: wenzelm@26846: wenzelm@26846: section {* Resolution tactics *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: Classic Isabelle provides several variant forms of tactics for wenzelm@26846: single-step rule applications (based on higher-order resolution). wenzelm@26846: The space of resolution tactics has the following main dimensions. wenzelm@26846: wenzelm@26846: \begin{enumerate} wenzelm@26846: wenzelm@26846: \item The ``mode'' of resolution: intro, elim, destruct, or forward wenzelm@26846: (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac}, wenzelm@26846: @{ML forward_tac}). wenzelm@26846: wenzelm@26846: \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ wenzelm@27239: @{ML res_inst_tac}). wenzelm@26846: wenzelm@26846: \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} wenzelm@26846: vs.\ @{ML rtac}). wenzelm@26846: wenzelm@26846: \end{enumerate} wenzelm@26846: wenzelm@26846: Basically, the set of Isar tactic emulations @{method rule_tac}, wenzelm@26846: @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see wenzelm@26846: \secref{sec:tactics}) would be sufficient to cover the four modes, wenzelm@26846: either with or without instantiation, and either with single or wenzelm@26846: multiple arguments. Although it is more convenient in most cases to wenzelm@26846: use the plain @{method rule} method (see wenzelm@26846: \secref{sec:pure-meth-att}), or any of its ``improper'' variants wenzelm@26846: @{method erule}, @{method drule}, @{method frule} (see wenzelm@26846: \secref{sec:misc-meth-att}). Note that explicit goal addressing is wenzelm@26846: only supported by the actual @{method rule_tac} version. wenzelm@26846: wenzelm@26846: With this in mind, plain resolution tactics correspond to Isar wenzelm@26846: methods as follows. wenzelm@26846: wenzelm@26846: \medskip wenzelm@26846: \begin{tabular}{lll} wenzelm@26846: @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ wenzelm@26846: @{ML resolve_tac}~@{text "[a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ wenzelm@27239: @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a 1"} & & wenzelm@26846: @{text "rule_tac x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\[0.5ex] wenzelm@26846: @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ wenzelm@26846: @{ML resolve_tac}~@{text "[a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ wenzelm@27239: @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a i"} & & wenzelm@26846: @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\ wenzelm@26846: \end{tabular} wenzelm@26846: \medskip wenzelm@26846: wenzelm@26846: Note that explicit goal addressing may be usually avoided by wenzelm@26846: changing the order of subgoals with @{command "defer"} or @{command wenzelm@26846: "prefer"} (see \secref{sec:tactic-commands}). wenzelm@26846: *} wenzelm@26846: wenzelm@26846: wenzelm@26846: section {* Simplifier tactics *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: The main Simplifier tactics @{ML simp_tac} and variants (cf.\ wenzelm@26846: \cite{isabelle-ref}) are all covered by the @{method simp} and wenzelm@26846: @{method simp_all} methods (see \secref{sec:simplifier}). Note that wenzelm@26846: there is no individual goal addressing available, simplification wenzelm@26846: acts either on the first goal (@{method simp}) or all goals wenzelm@26846: (@{method simp_all}). wenzelm@26846: wenzelm@26846: \medskip wenzelm@26846: \begin{tabular}{lll} wenzelm@26846: @{ML asm_full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp} \\ wenzelm@26846: @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{simpset}"}) & & @{method simp_all} \\[0.5ex] wenzelm@26846: @{ML simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm)"} \\ wenzelm@26846: @{ML asm_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\ wenzelm@26846: @{ML full_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\ wenzelm@26846: @{ML asm_lr_simp_tac}~@{text "@{simpset} 1"} & & @{method simp}~@{text "(asm_lr)"} \\ wenzelm@26846: \end{tabular} wenzelm@26846: \medskip wenzelm@26846: *} wenzelm@26846: wenzelm@26846: wenzelm@26846: section {* Classical Reasoner tactics *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: The Classical Reasoner provides a rather large number of variations wenzelm@26846: of automated tactics, such as @{ML blast_tac}, @{ML fast_tac}, @{ML wenzelm@26846: clarify_tac} etc.\ (see \cite{isabelle-ref}). The corresponding wenzelm@26846: Isar methods usually share the same base name, such as @{method wenzelm@26846: blast}, @{method fast}, @{method clarify} etc.\ (see wenzelm@26846: \secref{sec:classical}). wenzelm@26846: *} wenzelm@26846: wenzelm@26846: wenzelm@26846: section {* Miscellaneous tactics *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: There are a few additional tactics defined in various theories of wenzelm@26846: Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF. wenzelm@26846: The most common ones of these may be ported to Isar as follows. wenzelm@26846: wenzelm@26846: \medskip wenzelm@26846: \begin{tabular}{lll} wenzelm@26846: @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\ wenzelm@26846: @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\ wenzelm@26846: @{ML strip_tac}~@{text 1} & @{text "\"} & @{text "intro strip"} \\ wenzelm@26846: @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\ wenzelm@26846: & @{text "\"} & @{text "simp only: split_tupled_all"} \\ wenzelm@26846: & @{text "\"} & @{text "clarify"} \\ wenzelm@26846: \end{tabular} wenzelm@26846: *} wenzelm@26846: wenzelm@26846: wenzelm@26846: section {* Tacticals *} wenzelm@26846: wenzelm@26846: text {* wenzelm@26846: Classic Isabelle provides a huge amount of tacticals for combination wenzelm@26846: and modification of existing tactics. This has been greatly reduced wenzelm@26846: in Isar, providing the bare minimum of combinators only: ``@{text wenzelm@26846: ","}'' (sequential composition), ``@{text "|"}'' (alternative wenzelm@26846: choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least wenzelm@26846: once). These are usually sufficient in practice; if all fails, wenzelm@26846: arbitrary ML tactic code may be invoked via the @{method tactic} wenzelm@26846: method (see \secref{sec:tactics}). wenzelm@26846: wenzelm@26846: \medskip Common ML tacticals may be expressed directly in Isar as wenzelm@26846: follows: wenzelm@26846: wenzelm@26846: \medskip wenzelm@26846: \begin{tabular}{lll} wenzelm@26846: @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\ wenzelm@26846: @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\ wenzelm@26846: @{ML TRY}~@{text tac} & & @{text "meth?"} \\ wenzelm@26846: @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\ wenzelm@26846: @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\ wenzelm@26846: @{ML EVERY}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1, \"} \\ wenzelm@26846: @{ML FIRST}~@{text "[tac\<^sub>1, \]"} & & @{text "meth\<^sub>1 | \"} \\ wenzelm@26846: \end{tabular} wenzelm@26846: \medskip wenzelm@26846: wenzelm@26846: \medskip @{ML CHANGED} (see \cite{isabelle-ref}) is usually not wenzelm@26846: required in Isar, since most basic proof methods already fail unless wenzelm@26846: there is an actual change in the goal state. Nevertheless, ``@{text wenzelm@26846: "?"}'' (try) may be used to accept \emph{unchanged} results as wenzelm@26846: well. wenzelm@26846: wenzelm@26846: \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see wenzelm@26846: \cite{isabelle-ref}) are not available in Isar, since there is no wenzelm@26846: direct goal addressing. Nevertheless, some basic methods address wenzelm@26846: all goals internally, notably @{method simp_all} (see wenzelm@26846: \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be wenzelm@26846: often replaced by ``@{text "+"}'' (repeat at least once), although wenzelm@26846: this usually has a different operational behavior, such as solving wenzelm@26846: goals in a different order. wenzelm@26846: wenzelm@26846: \medskip Iterated resolution, such as @{ML_text "REPEAT (FIRSTGOAL wenzelm@26846: (resolve_tac \))"}, is usually better expressed using the @{method wenzelm@26846: intro} and @{method elim} methods of Isar (see wenzelm@26846: \secref{sec:classical}). wenzelm@26846: *} wenzelm@26846: wenzelm@26846: end