diff -r b6333712cb02 -r fc749f19b894 Current_prop.thy
--- a/Current_prop.thy	Mon Jun 24 15:22:37 2013 +0800
+++ b/Current_prop.thy	Tue Jul 09 14:43:51 2013 +0800
@@ -55,15 +55,332 @@
   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
 by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
 
-(*********** simpset for info_flow_shm **************)
+lemma flag_of_proc_shm_prop1:
+  "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
+apply (induct s arbitrary:p flag)
+apply (simp, drule init_shmflag_has_proc, simp)
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
+done
+
+(*********** simpset for one_flow_shm **************)
+
+lemma one_flow_not_self:
+  "one_flow_shm s h p p \<Longrightarrow> False"
+by (simp add:one_flow_shm_def)
+
+lemma one_flow_shm_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb. 
+     if (h' = h) 
+     then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
+          (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
+          (one_flow_shm s h pa pb)               
+     else one_flow_shm s h' pa pb        )"
+apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)
+by (auto simp add: one_flow_shm_def)
+
+lemma one_flow_shm_detach:
+  "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.
+     if (h' = h) 
+     then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)
+     else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb. 
+     if (h' = h) 
+     then False
+     else one_flow_shm s h' pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os)
+by (auto simp: one_flow_shm_def)
+
+lemma one_flow_shm_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb. 
+     if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)
+     then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)
+     else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)
+          then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)
+          else one_flow_shm s h pa pb)"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
+apply (frule_tac p = p' in procs_of_shm_prop2', simp)
+apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)
+done
+
+lemma one_flow_shm_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb    )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_kill:
+  "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb                 )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_exit:
+  "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb. 
+     pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb                          )"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+by (auto simp:one_flow_shm_def)
+
+lemma one_flow_shm_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p
+   \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"
+apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
+apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)
+apply (drule procs_of_shm_prop1, auto)
+done
+
+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''"
+
+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)
+
+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))
+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+)
+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 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 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)
+
+(********* simpset for inductive Info_flow_shm **********)
 
-lemma info_flow_shm_attach:
-  "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
-     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
-     (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
-     (info_flow_shm s pa pb)                       )"
-apply (rule ext, rule ext, frule vt_grant_os)
-by (auto simp add:info_flow_shm_def one_flow_shm_def)
+lemma Info_flow_shm_attach1:
+  "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 
+    ((Info_flow_shm s pa pb) \<or> 
+     (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+     (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 
+       (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"
+proof (induct rule:Info_flow_shm.induct)
+  case (ifs_self 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 "Info_flow_shm s proc proc \<or>
+          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and> 
+           (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>
+          (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> 
+           (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"
+      using p4 p3 by auto
+  qed
+next
+  case (ifs_flow \<tau> pa 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> Info_flow_shm s pa pb \<or>
+     \<not> Info_flow_shm s pa pb \<and> pa = p \<and>
+     pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
+     \<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"
+    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': "Info_flow_shm s pa pb \<or> 
+      (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+      (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 
+       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+      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 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) 
+    
+    have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp
+    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> 
+      \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
+      sorry
+    moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
+      \<Longrightarrow> Info_flow_shm s pa pc"
+      sorry
+    moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>
+      \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"
+      sorry
+    ultimately 
+
+      
+    
+    show "Info_flow_shm s pa pc \<or>
+      (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> 
+       (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>
+      (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and> 
+       (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
+      apply auto
+      sorry
+  qed
+qed
+
+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 Info_flow_shm_attach1:
+  "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>)
+  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
+  qed
+next
+  case (ifs_flow \<tau> pa 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))"
+      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))"
+      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 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) 
+
+    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"
+      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"
+      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"
+      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)
+      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
+  qed
+qed
+
+      
+
+
+
+
+
+
+
+
+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>
+     (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
+     (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"
+apply (rule ext, rule ext, rule iffI)
+apply (case_tac "Info_flow_shm s pa pb", simp)
+apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)
+
+apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)
+apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)
+
+
+
+apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)
+apply (simp)
+apply (simp, erule Info_flow_shm_cases', simp, simp)
+apply (rule_tac x = 
+apply (auto dest:Info_flow_shm.cases)
+apply (auto simp add:one_flow_shm_simps)
 
 lemma info_flow_shm_detach:
   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb.