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
|
\DOC CONJ_SET_CONV
\TYPE {CONJ_SET_CONV : (term list -> term list -> thm)}
\SYNOPSIS
Proves the equivalence of the conjunctions of two equal sets of terms.
\KEYWORDS
conversion, conjunction.
\DESCRIBE
The arguments to {CONJ_SET_CONV} are two lists of terms {[t1;...;tn]} and
{[u1;...;um]}. If these are equal when considered as sets, that is if the sets
{
{{t1,...,tn}} and {{u1,...,um}}
}
\noindent are equal, then {CONJ_SET_CONV} returns the theorem:
{
|- (t1 /\ ... /\ tn) = (u1 /\ ... /\ um)
}
\noindent Otherwise {CONJ_SET_CONV} fails.
\FAILURE
{CONJ_SET_CONV [t1;...;tn] [u1;...;um]} fails if {[t1,...,tn]} and
{[u1,...,um]}, regarded as sets of terms, are not equal. Also fails
if any {ti} or {ui} does not have type {bool}.
\USES
Used to order conjuncts. First sort a list of conjuncts {l1} into the
desired order to get a new list {l2}, then call {CONJ_SET_CONV l1 l2}.
\COMMENTS
This is not a true conversion, so perhaps it ought to be called something else.
\SEEALSO
CONJUNCTS_CONV.
\ENDDOC
|
