src/Doc/Implementation/Tactic.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
wenzelm@29755
     1
theory Tactic
wenzelm@29755
     2
imports Base
wenzelm@29755
     3
begin
wenzelm@18537
     4
wenzelm@58618
     5
chapter \<open>Tactical reasoning\<close>
wenzelm@18537
     6
wenzelm@58618
     7
text \<open>Tactical reasoning works by refining an initial claim in a
wenzelm@20474
     8
  backwards fashion, until a solved form is reached.  A @{text "goal"}
wenzelm@20474
     9
  consists of several subgoals that need to be solved in order to
wenzelm@20474
    10
  achieve the main statement; zero subgoals means that the proof may
wenzelm@20474
    11
  be finished.  A @{text "tactic"} is a refinement operation that maps
wenzelm@20474
    12
  a goal to a lazy sequence of potential successors.  A @{text
wenzelm@58618
    13
  "tactical"} is a combinator for composing tactics.\<close>
wenzelm@18537
    14
wenzelm@18537
    15
wenzelm@58618
    16
section \<open>Goals \label{sec:tactical-goals}\<close>
wenzelm@18537
    17
wenzelm@58618
    18
text \<open>
wenzelm@29758
    19
  Isabelle/Pure represents a goal as a theorem stating that the
wenzelm@29758
    20
  subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
wenzelm@29758
    21
  C"}.  The outermost goal structure is that of a Horn Clause: i.e.\
wenzelm@29758
    22
  an iterated implication without any quantifiers\footnote{Recall that
wenzelm@29758
    23
  outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
wenzelm@29758
    24
  variables in the body: @{text "\<phi>[?x]"}.  These variables may get
wenzelm@29758
    25
  instantiated during the course of reasoning.}.  For @{text "n = 0"}
wenzelm@29758
    26
  a goal is called ``solved''.
wenzelm@18537
    27
wenzelm@29761
    28
  The structure of each subgoal @{text "A\<^sub>i"} is that of a
wenzelm@29761
    29
  general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
