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:
                             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]
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.
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",
   COND_CASES_TAC ([], "x = (P y => z1 | z2)");;
   ([(["P y"], "x = z1"); (["~P y"], "x = z2")], -) : subgoals
but it fails, for example, if "y" is not free in the term part of the goal:
   COND_CASES_TAC ([], "!y. x = (P y => z1 | z2)");;
   evaluation failed     COND_CASES_TAC
In contrast, ASM_CASES_TAC does not perform the replacement:
   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-13