(* 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 *) 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 labels = labels_seq "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_XXX#t_list_XXX) = (((is_v_of_t t_XXX) & (is_v_of_t_list t_list_XXX)))" "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_XXX#C_list_XXX) = ((fv_C C_XXX) @ (fv_C_list C_list_XXX))" "fv_t_list Nil = ([])" "fv_t_list (t_XXX#t_list_XXX) = ((fv_t t_XXX) @ (fv_t_list t_list_XXX))" "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_XXX#C_list_XXX) = ((subst_C t_5 x_5 C_XXX) # (subst_C_list t_5 x_5 C_list_XXX))" "subst_t_list t_5 x_5 Nil = (Nil)" "subst_t_list t_5 x_5 (t_XXX#t_list_XXX) = ((subst_t t_5 x_5 t_XXX) # (subst_t_list t_5 x_5 t_list_XXX))" "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_XXX. is_v_of_t v_XXX) v_list ; (1 <= j & j <= length (v_list) ) |] ==> ( (TmProjTp (TmTuple (v_list)) j) , ((%v_XXX . v_XXX) (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_XXX. is_v_of_t v_XXX) 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_XXX::label),(x_XXX::termvar),(t_XXX::t)).t_XXX) l_x_t_list)) ) |] ==> ( (TmCase (TmVariant ((%(l_XXX,x_XXX,t_XXX) . l_XXX) (List.nth l_x_t_list (j - 1))) v T) ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t)).(CCase l_XXX x_XXX t_XXX)) l_x_t_list))) , (subst_t v ((%(l_XXX,x_XXX,t_XXX) . x_XXX) (List.nth l_x_t_list (j - 1))) ((%(l_XXX,x_XXX,t_XXX) . t_XXX) (List.nth l_x_t_list (j - 1))) ) ) : red" E_CaseI: "[| ( t , t' ) : red|] ==> ( (TmCase t ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t)).(CCase l_XXX x_XXX t_XXX)) l_x_t_list))) , (TmCase t' ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t)).(CCase l_XXX x_XXX t_XXX)) 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_XXX::t),(T_XXX::T)). ( G , t_XXX , T_XXX ) : typing) t_T_list)))|] ==> ( G , (TmTuple ((List.map (%((t_XXX::t),(T_XXX::T)).t_XXX) t_T_list))) , (TyTuple ((List.map (%((t_XXX::t),(T_XXX::T)).T_XXX) t_T_list))) ) : typing" T_ProjTpI: "[| ( G , t1 , (TyTuple (T_list)) ) : typing ; (1 <= j & j <= length (T_list) ) |] ==> ( G , (TmProjTp t1 j) , ((%T_XXX . T_XXX) (List.nth T_list (j - 1))) ) : typing" T_VariantI: "[| ( G , t , ((%(l_XXX,T_XXX) . T_XXX) (List.nth l_T_list (j - 1))) ) : typing ; (1 <= j & j <= length ((List.map (%((l_XXX::label),(T_XXX::T)).T_XXX) l_T_list)) ) |] ==> ( G , (TmVariant ((%(l_XXX,T_XXX) . l_XXX) (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_XXX::label),(x_XXX::termvar),(t_XXX::t),(T_XXX::T)).(l_XXX,T_XXX)) l_x_t_T_list))) ) : typing ; (List.list_all (% b . b) ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t),(T_XXX::T)). ( ( x_XXX , T_XXX )# G , t_XXX , T ) : typing) l_x_t_T_list))) ; (distinct ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t),(T_XXX::T)).l_XXX) l_x_t_T_list)) ) |] ==> ( G , (TmCase t ((List.map (%((l_XXX::label),(x_XXX::termvar),(t_XXX::t),(T_XXX::T)).(CCase l_XXX x_XXX t_XXX)) l_x_t_T_list))) , T ) : typing" end