<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/leroy-jfp96.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";


val _ = hide "S";


(** syntax *)
val _ = type_abbrev("name", ``:string``);
val _ = type_abbrev("stamp", ``:num``);
val _ = type_abbrev("m", ``:num``);
val _ = Hol_datatype ` 
ident = 
   Id of name => stamp
`;
val _ = Hol_datatype ` 
p = 
   Mid of ident
 | Mpath of p => name
`;
val _ = Hol_datatype ` 
Ty = 
   Tyvar of ident
 | Typath of p => name
 | Tyarrow of Ty => Ty
`;
val _ = Hol_datatype ` 
C = 
   Otyspec of ident
 | Mtyspec of ident => Ty
 | Modspec of ident => S
 | Valspec of ident => Ty
;
D = 
   DNil
 | DCons of C => D
;
S = 
   Strsig of D
 | Ftorsig of ident => S => S
`;
val _ = Hol_datatype ` 
M = 
   Var of ident
 | Vpath of p => name
 | Fun of ident => Ty => M
 | Fapp of M => M
 | Letexp of d => M
;
c = 
   Typebind of ident => Ty
 | Dtype of ident
 | Strbind of ident => s
 | Valbind of ident => M
;
d = 
   dNil_d
 | dCons of c => d
;
s = 
   Path of p
 | Strexp of d
 | Ftorexp of ident => S => s
 | Ftorapp of s => p
 | Seal of s => S
`;
val _ = type_abbrev("E", ``:C list``);
val _ = type_abbrev("delta", ``:c list``);


(** subrules *)
val _ = ottDefine "is_V_of_M" `
    ( is_V_of_M (Var vi) = F)
/\  ( is_V_of_M (Vpath p v) = F)
/\  ( is_V_of_M (Fun vi Ty M) = (T))
/\  ( is_V_of_M (Fapp M1 M2) = F)
/\  ( is_V_of_M (Letexp d M) = F)
`;

val _ = ottDefine "is_dV_of_d" `
    ( is_dV_of_d dNil_d = (T))
/\  ( is_dV_of_d (dCons c d) = ((is_cV_of_c c) /\ (is_dV_of_d d)))
/\  ( is_sV_of_s (Path p) = F)
/\  ( is_sV_of_s (Strexp d) = ((is_dV_of_d d)))
/\  ( is_sV_of_s (Ftorexp xi S s) = (T))
/\  ( is_sV_of_s (Ftorapp s p) = F)
/\  ( is_sV_of_s (Seal s S) = F)
/\  ( is_cV_of_c (Typebind ti Ty) = (T))
/\  ( is_cV_of_c (Dtype ti) = (T))
/\  ( is_cV_of_c (Strbind xi s) = ((is_sV_of_s s)))
/\  ( is_cV_of_c (Valbind vi M) = ((is_V_of_M M)))
`;

(** auxiliary functions *)
val _ = ottDefine "aux_Cbinders_C_of_C" `
    ( aux_Cbinders_C_of_C (Otyspec ti) = [ti])
/\  ( aux_Cbinders_C_of_C (Mtyspec ti Ty) = [ti])
/\  ( aux_Cbinders_C_of_C (Modspec xi S) = [xi])
/\  ( aux_Cbinders_C_of_C (Valspec vi Ty) = [vi])
`;

val _ = ottDefine "aux_cbinders_c_of_c" `
    ( aux_cbinders_c_of_c (Typebind ti Ty) = [ti])
/\  ( aux_cbinders_c_of_c (Dtype ti) = [ti])
/\  ( aux_cbinders_c_of_c (Strbind xi s) = [xi])
/\  ( aux_cbinders_c_of_c (Valbind vi M) = [vi])
`;

(** substitutions *)
val _ = ottDefine "subst_p" `
    ( subst_p p5 ti5 (Mid xi) = (if xi=ti5 then p5 else (Mid xi)))
/\  ( subst_p p5 ti5 (Mpath p x) = Mpath (subst_p p5 ti5 p) x)
`;

val _ = ottDefine "msubst_p" `
    ( msubst_p sub (Mid xi) = (case list_assoc xi sub of NONE -> (Mid xi) || SOME p5 -> p5))
/\  ( msubst_p sub (Mpath p x) = Mpath (msubst_p sub p) x)
`;

val _ = ottDefine "subst_Ty" `
    ( subst_Ty p5 ti5 (Tyvar ti) = Tyvar ti)
/\  ( subst_Ty p5 ti5 (Typath p t) = Typath (subst_p p5 ti5 p) t)
/\  ( subst_Ty p5 ti5 (Tyarrow Ty1 Ty2) = Tyarrow (subst_Ty p5 ti5 Ty1) (subst_Ty p5 ti5 Ty2))
`;

val _ = ottDefine "msubst_Ty" `
    ( msubst_Ty sub (Tyvar ti) = Tyvar ti)
/\  ( msubst_Ty sub (Typath p t) = Typath (msubst_p sub p) t)
/\  ( msubst_Ty sub (Tyarrow Ty1 Ty2) = Tyarrow (msubst_Ty sub Ty1) (msubst_Ty sub Ty2))
`;

