section {*

  This file contains lemmas used to guide the recalculation of current precedence 

  after every system call (or system operation)

*}

theory Implementation

imports PIPBasics Max RTree

begin

text {* @{text "the_preced"} is also the same as @{text "preced"}, the only

       difference is the order of arguemts. *}

definition "the_preced s th = preced th s"

lemma inj_the_preced: 

  "inj_on (the_preced s) (threads s)"

  by (metis inj_onI preced_unique the_preced_def)

text {* @{term "the_thread"} extracts thread out of RAG node. *}

fun the_thread :: "node \<Rightarrow> thread" where

   "the_thread (Th th) = th"

text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}

definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"

text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}

definition "hRAG (s::state) =  {(Cs cs, Th th) | th cs. holding s th cs}"

text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"

  by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv 

             s_holding_abv cs_RAG_def, auto)

text {* 

  The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.

  It characterizes the dependency between threads when calculating current

  precedences. It is defined as the composition of the above two sub-graphs, 

  names @{term "wRAG"} and @{term "hRAG"}.

 *}

definition "tRAG s = wRAG s O hRAG s"

(* ccc *)

definition "cp_gen s x =

                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

lemma tRAG_alt_def: 

  "tRAG s = {(Th th1, Th th2) | th1 th2. 

                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"

 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)

lemma tRAG_Field:

  "Field (tRAG s) \<subseteq> Field (RAG s)"

  by (unfold tRAG_alt_def Field_def, auto)

lemma tRAG_ancestorsE:

  assumes "x \<in> ancestors (tRAG s) u"

  obtains th where "x = Th th"

proof -

  from assms have "(u, x) \<in> (tRAG s)^+" 

      by (unfold ancestors_def, auto)

  from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto

  then obtain th where "x = Th th"

    by (unfold tRAG_alt_def, auto)

  from that[OF this] show ?thesis .

qed

lemma tRAG_mono:

  assumes "RAG s' \<subseteq> RAG s"

  shows "tRAG s' \<subseteq> tRAG s"

  using assms 

  by (unfold tRAG_alt_def, auto)

lemma holding_next_thI:

  assumes "holding s th cs"

  and "length (wq s cs) > 1"

  obtains th' where "next_th s th cs th'"

proof -

  from assms(1)[folded eq_holding, unfolded cs_holding_def]

  have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" .

  then obtain rest where h1: "wq s cs = th#rest" 

    by (cases "wq s cs", auto)

  with assms(2) have h2: "rest \<noteq> []" by auto

  let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"

  have "next_th s th cs ?th'" using  h1(1) h2 

    by (unfold next_th_def, auto)

  from that[OF this] show ?thesis .

qed

lemma RAG_tRAG_transfer:

  assumes "vt s'"

  assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"

  and "(Cs cs, Th th'') \<in> RAG s'"

  shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")

proof -

  interpret vt_s': valid_trace "s'" using assms(1)

    by (unfold_locales, simp)

  interpret rtree: rtree "RAG s'"

  proof

  show "single_valued (RAG s')"

  apply (intro_locales)

    by (unfold single_valued_def, 

        auto intro:vt_s'.unique_RAG)

  show "acyclic (RAG s')"

     by (rule vt_s'.acyclic_RAG)

  qed

  { fix n1 n2

    assume "(n1, n2) \<in> ?L"

    from this[unfolded tRAG_alt_def]

    obtain th1 th2 cs' where 

      h: "n1 = Th th1" "n2 = Th th2" 

         "(Th th1, Cs cs') \<in> RAG s"

         "(Cs cs', Th th2) \<in> RAG s" by auto

    from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto

    from h(3) and assms(2) 

    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 

          (Th th1, Cs cs') \<in> RAG s'" by auto

    hence "(n1, n2) \<in> ?R"

    proof

      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"

      hence eq_th1: "th1 = th" by simp

      moreover have "th2 = th''"

      proof -

        from h1 have "cs' = cs" by simp

        from assms(3) cs_in[unfolded this] rtree.sgv

        show ?thesis

          by (unfold single_valued_def, auto)

      qed

      ultimately show ?thesis using h(1,2) by auto

    next

      assume "(Th th1, Cs cs') \<in> RAG s'"

      with cs_in have "(Th th1, Th th2) \<in> tRAG s'"

        by (unfold tRAG_alt_def, auto)

      from this[folded h(1, 2)] show ?thesis by auto

    qed

  } moreover {

    fix n1 n2

    assume "(n1, n2) \<in> ?R"

    hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto

    hence "(n1, n2) \<in> ?L" 

    proof

      assume "(n1, n2) \<in> tRAG s'"

      moreover have "... \<subseteq> ?L"

      proof(rule tRAG_mono)

        show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)

      qed

      ultimately show ?thesis by auto

    next

      assume eq_n: "(n1, n2) = (Th th, Th th'')"

      from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto

      moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto

      ultimately show ?thesis 

        by (unfold eq_n tRAG_alt_def, auto)

    qed

  } ultimately show ?thesis by auto

qed

context valid_trace

begin

lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

end

lemma cp_alt_def:

  "cp s th =  

           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"

proof -

  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =

        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 

          (is "Max (_ ` ?L) = Max (_ ` ?R)")

  proof -

    have "?L = ?R" 

    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)

    thus ?thesis by simp

  qed

  thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)

