State.ML

open State;

Addsimps [update_def2];

val if_Some = prove_goal thy 
 "!!X. y ~= None ==> (if x = None then Some y else x) ~= None"
	(K [not_None_tac 1,TRY (Asm_simp_tac 1)]);
Addsimps [if_Some];



section "obj";

val the_Obj_Obj = prove_goalw thy [the_Obj_def] 
	"the_Obj (Some (Obj C fs)) = (C,fs)" (K [Auto_tac]);

val the_Arr_Arr = prove_goalw thy [the_Arr_def] 
	"the_Arr (Some (Arr T cs)) = (T,cs)" (K [Auto_tac]);

Addsimps [the_Obj_Obj, the_Arr_Arr];

local 
  fun prover s = prove_goal thy s (K [obj.induct_tac "obj" 1, Auto_tac]) RS mp;
in
  val obj_ty_ObjD = prover "obj_ty obj = Class C --> (? fs. obj = Obj C fs)";
  val obj_ty_ArrD = prover "obj_ty obj = T[.]    --> (? cs. obj = Arr T cs)";
end;
AddSDs [obj_ty_ObjD, obj_ty_ArrD];

val objE = prove_goal thy
    "[| !!C fs. obj = Obj C fs ==> P;  \
\       !!T cs. obj = Arr T cs ==> P  |] ==> P" (fn prems => [
	rtac (split_obj_case RS iffD2) 1,
	safe_tac HOL_cs,
	ALLGOALS (eresolve_tac prems)]);


section "xcpt";

val the_XcptLoc_XcptLoc = prove_goalw thy [the_XcptLoc_def] 
	"the_XcptLoc (XcptLoc a) = a" (K [Auto_tac]);

val the_SysXcpt_SysXcpt = prove_goalw thy [the_SysXcpt_def] 
	"the_SysXcpt (SysXcpt xn) = xn" (K [Auto_tac]);

Addsimps [the_XcptLoc_XcptLoc,the_SysXcpt_SysXcpt];


section "new_Addr";

goalw thy [new_Addr_def] "!!X. new_Addr h = y ==> \
\ y = Some (a, x) --> h a = None &  (x = None |  x = Some (SysXcpt OutOfMemory))";
b y etac subst 1;
b y rtac selectI2 1;
b y  Fast_tac 2;
b y case_tac "(!a. h a ~= None)" 1;
b y  subgoal_tac "(if (!a. h a ~= None) then None else Some (@(a,x). h a = None &  (x = None |  x = Some (SysXcpt OutOfMemory))))=None" 1;
b y  rtac disjI1 1;
b y  rtac conjI 1;
b y   atac 1;
b y  atac 1;
b y  ALLGOALS Asm_full_simp_tac;
b y Clarify_tac 1;
b y rtac selectI2 1;
b y  Auto_tac;
val new_AddrD_lemma = result();

val new_AddrD = prove_goal thy "!!X. new_Addr h = Some (a,x) ==> \
\ h a = None &  (x = None |  x = Some (SysXcpt OutOfMemory))" (K [
	rtac (new_AddrD_lemma RS mp) 1,
	ALLGOALS Fast_tac]);


section "raise_if";

val raise_if_True  = prove_goalw thy [raise_if_def] 
	"raise_if True x y ~= None"			(K [Simp_tac 1]);
val raise_if_True2 = prove_goalw thy [raise_if_def] 
	"raise_if True x None = Some (SysXcpt x)"	(K [Simp_tac 1]);
val raise_if_False = prove_goalw thy [raise_if_def] 
	"raise_if False x y = y"			(K [Simp_tac 1]);
val raise_if_Some  = prove_goalw thy [raise_if_def] 
	"raise_if c x (Some y) = Some y" 		(K [Asm_simp_tac 1]);
val raise_if_not_None = prove_goalw thy [raise_if_def] 
	"!!X. c |  y ~= None ==> raise_if c x y ~= None"	(K [Auto_tac]);
val raise_if_NoneD = prove_goalw thy [raise_if_def] 
	"!!X. raise_if c x y = None ==> ~ c &  y = None"	(K [Auto_tac]);
AddSDs[raise_if_NoneD];
Addsimps [raise_if_True,raise_if_True2,raise_if_False,
	  raise_if_not_None,raise_if_Some];



section"upd";

val lupd_def2 = prove_goalw thy [lupd_def] "lupd[vn|->v] (h,l) = (h,l[vn|->v])"
	(K [Simp_tac 1]);
val hupd_def2 = prove_goalw thy [hupd_def] "hupd[a|->obj](h,l) = (h[a|->obj],l)"
	(K [Simp_tac 1]);
Addsimps[lupd_def2, hupd_def2];

val c_hupd_None = prove_goalw thy [c_hupd_def] 
	"c_hupd[a|->obj] (Norm (h,l)) = Norm (h[a|->obj], l)" (K [Simp_tac 1]);
val c_hupd_Some = prove_goalw thy [c_hupd_def] 
	"!!X. x ~= None ==> c_hupd[a|->obj] (x,s) = (x,s)" (K [
	not_None_tac 1, TRY (Asm_simp_tac 1)]);
Addsimps[c_hupd_None, c_hupd_Some];


section"hext";

val hextI = prove_goalw thy [hext_def] "!!X. !a obj. h a = Some obj --> \
\ (? obj'. h' a = Some obj' &  obj_ty obj'=obj_ty obj) ==> h<=|h'" 
	(K [atac 1]);
