1\DOC CONJ_LIST
2
3\TYPE {CONJ_LIST : (int -> thm -> thm list)}
4
5\SYNOPSIS
6Extracts a list of conjuncts from a theorem (non-flattening version).
7
8\KEYWORDS
9rule, conjunction.
10
11\DESCRIBE
12{CONJ_LIST} is the proper inverse of {LIST_CONJ}. Unlike {CONJUNCTS} which
13recursively splits as many conjunctions as possible both to the left and to
14the right, {CONJ_LIST} splits the top-level conjunction and then splits
15(recursively) only the right conjunct. The integer argument is required
16because the term {tn} may itself be a conjunction. A list of {n} theorems is
17returned.
18{
19    A |- t1 /\ (t2 /\ ( ... /\ tn)...)
20   ------------------------------------  CONJ_LIST n (A |- t1 /\ ... /\ tn)
21    A |- t1   A |- t2   ...   A |- tn
22}
23
24
25\FAILURE
26Fails if the integer argument ({n}) is less than one, or if the input theorem
27has less than {n} conjuncts.
28
29\EXAMPLE
30Suppose the identifier {th} is bound to the theorem:
31{
32   A |- (x /\ y) /\ z /\ w
33}
34Here are some applications of {CONJ_LIST} to {th}:
35{
36   - CONJ_LIST 0 th;
37   ! Uncaught exception:
38   ! HOL_ERR
39
40   - CONJ_LIST 1 th;
41   > val it = [[A] |- (x /\ y) /\ z /\ w] : thm list
42
43   - CONJ_LIST 2 th;
44   > val it = [ [A] |- x /\ y,  [A] |- z /\ w] : thm list
45
46   - CONJ_LIST 3 th;
47   > val it = [ [A] |- x /\ y,  [A] |- z,  [A] |- w] : thm list
48
49   - CONJ_LIST 4 th;
50   ! Uncaught exception:
51   ! HOL_ERR
52}
53
54
55\SEEALSO
56Drule.BODY_CONJUNCTS, Drule.LIST_CONJ, Drule.CONJUNCTS, Thm.CONJ, Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJ_PAIR.
57\ENDDOC
58