--- a/Flask.thy	Mon Jun 24 09:01:42 2013 +0800
+++ b/Flask.thy	Mon Jun 24 15:22:37 2013 +0800
@@ -473,17 +473,25 @@
     (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})"
 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>"
 
+(*
 inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
   "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
 | "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk>
    \<Longrightarrow> info_flow_shm s p p''"
-(*
+*)
+definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "one_flow_shm s h from to \<equiv> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> (\<exists> flag. (to, flag) \<in> procs_of_shm s h)"
+
+fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "self_shm s p p' = (p = p' \<and> p' \<in> current_procs s)"
+
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
-  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. 
-    (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
-*)
+  "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" 
+
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
 where