wenzelm@29761
    30
  \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}.  Here @{text
wenzelm@29761
    31
  "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
wenzelm@29761
    32
  arbitrary-but-fixed entities of certain types, and @{text
wenzelm@29761
    33
  "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
wenzelm@29761
    34
  be assumed locally.  Together, this forms the goal context of the
wenzelm@29761
    35
  conclusion @{text B} to be established.  The goal hypotheses may be
wenzelm@29761
    36
  again arbitrary Hereditary Harrop Formulas, although the level of
wenzelm@29761
    37
  nesting rarely exceeds 1--2 in practice.
wenzelm@18537
    38
wenzelm@20451
    39
  The main conclusion @{text C} is internally marked as a protected
wenzelm@29758
    40
  proposition, which is represented explicitly by the notation @{text
wenzelm@34930
    41
  "#C"} here.  This ensures that the decomposition into subgoals and
wenzelm@34930
    42
  main conclusion is well-defined for arbitrarily structured claims.
wenzelm@18537
    43
wenzelm@20451
    44
  \medskip Basic goal management is performed via the following
wenzelm@20451
    45
  Isabelle/Pure rules:
wenzelm@18537
    46
wenzelm@18537
    47
  \[
wenzelm@18537
    48
  \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
wenzelm@20547
    49
  \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
wenzelm@18537
    50
  \]
wenzelm@18537
    51
wenzelm@18537
    52
  \medskip The following low-level variants admit general reasoning
wenzelm@18537
    53
  with protected propositions:
wenzelm@18537
    54
wenzelm@18537
    55
  \[
wenzelm@52456
    56
  \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
wenzelm@52456
    57
  \]
wenzelm@52456
    58
  \[
wenzelm@52456
    59
  \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
wenzelm@18537
    60
  \]
wenzelm@58618
    61
\<close>
wenzelm@18537
    62
wenzelm@58618
    63
text %mlref \<open>
wenzelm@18537
    64
  \begin{mldecls}
wenzelm@18537
    65
  @{index_ML Goal.init: "cterm -> thm"} \\
wenzelm@32201
    66
  @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
wenzelm@52456
    67
  @{index_ML Goal.protect: "int -> thm -> thm"} \\
wenzelm@18537
    68
  @{index_ML Goal.conclude: "thm -> thm"} \\
wenzelm@18537
    69
  \end{mldecls}
wenzelm@18537
    70
wenzelm@18537
    71
  \begin{description}
wenzelm@18537
    72
wenzelm@20474
    73
  \item @{ML "Goal.init"}~@{text C} initializes a tactical goal from
wenzelm@20474
    74
  the well-formed proposition @{text C}.
wenzelm@18537
    75
wenzelm@32201
    76
  \item @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
wenzelm@20474
    77
  @{text "thm"} is a solved goal (no subgoals), and concludes the
wenzelm@32201
    78
  result by removing the goal protection.  The context is only
wenzelm@32201
    79
  required for printing error messages.
wenzelm@18537
    80
wenzelm@52456
    81
  \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement
wenzelm@52456
    82
  of theorem @{text "thm"}.  The parameter @{text n} indicates the
wenzelm@52456
    83
  number of premises to be retained.
wenzelm@18537
    84
wenzelm@20474
    85
  \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal
wenzelm@20474
    86
  protection, even if there are pending subgoals.
wenzelm@18537
    87
wenzelm@18537
    88
  \end{description}
wenzelm@58618
    89
\<close>
wenzelm@18537
    90
wenzelm@18537
    91
wenzelm@58618
    92
section \<open>Tactics\label{sec:tactics}\<close>
wenzelm@18537
    93
wenzelm@58618
    94
text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
wenzelm@28781
    95
  maps a given goal state (represented as a theorem, cf.\
wenzelm@28781
    96
  \secref{sec:tactical-goals}) to a lazy sequence of potential
wenzelm@28781
    97
  successor states.  The underlying sequence implementation is lazy
wenzelm@28781
    98
  both in head and tail, and is purely functional in \emph{not}
wenzelm@28781
    99
  supporting memoing.\footnote{The lack of memoing and the strict
wenzelm@57421
   100
  nature of ML requires some care when working with low-level
wenzelm@28781
   101
  sequence operations, to avoid duplicate or premature evaluation of
wenzelm@34930
   102
  results.  It also means that modified runtime behavior, such as
wenzelm@34930
   103
  timeout, is very hard to achieve for general tactics.}
wenzelm@18537
   104
wenzelm@28781
   105
  An \emph{empty result sequence} means that the tactic has failed: in
wenzelm@34930
   106
  a compound tactic expression other tactics might be tried instead,
wenzelm@28781
   107
  or the whole refinement step might fail outright, producing a
wenzelm@34930
   108
  toplevel error message in the end.  When implementing tactics from
wenzelm@34930
   109
  scratch, one should take care to observe the basic protocol of
wenzelm@34930
   110
  mapping regular error conditions to an empty result; only serious
wenzelm@34930
   111
  faults should emerge as exceptions.
wenzelm@28781
   112
wenzelm@28781
   113
  By enumerating \emph{multiple results}, a tactic can easily express
wenzelm@28781
   114
  the potential outcome of an internal search process.  There are also
wenzelm@28781
   115
  combinators for building proof tools that involve search
wenzelm@28781
   116
  systematically, see also \secref{sec:tacticals}.
wenzelm@28781
   117
wenzelm@34930
   118
  \medskip As explained before, a goal state essentially consists of a
wenzelm@34930
   119
  list of subgoals that imply the main goal (conclusion).  Tactics may
wenzelm@34930
   120
  operate on all subgoals or on a particularly specified subgoal, but
wenzelm@34930
   121
  must not change the main conclusion (apart from instantiating
wenzelm@34930
   122
  schematic goal variables).
wenzelm@18537
   123
wenzelm@28781
   124
  Tactics with explicit \emph{subgoal addressing} are of the form
wenzelm@28781
   125
  @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
wenzelm@28781
   126
  (counting from 1).  If the subgoal number is out of range, the
wenzelm@28781
   127
  tactic should fail with an empty result sequence, but must not raise
wenzelm@28781
   128
  an exception!
wenzelm@28781
   129
wenzelm@28781
   130
  Operating on a particular subgoal means to replace it by an interval
wenzelm@28781
   131
  of zero or more subgoals in the same place; other subgoals must not
wenzelm@28781
   132
  be affected, apart from instantiating schematic variables ranging
wenzelm@28781
   133
  over the whole goal state.
wenzelm@28781
   134
wenzelm@28781
   135
  A common pattern of composing tactics with subgoal addressing is to
wenzelm@28781
   136
  try the first one, and then the second one only if the subgoal has
wenzelm@28781
   137
  not been solved yet.  Special care is required here to avoid bumping
wenzelm@28782
   138
  into unrelated subgoals that happen to come after the original
wenzelm@28782
   139
  subgoal.  Assuming that there is only a single initial subgoal is a
wenzelm@28782
   140
  very common error when implementing tactics!
wenzelm@28782
   141
wenzelm@28782
   142
  Tactics with internal subgoal addressing should expose the subgoal
wenzelm@28782
   143
  index as @{text "int"} argument in full generality; a hardwired
wenzelm@34930
   144
  subgoal 1 is not acceptable.
wenzelm@28781
   145
  
wenzelm@28781
   146
  \medskip The main well-formedness conditions for proper tactics are
wenzelm@28781
   147
  summarized as follows.
wenzelm@28781
   148
wenzelm@28781
   149
  \begin{itemize}
wenzelm@28781
   150
wenzelm@28781
   151
  \item General tactic failure is indicated by an empty result, only
wenzelm@28781
   152
  serious faults may produce an exception.
wenzelm@28781
   153
wenzelm@28781
   154
  \item The main conclusion must not be changed, apart from
wenzelm@28781
   155
  instantiating schematic variables.
wenzelm@28781
   156
wenzelm@28781
   157
  \item A tactic operates either uniformly on all subgoals, or
wenzelm@28781
   158
  specifically on a selected subgoal (without bumping into unrelated
wenzelm@28781
   159
  subgoals).
wenzelm@28781
   160
wenzelm@28781
   161
  \item Range errors in subgoal addressing produce an empty result.
wenzelm@28781
   162
wenzelm@28781
   163
  \end{itemize}
wenzelm@28782
   164
wenzelm@28782
   165
  Some of these conditions are checked by higher-level goal
wenzelm@34930
   166
  infrastructure (\secref{sec:struct-goals}); others are not checked
wenzelm@28782
   167
  explicitly, and violating them merely results in ill-behaved tactics
wenzelm@28782
   168
  experienced by the user (e.g.\ tactics that insist in being
wenzelm@34930
   169
  applicable only to singleton goals, or prevent composition via
wenzelm@46260
   170
  standard tacticals such as @{ML REPEAT}).
wenzelm@58618
   171
\<close>
wenzelm@28782
   172
wenzelm@58618
   173
text %mlref \<open>
wenzelm@28782
   174
  \begin{mldecls}
wenzelm@28782
   175
  @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
wenzelm@28783
   176
  @{index_ML no_tac: tactic} \\
wenzelm@28783
   177
  @{index_ML all_tac: tactic} \\
wenzelm@56491
   178
  @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
wenzelm@28783
   179
  @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
wenzelm@28782
   180
  @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
wenzelm@28782
   181
  @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
wenzelm@52463
   182
  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
wenzelm@52463
   183
  @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
wenzelm@28782
   184
  \end{mldecls}
wenzelm@28782
   185
wenzelm@28782
   186
  \begin{description}
wenzelm@28782
   187
wenzelm@39864
   188
  \item Type @{ML_type tactic} represents tactics.  The
wenzelm@39864
   189
  well-formedness conditions described above need to be observed.  See
wenzelm@40800
   190
  also @{file "~~/src/Pure/General/seq.ML"} for the underlying
wenzelm@39864
   191
  implementation of lazy sequences.
wenzelm@28782
   192
wenzelm@39864
   193
  \item Type @{ML_type "int -> tactic"} represents tactics with
wenzelm@39864
   194
  explicit subgoal addressing, with well-formedness conditions as
wenzelm@39864
   195
  described above.
wenzelm@28782
   196
wenzelm@28783
   197
  \item @{ML no_tac} is a tactic that always fails, returning the
wenzelm@28783
   198
  empty sequence.
wenzelm@28783
   199
wenzelm@28783
   200
  \item @{ML all_tac} is a tactic that always succeeds, returning a
wenzelm@28783
   201
  singleton sequence with unchanged goal state.
wenzelm@28783
   202
wenzelm@56491
   203
  \item @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
wenzelm@28783
   204
  prints a message together with the goal state on the tracing
wenzelm@28783
   205
  channel.
wenzelm@28783
   206
wenzelm@28782
   207
  \item @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
wenzelm@28782
   208
  into a tactic with unique result.  Exception @{ML THM} is considered
wenzelm@28782
   209
  a regular tactic failure and produces an empty result; other
wenzelm@28782
   210
  exceptions are passed through.
wenzelm@28782
   211
wenzelm@28782
   212
  \item @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
wenzelm@28783
   213
  most basic form to produce a tactic with subgoal addressing.  The
wenzelm@28782
   214
  given abstraction over the subgoal term and subgoal number allows to
wenzelm@28782
   215
  peek at the relevant information of the full goal state.  The
wenzelm@28782
   216
  subgoal range is checked as required above.
wenzelm@28782
   217
wenzelm@28782
   218
  \item @{ML CSUBGOAL} is similar to @{ML SUBGOAL}, but passes the
wenzelm@28783
   219
  subgoal as @{ML_type cterm} instead of raw @{ML_type term}.  This
wenzelm@28782
   220
  avoids expensive re-certification in situations where the subgoal is
wenzelm@28782
   221
  used directly for primitive inferences.
wenzelm@28782
   222
wenzelm@52463
   223
  \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
wenzelm@52463
   224
  specified subgoal @{text "i"}.  This rearranges subgoals and the
wenzelm@52463
   225
  main goal protection (\secref{sec:tactical-goals}), while retaining
wenzelm@52463
   226
  the syntactic context of the overall goal state (concerning
wenzelm@52463
   227
  schematic variables etc.).
wenzelm@52463
   228
wenzelm@52463
   229
  \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
wenzelm@52463
   230
  @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but
wenzelm@52463
   231
  without changing the main goal protection.
wenzelm@52463
   232
wenzelm@28782
   233
  \end{description}
wenzelm@58618
   234
\<close>
wenzelm@18537
   235
wenzelm@18537
   236
wenzelm@58618
   237
subsection \<open>Resolution and assumption tactics \label{sec:resolve-assume-tac}\<close>
wenzelm@28783
   238
wenzelm@58618
   239
text \<open>\emph{Resolution} is the most basic mechanism for refining a
wenzelm@28783
   240
  subgoal using a theorem as object-level rule.
wenzelm@28783
   241
  \emph{Elim-resolution} is particularly suited for elimination rules:
wenzelm@28783
   242
  it resolves with a rule, proves its first premise by assumption, and
wenzelm@28783
   243
  finally deletes that assumption from any new subgoals.
wenzelm@28783
   244
  \emph{Destruct-resolution} is like elim-resolution, but the given
wenzelm@28783
   245
  destruction rules are first turned into canonical elimination
wenzelm@28783
   246
  format.  \emph{Forward-resolution} is like destruct-resolution, but
wenzelm@28785
   247
  without deleting the selected assumption.  The @{text "r/e/d/f"}
wenzelm@28785
   248
  naming convention is maintained for several different kinds of
wenzelm@28785
   249
  resolution rules and tactics.
wenzelm@28783
   250
wenzelm@28783
   251
  Assumption tactics close a subgoal by unifying some of its premises
wenzelm@28783
   252
  against its conclusion.
wenzelm@28783
   253
wenzelm@28783
   254
  \medskip All the tactics in this section operate on a subgoal
wenzelm@28783
   255
  designated by a positive integer.  Other subgoals might be affected
wenzelm@28783
   256
  indirectly, due to instantiation of schematic variables.
wenzelm@28783
   257
wenzelm@28783
   258
  There are various sources of non-determinism, the tactic result
wenzelm@28783
   259
  sequence enumerates all possibilities of the following choices (if
wenzelm@28783
   260
  applicable):
wenzelm@28783
   261
wenzelm@28783
   262
  \begin{enumerate}
wenzelm@28783
   263
wenzelm@28783
   264
  \item selecting one of the rules given as argument to the tactic;
wenzelm@28783
   265
wenzelm@28783
   266
  \item selecting a subgoal premise to eliminate, unifying it against
wenzelm@28783
   267
  the first premise of the rule;
wenzelm@28783
   268
wenzelm@28783
   269
  \item unifying the conclusion of the subgoal to the conclusion of
wenzelm@28783
   270
  the rule.
wenzelm@28783
   271
wenzelm@28783
   272
  \end{enumerate}
wenzelm@28783
   273
wenzelm@28783
   274
  Recall that higher-order unification may produce multiple results
wenzelm@28783
   275
  that are enumerated here.
wenzelm@58618
   276
\<close>
wenzelm@28783
   277
wenzelm@58618
   278
text %mlref \<open>
wenzelm@28783
   279
  \begin{mldecls}
wenzelm@28783
   280
  @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
wenzelm@28783
   281
  @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
wenzelm@28783
   282
  @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
wenzelm@50072
   283
  @{index_ML forward_tac: "thm list -> int -> tactic"} \\
wenzelm@50072
   284
  @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
wenzelm@28783
   285
  @{index_ML assume_tac: "int -> tactic"} \\
wenzelm@28783
   286
  @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
wenzelm@58957
   287
  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
wenzelm@58957
   288
  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
wenzelm@58957
   289
  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
wenzelm@58957
   290
  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
wenzelm@28783
   291
  \end{mldecls}
wenzelm@28783
   292
wenzelm@28783
   293
  \begin{description}
wenzelm@28783
   294
wenzelm@28783
   295
  \item @{ML resolve_tac}~@{text "thms i"} refines the goal state
wenzelm@28783
   296
  using the given theorems, which should normally be introduction
wenzelm@28783
   297
  rules.  The tactic resolves a rule's conclusion with subgoal @{text
wenzelm@28783
   298
  i}, replacing it by the corresponding versions of the rule's
wenzelm@28783
   299
  premises.
wenzelm@28783
   300
wenzelm@28783
   301
  \item @{ML eresolve_tac}~@{text "thms i"} performs elim-resolution
wenzelm@46278
   302
  with the given theorems, which are normally be elimination rules.
wenzelm@46278
   303
wenzelm@46278
   304
  Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML
wenzelm@46278
   305
  assume_tac}, which facilitates mixing of assumption steps with
