%%%%%%
% Assignment: PVS exercises; Deadline: Dec, 7th, 2007.
%%%%%%


simple : THEORY

BEGIN
p,q,r: bool	% Proposition names

arb: TYPE+
arb_pred: TYPE = [arb -> bool]
a,b,c: arb
x,y,z: VAR arb                    % Variables of type arb
P,Q,R: arb_pred

%%% Questions %%%

%%% Section 1: %%%
% Use the typecheck command M-x tc. Correct the following mistakes
%%%

% error_1: LEMMA (P AND q) => (p and q)
% error_2: LEMMA ((not p => q) => r


%% Section 2: 
% Prove all of the following using only flatten and split.
%%%

section2_1: LEMMA (( p=>q ) AND p) => q

section2_2: LEMMA ((p AND q) AND r) => (p AND (q AND r))	  

section2_3: LEMMA  (p => (q => r)) IFF (p AND q => r)

section2_4: LEMMA  (p AND (q OR r)) IFF (p AND q) OR (p AND r)

section2_5: LEMMA  (p OR (q AND r)) IFF (p OR q) AND (p OR r)

section2_6: LEMMA  ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))

section2_7: LEMMA ((p AND q) AND ((p => r) OR (q => r))) => r

section2_8: LEMMA ((NOT p => q) AND (NOT q => NOT p) AND (q => p)) => (p AND q)

%%%
% Section 3: 
% Prove using only flatten, split, skolem and inst
% Do NOT use (skosimp*) or (inst?). You can use previously proven lemmas, 
%i.e. if you have a proof of quant_0 you can use it for quant_3. Using 
%lemmas unnecesarily complicates your proof. 
%%%

quant_0: LEMMA  (FORALL x: P(x)) => P(a)

quant_1: LEMMA  ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a)

quant_2: LEMMA  (FORALL x: P(x)) => (EXISTS y: P(y))

quant_3: LEMMA  (FORALL x: P(x)) OR (EXISTS y: NOT P(y))

quant_4: LEMMA  NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x))

quant_5: LEMMA  NOT (EXISTS x: P(x)) IFF (FORALL x: NOT P(x))

quant_6: LEMMA  (FORALL x: P(x)) AND (FORALL x: Q(x))
                  IFF (FORALL x: P(x) AND Q(x))

quant_7: LEMMA  (EXISTS x: P(x)) OR (EXISTS x: Q(x))
                  IFF (EXISTS x: P(x) OR Q(x))

quant_8: LEMMA  ((FORALL x: P(x) OR Q(x)) AND (EXISTS x: NOT Q(x))) => EXISTS x: P(x) 

END simple