val hextD = prove_goalw thy [hext_def] "!!X. [|h<=|h'; h a = Some obj|] ==> \
\ ? obj'. h' a = Some obj' &  obj_ty obj' = obj_ty obj" (K [Fast_tac 1]);
val hextD2 = prove_goalw thy [hext_def] "!!X. [|h a = Some obj; h<=|h'|] ==> \
\ ? obj'. h' a = Some obj' &  obj_ty obj' = obj_ty obj" (K [Fast_tac 1]);

val hext_refl = prove_goal thy "h<=|h" (K [
	rtac hextI 1,Fast_tac 1]);

val hext_new = prove_goal thy "!!h. h a = None ==> h<=|h[a|->x]" (K [
	rtac hextI 1, Auto_tac]);
AddEs [hext_new];

val hext_trans = prove_goal thy "!!h. [|h<=|h'; h'<=|h''|] ==> h<=|h''" (K [
	force_tac(claset() addIs [hextI] addDs [hextD], simpset()) 1]);
AddEs [hext_trans];
Addsimps [hext_refl, hext_new];

val hext_upd_Obj = prove_goal thy 
"!!h. h a = Some (Obj C fs) ==> h<=|h[a|->Obj C fs']" (K [
	rtac hextI 1,
	Auto_tac]);

val hext_upd_Arr = prove_goal thy 
"!!h. h a = Some (Arr T cs) ==> h<=|h[a|->Arr T cs']" (K [
	rtac hextI 1,
	Auto_tac]);


section"conf";

val conf_ClassD = prove_goalw thy [conf_def] 
 	"G,h|-a'::<=:Class tn --> a'=Null | (? a. a'=Addr a)" (K [
	rtac val_.induct 1,
	    Auto_tac]) RS mp;

goalw thy [conf_def]
 	"!!X. [|G,h|-Addr a::<=:Class tn; tn~=Object|] ==> \
\ ? C fs. h a = Some (Obj C fs) &  G|-Class C<=:Class tn";
b y Auto_tac;
b y res_inst_tac [("obj", "z")] objE 1;
b y  dtac widen_Class2 2;
b y  Auto_tac;
val conf_Addr_ClassD = result();

val conf_NullT = prove_goalw thy [conf_def] 
"G,h|-Null::<=:T = G|-NT<=:T" (K [Simp_tac 1]);
Addsimps [conf_NullT];

val conf_litval = prove_goalw thy [conf_def, empty_dt_def] 
"typeof empty_dt v = Some T --> G,h|-v::<=:T" (K [
	rtac val_.induct 1,
	    Auto_tac]) RS mp;

val conf_AddrI = prove_goalw thy [conf_def] 
"!!X. [|h a = Some obj; G|-obj_ty obj<=:T|] ==> G,h|-Addr a::<=:T"
(K [Asm_full_simp_tac 1]);

val conf_Obj_AddrI = prove_goalw thy [conf_def]
 "!!X. [|h a = Some (Obj C fs); G|-Class C<=:Class D|] ==> G,h|-Addr a::<=:Class D" 
(K [Asm_full_simp_tac 1]);

val conf_Arr_AddrI = prove_goalw thy [conf_def]
 "!!X. [|is_type G T; h a = Some (Arr T cs)|] ==> G,h|-Addr a::<=:T[.]"
(K [Asm_full_simp_tac 1]);

val defval_conf = prove_goalw thy [conf_def] 
	"is_type G T --> G,h|-default_val T::<=:T" (K [
	Simp_tac 1,
	rtac ty.induct 1,
	 rtac prim_ty.induct 1,
	   ALLGOALS (simp_tac (simpset() addsimps [widen.null]))]) RS mp;

val conf_upd_Obj = prove_goalw thy [conf_def] 
"!!X. h a = Some (Obj C fs) ==> (G,h[a|->Obj C fs']|-x::<=:T) = (G,h|-x::<=:T)" (K [
	rtac val_.induct 1,
	 Auto_tac]);

val conf_upd_Arr = prove_goalw thy [conf_def] 
"!!X. h a = Some (Arr T' cs) ==> (G,h[a|->Arr T' cs']|-x::<=:T) = (G,h|-x::<=:T)" (K [
	rtac val_.induct 1, Auto_tac]);

val conf_widen = prove_goalw thy [conf_def] 
"!!X. wf_prog G ==> G,h|-x::<=:T --> G|-T<=:T' --> G,h|-x::<=:T'" (K [
	rtac val_.induct 1, Auto_tac]) RS mp RS mp;

val conf_widen2 = prove_goal thy
"!!X. [|G|-T<=:T'; G,h|-x::<=:T; wf_prog G|] ==> G,h|-x::<=:T'"	
	 (K [fast_tac (HOL_cs addIs [conf_widen]) 1]);
AddEs [conf_widen2];

val conf_hext = prove_goalw thy [conf_def] 
	"!!h. h<=|h' ==> G,h|-v::<=:T --> G,h'|-v::<=:T" (K [
	rtac val_.induct 1,
	     ALLGOALS Simp_tac,
	Safe_tac,
	dtac hextD 1,
	 atac 1,
	Auto_tac]) RS mp;

val new_locD = prove_goalw thy [conf_def]
	"!!X. [|h a = None; G,h|-Addr t::<=:T|] ==> t~=a" (K [
	Full_simp_tac 1,
	safe_tac HOL_cs,
	Asm_full_simp_tac 1]);

val conf_RefTD = prove_goalw thy [conf_def] "G,h|-a'::<=:RefT T --> a' = Null |  \
\ (? a obj T'. a' = Addr a &  h a = Some obj &  obj_ty obj = T' &  G|-T'<=:RefT T)" (K [
	val_.induct_tac "a'" 1,
	    Auto_tac,
	    REPEAT (etac widen_PrimT_RefT 1),
	Auto_tac]) RS mp;

val conf_NTD = prove_goal thy "!!X. G,h|-a'::<=:NT ==> a' = Null" (K [
	dtac conf_RefTD 1,
	Safe_tac,
	res_inst_tac [("obj","obj")] objE 1,
	 Auto_tac,
	 etac widen_Class_NT 1,
	etac widen_Array_NT 1]);

val conf_IfaceD = prove_goal thy "!!X. [|G,h|-a'::<=:Iface I; wf_prog G|] ==> \
\ a' = Null |  (? C. G,h|-a'::<=:Class C &  G|-Class C<=:Iface I &  C ~= Object)" (K [
	dtac conf_RefTD 1,
	Safe_tac,
	etac swap 1,
	res_inst_tac [("obj","obj")] objE 1,
	 ALLGOALS Asm_full_simp_tac,
	 etac widen_Array_Iface 2,
	forward_tac [widen_is_type] 1,
	fast_tac (HOL_cs addIs [widen.implmt,widen.refl, conf_Obj_AddrI] 		 addDs [implmt_ObjectE,widen_Class_Iface]) 1]);

val non_npD = prove_goal thy "!!X. [|a' ~= Null; G,h|-a'::<=:RefT t|] ==> \
\ (? a C fs. a' = Addr a &  h a = Some (Obj C fs) &  G|-Class C<=:RefT t) |  \
\ (? a T cs. a' = Addr a &  h a = Some (Arr T cs) &  G|-T[.]<=:RefT t)" (K [
	dtac conf_RefTD 1,
	Step_tac 1,
	res_inst_tac [("obj","obj")] objE 1,
	 Auto_tac]);

val non_np_ObjD = prove_goal thy "!!X. [|G,h|-a'::<=:Class C; a'~=Null; C ~= Object|] ==>\
\ (? a C' fs. a' = Addr a &  h a = Some (Obj C' fs) &  G|-Class C'<=:Class C)" 
	(K[fast_tac (HOL_cs addDs [non_npD, widen_Array_Class]) 1]);
AddSDs [non_np_ObjD];
(*
goal thy "!!X. [|a' ~= Null; wf_prog G|] ==> G,h|-a'::<=:RefT t --> (RefT t ~= Class Object) --> ~ (? T. RefT t = T[.]) --> (? C. G,h|-a'::<=:Class C &  G|-Class C<=:RefT t)";
b y Rt.induct_tac "t" 1;
b y    Auto_tac;
b y   dtac conf_NTD 1;
b y   contr_tac 1;
b y  dtac conf_IfaceD 1;
b y   atac 1;
b y  forward_tac [widen_is_type] 2;
b y   auto_tac (claset() addEs [conf_AddrI], simpset());
val non_np_conf_RefTD = result() RS mp RS mp RS mp;
*)
val non_np_ObjD' = prove_goal thy"!!X. [|a' ~= Null; wf_prog G|] ==> \
\ G,h|-a'::<=:RefT t --> (!C. t = ClassT C --> C ~= Object) --> ~ (? T. RefT t = T[.]) -->\
\ (? a C fs. a' = Addr a &  h a = Some (Obj C fs) &  G|-Class C<=:RefT t)" (K[
	Rt.induct_tac "t" 1,
	safe_tac HOL_cs,
	   Fast_tac 4,
	  dtac conf_NTD 1,
	  contr_tac 1,
	 Fast_tac 2,
	dtac conf_IfaceD 1,
	 atac 1,
	Fast_tac 1]) RS mp RS mp RS mp;

val non_np_ArrD = prove_goal thy "!!X. [|G,h|-a'::<=:T[.]; a' ~= Null|] ==> \
\ (? a T' cs. a' = Addr a &  h a = Some (Arr T' cs) &  G|-T'[.]<=:T[.])"
	(K[fast_tac (HOL_cs addSDs [non_npD, widen_Class_Array]) 1]);
AddSDs [non_np_ArrD];

goal thy "!!X. [|G,h|-v::<=:RefT x; v ~= Null; G|-obj_ty (the (h (the_Addr v)))<=:T|] ==> \
\ G,h|-v::<=:T";
b y dtac non_npD 1;
b y  atac 1;
b y Safe_tac ;
b y  auto_tac (claset() , simpset() addsimps [conf_AddrI]);
val non_np_conf = result();


section "fits";

val fits_Null = prove_goalw thy [fits_def] "G,h|-Null fits T" (K [
	Simp_tac 1]);
Addsimps [fits_Null];

goalw thy [fits_def] "!!X. G,h|-v::<=:T ==> G,h|-v fits T";
b y Clarify_tac 1;
b y EVERY[etac swap 1, Full_simp_tac 1, dtac (non_PrimT RS iffD1) 1];
b y Clarify_tac 1;
b y dtac non_npD 1;
b y Auto_tac;
val conf_fits = result();

goalw thy [fits_def] "!!X. G,h|-v fits T ==> (? pt. T = PrimT pt) |  \
\ (? t. T = RefT t) &  v = Null |  \
\ (? t. T = RefT t) &  v ~= Null &   G|-obj_ty (the (h (the_Addr v)))<=:T";
b y case_tac "? pt. T = PrimT pt" 1;
b y  ALLGOALS Asm_full_simp_tac;
b y case_tac "v = Null" 1;
b y  ALLGOALS Asm_full_simp_tac;
b y  ALLGOALS (etac (non_PrimT RS iffD1));
val fitsD = result();

goal thy "!!X. [|G,h|-v::<=:T; G|-T<=:? T'; G,h|-v fits T'; wf_prog G|] ==> G,h|-v::<=:T'";
b y dtac fitsD 1;
b y Safe_tac;
b y   dtac cast_PrimT2 1;
b y   Fast_tac 1;
b y  forward_tac [cast_is_type] 1;
b y  Asm_full_simp_tac 1;
b y dtac cast_RefT2 1;
b y Clarify_tac 1;
b y etac non_np_conf 1 THEN ALLGOALS atac;
val fits_conf = result();

goal thy "!!X. [|G,h|-v::<=:T; G|-T<=:Ty; G|-T'[.]<=:Ty[.]; G,h|-v fits T'; wf_prog G|] ==> \
\ G,h|-v::<=:T'";
b y dtac fitsD 1;
b y Safe_tac;
b y   dtac widen_ArrayPrimT 1;
b y   Fast_tac 1;
b y  ALLGOALS (dtac widen_Array_Array);
b y  Asm_full_simp_tac 1;
b y dtac widen_RefT 1;
b y Clarify_tac 1;
b y dtac widen_RefT2 1;
b y Clarify_tac 1;
b y etac non_np_conf 1 THEN ALLGOALS atac;
val fits_conf2 = result();


section "lconf";

val lconfD = prove_goalw thy [lconf_def] 
    "!!X. [|G,h|-vs[::<=:]Ts; Ts n = Some T|] ==> G,h|-(the (vs n))::<=:T" (K [Auto_tac]);

val lconf_Arr = prove_goalw thy [lconf_def]
"(G,h|-cs[::<=:]option_map (%i. T)  o  cs) = (!i v. cs i = Some v --> G,h|-v::<=:T)" (K [
	Auto_tac]);

val lconf_new = prove_goalw thy [lconf_def] 
"!!X. [|L vn = None; G,h|-l[::<=:]L|] ==> G,h|-l[vn|->v][::<=:]L" (K [
	Auto_tac]);

val lconf_empty = prove_goalw thy [lconf_def] 
"G,h|-vs[::<=:]empty" (K [Auto_tac]);

val lconf_upd = prove_goalw thy [lconf_def] 
"!!X. [|G,h|-l[::<=:]L; G,h|-v::<=:T|] ==> G,h|-l[vn|->v][::<=:]L[vn|->T]" (K [Auto_tac]);

val lconf_upd2 = prove_goalw thy [lconf_def] 
"!!X. [|G,h|-l[::<=:]L; G,h|-v::<=:T; L vn = Some T|] ==> \
\ G,h|-l[vn|->v][::<=:]L" (K [Auto_tac]);

(*unused
val lconf_upd2a = prove_goalw thy [lconf_def]
"!!X. [|G,h|-l[::<=:]L; L vn = None|] ==> G,h|-l[vn|->v][::<=:]L" (K [Auto_tac]);
*)

val lconf_updD = prove_goalw thy [lconf_def] 
"!!X. [|G,h|-l[::<=:]L[vn|->T]; L vn = None|] ==> G,h|-l[::<=:]L" (K [Auto_tac]);

goalw thy [init_vars_def, lconf_def] 
	"(!(f,T):set fs. is_type G T) --> G,h|-init_vars fs[::<=:]table_of fs";
b y list.induct_tac "fs" 1;
b y  Simp_tac 1;
b y Asm_full_simp_tac 1;
b y Clarify_tac 1;
b y etac defval_conf 1;
val lconf_init_vars = result() RS mp;

val lconf_hext = prove_goalw thy [lconf_def] 
	"!!X. [|h<=|h'; G,h|-l[::<=:]L|] ==> G,h'|-l[::<=:]L" (K [
	fast_tac (HOL_cs addIs [conf_hext]) 1]);


section"oconf";

val oconf_hext = prove_goal thy
"G,h|-obj::<=:<> --> h<=|h' --> G,h'|-obj::<=:<>" (K [
	rtac obj.induct 1,
	 ALLGOALS Simp_tac,
	 ALLGOALS (fast_tac (HOL_cs addEs [lconf_hext,conf_hext]))
	]) RS mp RS mp;
AddEs [oconf_hext];

val oconf_Obj = prove_goal thy "G,h|-Obj C fs::<=:<> = \
\ (G,h|-fs[::<=:]table_of (fields G C))" (K [Simp_tac 1]);
val oconf_Obj' = prove_goal thy "G,h|-Obj C fs::<=:<> = \
\ (!f T. table_of (fields G C) f = Some T --> (? v. fs f = Some v &  G,h|-v::<=:T))"
	(K [simp_tac (simpset() addsimps [lconf_def]) 1]);
val oconf_ObjD = oconf_Obj' RS iffD1 RS spec RS spec RS mp;
val oconf_ObjI = oconf_Obj' RS iffD2;

val oconf_Arr = prove_goal thy
	"G,h|-Arr T cs::<=:<> = (!i v. cs i = Some v --> G,h|-v::<=:T)" (K [
	simp_tac (simpset() addsimps [lconf_Arr]) 1]);
val oconf_ArrD = oconf_Arr RS iffD1 RS spec RS spec RS mp;
val oconf_ArrI = oconf_Arr RS iffD2;