val _ = ottDefine "subst_C" `
    ( subst_C p5 ti5 (Otyspec ti) = Otyspec ti)
/\  ( subst_C p5 ti5 (Mtyspec ti Ty) = Mtyspec ti (subst_Ty p5 ti5 Ty))
/\  ( subst_C p5 ti5 (Modspec xi S) = Modspec xi (subst_S p5 ti5 S))
/\  ( subst_C p5 ti5 (Valspec vi Ty) = Valspec vi (subst_Ty p5 ti5 Ty))
/\  ( subst_D p5 ti5 DNil = DNil )
/\  ( subst_D p5 ti5 (DCons C D) = DCons (subst_C p5 ti5 C) (if MEM ti5 (aux_Cbinders_C_of_C C) then D else (subst_D p5 ti5 D)))
/\  ( subst_S p5 ti5 (Strsig D) = Strsig (subst_D p5 ti5 D))
/\  ( subst_S p5 ti5 (Ftorsig xi S1 S2) = Ftorsig xi (subst_S p5 ti5 S1) (if MEM ti5 [xi] then S2 else (subst_S p5 ti5 S2)))
`;

val _ = ottDefine "msubst_C" `
    ( msubst_C sub (Otyspec ti) = Otyspec ti)
/\  ( msubst_C sub (Mtyspec ti Ty) = Mtyspec ti (msubst_Ty sub Ty))
/\  ( msubst_C sub (Modspec xi S) = Modspec xi (msubst_S sub S))
/\  ( msubst_C sub (Valspec vi Ty) = Valspec vi (msubst_Ty sub Ty))
/\  ( msubst_D sub DNil = DNil )
/\  ( msubst_D sub (DCons C D) = DCons (msubst_C sub C) (msubst_D (FILTER (\(ti5,p5). ~(MEM ti5 (aux_Cbinders_C_of_C C))) sub) D))
/\  ( msubst_S sub (Strsig D) = Strsig (msubst_D sub D))
/\  ( msubst_S sub (Ftorsig xi S1 S2) = Ftorsig xi (msubst_S sub S1) (msubst_S (FILTER (\(ti5,p5). ~(MEM ti5 [xi])) sub) S2))
`;

val _ = ottDefine "subst_M" `
    ( subst_M p5 ti5 (Var vi) = Var vi)
/\  ( subst_M p5 ti5 (Vpath p v) = Vpath (subst_p p5 ti5 p) v)
/\  ( subst_M p5 ti5 (Fun vi Ty M) = Fun vi (subst_Ty p5 ti5 Ty) (if MEM ti5 [vi] then M else (subst_M p5 ti5 M)))
/\  ( subst_M p5 ti5 (Fapp M1 M2) = Fapp (subst_M p5 ti5 M1) (subst_M p5 ti5 M2))
/\  ( subst_M p5 ti5 (Letexp d M) = Letexp (subst_d p5 ti5 d) (subst_M p5 ti5 M))
/\  ( subst_c p5 ti5 (Typebind ti Ty) = Typebind ti (subst_Ty p5 ti5 Ty))
/\  ( subst_c p5 ti5 (Dtype ti) = Dtype ti)
/\  ( subst_c p5 ti5 (Strbind xi s) = Strbind xi (subst_s p5 ti5 s))
/\  ( subst_c p5 ti5 (Valbind vi M) = Valbind vi (subst_M p5 ti5 M))
/\  ( subst_d p5 ti5 dNil_d = dNil_d )
/\  ( subst_d p5 ti5 (dCons c d) = dCons (subst_c p5 ti5 c) (if MEM ti5 (aux_cbinders_c_of_c c) then d else (subst_d p5 ti5 d)))
/\  ( subst_s p5 ti5 (Path p) = Path (subst_p p5 ti5 p))
/\  ( subst_s p5 ti5 (Strexp d) = Strexp (subst_d p5 ti5 d))
/\  ( subst_s p5 ti5 (Ftorexp xi S s) = Ftorexp xi (subst_S p5 ti5 S) (if MEM ti5 [xi] then s else (subst_s p5 ti5 s)))
/\  ( subst_s p5 ti5 (Ftorapp s p) = Ftorapp (subst_s p5 ti5 s) (subst_p p5 ti5 p))
/\  ( subst_s p5 ti5 (Seal s S) = Seal (subst_s p5 ti5 s) (subst_S p5 ti5 S))
`;

