<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 *)
theory out imports Main Multiset begin

(** syntax *)
types termvar = "string"
types typvar = "string"
datatype 
T = 
   T_var "typvar"  
 | T_arrow "T" "T"  

datatype 
t = 
   t_Var "termvar"  
 | t_Lam "termvar" "t"  
 | t_App "t" "t"  

types G = "(termvar*T) list"


(** library functions *)
consts
list_minus :: "'a list => 'a list => 'a list"

primrec
"list_minus Nil ys = Nil"
"list_minus (Cons x xs) ys = (if Not(x : set ys) then Cons x (list_minus xs ys) else list_minus xs ys)"


(** subrules *)
consts
is_v_of_t :: "t => bool"
primrec
"is_v_of_t (t_Var x) = (False)"
"is_v_of_t (t_Lam x t) = ((True))"
"is_v_of_t (t_App t t') = (False)"


(** free variables *)
consts
fv_t :: "t => termvar list"
primrec
"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 *)
consts
tsubst_t :: "t => termvar => t => t"
primrec
"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 x5 mem [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 *)
consts
  GtT :: "(G*t*T) set"

inductive GtT
intros

(* defn GtT *)

GtT_value_nameI: "[| ? G1 G2.  G  = G1 @ ( x , T )# G2  &  x ~:fst ` set G1 |] ==> 
 ( G , (t_Var x) , T ) : GtT"

GtT_applyI: "[| ( G , t , (T_arrow T1 T2) ) : GtT ;
 ( G , t' , T1 ) : GtT|] ==> 
 ( G , (t_App t t') , T2 ) : GtT"

GtT_lambdaI: "[| (  ( x1 , T1 )# G  , t , T ) : GtT|] ==> 
 ( G , (t_Lam x1 t) , (T_arrow T1 T) ) : GtT"

(*defns Jop *)
consts
  reduce :: "(t*t) set"

inductive reduce
intros

(* defn reduce *)

ax_appI: "[|is_v_of_t v2|] ==> 
 ( (t_App  (t_Lam x t12)  v2) ,  ( tsubst_t  v2   x   t12  )  ) : reduce"

ctx_app_funI: "[| ( t1 , t1' ) : reduce|] ==> 
 ( (t_App t1 t) , (t_App t1' t) ) : reduce"

ctx_app_argI: "[|is_v_of_t v ;
 ( t1 , t1' ) : reduce|] ==> 
 ( (t_App v t1) , (t_App v t1') ) : reduce"


end