File TypeSafe.ML

open TypeSafe;

section "fits & conf";
(* unused *)
Goalw [fits_def] "\<And>X. G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T";
b y Clarify_tac 1;
b y EVERY[etac swap 1, Full_simp_tac 1];
b y dtac conf_RefTD 1;
b y Auto_tac;
qed "conf_fits";

Goal "\<And>X. \<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'";
b y auto_tac (claset() addSDs [fitsD, cast_PrimT2, cast_RefT2],simpset());
b y force_tac (claset() addDs [conf_RefTD] addIs [conf_AddrI],simpset()) 1;
qed "fits_conf";

Goal "\<And>X. \<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> \
\ G,s\<turnstile>v\<Colon>\<preceq>T'";
b y auto_tac (claset() addSDs [fitsD, widen_ArrayPrimT, 
					widen_ArrayRefT],simpset());
b y force_tac (claset() addDs [conf_RefTD] addIs [conf_AddrI],simpset()) 1;
qed "fits_Array";



section "gext";

Goal "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2";
b y split_all_tac 1;
b y etac halloc.induct 1;
b y  auto_tac (claset() addSDs [new_AddrD], simpset());
qed "halloc_gext";

Goal "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2";
b y split_all_tac 1;
b y etac sxalloc.induct 1;
b y   auto_tac (claset() addSDs [halloc_gext],simpset());
qed "sxalloc_gext";

Goal "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> snd s\<le>|snd s' \<and> (case w of \
\   In1 v \<Rightarrow> (\<forall>C. t = In1r (init C) \<longrightarrow> normal s \<longrightarrow> initd C s') \
\ | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s))) \
\ | In3 vs \<Rightarrow> True)";
b y rtac eval_induct 1;
b y ALLGOALS (clarsimp_tac (claset(), simpset() addsimps [lvar_def]
   delsplits [split_if_asm,option.split_asm] addsplits [sum3.split]));
(* 15 subgoals *)
b y force_tac(claset() addSDs [sxalloc_gext], 
		simpset() addsimps [Let_def]) 12; (* Try *)
b y TRYALL (force_tac (claset() addSEs [init_obj_gextD] 
 addSDs [halloc_gext,gext_new], simpset() delsplits [split_if_asm]
			addsimps[fvar_def2,avar_def2]));
b y   Force_tac 1; (* If? *)
(* Init,Call *)
b y  case_tac "inited C (globs s0)" 1;
b y   Clarsimp_tac 1;
b y  auto_tac(claset() addSEs [inited_gext] addSDs [],
 simpset()delsplits[split_if_asm]addsimps[init_lvars_def2]);
b y  ALLGOALS (dtac not_initedD);
b y  fast_tac (claset() addSDs [gext_new]) 1;
b y fast_tac (claset() addIs [inited_gext]) 1;
qed_spec_mp "eval_gext_lemma";


qed_goal "evar_gext_f" thy 
  "\<And>X. G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
  (K [dtac (eval_gext_lemma RS conjunct2) 1, Auto_tac]);
val eval_gext = eval_gext_lemma RS conjunct1;
Goal "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2";
b y dtac eval_gext 1;
b y Auto_tac;
qed "eval_gext'";

Goal "G\<turnstile>Norm s1 \<midarrow>init C\<rightarrow> s2 \<Longrightarrow> initd C s2";
b y dtac (eval_gext_lemma RS conjunct2) 1;
b y Auto_tac;
qed "init_yields_initd";


section "Lemmas";

Goalw [init_comp_ty_def] 
"is_type G T \<Longrightarrow> (G,L)\<turnstile>init_comp_ty T\<Colon>\<surd>";
b y Clarsimp_tac 1;
qed "wt_init_comp_ty";

Goal "\<And>X. \<lbrakk>wf_prog G; \
\(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() addSIs[oconf_init_obj_lemma,unique_fields] ,simpset());
qed "oconf_init_obj";

Goalw [init_obj_def] "\<And>X. \<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);  \
\ wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs)) \
\                       | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow> \
\ (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)";
b y auto_tac (claset() addSEs [conforms_gupd,oconf_init_obj], simpset());
qed "conforms_newG";

