(* generated by Ott 0.10.14 from: ../tests/test10st.ott *) (* to compile: Holmake outTheory.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 "out"; (** syntax *) val _ = type_abbrev("termvar", ``:string``); val _ = type_abbrev("typvar", ``:string``); val _ = Hol_datatype ` T = T_var of typvar | T_arrow of T => T `; val _ = Hol_datatype ` t = t_Var of termvar | t_Lam of termvar => t | t_App of t => t `; val _ = type_abbrev("G", ``:(termvar#T) list``); (** 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) `; (** free variables *) val _ = ottDefine "fv_t" ` ( 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 *) 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 Jtype *) val (Jtype_rules, Jtype_ind, Jtype_cases) = Hol_reln ` (* defn GtT *) ( (* GtT_value_name *) !(G:G) (x:termvar) (T:T) . (clause_name "GtT_value_name") /\ (( ? G1 G2. ( G = G1 ++ ( x , T ):: G2 ) /\ ~(MEM x (MAP FST G1)) )) ==> ( ( GtT G (t_Var x) T ))) /\ ( (* GtT_apply *) !(G:G) (t:t) (t':t) (T2:T) (T1:T) . (clause_name "GtT_apply") /\ (( ( GtT G t (T_arrow T1 T2) )) /\ ( ( GtT G t' T1 ))) ==> ( ( GtT G (t_App t t') T2 ))) /\ ( (* GtT_lambda *) !(G:G) (x1:termvar) (t:t) (T1:T) (T:T) . (clause_name "GtT_lambda") /\ (( ( GtT (( x1 , T1 ):: G ) t T ))) ==> ( ( GtT G (t_Lam x1 t) (T_arrow T1 T) ))) `; (* 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 ();