equal
deleted
inserted
replaced
599 |
599 |
600 lemma obj2sobj_ipc_remains_cons: |
600 lemma obj2sobj_ipc_remains_cons: |
601 "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk> |
601 "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk> |
602 \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri" |
602 \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri" |
603 apply (frule valid_cons, frule valid_os, case_tac e) |
603 apply (frule valid_cons, frule valid_os, case_tac e) |
604 by (auto simp:ni_init_deled ni_notin_curi split:option.splits |
604 by (auto split:option.splits dest!:current_proc_has_role') |
605 dest!:current_proc_has_role') |
|
606 |
605 |
607 lemma obj2sobj_ipc_remains_cons': |
606 lemma obj2sobj_ipc_remains_cons': |
608 "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk> |
607 "\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk> |
609 \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri" |
608 \<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri" |
610 by (auto intro!:obj2sobj_ipc_remains_cons nodel_imp_un_deleted |
609 by (auto intro!:obj2sobj_ipc_remains_cons nodel_imp_un_deleted |