Theory Exceptions

(*  Title:      HOL/MicroJava/J/Exceptions.thy
    ID:         $Id: Exceptions.thy,v 1.3 2008-10-07 14:07:44 fhaftmann Exp $
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{Exceptions} *}

theory Exceptions imports Objects begin

constdefs
  NullPointer :: cname
  "NullPointer ≡ ''NullPointer''"

  ClassCast :: cname
  "ClassCast ≡ ''ClassCast''"

  OutOfMemory :: cname
  "OutOfMemory ≡ ''OutOfMemory''"

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

  addr_of_sys_xcpt :: "cname => addr"
  "addr_of_sys_xcpt s ≡ if s = NullPointer then 0 else
                        if s = ClassCast then 1 else
                        if s = OutOfMemory then 2 else undefined"

  start_heap :: "'c prog => heap"
  "start_heap G ≡ empty (addr_of_sys_xcpt NullPointer \<mapsto> blank G NullPointer)
                        (addr_of_sys_xcpt ClassCast \<mapsto> blank G ClassCast)
                        (addr_of_sys_xcpt OutOfMemory \<mapsto> blank G OutOfMemory)"

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


section "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)(*>*)


section "@{term preallocated}"

lemma preallocated_dom [simp]: 
  "[| preallocated h; C ∈ sys_xcpts |] ==> addr_of_sys_xcpt C ∈ dom h"
(*<*)by (fastsimp 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 ==> typeofh (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)" 
(*<*)by (auto elim: preallocatedE)(*>*)


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


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


lemma preallocated_hext:
  "[| preallocated h; h \<unlhd> 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