th_D: THEORY

%%%
%%% In addition to commands seen in the previous exercises, commands dealing
%%% with arithmetic reasoning are used below.  In particular, LEMMA, EXPAND,
%%% REPLACE, SIMPLIFY are enough to finish all these proofs.
%%%

BEGIN

m, n: VAR int

%%%
%%% Here is one way to introduce a new predicate.
%%% Give it a name and axiomatize its properties.
%%%

even_predicate: [int -> bool]
defn_even_predicate: AXIOM even_predicate(n) IFF (EXISTS m: n = 2 * m)

%%%
%%% Or we may give a definition.
%%%

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

%%%
%%% PVS knows about 0, but...
%%%
D_0: PROPOSITION even_predicate(0)
D_1a: PROPOSITION even?(0)
D_1b: PROPOSITION even?(42)

%%%
%%% The predicate formulation is more primitive and
%%% harder to work with, but is used in some cases
%%%

D_2x: PROPOSITION FORALL n: even_predicate(n) IMPLIES even_predicate(n + n)

%%%
%%% It is usually preferable to work with the functional
%%% form, if you can.

D_2: PROPOSITION FORALL n: even?(n) IMPLIES even?(n + n)
D_3: PROPOSITION FORALL n: odd?(n) IMPLIES even?(n + n)
D_4: PROPOSITION FORALL n: even?(n + n)

%%%
%%% In theorems, universal quantification is implicit
%%%

D_5: PROPOSITION even?(n) IMPLIES even?(n * n)
D_6: PROPOSITION odd?(n) IMPLIES odd?(n * n)
D_7: PROPOSITION even?(n) AND even?(m) IMPLIES even?(n + m)

%%%
%%% You can declare variables locally
%%%

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

D_9: PROPOSITION odd?(n) AND even?(m) IMPLIES odd?(n + m)
D_10: PROPOSITION odd?(n) AND odd?(m) IMPLIES odd?(n * m)
D_11: PROPOSITION even?(n) IMPLIES even?(n + n)

%%%
%%% Bonus problem, you are not required to prove it, but you
%%% might want to try it.
%%%

D_12: THEOREM not even?(n) IMPLIES odd?(n)

END th_D