313 \end{ttdescription} |
313 \end{ttdescription} |
314 |
314 |
315 |
315 |
316 \section{Obscure tactics} |
316 \section{Obscure tactics} |
317 |
317 |
318 \subsection{Rotating assumptions} |
|
319 \index{assumptions!rotating} |
|
320 \begin{ttbox} |
|
321 rotate_tac : int -> int -> tactic |
|
322 \end{ttbox} |
|
323 \begin{ttdescription} |
|
324 \item[\ttindexbold{rotate_tac} $n$ $i$] |
|
325 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left, |
|
326 if $n$ is positive, and from left to right, if $n$ is negative. Sometimes |
|
327 necessary in connection with \ttindex{asm_full_simp_tac}. |
|
328 |
|
329 \end{ttdescription} |
|
330 |
|
331 \subsection{Tidying the proof state} |
|
332 \index{parameters!removing unused} |
|
333 \index{flex-flex constraints} |
|
334 \begin{ttbox} |
|
335 prune_params_tac : tactic |
|
336 flexflex_tac : tactic |
|
337 \end{ttbox} |
|
338 \begin{ttdescription} |
|
339 \item[\ttindexbold{prune_params_tac}] |
|
340 removes unused parameters from all subgoals of the proof state. It works |
|
341 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can |
|
342 make the proof state more readable. It is used with |
|
343 \ttindex{rule_by_tactic} to simplify the resulting theorem. |
|
344 |
|
345 \item[\ttindexbold{flexflex_tac}] |
|
346 removes all flex-flex pairs from the proof state by applying the trivial |
|
347 unifier. This drastic step loses information, and should only be done as |
|
348 the last step of a proof. |
|
349 |
|
350 Flex-flex constraints arise from difficult cases of higher-order |
|
351 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate |
|
352 some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex |
|
353 constraints can be ignored; they often disappear as unknowns get |
|
354 instantiated. |
|
355 \end{ttdescription} |
|
356 |
|
357 |
|
358 \subsection{Renaming parameters in a goal} \index{parameters!renaming} |
318 \subsection{Renaming parameters in a goal} \index{parameters!renaming} |
359 \begin{ttbox} |
319 \begin{ttbox} |
360 rename_tac : string -> int -> tactic |
320 rename_tac : string -> int -> tactic |
361 rename_last_tac : string -> string list -> int -> tactic |
321 rename_last_tac : string -> string list -> int -> tactic |
362 Logic.set_rename_prefix : string -> unit |
322 Logic.set_rename_prefix : string -> unit |
396 sets the prefix for uniform renaming to~{\it prefix}. The default prefix |
356 sets the prefix for uniform renaming to~{\it prefix}. The default prefix |
397 is {\tt"k"}. |
357 is {\tt"k"}. |
398 |
358 |
399 \item[\ttindexbold{Logic.auto_rename} := true;] |
359 \item[\ttindexbold{Logic.auto_rename} := true;] |
400 makes Isabelle generate uniform names for parameters. |
360 makes Isabelle generate uniform names for parameters. |
|
361 \end{ttdescription} |
|
362 |
|
363 |
|
364 \subsection{Manipulating assumptions} |
|
365 \index{assumptions!rotating} |
|
366 \begin{ttbox} |
|
367 thin_tac : string -> int -> tactic |
|
368 rotate_tac : int -> int -> tactic |
|
369 \end{ttbox} |
|
370 \begin{ttdescription} |
|
371 \item[\ttindexbold{thin_tac} {\it formula} $i$] |
|
372 \index{assumptions!deleting} |
|
373 deletes the specified assumption from subgoal $i$. Often the assumption |
|
374 can be abbreviated, replacing subformul{\ae} by unknowns; the first matching |
|
375 assumption will be deleted. Removing useless assumptions from a subgoal |
|
376 increases its readability and can make search tactics run faster. |
|
377 |
|
378 \item[\ttindexbold{rotate_tac} $n$ $i$] |
|
379 \index{assumptions!rotating} |
|
380 rotates the assumptions of subgoal $i$ by $n$ positions: from right to left |
|
381 if $n$ is positive, and from left to right if $n$ is negative. This is |
|
382 sometimes necessary in connection with \ttindex{asm_full_simp_tac}, which |
|
383 processes assumptions from left to right. |
|
384 \end{ttdescription} |
|
385 |
|
386 |
|
387 \subsection{Tidying the proof state} |
|
388 \index{parameters!removing unused} |
|
389 \index{flex-flex constraints} |
|
390 \begin{ttbox} |
|
391 prune_params_tac : tactic |
|
392 flexflex_tac : tactic |
|
393 \end{ttbox} |
|
394 \begin{ttdescription} |
|
395 \item[\ttindexbold{prune_params_tac}] |
|
396 removes unused parameters from all subgoals of the proof state. It works |
|
397 by rewriting with the theorem $(\Forall x. V)\equiv V$. This tactic can |
|
398 make the proof state more readable. It is used with |
|
399 \ttindex{rule_by_tactic} to simplify the resulting theorem. |
|
400 |
|
401 \item[\ttindexbold{flexflex_tac}] |
|
402 removes all flex-flex pairs from the proof state by applying the trivial |
|
403 unifier. This drastic step loses information, and should only be done as |
|
404 the last step of a proof. |
|
405 |
|
406 Flex-flex constraints arise from difficult cases of higher-order |
|
407 unification. To prevent this, use \ttindex{res_inst_tac} to instantiate |
|
408 some variables in a rule~(\S\ref{res_inst_tac}). Normally flex-flex |
|
409 constraints can be ignored; they often disappear as unknowns get |
|
410 instantiated. |
401 \end{ttdescription} |
411 \end{ttdescription} |
402 |
412 |
403 |
413 |
404 \subsection{Composition: resolution without lifting} |
414 \subsection{Composition: resolution without lifting} |
405 \index{tactics!for composition} |
415 \index{tactics!for composition} |