135 apply (rule impI|rule allI|erule conjE|rule conjI)+ |
135 apply (rule impI|rule allI|erule conjE|rule conjI)+ |
136 apply (drule_tac obj = "Proc pa" in nodel_imp_exists, simp, simp) |
136 apply (drule_tac obj = "Proc pa" in nodel_imp_exists, simp, simp) |
137 apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp) |
137 apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp) |
138 apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp) |
138 apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp) |
139 apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e) |
139 apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e) |
140 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps |
140 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps dest:nodel_imp_exists[where obj = "Proc pa"] |
141 split:option.splits dest!:current_proc_has_sproc') |
141 split:option.splits dest!:current_proc_has_sproc') |
|
142 apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+ |
142 done |
143 done |
143 |
144 |
144 lemma initp_intact_I_exec: |
145 lemma initp_intact_I_exec: |
145 "\<lbrakk>initp_intact s; valid (Execute (new_proc s) f # Clone p (new_proc s) # s)\<rbrakk> |
146 "\<lbrakk>initp_intact s; valid (Execute (new_proc s) f # Clone p (new_proc s) # s)\<rbrakk> |
146 \<Longrightarrow> initp_intact (Execute (new_proc s) f # Clone p (new_proc s) # s)" |
147 \<Longrightarrow> initp_intact (Execute (new_proc s) f # Clone p (new_proc s) # s)" |
189 apply (frule no_del_event_cons_D, drule_tac obj = "Proc p" and s = s in nodel_imp_exists, simp) |
190 apply (frule no_del_event_cons_D, drule_tac obj = "Proc p" and s = s in nodel_imp_exists, simp) |
190 apply (subgoal_tac "p \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp) |
191 apply (subgoal_tac "p \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp) |
191 apply (erule_tac x = p in allE, case_tac e) |
192 apply (erule_tac x = p in allE, case_tac e) |
192 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps |
193 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps |
193 split:option.splits dest!:current_proc_has_sproc') |
194 split:option.splits dest!:current_proc_has_sproc') |
|
195 apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+ |
194 done |
196 done |
195 |
197 |
196 end |
198 end |
197 |
199 |
198 end |
200 end |