diff -r e298d755bc35 -r 622516c0fe34 Current_prop.thy
--- a/Current_prop.thy	Thu Jul 11 07:52:06 2013 +0800
+++ b/Current_prop.thy	Thu Aug 01 12:19:42 2013 +0800
@@ -4,6 +4,8 @@
 begin
 (*>*)
 
+ML {*quick_and_dirty := true*}
+
 context flask begin
 
 lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
@@ -143,232 +145,624 @@
 lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm
   one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit
 
-
-inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
-where
-  ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"
-| ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
+type_synonym t_edge_shm = "t_process \<times> t_shm \<times> t_process"
+fun Fst:: "t_edge_shm \<Rightarrow> t_process" where "Fst (a, b, c) = a"
+fun Snd:: "t_edge_shm \<Rightarrow> t_shm" where "Snd (a, b, c) = b"
+fun Trd:: "t_edge_shm \<Rightarrow> t_process" where "Trd (a, b, c) = c"
 
-lemma Info_flow_trans_aux:
-  "Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"
-apply (erule Info_flow_shm.induct)
-by (auto intro:Info_flow_shm.intros)
+fun edge_related:: "t_edge_shm list \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> bool"
+where
+  "edge_related [] p h = False"
+| "edge_related ((from, shm, to) # path) p h = 
+     (if (((p = from) \<or> (p = to)) \<and> (h = shm)) then True 
+      else edge_related path p h)"
+         
+inductive path_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  pbs1: "p \<in> current_procs s \<Longrightarrow> path_by_shm s p [] p"
+| pbs2: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path)\<rbrakk> 
+         \<Longrightarrow> path_by_shm s p ((p', h, p'')# path) p''"
 
-lemma Info_flow_trans:
-  "\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
-by (auto dest:Info_flow_trans_aux)
 
-lemma one_flow_flows:
-  "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p'"
-apply (rule Info_flow_shm.intros(2), simp_all)
-apply (rule Info_flow_shm.intros(1))
+lemma one_step_path: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [(p, h, p')] p'"
+apply (rule_tac path = "[]" and p = p in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1))
 apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)
 done
 
-lemma ifs_flow': "\<lbrakk>one_flow_shm s h p p'; Info_flow_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
-apply (drule one_flow_flows, simp+)
-apply (erule Info_flow_trans, simp+)
+lemma pbs_prop1:
+  "path_by_shm s p path p' \<Longrightarrow> ((path = []) = (p = p')) \<and> (path \<noteq> [] \<longrightarrow> p \<in> set (map Fst path))"
+apply (erule path_by_shm.induct, simp)
+apply (auto simp:one_flow_shm_def)
+done
+
+lemma pbs_prop2:
+  "path_by_shm s p path p' \<Longrightarrow> (path = []) = (p = p')"
+by (simp add:pbs_prop1)
+
+lemma pbs_prop2':
+  "path_by_shm s p path p \<Longrightarrow> path = []"
+by (simp add:pbs_prop2)
+
+lemma pbs_prop3:
+  "\<lbrakk>path_by_shm s p path p'; path \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set (map Fst path)"
+by (drule pbs_prop1, auto)
+
+lemma pbs_prop4[rule_format]:
+  "path_by_shm s p path p'\<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<in> set (map Trd path)"
+by (erule path_by_shm.induct, auto)
+
+lemma pbs_prop5[rule_format]:
+  "path_by_shm s p path p' \<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<notin> set (map Fst path)"
+by (erule path_by_shm.induct, auto simp:one_flow_shm_def)
+
+lemma pbs_prop6_aux:
+  "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Fst pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"
+apply (erule path_by_shm.induct)
+apply simp
+apply clarify
+apply (case_tac "pb = p'", simp)
+apply (rule_tac x = path in exI, simp)
+apply (erule one_step_path, simp)
+apply (erule_tac x = pb in ballE, simp_all, clarsimp)
+apply (rule_tac x = pathab in exI, simp)
+apply (erule pbs2, auto)
+done
+
+lemma pbs_prop6:
+  "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Fst pathac); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"
+by (drule pbs_prop6_aux, auto)
+
+lemma pbs_prop7_aux:
+  "path_by_shm s pa pathac pc \<Longrightarrow> valid s \<longrightarrow> (\<forall> pb \<in> set (map Trd pathac). \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab)"
+apply (erule path_by_shm.induct)
+apply simp
+apply clarify
+apply (case_tac "pb = p''", simp)
+apply (rule_tac x = "(p',h,p'') # path" in exI, simp)
+apply (rule conjI, erule pbs2, simp+)
+apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)
+apply (erule_tac x = pb in ballE, simp_all, clarsimp)
+apply (rule_tac x = pathab in exI, simp)
+apply (erule pbs2, auto)
+done
+
+lemma pbs_prop7:
+  "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Trd pathac); valid s\<rbrakk>
+   \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"
+by (drule pbs_prop7_aux, drule mp, simp, erule_tac x = pb in ballE, auto)
+
+lemma pbs_prop8:
+  "path_by_shm s p path p' \<Longrightarrow> (set (map Fst path) - {p}) = (set (map Trd path) - {p'})"
+proof (induct rule:path_by_shm.induct)
+  case (pbs1 p s)
+  thus ?case by simp
+next
+  case (pbs2 s p path p' h p'')
+  assume p1:"path_by_shm s p path p'" and p2: "set (map Fst path) - {p} = set (map Trd path) - {p'}"
+    and p3: "one_flow_shm s h p' p''" and p4: "p'' \<notin> set (map Fst path)" 
+  show "set (map Fst ((p', h, p'') # path)) - {p} = set (map Trd ((p', h, p'') # path)) - {p''}"
+    (is "?left = ?right")
+  proof (cases "path = []")
+    case True
+    with p1 have "p = p'" by (drule_tac pbs_prop2, simp)
+    thus ?thesis using True
+      using p2 by (simp)
+  next
+    case False
+    with p1 have a1: "p \<noteq> p'" by (drule_tac pbs_prop2, simp)
+    from p3 have a2: "p' \<noteq> p''" by (simp add:one_flow_shm_def)
+    from p1 False have a3: "p' \<in> set (map Trd path)" by (drule_tac pbs_prop4, simp+)
+    from p4 p1 False have a4: "p \<noteq> p''" by (drule_tac pbs_prop3, auto)
+    with p2 a2 p4 have a5: "p'' \<notin> set (map Trd path)" by auto
+    
+    have "?left = (set (map Fst path) - {p}) \<union> {p'}" using a1 by auto
+    moreover have "... = (set (map Trd path) - {p'}) \<union> {p'}"  
+      using p2 by auto
+    moreover have "... = set (map Trd path)" using a3 by auto
+    moreover have "... = set (map Trd path) - {p''}" using a5 by simp
+    moreover have "... = ?right" by simp
+    ultimately show ?thesis by simp
+  qed
+qed
+
+lemma pbs_prop9_aux[rule_format]:
+  "path_by_shm s p path p' \<Longrightarrow> h \<in> set (map Snd path) \<and> valid s \<longrightarrow> (\<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha))"
+apply (erule path_by_shm.induct, simp)
+apply (rule impI, case_tac "h \<in> set (map Snd path)", simp_all)
+apply (erule exE|erule conjE)+
+apply (rule_tac x = pa in exI, rule_tac x = pb in exI, rule_tac x = patha in exI, simp)
+apply (rule pbs2, auto)
+apply (rule_tac x = p' in exI, rule_tac x = p'' in exI, rule_tac x = path in exI, simp)
+apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)
 done
 
-lemma Info_flow_shm_cases1:
-  "\<lbrakk>Info_flow_shm s pa pb; 
-    \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P;
-    \<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk>
-   \<Longrightarrow> P"
-by (erule Info_flow_shm.cases, auto)
+lemma pbs_prop9:
+  "\<lbrakk>h \<in> set (map Snd path); path_by_shm s p path p'; valid s\<rbrakk>
+   \<Longrightarrow> \<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> 
+        one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha)"
+by (rule pbs_prop9_aux, auto)
+
+lemma path_by_shm_trans_aux[rule_format]:
+  "path_by_shm s p' path' p'' \<Longrightarrow> valid s \<longrightarrow> (\<forall> p path. path_by_shm s p path p' \<longrightarrow> (\<exists> path''. path_by_shm s p path'' p''))"
+proof (induct rule:path_by_shm.induct)
+  case (pbs1 p s)
+  thus ?case
+    by (clarify, rule_tac x = path in exI, simp)
+next
+  case (pbs2 s p path p' h p'')
+  hence p1: "path_by_shm s p path p'" and p2: "one_flow_shm s h p' p''" 
+    and p3: "valid s \<longrightarrow> (\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p'))"
+    and p4: "p'' \<notin> set (map Fst path)" by auto
+  show ?case
+  proof clarify
+    fix pa path'
+    assume p5: "path_by_shm s pa path' p" and p6: "valid s"
+    with p3 obtain path'' where a1: "path_by_shm s pa path'' p'" by auto
+    have p3': "\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p')" 
+      using p3 p6 by simp
+    show "\<exists>path''. path_by_shm s pa path'' p''"
+    proof (cases "p'' \<in> set (map Fst path'')")
+      case True
+      then obtain res where "path_by_shm s pa res p''" using a1 pbs_prop6 p6 by blast
+      thus ?thesis by auto
+    next
+      case False
+      with p2 a1 show ?thesis 
+        apply (rule_tac x = "(p', h, p'') # path''" in exI)
+        apply (rule path_by_shm.intros(2), auto)
+        done
+    qed
+  qed
+qed
+
+lemma path_by_shm_trans:
+  "\<lbrakk>path_by_shm s p path p'; path_by_shm s p' path' p''; valid s\<rbrakk> \<Longrightarrow> \<exists> path''. path_by_shm s p path'' p''"
+by (drule_tac p' = p' and p'' = p'' in path_by_shm_trans_aux, auto)
+
+lemma path_by_shm_intro1_prop:
+  "\<not> path_by_shm s p [] p \<Longrightarrow> p \<notin> current_procs s"
+by (auto dest:path_by_shm.intros(1))
+
+lemma path_by_shm_intro3:
+  "\<lbrakk>path_by_shm s p path from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; 
+    to \<notin> set (map Fst path); from \<noteq> to\<rbrakk>
+   \<Longrightarrow> path_by_shm s p ((from, h, to)#path) to"
+apply (rule path_by_shm.intros(2), simp_all)
+by (auto simp:one_flow_shm_def)
+
+lemma path_by_shm_intro4:
+  "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [] p"
+by (drule procs_of_shm_prop2, simp, simp add:path_by_shm.intros(1))
 
-lemma Info_flow_shm_prop1:
-  "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" 
-by (rule notI, drule Info_flow_shm.intros(1), simp)
+lemma path_by_shm_intro5:
+  "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>
+   \<Longrightarrow> path_by_shm s from [(from, h, to)] to"
+apply (rule_tac p' = "from" and h = h in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
+apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)
+done
+
+(* p'' \<notin> set (map Fst path): not duplicated target process;
+ * p1 - ha \<rightarrow> p2; p2 - hb \<rightarrow> p3; p3 - ha \<rightarrow> p4; so path_by_shm p1 [(p3,ha,p4), (p2,hb,p3),(p1,ha,p2)] p4,
+ * but this could be also path_by_shm p1 [(p1,ha,p4)] p4, so the former one is redundant!  *)
+
+inductive path_by_shm':: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  pbs1': "p \<in> current_procs s \<Longrightarrow> path_by_shm' s p [] p"
+| pbs2': "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path); 
+           h \<notin> set (map Snd path)\<rbrakk> 
+          \<Longrightarrow> path_by_shm' s p ((p', h, p'')# path) p''"
 
-lemma Info_flow_shm_intro3:
-  "\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>
-   \<Longrightarrow> Info_flow_shm s p to"
-apply (case_tac "from = to", simp)
-apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)
-by (rule_tac x = flag in exI, simp)
+lemma pbs_imp_pbs'[rule_format]:
+  "path_by_shm s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm' s p path' p')"
+apply (erule path_by_shm.induct)
+apply (rule impI, rule_tac x = "[]" in exI, erule pbs1')
+apply (rule impI, simp,  erule exE, case_tac "h \<in> set (map Snd path)")
+apply (drule_tac s = s and p = p and p' = p' in pbs_prop9, simp+) defer
+apply (rule_tac x = "(p', h, p'') # path" in exI, erule pbs2', simp+) 
+apply ((erule exE|erule conjE)+)
+apply (rule_tac x = "(pa, h, p'') # patha" in exI)
+apply (erule pbs2', auto simp:one_flow_shm_def)
+done
+
+lemma pbs'_imp_pbs[rule_format]:
+  "path_by_shm' s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm s p path' p')"
+apply (erule path_by_shm'.induct)
+apply (rule impI, rule_tac x = "[]" in exI, simp add:pbs1)
+apply (rule impI, rule_tac x = "(p', h, p'') # path" in exI, simp add:pbs2)
+done
+
+definition flow_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
+where
+  "flow_by_shm s p p' \<equiv> \<exists> path. path_by_shm s p path p'"
+
+lemma flow_by_shm_intro':
+  "valid s \<Longrightarrow> flow_by_shm s p p' = (\<exists> path. path_by_shm' s p path p')"
+by (auto simp:flow_by_shm_def intro: pbs_imp_pbs' pbs'_imp_pbs)
+
+lemma one_step_flows: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p'"
+by (drule one_step_path, auto simp:flow_by_shm_def)
+
+lemma flow_by_shm_trans:
+  "\<lbrakk>flow_by_shm s p p'; flow_by_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"
+by (auto simp:flow_by_shm_def intro!:path_by_shm_trans)
+
+lemma flow_by_shm_intro1_prop:
+  "\<not> flow_by_shm s p p \<Longrightarrow> p \<notin> current_procs s"
+by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)
+
+lemma flow_by_shm_intro1:
+  "p \<in> current_procs s \<Longrightarrow> flow_by_shm s p p"
+by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)
 
-lemma Info_flow_shm_intro4:
-  "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
-by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
+lemma flow_by_shm_intro2:
+  "\<lbrakk>flow_by_shm s p p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"
+by (auto intro:flow_by_shm_trans dest:one_step_flows)
+
+lemma flow_by_shm_intro3:
+  "\<lbrakk>flow_by_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h; from \<noteq> to; valid s\<rbrakk>
+   \<Longrightarrow> flow_by_shm s p to"
+apply (rule flow_by_shm_intro2)
+by (auto simp:one_flow_shm_def)
+
+lemma flow_by_shm_intro4:
+  "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p"
+by (drule procs_of_shm_prop2, simp, simp add:flow_by_shm_intro1)
+
+lemma flow_by_shm_intro5:
+  "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>
+   \<Longrightarrow> flow_by_shm s from  to"
+apply (rule_tac p' = "from" and h = h in flow_by_shm_intro2)
+apply (rule flow_by_shm_intro1, simp add:procs_of_shm_prop2)
+apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)
+done
 
+lemma flow_by_shm_intro6:
+  "path_by_shm s p path p' \<Longrightarrow> flow_by_shm s p p'"
+by (auto simp:flow_by_shm_def)
 (********* simpset for inductive Info_flow_shm **********)
+term edge_related
+lemma path_by_shm_detach1_aux:
+  "path_by_shm s' pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> (s' = Detach p h # s) 
+     \<longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"
+apply (erule path_by_shm.induct, simp)
+apply (rule impI, rule path_by_shm.intros(1), simp+)
+by (auto simp:one_flow_shm_def split:if_splits intro:path_by_shm_intro3)
+
+lemma path_by_shm_detach1:
+  "\<lbrakk>path_by_shm (Detach p h # s) pa path pb; valid (Detach p h # s)\<rbrakk> 
+   \<Longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"
+by (auto dest:path_by_shm_detach1_aux)
+
+lemma path_by_shm_detach2_aux[rule_format]:
+  "path_by_shm s pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> \<not> edge_related path p h 
+   \<longrightarrow> path_by_shm (Detach p h # s) pa path pb"
+apply (induct rule:path_by_shm.induct)
+apply (rule impI, rule path_by_shm.intros(1), simp)
+apply (rule impI, erule conjE, simp split:if_splits)
+apply (rule path_by_shm.intros(2), simp)
+apply (simp add:one_flow_shm_detach)
+apply (rule impI, simp+)
+done
+
+lemma path_by_shm_detach2:
+  "\<lbrakk>valid (Detach p h # s); \<not> edge_related path p h; path_by_shm s pa path pb\<rbrakk> 
+   \<Longrightarrow> path_by_shm (Detach p h # s) pa path pb"
+by (auto intro!:path_by_shm_detach2_aux)
 
-lemma Info_flow_shm_attach1_aux:
-  "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 
-     (if Info_flow_shm s pa pb then True else
-     (if (pa = p \<and> flag = SHM_RDWR) 
-      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
-      else if (pb = p) 
-           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
-           else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
-                             Info_flow_shm s p' pb) \<or>
-                (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
-     )  )"
-proof (induct rule:Info_flow_shm.induct)
-  case (ifs_self proc \<tau>)
+lemma path_by_shm_detach:
+  "valid (Detach p h # s) \<Longrightarrow>
+   path_by_shm (Detach p h # s) pa path pb = (\<not> edge_related path p h  \<and> path_by_shm s pa path pb)"
+by (auto dest:path_by_shm_detach1 path_by_shm_detach2)
+
+lemma flow_by_shm_detach:
+  "valid (Detach p h # s) \<Longrightarrow> 
+   flow_by_shm (Detach p h # s) pa pb = (\<exists> path. \<not> edge_related path p h \<and> path_by_shm s pa path pb)"
+by (auto dest:path_by_shm_detach simp:flow_by_shm_def)
+
+lemma path_by_shm_attach1_aux:
+  "path_by_shm s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
+     (path_by_shm s pa path pb) \<or>
+     (\<exists> path1 path2 p'. path_by_shm s pa path1 p' \<and> path_by_shm s p path2 pb \<and> 
+         (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path = path2 @ [(p', h, p)] @ path1 ) \<or>
+     (\<exists> path1 path2 p' flag'. path_by_shm s pa path1 p \<and> path_by_shm s p' path2 pb \<and> 
+         (p', flag') \<in> procs_of_shm s h \<and> path = path2 @ [(p, h, p')] @ path1 \<and> flag = SHM_RDWR)"
+apply (erule path_by_shm.induct)
+apply (simp, rule impI, rule pbs1, simp)
+apply (rule impI, erule impE, clarsimp)
+apply (erule disjE)
+apply (clarsimp simp:one_flow_shm_attach split:if_splits)
+apply (erule disjE, clarsimp)
+apply (erule_tac x = path in allE, clarsimp)
+apply (erule impE, rule pbs1, erule procs_of_shm_prop2, erule vd_cons, simp)
+apply (erule disjE, clarsimp)
+apply (rule_tac x = path in exI, rule_tac x = "[]" in exI, rule_tac x = p' in exI, simp)
+apply (rule pbs1, drule vt_grant_os, clarsimp)
+apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2, simp+)
+apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2, simp+)
+
+apply (erule disjE)
+apply ((erule exE|erule conjE)+, simp split:if_splits add:one_flow_shm_attach)
+apply (clarsimp simp:one_flow_shm_attach split:if_splits)
+apply (erule disjE, clarsimp)
+apply (clarsimp)
+
+
+apply (erule conjE)+
+
+
+
+apply (erule conjE, clarsimp simp only:one_flow_shm_attach split:if_splits)
+apply simp
+
+
+
+lemma path_by_shm_attach1_aux:
+  "path_by_shm s' pa path pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 
+     path_by_shm s pa path pb \<or>
+      (if (pa = p \<and> flag = SHM_RDWR)
+       then \<exists> p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> 
+               path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+       else if (pb = p)
+            then \<exists> p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> 
+                   (p', SHM_RDWR) \<in> procs_of_shm s h
+            else (\<exists> p' flag' patha pathb. path_by_shm s pa patha p \<and> flag = SHM_RDWR \<and> 
+                   (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 
+                   path = pathb @ [(p, h, p')] @ patha) \<or>
+                 (\<exists> p' patha pathb. path_by_shm s pa patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> 
+                   path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ patha))"
+proof (induct rule:path_by_shm.induct)
+  case (pbs1 proc \<tau>)
   show ?case
   proof (rule impI)
     assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
-    hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
-    hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
-    from ifs_self pre have "proc \<in> current_procs s" by simp 
-    hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
-    show "if Info_flow_shm s proc proc then True
-    else if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc
-         else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'
-              else (\<exists>p' flag'. Info_flow_shm s proc p \<and>
-                       flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>
-                   (\<exists>p'. Info_flow_shm s proc p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p proc)"      using p4 p3 by auto
+    from pbs1 pre have "proc \<in> current_procs s" by simp 
+    thus "path_by_shm s proc [] proc \<or>
+         (if proc = p \<and> flag = SHM_RDWR
+          then \<exists>p' flagb path'.
+                  (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' proc \<and> [] = path' @ [(p, h, p')]
+          else if proc = p
+               then \<exists>p' path'.
+                       path_by_shm s proc path' p' \<and> [] = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+               else (\<exists>p' flag' patha pathb.
+                        path_by_shm s proc patha p \<and>
+                        flag = SHM_RDWR \<and>
+                        (p', flag') \<in> procs_of_shm s h \<and>
+                        path_by_shm s p' pathb proc \<and> [] = pathb @ [(p, h, p')] @ patha) \<or>
+                    (\<exists>p' patha pathb.
+                        path_by_shm s proc patha p' \<and>
+                        (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+                        path_by_shm s p pathb proc \<and> [] = pathb @ [(p', h, p)] @ patha))"
+      by (auto intro:path_by_shm.intros)
   qed
 next
-  case (ifs_flow \<tau> pa pb h' pc)
+  case (pbs2 \<tau> pa path pb h' pc)
   thus ?case
   proof (rule_tac impI)
-    assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
-     (if Info_flow_shm s pa pb then True
-      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
-           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
-                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
-                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
-                     (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+    assume p1:"path_by_shm \<tau> pa path pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
+     path_by_shm s pa path pb \<or>
+     (if pa = p \<and> flag = SHM_RDWR
+      then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+      else if pb = p
+           then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+           else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 
+                    (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 
+                    path = pathb @ [(p, h, p')] @ pathaa) \<or>
+                (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+                    path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"
       and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
-
-    from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True
-      else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
-           else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
-                else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
-                         flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
-                     (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
+    
+    from p2 and p4 have p2': "
+      path_by_shm s pa path pb \<or>
+     (if pa = p \<and> flag = SHM_RDWR
+      then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]
+      else if pb = p
+           then \<exists>p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+           else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 
+                    (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 
+                    path = pathb @ [(p, h, p')] @ pathaa) \<or>
+                (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+                    path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"
       by (erule_tac impE, simp)
     from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
-    from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
+    from p6 have "p \<in> current_procs s" by simp hence p7:"path_by_shm s p [] p" by (erule_tac path_by_shm.intros)
     from p3 p4 have p8: "if (h' = h) 
      then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
           (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
           (one_flow_shm s h pb pc)               
-     else one_flow_shm s h' pb pc        " by (auto simp add:one_flow_shm_attach) 
-
+     else one_flow_shm s h' pb pc" by (auto simp add:one_flow_shm_attach) 
+    
+    
+(*
     have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h 
-      \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+      \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' [] pc"
       apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)
-      by (simp add:p5, simp add:Info_flow_shm.intros(1))
-    hence p10: "\<not> Info_flow_shm s p pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
-      Info_flow_shm s pa pc"
-      using p2' p7 p8 p5
-      by (auto split:if_splits dest:Info_flow_shm.intros(2))      
-  (*     apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+  *)
-    moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') 
-                            \<or> Info_flow_shm s pa pc"
+      by (simp add:p5, simp add:path_by_shm.intros(1))
+    hence p10: "\<not> path_by_shm s p path pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p'  pc) \<or>
+      path_by_shm s pa pc"
       using p2' p7 p8 p5
-      by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
-    moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag'. Info_flow_shm s pa p \<and>
-                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
-                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc) \<or>
-                      Info_flow_shm s pa pc"
+      by (auto split:if_splits dest:path_by_shm.intros(2))      
+  (*     apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+  *) *)
+
+    from p1 have a0: "(path = []) = (pa = pb)" using pbs_prop2 by simp
+    have a1:"\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pb\<rbrakk> \<Longrightarrow> 
+      \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]"
+      using p2' by auto
+    have b1: "\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pc\<rbrakk> \<Longrightarrow> 
+      \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and>
+        (pb, h', pc) # path = path' @ [(p, h, p')]"
+      
+      
+      using p8 a1 p7 p5 a0 
+      apply (auto split:if_splits elim:path_by_shm_intro4)
+      apply (rule_tac x = pb in exI, rule conjI, rule_tac x = SHM_RDWR in exI, simp)
+      apply (rule_tac x = pc in exI, rule conjI, rule_tac x = flagb in exI, simp)
+      apply (rule_tac x = "[]" in exI, rule conjI)
+apply (erule path_by_shm_intro4, simp)
+
+      apply (case_tac "path_by_shm s pa path pb", simp) defer
+      apply (drule a1, simp+, clarsimp)
+      apply (rule conjI, rule_tac x = flagb in exI, simp)
+      apply (rule path_by_shm_
+      using p2' p8 p5
+      apply (auto split:if_splits dest!:pbs_prop2' simp:path_by_shm_intro4)
+      apply (drule pbs_prop2', simp)
+      apply (erule_tac x = pc in allE, simp add:path_by_shm_intro4)
+     
+      apply (drule_tac x = "pc" in allE)
+      
+      apply simp
+
+      sorry
+    moreover have "pc = p \<Longrightarrow> (\<exists>p' path'. path_by_shm s pa path' p' \<and>
+             (pb, h', pc) # path = path' @ [(p', h, p)] \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) \<or>
+      (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"
       using p2' p7 p8 p5
-      apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
-      apply (rule_tac x = pc in exI, simp add:Info_flow_shm_intro4)
+      sorry (*
+      apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) *)
+    moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> 
+      (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
+           path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p, h, p')] @ pathb) \<or>
+      (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+           path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p', h, p)] @ pathb) \<or>
+      (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"
+      using p2' p7 p8 p5 (*
+      apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def)
+      apply (rule_tac x = pc in exI, simp add:path_by_shm_intro4)
       apply (rule_tac x = flagb in exI, simp)      
-      done
-    ultimately  show "if Info_flow_shm s pa pc then True
-       else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc
-            else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
-                 else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
-                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
-                      (\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)"
-      using p7 by auto
+      done *)
+      sorry
+    ultimately  
+    show "if (pb, h', pc) # path = [] then pa = pc \<and> pa \<in> current_procs s
+       else path_by_shm s pa ((pb, h', pc) # path) pc \<and> \<not> edge_related ((pb, h', pc) # path) p h \<or>
+       (if pa = p \<and> flag = SHM_RDWR
+        then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and>
+                path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')]
+        else if pc = p
+             then \<exists>p' path'. path_by_shm s pa path' p' \<and>
+                     (pb, h', pc) # path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h
+             else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>
+                      (p', flag') \<in> procs_of_shm s h \<and>
+                      path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathb @ [(p, h, p')] @ pathaa) \<or>
+                  (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>
+                      path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathb @ [(p', h, p)] @ pathaa))"
+        apply (auto split:if_splits)
+        using p7 by auto
   qed
 qed
 
-lemma Info_flow_shm_attach1:
-  "\<lbrakk>valid (Attach p h flag # s); Info_flow_shm (Attach p h flag # s) pa pb\<rbrakk>
-   \<Longrightarrow> (if Info_flow_shm s pa pb then True else
+lemma path_by_shm_attach1:
+  "\<lbrakk>valid (Attach p h flag # s); path_by_shm (Attach p h flag # s) pa pb\<rbrakk>
+   \<Longrightarrow> (if path_by_shm s pa pb then True else
      (if (pa = p \<and> flag = SHM_RDWR) 
-      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
       else if (pb = p) 
-           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
-           else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
-                             Info_flow_shm s p' pb) \<or>
-                (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+           else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
+                             path_by_shm s p' pb) \<or>
+                (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)
      )  )"
-apply (drule_tac p = p and h = h and flag = flag in Info_flow_shm_attach1_aux)
+apply (drule_tac p = p and h = h and flag = flag in path_by_shm_attach1_aux)
 by auto
 
-lemma Info_flow_shm_attach_aux[rule_format]:
-  "Info_flow_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb"
-apply (erule Info_flow_shm.induct)
-apply (rule impI, rule Info_flow_shm.intros(1), simp)
-apply (rule impI, simp, rule_tac h = ha in Info_flow_shm.intros(2), simp)
+lemma path_by_shm_attach_aux[rule_format]:
+  "path_by_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> path_by_shm (Attach p h flag # s) pa pb"
+apply (erule path_by_shm.induct)
+apply (rule impI, rule path_by_shm.intros(1), simp)
+apply (rule impI, simp, rule_tac h = ha in path_by_shm.intros(2), simp)
 apply (auto simp add:one_flow_shm_simps)
 done
 
-lemma Info_flow_shm_attach2:
-  "\<lbrakk>valid (Attach p h flag # s); if Info_flow_shm s pa pb then True else
+lemma path_by_shm_attach2:
+  "\<lbrakk>valid (Attach p h flag # s); if path_by_shm s pa pb then True else
      (if (pa = p \<and> flag = SHM_RDWR) 
-      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
       else if (pb = p) 
-           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
-           else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
-                             Info_flow_shm s p' pb) \<or>
-                (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))\<rbrakk>
-   \<Longrightarrow> Info_flow_shm (Attach p h flag # s) pa pb"
+           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+           else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
+                             path_by_shm s p' pb) \<or>
+                (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb))\<rbrakk>
+   \<Longrightarrow> path_by_shm (Attach p h flag # s) pa pb"
 apply (frule vt_grant_os, frule vd_cons)
-apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def intro:Info_flow_shm_attach_aux)
+apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def intro:path_by_shm_attach_aux)
 apply (rule_tac p' = p' in Info_flow_trans)
-apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2))
-apply (rule Info_flow_shm.intros(1), simp)
+apply (rule_tac p' = p and h = h in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1), simp)
 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
 apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)
-apply (simp add:Info_flow_shm_attach_aux)
+apply (simp add:path_by_shm_attach_aux)
 
 apply (rule_tac p' = p' in Info_flow_trans)
 apply (rule_tac p' = p in Info_flow_trans)
-apply (simp add:Info_flow_shm_attach_aux)
-apply (rule_tac p' = p and h = h in Info_flow_shm.intros(2))
-apply (rule Info_flow_shm.intros(1), simp)
+apply (simp add:path_by_shm_attach_aux)
+apply (rule_tac p' = p and h = h in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1), simp)
 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
 apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)
-apply (simp add:Info_flow_shm_attach_aux)
+apply (simp add:path_by_shm_attach_aux)
+
+apply (rule_tac p' = p in Info_flow_trans)
+apply (rule_tac p' = p' in Info_flow_trans)
+apply (simp add:path_by_shm_attach_aux)
+apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
+apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
+apply (rule notI, simp)
+apply (simp add:path_by_shm_attach_aux)
 
 apply (rule_tac p' = p in Info_flow_trans)
 apply (rule_tac p' = p' in Info_flow_trans)
-apply (simp add:Info_flow_shm_attach_aux)
-apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2))
-apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2)
+apply (simp add:path_by_shm_attach_aux)
+apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))
+apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)
 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
 apply (rule notI, simp)
-apply (simp add:Info_flow_shm_attach_aux)
-
-apply (rule_tac p' = p in Info_flow_trans)
-apply (rule_tac p' = p' in Info_flow_trans)
-apply (simp add:Info_flow_shm_attach_aux)
-apply (rule_tac p' = p' and h = h in Info_flow_shm.intros(2))
-apply (rule Info_flow_shm.intros(1), simp add:procs_of_shm_prop2)
-apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)
-apply (rule notI, simp)
-apply (simp add:Info_flow_shm_attach_aux)
+apply (simp add:path_by_shm_attach_aux)
 done
 
-lemma Info_flow_shm_attach:
-  "valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
-     Info_flow_shm s pa pb \<or>
+lemma path_by_shm_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> path_by_shm (Attach p h flag # s) = (\<lambda> pa pb. 
+     path_by_shm s pa pb \<or>
      (if (pa = p \<and> flag = SHM_RDWR) 
-      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
+      then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' pb)
       else if (pb = p) 
-           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
-           else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
-                             Info_flow_shm s p' pb) \<or>
-                (\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
+           then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s pa p')
+           else (\<exists> p' flag'. path_by_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 
+                             path_by_shm s p' pb) \<or>
+                (\<exists> p'. path_by_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path_by_shm s p pb)
      )  )"
 apply (rule ext, rule ext, rule iffI)
-apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach1, simp)
+apply (drule_tac pa = pa and pb = pb in path_by_shm_attach1, simp)
 apply (auto split:if_splits)[1]
-apply (drule_tac pa = pa and pb = pb in Info_flow_shm_attach2)
+apply (drule_tac pa = pa and pb = pb in path_by_shm_attach2)
 apply (auto split:if_splits)
 done
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 lemma info_flow_shm_detach:
   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 
      self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
@@ -389,8 +783,9 @@
      (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
 apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+sorry (*
 apply (auto simp:info_flow_shm_def one_flow_shm_def)
-done
+done *)
 
 lemma info_flow_shm_execve:
   "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 
@@ -487,7 +882,7 @@
 apply (rule notI, erule info_flow_shm.cases, simp+)
 pr 5
 *)
-lemmas info_flow_shm_simps = info_flow_shm_other info_flow_shm_attach info_flow_shm_detach info_flow_shm_deleteshm
+lemmas info_flow_shm_simps = info_flow_shm_other (* info_flow_shm_attach *) info_flow_shm_detach info_flow_shm_deleteshm
   info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit
 
 lemma has_same_inode_in_current: