File State.ML

open State;


section "objects";

qed_goalw "the_Arr_Arr" thy [the_Arr_def] 
        "the_Arr (Some (Arr T k,cs)) = (T,k,cs)" (K [Auto_tac]);
Addsimps [the_Arr_Arr];

qed_goal "obj_tagE" thy
    "[| !!C  . oi = CInst C ==> P;  \
\       !!T k. oi = Arr T k ==> P  |] ==> P" (fn prems => [
	rtac (obj_tag.split RS iffD2) 1,
	safe_tac HOL_cs,
	ALLGOALS (eresolve_tac prems)]);
fun obj_tag_case_tac s = res_inst_tac [("oi",s)] obj_tagE;

qed_goalw "upd_obj_def2" thy [upd_obj_def] 
  "\<And>obj. upd_obj n v (oi, vs) = (oi, vs(n\<mapsto>v))" (K [Auto_tac]);
Addsimps [upd_obj_def2];

qed_goalw "obj_ty_eq" thy [obj_ty_def] 
   "obj_ty (oi,x) = obj_ty (oi,y)" (K [Simp_tac 1]);
AddSIs[obj_ty_eq];
qed_goal "obj_ty_cong" thy 
	"obj_ty (oi, vs(n\<mapsto>v)) = obj_ty (oi, vs)" (K [rtac obj_ty_eq 1]);
Addsimps [obj_ty_cong];

qed_goalw "obj_ty_CInst" thy [obj_ty_def] 
   "obj_ty (CInst C,x) = Class C" (K [Simp_tac 1]);
qed_goalw "obj_ty_Arr"   thy [obj_ty_def] 
   "obj_ty (Arr T i,x) = T.[]" (K [Simp_tac 1]);
Addsimps[obj_ty_CInst, obj_ty_Arr];

Goalw [obj_ty_def] "G\<turnstile>obj_ty (oi, vs)\<preceq>RefT t \<Longrightarrow> (\<exists>C. oi = CInst C) \<or> (\<exists>T k. oi = Arr T k)";
b y auto_tac (claset(), simpset() addsplits [obj_tag.split_asm]);
qed "obj_ty_widenD";

qed_goalw "obj_class_CInst" thy [obj_class_def] 
        "obj_class (CInst C,fs) = C" (K [Auto_tac]);
qed_goalw "obj_class_Arr" thy [obj_class_def] 
        "obj_class (Arr T k,fs) = Object" (K [Auto_tac]);
Addsimps [obj_class_CInst, obj_class_Arr];


section "object references";

