Meta = Env +

(* de Bruijn terms. *)

(* Tags for occurrences of variables. Tag Both
will be used for occurrences of nonlinear variables. *)

datatype tag = Pos | Neg | Both 

record var = 
  index :: nat
  tag :: tag

(* 'a is the type of constants. *)

datatype 'a meta =
  mCon 'a                             (* constant *)
| mVar var                            (* variable *)
| mAbs ('a meta)                      (* abstraction *)
| mApp ('a meta) ('a meta)            (* application *)

(* Substitution. *)

(* substvar v x i  is the result (as a variable position) of substituting
x for i on variable v. Precondition is that x ~= i and v ~= i. *)

constdefs substvar :: "nat => nat => nat => nat"
"substvar v x i == (if v = i then newpos i x \ 
\                   else newpos i v)"

constdefs substv :: "var => nat => nat => var"
"substv v x i == v (| index := substvar (index v) x i |)"

(* mSUBST t x i   is the term obtained from t by substituting the
variable x for the variable i. Precondition is that x ~= i. *)

consts mSUBST :: "('a meta) => nat => nat => ('a meta)"
  ("_[_'/'/_]" [1000,0,0] 1000)
primrec
"mSUBST (mCon c)   x i = mCon c"
"mSUBST (mVar v)   x i = mVar (substv v x i)"
"mSUBST (mAbs t)   x i = mAbs (mSUBST t (Suc x) (Suc i))"
"mSUBST (mApp t u) x i = mApp (mSUBST t x i) (mSUBST u x i)"

(* SUB t xs  substitutes the variables xs for the consecutive variables
from position 0 onwards. *)

consts sub :: "('a meta) * (nat list) => 'a meta"
recdef sub "measure (%(t,xs). size xs)"
"sub (t,[])     = t"
"sub (t,(x#xs)) = sub (t[x//0],(map (newpos 0) xs))"

constdefs SUB :: "('a meta) => nat list => ('a meta)"
"SUB t xs == sub (t,xs)"

(* n-ary abstraction. *)

consts mABS :: "nat => ('a meta) => ('a meta)"
primrec
"mABS 0       t = t"
"mABS (Suc n) t = mAbs (mABS n t)"

(* n-ary application. t is applied to the terms in the list in reverse
order; this does not matter, as it is not really application, just
collecting together. *)

consts mAPP :: "('a meta) => ('a meta list) => ('a meta)"
primrec
"mAPP t []     = t"
"mAPP t (u#us) = mApp (mAPP t us) u" 

(* Lifting. lift i n t  is the term obtained from t by adding n to all 
free variable references from position i onwards. *)

constdefs liftvar :: "nat => nat => nat => nat"
"liftvar i n v == (if v<i then v else v+n)"

constdefs liftv :: "nat => nat => var => var"
"liftv i n v == v (| index := liftvar i n (index v) |)"

consts lift :: "nat => nat => ('a meta) => ('a meta)"
primrec
lift_mCon "lift i n (mCon c)   = mCon c"
lift_mVar "lift i n (mVar v)   = mVar (liftv i n v)"
lift_mAbs "lift i n (mAbs t)   = mAbs (lift (Suc i) n t)"
lift_mApp "lift i n (mApp t u) = mApp (lift i n t) (lift i n u)"

end