1\DOC CONJUNCTS_THEN
2
3\TYPE {CONJUNCTS_THEN : thm_tactical}
4
5\SYNOPSIS
6Applies a theorem-tactic to each conjunct of a theorem.
7
8\KEYWORDS
9theorem-tactic, conjunction.
10
11\DESCRIBE
12{CONJUNCTS_THEN} takes a theorem-tactic {f}, and a theorem {t} whose conclusion
13must be a conjunction. {CONJUNCTS_THEN} breaks {t} into two new theorems, {t1}
14and {t2} which are {CONJUNCT1} and {CONJUNCT2} of {t} respectively, and then
15returns a new tactic: {f t1 THEN f t2}. That is,
16{
17   CONJUNCTS_THEN f (A |- l /\ r) =  f (A |- l) THEN f (A |- r)
18}
19so if
20{
21   A1 ?- t1                    A2 ?- t2
22  ==========  f (A |- l)      ==========  f (A |- r)
23   A2 ?- t2                    A3 ?- t3
24}
25then
26{
27    A1 ?- t1
28   ==========  CONJUNCTS_THEN f (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
38{CONJUNCTS_THEN f (A |- u1 /\ ... /\ un)} results in the tactic:
39{
40   f (A |- u1) THEN f (A |- u2 /\ ... /\ un)
41}
42Unfortunately, it is more likely that the user had wanted the tactic:
43{
44   f (A |- u1) THEN ... THEN f(A |- un)
45}
46Such a tactic could be defined as follows:
47{
48   fun CONJUNCTS_THENL (f:thm_tactic) thm =
49     List.foldl (op THEN) ALL_TAC (map f (CONJUNCTS thm));
50}
51or by using {REPEAT_TCL}.
52
53\SEEALSO
54Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJUNCTS, Tactic.CONJ_TAC, Thm_cont.CONJUNCTS_THEN2, Thm_cont.STRIP_THM_THEN.
55\ENDDOC
56