CONJ_LIST

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

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

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

See also

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