
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, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
wenzelm@27239:     @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
wenzelm@26846:     @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
wenzelm@26846:     @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
wenzelm@26846:     @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
wenzelm@27239:     @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
wenzelm@26846:     @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> 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 "\<approx>"} & @{text "intro strip"} \\
wenzelm@26846:     @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
wenzelm@26846:       & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
wenzelm@26846:       & @{text "\<lless>"} & @{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, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\
wenzelm@26846:     @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\
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 \<dots>))"}, 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