val _ = ottDefine "msubst_M" `
    ( msubst_M sub (Var vi) = Var vi)
/\  ( msubst_M sub (Vpath p v) = Vpath (msubst_p sub p) v)
/\  ( msubst_M sub (Fun vi Ty M) = Fun vi (msubst_Ty sub Ty) (msubst_M (FILTER (\(ti5,p5). ~(MEM ti5 [vi])) sub) M))
/\  ( msubst_M sub (Fapp M1 M2) = Fapp (msubst_M sub M1) (msubst_M sub M2))
/\  ( msubst_M sub (Letexp d M) = Letexp (msubst_d sub d) (msubst_M sub M))
/\  ( msubst_c sub (Typebind ti Ty) = Typebind ti (msubst_Ty sub Ty))
/\  ( msubst_c sub (Dtype ti) = Dtype ti)
/\  ( msubst_c sub (Strbind xi s) = Strbind xi (msubst_s sub s))
/\  ( msubst_c sub (Valbind vi M) = Valbind vi (msubst_M sub M))
/\  ( msubst_d sub dNil_d = dNil_d )
/\  ( msubst_d sub (dCons c d) = dCons (msubst_c sub c) (msubst_d (FILTER (\(ti5,p5). ~(MEM ti5 (aux_cbinders_c_of_c c))) sub) d))
/\  ( msubst_s sub (Path p) = Path (msubst_p sub p))
/\  ( msubst_s sub (Strexp d) = Strexp (msubst_d sub d))
/\  ( msubst_s sub (Ftorexp xi S s) = Ftorexp xi (msubst_S sub S) (msubst_s (FILTER (\(ti5,p5). ~(MEM ti5 [xi])) sub) s))
/\  ( msubst_s sub (Ftorapp s p) = Ftorapp (msubst_s sub s) (msubst_p sub p))
/\  ( msubst_s sub (Seal s S) = Seal (msubst_s sub s) (msubst_S sub S))
`;

val _ = ottDefine "vsubst_M" `
    ( vsubst_M M_5 ti5 (Var vi) = (if vi=ti5 then M_5 else (Var vi)))
/\  ( vsubst_M M_5 ti5 (Vpath p v) = Vpath p v)
/\  ( vsubst_M M_5 ti5 (Fun vi Ty M) = Fun vi Ty (if MEM ti5 [vi] then M else (vsubst_M M_5 ti5 M)))
/\  ( vsubst_M M_5 ti5 (Fapp M1 M2) = Fapp (vsubst_M M_5 ti5 M1) (vsubst_M M_5 ti5 M2))
/\  ( vsubst_M M_5 ti5 (Letexp d M) = Letexp (vsubst_d M_5 ti5 d) (vsubst_M M_5 ti5 M))
/\  ( vsubst_c M5 ti5 (Typebind ti Ty) = Typebind ti Ty)
/\  ( vsubst_c M5 ti5 (Dtype ti) = Dtype ti)
/\  ( vsubst_c M5 ti5 (Strbind xi s) = Strbind xi (vsubst_s M5 ti5 s))
/\  ( vsubst_c M5 ti5 (Valbind vi M) = Valbind vi (vsubst_M M5 ti5 M))
/\  ( vsubst_d M5 ti5 dNil_d = dNil_d )
/\  ( vsubst_d M5 ti5 (dCons c d) = dCons (vsubst_c M5 ti5 c) (if MEM ti5 (aux_cbinders_c_of_c c) then d else (vsubst_d M5 ti5 d)))
/\  ( vsubst_s M5 ti5 (Path p) = Path p)
/\  ( vsubst_s M5 ti5 (Strexp d) = Strexp (vsubst_d M5 ti5 d))
/\  ( vsubst_s M5 ti5 (Ftorexp xi S s) = Ftorexp xi S (if MEM ti5 [xi] then s else (vsubst_s M5 ti5 s)))
/\  ( vsubst_s M5 ti5 (Ftorapp s p) = Ftorapp (vsubst_s M5 ti5 s) p)
/\  ( vsubst_s M5 ti5 (Seal s S) = Seal (vsubst_s M5 ti5 s) S)
`;

val C_BV_def = Define `
(C_BV (Otyspec ti) = ti) /\
(C_BV (Mtyspec ti Ty) = ti) /\
(C_BV (Modspec xi S) = xi) /\
(C_BV (Valspec vi Ty) = vi)`;

val c_BV_def = Define `
(c_BV (Typebind ti Ty) = ti) /\
(c_BV (Dtype ti) = ti) /\
(c_BV (Strbind xi s) = xi) /\
(c_BV (Valbind vi M) = vi)`;

val BV_def = Define `
BV = MAP C_BV`;

val D_BV_def = Define `
(D_BV DNil = []) /\
(D_BV (DCons C D) = C_BV C :: D_BV D)`;

val d_BV_def = Define `
(d_BV dNil = []) /\
(d_BV (dCons c d) = c_BV c :: d_BV d)`;

val build_msubst_D_def = Define `
build_msubst_D p D = 
MAP (\id. case id of Id n i -> (id, (Mpath p n)))
    (D_BV D)`;

val build_msubst_d_def = Define `
build_msubst_d p d = 
MAP (\id. case id of Id n i -> (id, (Mpath p n)))
    (d_BV d)`;


