DNF_ss : ssfrag
STRUCTURE
SYNOPSIS
A simpset fragment that does aggressive propositional and quantifier normalisation.
DESCRIPTION
Adding the DNF_ss simpset fragment to a simpset augments it with rewrites that make the simplifier normalise “towards” disjunctive normal form. This normalisation at the propositional level does leave implications alone (rather than convert them to disjunctions). DNF_ss also includes normalisations pertaining to quantifiers. The complete list of rewrites is
   |- !P Q. (!x. P x /\ Q x) <=> (!x. P x) /\ !x. Q x
   |- !P Q. (?x. P x \/ Q x) <=> (?x. P x) \/ ?x. Q x
   |- !P Q R. P \/ Q ==> R <=> (P ==> R) /\ (Q ==> R)
   |- !P Q R. P ==> Q /\ R <=> (P ==> Q) /\ (P ==> R)
   |- !A B C. (B \/ C) /\ A <=> B /\ A \/ C /\ A
   |- !A B C. A /\ (B \/ C) <=> A /\ B \/ A /\ C
   |- !P Q. (?x. P x) ==> Q <=> !x. P x ==> Q
   |- !P Q. P ==> (!x. Q x) <=> !x. P ==> Q x
   |- !P Q. (?x. P x) /\ Q <=> ?x. P x /\ Q
   |- !P Q. P /\ (?x. Q x) <=> ?x. P /\ Q x
FAILURE
As a value rather than a function, DNF_ss can’t fail.
EXAMPLE
> SIMP_CONV (bool_ss ++ DNF_ss) []
            ``!x. (?y. P x y) /\ Q z ==> R1 x z /\ R2 z x``;
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
val it =
   |- (!x. (?y. P x y) /\ Q z ==> R1 x z /\ R2 z x) <=>
        (!x y. P x y /\ Q z ==> R1 x z) /\
        !x y. P x y /\ Q z ==> R2 z x : thm
COMMENTS
The DNF_ss fragment interacts well with the one-point elimination rules for equalities under quantifiers (provided in bool_ss and its descendants).
SEEALSO
HOL  Kananaskis-13