wenzelm@46278
   306
  genuine eliminations.
wenzelm@28783
   307
wenzelm@28783
   308
  \item @{ML dresolve_tac}~@{text "thms i"} performs
wenzelm@28783
   309
  destruct-resolution with the given theorems, which should normally
wenzelm@28783
   310
  be destruction rules.  This replaces an assumption by the result of
wenzelm@28783
   311
  applying one of the rules.
wenzelm@28783
   312
wenzelm@28783
   313
  \item @{ML forward_tac} is like @{ML dresolve_tac} except that the
wenzelm@28783
   314
  selected assumption is not deleted.  It applies a rule to an
wenzelm@28783
   315
  assumption, adding the result as a new assumption.
wenzelm@28783
   316
wenzelm@50072
   317
  \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state
wenzelm@50072
   318
  by resolution or elim-resolution on each rule, as indicated by its
wenzelm@50072
   319
  flag.  It affects subgoal @{text "i"} of the proof state.
wenzelm@50072
   320
wenzelm@50072
   321
  For each pair @{text "(flag, rule)"}, it applies resolution if the
wenzelm@50072
   322
  flag is @{text "false"} and elim-resolution if the flag is @{text
wenzelm@50072
   323
  "true"}.  A single tactic call handles a mixture of introduction and
wenzelm@50072
   324
  elimination rules, which is useful to organize the search process
wenzelm@50072
   325
  systematically in proof tools.
wenzelm@50072
   326
wenzelm@28783
   327
  \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
wenzelm@28783
   328
  by assumption (modulo higher-order unification).
wenzelm@28783
   329
wenzelm@28783
   330
  \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
wenzelm@28783
   331
  only for immediate @{text "\<alpha>"}-convertibility instead of using
wenzelm@28783
   332
  unification.  It succeeds (with a unique next state) if one of the
wenzelm@28783
   333
  assumptions is equal to the subgoal's conclusion.  Since it does not
wenzelm@28783
   334
  instantiate variables, it cannot make other subgoals unprovable.
wenzelm@28783
   335
wenzelm@50072
   336
  \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
wenzelm@50072
   337
  bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
wenzelm@50072
   338
  @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
paulson@53096
   339
  not instantiate schematic variables in the goal state.%
