(* generated by Ott 0.10.5 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 *)
theory stlc imports Main Multiset begin

(** syntax *)
types index = "nat"
types label = "string"
types termvar = "string"
types basetype = "string"
datatype 
T = 
   TyBool  
 | TyNat  
 | TyArr "T" "T"  
 | TyId "basetype"  
 | TyUnit  
 | TyPair "T" "T"  
 | TySum "T" "T"  
 | TyTuple "T list"  
 | TyVariant "(label*T) list"  

datatype 
C = 
   CCase "label" "termvar" "t"  
and t = 
   TmTrue  
 | TmFalse  
 | TmIf "t" "t" "t"  
 | TmZero  
 | TmSucc "t"  
 | TmPred "t"  
 | TmIszero "t"  
 | TmVar "termvar"  
 | TmAbs "termvar" "T" "t"  
 | TmApp "t" "t"  
 | TmUnit  
 | TmSeq "t" "t"  
 | TmAscribe "t" "T"  
 | TmLet "termvar" "t" "t"  
 | TmPair "t" "t"  
 | TmProj1 "t"  
 | TmProj2 "t"  
 | TmInl "t"  
 | TmInr "t"  
 | TmCaseSm "t" "termvar" "t" "termvar" "t"  
 | TmFix "t"  
 | TmTuple "t list"  
 | TmProjTp "t" "index"  
 | TmVariant "label" "t" "T"  
 | TmCase "t" "C list"  

types G = "(termvar*T) list"
datatype 
ott_bug_workaround__ = 
   ott_bug_workaround__missing_list_label "label list"  



(** library functions *)
lemma [mono]:"
         (!! x. f x --> g x) ==> list_all (%b. b) (map f foo_list)-->
                    list_all (%b. b) (map g foo_list) "
   apply(induct_tac foo_list, auto) done

lemma [mono]: "split f p = f (fst p) (snd p)" by (simp add: split_def)
consts
list_minus :: "'a list => 'a list => 'a list"

primrec
"list_minus Nil ys = Nil"
"list_minus (Cons x xs) ys = (if Not(x : set ys) then Cons x (list_minus xs ys) else list_minus xs ys)"


(** subrules *)
consts
is_v_of_t_list :: "t list => bool"
is_v_of_t :: "t => bool"
primrec
"is_v_of_t_list Nil = (True)"
"is_v_of_t_list (t_#t_list_) = ((is_v_of_t t_) & (is_v_of_t_list t_list_))"
"is_v_of_t TmTrue = ((True))"
"is_v_of_t TmFalse = ((True))"
"is_v_of_t (TmIf t1 t2 t3) = (False)"
"is_v_of_t TmZero = ((True))"
"is_v_of_t (TmSucc t) = (((is_v_of_t t)))"
"is_v_of_t (TmPred t) = (False)"
"is_v_of_t (TmIszero t) = (False)"
"is_v_of_t (TmVar x) = (False)"
"is_v_of_t (TmAbs x T t) = ((True))"
"is_v_of_t (TmApp t1 t2) = (False)"
"is_v_of_t TmUnit = ((True))"
"is_v_of_t (TmSeq t1 t2) = (False)"
"is_v_of_t (TmAscribe t T) = (False)"
"is_v_of_t (TmLet x t t') = (False)"
"is_v_of_t (TmPair t1 t2) = (((is_v_of_t t1) & (is_v_of_t t2)))"
"is_v_of_t (TmProj1 t) = (False)"
"is_v_of_t (TmProj2 t) = (False)"
"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) = (False)"
"is_v_of_t (TmFix t) = (False)"
"is_v_of_t (TmTuple (t_list)) = ((is_v_of_t_list t_list))"
"is_v_of_t (TmProjTp t i) = (False)"
"is_v_of_t (TmVariant l t T) = (((is_v_of_t t)))"
"is_v_of_t (TmCase t (C_list)) = (False)"


(** free variables *)
consts
fv_C :: "C => termvar list"
fv_C_list :: "C list => termvar list"
fv_t_list :: "t list => termvar list"
fv_t :: "t => termvar list"
primrec
"fv_C (CCase l x t) = ((list_minus (fv_t t) [x]))"
"fv_C_list Nil = ([])"
"fv_C_list (C_#C_list_) = ((fv_C C_) @ (fv_C_list C_list_))"
"fv_t_list Nil = ([])"
"fv_t_list (t_#t_list_) = ((fv_t t_) @ (fv_t_list t_list_))"
"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 T 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 T) = ((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)) = ((fv_t_list t_list))"
"fv_t (TmProjTp t i) = ((fv_t t))"
"fv_t (TmVariant l t T) = ((fv_t t))"
"fv_t (TmCase t (C_list)) = ((fv_t t) @ (fv_C_list C_list))"


