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}"

definition addr_of_sys_xcpt :: "cname ⇒ addr"
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"
(*<*)by(simp add: sys_xcpts_def)(*>*)


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
                     addr_of_sys_xcpt_def preallocated_def)(*>*)


end