133 by (auto dest:valid_os valid_rc valid_cons) |
133 by (auto dest:valid_os valid_rc valid_cons) |
134 |
134 |
135 from initp fstdel vs' have "source_proc s' p = Some p" |
135 from initp fstdel vs' have "source_proc s' p = Some p" |
136 apply (induct s', simp) |
136 apply (induct s', simp) |
137 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp) |
137 apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp) |
138 by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp) |
138 by (case_tac a, auto dest:not_deleted_imp_exists) |
139 with exp initp vs' obtain r fr pt u |
139 with exp initp vs' obtain r fr pt u |
140 where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)" |
140 where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)" |
141 apply (frule_tac current_proc_has_sobj, simp) |
141 apply (frule_tac current_proc_has_sobj, simp) |
142 by (simp add:obj2sobj.simps split:option.splits, blast) |
142 by (simp add:obj2sobj.simps split:option.splits, blast) |
143 with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"] |
143 with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"] |