theory Exceptions imports State begin

text {* a new, blank object with default values in all fields: *}

definition blank :: "'c prog => cname => obj" where

"blank G C ≡ (C,init_vars (fields(G,C)))"

definition start_heap :: "'c prog => aheap" where

"start_heap G ≡ empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))

(XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))

(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"

abbreviation

cname_of :: "aheap => val => cname"

where "cname_of hp v == fst (the (hp (the_Addr v)))"

definition preallocated :: "aheap => bool" where

"preallocated hp ≡ ∀x. ∃fs. hp (XcptRef x) = Some (Xcpt x, fs)"

lemma preallocatedD:

"preallocated hp ==> ∃fs. hp (XcptRef x) = Some (Xcpt x, fs)"

by (unfold preallocated_def) fast

lemma preallocatedE [elim?]:

"preallocated hp ==> (!!fs. hp (XcptRef x) = Some (Xcpt x, fs) ==> P hp) ==> P hp"

by (fast dest: preallocatedD)

lemma cname_of_xcp:

"raise_if b x None = Some xcp ==> preallocated hp

==> cname_of (hp::aheap) xcp = Xcpt x"

proof -

assume "raise_if b x None = Some xcp"

hence "xcp = Addr (XcptRef x)"

by (simp add: raise_if_def split: split_if_asm)

moreover

assume "preallocated hp"

then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..

ultimately

show ?thesis by simp

qed

lemma preallocated_start:

"preallocated (start_heap G)"

apply (unfold preallocated_def)

apply (unfold start_heap_def)

apply (rule allI)

apply (case_tac x)

apply (auto simp add: blank_def)

done

end