theory PIPBasics

imports PIPDefs RTree

begin

text {* (* ddd *)

  Following the HOL convention of {\em definitional extension}, we have

  given a concise and miniature model of PIP. To assure ourselves of the

  correctness of this model, we are going to derive a series of expected

  properties out of it.

  This file contains the very basic properties, useful for self-assurance,

  as well as for deriving more advance properties concerning the correctness

  and implementation of PIP. *}

section {* Generic auxiliary lemmas *}

lemma rel_eqI:

  assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"

  and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"

  shows "A = B"

  using assms by auto

lemma f_image_eq:

  assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"

  shows "f ` A = g ` A"

proof

  show "f ` A \<subseteq> g ` A"

    by(rule image_subsetI, auto intro:h)

next

  show "g ` A \<subseteq> f ` A"

   by (rule image_subsetI, auto intro:h[symmetric])

qed

section {* Lemmas do not depend on trace validity *}

text {* The following lemma serves to proof @{text "preced_tm_lt"} *}

lemma birth_time_lt:  

  assumes "s \<noteq> []"

  shows "last_set th s < length s"

  using assms

proof(induct s)

  case (Cons a s)

  show ?case

  proof(cases "s \<noteq> []")

    case False

    thus ?thesis

      by (cases a, auto)

  next

    case True

    show ?thesis using Cons(1)[OF True]

      by (cases a, auto)

  qed

qed simp

text {* The following lemma also serves to proof @{text "preced_tm_lt"} *}

lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"

  by (induct s, auto)

text {* The following lemma is used in Correctness.thy *}

lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"

  by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)

text {*

  The following lemma says that if a resource is waited for, it must be held

  by someone else. *}

lemma waiting_holding:

  assumes "waiting (s::state) th cs"

  obtains th' where "holding s th' cs"

proof -

  from assms[unfolded s_waiting_def, folded wq_def]

  obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"

    by (metis empty_iff hd_in_set list.set(1))

  hence "holding s th' cs" 

    unfolding s_holding_def by auto

  from that[OF this] show ?thesis .

qed

text {*

  The following @{text "children_RAG_alt_def"} relates

  @{term children} in @{term RAG} to the notion of @{term holding}.

  It is a technical lemmas used to prove the two following lemmas.

*}

lemma children_RAG_alt_def:

  "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"

  by (unfold s_RAG_def, auto simp:children_def s_holding_abv)

text {*

  The following two lemmas relate @{term holdents} and @{term cntCS}

  to @{term children} in @{term RAG}, so that proofs about

  @{term holdents} and @{term cntCS} can be carried out under 

  the support of the abstract theory of {\em relational graph}

  (and specifically {\em relational tree} and {\em relational forest}).

*}

lemma holdents_alt_def:

  "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"

  by (unfold children_RAG_alt_def holdents_def, simp add: image_image)

lemma cntCS_alt_def:

  "cntCS s th = card (children (RAG s) (Th th))"

  apply (unfold children_RAG_alt_def cntCS_def holdents_def)

  by (rule card_image[symmetric], auto simp:inj_on_def)

text {*

  The following two lemmas show the inclusion relations

  among three key sets, namely @{term running}, @{term readys}

  and @{term threads}.

*}

lemma running_ready: 

  shows "running s \<subseteq> readys s"

  unfolding running_def readys_def

  by auto 

lemma readys_threads:

  shows "readys s \<subseteq> threads s"

  unfolding readys_def

  by auto

text {*

  The following lemma says that if a thread is running, 

  it must be the head of every waiting queue it is in. 

  In other words, a running thread must have got every 

  resource it has requested.

*}

lemma running_wqE:

  assumes "th \<in> running s"

  and "th \<in> set (wq s cs)"

  obtains rest where "wq s cs = th#rest"

proof -

  from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"

    by (metis empty_iff list.exhaust list.set(1))

  have "th' = th"

  proof(rule ccontr)

    assume "th' \<noteq> th"

    hence "th \<noteq> hd (wq s cs)" using eq_wq by auto 

    with assms(2)

    have "waiting s th cs" 

      by (unfold s_waiting_def, fold wq_def, auto)

    with assms show False 

      by (unfold running_def readys_def, auto)

  qed

  with eq_wq that show ?thesis by metis

qed

text {*

  Every thread can only be blocked on one critical resource, 

  symmetrically, every critical resource can only be held by one thread. 

  This fact is much more easier according to our definition. 

*}

lemma held_unique:

  assumes "holding (s::event list) th1 cs"

  and "holding s th2 cs"

  shows "th1 = th2"

 by (insert assms, unfold s_holding_def, auto)

text {*

  The following three lemmas establishes the uniqueness of

  precedence, a key property about precedence.

  The first two are just technical lemmas to assist the proof

  of the third.

*}

lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits)

lemma last_set_unique: 

  "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>

          \<Longrightarrow> th1 = th2"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits dest:last_set_lt)

lemma preced_unique : 

  assumes pcd_eq: "preced th1 s = preced th2 s"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "th1 = th2"

proof -

  from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)

  from last_set_unique [OF this th_in1 th_in2]

  show ?thesis .

