58 (*********** simpset for info_flow_shm **************)

    58 lemma flag_of_proc_shm_prop1:

    59 

    59   "\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"

    60 lemma info_flow_shm_attach:

    60 apply (induct s arbitrary:p flag)

    61   "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 

    61 apply (simp, drule init_shmflag_has_proc, simp)

    62      (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>

    62 apply (frule vd_cons, frule vt_grant_os)

    63      (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>

    63 apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)

    64      (info_flow_shm s pa pb)                       )"

    64 done

    65 apply (rule ext, rule ext, frule vt_grant_os)

    65 

    66 by (auto simp add:info_flow_shm_def one_flow_shm_def)

    66 (*********** simpset for one_flow_shm **************)

    67 

    68 lemma one_flow_not_self:

    69   "one_flow_shm s h p p \<Longrightarrow> False"

    70 by (simp add:one_flow_shm_def)

    71 

    72 lemma one_flow_shm_attach:

    73   "valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb. 

    74      if (h' = h) 

    75      then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>

    76           (pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>

    77           (one_flow_shm s h pa pb)               

    78      else one_flow_shm s h' pa pb        )"

    79 apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)

    80 by (auto simp add: one_flow_shm_def)

    81 

    82 lemma one_flow_shm_detach:

    83   "valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.

    84      if (h' = h) 

    85      then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)

    86      else one_flow_shm s h' pa pb)"

    87 apply (rule ext, rule ext, rule ext, frule vt_grant_os)

    88 by (auto simp:one_flow_shm_def)

    89 

    90 lemma one_flow_shm_deleteshm:

    91   "valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb. 

    92      if (h' = h) 

    93      then False

    94      else one_flow_shm s h' pa pb)"

    95 apply (rule ext, rule ext, rule ext, frule vt_grant_os)

    96 by (auto simp: one_flow_shm_def)

    97 

    98 lemma one_flow_shm_clone:

    99   "valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb. 

   100      if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)

   101      then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)

   102      else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)

   103           then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)

   104           else one_flow_shm s h pa pb)"

   105 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)

   106 apply (frule_tac p = p' in procs_of_shm_prop2', simp)

   107 apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)

   108 done

   109 

   110 lemma one_flow_shm_execve:

   111   "valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb. 

   112      pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb    )"

   113 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   114 by (auto simp:one_flow_shm_def)

   115 

   116 lemma one_flow_shm_kill:

   117   "valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb. 

   118      pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb                 )"

   119 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   120 by (auto simp:one_flow_shm_def)

   121 

   122 lemma one_flow_shm_exit:

   123   "valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb. 

   124      pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb                          )"

   125 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   126 by (auto simp:one_flow_shm_def)

   127 

   128 lemma one_flow_shm_other:

   129   "\<lbrakk>valid (e # s); 

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

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

   132     \<forall> p h. e \<noteq> DeleteShM p h;

   133     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;

   134     \<forall> p f fds. e \<noteq> Execve p f fds;

   135     \<forall> p p'. e \<noteq> Kill p p';

   136     \<forall> p. e \<noteq> Exit p

   137    \<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"

   138 apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)

   139 apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)

   140 apply (drule procs_of_shm_prop1, auto)

   141 done

   142 

   143 lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm

   144   one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit

   145 

   146 

   147 inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   148 where

   149   ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"

   150 | ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"

   151 

   152 lemma Info_flow_trans_aux:

   153   "Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"

   154 apply (erule Info_flow_shm.induct)

   155 by (auto intro:Info_flow_shm.intros)

   156 

   157 lemma Info_flow_trans:

   158   "\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"

   159 by (auto dest:Info_flow_trans_aux)

   160 

   161 lemma one_flow_flows:

   162   "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p'"

   163 apply (rule Info_flow_shm.intros(2), simp_all)

   164 apply (rule Info_flow_shm.intros(1))

   165 apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)

   166 done

   167 

   168 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''"

   169 apply (drule one_flow_flows, simp+)

   170 apply (erule Info_flow_trans, simp+)

   171 done

   172 

   173 lemma Info_flow_shm_cases1:

   174   "\<lbrakk>Info_flow_shm s pa pb; 

   175     \<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P;

   176     \<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>

   177    \<Longrightarrow> P"

   178 by (erule Info_flow_shm.cases, auto)

   179 

   180 

   181 lemma Info_flow_shm_prop1:

   182   "\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s" 

   183 by (rule notI, drule Info_flow_shm.intros(1), simp)

   184 

   185 lemma Info_flow_shm_intro4:

   186   "\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"

   187 by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)

   188 

   189 (********* simpset for inductive Info_flow_shm **********)

   190 

   191 lemma Info_flow_shm_attach1:

   192   "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 

   193     ((Info_flow_shm s pa pb) \<or> 

   194      (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 

   195        (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>

   196      (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 

   197        (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"

   198 proof (induct rule:Info_flow_shm.induct)

   199   case (ifs_self proc \<tau>)

   200   show ?case

   201   proof (rule impI)

   202     assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"

   203     hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)

   204     hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)

   205     from ifs_self pre have "proc \<in> current_procs s" by simp 

   206     hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)

   207     show "Info_flow_shm s proc proc \<or>

   208           (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and> 

   209            (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>

   210           (\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> 

   211            (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"

   212       using p4 p3 by auto

   213   qed

   214 next

   215   case (ifs_flow \<tau> pa pb h' pc)

   216   thus ?case

   217   proof (rule_tac impI)

   218     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>

   219      \<not> Info_flow_shm s pa pb \<and> pa = p \<and>

   220      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>

   221      \<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')"

   222     and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s" 

   223     from p2 and p4 have p2': "Info_flow_shm s pa pb \<or> 

   224       (\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> 

   225        (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>

   226       (\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> 

   227        (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"

   228       by (erule_tac impE, simp)

   229     from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)

   230     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)

   231     from p3 p4 have p8: "if (h' = h) 

   232      then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>

   233           (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>

   234           (one_flow_shm s h pb pc)               

   235      else one_flow_shm s h' pb pc        " by (auto simp add:one_flow_shm_attach) 

   236     

   237     have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp

   238     moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk> 

   239       \<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"

   240       sorry

   241     moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>

   242       \<Longrightarrow> Info_flow_shm s pa pc"

   243       sorry

   244     moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>

   245       \<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"

   246       sorry

   247     ultimately 

   248 

   249       

   250     

   251     show "Info_flow_shm s pa pc \<or>

   252       (\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> 

   253        (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>

   254       (\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and> 

   255        (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"

   256       apply auto

   257       sorry

   258   qed

   259 qed

   260 

   261 lemma Info_flow_shm_intro3:

   262   "\<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>

   263    \<Longrightarrow> Info_flow_shm s p to"

   264 apply (case_tac "from = to", simp)

   265 apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)

   266 by (rule_tac x = flag in exI, simp)

   267 

   268 lemma Info_flow_shm_attach1:

   269   "Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow> 

   270      (if Info_flow_shm s pa pb then True else

   271      (if (pa = p \<and> flag = SHM_RDWR) 

   272       then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)

   273       else if (pb = p) 

   274            then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')

   275            else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> 

   276                              Info_flow_shm s p' pb) \<or>

   277                 (\<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)

   278      )  )"

   279 proof (induct rule:Info_flow_shm.induct)

   280   case (ifs_self proc \<tau>)

   281   show ?case

   282   proof (rule impI)

   283     assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"

   284     hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)

   285     hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)

   286     from ifs_self pre have "proc \<in> current_procs s" by simp 

   287     hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)

   288     show "if Info_flow_shm s proc proc then True

   289     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

   290          else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'

   291               else (\<exists>p' flag'. Info_flow_shm s proc p \<and>

   292                        flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>

   293                    (\<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

   294   qed

   295 next

   296   case (ifs_flow \<tau> pa pb h' pc)

   297   thus ?case

   298   proof (rule_tac impI)

   299     assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>

   300      (if Info_flow_shm s pa pb then True

   301       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

   302            else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

   303                 else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

   304                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>

   305                      (\<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))"

   306       and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"

   307 

   308     from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True

   309       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

   310            else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

   311                 else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

   312                          flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>

   313                      (\<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))"

   314       by (erule_tac impE, simp)

   315     from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)

   316     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)

   317     from p3 p4 have p8: "if (h' = h) 

   318      then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>

   319           (pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>

   320           (one_flow_shm s h pb pc)               

   321      else one_flow_shm s h' pb pc        " by (auto simp add:one_flow_shm_attach) 

   322 

   323     have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h 

   324       \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"

   325       apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)

   326       by (simp add:p5, simp add:Info_flow_shm.intros(1))

   327     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>

   328       Info_flow_shm s pa pc"

   329       using p2' p7 p8 p5

   330       by (auto split:if_splits dest:Info_flow_shm.intros(2))      

   331   (*     apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+  *)

   332     moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p') 

   333                             \<or> Info_flow_shm s pa pc"

   334       using p2' p7 p8 p5

   335       by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)

   336     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>

   337                           flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>

   338                       (\<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>

   339                       Info_flow_shm s pa pc"

   340       using p2' p7 p8 p5

   341       apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)

   342       apply (rule_tac x = pc in exI, simp add:Info_flow_shm_intro4)

   343       apply (rule_tac x = flagb in exI, simp)      

   344       done

   345     ultimately  show "if Info_flow_shm s pa pc then True

   346        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

   347             else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'

   348                  else (\<exists>p' flag'. Info_flow_shm s pa p \<and>

   349                           flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>

   350                       (\<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)"

   351       using p7 by auto

   352   qed

   353 qed

   354 

   355       

   356 

   357 

   358 

   359 

   360 

   361 

   362 

   363 

   364 lemma Info_flow_shm_attach:

   365   "valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 

   366      (Info_flow_shm s pa pb) \<or>

   367      (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>

   368      (pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"

   369 apply (rule ext, rule ext, rule iffI)

   370 apply (case_tac "Info_flow_shm s pa pb", simp)

   371 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)

   372 

   373 apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)

   374 apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)

   375 

   376 

   377 

   378 apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)

   379 apply (simp)

   380 apply (simp, erule Info_flow_shm_cases', simp, simp)

   381 apply (rule_tac x = 

   382 apply (auto dest:Info_flow_shm.cases)

   383 apply (auto simp add:one_flow_shm_simps)