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