1\DOC COND_CASES_TAC 2 3\TYPE {COND_CASES_TAC : tactic} 4 5\SYNOPSIS 6Induces a case split on a conditional expression in the goal. 7 8\KEYWORDS 9tactic, conditional, cases. 10 11\DESCRIBE 12{COND_CASES_TAC} searches for a conditional sub-term in the term of a goal, 13i.e. a sub-term of the form {p=>u|v}, choosing one by its own criteria if there 14is more than one. It then induces a case split over {p} as follows: 15{ 16 A ?- t 17 ============================================================== COND_CASES_TAC 18 A u {p} ?- t[u/(p=>u|v),T/p] A u {~p} ?- t[v/(p=>u|v),F/p] 19} 20where {p} is not a constant, and the term {p=>u|v} is free in {t}. 21Note that it both enriches the assumptions and inserts the assumed value into 22the conditional. 23 24\FAILURE 25{COND_CASES_TAC} fails if there is no conditional sub-term as described above. 26 27\EXAMPLE 28For {"x"}, {"y"}, {"z1"} and {"z2"} of type {":*"}, and {"P:*->bool"}, 29{ 30 COND_CASES_TAC ([], "x = (P y => z1 | z2)");; 31 ([(["P y"], "x = z1"); (["~P y"], "x = z2")], -) : subgoals 32} 33but it fails, for example, if {"y"} is not free in the 34term part of the goal: 35{ 36 COND_CASES_TAC ([], "!y. x = (P y => z1 | z2)");; 37 evaluation failed COND_CASES_TAC 38} 39In contrast, {ASM_CASES_TAC} does not perform the replacement: 40{ 41 ASM_CASES_TAC "P y" ([], "x = (P y => z1 | z2)");; 42 ([(["P y"], "x = (P y => z1 | z2)"); (["~P y"], "x = (P y => z1 | z2)")], 43 -) 44 : subgoals 45} 46 47 48\USES 49Useful for case analysis and replacement in one step, when there is a 50conditional sub-term in the term part of the goal. When there is more than 51one such sub-term and one in particular is to be analyzed, {COND_CASES_TAC} 52cannot be depended on to choose the `desired' one. It can, however, be used 53repeatedly to analyze all conditional sub-terms of a goal. 54 55\SEEALSO 56Tactic.ASM_CASES_TAC, Tactic.DISJ_CASES_TAC, Tactic.STRUCT_CASES_TAC. 57\ENDDOC 58