Converts a term already in negation normal form into conjunctive normal form.
DESCRIPTION
When applied to a term already in negation normal form (see NNF_CONV),
meaning that all other propositional connectives have been eliminated in favour
of conjunction, disjunction and negation, and negation is only applied to
atomic formulas, WEAK_CNF_CONV puts the term into an equivalent conjunctive
normal form, which is a conjunction of disjunctions.
FAILURE CONDITIONS
Never fails; non-Boolean terms will just yield a reflexive theorem.
EXAMPLE
# WEAK_CNF_CONV `(a /\ b) \/ (a /\ b /\ c) \/ d`;;
val it : thm =
|- a /\ b \/ a /\ b /\ c \/ d <=>
((a \/ a \/ d) /\ (b \/ a \/ d)) /\
((a \/ b \/ d) /\ (b \/ b \/ d)) /\
(a \/ c \/ d) /\
(b \/ c \/ d)
COMMENTS
The ordering and associativity of the resulting form are not guaranteed, and it
may contain duplicates. See CNF_CONV for a stronger (but somewhat slower)
variant where this is important.