# Theory Exceptions

theory Exceptions
imports State
```(*  Title:      HOL/MicroJava/J/Exceptions.thy
Author:     Gerwin Klein, Martin Strecker
*)

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 ↦ blank G (Xcpt NullPointer))
(XcptRef ClassCast ↦ blank G (Xcpt ClassCast))
(XcptRef OutOfMemory ↦ 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: if_split_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)