Goal"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; ¬ inited C (globs s)\<rbrakk> \<Longrightarrow> \
\ (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"; 
b y rtac (not_initedD RS conforms_newG) 1;
b y    Auto_tac;
qed "conforms_init_class_obj";


Goal "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = \
\ (if m then x else (np a') x)";
b y simp_tac (simpset() addsimps [init_lvars_def2]) 1;
qed "fst_init_lvars";
Addsimps [fst_init_lvars];

Goal "\<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); \
\ is_type G (obj_ty (oi,fs))\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)";
b y pair_tac "s1" 1;
b y case_tac "x" 1;
b y  auto_tac (claset() addSEs halloc_elim_cases addSDs [new_AddrD] addSIs 
 [conforms_newG RS conforms_xconf,conf_AddrI], simpset());
qed "halloc_conforms";

Goal "\<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); \
\ T = obj_ty (oi,fs); is_type G T\<rbrakk> \<Longrightarrow> \
\ s2\<Colon>\<preceq>(G, L) \<and> (\<lambda>(x',s'). x' = None \<longrightarrow> G,s'\<turnstile>Addr a\<Colon>\<preceq>T) s2";
b y auto_tac (claset() addSEs [halloc_conforms], simpset());
b y pair_tac "s1" 1;
b y case_tac "x" 1;
b y stac obj_ty_eq 1;
b y  auto_tac (claset() addSEs halloc_elim_cases addSDs [new_AddrD]
			addSIs [conf_AddrI], simpset());
qed "halloc_type_sound";

Goal "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> case fst s1 of \
\ None \<Rightarrow> s2 = s1 | Some x \<Rightarrow> \
\ (\<exists>a. fst s2 = Some(XcptLoc a) \<and> (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))";
b y split_all_tac 1;
b y etac sxalloc.induct 1;
b y   Auto_tac;
b y rtac (halloc_conforms RS conforms_xconf) 1;
b y     auto_tac (claset() addSEs halloc_elim_cases addSDs [new_AddrD]
  addSIs [conf_AddrI], simpset());
qed "sxalloc_type_sound";


Delsimps [fun_upd_apply];
simpset_ref():=simpset() delsimps [split_paired_All,split_paired_Ex] 
		 delsplits [split_if    , option.split    ]
		 delsplits [split_if_asm, option.split_asm]
		 delloop "split_all_tac";
claset_ref ():=claset()  delSWrapper "split_all_tac";

Addsimps [fun_upd_same];

Goalw [DynT_prop_def]
 "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT t; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> \<Longrightarrow> \
\ G\<turnstile>mode\<rightarrow>target mode s a' cT\<preceq>t";
b y Clarsimp_tac 1;
b y datac conforms_RefTD 2 1;
b y Clarsimp_tac 1;
b y ftac obj_ty_widenD 1;
b y auto_tac (claset() addSDs [widen_Array,widen_Array2], 
		simpset() addsplits[split_if]);
qed "DynT_propI";

fun exhaust_cmethd_tac s = EVERY'[
	res_inst_tac [("p",s)] PairE, rename_tac "md' j0",
	res_inst_tac [("p","j0")] PairE, rename_tac "j00 j1",
	res_inst_tac [("p","j1")] PairE, rename_tac "lvars body",
	res_inst_tac [("p","body")] PairE, rename_tac "blk res",
	res_inst_tac [("p","j00")] PairE, rename_tac "m' j2",
	res_inst_tac [("p","j2")] PairE, rename_tac "pns' rT'",
	hyp_subst_tac, K prune_params_tac];

