COND_CASES_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Induces a case split on a conditional expression in the goal.
- DESCRIPTION
- COND_CASES_TAC searches for a conditional sub-term in the term of a goal, i.e. a sub-term of the form p=>u|v, choosing one by its own criteria if there is more than one. It then induces a case split over p as follows:where p is not a constant, and the term p=>u|v is free in t. Note that it both enriches the assumptions and inserts the assumed value into the conditional.
A ?- t ============================================================== COND_CASES_TAC A u {p} ?- t[u/(p=>u|v),T/p] A u {~p} ?- t[v/(p=>u|v),F/p]

- FAILURE
- COND_CASES_TAC fails if there is no conditional sub-term as described above.
- EXAMPLE
- For "x", "y", "z1" and "z2" of type ":*", and "P:*->bool",but it fails, for example, if "y" is not free in the term part of the goal:
COND_CASES_TAC ([], "x = (P y => z1 | z2)");; ([(["P y"], "x = z1"); (["~P y"], "x = z2")], -) : subgoals

In contrast, ASM_CASES_TAC does not perform the replacement:COND_CASES_TAC ([], "!y. x = (P y => z1 | z2)");; evaluation failed COND_CASES_TAC

ASM_CASES_TAC "P y" ([], "x = (P y => z1 | z2)");; ([(["P y"], "x = (P y => z1 | z2)"); (["~P y"], "x = (P y => z1 | z2)")], -) : subgoals

- USES
- Useful for case analysis and replacement in one step, when there is a conditional sub-term in the term part of the goal. When there is more than one such sub-term and one in particular is to be analyzed, COND_CASES_TAC cannot be depended on to choose the ‘desired’ one. It can, however, be used repeatedly to analyze all conditional sub-terms of a goal.
- SEEALSO

HOL Kananaskis-14