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