%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Proofs for subtyping relations.
%%
%% Author: Fernando Magno Quintao Pereira, 03-26-2007
%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If G <= G' and G'[r] = p then G[r] = p

subRegLemma : sub (CodeTp G) (CodeTp G')
	-> proj_exp G' Nr (psd Np)
	-> not_zero Np
	-> proj_exp G Nr (psd Np)
	-> type.

%mode subRegLemma +SUB +G +NZ -G'.

subRegLemma_zz : subRegLemma (sub_rnotz SUB) proj_exp_z NZ proj_exp_z.

subRegLemma_sz : subRegLemma (sub_rnotz SUB) (proj_exp_s PG) NZ (proj_exp_s PG')
	<- subRegLemma SUB PG NZ PG'.

subRegLemma_ss : subRegLemma (sub_rzero SUB) (proj_exp_s PG) NZ (proj_exp_s PG')
	<- subRegLemma SUB PG NZ PG'.

%worlds () (subRegLemma _ _ _ _).
%total SUB (subRegLemma SUB _ _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% If S <= T and T <= R, then S <= R

subTransLemma : sub S T -> sub T R -> sub S R -> type.

%mode subTransLemma +ST +TR -SR.

subTransLemma_zzz : subTransLemma sub_empbk sub_empbk sub_empbk.

subTransLemma_nzz : subTransLemma (sub_rzero ST) (sub_rzero TR) (sub_rzero SR)
	<- subTransLemma ST TR SR.

subTransLemma_nnz : subTransLemma (sub_rnotz ST) (sub_rzero TR) (sub_rzero SR)
	<- subTransLemma ST TR SR.

subTransLemma_nnn : subTransLemma (sub_rnotz ST) (sub_rnotz TR) (sub_rnotz SR)
	<- subTransLemma ST TR SR.

%worlds () (subTransLemma _ _ _).
%total SUB (subTransLemma SUB _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The proof that the bank of registers can be updated if its supertype can.

subUpdtLemma : sub (CodeTp G) (CodeTp G')
	-> update_exp G' (psd Np) Nr GU' Y'
	-> update_exp G  (psd Np) Nr GU  Y
	-> type.

%mode subUpdtLemma +SUB +UG -UG'.

subUpdtLemma_nz : subUpdtLemma (sub_rnotz SUB) update_exp_z update_exp_z.

subUpdtLemma_zz : subUpdtLemma (sub_rzero SUB) update_exp_z update_exp_z.

subUpdtLemma_sz : subUpdtLemma (sub_rzero SUB) (update_exp_s UG) (update_exp_s UG')
	<- subUpdtLemma SUB UG UG'.

subUpdtLemma_sn : subUpdtLemma (sub_rnotz SUB) (update_exp_s UG) (update_exp_s UG')
	<- subUpdtLemma SUB UG UG'.

%worlds () (subUpdtLemma  _ _ _).
%total SUB (subUpdtLemma  SUB _ _).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The proof that the bank of registers can be updated if its supertype can.

subUpdtSubLemma : sub (CodeTp G) (CodeTp G')
        -> update_exp G' (psd Np) Nr GU' Y'
        -> update_exp G  (psd Np) Nr GU  Y
	-> not_zero Np
        -> sub (CodeTp GU) (CodeTp GU')
        -> type.

%mode subUpdtSubLemma +SUB +UG +UG' +NZ -SUB'.

subUpdtSubLemma_nz : subUpdtSubLemma (sub_rnotz SUB) update_exp_z update_exp_z NZ (sub_rnotz SUB).

subUpdtSubLemma_zz : subUpdtSubLemma (sub_rzero SUB) update_exp_z update_exp_z NZ (sub_rnotz SUB).

subUpdtSubLemma_sz : subUpdtSubLemma (sub_rzero SUB) (update_exp_s UG) (update_exp_s UG') NZ (sub_rzero SUB')
	<- subUpdtSubLemma SUB UG UG' NZ SUB'.

subUpdtSubLemma_sn : subUpdtSubLemma (sub_rnotz SUB) (update_exp_s UG) (update_exp_s UG') NZ (sub_rnotz SUB')
	<- subUpdtSubLemma SUB UG UG' NZ SUB'.

%worlds () (subUpdtSubLemma _ _ _ _ _).
%total SUB (subUpdtSubLemma SUB _ _ _ _).