1\DOC DISJ_CASES_THENL
2
3\TYPE {DISJ_CASES_THENL : (thm_tactic list -> thm_tactic)}
4
5\SYNOPSIS
6Applies theorem-tactics in a list to the corresponding disjuncts in a theorem.
7
8\KEYWORDS
9theorem-tactic, disjunction, cases.
10
11\DESCRIBE
12If the theorem-tactics {f1...fn} applied to the {ASSUME}d disjuncts of a
13theorem
14{
15   |- d1 \/ d2 \/...\/ dn
16}
17produce results as follows when applied to a goal {(A ?- t)}:
18{
19    A ?- t                                A ?- t
20   =========  f1 (d1 |- d1) and ... and =========  fn (dn |- dn)
21    A ?- t1                              A ?- tn
22}
23then applying {DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn)}
24to the goal {(A ?- t)} produces n subgoals.
25{
26           A ?- t
27   =======================  DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn)
28    A ?- t1  ...  A ?- tn
29}
30{DISJ_CASES_THENL} is defined using iteration, hence for
31theorems with more than {n} disjuncts, {dn} would itself be disjunctive.
32
33\FAILURE
34Fails if the number of tactic generating functions in the list exceeds
35the number of disjuncts in the theorem.  An invalid tactic is
36produced if the theorem has any hypothesis which is not
37alpha-convertible to an assumption of the goal.
38
39\USES
40Used when the goal is to be split into several cases, where a
41different tactic-generating function is to be applied to each case.
42
43\SEEALSO
44Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THEN2, Thm_cont.STRIP_THM_THEN.
45\ENDDOC
46