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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Weaken Store Typing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% sttp_lookup
%theorem
sttp_weak_sttp_lookup_thm :
          forall* {ST1:sttp} {L:loc} {T:tp} {ST2:sttp}
          forall {DSttpLookup: sttp_lookup ST1 L T}
                 {DSttpExtend: sttp_extend ST1 ST2}
          exists {DSttpLookup': sttp_lookup ST2 L T}
          true.
%prove 4 DSttpExtend (sttp_weak_sttp_lookup_thm _ DSttpExtend _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% |-loc
%theorem
sttp_weak_|-loc_thm :
          forall* {ST1:sttp} {L:loc} {T:tp} {ST2:sttp}
          forall {DLocTc: |-loc ST1 L T}
                 {DSttpExtend: sttp_extend ST1 ST2}
          exists {DLocTc': |-loc ST2 L T}
          true.
%prove 3 {} (sttp_weak_|-loc_thm _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% |-exp
%theorem
sttp_weak_|-exp_thm :
          forallG (some {T:tp} pi {x:exp} {DVarTcX: |-var x T})
          forall* {ST1:sttp} {E:exp} {T:tp} {ST2:sttp}
          forall {DExpTc: |-exp ST1 E T}
                 {DSttpExtend: sttp_extend ST1 ST2}
          exists {DExpTc': |-exp ST2 E T}
          true.
%prove 3 DExpTc (sttp_weak_|-exp_thm DExpTc _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% |-val
%theorem
sttp_weak_|-val_thm :
          forallG (some {T:tp} pi {x:exp} {DVarTcX: |-var x T})
          forall* {ST1:sttp} {V:val} {T:tp} {ST2:sttp}
          forall {DValTc: |-val ST1 V T}
                 {DSttpExtend: sttp_extend ST1 ST2}
          exists {DValTc': |-val ST2 V T}
          true.
%% %prove 4 {} (sttp_weak_|-val_thm _ _ _).