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) |
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) |
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"] |
144 have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp |
144 have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp |
145 |
145 |
146 from exp' vs' obtain r' fr' pt' u' srp' where |
146 from exp' vs' obtain r' fr' pt' u' srp' where |
147 SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'" |
147 SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'" |