val Sstrengthen_def = Define `
( (Sstrengthen   (Strsig D)    p )  = (Strsig  (Dstrengthen  D   p ) )) /\
( (Sstrengthen   (Ftorsig xi S1 S2)    p )  = (Ftorsig xi S1 S2)) /\
( (Dstrengthen  DNil   p )  = DNil) /\
( (Dstrengthen   (DCons C D)    p )  = (DCons  (Cstrengthen  C   p )    (Dstrengthen  D   p )  )) /\
( (Cstrengthen   (Otyspec (Id t i))    p )  = (Mtyspec (Id t i) (Typath p t))) /\
( (Cstrengthen   (Mtyspec ti Ty)    p )  = (Mtyspec ti Ty)) /\
( (Cstrengthen   (Modspec (Id x i) S)    p )  = (Modspec (Id x i)   (Sstrengthen  S   (Mpath p x) )  )) /\
( (Cstrengthen   (Valspec vi Ty)    p )  = (Valspec vi Ty))`;

val sstrengthen_def = Define `
( (sstrengthen   (Strexp d)    p )  = (Strexp  (dstrengthen  d   p ) )) /\
( (sstrengthen   (Ftorexp xi S s)    p )  = Ftorexp xi S s) /\
((PARSE_ERROR "line 252 char 1 - 13" " no parses (char 6): :dNil:***/p ") = dNil) /\
( (dstrengthen   (dCons c d)    p )  = (dCons  (cstrengthen  c   p )    (dstrengthen  d   p )  )) /\
( (cstrengthen   cV    p )  = Typebind ti Ty) /\
( (cstrengthen   cV    p )  = Typebind (Id t i) (Typath p t)) /\
( (cstrengthen   cV    p )  = (Strbind (Id x i)   (sstrengthen  s   (Mpath p x) )  )) /\
( (cstrengthen   cV    p )  = Valbind vi M)`;


val D_append_def = Define `
( (D_append   DNil    C   D2 )  = (DCons C D2)) /\
( (D_append   (DCons C1 D1)    C2   D2 )  = (DCons C1   (D_append  D1   C2   D2 )  ))`;

val d_append_def = Define `
( (d_append   dNil_d    c   d2 )  = (dCons c d2)) /\
( (d_append   (dCons c1 d1)    c2   d2 )  = (dCons c1   (d_append  d1   c2   d2 )  ))`;

val d_to_list_def = Define `
(d_to_list dNil = []) /\
(d_to_list (dCons c d) = c::d_to_list d)`;

val D_to_list_def = Define `
(D_to_list DNil = []) /\
(D_to_list (DCons c d) = c::D_to_list d)`;


(** definitions *)
(* defns pathE *)

val (pathE_rules, pathE_ind, pathE_cases) = Hol_reln `
(* defn pathE *)

( (* pathE1 *)  !(E1:E) (xi:ident) (S:S) (E2:E) . (clause_name "pathE1") ==> 
( ( pathE  ( E2  ++  (Modspec xi S)  ::  E1 )  (Mid xi)  (Sstrengthen  S   (Mid xi) )  )))

/\ ( (* pathE2 *)  !(E:E) (p:p) (x:name) (S:S) (D1:D) (i:stamp) (D2:D) . (clause_name "pathE2") /\
(( ( pathE E p (Strsig  (D_append  D1   (Modspec (Id x i) S)   D2 ) ) )))
 ==> 
( ( pathE E (Mpath p x)  (msubst_S (build_msubst_D  p   D1 )  S )  )))

`;

(* defns WFtype *)

val (WFtype_rules, WFtype_ind, WFtype_cases) = Hol_reln `
(* defn WFtype *)

( (* WFtype1 *)  !(E1:E) (ti:ident) (E2:E) . (clause_name "WFtype1") ==> 
( ( WFtype  ( E2  ++  (Otyspec ti)  ::  E1 )  (Tyvar ti) )))

/\ ( (* WFtype2 *)  !(E1:E) (ti:ident) (Ty:Ty) (E2:E) . (clause_name "WFtype2") ==> 
( ( WFtype  ( E2  ++  (Mtyspec ti Ty)  ::  E1 )  (Tyvar ti) )))

/\ ( (* WFtype3 *)  !(E:E) (p:p) (t:name) (D1:D) (i:stamp) (D2:D) . (clause_name "WFtype3") /\
(( ( pathE E p (Strsig  (D_append  D1   (Otyspec (Id t i))   D2 ) ) )))
 ==> 
( ( WFtype E (Typath p t) )))

/\ ( (* WFtype4 *)  !(E:E) (p:p) (t:name) (D1:D) (i:stamp) (Ty:Ty) (D2:D) . (clause_name "WFtype4") /\
(( ( pathE E p (Strsig  (D_append  D1   (Mtyspec (Id t i) Ty)   D2 ) ) )))
 ==> 
( ( WFtype E (Typath p t) )))

/\ ( (* WFtype5 *)  !(E:E) (Ty1:Ty) (Ty2:Ty) . (clause_name "WFtype5") /\
(( ( WFtype E Ty1 )) /\
( ( WFtype E Ty2 )))
 ==> 
( ( WFtype E  (Tyarrow Ty1 Ty2)  )))

`;