Goalw [DynT_prop_def]    
"\<lbrakk>the (cmethd G dynT sig)=(md,(m',pns,rT),lvars,bdy); G\<turnstile>invmode m e\<rightarrow>dynT\<preceq>t;\
\ wf_prog G; (G, L)\<turnstile>e\<Colon>-RefT t; (cT, m, pnsa, T) \<in> mheads G t sig;\
\ target (invmode m e) s2 a' cT = dynT\<rbrakk> \<Longrightarrow> \
\ cmethd G dynT sig = Some (md, (m, pns, rT), lvars, bdy) \<and> G\<turnstile>rT\<preceq>T \<and> m' = m \<and>\
\ wf_mdecl G md (sig, (m, pns, rT), lvars, bdy) \<and> \
\ is_class G dynT \<and> G\<turnstile>dynT\<preceq>C md \<and> is_class G md \<and> \
\(invmode m e \<noteq> IntVir \<longrightarrow> (\<exists>C. t=ClassT C \<and> G\<turnstile>C \<preceq>C md) \<and> cT = ClassT md)";
b y fatac ty_expr_is_type 1 1;
b y EVERY'[case_tac "invmode m e = IntVir" THEN_ALL_NEW 
	clarsimp_tac (claset(), simpset() addsimps [target_notIntVir])] 1;
b y  ALLGOALS (clarsimp_tac (claset(), simpset() addsimps [invmode_IntVir_eq]));
b y  datac class_mheadsD 4 1;
b y  EVERY'[datac static_mheadsD 3, 
	    Clarsimp_tac, ftac cmethd_defpl, etac wf_ws_prog, Asm_simp_tac] 2;
b y  ALLGOALS (EVERY'[Clarsimp_tac, datac cmethd_wf_mdecl 2, Clarsimp_tac]);
qed "DynT_mheadsD";

Goal "\<lbrakk>G\<turnstile>target mode s2 a' cT\<preceq>C md; wf_prog G; \
\ G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; mode = IntVir \<longrightarrow> a' \<noteq> Null; \
\ mode \<noteq> IntVir \<longrightarrow> (\<exists>C. t=ClassT C \<and> G\<turnstile>C\<preceq>C md) \<and> cT = ClassT md\<rbrakk>\<Longrightarrow>\
\ G,s2\<turnstile>a'\<Colon>\<preceq>Class md";
b y (case_tac "mode \<noteq> IntVir" THEN_ALL_NEW Clarsimp_tac) 1;
b y  eatac (widen.subcls RS conf_widen) 1 1;
b y  etac wf_ws_prog 1;
b y dtac conf_RefTD 1;
b y Clarsimp_tac 1;
b y etac conf_AddrI 1;
b y rewtac obj_class_def;
b y auto_tac (claset(), simpset() addsplits [obj_tag.split_asm]);
qed "DynT_conf";

Goal "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2; G,s2\<turnstile>v\<Colon>\<preceq>T'; s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and> (\<lambda>(x',s'). x' = None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T') (assign f v (Norm s2))";
b y dres_inst_tac [("x","None"),("s","s2"),("v","v")] evar_gext_f 1;
b y EVERY'[dtac eval_gext', Clarsimp_tac] 1;
b y etac conf_gext 1;
b y Asm_full_simp_tac 1;
qed "Ass_lemma";

Goal "\<lbrakk>G\<turnstile>tn\<preceq>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L); \
\   x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq>Class tn\<rbrakk> \<Longrightarrow> xupd (throw a') (x1, s1)\<Colon>\<preceq>(G, L)"; 
b y auto_tac (claset(), simpset() addsplits[split_xcpt_if]addsimps[throw_def2]);
b y etac conforms_xconf 1;
b y ftac conf_RefTD 1;
b y auto_tac (claset()addEs[widen.subcls RS conf_widen], simpset());
qed "Throw_lemma";

Goal "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; (Some (XcptLoc a), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))";
b y rtac conforms_allocL 1;
b y  etac conforms_NormI 1;
b y EVERY'[dtac (conforms_XcptLocD RS conf_RefTD), rtac refl] 1;
b y auto_tac (claset() addEs [conf_AddrI],simpset());
qed "Try_lemma";

