header {* \isaheader{Objects and the Heap} *}
theory Objects imports SubObj begin
section{* Objects *}
types
subo = "(path × (vname \<rightharpoonup> val))" -- "subobjects realized on the heap"
obj = "cname × subo set" -- "mdc and subobject"
constdefs
init_class_fieldmap :: "prog => cname => (vname \<rightharpoonup> val)"
"init_class_fieldmap P C ≡
map_of (map (λ(F,T).(F,default_val T)) (fst(snd(the(class P C)))) )"
inductive
init_obj :: "prog => cname => (path × (vname \<rightharpoonup> val)) => bool"
for P :: prog and C :: cname
where
"Subobjs P C Cs ==> init_obj P C (Cs,init_class_fieldmap P (last Cs))"
lemma init_obj_nonempty: "init_obj P C (Cs,fs) ==> Cs ≠ []"
by (fastsimp elim:init_obj.cases dest:Subobjs_nonempty)
lemma init_obj_no_Ref:
"[|init_obj P C (Cs,fs); fs F = Some(Ref(a',Cs'))|] ==> False"
by (fastsimp elim:init_obj.cases default_val_no_Ref
simp:init_class_fieldmap_def map_of_map)
lemma SubobjsSet_init_objSet:
"{Cs. Subobjs P C Cs} = {Cs. ∃vmap. init_obj P C (Cs,vmap)}"
by ( fastsimp intro:init_obj.intros elim:init_obj.cases)
constdefs
obj_ty :: "obj => ty"
"obj_ty obj ≡ Class (fst obj)"
-- "a new, blank object with default values in all fields:"
blank :: "prog => cname => obj"
"blank P C ≡ (C, Collect (init_obj P C))"
lemma [simp]: "obj_ty (C,S) = Class C"
by (simp add: obj_ty_def)
section{* Heap *}
types heap = "addr \<rightharpoonup> obj"
abbreviation
cname_of :: "heap => addr => cname" where
"cname_of hp a == fst (the (hp a))"
constdefs
new_Addr :: "heap => addr option"
"new_Addr h ≡ if ∃a. h a = None then Some(SOME a. h a = None) else None"
lemma new_Addr_SomeD:
"new_Addr h = Some a ==> h a = None"
by(fastsimp simp add:new_Addr_def split:if_splits intro:someI)
end