paulson@53096
   340
\footnote{Strictly speaking, matching means to treat the unknowns in the goal
paulson@53096
   341
  state as constants, but these tactics merely discard unifiers that would
paulson@53096
   342
  update the goal state. In rare situations (where the conclusion and 
paulson@53096
   343
  goal state have flexible terms at the same position), the tactic
paulson@53096
   344
  will fail even though an acceptable unifier exists.}
paulson@53096
   345
  These tactics were written for a specific application within the classical reasoner.
wenzelm@28783
   346
wenzelm@28783
   347
  Flexible subgoals are not updated at will, but are left alone.
wenzelm@28783
   348
  \end{description}
wenzelm@58618
   349
\<close>
wenzelm@28783
   350
wenzelm@28783
   351
wenzelm@58618
   352
subsection \<open>Explicit instantiation within a subgoal context\<close>
wenzelm@28785
   353
wenzelm@58618
   354
text \<open>The main resolution tactics (\secref{sec:resolve-assume-tac})
wenzelm@28785
   355
  use higher-order unification, which works well in many practical
wenzelm@28785
   356
  situations despite its daunting theoretical properties.
wenzelm@28785
   357
  Nonetheless, there are important problem classes where unguided
wenzelm@28785
   358
  higher-order unification is not so useful.  This typically involves
wenzelm@28785
   359
  rules like universal elimination, existential introduction, or
wenzelm@28785
   360
  equational substitution.  Here the unification problem involves
wenzelm@28785
   361
  fully flexible @{text "?P ?x"} schemes, which are hard to manage
wenzelm@28785
   362
  without further hints.
wenzelm@28785
   363
wenzelm@28785
   364
  By providing a (small) rigid term for @{text "?x"} explicitly, the
wenzelm@28785
   365
  remaining unification problem is to assign a (large) term to @{text
wenzelm@28785
   366
  "?P"}, according to the shape of the given subgoal.  This is
wenzelm@28785
   367
  sufficiently well-behaved in most practical situations.
wenzelm@28785
   368
wenzelm@28785
   369
  \medskip Isabelle provides separate versions of the standard @{text
wenzelm@28785
   370
  "r/e/d/f"} resolution tactics that allow to provide explicit
wenzelm@28785
   371
  instantiations of unknowns of the given rule, wrt.\ terms that refer
wenzelm@28785
   372
  to the implicit context of the selected subgoal.
wenzelm@28785
   373
