(* generated by Ott 0.10.14 from: common.ott common_index.ott common_labels.ott common_typing.ott bool.ott bool_typing.ott nat.ott nat_typing.ott arrow_typing.ott basety.ott unit.ott seq.ott ascribe.ott let.ott product.ott sum.ott fix.ott tuple.ott variant.ott *)
(* to compile: Holmake stlcTheory.uo   *)
(* for interactive use:
  app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"];
*)

open HolKernel boolLib Parse bossLib ottLib;
infix THEN THENC |-> ## ;
local open arithmeticTheory stringTheory containerTheory pred_setTheory listTheory 
  finite_mapTheory in end;

val _ = new_theory "stlc";

(** syntax *)
val _ = type_abbrev("index", ``:num``);
val _ = type_abbrev("label", ``:string``);
val _ = type_abbrev("termvar", ``:string``);
val _ = type_abbrev("basetype", ``:string``);
val _ = Hol_datatype ` 
Typ = 
   TyBool
 | TyNat
 | TyArr of Typ => Typ
 | TyId of basetype
 | TyUnit
 | TyPair of Typ => Typ
 | TySum of Typ => Typ
 | TyTuple of Typ list
 | TyVariant of (label#Typ) list
`;
val _ = Hol_datatype ` 
C = 
   CCase of label => termvar => t
;
t = 
   TmTrue
 | TmFalse
 | TmIf of t => t => t
 | TmZero
 | TmSucc of t
 | TmPred of t
 | TmIszero of t
 | TmVar of termvar
 | TmAbs of termvar => Typ => t
 | TmApp of t => t
 | TmUnit
 | TmSeq of t => t
 | TmAscribe of t => Typ
 | TmLet of termvar => t => t
 | TmPair of t => t
 | TmProj1 of t
 | TmProj2 of t
 | TmInl of t
 | TmInr of t
 | TmCaseSm of t => termvar => t => termvar => t
 | TmFix of t
 | TmTuple of t list
 | TmProjTp of t => index
 | TmVariant of label => t => Typ
 | TmCase of t => C list
`;
val _ = type_abbrev("G", ``:(termvar#Typ) list``);
val _ = Hol_datatype ` 
labels = 
   labels_seq of label list
`;


(** subrules *)
val _ = ottDefine "is_v_of_t" `
    ( is_v_of_t TmTrue = (T))
/\  ( is_v_of_t TmFalse = (T))
/\  ( is_v_of_t (TmIf t1 t2 t3) = F)
/\  ( is_v_of_t TmZero = (T))
/\  ( is_v_of_t (TmSucc t) = ((is_v_of_t t)))
/\  ( is_v_of_t (TmPred t) = F)
/\  ( is_v_of_t (TmIszero t) = F)
/\  ( is_v_of_t (TmVar x) = F)
/\  ( is_v_of_t (TmAbs x Typ t) = (T))
/\  ( is_v_of_t (TmApp t1 t2) = F)
/\  ( is_v_of_t TmUnit = (T))
/\  ( is_v_of_t (TmSeq t1 t2) = F)
/\  ( is_v_of_t (TmAscribe t Typ) = F)
/\  ( is_v_of_t (TmLet x t t') = F)
/\  ( is_v_of_t (TmPair t1 t2) = ((is_v_of_t t1) /\ (is_v_of_t t2)))
/\  ( is_v_of_t (TmProj1 t) = F)
/\  ( is_v_of_t (TmProj2 t) = F)
/\  ( is_v_of_t (TmInl t) = ((is_v_of_t t)))
/\  ( is_v_of_t (TmInr t) = ((is_v_of_t t)))
/\  ( is_v_of_t (TmCaseSm t x1 t1 x2 t2) = F)
/\  ( is_v_of_t (TmFix t) = F)
/\  ( is_v_of_t (TmTuple (t_list)) = ((EVERY (\t_. (is_v_of_t t_)) t_list)))
/\  ( is_v_of_t (TmProjTp t i) = F)
/\  ( is_v_of_t (TmVariant l t Typ) = ((is_v_of_t t)))
/\  ( is_v_of_t (TmCase t (C_list)) = F)
`;

(** free variables *)
val _ = ottDefine "fv_C" `
    ( fv_C (CCase l x t) = (list_minus (fv_t t) [x]))
/\  ( fv_t TmTrue = [])
/\  ( fv_t TmFalse = [])
/\  ( fv_t (TmIf t1 t2 t3) = (fv_t t1) ++ (fv_t t2) ++ (fv_t t3))
/\  ( fv_t TmZero = [])
/\  ( fv_t (TmSucc t) = (fv_t t))
/\  ( fv_t (TmPred t) = (fv_t t))
/\  ( fv_t (TmIszero t) = (fv_t t))
/\  ( fv_t (TmVar x) = [x])
/\  ( fv_t (TmAbs x Typ t) = (list_minus (fv_t t) [x]))
/\  ( fv_t (TmApp t1 t2) = (fv_t t1) ++ (fv_t t2))
/\  ( fv_t TmUnit = [])
/\  ( fv_t (TmSeq t1 t2) = (fv_t t1) ++ (fv_t t2))
/\  ( fv_t (TmAscribe t Typ) = (fv_t t))
/\  ( fv_t (TmLet x t t') = (fv_t t) ++ (list_minus (fv_t t') [x]))
/\  ( fv_t (TmPair t1 t2) = (fv_t t1) ++ (fv_t t2))
/\  ( fv_t (TmProj1 t) = (fv_t t))
/\  ( fv_t (TmProj2 t) = (fv_t t))
/\  ( fv_t (TmInl t) = (fv_t t))
/\  ( fv_t (TmInr t) = (fv_t t))
/\  ( fv_t (TmCaseSm t x1 t1 x2 t2) = (fv_t t) ++ (list_minus (fv_t t1) [x1]) ++ (list_minus (fv_t t2) [x2]))
/\  ( fv_t (TmFix t) = (fv_t t))
/\  ( fv_t (TmTuple (t_list)) = (FLAT (MAP (\t_. (fv_t t_)) t_list)))
/\  ( fv_t (TmProjTp t i) = (fv_t t))
/\  ( fv_t (TmVariant l t Typ) = (fv_t t))
/\  ( fv_t (TmCase t (C_list)) = (fv_t t) ++ (FLAT (MAP (\C_. (fv_C C_)) C_list)))
`;

(** substitutions *)
val _ = ottDefine "subst_C" `
    ( subst_C t5 x5 (CCase l x t) = CCase l x (if MEM x5 [x] then t else (subst_t t5 x5 t)))
/\  ( subst_t t_5 x_5 TmTrue = TmTrue )
/\  ( subst_t t_5 x_5 TmFalse = TmFalse )
/\  ( subst_t t_5 x_5 (TmIf t1 t2 t3) = TmIf (subst_t t_5 x_5 t1) (subst_t t_5 x_5 t2) (subst_t t_5 x_5 t3))
/\  ( subst_t t_5 x_5 TmZero = TmZero )
/\  ( subst_t t_5 x_5 (TmSucc t) = TmSucc (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmPred t) = TmPred (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmIszero t) = TmIszero (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmVar x) = (if x=x_5 then t_5 else (TmVar x)))
/\  ( subst_t t_5 x_5 (TmAbs x Typ t) = TmAbs x Typ (if MEM x_5 [x] then t else (subst_t t_5 x_5 t)))
/\  ( subst_t t_5 x_5 (TmApp t1 t2) = TmApp (subst_t t_5 x_5 t1) (subst_t t_5 x_5 t2))
/\  ( subst_t t_5 x_5 TmUnit = TmUnit )
/\  ( subst_t t_5 x_5 (TmSeq t1 t2) = TmSeq (subst_t t_5 x_5 t1) (subst_t t_5 x_5 t2))
/\  ( subst_t t_5 x_5 (TmAscribe t Typ) = TmAscribe (subst_t t_5 x_5 t) Typ)
/\  ( subst_t t_5 x_5 (TmLet x t t') = TmLet x (subst_t t_5 x_5 t) (if MEM x_5 [x] then t' else (subst_t t_5 x_5 t')))
/\  ( subst_t t_5 x_5 (TmPair t1 t2) = TmPair (subst_t t_5 x_5 t1) (subst_t t_5 x_5 t2))
/\  ( subst_t t_5 x_5 (TmProj1 t) = TmProj1 (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmProj2 t) = TmProj2 (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmInl t) = TmInl (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmInr t) = TmInr (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmCaseSm t x1 t1 x2 t2) = TmCaseSm (subst_t t_5 x_5 t) x1 (if MEM x_5 [x1] then t1 else (subst_t t_5 x_5 t1)) x2 (if MEM x_5 [x2] then t2 else (subst_t t_5 x_5 t2)))
/\  ( subst_t t_5 x_5 (TmFix t) = TmFix (subst_t t_5 x_5 t))
/\  ( subst_t t_5 x_5 (TmTuple (t_list)) = TmTuple (MAP (\t_. (subst_t t_5 x_5 t_)) t_list))
/\  ( subst_t t_5 x_5 (TmProjTp t i) = TmProjTp (subst_t t_5 x_5 t) i)
/\  ( subst_t t_5 x_5 (TmVariant l t Typ) = TmVariant l (subst_t t_5 x_5 t) Typ)
/\  ( subst_t t_5 x_5 (TmCase t (C_list)) = TmCase (subst_t t_5 x_5 t) (MAP (\C_. (subst_C t_5 x_5 C_)) C_list))
`;

(** definitions *)
(* defns Jop *)

val (Jop_rules, Jop_ind, Jop_cases) = Hol_reln `
(* defn red *)

( (* E_IfTrue *)  !(t2:t) (t3:t) . (clause_name "E_IfTrue") ==> 
( ( red (TmIf TmTrue t2 t3) t2 )))

/\ ( (* E_IfFalse *)  !(t2:t) (t3:t) . (clause_name "E_IfFalse") ==> 
( ( red (TmIf TmFalse t2 t3) t3 )))

/\ ( (* E_If *)  !(t1:t) (t2:t) (t3:t) (t1':t) . (clause_name "E_If") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmIf t1 t2 t3) (TmIf t1' t2 t3) )))

/\ ( (* E_Succ *)  !(t1:t) (t1':t) . (clause_name "E_Succ") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmSucc t1) (TmSucc t1') )))

/\ ( (* E_PredZero *)  (clause_name "E_PredZero") ==> 
( ( red (TmPred TmZero) TmZero )))

/\ ( (* E_PredSucc *)  !(v1:t) . (clause_name "E_PredSucc") /\
((is_v_of_t v1))
 ==> 
( ( red (TmPred  (TmSucc v1) ) v1 )))

/\ ( (* E_Pred *)  !(t1:t) (t1':t) . (clause_name "E_Pred") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmPred t1) (TmPred t1') )))

/\ ( (* E_IsZeroZero *)  (clause_name "E_IsZeroZero") ==> 
( ( red (TmIszero TmZero) TmTrue )))

/\ ( (* E_IsZeroSucc *)  !(v1:t) . (clause_name "E_IsZeroSucc") /\
((is_v_of_t v1))
 ==> 
( ( red (TmIszero  (TmSucc v1) ) TmFalse )))

/\ ( (* E_IsZero *)  !(t1:t) (t1':t) . (clause_name "E_IsZero") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmIszero t1) (TmIszero t1') )))

/\ ( (* E_App1 *)  !(t1:t) (t2:t) (t1':t) . (clause_name "E_App1") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmApp t1 t2) (TmApp t1' t2) )))

/\ ( (* E_App2 *)  !(v1:t) (t2:t) (t2':t) . (clause_name "E_App2") /\
((is_v_of_t v1) /\
( ( red t2 t2' )))
 ==> 
( ( red (TmApp v1 t2) (TmApp v1 t2') )))

/\ ( (* E_AppAbs *)  !(x:termvar) (Typ:Typ) (t12:t) (v2:t) . (clause_name "E_AppAbs") /\
((is_v_of_t v2))
 ==> 
( ( red (TmApp  (TmAbs x Typ t12)  v2)  (subst_t  v2   x   t12 )  )))

/\ ( (* E_Seq *)  !(t1:t) (t2:t) (t1':t) . (clause_name "E_Seq") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmSeq t1 t2) (TmSeq t1' t2) )))

/\ ( (* E_SeqNext *)  !(t2:t) . (clause_name "E_SeqNext") ==> 
( ( red (TmSeq TmUnit t2) t2 )))

/\ ( (* E_Ascribe *)  !(v1:t) (Typ:Typ) . (clause_name "E_Ascribe") /\
((is_v_of_t v1))
 ==> 
( ( red (TmAscribe v1 Typ) v1 )))

/\ ( (* E_Ascribe1 *)  !(t1:t) (Typ:Typ) (t1':t) . (clause_name "E_Ascribe1") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmAscribe t1 Typ) (TmAscribe t1' Typ) )))

/\ ( (* E_LetV *)  !(x:termvar) (v1:t) (t2:t) . (clause_name "E_LetV") /\
((is_v_of_t v1))
 ==> 
( ( red (TmLet x v1 t2)  (subst_t  v1   x   t2 )  )))

/\ ( (* E_Let *)  !(x:termvar) (t1:t) (t2:t) (t1':t) . (clause_name "E_Let") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmLet x t1 t2) (TmLet x t1' t2) )))

/\ ( (* E_PairBeta1 *)  !(v1:t) (v2:t) . (clause_name "E_PairBeta1") /\
((is_v_of_t v1) /\
(is_v_of_t v2))
 ==> 
( ( red (TmProj1 (TmPair v1 v2)) v1 )))

/\ ( (* E_PairBeta2 *)  !(v1:t) (v2:t) . (clause_name "E_PairBeta2") /\
((is_v_of_t v1) /\
(is_v_of_t v2))
 ==> 
( ( red (TmProj2 (TmPair v1 v2)) v2 )))

/\ ( (* E_Proj1 *)  !(t1:t) (t1':t) . (clause_name "E_Proj1") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmProj1 t1) (TmProj1 t1') )))

/\ ( (* E_Proj2 *)  !(t1:t) (t1':t) . (clause_name "E_Proj2") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmProj2 t1) (TmProj2 t1') )))

/\ ( (* E_Pair1 *)  !(t1:t) (t2:t) (t1':t) . (clause_name "E_Pair1") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmPair t1 t2) (TmPair t1' t2) )))

/\ ( (* E_Pair2 *)  !(v1:t) (t2:t) (t2':t) . (clause_name "E_Pair2") /\
((is_v_of_t v1) /\
( ( red t2 t2' )))
 ==> 
( ( red (TmPair v1 t2) (TmPair v1 t2') )))

/\ ( (* E_CaseInl *)  !(v0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) . (clause_name "E_CaseInl") /\
((is_v_of_t v0))
 ==> 
( ( red (TmCaseSm  (TmInl v0)  x1 t1 x2 t2)  (subst_t  v0   x1   t1 )  )))

/\ ( (* E_CaseInr *)  !(v0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) . (clause_name "E_CaseInr") /\
((is_v_of_t v0))
 ==> 
( ( red (TmCaseSm  (TmInr v0)  x1 t1 x2 t2)  (subst_t  v0   x2   t2 )  )))

/\ ( (* E_CaseSm *)  !(t0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) (t0':t) . (clause_name "E_CaseSm") /\
(( ( red t0 t0' )))
 ==> 
( ( red (TmCaseSm t0 x1 t1 x2 t2) (TmCaseSm t0' x1 t1 x2 t2) )))

/\ ( (* E_Inl *)  !(t1:t) (t1':t) . (clause_name "E_Inl") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmInl t1) (TmInl t1') )))

/\ ( (* E_Inr *)  !(t1:t) (t1':t) . (clause_name "E_Inr") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmInr t1) (TmInr t1') )))

/\ ( (* E_FixBeta *)  !(x:termvar) (Typ1:Typ) (t2:t) . (clause_name "E_FixBeta") ==> 
( ( red (TmFix  (TmAbs x Typ1 t2) )  (subst_t   (TmFix  (TmAbs x Typ1 t2) )    x   t2 )  )))

/\ ( (* E_Fix *)  !(t1:t) (t1':t) . (clause_name "E_Fix") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmFix t1) (TmFix t1') )))

/\ ( (* E_ProjTuple *)  !(v_list:t list) (j:index) . (clause_name "E_ProjTuple") /\
((EVERY (\v_. is_v_of_t v_) v_list) /\
( (1 <=  j  /\  j  <= LENGTH  (v_list) ) ))
 ==> 
( ( red (TmProjTp (TmTuple (v_list)) j)  ((\ v_ . v_) (EL  (j - 1) v_list))  )))

/\ ( (* E_ProjTp *)  !(t1:t) (i:index) (t1':t) . (clause_name "E_ProjTp") /\
(( ( red t1 t1' )))
 ==> 
( ( red (TmProjTp t1 i) (TmProjTp t1' i) )))

/\ ( (* E_Tuple *)  !(t_list:t list) (v_list:t list) (t:t) (t':t) . (clause_name "E_Tuple") /\
((EVERY (\v_. is_v_of_t v_) v_list) /\
( ( red t t' )))
 ==> 
( ( red (TmTuple (v_list ++ [(t)] ++ t_list)) (TmTuple (v_list ++ [(t')] ++ t_list)) )))

/\ ( (* E_CaseVariant *)  !(l_x_t_list:(label#termvar#t) list) (v:t) (Typ:Typ) (j:index) . (clause_name "E_CaseVariant") /\
((is_v_of_t v) /\
( (1 <=  j  /\  j  <= LENGTH  ((MAP (\(l_,x_,t_) . t_) l_x_t_list)) ) ))
 ==> 
( ( red (TmCase  (TmVariant  ((\ (l_,x_,t_) . l_) (EL  (j - 1) l_x_t_list))  v Typ)  ((MAP (\(l_,x_,t_) . (CCase l_ x_ t_)) l_x_t_list)))  (subst_t  v    ((\ (l_,x_,t_) . x_) (EL  (j - 1) l_x_t_list))     ((\ (l_,x_,t_) . t_) (EL  (j - 1) l_x_t_list))  )  )))

/\ ( (* E_Case *)  !(l_x_t_list:(label#termvar#t) list) (t:t) (t':t) . (clause_name "E_Case") /\
(( ( red t t' )))
 ==> 
( ( red (TmCase t ((MAP (\(l_,x_,t_) . (CCase l_ x_ t_)) l_x_t_list))) (TmCase t' ((MAP (\(l_,x_,t_) . (CCase l_ x_ t_)) l_x_t_list))) )))

/\ ( (* E_Variant *)  !(li:label) (ti:t) (Typ:Typ) (ti':t) . (clause_name "E_Variant") /\
(( ( red ti ti' )))
 ==> 
( ( red (TmVariant li ti Typ) (TmVariant li ti' Typ) )))

`;

(* defns Jtype *)

val (Jtype_rules, Jtype_ind, Jtype_cases) = Hol_reln `
(* defn typing *)

( (* T_True *)  !(G:G) . (clause_name "T_True") ==> 
( ( typing G TmTrue TyBool )))

/\ ( (* T_False *)  !(G:G) . (clause_name "T_False") ==> 
( ( typing G TmFalse TyBool )))

/\ ( (* T_If *)  !(G:G) (t1:t) (t2:t) (t3:t) (Typ:Typ) . (clause_name "T_If") /\
(( ( typing G t1 TyBool )) /\
( ( typing G t2 Typ )) /\
( ( typing G t3 Typ )))
 ==> 
( ( typing G (TmIf t1 t2 t3) Typ )))

/\ ( (* T_Zero *)  !(G:G) . (clause_name "T_Zero") ==> 
( ( typing G TmZero TyNat )))

/\ ( (* T_Succ *)  !(G:G) (t1:t) . (clause_name "T_Succ") /\
(( ( typing G t1 TyNat )))
 ==> 
( ( typing G (TmSucc t1) TyNat )))

/\ ( (* T_Pred *)  !(G:G) (t1:t) . (clause_name "T_Pred") /\
(( ( typing G t1 TyNat )))
 ==> 
( ( typing G (TmPred t1) TyNat )))

/\ ( (* T_IsZero *)  !(G:G) (t1:t) . (clause_name "T_IsZero") /\
(( ( typing G t1 TyNat )))
 ==> 
( ( typing G (TmIszero t1) TyBool )))

/\ ( (* T_Var *)  !(G:G) (x:termvar) (Typ:Typ) . (clause_name "T_Var") /\
(( ? G1 G2. ( G  = G1 ++ ( x , Typ )::G2) /\ ~(MEM  x  (MAP FST G1)) ))
 ==> 
( ( typing G (TmVar x) Typ )))

/\ ( (* T_Abs *)  !(G:G) (x:termvar) (Typ1:Typ) (t2:t) (Typ2:Typ) . (clause_name "T_Abs") /\
(( ( typing  (( x , Typ1 ):: G )  t2 Typ2 )))
 ==> 
( ( typing G (TmAbs x Typ1 t2) (TyArr Typ1 Typ2) )))

/\ ( (* T_App *)  !(G:G) (t1:t) (t2:t) (Typ12:Typ) (Typ11:Typ) . (clause_name "T_App") /\
(( ( typing G t1 (TyArr Typ11 Typ12) )) /\
( ( typing G t2 Typ11 )))
 ==> 
( ( typing G (TmApp t1 t2) Typ12 )))

/\ ( (* T_Unit *)  !(G:G) . (clause_name "T_Unit") ==> 
( ( typing G TmUnit TyUnit )))

/\ ( (* T_Seq *)  !(G:G) (t1:t) (t2:t) (Typ2:Typ) . (clause_name "T_Seq") /\
(( ( typing G t1 TyUnit )) /\
( ( typing G t2 Typ2 )))
 ==> 
( ( typing G (TmSeq t1 t2) Typ2 )))

/\ ( (* T_Ascribe *)  !(G:G) (t1:t) (Typ:Typ) . (clause_name "T_Ascribe") /\
(( ( typing G t1 Typ )))
 ==> 
( ( typing G (TmAscribe t1 Typ) Typ )))

/\ ( (* T_Let *)  !(G:G) (x:termvar) (t1:t) (t2:t) (Typ2:Typ) (Typ1:Typ) . (clause_name "T_Let") /\
(( ( typing G t1 Typ1 )) /\
( ( typing  (( x , Typ1 ):: G )  t2 Typ2 )))
 ==> 
( ( typing G (TmLet x t1 t2) Typ2 )))

/\ ( (* T_Pair *)  !(G:G) (t1:t) (t2:t) (Typ1:Typ) (Typ2:Typ) . (clause_name "T_Pair") /\
(( ( typing G t1 Typ1 )) /\
( ( typing G t2 Typ2 )))
 ==> 
( ( typing G (TmPair t1 t2) (TyPair Typ1 Typ2) )))

/\ ( (* T_Proj1 *)  !(G:G) (t1:t) (Typ1:Typ) (Typ2:Typ) . (clause_name "T_Proj1") /\
(( ( typing G t1 (TyPair Typ1 Typ2) )))
 ==> 
( ( typing G (TmProj1 t1) Typ1 )))

/\ ( (* T_Proj2 *)  !(G:G) (t1:t) (Typ2:Typ) (Typ1:Typ) . (clause_name "T_Proj2") /\
(( ( typing G t1 (TyPair Typ1 Typ2) )))
 ==> 
( ( typing G (TmProj2 t1) Typ2 )))

/\ ( (* T_Inl *)  !(G:G) (t1:t) (Typ1:Typ) (Typ2:Typ) . (clause_name "T_Inl") /\
(( ( typing G t1 Typ1 )))
 ==> 
( ( typing G (TmInl t1) (TySum Typ1 Typ2) )))

/\ ( (* T_Inr *)  !(G:G) (t1:t) (Typ1:Typ) (Typ2:Typ) . (clause_name "T_Inr") /\
(( ( typing G t1 Typ2 )))
 ==> 
( ( typing G (TmInr t1) (TySum Typ1 Typ2) )))

/\ ( (* T_CaseSm *)  !(G:G) (t0:t) (x1:termvar) (t1:t) (x2:termvar) (t2:t) (Typ:Typ) (Typ1:Typ) (Typ2:Typ) . (clause_name "T_CaseSm") /\
(( ( typing G t0 (TySum Typ1 Typ2) )) /\
( ( typing  (( x1 , Typ1 ):: G )  t1 Typ )) /\
( ( typing  (( x2 , Typ2 ):: G )  t2 Typ )))
 ==> 
( ( typing G (TmCaseSm t0 x1 t1 x2 t2) Typ )))

/\ ( (* T_Fix *)  !(G:G) (t1:t) (Typ1:Typ) . (clause_name "T_Fix") /\
(( ( typing G t1 (TyArr Typ1 Typ1) )))
 ==> 
( ( typing G (TmFix t1) Typ1 )))

/\ ( (* T_Tuple *)  !(t_Typ_list:(t#Typ) list) (G:G) . (clause_name "T_Tuple") /\
(((EVERY (\ b . b) ((MAP (\(t_,Typ_) .  ( typing G t_ Typ_ )) t_Typ_list)))))
 ==> 
( ( typing G (TmTuple ((MAP (\(t_,Typ_) . t_) t_Typ_list))) (TyTuple ((MAP (\(t_,Typ_) . Typ_) t_Typ_list))) )))

/\ ( (* T_ProjTp *)  !(Typ_list:Typ list) (G:G) (t1:t) (j:index) . (clause_name "T_ProjTp") /\
(( ( typing G t1 (TyTuple (Typ_list)) )) /\
( (1 <=  j  /\  j  <= LENGTH  (Typ_list) ) ))
 ==> 
( ( typing G (TmProjTp t1 j)  ((\ Typ_ . Typ_) (EL  (j - 1) Typ_list))  )))

/\ ( (* T_Variant *)  !(l_Typ_list:(label#Typ) list) (G:G) (t:t) (j:index) . (clause_name "T_Variant") /\
(( ( typing G t  ((\ (l_,Typ_) . Typ_) (EL  (j - 1) l_Typ_list))  )) /\
( (1 <=  j  /\  j  <= LENGTH  ((MAP (\(l_,Typ_) . Typ_) l_Typ_list)) ) ))
 ==> 
( ( typing G (TmVariant  ((\ (l_,Typ_) . l_) (EL  (j - 1) l_Typ_list))  t (TyVariant (l_Typ_list))) (TyVariant (l_Typ_list)) )))

/\ ( (* T_Case *)  !(l_x_t_Typ_list:(label#termvar#t#Typ) list) (G:G) (t:t) (Typ:Typ) . (clause_name "T_Case") /\
(( ( typing G t (TyVariant ((MAP (\(l_,x_,t_,Typ_) . (l_,Typ_)) l_x_t_Typ_list))) )) /\
((EVERY (\ b . b) ((MAP (\(l_,x_,t_,Typ_) .  ( typing  (( x_ , Typ_ ):: G )  t_ Typ )) l_x_t_Typ_list)))) /\
( (ALL_DISTINCT  ((MAP (\(l_,x_,t_,Typ_) . l_) l_x_t_Typ_list)) ) ))
 ==> 
( ( typing G (TmCase t ((MAP (\(l_,x_,t_,Typ_) . (CCase l_ x_ t_)) l_x_t_Typ_list))) Typ )))

`;


val _ = export_theory ();