Goalw [fields_table_def] "\<lbrakk>table_of (fields G C) f = Some (m,T); P m\<rbrakk> \
\ \<Longrightarrow> fields_table G C P f = Some T";
b y Clarsimp_tac 1;
b y rtac exI 1;
b y dres_inst_tac [("P","P o fst")] map_of_filter_in 1;
b y Auto_tac;
b y subgoal_tac "(\<lambda>(fn\<Colon>ename × tname,m\<Colon>bool,fT\<Colon>ty). P m)=split (\<lambda>k. P \<circ> fst)"1;
b y  asm_full_simp_tac (simpset() addsimps [(*###*)o_def]) 1;
b y rtac ext 1;
b y Auto_tac;
qed "fields_table_SomeI";

Goalw [fields_table_def] "\<And>X. fields_table G C P fn = Some T \<Longrightarrow> \
\ \<exists>m. (fn,(m,T))\<in>set(fields G C)";
b y Clarsimp_tac 1;
b y dtac map_of_SomeD 1;
b y Auto_tac;
qed "fields_table_SomeD";

Goalw [fields_table_def] 
"\<lbrakk>fields_table G C P fn = Some T; unique (fields G C)\<rbrakk> \<Longrightarrow> \
\ \<exists>m. table_of (fields G C) fn = Some (m,T)";
b y Clarsimp_tac 1;
b y rtac exI 1;
b y eatac table_of_filter_unique_SomeD 1 1;
qed "fields_table_SomeD";

qed_goalw "var_tys_Some_eq" thy [var_tys_def]
 "var_tys G oi r n = Some T = (case r of Inl a \<Rightarrow> (case oi of \
\   CInst C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> fields_table G C Not nt = Some T) \
\ | Arr t k \<Rightarrow> (\<exists> i. n = Inr i  \<and> #0 \<le> i \<and> i < k \<and> t = T)) \
\ | Inr C   \<Rightarrow> (\<exists>nt. n = Inl nt \<and> fields_table G C id  nt = Some T))"
 (K [force_tac (claset(), simpset() addsplits 
  [sum.split_asm, sum.split, obj_tag.split]) 1]);


section "st access";

qed_goalw  "globs_def2" thy [ globs_def] " globs (st g l) = g" (K [Simp_tac 1]);
qed_goalw "locals_def2" thy [locals_def] "locals (st g l) = l" (K [Simp_tac 1]);
Addsimps[globs_def2,locals_def2];

qed_goalw "heap_def2" thy [heap_def] "heap s a=globs s (Heap a)"(K[Simp_tac 1]);
Addsimps[heap_def2];


section "st update";

Goalw [gupd_def] "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l";
b y Simp_tac 1;
qed "gupd_def2";
Addsimps[gupd_def2];

Goalw [lupd_def] "lupd(vn\<mapsto>v) (st g l) = st g (l(vn\<mapsto>v))";
b y Simp_tac 1;
qed "lupd_def2";
Addsimps[lupd_def2];

qed_goalw "globs_gupd" thy [gupd_def] 
	"\<And>s. globs  (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
	 (K [induct_tac "s" 1,Simp_tac 1]);
qed_goalw "globs_lupd" thy [lupd_def]
	"\<And>s. globs  (lupd(vn\<mapsto>v ) s) = globs  s"
	 (K [induct_tac "s" 1,Simp_tac 1]);
qed_goalw "locals_gupd" thy [gupd_def] 
	"\<And>s. locals (gupd(r\<mapsto>obj) s) = locals s"
	 (K [induct_tac "s" 1,Simp_tac 1]);
qed_goalw "locals_lupd" thy [lupd_def]
	"\<And>s. locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
	 (K [induct_tac "s" 1,Simp_tac 1]);
Addsimps[globs_gupd, globs_lupd, locals_gupd, locals_lupd];

Goalw [upd_gobj_def] "globs s r = None \<longrightarrow> globs (upd_gobj r n v s) = globs s";
b y induct_tac "s" 1;
b y Auto_tac;
qed_spec_mp "globs_upd_gobj_new";

Goalw [upd_gobj_def]
"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"; 
b y induct_tac "s" 1;
b y Auto_tac;
qed_spec_mp "globs_upd_gobj_upd";

Addsimps[globs_upd_gobj_new,globs_upd_gobj_upd];

qed_goalw "locals_upd_gobj" thy [upd_gobj_def] 
 "\<And>s. locals (upd_gobj r n v s) = locals s" (K [induct_tac "s" 1,Auto_tac]);
Addsimps[locals_upd_gobj];

Goalw [init_obj_def] "globs (init_obj G oi r s) t = \
\ (if t=r then Some (oi, init_vals (var_tys G oi r)) else globs s t)";
b y Simp_tac 1;
qed "globs_init_obj";
Addsimps[globs_init_obj];

qed_goalw "locals_init_obj" thy [init_obj_def] 
  "locals (init_obj G oi r s) = locals s" (K [Simp_tac 1]);
Addsimps[locals_init_obj];

qed_goal "surjective_st" thy 
"st (globs s) (locals s) = s" (K [induct_tac "s" 1,Auto_tac]);
Addsimps [surjective_st];

Goal "st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s";
b y stac (locals_init_obj RS sym) 1;
b y rtac surjective_st 1;
qed "surjective_st_init_obj";




section "exceptions";

Goalw [normal_def] "normal s = (fst s = None)";
b y Simp_tac 1;
qed "normal_def2";
Addsimps[normal_def2];

Goal "\<forall>Z. Z = (s::state) \<Longrightarrow> False";
b y eres_inst_tac [("x","(Some k,y)")] all_dupE 1;
b y eres_inst_tac [("x","(None  ,y)")] allE 1;
b y Clarify_tac 1;
qed "single_stateE";

Goal "All (op = (x::('a option) × 'b)) \<Longrightarrow> R";
b y dres_inst_tac [("x","(if fst x = None then Some ?x else None,?y)")] spec 1;
b y Clarsimp_tac 1;
qed "state_not_single";

qed_goalw "the_XcptLoc_XcptLoc" thy [the_XcptLoc_def] 
	"the_XcptLoc (XcptLoc a) = a" (K [Auto_tac]);
qed_goalw "the_StdXcpt_StdXcpt" thy [the_StdXcpt_def] 
	"the_StdXcpt (StdXcpt xn) = xn" (K [Auto_tac]);
Addsimps [the_XcptLoc_XcptLoc,the_StdXcpt_StdXcpt];

(* unused *)
qed_goal "xcpt_exh" thy "(\<exists>a. xc = XcptLoc a) | (\<exists>x. xc = StdXcpt x)"
	(K [induct_tac "xc" 1, Auto_tac]);

(* unused *)
qed_goal "xcptE" thy 
	"[| !!a. xc = XcptLoc a ==> P;  !!x. xc = StdXcpt x ==> P |] ==> P" 
(fn prems => [
	cut_facts_tac [read_instantiate [("xc","xc")] xcpt_exh] 1,
	etac disjE 1,
	ALLGOALS (etac exE THEN' eresolve_tac prems)]);

section "xcpt_if";

qed_goalw "xcpt_if_True_None" thy [xcpt_if_def] 
	"xcpt_if True x None = x"			(K [Simp_tac 1]);
qed_goalw "xcpt_if_True_not_None" thy [xcpt_if_def] 
	"\<And>X. x \<noteq> None \<Longrightarrow> xcpt_if True x y \<noteq> None"	(K [Auto_tac]);
qed_goalw "xcpt_if_False" thy [xcpt_if_def] 
	"xcpt_if False x y = y"				(K [Simp_tac 1]);
qed_goalw "xcpt_if_Some" thy [xcpt_if_def] 
	"xcpt_if c x (Some y) = Some y" 		(K [Asm_simp_tac 1]);
qed_goalw "xcpt_if_not_None" thy [xcpt_if_def] 
	"\<And>X. y \<noteq> None \<Longrightarrow> xcpt_if c x y = y"		(K [Asm_simp_tac 1]);
Addsimps [xcpt_if_True_None,xcpt_if_True_not_None,
	  xcpt_if_False,xcpt_if_Some,xcpt_if_not_None];
Goalw [xcpt_if_def]
"P (xcpt_if c x' x) = ((c \<and> x = None \<longrightarrow> P x') \<and> (¬ (c \<and> x = None) \<longrightarrow> P x))";
b y split_tac [split_if] 1;
b y Auto_tac;
qed "split_xcpt_if";

qed_goalw "raise_if_None" thy [xcpt_if_def] 
	"(raise_if c x y = None) = (¬c \<and> y = None)"	(K [Auto_tac]);
Addsimps [raise_if_None];
AddSDs[raise_if_None RS iffD1];
qed_goalw "if_raise_if_None" thy [xcpt_if_def] 
 "((if b then y else raise_if c x y) = None) = ((c \<longrightarrow> b) \<and> y = None)"
	(K [Auto_tac]);
Addsimps[if_raise_if_None];
qed_goal "raise_if_SomeD" thy 
	"\<And>X. raise_if c x y = Some z \<Longrightarrow> c \<and> z=StdXcpt x \<and> y=None \<or> (y=Some z)"
(K [
	case_tac "y" 1,
	 Asm_full_simp_tac 2,
	case_tac "c" 1,
	 Auto_tac]);
AddSDs[raise_if_SomeD];


section "initialisation test";

Goalw [inited_def] "¬inited C empty";
b y Simp_tac 1;
qed "not_inited_empty";
Addsimps[not_inited_empty];

Goalw [inited_def] "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)";
b y auto_tac (claset(), simpset() addsplits [st.split]);
qed "inited_gupdate";
Addsimps[inited_gupdate];

Goalw [inited_def] "inited C (globs (init_class_obj G C s))";
b y Simp_tac 1;
qed "inited_init_class_obj";
AddSIs [inited_init_class_obj];

Goalw [inited_def] "¬ inited C g \<Longrightarrow> g (Stat C) = None";
b y etac notnotD 1;
qed "not_initedD";

Goalw [inited_def] "inited C g \<Longrightarrow> \<exists>oi fs. g (Stat C) = Some (oi, fs)";
b y Auto_tac;
qed "initedD";

Goalw [initd_def] "initd C s = inited C (globs (snd s))";
b y Simp_tac 1;
qed "initd_def2";
Addsimps [initd_def2];


section "state update";

qed_goalw "xupd_def2" thy [xupd_def] 
	"\<And>s. xupd f (x,s) = (f x,s)" (K [Simp_tac 1]);
Addsimps[xupd_def2];

Goal "\<And>s. xupd (xcpt_if False xo) s = s";
b y Simp_tac 1;
qed "xupd_xcpt_if_False";
Addsimps[xupd_xcpt_if_False];


qed_goalw "supd_def2" thy [supd_def] 
	"\<And>s. supd f (x,s) = (x,f s)" (K [Simp_tac 1]);
Addsimps[supd_def2];

Goal "\<And>s. supd (lupd vn v ) s = (fst s,lupd vn v (snd s))";
b y split_all_tac 1;
b y Simp_tac 1;
qed "supd_lupd";
Addsimps[supd_lupd];

Goal "\<And>s. supd (gupd r obj) s = (fst s,gupd r obj (snd s))";
b y split_all_tac 1;
b y Simp_tac 1;
qed "supd_gupd";
Addsimps[supd_gupd];

Goalw [init_obj_def] "supd (init_obj G oi r) s = (fst s, init_obj G oi r (snd s))";
b y Simp_tac 1;
qed "supd_init_obj";
Addsimps[supd_init_obj];

Goalw [set_locals_def] "set_locals l (st g l') = st g l";
b y Simp_tac 1;
qed "set_locals_def2";
Addsimps[set_locals_def2];

Goalw [set_locals_def] "set_locals (locals s) s = s";
b y induct_tac "s" 1;
b y Simp_tac 1;
qed "set_locals_id";
Addsimps[set_locals_id];

Goalw [set_locals_def] "set_locals l (set_locals l' s) = set_locals l s";
b y induct_tac "s" 1;
b y Simp_tac 1;
qed "set_set_locals";
Addsimps[set_set_locals];

Goalw [set_locals_def] "locals (set_locals l s) = l";
b y induct_tac "s" 1;
b y Simp_tac 1;
qed "locals_set_locals";
Addsimps[locals_set_locals];

Goalw [set_locals_def] "globs (set_locals l s) = globs s";
b y induct_tac "s" 1;
b y Simp_tac 1;
qed "globs_set_locals";
Addsimps[globs_set_locals];

Goalw [heap_def] "heap (set_locals l s) = heap s";
b y induct_tac "s" 1;
b y Simp_tac 1;
qed "heap_set_locals";
Addsimps[heap_set_locals];

Goal "\<And>s. set_lvars l (set_lvars l' s) = set_lvars l s";
b y split_all_tac 1;
b y Simp_tac 1;
qed "set_set_lvars";
Addsimps[set_set_lvars];

Goal "\<And>s. set_lvars (locals (snd s)) s = s";
b y split_all_tac 1;
b y Simp_tac 1;
qed "set_lvars_id";
Addsimps[set_lvars_id];