BOOL_CASES_TAC : (term -> tactic)

- STRUCTURE
- SYNOPSIS
- Performs boolean case analysis on a (free) term in the goal.
- DESCRIPTION
- 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.
A ?- t ============================ BOOL_CASES_TAC "x" A ?- t[F/x] A ?- t[T/x]

- FAILURE
- Fails unless the term x has type bool.
- EXAMPLE
- The goal: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:
?- (b ==> ~b) ==> (b ==> a)

BOOL_CASES_TAC (Parse.Term `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

HOL Kananaskis-14