Up to index of Isabelle/Bali5
theory State = TypeRel:(* Title: isabelle/Bali/State.thy
ID: $Id: State.thy,v 1.64 2001/05/11 14:41:59 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
State for evaluation of Java expressions and statements
design issues:
* all kinds of objects (class instances, arrays, and class objects)
are handeled via a general object abstraction
* the heap and the map for class objects are combined into a single table
(recall (loc, obj) table × (tname, obj) table ~= (loc + tname, obj) table)
simplifications:
*)
theory State = TypeRel:
section "objects"
datatype obj_tag = (* tag for generic object *)
CInst tname (* class instance *)
| Arr ty int (* array with component type and length *)
(* | CStat the tag is irrelevant for a class object,
i.e. the static fields of a class *)
types vn = "fspec + int" (* variable name *)
obj = "obj_tag × (vn, val) table" (* generalized object *)
constdefs
the_Arr :: "obj option \<Rightarrow> ty × int × (vn, val) table"
"the_Arr obj \<equiv> \<epsilon>(T,k,t). obj = Some (Arr T k,t)"
lemma the_Arr_Arr [simp]: "the_Arr (Some (Arr T k,cs)) = (T,k,cs)"
apply (auto simp: the_Arr_def)
done
constdefs
upd_obj :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj"
"upd_obj n v \<equiv> \<lambda>(oi,vs). (oi,vs(n\<mapsto>v))"
lemma upd_obj_def2 [simp]: "upd_obj n v (oi, vs) = (oi, vs(n\<mapsto>v))"
apply (auto simp: upd_obj_def)
done
constdefs
obj_ty :: "obj \<Rightarrow> ty"
"obj_ty obj \<equiv> case fst obj of CInst C \<Rightarrow> Class C | Arr T k \<Rightarrow> T.[]"
lemma obj_ty_eq [intro!]: "obj_ty (oi,x) = obj_ty (oi,y)"
apply (simp add: obj_ty_def)
done
lemma obj_ty_cong [simp]: "obj_ty (oi, vs(n\<mapsto>v)) = obj_ty (oi, vs)"
apply (rule obj_ty_eq)
done
lemma obj_ty_CInst [simp]: "obj_ty (CInst C,x) = Class C"
apply (simp add: obj_ty_def)
done
lemma obj_ty_Arr [simp]: "obj_ty (Arr T i,x) = T.[]"
apply (simp add: obj_ty_def)
done
lemma obj_ty_widenD: "G\<turnstile>obj_ty (oi, vs)\<preceq>RefT t \<Longrightarrow> (\<exists>C. oi = CInst C) \<or> (\<exists>T k. oi = Arr T k)"
apply (unfold obj_ty_def)
apply (auto split add: obj_tag.split_asm)
done
constdefs
obj_class :: "obj \<Rightarrow> tname"
"obj_class obj \<equiv> case fst obj of CInst C \<Rightarrow> C | Arr T k \<Rightarrow> Object"
lemma obj_class_CInst [simp]: "obj_class (CInst C,fs) = C"
apply (auto simp: obj_class_def)
done
lemma obj_class_Arr [simp]: "obj_class (Arr T k,fs) = Object"
apply (auto simp: obj_class_def)
done
section "object references"
types oref = "loc + tname" (* generalized object reference *)
syntax
Heap :: "loc \<Rightarrow> oref"
Stat :: "tname \<Rightarrow> oref"
translations
"Heap" => "Inl"
"Stat" => "Inr"
constdefs
fields_table :: "prog \<Rightarrow> tname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table"
"fields_table G C P \<equiv> option_map snd \<circ> table_of (filter (split P) (fields G C))"
lemma fields_table_SomeI: "\<lbrakk>table_of (fields G C) n = Some (m,T); P n (m,T)\<rbrakk> \<Longrightarrow>
fields_table G C P n = Some T"
apply (unfold fields_table_def)
apply clarsimp
apply (rule exI)
apply (erule map_of_filter_in)
apply assumption
done
(* unused *)
lemma fields_table_SomeD': "fields_table G C P fn = Some T \<Longrightarrow>
\<exists>m. (fn,(m,T))\<in>set(fields G C)"
apply (unfold fields_table_def)
apply clarsimp
apply (drule map_of_SomeD)
apply auto
done
lemma fields_table_SomeD:
"\<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)"
apply (unfold fields_table_def)
apply clarsimp
apply (rule exI)
apply (erule table_of_filter_unique_SomeD)
apply assumption
done
constdefs
in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool" ("(_/ in'_bounds _)" [50, 51] 50)
"i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
"arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
var_tys :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table"
"var_tys G oi r \<equiv> case r of Heap a \<Rightarrow> (case oi of
CInst C \<Rightarrow> fields_table G C (\<lambda>n (m,fT). ¬static m) (+) empty
| Arr T k \<Rightarrow> empty (+) arr_comps T k)
| Stat C \<Rightarrow> fields_table G C
(\<lambda>(fn,fd) (m,fT). fd = C \<and> static m) (+) empty"
lemma var_tys_Some_eq:
"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 (\<lambda>n (m,fT). ¬static m) nt = Some T)
| Arr t k \<Rightarrow> (\<exists> i. n = Inr i \<and> i in_bounds k \<and> t = T))
| Inr C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> fields_table G C (\<lambda>(fn,fd) (m,fT). fd = C \<and> static m) nt = Some T))"
apply (unfold var_tys_def arr_comps_def)
apply (force split add: sum.split_asm sum.split obj_tag.split)
done
section "stores"
types globs (* global variables: heap and static variables *)
= "(oref , obj) table"
heap
= "(loc , obj) table"
locals
= "(lname, val) table" (* local variables *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
subsection "access"
constdefs
globs :: "st \<Rightarrow> globs"
"globs \<equiv> st_case (\<lambda>g l. g)"
locals :: "st \<Rightarrow> locals"
"locals \<equiv> st_case (\<lambda>g l. l)"
heap :: "st \<Rightarrow> heap"
"heap s \<equiv> globs s \<circ> Heap"
lemma globs_def2 [simp]: " globs (st g l) = g"
by (simp add: globs_def)
lemma locals_def2 [simp]: "locals (st g l) = l"
by (simp add: locals_def)
lemma heap_def2 [simp]: "heap s a=globs s (Heap a)"
by (simp add: heap_def)
syntax
val_this :: "st \<Rightarrow> val"
lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
translations
"val_this s" == "the (locals s This)"
"lookup_obj s a'" == "the (heap s (the_Addr a'))"
subsection "memory allocation"
constdefs
new_Addr :: "heap \<Rightarrow> loc option"
"new_Addr h \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
apply (unfold new_Addr_def)
apply auto
apply (drule split_paired_All [THEN iffD2])
apply (fast intro: someI2)
done
lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a"
apply (drule new_AddrD)
apply auto
done
lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
apply (unfold new_Addr_def)
apply (frule not_Some_eq [THEN iffD2])
apply auto
apply (drule not_Some_eq [THEN iffD2])
apply auto
apply (fast intro!: someI2)
done
subsection "initialization"
syntax
init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
translations
"init_vals vs" == "option_map default_val \<circ> vs"
lemma init_arr_comps_base [simp]: "init_vals (arr_comps T #0) = empty"
apply (unfold arr_comps_def in_bounds_def)
apply (rule ext)
apply auto
done
lemma init_arr_comps_step [simp]:
"0 < j \<Longrightarrow> init_vals (arr_comps T j ) =
init_vals (arr_comps T (j-#1))(j-#1\<mapsto>default_val T)"
apply (unfold arr_comps_def in_bounds_def)
apply (rule ext)
apply auto
done
subsection "update"
constdefs
gupd :: "oref \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st" ("gupd'(_\<mapsto>_')"[10,10]1000)
"gupd r obj \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
lupd :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" ("lupd'(_\<mapsto>_')"[10,10]1000)
"lupd vn v \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
upd_gobj :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
"upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
set_locals :: "locals \<Rightarrow> st \<Rightarrow> st"
"set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
init_obj :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
"init_obj G oi r \<equiv> gupd(r\<mapsto>(oi, init_vals (var_tys G oi r)))"
syntax
init_class_obj :: "prog \<Rightarrow> tname \<Rightarrow> st \<Rightarrow> st"
translations
"init_class_obj G C" == "init_obj G arbitrary (Inr C)"
lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
apply (unfold gupd_def)
apply (simp (no_asm))
done
lemma lupd_def2 [simp]: "lupd(vn\<mapsto>v) (st g l) = st g (l(vn\<mapsto>v))"
apply (unfold lupd_def)
apply (simp (no_asm))
done
lemma globs_gupd [simp]: "globs (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
apply (induct "s")
by (simp add: gupd_def)
lemma globs_lupd [simp]: "globs (lupd(vn\<mapsto>v ) s) = globs s"
apply (induct "s")
by (simp add: lupd_def)
lemma locals_gupd [simp]: "locals (gupd(r\<mapsto>obj) s) = locals s"
apply (induct "s")
by (simp add: gupd_def)
lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
apply (induct "s")
by (simp add: lupd_def)
lemma globs_upd_gobj_new [rule_format (no_asm), simp]:
"globs s r = None \<longrightarrow> globs (upd_gobj r n v s) = globs s"
apply (unfold upd_gobj_def)
apply (induct "s")
apply auto
done
lemma globs_upd_gobj_upd [rule_format (no_asm), simp]:
"globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"
apply (unfold upd_gobj_def)
apply (induct "s")
apply auto
done
lemma locals_upd_gobj [simp]: "locals (upd_gobj r n v s) = locals s"
apply (induct "s")
by (simp add: upd_gobj_def)
lemma globs_init_obj [simp]: "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)"
apply (unfold init_obj_def)
apply (simp (no_asm))
done
lemma locals_init_obj [simp]: "locals (init_obj G oi r s) = locals s"
by (simp add: init_obj_def)
lemma surjective_st [simp]: "st (globs s) (locals s) = s"
apply (induct "s")
by auto
lemma surjective_st_init_obj:
"st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s"
apply (subst locals_init_obj [THEN sym])
apply (rule surjective_st)
done
lemma heap_heap_upd [simp]: "heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)"
apply (rule ext)
apply (simp (no_asm))
done
lemma heap_stat_upd [simp]: "heap (st (g(Inr C\<mapsto>obj)) l) = heap (st g l)"
apply (rule ext)
apply (simp (no_asm))
done
lemma heap_local_upd [simp]: "heap (st g (l(vn\<mapsto>v))) = heap (st g l)"
apply (rule ext)
apply (simp (no_asm))
done
lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)"
apply (rule ext)
apply (simp (no_asm))
done
lemma heap_gupd_Stat [simp]: "heap (gupd(Stat C\<mapsto>obj) s) = heap s"
apply (rule ext)
apply (simp (no_asm))
done
lemma heap_lupd [simp]: "heap (lupd(vn\<mapsto>v) s) = heap s"
apply (rule ext)
apply (simp (no_asm))
done
(*
lemma heap_upd_gobj_Heap: "!!a. heap (upd_gobj (Heap a) n v s) = ?X"
apply (rule ext)
apply (simp (no_asm))
apply (case_tac "globs s (Heap a)")
apply auto
*)
lemma heap_upd_gobj_Stat [simp]: "heap (upd_gobj (Stat C) n v s) = heap s"
apply (rule ext)
apply (simp (no_asm))
apply (case_tac "globs s (Stat C)")
apply auto
done
lemma set_locals_def2 [simp]: "set_locals l (st g l') = st g l"
apply (unfold set_locals_def)
apply (simp (no_asm))
done
lemma set_locals_id [simp]: "set_locals (locals s) s = s"
apply (unfold set_locals_def)
apply (induct_tac "s")
apply (simp (no_asm))
done
lemma set_set_locals [simp]: "set_locals l (set_locals l' s) = set_locals l s"
apply (unfold set_locals_def)
apply (induct_tac "s")
apply (simp (no_asm))
done
lemma locals_set_locals [simp]: "locals (set_locals l s) = l"
apply (unfold set_locals_def)
apply (induct_tac "s")
apply (simp (no_asm))
done
lemma globs_set_locals [simp]: "globs (set_locals l s) = globs s"
apply (unfold set_locals_def)
apply (induct_tac "s")
apply (simp (no_asm))
done
lemma heap_set_locals [simp]: "heap (set_locals l s) = heap s"
apply (unfold heap_def)
apply (induct_tac "s")
apply (simp (no_asm))
done
section "exceptions"
datatype xcpt (* exception *)
= XcptLoc loc (* location of allocated execption object *)
| StdXcpt xname (* intermediate standard exception, see Eval.thy *)
consts
the_XcptLoc :: "xcpt \<Rightarrow> loc"
the_StdXcpt :: "xcpt \<Rightarrow> xname"
primrec "the_XcptLoc (XcptLoc a) = a"
primrec "the_StdXcpt (StdXcpt x) = x"
types
xopt = "xcpt option"
constdefs
xcpt_if :: "bool \<Rightarrow> xopt \<Rightarrow> xopt \<Rightarrow> xopt"
"xcpt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
lemma xcpt_if_True_None [simp]: "xcpt_if True x None = x"
by (simp add: xcpt_if_def)
lemma xcpt_if_True_not_None [simp]: "x \<noteq> None \<Longrightarrow> xcpt_if True x y \<noteq> None"
by (simp add: xcpt_if_def)
lemma xcpt_if_False [simp]: "xcpt_if False x y = y"
by (simp add: xcpt_if_def)
lemma xcpt_if_Some [simp]: "xcpt_if c x (Some y) = Some y"
by (simp add: xcpt_if_def)
lemma xcpt_if_not_None [simp]: "y \<noteq> None \<Longrightarrow> xcpt_if c x y = y"
apply (simp add: xcpt_if_def)
by auto
lemma split_xcpt_if:
"P (xcpt_if c x' x) = ((c \<and> x = None \<longrightarrow> P x') \<and> (¬ (c \<and> x = None) \<longrightarrow> P x))"
apply (unfold xcpt_if_def)
apply (split split_if)
apply auto
done
syntax
raise_if :: "bool \<Rightarrow> xname \<Rightarrow> xopt \<Rightarrow> xopt"
np :: "val \<Rightarrow> xopt \<Rightarrow> xopt"
check_neg:: "val \<Rightarrow> xopt \<Rightarrow> xopt"
translations
"raise_if c xn" == "xcpt_if c (Some (StdXcpt xn))"
"np v" == "raise_if (v = Null) NullPointer"
"check_neg i'" == "raise_if (the_Intg i'<0) NegArrSize"
lemma raise_if_None [simp]: "(raise_if c x y = None) = (¬c \<and> y = None)"
apply (simp add: xcpt_if_def)
by auto
declare raise_if_None [THEN iffD1, dest!]
lemma if_raise_if_None [simp]:
"((if b then y else raise_if c x y) = None) = ((c \<longrightarrow> b) \<and> y = None)"
apply (simp add: xcpt_if_def)
apply auto
done
lemma raise_if_SomeD [dest!]:
"raise_if c x y = Some z \<Longrightarrow> c \<and> z=StdXcpt x \<and> y=None \<or> (y=Some z)"
apply (case_tac y)
apply (case_tac c)
apply (simp add: xcpt_if_def)
apply (simp add: xcpt_if_def)
apply auto
done
section "full program state"
types
state = "xopt × st" (* state including exception information *)
syntax
Norm :: "st \<Rightarrow> state"
translations
"Norm s" == "(None,s)"
"xopt" <= (type) "State.xcpt option"
"xopt" <= (type) "xcpt option"
"state" <= (type) "xopt × State.st"
"state" <= (type) "xopt × st"
lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
apply (erule_tac x = "(Some k,y)" in all_dupE)
apply (erule_tac x = "(None ,y)" in allE)
apply clarify
done
lemma state_not_single: "All (op = (x::('a option) × 'b)) \<Longrightarrow> R"
apply (drule_tac x = "(if fst x = None then Some ?x else None,?y)" in spec)
apply clarsimp
done
constdefs
normal :: "state \<Rightarrow> bool"
"normal \<equiv> \<lambda>s. fst s = None"
lemma normal_def2 [simp]: "normal s = (fst s = None)"
apply (unfold normal_def)
apply (simp (no_asm))
done
constdefs
heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
"heap_free n \<equiv> \<lambda>s. atleast_free (heap (snd s)) n"
lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (snd s)) n"
apply (unfold heap_free_def)
apply simp
done
subsection "update"
constdefs
xupd :: "(xopt \<Rightarrow> xopt) \<Rightarrow> state \<Rightarrow> state"
"xupd f \<equiv> prod_fun f id"
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
"supd \<equiv> prod_fun id"
lemma xupd_def2 [simp]: "xupd f (x,s) = (f x,s)"
by (simp add: xupd_def)
lemma xupd_xcpt_if_False [simp]: "\<And> s. xupd (xcpt_if False xo) s = s"
by simp
lemma supd_def2 [simp]: "supd f (x,s) = (x,f s)"
by (simp add: supd_def)
lemma supd_lupd [simp]: "\<And> s. supd (lupd vn v ) s = (fst s,lupd vn v (snd s))"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done
lemma supd_gupd [simp]: "\<And> s. supd (gupd r obj) s = (fst s,gupd r obj (snd s))"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done
lemma supd_init_obj [simp]:
"supd (init_obj G oi r) s = (fst s, init_obj G oi r (snd s))"
apply (unfold init_obj_def)
apply (simp (no_asm))
done
syntax
set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
restore_lvars :: "state \<Rightarrow> state \<Rightarrow> state"
translations
"set_lvars l" == "supd (set_locals l)"
"restore_lvars s' s" == "set_lvars (locals (snd s')) s"
lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done
lemma set_lvars_id [simp]: "\<And> s. set_lvars (locals (snd s)) s = s"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (simp (no_asm))
done
section "initialisation test"
constdefs
inited :: "tname \<Rightarrow> globs \<Rightarrow> bool"
"inited C g \<equiv> g (Stat C) \<noteq> None"
initd :: "tname \<Rightarrow> state \<Rightarrow> bool"
"initd C \<equiv> inited C \<circ> globs \<circ> snd"
lemma not_inited_empty [simp]: "¬inited C empty"
apply (unfold inited_def)
apply (simp (no_asm))
done
lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
apply (unfold inited_def)
apply (auto split add: st.split)
done
lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
apply (unfold inited_def)
apply (simp (no_asm))
done
lemma not_initedD: "¬ inited C g \<Longrightarrow> g (Stat C) = None"
apply (unfold inited_def)
apply (erule notnotD)
done
lemma initedD: "inited C g \<Longrightarrow> \<exists>oi fs. g (Stat C) = Some (oi, fs)"
apply (unfold inited_def)
apply auto
done
lemma initd_def2 [simp]: "initd C s = inited C (globs (snd s))"
apply (unfold initd_def)
apply (simp (no_asm))
done
end
lemma the_Arr_Arr:
the_Arr (Some (Arr T k, cs)) = (T, k, cs)
lemma upd_obj_def2:
upd_obj n v (oi, vs) = (oi, vs(n|->v))
lemma obj_ty_eq:
obj_ty (oi, x) = obj_ty (oi, y)
lemma obj_ty_cong:
obj_ty (oi, vs(n|->v)) = obj_ty (oi, vs)
lemma obj_ty_CInst:
obj_ty (CInst C, x) = Class C
lemma obj_ty_Arr:
obj_ty (Arr T i, x) = T.[]
lemma obj_ty_widenD:
G|-obj_ty (oi, vs)<=:RefT t ==> (EX C. oi = CInst C) | (EX T k. oi = Arr T k)
lemma obj_class_CInst:
obj_class (CInst C, fs) = C
lemma obj_class_Arr:
obj_class (Arr T k, fs) = Object
lemma fields_table_SomeI:
[| table_of (fields G C) n = Some (m, T); P n (m, T) |] ==> fields_table G C P n = Some T
lemma fields_table_SomeD':
fields_table G C P fn = Some T ==> EX m. (fn, m, T) : set (fields G C)
lemma fields_table_SomeD:
[| fields_table G C P fn = Some T; unique (fields G C) |] ==> EX m. table_of (fields G C) fn = Some (m, T)
lemma var_tys_Some_eq:
(var_tys G oi r n = Some T) =
(case r of
Inl a =>
case oi of
CInst C =>
EX nt. n = Inl nt & fields_table G C (%n (m, fT). ¬ id m) nt = Some T
| Arr t k => EX i. n = Inr i & i in_bounds k & t = T
| Inr C =>
EX nt. n = Inl nt &
fields_table G C (%(fn, fd) (m, fT). fd = C & id m) nt = Some T)
lemma globs_def2:
globs (st g l) = g
lemma locals_def2:
locals (st g l) = l
lemma heap_def2:
heap s a = globs s (Inl a)
lemma new_AddrD:
new_Addr h = Some a ==> h a = None
lemma new_AddrD2:
new_Addr h = Some a ==> ALL b. h b ~= None --> b ~= a
lemma new_Addr_SomeI:
h a = None ==> EX b. new_Addr h = Some b & h b = None
lemma init_arr_comps_base:
init_vals (arr_comps T #0) = empty
lemma init_arr_comps_step:
0 < j
==> init_vals (arr_comps T j) = init_vals (arr_comps T (j - #1))(j - #1
|->default_val T)
lemma gupd_def2:
gupd(r\<mapsto>obj) (st g l) = st (g(r|->obj)) l
lemma lupd_def2:
lupd(vn\<mapsto>v) (st g l) = st g (l(vn|->v))
lemma globs_gupd:
globs (gupd(r\<mapsto>obj) s) = globs s(r|->obj)
lemma globs_lupd:
globs (lupd(vn\<mapsto>v) s) = globs s
lemma locals_gupd:
locals (gupd(r\<mapsto>obj) s) = locals s
lemma locals_lupd:
locals (lupd(vn\<mapsto>v) s) = locals s(vn|->v)
lemma globs_upd_gobj_new:
globs s r = None ==> globs (upd_gobj r n v s) = globs s
lemma globs_upd_gobj_upd:
globs s r = Some obj ==> globs (upd_gobj r n v s) = globs s(r|->upd_obj n v obj)
lemma locals_upd_gobj:
locals (upd_gobj r n v s) = locals s
lemma globs_init_obj:
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)
lemma locals_init_obj:
locals (init_obj G oi r s) = locals s
lemma surjective_st:
st (globs s) (locals s) = s
lemma surjective_st_init_obj:
st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s
lemma heap_heap_upd:
heap (st (g(Inl a|->obj)) l) = heap (st g l)(a|->obj)
lemma heap_stat_upd:
heap (st (g(Inr C|->obj)) l) = heap (st g l)
lemma heap_local_upd:
heap (st g (l(vn|->v))) = heap (st g l)
lemma heap_gupd_Heap:
heap (gupd(Inl a\<mapsto>obj) s) = heap s(a|->obj)
lemma heap_gupd_Stat:
heap (gupd(Inr C\<mapsto>obj) s) = heap s
lemma heap_lupd:
heap (lupd(vn\<mapsto>v) s) = heap s
lemma heap_upd_gobj_Stat:
heap (upd_gobj (Inr C) n v s) = heap s
lemma set_locals_def2:
set_locals l (st g l') = st g l
lemma set_locals_id:
set_locals (locals s) s = s
lemma set_set_locals:
set_locals l (set_locals l' s) = set_locals l s
lemma locals_set_locals:
locals (set_locals l s) = l
lemma globs_set_locals:
globs (set_locals l s) = globs s
lemma heap_set_locals:
heap (set_locals l s) = heap s
lemma xcpt_if_True_None:
xcpt_if True x None = x
lemma xcpt_if_True_not_None:
x ~= None ==> xcpt_if True x y ~= None
lemma xcpt_if_False:
xcpt_if False x y = y
lemma xcpt_if_Some:
xcpt_if c x (Some y) = Some y
lemma xcpt_if_not_None:
y ~= None ==> xcpt_if c x y = y
lemma split_xcpt_if:
P (xcpt_if c x' x) = ((c & x = None --> P x') & (¬ (c & x = None) --> P x))
lemma raise_if_None:
((raise_if c x) y = None) = (¬ c & y = None)
lemma if_raise_if_None:
((if b then y else (raise_if c x) y) = None) = ((c --> b) & y = None)
lemma raise_if_SomeD:
(raise_if c x) y = Some z ==> c & z = StdXcpt x & y = None | y = Some z
lemma single_stateE:
ALL Z. Z = s ==> False
lemma state_not_single:
All (op = x) ==> R
lemma normal_def2:
normal s = (fst s = None)
lemma heap_free_def2:
heap_free n s = atleast_free (heap (snd s)) n
lemma xupd_def2:
xupd f (x, s) = (f x, s)
lemma xupd_xcpt_if_False:
xupd (xcpt_if False xo) s = s
lemma supd_def2:
supd f (x, s) = (x, f s)
lemma supd_lupd:
supd lupd(vn\<mapsto>v) s = (fst s, lupd(vn\<mapsto>v) (snd s))
lemma supd_gupd:
supd gupd(r\<mapsto>obj) s = (fst s, gupd(r\<mapsto>obj) (snd s))
lemma supd_init_obj:
supd (init_obj G oi r) s = (fst s, init_obj G oi r (snd s))
lemma set_set_lvars:
(set_lvars l) ((set_lvars l') s) = (set_lvars l) s
lemma set_lvars_id:
(set_lvars (locals (snd s))) s = s
lemma not_inited_empty:
¬ inited C empty
lemma inited_gupdate:
inited C (g(r|->obj)) = (inited C g | r = Inr C)
lemma inited_init_class_obj:
inited C (globs ((init_class_obj G C) s))
lemma not_initedD:
¬ inited C g ==> g (Inr C) = None
lemma initedD:
inited C g ==> EX oi fs. g (Inr C) = Some (oi, fs)
lemma initd_def2:
initd C s = inited C (globs (snd s))