47 (ex_table_of (snd(snd(the(method (G,C) sig))))) of |
47 (ex_table_of (snd(snd(the(method (G,C) sig))))) of |
48 None \<Rightarrow> find_handler G (Some xc) hp frs |
48 None \<Rightarrow> find_handler G (Some xc) hp frs |
49 | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))" |
49 | Some handler_pc \<Rightarrow> (None, hp, ([xc], loc, C, sig, handler_pc)#frs)))" |
50 |
50 |
51 |
51 |
|
52 text {* |
|
53 System exceptions are allocated in all heaps, |
|
54 and they don't carry any information other than their type: |
|
55 *} |
|
56 constdefs |
|
57 preallocated :: "aheap \<Rightarrow> bool" |
|
58 "preallocated hp \<equiv> \<forall>x. hp (XcptRef x) = Some (Xcpt x, empty)" |
|
59 |
|
60 lemma preallocated_iff [iff]: |
|
61 "preallocated hp \<Longrightarrow> hp (XcptRef x) = Some (Xcpt x, empty)" |
|
62 by (unfold preallocated_def) fast |
52 |
63 |
53 lemma cname_of_xcp: |
64 lemma cname_of_xcp: |
54 "raise_system_xcpt b x = Some xcp \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" |
65 "raise_system_xcpt b x = Some xcp \<Longrightarrow> preallocated hp |
|
66 \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" |
55 proof - |
67 proof - |
56 assume "raise_system_xcpt b x = Some xcp" |
68 assume "raise_system_xcpt b x = Some xcp" |
57 hence "xcp = Addr (XcptRef x)" |
69 hence "xcp = Addr (XcptRef x)" |
58 by (simp add: raise_system_xcpt_def split: split_if_asm) |
70 by (simp add: raise_system_xcpt_def split: split_if_asm) |
59 moreover |
71 moreover |
60 have "hp (XcptRef x) = Some (Xcpt x, empty)" |
72 assume "preallocated hp" |
61 by (rule system_xcpt_allocated) |
73 hence "hp (XcptRef x) = Some (Xcpt x, empty)" .. |
62 ultimately |
74 ultimately |
63 show ?thesis by simp |
75 show ?thesis by simp |
64 qed |
76 qed |
65 |
77 |
66 end |
78 end |