1\DOC BOOL_CASES_TAC
2
3\TYPE {BOOL_CASES_TAC : (term -> tactic)}
4
5\SYNOPSIS
6Performs boolean case analysis on a (free) term in the goal.
7
8\KEYWORDS
9tactic, cases.
10
11\DESCRIBE
12When applied to a term {x} (which must be of type {bool} but need not be simply
13a variable), and a goal {A ?- t}, the tactic {BOOL_CASES_TAC} generates the two
14subgoals corresponding to {A ?- t} but with any free instances of {x} replaced
15by {F} and {T} respectively.
16{
17              A ?- t
18   ============================  BOOL_CASES_TAC "x"
19    A ?- t[F/x]    A ?- t[T/x]
20}
21The term given does not have to be free in the goal, but if it isn't,
22{BOOL_CASES_TAC} will merely duplicate the original goal twice.
23
24\FAILURE
25Fails unless the term {x} has type {bool}.
26
27\EXAMPLE
28The goal:
29{
30   ?- (b ==> ~b) ==> (b ==> a)
31}
32can be completely solved by using {BOOL_CASES_TAC} on the variable
33{b}, then simply rewriting the two subgoals using only the inbuilt tautologies,
34i.e. by applying the following tactic:
35{
36   BOOL_CASES_TAC (Parse.Term `b:bool`) THEN REWRITE_TAC[]
37}
38
39
40\USES
41Avoiding fiddly logical proofs by brute-force case analysis, possibly only
42over a key term as in the above example, possibly over all free boolean
43variables.
44
45\SEEALSO
46Tactic.ASM_CASES_TAC, Tactic.COND_CASES_TAC, Tactic.DISJ_CASES_TAC, Tactic.STRUCT_CASES_TAC.
47\ENDDOC
48