1\DOC DISJ_CASES_THEN
2
3\TYPE {DISJ_CASES_THEN : thm_tactical}
4
5\SYNOPSIS
6Applies a theorem-tactic to each disjunct of a disjunctive theorem.
7
8\KEYWORDS
9theorem-tactic, disjunction, cases.
10
11\DESCRIBE
12If the theorem-tactic {f:thm->tactic} applied to either
13{ASSUME}d disjunct produces results as follows when applied to a goal
14{(A ?- t)}:
15{
16    A ?- t                                A ?- t
17   =========  f (u |- u)      and        =========  f (v |- v)
18    A ?- t1                               A ?- t2
19}
20then applying {DISJ_CASES_THEN f (|- u \/ v)}
21to the goal {(A ?- t)} produces two subgoals.
22{
23           A ?- t
24   ======================  DISJ_CASES_THEN f (|- u \/ v)
25    A ?- t1      A ?- t2
26}
27
28
29\FAILURE
30Fails if the theorem is not a disjunction.  An invalid tactic is
31produced if the theorem has any hypothesis which is not
32alpha-convertible to an assumption of the goal.
33
34\EXAMPLE
35Given the theorem
36{
37   th = |- (m = 0) \/ (?n. m = SUC n)
38}
39and a goal of the form {?- (PRE m = m) = (m = 0)},
40applying the tactic
41{
42   DISJ_CASES_THEN ASSUME_TAC th
43}
44produces two subgoals, each with one disjunct as an added
45assumption:
46{
47   ?n. m = SUC n ?- (PRE m = m) = (m = 0)
48
49   m = 0 ?- (PRE m = m) = (m = 0)
50}
51
52
53\USES
54Building cases tactics. For example, {DISJ_CASES_TAC} could be defined by:
55{
56   val DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC
57}
58
59
60\COMMENTS
61Use {DISJ_CASES_THEN2} to apply different tactic generating functions
62to each case.
63
64\SEEALSO
65Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm.DISJ_CASES, Tactic.DISJ_CASES_TAC, Thm_cont.DISJ_CASES_THEN2, Thm_cont.DISJ_CASES_THENL, Thm_cont.STRIP_THM_THEN.
66\ENDDOC
67