goalw thy [init_Obj_def] "!!X. [|is_class G C; wf_prog G|] ==> G,h|-init_Obj G C::<=:<>";
b y Simp_tac 1;
b y rtac lconf_init_vars 1;
b y Clarify_tac 1;
b y dtac is_type_fields 1;
b y   Auto_tac;
val oconf_init_Obj = result();

goalw thy [init_Arr_def] "!!X. is_type G T ==> G,h|-init_Arr T i::<=:<>";
b y stac oconf_Arr 1;
b y strip_tac 1;
b y Asm_full_simp_tac 1;
b y etac subst 1;
b y etac defval_conf 1;
val oconf_init_Arr = result();


section "conforms";

val conforms_SysXcpt = prove_goalw thy [conforms_def]
   "((Some (SysXcpt xn), s)::<=:(G, L)) = (Norm s::<=:(G, L))"
	(K [Asm_full_simp_tac 1]);
AddIffs [conforms_SysXcpt];

val raise_if_conforms = prove_goalw thy [raise_if_def]
   "((raise_if c xn x, h, l)::<=:(G, L)) = ((x, h, l)::<=:(G, L))"
	(K [Simp_tac 1]);
AddIffs [raise_if_conforms];

(*##
val np_conforms = prove_goal thy
   "((np a' x, h, l)::<=:(G, L)) = ((x, h, l)::<=:(G, L))"
	(K [Simp_tac 1]);
AddIffs [np_conforms];
*)

val conforms_NormI = prove_goalw thy [conforms_def, Let_def]
   "!!X. (x, h, l)::<=:(G, L) ==> Norm (h, l)::<=:(G, L)"
	(K [Asm_full_simp_tac 1]);

val conforms_heapD = prove_goalw thy [conforms_def, Let_def]
	"!!X. [|(x, h, l)::<=:(G, L); h a = Some obj|] ==> G,h|-obj::<=:<>"
	(K [Asm_full_simp_tac 1]);

val conforms_localD = prove_goalw thy [conforms_def, Let_def]
	 "!!X. (x, h, l)::<=:(G, L) ==> G,h|-l[::<=:]L" 
	(K [Asm_full_simp_tac 1]);

val conforms_XcptLocD = prove_goalw thy [conforms_def, Let_def] 
	"!!X. [|(x, h, l)::<=:(G, L); x = Some (XcptLoc a)|] ==> \
	\ G,h|-Addr a::<=:Class (SXcpt Throwable)"
	(K [Asm_full_simp_tac 1]);

val conformsI = prove_goalw thy [conforms_def, Let_def] 
"!!X. [|!a obj. h a = Some obj --> G,h|-obj::<=:<>; G,h|-l[::<=:]L; \
\     !a. x = Some (XcptLoc a) --> G,h|-Addr a ::<=: Class (SXcpt Throwable)|] ==>\
\ (x, h, l)::<=:(G, L)" (K [Auto_tac]);


val obj_ty_init_Obj = prove_goalw thy [init_Obj_def] 
	"obj_ty (init_Obj G C) = Class C" 
	(K [Simp_tac 1]);
Addsimps [obj_ty_init_Obj];

val conforms_hext = prove_goal thy
"!!X. [|(x, h, l)::<=:(G,L); h<=|h'; !a obj. h' a = Some obj --> G,h'|-obj::<=:<>|] ==> \
\ (x,h',l)::<=:(G,L)" (K [
	fast_tac (HOL_cs addSEs [conformsI, conf_hext, lconf_hext,
			conforms_localD, conforms_XcptLocD]) 1]);

val conforms_xconf = prove_goal thy
"!!X. [|(x, h, l)::<=:(G,L); !a. x' = Some (XcptLoc a) --> G,h|-Addr a::<=:Class (SXcpt Throwable)|] ==> \
\     (x',h, l)::<=:(G,L)" (K [
	fast_tac (HOL_cs addIs [conformsI] addSEs [conforms_heapD,
			conforms_localD]) 1]);

val conforms_xhext = prove_goal thy
"!!X. [|(x, h, l)::<=:(G,L); (x', h', l')::<=:(G, L); h'<=|h|] ==> \
\     (x',h, l)::<=:(G,L)" (K [
	etac conforms_xconf 1,
	fast_tac (HOL_cs addDs [conforms_XcptLocD, conf_hext]) 1]);

val conforms_XcptLoc = prove_goal thy
"!!X. [|(x, h, l)::<=:(G,L); G,h|-Addr a::<=:Class (SXcpt Throwable)|] ==> \
\     (Some (XcptLoc a),h, l)::<=:(G,L)" (K [
	fast_tac (claset() addSIs [conformsI] addSEs [conforms_heapD,
			conforms_localD]) 1]);

goal thy "!!h. [|(x, h, l)::<=:(G, L); G,h|-obj::<=:<>; \
\ !obj'. h a = Some obj' --> obj_ty obj = obj_ty obj'|] ==> \
\ (x, h[a|->obj], l)::<=:(G, L)";
b y subgoal_tac "h<=|h[a|->obj]" 1; (* needed twice *)
b y  SELECT_GOAL (EVERY [rtac hextI 1, Auto_tac]) 2;
b y rtac conforms_hext 1;
b y   atac 1;
b y  atac 1;
b y Clarify_tac 1;
b y thin_tac "All ?P" 1;
b y Auto_tac;      
b y dtac conforms_heapD 1;
b y  atac 1;
b y Fast_tac 1;
val conforms_upd_obj = result();

