<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/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 ();