wenzelm@28785
   374
  An instantiation consists of a list of pairs of the form @{text
wenzelm@28785
   375
  "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
wenzelm@28785
   376
  the given rule, and @{text t} is a term from the current proof
wenzelm@28785
   377
  context, augmented by the local goal parameters of the selected
wenzelm@28785
   378
  subgoal; cf.\ the @{text "focus"} operation described in
wenzelm@28785
   379
  \secref{sec:variables}.
wenzelm@28785
   380
wenzelm@28785
   381
  Entering the syntactic context of a subgoal is a brittle operation,
wenzelm@28785
   382
  because its exact form is somewhat accidental, and the choice of
wenzelm@28785
   383
  bound variable names depends on the presence of other local and
wenzelm@28785
   384
  global names.  Explicit renaming of subgoal parameters prior to
wenzelm@28785
   385
  explicit instantiation might help to achieve a bit more robustness.
wenzelm@28785
   386
wenzelm@28785
   387
  Type instantiations may be given as well, via pairs like @{text
wenzelm@28785
   388
  "(?'a, \<tau>)"}.  Type instantiations are distinguished from term
wenzelm@28785
   389
  instantiations by the syntactic form of the schematic variable.
wenzelm@28785
   390
  Types are instantiated before terms are.  Since term instantiation
wenzelm@34930
   391
  already performs simple type-inference, so explicit type
wenzelm@28785
   392
  instantiations are seldom necessary.
wenzelm@58618
   393
\<close>
wenzelm@28785
   394
wenzelm@58618
   395
text %mlref \<open>
wenzelm@28785
   396
  \begin{mldecls}
wenzelm@28785
   397
  @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@28785
   398
  @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@28785
   399
  @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@46271
   400
  @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\
wenzelm@46271
   401
  @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
wenzelm@46277
   402
  @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\
wenzelm@28785
   403
  @{index_ML rename_tac: "string list -> int -> tactic"} \\
wenzelm@28785
   404
  \end{mldecls}
wenzelm@28785
   405
wenzelm@28785
   406
  \begin{description}
wenzelm@28785
   407
wenzelm@28785
   408
  \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
wenzelm@28785
   409
  rule @{text thm} with the instantiations @{text insts}, as described
wenzelm@28785
   410
  above, and then performs resolution on subgoal @{text i}.
wenzelm@28785
   411
  
wenzelm@28785
   412
  \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
wenzelm@28785
   413
  elim-resolution.
wenzelm@28785
   414
wenzelm@28785
   415
  \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
wenzelm@28785
   416
  destruct-resolution.
wenzelm@28785
   417
wenzelm@28785
   418
  \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
wenzelm@28785
   419
  the selected assumption is not deleted.
wenzelm@28785
   420
wenzelm@46271
   421
  \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
wenzelm@46271
   422
  @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
wenzelm@46271
   423
  same as a new subgoal @{text "i + 1"} (in the original context).
wenzelm@46271
   424
wenzelm@46277
   425
  \item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
wenzelm@46277
   426
  premise from subgoal @{text i}.  Note that @{text \<phi>} may contain
wenzelm@46277
   427
  schematic variables, to abbreviate the intended proposition; the
wenzelm@46277
   428
  first matching subgoal premise will be deleted.  Removing useless
wenzelm@46277
   429
  premises from a subgoal increases its readability and can make
wenzelm@46277
   430
  search tactics run faster.
wenzelm@46277
   431
wenzelm@28785
   432
  \item @{ML rename_tac}~@{text "names i"} renames the innermost
wenzelm@28785
   433
  parameters of subgoal @{text i} according to the provided @{text
wenzelm@56579
   434
  names} (which need to be distinct identifiers).
wenzelm@28785
   435
wenzelm@28785
   436
  \end{description}
wenzelm@34930
   437
wenzelm@34930
   438
  For historical reasons, the above instantiation tactics take
wenzelm@34930
   439
  unparsed string arguments, which makes them hard to use in general
wenzelm@34930
   440
  ML code.  The slightly more advanced @{ML Subgoal.FOCUS} combinator
wenzelm@34930
   441
  of \secref{sec:struct-goals} allows to refer to internal goal
wenzelm@34930
   442
  structure with explicit context management.
wenzelm@58618
   443
\<close>
wenzelm@28785
   444
wenzelm@28785
   445
wenzelm@58618
   446
subsection \<open>Rearranging goal states\<close>
wenzelm@46274
   447
wenzelm@58618
   448
text \<open>In rare situations there is a need to rearrange goal states:
wenzelm@46274
   449
  either the overall collection of subgoals, or the local structure of
wenzelm@46274
   450
  a subgoal.  Various administrative tactics allow to operate on the
wenzelm@58618
   451
  concrete presentation these conceptual sets of formulae.\<close>
wenzelm@46274
   452
wenzelm@58618
   453
text %mlref \<open>
wenzelm@46274
   454
  \begin{mldecls}
wenzelm@46274
   455
  @{index_ML rotate_tac: "int -> int -> tactic"} \\
wenzelm@46276
   456
  @{index_ML distinct_subgoals_tac: tactic} \\
wenzelm@58950
   457
  @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
wenzelm@46274
   458
  \end{mldecls}
wenzelm@46274
   459
wenzelm@46274
   460
  \begin{description}
wenzelm@46274
   461
wenzelm@46274
   462
  \item @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal
wenzelm@46274
   463
  @{text i} by @{text n} positions: from right to left if @{text n} is
wenzelm@46274
   464
  positive, and from left to right if @{text n} is negative.
wenzelm@46274
   465
wenzelm@46276
   466
  \item @{ML distinct_subgoals_tac} removes duplicate subgoals from a
wenzelm@46276
   467
  proof state.  This is potentially inefficient.
wenzelm@46276
   468
wenzelm@46276
   469
  \item @{ML flexflex_tac} removes all flex-flex pairs from the proof
wenzelm@46276
   470
  state by applying the trivial unifier.  This drastic step loses
wenzelm@46276
   471
  information.  It is already part of the Isar infrastructure for
wenzelm@46276
   472
  facts resulting from goals, and rarely needs to be invoked manually.
wenzelm@46276
   473
wenzelm@46276
   474
  Flex-flex constraints arise from difficult cases of higher-order
wenzelm@46276
   475
  unification.  To prevent this, use @{ML res_inst_tac} to instantiate
wenzelm@46276
   476
  some variables in a rule.  Normally flex-flex constraints can be
wenzelm@46276
   477
  ignored; they often disappear as unknowns get instantiated.
wenzelm@46276
   478
wenzelm@46274
   479
  \end{description}
wenzelm@58618
   480
\<close>
wenzelm@46274
   481
wenzelm@50074
   482
wenzelm@58618
   483
subsection \<open>Raw composition: resolution without lifting\<close>
wenzelm@50074
   484
wenzelm@58618
   485
text \<open>
wenzelm@50074
   486
  Raw composition of two rules means resolving them without prior
wenzelm@50074
   487
  lifting or renaming of unknowns.  This low-level operation, which
wenzelm@50074
   488
  underlies the resolution tactics, may occasionally be useful for
wenzelm@52467
   489
  special effects.  Schematic variables are not renamed by default, so
wenzelm@52467
   490
  beware of clashes!
wenzelm@58618
   491
\<close>
wenzelm@50074
   492
wenzelm@58618
   493
text %mlref \<open>
wenzelm@50074
   494
  \begin{mldecls}
wenzelm@58956
   495
  @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
wenzelm@52467
   496
  @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
wenzelm@50074
   497
  @{index_ML_op COMP: "thm * thm -> thm"} \\
wenzelm@50074
   498
  \end{mldecls}
wenzelm@50074
   499
wenzelm@50074
   500
  \begin{description}
wenzelm@50074
   501
wenzelm@58956
   502
  \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
wenzelm@50074
   503
  @{text "i"} using @{text "rule"}, without lifting.  The @{text
wenzelm@50074
   504
  "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
wenzelm@50074
   505
  @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
wenzelm@50074
   506
  number of new subgoals.  If @{text "flag"} is @{text "true"} then it
wenzelm@50074
   507
  performs elim-resolution --- it solves the first premise of @{text
wenzelm@50074
   508
  "rule"} by assumption and deletes that assumption.
wenzelm@50074
   509
wenzelm@52465
   510
  \item @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
wenzelm@50074
   511
  regarded as an atomic formula, to solve premise @{text "i"} of
wenzelm@50074
   512
  @{text "thm\<^sub>2"}.  Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
wenzelm@52467
   513
  "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}.  The unique @{text "s"} that
wenzelm@53015
   514
  unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
wenzelm@52467
   515
  \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.  Multiple results are considered as
wenzelm@52467
   516
  error (exception @{ML THM}).
wenzelm@50074
   517
wenzelm@52467
   518
  \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
wenzelm@52467
   519
  (thm\<^sub>1, 1, thm\<^sub>2)"}.
wenzelm@50074
   520
wenzelm@50074
   521
  \end{description}
wenzelm@50074
   522
wenzelm@50074
   523
  \begin{warn}
wenzelm@50074
   524
  These low-level operations are stepping outside the structure
wenzelm@50074
   525
  imposed by regular rule resolution.  Used without understanding of
wenzelm@50074
   526
  the consequences, they may produce results that cause problems with
wenzelm@50074
   527
  standard rules and tactics later on.
wenzelm@50074
   528
  \end{warn}
wenzelm@58618
   529
\<close>
wenzelm@50074
   530
wenzelm@50074
   531
wenzelm@58618
   532
section \<open>Tacticals \label{sec:tacticals}\<close>
wenzelm@18537
   533
wenzelm@58618
   534
text \<open>A \emph{tactical} is a functional combinator for building up
wenzelm@46258
   535
  complex tactics from simpler ones.  Common tacticals perform
wenzelm@46258
   536
  sequential composition, disjunctive choice, iteration, or goal
wenzelm@46258
   537
  addressing.  Various search strategies may be expressed via
wenzelm@46258
   538
  tacticals.
wenzelm@58618
   539
\<close>
wenzelm@46258
   540
wenzelm@46258
   541
wenzelm@58618
   542
subsection \<open>Combining tactics\<close>
wenzelm@46258
   543
wenzelm@58618
   544
text \<open>Sequential composition and alternative choices are the most
wenzelm@46258
   545
  basic ways to combine tactics, similarly to ``@{verbatim ","}'' and
wenzelm@46258
   546
  ``@{verbatim "|"}'' in Isar method notation.  This corresponds to
wenzelm@46262
   547
  @{ML_op "THEN"} and @{ML_op "ORELSE"} in ML, but there are further
wenzelm@46262
   548
  possibilities for fine-tuning alternation of tactics such as @{ML_op
wenzelm@46258
   549
  "APPEND"}.  Further details become visible in ML due to explicit
wenzelm@46262
   550
  subgoal addressing.
wenzelm@58618
   551
\<close>
wenzelm@46258
   552
wenzelm@58618
   553
text %mlref \<open>
wenzelm@46258
   554
  \begin{mldecls}
wenzelm@46262
   555
  @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\
wenzelm@46262
   556
  @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\
wenzelm@46262
   557
  @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\
wenzelm@46258
   558
  @{index_ML "EVERY": "tactic list -> tactic"} \\
wenzelm@46258
   559
  @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
wenzelm@46258
   560
wenzelm@46262
   561
  @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
wenzelm@46262
   562
  @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
wenzelm@46262
   563
  @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
wenzelm@46258
   564
  @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
wenzelm@46258
   565
  @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
wenzelm@46258
   566
  \end{mldecls}
wenzelm@46258
   567
wenzelm@46258
   568
  \begin{description}
wenzelm@18537
   569
wenzelm@46262
   570
  \item @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential
wenzelm@46269
   571
  composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a goal
wenzelm@46269
   572
  state, it returns all states reachable in two steps by applying
wenzelm@46269
   573
  @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}.  First, it applies @{text
wenzelm@46269
   574
  "tac\<^sub>1"} to the goal state, getting a sequence of possible next
wenzelm@46269
   575
  states; then, it applies @{text "tac\<^sub>2"} to each of these and
wenzelm@46269
   576
  concatenates the results to produce again one flat sequence of
wenzelm@46269
   577
  states.
wenzelm@46258
   578
wenzelm@46262
   579
  \item @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
wenzelm@46262
   580
  between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Applied to a state, it
wenzelm@46262
   581
  tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text
wenzelm@46262
   582
  "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}.  This is a deterministic
wenzelm@46262
   583
  choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded
wenzelm@46262
   584
  from the result.
wenzelm@46258
   585
wenzelm@46262
   586
  \item @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the
wenzelm@46262
   587
  possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}.  Unlike