val unusedL_conforms = prove_goal thy 
"!!X. [|L vn = None; (x, h, l)::<=:(G, L)|] ==> (x, h, l[vn|->v])::<=:(G,L)"
    (K [fast_tac (HOL_cs addSIs [conformsI] addSEs [conforms_heapD,
	   conforms_localD, conforms_XcptLocD, lconf_new]) 1]);

val allocL_conforms = prove_goal thy 
"!!X. [|(x, h, l)::<=:(G, L); G,h|-v::<=:T|] ==> \
\ (x, h, l[vn|->v])::<=:(G, L[vn|->T])"
    (K [fast_tac (HOL_cs addSIs [conformsI] addSEs [conforms_heapD,
	conforms_localD RS lconf_upd, conforms_XcptLocD]) 1]);

val deallocL_conforms = prove_goal thy 
"!!X. [|(x, h, l)::<=:(G, L[vn|->T]); L vn = None|] ==> (x, h, l)::<=:(G,L)"
    (K [fast_tac (HOL_cs addSIs [conformsI] addSEs [conforms_heapD,
	 conforms_localD RS lconf_updD, conforms_XcptLocD]) 1]);


(******************************************************************************)

section "NewC";

goal thy "!!X. [|h a = None; (x, h, l)::<=:(G,L); wf_prog G; is_class G C|] ==> \
\(x, h[a|->init_Obj G C], l)::<=:(G, L)";
b y etac conforms_upd_obj 1;
b y  etac oconf_init_Obj 1;
b y  Auto_tac;
val NewC_conforms = result();

goal thy "!!X. [|wf_prog G; new_Addr h = Some (a, x); c_hupd[a|->init_Obj G C]\
\ (x, h, l) = (x', h', l'); Norm (h, l)::<=:(G, L); is_class G C|] ==>\
\ h<=|h' &  (x', h', l')::<=:(G, L) &  (x' = None --> G,h'|-Addr a::<=:Class C)";
b y dtac new_AddrD 1;
b y Auto_tac;
b y  fast_tac (HOL_cs addEs [NewC_conforms]) 1;
b y rtac conf_Obj_AddrI 1;
b y  rtac widen.refl 2;
b y  Asm_simp_tac 2;
b y simp_tac (simpset() addsimps [init_Obj_def]) 1;
val NewC_type_sound = result();


section "NewA";

goal thy "!!X. [|h a = None; (x, h, l)::<=:(G, L); is_type G T|] ==> \
\ (x, h[a|->init_Arr T i],l)::<=:(G, L)";
b y etac conforms_upd_obj 1;
b y  etac oconf_init_Arr 1;
b y Auto_tac;
val NewA_conforms = result();

goal thy "!!X. [|wf_prog G; c_hupd[a|->init_Arr T (the_Intg i')] \
\ (raise_if (the_Intg i' < $#0) NegArrSize x, h, l) = (x', h', l');\
\ is_type G T; new_Addr h = Some (a, x); h0<=|h; Norm (h, l)::<=:(G, L)|] ==> \
\ h0<=|h' &  (x', h', l')::<=:(G, L) &  (x' = None --> G,h'|-Addr a::<=:T[.])";
b y dtac new_AddrD 1;
b y case_tac "the_Intg i' < $#0" 1;
b y  Auto_tac;
b y  fast_tac (HOL_cs addEs [NewA_conforms]) 1;
b y etac conf_Arr_AddrI 1;
b y simp_tac (simpset() addsimps [init_Arr_def]) 1;
val NewA_type_sound = result();


section "Cast";

goal thy "!!X. [|wf_prog G; G|-T<=:? T'; x1 = None --> G,h|-x::<=:T|] ==> \
\raise_if (~  G,h|-x fits T') ClassCast x1 = None --> G,h|-x::<=:T'";
b y optionE_tac "x1" 1;
b y auto_tac (claset() addDs [fits_conf], simpset());
val Cast_conf = result();


section "LAcc";

val LAcc_conf = prove_goal thy 
 "!!X. [|Norm (h, l)::<=:(G, L); L vn = Some T|] ==> G,h|-the (l vn)::<=:T" (K [
	dtac conforms_localD 1,
	rewtac lconf_def,
	Force_tac 1]);


section "LAss";

val LAss_conf = prove_goal thy 
"!!X. [|wf_prog G; Norm (h, l)::<=:(G,L); G,h|-v::<=:T'; G|-T'<=:T; L vn = Some T|] ==>\
\ Norm (h, l[vn|->v])::<=:(G, L)" (K [
	dtac conf_widen 1,
	  atac 1,
	 atac 1,
	fast_tac (claset() addSIs [conformsI, lconf_upd2] addDs [conforms_heapD,
			 conforms_localD, conforms_XcptLocD]) 1]);


section "FAcc";

goal thy "!!X. [|wf_prog G; cfield G C fn = Some (fd, ft); \
\  (x, h, l)::<=:(G, L); G,h|-a'::<=:Class C; a' ~= Null|] ==> \
\ G,h|-the (snd (the_Obj (h (the_Addr a'))) (fn, fd))::<=:ft";
b y Auto_tac;
b y rtac (oconf_Obj RS iffD1 RS lconfD) 1;
b y  fast_tac (claset() addEs [widen_cfs_fields]) 2;
b y etac conforms_heapD 1;
b y  atac 1;
val FAcc_conf = result();


section "FAss";

