(* generated by Ott 0.10.14 from: ../tests/test10st.ott *) theory out imports Main Multiset begin (** syntax *) types termvar = "string" types typvar = "string" datatype T = T_var "typvar" | T_arrow "T" "T" datatype t = t_Var "termvar" | t_Lam "termvar" "t" | t_App "t" "t" types G = "(termvar*T) list" (** library functions *) 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 :: "t => bool" primrec "is_v_of_t (t_Var x) = (False)" "is_v_of_t (t_Lam x t) = ((True))" "is_v_of_t (t_App t t') = (False)" (** free variables *) consts fv_t :: "t => termvar list" primrec "fv_t (t_Var x) = ([x])" "fv_t (t_Lam x t) = ((list_minus (fv_t t) [x]))" "fv_t (t_App t t') = ((fv_t t) @ (fv_t t'))" (** substitutions *) consts tsubst_t :: "t => termvar => t => t" primrec "tsubst_t t5 x5 (t_Var x) = ((if x=x5 then t5 else (t_Var x)))" "tsubst_t t5 x5 (t_Lam x t) = (t_Lam x (if x5 mem [x] then t else (tsubst_t t5 x5 t)))" "tsubst_t t5 x5 (t_App t t') = (t_App (tsubst_t t5 x5 t) (tsubst_t t5 x5 t'))" (** definitions *) (*defns Jtype *) consts GtT :: "(G*t*T) set" inductive GtT intros (* defn GtT *) GtT_value_nameI: "[| ? G1 G2. G = G1 @ ( x , T )# G2 & x ~:fst ` set G1 |] ==> ( G , (t_Var x) , T ) : GtT" GtT_applyI: "[| ( G , t , (T_arrow T1 T2) ) : GtT ; ( G , t' , T1 ) : GtT|] ==> ( G , (t_App t t') , T2 ) : GtT" GtT_lambdaI: "[| ( ( x1 , T1 )# G , t , T ) : GtT|] ==> ( G , (t_Lam x1 t) , (T_arrow T1 T) ) : GtT" (*defns Jop *) consts reduce :: "(t*t) set" inductive reduce intros (* defn reduce *) ax_appI: "[|is_v_of_t v2|] ==> ( (t_App (t_Lam x t12) v2) , ( tsubst_t v2 x t12 ) ) : reduce" ctx_app_funI: "[| ( t1 , t1' ) : reduce|] ==> ( (t_App t1 t) , (t_App t1' t) ) : reduce" ctx_app_argI: "[|is_v_of_t v ; ( t1 , t1' ) : reduce|] ==> ( (t_App v t1) , (t_App v t1') ) : reduce" end