header {* \isaheader{Exceptions} *}
theory Exceptions imports Objects begin
section {* Exceptions *}
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 :: "prog => heap"
"start_heap P ≡ empty (addr_of_sys_xcpt NullPointer \<mapsto> blank P NullPointer)
(addr_of_sys_xcpt ClassCast \<mapsto> blank P ClassCast)
(addr_of_sys_xcpt OutOfMemory \<mapsto> blank P OutOfMemory)"
preallocated :: "heap => bool"
"preallocated h ≡ ∀C ∈ sys_xcpts. ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"
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 (fastsimp simp:preallocated_def dom_def)
lemma preallocatedD:
"[| preallocated h; C ∈ sys_xcpts |] ==> ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"
by(auto simp add: preallocated_def sys_xcpts_def)
lemma preallocatedE [elim?]:
"[| preallocated h; C ∈ sys_xcpts; !!S. h (addr_of_sys_xcpt C) = Some(C,S) ==> 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 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)
subsection "@{term start_heap}"
lemma start_Subobj:
"[|start_heap P a = Some(C, S); (Cs,fs) ∈ S|] ==> Subobjs P C Cs"
by (fastsimp elim:init_obj.cases simp:start_heap_def blank_def
fun_upd_apply split:split_if_asm)
lemma start_SuboSet:
"[|start_heap P a = Some(C, S); Subobjs P C Cs|] ==> ∃fs. (Cs,fs) ∈ S"
by (fastsimp intro:init_obj.intros simp:start_heap_def blank_def
split:split_if_asm)
lemma start_init_obj: "start_heap P a = Some(C,S) ==> S = Collect (init_obj P C)"
by (auto simp:start_heap_def blank_def split:split_if_asm)
lemma start_subobj:
"[|start_heap P a = Some(C, S); ∃fs. (Cs, fs) ∈ S|] ==> Subobjs P C Cs"
by (fastsimp elim:init_obj.cases simp:start_heap_def blank_def
split:split_if_asm)
end