equal
deleted
inserted
replaced
35 "raise_if b x None = Some xcp \<Longrightarrow> preallocated hp |
35 "raise_if b x None = Some xcp \<Longrightarrow> preallocated hp |
36 \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" |
36 \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x" |
37 proof - |
37 proof - |
38 assume "raise_if b x None = Some xcp" |
38 assume "raise_if b x None = Some xcp" |
39 hence "xcp = Addr (XcptRef x)" |
39 hence "xcp = Addr (XcptRef x)" |
40 by (simp add: raise_if_def split: split_if_asm) |
40 by (simp add: raise_if_def split: if_split_asm) |
41 moreover |
41 moreover |
42 assume "preallocated hp" |
42 assume "preallocated hp" |
43 then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" .. |
43 then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" .. |
44 ultimately |
44 ultimately |
45 show ?thesis by simp |
45 show ?thesis by simp |