qed

lemma cp_gen_alt_def:

  "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"

    by (auto simp:cp_gen_def)

lemma tRAG_nodeE:

  assumes "(n1, n2) \<in> tRAG s"

  obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"

  using assms

  by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)

lemma subtree_nodeE:

  assumes "n \<in> subtree (tRAG s) (Th th)"

  obtains th1 where "n = Th th1"

proof -

  show ?thesis

  proof(rule subtreeE[OF assms])

    assume "n = Th th"

    from that[OF this] show ?thesis .

  next

    assume "Th th \<in> ancestors (tRAG s) n"

    hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

    hence "\<exists> th1. n = Th th1"

    proof(induct)

      case (base y)

      from tRAG_nodeE[OF this] show ?case by metis

    next

      case (step y z)

      thus ?case by auto

    qed

    with that show ?thesis by auto

  qed

qed

lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"

proof -

  have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 

    by (rule rtrancl_mono, auto simp:RAG_split)

  also have "... \<subseteq> ((RAG s)^*)^*"

    by (rule rtrancl_mono, auto)

  also have "... = (RAG s)^*" by simp

  finally show ?thesis by (unfold tRAG_def, simp)

qed

lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"

proof -

  { fix a

    assume "a \<in> subtree (tRAG s) x"

    hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)

    with tRAG_star_RAG[of s]

    have "(a, x) \<in> (RAG s)^*" by auto

    hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)

  } thus ?thesis by auto

qed

lemma tRAG_trancl_eq:

   "{th'. (Th th', Th th)  \<in> (tRAG s)^+} = 

    {th'. (Th th', Th th)  \<in> (RAG s)^+}"

   (is "?L = ?R")

proof -

  { fix th'

    assume "th' \<in> ?L"

    hence "(Th th', Th th) \<in> (tRAG s)^+" by auto

    from tranclD[OF this]

    obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto

    from tRAG_subtree_RAG[of s] and this(2)

    have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) 

    moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto 

    ultimately have "th' \<in> ?R"  by auto 

  } moreover 

  { fix th'

    assume "th' \<in> ?R"

    hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)

    from plus_rpath[OF this]

    obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto

    hence "(Th th', Th th) \<in> (tRAG s)^+"

    proof(induct xs arbitrary:th' th rule:length_induct)

      case (1 xs th' th)

      then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)

      show ?case

      proof(cases "xs1")

        case Nil

        from 1(2)[unfolded Cons1 Nil]

        have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .

        hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)

        then obtain cs where "x1 = Cs cs" 

              by (unfold s_RAG_def, auto)

        from rpath_nnl_lastE[OF rp[unfolded this]]

        show ?thesis by auto

      next

        case (Cons x2 xs2)

        from 1(2)[unfolded Cons1[unfolded this]]

        have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .

        from rpath_edges_on[OF this]

        have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .

        have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"

            by (simp add: edges_on_unfold)

        with eds have rg1: "(Th th', x1) \<in> RAG s" by auto

        then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)

        have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"

            by (simp add: edges_on_unfold)

        from this eds

        have rg2: "(x1, x2) \<in> RAG s" by auto

        from this[unfolded eq_x1] 

        obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)

        from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]

        have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)

        from rp have "rpath (RAG s) x2 xs2 (Th th)"

           by  (elim rpath_ConsE, simp)

        from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .

        show ?thesis

        proof(cases "xs2 = []")

          case True

          from rpath_nilE[OF rp'[unfolded this]]

          have "th1 = th" by auto

          from rt1[unfolded this] show ?thesis by auto

        next

          case False

          from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]

          have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp

          with rt1 show ?thesis by auto

        qed

      qed

    qed

    hence "th' \<in> ?L" by auto

  } ultimately show ?thesis by blast

qed

