BOOL_CASES_TAC : term -> tactic
Performs boolean case analysis on a (free) term in the goal.
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.
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
A ?- t
============================ BOOL_CASES_TAC `x`
A ?- t[F/x] A ?- t[T/x]
- FAILURE CONDITIONS
Fails unless the term x has type bool.
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:
# g `(b ==> ~b) ==> (b ==> a)`;;
# e(BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC);;
val it : goalstack = No subgoals
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
- SEE ALSO
ASM_CASES_TAC, COND_CASES_TAC, DISJ_CASES_TAC, ITAUT, STRUCT_CASES_TAC, TAUT.