`COND_CASES_TAC : tactic`

SYNOPSIS
Induces a case split on a conditional expression in the goal.

DESCRIPTION
COND_CASES_TAC searches for a free conditional subterm in the term of a goal, i.e. a subterm of the form if p then u else v, choosing some topmost one if there are several. It then induces a case split over p as follows:
```                       A ?- t
==========================================  COND_CASES_TAC
A u {p} ?- t[T/p; u/(if p then u else v)]
A u {~p} ?- t[F/p; v/(if p then u else v)]
```
where p is not a constant, and the term p then u else v is free in t. Note that it both enriches the assumptions and inserts the assumed value into the conditional.

FAILURE CONDITIONS
COND_CASES_TAC fails if there is no conditional sub-term as described above.

EXAMPLE
We can prove the following just by REAL_ARITH `!x y:real. x <= max x y`, but it is instructive to consider a manual proof.
```  # g `!x y:real. x <= max x y`;;
val it : goalstack = 1 subgoal (1 total)

`!x y. x <= max x y`

# e(REPEAT GEN_TAC THEN REWRITE_TAC[real_max]);;'
val it : goalstack = 1 subgoal (1 total)

`x <= (if x <= y then y else x)`

# e COND_CASES_TAC;;
val it : goalstack = 1 subgoal (1 total)

0 [`~(x <= y)`]

`x <= x`
```

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 always be depended on to choose the `desired' one. It can, however, be used repeatedly to analyze all conditional sub-terms of a goal.