File Conform.ML

open Conform;


section "gext";

qed_goalw "gext_objD" thy [gext_def] 
"\<And>X. \<lbrakk>s\<le>|s'; globs s r = Some (oi, fs)\<rbrakk> \<Longrightarrow> \<exists>fs'. globs s' r = Some (oi, fs')"
 (K [Force_tac 1]);
bind_thm ("rev_gext_objD", permute_prems 0 1 gext_objD);

Goalw [init_obj_def] "init_obj G oi r s1\<le>|s2 \<Longrightarrow> \<exists>obj. globs s2 r = Some obj";
b y auto_tac (claset() addSDs [gext_objD], simpset());
qed "init_obj_gextD";

Goalw [gext_def] "s\<le>|s";
b y fast_tac (claset() delrules [fst_splitE]) 1;
qed "gext_refl";
AddSIs [gext_refl];
Addsimps [gext_refl];

qed_goalw "gext_gupd"  thy [gext_def]"\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
	 (K [Auto_tac]);
qed_goalw "gext_new" thy [init_obj_def] 
"\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s" (K [etac gext_gupd 1]);
Addsimps [gext_gupd,gext_new];
AddSEs   [gext_gupd,gext_new];

qed_goalw "gext_trans" thy [gext_def] "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
	(K [Force_tac 1]);
AddEs [gext_trans];

qed_goalw "gext_upd_gobj" thy [gext_def] 
"s\<le>|upd_gobj r n v s" (K [
	Auto_tac, case_tac "ra = r" 1,
	Auto_tac, case_tac "globs s r = None" 1, Auto_tac]);
AddSIs [gext_upd_gobj];

qed_goalw "gext_cong1" thy  [gext_def] 
	"set_locals l s1\<le>|s2 = s1\<le>|s2" (K [Auto_tac]);
qed_goalw "gext_cong2" thy  [gext_def] 
	"s1\<le>|set_locals l s2 = s1\<le>|s2" (K [Auto_tac]);
Addsimps [gext_cong1, gext_cong2];

qed_goalw "gext_lupd1" thy [gext_def]
	"lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2" (K [Auto_tac]);
qed_goalw "gext_lupd2" thy [gext_def]
	"s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2" (K [Auto_tac]);
Addsimps [gext_lupd1, gext_lupd2];

Goalw  [inited_def] "\<And>X. \<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')";
b y auto_tac (claset()addDs [gext_objD], simpset());
qed "inited_gext";


section "value conformance";

qed_goalw "conf_cong" thy [conf_def] 
	"G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" (K [Auto_tac]);
Addsimps [conf_cong];

qed_goalw "conf_lupd" thy [conf_def] 
	"G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" (K [Auto_tac]);
Addsimps [conf_lupd];

qed_goalw "conf_PrimT" thy [conf_def] 
"\<And>X. \<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t" (K [Auto_tac]);
Addsimps [conf_PrimT];

Goalw [conf_def] "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T";
b y rtac val_.induct 1;
b y     Auto_tac;
qed_spec_mp "conf_litval";

qed_goalw "conf_Null" thy [conf_def] 
"G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T" (K [Simp_tac 1]);
Addsimps [conf_Null];

qed_goalw "conf_Addr" thy [conf_def] 
 "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)" (K[Auto_tac]);
val conf_AddrI=full_simplify(simpset()) (conjI RS(exI RS (conf_Addr RS iffD2)));

Goalw [conf_def] "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T";
b y tyE_tac "T" 1;
b y  rtac prim_ty.induct 1;
b y    Auto_tac;
qed_spec_mp "defval_conf";
AddEs [defval_conf];

Goalw [conf_def] "G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'";
b y rtac val_.induct 1;
b y    auto_tac (claset() addEs[ws_widen_trans],simpset());
qed_spec_mp "conf_widen";
AddEs [conf_widen];

Goalw [gext_def,conf_def] "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T";
b y rtac val_.induct 1;
b y     ALLGOALS Force_tac;
qed_spec_mp "conf_gext";
AddEs [conf_gext];

