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