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
44
45
46
47
48
49
50
|
\DOC BOOL_CASES_TAC
\TYPE {BOOL_CASES_TAC : term -> tactic}
\SYNOPSIS
Performs boolean case analysis on a (free) term in the goal.
\KEYWORDS
tactic, cases.
\DESCRIBE
When applied to a term {x} (which must be of type {bool} but need not be simply
a variable), and a goal {A ?- t}, the tactic {BOOL_CASES_TAC} generates the two
subgoals corresponding to {A ?- t} but with any free instances of {x} replaced
by {F} and {T} respectively.
{
A ?- t
============================ BOOL_CASES_TAC `x`
A ?- t[F/x] A ?- t[T/x]
}
\noindent The term given does not have to be free in the goal, but if it isn't,
{BOOL_CASES_TAC} will merely duplicate the original goal twice. Note that in
the new goals, we don't have {x} and {~x} as assumptions; for that use
{ASM_CASES_TAC}.
\FAILURE
Fails unless the term {x} has type {bool}.
\EXAMPLE
The goal:
{
# g `(b ==> ~b) ==> (b ==> a)`;;
}
\noindent can be completely solved by using {BOOL_CASES_TAC} on the variable
{b}, then simply rewriting the two subgoals using only the inbuilt tautologies,
i.e. by applying the following tactic:
{
# e(BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
val it : goalstack = No subgoals
}
\USES
Avoiding fiddly logical proofs by brute-force case analysis, possibly only
over a key term as in the above example, possibly over all free boolean
variables.
\SEEALSO
ASM_CASES_TAC, COND_CASES_TAC, DISJ_CASES_TAC, ITAUT, STRUCT_CASES_TAC, TAUT.
\ENDDOC
|
