FDL > PVS > Prelude > quantifier_props : Theory

PVS-2.4 prelude.pvs

 quantifier_props defines some useful properties of quantifiers.  Note
 that these work well with the higher-order matching facility of the prover.

quantifier_props [t:TYPE] : THEORY
BEGIN

x: VAR t

p: VAR [t- > bool]

q: VAR [t- > bool]

not exists: LEMMA (EXISTS x : p(x)) = (NOT (FORALL x : NOT p(x)))

exists not: LEMMA (EXISTS x : NOT p(x)) = (NOT (FORALL x : p(x)))

exists or: LEMMA (EXISTS x : p(x) OR q(x)) = ((EXISTS x : p(x)) OR (EXISTS x : q(x)))

exists implies: LEMMA (EXISTS x : p(x) IMPLIES q(x)) = ((EXISTS x : NOT p(x)) OR (EXISTS x : q(x)))

exists and: LEMMA (EXISTS x : p(x) AND q(x)) IMPLIES ((EXISTS x : p(x)) AND (EXISTS x : q(x)))

not forall: LEMMA (FORALL x : p(x)) = (NOT (EXISTS x : NOT p(x)))

forall not: LEMMA (FORALL x : NOT p(x)) = (NOT (EXISTS x : p(x)))

forall and: LEMMA (FORALL x : p(x) AND q(x)) = ((FORALL x : p(x)) AND (FORALL x : q(x)))

forall or: LEMMA ((FORALL x : p(x)) OR (FORALL x : q(x))) IMPLIES (FORALL x : p(x) OR q(x))

END quantifier_props