qed

text {*

  The following lemma shows that there exits a linear order

  on precedences, which is crucial for the notion of 

  @{term Max} to be applicable.

*}

lemma preced_linorder: 

  assumes neq_12: "th1 \<noteq> th2"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"

proof -

  from preced_unique [OF _ th_in1 th_in2] and neq_12 

  have "preced th1 s \<noteq> preced th2 s" by auto

  thus ?thesis by auto

qed

text {*

  The following lemma case analysis the situations when

  two nodes are in @{term RAG}.

*}

lemma in_RAG_E:

  assumes "(n1, n2) \<in> RAG (s::state)"

  obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"

        | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"

  using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv]

  by auto

text {*

  The following lemmas are the simplification rules 

  for @{term count}, @{term cntP}, @{term cntV}.

  It is part of the scheme to use the counting 

  of @{term "P"} and @{term "V"} operations to reason about

  the number of resources occupied by one thread.

*}

lemma count_rec1 [simp]: 

  assumes "Q e"

  shows "count Q (e#es) = Suc (count Q es)"

  using assms

  by (unfold count_def, auto)

lemma count_rec2 [simp]: 

  assumes "\<not>Q e"

  shows "count Q (e#es) = (count Q es)"

  using assms

  by (unfold count_def, auto)

lemma count_rec3 [simp]: 

  shows "count Q [] =  0"

  by (unfold count_def, auto)

lemma cntP_simp1[simp]:

  "cntP (P th cs'#s) th = cntP s th + 1"

  by (unfold cntP_def, simp)

lemma cntP_simp2[simp]:

  assumes "th' \<noteq> th"

  shows "cntP (P th cs'#s) th' = cntP s th'"

  using assms

  by (unfold cntP_def, simp)

lemma cntP_simp3[simp]:

  assumes "\<not> isP e"

  shows "cntP (e#s) th' = cntP s th'"

  using assms

  by (unfold cntP_def, cases e, simp+)

lemma cntV_simp1[simp]:

  "cntV (V th cs'#s) th = cntV s th + 1"

  by (unfold cntV_def, simp)

lemma cntV_simp2[simp]:

  assumes "th' \<noteq> th"

  shows "cntV (V th cs'#s) th' = cntV s th'"

  using assms

  by (unfold cntV_def, simp)

lemma cntV_simp3[simp]:

  assumes "\<not> isV e"

  shows "cntV (e#s) th' = cntV s th'"

  using assms

  by (unfold cntV_def, cases e, simp+)

text {*

  The following two lemmas show that only @{term P}

  and @{term V} operation can change the value 

  of @{term cntP} and @{term cntV}, which is true

  obviously.

*}

lemma cntP_diff_inv:

  assumes "cntP (e#s) th \<noteq> cntP s th"

  obtains cs where "e = P th cs"

proof(cases e)

  case (P th' pty)

  show ?thesis using that

  by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 

        insert assms P, auto simp:cntP_def)

qed (insert assms, auto simp:cntP_def)

lemma cntV_diff_inv:

  assumes "cntV (e#s) th \<noteq> cntV s th"

  obtains cs' where "e = V th cs'"

proof(cases e)

  case (V th' pty)

  show ?thesis using that

  by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 

        insert assms V, auto simp:cntV_def)

qed (insert assms, auto simp:cntV_def)

text {* 

  The following three lemmas shows the shape

  of nodes in @{term tRAG}.

*}

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)

lemma tRAG_tG:

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

  shows "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "(the_thread n1, the_thread n2) \<in> tG s"

  using assms

  by (unfold tRAG_def_tG tG_alt_def, auto)

