author | wenzelm |
Sun, 29 Jan 2012 21:40:29 +0100 | |
changeset 46276 | 8f1f33faf24e |
parent 46274 | 67139209b548 |
child 46277 | aea65ff733b4 |
permissions | -rw-r--r-- |
30296 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Tactic}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Tactic\isanewline |
|
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupchapter{Tactical reasoning% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\begin{isamarkuptext}% |
|
35001 | 26 |
Tactical reasoning works by refining an initial claim in a |
30296 | 27 |
backwards fashion, until a solved form is reached. A \isa{goal} |
28 |
consists of several subgoals that need to be solved in order to |
|
29 |
achieve the main statement; zero subgoals means that the proof may |
|
30 |
be finished. A \isa{tactic} is a refinement operation that maps |
|
31 |
a goal to a lazy sequence of potential successors. A \isa{tactical} is a combinator for composing tactics.% |
|
32 |
\end{isamarkuptext}% |
|
33 |
\isamarkuptrue% |
|
34 |
% |
|
35 |
\isamarkupsection{Goals \label{sec:tactical-goals}% |
|
36 |
} |
|
37 |
\isamarkuptrue% |
|
38 |
% |
|
39 |
\begin{isamarkuptext}% |
|
40 |
Isabelle/Pure represents a goal as a theorem stating that the |
|
40406 | 41 |
subgoals imply the main goal: \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}. The outermost goal structure is that of a Horn Clause: i.e.\ |
30296 | 42 |
an iterated implication without any quantifiers\footnote{Recall that |
40406 | 43 |
outermost \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}} is always represented via schematic |
44 |
variables in the body: \isa{{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}}. These variables may get |
|
45 |
instantiated during the course of reasoning.}. For \isa{n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} |
|
30296 | 46 |
a goal is called ``solved''. |
47 |
||
40406 | 48 |
The structure of each subgoal \isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub i} is that of a |
49 |
general Hereditary Harrop Formula \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{2E}{\isachardot}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B}. Here \isa{x\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ x\isaliteral{5C3C5E7375623E}{}\isactrlsub k} are goal parameters, i.e.\ |
|
50 |
arbitrary-but-fixed entities of certain types, and \isa{H\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ H\isaliteral{5C3C5E7375623E}{}\isactrlsub m} are goal hypotheses, i.e.\ facts that may |
|
30296 | 51 |
be assumed locally. Together, this forms the goal context of the |
52 |
conclusion \isa{B} to be established. The goal hypotheses may be |
|
53 |
again arbitrary Hereditary Harrop Formulas, although the level of |
|
54 |
nesting rarely exceeds 1--2 in practice. |
|
55 |
||
56 |
The main conclusion \isa{C} is internally marked as a protected |
|
40406 | 57 |
proposition, which is represented explicitly by the notation \isa{{\isaliteral{23}{\isacharhash}}C} here. This ensures that the decomposition into subgoals and |
35001 | 58 |
main conclusion is well-defined for arbitrarily structured claims. |
30296 | 59 |
|
60 |
\medskip Basic goal management is performed via the following |
|
61 |
Isabelle/Pure rules: |
|
62 |
||
63 |
\[ |
|
40406 | 64 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}init{\isaliteral{29}{\isacharparenright}}}]{\isa{C\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}}{} \qquad |
65 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}finish{\isaliteral{29}{\isacharparenright}}}]{\isa{C}}{\isa{{\isaliteral{23}{\isacharhash}}C}} |
|
30296 | 66 |
\] |
67 |
||
68 |
\medskip The following low-level variants admit general reasoning |
|
69 |
with protected propositions: |
|
70 |
||
71 |
\[ |
|
40406 | 72 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}protect{\isaliteral{29}{\isacharparenright}}}]{\isa{{\isaliteral{23}{\isacharhash}}C}}{\isa{C}} \qquad |
73 |
\infer[\isa{{\isaliteral{28}{\isacharparenleft}}conclude{\isaliteral{29}{\isacharparenright}}}]{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C}}{\isa{A\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{23}{\isacharhash}}C}} |
|
30296 | 74 |
\]% |
75 |
\end{isamarkuptext}% |
|
76 |
\isamarkuptrue% |
|
77 |
% |
|
78 |
\isadelimmlref |
|
79 |
% |
|
80 |
\endisadelimmlref |
|
81 |
% |
|
82 |
\isatagmlref |
|
83 |
% |
|
84 |
\begin{isamarkuptext}% |
|
85 |
\begin{mldecls} |
|
86 |
\indexdef{}{ML}{Goal.init}\verb|Goal.init: cterm -> thm| \\ |
|
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30296
diff
changeset
|
87 |
\indexdef{}{ML}{Goal.finish}\verb|Goal.finish: Proof.context -> thm -> thm| \\ |
30296 | 88 |
\indexdef{}{ML}{Goal.protect}\verb|Goal.protect: thm -> thm| \\ |
89 |
\indexdef{}{ML}{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\ |
|
90 |
\end{mldecls} |
|
91 |
||
92 |
\begin{description} |
|
93 |
||
94 |
\item \verb|Goal.init|~\isa{C} initializes a tactical goal from |
|
95 |
the well-formed proposition \isa{C}. |
|
96 |
||
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30296
diff
changeset
|
97 |
\item \verb|Goal.finish|~\isa{ctxt\ thm} checks whether theorem |
30296 | 98 |
\isa{thm} is a solved goal (no subgoals), and concludes the |
32201
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30296
diff
changeset
|
99 |
result by removing the goal protection. The context is only |
3689b647356d
updated Variable.focus, SUBPROOF, Obtain.result, Goal.finish;
wenzelm
parents:
30296
diff
changeset
|
100 |
required for printing error messages. |
30296 | 101 |
|
102 |
\item \verb|Goal.protect|~\isa{thm} protects the full statement |
|
103 |
of theorem \isa{thm}. |
|
104 |
||
105 |
\item \verb|Goal.conclude|~\isa{thm} removes the goal |
|
106 |
protection, even if there are pending subgoals. |
|
107 |
||
108 |
\end{description}% |
|
109 |
\end{isamarkuptext}% |
|
110 |
\isamarkuptrue% |
|
111 |
% |
|
112 |
\endisatagmlref |
|
113 |
{\isafoldmlref}% |
|
114 |
% |
|
115 |
\isadelimmlref |
|
116 |
% |
|
117 |
\endisadelimmlref |
|
118 |
% |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
119 |
\isamarkupsection{Tactics\label{sec:tactics}% |
30296 | 120 |
} |
121 |
\isamarkuptrue% |
|
122 |
% |
|
123 |
\begin{isamarkuptext}% |
|
40406 | 124 |
A \isa{tactic} is a function \isa{goal\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ goal\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}} that |
30296 | 125 |
maps a given goal state (represented as a theorem, cf.\ |
126 |
\secref{sec:tactical-goals}) to a lazy sequence of potential |
|
127 |
successor states. The underlying sequence implementation is lazy |
|
128 |
both in head and tail, and is purely functional in \emph{not} |
|
129 |
supporting memoing.\footnote{The lack of memoing and the strict |
|
130 |
nature of SML requires some care when working with low-level |
|
131 |
sequence operations, to avoid duplicate or premature evaluation of |
|
35001 | 132 |
results. It also means that modified runtime behavior, such as |
133 |
timeout, is very hard to achieve for general tactics.} |
|
30296 | 134 |
|
135 |
An \emph{empty result sequence} means that the tactic has failed: in |
|
35001 | 136 |
a compound tactic expression other tactics might be tried instead, |
30296 | 137 |
or the whole refinement step might fail outright, producing a |
35001 | 138 |
toplevel error message in the end. When implementing tactics from |
139 |
scratch, one should take care to observe the basic protocol of |
|
140 |
mapping regular error conditions to an empty result; only serious |
|
141 |
faults should emerge as exceptions. |
|
30296 | 142 |
|
143 |
By enumerating \emph{multiple results}, a tactic can easily express |
|
144 |
the potential outcome of an internal search process. There are also |
|
145 |
combinators for building proof tools that involve search |
|
146 |
systematically, see also \secref{sec:tacticals}. |
|
147 |
||
35001 | 148 |
\medskip As explained before, a goal state essentially consists of a |
149 |
list of subgoals that imply the main goal (conclusion). Tactics may |
|
150 |
operate on all subgoals or on a particularly specified subgoal, but |
|
151 |
must not change the main conclusion (apart from instantiating |
|
152 |
schematic goal variables). |
|
30296 | 153 |
|
154 |
Tactics with explicit \emph{subgoal addressing} are of the form |
|
40406 | 155 |
\isa{int\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ tactic} and may be applied to a particular subgoal |
30296 | 156 |
(counting from 1). If the subgoal number is out of range, the |
157 |
tactic should fail with an empty result sequence, but must not raise |
|
158 |
an exception! |
|
159 |
||
160 |
Operating on a particular subgoal means to replace it by an interval |
|
161 |
of zero or more subgoals in the same place; other subgoals must not |
|
162 |
be affected, apart from instantiating schematic variables ranging |
|
163 |
over the whole goal state. |
|
164 |
||
165 |
A common pattern of composing tactics with subgoal addressing is to |
|
166 |
try the first one, and then the second one only if the subgoal has |
|
167 |
not been solved yet. Special care is required here to avoid bumping |
|
168 |
into unrelated subgoals that happen to come after the original |
|
169 |
subgoal. Assuming that there is only a single initial subgoal is a |
|
170 |
very common error when implementing tactics! |
|
171 |
||
172 |
Tactics with internal subgoal addressing should expose the subgoal |
|
173 |
index as \isa{int} argument in full generality; a hardwired |
|
35001 | 174 |
subgoal 1 is not acceptable. |
30296 | 175 |
|
176 |
\medskip The main well-formedness conditions for proper tactics are |
|
177 |
summarized as follows. |
|
178 |
||
179 |
\begin{itemize} |
|
180 |
||
181 |
\item General tactic failure is indicated by an empty result, only |
|
182 |
serious faults may produce an exception. |
|
183 |
||
184 |
\item The main conclusion must not be changed, apart from |
|
185 |
instantiating schematic variables. |
|
186 |
||
187 |
\item A tactic operates either uniformly on all subgoals, or |
|
188 |
specifically on a selected subgoal (without bumping into unrelated |
|
189 |
subgoals). |
|
190 |
||
191 |
\item Range errors in subgoal addressing produce an empty result. |
|
192 |
||
193 |
\end{itemize} |
|
194 |
||
195 |
Some of these conditions are checked by higher-level goal |
|
35001 | 196 |
infrastructure (\secref{sec:struct-goals}); others are not checked |
30296 | 197 |
explicitly, and violating them merely results in ill-behaved tactics |
198 |
experienced by the user (e.g.\ tactics that insist in being |
|
35001 | 199 |
applicable only to singleton goals, or prevent composition via |
46260 | 200 |
standard tacticals such as \verb|REPEAT|).% |
30296 | 201 |
\end{isamarkuptext}% |
202 |
\isamarkuptrue% |
|
203 |
% |
|
204 |
\isadelimmlref |
|
205 |
% |
|
206 |
\endisadelimmlref |
|
207 |
% |
|
208 |
\isatagmlref |
|
209 |
% |
|
210 |
\begin{isamarkuptext}% |
|
211 |
\begin{mldecls} |
|
212 |
\indexdef{}{ML type}{tactic}\verb|type tactic = thm -> thm Seq.seq| \\ |
|
213 |
\indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\ |
|
214 |
\indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\ |
|
215 |
\indexdef{}{ML}{print\_tac}\verb|print_tac: string -> tactic| \\[1ex] |
|
216 |
\indexdef{}{ML}{PRIMITIVE}\verb|PRIMITIVE: (thm -> thm) -> tactic| \\[1ex] |
|
217 |
\indexdef{}{ML}{SUBGOAL}\verb|SUBGOAL: (term * int -> tactic) -> int -> tactic| \\ |
|
218 |
\indexdef{}{ML}{CSUBGOAL}\verb|CSUBGOAL: (cterm * int -> tactic) -> int -> tactic| \\ |
|
219 |
\end{mldecls} |
|
220 |
||
221 |
\begin{description} |
|
222 |
||
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
223 |
\item Type \verb|tactic| represents tactics. The |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
224 |
well-formedness conditions described above need to be observed. See |
40802 | 225 |
also \verb|~~/src/Pure/General/seq.ML| for the underlying |
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
226 |
implementation of lazy sequences. |
30296 | 227 |
|
39885
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
228 |
\item Type \verb|int -> tactic| represents tactics with |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
229 |
explicit subgoal addressing, with well-formedness conditions as |
6a3f7941c3a0
cumulative update of generated files (since bf164c153d10);
wenzelm
parents:
35001
diff
changeset
|
230 |
described above. |
30296 | 231 |
|
232 |
\item \verb|no_tac| is a tactic that always fails, returning the |
|
233 |
empty sequence. |
|
234 |
||
235 |
\item \verb|all_tac| is a tactic that always succeeds, returning a |
|
236 |
singleton sequence with unchanged goal state. |
|
237 |
||
238 |
\item \verb|print_tac|~\isa{message} is like \verb|all_tac|, but |
|
239 |
prints a message together with the goal state on the tracing |
|
240 |
channel. |
|
241 |
||
242 |
\item \verb|PRIMITIVE|~\isa{rule} turns a primitive inference rule |
|
243 |
into a tactic with unique result. Exception \verb|THM| is considered |
|
244 |
a regular tactic failure and produces an empty result; other |
|
245 |
exceptions are passed through. |
|
246 |
||
40406 | 247 |
\item \verb|SUBGOAL|~\isa{{\isaliteral{28}{\isacharparenleft}}fn\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{2C}{\isacharcomma}}\ i{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ tactic{\isaliteral{29}{\isacharparenright}}} is the |
30296 | 248 |
most basic form to produce a tactic with subgoal addressing. The |
249 |
given abstraction over the subgoal term and subgoal number allows to |
|
250 |
peek at the relevant information of the full goal state. The |
|
251 |
subgoal range is checked as required above. |
|
252 |
||
253 |
\item \verb|CSUBGOAL| is similar to \verb|SUBGOAL|, but passes the |
|
254 |
subgoal as \verb|cterm| instead of raw \verb|term|. This |
|
255 |
avoids expensive re-certification in situations where the subgoal is |
|
256 |
used directly for primitive inferences. |
|
257 |
||
258 |
\end{description}% |
|
259 |
\end{isamarkuptext}% |
|
260 |
\isamarkuptrue% |
|
261 |
% |
|
262 |
\endisatagmlref |
|
263 |
{\isafoldmlref}% |
|
264 |
% |
|
265 |
\isadelimmlref |
|
266 |
% |
|
267 |
\endisadelimmlref |
|
268 |
% |
|
269 |
\isamarkupsubsection{Resolution and assumption tactics \label{sec:resolve-assume-tac}% |
|
270 |
} |
|
271 |
\isamarkuptrue% |
|
272 |
% |
|
273 |
\begin{isamarkuptext}% |
|
274 |
\emph{Resolution} is the most basic mechanism for refining a |
|
275 |
subgoal using a theorem as object-level rule. |
|
276 |
\emph{Elim-resolution} is particularly suited for elimination rules: |
|
277 |
it resolves with a rule, proves its first premise by assumption, and |
|
278 |
finally deletes that assumption from any new subgoals. |
|
279 |
\emph{Destruct-resolution} is like elim-resolution, but the given |
|
280 |
destruction rules are first turned into canonical elimination |
|
281 |
format. \emph{Forward-resolution} is like destruct-resolution, but |
|
40406 | 282 |
without deleting the selected assumption. The \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} |
30296 | 283 |
naming convention is maintained for several different kinds of |
284 |
resolution rules and tactics. |
|
285 |
||
286 |
Assumption tactics close a subgoal by unifying some of its premises |
|
287 |
against its conclusion. |
|
288 |
||
289 |
\medskip All the tactics in this section operate on a subgoal |
|
290 |
designated by a positive integer. Other subgoals might be affected |
|
291 |
indirectly, due to instantiation of schematic variables. |
|
292 |
||
293 |
There are various sources of non-determinism, the tactic result |
|
294 |
sequence enumerates all possibilities of the following choices (if |
|
295 |
applicable): |
|
296 |
||
297 |
\begin{enumerate} |
|
298 |
||
299 |
\item selecting one of the rules given as argument to the tactic; |
|
300 |
||
301 |
\item selecting a subgoal premise to eliminate, unifying it against |
|
302 |
the first premise of the rule; |
|
303 |
||
304 |
\item unifying the conclusion of the subgoal to the conclusion of |
|
305 |
the rule. |
|
306 |
||
307 |
\end{enumerate} |
|
308 |
||
309 |
Recall that higher-order unification may produce multiple results |
|
310 |
that are enumerated here.% |
|
311 |
\end{isamarkuptext}% |
|
312 |
\isamarkuptrue% |
|
313 |
% |
|
314 |
\isadelimmlref |
|
315 |
% |
|
316 |
\endisadelimmlref |
|
317 |
% |
|
318 |
\isatagmlref |
|
319 |
% |
|
320 |
\begin{isamarkuptext}% |
|
321 |
\begin{mldecls} |
|
322 |
\indexdef{}{ML}{resolve\_tac}\verb|resolve_tac: thm list -> int -> tactic| \\ |
|
323 |
\indexdef{}{ML}{eresolve\_tac}\verb|eresolve_tac: thm list -> int -> tactic| \\ |
|
324 |
\indexdef{}{ML}{dresolve\_tac}\verb|dresolve_tac: thm list -> int -> tactic| \\ |
|
325 |
\indexdef{}{ML}{forward\_tac}\verb|forward_tac: thm list -> int -> tactic| \\[1ex] |
|
326 |
\indexdef{}{ML}{assume\_tac}\verb|assume_tac: int -> tactic| \\ |
|
327 |
\indexdef{}{ML}{eq\_assume\_tac}\verb|eq_assume_tac: int -> tactic| \\[1ex] |
|
328 |
\indexdef{}{ML}{match\_tac}\verb|match_tac: thm list -> int -> tactic| \\ |
|
329 |
\indexdef{}{ML}{ematch\_tac}\verb|ematch_tac: thm list -> int -> tactic| \\ |
|
330 |
\indexdef{}{ML}{dmatch\_tac}\verb|dmatch_tac: thm list -> int -> tactic| \\ |
|
331 |
\end{mldecls} |
|
332 |
||
333 |
\begin{description} |
|
334 |
||
335 |
\item \verb|resolve_tac|~\isa{thms\ i} refines the goal state |
|
336 |
using the given theorems, which should normally be introduction |
|
337 |
rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's |
|
338 |
premises. |
|
339 |
||
340 |
\item \verb|eresolve_tac|~\isa{thms\ i} performs elim-resolution |
|
341 |
with the given theorems, which should normally be elimination rules. |
|
342 |
||
343 |
\item \verb|dresolve_tac|~\isa{thms\ i} performs |
|
344 |
destruct-resolution with the given theorems, which should normally |
|
345 |
be destruction rules. This replaces an assumption by the result of |
|
346 |
applying one of the rules. |
|
347 |
||
348 |
\item \verb|forward_tac| is like \verb|dresolve_tac| except that the |
|
349 |
selected assumption is not deleted. It applies a rule to an |
|
350 |
assumption, adding the result as a new assumption. |
|
351 |
||
352 |
\item \verb|assume_tac|~\isa{i} attempts to solve subgoal \isa{i} |
|
353 |
by assumption (modulo higher-order unification). |
|
354 |
||
355 |
\item \verb|eq_assume_tac| is similar to \verb|assume_tac|, but checks |
|
40406 | 356 |
only for immediate \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}}-convertibility instead of using |
30296 | 357 |
unification. It succeeds (with a unique next state) if one of the |
358 |
assumptions is equal to the subgoal's conclusion. Since it does not |
|
359 |
instantiate variables, it cannot make other subgoals unprovable. |
|
360 |
||
361 |
\item \verb|match_tac|, \verb|ematch_tac|, and \verb|dmatch_tac| are |
|
362 |
similar to \verb|resolve_tac|, \verb|eresolve_tac|, and \verb|dresolve_tac|, respectively, but do not instantiate schematic |
|
363 |
variables in the goal state. |
|
364 |
||
365 |
Flexible subgoals are not updated at will, but are left alone. |
|
366 |
Strictly speaking, matching means to treat the unknowns in the goal |
|
367 |
state as constants; these tactics merely discard unifiers that would |
|
368 |
update the goal state. |
|
369 |
||
370 |
\end{description}% |
|
371 |
\end{isamarkuptext}% |
|
372 |
\isamarkuptrue% |
|
373 |
% |
|
374 |
\endisatagmlref |
|
375 |
{\isafoldmlref}% |
|
376 |
% |
|
377 |
\isadelimmlref |
|
378 |
% |
|
379 |
\endisadelimmlref |
|
380 |
% |
|
381 |
\isamarkupsubsection{Explicit instantiation within a subgoal context% |
|
382 |
} |
|
383 |
\isamarkuptrue% |
|
384 |
% |
|
385 |
\begin{isamarkuptext}% |
|
386 |
The main resolution tactics (\secref{sec:resolve-assume-tac}) |
|
387 |
use higher-order unification, which works well in many practical |
|
388 |
situations despite its daunting theoretical properties. |
|
389 |
Nonetheless, there are important problem classes where unguided |
|
390 |
higher-order unification is not so useful. This typically involves |
|
391 |
rules like universal elimination, existential introduction, or |
|
392 |
equational substitution. Here the unification problem involves |
|
40406 | 393 |
fully flexible \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x} schemes, which are hard to manage |
30296 | 394 |
without further hints. |
395 |
||
40406 | 396 |
By providing a (small) rigid term for \isa{{\isaliteral{3F}{\isacharquery}}x} explicitly, the |
397 |
remaining unification problem is to assign a (large) term to \isa{{\isaliteral{3F}{\isacharquery}}P}, according to the shape of the given subgoal. This is |
|
30296 | 398 |
sufficiently well-behaved in most practical situations. |
399 |
||
40406 | 400 |
\medskip Isabelle provides separate versions of the standard \isa{r{\isaliteral{2F}{\isacharslash}}e{\isaliteral{2F}{\isacharslash}}d{\isaliteral{2F}{\isacharslash}}f} resolution tactics that allow to provide explicit |
30296 | 401 |
instantiations of unknowns of the given rule, wrt.\ terms that refer |
402 |
to the implicit context of the selected subgoal. |
|
403 |
||
40406 | 404 |
An instantiation consists of a list of pairs of the form \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}, where \isa{{\isaliteral{3F}{\isacharquery}}x} is a schematic variable occurring in |
30296 | 405 |
the given rule, and \isa{t} is a term from the current proof |
406 |
context, augmented by the local goal parameters of the selected |
|
407 |
subgoal; cf.\ the \isa{focus} operation described in |
|
408 |
\secref{sec:variables}. |
|
409 |
||
410 |
Entering the syntactic context of a subgoal is a brittle operation, |
|
411 |
because its exact form is somewhat accidental, and the choice of |
|
412 |
bound variable names depends on the presence of other local and |
|
413 |
global names. Explicit renaming of subgoal parameters prior to |
|
414 |
explicit instantiation might help to achieve a bit more robustness. |
|
415 |
||
40406 | 416 |
Type instantiations may be given as well, via pairs like \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}. Type instantiations are distinguished from term |
30296 | 417 |
instantiations by the syntactic form of the schematic variable. |
418 |
Types are instantiated before terms are. Since term instantiation |
|
35001 | 419 |
already performs simple type-inference, so explicit type |
30296 | 420 |
instantiations are seldom necessary.% |
421 |
\end{isamarkuptext}% |
|
422 |
\isamarkuptrue% |
|
423 |
% |
|
424 |
\isadelimmlref |
|
425 |
% |
|
426 |
\endisadelimmlref |
|
427 |
% |
|
428 |
\isatagmlref |
|
429 |
% |
|
430 |
\begin{isamarkuptext}% |
|
431 |
\begin{mldecls} |
|
432 |
\indexdef{}{ML}{res\_inst\_tac}\verb|res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
433 |
\indexdef{}{ML}{eres\_inst\_tac}\verb|eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
434 |
\indexdef{}{ML}{dres\_inst\_tac}\verb|dres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
|
46271 | 435 |
\indexdef{}{ML}{forw\_inst\_tac}\verb|forw_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic| \\ |
436 |
\indexdef{}{ML}{subgoal\_tac}\verb|subgoal_tac: Proof.context -> string -> int -> tactic| \\ |
|
30296 | 437 |
\indexdef{}{ML}{rename\_tac}\verb|rename_tac: string list -> int -> tactic| \\ |
438 |
\end{mldecls} |
|
439 |
||
440 |
\begin{description} |
|
441 |
||
442 |
\item \verb|res_inst_tac|~\isa{ctxt\ insts\ thm\ i} instantiates the |
|
443 |
rule \isa{thm} with the instantiations \isa{insts}, as described |
|
444 |
above, and then performs resolution on subgoal \isa{i}. |
|
445 |
||
446 |
\item \verb|eres_inst_tac| is like \verb|res_inst_tac|, but performs |
|
447 |
elim-resolution. |
|
448 |
||
449 |
\item \verb|dres_inst_tac| is like \verb|res_inst_tac|, but performs |
|
450 |
destruct-resolution. |
|
451 |
||
452 |
\item \verb|forw_inst_tac| is like \verb|dres_inst_tac| except that |
|
453 |
the selected assumption is not deleted. |
|
454 |
||
46271 | 455 |
\item \verb|subgoal_tac|~\isa{ctxt\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ i} adds the proposition |
456 |
\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} as local premise to subgoal \isa{i}, and poses the |
|
457 |
same as a new subgoal \isa{i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}} (in the original context). |
|
458 |
||
30296 | 459 |
\item \verb|rename_tac|~\isa{names\ i} renames the innermost |
460 |
parameters of subgoal \isa{i} according to the provided \isa{names} (which need to be distinct indentifiers). |
|
461 |
||
35001 | 462 |
\end{description} |
463 |
||
464 |
For historical reasons, the above instantiation tactics take |
|
465 |
unparsed string arguments, which makes them hard to use in general |
|
466 |
ML code. The slightly more advanced \verb|Subgoal.FOCUS| combinator |
|
467 |
of \secref{sec:struct-goals} allows to refer to internal goal |
|
468 |
structure with explicit context management.% |
|
30296 | 469 |
\end{isamarkuptext}% |
470 |
\isamarkuptrue% |
|
471 |
% |
|
472 |
\endisatagmlref |
|
473 |
{\isafoldmlref}% |
|
474 |
% |
|
475 |
\isadelimmlref |
|
476 |
% |
|
477 |
\endisadelimmlref |
|
478 |
% |
|
46274 | 479 |
\isamarkupsubsection{Rearranging goal states% |
480 |
} |
|
481 |
\isamarkuptrue% |
|
482 |
% |
|
483 |
\begin{isamarkuptext}% |
|
484 |
In rare situations there is a need to rearrange goal states: |
|
485 |
either the overall collection of subgoals, or the local structure of |
|
486 |
a subgoal. Various administrative tactics allow to operate on the |
|
487 |
concrete presentation these conceptual sets of formulae.% |
|
488 |
\end{isamarkuptext}% |
|
489 |
\isamarkuptrue% |
|
490 |
% |
|
491 |
\isadelimmlref |
|
492 |
% |
|
493 |
\endisadelimmlref |
|
494 |
% |
|
495 |
\isatagmlref |
|
496 |
% |
|
497 |
\begin{isamarkuptext}% |
|
498 |
\begin{mldecls} |
|
499 |
\indexdef{}{ML}{rotate\_tac}\verb|rotate_tac: int -> int -> tactic| \\ |
|
46276 | 500 |
\indexdef{}{ML}{distinct\_subgoals\_tac}\verb|distinct_subgoals_tac: tactic| \\ |
501 |
\indexdef{}{ML}{flexflex\_tac}\verb|flexflex_tac: tactic| \\ |
|
46274 | 502 |
\end{mldecls} |
503 |
||
504 |
\begin{description} |
|
505 |
||
506 |
\item \verb|rotate_tac|~\isa{n\ i} rotates the premises of subgoal |
|
507 |
\isa{i} by \isa{n} positions: from right to left if \isa{n} is |
|
508 |
positive, and from left to right if \isa{n} is negative. |
|
509 |
||
46276 | 510 |
\item \verb|distinct_subgoals_tac| removes duplicate subgoals from a |
511 |
proof state. This is potentially inefficient. |
|
512 |
||
513 |
\item \verb|flexflex_tac| removes all flex-flex pairs from the proof |
|
514 |
state by applying the trivial unifier. This drastic step loses |
|
515 |
information. It is already part of the Isar infrastructure for |
|
516 |
facts resulting from goals, and rarely needs to be invoked manually. |
|
517 |
||
518 |
Flex-flex constraints arise from difficult cases of higher-order |
|
519 |
unification. To prevent this, use \verb|res_inst_tac| to instantiate |
|
520 |
some variables in a rule. Normally flex-flex constraints can be |
|
521 |
ignored; they often disappear as unknowns get instantiated. |
|
522 |
||
46274 | 523 |
\end{description}% |
524 |
\end{isamarkuptext}% |
|
525 |
\isamarkuptrue% |
|
526 |
% |
|
527 |
\endisatagmlref |
|
528 |
{\isafoldmlref}% |
|
529 |
% |
|
530 |
\isadelimmlref |
|
531 |
% |
|
532 |
\endisadelimmlref |
|
533 |
% |
|
30296 | 534 |
\isamarkupsection{Tacticals \label{sec:tacticals}% |
535 |
} |
|
536 |
\isamarkuptrue% |
|
537 |
% |
|
538 |
\begin{isamarkuptext}% |
|
46258 | 539 |
A \emph{tactical} is a functional combinator for building up |
540 |
complex tactics from simpler ones. Common tacticals perform |
|
541 |
sequential composition, disjunctive choice, iteration, or goal |
|
542 |
addressing. Various search strategies may be expressed via |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
543 |
tacticals.% |
46258 | 544 |
\end{isamarkuptext}% |
545 |
\isamarkuptrue% |
|
546 |
% |
|
547 |
\isamarkupsubsection{Combining tactics% |
|
548 |
} |
|
549 |
\isamarkuptrue% |
|
550 |
% |
|
551 |
\begin{isamarkuptext}% |
|
552 |
Sequential composition and alternative choices are the most |
|
553 |
basic ways to combine tactics, similarly to ``\verb|,|'' and |
|
554 |
``\verb||\verb,|,\verb||'' in Isar method notation. This corresponds to |
|
46262 | 555 |
\verb|THEN| and \verb|ORELSE| in ML, but there are further |
556 |
possibilities for fine-tuning alternation of tactics such as \verb|APPEND|. Further details become visible in ML due to explicit |
|
46258 | 557 |
subgoal addressing.% |
30296 | 558 |
\end{isamarkuptext}% |
559 |
\isamarkuptrue% |
|
560 |
% |
|
46258 | 561 |
\isadelimmlref |
562 |
% |
|
563 |
\endisadelimmlref |
|
564 |
% |
|
565 |
\isatagmlref |
|
566 |
% |
|
567 |
\begin{isamarkuptext}% |
|
568 |
\begin{mldecls} |
|
46262 | 569 |
\indexdef{}{ML infix}{THEN}\verb|infix THEN: tactic * tactic -> tactic| \\ |
570 |
\indexdef{}{ML infix}{ORELSE}\verb|infix ORELSE: tactic * tactic -> tactic| \\ |
|
571 |
\indexdef{}{ML infix}{APPEND}\verb|infix APPEND: tactic * tactic -> tactic| \\ |
|
46258 | 572 |
\indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\ |
573 |
\indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex] |
|
574 |
||
46262 | 575 |
\indexdef{}{ML infix}{THEN'}\verb|infix THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ |
576 |
\indexdef{}{ML infix}{ORELSE'}\verb|infix ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ |
|
577 |
\indexdef{}{ML infix}{APPEND'}\verb|infix APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ |
|
46258 | 578 |
\indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\ |
579 |
\indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\ |
|
580 |
\end{mldecls} |
|
581 |
||
582 |
\begin{description} |
|
583 |
||
46262 | 584 |
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
585 |
composition of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
586 |
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
|
587 |
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{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
|
588 |
states; then, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
589 |
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
|
590 |
states. |
46258 | 591 |
|
46262 | 592 |
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice |
593 |
between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it |
|
594 |
tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic |
|
595 |
choice: if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded |
|
596 |
from the result. |
|
46258 | 597 |
|
46262 | 598 |
\item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|APPEND|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the |
599 |
possible results of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike |
|
600 |
\verb|ORELSE| there is \emph{no commitment} to either tactic, so |
|
601 |
\verb|APPEND| helps to avoid incompleteness during search, at |
|
602 |
the cost of potential inefficiencies. |
|
46258 | 603 |
|
46262 | 604 |
\item \verb|EVERY|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. |
605 |
Note that \verb|EVERY []| is the same as \verb|all_tac|: it always |
|
606 |
succeeds. |
|
46258 | 607 |
|
46262 | 608 |
\item \verb|FIRST|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \verb|FIRST []| is the same as \verb|no_tac|: it |
609 |
always fails. |
|
46258 | 610 |
|
46264 | 611 |
\item \verb|THEN'| is the lifted version of \verb|THEN|, for |
46266 | 612 |
tactics with explicit subgoal addressing. So \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}. |
46258 | 613 |
|
46264 | 614 |
The other primed tacticals work analogously. |
46258 | 615 |
|
616 |
\end{description}% |
|
617 |
\end{isamarkuptext}% |
|
618 |
\isamarkuptrue% |
|
619 |
% |
|
620 |
\endisatagmlref |
|
621 |
{\isafoldmlref}% |
|
622 |
% |
|
623 |
\isadelimmlref |
|
624 |
% |
|
625 |
\endisadelimmlref |
|
626 |
% |
|
46259 | 627 |
\isamarkupsubsection{Repetition tacticals% |
628 |
} |
|
629 |
\isamarkuptrue% |
|
630 |
% |
|
631 |
\begin{isamarkuptext}% |
|
632 |
These tacticals provide further control over repetition of |
|
633 |
tactics, beyond the stylized forms of ``\verb|?|'' and |
|
634 |
``\verb|+|'' in Isar method expressions.% |
|
635 |
\end{isamarkuptext}% |
|
636 |
\isamarkuptrue% |
|
637 |
% |
|
638 |
\isadelimmlref |
|
639 |
% |
|
640 |
\endisadelimmlref |
|
641 |
% |
|
642 |
\isatagmlref |
|
643 |
% |
|
644 |
\begin{isamarkuptext}% |
|
645 |
\begin{mldecls} |
|
646 |
\indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\ |
|
46266 | 647 |
\indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\ |
648 |
\indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\ |
|
46259 | 649 |
\indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\ |
650 |
\indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\ |
|
651 |
\end{mldecls} |
|
652 |
||
653 |
\begin{description} |
|
654 |
||
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
655 |
\item \verb|TRY|~\isa{tac} applies \isa{tac} to the goal |
46259 | 656 |
state and returns the resulting sequence, if non-empty; otherwise it |
657 |
returns the original state. Thus, it applies \isa{tac} at most |
|
658 |
once. |
|
659 |
||
46266 | 660 |
Note that for tactics with subgoal addressing, the combinator can be |
661 |
applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}. There is no need for \verb|TRY'|. |
|
46259 | 662 |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
663 |
\item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the goal |
46259 | 664 |
state and, recursively, to each element of the resulting sequence. |
665 |
The resulting sequence consists of those states that make \isa{tac} fail. Thus, it applies \isa{tac} as many times as |
|
666 |
possible (including zero times), and allows backtracking over each |
|
667 |
invocation of \isa{tac}. \verb|REPEAT| is more general than \verb|REPEAT_DETERM|, but requires more space. |
|
668 |
||
669 |
\item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac} |
|
670 |
but it always applies \isa{tac} at least once, failing if this |
|
671 |
is impossible. |
|
672 |
||
46266 | 673 |
\item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
674 |
goal state and, recursively, to the head of the resulting sequence. |
46266 | 675 |
It returns the first state to make \isa{tac} fail. It is |
676 |
deterministic, discarding alternative outcomes. |
|
677 |
||
678 |
\item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound |
|
679 |
by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}). |
|
46259 | 680 |
|
681 |
\end{description}% |
|
682 |
\end{isamarkuptext}% |
|
683 |
\isamarkuptrue% |
|
684 |
% |
|
685 |
\endisatagmlref |
|
686 |
{\isafoldmlref}% |
|
687 |
% |
|
688 |
\isadelimmlref |
|
689 |
% |
|
690 |
\endisadelimmlref |
|
691 |
% |
|
692 |
\isadelimmlex |
|
693 |
% |
|
694 |
\endisadelimmlex |
|
695 |
% |
|
696 |
\isatagmlex |
|
697 |
% |
|
698 |
\begin{isamarkuptext}% |
|
46260 | 699 |
The basic tactics and tacticals considered above follow |
700 |
some algebraic laws: |
|
701 |
||
702 |
\begin{itemize} |
|
703 |
||
46262 | 704 |
\item \verb|all_tac| is the identity element of the tactical \verb|THEN|. |
46260 | 705 |
|
46262 | 706 |
\item \verb|no_tac| is the identity element of \verb|ORELSE| and |
707 |
\verb|APPEND|. Also, it is a zero element for \verb|THEN|, |
|
708 |
which means that \isa{tac}~\verb|THEN|~\verb|no_tac| is |
|
709 |
equivalent to \verb|no_tac|. |
|
46260 | 710 |
|
711 |
\item \verb|TRY| and \verb|REPEAT| can be expressed as (recursive) |
|
712 |
functions over more basic combinators (ignoring some internal |
|
713 |
implementation tricks): |
|
714 |
||
715 |
\end{itemize}% |
|
46259 | 716 |
\end{isamarkuptext}% |
717 |
\isamarkuptrue% |
|
718 |
% |
|
719 |
\endisatagmlex |
|
720 |
{\isafoldmlex}% |
|
721 |
% |
|
722 |
\isadelimmlex |
|
723 |
% |
|
724 |
\endisadelimmlex |
|
725 |
% |
|
726 |
\isadelimML |
|
727 |
% |
|
728 |
\endisadelimML |
|
729 |
% |
|
730 |
\isatagML |
|
731 |
\isacommand{ML}\isamarkupfalse% |
|
732 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
733 |
\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
734 |
\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
735 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
|
736 |
\endisatagML |
|
737 |
{\isafoldML}% |
|
738 |
% |
|
739 |
\isadelimML |
|
740 |
% |
|
741 |
\endisadelimML |
|
742 |
% |
|
743 |
\begin{isamarkuptext}% |
|
46262 | 744 |
If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|ORELSE| and not |
745 |
\verb|APPEND|, it applies \isa{tac} as many times as |
|
46259 | 746 |
possible in each outcome. |
747 |
||
748 |
\begin{warn} |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
749 |
Note the explicit abstraction over the goal state in the ML |
46260 | 750 |
definition of \verb|REPEAT|. Recursive tacticals must be coded in |
751 |
this awkward fashion to avoid infinite recursion of eager functional |
|
752 |
evaluation in Standard ML. The following attempt would make \verb|REPEAT|~\isa{tac} loop: |
|
46259 | 753 |
\end{warn}% |
754 |
\end{isamarkuptext}% |
|
755 |
\isamarkuptrue% |
|
756 |
% |
|
757 |
\isadelimML |
|
758 |
% |
|
759 |
\endisadelimML |
|
760 |
% |
|
761 |
\isatagML |
|
762 |
\isacommand{ML}\isamarkupfalse% |
|
763 |
\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline |
|
46260 | 764 |
\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}\ does\ not\ terminate{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline |
765 |
\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
46259 | 766 |
{\isaliteral{2A7D}{\isacharverbatimclose}}% |
767 |
\endisatagML |
|
768 |
{\isafoldML}% |
|
769 |
% |
|
770 |
\isadelimML |
|
771 |
% |
|
772 |
\endisadelimML |
|
46263 | 773 |
% |
46267 | 774 |
\isamarkupsubsection{Applying tactics to subgoal ranges% |
46263 | 775 |
} |
776 |
\isamarkuptrue% |
|
777 |
% |
|
778 |
\begin{isamarkuptext}% |
|
779 |
Tactics with explicit subgoal addressing |
|
780 |
\verb|int -> tactic| can be used together with tacticals that |
|
781 |
act like ``subgoal quantifiers'': guided by success of the body |
|
782 |
tactic a certain range of subgoals is covered. Thus the body tactic |
|
46267 | 783 |
is applied to \emph{all} subgoals, \emph{some} subgoal etc. |
46263 | 784 |
|
785 |
Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of |
|
786 |
these tacticals address subgoal ranges counting downwards from |
|
787 |
\isa{n} towards \isa{{\isadigit{1}}}. This has the fortunate effect that |
|
788 |
newly emerging subgoals are concatenated in the result, without |
|
789 |
interfering each other. Nonetheless, there might be situations |
|
46266 | 790 |
where a different order is desired.% |
46263 | 791 |
\end{isamarkuptext}% |
792 |
\isamarkuptrue% |
|
793 |
% |
|
794 |
\isadelimmlref |
|
795 |
% |
|
796 |
\endisadelimmlref |
|
797 |
% |
|
798 |
\isatagmlref |
|
799 |
% |
|
800 |
\begin{isamarkuptext}% |
|
801 |
\begin{mldecls} |
|
802 |
\indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\ |
|
803 |
\indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\ |
|
804 |
\indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\ |
|
46267 | 805 |
\indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\ |
46263 | 806 |
\indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\ |
807 |
\indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\ |
|
46267 | 808 |
\indexdef{}{ML}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\ |
46263 | 809 |
\end{mldecls} |
810 |
||
811 |
\begin{description} |
|
812 |
||
813 |
\item \verb|ALLGOALS|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\ {\isadigit{1}}}. It |
|
814 |
applies the \isa{tac} to all the subgoals, counting downwards. |
|
815 |
||
816 |
\item \verb|SOMEGOAL|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ {\isadigit{1}}}. It |
|
817 |
applies \isa{tac} to one subgoal, counting downwards. |
|
818 |
||
819 |
\item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}. It |
|
820 |
applies \isa{tac} to one subgoal, counting upwards. |
|
821 |
||
46267 | 822 |
\item \verb|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}. |
823 |
It applies \isa{tac} unconditionally to the first subgoal. |
|
824 |
||
46263 | 825 |
\item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or |
826 |
more to a subgoal, counting downwards. |
|
827 |
||
828 |
\item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or |
|
829 |
more to a subgoal, counting upwards. |
|
830 |
||
46267 | 831 |
\item \verb|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to |
832 |
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}. It applies the given list of tactics to the |
|
833 |
corresponding range of subgoals, counting downwards. |
|
834 |
||
46263 | 835 |
\end{description}% |
836 |
\end{isamarkuptext}% |
|
837 |
\isamarkuptrue% |
|
838 |
% |
|
839 |
\endisatagmlref |
|
840 |
{\isafoldmlref}% |
|
841 |
% |
|
842 |
\isadelimmlref |
|
843 |
% |
|
844 |
\endisadelimmlref |
|
46259 | 845 |
% |
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
846 |
\isamarkupsubsection{Control and search tacticals% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
847 |
} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
848 |
\isamarkuptrue% |
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 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
851 |
A predicate on theorems \verb|thm -> bool| can test |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
852 |
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
|
853 |
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
|
854 |
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
|
855 |
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
|
856 |
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
|
857 |
given tactic.% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
858 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
859 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
860 |
% |
46270 | 861 |
\isadelimmlref |
862 |
% |
|
863 |
\endisadelimmlref |
|
864 |
% |
|
865 |
\isatagmlref |
|
866 |
% |
|
867 |
\begin{isamarkuptext}% |
|
868 |
% |
|
869 |
\end{isamarkuptext}% |
|
870 |
\isamarkuptrue% |
|
871 |
% |
|
872 |
\endisatagmlref |
|
873 |
{\isafoldmlref}% |
|
874 |
% |
|
875 |
\isadelimmlref |
|
876 |
% |
|
877 |
\endisadelimmlref |
|
878 |
% |
|
46269
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
879 |
\isamarkupsubsubsection{Filtering a tactic's results% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
880 |
} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
881 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
882 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
883 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
884 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
885 |
\indexdef{}{ML}{FILTER}\verb|FILTER: (thm -> bool) -> tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
886 |
\indexdef{}{ML}{CHANGED}\verb|CHANGED: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
887 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
888 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
889 |
\begin{description} |
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 \verb|FILTER|~\isa{sat\ tac} applies \isa{tac} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
892 |
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
|
893 |
states that are satisfactory in the sense of \isa{sat}. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
894 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
895 |
\item \verb|CHANGED|~\isa{tac} applies \isa{tac} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
896 |
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
|
897 |
original state (according to \verb|Thm.eq_thm|). Thus \verb|CHANGED|~\isa{tac} always has some effect on the state. |
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 |
\end{description}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
900 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
901 |
\isamarkuptrue% |
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 |
\isamarkupsubsubsection{Depth-first search% |
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 |
\isamarkuptrue% |
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 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
908 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
909 |
\indexdef{}{ML}{DEPTH\_FIRST}\verb|DEPTH_FIRST: (thm -> bool) -> tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
910 |
\indexdef{}{ML}{DEPTH\_SOLVE}\verb|DEPTH_SOLVE: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
911 |
\indexdef{}{ML}{DEPTH\_SOLVE\_1}\verb|DEPTH_SOLVE_1: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
912 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
913 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
914 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
915 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
916 |
\item \verb|DEPTH_FIRST|~\isa{sat\ tac} returns the goal state if |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
917 |
\isa{sat} returns true. Otherwise it applies \isa{tac}, |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
918 |
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
|
919 |
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
|
920 |
\isa{tac}~\verb|THEN|~\verb|DEPTH_FIRST|~\isa{sat\ tac} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
921 |
the state. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
922 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
923 |
\item \verb|DEPTH_SOLVE|\isa{tac} uses \verb|DEPTH_FIRST| to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
924 |
search for states having no subgoals. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
925 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
926 |
\item \verb|DEPTH_SOLVE_1|~\isa{tac} uses \verb|DEPTH_FIRST| to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
927 |
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
|
928 |
it insists upon solving at least one subgoal. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
929 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
930 |
\end{description}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
931 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
932 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
933 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
934 |
\isamarkupsubsubsection{Other search strategies% |
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 |
\isamarkuptrue% |
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 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
939 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
940 |
\indexdef{}{ML}{BREADTH\_FIRST}\verb|BREADTH_FIRST: (thm -> bool) -> tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
941 |
\indexdef{}{ML}{BEST\_FIRST}\verb|BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
942 |
\indexdef{}{ML}{THEN\_BEST\_FIRST}\verb|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
|
943 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
944 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
945 |
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
|
946 |
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
|
947 |
the first satisfactory result from \isa{tac}. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
948 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
949 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
950 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
951 |
\item \verb|BREADTH_FIRST|~\isa{sat\ tac} uses breadth-first |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
952 |
search to find states for which \isa{sat} is true. For most |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
953 |
applications, it is too slow. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
954 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
955 |
\item \verb|BEST_FIRST|~\isa{{\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} does a heuristic |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
956 |
search, using \isa{dist} to estimate the distance from a |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
957 |
satisfactory state (in the sense of \isa{sat}). It maintains a |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
958 |
list of states ordered by distance. It applies \isa{tac} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
959 |
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
|
960 |
then it returns them. Otherwise, \verb|BEST_FIRST| adds the new |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
961 |
states to the list, and continues. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
962 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
963 |
The distance function is typically \verb|size_of_thm|, which computes |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
964 |
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
|
965 |
subgoals it has. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
966 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
967 |
\item \verb|THEN_BEST_FIRST|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}\ {\isaliteral{28}{\isacharparenleft}}sat{\isaliteral{2C}{\isacharcomma}}\ dist{\isaliteral{29}{\isacharparenright}}\ tac} is like |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
968 |
\verb|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
|
969 |
the result of applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{0}}} to the goal state. This |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
970 |
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
|
971 |
continuing the search. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
972 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
973 |
\end{description}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
974 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
975 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
976 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
977 |
\isamarkupsubsubsection{Auxiliary tacticals for searching% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
978 |
} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
979 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
980 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
981 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
982 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
983 |
\indexdef{}{ML}{COND}\verb|COND: (thm -> bool) -> tactic -> tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
984 |
\indexdef{}{ML}{IF\_UNSOLVED}\verb|IF_UNSOLVED: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
985 |
\indexdef{}{ML}{SOLVE}\verb|SOLVE: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
986 |
\indexdef{}{ML}{DETERM}\verb|DETERM: tactic -> tactic| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
987 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
988 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
989 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
990 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
991 |
\item \verb|COND|~\isa{sat\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
992 |
the goal state if it satisfies predicate \isa{sat}, and applies |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
993 |
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{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
|
994 |
\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is applied to a goal state. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
995 |
However, both \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are evaluated |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
996 |
because ML uses eager evaluation. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
997 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
998 |
\item \verb|IF_UNSOLVED|~\isa{tac} applies \isa{tac} to the |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
999 |
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
|
1000 |
otherwise. Many common tactics, such as \verb|resolve_tac|, fail if |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1001 |
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
|
1002 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1003 |
\item \verb|SOLVE|~\isa{tac} applies \isa{tac} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1004 |
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
|
1005 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1006 |
\item \verb|DETERM|~\isa{tac} applies \isa{tac} to the goal |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1007 |
state and returns the head of the resulting sequence. \verb|DETERM| |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1008 |
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
|
1009 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1010 |
\end{description}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1011 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1012 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1013 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1014 |
\isamarkupsubsubsection{Predicates and functions useful for searching% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1015 |
} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1016 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1017 |
% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1018 |
\begin{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1019 |
\begin{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1020 |
\indexdef{}{ML}{has\_fewer\_prems}\verb|has_fewer_prems: int -> thm -> bool| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1021 |
\indexdef{}{ML}{Thm.eq\_thm}\verb|Thm.eq_thm: thm * thm -> bool| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1022 |
\indexdef{}{ML}{Thm.eq\_thm\_prop}\verb|Thm.eq_thm_prop: thm * thm -> bool| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1023 |
\indexdef{}{ML}{size\_of\_thm}\verb|size_of_thm: thm -> int| \\ |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1024 |
\end{mldecls} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1025 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1026 |
\begin{description} |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1027 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1028 |
\item \verb|has_fewer_prems|~\isa{n\ thm} reports whether \isa{thm} has fewer than \isa{n} premises. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1029 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1030 |
\item \verb|Thm.eq_thm|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. Both theorems must have |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1031 |
compatible background theories. Both theorems must have the same |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1032 |
conclusions, the same set of hypotheses, and the same set of sort |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1033 |
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
|
1034 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1035 |
\item \verb|Thm.eq_thm_prop|~\isa{{\isaliteral{28}{\isacharparenleft}}thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} reports whether |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1036 |
the propositions of \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{thm\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} are equal. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1037 |
Names of bound variables are ignored. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1038 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1039 |
\item \verb|size_of_thm|~\isa{thm} computes the size of \isa{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
|
1040 |
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
|
1041 |
\verb|BEST_FIRST|. |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1042 |
|
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1043 |
\end{description}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1044 |
\end{isamarkuptext}% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1045 |
\isamarkuptrue% |
e75181672150
updated "Control and search tacticals" (moved from ref to implementation);
wenzelm
parents:
46267
diff
changeset
|
1046 |
% |
30296 | 1047 |
\isadelimtheory |
1048 |
% |
|
1049 |
\endisadelimtheory |
|
1050 |
% |
|
1051 |
\isatagtheory |
|
1052 |
\isacommand{end}\isamarkupfalse% |
|
1053 |
% |
|
1054 |
\endisatagtheory |
|
1055 |
{\isafoldtheory}% |
|
1056 |
% |
|
1057 |
\isadelimtheory |
|
1058 |
% |
|
1059 |
\endisadelimtheory |
|
1060 |
\isanewline |
|
1061 |
\end{isabellebody}% |
|
1062 |
%%% Local Variables: |
|
1063 |
%%% mode: latex |
|
1064 |
%%% TeX-master: "root" |
|
1065 |
%%% End: |