# Theory Exceptions

```(*  Title:      HOL/MicroJava/J/Exceptions.thy

Author:     Gerwin Klein, Martin Strecker
Copyright   2002 Technische Universitaet Muenchen
*)

section ‹Exceptions›

theory Exceptions imports Objects begin

definition NullPointer :: cname
where
"NullPointer ≡ ''NullPointer''"

definition ClassCast :: cname
where
"ClassCast ≡ ''ClassCast''"

definition OutOfMemory :: cname
where
"OutOfMemory ≡ ''OutOfMemory''"

definition sys_xcpts :: "cname set"
where
"sys_xcpts  ≡  {NullPointer, ClassCast, OutOfMemory}"

where
"addr_of_sys_xcpt s ≡ if s = NullPointer then 0 else
if s = ClassCast then 1 else
if s = OutOfMemory then 2 else undefined"

definition start_heap :: "'c prog ⇒ heap"
where
"start_heap G ≡ Map.empty (addr_of_sys_xcpt NullPointer ↦ blank G NullPointer,
addr_of_sys_xcpt ClassCast ↦ blank G ClassCast,
addr_of_sys_xcpt OutOfMemory ↦ blank G OutOfMemory)"

definition preallocated :: "heap ⇒ bool"
where
"preallocated h ≡ ∀C ∈ sys_xcpts. ∃fs. h(addr_of_sys_xcpt C) = Some (C,fs)"

subsection "System exceptions"

lemma [simp]: "NullPointer ∈ sys_xcpts ∧ OutOfMemory ∈ sys_xcpts ∧ ClassCast ∈ sys_xcpts"

lemma sys_xcpts_cases [consumes 1, cases set]:
"⟦ C ∈ sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast⟧ ⟹ P C"
(*<*)by (auto simp add: sys_xcpts_def)(*>*)

subsection "@{term preallocated}"

lemma preallocated_dom [simp]:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ addr_of_sys_xcpt C ∈ dom h"
(*<*)by (fastforce simp:preallocated_def dom_def)(*>*)

lemma preallocatedD:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ ∃fs. h(addr_of_sys_xcpt C) = Some (C, fs)"
(*<*)by(auto simp add: preallocated_def sys_xcpts_def)(*>*)

lemma preallocatedE [elim?]:
"⟦ preallocated h;  C ∈ sys_xcpts; ⋀fs. h(addr_of_sys_xcpt C) = Some(C,fs) ⟹ P h C⟧
⟹ P h C"
(*<*)by (fast dest: preallocatedD)(*>*)

lemma cname_of_xcp [simp]:
"⟦ preallocated h; C ∈ sys_xcpts ⟧ ⟹ cname_of h (addr_of_sys_xcpt C) = C"
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_ClassCast [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)"
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_OutOfMemory [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)"
(*<*)by (auto elim: preallocatedE)(*>*)

lemma typeof_NullPointer [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)"
(*<*)by (auto elim: preallocatedE)(*>*)

lemma preallocated_hext:
"⟦ preallocated h; h ⊴ h' ⟧ ⟹ preallocated h'"
(*<*)by (simp add: preallocated_def hext_def)(*>*)

(*<*)
lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new  = preallocated_hext [OF _ hext_new]
(*>*)

lemma preallocated_start:
"preallocated (start_heap P)"
(*<*)by (auto simp add: start_heap_def blank_def sys_xcpts_def fun_upd_apply