lemma tG_tRAG: 

  assumes "(th1, th2) \<in> tG s"

  shows "(Th th1, Th th2) \<in> tRAG s"

  using assms

  by (unfold tRAG_def_tG, 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 map_prod_RE:

  assumes "(u, v) \<in> (map_prod f f ` R)"

  obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R"

  using assms

  by auto

lemma map_prod_tranclE:

  assumes "(u, v) \<in> (map_prod f f ` R)^+"

  and "inj_on f (Field R)"

  obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^+"

proof -

  from assms(1)

  have "\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>+"

  proof(induct rule:trancl_induct)

    case (base y)

    thus ?case by auto

  next

    case (step y z)

    then obtain u' v' where h1: "u = f u'"  "y = f v'" "(u', v') \<in> R\<^sup>+" by auto

    from map_prod_RE[OF step(2)] obtain v'' u'' 

                      where h2: "y = f v''" "z = f u''" "(v'', u'') \<in> R" by auto

    from h1 h2 have "f v' = f v''" by simp

    hence eq_v': "v' = v''"

    proof(cases rule:inj_onD[OF assms(2), consumes 1])

      case 1

      from h1(3) show ?case using trancl_subset_Field2[of R] by auto

    next

      case 2

      from h2(3) show ?case by (simp add: Domain.DomainI Field_def) 

    qed

    let ?u = "u'" and ?v = "u''"

    have "(?u, ?v) \<in> R^+" using h1(3)[unfolded eq_v'] h2(3) by auto

    with h1 h2

    show ?case by auto

  qed

  thus ?thesis using that by metis

qed

lemma map_prod_rtranclE:

  assumes "(u, v) \<in> (map_prod f f ` R)^*"

  and "inj_on f (Field R)"

  obtains (root) "u = v" 

        | (trancl) u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^*"

proof -

  from rtranclD[OF assms(1)]

  have "u = v \<or> (\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>*)"

  proof

    assume "u = v" thus ?thesis by auto

  next

    assume "u \<noteq> v \<and> (u, v) \<in> (map_prod f f ` R)\<^sup>+"

    hence "(u, v) \<in> (map_prod f f ` R)\<^sup>+" by auto

    thus ?thesis

     by (rule map_prod_tranclE[OF _ assms(2)], auto dest!:trancl_into_rtrancl)

  qed

  with that show ?thesis by auto

qed

lemma Field_tRAGE:

  assumes "n \<in> (Field (tRAG s))"

  obtains th where "n = Th th"

proof -

  from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def]

  show ?thesis using that by auto

qed

lemma trancl_tG_tRAG:

  assumes "(th1, th2) \<in> (tG s)^+"

  shows "(Th th1, Th th2) \<in> (tRAG s)^+"

proof -

  have "inj_on the_thread (Field (tRAG s))"

    by (unfold inj_on_def Field_def tRAG_alt_def, auto)

  from map_prod_tranclE[OF assms[unfolded tG_def] this]

  obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"

    by auto

  hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)

  from this[unfolded trancl_domain trancl_range]

  have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" 

    by (unfold Field_def, auto)

  then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"

    by (auto elim!:Field_tRAGE)

  with h have "th1' = th1" "th2' = th2" by (auto)

  from h(3)[unfolded h' this]

  show ?thesis by (auto simp:ancestors_def)

qed

lemma rtrancl_tG_tRAG:

  assumes "(th1, th2) \<in> (tG s)^*"

  shows "(Th th1, Th th2) \<in> (tRAG s)^*"

proof -

  from rtranclD[OF assms]

  show ?thesis

  proof

    assume "th1 = th2" thus "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" by auto

  next

    assume "th1 \<noteq> th2 \<and> (th1, th2) \<in> (tG s)\<^sup>+"

    hence "(th1, th2) \<in> (tG s)\<^sup>+" by auto

    from trancl_into_rtrancl[OF trancl_tG_tRAG[OF this]]

    show "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" .

  qed

qed

lemma trancl_tRAG_tG:

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

  obtains "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" 

          "(the_thread n1, the_thread n2) \<in> (tG s)^+"

proof -

  have inj: "inj_on Th (Field (tG s))" 

    by (unfold inj_on_def Field_def, auto)

  show ?thesis 

    by (rule map_prod_tranclE[OF assms[unfolded tRAG_def_tG] inj], auto intro!:that)

qed

lemma rtrancl_tRAG_tG:

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

  obtains "n1 = n2" 

          | "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "the_thread n1 \<noteq> the_thread n2"

            "(the_thread n1, the_thread n2) \<in> (tG s)^*"

proof -

  from rtranclD[OF assms]

  have "n1 = n2 \<or>

          n1 = Th (the_thread n1) \<and> n2 = Th (the_thread n2) \<and> the_thread n1 \<noteq> the_thread n2 \<and>

          (the_thread n1, the_thread n2) \<in> (tG s)^*"

  proof

    assume h: "n1 \<noteq> n2 \<and> (n1, n2) \<in> (tRAG s)\<^sup>+"

    hence "(n1, n2) \<in> (tRAG s)\<^sup>+" by auto

    from trancl_tRAG_tG[OF this]

    have "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" 

          "(the_thread n1, the_thread n2) \<in> (tG s)\<^sup>+" by auto

    with h 

    show ?thesis by auto

  qed auto

    with that show ?thesis by auto

qed

lemma ancestors_imageE:

  assumes "u \<in> ancestors ((map_prod f f) ` R) v"

  and "inj_on f (Field R)"

  obtains u' v' where "u = (f u')" "v = (f v')" "u' \<in> ancestors R v'"

  using assms unfolding ancestors_def

  by (metis map_prod_tranclE mem_Collect_eq)

lemma tRAG_ancestorsE_tG:

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

  obtains "x = Th (the_thread x)" "u = Th (the_thread u)" 

           "the_thread x \<in> ancestors (tG s) (the_thread u)"

proof -

  from assms[unfolded ancestors_def]

  have "(u, x) \<in> (tRAG s)\<^sup>+" by simp

  from trancl_tRAG_tG[OF this]

  show ?thesis using that by (auto simp:ancestors_def)

qed

lemma ancestors_tG_tRAG:

  assumes "th1 \<in> ancestors (tG s) th2"

  shows "Th th1 \<in> ancestors (tRAG s) (Th th2)"

proof -

  from assms[unfolded ancestors_def]

  have "(th2, th1) \<in> (tG s)\<^sup>+" by simp

  from trancl_tG_tRAG[OF this]