equal
deleted
inserted
replaced
764 apply (erule CollectE, erule exE, erule conjE) |
764 apply (erule CollectE, erule exE, erule conjE) |
765 apply (rule CollectI, rule_tac x = obj in exI) |
765 apply (rule CollectI, rule_tac x = obj in exI) |
766 apply (simp add:co2sobj_writefile_unchange alive_simps) |
766 apply (simp add:co2sobj_writefile_unchange alive_simps) |
767 done |
767 done |
768 |
768 |
769 |
769 lemma s2ss_closefd: |
|
770 "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = ( |
|
771 case (file_of_proc_fd s p fd) of |
|
772 Some f \<Rightarrow> if (" |
770 |
773 |
771 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
774 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
772 s2ss_readfile s2ss_writefile |
775 s2ss_readfile s2ss_writefile |
773 |
776 |