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