Tactic.COND_CASES

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

ASM_CASES_TAC, DISJ_CASES_TAC, STRUCT_CASES_TAC