1\DOC CONJUNCTS_THEN2
2
3\TYPE {CONJUNCTS_THEN2 : (thm_tactic -> thm_tactical)}
4
5\SYNOPSIS
6Applies two theorem-tactics to the corresponding conjuncts of a theorem.
7
8\KEYWORDS
9theorem-tactic, conjunction.
10
11\DESCRIBE
12{CONJUNCTS_THEN2} takes two theorem-tactics, {f1} and {f2}, and a theorem {t}
13whose conclusion must be a conjunction. {CONJUNCTS_THEN2} breaks {t} into two
14new theorems, {t1} and {t2} which are {CONJUNCT1} and {CONJUNCT2} of {t}
15respectively, and then returns the tactic {f1 t1 THEN f2 t2}. Thus
16{
17   CONJUNCTS_THEN2 f1 f2 (A |- l /\ r) =  f1 (A |- l) THEN f2 (A |- r)
18}
19so if
20{
21   A1 ?- t1                     A2 ?- t2
22  ==========  f1 (A |- l)      ==========  f2 (A |- r)
23   A2 ?- t2                     A3 ?- t3
24}
25then
26{
27    A1 ?- t1
28   ==========  CONJUNCTS_THEN2 f1 f2 (A |- l /\ r)
29    A3 ?- t3
30}
31
32
33\FAILURE
34{CONJUNCTS_THEN f} will fail if applied to a theorem whose conclusion is not a
35conjunction.
36
37\COMMENTS
38The system shows the type as {(thm_tactic -> thm_tactical)}.
39
40\USES
41The construction of complex {tactical}s like {CONJUNCTS_THEN}.
42
43\SEEALSO
44Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJUNCTS, Tactic.CONJ_TAC, Thm_cont.CONJUNCTS_THEN2, Thm_cont.STRIP_THM_THEN.
45\ENDDOC
46