Goal "\<And>s2. \<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2; wf_prog G; (x1, s1)\<Colon>\<preceq>(G, L); s2\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> \
\ xupd (xcpt_if (\<exists>y. x1 = Some y) x1) s2\<Colon>\<preceq>(G, L)";
b y split_all_tac 1;
b y force_tac (claset() addEs [eval_gext', conforms_xgext], 
	simpset()addsplits[split_xcpt_if]) 1;
qed "Fin_lemma";

Goal "\<lbrakk>table_of (fields G Ca) (fn, C) = Some (stat, fT); x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; \
\ wf_prog G; class G Ca = Some y; G\<turnstile>Ca\<preceq>C C; C \<noteq> Object; class G C = Some ya; \
\ (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1); (if stat then id else np a) x2 = None\<rbrakk> \<Longrightarrow> \
\ \<exists>oi fs. globs s2 (if stat then Inr C else Inl (the_Addr a)) = Some (oi,fs) \<and>\
\ var_tys G oi (if stat then Inr C else Inl(the_Addr a)) (Inl(fn,C)) = Some fT";
b y dtac initedD 1;
b y (case_tac "stat" THEN_ALL_NEW Clarsimp_tac) 1;
b y  EVERY'[datac rev_gext_objD 1, Clarsimp_tac] 1;
b y  EVERY'[ftac fields_defpl, etac wf_ws_prog, Asm_simp_tac] 1;
b y  rtac (var_tys_Some_eq RS iffD2) 1;
b y  Clarsimp_tac 1;
b y  EVERY'[etac fields_table_SomeI, Simp_tac] 1;
b y EVERY'[dtac conf_RefTD, Clarsimp_tac, rtac (var_tys_Some_eq RS iffD2)] 1;
b y auto_tac (claset() addSDs [widen_Array], simpset()addsplits[obj_tag.split]);
b y rtac fields_table_SomeI 1;
b y auto_tac (claset() addSEs [fields_mono, subcls_is_class], simpset());
qed "FVar_lemma1";

Goal "\<lbrakk>(v, Norm s2') = fvar C stat fn a (x2, s2); class G Ca = Some y; G\<turnstile>Ca\<preceq>C C; \
\ table_of (fields G Ca) (fn, C) = Some (stat, fT); wf_prog G;  \
\ x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C \<noteq> Object; class G C = Some ya;  \
\ (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1)\<rbrakk> \<Longrightarrow> \
\ G,s2'\<turnstile>fst v\<Colon>\<preceq>fT \<and> (\<forall>s'. Norm s'\<Colon>\<preceq>(G, L) \<longrightarrow> \
\ (\<forall>w. G,s'\<turnstile>w\<Colon>\<preceq>fT \<longrightarrow> s2'\<le>|s' \<longrightarrow> assign (snd v) w (Norm s')\<Colon>\<preceq>(G, L)))";
b y dtac sym 1;
b y clarsimp_tac (claset(), simpset() addsimps [fvar_def2]) 1;
b y datac FVar_lemma1 10 1;
b y EVERY'[Clarsimp_tac, datac (conforms_globsD RS oconf_lconf RS lconfD) 2] 1;
b y Clarsimp_tac 1;
b y EVERY'[datac rev_gext_objD 1,fast_tac (claset()addSEs[conforms_upd_gobj])]1;
qed "FVar_lemma";

Goal "\<lbrakk>globs s2 (Inl a) = Some (Arr ty i, vs); #0 \<le> the_Intg i'; the_Intg i' < i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s2\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> G,s2\<turnstile>the (vs (Inr (the_Intg i')))\<Colon>\<preceq>Tb";
b y etac (widen_Array_Array RS conf_widen) 1;
b y  etac wf_ws_prog 2;
b y datac (conforms_globsD RS oconf_lconf RS lconfD) 1 1 THEN atac 2;
b y force_tac (claset() addIs [var_tys_Some_eq RS iffD2], simpset()) 1;
qed "AVar_lemma1";

Goal "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2); (v, Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[]; (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>fst v\<Colon>\<preceq>Ta \<and> (\<forall>s'. Norm s'\<Colon>\<preceq>(G, L) \<longrightarrow> (\<forall>w. G,s'\<turnstile>w\<Colon>\<preceq>Ta \<longrightarrow> s2'\<le>|s' \<longrightarrow> assign (snd v) w (Norm s')\<Colon>\<preceq>(G, L)))";
b y dtac sym 1;
b y clarsimp_tac (claset(), simpset() addsimps [avar_def2]) 1;
b y datac conf_gext 1 1;
b y EVERY'[dtac conf_RefTD, Clarsimp_tac] 1;
b y EVERY'[ftac obj_ty_widenD, SELECT_GOAL 
		(auto_tac (claset() addSDs [widen_Class], simpset()))] 1;
