%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% storetp-lemmas.elf

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing WF Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sttp!wf_tail   : sttp_wf (cons_sttp L T ST') -> sttp_wf ST' -> type.
%mode sttp!wf_tail +DSTWf -DSTWf'.
-cons_nil      : sttp!wf_tail (sttp_wf_cons_nil) sttp_wf_nil.
-cons_cons     : sttp!wf_tail (sttp_wf_cons_cons DSTWf' _) DSTWf'.
%terminates {} (sttp!wf_tail _ _).
%worlds () (sttp!wf_tail _ _).
%covers sttp!wf_tail +DSTWf -DSTWf'.
%total {} (sttp!wf_tail _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing Alloc Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sttp!alloc_preserves_wf  
               : sttp_wf ST1 -> sttp_alloc ST1 T ST2 L -> sttp_wf ST2 -> type.
%mode sttp!alloc_preserves_wf +DSTWf1 +DSttpAlloc -DSTWf2.
-nil           : sttp!alloc_preserves_wf (sttp_wf_nil)
                                         (sttp_alloc_nil)
                                         (sttp_wf_cons_nil).
-cons          : sttp!alloc_preserves_wf DSTWf
                                         (sttp_alloc_cons)
                                         (sttp_wf_cons_cons DSTWf (loc_lt_ DNatLt))
		 <- nat!N_lt_sN _ DNatLt.
%terminates DSttpAlloc (sttp!alloc_preserves_wf _ DSttpAlloc _).
%worlds () (sttp!alloc_preserves_wf _ _ _).
%covers sttp!alloc_preserves_wf +DSTWf1 +DSttpAlloc -DSttpWf2.
%total DSttpAlloc (sttp!alloc_preserves_wf _ DSttpAlloc _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing Extend Lemmas
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sttp!extend_refl
               : {ST:sttp} sttp_extend ST ST -> type.
%mode sttp!extend_refl +ST -DSttpExtend.
-nil           : sttp!extend_refl nil_sttp 
                                  (sttp_extend_nil).
-cons          : sttp!extend_refl (cons_sttp L T ST') 
		                  (sttp_extend_cons_hit DSttpExtend')
		  <- sttp!extend_refl ST' DSttpExtend'.
%terminates ST (sttp!extend_refl ST _).
%worlds () (sttp!extend_refl _ _).
%covers sttp!extend_refl +ST -DSttpExtend.
%total ST (sttp!extend_refl ST _).

sttp!extend_trans
               : sttp_extend ST1 ST2 ->
		 sttp_extend ST2 ST3 
                  -> sttp_extend ST1 ST3 -> type.
%mode sttp!extend_trans +DSttpExtend12 +DSttpExtend23 -DSttpExtend13.
-nil__*        : sttp!extend_trans (sttp_extend_nil)
                                   _
                                   (sttp_extend_nil).
-cons_hit__cons_hit
               : sttp!extend_trans (sttp_extend_cons_hit DSttpExtend1'2')
                                   (sttp_extend_cons_hit DSttpExtend2'3')
                                   (sttp_extend_cons_hit DSttpExtend1'3')
		  <- sttp!extend_trans DSttpExtend1'2' DSttpExtend2'3' DSttpExtend1'3'.
-cons_miss__cons_hit
               : sttp!extend_trans (sttp_extend_cons_miss DSttpExtend12' DLocLt)
                                   (sttp_extend_cons_hit DSttpExtend2'3')
                                   (sttp_extend_cons_miss DSttpExtend13' DLocLt)
		  <- sttp!extend_trans DSttpExtend12' DSttpExtend2'3' DSttpExtend13'.
-cons_hit__cons_miss
               : sttp!extend_trans (sttp_extend_cons_hit DSttpExtend1'2')
                                   (sttp_extend_cons_miss DSttpExtend23' DLocLt)
                                   (sttp_extend_cons_miss DSttpExtend13' DLocLt)
		  <- sttp!extend_trans (sttp_extend_cons_hit DSttpExtend1'2')
                                       DSttpExtend23' 
                                       DSttpExtend13'.
-cons_miss__cons_miss
               : sttp!extend_trans (sttp_extend_cons_miss DSttpExtend12' DLocLt)
                                   (sttp_extend_cons_miss DSttpExtend23' DLocLt')
                                   (sttp_extend_cons_miss DSttpExtend13' DLocLt'')
		  <- sttp!extend_trans (sttp_extend_cons_miss DSttpExtend12' DLocLt)
                                       DSttpExtend23'
                                       DSttpExtend13'
		  <- loc!lt_trans DLocLt DLocLt' DLocLt''.
%terminates DSttpExtend23 (sttp!extend_trans _ DSttpExtend23 _).
%worlds () (sttp!extend_trans _ _ _).
%covers sttp!extend_trans +DSttpExtend12 +DSttpExtend23 -DSttpExtend13.
%total DSttpExtend23 (sttp!extend_trans _ DSttpExtend23 _).

%%% Store typing allocation yields an extension of the original store typing.
sttp!alloc_implies_extend
               : sttp_alloc ST T ST' _
		  -> sttp_extend ST ST' -> type.
%mode sttp!alloc_implies_extend +DStAlloc -DSttpExtend.
-nil           : sttp!alloc_implies_extend (sttp_alloc_nil)
                                           (sttp_extend_nil).
-cons          : sttp!alloc_implies_extend (sttp_alloc_cons)
                                           (sttp_extend_cons_miss DSttpExtend 
				                                  (loc_lt_ DNatLt))
		  <- sttp!extend_refl _ DSttpExtend
		  <- nat!N_lt_sN _ DNatLt.
%terminates DStAlloc (sttp!alloc_implies_extend DStAlloc _).
%worlds () (sttp!alloc_implies_extend _ _).
%covers sttp!alloc_implies_extend +DStAlloc -DStExtend.
%total DStAlloc (sttp!alloc_implies_extend DStAlloc _).

%%% A well-formed, non-empty store typing is an extension of its tail.
sttp!wf_cons_implies_extend_cons 
               : sttp_wf (cons_sttp L T ST')
		  -> sttp_extend ST' (cons_sttp L T ST') -> type.
%mode sttp!wf_cons_implies_extend_cons +DSTWf -DSttpExtend.
-nil           : sttp!wf_cons_implies_extend_cons (sttp_wf_cons_nil)
                                                  (sttp_extend_nil).
-cons          : sttp!wf_cons_implies_extend_cons (sttp_wf_cons_cons _ DLocLt)
                                                  (sttp_extend_cons_miss DSttpExtend 
                                                                         DLocLt)
		  <- sttp!extend_refl _ DSttpExtend.
%terminates {} (sttp!wf_cons_implies_extend_cons _ _).
%worlds () (sttp!wf_cons_implies_extend_cons _ _).
%covers sttp!wf_cons_implies_extend_cons +DSTWf -DSttpExtend.
%total {} (sttp!wf_cons_implies_extend_cons _ _).