Goalw [widens_def] "ws_prog G \<Longrightarrow> \<forall>Ts Ts'. list_all2 (conf G s) vs Ts \<longrightarrow> \
\ G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'";
b y induct_tac "vs" 1;
b y  ALLGOALS(EVERY'[Clarsimp_tac,ftac(list_all2_lengthD RS sym)]);
b y EVERY'[Asm_full_simp_tac, Clarify_tac, smp_tac 1] 1;
b y EVERY'[Clarsimp_tac,ftac(list_all2_lengthD RS sym)] 1;
b y Auto_tac;
qed_spec_mp "conf_list_widen";

Goalw [conf_def] "G,s\<turnstile>a'\<Colon>\<preceq>RefT T \<longrightarrow> a' = Null \<or> \
\(\<exists>a oi vs T'. a' = Addr a \<and> heap s a = Some (oi,vs) \<and> \
\              obj_ty (oi,vs) = T' \<and> G\<turnstile>T'\<preceq>RefT T)";
b y induct_tac "a'" 1;
b y     Auto_tac;
b y     ALLGOALS (dtac widen_PrimT);
b y Auto_tac;
qed_spec_mp "conf_RefTD";

section "lconf";

qed_goalw "lconfD" thy [lconf_def] 
   "\<And>X. \<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T" (K [Force_tac 1]);

qed_goalw "lconf_cong" thy [lconf_def] 
	"\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" (K [Auto_tac]);
Addsimps [lconf_cong];

qed_goalw "lconf_lupd" thy [lconf_def] 
"G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" (K [Auto_tac]);
Addsimps [lconf_lupd];

(* unused *)
qed_goalw "lconf_new" thy [lconf_def] 
"\<And>X. \<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" (K [
Auto_tac]);

qed_goalw "lconf_upd" thy [lconf_def] 
"\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow> \
\ G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" (K [Auto_tac]);


qed_goalw "lconf_ext" thy [lconf_def] 
"\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)" (K [Auto_tac]);

Goalw [lconf_def] 
 "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)";
b y Safe_tac;
b y   case_tac "n" 3;
b y    ALLGOALS (force_tac (claset(), simpset() addsplits [sum.split]));
qed "lconf_map_sum";
Addsimps[lconf_map_sum];

Goalw [lconf_def] "\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> \<forall>vs Ts. nodups vns \<longrightarrow> length Ts = length vns \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)";
b y induct_tac "vns" 1;
b y  ALLGOALS Clarsimp_tac;
b y ftac list_all2_lengthD 1;
b y Clarsimp_tac 1;
qed_spec_mp "lconf_ext_list";


qed_goalw "lconf_deallocL" thy [lconf_def] 
"\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L" 
	(K [Safe_tac, dtac spec 1, dtac ospec 1, Auto_tac]);

qed_goalw "lconf_gext" thy [lconf_def] 
	"\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L" (K [Fast_tac 1]);
AddEs [lconf_gext];

Goalw [lconf_def] "G,s\<turnstile>vs[\<Colon>\<preceq>]empty";
b y Force_tac 1;
qed "lconf_empty";
AddSIs [lconf_empty];
Addsimps [lconf_empty];

Goalw [lconf_def] 
	"\<And>X. \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs";
b y Force_tac 1;
qed "lconf_init_vals";
AddSIs [lconf_init_vals];


section "object conformance";

qed_goalw "oconf_def2" thy [oconf_def,Let_def] "G,s\<turnstile>(oi,fs)\<Colon>\<preceq>\<surd>r = \
\ (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and> (case r of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs)) | Stat C \<Rightarrow> True))"
	(K [Simp_tac 1]);

qed_goalw "oconf_is_type" thy [oconf_def,Let_def] 
	"\<And>X. G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
	(K [Auto_tac]);

val oconf_lconf = oconf_def2 RS iffD1 RS conjunct1;

qed_goalw "oconf_cong" thy [oconf_def,Let_def] 
	"G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r" (K [Auto_tac]);
Addsimps [oconf_cong];

Goal "\<And>X. \<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C); \
\ \<And>C c f m T. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some (m, T) \<rbrakk>\
\           \<Longrightarrow> is_type G T; \
\(case r of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs)) | Stat C \<Rightarrow> is_class G C)\<rbrakk> \<Longrightarrow>\
\ G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r";
b y auto_tac (claset()  ,simpset() addsimps [oconf_def2]);
b y  dtac (var_tys_Some_eq RS iffD1) 1;
b y  stac obj_ty_eq 2;
b y auto_tac (claset() addSDs [fields_table_SomeD],simpset() 
      addsplits [sum.split_asm, obj_tag.split_asm]);
qed "oconf_init_obj_lemma";

section "conforms";

qed_goalw "conforms_globsD" thy [conforms_def, Let_def]
 "\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi,fs)\<rbrakk> \<Longrightarrow> G,s\<turnstile>(oi,fs)\<Colon>\<preceq>\<surd>r" 
	(K [Auto_tac]);

qed_goalw "conforms_localD" thy [conforms_def, Let_def]
	 "\<And>X. (x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L" 
	(K [Asm_full_simp_tac 1]);

qed_goalw "conforms_XcptLocD" thy [conforms_def, Let_def] 
	"\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (XcptLoc a)\<rbrakk> \<Longrightarrow> \
	\ G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)"
	(K [Asm_full_simp_tac 1]);

Goal "\<lbrakk>G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x2,s2) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> \
\ \<exists>a oi vs. a' = Addr a \<and> globs s2 (Inl a) = Some (oi, vs) \<and> \
\ G\<turnstile>obj_ty (oi, vs)\<preceq>RefT t \<and> is_type G (obj_ty (oi, vs))";
b y EVERY'[dtac conf_RefTD, Clarsimp_tac] 1;
b y eatac (conforms_globsD RS oconf_is_type) 1 1;
qed "conforms_RefTD";

qed_goalw "conforms_StdXcpt" thy [conforms_def]
   "((Some (StdXcpt xn), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
	(K [Asm_full_simp_tac 1]);
AddIffs [conforms_StdXcpt];

qed_goalw "conforms_raise_if" thy [xcpt_if_def]
   "\<And>s. ((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
	(K [Auto_tac]);
AddIffs [conforms_raise_if];


qed_goalw "conforms_NormI" thy [conforms_def, Let_def]
   "\<And>X. (x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)" (K [Auto_tac]);

qed_goalw "conformsI" thy [conforms_def, Let_def] 
"\<And>X. \<lbrakk>\<forall>r. \<forall>(oi,fs)\<in>globs s r: G,s\<turnstile>(oi,fs)\<Colon>\<preceq>\<surd>r; \
\     G,s\<turnstile>locals s[\<Colon>\<preceq>]L; \
\     \<forall>a. x = Some (XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow>\
\ (x, s)\<Colon>\<preceq>(G, L)" (K [Auto_tac]);

qed_goal "conforms_xconf" thy "\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G,L);  \
\\<forall>a. x' = Some (XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow>  \
\     (x',s)\<Colon>\<preceq>(G,L)" (K [fast_tac 
  (claset() addSIs [conformsI] addDs[conforms_globsD,conforms_localD]) 1]);


qed_goal "conforms_lupd" thy "\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T;\
\ G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)" (K [
	force_tac (claset() addSIs [conformsI, lconf_upd]
     addDs [conforms_globsD, conforms_localD, conforms_XcptLocD],
	simpset() addsimps[oconf_def2]) 1]);

qed_goal "conforms_allocL" thy 
"\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))"
    (K [force_tac (claset() addSIs [conformsI] addDs [conforms_globsD]
	addSEs [conforms_localD RS lconf_ext, conforms_XcptLocD],
		simpset() addsimps[oconf_def2]) 1]);

qed_goal "conforms_deallocL" thy 
"\<And>s. \<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
    (K [split_all_tac 1, fast_tac (claset() addSIs [conformsI]
	   addDs [conforms_globsD]
	 addSEs [conforms_localD RS lconf_deallocL, conforms_XcptLocD]) 1]);

Goal "\<And>X. \<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s'; \
\ \<forall>r. \<forall>(oi,fs)\<in>globs s' r: G,s'\<turnstile>(oi,fs)\<Colon>\<preceq>\<surd>r; \
\  locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)";
b y force_tac (claset() addSIs [conformsI] 
       addDs [conforms_localD, conforms_XcptLocD],simpset()) 1;
qed "conforms_gext";

Goal "\<And>s s'. \<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)";
b y etac conforms_xconf 1;
b y fast_tac (claset() addDs [conforms_XcptLocD]) 1;
qed "conforms_xgext";

Goal "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>|gupd(r\<mapsto>obj)s\<rbrakk> \<Longrightarrow> \
\ (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)";
b y rtac conforms_gext 1;
b y    Auto_tac;
b y  ALLGOALS (force_tac (claset() addDs [conforms_globsD],
		           simpset() addsimps[oconf_def2]));
qed "conforms_gupd";

Goal "\<And>X. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, vs); \
\ var_tys G oi r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)";
b y rtac conforms_gext 1;
b y    Auto_tac;
b y  ALLGOALS (force_tac (claset() addDs [conforms_globsD] addSIs [lconf_upd],
         simpset() addsimps[oconf_def2] delcongs[thm "sum.weak_case_cong"]));
qed "conforms_upd_gobj";

Goal "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)";
b y auto_tac (claset() addSIs [conformsI]
	   addDs [conforms_globsD] addSEs [conforms_XcptLocD],
	simpset() addsimps[oconf_def2]);
qed"conforms_set_locals";

Goal "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow> \
\ (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)";
b y rtac conforms_xconf 1;
b y  force_tac (claset() addDs [conforms_XcptLocD],simpset()) 2;
b y etac conforms_gext 1;
b y   ALLGOALS(force_tac (claset() addDs [conforms_globsD],simpset()));
qed "conforms_return";