(** substitutions *)
consts
subst_C :: "t => termvar => C => C"
subst_C_list :: "t => termvar => C list => C list"
subst_t_list :: "t => termvar => t list => t list"
subst_t :: "t => termvar => t => t"
primrec
"subst_C t5 x5 (CCase l x t) = (CCase l x (if x5 mem [x] then t else (subst_t t5 x5 t)))"
"subst_C_list t_5 x_5 Nil = (Nil)"
"subst_C_list t_5 x_5 (C_#C_list_) = ((subst_C t_5 x_5 C_) # (subst_C_list t_5 x_5 C_list_))"
"subst_t_list t_5 x_5 Nil = (Nil)"
"subst_t_list t_5 x_5 (t_#t_list_) = ((subst_t t_5 x_5 t_) # (subst_t_list t_5 x_5 t_list_))"
"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 T t) = (TmAbs x T (if x_5 mem [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 T) = (TmAscribe (subst_t t_5 x_5 t) T)"
"subst_t t_5 x_5 (TmLet x t t') = (TmLet x (subst_t t_5 x_5 t) (if x_5 mem [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 x_5 mem [x1] then t1 else (subst_t t_5 x_5 t1)) x2 (if x_5 mem [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 (subst_t_list t_5 x_5 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 T) = (TmVariant l (subst_t t_5 x_5 t) T)"
"subst_t t_5 x_5 (TmCase t (C_list)) = (TmCase (subst_t t_5 x_5 t) (subst_C_list t_5 x_5 C_list))"


(** definitions *)
(*defns Jop *)
consts
  red :: "(t*t) set"

inductive red
intros

(* defn red *)

E_IfTrueI: " ( (TmIf TmTrue t2 t3) , t2 ) : red"

E_IfFalseI: " ( (TmIf TmFalse t2 t3) , t3 ) : red"