wenzelm@46262
   588
  @{ML_op "ORELSE"} there is \emph{no commitment} to either tactic, so
wenzelm@46262
   589
  @{ML_op "APPEND"} helps to avoid incompleteness during search, at
wenzelm@46262
   590
  the cost of potential inefficiencies.
wenzelm@39852
   591
wenzelm@46262
   592
  \item @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
wenzelm@46262
   593
  "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.
wenzelm@46262
   594
  Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always
wenzelm@46262
   595
  succeeds.
wenzelm@46258
   596
wenzelm@46262
   597
  \item @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
wenzelm@46262
   598
  "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text
wenzelm@46262
   599
  "tac\<^sub>n"}.  Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
wenzelm@46262
   600
  always fails.
wenzelm@46258
   601
wenzelm@46264
   602
  \item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
wenzelm@46266
   603
  tactics with explicit subgoal addressing.  So @{text
wenzelm@46264
   604
  "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
wenzelm@46264
   605
  "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
wenzelm@46258
   606
wenzelm@46264
   607
  The other primed tacticals work analogously.
wenzelm@46258
   608
wenzelm@46258
   609
  \end{description}
wenzelm@58618
   610
\<close>
wenzelm@30272
   611
wenzelm@46259
   612
wenzelm@58618
   613
subsection \<open>Repetition tacticals\<close>
wenzelm@46259
   614
wenzelm@58618
   615
text \<open>These tacticals provide further control over repetition of
wenzelm@46259
   616
  tactics, beyond the stylized forms of ``@{verbatim "?"}''  and
wenzelm@58618
   617
  ``@{verbatim "+"}'' in Isar method expressions.\<close>
wenzelm@46259
   618
wenzelm@58618
   619
text %mlref \<open>
wenzelm@46259
   620
  \begin{mldecls}
wenzelm@46259
   621
  @{index_ML "TRY": "tactic -> tactic"} \\
wenzelm@46266
   622
  @{index_ML "REPEAT": "tactic -> tactic"} \\
wenzelm@46266
   623
  @{index_ML "REPEAT1": "tactic -> tactic"} \\
wenzelm@46259
   624
  @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
wenzelm@46259
   625
  @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
wenzelm@46259
   626
  \end{mldecls}
wenzelm@46259
   627
wenzelm@46259
   628
  \begin{description}
wenzelm@46259
   629
wenzelm@46269
   630
  \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
wenzelm@46259
   631
  state and returns the resulting sequence, if non-empty; otherwise it
wenzelm@46259
   632
  returns the original state.  Thus, it applies @{text "tac"} at most
wenzelm@46259
   633
  once.
wenzelm@46259
   634
wenzelm@46266
   635
  Note that for tactics with subgoal addressing, the combinator can be
wenzelm@46266
   636
  applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
wenzelm@46266
   637
  "tac"}.  There is no need for @{verbatim TRY'}.
wenzelm@46259
   638
wenzelm@46269
   639
  \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal
wenzelm@46259
   640
  state and, recursively, to each element of the resulting sequence.
wenzelm@46259
   641
  The resulting sequence consists of those states that make @{text
wenzelm@46259
   642
  "tac"} fail.  Thus, it applies @{text "tac"} as many times as
wenzelm@46259
   643
  possible (including zero times), and allows backtracking over each
wenzelm@46259
   644
  invocation of @{text "tac"}.  @{ML REPEAT} is more general than @{ML
wenzelm@46259
   645
  REPEAT_DETERM}, but requires more space.
wenzelm@46259
   646
wenzelm@46259
   647
  \item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}
wenzelm@46259
   648
  but it always applies @{text "tac"} at least once, failing if this
wenzelm@46259
   649
  is impossible.
wenzelm@46259
   650
wenzelm@46266
   651
  \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
wenzelm@46269
   652
  goal state and, recursively, to the head of the resulting sequence.
wenzelm@46266
   653
  It returns the first state to make @{text "tac"} fail.  It is
wenzelm@46266
   654
  deterministic, discarding alternative outcomes.
wenzelm@46266
   655
wenzelm@46266
   656
  \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
wenzelm@46266
   657
  REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
wenzelm@46266
   658
  by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
wenzelm@46259
   659
wenzelm@46259
   660
  \end{description}
wenzelm@58618
   661
\<close>
wenzelm@46259
   662
wenzelm@58618
   663
text %mlex \<open>The basic tactics and tacticals considered above follow
wenzelm@46260
   664
  some algebraic laws:
wenzelm@46259
   665
wenzelm@46260
   666
  \begin{itemize}
wenzelm@46259
   667
wenzelm@46262
   668
  \item @{ML all_tac} is the identity element of the tactical @{ML_op
wenzelm@46262
   669
  "THEN"}.
wenzelm@46259
   670
wenzelm@46262
   671
  \item @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
wenzelm@46262
   672
  @{ML_op "APPEND"}.  Also, it is a zero element for @{ML_op "THEN"},
wenzelm@46262
   673
  which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
wenzelm@46262
   674
  equivalent to @{ML no_tac}.
wenzelm@46259
   675
wenzelm@46260
   676
  \item @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
wenzelm@46260
   677
  functions over more basic combinators (ignoring some internal
wenzelm@46260
   678
  implementation tricks):
wenzelm@46259
   679
wenzelm@46260
   680
  \end{itemize}
wenzelm@58618
   681
\<close>
wenzelm@46259
   682
wenzelm@58618
   683
ML \<open>
wenzelm@46259
   684
  fun TRY tac = tac ORELSE all_tac;
wenzelm@46259
   685
  fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;
wenzelm@58618
   686
\<close>
wenzelm@46259
   687
wenzelm@58618
   688
text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML
wenzelm@46262
   689
  REPEAT}~@{text "tac"}.  @{ML REPEAT} uses @{ML_op "ORELSE"} and not
wenzelm@46262
   690
  @{ML_op "APPEND"}, it applies @{text "tac"} as many times as
