----------------------------------------------------------------------
DNF_ss                                                     (boolSimps)
----------------------------------------------------------------------
DNF_ss : ssfrag

SYNOPSIS
A simpset fragment that does aggressive propositional and quantifier
normalisation.

KEYWORDS
Simplification, normalisation, quantifiers.

DESCRIBE
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
boolSimps.bool_ss, simpLib.SIMP_CONV.

----------------------------------------------------------------------