(* defns WFsig *)

val (WFsig_rules, WFsig_ind, WFsig_cases) = Hol_reln `
(* defn WFdecl *)

( (* WFdecl1 *)  !(E:E) . (clause_name "WFdecl1") ==> 
( ( WFdecl E DNil )))

/\ ( (* WFdecl2 *)  !(E:E) (ti:ident) (Ty:Ty) (D:D) . (clause_name "WFdecl2") /\
(( ( WFtype E Ty )) /\
( ( WFdecl  ( (Mtyspec ti Ty)  ::  E )  D )))
 ==> 
( ( WFdecl E  (DCons (Mtyspec ti Ty) D)  )))

/\ ( (* WFdecl3 *)  !(E:E) (ti:ident) (D:D) . (clause_name "WFdecl3") /\
(( ( WFdecl  ( (Otyspec ti)  ::  E )  D )))
 ==> 
( ( WFdecl E  (DCons (Otyspec ti) D)  )))

/\ ( (* WFdecl4 *)  !(E:E) (xi:ident) (S:S) (D:D) . (clause_name "WFdecl4") /\
(( ( WFsig E S )) /\
( ( WFdecl  ( (Modspec xi S)  ::  E )  D )))
 ==> 
( ( WFdecl E  (DCons (Modspec xi S) D)  )))

/\ ( (* WFdecl5 *)  !(E:E) (vi:ident) (Ty:Ty) (D:D) . (clause_name "WFdecl5") /\
(( ( WFtype E Ty )) /\
( ( WFdecl  ( (Valspec vi Ty)  ::  E )  D )))
 ==> 
( ( WFdecl E  (DCons (Valspec vi Ty) D)  )))

/\
(* defn WFsig *)

( (* WFsig1 *)  !(E:E) (D:D) . (clause_name "WFsig1") /\
(( ( WFdecl E D )))
 ==> 
( ( WFsig E  (Strsig D)  )))

/\ ( (* WFsig2 *)  !(E:E) (xi:ident) (S1:S) (S2:S) . (clause_name "WFsig2") /\
(( ( WFsig E S1 )) /\
( ( WFsig  ( (Modspec xi S1)  ::  E )  S2 )))
 ==> 
( ( WFsig E  (Ftorsig xi S1 S2)  )))

`;

(* defns eq *)

val (eq_rules, eq_ind, eq_cases) = Hol_reln `
(* defn eqT *)

( (* eqT1 *)  !(E1:E) (ti:ident) (Ty:Ty) (E2:E) . (clause_name "eqT1") ==> 
( ( eqT  ( E2  ++  (Mtyspec ti Ty)  ::  E1 )  (Tyvar ti) Ty )))

/\ ( (* eqT2 *)  !(E:E) (p:p) (t:name) (Ty:Ty) (D1:D) (i:stamp) (D2:D) . (clause_name "eqT2") /\
(( ( pathE E p (Strsig  (D_append  D1   (Mtyspec (Id t i) Ty)   D2 ) ) )))
 ==> 
( ( eqT E (Typath p t)  (msubst_T (build_msubst_D  p   D1 )  Ty )  )))

/\ ( (* eqT3 *)  !(E:E) (Ty:Ty) . (clause_name "eqT3") ==> 
( ( eqT E Ty Ty )))

/\ ( (* eqT4 *)  !(E:E) (Ty1:Ty) (Ty2:Ty) . (clause_name "eqT4") /\
(( ( eqT E Ty2 Ty1 )))
 ==> 
( ( eqT E Ty1 Ty2 )))

/\ ( (* eqT5 *)  !(E:E) (Ty1:Ty) (Ty3:Ty) (Ty2:Ty) . (clause_name "eqT5") /\
(( ( eqT E Ty1 Ty2 )) /\
( ( eqT E Ty2 Ty3 )))
 ==> 
( ( eqT E Ty1 Ty3 )))

/\ ( (* eqT6 *)  !(E:E) (Ty1:Ty) (Ty2:Ty) (Ty3:Ty) (Ty4:Ty) . (clause_name "eqT6") /\
(( ( eqT E Ty1 Ty3 )) /\
( ( eqT E Ty2 Ty4 )))
 ==> 
( ( eqT E  (Tyarrow Ty1 Ty2)   (Tyarrow Ty3 Ty4)  )))

`;

(* defns sub *)

