(* generated by Ott 0.10.14 from: ../tests/test10.ott *) (* to compile: Holmake test10Theory.uo *) (* for interactive use: app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"]; *) open HolKernel boolLib Parse bossLib ottLib; infix THEN THENC |-> ## ; local open arithmeticTheory stringTheory containerTheory pred_setTheory listTheory finite_mapTheory in end; val _ = new_theory "test10"; (** syntax *) val _ = type_abbrev("termvar", ``:string``); val _ = Hol_datatype ` t = t_Var of termvar | t_Lam of termvar => t | t_App of t => t `; (** subrules *) val _ = ottDefine "is_v_of_t" ` ( is_v_of_t (t_Var x) = F) /\ ( is_v_of_t (t_Lam x t) = (T)) /\ ( is_v_of_t (t_App t t') = F) `; (** substitutions *) val _ = ottDefine "tsubst_t" ` ( 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 MEM x5 [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 *) val (Jop_rules, Jop_ind, Jop_cases) = Hol_reln ` (* defn reduce *) ( (* ax_app *) !(x:termvar) (t12:t) (v2:t) . (clause_name "ax_app") /\ ((is_v_of_t v2)) ==> ( ( reduce (t_App (t_Lam x t12) v2) (tsubst_t v2 x t12 ) ))) /\ ( (* ctx_app_fun *) !(t1:t) (t:t) (t1':t) . (clause_name "ctx_app_fun") /\ (( ( reduce t1 t1' ))) ==> ( ( reduce (t_App t1 t) (t_App t1' t) ))) /\ ( (* ctx_app_arg *) !(v:t) (t1:t) (t1':t) . (clause_name "ctx_app_arg") /\ ((is_v_of_t v) /\ ( ( reduce t1 t1' ))) ==> ( ( reduce (t_App v t1) (t_App v t1') ))) `; val _ = export_theory ();