CONJUNCTS_ACDrule.CONJUNCTS_AC : term * term -> thmProve equivalence under idempotence, symmetry and associativity of conjunction.
CONJUNCTS_AC takes a pair of terms (t1, t2)
and proves |- t1 = t2 if t1 and
t2 are equivalent up to idempotence, symmetry and
associativity of conjunction. That is, if t1 and
t2 are two (different) arbitrarily-nested conjunctions of
the same set of terms, then CONJUNCTS_AC (t1,t2) returns
|- t1 = t2. Otherwise, it fails.
Fails if t1 and t2 are not equivalent, as
described above.
- CONJUNCTS_AC (Term `(P /\ Q) /\ R`, Term `R /\ (Q /\ R) /\ P`);
> val it = |- (P /\ Q) /\ R = R /\ (Q /\ R) /\ P : thmUsed to reorder a conjunction. First sort the conjuncts in a term
t1 into the desired order (e.g., lexicographic order, for
normalization) to get a new term t2, then call
CONJUNCTS_AC(t1,t2).