author | Christian Sternagel |
Thu, 30 Aug 2012 15:44:03 +0900 | |
changeset 49093 | fdc301f592c4 |
parent 35416 | d8d7d1b785af |
child 61361 | 8b5f00202e1a |
permissions | -rw-r--r-- |
13672 | 1 |
(* Title: HOL/MicroJava/J/Exceptions.thy |
2 |
Author: Gerwin Klein, Martin Strecker |
|
3 |
Copyright 2002 Technische Universitaet Muenchen |
|
4 |
*) |
|
5 |
||
16417 | 6 |
theory Exceptions imports State begin |
13672 | 7 |
|
8 |
text {* a new, blank object with default values in all fields: *} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
9 |
definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where |
13672 | 10 |
"blank G C \<equiv> (C,init_vars (fields(G,C)))" |
11 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
12 |
definition start_heap :: "'c prog \<Rightarrow> aheap" where |
13672 | 13 |
"start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
14 |
(XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
|
15 |
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
|
16 |
||
17 |
||
35102 | 18 |
abbreviation |
13672 | 19 |
cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" |
35102 | 20 |
where "cname_of hp v == fst (the (hp (the_Addr v)))" |
13672 | 21 |
|
22 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35102
diff
changeset
|
23 |
definition preallocated :: "aheap \<Rightarrow> bool" where |
13672 | 24 |
"preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
25 |
||
26 |
lemma preallocatedD: |
|
27 |
"preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
|
28 |
by (unfold preallocated_def) fast |
|
29 |
||
30 |
lemma preallocatedE [elim?]: |
|
31 |
"preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp" |
|
32 |
by (fast dest: preallocatedD) |
|
33 |
||
34 |
lemma cname_of_xcp: |
|
35 |
"raise_if b x None = Some xcp \<Longrightarrow> preallocated hp |
|
36 |
\<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" |
|
37 |
proof - |
|
38 |
assume "raise_if b x None = Some xcp" |
|
39 |
hence "xcp = Addr (XcptRef x)" |
|
40 |
by (simp add: raise_if_def split: split_if_asm) |
|
41 |
moreover |
|
42 |
assume "preallocated hp" |
|
43 |
then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" .. |
|
44 |
ultimately |
|
45 |
show ?thesis by simp |
|
46 |
qed |
|
47 |
||
48 |
lemma preallocated_start: |
|
49 |
"preallocated (start_heap G)" |
|
50 |
apply (unfold preallocated_def) |
|
51 |
apply (unfold start_heap_def) |
|
52 |
apply (rule allI) |
|
53 |
apply (case_tac x) |
|
54 |
apply (auto simp add: blank_def) |
|
55 |
done |
|
56 |
||
57 |
||
58 |
||
59 |
end |
|
60 |