----------------------------------------------------------------------
CONJ_LIST                                                      (Drule)
----------------------------------------------------------------------
CONJ_LIST : (int -> thm -> thm list)

SYNOPSIS
Extracts a list of conjuncts from a theorem (non-flattening version).

KEYWORDS
rule, conjunction.

DESCRIBE
{CONJ_LIST} is the proper inverse of {LIST_CONJ}. Unlike {CONJUNCTS} which
recursively splits as many conjunctions as possible both to the left and to
the right, {CONJ_LIST} splits the top-level conjunction and then splits
(recursively) only the right conjunct. The integer argument is required
because the term {tn} may itself be a conjunction. A list of {n} theorems is
returned.

    A |- t1 /\ (t2 /\ ( ... /\ tn)...)
   ------------------------------------  CONJ_LIST n (A |- t1 /\ ... /\ tn)
    A |- t1   A |- t2   ...   A |- tn




FAILURE
Fails if the integer argument ({n}) is less than one, or if the input theorem
has less than {n} conjuncts.

EXAMPLE
Suppose the identifier {th} is bound to the theorem:

   A |- (x /\ y) /\ z /\ w

Here are some applications of {CONJ_LIST} to {th}:

   - CONJ_LIST 0 th;
   ! Uncaught exception:
   ! HOL_ERR

   - CONJ_LIST 1 th;
   > val it = [[A] |- (x /\ y) /\ z /\ w] : thm list

   - CONJ_LIST 2 th;
   > val it = [ [A] |- x /\ y,  [A] |- z /\ w] : thm list

   - CONJ_LIST 3 th;
   > val it = [ [A] |- x /\ y,  [A] |- z,  [A] |- w] : thm list

   - CONJ_LIST 4 th;
   ! Uncaught exception:
   ! HOL_ERR




SEEALSO
Drule.BODY_CONJUNCTS, Drule.LIST_CONJ, Drule.CONJUNCTS, Thm.CONJ,
Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJ_PAIR.

----------------------------------------------------------------------