Env = Main + Tactics +
(* Type of a variable in an environment *)

constdefs typeof :: "nat => 'a list => 'a"
"typeof x G == G!x"

(* Types of a list of variables in an environment *)

constdefs typesof :: "nat list => 'a list => 'a list"
"typesof xs G == map (%x. typeof x G) xs"

(* Predicates expressing desired bounds on lists of variables. *)

consts allless :: "nat list => nat => bool"
primrec
"allless [] n     = True"
"allless (x#xs) n = ((x<n) & (allless xs n))"

consts allgreater :: "nat list => nat => bool"
primrec
"allgreater []     n = True"
"allgreater (x#xs) n = ((n < x) & (allgreater xs n))" 

consts allgreatereq :: "nat list => nat => bool"
primrec
"allgreatereq []     n = True"
"allgreatereq (x#xs) n = ((n <= x) & (allgreatereq xs n))"

(* Insertion of types into an environment. This goes with lifting. 
ins ts n G  is the environment obtained from G by inserting the
list ts at position n (so that in the new environment, ts starts at
position n.) *)

consts ins :: "'a list => nat => 'a list => 'a list"
primrec
"ins ts 0       G = ts @ G"
"ins ts (Suc n) G = (hd G) # (ins ts n (tl G))"

(* Removal of types from an environment.

remove m n G  is the environment obtained from G by removing m entries
from position n onwards. Precondition is that m + n <= length G.

rem n G  is the environment obtained from G by removing entry
n. Precondition is that n < length G. *)

consts rem :: "nat => 'a list => 'a list"
primrec
"rem 0       G = tl G"
"rem (Suc n) G = (hd G) # (rem n (tl G))" 

consts remove :: "nat => nat => 'a list => 'a list"
primrec
"remove 0       n G = G"
"remove (Suc m) n G = remove m n (rem n G)"

(* Adjustment of position of variables in an environment. 

newpos i v  is the new position of variable v when variable i is
removed from the environment. Precondition is that v ~= i. *)

constdefs newpos :: "nat => nat => nat"
"newpos i v == (if v < i then v else v - 1)"

(* Subenvironment.

midenv m n G  consists of n elements of G from position m
onwards. Precondition is that m + n <= length G. *)

constdefs midenv :: "nat => nat => 'a list => 'a list"
"midenv m n G == take n (drop m G)"

end