goal thy "!!X. [|(x, h, l)::<=:(G, L); h a = Some (Obj C fs); wf_prog G; \
\ table_of (fields G C) (fn, fd) = Some T'; G,h|-v::<=:T; G|-T<=:T'|] ==> \
\ (x, h[a|->Obj C (fs[(fn, fd)|->v])], l)::<=:(G, L)";
b y rtac conforms_upd_obj 1;
b y   rtac oconf_ObjI 2;
b y auto_tac (claset() addDs [conforms_heapD, oconf_ObjD], simpset());
val conforms_upd_Obj = result();

goal thy "!!X. [|wf_prog G; a = the_Addr a'; (c, fs) = the_Obj (h a); \
\   (G, L)|-v::T'; G|-T'<=:fT; \
\   (G, L)|-aa::Class C; \
\   cfield G C fn = Some (fd, fT); h''<=|h'; \
\   x' = None --> G,h'|-a'::<=:Class C; h'<=|h; \
\   (x, h, l)::<=:(G, L); G,h|-y::<=:T'; np a' x' = None|] ==> \
\ h''<=|h[a|->Obj c (fs[(fn, fd)|->y])] &  \
\  (x, h[a|->Obj c (fs[(fn, fd)|->y])], l)::<=:(G, L) &  \
\ G,h[a|->Obj c (fs[(fn, fd)|->y])]|-y::<=:T'";
b y auto_tac (claset() addSaltern ("",dtac hextD2 THEN' atac), simpset());
b y   ALLGOALS (EVERY' [Asm_full_simp_tac, Clarify_tac]);
b y   fast_tac (claset() addEs [hext_upd_Obj]) 1;
b y  fast_tac (HOL_cs addEs [conf_upd_Obj RS iffD2]) 2;
b y dtac widen_cfs_fields 1;
b y   etac conforms_upd_Obj 3;
b y       ALLGOALS atac;
val FAss_type_sound = result();


section "AAcc";

goal thy "!!X. [|wf_prog G; G,h|-a'::<=:T[.]; h<=|h'; \
\ Norm (h', l)::<=:(G, L); G,h'|-i'::<=:PrimT IntDefer; \
\ raise_if (snd (the_Arr (h' (the_Addr a'))) (the_Intg i') = None) \
\ IndOutBound (np a' None) = None|] ==> \
\ G,h'|-the (snd (the_Arr (h' (the_Addr a'))) (the_Intg i'))::<=:T";
b y auto_tac (claset() addSaltern ("",dtac hextD THEN' atac), simpset());
b y not_None_tac 1;
b y fast_tac (claset() addDs [widen_Array_Array, conforms_heapD, oconf_ArrD]) 1;
val AAcc_conf = result();


section "AAss";

goal thy "!!X. [|(x, h, l)::<=:(G, L); h a = Some (Obj C fs); wf_prog G; \
\ table_of (fields G C) (fn, fd) = Some T'; G,h|-v::<=:T; G|-T<=:T'|] ==> \
\ (x, h[a|->Obj C (fs[(fn, fd)|->v])], l)::<=:(G, L)";

goal thy "!!X. [|(x, h, l)::<=:(G, L); h a = Some (Arr T cs); wf_prog G; G,h|-v::<=:T'; \
\ G|-T'<=:Ty; G|-T[.]<=:Ty[.]; G,h|-v fits T|] ==> (x, h[a|->Arr T (cs[i|->v])], l)::<=:(G, L)";
b y rtac conforms_upd_obj 1;
b y   rtac oconf_ArrI 2;
b y auto_tac (claset() addEs [fits_conf2]
		  addDs [conforms_heapD, oconf_ArrD], simpset());
val conforms_upd_Arr = result();

goal thy 
"!!X. [|wf_prog G; (T, cs) = the_Arr (xd (the_Addr a')); (G, L)|-ad::Tc[.]; \
\ (G, L)|-ia::PrimT IntDefer; (G, L)|-v::T'; G|-T'<=:Tc;  xa<=|xf; \
\ G,xf|-a'::<=:Tc[.]; xf<=|xg; G,xg|-i'::<=:PrimT IntDefer; xg<=|xd; \
\ Norm (xd, xh)::<=:(G, L); G,xd|-y::<=:T'; c_hupd[the_Addr a'|->Arr T \
\   (cs[the_Intg i'|->y])] (raise_if (~  G,xd|-y fits T) ArrStore \
\        (raise_if (cs (the_Intg i') = None) IndOutBound (np a' None)), \
\   xd, xh) = (a, aa, ab)|] ==> \
\ xa<=|aa &  (a, aa, ab)::<=:(G, L) &  (a = None --> G,aa|-y::<=:T')";
b y case_tac "a' = Null" 1;
b y  Force_tac 1;
b y case_tac "cs (the_Intg i') = None" 1;
b y  Force_tac 1;
b y Asm_full_simp_tac 1;
b y case_tac "~  G,xd|-y fits T" 1;
b y  Asm_full_simp_tac 1;
b y  Fast_tac 1;
b y auto_tac (claset() addSaltern ("",dtac hextD2 THEN' atac), simpset());
b y   ALLGOALS (EVERY' [Asm_full_simp_tac, Clarify_tac]);
b y   fast_tac (claset() addEs [hext_upd_Arr]) 1;
b y  fast_tac (HOL_cs addEs [conf_upd_Arr RS iffD2]) 2;
b y etac conforms_upd_Arr 1;
b y      ALLGOALS atac;
val AAss_type_sound = result();


section "Call";

goal thy "!!X. [|! (f,T):set lvars. is_type G T; (x, h, l)::<=:(G, L); \
\ h a = Some (Obj C fs'); G|-Class C<=:Class C'; G,h|-pv::<=:pT; wf_prog G|] ==>\
\Norm (h, init_vars lvars[This|->Addr a][pn|->pv])::<=:(G, table_of lvars[This|->Class C'][pn|->pT])";
b y rtac conformsI 1;
b y   fast_tac (HOL_cs addSDs [conforms_heapD]) 1;
b y  Fast_tac 2;
b y dtac conf_Obj_AddrI 1;
b y  atac 1;
b y fast_tac (HOL_cs addIs [lconf_upd, lconf_init_vars]) 1;
val conforms_call = result();

goal thy 
"!!X. [|(x, h, l)::<=:(G, L); h<=|h'; (x', h', l')::<=:(G, L')|] ==> (x', h', l)::<=:(G, L)";
b y rtac conforms_xconf 1;
b y  fast_tac (HOL_cs addDs [conforms_XcptLocD]) 2;
b y etac conforms_hext 1;
b y  atac 1;
b y fast_tac (HOL_cs addEs [conforms_heapD]) 1;
val conforms_return = result();

goal thy "!!X. [|wf_prog G; a' ~= Null; Norm (h, l)::<=:(G, L); \
\ max_spec G T (mn, pT) = {((md', (pn',rT')), pT')}; xc<=|xh; xh<=|h; G,h|-pv::<=:pT;\
\ (md,(pn,rT),lvars,blk,res)=the(cmethd G (fst(the_Obj (h (the_Addr a')))) (mn, pT'));\
\ !L. Norm (h, init_vars lvars[This|->a'][pn|->pv])::<=:(G, L) --> (G, L)|-blk::<> --> \
\         h<=|xi &  (xd, xi, xl)::<=:(G, L); \
\ !L. (xd, xi, xl)::<=:(G, L) --> (!T. (G, L)|-res::T --> \
\         xi<=|h' &  (x', h', xj)::<=:(G, L) &  (x' = None --> G,h'|-v::<=:T)); \
\ G,xh|-a'::<=:RefT T |] ==> \
\ xc<=|h' &  (x', h', l)::<=:(G, L) &  (x' = None --> G,h'|-v::<=:rT')";
b y dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1;
b y dtac (max_spec2appl_meths RS appl_methsD) 1;
b y dtac non_np_ObjD' 1 THEN 
    ALLGOALS (EVERY'[Clarify_tac, Asm_full_simp_tac]);
b y  Asm_full_simp_tac 1; (* ###*)
b y safe_tac (claset() delrules [conjI] 
		addSaltern ("",dtac hextD2 THEN' atac) addSss (simpset()));
b y Asm_full_simp_tac 1;

b y dtac (rewrite_rule [Let_def] Call_lemma) 1;
b y   atac 1;
b y  atac 1;
b y Clarify_tac 1;
b y Asm_full_simp_tac 1;

b y Clarify_tac 1;
b y EVERY'[dtac spec, etac impE] 1;
b y mp_tac 2;
b y  fast_tac (claset() addEs [conforms_call]) 1;
b y fast_tac (claset() addEs [conforms_return]) 1;
val Call_type_sound = result();

section "SXcpt";

(*
goal thy "!!s0 s1. [|wf_prog G; new_Addr (heap s1) = Some (a, x); \
\ Norm s0::<=:(G, L); heap s0<=|heap s1; Norm s1::<=:(G, L); \
\xobj = init_Obj G (SXcpt (if x = None then xn else OutOfMemory))|] ==> \
\heap s0<=|heap (hupd[a|->xobj] s1) &  (Some (XcptLoc a), hupd[a|->xobj] s1)::<=:(G, L)";
*)
goal thy "!!X. [|wf_prog G; new_Addr h1 = Some (a, x); \
\ Norm (h, l)::<=:(G, L); h<=|h1; Norm (h1, l1)::<=:(G, L)|] ==> \
\ h<=|h1[a|->init_Obj G (SXcpt (if x = None then xn else OutOfMemory))] &  \
\ (Some (XcptLoc a), h1[a|->init_Obj G (SXcpt (if x = None then xn else OutOfMemorl))], l1)::<=:(G, L)";
b y dtac new_AddrD 1;
b y asm_full_simp_tac (simpset() setloop (K no_tac)) 1;
b y rtac conjI 1;
b y  Fast_tac 1;
b y Clarify_tac 1;
b y rtac conforms_xconf 1;
b y  etac NewC_conforms 1;
b y    atac 1;
b y   atac 1;
b y  etac is_class_SXcpt 1;
b y Clarify_tac 1;
b y rtac conf_AddrI 1;
b y  rtac update_same 1;
b y Asm_simp_tac 1;
val SXcpt_type_sound = result();

section "Throw";

Delrules (map make_elim [non_np_ObjD, non_np_ArrD]);

goal thy "!!X. [|(x, h, l)::<=:(G, L); G,h|-a'::<=:Class tn; a' ~= Null; \
\ G|-Class tn<=:Class (SXcpt Throwable); wf_prog G|] ==> \
\ (Some (XcptLoc (the_Addr a')), h, l)::<=:(G, L)";
b y etac conforms_xconf 1;
b y forward_tac [conf_ClassD] 1;
b y auto_tac (claset() delrules (map make_elim [non_np_ObjD, non_np_ArrD]),
	      simpset());
val Throw_conforms = result();