# Theory Exceptions

Up to index of Isabelle/HOL/MicroJava

theory Exceptions
imports State
begin

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