1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
\DOC CONJ_LIST
\TYPE {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
}
\noindent Here are some applications of {CONJ_LIST} to {th}:
{
#CONJ_LIST 0 th;;
evaluation failed CONJ_LIST
#CONJ_LIST 1 th;;
[A |- (x /\ y) /\ z /\ w] : thm list
#CONJ_LIST 2 th;;
[A |- x /\ y; A |- z /\ w] : thm list
#CONJ_LIST 3 th;;
[A |- x /\ y; A |- z; A |- w] : thm list
#CONJ_LIST 4 th;;
evaluation failed CONJ_LIST
}
\SEEALSO
BODY_CONJUNCTS, LIST_CONJ, CONJUNCTS, CONJ, CONJUNCT1, CONJUNCT2, CONJ_PAIR.
\ENDDOC
|
