(* generated by Ott 0.32 from: ../tests/test10.ott ../tests/non_super_tabular.ott *) theory test10 imports Main begin type_synonym "var" = "string" \ \term variable\ datatype "term" = \ \term\ t_var "var" \ \variable\ | t_lam "var" "term" \ \lambda\ | t_app "term" "term" \ \app\ (** subrules *) primrec is_val_of_term :: "term => bool" where "is_val_of_term (t_var x) = (False)" | "is_val_of_term (t_lam x t) = ((True))" | "is_val_of_term (t_app t t') = (False)" (** substitutions *) primrec tsubst_term :: "term => var => term => term" where "tsubst_term t5 x5 (t_var x) = ((if x=x5 then t5 else (t_var x)))" | "tsubst_term t5 x5 (t_lam x t) = (t_lam x (if x5 : set [x] then t else (tsubst_term t5 x5 t)))" | "tsubst_term t5 x5 (t_app t t') = (t_app (tsubst_term t5 x5 t) (tsubst_term t5 x5 t'))" (** definitions *) (* defns Jop *) inductive reduce :: "term \ term \ bool" where (* defn reduce *) ax_appI: "\is_val_of_term v2\ \ reduce ((t_app (t_lam x t1) v2)) ( (tsubst_term v2 x t1 ) )" | ctx_app_funI: "\reduce (t1) (t1')\ \ reduce ((t_app t1 t)) ((t_app t1' t))" | ctx_app_argI: "\is_val_of_term v ; reduce (t1) (t1')\ \ reduce ((t_app v t1)) ((t_app v t1'))" end