1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
\DOC TRY
\TYPE {TRY : tactic -> tactic}
\SYNOPSIS
Makes a tactic have no effect rather than fail.
\KEYWORDS
tactical, failure.
\DESCRIBE
For any tactic {t}, the application {TRY t} gives a new tactic
which has the same effect as {t} if that succeeds, and otherwise has
no effect.
\FAILURE
The application of {TRY} to a tactic never fails. The resulting
tactic never fails.
\EXAMPLE
We might want to try a certain tactic ``speculatively'', even if we're not sure
that it will work, for example, to handle the ``easy'' subgoals from breaking
apart a large conjunction. On a small scale, we might want to prove:
{
# g `(x + 1) EXP 2 = x EXP 2 + 2 * x + 1 /\
(x EXP 2 = y EXP 2 ==> x = y) /\
(x < y ==> 2 * x + 1 < 2 * y)`;;
...
}
\noindent and just see which conjuncts we can get rid of automatically by
{ARITH_TAC}. It turns out that it only leaves one subgoal with some nonlinear
reasoning:
{
# e(REPEAT CONJ_TAC THEN TRY ARITH_TAC);;
val it : goalstack = 1 subgoal (1 total)
`x EXP 2 = y EXP 2 ==> x = y`
}
\SEEALSO
CHANGED_TAC, VALID.
\ENDDOC
|
