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

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

%theorem
sttp!wf_tail_thm : 
          forall* {L:loc} {T:tp} {ST':sttp}
          forall {DSTWf: sttp_wf (cons_sttp L T ST')}
          exists {DSTWf': sttp_wf ST'}
          true.
%prove 2 {} (sttp!wf_tail_thm _ _).

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

%theorem
sttp!alloc_preserves_wf_thm :
          forall* {ST1:sttp} {T:tp} {ST2:sttp} {L:loc}
          forall {DSTWf1: sttp_wf ST1}
                 {DSttpAlloc: sttp_alloc ST1 T ST2 L}
          exists {DSTWf2: sttp_wf ST2}
          true.
%prove 4 DSttpAlloc (sttp!alloc_preserves_wf_thm _ DSttpAlloc _).

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

%theorem
sttp!extend_refl_thm :
          forall {ST:sttp}
          exists {DSttpExtend: sttp_extend ST ST}
          true.
%prove 2 ST (sttp!extend_refl_thm ST _).

%theorem
sttp!extend_trans_thm :
          forall* {ST1:sttp} {ST2:sttp} {ST3:sttp}
          forall {DSttpExtend12: sttp_extend ST1 ST2}
                 {DSttpExtend23: sttp_extend ST2 ST3}
          exists {DSttpExtend13: sttp_extend ST1 ST3}
          true.
%prove 4 DSttpExtend23 (sttp!extend_trans_thm _ DSttpExtend23 _).

%%% Store typing allocation yields an extension of the original store typing.
%theorem
sttp!alloc_implies_extend_thm :
          forall* {ST:sttp} {T:tp} {ST':sttp} {L:loc}
          forall {DStAlloc: sttp_alloc ST T ST' L}
          exists {DSttpExtend: sttp_extend ST ST'}
          true.
%prove 4 DStAlloc (sttp!alloc_implies_extend_thm DStAlloc _).

%%% A well-formed, non-empty store typing is an extension of its tail.
%theorem
sttp!wf_cons_implies_extend_cons_thm :
          forall* {L:loc} {T:tp} {ST':sttp}
          forall {DSTWf: sttp_wf (cons_sttp L T ST')}
          exists {DSttpExtend: sttp_extend ST' (cons_sttp L T ST')}
          true.
%prove 2 {} (sttp!wf_cons_implies_extend_cons_thm _ _).