ML {*quick_and_dirty := true*}

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"

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

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)

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

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