FDL > PVS > Prelude > boolean_props : Theory

PVS-2.4 prelude.pvs

 boolean_props provides lemmas about the boolean constants and
 connectives.  The lemmas define them in terms of IF-THEN-ELSE, though
 these lemmas should never be needed since the prover "knows" the
 connectives as primitives.  WHEN is a special case - it is translated to
 IMPLIES with the arguments reversed by the typechecker.

boolean_props : THEORY
BEGIN

A: VAR bool

B: VAR bool

bool exclusive: POSTULATE NOT (FALSE = TRUE)

bool inclusive: POSTULATE (A = FALSE) OR (A = TRUE)

not def: POSTULATE (NOT A) = IF A THEN FALSE ELSE TRUE ENDIF

and def: POSTULATE (A AND B) = IF A THEN B ELSE FALSE ENDIF

syand def: POSTULATE & = AND

or def: POSTULATE (A OR B) = IF A THEN TRUE ELSE B ENDIF

implies def: POSTULATE (A IMPLIES B) = IF A THEN B ELSE TRUE ENDIF

syimplies def: POSTULATE = > = IMPLIES

when def: POSTULATE infix"WHEN"(A, B) = (B IMPLIES A)

iff def: POSTULATE (A IFF B) = ((A AND B) OR ((NOT A) AND (NOT B)))

syiff def: POSTULATE < = > = IFF

excluded middle: LEMMA A OR (NOT A)

END boolean_props