Thm_cont.DISJ_CASES

STRUCTURE

SYNOPSIS

Applies theorem-tactics in a list to the corresponding disjuncts in a theorem.

DESCRIPTION

If the theorem-tactics f1...fn applied to the ASSUMEd disjuncts of a theorem

   |- d1 \/ d2 \/...\/ dn

produce results as follows when applied to a goal (A ?- t):

    A ?- t                                A ?- t
   =========  f1 (d1 |- d1) and ... and =========  fn (dn |- dn)
    A ?- t1                              A ?- tn

then applying DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn) to the goal (A ?- t) produces n subgoals.

           A ?- t
   =======================  DISJ_CASES_THENL [f1;...;fn] (|- d1 \/...\/ dn)
    A ?- t1  ...  A ?- tn

DISJ_CASES_THENL is defined using iteration, hence for theorems with more than n disjuncts, dn would itself be disjunctive.

FAILURE

Fails if the number of tactic generating functions in the list exceeds the number of disjuncts in the theorem. An invalid tactic is produced if the theorem has any hypothesis which is not alpha-convertible to an assumption of the goal.

USES

Used when the goal is to be split into several cases, where a different tactic-generating function is to be applied to each case.

SEEALSO

CHOOSE_THEN, CONJUNCTS_THEN, CONJUNCTS_THEN2, DISJ_CASES_THEN, DISJ_CASES_THEN2, STRIP_THM_THEN