b y  eatac AVar_lemma1 5 1;
b y force_tac (claset() addEs [fits_Array] addDs [gext_objD] addIs 
   [var_tys_Some_eq RS iffD2,conforms_upd_gobj],simpset() addsplits[split_if])1;
qed "AVar_lemma";


section "Call";

Goalw [wf_mhead_def] "\<lbrakk>wf_prog G; \
\ wf_mhead G (mn,pTs) (m,pns,rT); Ball (set lvars) (split (\<lambda>vn. is_type G));\
\ list_all2 (conf G s2) pvs pTsa; G\<turnstile>pTsa[\<preceq>]pTs\<rbrakk> \<Longrightarrow> \
\ G,s2\<turnstile>init_vals (table_of lvars)(pns[\<mapsto>]pvs)[\<Colon>\<preceq>]table_of lvars(pns[\<mapsto>]pTs)";
b y Clarify_tac 1;
b y eatac (Ball_set_table RS lconf_init_vals RS lconf_ext_list) 2 1;
b y dtac wf_ws_prog 1;
b y eatac conf_list_widen 2 1;
qed "conforms_init_lvars_lemma";

Goal "\<lbrakk>wf_mhead G (mn, pTs) (m, pns', rT'); wf_prog G; \
\ Ball (set lvars) (split (\<lambda>vn. is_type G)); \
\ list_all2 (conf G s2) pvs pTsa; G\<turnstile>pTsa[\<preceq>] pTs; \
\ (x2, s2)\<Colon>\<preceq>(G, L); cmethd G (target (invmode m e) s2 a' cT) (mn, pTs) = \
\ Some (md, (ma, pns', rT'), lvars, blk, res); \
\ G\<turnstile>target (invmode m e) s2 a' cT\<preceq>C md; G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; \
\ invmode m e = IntVir \<longrightarrow> a' \<noteq> Null; invmode m e \<noteq> IntVir \<longrightarrow> \
\ (\<exists>C. t = ClassT C \<and> G\<turnstile>C\<preceq>C md) \<and> cT = ClassT md\<rbrakk> \<Longrightarrow> \
\ init_lvars G (target (invmode m e) s2 a' cT) (mn, pTs) (invmode m e) a' \
\ pvs (x2,s2)\<Colon>\<preceq>(G, table_of lvars(pns'[\<mapsto>]pTs) (+)¬m ?\<mapsto>Class md)";
b y asm_full_simp_tac (simpset() addsimps [init_lvars_def2]) 1;
b y rtac conforms_set_locals 1;
b y  asm_simp_tac (simpset() addsplits [split_if]) 1;
b y datac DynT_conf 4 1;
b y (case_tac "m" THEN_ALL_NEW Asm_full_simp_tac) 1;
b y  rtac conjI 2;
b y   EVERY'[rtac lconf_ext, Simp_tac, atac] 3;
b y  ALLGOALS (eatac conforms_init_lvars_lemma 4);
qed "conforms_init_lvars";

val prems = goal thy "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2, s2); \
\ C = target (invmode m e) s2 a' cT; \
\ s2' = init_lvars G C (mn, pTs) (invmode m e) a' pvs (x2,s2);\
\ G\<turnstile>s2' \<midarrow>Methd C (mn, pTs)-\<succ>v\<rightarrow> (x3, s3);   \
\ \<forall>L. s2'\<Colon>\<preceq>(G, L) \<longrightarrow> (\<forall>T. (G, L)\<turnstile>Methd C (mn, pTs)\<Colon>-T \<longrightarrow> \
\  (x3, s3)\<Colon>\<preceq>(G, L) \<and> (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>T)); \
\ Norm s0\<Colon>\<preceq>(G, L); (G, L)\<turnstile>e\<Colon>-RefT t; (G, L)\<turnstile>ps\<Colon>\<doteq>pTsa; \
\ max_spec G t (mn, pTsa) = {((cT, m, pns, rT), pTs)}; (x1, s1)\<Colon>\<preceq>(G, L);\
\ x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq>RefT t; (x2, s2)\<Colon>\<preceq>(G, L); \
\ x2 = None \<longrightarrow> list_all2 (conf G s2) pvs pTsa\<rbrakk> \<Longrightarrow>    \
\ (x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) \<and> (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>rT)";
b y cut_facts_tac prems 1;
b y hyp_subst_tac 1;
b y case_tac "x2" 1;
b y  EVERY'[REPEAT o thin_All_tac, clarsimp_tac(claset(),simpset() 
     addsplits[split_if_asm] addsimps[init_lvars_def2])] 2;
