<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* 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 ();