src/Doc/Isar_Ref/ML_Tactic.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59763 56d2c357e6b5
permissions -rw-r--r--
tuned signature;
     1 theory ML_Tactic
     2 imports Base Main
     3 begin
     4 
     5 chapter \<open>ML tactic expressions\<close>
     6 
     7 text \<open>
     8   Isar Proof methods closely resemble traditional tactics, when used
     9   in unstructured sequences of @{command "apply"} commands.
    10   Isabelle/Isar provides emulations for all major ML tactics of
    11   classic Isabelle --- mostly for the sake of easy porting of existing
    12   developments, as actual Isar proof texts would demand much less
    13   diversity of proof methods.
    14 
    15   Unlike tactic expressions in ML, Isar proof methods provide proper
    16   concrete syntax for additional arguments, options, modifiers etc.
    17   Thus a typical method text is usually more concise than the
    18   corresponding ML tactic.  Furthermore, the Isar versions of classic
    19   Isabelle tactics often cover several variant forms by a single
    20   method with separate options to tune the behavior.  For example,
    21   method @{method simp} replaces all of @{ML simp_tac}~/ @{ML
    22   asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there
    23   is also concrete syntax for augmenting the Simplifier context (the
    24   current ``simpset'') in a convenient way.
    25 \<close>
    26 
    27 
    28 section \<open>Resolution tactics\<close>
    29 
    30 text \<open>
    31   Classic Isabelle provides several variant forms of tactics for
    32   single-step rule applications (based on higher-order resolution).
    33   The space of resolution tactics has the following main dimensions.
    34 
    35   \begin{enumerate}
    36 
    37   \item The ``mode'' of resolution: intro, elim, destruct, or forward
    38   (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
    39   @{ML forward_tac}).
    40 
    41   \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
    42   @{ML Rule_Insts.res_inst_tac}).
    43 
    44   \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
    45   vs.\ @{ML rtac}).
    46 
    47   \end{enumerate}
    48 
    49   Basically, the set of Isar tactic emulations @{method rule_tac},
    50   @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see
    51   \secref{sec:tactics}) would be sufficient to cover the four modes,
    52   either with or without instantiation, and either with single or
    53   multiple arguments.  Although it is more convenient in most cases to
    54   use the plain @{method_ref (Pure) rule} method, or any of its
    55   ``improper'' variants @{method erule}, @{method drule}, @{method
    56   frule}.  Note that explicit goal addressing is only supported by the
    57   actual @{method rule_tac} version.
    58 
    59   With this in mind, plain resolution tactics correspond to Isar
    60   methods as follows.
    61 
    62   \medskip
    63   \begin{tabular}{lll}
    64     @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
    65     @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
    66     @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    67     @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
    68     @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
    69     @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
    70     @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    71     @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
    72   \end{tabular}
    73   \medskip
    74 
    75   Note that explicit goal addressing may be usually avoided by
    76   changing the order of subgoals with @{command "defer"} or @{command
    77   "prefer"} (see \secref{sec:tactic-commands}).
    78 \<close>
    79 
    80 
    81 section \<open>Simplifier tactics\<close>
    82 
    83 text \<open>The main Simplifier tactics @{ML simp_tac} and variants are
    84   all covered by the @{method simp} and @{method simp_all} methods
    85   (see \secref{sec:simplifier}).  Note that there is no individual
    86   goal addressing available, simplification acts either on the first
    87   goal (@{method simp}) or all goals (@{method simp_all}).
    88 
    89   \medskip
    90   \begin{tabular}{lll}
    91     @{ML asm_full_simp_tac}~@{text "@{context} 1"} & & @{method simp} \\
    92     @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex]
    93     @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\
    94     @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\
    95     @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\
    96     @{ML asm_lr_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(asm_lr)"} \\
    97   \end{tabular}
    98   \medskip
    99 \<close>
   100 
   101 
   102 section \<open>Classical Reasoner tactics\<close>
   103 
   104 text \<open>The Classical Reasoner provides a rather large number of
   105   variations of automated tactics, such as @{ML blast_tac}, @{ML
   106   fast_tac}, @{ML clarify_tac} etc.  The corresponding Isar methods
   107   usually share the same base name, such as @{method blast}, @{method
   108   fast}, @{method clarify} etc.\ (see \secref{sec:classical}).\<close>
   109 
   110 
   111 section \<open>Miscellaneous tactics\<close>
   112 
   113 text \<open>
   114   There are a few additional tactics defined in various theories of
   115   Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
   116   The most common ones of these may be ported to Isar as follows.
   117 
   118   \medskip
   119   \begin{tabular}{lll}
   120     @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
   121     @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
   122     @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
   123       & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
   124       & @{text "\<lless>"} & @{text "clarify"} \\
   125   \end{tabular}
   126 \<close>
   127 
   128 
   129 section \<open>Tacticals\<close>
   130 
   131 text \<open>
   132   Classic Isabelle provides a huge amount of tacticals for combination
   133   and modification of existing tactics.  This has been greatly reduced
   134   in Isar, providing the bare minimum of combinators only: ``@{text
   135   ","}'' (sequential composition), ``@{text "|"}'' (alternative
   136   choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least
   137   once).  These are usually sufficient in practice; if all fails,
   138   arbitrary ML tactic code may be invoked via the @{method tactic}
   139   method (see \secref{sec:tactics}).
   140 
   141   \medskip Common ML tacticals may be expressed directly in Isar as
   142   follows:
   143 
   144   \medskip
   145   \begin{tabular}{lll}
   146     @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\
   147     @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\
   148     @{ML TRY}~@{text tac} & & @{text "meth?"} \\
   149     @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\
   150     @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\
   151     @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\
   152     @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\
   153   \end{tabular}
   154   \medskip
   155 
   156   \medskip @{ML CHANGED} (see @{cite "isabelle-implementation"}) is
   157   usually not required in Isar, since most basic proof methods already
   158   fail unless there is an actual change in the goal state.
   159   Nevertheless, ``@{text "?"}''  (try) may be used to accept
   160   \emph{unchanged} results as well.
   161 
   162   \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see
   163   @{cite "isabelle-implementation"}) are not available in Isar, since
   164   there is no direct goal addressing.  Nevertheless, some basic
   165   methods address all goals internally, notably @{method simp_all}
   166   (see \secref{sec:simplifier}).  Also note that @{ML ALLGOALS} can be
   167   often replaced by ``@{text "+"}'' (repeat at least once), although
   168   this usually has a different operational behavior: subgoals are
   169   solved in a different order.
   170 
   171   \medskip Iterated resolution, such as
   172   @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better
   173   expressed using the @{method intro} and @{method elim} methods of
   174   Isar (see \secref{sec:classical}).
   175 \<close>
   176 
   177 end