b y case_tac "a' = Null \<and> ¬ m \<and> e \<noteq> Super" 1;
b y  clarsimp_tac (claset(), simpset() addsimps[init_lvars_def2]) 1;
b y Clarsimp_tac 1;
b y dtac eval_gext' 1;
b y fatac conf_gext 1 1;
b y EVERY'[dtac max_spec2mheads, Clarsimp_tac] 1;
b y subgoal_tac "invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" 1;
b y  clarsimp_tac (claset(),simpset() addsimps [invmode_IntVir_eq]) 2;
b y EVERY'[exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s2 a' cT) (mn, pTs))", Clarsimp_tac] 1;
b y EVERY'[datac (DynT_propI RSN (2, DynT_mheadsD)) 7, rtac refl]1;
b y Clarify_tac 1;
b y EVERY'[dtac wf_mdeclD1, Clarsimp_tac] 1;
b y EVERY'[datac conforms_init_lvars 10, smp_tac 1] 1;
b y EVERY'[fatac wt_MethdI 2, Clarsimp_tac] 1;
b y smp_tac 1 1;
b y EVERY'[Clarify_tac, rtac conjI] 1;
b y  eatac conforms_return 1 1;
b y  force_tac (claset() addSDs [eval_gext] 
		delrules [impCE],simpset() addsimps [init_lvars_def2]) 1;
b y Clarsimp_tac 1;
b y etac(permute_prems 0 1 conf_widen) 1;
b y  etac wf_ws_prog 1;
b y eatac widen_trans 2 1;
qed "Call_type_sound";


section "TypeSafe";

val forward_hyp_tac = EVERY' [smp_tac 1,
	FIRST'[mp_tac,etac exI,smp_tac 1,EVERY'[etac impE,etac exI]],
	REPEAT o (etac conjE)];
val typD_tac = eresolve_tac wt_elim_cases THEN_ALL_NEW 
	EVERY' [full_simp_tac (simpset() setloop (K no_tac)), Clarify_tac];

Goal "\<And>X. wf_prog G \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1) \<longrightarrow> (\<forall>L. s0\<Colon>\<preceq>(G,L) \<longrightarrow>   \
\ (\<forall>T. (G,L)\<turnstile>t\<Colon>T \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (let (x,s) = s1 in x = None \<longrightarrow> (case T of \
\   Inl T  \<Rightarrow> if (\<exists>vf. t=In2 vf) then G,s\<turnstile>fst(the_In2 v)\<Colon>\<preceq>T \<and> \
\                         (\<forall>s' w. Norm s'\<Colon>\<preceq>(G,L) \<longrightarrow> G,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> \
\                                   assign (snd (the_In2 v)) w (Norm s')\<Colon>\<preceq>(G,L))\
\             else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T \
\ | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts))))";
b y rtac eval_induct 1;

