TypedMeta = Meta + TypedEnv + (* Typed meta terms. *) types ('a,'b,'c) mtic = "(('a,'b) env) * ('c meta)" consts TYPEDMETA :: "('a,'b,'c) mtic set" inductive TYPEDMETA intrs conI "unlimited G ==> (G , mCon c) : TYPEDMETA" NLvarI "[| unlimited G ; x < length G ; canaddtypetoenv G x (NLinV t) ; \ \ index v = x ; tag v = Both ; \ \ H = addtypetoenv G x (NLinV t) |] ==> \ \ (H , mVar v) : TYPEDMETA" LPvarI "[| unlimited G ; x < length G ; canaddtypetoenv G x (LinV t) ; \ \ index v = x ; tag v = Pos ; pos t = One u ; neg t = Zero ; \ \ H = addtypetoenv G x (LinV t) |] ==> \ \ (H , mVar v) : TYPEDMETA" LNvarI "[| unlimited G ; x < length G ; canaddtypetoenv G x (LinV t) ; \ \ index v = x ; tag v = Neg ; pos t = Zero ; neg t = One u ; \ \ H = addtypetoenv G x (LinV t) |] ==> \ \ (H , mVar v) : TYPEDMETA" absI "(t # G , p) : TYPEDMETA ==> (G , mAbs p) : TYPEDMETA" appI "[| (G , p) : TYPEDMETA ; (H , q) : TYPEDMETA ; canaddenv G H ; \ \ I = addenv G H |] ==> \ \ (I , mApp p q) : TYPEDMETA" constdefs tvocc :: "('a,'b) vty => tag => bool" "tvocc t v == \ \ (case t of \ \ LinV x => (case v of \ \ Pos => ((? u. pos x = One u) & neg x = Zero) \ \ | Neg => (pos x = Zero & (? u. neg x = One u)) \ \ | Both => False) \ \ | NLinV x => (v = Both))" consts tvoccs :: "('a,'b) vty list => tag list => bool" primrec "tvoccs [] ts = (ts = [])" "tvoccs (v#vs) ts = \ \ (case ts of \ \ [] => False \ \ | (x#xs) => (tvocc v x & tvoccs vs xs))" end