val (sub_rules, sub_ind, sub_cases) = Hol_reln `
(* defn subS *)

( (* subS1 *)  !(E:E) (xi:ident) (S1:S) (S1':S) (S2:S) (S2':S) . (clause_name "subS1") /\
(( ( subS E S2 S1 )) /\
( ( subS  ( (Modspec xi S2)  ::  E )  S1' S2' )))
 ==> 
( ( subS E (Ftorsig xi S1 S1') (Ftorsig xi S2 S2') )))

/\ ( (* subS2 *)  !(E:E) (D:D) (D':D) . (clause_name "subS2") /\
(( ( subD E D D' )))
 ==> 
( ( subS E (Strsig D) (Strsig D') )))

/\
(* defn subD *)

( (* subD1 *)  !(E:E) . (clause_name "subD1") ==> 
( ( subD E DNil DNil )))

/\ ( (* subD2 *)  !(E:E) (C:C) (D:D) (C':C) (D':D) . (clause_name "subD2") /\
(( ( subC E C C' )) /\
( ( subD  ( C  ::  E )  D D' )))
 ==> 
( ( subD E (DCons C D) (DCons C' D') )))

/\ ( (* subD3 *)  !(E:E) (C:C) (D:D) (D':D) . (clause_name "subD3") /\
(( ( subD  ( C  ::  E )  D D' )))
 ==> 
( ( subD E (DCons C D) D' )))

/\
(* defn subC *)

( (* subC1 *)  !(E:E) (ti:ident) . (clause_name "subC1") ==> 
( ( subC E  (Otyspec ti)   (Otyspec ti)  )))

/\ ( (* subC2 *)  !(E:E) (ti:ident) (Ty:Ty) . (clause_name "subC2") ==> 
( ( subC E  (Mtyspec ti Ty)   (Otyspec ti)  )))

/\ ( (* subC4 *)  !(E:E) (ti:ident) (Ty1:Ty) (Ty2:Ty) . (clause_name "subC4") /\
(( ( eqT E Ty1 Ty2 )))
 ==> 
( ( subC E  (Mtyspec ti Ty1)   (Mtyspec ti Ty2)  )))

/\ ( (* subC5 *)  !(E:E) (xi:ident) (S1:S) (S2:S) . (clause_name "subC5") /\
(( ( subS E S1 S2 )))
 ==> 
( ( subC E  (Modspec xi S1)   (Modspec xi S2)  )))

/\ ( (* subC6 *)  !(E:E) (vi:ident) (Ty1:Ty) (Ty2:Ty) . (clause_name "subC6") /\
(( ( eqT E Ty1 Ty2 )))
 ==> 
( ( subC E  (Valspec vi Ty1)   (Valspec vi Ty2)  )))

`;

(* defns typ *)

val (typ_rules, typ_ind, typ_cases) = Hol_reln `
(* defn type_s *)

( (* type_s1 *)  !(E:E) (p:p) (S:S) . (clause_name "type_s1") /\
(( ( pathE E p S )))
 ==> 
( ( type_s E (Path p) S )))

/\ ( (* type_s2 *)  !(E:E) (xi:ident) (S:S) (s:s) (S':S) . (clause_name "type_s2") /\
(( ( WFsig E S )) /\
( ~(MEM  xi  (BV E )) ) /\
( ( type_s  ( (Modspec xi S)  ::  E )  s S' )))
 ==> 
( ( type_s E (Ftorexp xi S s) (Ftorsig xi S S') )))

/\ ( (* type_s3 *)  !(E:E) (s:s) (p:p) (S:S) (xi:ident) (S':S) (S'':S) . (clause_name "type_s3") /\
(( ( type_s E s (Ftorsig xi S' S) )) /\
( ( pathE E p S'' )) /\
( ( subS E S'' S' )))
 ==> 
( ( type_s E (Ftorapp s p)  (subst_S  p   xi   S )  )))

/\ ( (* type_s4 *)  !(E:E) (d:d) (D:D) . (clause_name "type_s4") /\
(( ( type_d E d D )))
 ==> 
( ( type_s E (Strexp d) (Strsig D) )))

/\ ( (* type_s5 *)  !(E:E) (s:s) (S1:S) (S2:S) . (clause_name "type_s5") /\
(( ( WFsig E S1 )) /\
( ( type_s E s S2 )) /\
( ( subS E S2 S1 )))
 ==> 
( ( type_s E (Seal s S1) S1 )))

/\
(* defn type_c *)

( (* type_c1 *)  !(E:E) (ti:ident) (Ty:Ty) . (clause_name "type_c1") /\
(( ( WFtype E Ty )) /\
( ~(MEM  ti  (BV E )) ))
 ==> 
( ( type_c E (Typebind ti Ty) (Mtyspec ti Ty) )))

/\ ( (* type_c2 *)  !(E:E) (ti:ident) . (clause_name "type_c2") /\
(( ~(MEM  ti  (BV E )) ))
 ==> 
( ( type_c E (Dtype ti) (Otyspec ti) )))

/\ ( (* type_c3 *)  !(E:E) (xi:ident) (s:s) (S:S) . (clause_name "type_c3") /\
(( ( type_s E s S )) /\
( ~(MEM  xi  (BV E )) ))
 ==> 
( ( type_c E (Strbind xi s) (Modspec xi S) )))

/\ ( (* type_c4 *)  !(E:E) (vi:ident) (M:M) (Ty:Ty) . (clause_name "type_c4") /\
(( ( typeM E M Ty )) /\
( ~(MEM  vi  (BV E )) ))
 ==> 
( ( type_c E (Valbind vi M) (Valspec vi Ty) )))

/\
(* defn type_d *)

( (* type_d1 *)  !(E:E) . (clause_name "type_d1") ==> 
( ( type_d E dNil_d DNil )))

/\ ( (* type_d2 *)  !(E:E) (c:c) (d:d) (C:C) (D:D) . (clause_name "type_d2") /\
(( ( type_c E c C )) /\
( ( type_d  ( C  ::  E )  d D )))
 ==> 
( ( type_d E (dCons c d) (DCons C D) )))

/\
(* defn typeM *)

( (* typeM1 *)  !(E1:E) (vi:ident) (Ty:Ty) (E2:E) . (clause_name "typeM1") ==> 
( ( typeM  ( E2  ++  (Valspec vi Ty)  ::  E1 )  (Var vi) Ty )))

/\ ( (* typeM2 *)  !(E:E) (p:p) (v:name) (Ty:Ty) (D1:D) (i:stamp) (D2:D) . (clause_name "typeM2") /\
(( ( pathE E p (Strsig  (D_append  D1   (Valspec (Id v i) Ty)   D2 ) ) )))
 ==> 
( ( typeM E (Vpath p v)  (msubst_T (build_msubst_D  p   D1 )  Ty )  )))

/\ ( (* typeM3 *)  !(E:E) (vi:ident) (Ty1:Ty) (M:M) (Ty2:Ty) . (clause_name "typeM3") /\
(( ~(MEM  vi  (BV E )) ) /\
( ( WFtype E Ty1 )) /\
( ( typeM  ( (Valspec vi Ty1)  ::  E )  M Ty2 )))
 ==> 
( ( typeM E (Fun vi Ty1 M) (Tyarrow Ty1 Ty2) )))

/\ ( (* typeM4 *)  !(E:E) (M1:M) (M2:M) (Ty2:Ty) (Ty1:Ty) . (clause_name "typeM4") /\
(( ( typeM E M1 (Tyarrow Ty1 Ty2) )) /\
( ( typeM E M2 Ty1 )))
 ==> 
( ( typeM E (Fapp M1 M2) Ty2 )))

/\ ( (* typeM5 *)  !(E:E) (d:d) (M:M) (Ty2:Ty) (D:D) (Ty1:Ty) . (clause_name "typeM5") /\
(( ( type_d E d D )) /\
( ( typeM  (REVERSE (D_to_list  D ) ++  E )  M Ty1 )) /\
( ( eqT  (REVERSE (D_to_list  D ) ++  E )  Ty1 Ty2 )) /\
( ( WFtype E Ty2 )))
 ==> 
( ( typeM E (Letexp d M) Ty2 )))

`;

