(* generated by Ott 0.10.14 from: ../tests/test10.ott *) theory test10 imports Main Multiset begin (** syntax *) types termvar = "string" datatype t = t_Var "termvar" | t_Lam "termvar" "t" | t_App "t" "t" (** 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)" (** 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 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