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