--- a/Current_prop.thy	Sat Jun 08 09:59:33 2013 +0800
+++ b/Current_prop.thy	Sun Jun 09 14:28:58 2013 +0800
@@ -47,6 +47,10 @@
   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 using not_deleted_init_proc by auto
 
+lemma info_shm_flow_in_procs:
+  "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
+by (auto simp:info_flow_shm_def intro:procs_of_shm_prop2)
+
 lemma has_same_inode_in_current:
   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
 by (auto simp add:has_same_inode_def current_files_def)