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

(** syntax *)
types value_name = "string"
types ident = "string"
types integer_literal = "int"
types index = "nat"
datatype 
typeconstr = 
   TC_unit  
 | TC_bool  
 | TC_int  

datatype 
typvar = 
   TV_ident "ident"  

datatype 
typexpr = 
   TE_var "typvar"  
 | TE_arrow "typexpr" "typexpr"  
 | TE_constr0 "typeconstr"  

datatype 
constant = 
   CONST_int "integer_literal"  
 | CONST_false  
 | CONST_true  
 | CONST_unit  
 | CONST_and  
 | CONST_not  

datatype 
typscheme = 
   TS_ts "typvar list" "typexpr"  

datatype 
expr = 
   E_ident "value_name"  
 | E_constant "constant"  
 | E_apply "expr" "expr"  
 | E_function "value_name" "expr"  
 | E_let "value_name" "expr" "expr"  

datatype 
G = 
   G_em  
 | G_vn "G" "value_name" "typscheme"  


(** library functions *)
lemma [mono]:"
         (!! x. f x --> g x) ==> list_all (%b. b) (map f foo_list)-->
                    list_all (%b. b) (map g foo_list) "
   apply(induct_tac foo_list, auto) done

lemma [mono]: "split f p = f (fst p) (snd p)" by (simp add: split_def)
consts
list_assoc :: "'a => ('a*'b) list => 'b option"

primrec
"list_assoc x0 Nil = None"
"list_assoc x0 (Cons xy  xys) = (if x0=fst xy then Some (snd xy) else list_assoc x0 xys)"

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_value_of_expr :: "expr => bool"
primrec
"is_value_of_expr (E_ident value_name) = (False)"
"is_value_of_expr (E_constant constant) = ((True))"
"is_value_of_expr (E_apply expr expr') = (False)"
"is_value_of_expr (E_function value_name expr) = ((True))"
"is_value_of_expr (E_let value_name expr expr') = (False)"


(** free variables *)
consts
ftv_typexpr :: "typexpr => typvar list"
primrec
"ftv_typexpr (TE_var typvar) = ([typvar])"
"ftv_typexpr (TE_arrow typexpr typexpr') = ((ftv_typexpr typexpr) @ (ftv_typexpr typexpr'))"
"ftv_typexpr (TE_constr0 typeconstr) = ([])"

consts
ftv_typscheme :: "typscheme => typvar list"
primrec
"ftv_typscheme (TS_ts (typvar_list) typexpr) = ([] @ (list_minus (ftv_typexpr typexpr) typvar_list))"

consts
ftv_G :: "G => typvar list"
primrec
"ftv_G G_em = ([])"
"ftv_G (G_vn G value_name typscheme) = ((ftv_G G) @ (ftv_typscheme typscheme))"


(** substitutions *)
consts
tsubst_typexpr :: "(typvar*typexpr) list => typexpr => typexpr"
primrec
"tsubst_typexpr sub (TE_var typvar) = ((case list_assoc typvar sub of None => (TE_var typvar) | Some t5 => t5))"
"tsubst_typexpr sub (TE_arrow typexpr typexpr') = (TE_arrow (tsubst_typexpr sub typexpr) (tsubst_typexpr sub typexpr'))"
"tsubst_typexpr sub (TE_constr0 typeconstr) = (TE_constr0 typeconstr)"

consts
tsubst_typscheme :: "(typvar*typexpr) list => typscheme => typscheme"
primrec
"tsubst_typscheme sub (TS_ts (typvar_list) typexpr) = (TS_ts typvar_list (tsubst_typexpr (List.filter (%(tv5,t5).Not(tv5 mem typvar_list)) sub) typexpr))"

consts
subst_expr :: "expr => value_name => expr => expr"
primrec
"subst_expr e5 x5 (E_ident value_name) = ((if value_name=x5 then e5 else (E_ident value_name)))"
"subst_expr e5 x5 (E_constant constant) = (E_constant constant)"
"subst_expr e5 x5 (E_apply expr expr') = (E_apply (subst_expr e5 x5 expr) (subst_expr e5 x5 expr'))"
"subst_expr e5 x5 (E_function value_name expr) = (E_function value_name (if x5 mem [value_name] then expr else (subst_expr e5 x5 expr)))"
"subst_expr e5 x5 (E_let value_name expr expr') = (E_let value_name (subst_expr e5 x5 expr) (if x5 mem [value_name] then expr' else (subst_expr e5 x5 expr')))"