wenzelm@46259
   691
  possible in each outcome.
wenzelm@46259
   692
wenzelm@46259
   693
  \begin{warn}
wenzelm@46269
   694
  Note the explicit abstraction over the goal state in the ML
wenzelm@46260
   695
  definition of @{ML REPEAT}.  Recursive tacticals must be coded in
wenzelm@46260
   696
  this awkward fashion to avoid infinite recursion of eager functional
wenzelm@46260
   697
  evaluation in Standard ML.  The following attempt would make @{ML
wenzelm@46260
   698
  REPEAT}~@{text "tac"} loop:
wenzelm@46259
   699
  \end{warn}
wenzelm@58618
   700
\<close>
wenzelm@46259
   701
wenzelm@58618
   702
ML \<open>
wenzelm@46260
   703
  (*BAD -- does not terminate!*)
wenzelm@46260
   704
  fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
wenzelm@58618
   705
\<close>
wenzelm@46259
   706
wenzelm@46263
   707
wenzelm@58618
   708
subsection \<open>Applying tactics to subgoal ranges\<close>
wenzelm@46263
   709
wenzelm@58618
   710
text \<open>Tactics with explicit subgoal addressing
wenzelm@46263
   711
  @{ML_type "int -> tactic"} can be used together with tacticals that
wenzelm@46263
   712
  act like ``subgoal quantifiers'': guided by success of the body
wenzelm@46263
   713
  tactic a certain range of subgoals is covered.  Thus the body tactic
wenzelm@46267
   714
  is applied to \emph{all} subgoals, \emph{some} subgoal etc.
wenzelm@46263
   715
wenzelm@46263
   716
  Suppose that the goal state has @{text "n \<ge> 0"} subgoals.  Many of
wenzelm@46263
   717
  these tacticals address subgoal ranges counting downwards from
wenzelm@46263
   718
  @{text "n"} towards @{text "1"}.  This has the fortunate effect that
wenzelm@46263
   719
  newly emerging subgoals are concatenated in the result, without
wenzelm@46263
   720
  interfering each other.  Nonetheless, there might be situations
wenzelm@58618
   721
  where a different order is desired.\<close>
wenzelm@46263
   722
wenzelm@58618
   723
text %mlref \<open>
wenzelm@46263
   724
  \begin{mldecls}
wenzelm@46263
   725
  @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
wenzelm@46263
   726
  @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
wenzelm@46263
   727
  @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
wenzelm@46267
   728
  @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
wenzelm@46263
   729
  @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
wenzelm@46263
   730
  @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
wenzelm@46267
   731
  @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
wenzelm@46263
   732
  \end{mldecls}
wenzelm@46263
   733
wenzelm@46263
   734
  \begin{description}
wenzelm@46263
   735
wenzelm@46263
   736
  \item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
wenzelm@46263
   737
  n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}.  It
wenzelm@46263
   738
  applies the @{text tac} to all the subgoals, counting downwards.
wenzelm@46263
   739
wenzelm@46263
   740
  \item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac
wenzelm@46263
   741
  n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}.  It
wenzelm@46263
   742
  applies @{text "tac"} to one subgoal, counting downwards.
wenzelm@46263
   743
wenzelm@46263
   744
  \item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac
wenzelm@46263
   745
  1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}.  It
wenzelm@46263
   746
  applies @{text "tac"} to one subgoal, counting upwards.
wenzelm@46263
   747
wenzelm@46267
   748
  \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
wenzelm@46267
   749
  It applies @{text "tac"} unconditionally to the first subgoal.
wenzelm@46267
   750
wenzelm@46263
   751
  \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
wenzelm@46263
   752
  more to a subgoal, counting downwards.
wenzelm@46263
   753
wenzelm@46263
   754
  \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
wenzelm@46263
   755
  more to a subgoal, counting upwards.
wenzelm@46263
   756
wenzelm@46267
   757
  \item @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to
wenzelm@46267
   758
  @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
wenzelm@46267
   759
  THEN}~@{text "tac\<^sub>1 i"}.  It applies the given list of tactics to the
wenzelm@46267
   760
  corresponding range of subgoals, counting downwards.
wenzelm@46267
   761
wenzelm@46263
   762
  \end{description}
wenzelm@58618
   763
\<close>
wenzelm@46263
   764
wenzelm@46269
   765
wenzelm@58618
   766
subsection \<open>Control and search tacticals\<close>
wenzelm@46269
   767
wenzelm@58618
   768
text \<open>A predicate on theorems @{ML_type "thm -> bool"} can test
wenzelm@46269
   769
  whether a goal state enjoys some desirable property --- such as
wenzelm@46269
   770
  having no subgoals.  Tactics that search for satisfactory goal
wenzelm@46269
   771
  states are easy to express.  The main search procedures,
wenzelm@46269
   772
  depth-first, breadth-first and best-first, are provided as
wenzelm@46269
   773
  tacticals.  They generate the search tree by repeatedly applying a
wenzelm@58618
   774
  given tactic.\<close>
wenzelm@46269
   775
wenzelm@46269
   776
wenzelm@46270
   777
text %mlref ""
wenzelm@46270
   778
wenzelm@58618
   779
subsubsection \<open>Filtering a tactic's results\<close>
wenzelm@46269
   780
wenzelm@58618
   781
text \<open>
wenzelm@46269
   782
  \begin{mldecls}
wenzelm@46269
   783
  @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
wenzelm@46269
   784
  @{index_ML CHANGED: "tactic -> tactic"} \\
wenzelm@46269
   785
  \end{mldecls}
wenzelm@46269
   786
wenzelm@46269
   787
  \begin{description}
wenzelm@46269
   788
wenzelm@46269
   789
  \item @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
wenzelm@46269
   790
  goal state and returns a sequence consisting of those result goal
wenzelm@46269
   791
  states that are satisfactory in the sense of @{text "sat"}.
wenzelm@46269
   792
wenzelm@46269
   793
  \item @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal
wenzelm@46269
   794
  state and returns precisely those states that differ from the
wenzelm@46269
   795
  original state (according to @{ML Thm.eq_thm}).  Thus @{ML
wenzelm@46269
   796
  CHANGED}~@{text "tac"} always has some effect on the state.
wenzelm@46269
   797
wenzelm@46269
   798
  \end{description}
wenzelm@58618
   799
\<close>
wenzelm@46269
   800
wenzelm@46269
   801
wenzelm@58618
   802
subsubsection \<open>Depth-first search\<close>
wenzelm@46269
   803
wenzelm@58618
   804
text \<open>
wenzelm@46269
   805
  \begin{mldecls}
wenzelm@46269
   806
  @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
wenzelm@46269
   807
  @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\
wenzelm@46269
   808
  @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
wenzelm@46269
   809
  \end{mldecls}
wenzelm@46269
   810
wenzelm@46269
   811
  \begin{description}
wenzelm@46269
   812
wenzelm@46269
   813
  \item @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
wenzelm@46269
   814
  @{text "sat"} returns true.  Otherwise it applies @{text "tac"},
