<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 *)
(* 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("value_name", ``:string``);
val _ = type_abbrev("ident", ``:string``);
val _ = type_abbrev("integer_literal", ``:num``);
val _ = type_abbrev("index", ``:num``);
val _ = Hol_datatype ` 
typeconstr = 
   TC_unit
 | TC_bool
 | TC_int
`;
val _ = Hol_datatype ` 
typvar = 
   TV_ident of ident
`;
val _ = Hol_datatype ` 
typexpr = 
   TE_var of typvar
 | TE_arrow of typexpr => typexpr
 | TE_constr0 of typeconstr
`;
val _ = Hol_datatype ` 
constant = 
   CONST_int of integer_literal
 | CONST_false
 | CONST_true
 | CONST_unit
 | CONST_and
 | CONST_not
`;
val _ = Hol_datatype ` 
typscheme = 
   TS_ts of typvar list => typexpr
`;
val _ = Hol_datatype ` 
expr = 
   E_ident of value_name
 | E_constant of constant
 | E_apply of expr => expr
 | E_function of value_name => expr
 | E_let of value_name => expr => expr
`;
val _ = Hol_datatype ` 
G = 
   G_em
 | G_vn of G => value_name => typscheme
`;


(** subrules *)
val _ = ottDefine "is_value_of_expr" `
    ( is_value_of_expr (E_ident value_name) = F)
/\  ( is_value_of_expr (E_constant constant) = (T))
/\  ( is_value_of_expr (E_apply expr expr') = F)
/\  ( is_value_of_expr (E_function value_name expr) = (T))
/\  ( is_value_of_expr (E_let value_name expr expr') = F)
`;

(** free variables *)
val _ = ottDefine "ftv_typexpr" `
    ( ftv_typexpr (TE_var typvar) = [typvar])
/\  ( ftv_typexpr (TE_arrow typexpr typexpr') = (ftv_typexpr typexpr) ++ (ftv_typexpr typexpr'))
/\  ( ftv_typexpr (TE_constr0 typeconstr) = [])
`;

val _ = ottDefine "ftv_typscheme" `
    ( ftv_typscheme (TS_ts (typvar_list) typexpr) = [] ++ (list_minus (ftv_typexpr typexpr) typvar_list))
`;

val _ = ottDefine "ftv_G" `
    ( ftv_G G_em = [])
/\  ( ftv_G (G_vn G value_name typscheme) = (ftv_G G) ++ (ftv_typscheme typscheme))
`;

(** substitutions *)
val _ = ottDefine "tsubst_typexpr" `
    ( 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)
`;

val _ = ottDefine "tsubst_typscheme" `
    ( tsubst_typscheme sub (TS_ts (typvar_list) typexpr) = TS_ts typvar_list (tsubst_typexpr (FILTER (\(tv5,t5). ~(MEM tv5 typvar_list)) sub) typexpr))
`;

val _ = ottDefine "subst_expr" `
    ( 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 MEM x5 [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 MEM x5 [value_name] then expr' else (subst_expr e5 x5 expr')))
`;

val _ = ottDefine "tsubst_G" `
    ( 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))
`;
val _ = Define `
  (remove_duplicates [] = []) /\
  (remove_duplicates (x::xs) = if (MEM x xs) then remove_duplicates xs 
                               else x::(remove_duplicates xs))
`; 


(** definitions *)
(* defns Jtype *)

val (Jtype_rules, Jtype_ind, Jtype_cases) = Hol_reln `
(* defn VTSin *)

( (* VTSin_vn1 *)  !(value_name:value_name) (typscheme:typscheme) (G:G) . (clause_name "VTSin_vn1") ==> 
( ( VTSin value_name typscheme (G_vn G value_name typscheme) )))

/\ ( (* VTSin_vn2 *)  !(value_name:value_name) (typscheme:typscheme) (G:G) (value_name':value_name) (typscheme':typscheme) . (clause_name "VTSin_vn2") /\
(( ( VTSin value_name typscheme G )) /\
( ~(  value_name = value_name'  ) ))
 ==> 
( ( VTSin value_name typscheme (G_vn G value_name' typscheme') )))

/\
(* defn G_constant *)

( (* constant_int *)  !(G:G) (integer_literal:integer_literal) . (clause_name "constant_int") ==> 
( ( G_constant G (CONST_int integer_literal) (TE_constr0 TC_int) )))

/\ ( (* constant_false *)  !(G:G) . (clause_name "constant_false") ==> 
( ( G_constant G CONST_false (TE_constr0 TC_bool) )))

/\ ( (* constant_true *)  !(G:G) . (clause_name "constant_true") ==> 
( ( G_constant G CONST_true (TE_constr0 TC_bool) )))

/\ ( (* constant_unit *)  !(G:G) . (clause_name "constant_unit") ==> 
( ( G_constant G CONST_unit (TE_constr0 TC_unit) )))

/\ ( (* constant_and *)  !(G:G) . (clause_name "constant_and") ==> 
( ( G_constant G CONST_and (TE_arrow (TE_constr0 TC_bool)  (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool)) ) )))

/\ ( (* constant_not *)  !(G:G) . (clause_name "constant_not") ==> 
( ( G_constant G CONST_not (TE_arrow (TE_constr0 TC_bool) (TE_constr0 TC_bool)) )))

/\
(* defn Get *)

( (* Get_value_name *)  !(G:G) (x:value_name) (t:typexpr) (typscheme:typscheme) . (clause_name "Get_value_name") /\
(( ( VTSin x typscheme G )) /\
( ? typvars typexpr s . 
             ( typscheme  = TS_ts typvars typexpr )
             /\ (typvars=MAP FST s )
             /\ (tsubst_typexpr s typexpr =  t ) ))
 ==> 
( ( Get G (E_ident x) t )))

/\ ( (* Get_constant *)  !(G:G) (constant:constant) (t:typexpr) . (clause_name "Get_constant") /\
(( ( G_constant G constant t )))
 ==> 
( ( Get G (E_constant constant) t )))

/\ ( (* Get_apply *)  !(G:G) (e:expr) (e':expr) (t2:typexpr) (t1:typexpr) . (clause_name "Get_apply") /\
(( ( Get G e (TE_arrow t1 t2) )) /\
( ( Get G e' t1 )))
 ==> 
( ( Get G (E_apply e e') t2 )))

/\ ( (* Get_lambda *)  !(G:G) (x1:value_name) (e:expr) (t1:typexpr) (t:typexpr) . (clause_name "Get_lambda") /\
(( ( Get (G_vn G x1 (TS_ts NIL t1)) e t )))
 ==> 
( ( Get G (E_function x1 e) (TE_arrow t1 t) )))

/\ ( (* Get_let *)  !(G:G) (x:value_name) (e:expr) (e':expr) (t':typexpr) (t:typexpr) (typscheme:typscheme) . (clause_name "Get_let") /\
(( ( Get G e t )) /\
( ( Get (G_vn G x typscheme) e' t' )) /\
( typscheme =  (TS_ts (remove_duplicates (list_minus (ftv_typexpr  t ) (ftv_G  G )))  t )  ))
 ==> 
( ( Get G (E_let x e e') t' )))

`;

(* defns Jop *)

val (Jop_rules, Jop_ind, Jop_cases) = Hol_reln `
(* defn red *)

( (* JO_red_app *)  !(x:value_name) (e:expr) (v:expr) . (clause_name "JO_red_app") /\
((is_value_of_expr v))
 ==> 
( ( JO_red (E_apply  (E_function x e)  v)  (subst_expr  v   x   e )  )))

/\ ( (* JO_red_let *)  !(x:value_name) (e:expr) (v:expr) . (clause_name "JO_red_let") /\
((is_value_of_expr v))
 ==> 
( ( JO_red (E_let x v e)  (subst_expr  v   x   e )  )))

/\ ( (* JO_red_context_app1 *)  !(e:expr) (e1:expr) (e':expr) . (clause_name "JO_red_context_app1") /\
(( ( JO_red e e' )))
 ==> 
( ( JO_red (E_apply e e1) (E_apply e' e1) )))

/\ ( (* JO_red_context_app2 *)  !(v:expr) (e:expr) (e':expr) . (clause_name "JO_red_context_app2") /\
((is_value_of_expr v) /\
( ( JO_red e e' )))
 ==> 
( ( JO_red (E_apply v e) (E_apply v e') )))

/\ ( (* JO_red_context_let *)  !(x:value_name) (e:expr) (e1:expr) (e':expr) . (clause_name "JO_red_context_let") /\
(( ( JO_red e e' )))
 ==> 
( ( JO_red (E_let x e e1) (E_let x e' e1) )))

/\ ( (* JO_red_not_1 *)  (clause_name "JO_red_not_1") ==> 
( ( JO_red (E_apply (E_constant CONST_not) (E_constant CONST_true)) (E_constant CONST_false) )))

/\ ( (* JO_red_not_2 *)  (clause_name "JO_red_not_2") ==> 
( ( JO_red (E_apply (E_constant CONST_not) (E_constant CONST_false)) (E_constant CONST_true) )))

/\ ( (* JO_red_and_1 *)  !(e:expr) . (clause_name "JO_red_and_1") ==> 
( ( JO_red (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_true))  e) e )))

/\ ( (* JO_red_and_2 *)  !(e:expr) . (clause_name "JO_red_and_2") ==> 
( ( JO_red (E_apply  (E_apply (E_constant CONST_and) (E_constant CONST_false))  e) (E_constant CONST_false) )))

`;


val _ = export_theory ();