(* 27 subgoals *)
(* Xcpt, Inst, Acc, Methd, Nil, Skip, Expr, Comp *)
b y         ALLGOALS (full_simp_tac (simpset() addsimps [Let_def,body_def]));
b y       ALLGOALS (EVERY'[Clarify_tac, TRY o typD_tac, TRY o forward_hyp_tac]);
b y      ALLGOALS (EVERY'[Asm_simp_tac,TRY o Clarify_tac]);

(* 19 subgoals *)
(* Cons *)
b y thin_tac "G\<turnstile>Norm s0 \<midarrow>?ea\<succ>\<rightarrow> ?vs1" 1;
b y ftac eval_gext' 1;
b y Force_tac 1;

(* LVar *)
b y force_tac (claset() addEs [conforms_localD RS lconfD, conforms_lupd],
		simpset() addsimps[lvar_def]) 1;

(* Cast *)
b y force_tac (claset() addDs [fits_conf], simpset()) 1;

(* Lit *)
b y rtac conf_litval 1;
b y asm_full_simp_tac (simpset() addsimps [empty_dt_def]) 1;

(* Super *)
b y rtac conf_widen 1;
b y   eatac (subcls_direct RS widen.subcls) 1 1;
b y  eatac (conforms_localD RS lconfD) 1 1;
b y etac wf_ws_prog 1;

(* Body *) 
b y forward_hyp_tac 1;
b y forward_hyp_tac 1;
b y Asm_full_simp_tac 1;

(* Cond *)
b y (split_asm_tac [split_if_asm] THEN_ALL_NEW 
	EVERY'[Asm_full_simp_tac, forward_hyp_tac, Force_tac]) 1;

(* If *)
b y force_tac (claset(), simpset() addsplits [split_if_asm]) 1;

(* Loop *)
b y datac wt.Loop 1 1;
b y (split_asm_tac [split_if_asm] THEN_ALL_NEW EVERY'[
	Asm_full_simp_tac, Clarsimp_tac]) 1;

(* Fin *)
b y EVERY'[case_tac "x1", Force_tac] 1;
b y EVERY'[dtac spec, etac impE, etac conforms_NormI] 1;
b y mp_tac 1;
b y (etac Fin_lemma THEN_ALL_NEW atac) 1;

(* Throw *)
b y (etac Throw_lemma THEN_ALL_NEW atac) 1;

(* NewC *)
b y (etac halloc_type_sound THEN_ALL_NEW Force_tac) 1;

(* NewA *)
b y EVERY' [smp_tac 1, ftac wt_init_comp_ty, mp_tac] 1;
b y forward_hyp_tac 1;
b y (case_tac "check_neg i' x2" THEN_ALL_NEW Clarsimp_tac) 1;
b y  (etac halloc_type_sound THEN_ALL_NEW Force_tac) 1;
b y Force_tac 1;

(* Level 33, 6 subgoals *)

(* Init *)
b y (split_asm_tac [split_if_asm] THEN_ALL_NEW Clarsimp_tac) 1;
b y fatac wf_prog_cdecl 1 1;
b y EVERY'[dtac spec, etac impE, eatac conforms_init_class_obj 3] 1; 
b y EVERY'[dres_inst_tac [("psi","class G C = ?x")] asm_rl, etac impE,
	   thin_All_tac, force_tac (claset()addSDs[wf_cdecl_supD], 
		simpset()addsplits[split_if])] 1;
b y EVERY'[dtac spec, etac impE, etac conforms_set_locals, rtac lconf_empty] 1; 
b y EVERY'[etac impE, etac wf_cdecl_wt_init] 1;
b y EVERY'[eatac conforms_return 1, 
	   force_tac (claset() addDs [eval_gext'],simpset())] 1;

(* Ass *)
b y forward_hyp_tac 1;
b y case_tac "x1" 1;
b y  Force_tac 2;
b y case_tac "x2" 1;
b y  Force_tac 2;
b y EVERY'[Asm_full_simp_tac, dtac conjunct2] 1;
b y datac conf_widen 1 1;
b y  etac wf_ws_prog 1;
b y forward_hyp_tac 1;
b y eatac Ass_lemma 3 1;

(* Try *)
b y EVERY'[datac sxalloc_type_sound 1, Full_simp_tac] 1;
b y (split_asm_tac [option.split_asm] THEN_ALL_NEW Clarsimp_tac) 1;
b y smp_tac 1 1;
b y asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1;
b y fast_tac (claset() addDs [conforms_deallocL,Try_lemma]) 1;

(* FVar *)
b y ftac cfield_fields 1;
b y fatac (ty_expr_is_type RS type_is_class) 1 1;
b y ftac wf_ws_prog 1;
b y fatac fields_defpl 2 1;
b y Clarsimp_tac 1;
(*b y EVERY'[datac cfield_defpl_is_class 2, Clarsimp_tac] 1; not useful here*)
b y smp_tac 1 1;
b y forward_hyp_tac 1;
b y EVERY'[rtac conjI, force_tac (claset(), simpset() addsplits [split_if]
		addsimps [fvar_def2])] 1;
b y EVERY'[dtac init_yields_initd, ftac eval_gext'] 1;
b y Clarsimp_tac 1;
b y case_tac "C=Object" 1;
b y  Clarsimp_tac 1;
b y (etac FVar_lemma THEN_ALL_NEW atac) 1;

(* AVar *)
b y EVERY'[Full_simp_tac, forward_hyp_tac] 1;
b y EVERY'[thin_tac "G\<turnstile>Norm s0 \<midarrow>?e1-\<succ>?a'\<rightarrow> (?x1, ?s1)", ftac eval_gext'] 1;
b y rtac conjI 1;
b y  clarsimp_tac (claset(), simpset() addsimps [avar_def2]) 1;
b y Clarsimp_tac 1;
b y (etac AVar_lemma THEN_ALL_NEW atac) 1;

(* Call *)
b y EVERY'[Full_simp_tac, forward_hyp_tac, Full_simp_tac] 1; 
b y (etac Call_type_sound THEN_ALL_NEW ares_tac [refl]) 1;
qed_spec_mp "eval_type_sound";


Addsimps [fun_upd_apply];
simpset_ref() := simpset() addsimps [split_paired_All,split_paired_Ex]
        addsplits [split_if    , option.split    ]
	addsplits [split_if_asm, option.split_asm]
	addloop ("split_all_tac", split_all_tac);
claset_ref() := claset() addSWrapper ("split_all_tac", 
				      fn tac2 => split_all_tac ORELSE' tac2);

Goal "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>  \
\ (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T)";
b y datac eval_type_sound 3 1;
b y rewtac Let_def;
b y Clarsimp_tac 1;
qed "eval_ts";

Goal "\<lbrakk>G\<turnstile>s \<midarrow>es\<doteq>\<succ>vs\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> \
\ (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> list_all2 (conf G s') vs Ts)";
b y datac eval_type_sound 3 1;
b y rewtac Let_def;
b y Clarsimp_tac 1;
qed "evals_ts";

Goal "\<lbrakk>G\<turnstile>s \<midarrow>v=\<succ>(w, f)\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>v\<Colon>=T\<rbrakk> \<Longrightarrow> \
\ (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,s'\<turnstile>w\<Colon>\<preceq>T \<and> \
\  (\<forall>s'' w'. Norm s''\<Colon>\<preceq>(G,L) \<longrightarrow> G,s''\<turnstile>w'\<Colon>\<preceq>T \<longrightarrow> s'\<le>|s'' \<longrightarrow> \
\                                    assign f w' (Norm s'')\<Colon>\<preceq>(G,L)))";
b y datac eval_type_sound 3 1;
b y rewtac Let_def;
b y Clarsimp_tac 1;
qed "evar_ts";

Goal "\<lbrakk>G\<turnstile>s \<midarrow>s0\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>s0\<Colon>\<surd>\<rbrakk> \<Longrightarrow> s'\<Colon>\<preceq>(G,L)";
b y datac eval_type_sound 3 1;
b y rewtac Let_def;
b y Clarsimp_tac 1;
qed "exec_ts";

Goal "\<And>s. \<lbrakk>wf_prog G; (G,L)\<turnstile>{t,md,mode}e..mn({pTs'}ps)\<Colon>-rT; \
\ s\<Colon>\<preceq>(G,L); G\<turnstile>s \<midarrow>e-\<succ>a'\<rightarrow> Norm s'; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> \<Longrightarrow> \
\ cmethd G (target mode s' a' md) (mn, pTs') \<noteq> None";
b y eresolve_tac wt_elim_cases 1;
b y dtac max_spec2mheads 1;
b y datac eval_ts 3 1;
b y clarsimp_tac (claset(), simpset() delsplits[split_if,split_if_asm]) 1;
b y datac DynT_propI 3 1;
b y exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s' a' md) (mn, pTs'))" 1;
b y EVERY'[datac (DynT_mheadsD RS conjunct1) 4, rtac refl] 1;
b y Fast_tac 1;
qed "all_methods_understood";