consts
tsubst_G :: "(typvar*typexpr) list => G => G"
primrec
"tsubst_G sub G_em = (G_em )"
"tsubst_G sub (G_vn G value_name typscheme) = (G_vn (tsubst_G sub G) value_name (tsubst_typscheme sub typscheme))"


(** definitions *)
(*defns Jtype *)
consts
  VTSin :: "(value_name*typscheme*G) set"
  G_constant :: "(G*constant*typexpr) set"
  Get :: "(G*expr*typexpr) set"

inductive VTSin G_constant Get
intros

(* defn VTSin *)

VTSin_vn1I: " ( value_name , typscheme , (G_vn G value_name typscheme) ) : VTSin"

VTSin_vn2I: "[| ( value_name , typscheme , G ) : VTSin ;
 Not(  value_name = value_name'  ) |] ==> 
 ( value_name , typscheme , (G_vn G value_name' typscheme') ) : VTSin"

(* defn G_constant *)

constant_intI: " ( G , (CONST_int integer_literal) , (TE_constr0 TC_int) ) : G_constant"

constant_falseI: " ( G , CONST_false , (TE_constr0 TC_bool) ) : G_constant"

constant_trueI: " ( G , CONST_true , (TE_constr0 TC_bool) ) : G_constant"

constant_unitI: " ( G , CONST_unit , (TE_constr0 TC_unit) ) : G_constant"

constant_andI: " ( G , CONST_and , (TE_arrow (TE_constr0 TC_bool)  (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool)) ) ) : G_constant"

constant_notI: " ( G , CONST_not , (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool)) ) : G_constant"

(* defn Get *)

Get_value_nameI: "[| ( x , typscheme , G ) : VTSin ;
 ? typvars . ? typexpr . ? s . 
              typscheme  = TS_ts typvars typexpr 
             & typvars=List.map fst s 
             & tsubst_typexpr s typexpr =  t |] ==> 
 ( G , (E_ident x) , t ) : Get"

Get_constantI: "[| ( G , constant , t ) : G_constant|] ==> 
 ( G , (E_constant constant) , t ) : Get"

Get_applyI: "[| ( G , e , (TE_arrow t1 t2) ) : Get ;
 ( G , e' , t1 ) : Get|] ==> 
 ( G , (E_apply e e') , t2 ) : Get"

Get_lambdaI: "[| ( (G_vn G x1 (TS_ts [] t1)) , e , t ) : Get|] ==> 
 ( G , (E_function x1 e) , (TE_arrow t1 t) ) : Get"

Get_letI: "[| ( G , e , t ) : Get ;
 ( (G_vn G x typscheme) , e' , t' ) : Get ;
 typscheme =  (TS_ts (List.remdups (list_minus (ftv_typexpr  t ) (ftv_G  G )))  t )  |] ==> 
 ( G , (E_let x e e') , t' ) : Get"

(*defns Jop *)
consts
  JO_red :: "(expr*expr) set"

inductive JO_red
intros

(* defn red *)

JO_red_appI: "[|is_value_of_expr v|] ==> 
 ( (E_apply  (E_function x e)  v) ,  subst_expr  v   x   e  ) : JO_red"

JO_red_letI: "[|is_value_of_expr v|] ==> 
 ( (E_let x v e) ,  subst_expr  v   x   e  ) : JO_red"

JO_red_context_app1I: "[| ( e , e' ) : JO_red|] ==> 
 ( (E_apply e e1) , (E_apply e' e1) ) : JO_red"

JO_red_context_app2I: "[|is_value_of_expr v ;
 ( e , e' ) : JO_red|] ==> 
 ( (E_apply v e) , (E_apply v e') ) : JO_red"

JO_red_context_letI: "[| ( e , e' ) : JO_red|] ==> 
 ( (E_let x e e1) , (E_let x e' e1) ) : JO_red"

JO_red_not_1I: " ( (E_apply (E_constant CONST_not) (E_constant CONST_true)) , (E_constant CONST_false) ) : JO_red"

JO_red_not_2I: " ( (E_apply (E_constant CONST_not) (E_constant CONST_false)) , (E_constant CONST_true) ) : JO_red"

JO_red_and_1I: " ( (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_true))  e) , e ) : JO_red"

JO_red_and_2I: " ( (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_false))  e) , (E_constant CONST_false) ) : JO_red"


end