E_IfI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmIf t1 t2 t3) , (TmIf t1' t2 t3) ) : red"

E_SuccI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmSucc t1) , (TmSucc t1') ) : red"

E_PredZeroI: " ( (TmPred TmZero) , TmZero ) : red"

E_PredSuccI: "[|is_v_of_t v1|] ==> 
 ( (TmPred  (TmSucc v1) ) , v1 ) : red"

E_PredI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmPred t1) , (TmPred t1') ) : red"

E_IsZeroZeroI: " ( (TmIszero TmZero) , TmTrue ) : red"

E_IsZeroSuccI: "[|is_v_of_t v1|] ==> 
 ( (TmIszero  (TmSucc v1) ) , TmFalse ) : red"

E_IsZeroI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmIszero t1) , (TmIszero t1') ) : red"

E_App1I: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmApp t1 t2) , (TmApp t1' t2) ) : red"

E_App2I: "[|is_v_of_t v1 ;
 ( t2 , t2' ) : red|] ==> 
 ( (TmApp v1 t2) , (TmApp v1 t2') ) : red"

E_AppAbsI: "[|is_v_of_t v2|] ==> 
 ( (TmApp  (TmAbs x T t12)  v2) ,  (subst_t  v2   x   t12 )  ) : red"

E_SeqI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmSeq t1 t2) , (TmSeq t1' t2) ) : red"

E_SeqNextI: " ( (TmSeq TmUnit t2) , t2 ) : red"

E_AscribeI: "[|is_v_of_t v1|] ==> 
 ( (TmAscribe v1 T) , v1 ) : red"

E_Ascribe1I: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmAscribe t1 T) , (TmAscribe t1' T) ) : red"

E_LetVI: "[|is_v_of_t v1|] ==> 
 ( (TmLet x v1 t2) ,  (subst_t  v1   x   t2 )  ) : red"

E_LetI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmLet x t1 t2) , (TmLet x t1' t2) ) : red"

E_PairBeta1I: "[|is_v_of_t v1 ;
is_v_of_t v2|] ==> 
 ( (TmProj1 (TmPair v1 v2)) , v1 ) : red"

E_PairBeta2I: "[|is_v_of_t v1 ;
is_v_of_t v2|] ==> 
 ( (TmProj2 (TmPair v1 v2)) , v2 ) : red"

E_Proj1I: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmProj1 t1) , (TmProj1 t1') ) : red"

E_Proj2I: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmProj2 t1) , (TmProj2 t1') ) : red"

E_Pair1I: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmPair t1 t2) , (TmPair t1' t2) ) : red"

E_Pair2I: "[|is_v_of_t v1 ;
 ( t2 , t2' ) : red|] ==> 
 ( (TmPair v1 t2) , (TmPair v1 t2') ) : red"

E_CaseInlI: "[|is_v_of_t v0|] ==> 
 ( (TmCaseSm  (TmInl v0)  x1 t1 x2 t2) ,  (subst_t  v0   x1   t1 )  ) : red"

E_CaseInrI: "[|is_v_of_t v0|] ==> 
 ( (TmCaseSm  (TmInr v0)  x1 t1 x2 t2) ,  (subst_t  v0   x2   t2 )  ) : red"

E_CaseSmI: "[| ( t0 , t0' ) : red|] ==> 
 ( (TmCaseSm t0 x1 t1 x2 t2) , (TmCaseSm t0' x1 t1 x2 t2) ) : red"

E_InlI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmInl t1) , (TmInl t1') ) : red"

E_InrI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmInr t1) , (TmInr t1') ) : red"

E_FixBetaI: " ( (TmFix  (TmAbs x T1 t2) ) ,  (subst_t   (TmFix  (TmAbs x T1 t2) )    x   t2 )  ) : red"

E_FixI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmFix t1) , (TmFix t1') ) : red"

E_ProjTupleI: "[|List.list_all (%v_. is_v_of_t v_) v_list ;
 (1 <=  j  &  j  <= length  (v_list) ) |] ==> 
 ( (TmProjTp (TmTuple (v_list)) j) , ((%v_ . v_) (List.nth v_list (j - 1))) ) : red"

E_ProjTpI: "[| ( t1 , t1' ) : red|] ==> 
 ( (TmProjTp t1 i) , (TmProjTp t1' i) ) : red"

E_TupleI: "[|List.list_all (%v_. is_v_of_t v_) v_list ;
 ( t , t' ) : red|] ==> 
 ( (TmTuple (v_list @ [(t)] @ t_list)) , (TmTuple (v_list @ [(t')] @ t_list)) ) : red"

E_CaseVariantI: "[|is_v_of_t v ;
 (1 <=  j  &  j  <= length  ((List.map (%(l_,x_,t_).t_) l_x_t_list)) ) |] ==> 
 ( (TmCase  (TmVariant ((%(l_,x_,t_) . l_) (List.nth l_x_t_list (j - 1))) v T)  ((List.map (%(l_,x_,t_).(CCase l_ x_ t_)) l_x_t_list))) ,  (subst_t  v   ((%(l_,x_,t_) . x_) (List.nth l_x_t_list (j - 1)))   ((%(l_,x_,t_) . t_) (List.nth l_x_t_list (j - 1))) )  ) : red"

E_CaseI: "[| ( t , t' ) : red|] ==> 
 ( (TmCase t ((List.map (%(l_,x_,t_).(CCase l_ x_ t_)) l_x_t_list))) , (TmCase t' ((List.map (%(l_,x_,t_).(CCase l_ x_ t_)) l_x_t_list))) ) : red"

E_VariantI: "[| ( ti , ti' ) : red|] ==> 
 ( (TmVariant li ti T) , (TmVariant li ti' T) ) : red"

(*defns Jtype *)
consts
  typing :: "(G*t*T) set"

inductive typing
intros

(* defn typing *)

T_TrueI: " ( G , TmTrue , TyBool ) : typing"

T_FalseI: " ( G , TmFalse , TyBool ) : typing"

T_IfI: "[| ( G , t1 , TyBool ) : typing ;
 ( G , t2 , T ) : typing ;
 ( G , t3 , T ) : typing|] ==> 
 ( G , (TmIf t1 t2 t3) , T ) : typing"

T_ZeroI: " ( G , TmZero , TyNat ) : typing"

T_SuccI: "[| ( G , t1 , TyNat ) : typing|] ==> 
 ( G , (TmSucc t1) , TyNat ) : typing"

T_PredI: "[| ( G , t1 , TyNat ) : typing|] ==> 
 ( G , (TmPred t1) , TyNat ) : typing"

T_IsZeroI: "[| ( G , t1 , TyNat ) : typing|] ==> 
 ( G , (TmIszero t1) , TyBool ) : typing"

T_VarI: "[| ? G1 G2.  G  = G1 @ ( x , T )#G2 &  x ~:fst ` set G1 |] ==> 
 ( G , (TmVar x) , T ) : typing"

T_AbsI: "[| (  ( x , T1 )# G  , t2 , T2 ) : typing|] ==> 
 ( G , (TmAbs x T1 t2) , (TyArr T1 T2) ) : typing"

T_AppI: "[| ( G , t1 , (TyArr T11 T12) ) : typing ;
 ( G , t2 , T11 ) : typing|] ==> 
 ( G , (TmApp t1 t2) , T12 ) : typing"

T_UnitI: " ( G , TmUnit , TyUnit ) : typing"

T_SeqI: "[| ( G , t1 , TyUnit ) : typing ;
 ( G , t2 , T2 ) : typing|] ==> 
 ( G , (TmSeq t1 t2) , T2 ) : typing"

T_AscribeI: "[| ( G , t1 , T ) : typing|] ==> 
 ( G , (TmAscribe t1 T) , T ) : typing"

T_LetI: "[| ( G , t1 , T1 ) : typing ;
 (  ( x , T1 )# G  , t2 , T2 ) : typing|] ==> 
 ( G , (TmLet x t1 t2) , T2 ) : typing"

T_PairI: "[| ( G , t1 , T1 ) : typing ;
 ( G , t2 , T2 ) : typing|] ==> 
 ( G , (TmPair t1 t2) , (TyPair T1 T2) ) : typing"

T_Proj1I: "[| ( G , t1 , (TyPair T1 T2) ) : typing|] ==> 
 ( G , (TmProj1 t1) , T1 ) : typing"

T_Proj2I: "[| ( G , t1 , (TyPair T1 T2) ) : typing|] ==> 
 ( G , (TmProj2 t1) , T2 ) : typing"

T_InlI: "[| ( G , t1 , T1 ) : typing|] ==> 
 ( G , (TmInl t1) , (TySum T1 T2) ) : typing"

T_InrI: "[| ( G , t1 , T2 ) : typing|] ==> 
 ( G , (TmInr t1) , (TySum T1 T2) ) : typing"

T_CaseSmI: "[| ( G , t0 , (TySum T1 T2) ) : typing ;
 (  ( x1 , T1 )# G  , t1 , T ) : typing ;
 (  ( x2 , T2 )# G  , t2 , T ) : typing|] ==> 
 ( G , (TmCaseSm t0 x1 t1 x2 t2) , T ) : typing"

T_FixI: "[| ( G , t1 , (TyArr T1 T1) ) : typing|] ==> 
 ( G , (TmFix t1) , T1 ) : typing"

T_TupleI: "[|(List.list_all (% b . b) ((List.map (%(t_,T_). ( G , t_ , T_ ) : typing) t_T_list)))|] ==> 
 ( G , (TmTuple ((List.map (%(t_,T_).t_) t_T_list))) , (TyTuple ((List.map (%(t_,T_).T_) t_T_list))) ) : typing"

T_ProjTpI: "[| ( G , t1 , (TyTuple (T_list)) ) : typing ;
 (1 <=  j  &  j  <= length  (T_list) ) |] ==> 
 ( G , (TmProjTp t1 j) , ((%T_ . T_) (List.nth T_list (j - 1))) ) : typing"

T_VariantI: "[| ( G , t , ((%(l_,T_) . T_) (List.nth l_T_list (j - 1))) ) : typing ;
 (1 <=  j  &  j  <= length  ((List.map (%(l_,T_).T_) l_T_list)) ) |] ==> 
 ( G , (TmVariant ((%(l_,T_) . l_) (List.nth l_T_list (j - 1))) t (TyVariant (l_T_list))) , (TyVariant (l_T_list)) ) : typing"

T_CaseI: "[| ( G , t , (TyVariant ((List.map (%(l_,x_,t_,T_).(l_,T_)) l_x_t_T_list))) ) : typing ;
(List.list_all (% b . b) ((List.map (%(l_,x_,t_,T_). (  ( x_ , T_ )# G  , t_ , T ) : typing) l_x_t_T_list))) ;
 (distinct  ((List.map (%(l_,x_,t_,T_).l_) l_x_t_T_list)) ) |] ==> 
 ( G , (TmCase t ((List.map (%(l_,x_,t_,T_).(CCase l_ x_ t_)) l_x_t_T_list))) , T ) : typing"


end