src/HOL/MicroJava/J/Exceptions.thy
author nipkow
Wed Jan 04 19:22:53 2006 +0100 (2006-01-04)
changeset 18576 8d98b7711e47
parent 16417 9bc16273c2d4
child 30235 58d147683393
permissions -rw-r--r--
Reversed Larry's option/iff change.
     1 (*  Title:      HOL/MicroJava/J/Exceptions.thy
     2     ID:         $Id$
     3     Author:     Gerwin Klein, Martin Strecker
     4     Copyright   2002 Technische Universitaet Muenchen
     5 *)
     6 
     7 theory Exceptions imports State begin
     8 
     9 text {* a new, blank object with default values in all fields: *}
    10 constdefs
    11   blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
    12   "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
    13 
    14   start_heap :: "'c prog \<Rightarrow> aheap"
    15   "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
    16                         (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
    17                         (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
    18 
    19 
    20 consts
    21   cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
    22 
    23 translations
    24   "cname_of hp v" == "fst (the (hp (the_Addr v)))"
    25 
    26 
    27 constdefs
    28   preallocated :: "aheap \<Rightarrow> bool"
    29   "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
    30 
    31 lemma preallocatedD:
    32   "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
    33   by (unfold preallocated_def) fast
    34 
    35 lemma preallocatedE [elim?]:
    36   "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
    37   by (fast dest: preallocatedD)
    38 
    39 lemma cname_of_xcp:
    40   "raise_if b x None = Some xcp \<Longrightarrow> preallocated hp 
    41   \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
    42 proof -
    43   assume "raise_if b x None = Some xcp"
    44   hence "xcp = Addr (XcptRef x)"
    45     by (simp add: raise_if_def split: split_if_asm)
    46   moreover
    47   assume "preallocated hp" 
    48   then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
    49   ultimately
    50   show ?thesis by simp
    51 qed
    52 
    53 lemma preallocated_start:
    54   "preallocated (start_heap G)"
    55   apply (unfold preallocated_def)
    56   apply (unfold start_heap_def)
    57   apply (rule allI)
    58   apply (case_tac x)
    59   apply (auto simp add: blank_def)
    60   done
    61 
    62 
    63 
    64 end
    65