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