|
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 = State: |
|
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 |