68 (*********** simpset for one_flow_shm **************)

    70 lemma one_flow_not_self:

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

    72 by (simp add:one_flow_shm_def)

    73 

    74 lemma one_flow_shm_attach:

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

    76      if (h' = h) 

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

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

    79           (one_flow_shm s h pa pb)               

    80      else one_flow_shm s h' pa pb        )"

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

    82 by (auto simp add: one_flow_shm_def)

    83 

    84 lemma one_flow_shm_detach:

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

    86      if (h' = h) 

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

    88      else one_flow_shm s h' pa pb)"

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

    90 by (auto simp:one_flow_shm_def)

    91 

    92 lemma one_flow_shm_deleteshm:

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

    94      if (h' = h) 

    95      then False

    96      else one_flow_shm s h' pa pb)"

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

    98 by (auto simp: one_flow_shm_def)

    99 

   100 lemma one_flow_shm_clone:

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

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

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

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

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

   106           else one_flow_shm s h pa pb)"

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

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

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

   110 done

   111 

   112 lemma one_flow_shm_execve:

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

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

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

   116 by (auto simp:one_flow_shm_def)

   117 

   118 lemma one_flow_shm_kill:

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

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

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

   122 by (auto simp:one_flow_shm_def)

   123 

   124 lemma one_flow_shm_exit:

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

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

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

   128 by (auto simp:one_flow_shm_def)

   129 

   130 lemma one_flow_shm_other:

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

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

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

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

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

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

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

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

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

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

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

   142 apply (drule procs_of_shm_prop1, auto)

   143 done

   144 

   145 lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm

   146   one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit

   147 

   148 type_synonym t_edge_shm = "t_process \<times> t_shm \<times> t_process"

   149 fun Fst:: "t_edge_shm \<Rightarrow> t_process" where "Fst (a, b, c) = a"

   150 fun Snd:: "t_edge_shm \<Rightarrow> t_shm" where "Snd (a, b, c) = b"

   151 fun Trd:: "t_edge_shm \<Rightarrow> t_process" where "Trd (a, b, c) = c"

   152 

   153 fun edge_related:: "t_edge_shm list \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> bool"

   154 where

   155   "edge_related [] p h = False"

   156 | "edge_related ((from, shm, to) # path) p h = 

   157      (if (((p = from) \<or> (p = to)) \<and> (h = shm)) then True 

   158       else edge_related path p h)"

   159          

   160 inductive path_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"

   161 where

   162   pbs1: "p \<in> current_procs s \<Longrightarrow> path_by_shm s p [] p"

   163 | pbs2: "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path)\<rbrakk> 

   164          \<Longrightarrow> path_by_shm s p ((p', h, p'')# path) p''"

   165 

   166 

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

   168 apply (rule_tac path = "[]" and p = p in path_by_shm.intros(2))

   169 apply (rule path_by_shm.intros(1))

   170 apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)

   171 done

   172 

   173 lemma pbs_prop1:

   174   "path_by_shm s p path p' \<Longrightarrow> ((path = []) = (p = p')) \<and> (path \<noteq> [] \<longrightarrow> p \<in> set (map Fst path))"

   175 apply (erule path_by_shm.induct, simp)

   176 apply (auto simp:one_flow_shm_def)

   177 done

   178 

   179 lemma pbs_prop2:

   180   "path_by_shm s p path p' \<Longrightarrow> (path = []) = (p = p')"

   181 by (simp add:pbs_prop1)

   182 

   183 lemma pbs_prop2':

   184   "path_by_shm s p path p \<Longrightarrow> path = []"

   185 by (simp add:pbs_prop2)

   186 

   187 lemma pbs_prop3:

   188   "\<lbrakk>path_by_shm s p path p'; path \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set (map Fst path)"

   189 by (drule pbs_prop1, auto)

   190 

   191 lemma pbs_prop4[rule_format]:

   192   "path_by_shm s p path p'\<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<in> set (map Trd path)"

   193 by (erule path_by_shm.induct, auto)

   194 

   195 lemma pbs_prop5[rule_format]:

   196   "path_by_shm s p path p' \<Longrightarrow> path \<noteq> [] \<longrightarrow> p' \<notin> set (map Fst path)"

   197 by (erule path_by_shm.induct, auto simp:one_flow_shm_def)

   198 

   199 lemma pbs_prop6_aux:

   200   "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)"

   201 apply (erule path_by_shm.induct)

   202 apply simp

   203 apply clarify

   204 apply (case_tac "pb = p'", simp)

   205 apply (rule_tac x = path in exI, simp)

   206 apply (erule one_step_path, simp)

   207 apply (erule_tac x = pb in ballE, simp_all, clarsimp)

   208 apply (rule_tac x = pathab in exI, simp)

   209 apply (erule pbs2, auto)

   210 done

   211 

   212 lemma pbs_prop6:

   213   "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Fst pathac); valid s\<rbrakk>

   214    \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"

   215 by (drule pbs_prop6_aux, auto)

   216 

   217 lemma pbs_prop7_aux:

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

   219 apply (erule path_by_shm.induct)

   220 apply simp

   221 apply clarify

   222 apply (case_tac "pb = p''", simp)

   223 apply (rule_tac x = "(p',h,p'') # path" in exI, simp)

   224 apply (rule conjI, erule pbs2, simp+)

   225 apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)

   226 apply (erule_tac x = pb in ballE, simp_all, clarsimp)

   227 apply (rule_tac x = pathab in exI, simp)

   228 apply (erule pbs2, auto)

   229 done

   230 

   231 lemma pbs_prop7:

   232   "\<lbrakk>path_by_shm s pa pathac pc; pb \<in> set (map Trd pathac); valid s\<rbrakk>

   233    \<Longrightarrow> \<exists> pathab pathbc. path_by_shm s pa pathab pb \<and> path_by_shm s pb pathbc pc \<and> pathac = pathbc @ pathab"

   234 by (drule pbs_prop7_aux, drule mp, simp, erule_tac x = pb in ballE, auto)

   235 

   236 lemma pbs_prop8:

   237   "path_by_shm s p path p' \<Longrightarrow> (set (map Fst path) - {p}) = (set (map Trd path) - {p'})"

   238 proof (induct rule:path_by_shm.induct)

   239   case (pbs1 p s)

   240   thus ?case by simp

   241 next

   242   case (pbs2 s p path p' h p'')

   243   assume p1:"path_by_shm s p path p'" and p2: "set (map Fst path) - {p} = set (map Trd path) - {p'}"

   244     and p3: "one_flow_shm s h p' p''" and p4: "p'' \<notin> set (map Fst path)" 

   245   show "set (map Fst ((p', h, p'') # path)) - {p} = set (map Trd ((p', h, p'') # path)) - {p''}"

   246     (is "?left = ?right")

   247   proof (cases "path = []")

   248     case True

   249     with p1 have "p = p'" by (drule_tac pbs_prop2, simp)

   250     thus ?thesis using True

   251       using p2 by (simp)

   252   next

   253     case False

   254     with p1 have a1: "p \<noteq> p'" by (drule_tac pbs_prop2, simp)

   255     from p3 have a2: "p' \<noteq> p''" by (simp add:one_flow_shm_def)

   256     from p1 False have a3: "p' \<in> set (map Trd path)" by (drule_tac pbs_prop4, simp+)

   257     from p4 p1 False have a4: "p \<noteq> p''" by (drule_tac pbs_prop3, auto)

   258     with p2 a2 p4 have a5: "p'' \<notin> set (map Trd path)" by auto

   259     

   260     have "?left = (set (map Fst path) - {p}) \<union> {p'}" using a1 by auto

   261     moreover have "... = (set (map Trd path) - {p'}) \<union> {p'}"  

   262       using p2 by auto

   263     moreover have "... = set (map Trd path)" using a3 by auto

   264     moreover have "... = set (map Trd path) - {p''}" using a5 by simp

   265     moreover have "... = ?right" by simp

   266     ultimately show ?thesis by simp

   267   qed

   268 qed

   269 

   270 lemma pbs_prop9_aux[rule_format]:

   271   "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))"

   272 apply (erule path_by_shm.induct, simp)

   273 apply (rule impI, case_tac "h \<in> set (map Snd path)", simp_all)

   274 apply (erule exE|erule conjE)+

   275 apply (rule_tac x = pa in exI, rule_tac x = pb in exI, rule_tac x = patha in exI, simp)

   276 apply (rule pbs2, auto)

   277 apply (rule_tac x = p' in exI, rule_tac x = p'' in exI, rule_tac x = path in exI, simp)

   278 apply (rule pbs1, clarsimp simp:one_flow_shm_def procs_of_shm_prop2)

   279 done

   280 

   281 lemma pbs_prop9:

   282   "\<lbrakk>h \<in> set (map Snd path); path_by_shm s p path p'; valid s\<rbrakk>

   283    \<Longrightarrow> \<exists> pa pb patha pathb. path_by_shm s p patha pa \<and> path_by_shm s pb pathb p' \<and> 

   284         one_flow_shm s h pa pb \<and> path = pathb @ [(pa, h, pb)] @ patha \<and> h \<notin> set (map Snd patha)"

   285 by (rule pbs_prop9_aux, auto)

   286 

   287 lemma path_by_shm_trans_aux[rule_format]:

   288   "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''))"

   289 proof (induct rule:path_by_shm.induct)

   290   case (pbs1 p s)

   291   thus ?case

   292     by (clarify, rule_tac x = path in exI, simp)

   293 next

   294   case (pbs2 s p path p' h p'')

   295   hence p1: "path_by_shm s p path p'" and p2: "one_flow_shm s h p' p''" 

   296     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'))"

   297     and p4: "p'' \<notin> set (map Fst path)" by auto

   298   show ?case

   299   proof clarify

   300     fix pa path'

   301     assume p5: "path_by_shm s pa path' p" and p6: "valid s"

   302     with p3 obtain path'' where a1: "path_by_shm s pa path'' p'" by auto

   303     have p3': "\<forall>pa path. path_by_shm s pa path p \<longrightarrow> (\<exists>path''. path_by_shm s pa path'' p')" 

   304       using p3 p6 by simp

   305     show "\<exists>path''. path_by_shm s pa path'' p''"

   306     proof (cases "p'' \<in> set (map Fst path'')")

   307       case True

   308       then obtain res where "path_by_shm s pa res p''" using a1 pbs_prop6 p6 by blast

   309       thus ?thesis by auto

   310     next

   311       case False

   312       with p2 a1 show ?thesis 

   313         apply (rule_tac x = "(p', h, p'') # path''" in exI)

   314         apply (rule path_by_shm.intros(2), auto)

   315         done

   316     qed

   317   qed

   318 qed

   319 

   320 lemma path_by_shm_trans:

   321   "\<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''"

   322 by (drule_tac p' = p' and p'' = p'' in path_by_shm_trans_aux, auto)

   323 

   324 lemma path_by_shm_intro1_prop:

   325   "\<not> path_by_shm s p [] p \<Longrightarrow> p \<notin> current_procs s"

   326 by (auto dest:path_by_shm.intros(1))

   327 

   328 lemma path_by_shm_intro3:

   329   "\<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; 

   330     to \<notin> set (map Fst path); from \<noteq> to\<rbrakk>

   331    \<Longrightarrow> path_by_shm s p ((from, h, to)#path) to"

   332 apply (rule path_by_shm.intros(2), simp_all)

   333 by (auto simp:one_flow_shm_def)

   334 

   335 lemma path_by_shm_intro4:

   336   "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> path_by_shm s p [] p"

   337 by (drule procs_of_shm_prop2, simp, simp add:path_by_shm.intros(1))

   338 

   339 lemma path_by_shm_intro5:

   340   "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>

   341    \<Longrightarrow> path_by_shm s from [(from, h, to)] to"

   342 apply (rule_tac p' = "from" and h = h in path_by_shm.intros(2))

   343 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   344 apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)

   345 done

   346 

   347 (* p'' \<notin> set (map Fst path): not duplicated target process;

   348  * 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,

   349  * but this could be also path_by_shm p1 [(p1,ha,p4)] p4, so the former one is redundant!  *)

   350 

   351 inductive path_by_shm':: "t_state \<Rightarrow> t_process \<Rightarrow> t_edge_shm list \<Rightarrow> t_process \<Rightarrow> bool"

   352 where

   353   pbs1': "p \<in> current_procs s \<Longrightarrow> path_by_shm' s p [] p"

   354 | pbs2': "\<lbrakk>path_by_shm s p path p'; one_flow_shm s h p' p''; p'' \<notin> set (map Fst path); 

   355            h \<notin> set (map Snd path)\<rbrakk> 

   356           \<Longrightarrow> path_by_shm' s p ((p', h, p'')# path) p''"

   357 

   358 lemma pbs_imp_pbs'[rule_format]:

   359   "path_by_shm s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm' s p path' p')"

   360 apply (erule path_by_shm.induct)

   361 apply (rule impI, rule_tac x = "[]" in exI, erule pbs1')

   362 apply (rule impI, simp,  erule exE, case_tac "h \<in> set (map Snd path)")

   363 apply (drule_tac s = s and p = p and p' = p' in pbs_prop9, simp+) defer

   364 apply (rule_tac x = "(p', h, p'') # path" in exI, erule pbs2', simp+) 

   365 apply ((erule exE|erule conjE)+)

   366 apply (rule_tac x = "(pa, h, p'') # patha" in exI)

   367 apply (erule pbs2', auto simp:one_flow_shm_def)

   368 done

   369 

   370 lemma pbs'_imp_pbs[rule_format]:

   371   "path_by_shm' s p path p' \<Longrightarrow> valid s \<longrightarrow> (\<exists> path'. path_by_shm s p path' p')"

   372 apply (erule path_by_shm'.induct)

   373 apply (rule impI, rule_tac x = "[]" in exI, simp add:pbs1)

   374 apply (rule impI, rule_tac x = "(p', h, p'') # path" in exI, simp add:pbs2)

   375 done

   376 

   377 definition flow_by_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   378 where

   379   "flow_by_shm s p p' \<equiv> \<exists> path. path_by_shm s p path p'"

   380 

   381 lemma flow_by_shm_intro':

   382   "valid s \<Longrightarrow> flow_by_shm s p p' = (\<exists> path. path_by_shm' s p path p')"

   383 by (auto simp:flow_by_shm_def intro: pbs_imp_pbs' pbs'_imp_pbs)

   384 

   385 lemma one_step_flows: "\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p'"

   386 by (drule one_step_path, auto simp:flow_by_shm_def)

   387 

   388 lemma flow_by_shm_trans:

   389   "\<lbrakk>flow_by_shm s p p'; flow_by_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"

   390 by (auto simp:flow_by_shm_def intro!:path_by_shm_trans)

   391 

   392 lemma flow_by_shm_intro1_prop:

   393   "\<not> flow_by_shm s p p \<Longrightarrow> p \<notin> current_procs s"

   394 by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)

   395 

   396 lemma flow_by_shm_intro1:

   397   "p \<in> current_procs s \<Longrightarrow> flow_by_shm s p p"

   398 by (auto dest:path_by_shm.intros(1) simp:flow_by_shm_def)

   399 

   400 lemma flow_by_shm_intro2:

   401   "\<lbrakk>flow_by_shm s p p'; one_flow_shm s h p' p''; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p''"

   402 by (auto intro:flow_by_shm_trans dest:one_step_flows)

   403 

   404 lemma flow_by_shm_intro3:

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

   406    \<Longrightarrow> flow_by_shm s p to"

   407 apply (rule flow_by_shm_intro2)

   408 by (auto simp:one_flow_shm_def)

   409 

   410 lemma flow_by_shm_intro4:

   411   "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flow_by_shm s p p"

   412 by (drule procs_of_shm_prop2, simp, simp add:flow_by_shm_intro1)

   413 

   414 lemma flow_by_shm_intro5:

   415   "\<lbrakk>(from, SHM_RDWR) \<in> procs_of_shm s h; (to,flag) \<in> procs_of_shm s h; valid s; from \<noteq> to\<rbrakk>

   416    \<Longrightarrow> flow_by_shm s from  to"

   417 apply (rule_tac p' = "from" and h = h in flow_by_shm_intro2)

   418 apply (rule flow_by_shm_intro1, simp add:procs_of_shm_prop2)

   419 apply (simp add:one_flow_shm_def, rule_tac x = flag in exI, auto)

   420 done

   421 

   422 lemma flow_by_shm_intro6:

   423   "path_by_shm s p path p' \<Longrightarrow> flow_by_shm s p p'"

   424 by (auto simp:flow_by_shm_def)

   425 (********* simpset for inductive Info_flow_shm **********)

   426 term edge_related

   427 lemma path_by_shm_detach1_aux:

   428   "path_by_shm s' pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> (s' = Detach p h # s) 

   429      \<longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"

   430 apply (erule path_by_shm.induct, simp)

   431 apply (rule impI, rule path_by_shm.intros(1), simp+)

   432 by (auto simp:one_flow_shm_def split:if_splits intro:path_by_shm_intro3)

   433 

   434 lemma path_by_shm_detach1:

   435   "\<lbrakk>path_by_shm (Detach p h # s) pa path pb; valid (Detach p h # s)\<rbrakk> 

   436    \<Longrightarrow> \<not> edge_related path p h \<and> path_by_shm s pa path pb"

   437 by (auto dest:path_by_shm_detach1_aux)

   438 

   439 lemma path_by_shm_detach2_aux[rule_format]:

   440   "path_by_shm s pa path pb \<Longrightarrow> valid (Detach p h # s) \<and> \<not> edge_related path p h 

   441    \<longrightarrow> path_by_shm (Detach p h # s) pa path pb"

   442 apply (induct rule:path_by_shm.induct)

   443 apply (rule impI, rule path_by_shm.intros(1), simp)

   444 apply (rule impI, erule conjE, simp split:if_splits)

   445 apply (rule path_by_shm.intros(2), simp)

   446 apply (simp add:one_flow_shm_detach)

   447 apply (rule impI, simp+)

   448 done

   449 

   450 lemma path_by_shm_detach2:

   451   "\<lbrakk>valid (Detach p h # s); \<not> edge_related path p h; path_by_shm s pa path pb\<rbrakk> 

   452    \<Longrightarrow> path_by_shm (Detach p h # s) pa path pb"

   453 by (auto intro!:path_by_shm_detach2_aux)

   454 

   455 lemma path_by_shm_detach:

   456   "valid (Detach p h # s) \<Longrightarrow>

   457    path_by_shm (Detach p h # s) pa path pb = (\<not> edge_related path p h  \<and> path_by_shm s pa path pb)"

   458 by (auto dest:path_by_shm_detach1 path_by_shm_detach2)

   459 

   460 lemma flow_by_shm_detach:

   461   "valid (Detach p h # s) \<Longrightarrow> 

   462    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)"

   463 by (auto dest:path_by_shm_detach simp:flow_by_shm_def)

   464 

   465 lemma path_by_shm_attach1_aux:

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

   467      (path_by_shm s pa path pb) \<or>

   468      (\<exists> path1 path2 p'. path_by_shm s pa path1 p' \<and> path_by_shm s p path2 pb \<and> 

   469          (p', SHM_RDWR) \<in> procs_of_shm s h \<and> path = path2 @ [(p', h, p)] @ path1 ) \<or>

   470      (\<exists> path1 path2 p' flag'. path_by_shm s pa path1 p \<and> path_by_shm s p' path2 pb \<and> 

   471          (p', flag') \<in> procs_of_shm s h \<and> path = path2 @ [(p, h, p')] @ path1 \<and> flag = SHM_RDWR)"

   472 apply (erule path_by_shm.induct)

   473 apply (simp, rule impI, rule pbs1, simp)

   474 apply (rule impI, erule impE, clarsimp)

   475 apply (erule disjE)

   476 apply (clarsimp simp:one_flow_shm_attach split:if_splits)

   477 apply (erule disjE, clarsimp)

   478 apply (erule_tac x = path in allE, clarsimp)

   479 apply (erule impE, rule pbs1, erule procs_of_shm_prop2, erule vd_cons, simp)

   480 apply (erule disjE, clarsimp)

   481 apply (rule_tac x = path in exI, rule_tac x = "[]" in exI, rule_tac x = p' in exI, simp)

   482 apply (rule pbs1, drule vt_grant_os, clarsimp)

   483 apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2, simp+)

   484 apply (drule_tac p = pa and p' = p' and p'' = p'' in pbs2, simp+)

   485 

   486 apply (erule disjE)

   487 apply ((erule exE|erule conjE)+, simp split:if_splits add:one_flow_shm_attach)

   488 apply (clarsimp simp:one_flow_shm_attach split:if_splits)

   489 apply (erule disjE, clarsimp)

   490 apply (clarsimp)

   491 

   492 

   493 apply (erule conjE)+

   494 

   495 

   496 

   497 apply (erule conjE, clarsimp simp only:one_flow_shm_attach split:if_splits)

   498 apply simp

   499 

   500 

   501 

   502 lemma path_by_shm_attach1_aux:

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

   504      path_by_shm s pa path pb \<or>

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

   506        then \<exists> p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> 

   507                path_by_shm s p' path' pb \<and> path = path' @ [(p, h, p')]

   508        else if (pb = p)

   509             then \<exists> p' path'. path_by_shm s pa path' p' \<and> path = (p', h, p) # path' \<and> 

   510                    (p', SHM_RDWR) \<in> procs_of_shm s h

   511             else (\<exists> p' flag' patha pathb. path_by_shm s pa patha p \<and> flag = SHM_RDWR \<and> 

   512                    (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   513                    path = pathb @ [(p, h, p')] @ patha) \<or>

   514                  (\<exists> p' patha pathb. path_by_shm s pa patha p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> 

   515                    path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ patha))"

   516 proof (induct rule:path_by_shm.induct)

   517   case (pbs1 proc \<tau>)

   518   show ?case

   519   proof (rule impI)

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

   521     from pbs1 pre have "proc \<in> current_procs s" by simp 

   522     thus "path_by_shm s proc [] proc \<or>

   523          (if proc = p \<and> flag = SHM_RDWR

   524           then \<exists>p' flagb path'.

   525                   (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' proc \<and> [] = path' @ [(p, h, p')]

   526           else if proc = p

   527                then \<exists>p' path'.

   528                        path_by_shm s proc path' p' \<and> [] = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   529                else (\<exists>p' flag' patha pathb.

   530                         path_by_shm s proc patha p \<and>

   531                         flag = SHM_RDWR \<and>

   532                         (p', flag') \<in> procs_of_shm s h \<and>

   533                         path_by_shm s p' pathb proc \<and> [] = pathb @ [(p, h, p')] @ patha) \<or>

   534                     (\<exists>p' patha pathb.

   535                         path_by_shm s proc patha p' \<and>

   536                         (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   537                         path_by_shm s p pathb proc \<and> [] = pathb @ [(p', h, p)] @ patha))"

   538       by (auto intro:path_by_shm.intros)

   539   qed

   540 next

   541   case (pbs2 \<tau> pa path pb h' pc)

   542   thus ?case

   543   proof (rule_tac impI)

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

   545      path_by_shm s pa path pb \<or>

   546      (if pa = p \<and> flag = SHM_RDWR

   547       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')]

   548       else if pb = p

   549            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

   550            else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 

   551                     (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   552                     path = pathb @ [(p, h, p')] @ pathaa) \<or>

   553                 (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   554                     path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"

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

   556     

   557     from p2 and p4 have p2': "

   558       path_by_shm s pa path pb \<or>

   559      (if pa = p \<and> flag = SHM_RDWR

   560       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')]

   561       else if pb = p

   562            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

   563            else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and> 

   564                     (p', flag') \<in> procs_of_shm s h \<and> path_by_shm s p' pathb pb \<and> 

   565                     path = pathb @ [(p, h, p')] @ pathaa) \<or>

   566                 (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   567                     path_by_shm s p pathb pb \<and> path = pathb @ [(p', h, p)] @ pathaa))"

   568       by (erule_tac impE, simp)

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

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

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

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

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

   574           (one_flow_shm s h pb pc)               

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

   576     

   577     

   578 (*

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

   580       \<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' [] pc"

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

   582       by (simp add:p5, simp add:path_by_shm.intros(1))

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

   584       path_by_shm s pa pc"

   585       using p2' p7 p8 p5

   586       by (auto split:if_splits dest:path_by_shm.intros(2))      

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

   588 

   589     from p1 have a0: "(path = []) = (pa = pb)" using pbs_prop2 by simp

   590     have a1:"\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pb\<rbrakk> \<Longrightarrow> 

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

   592       using p2' by auto

   593     have b1: "\<lbrakk>pa = p; flag = SHM_RDWR; \<not> path_by_shm s pa path pc\<rbrakk> \<Longrightarrow> 

   594       \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and> path_by_shm s p' path' pc \<and>

   595         (pb, h', pc) # path = path' @ [(p, h, p')]"

   596       

   597       

   598       using p8 a1 p7 p5 a0 

   599       apply (auto split:if_splits elim:path_by_shm_intro4)

   600       apply (rule_tac x = pb in exI, rule conjI, rule_tac x = SHM_RDWR in exI, simp)

   601       apply (rule_tac x = pc in exI, rule conjI, rule_tac x = flagb in exI, simp)

   602       apply (rule_tac x = "[]" in exI, rule conjI)

   603 apply (erule path_by_shm_intro4, simp)

   604 

   605       apply (case_tac "path_by_shm s pa path pb", simp) defer

   606       apply (drule a1, simp+, clarsimp)

   607       apply (rule conjI, rule_tac x = flagb in exI, simp)

   608       apply (rule path_by_shm_

   609       using p2' p8 p5

   610       apply (auto split:if_splits dest!:pbs_prop2' simp:path_by_shm_intro4)

   611       apply (drule pbs_prop2', simp)

   612       apply (erule_tac x = pc in allE, simp add:path_by_shm_intro4)

   613      

   614       apply (drule_tac x = "pc" in allE)

   615       

   616       apply simp

   617 

   618       sorry

   619     moreover have "pc = p \<Longrightarrow> (\<exists>p' path'. path_by_shm s pa path' p' \<and>

   620              (pb, h', pc) # path = path' @ [(p', h, p)] \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) \<or>

   621       (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"

   622       using p2' p7 p8 p5

   623       sorry (*

   624       apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def) *)

   625     moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> 

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

   627            path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p, h, p')] @ pathb) \<or>

   628       (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   629            path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathaa @ [(p', h, p)] @ pathb) \<or>

   630       (path_by_shm s pa path pc \<and> \<not> edge_related path p h)"

   631       using p2' p7 p8 p5 (*

   632       apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def)

   633       apply (rule_tac x = pc in exI, simp add:path_by_shm_intro4)

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

   635       done *)

   636       sorry

   637     ultimately  

   638     show "if (pb, h', pc) # path = [] then pa = pc \<and> pa \<in> current_procs s

   639        else path_by_shm s pa ((pb, h', pc) # path) pc \<and> \<not> edge_related ((pb, h', pc) # path) p h \<or>

   640        (if pa = p \<and> flag = SHM_RDWR

   641         then \<exists>p' flagb path'. (p', flagb) \<in> procs_of_shm s h \<and>

   642                 path_by_shm s p' path' pc \<and> (pb, h', pc) # path = path' @ [(p, h, p')]

   643         else if pc = p

   644              then \<exists>p' path'. path_by_shm s pa path' p' \<and>

   645                      (pb, h', pc) # path = (p', h, p) # path' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h

   646              else (\<exists>p' flag' pathaa pathb. path_by_shm s pa pathaa p \<and> flag = SHM_RDWR \<and>

   647                       (p', flag') \<in> procs_of_shm s h \<and>

   648                       path_by_shm s p' pathb pc \<and> (pb, h', pc) # path = pathb @ [(p, h, p')] @ pathaa) \<or>

   649                   (\<exists>p' pathaa pathb. path_by_shm s pa pathaa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and>

   650                       path_by_shm s p pathb pc \<and> (pb, h', pc) # path = pathb @ [(p', h, p)] @ pathaa))"

   651         apply (auto split:if_splits)

   652         using p7 by auto

   653   qed

   654 qed

   655 

   656 lemma path_by_shm_attach1:

   657   "\<lbrakk>valid (Attach p h flag # s); path_by_shm (Attach p h flag # s) pa pb\<rbrakk>

   658    \<Longrightarrow> (if path_by_shm s pa pb then True else

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

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

   661       else if (pb = p) 

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

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

   664                              path_by_shm s p' pb) \<or>

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

   666      )  )"

   667 apply (drule_tac p = p and h = h and flag = flag in path_by_shm_attach1_aux)

   668 by auto

   669 

   670 lemma path_by_shm_attach_aux[rule_format]:

   671   "path_by_shm s pa pb \<Longrightarrow> valid (Attach p h flag # s) \<longrightarrow> path_by_shm (Attach p h flag # s) pa pb"

   672 apply (erule path_by_shm.induct)

   673 apply (rule impI, rule path_by_shm.intros(1), simp)

   674 apply (rule impI, simp, rule_tac h = ha in path_by_shm.intros(2), simp)

   675 apply (auto simp add:one_flow_shm_simps)

   676 done

   677 

   678 lemma path_by_shm_attach2:

   679   "\<lbrakk>valid (Attach p h flag # s); if path_by_shm s pa pb then True else

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

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

   682       else if (pb = p) 

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

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

   685                              path_by_shm s p' pb) \<or>

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

   687    \<Longrightarrow> path_by_shm (Attach p h flag # s) pa pb"

   688 apply (frule vt_grant_os, frule vd_cons)

   689 apply (auto split:if_splits intro:path_by_shm_intro3 simp:one_flow_shm_def intro:path_by_shm_attach_aux)

   690 apply (rule_tac p' = p' in Info_flow_trans)

   691 apply (rule_tac p' = p and h = h in path_by_shm.intros(2))

   692 apply (rule path_by_shm.intros(1), simp)

   693 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   694 apply (rule conjI, rule notI, simp, rule_tac x = flagb in exI, simp)

   695 apply (simp add:path_by_shm_attach_aux)

   696 

   697 apply (rule_tac p' = p' in Info_flow_trans)

   698 apply (rule_tac p' = p in Info_flow_trans)

   699 apply (simp add:path_by_shm_attach_aux)

   700 apply (rule_tac p' = p and h = h in path_by_shm.intros(2))

   701 apply (rule path_by_shm.intros(1), simp)

   702 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   703 apply (rule conjI, rule notI, simp, rule_tac x = flag' in exI, simp)

   704 apply (simp add:path_by_shm_attach_aux)

   705 

   706 apply (rule_tac p' = p in Info_flow_trans)

   707 apply (rule_tac p' = p' in Info_flow_trans)

   708 apply (simp add:path_by_shm_attach_aux)

   709 apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))

   710 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   711 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   712 apply (rule notI, simp)

   713 apply (simp add:path_by_shm_attach_aux)

   714 

   715 apply (rule_tac p' = p in Info_flow_trans)

   716 apply (rule_tac p' = p' in Info_flow_trans)

   717 apply (simp add:path_by_shm_attach_aux)

   718 apply (rule_tac p' = p' and h = h in path_by_shm.intros(2))

   719 apply (rule path_by_shm.intros(1), simp add:procs_of_shm_prop2)

   720 apply (simp add:one_flow_shm_simps, simp add:one_flow_shm_def)

   721 apply (rule notI, simp)

   722 apply (simp add:path_by_shm_attach_aux)

   723 done

   724 

   725 lemma path_by_shm_attach:

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

   727      path_by_shm s pa pb \<or>

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

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

   730       else if (pb = p) 

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

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

   733                              path_by_shm s p' pb) \<or>

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

   735      )  )"

   736 apply (rule ext, rule ext, rule iffI)

   737 apply (drule_tac pa = pa and pb = pb in path_by_shm_attach1, simp)

   738 apply (auto split:if_splits)[1]

   739 apply (drule_tac pa = pa and pb = pb in path_by_shm_attach2)

   740 apply (auto split:if_splits)

   741 done

   742 

   743 

   744 

   745 

   746 

   747 

   748 

   749 

   750 

   751 

   752 

   753 

   754 

   755 

   756 

   757 

   758 

   759 

   760 

   761 

   762 

   763 

   764 

   765 

   766 lemma info_flow_shm_detach:

   767   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 

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

   769      (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"

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

   771 by (auto simp:info_flow_shm_def one_flow_shm_def)

   772 

   773 lemma info_flow_shm_deleteshm:

   774   "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. 

   775      self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)     )"

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

   777 by (auto simp:info_flow_shm_def one_flow_shm_def)

   778 

   779 lemma info_flow_shm_clone:

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

   781      (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> 

   782      (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> 

   783      (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"

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

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

   786 sorry (*

   787 apply (auto simp:info_flow_shm_def one_flow_shm_def)

   788 done *)

   789 

   790 lemma info_flow_shm_execve:

   791   "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 

   792      (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb)    )"

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

   794 by (auto simp:info_flow_shm_def one_flow_shm_def)

   795 

   796 lemma info_flow_shm_kill:

   797   "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. 

   798      pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb                 )"

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

   800 by (auto simp:info_flow_shm_def one_flow_shm_def)

   801 

   802 lemma info_flow_shm_exit:

   803   "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. 

   804      pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb                          )"

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

   806 by (auto simp:info_flow_shm_def one_flow_shm_def)

   807 

   808 lemma info_flow_shm_other:

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

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

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

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

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

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

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

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

   817    \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"

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

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

   820 apply (erule_tac x = h in allE, simp)

   821 apply (drule procs_of_shm_prop1, auto)

   822 done

   823 

   824 

   825 (*

   826 lemma info_flow_shm_prop1: 

   827   "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 

   828    \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"

   829 by (induct rule: info_flow_shm.induct, auto)

   830 

   831 lemma info_flow_shm_cases:

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

   833   \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;

   834                        (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>

   835   \<Longrightarrow> P"

   836 by (erule info_flow_shm.cases, auto)

   837 

   838 definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   839 where

   840   "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"

   841 

   842 inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

   843 where

   844   "p \<in> current_procs s \<Longrightarrow> flows_shm s p p"

   845 | "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"

   846 

   847 definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"

   848 where

   849   "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"

   850 

   851 definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"

   852 where

   853   "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"

   854 

   855 inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"

   856 

   857 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"

   858 where

   859   "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"

   860 | "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. 

   861      if (p' = p) then flowed_procs s h 

   862      else if ()

   863     "

   864 

   865 

   866 lemma info_flow_shm_attach:

   867   "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> 

   868      (if (pa = p) 

   869       then (if (flag = SHM_RDWR) 

   870             then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)

   871             else (pb = p)) 

   872       else (if (pb = p) 

   873             then (pa, SHM_RDWR) \<in> procs_of_shm s h

   874             else info_flow_shm s pa pb)) )"

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

   876 apply (case_tac "info_flow_shm s pa pb", simp)

   877 

   878 thm info_flow_shm.cases

   879 apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)

   880 apply (erule info_flow_shm_cases, simp, simp split:if_splits)

   881 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)

   882 apply (rule notI, erule info_flow_shm.cases, simp+)

   883 pr 5

   884 *)

   885 lemmas info_flow_shm_simps = info_flow_shm_other (* info_flow_shm_attach *) info_flow_shm_detach info_flow_shm_deleteshm

   886   info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit