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