(* defns pathDelta *)

val (pathDelta_rules, pathDelta_ind, pathDelta_cases) = Hol_reln `
(* defn pathDelta *)

( (* pathDelta1 *)  !(delta1:delta) (xi:ident) (s:s) (delta2:delta) . (clause_name "pathDelta1") ==> 
( ( pathDelta  ( delta2  ++  (Strbind xi s)  ::  delta1 )  (Mid xi)  (sstrengthen  s   (Mid xi) )  )))

/\ ( (* pathDelta2 *)  !(delta:delta) (p:p) (x:name) (s:s) (d1:d) (i:stamp) (d2:d) . (clause_name "pathDelta2") /\
(( ( pathDelta delta p (Strexp  (d_append  d1   (Strbind (Id x i) s)   d2 ) ) )))
 ==> 
( ( pathDelta delta (Mpath p x)  (msubst_s (build_msubst_d  p   d1 )  s )  )))

`;

(* defns reduce *)

val (reduce_rules, reduce_ind, reduce_cases) = Hol_reln `
(* defn redM *)

( (* redMvar *)  !(delta1:delta) (vi:ident) (V:M) (delta2:delta) . (clause_name "redMvar") /\
((is_V_of_M V))
 ==> 
( ( redM  ( delta2  ++  (Valbind vi V)  ::  delta1 )  (Var vi) V )))

/\ ( (* redMpath *)  !(delta:delta) (p:p) (v:name) (V:M) (dV1:d) (i:stamp) (dV2:d) . (clause_name "redMpath") /\
((is_V_of_M V) /\
(is_dV_of_d dV1) /\
(is_dV_of_d dV2) /\
( ( pathDelta delta p (Strexp  (d_append  dV1   (Valbind (Id v i) V)   dV2 ) ) )))
 ==> 
( ( redM delta (Vpath p v)  (msubst_M (build_msubst_d  p   dV1 )  V )  )))

/\ ( (* redMapp *)  !(delta:delta) (vi:ident) (Ty:Ty) (M:M) (V:M) . (clause_name "redMapp") /\
((is_V_of_M V) /\
(is_V_of_M V))
 ==> 
( ( redM delta (Fapp  (Fun vi Ty M)  V)  (vsubst_M  V   vi   M )  )))

/\ ( (* redMlet *)  !(delta:delta) (dV:d) (vi:ident) (Ty:Ty) (M:M) . (clause_name "redMlet") /\
((is_dV_of_d dV))
 ==> 
( ( redM delta (Letexp dV  (Fun vi Ty M) ) (Fun vi Ty (Letexp dV M)) )))

/\ ( (* redMapp_ctxt1 *)  !(delta:delta) (M1:M) (M2:M) (M3:M) . (clause_name "redMapp_ctxt1") /\
(( ( redM delta M1 M3 )))
 ==> 
( ( redM delta (Fapp M1 M2) (Fapp M3 M2) )))

/\ ( (* redMapp_ctxt2 *)  !(delta:delta) (V:M) (M1:M) (M2:M) . (clause_name "redMapp_ctxt2") /\
((is_V_of_M V) /\
( ( redM delta M1 M2 )))
 ==> 
( ( redM delta (Fapp V M1) (Fapp V M2) )))

/\ ( (* redMlet_ctxt1 *)  !(delta:delta) (d1:d) (M:M) (d2:d) . (clause_name "redMlet_ctxt1") /\
(( ( red_d delta d1 d2 )))
 ==> 
( ( redM delta (Letexp d1 M) (Letexp d2 M) )))

/\ ( (* redMlet_ctxt2 *)  !(delta:delta) (dV:d) (M1:M) (M2:M) . (clause_name "redMlet_ctxt2") /\
((is_dV_of_d dV) /\
( ( redM  (REVERSE (d_to_list  dV ) ++  delta )  M1 M2 )))
 ==> 
( ( redM delta (Letexp dV M1) (Letexp dV M2) )))

/\
(* defn red_c *)

( (* rec_c_str_ctxt *)  !(delta:delta) (xi:ident) (s1:s) (s2:s) . (clause_name "rec_c_str_ctxt") /\
(( ( red_s delta s1 s2 )))
 ==> 
( ( red_c delta (Strbind xi s1) (Strbind xi s2) )))

/\ ( (* rec_c_val_ctxt *)  !(delta:delta) (vi:ident) (M1:M) (M2:M) . (clause_name "rec_c_val_ctxt") /\
(( ( redM delta M1 M2 )))
 ==> 
( ( red_c delta (Valbind vi M1) (Valbind vi M2) )))

/\
(* defn red_d *)

( (* red_d_d_ctxt1 *)  !(delta:delta) (c1:c) (d:d) (c2:c) . (clause_name "red_d_d_ctxt1") /\
(( ( red_c delta c1 c2 )))
 ==> 
( ( red_d delta (dCons c1 d) (dCons c2 d) )))

/\ ( (* red_d_d_ctxt2 *)  !(delta:delta) (cV:c) (d1:d) (d2:d) . (clause_name "red_d_d_ctxt2") /\
((is_cV_of_c cV) /\
( ( red_d  ( cV  ::  delta )  d1 d2 )))
 ==> 
( ( red_d delta (dCons cV d1) (dCons cV d2) )))

/\
(* defn red_s *)

( (* red_s_path *)  !(delta:delta) (p:p) (sV:s) . (clause_name "red_s_path") /\
((is_sV_of_s sV) /\
( ( pathDelta delta p sV )))
 ==> 
( ( red_s delta (Path p) sV )))

/\ ( (* red_s_ftorapp *)  !(delta:delta) (xi:ident) (S:S) (s:s) (p:p) . (clause_name "red_s_ftorapp") ==> 
( ( red_s delta (Ftorapp  (Ftorexp xi S s)  p)  (subst_s  p   xi   s )  )))

/\ ( (* red_s_seal *)  !(delta:delta) (s:s) (S:S) . (clause_name "red_s_seal") ==> 
( ( red_s delta (Seal s S) s )))

/\ ( (* red_s_str_ctxt *)  !(delta:delta) (d1:d) (d2:d) . (clause_name "red_s_str_ctxt") /\
(( ( red_d delta d1 d2 )))
 ==> 
( ( red_s delta (Strexp d1) (Strexp d2) )))

/\ ( (* red_s_ftorapp_ctxt *)  !(delta:delta) (s1:s) (p:p) (s2:s) . (clause_name "red_s_ftorapp_ctxt") /\
(( ( red_s delta s1 s2 )))
 ==> 
( ( red_s delta (Ftorapp s1 p) (Ftorapp s2 p) )))

`;

(* defns deltaE *)

val (deltaE_rules, deltaE_ind, deltaE_cases) = Hol_reln `
(* defn deltaE *)

( (* deltaE1 *)  (clause_name "deltaE1") ==> 
( ( deltaE  []   []  )))

/\ ( (* deltaE2 *)  !(delta:delta) (cV:c) (E:E) (C:C) . (clause_name "deltaE2") /\
((is_cV_of_c cV) /\
( ( deltaE delta E )) /\
( ( type_c E cV C )))
 ==> 
( ( deltaE  ( cV  ::  delta )   ( C  ::  E )  )))

`;


val _ = export_theory ();