lemma tRAG_trancl_eq_Th:

   "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 

    {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"

    using tRAG_trancl_eq by auto

lemma dependants_alt_def:

  "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"

  by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

context valid_trace

begin

lemma count_eq_tRAG_plus:

  assumes "cntP s th = cntV s th"

  shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"

  using assms count_eq_dependants dependants_alt_def eq_dependants by auto 

lemma count_eq_RAG_plus:

  assumes "cntP s th = cntV s th"

  shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"

  using assms count_eq_dependants cs_dependants_def eq_RAG by auto

lemma count_eq_RAG_plus_Th:

  assumes "cntP s th = cntV s th"

  shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"

  using count_eq_RAG_plus[OF assms] by auto

lemma count_eq_tRAG_plus_Th:

  assumes "cntP s th = cntV s th"

  shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"

   using count_eq_tRAG_plus[OF assms] by auto

end

lemma tRAG_subtree_eq: 

   "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"

   (is "?L = ?R")

proof -

  { fix n 

    assume h: "n \<in> ?L"

    hence "n \<in> ?R"

    by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 

  } moreover {

    fix n

    assume "n \<in> ?R"

    then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"

      by (auto simp:subtree_def)

    from rtranclD[OF this(2)]

    have "n \<in> ?L"

    proof

      assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"

      with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto

      thus ?thesis using subtree_def tRAG_trancl_eq by fastforce

    qed (insert h, auto simp:subtree_def)

  } ultimately show ?thesis by auto

qed

lemma threads_set_eq: 

   "the_thread ` (subtree (tRAG s) (Th th)) = 

                  {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")

   by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

lemma cp_alt_def1: 

  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"

proof -

  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =

       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"

       by auto

  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)

qed

lemma cp_gen_def_cond: 

  assumes "x = Th th"

  shows "cp s th = cp_gen s (Th th)"

by (unfold cp_alt_def1 cp_gen_def, simp)

lemma cp_gen_over_set:

  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"

  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"

proof(rule f_image_eq)

  fix a

  assume "a \<in> A"

  from assms[rule_format, OF this]

  obtain th where eq_a: "a = Th th" by auto

  show "cp_gen s a = (cp s \<circ> the_thread) a"

    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)

qed

context valid_trace

begin

lemma RAG_threads:

  assumes "(Th th) \<in> Field (RAG s)"

  shows "th \<in> threads s"

  using assms

  by (metis Field_def UnE dm_RAG_threads range_in vt)

lemma subtree_tRAG_thread:

  assumes "th \<in> threads s"

  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")

proof -

  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

    by (unfold tRAG_subtree_eq, simp)

  also have "... \<subseteq> ?R"

  proof

    fix x

    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"

    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto

    from this(2)

    show "x \<in> ?R"

    proof(cases rule:subtreeE)

      case 1

      thus ?thesis by (simp add: assms h(1)) 

    next

      case 2

      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 

    qed

  qed

  finally show ?thesis .

qed

lemma readys_root:

  assumes "th \<in> readys s"

  shows "root (RAG s) (Th th)"

proof -

  { fix x

    assume "x \<in> ancestors (RAG s) (Th th)"

    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)

    from tranclD[OF this]

    obtain z where "(Th th, z) \<in> RAG s" by auto

    with assms(1) have False

         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)

         by (fold wq_def, blast)

  } thus ?thesis by (unfold root_def, auto)

qed

lemma readys_in_no_subtree:

  assumes "th \<in> readys s"

  and "th' \<noteq> th"

  shows "Th th \<notin> subtree (RAG s) (Th th')" 

proof

   assume "Th th \<in> subtree (RAG s) (Th th')"

   thus False

   proof(cases rule:subtreeE)

      case 1

      with assms show ?thesis by auto

   next

      case 2

      with readys_root[OF assms(1)]

      show ?thesis by (auto simp:root_def)

   qed

qed

lemma not_in_thread_isolated:

  assumes "th \<notin> threads s"

  shows "(Th th) \<notin> Field (RAG s)"

proof

  assume "(Th th) \<in> Field (RAG s)"

  with dm_RAG_threads and range_in assms

  show False by (unfold Field_def, blast)

qed

lemma wf_RAG: "wf (RAG s)"

proof(rule finite_acyclic_wf)

  from finite_RAG show "finite (RAG s)" .

next

  from acyclic_RAG show "acyclic (RAG s)" .

qed

lemma sgv_wRAG: "single_valued (wRAG s)"

  using waiting_unique

  by (unfold single_valued_def wRAG_def, auto)

lemma sgv_hRAG: "single_valued (hRAG s)"

  using holding_unique 

  by (unfold single_valued_def hRAG_def, auto)

lemma sgv_tRAG: "single_valued (tRAG s)"

  by (unfold tRAG_def, rule single_valued_relcomp, 

              insert sgv_wRAG sgv_hRAG, auto)

lemma acyclic_tRAG: "acyclic (tRAG s)"

proof(unfold tRAG_def, rule acyclic_compose)

  show "acyclic (RAG s)" using acyclic_RAG .

next

  show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto

next

  show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto

qed

lemma sgv_RAG: "single_valued (RAG s)"

  using unique_RAG by (auto simp:single_valued_def)

lemma rtree_RAG: "rtree (RAG s)"

  using sgv_RAG acyclic_RAG

  by (unfold rtree_def rtree_axioms_def sgv_def, auto)

end

sublocale valid_trace < rtree_RAG: rtree "RAG s"

proof

  show "single_valued (RAG s)"

  apply (intro_locales)

    by (unfold single_valued_def, 

        auto intro:unique_RAG)

  show "acyclic (RAG s)"

     by (rule acyclic_RAG)

qed

sublocale valid_trace < rtree_s: rtree "tRAG s"

proof(unfold_locales)

  from sgv_tRAG show "single_valued (tRAG s)" .

next

  from acyclic_tRAG show "acyclic (tRAG s)" .

qed

sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"

proof -

  show "fsubtree (RAG s)"

  proof(intro_locales)