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