th_D: THEORY

%%%
%%% In addition to commands seen in the previous exercises, commands dealing
%%% with arithmetic reasoning are used below.  In addition to the logical
%%% rules PROP (SPLIT/FLATTEN), SKOLEM, and INST, the arithmetic
%%% rules EXPAND, REPLACE, and SIMPLIFY are enough to finish all these proofs.
%%%

BEGIN

m, n: VAR int

%%%
%%% Predicate Function Definitions
%%% even?, odd?: int -> bool
%%%

even?(n):bool = EXISTS m: n = 2 * m
odd?(n):bool = EXISTS m: n = 2 * m + 1

%%%
%%% PVS knows about 0, but...
%%%

 D_1: PROPOSITION even?(0)
 D_2: PROPOSITION even?(42)
 D_3: PROPOSITION odd?(55)
 
 D_4: PROPOSITION even?(n) IMPLIES odd?(n+1)
 D_5: PROPOSITION odd?(n) IMPLIES even?(n+1)

%%%
%%% In theorems, universal quantification is implicit.  For instance,
%%% Proposition D_3 says,
%%%    "For all n and m, even?(n) AND even?(m) IMPLIES even?(n+m)"
%%%     ~~~~~~~~~~~~~~~~
%%%

 D_6: PROPOSITION even?(n) AND even?(m) IMPLIES even?(n + m)
 D_7: PROPOSITION FORALL (k,l: int): odd?(k) AND odd?(l) IMPLIES even?(k + l)
 D_8: PROPOSITION odd?(n) AND even?(m) IMPLIES odd?(n + m)

 D_9: PROPOSITION even?(n) IMPLIES even?(n * n)
D_10: PROPOSITION odd?(n) IMPLIES odd?(n * n)

END th_D