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
|
\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.
\FAILURE
Fails unless the term {x} has type {bool}.
\EXAMPLE
The goal:
{
?- (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:
{
BOOL_CASES_TAC "b:bool" THEN REWRITE_TAC[]
}
\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, STRUCT_CASES_TAC.
\ENDDOC
|
