Translating from HOL interpreter to TAC_PROOF with THENL

The steps in the THENL brackets work correctly if I type them sequentially into the HOL interpreter. But when I combine them with TAC_PROOF using THENL, I get an error.

I think I understand the difference between THEN and THENL (all subgoals versus single subgoal). But I can't find the syntax to differentiate between the 2 initial subgoals. DISJ1_TAC and RES_TAC should only apply to subgoal1. While DISJ2_TAC and RES_TAC should only apply to subgoal2.

How can I fix this?

val constructiveDilemmaRule =
TAC_PROOF (([],``! p q r s .(p==>q) /\ (r==>s) ==> p \/ r ==>q \/s``),
REPEAT STRIP_TAC
THENL [DISJ1_TAC THEN RES_TAC]
THENL [DISJ2_TAC, RES_TAC]);

Solution

You've almost got it. Applying REPEAT STRIP_TAC gives two subgoals, so the list argument to THENL should contain two tactics:

val g = (([], ``! p q r s .(p ==> q) /\ (r ==> s) ==> p \/ r ==> q \/ s``) : goal);
val tac = (REPEAT STRIP_TAC)
          THENL [DISJ1_TAC THEN RES_TAC,
                 DISJ2_TAC THEN RES_TAC];
val constructiveDilemmaRule = TAC_PROOF (g, tac);

The first element of the argument list (DISJ1_TAC...) is applied to the first subgoal. The second element of the argument list (DISJ2_TAC) is applied to the second subgoal.