wenzelm@46269
   815
  then recursively searches from each element of the resulting
wenzelm@46269
   816
  sequence.  The code uses a stack for efficiency, in effect applying
wenzelm@46269
   817
  @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to
wenzelm@46269
   818
  the state.
wenzelm@46269
   819
wenzelm@46269
   820
  \item @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
wenzelm@46269
   821
  search for states having no subgoals.
wenzelm@46269
   822
wenzelm@46269
   823
  \item @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
wenzelm@46269
   824
  search for states having fewer subgoals than the given state.  Thus,
wenzelm@46269
   825
  it insists upon solving at least one subgoal.
wenzelm@46269
   826
wenzelm@46269
   827
  \end{description}
wenzelm@58618
   828
\<close>
wenzelm@46269
   829
wenzelm@46269
   830
wenzelm@58618
   831
subsubsection \<open>Other search strategies\<close>
wenzelm@46269
   832
wenzelm@58618
   833
text \<open>
wenzelm@46269
   834
  \begin{mldecls}
wenzelm@46269
   835
  @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
wenzelm@46269
   836
  @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
wenzelm@46269
   837
  @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
wenzelm@46269
   838
  \end{mldecls}
wenzelm@46269
   839
wenzelm@46269
   840
  These search strategies will find a solution if one exists.
wenzelm@46269
   841
  However, they do not enumerate all solutions; they terminate after
wenzelm@46269
   842
  the first satisfactory result from @{text "tac"}.
wenzelm@46269
   843
wenzelm@46269
   844
  \begin{description}
wenzelm@46269
   845
wenzelm@46269
   846
  \item @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
wenzelm@46269
   847
  search to find states for which @{text "sat"} is true.  For most
wenzelm@46269
   848
  applications, it is too slow.
wenzelm@46269
   849
wenzelm@46269
   850
  \item @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic
wenzelm@46269
   851
  search, using @{text "dist"} to estimate the distance from a
wenzelm@46269
   852
  satisfactory state (in the sense of @{text "sat"}).  It maintains a
wenzelm@46269
   853
  list of states ordered by distance.  It applies @{text "tac"} to the
wenzelm@46269
   854
  head of this list; if the result contains any satisfactory states,
wenzelm@46269
   855
  then it returns them.  Otherwise, @{ML BEST_FIRST} adds the new
wenzelm@46269
   856
  states to the list, and continues.
wenzelm@46269
   857
wenzelm@46269
   858
  The distance function is typically @{ML size_of_thm}, which computes
wenzelm@46269
   859
  the size of the state.  The smaller the state, the fewer and simpler
wenzelm@46269
   860
  subgoals it has.
wenzelm@46269
   861
wenzelm@46269
   862
  \item @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like
wenzelm@46269
   863
  @{ML BEST_FIRST}, except that the priority queue initially contains
wenzelm@46269
   864
  the result of applying @{text "tac\<^sub>0"} to the goal state.  This
wenzelm@46269
   865
  tactical permits separate tactics for starting the search and
wenzelm@46269
   866
  continuing the search.
wenzelm@46269
   867
wenzelm@46269
   868
  \end{description}
wenzelm@58618
   869
\<close>
wenzelm@46269
   870
wenzelm@46269
   871
wenzelm@58618
   872
subsubsection \<open>Auxiliary tacticals for searching\<close>
wenzelm@46269
   873
wenzelm@58618
   874
text \<open>
wenzelm@46269
   875
  \begin{mldecls}
wenzelm@46269
   876
  @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
wenzelm@46269
   877
  @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\
wenzelm@46269
   878
  @{index_ML SOLVE: "tactic -> tactic"} \\
wenzelm@46269
   879
  @{index_ML DETERM: "tactic -> tactic"} \\
wenzelm@46269
   880
  \end{mldecls}
wenzelm@46269
   881
wenzelm@46269
   882
  \begin{description}
wenzelm@46269
   883
wenzelm@46269
   884
  \item @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to
wenzelm@46269
   885
  the goal state if it satisfies predicate @{text "sat"}, and applies
wenzelm@46269
   886
  @{text "tac\<^sub>2"}.  It is a conditional tactical in that only one of
wenzelm@46269
   887
  @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.
wenzelm@46269
   888
  However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated
wenzelm@46269
   889
  because ML uses eager evaluation.
wenzelm@46269
   890
wenzelm@46269
   891
  \item @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the
wenzelm@46269
   892
  goal state if it has any subgoals, and simply returns the goal state
wenzelm@46269
   893
  otherwise.  Many common tactics, such as @{ML resolve_tac}, fail if
wenzelm@46269
   894
  applied to a goal state that has no subgoals.
wenzelm@46269
   895
wenzelm@46269
   896
  \item @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
wenzelm@46269
   897
  state and then fails iff there are subgoals left.
wenzelm@46269
   898
wenzelm@46269
   899
  \item @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
wenzelm@46269
   900
  state and returns the head of the resulting sequence.  @{ML DETERM}
wenzelm@46269
   901
  limits the search space by making its argument deterministic.
wenzelm@46269
   902
wenzelm@46269
   903
  \end{description}
wenzelm@58618
   904
\<close>
wenzelm@46269
   905
wenzelm@46269
   906
wenzelm@58618
   907
subsubsection \<open>Predicates and functions useful for searching\<close>
wenzelm@46269
   908
wenzelm@58618
   909
text \<open>
wenzelm@46269
   910
  \begin{mldecls}
wenzelm@46269
   911
  @{index_ML has_fewer_prems: "int -> thm -> bool"} \\
wenzelm@46269
   912
  @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\
wenzelm@46269
   913
  @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
wenzelm@46269
   914
  @{index_ML size_of_thm: "thm -> int"} \\
wenzelm@46269
   915
  \end{mldecls}
wenzelm@46269
   916
wenzelm@46269
   917
  \begin{description}
wenzelm@46269
   918
wenzelm@46269
   919
  \item @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
wenzelm@46269
   920
  "thm"} has fewer than @{text "n"} premises.
wenzelm@46269
   921
wenzelm@46269
   922
  \item @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
wenzelm@55547
   923
  "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.  Both theorems must have the
wenzelm@55547
   924
  same conclusions, the same set of hypotheses, and the same set of sort
wenzelm@46269
   925
  hypotheses.  Names of bound variables are ignored as usual.
wenzelm@46269
   926
wenzelm@46269
   927
  \item @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
wenzelm@46269
   928
  the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.
wenzelm@46269
   929
  Names of bound variables are ignored.
wenzelm@46269
   930
wenzelm@46269
   931
  \item @{ML size_of_thm}~@{text "thm"} computes the size of @{text
wenzelm@46269
   932
  "thm"}, namely the number of variables, constants and abstractions
wenzelm@46269
   933
  in its conclusion.  It may serve as a distance function for
wenzelm@46269
   934
  @{ML BEST_FIRST}.
wenzelm@46269
   935
wenzelm@46269
   936
  \end{description}
wenzelm@58618
   937
\<close>
wenzelm@46269
   938
wenzelm@18537
   939
end