1\DOC DISJ_CASES_THEN2
2
3\TYPE {DISJ_CASES_THEN2 : (thm_tactic -> thm_tactical)}
4
5\SYNOPSIS
6Applies separate theorem-tactics to the two disjuncts of a theorem.
7
8\KEYWORDS
9theorem-tactic, disjunction, cases.
10
11\DESCRIBE
12If the theorem-tactics {f1} and {f2}, applied to the {ASSUME}d left and right
13disjunct of a theorem {|- u \/ v} respectively, produce results as follows when
14applied to a goal {(A ?- t)}:
15{
16    A ?- t                                 A ?- t
17   =========  f1 (u |- u)      and        =========  f2 (v |- v)
18    A ?- t1                                A ?- t2
19}
20then applying {DISJ_CASES_THEN2 f1 f2 (|- u \/ v)} to the
21goal {(A ?- t)} produces two subgoals.
22{
23           A ?- t
24   ======================  DISJ_CASES_THEN2 f1 f2 (|- 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_THEN2 SUBST1_TAC ASSUME_TAC th
43}
44to the goal will produce two subgoals
45{
46   ?n. m = SUC n ?- (PRE m = m) = (m = 0)
47
48   ?- (PRE 0 = 0) = (0 = 0)
49}
50The first subgoal has had the disjunct {m = 0} used
51for a substitution, and the second has added the disjunct to the
52assumption list.  Alternatively, applying the tactic
53{
54   DISJ_CASES_THEN2 SUBST1_TAC (CHOOSE_THEN SUBST1_TAC) th
55}
56to the goal produces the subgoals:
57{
58   ?- (PRE(SUC n) = SUC n) = (SUC n = 0)
59
60   ?- (PRE 0 = 0) = (0 = 0)
61}
62
63
64\USES
65Building cases tacticals. For example, {DISJ_CASES_THEN} could be defined by:
66{
67  let DISJ_CASES_THEN f = DISJ_CASES_THEN2 f f
68}
69
70
71\SEEALSO
72Thm_cont.STRIP_THM_THEN, Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THENL.
73\ENDDOC
74