(* Title: HOL/MicroJava/J/Exceptions.thy ID: $Id: Exceptions.thy,v 1.2 2005/06/17 14:13:09 haftmann Exp $ Author: Gerwin Klein, Martin Strecker Copyright 2002 Technische Universitaet Muenchen *) theory Exceptions imports State begin text {* a new, blank object with default values in all fields: *} constdefs blank :: "'c prog => cname => obj" "blank G C ≡ (C,init_vars (fields(G,C)))" start_heap :: "'c prog => aheap" "start_heap G ≡ empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" consts cname_of :: "aheap => val => cname" translations "cname_of hp v" == "fst (the (hp (the_Addr v)))" constdefs preallocated :: "aheap => bool" "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: split_if_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) apply (auto simp add: blank_def) done end
lemma preallocatedD:
preallocated hp ==> ∃fs. hp (XcptRef x) = Some (Xcpt x, fs)
lemma preallocatedE:
[| preallocated hp; !!fs. hp (XcptRef x) = Some (Xcpt x, fs) ==> P hp |] ==> P hp
lemma cname_of_xcp:
[| raise_if b x None = Some xcp; preallocated hp |] ==> cname_of hp xcp = Xcpt x
lemma preallocated_start:
preallocated (start_heap G)