146 thm has_same_inode_def

   146 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   147 apply (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits)

   147 

   148 

   148 lemma same_inode_files_prop8:

   149   "f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"

   150 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   494 thm has_same_inode_def

   496 

   495 done

   497 (* should delete has_same_inode !?!?*)

   498 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   498   "\<lbrakk>valid (CloseFd p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (

   501   "\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (

   501                         Some f \<Rightarrow> (if (f "

   504                         Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>

   505                                        f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f. 

   506                                        f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))

   507                                    then (case (cf2sfile s f, co2sobj s (O_file f')) of

   508                                            (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)

   509                                          | _                              \<Rightarrow> None)

   510                                    else co2sobj s obj)

   511                      | _       \<Rightarrow> co2sobj s obj)

   512       | O_proc p' \<Rightarrow> (if (p = p') 

   513                       then (case (cp2sproc (CloseFd p fd # s) p) of

   514                               Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   515                             | _       \<Rightarrow> None)

   516                       else co2sobj s obj)

   517       | _         \<Rightarrow> co2sobj s obj) "

   518 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   519 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   520 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   521            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   522 

   523 apply (frule is_file_in_current)

   524 apply (case_tac "file_of_proc_fd s p fd")

   525 apply (simp add:tainted_eq_Tainted)

   526 apply (drule_tac f' = list in cf2sfiles_closefd, simp add:current_files_closefd, simp)

   527 apply (frule_tac f' = list in cf2sfiles_closefd, simp)

   528 apply (simp add:is_file_simps current_files_simps)

   529 apply (auto simp add:tainted_eq_Tainted cf2sfile_closefd split:if_splits option.splits

   530   dest!:current_file_has_sfile' dest:hung_file_in_current)[1]

   531 

   532 apply (simp add:is_dir_simps, frule is_dir_in_current)

   533 apply (frule_tac f = list in cf2sfile_closefd)

   534 apply (clarsimp simp:current_files_closefd split:option.splits)

   535 apply (drule file_of_pfd_is_file', simp+)

   536 done

   537 

   538 lemma co2sobj_unlink:

   539   "\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (

   540       case obj of

   541         O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 

   542                         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))

   543                      then (case (cf2sfile s f, co2sobj s (O_file f')) of

   544                              (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)

   545                            | _                              \<Rightarrow> None)

   546                      else co2sobj s obj

   547       | _         \<Rightarrow> co2sobj s obj)"

   548 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   549 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   550 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   551            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   552 apply (frule is_file_in_current)

   553 apply (frule_tac f' = list in cf2sfile_unlink, simp)

   554 apply (frule_tac f' = list in cf2sfiles_unlink, simp)

   555 apply (simp add:is_file_simps current_files_simps)

   556 apply (auto simp add:tainted_eq_Tainted is_file_in_current split:if_splits option.splits

   557   dest!:current_file_has_sfile')[1]

   558 

   559 apply (simp add:is_dir_simps, frule is_dir_in_current)

   560 apply (frule_tac f' = list in cf2sfile_unlink)

   561 apply (clarsimp simp:current_files_unlink split:option.splits)

   562 apply (drule file_dir_conflict, simp+)

   563 done

   564 

   565 lemma co2sobj_rmdir:

   566   "\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"

   567 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   568 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   569 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   570            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   571 apply (simp add:is_file_simps dir_is_empty_def)

   572 apply (case_tac "f = list", drule file_dir_conflict, simp, simp)

   573 apply (simp add:cf2sfiles_other)

   574 apply (auto simp:cf2sfile_simps dest:is_dir_in_current)

   575 done

   576 

   577 lemma co2sobj_mkdir:

   578   "\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (

   579       if (obj = O_dir f) 

   580       then (case (cf2sfile (Mkdir p f i # s) f) of 

   581               Some sf \<Rightarrow> Some (S_dir sf)

   582             | _       \<Rightarrow> None)

   583       else co2sobj s obj)"

   584 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   585 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   586 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   587            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   588 apply (frule_tac cf2sfiles_other, simp+)

   589 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir)

   590 apply (frule current_file_has_sfile, simp, erule exE, simp)

   591 apply (drule cf2sfile_mkdir1, simp+)

   592 done

   593 

   594 lemma same_inodes_Tainted:

   595   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"

   596 apply (frule same_inode_files_prop8, frule same_inode_files_prop7)

   597 apply (auto intro:has_same_inode_Tainted)

   598 done

   599 

   600 lemma co2sobj_linkhard:

   601   "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> 

   602    \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (

   603     case obj of

   604       O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)

   605                    then (case (cf2sfile (LinkHard p oldf f # s) f) of

   606                            Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> Tainted s))

   607                          | _       \<Rightarrow> None)

   608                    else co2sobj s obj

   609     | _         \<Rightarrow> co2sobj s obj)"

   610 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   611 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   612 apply (auto simp:cp2sproc_simps tainted_eq_Tainted split:option.splits if_splits

   613            dest!:current_proc_has_sp' intro:info_flow_shm_Tainted)[1]

   614 apply (frule_tac cf2sfiles_linkhard, simp+)

   615 apply (frule_tac f' = f in cf2sfile_linkhard, simp add:current_files_linkhard)

   616 apply (auto simp:is_file_simps sectxt_of_obj_simps current_files_simps is_file_in_current same_inodes_Tainted

   617   split:option.splits if_splits dest:Tainted_in_current 

   618   dest!:current_has_sec' current_file_has_sfile')[1]

   619 

   620 apply (frule is_dir_in_current, simp add:current_files_linkhard is_dir_simps is_dir_in_current)

   621 apply (frule is_dir_in_current)

   622 apply (frule current_file_has_sfile, simp)

   623 apply (drule cf2sfile_linkhard1, simp+)

   624 done

   625 

   626 lemma co2sobj_truncate:

   627   "\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (

   628       case obj of

   629         O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)

   630                      then Some (S_file (cf2sfiles s f') (O_file f' \<in> Tainted s \<or> O_proc p \<in> Tainted s))

   631                      else co2sobj s obj

   632       | _         \<Rightarrow> co2sobj s obj)"

   633 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   634 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   635 

   636 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   637              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   638                   same_inode_files_prop6

   639              dest:is_file_in_current is_dir_in_current)

   640 

   641 (* should delete has_same_inode !?!?*)

   642 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)

   643 

   644 lemma co2sobj_kill:

   645   "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"

   646 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   647 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   648 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   649              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   650                   same_inode_files_prop6

   651              dest:is_file_in_current is_dir_in_current)

   652 done

   653 

   654 lemma co2sobj_exit:

   655   "\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"

   656 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   657 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   658 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   659              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   660                   same_inode_files_prop6

   661              dest:is_file_in_current is_dir_in_current)

   662 done

   663 

   664 lemma co2sobj_createmsgq:

   665   "\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (

   666       case obj of

   667         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of

   668                                          Some sq \<Rightarrow> Some (S_msgq sq)

   669                                        | _       \<Rightarrow> None)

   670                      else co2sobj s obj

   671       | _        \<Rightarrow> co2sobj s obj)"

   672 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   673 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   674 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   675              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   676                   same_inode_files_prop6

   677              dest!:current_has_smsgq'

   678              dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)

   679 done

   680 

   681 lemma co2sobj_sendmsg:

   682   "\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (

   683       case obj of

   684         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of

   685                                          Some sq \<Rightarrow> Some (S_msgq sq)

   686                                        | _       \<Rightarrow> None)

   687                      else co2sobj s obj

   688       | _        \<Rightarrow> co2sobj s obj)"

   689 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   690 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   691 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   692              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   693                   same_inode_files_prop6

   694              dest!:current_has_smsgq'

   695              dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)

   696 done

   697 

   698 lemma co2sobj_recvmsg:

   699   "\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (

   700       case obj of

   701         O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of

   702                                          Some sq \<Rightarrow> Some (S_msgq sq)

   703                                        | _       \<Rightarrow> None)

   704                      else co2sobj s obj

   705       | O_proc p' \<Rightarrow> if (info_flow_shm s p p' \<and> O_msg q m \<in> Tainted s)

   706                      then (case (cp2sproc s p') of

   707                              Some sp \<Rightarrow> Some (S_proc sp True)

   708                            | _       \<Rightarrow> None)

   709                      else co2sobj s obj

   710       | _         \<Rightarrow> co2sobj s obj)"

   711 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   712 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   713 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   714              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   715                   same_inode_files_prop6

   716              dest!:current_has_smsgq'

   717              dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)

   718 done

   719 

   720 lemma co2sobj_removemsgq:

   721   "\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk> 

   722    \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"

   723 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   724 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   725 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   726              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   727                   same_inode_files_prop6

   728              dest!:current_has_smsgq'

   729              dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)

   730 done

   731 

   732 lemma co2sobj_createshm:

   733   "\<lbrakk>valid (CreateShM p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = co2sobj s obj"

   734 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   735 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   736 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   737              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   738                   same_inode_files_prop6 ch2sshm_simps

   739              dest!:current_shm_has_sh'

   740              dest:is_file_in_current is_dir_in_current)

   741 done

   742 

   743 lemma co2sobj_detach:

   744   "\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (

   745       case obj of

   746         O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of

   747                                          Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s))

   748                                        | _       \<Rightarrow> None)

   749                      else co2sobj s obj

   750       | _         \<Rightarrow> co2sobj s obj)"

   751 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   752 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   753 

   754 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   755              simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted

   756                   same_inode_files_prop6 ch2sshm_simps

   757              dest!:current_shm_has_sh'

   758              dest:is_file_in_current is_dir_in_current)

   759 done

   760 

   761 lemma co2sobj_deleteshm:

   762   "\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (

   763       case obj of

   764         O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of

   765                         Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s))

   766                       | _       \<Rightarrow> None)

   767       | _         \<Rightarrow> co2sobj s obj)"

   768 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   769 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   770 

   771 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'

   772              simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted

   773                   same_inode_files_prop6 ch2sshm_simps

   774              dest!:current_shm_has_sh' 

   775              dest:is_file_in_current is_dir_in_current)

   776 done

   777 

   778 lemma co2sobj_attach:

   779   "\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (

   780       case obj of

   781         O_proc p' \<Rightarrow> if (p' = p)

   782                      then (case (cp2sproc (Attach p h flag # s) p) of

   783                              Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> Tainted s \<or> 

   784               (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)))

   785                            | _       \<Rightarrow> None)

   786                      else if (\<exists> flag'. (p', flag') \<in> procs_of_shm s h)

   787                           then (case (cp2sproc s p') of 

   788                                   Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> Tainted s \<or>

   789               (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR)))

   790                                 | _       \<Rightarrow> None)

   791                           else co2sobj s obj

   792       | _         \<Rightarrow> co2sobj s obj)"

   793 apply (frule vt_grant_os, frule vd_cons, case_tac obj)

   794 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)

   795 

   796 apply (rule conjI|rule impI|erule exE)+

   797 apply (simp split:option.splits)

   798 apply (rule impI, frule current_proc_has_sp, simp)

   799 apply ((erule exE)+, auto simp:cp2sproc_attach tainted_eq_Tainted)[1]

   800 apply (rule impI|rule conjI)+

   801 apply (subgoal_tac "p \<in> current_procs (Attach p h flag # s)")

   802 apply (drule_tac p = p in current_proc_has_sp, simp, erule exE)

   803 apply (auto simp:tainted_eq_Tainted)[1]

   804 apply (simp, rule impI)

   805 apply (subgoal_tac "nat \<in> current_procs (Attach p h flag # s)")

   806 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)

   807 apply (drule_tac p = nat in current_proc_has_sp, simp, erule exE)

   808 apply (auto simp:cp2sproc_attach tainted_eq_Tainted)[1]

   809 apply simp

   810 

   811 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' 

   812              simp:current_files_simps cf2sfiles_simps cf2sfile_simps tainted_eq_Tainted

   813                   same_inode_files_prop6 

   814              dest:is_file_in_current is_dir_in_current)

   815 done

   816 

   508     \<forall> 

   823     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   824     \<forall> p fd. e \<noteq> ReadFile p fd;

   825     \<forall> p fd. e \<noteq> WriteFile p fd;

   826     \<forall> p fd. e \<noteq> CloseFd p fd;

   827     \<forall> p f. e \<noteq> UnLink p f;

   828     \<forall> p f. e \<noteq> Rmdir p f;

   829     \<forall> p f i. e \<noteq> Mkdir p f i;

   830     \<forall> p f f'. e \<noteq> LinkHard p f f';

   831     \<forall> p f len. e \<noteq> Truncate p f len;

   832     \<forall> p q. e \<noteq> CreateMsgq p q;

   833     \<forall> p q m. e \<noteq> SendMsg p q m;

   834     \<forall> p q m. e \<noteq> RecvMsg p q m;

   835     \<forall> p q. e \<noteq> RemoveMsgq p q;

   836     \<forall> p h. e \<noteq> CreateShM p h;

   837     \<forall> p h flag. e \<noteq> Attach p h flag;

   838     \<forall> p h. e \<noteq> Detach p h;

   839     \<forall> p h. e \<noteq> DeleteShM p h

   510 

   841 apply (frule vt_grant, case_tac e)

   511 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open

   842 apply (auto intro:co2sobj_kill co2sobj_exit)

   843 done

   844 

   845 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile

   846   co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard

   847   co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg

   848   co2sobj_removemsgq co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm