Subst = TypedMeta +

(* Condition for a single substitution to be possible. *)

constdefs oksubst :: "nat => nat => ('a,'b) env => bool"
"oksubst x i G == ((x ~= i) & (x < length G) & \ 
\ (i < length G) & (canaddtypetoenv G x (typeof i G)))"

(* substenv x i G  is the environment resulting from substituting x
for i in G. Precondition is  oksubst x i G. *)

constdefs substenv :: "nat => nat => ('a,'b) env => ('a,'b) env"
"substenv x i G == rem i (addtypetoenv G x (typeof i G))"

(* Condition for a substitution to be possible. *)

consts oksb :: "(nat list) * nat * (('a,'b) env) => bool"
recdef oksb "measure (%(xs,i,G). size xs)"
"oksb ([],i,G)     = True"
"oksb ((x#xs),i,G) = ((oksubst x i G) & \ 
\                     (oksb (map (newpos i) xs, i, substenv x i G)))" 

constdefs oksub :: "nat list => nat => ('a,'b) env => bool"
"oksub xs i G == oksb(xs,i,G)"

(* subenv xs i G  is the environment resulting from substituting xs
for consecutive variables from i onwards in G. Precondition is  
oksub xs i G. *)

consts sbenv :: "(nat list) * nat * (('a,'b) env) => ('a,'b) env"
recdef sbenv "measure (%(xs,i,G). size xs)"
"sbenv ([],i,G)   = G"
"sbenv (x#xs,i,G) = sbenv (map (newpos i) xs, i, (substenv x i G))"

constdefs subenv :: "nat list => nat => ('a,'b) env => ('a,'b) env"
"subenv xs i G == sbenv (xs,i,G)"

end