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)^+"+
−
  using assms unfolding tRAG_def_tG+
−
proof(induct rule:trancl_induct)+
−
  case (step y z)+
−
  from step(2) have "(Th y, Th z) \<in> map_prod Th Th ` (tG s)" by auto+
−
  with step(3)+
−
  show ?case by auto+
−
qed auto+
−
+
−
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]+
−
  show ?thesis by (simp add:ancestors_def)+
−
qed+
−
+
−
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 subtree_nodeE_tG:+
−
  assumes "n \<in> subtree (tRAG s) (Th th)"+
−
  obtains "n = Th (the_thread n)" "the_thread n \<in> subtree (tG s) th" +
−
proof -+
−
  from assms[unfolded subtree_def]+
−
  have "(n, Th th) \<in> (tRAG s)\<^sup>*" by simp+
−
  hence "n = Th (the_thread n) \<and> the_thread n \<in> subtree (tG s) th"+
−
   by (cases rule:rtrancl_tRAG_tG, auto simp:subtree_def)+
−
  thus ?thesis using that by auto+
−
qed+
−
+
−
lemma subtree_tRAG_tG:+
−
  "subtree (tRAG s) (Th th) = Th ` (subtree (tG s) th)" (is "?L = ?R")+
−
proof -+
−
  { fix n+
−
    assume "n \<in> ?L"+
−
    from subtree_nodeE_tG[OF this]+
−
    have "n \<in> ?R" by auto+
−
  } moreover {+
−
    fix n+
−
    assume "n \<in> ?R"+
−
    then obtain th' where h: "th' \<in> subtree (tG s) th" "n = Th th'" by auto+
−
    hence "(th', th) \<in> (tG s)^*" by (auto simp:subtree_def)+
−
    from rtrancl_tG_tRAG[OF this] and h+
−
    have "n \<in> ?L" by (auto simp:subtree_def)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma subtree_tG_tRAG:+
−
  "(subtree (tG s) th) = the_thread ` (subtree (tRAG s) (Th th))" (is "?L = ?R")+
−
proof -+
−
  have "?R = (the_thread \<circ> Th) ` subtree (tG s) th"+
−
    by (unfold subtree_tRAG_tG image_comp, simp)+
−
  also have "... = id ` ?L" by (rule image_cong, auto)+
−
  finally show ?thesis by simp+
−
qed+
−
+
−
text {*+
−
  The following lemmas relate @{term tRAG} with +
−
  @{term RAG} from different perspectives. +
−
*}+
−
+
−
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+
−
    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 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, auto)+
−
        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 tRAG_Field:+
−
  "Field (tRAG s) \<subseteq> Field (RAG s)"+
−
  by (unfold tRAG_alt_def Field_def, auto)+
−
+
−
lemma tRAG_mono:+
−
  assumes "RAG s' \<subseteq> RAG s"+
−
  shows "tRAG s' \<subseteq> tRAG s"+
−
  using assms +
−
  by (unfold tRAG_alt_def, auto)+
−
+
−
+
−
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 (* ccc *)+
−
    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)+
−
+
−
text {*+
−
  The following lemmas is an alternative definition of @{term cp},+
−
  which is based on the notion of subtrees in @{term RAG} and +
−
  is handy to use once the abstract theory of {\em relational graph}+
−
  (and specifically {\em relational tree} and {\em relational forest})+
−
  are in place.+
−
*}+
−
+
−
lemma cp_s_def: "cp s th = Max (preceds (subtree (tG s) th) s)"+
−
  by (unfold cp_eq cpreced_def s_tG_abv, simp)+
−
+
−
lemma cp_alt_def:+
−
  "cp s th =  Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"+
−
  apply (unfold cp_s_def subtree_tG_tRAG threads_set_eq)+
−
  by (smt Collect_cong Setcompr_eq_image the_preced_def)+
−
+
−
text {*+
−
  The following is another definition of @{term cp}.+
−
*}+
−
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+
−
+
−
text {*+
−
  The following is another definition of @{term cp} based on @{term tG}:+
−
*}+
−
lemma cp_alt_def2: +
−
  "cp s th = Max (the_preced s ` (subtree (tG s) th))"+
−
  by (unfold cp_alt_def1 subtree_tG_tRAG image_comp, simp)+
−
+
−
+
−
lemma RAG_tRAG_transfer:+
−
  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 -+
−
  { 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(1) have cs_in: "(Cs cs', Th th2) \<in> RAG s" by auto+
−
    from h(3) and assms(1) +
−
    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)"+
−
      with assms(1) have "(Th th1, Cs cs) \<in> RAG s'" by auto+
−
      moreover have "th2 = th''"+
−
      proof -+
−
        from h1 have "cs' = cs" by simp+
−
        from assms(2) cs_in[unfolded this]+
−
        have "holding s th'' cs" "holding s th2 cs"+
−
          by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
        from held_unique[OF this]+
−
        show ?thesis by simp +
−
      qed+
−
      ultimately show ?thesis using h(1,2) h1 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(1), auto)+
−
      qed+
−
      ultimately show ?thesis by auto+
−
    next+
−
      assume eq_n: "(n1, n2) = (Th th, Th th'')"+
−
      from assms(1, 2) have "(Cs cs, Th th'') \<in> RAG s'" by auto+
−
      moreover have "(Th th, Cs cs) \<in> RAG s'" using assms(1) by auto+
−
      ultimately show ?thesis +
−
        by (unfold eq_n tRAG_alt_def, auto)+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
section {* Locales used to investigate the execution of PIP *}+
−
+
−
text {* +
−
  The following locale @{text valid_trace} is used to constrain the +
−
  trace to be valid. All properties hold for valid traces are +
−
  derived under this locale. +
−
*}+
−
locale valid_trace = +
−
  fixes s+
−
  assumes vt : "vt s"+
−
+
−
text {* +
−
  The following locale @{text valid_trace_e} describes +
−
  the valid extension of a valid trace. The event @{text "e"}+
−
  represents an event in the system, which corresponds +
−
  to a one step operation of the PIP protocol. +
−
  It is required that @{text "e"} is an event eligible to happen+
−
  under state @{text "s"}, which is already required to be valid+
−
  by the parent locale @{text "valid_trace"}.+
−
+
−
  This locale is used to investigate one step execution of PIP, +
−
  properties concerning the effects of @{text "e"}'s execution, +
−
  for example, how the values of observation functions are changed, +
−
  or how desirable properties are kept invariant, are derived+
−
  under this locale. The state before execution is @{text "s"}, while+
−
  the state after execution is @{text "e#s"}. Therefore, the lemmas +
−
  derived usually relate observations on @{text "e#s"} to those +
−
  on @{text "s"}.+
−
*}+
−
+
−
locale valid_trace_e = valid_trace ++
−
  fixes e+
−
  assumes vt_e: "vt (e#s)"+
−
begin+
−
+
−
text {*+
−
  The following lemma shows that @{text "e"} must be a +
−
  eligible event (or a valid step) to be taken under+
−
  the state represented by @{text "s"}.+
−
*}+
−
lemma pip_e: "PIP s e"+
−
  using vt_e by (cases, simp)  +
−
+
−
end+
−
+
−
text {*+
−
  Because @{term "e#s"} is also a valid trace, properties +
−
  derived for valid trace @{term s} also hold on @{term "e#s"}.+
−
*}+
−
sublocale valid_trace_e < vat_es: valid_trace "e#s" +
−
  using vt_e+
−
  by (unfold_locales, simp)+
−
+
−
text {*+
−
  For each specific event (or operation), there is a sublocale+
−
  further constraining that the event @{text e} to be that +
−
  particular event. +
−
+
−
  For example, the following +
−
  locale @{text "valid_trace_create"} is the sublocale for +
−
  event @{term "Create"}:+
−
*}+
−
locale valid_trace_create = valid_trace_e + +
−
  fixes th prio+
−
  assumes is_create: "e = Create th prio"+
−
+
−
locale valid_trace_exit = valid_trace_e + +
−
  fixes th+
−
  assumes is_exit: "e = Exit th"+
−
+
−
locale valid_trace_p = valid_trace_e + +
−
  fixes th cs+
−
  assumes is_p: "e = P th cs"+
−
+
−
text {*+
−
  locale @{text "valid_trace_p"} is divided further into two +
−
  sublocales, namely, @{text "valid_trace_p_h"} +
−
  and @{text "valid_trace_p_w"}.+
−
*}+
−
+
−
text {*+
−
  The following two sublocales @{text "valid_trace_p_h"}+
−
  and @{text "valid_trace_p_w"} represent two complementary +
−
  cases under @{text "valid_trace_p"}, where+
−
  @{text "valid_trace_p_h"} further constraints that+
−
  @{text "wq s cs = []"}, which means the waiting queue of +
−
  the requested resource @{text "cs"} is empty, in which+
−
  case,  the requesting thread @{text "th"} +
−
  will take hold of @{text "cs"}. +
−
+
−
  Opposite to @{text "valid_trace_p_h"},+
−
  @{text "valid_trace_p_w"} constraints that+
−
  @{text "wq s cs \<noteq> []"}, which means the waiting queue of +
−
  the requested resource @{text "cs"} is nonempty, in which+
−
  case,  the requesting thread @{text "th"} will be blocked+
−
  on @{text "cs"}: +
−
+
−
  Peculiar properties will be derived under respective +
−
  locales.+
−
*}+
−
+
−
locale valid_trace_p_h = valid_trace_p ++
−
  assumes we: "wq s cs = []"+
−
+
−
locale valid_trace_p_w = valid_trace_p ++
−
  assumes wne: "wq s cs \<noteq> []"+
−
begin+
−
+
−
text {*+
−
  The following @{text "holder"} designates+
−
  the holder of @{text "cs"} before the @{text "P"}-operation.+
−
*}+
−
definition "holder = hd (wq s cs)"+
−
+
−
text {*+
−
  The following @{text "waiters"} designates+
−
  the list of threads waiting for @{text "cs"} +
−
  before the @{text "P"}-operation.+
−
*}+
−
definition "waiters = tl (wq s cs)"+
−
end+
−
+
−
text {* +
−
  @{text "valid_trace_v"} is set for the @{term V}-operation.+
−
*}+
−
locale valid_trace_v = valid_trace_e + +
−
  fixes th cs+
−
  assumes is_v: "e = V th cs"+
−
begin+
−
  -- {* The following @{text "rest"} is the tail of +
−
        waiting queue of the resource @{text "cs"}+
−
        to be released by this @{text "V"}-operation.+
−
     *}+
−
  definition "rest = tl (wq s cs)"+
−
+
−
  text {*+
−
    The following @{text "wq'"} is the waiting+
−
    queue of @{term "cs"}+
−
    after the @{text "V"}-operation, which+
−
    is simply a reordering of @{term "rest"}. +
−
+
−
    The effect of this reordering needs to be +
−
    understood by two cases:+
−
    \begin{enumerate}+
−
    \item When @{text "rest = []"},+
−
    the reordering gives rise to an empty list as well, +
−
    which means there is no thread holding or waiting +
−
    for resource @{term "cs"}, therefore, it is free.+
−
+
−
    \item When @{text "rest \<noteq> []"}, the effect of +
−
    this reordering is to arbitrarily +
−
    switch one thread in @{term "rest"} to the +
−
    head, which, by definition take over the hold+
−
    of @{term "cs"} and is designated by @{text "taker"}+
−
    in the following sublocale @{text "valid_trace_v_n"}.+
−
  *}+
−
  definition "wq' = (SOME q. distinct q \<and> set q = set rest)"+
−
+
−
  text {* +
−
  The following @{text "rest'"} is the tail of the +
−
  waiting queue after the @{text "V"}-operation. +
−
  It plays only auxiliary role to ease reasoning. +
−
  *}+
−
  definition "rest' = tl wq'"+
−
+
−
end+
−
+
−
text {* +
−
  In the following, @{text "valid_trace_v"} is also +
−
  divided into two +
−
  sublocales: when @{text "rest"} is empty (represented+
−
  by @{text "valid_trace_v_e"}), which means, there is no thread waiting +
−
  for @{text "cs"}, therefore, after the @{text "V"}-operation, +
−
  it will become free; otherwise (represented +
−
  by @{text "valid_trace_v_n"}), one thread +
−
  will be picked from those in @{text "rest"} to take +
−
  over @{text "cs"}.+
−
*}+
−
+
−
locale valid_trace_v_e = valid_trace_v ++
−
  assumes rest_nil: "rest = []"+
−
+
−
locale valid_trace_v_n = valid_trace_v ++
−
  assumes rest_nnl: "rest \<noteq> []"+
−
begin+
−
+
−
text {* +
−
  The following @{text "taker"} is the thread to +
−
  take over @{text "cs"}. +
−
*}+
−
  definition "taker = hd wq'"+
−
+
−
end+
−
+
−
+
−
locale valid_trace_set = valid_trace_e + +
−
  fixes th prio+
−
  assumes is_set: "e = Set th prio"+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  Induction rule introduced to easy the +
−
  derivation of properties for valid trace @{term "s"}.+
−
  One more premises, namely @{term "valid_trace_e s e"}+
−
  is added, so that an interpretation of +
−
  @{text "valid_trace_e"} can be instantiated +
−
  so that all properties derived so far becomes +
−
  available in the proof of induction step.+
−
+
−
  You will see its use in the proofs that follows.+
−
*}+
−
lemma ind [consumes 0, case_names Nil Cons, induct type]:+
−
  assumes "PP []"+
−
     and "(\<And>s e. valid_trace_e s e \<Longrightarrow>+
−
                   PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"+
−
     shows "PP s"+
−
proof(induct rule:vt.induct[OF vt, case_names Init Step])+
−
  case Init+
−
  from assms(1) show ?case .+
−
next+
−
  case (Step s e)+
−
  show ?case+
−
  proof(rule assms(2))+
−
    show "valid_trace_e s e" using Step by (unfold_locales, auto)+
−
  next+
−
    show "PP s" using Step by simp+
−
  next+
−
    show "PIP s e" using Step by simp+
−
  qed+
−
qed+
−
+
−
+
−
lemma finite_threads:+
−
  shows "finite (threads s)"+
−
  using vt by (induct) (auto elim: step.cases)+
−
+
−
lemma  finite_readys: "finite (readys s)"+
−
  using finite_threads readys_threads rev_finite_subset by blast+
−
+
−
end+
−
+
−
+
−
section {* Waiting queues are distinct *}+
−
+
−
text {*+
−
  This section proves that every waiting queue in the system+
−
  is distinct, given in lemma @{text wq_distinct}.+
−
+
−
  The proof is split into the locales for events (or operations),+
−
  all contain a lemma named @{text "wq_distinct_kept"} to show that+
−
  the distinctiveness is preserved by the respective operation. All lemmas+
−
  before are to facilitate the proof of @{text "wq_distinct_kept"}.+
−
+
−
  The proof also demonstrates the common pattern to prove+
−
  invariant properties over valid traces, i.e. to spread the +
−
  invariant proof into locales and to assemble the results of all +
−
  locales to complete the final proof.+
−
  +
−
*}+
−
+
−
context valid_trace_create+
−
begin+
−
+
−
lemma wq_kept [simp]:+
−
  shows "wq (e#s) cs' = wq s cs'"+
−
  unfolding is_create wq_def+
−
  by (auto simp:Let_def)+
−
+
−
lemma wq_distinct_kept:+
−
  assumes "distinct (wq s cs')"+
−
  shows "distinct (wq (e#s) cs')"+
−
  using assms by simp+
−
end+
−
+
−
context valid_trace_exit+
−
begin+
−
+
−
lemma wq_kept [simp]:+
−
  shows "wq (e#s) cs' = wq s cs'"+
−
  unfolding is_exit wq_def+
−
  by (auto simp:Let_def)+
−
+
−
lemma wq_distinct_kept:+
−
  assumes "distinct (wq s cs')"+
−
  shows "distinct (wq (e#s) cs')"+
−
  using assms by simp+
−
end+
−
+
−
context valid_trace_p +
−
begin+
−
+
−
lemma wq_neq_simp [simp]:+
−
  assumes "cs' \<noteq> cs"+
−
  shows "wq (e#s) cs' = wq s cs'"+
−
    using assms unfolding is_p wq_def+
−
  by (auto simp:Let_def)+
−
+
−
lemma running_th_s:+
−
  shows "th \<in> running s"+
−
proof -+
−
  from pip_e[unfolded is_p]+
−
  show ?thesis by (cases, simp)+
−
qed+
−
+
−
lemma th_not_in_wq: +
−
  shows "th \<notin> set (wq s cs)"+
−
proof+
−
  assume otherwise: "th \<in> set (wq s cs)"+
−
  from running_wqE[OF running_th_s this]+
−
  obtain rest where eq_wq: "wq s cs = th#rest" by blast+
−
  with otherwise+
−
  have "holding s th cs"+
−
    unfolding s_holding_def by auto+
−
  hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"+
−
    by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
  from pip_e[unfolded is_p]+
−
  show False+
−
  proof(cases)+
−
    case (thread_P)+
−
    with cs_th_RAG show ?thesis by auto+
−
  qed+
−
qed+
−
                  +
−
lemma wq_es_cs: +
−
  "wq (e#s) cs =  wq s cs @ [th]"+
−
  by (unfold is_p wq_def, auto simp:Let_def)+
−
+
−
lemma wq_distinct_kept:+
−
  assumes "distinct (wq s cs')"+
−
  shows "distinct (wq (e#s) cs')"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  show ?thesis using True assms th_not_in_wq+
−
    by (unfold True wq_es_cs, auto)+
−
qed (insert assms, simp)+
−
+
−
end+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma wq_neq_simp [simp]:+
−
  assumes "cs' \<noteq> cs"+
−
  shows "wq (e#s) cs' = wq s cs'"+
−
    using assms unfolding is_v wq_def+
−
  by (auto simp:Let_def)+
−
+
−
lemma wq_s_cs:+
−
  "wq s cs = th#rest"+
−
proof -+
−
  from pip_e[unfolded is_v]+
−
  show ?thesis+
−
  proof(cases)+
−
    case (thread_V)+
−
    from this(2) show ?thesis+
−
      unfolding s_holding_def+
−
      by (metis empty_iff empty_set hd_Cons_tl rest_def) +
−
  qed+
−
qed+
−
+
−
lemma wq_es_cs:+
−
  "wq (e#s) cs = wq'"+
−
 using wq_s_cs[unfolded wq_def]+
−
 by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) +
−
+
−
lemma wq_distinct_kept:+
−
  assumes "distinct (wq s cs')"+
−
  shows "distinct (wq (e#s) cs')"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  show ?thesis+
−
  proof(unfold True wq_es_cs wq'_def, rule someI2)+
−
    show "distinct rest \<and> set rest = set rest"+
−
        using assms[unfolded True wq_s_cs] by auto+
−
  qed simp+
−
qed (insert assms, simp)+
−
+
−
end+
−
+
−
context valid_trace_set+
−
begin+
−
+
−
lemma wq_kept [simp]:+
−
  shows "wq (e#s) cs' = wq s cs'"+
−
  unfolding is_set wq_def+
−
  by (auto simp:Let_def)+
−
+
−
lemma wq_distinct_kept:+
−
  assumes "distinct (wq s cs')"+
−
  shows "distinct (wq (e#s) cs')"+
−
  using assms by simp+
−
end+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  The proof of @{text "wq_distinct"} shows how the results +
−
  proved in the foregoing locales are assembled in+
−
  a overall structure of induction and case analysis+
−
  to get the final conclusion. This scheme will be +
−
  used repeatedly in the following.+
−
*}+
−
lemma wq_distinct: "distinct (wq s cs)"+
−
proof(induct rule:ind)+
−
  case (Cons s e)+
−
  interpret vt_e: valid_trace_e s e using Cons by simp+
−
  show ?case +
−
  proof(cases e)+
−
    case (Create th prio)+
−
    interpret vt_create: valid_trace_create s e th prio +
−
      using Create by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_create.wq_distinct_kept) +
−
  next+
−
    case (Exit th)+
−
    interpret vt_exit: valid_trace_exit s e th  +
−
        using Exit by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_exit.wq_distinct_kept) +
−
  next+
−
    case (P th cs)+
−
    interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_p.wq_distinct_kept) +
−
  next+
−
    case (V th cs)+
−
    interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_v.wq_distinct_kept) +
−
  next+
−
    case (Set th prio)+
−
    interpret vt_set: valid_trace_set s e th prio+
−
        using Set by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_set.wq_distinct_kept) +
−
  qed+
−
qed (unfold wq_def Let_def, simp)+
−
+
−
end+
−
+
−
section {* Waiting queues and threads *}+
−
+
−
text {*+
−
  This section shows that all threads withing waiting queues are+
−
  in the @{term threads}-set. In other words, @{term threads} covers+
−
  all the threads in waiting queue.+
−
+
−
  The proof follows the same pattern as @{thm valid_trace.wq_distinct}.+
−
  The desired property is shown to be kept by all operations (or events)+
−
  in their respective locales, and finally the main lemmas is +
−
  derived by assembling the invariant keeping results of the locales. +
−
*}+
−
+
−
context valid_trace_create+
−
begin+
−
+
−
lemma +
−
  th_not_in_threads: "th \<notin> threads s"+
−
proof -+
−
  from pip_e[unfolded is_create]+
−
  show ?thesis by (cases, simp)+
−
qed+
−
+
−
lemma +
−
  threads_es [simp]: "threads (e#s) = threads s \<union> {th}"+
−
  by (unfold is_create, simp)+
−
+
−
lemma wq_threads_kept:+
−
  assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"+
−
  and "th' \<in> set (wq (e#s) cs')"+
−
  shows "th' \<in> threads (e#s)"+
−
proof -+
−
  have "th' \<in> threads s"+
−
  proof -+
−
    from assms(2)[unfolded wq_kept]+
−
    have "th' \<in> set (wq s cs')" .+
−
    from assms(1)[OF this] show ?thesis .+
−
  qed+
−
  with threads_es show ?thesis by simp+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_exit+
−
begin+
−
+
−
lemma threads_es [simp]: "threads (e#s) = threads s - {th}"+
−
  by (unfold is_exit, simp)+
−
+
−
lemma +
−
  th_not_in_wq: "th \<notin> set (wq s cs)"+
−
proof -+
−
  from pip_e[unfolded is_exit]+
−
  show ?thesis+
−
  apply(cases)+
−
  unfolding holdents_def s_holding_def+
−
  by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE)+
−
qed+
−
+
−
lemma wq_threads_kept:+
−
  assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"+
−
  and "th' \<in> set (wq (e#s) cs')"+
−
  shows "th' \<in> threads (e#s)"+
−
proof -+
−
  have "th' \<in> threads s"+
−
  proof -+
−
    from assms(2)[unfolded wq_kept]+
−
    have "th' \<in> set (wq s cs')" .+
−
    from assms(1)[OF this] show ?thesis .+
−
  qed+
−
  moreover have "th' \<noteq> th"+
−
  proof+
−
    assume otherwise: "th' = th"+
−
    from assms(2)[unfolded wq_kept]+
−
    have "th' \<in> set (wq s cs')" .+
−
    with th_not_in_wq[folded otherwise]+
−
    show False by simp+
−
  qed+
−
  ultimately show ?thesis+
−
    by (unfold threads_es, simp)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma +
−
  threads_es [simp]: "threads (e#s) = threads s"+
−
  by (unfold is_v, simp)+
−
+
−
lemma +
−
  th_not_in_rest: "th \<notin> set rest"+
−
proof+
−
  assume otherwise: "th \<in> set rest"+
−
  have "distinct (wq s cs)" by (simp add: wq_distinct)+
−
  from this[unfolded wq_s_cs] and otherwise+
−
  show False by auto+
−
qed+
−
+
−
lemma distinct_rest: "distinct rest"+
−
  by (simp add: distinct_tl rest_def wq_distinct)+
−
+
−
lemma+
−
  set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"+
−
proof(unfold wq_es_cs wq'_def, rule someI2)+
−
  show "distinct rest \<and> set rest = set rest"+
−
    by (simp add: distinct_rest) +
−
next+
−
  fix x+
−
  assume "distinct x \<and> set x = set rest"+
−
  thus "set x = set (wq s cs) - {th}" +
−
      by (unfold wq_s_cs, simp add:th_not_in_rest)+
−
qed+
−
+
−
lemma wq_threads_kept:+
−
  assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"+
−
  and "th' \<in> set (wq (e#s) cs')"+
−
  shows "th' \<in> threads (e#s)"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  have " th' \<in> threads s"+
−
  proof -+
−
    from assms(2)[unfolded True set_wq_es_cs]+
−
    have "th' \<in> set (wq s cs) - {th}" .+
−
    hence "th' \<in> set (wq s cs)" by simp+
−
    from assms(1)[OF this]+
−
    show ?thesis .+
−
  qed+
−
  with threads_es show ?thesis by simp+
−
next+
−
    case False+
−
    have "th' \<in> threads s"+
−
    proof -+
−
      from wq_neq_simp[OF False]+
−
      have "wq (e # s) cs' = wq s cs'" .+
−
      from assms(2)[unfolded this]+
−
      have "th' \<in> set (wq s cs')" .+
−
      from assms(1)[OF this]+
−
      show ?thesis .+
−
    qed+
−
    with threads_es show ?thesis by simp+
−
qed+
−
end+
−
+
−
context valid_trace_p+
−
begin+
−
+
−
lemma threads_es [simp]: "threads (e#s) = threads s"+
−
  by (unfold is_p, simp)+
−
+
−
lemma ready_th_s: "th \<in> readys s"+
−
  using running_th_s+
−
  by (unfold running_def, auto)+
−
+
−
lemma live_th_s: "th \<in> threads s"+
−
  using readys_threads ready_th_s by auto+
−
+
−
lemma wq_threads_kept:+
−
  assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"+
−
  and "th' \<in> set (wq (e#s) cs')"+
−
  shows "th' \<in> threads (e#s)"+
−
proof(cases "cs' = cs")+
−
    case True+
−
    from assms(2)[unfolded True wq_es_cs]+
−
    have "th' \<in> set (wq s cs) \<or> th' = th" by auto+
−
    thus ?thesis+
−
    proof+
−
      assume "th' \<in> set (wq s cs)"+
−
      from assms(1)[OF this] have "th' \<in> threads s" .+
−
      with threads_es+
−
      show ?thesis by simp+
−
    next+
−
      assume "th' = th"+
−
      with live_th_s have "th' \<in> threads s" by simp+
−
      with threads_es show ?thesis by simp+
−
    qed+
−
next+
−
    case False+
−
    have "th' \<in> threads s"+
−
    proof -+
−
      from wq_neq_simp[OF False]+
−
      have "wq (e # s) cs' = wq s cs'" .+
−
      from assms(2)[unfolded this]+
−
      have "th' \<in> set (wq s cs')" .+
−
      from assms(1)[OF this]+
−
      show ?thesis .+
−
    qed+
−
    with threads_es show ?thesis by simp+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_set+
−
begin+
−
+
−
lemma threads_kept[simp]:+
−
  "threads (e#s) = threads s"+
−
  by (unfold is_set, simp)+
−
+
−
lemma wq_threads_kept: +
−
  assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"+
−
  and "th' \<in> set (wq (e#s) cs')"+
−
  shows "th' \<in> threads (e#s)"+
−
proof -+
−
  have "th' \<in> threads s"+
−
     using assms(1)[OF assms(2)[unfolded wq_kept]] .+
−
  with threads_kept show ?thesis by simp+
−
qed+
−
+
−
end+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  The is the main lemma of this section, which is derived+
−
  by induction, case analysis on event @{text e} and +
−
  assembling the @{text "wq_threads_kept"}-results of +
−
  all possible cases of @{text "e"}.+
−
*}+
−
lemma wq_threads: +
−
  assumes "th \<in> set (wq s cs)"+
−
  shows "th \<in> threads s"+
−
  using assms+
−
proof(induct arbitrary:th cs rule:ind)+
−
  case (Nil)+
−
  thus ?case by (auto simp:wq_def)+
−
next+
−
  case (Cons s e)+
−
  interpret vt_e: valid_trace_e s e using Cons by simp+
−
  show ?case+
−
  proof(cases e)+
−
    case (Create th' prio')+
−
    interpret vt: valid_trace_create s e th' prio'+
−
      using Create by (unfold_locales, simp)+
−
    show ?thesis using vt.wq_threads_kept Cons by auto+
−
  next+
−
    case (Exit th')+
−
    interpret vt: valid_trace_exit s e th'+
−
      using Exit by (unfold_locales, simp)+
−
    show ?thesis using vt.wq_threads_kept Cons by auto+
−
  next+
−
    case (P th' cs')+
−
    interpret vt: valid_trace_p s e th' cs'+
−
      using P by (unfold_locales, simp)+
−
   show ?thesis using vt.wq_threads_kept Cons by auto+
−
  next+
−
    case (V th' cs')+
−
    interpret vt: valid_trace_v s e th' cs'+
−
      using V by (unfold_locales, simp)+
−
   show ?thesis using vt.wq_threads_kept Cons by auto+
−
  next+
−
    case (Set th' prio)+
−
    interpret vt: valid_trace_set s e th' prio+
−
      using Set by (unfold_locales, simp)+
−
   show ?thesis using vt.wq_threads_kept Cons by auto+
−
  qed+
−
qed +
−
+
−
subsection {* RAG and threads *}+
−
+
−
+
−
text {*+
−
  As corollaries of @{thm wq_threads}, it is shown in this subsection+
−
  that the fields (including both domain+
−
  and range) of @{term RAG} are covered by @{term threads}.+
−
*}+
−
+
−
lemma  dm_RAG_threads:+
−
  assumes in_dom: "(Th th) \<in> Domain (RAG s)"+
−
  shows "th \<in> threads s"+
−
proof -+
−
  from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto+
−
  moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)+
−
  ultimately have "(Th th, Cs cs) \<in> RAG s" by simp+
−
  then have "th \<in> set (wq s cs)"+
−
    using in_RAG_E s_waiting_def wq_def by auto+
−
  then show ?thesis using wq_threads by simp+
−
qed+
−
+
−
lemma dm_tG_threads: +
−
  assumes "th \<in> Domain (tG s)"+
−
  shows "th \<in> threads s"+
−
proof -+
−
  from assms[unfolded tG_alt_def]+
−
  have "(Th th) \<in> Domain (RAG s)" by (unfold Domain_def, auto)+
−
  from dm_RAG_threads[OF this] show ?thesis .+
−
qed+
−
+
−
lemma rg_RAG_threads: +
−
  assumes "(Th th) \<in> Range (RAG s)"+
−
  shows "th \<in> threads s"+
−
  using assms+
−
  apply(erule_tac RangeE)+
−
  apply(erule_tac in_RAG_E)+
−
  apply(auto)+
−
  using s_holding_def wq_def wq_threads by auto+
−
+
−
lemma rg_tG_threads: +
−
  assumes "th \<in> Range (tG s)"+
−
  shows "th \<in> threads s"+
−
proof -+
−
  from assms[unfolded tG_alt_def]+
−
  have "(Th th) \<in> Range (RAG s)" by (unfold Range_def, auto)+
−
  from rg_RAG_threads[OF this] show ?thesis .+
−
qed+
−
+
−
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 rg_RAG_threads)+
−
+
−
lemma tG_threads:+
−
  assumes "th \<in> Field (tG s)"+
−
  shows "th \<in> threads s"+
−
  using assms+
−
  by (metis Field_def UnE dm_tG_threads rg_tG_threads)+
−
+
−
lemma not_in_thread_isolated:+
−
  assumes "th \<notin> threads s"+
−
  shows "(Th th) \<notin> Field (RAG s)"+
−
  using RAG_threads assms by auto+
−
+
−
lemma not_in_thread_isolated_tG:+
−
  assumes "th \<notin> threads s"+
−
  shows "th \<notin> Field (tG s)"+
−
  using assms+
−
  using tG_threads by auto+
−
+
−
text {*+
−
  As a corollary, this lemma shows that @{term tRAG}+
−
  is also covered by the @{term threads}-set.+
−
*}+
−
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 subtree_tG_thread:+
−
  assumes "th \<in> threads s"+
−
  shows "subtree (tG s) th \<subseteq> threads s" (is "?L \<subseteq> ?R")+
−
proof -+
−
  from subtree_tRAG_thread[OF assms]+
−
  have "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" .+
−
  from this[unfolded subtree_tRAG_tG]+
−
  have " Th ` subtree (tG s) th \<subseteq> Th ` threads s" .+
−
  thus ?thesis by auto+
−
qed+
−
+
−
end+
−
+
−
section {* The formation of @{term RAG} *}+
−
+
−
text {*+
−
  The whole of PIP resides on the understanding of the formation+
−
  of @{term RAG}. We are going to show that @{term RAG}+
−
  forms a finite branching forest. The formalization is divided +
−
  into a series of subsections.+
−
*}+
−
+
−
subsection {* The change of @{term RAG} with each step of execution *}+
−
+
−
text {*+
−
  The very essence to prove that @{term RAG} has a certain property is to +
−
  show that this property is preserved as an invariant by the execution +
−
  of the system, and the basis for such kind of invariant proofs is to +
−
  show how @{term RAG} is changed with the execution of every execution step+
−
  (or event, or system operation). In this subsection,+
−
  the effect of every event on @{text RAG} is derived in its respective+
−
  locale named @{text "RAG_es"} with all lemmas before auxiliary. +
−
+
−
  These derived @{text "RAG_es"}s constitute the foundation +
−
  to show the various well-formed properties of @{term RAG},  +
−
  for example, @{term RAG} is finite, acyclic, and single-valued, etc.+
−
*}+
−
+
−
text {*+
−
  The following three lemmas show that @{text "RAG"} does not change+
−
  by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}+
−
  events, respectively.+
−
*}+
−
+
−
lemma (in valid_trace_set) RAG_es [simp]: "(RAG (e # s)) = RAG s"+
−
   by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)+
−
+
−
lemma (in valid_trace_create) RAG_es [simp]: "(RAG (e # s)) = RAG s"+
−
 by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)+
−
+
−
lemma (in valid_trace_exit) RAG_es[simp]: "(RAG (e # s)) = RAG s"+
−
  by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma holding_cs_eq_th:+
−
  assumes "holding s t cs"+
−
  shows "t = th"+
−
proof -+
−
  from pip_e[unfolded is_v]+
−
  show ?thesis+
−
  proof(cases)+
−
    case (thread_V)+
−
    from held_unique[OF this(2) assms]+
−
    show ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma distinct_wq': "distinct wq'"+
−
  by (metis (mono_tags, lifting) distinct_rest  some_eq_ex wq'_def)+
−
  +
−
lemma set_wq': "set wq' = set rest"+
−
  by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)+
−
    +
−
lemma th'_in_inv:+
−
  assumes "th' \<in> set wq'"+
−
  shows "th' \<in> set rest"+
−
  using assms set_wq' by simp+
−
+
−
lemma running_th_s:+
−
  shows "th \<in> running s"+
−
proof -+
−
  from pip_e[unfolded is_v]+
−
  show ?thesis by (cases, simp)+
−
qed+
−
+
−
lemma neq_t_th: +
−
  assumes "waiting (e#s) t c"+
−
  shows "t \<noteq> th"+
−
proof+
−
  assume otherwise: "t = th"+
−
  show False+
−
  proof(cases "c = cs")+
−
    case True+
−
    have "t \<in> set wq'" +
−
     using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs]+
−
     by simp +
−
    from th'_in_inv[OF this] have "t \<in> set rest" .+
−
    with wq_s_cs[folded otherwise] wq_distinct[of cs]+
−
    show ?thesis by simp+
−
  next+
−
    case False+
−
    have "wq (e#s) c = wq s c" using False+
−
        by simp+
−
    hence "waiting s t c" using assms+
−
        by (simp add: s_waiting_def wq_def) +
−
    hence "t \<notin> readys s" by (unfold readys_def, auto)+
−
    hence "t \<notin> running s" using running_ready by auto +
−
    with running_th_s[folded otherwise] show ?thesis by auto +
−
  qed+
−
qed+
−
+
−
lemma waiting_esI1:+
−
  assumes "waiting s t c"+
−
      and "c \<noteq> cs" +
−
  shows "waiting (e#s) t c" +
−
proof -+
−
  have "wq (e#s) c = wq s c" +
−
    using assms(2) by auto+
−
  with assms(1) show ?thesis+
−
    by (simp add: s_waiting_def wq_def) +
−
qed+
−
+
−
lemma holding_esI2:+
−
  assumes "c \<noteq> cs" +
−
  and "holding s t c"+
−
  shows "holding (e#s) t c"+
−
proof -+
−
  from assms(1) have "wq (e#s) c = wq s c"  by auto+
−
  from assms(2)[unfolded s_holding_def, folded wq_def, +
−
                folded this, folded s_holding_def]+
−
  show ?thesis .+
−
qed+
−
+
−
lemma holding_esI1:+
−
  assumes "holding s t c"+
−
  and "t \<noteq> th"+
−
  shows "holding (e#s) t c"+
−
proof -+
−
  have "c \<noteq> cs" using assms using holding_cs_eq_th by blast +
−
  from holding_esI2[OF this assms(1)]+
−
  show ?thesis .+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v_n+
−
begin+
−
+
−
lemma neq_wq': "wq' \<noteq> []" +
−
proof (unfold wq'_def, rule someI2)+
−
  show "distinct rest \<and> set rest = set rest"+
−
    by (simp add: distinct_rest) +
−
next+
−
  fix x+
−
  assume " distinct x \<and> set x = set rest" +
−
  thus "x \<noteq> []" using rest_nnl by auto+
−
qed +
−
+
−
lemma eq_wq': "wq' = taker # rest'"+
−
  by (simp add: neq_wq' rest'_def taker_def)+
−
+
−
lemma next_th_taker: +
−
  shows "next_th s th cs taker"+
−
  using rest_nnl taker_def wq'_def wq_s_cs +
−
  by (auto simp:next_th_def)+
−
+
−
lemma taker_unique: +
−
  assumes "next_th s th cs taker'"+
−
  shows "taker' = taker"+
−
proof -+
−
  from assms+
−
  obtain rest' where +
−
    h: "wq s cs = th # rest'" +
−
       "taker' = hd (SOME q. distinct q \<and> set q = set rest')"+
−
          by (unfold next_th_def, auto)+
−
  with wq_s_cs have "rest' = rest" by auto+
−
  thus ?thesis using h(2) taker_def wq'_def by auto +
−
qed+
−
+
−
lemma waiting_set_eq:+
−
  "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}"+
−
  by (smt all_not_in_conv bot.extremum insertI1 insert_subset +
−
      mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)+
−
+
−
lemma holding_set_eq:+
−
  "{(Cs cs, Th th') |th'.  next_th s th cs th'} = {(Cs cs, Th taker)}"+
−
  using next_th_taker taker_def waiting_set_eq +
−
  by fastforce+
−
   +
−
lemma holding_taker:+
−
  shows "holding (e#s) taker cs"+
−
    by (unfold s_holding_def, unfold wq_es_cs, +
−
        auto simp:neq_wq' taker_def)+
−
+
−
lemma waiting_esI2:+
−
  assumes "waiting s t cs"+
−
      and "t \<noteq> taker"+
−
  shows "waiting (e#s) t cs" +
−
proof -+
−
  have "t \<in> set wq'" +
−
  proof(unfold wq'_def, rule someI2)+
−
    show "distinct rest \<and> set rest = set rest"+
−
          by (simp add: distinct_rest)+
−
  next+
−
    fix x+
−
    assume "distinct x \<and> set x = set rest"+
−
    moreover have "t \<in> set rest"+
−
        using assms(1) s_waiting_def set_ConsD wq_def wq_s_cs by auto +
−
    ultimately show "t \<in> set x" by simp+
−
  qed+
−
  moreover have "t \<noteq> hd wq'"+
−
    using assms(2) taker_def by auto +
−
  ultimately show ?thesis+
−
    by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)+
−
qed+
−
+
−
lemma waiting_esE:+
−
  assumes "waiting (e#s) t c" +
−
  obtains "c \<noteq> cs" "waiting s t c"+
−
     |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"+
−
proof(cases "c = cs")+
−
  case False+
−
  hence "wq (e#s) c = wq s c" by auto+
−
  with assms have "waiting s t c"+
−
    by (simp add: s_waiting_def wq_def) +
−
  from that(1)[OF False this] show ?thesis .+
−
next+
−
  case True+
−
  from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]+
−
  have "t \<noteq> hd wq'" "t \<in> set wq'" by auto+
−
  hence "t \<noteq> taker" by (simp add: taker_def) +
−
  moreover hence "t \<noteq> th" using assms neq_t_th by blast +
−
  moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) +
−
  ultimately have "waiting s t cs"+
−
    by (metis list.sel(1) list.set_sel(2) list.simps(3) rest_def s_waiting_def wq_def wq_s_cs)+
−
  show ?thesis using that(2)+
−
  using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto   +
−
qed+
−
+
−
lemma holding_esI1:+
−
  assumes "c = cs"+
−
  and "t = taker"+
−
  shows "holding (e#s) t c"+
−
  by (unfold assms, simp add: holding_taker)+
−
+
−
lemma holding_esE:+
−
  assumes "holding (e#s) t c" +
−
  obtains "c = cs" "t = taker"+
−
      | "c \<noteq> cs" "holding s t c"+
−
proof(cases "c = cs")+
−
  case True+
−
  from assms[unfolded True, unfolded s_holding_def, +
−
             folded wq_def, unfolded wq_es_cs]+
−
  have "t = taker" by (simp add: taker_def) +
−
  from that(1)[OF True this] show ?thesis .+
−
next+
−
  case False+
−
  hence "wq (e#s) c = wq s c" by auto+
−
  from assms[unfolded s_holding_def, folded wq_def, +
−
             unfolded this, folded s_holding_def]+
−
  have "holding s t c"  .+
−
  from that(2)[OF False this] show ?thesis .+
−
qed+
−
+
−
end +
−
+
−
+
−
context valid_trace_v_e+
−
begin+
−
+
−
lemma nil_wq': "wq' = []" +
−
proof (unfold wq'_def, rule someI2)+
−
  show "distinct rest \<and> set rest = set rest"+
−
    by (simp add: distinct_rest) +
−
next+
−
  fix x+
−
  assume " distinct x \<and> set x = set rest" +
−
  thus "x = []" using rest_nil by auto+
−
qed +
−
+
−
lemma no_taker: +
−
  assumes "next_th s th cs taker"+
−
  shows "False"+
−
proof -+
−
  from assms[unfolded next_th_def]+
−
  obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []"+
−
    by auto+
−
  thus ?thesis using rest_def rest_nil by auto +
−
qed+
−
+
−
lemma waiting_set_eq:+
−
  "{(Th th', Cs cs) |th'. next_th s th cs th'} = {}"+
−
  using no_taker by auto+
−
+
−
lemma holding_set_eq:+
−
  "{(Cs cs, Th th') |th'.  next_th s th cs th'} = {}"+
−
  using no_taker by auto+
−
   +
−
lemma no_holding:+
−
  assumes "holding (e#s) taker cs"+
−
  shows False+
−
proof -+
−
  from wq_es_cs[unfolded nil_wq']+
−
  have " wq (e # s) cs = []" .+
−
  from assms[unfolded s_holding_def, folded wq_def, unfolded this]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma no_waiter_before: "\<not> waiting s t cs"+
−
proof+
−
  assume otherwise: "waiting s t cs"+
−
  from this[unfolded s_waiting_def, folded wq_def, +
−
            unfolded wq_s_cs rest_nil]+
−
  show False by simp+
−
qed+
−
+
−
lemma no_waiter_after:+
−
  assumes "waiting (e#s) t cs"+
−
  shows False+
−
proof -+
−
  from wq_es_cs[unfolded nil_wq']+
−
  have " wq (e # s) cs = []" .+
−
  from assms[unfolded s_waiting_def, folded wq_def, unfolded this]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma waiting_esI2:+
−
  assumes "waiting s t c"+
−
  shows "waiting (e # s) t c"+
−
proof -+
−
  have "c \<noteq> cs" using assms+
−
    using no_waiter_before by blast+
−
  from waiting_esI1[OF assms this]+
−
  show ?thesis .+
−
qed+
−
+
−
lemma waiting_esE:+
−
  assumes "waiting (e#s) t c" +
−
  obtains "c \<noteq> cs" "waiting s t c"+
−
proof(cases "c = cs")+
−
  case False+
−
  hence "wq (e#s) c = wq s c"  by auto+
−
  with assms have "waiting s t c"+
−
    by (simp add: s_waiting_def wq_def) +
−
  from that(1)[OF False this] show ?thesis .+
−
next+
−
  case True+
−
  from no_waiter_after[OF assms[unfolded True]]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma holding_esE:+
−
  assumes "holding (e#s) t c" +
−
  obtains "c \<noteq> cs" "holding s t c"+
−
proof(cases "c = cs")+
−
  case True+
−
  from no_holding[OF assms[unfolded True]] +
−
  show ?thesis by auto+
−
next+
−
  case False+
−
  hence "wq (e#s) c = wq s c" by auto+
−
  from assms[unfolded s_holding_def, folded wq_def, +
−
             unfolded this, folded s_holding_def]+
−
  have "holding s t c"  .+
−
  from that[OF False this] show ?thesis .+
−
qed+
−
+
−
end +
−
+
−
  +
−
context valid_trace_v+
−
begin+
−
+
−
lemma RAG_es:+
−
  "RAG (e # s) =+
−
   RAG s - {(Cs cs, Th th)} -+
−
     {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>+
−
     {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")+
−
proof(rule rel_eqI)+
−
  fix n1 n2+
−
  assume "(n1, n2) \<in> ?L"+
−
  thus "(n1, n2) \<in> ?R"+
−
  proof(cases rule:in_RAG_E)+
−
    case (waiting th' cs')+
−
    show ?thesis+
−
    proof(cases "rest = []")+
−
      case False+
−
      interpret h_n: valid_trace_v_n s e th cs+
−
        by (unfold_locales, insert False, simp)+
−
      from waiting(3)+
−
      show ?thesis+
−
      proof(cases rule:h_n.waiting_esE)+
−
        case 1+
−
        with waiting(1,2)+
−
        show ?thesis+
−
        by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, +
−
             fold s_waiting_abv, auto)+
−
      next+
−
        case 2+
−
        with waiting(1,2)+
−
        show ?thesis+
−
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, +
−
             fold s_waiting_abv, auto)+
−
      qed+
−
    next+
−
      case True+
−
      interpret h_e: valid_trace_v_e s e th cs+
−
        by (unfold_locales, insert True, simp)+
−
      from waiting(3)+
−
      show ?thesis+
−
      proof(cases rule:h_e.waiting_esE)+
−
        case 1+
−
        with waiting(1,2)+
−
        show ?thesis+
−
        by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, +
−
             fold s_waiting_abv, auto)+
−
      qed+
−
    qed+
−
  next+
−
    case (holding th' cs')+
−
    show ?thesis+
−
    proof(cases "rest = []")+
−
      case False+
−
      interpret h_n: valid_trace_v_n s e th cs+
−
        by (unfold_locales, insert False, simp)+
−
      from holding(3)+
−
      show ?thesis+
−
      proof(cases rule:h_n.holding_esE)+
−
        case 1+
−
        with holding(1,2)+
−
        show ?thesis+
−
        by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, +
−
             fold s_waiting_abv, auto)+
−
      next+
−
        case 2+
−
        with holding(1,2)+
−
        show ?thesis+
−
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, +
−
             fold s_holding_abv, auto)+
−
      qed+
−
    next+
−
      case True+
−
      interpret h_e: valid_trace_v_e s e th cs+
−
        by (unfold_locales, insert True, simp)+
−
      from holding(3)+
−
      show ?thesis+
−
      proof(cases rule:h_e.holding_esE)+
−
        case 1+
−
        with holding(1,2)+
−
        show ?thesis+
−
        by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, +
−
             fold s_holding_abv, auto)+
−
      qed+
−
    qed+
−
  qed+
−
next+
−
  fix n1 n2+
−
  assume h: "(n1, n2) \<in> ?R"+
−
  show "(n1, n2) \<in> ?L"+
−
  proof(cases "rest = []")+
−
    case False+
−
    interpret h_n: valid_trace_v_n s e th cs+
−
        by (unfold_locales, insert False, simp)+
−
    from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq]+
−
    have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th)+
−
                            \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or> +
−
          (n2 = Th h_n.taker \<and> n1 = Cs cs)" +
−
      by auto+
−
   thus ?thesis+
−
   proof+
−
      assume "n2 = Th h_n.taker \<and> n1 = Cs cs"+
−
      with h_n.holding_taker+
−
      show ?thesis +
−
        by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
   next+
−
    assume h: "(n1, n2) \<in> RAG s \<and>+
−
        (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"+
−
    hence "(n1, n2) \<in> RAG s" by simp+
−
    thus ?thesis+
−
    proof(cases rule:in_RAG_E)+
−
      case (waiting th' cs')+
−
      from h and this(1,2)+
−
      have "th' \<noteq> h_n.taker \<or> cs' \<noteq> cs" by auto+
−
      hence "waiting (e#s) th' cs'" +
−
      proof+
−
        assume "cs' \<noteq> cs"+
−
        from waiting_esI1[OF waiting(3) this] +
−
        show ?thesis .+
−
      next+
−
        assume neq_th': "th' \<noteq> h_n.taker"+
−
        show ?thesis+
−
        proof(cases "cs' = cs")+
−
          case False+
−
          from waiting_esI1[OF waiting(3) this] +
−
          show ?thesis .+
−
        next+
−
          case True+
−
          from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True]+
−
          show ?thesis .+
−
        qed+
−
      qed+
−
      thus ?thesis using waiting(1,2)+
−
        by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    next+
−
      case (holding th' cs')+
−
      from h this(1,2)+
−
      have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto+
−
      hence "holding (e#s) th' cs'"+
−
      proof+
−
        assume "cs' \<noteq> cs"+
−
        from holding_esI2[OF this holding(3)] +
−
        show ?thesis .+
−
      next+
−
        assume "th' \<noteq> th"+
−
        from holding_esI1[OF holding(3) this]+
−
        show ?thesis .+
−
      qed+
−
      thus ?thesis using holding(1,2)+
−
        by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    qed+
−
   qed+
−
 next+
−
   case True+
−
   interpret h_e: valid_trace_v_e s e th cs+
−
        by (unfold_locales, insert True, simp)+
−
   from h[unfolded h_e.waiting_set_eq h_e.holding_set_eq]+
−
   have h_s: "(n1, n2) \<in> RAG s" "(n1, n2) \<noteq> (Cs cs, Th th)" +
−
      by auto+
−
   from h_s(1)+
−
   show ?thesis+
−
   proof(cases rule:in_RAG_E)+
−
    case (waiting th' cs')+
−
    from h_e.waiting_esI2[OF this(3)]+
−
    show ?thesis using waiting(1,2)+
−
      by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
   next+
−
    case (holding th' cs')+
−
    with h_s(2)+
−
    have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto+
−
    thus ?thesis+
−
    proof+
−
      assume neq_cs: "cs' \<noteq> cs"+
−
      from holding_esI2[OF this holding(3)]+
−
      show ?thesis using holding(1,2)+
−
        by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    next+
−
      assume "th' \<noteq> th"+
−
      from holding_esI1[OF holding(3) this]+
−
      show ?thesis using holding(1,2)+
−
        by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    qed+
−
   qed+
−
 qed+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_p+
−
begin+
−
+
−
lemma waiting_kept:+
−
  assumes "waiting s th' cs'"+
−
  shows "waiting (e#s) th' cs'"+
−
  using assms+
−
    by (metis butlast_snoc distinct.simps(2) distinct_singleton hd_append2 +
−
        in_set_butlastD s_waiting_def wq_def wq_es_cs wq_neq_simp)+
−
+
−
lemma holding_kept:+
−
  assumes "holding s th' cs'"+
−
  shows "holding (e#s) th' cs'"+
−
proof(cases "cs' = cs")+
−
  case False+
−
  hence "wq (e#s) cs' = wq s cs'" by simp+
−
  with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto +
−
next+
−
  case True+
−
  from assms[unfolded s_holding_def, folded wq_def]+
−
  obtain rest where eq_wq: "wq s cs' = th'#rest"+
−
    by (metis empty_iff list.collapse list.set(1)) +
−
  hence "wq (e#s) cs' = th'#(rest@[th])"+
−
    by (simp add: True wq_es_cs) +
−
  thus ?thesis+
−
    by (simp add: holding_raw_def s_holding_abv) +
−
qed+
−
end +
−
+
−
lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"+
−
proof -+
−
  have "th \<in> readys s"+
−
    using running_ready running_th_s by blast +
−
  thus ?thesis+
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
context valid_trace_p_h+
−
begin+
−
+
−
lemma wq_es_cs': "wq (e#s) cs = [th]"+
−
  using wq_es_cs[unfolded we] by simp+
−
+
−
lemma holding_es_th_cs: +
−
  shows "holding (e#s) th cs"+
−
proof -+
−
  from wq_es_cs'+
−
  have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto+
−
  thus ?thesis unfolding holding_raw_def s_holding_abv by blast +
−
qed+
−
+
−
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"+
−
  by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto)+
−
+
−
lemma waiting_esE:+
−
  assumes "waiting (e#s) th' cs'"+
−
  obtains "waiting s th' cs'"+
−
  using assms+
−
  by (metis empty_iff list.sel(1) list.set(1) s_waiting_def +
−
      set_ConsD wq_def wq_es_cs' wq_neq_simp)+
−
  +
−
lemma holding_esE:+
−
  assumes "holding (e#s) th' cs'"+
−
  obtains "cs' \<noteq> cs" "holding s th' cs'"+
−
    | "cs' = cs" "th' = th"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  from held_unique[OF holding_es_th_cs assms[unfolded True]]+
−
  have "th' = th" by simp+
−
  from that(2)[OF True this] show ?thesis .+
−
next+
−
  case False+
−
  have "holding s th' cs'" using assms+
−
    using False unfolding holding_raw_def s_holding_abv by auto+
−
  from that(1)[OF False this] show ?thesis .+
−
qed+
−
+
−
lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R")+
−
proof(rule rel_eqI)+
−
  fix n1 n2+
−
  assume "(n1, n2) \<in> ?L"+
−
  thus "(n1, n2) \<in> ?R" +
−
  proof(cases rule:in_RAG_E)+
−
    case (waiting th' cs')+
−
    from this(3)+
−
    show ?thesis+
−
    proof(cases rule:waiting_esE)+
−
      case 1+
−
      thus ?thesis using waiting(1,2)+
−
        by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    qed+
−
  next+
−
    case (holding th' cs')+
−
    from this(3)+
−
    show ?thesis+
−
    proof(cases rule:holding_esE)+
−
      case 1+
−
      with holding(1,2)+
−
      show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    next+
−
      case 2+
−
      with holding(1,2) show ?thesis by auto+
−
    qed+
−
  qed+
−
next+
−
  fix n1 n2+
−
  assume "(n1, n2) \<in> ?R"+
−
  hence "(n1, n2) \<in> RAG s \<or> (n1 = Cs cs \<and> n2 = Th th)" by auto+
−
  thus "(n1, n2) \<in> ?L"+
−
  proof+
−
    assume "(n1, n2) \<in> RAG s"+
−
    thus ?thesis+
−
    proof(cases rule:in_RAG_E)+
−
      case (waiting th' cs')+
−
      from waiting_kept[OF this(3)]+
−
      show ?thesis using waiting(1,2)+
−
         by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    next+
−
      case (holding th' cs')+
−
      from holding_kept[OF this(3)]+
−
      show ?thesis using holding(1,2)+
−
         by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    qed+
−
  next+
−
    assume "n1 = Cs cs \<and> n2 = Th th"+
−
    with holding_es_th_cs+
−
    show ?thesis +
−
      by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
  qed+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_p_w+
−
begin+
−
+
−
lemma wq_s_cs: "wq s cs = holder#waiters"+
−
    by (simp add: holder_def waiters_def wne)+
−
    +
−
lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"+
−
  by (simp add: wq_es_cs wq_s_cs)+
−
+
−
lemma waiting_es_th_cs: "waiting (e#s) th cs"+
−
  using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs+
−
  using Un_iff list.sel(1) list.set_intros(1) s_waiting_def+
−
   set_append wq_def wq_es_cs by auto+
−
+
−
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"+
−
   by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto)+
−
+
−
lemma holding_esE:+
−
  assumes "holding (e#s) th' cs'"+
−
  obtains "holding s th' cs'"+
−
  using assms +
−
proof(cases "cs' = cs")+
−
  case False+
−
  hence "wq (e#s) cs' = wq s cs'" by simp+
−
  with assms show ?thesis using that+
−
    using s_holding_def wq_def by auto+
−
next+
−
  case True+
−
  with assms show ?thesis+
−
    using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto+
−
qed+
−
+
−
lemma waiting_esE:+
−
  assumes "waiting (e#s) th' cs'"+
−
  obtains "th' \<noteq> th" "waiting s th' cs'"+
−
     |  "th' = th" "cs' = cs"+
−
proof(cases "waiting s th' cs'")+
−
  case True+
−
  have "th' \<noteq> th"+
−
  proof+
−
    assume otherwise: "th' = th"+
−
    from True[unfolded this]+
−
    show False by (simp add: th_not_waiting)+
−
  qed+
−
  from that(1)[OF this True] show ?thesis .+
−
next+
−
  case False+
−
  hence "th' = th \<and> cs' = cs"+
−
      by (metis assms hd_append2 insert_iff list.simps(15) rotate1.simps(2) +
−
          s_waiting_def set_rotate1 wne wq_def wq_es_cs wq_neq_simp)+
−
  with that(2) show ?thesis by metis+
−
qed+
−
+
−
lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")+
−
proof(rule rel_eqI)+
−
  fix n1 n2+
−
  assume "(n1, n2) \<in> ?L"+
−
  thus "(n1, n2) \<in> ?R" +
−
  proof(cases rule:in_RAG_E)+
−
    case (waiting th' cs')+
−
    from this(3)+
−
    show ?thesis+
−
    proof(cases rule:waiting_esE)+
−
      case 1+
−
      thus ?thesis using waiting(1,2)+
−
        by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    next+
−
      case 2+
−
      thus ?thesis using waiting(1,2) by auto+
−
    qed+
−
  next+
−
    case (holding th' cs')+
−
    from this(3)+
−
    show ?thesis+
−
    proof(cases rule:holding_esE)+
−
      case 1+
−
      with holding(1,2)+
−
      show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    qed+
−
  qed+
−
next+
−
  fix n1 n2+
−
  assume "(n1, n2) \<in> ?R"+
−
  hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto+
−
  thus "(n1, n2) \<in> ?L"+
−
  proof+
−
    assume "(n1, n2) \<in> RAG s"+
−
    thus ?thesis+
−
    proof(cases rule:in_RAG_E)+
−
      case (waiting th' cs')+
−
      from waiting_kept[OF this(3)]+
−
      show ?thesis using waiting(1,2)+
−
         by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    next+
−
      case (holding th' cs')+
−
      from holding_kept[OF this(3)]+
−
      show ?thesis using holding(1,2)+
−
         by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    qed+
−
  next+
−
    assume "n1 = Th th \<and> n2 = Cs cs"+
−
    thus ?thesis using RAG_edge by auto+
−
  qed+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_p+
−
begin+
−
+
−
lemma RAG_es: "RAG (e # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}+
−
                                                  else RAG s \<union> {(Th th, Cs cs)})"+
−
proof(cases "wq s cs = []")+
−
  case True+
−
  interpret vt_p: valid_trace_p_h using True+
−
    by (unfold_locales, simp)+
−
  show ?thesis by (simp add: vt_p.RAG_es vt_p.we) +
−
next+
−
  case False+
−
  interpret vt_p: valid_trace_p_w using False+
−
    by (unfold_locales, simp)+
−
  show ?thesis by (simp add: vt_p.RAG_es vt_p.wne) +
−
qed+
−
+
−
end+
−
+
−
subsection {* RAG is finite *}+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma +
−
  finite_RAG_kept:+
−
  assumes "finite (RAG s)"+
−
  shows "finite (RAG (e#s))"+
−
proof(cases "rest = []")+
−
  case True+
−
  interpret vt: valid_trace_v_e using True+
−
    by (unfold_locales, simp)+
−
  show ?thesis using assms+
−
    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)+
−
next+
−
  case False+
−
  interpret vt: valid_trace_v_n using False+
−
    by (unfold_locales, simp)+
−
  show ?thesis using assms+
−
    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma finite_RAG:+
−
  shows "finite (RAG s)"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  show ?case +
−
  by (auto simp: s_RAG_def waiting_raw_def+
−
                   holding_raw_def wq_def acyclic_def)+
−
next+
−
  case (Cons s e)+
−
  interpret vt_e: valid_trace_e s e using Cons by simp+
−
  show ?case+
−
  proof(cases e)+
−
    case (Create th prio)+
−
    interpret vt: valid_trace_create s e th prio using Create+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp+
−
  next+
−
    case (Exit th)+
−
    interpret vt: valid_trace_exit s e th using Exit+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp+
−
  next+
−
    case (P th cs)+
−
    interpret vt: valid_trace_p s e th cs using P+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons using vt.RAG_es by auto +
−
  next+
−
    case (V th cs)+
−
    interpret vt: valid_trace_v s e th cs using V+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt.finite_RAG_kept) +
−
  next+
−
    case (Set th prio)+
−
    interpret vt: valid_trace_set s e th prio using Set+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp+
−
  qed+
−
qed+
−
+
−
lemma finite_tRAG: "finite (tRAG s)"+
−
proof -+
−
  from finite_RAG[unfolded RAG_split]+
−
  have "finite (wRAG s)" "finite (hRAG s)" by auto+
−
  from finite_relcomp[OF this] tRAG_def+
−
  show ?thesis by simp+
−
qed+
−
+
−
find_theorems inj finite "_ ` _"+
−
+
−
find_theorems tG tRAG+
−
+
−
thm tRAG_def_tG+
−
+
−
find_theorems "finite (?f ` ?A)" "finite ?A"+
−
+
−
lemma finite_tG: "finite (tG s)"+
−
proof(rule finite_imageD)+
−
  from finite_tRAG[unfolded tRAG_def_tG]+
−
  show "finite (map_prod Th Th ` tG s)" .+
−
next+
−
  show "inj_on (map_prod Th Th) (tG s)"+
−
    using inj_on_def by fastforce+
−
qed+
−
+
−
end+
−
+
−
subsection {* Uniqueness of waiting *}+
−
+
−
text {*+
−
  {\em Uniqueness of waiting} means that +
−
  a thread can only be blocked on one resource.+
−
  This property is needed in order to prove that @{term RAG}+
−
  is acyclic. Therefore, we need to prove it first in the following+
−
  lemma @{text "waiting_unqiue"}, all lemmas before it are auxiliary. +
−
+
−
  The property is expressed by the following predicate over system +
−
  state (or event trace), which is also named @{text "waiting_unqiue"}.+
−
*}+
−
+
−
definition +
−
  "waiting_unique (ss::state) = +
−
     (\<forall> th cs1 cs2. waiting ss th cs1 \<longrightarrow> +
−
                    waiting ss th cs2 \<longrightarrow> cs1 = cs2)"+
−
+
−
text {*+
−
  We are going to show (in the +
−
  lemma named @{text waiting_unique}) that+
−
  this property holds on any valid trace (or system state).+
−
*}+
−
+
−
text {*+
−
  As a first step to prove lemma @{text "waiting_unqiue"}, +
−
  we need to understand how +
−
  a thread is get blocked. +
−
  We show in the following lemmas +
−
  (all named @{text "waiting_inv"}) that +
−
  @{term P}-operation is the only cause. +
−
*}+
−
+
−
context valid_trace_create+
−
begin+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
  using assms +
−
  by (unfold s_waiting_def, fold wq_def, simp)+
−
end+
−
+
−
context valid_trace_set+
−
begin+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
  using assms +
−
  by (unfold s_waiting_def, fold wq_def, simp)+
−
end+
−
+
−
context valid_trace_exit+
−
begin+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
  using assms +
−
  by (unfold s_waiting_def, fold wq_def, simp)+
−
end+
−
+
−
context valid_trace_p+
−
begin+
−
+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  moreover have "th' = th"+
−
  proof(rule ccontr)+
−
    assume otherwise: "th' \<noteq> th"+
−
    have "waiting s th' cs'"+
−
    proof -+
−
      from assms(2)[unfolded True s_waiting_def, +
−
              folded wq_def, unfolded wq_es_cs]+
−
      have h: "th' \<in> set (wq s cs @ [th])"+
−
              "th' \<noteq> hd (wq s cs @ [th])" by auto+
−
      from h(1) and otherwise+
−
      have "th' \<in> set (wq s cs)" by auto+
−
      hence "wq s cs \<noteq> []" by auto+
−
      hence "hd (wq s cs @ [th]) = hd (wq s cs)" by auto+
−
      with h otherwise+
−
      have "waiting s th' cs" +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
      from this[folded True] show ?thesis .+
−
    qed+
−
    with assms(1) show False by simp+
−
  qed+
−
  ultimately show ?thesis using is_p by simp+
−
next+
−
  case False+
−
  hence "wq (e#s) cs' = wq s cs'" by simp+
−
  from assms[unfolded s_waiting_def, folded wq_def, +
−
            unfolded this]+
−
  show ?thesis by simp+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v_n+
−
begin+
−
+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
proof -+
−
  from assms(2)+
−
  show ?thesis+
−
  by (cases rule:waiting_esE, insert assms, auto)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v_e+
−
begin+
−
+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th' cs'"+
−
  and "waiting (e#s) th' cs'"+
−
  shows "e = P th' cs'"+
−
proof -+
−
  from assms(2)+
−
  show ?thesis+
−
  by (cases rule:waiting_esE, insert assms, auto)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_e+
−
begin+
−
+
−
lemma waiting_inv:+
−
  assumes "\<not> waiting s th cs"+
−
  and "waiting (e#s) th cs"+
−
  shows "e = P th cs"+
−
proof(cases e)+
−
  case (Create th' prio')+
−
  then interpret vt: valid_trace_create s e th' prio'+
−
    by (unfold_locales, simp)+
−
  show ?thesis using vt.waiting_inv[OF assms] by simp+
−
next+
−
  case (Exit th')+
−
  then interpret vt: valid_trace_exit s e th'+
−
    by (unfold_locales, simp)+
−
  show ?thesis using vt.waiting_inv[OF assms] by simp+
−
next+
−
  case (Set th' prio')+
−
  then interpret vt: valid_trace_set s e th' prio'+
−
    by (unfold_locales, simp)+
−
  show ?thesis using vt.waiting_inv[OF assms] by simp+
−
next+
−
  case (P th' cs')+
−
  then interpret vt: valid_trace_p s e th' cs'+
−
    by (unfold_locales, simp)+
−
  show ?thesis using vt.waiting_inv[OF assms] by simp+
−
next+
−
  case (V th' cs')+
−
  then interpret vt_e: valid_trace_v s e th' cs'+
−
    by (unfold_locales, simp)+
−
  show ?thesis+
−
  proof(cases "vt_e.rest = []")+
−
    case True+
−
    then interpret vt: valid_trace_v_e s e th' cs'+
−
      by (unfold_locales, simp)+
−
    show ?thesis using vt.waiting_inv[OF assms] by simp+
−
  next+
−
    case False+
−
    then interpret vt: valid_trace_v_n s e th' cs'+
−
      by (unfold_locales, simp)+
−
    show ?thesis using vt.waiting_inv[OF assms] by simp+
−
  qed+
−
qed+
−
+
−
text {* +
−
  Now, with @{thm waiting_inv} in place, the following lemma+
−
  shows the uniqueness of waiting is kept by every operation +
−
  in the PIP protocol. This lemma constitutes the main part+
−
  in the proof of lemma @{text "waiting_unique"}.+
−
*}+
−
+
−
lemma waiting_unique_kept:+
−
  assumes "waiting_unique s"+
−
  shows "waiting_unique (e#s)"+
−
proof -+
−
  note h = assms[unfolded waiting_unique_def, rule_format]+
−
  { fix th cs1 cs2+
−
    assume w1: "waiting (e#s) th cs1"+
−
       and w2: "waiting (e#s) th cs2"+
−
    have "cs1 = cs2"+
−
    proof(rule ccontr)+
−
      assume otherwise: "cs1 \<noteq> cs2"+
−
      show False+
−
      proof(cases "waiting s th cs1")+
−
        case True+
−
        from h[OF this] and otherwise+
−
        have "\<not> waiting s th cs2" by auto+
−
        from waiting_inv[OF this w2]+
−
        have "e = P th cs2" .+
−
        then interpret vt: valid_trace_p  s e th cs2+
−
          by (unfold_locales, simp)+
−
        from vt.th_not_waiting and True+
−
        show ?thesis by simp+
−
      next+
−
        case False +
−
        from waiting_inv[OF this w1]+
−
        have "e = P th cs1" .+
−
        then interpret vt: valid_trace_p s e th cs1+
−
          by (unfold_locales, simp)+
−
        have "wq (e # s) cs2 = wq s cs2" +
−
          using otherwise by simp+
−
        from w2[unfolded s_waiting_def, folded wq_def, +
−
                  unfolded this]+
−
        have "waiting s th cs2" +
−
          by (unfold s_waiting_def, fold wq_def, simp)+
−
        thus ?thesis by (simp add: vt.th_not_waiting) +
−
      qed+
−
    qed+
−
  } thus ?thesis by (unfold waiting_unique_def, auto)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  With @{thm valid_trace_e.waiting_unique_kept} in place,+
−
  the proof of the following lemma @{text "waiting_unique"} +
−
  needs only a very simple induction.+
−
*}+
−
+
−
lemma waiting_unique +
−
  [unfolded waiting_unique_def, rule_format]:+
−
  shows "waiting_unique s"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  show ?case +
−
    by (unfold waiting_unique_def s_waiting_def, simp)+
−
next+
−
  case (Cons s e)+
−
  then interpret vt: valid_trace_e s e by simp+
−
  show ?case using Cons(2) vt.waiting_unique_kept+
−
    by simp+
−
qed+
−
+
−
end+
−
+
−
+
−
subsection {* Acyclic keeping *}+
−
+
−
text {*+
−
  To prove that @{term RAG} is acyclic, we need to show the acyclic property +
−
  is preserved by all system operations. There are only two non-trivial cases, +
−
  the @{term P} and @{term V} operation, where are treated in the following+
−
  locales, under the name @{text "acylic_RAG_kept"}:+
−
*}+
−
+
−
context valid_trace_v_e+
−
begin +
−
+
−
lemma +
−
  acylic_RAG_kept:+
−
  assumes "acyclic (RAG s)"+
−
  shows "acyclic (RAG (e#s))"+
−
proof(rule acyclic_subset[OF assms])+
−
  show "RAG (e # s) \<subseteq> RAG s"+
−
      by (unfold RAG_es waiting_set_eq holding_set_eq, auto)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v_n+
−
begin +
−
+
−
lemma waiting_taker: "waiting s taker cs"+
−
  apply (unfold s_waiting_def, fold wq_def, unfold wq_s_cs taker_def)+
−
  using eq_wq' set_wq' th_not_in_rest by auto+
−
+
−
lemma +
−
  acylic_RAG_kept:+
−
  assumes "acyclic (RAG s)"+
−
  shows "acyclic (RAG (e#s))"+
−
proof -+
−
  have "acyclic ((RAG s - {(Cs cs, Th th)} - {(Th taker, Cs cs)}) \<union> +
−
                 {(Cs cs, Th taker)})" (is "acyclic (?A \<union> _)")+
−
  proof -+
−
    from assms+
−
    have "acyclic ?A"+
−
       by (rule acyclic_subset, auto)+
−
    moreover have "(Th taker, Cs cs) \<notin> ?A^*"+
−
    proof+
−
      assume otherwise: "(Th taker, Cs cs) \<in> ?A^*"+
−
      hence "(Th taker, Cs cs) \<in> ?A^+"+
−
        by (unfold rtrancl_eq_or_trancl, auto)+
−
      from tranclD[OF this]+
−
      obtain cs' where h: "(Th taker, Cs cs') \<in> ?A" +
−
                          "(Th taker, Cs cs') \<in> RAG s"+
−
        by (unfold s_RAG_def, auto)+
−
      from this(2) have "waiting s taker cs'" +
−
        by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
      from waiting_unique[OF this waiting_taker] +
−
      have "cs' = cs" .+
−
      from h(1)[unfolded this] show False by auto+
−
    qed+
−
    ultimately show ?thesis by auto+
−
  qed+
−
  thus ?thesis +
−
    by (unfold RAG_es waiting_set_eq holding_set_eq, simp)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_p_h+
−
begin+
−
+
−
lemma +
−
  acylic_RAG_kept:+
−
  assumes "acyclic (RAG s)"+
−
  shows "acyclic (RAG (e#s))"+
−
proof -+
−
  have "acyclic (RAG s \<union> {(Cs cs, Th th)})" (is "acyclic (?A \<union> _)") +
−
  proof -+
−
    from assms+
−
    have "acyclic ?A"+
−
       by (rule acyclic_subset, auto)+
−
    moreover have "(Th th, Cs cs) \<notin> ?A^*"+
−
    proof+
−
      assume otherwise: "(Th th, Cs cs) \<in> ?A^*"+
−
      hence "(Th th, Cs cs) \<in> ?A^+"+
−
        by (unfold rtrancl_eq_or_trancl, auto)+
−
      from tranclD[OF this]+
−
      obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"+
−
        by (unfold s_RAG_def, auto)+
−
      hence "waiting s th cs'" +
−
        by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
      with th_not_waiting show False by auto +
−
    qed+
−
    ultimately show ?thesis by auto+
−
  qed+
−
  thus ?thesis by (unfold RAG_es, simp)+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_p_w+
−
begin+
−
+
−
lemma +
−
  acylic_RAG_kept:+
−
  assumes "acyclic (RAG s)"+
−
  shows "acyclic (RAG (e#s))"+
−
proof -+
−
  have "acyclic (RAG s \<union> {(Th th, Cs cs)})" (is "acyclic (?A \<union> _)") +
−
  proof -+
−
    from assms+
−
    have "acyclic ?A"+
−
       by (rule acyclic_subset, auto)+
−
    moreover have "(Cs cs, Th th) \<notin> ?A^*"+
−
    proof+
−
      assume otherwise: "(Cs cs, Th th) \<in> ?A^*"+
−
      from pip_e[unfolded is_p]+
−
      show False+
−
      proof(cases)+
−
        case (thread_P)+
−
        moreover from otherwise have "(Cs cs, Th th) \<in> ?A^+"+
−
            by (unfold rtrancl_eq_or_trancl, auto)+
−
        ultimately show ?thesis by auto+
−
      qed+
−
    qed+
−
    ultimately show ?thesis by auto+
−
  qed+
−
  thus ?thesis by (unfold RAG_es, simp)+
−
qed+
−
+
−
end+
−
+
−
+
−
subsection {* RAG is acyclic *}+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {* +
−
  With these @{text "acylic_RAG_kept"}-lemmas proved, +
−
  the proof of the following @{text "acyclic_RAG"} is+
−
  straight forward. +
−
 *}+
−
+
−
lemma acyclic_RAG:+
−
  shows "acyclic (RAG s)"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  show ?case +
−
  by (auto simp: s_RAG_def waiting_raw_def+
−
                   holding_raw_def wq_def acyclic_def)+
−
next+
−
  case (Cons s e)+
−
  interpret vt_e: valid_trace_e s e using Cons by simp+
−
  show ?case+
−
  proof(cases e)+
−
    case (Create th prio)+
−
    interpret vt: valid_trace_create s e th prio using Create+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp +
−
  next+
−
    case (Exit th)+
−
    interpret vt: valid_trace_exit s e th using Exit+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp+
−
  next+
−
    case (P th cs)+
−
    interpret vt: valid_trace_p s e th cs using P+
−
      by (unfold_locales, simp)+
−
    show ?thesis+
−
    proof(cases "wq s cs = []")+
−
      case True+
−
      then interpret vt_h: valid_trace_p_h s e th cs+
−
        by (unfold_locales, simp)+
−
      show ?thesis using Cons by (simp add: vt_h.acylic_RAG_kept) +
−
    next+
−
      case False+
−
      then interpret vt_w: valid_trace_p_w s e th cs+
−
        by (unfold_locales, simp)+
−
      show ?thesis using Cons by (simp add: vt_w.acylic_RAG_kept) +
−
    qed+
−
  next+
−
    case (V th cs)+
−
    interpret vt: valid_trace_v s e th cs using V+
−
      by (unfold_locales, simp)+
−
    show ?thesis+
−
    proof(cases "vt.rest = []")+
−
      case True+
−
      then interpret vt_e: valid_trace_v_e s e th cs+
−
        by (unfold_locales, simp)+
−
      show ?thesis by (simp add: Cons.hyps(2) vt_e.acylic_RAG_kept) +
−
    next+
−
      case False+
−
      then interpret vt_n: valid_trace_v_n s e th cs+
−
        by (unfold_locales, simp)+
−
      show ?thesis by (simp add: Cons.hyps(2) vt_n.acylic_RAG_kept) +
−
    qed+
−
  next+
−
    case (Set th prio)+
−
    interpret vt: valid_trace_set s e th prio using Set+
−
      by (unfold_locales, simp)+
−
    show ?thesis using Cons by simp +
−
  qed+
−
qed+
−
+
−
end+
−
+
−
subsection {* RAG is single-valued *}+
−
+
−
text {*+
−
  The proof that @{term RAG} is single-valued makes use of +
−
  @{text "unique_waiting"} and @{thm held_unique} and the+
−
  proof itself is very simple:+
−
*}+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"+
−
  apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv)+
−
  by(auto elim:waiting_unique held_unique)+
−
+
−
lemma sgv_RAG: "single_valued (RAG s)"+
−
  using unique_RAG by (auto simp:single_valued_def)+
−
+
−
end+
−
+
−
subsection {* RAG is well-founded *}+
−
+
−
text {*+
−
  In this section, it is proved that both @{term RAG} and +
−
  its converse @{term "(RAG s)^-1"} are well-founded.+
−
  The proof is very simple with the help of+
−
  already proved fact that @{term RAG} is finite.+
−
*}+
−
+
−
context valid_trace+
−
begin+
−
+
−
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 wf_RAG_converse: +
−
  shows "wf ((RAG s)^-1)"+
−
proof(rule finite_acyclic_wf_converse)+
−
  from finite_RAG +
−
  show "finite (RAG s)" .+
−
next+
−
  from acyclic_RAG+
−
  show "acyclic (RAG s)" .+
−
qed+
−
+
−
end+
−
+
−
subsection {* RAG forms a finite-branching forest (or tree) *}+
−
+
−
text {*+
−
  With all the well-formedness proofs about @{term RAG} in place, +
−
  it is easy to show.+
−
*}+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma forest_RAG: "forest (RAG s)"+
−
  using sgv_RAG acyclic_RAG+
−
  by (unfold forest_def, auto)+
−
+
−
end+
−
+
−
sublocale valid_trace < forest_RAG?: forest "RAG s"+
−
  using forest_RAG .+
−
+
−
sublocale valid_trace < fsbtRAGs?: fforest "RAG s"+
−
proof+
−
  show "\<And>x. finite (children (RAG s) x)"+
−
    by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) +
−
    (*by (rule finite_fbranchI[OF finite_RAG])*)+
−
next+
−
  show "wf (RAG s)" using wf_RAG .+
−
qed+
−
+
−
subsection {* Derived properties for sub-graphs of RAG *}+
−
+
−
context valid_trace+
−
begin+
−
+
−
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 rel_map_alt_def: "rel_map f R = map_prod f f ` R"+
−
  by (unfold rel_map_def pairself_def map_prod_def, auto)+
−
+
−
lemma acyclic_tG: "acyclic (tG s)"+
−
proof -+
−
  have "acyclic (rel_map the_thread (tRAG s))"+
−
  proof(rule rel_map_acyclic [OF acyclic_tRAG])+
−
    show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))"+
−
      by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto)+
−
  qed+
−
  thus ?thesis+
−
  by (unfold tG_def_tRAG, fold rel_map_alt_def, simp) +
−
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 held_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 sgv_tG: "single_valued (tG s)"+
−
proof -+
−
  { fix x y z+
−
    assume h: "(x, y) \<in> tG s" "(x, z) \<in> tG s"+
−
    from tG_tRAG[OF h(1)] tG_tRAG[OF h(2)]+
−
    have "(Th x, Th y) \<in> tRAG s" "(Th x, Th z) \<in> tRAG s" by auto+
−
    from sgv_tRAG[unfolded single_valued_def, rule_format, OF this]+
−
    have "y = z" by simp+
−
  } thus ?thesis by (unfold single_valued_def, auto)+
−
qed+
−
+
−
end+
−
+
−
+
−
+
−
text {*+
−
  It can be shown that @{term tRAG} is also a +
−
  finite-branch relational tree (or forest):  +
−
*}+
−
+
−
sublocale valid_trace < forest_s?: forest "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 < forest_s_tG?: forest "tG s"+
−
proof(unfold_locales)+
−
  from sgv_tG show "single_valued (tG s)" .+
−
next+
−
  from acyclic_tG show "acyclic (tG s)" .+
−
qed+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma wf_tRAG: "wf (tRAG s)"+
−
proof(rule wf_subset)+
−
      show "wf (RAG s O RAG s)" using wf_RAG+
−
        by (fold wf_comp_self, simp)+
−
next+
−
      show "tRAG s \<subseteq> (RAG s O RAG s)"+
−
        by (unfold tRAG_alt_def, auto)+
−
qed+
−
+
−
lemma wf_tG: "wf (tG s)"+
−
proof(rule finite_acyclic_wf)+
−
  from finite_tG show "finite (tG s)" .+
−
next+
−
  from acyclic_tG show "acyclic (tG s)" .+
−
qed+
−
+
−
lemma finite_children_tRAG: "finite (children (tRAG s) x)"+
−
  proof(unfold tRAG_def, rule fbranch_compose1[rule_format])+
−
    fix x show "finite (children (wRAG s) x)" +
−
    proof(rule finite_fbranchI1[rule_format])+
−
      show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto+
−
    qed+
−
  next+
−
    fix x+
−
    show "finite (children (hRAG s) x)"+
−
    proof(rule finite_fbranchI1[rule_format])+
−
      show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto+
−
    qed+
−
  qed+
−
+
−
lemma children_map_prod: +
−
  assumes "inj f"+
−
  shows " children (map_prod f f ` r) (f x) = f ` (children r x)" (is "?L = ?R")+
−
proof -+
−
  { fix e+
−
    assume "e \<in> ?L"+
−
    then obtain e' x' where h: "e = f e'" "f x' = f x" "(e', x') \<in> r"+
−
      by (auto simp:children_def)+
−
    with assms[unfolded inj_on_def, rule_format]+
−
    have eq_x': "x' = x" by auto+
−
    with h+
−
    have "e \<in> ?R" by  (unfold children_def, auto)+
−
  } moreover {+
−
    fix e+
−
    assume "e \<in> ?R"+
−
    hence "e \<in> ?L" by (auto simp:children_def)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma finite_children_tG: "finite (children (tG s) x)"+
−
proof -+
−
  have "(children (tRAG s) (Th x)) = Th ` children (tG s) x"+
−
    by (unfold tRAG_def_tG, subst children_map_prod, auto simp:inj_on_def)+
−
  from finite_children_tRAG[of "Th x", unfolded this]+
−
  have "finite (Th ` children (tG s) x)" .+
−
  from finite_imageD[OF this]+
−
  show ?thesis by (auto simp:inj_on_def)+
−
qed+
−
+
−
end+
−
+
−
sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"+
−
proof+
−
  fix x+
−
  show "finite (children (tRAG s) x)"+
−
  proof(unfold tRAG_def, rule fbranch_compose1[rule_format])+
−
    fix x show "finite (children (wRAG s) x)" +
−
    proof(rule finite_fbranchI1[rule_format])+
−
      show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto+
−
    qed+
−
  next+
−
    fix x+
−
    show "finite (children (hRAG s) x)"+
−
    proof(rule finite_fbranchI1[rule_format])+
−
      show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto+
−
    qed+
−
  qed+
−
next+
−
  show "wf (tRAG s)"+
−
  proof(rule wf_subset)+
−
      show "wf (RAG s O RAG s)" using wf_RAG+
−
        by (fold wf_comp_self, simp)+
−
  next+
−
      show "tRAG s \<subseteq> (RAG s O RAG s)"+
−
        by (unfold tRAG_alt_def, auto)+
−
  qed+
−
qed+
−
+
−
sublocale valid_trace < fsbttGs?: fforest "tG s"+
−
proof+
−
  fix x+
−
  show "finite (children (tG s) x)" +
−
    by (simp add:finite_children_tG)+
−
next+
−
  show "wf (tG s)" by (simp add:wf_tG)+
−
qed+
−
+
−
section {* Chain to readys *}+
−
+
−
text {*+
−
  In this section, based on the just derived+
−
  properties about the shape of @{term RAG}, +
−
  a more complete view of the relationship +
−
  between threads is established.+
−
*}+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {* The first lemma is technical, which says out of any node in the+
−
domain of @{term RAG} (no matter whether it is thread node or resource+
−
node), there is a path leading to a ready thread.+
−
*}+
−
+
−
lemma chain_building:+
−
  assumes "node \<in> Domain (RAG s)"+
−
  obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"+
−
proof -+
−
  from assms have "node \<in> Range ((RAG s)^-1)" by auto+
−
  from wf_base[OF wf_RAG_converse this]+
−
  obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto+
−
  obtain th' where eq_b: "b = Th th'"+
−
  proof(cases b)+
−
    case (Cs cs)+
−
    from h_b(1)[unfolded trancl_converse] +
−
    have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto+
−
    from tranclE[OF this]+
−
    obtain n where "(n, b) \<in> RAG s" by auto+
−
    from this[unfolded Cs]+
−
    obtain th1 where "waiting s th1 cs"+
−
      by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    from waiting_holding[OF this]+
−
    obtain th2 where "holding s th2 cs" .+
−
    hence "(Cs cs, Th th2) \<in> RAG s"+
−
      by (unfold s_RAG_def, fold s_holding_abv, auto)+
−
    with h_b(2)[unfolded Cs, rule_format]+
−
    have False by auto+
−
    thus ?thesis by auto+
−
  qed auto+
−
  have "th' \<in> readys s" +
−
  proof -+
−
    from h_b(2)[unfolded eq_b]+
−
    have "\<forall>cs. \<not> waiting s th' cs"+
−
      by (unfold s_RAG_def, fold s_waiting_abv, auto)+
−
    moreover have "th' \<in> threads s"+
−
    proof(rule rg_RAG_threads)+
−
      from tranclD[OF h_b(1), unfolded eq_b]+
−
      obtain z where "(z, Th th') \<in> (RAG s)" by auto+
−
      thus "Th th' \<in> Range (RAG s)" by auto+
−
    qed+
−
    ultimately show ?thesis by (auto simp:readys_def)+
−
  qed+
−
  moreover have "(node, Th th') \<in> (RAG s)^+" +
−
    using h_b(1)[unfolded trancl_converse] eq_b by auto+
−
  ultimately show ?thesis using that by metis+
−
qed+
−
+
−
text {* \noindent+
−
  The following lemma says for any living thread, +
−
  either it is ready or there is a path in @{term RAG}+
−
  leading from it to a ready thread. The lemma is proved easily+
−
  by instantiating @{thm "chain_building"}.+
−
*}                    +
−
lemma th_chain_to_ready:+
−
  assumes th_in: "th \<in> threads s"+
−
  shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"+
−
proof(cases "th \<in> readys s")+
−
  case True+
−
  thus ?thesis by auto+
−
next+
−
  case False+
−
  from False and th_in have "Th th \<in> Domain (RAG s)" +
−
    by (auto simp: readys_def s_waiting_def s_RAG_def wq_def waiting_raw_def+
−
 Domain_def)+
−
  from chain_building [rule_format, OF this]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma th_chain_to_ready_tG:+
−
  assumes th_in: "th \<in> threads s"+
−
  shows "\<exists>th'\<in> nancestors (tG s) th. th' \<in> readys s"+
−
proof -+
−
  from th_chain_to_ready[OF assms]+
−
  show ?thesis+
−
  proof+
−
    assume "th \<in> readys s"+
−
    thus ?thesis by (unfold nancestors_def, auto)+
−
  next+
−
    assume "\<exists>th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)\<^sup>+"+
−
    then obtain th' where h: "th' \<in> readys s" "(Th th, Th th') \<in> (RAG s)\<^sup>+" by auto+
−
    from h(2) tRAG_trancl_eq+
−
    have "(Th th, Th th') \<in> (tRAG s)^+" by auto+
−
    hence "(th, th') \<in> (tG s)^+"+
−
      by (metis the_thread.simps trancl_tRAG_tG)+
−
    with h(1)+
−
    show ?thesis+
−
      using ancestors_def mem_Collect_eq nancestors2 by fastforce+
−
  qed+
−
qed+
−
+
−
+
−
text {*+
−
  The following lemma is a technical one to show +
−
  that the set of threads in the subtree of any thread+
−
  is finite.+
−
*}+
−
lemma finite_subtree_threads:+
−
    "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A")+
−
proof -+
−
  have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"+
−
        by (auto, insert image_iff, fastforce)+
−
  moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"+
−
        (is "finite ?B")+
−
  proof -+
−
     have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}"+
−
      by auto+
−
     moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto+
−
     moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) +
−
     ultimately show ?thesis by auto+
−
  qed+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
(* ccc *)+
−
+
−
lemma readys_no_tRAG_chain:+
−
  assumes "th1 \<in> readys s"+
−
  and "th2 \<in> readys s"+
−
  and "th1 \<noteq> th2"+
−
  shows "(Th th1, Th th2) \<notin> (tRAG s)^*"+
−
proof+
−
  assume "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*"+
−
  from rtranclD[OF this]+
−
  show False+
−
  proof+
−
    assume "Th th1 = Th th2" with assms show ?thesis by simp+
−
  next+
−
    assume "Th th1 \<noteq> Th th2 \<and> (Th th1, Th th2) \<in> (tRAG s)\<^sup>+"+
−
    hence "(Th th1, Th th2) \<in> (tRAG s)\<^sup>+" by auto+
−
    from tranclD[OF this] obtain cs where "(Th th1, Cs cs) \<in> RAG s"+
−
      by (unfold tRAG_alt_def, auto)+
−
    from in_RAG_E[OF this] have "th1 \<notin> readys s" by (unfold readys_def, auto)+
−
    with assms show ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma root_readys:+
−
  assumes "th \<in> readys s"+
−
  shows "root (tRAG s) (Th th)"+
−
proof -+
−
  { assume "\<not> root (tRAG s) (Th th)"+
−
    then obtain n' where "(Th th, n') \<in> (tRAG s)^+"+
−
      unfolding root_def ancestors_def by auto+
−
    then obtain cs where "(Th th, Cs cs) \<in> RAG s"+
−
      unfolding tRAG_alt_def using tranclD by fastforce +
−
    then have "th \<notin> readys s" +
−
      unfolding readys_def using in_RAG_E by blast +
−
    with assms have False by simp+
−
  } then show "root (tRAG s) (Th th)" by auto+
−
qed+
−
+
−
lemma root_readys_tG:+
−
  assumes "th \<in> readys s"+
−
  shows "root (tG s) th"+
−
proof -+
−
  { assume "\<not> root (tG s) th"+
−
    then obtain th' where "(th, th') \<in> (tG s)^+"+
−
      unfolding root_def ancestors_def by auto+
−
    then have "(Th th, Th th') \<in> (tRAG s)^+" +
−
      using trancl_tG_tRAG by simp+
−
    with root_readys assms +
−
    have False +
−
      unfolding root_def ancestors_def by auto+
−
  } then show "root (tG s) th" by auto+
−
qed  +
−
+
−
lemma readys_indep:+
−
  assumes "th1 \<in> readys s"+
−
  and "th2 \<in> readys s"+
−
  and "th1 \<noteq> th2"+
−
  shows "indep (tRAG s) (Th th1) (Th th2)"+
−
  using assms readys_no_tRAG_chain+
−
  unfolding indep_def by blast+
−
+
−
lemma readys_indep_tG:+
−
  assumes "th1 \<in> readys s"+
−
  and "th2 \<in> readys s"+
−
  and "th1 \<noteq> th2"+
−
  shows "indep (tG s) th1 th2"+
−
  using assms+
−
  unfolding indep_def+
−
  using readys_no_tRAG_chain rtrancl_tG_tRAG by blast+
−
+
−
text {*+
−
  The following lemma @{text "thread_chain"} holds on any living thread, +
−
  not necessarily a running one. +
−
*}+
−
lemma thread_chain:+
−
  assumes "th \<in> threads s"+
−
  obtains th' where "th' \<in> subtree (tG s) th" "th' \<in> threads s"+
−
                    "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"+
−
proof -+
−
  have "Max (the_preced s ` subtree (tG s) th) \<in> the_preced s ` subtree (tG s) th"+
−
  proof(rule Max_in)+
−
    show "finite (the_preced s ` subtree (tG s) th)" +
−
        by (simp add: fsbttGs.finite_subtree)+
−
  next+
−
    show "the_preced s ` subtree (tG s) th \<noteq> {}" using subtree_def by fastforce +
−
  qed+
−
  then obtain th' where +
−
       h: "th' \<in> subtree (tG s) th"+
−
                    "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"+
−
  by auto+
−
  moreover have "th' \<in> threads s"+
−
  proof -+
−
    from assms have "th \<in> threads s" .+
−
    from subtree_tG_thread[OF this] and h +
−
    show ?thesis by auto+
−
  qed+
−
  ultimately show ?thesis using that by auto+
−
qed+
−
+
−
text {*+
−
  The following two lemmas shows there is at most one running thread +
−
  in the system.+
−
*}+
−
+
−
+
−
lemma running_unique:+
−
  assumes running_1: "th1 \<in> running s"+
−
  and running_2: "th2 \<in> running s"+
−
  shows "th1 = th2"+
−
proof -+
−
  -- {* +
−
+
−
  According to lemma @{thm thread_chain}, each live thread is chained to a+
−
  thread in its subtree, who holds the highest precedence of the subtree.+
−
+
−
  The chains for @{term th1} and @{term th2} are established first in the+
−
  following in @{text "chain1"} and @{text "chain2"}. These chains start+
−
  with the threads @{text "th1'"} and @{text "th2'"} respectively. *}+
−
  +
−
  have "th1 \<in> threads s" using assms+
−
    by (unfold running_def readys_def, auto)+
−
  with thread_chain+
−
  obtain th1' where +
−
      chain1: "th1' \<in> subtree (tG s) th1" +
−
          "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"+
−
          "th1' \<in> threads s"+
−
      by auto+
−
  have "th2 \<in> threads s" using assms+
−
    by (unfold running_def readys_def, auto)+
−
  with thread_chain+
−
  obtain th2' where +
−
      chain2: "th2' \<in> subtree (tG s) th2" +
−
          "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"+
−
          "th2' \<in> threads s"+
−
      by auto+
−
  -- {* From these two chains we can be prove that the threads +
−
        @{term th1} and @{term th2} must be equal. For this we first+
−
        show that the starting points of the chains are equal.+
−
     *}+
−
  have eq_th': "th1' = th2'"+
−
  proof -+
−
    -- {* from @{text th1} and @{text th2} running, we know their +
−
          cp-value is the same *}+
−
    from running_1 and running_2 have "cp s th1 = cp s th2"+
−
      unfolding running_def by auto+
−
    -- {* that means the preced of @{text th1'} and @{text th2'} +
−
          must be the same *}+
−
    then +
−
    have eq_max: "Max (the_preced s ` subtree (tG s) th1) = +
−
                  Max (the_preced s ` subtree (tG s) th2)" +
−
      unfolding cp_alt_def2 .+
−
    with chain1(2) chain2(2)+
−
    have "the_preced s th1' = the_preced s th2'" by simp+
−
    -- {* since the precedences are the same, we can conclude+
−
          that  @{text th1'} and @{text th2'} are the same *}+
−
    with preced_unique chain1(3) chain2(3)+
−
    show "th1' = th2'" unfolding the_preced_def by auto+
−
  qed+
−
  moreover+
−
  have "root (tG s) th1" "root (tG s) th2" using assms+
−
    using assms root_readys_tG+
−
    unfolding running_def by auto+
−
  ultimately show "th1 = th2" using root_unique chain1(1) chain2(1)+
−
     by fastforce+
−
qed+
−
+
−
lemma card_running: +
−
  shows "card (running s) \<le> 1"+
−
proof(cases "running s = {}")+
−
  case True+
−
  thus ?thesis by auto+
−
next+
−
  case False+
−
  then obtain th where "th \<in> running s" by auto+
−
  with running_unique+
−
  have "running s = {th}" by auto+
−
  thus ?thesis by auto+
−
qed+
−
+
−
text {*+
−
  The following two lemmas show that the set of living threads+
−
  in the system can be partitioned into subtrees of those +
−
  threads in the @{term readys} set. The first lemma+
−
  @{text threads_alt_def} shows the union of +
−
  these subtrees equals to the set of living threads+
−
  and the second lemma @{text "readys_subtree_disjoint"} shows +
−
  subtrees of different threads in @{term readys}-set+
−
  are disjoint.+
−
*}+
−
+
−
lemma subtree_RAG_tG: +
−
  shows "subtree (tG s) th = {th'. Th th' \<in> subtree (RAG s) (Th th)}"+
−
  using subtree_tG_tRAG threads_set_eq by auto+
−
+
−
+
−
lemma threads_alt_def:+
−
  "threads s = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"+
−
    (is "?L = ?R")+
−
proof -+
−
  { fix th1+
−
    assume "th1 \<in> ?L"+
−
    from th_chain_to_ready[OF this]+
−
    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .+
−
    hence "th1 \<in> ?R" by (auto simp:subtree_def)+
−
  } moreover +
−
  { fix th'+
−
    assume "th' \<in> ?R"+
−
    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"+
−
      by auto+
−
    from this(2)+
−
    have "th' \<in> ?L" +
−
    proof(cases rule:subtreeE)+
−
      case 1+
−
      with h(1) show ?thesis by (auto simp:readys_def)+
−
    next+
−
      case 2+
−
      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]+
−
      have "Th th' \<in> Domain (RAG s)" by auto+
−
      from dm_RAG_threads[OF this]+
−
      show ?thesis .+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma threads_alt_def1:+
−
  shows "(threads s) = (\<Union> th \<in> readys s. subtree (tG s) th)"+
−
unfolding threads_alt_def subtree_RAG_tG  ..+
−
+
−
lemma readys_subtree_disjoint:+
−
  assumes "th1 \<in> readys s"+
−
  and "th2 \<in> readys s"+
−
  and "th1 \<noteq> th2"+
−
  shows "subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2) = {}"+
−
proof -+
−
  { fix n+
−
    assume "n \<in> subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2)"+
−
    hence "(n, Th th1) \<in> (RAG s)^*" "(n, Th th2) \<in> (RAG s)^*"+
−
      by (auto simp:subtree_def)+
−
    from star_rpath[OF this(1)] star_rpath[OF this(2)]+
−
    obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)"+
−
                         "rpath (RAG s) n xs2 (Th th2)" by metis+
−
    hence False+
−
    proof(cases rule:forest_RAG.rpath_overlap')+
−
      case (less_1 xs3)+
−
      from rpath_star[OF this(3)]+
−
      have "Th th1 \<in> subtree (RAG s) (Th th2)"+
−
        by (auto simp:subtree_def)+
−
      thus ?thesis+
−
      proof(cases rule:subtreeE)+
−
        case 1+
−
        with assms(3) show ?thesis by auto+
−
      next+
−
        case 2+
−
        hence "(Th th1, Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)+
−
        from tranclD[OF this]+
−
        obtain z where "(Th th1, z) \<in> RAG s" by auto+
−
        from this[unfolded s_RAG_def, folded wq_def]+
−
        obtain cs' where "waiting s th1 cs'"+
−
          by (auto simp:s_waiting_abv)+
−
        with assms(1) show False by (auto simp:readys_def)+
−
      qed+
−
    next+
−
      case (less_2 xs3)+
−
      from rpath_star[OF this(3)]+
−
      have "Th th2 \<in> subtree (RAG s) (Th th1)"+
−
        by (auto simp:subtree_def)+
−
      thus ?thesis+
−
      proof(cases rule:subtreeE)+
−
        case 1+
−
        with assms(3) show ?thesis by auto+
−
      next+
−
        case 2+
−
        hence "(Th th2, Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)+
−
        from tranclD[OF this]+
−
        obtain z where "(Th th2, z) \<in> RAG s" by auto+
−
        from this[unfolded s_RAG_def, folded wq_def]+
−
        obtain cs' where "waiting s th2 cs'"+
−
          by (auto simp:s_waiting_abv)+
−
        with assms(2) show False by (auto simp:readys_def)+
−
      qed+
−
    qed+
−
  } thus ?thesis by auto+
−
qed+
−
+
−
end+
−
+
−
section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}+
−
+
−
text {*+
−
 @{term cp} of a thread is defined to be the maximum of +
−
 the @{term preced}-values (precedences) of all threads in +
−
 its subtree given by @{term RAG}. Therefore, there exits +
−
 a relationship between @{term cp} and @{term preced} (and +
−
 also its variation @{term "the_preced"}) to be explored, +
−
 and this is the target of this section.+
−
*}+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  Since @{term cp} is the maximum of all @{term preced}s in its subtree, +
−
  which includes itself, it is not difficult to show+
−
  that the one thread's precedence is less or equal to its+
−
  @{text cp}-value:+
−
*}+
−
+
−
lemma le_cp:+
−
  shows "preced th s \<le> cp s th"+
−
  proof(unfold cp_alt_def, rule Max_ge)+
−
    show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"+
−
      by (simp add: finite_subtree_threads)+
−
  next+
−
    show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"+
−
      by (simp add: subtree_def the_preced_def)   +
−
  qed+
−
+
−
text {*+
−
  Since @{term cp} is the maximum precedence of its subtree,+
−
  and the subtree is only a subset of the set of all threads,+
−
  it can be shown that @{text cp} is less or equal to the maximum of+
−
  all threads:+
−
*}+
−
+
−
lemma cp_le:+
−
  assumes th_in: "th \<in> threads s"+
−
  shows "cp s th \<le> Max (the_preced s ` threads s)"+
−
proof(unfold cp_alt_def, rule Max_f_mono)+
−
  show "finite (threads s)" by (simp add: finite_threads) +
−
next+
−
  show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}"+
−
    using subtree_def by fastforce+
−
next+
−
  show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s"+
−
    using assms+
−
    by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq +
−
        node.inject(1) rtranclD subsetI subtree_def trancl_domain) +
−
qed+
−
+
−
text {*+
−
  Since the @{term cp}-value of each individual thread is less or equal to the +
−
  maximum precedence value of all threads (shown in lemma @{thm cp_le}),+
−
  it is easy to derive further that maximum @{term "cp"}-value of+
−
  all threads is also less or equal to the latter.+
−
+
−
  On the other hand, since the precedence value of each individual +
−
  thread is less of equal to its own @{term cp}-value (shown in lemma @{thm le_cp}),+
−
  it is easy to show that the maximum of the former is less or equal to the +
−
  maximum of the latter. +
−
+
−
  By combining these two perspectives, we get the following equality +
−
  between the two maximums:+
−
*}+
−
+
−
lemma max_cp_eq: +
−
  shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"+
−
  (is "?L = ?R")+
−
proof -+
−
  have "?L \<le> ?R" +
−
  proof(cases "threads s = {}")+
−
    case False+
−
    show ?thesis +
−
      by (rule Max.boundedI, +
−
          insert cp_le, +
−
          auto simp:finite_threads False)+
−
  qed auto+
−
  moreover have "?R \<le> ?L"+
−
    by (rule Max_fg_mono, +
−
        simp add: finite_threads,+
−
        simp add: le_cp the_preced_def)+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
text {* (* ddd *) \noindent+
−
  According to @{thm threads_alt_def} and @{thm readys_subtree_disjoint} , +
−
  the set of @{term threads} can be partitioned into subtrees of the +
−
  threads in @{term readys}, and also because  @{term cp}-value of a thread is +
−
  the maximum precedence of its own subtree, by applying +
−
  the absorbing property of @{term Max} (lemma @{thm Max_UNION}) +
−
  over the union of subtrees, the following equation can be derived:+
−
*}+
−
+
−
lemma cp_alt_def3:+
−
  shows "cp s th = Max (preceds (subtree (tG s) th) s)"+
−
unfolding cp_alt_def2+
−
unfolding image_def+
−
unfolding the_preced_def+
−
by meson+
−
+
−
lemma KK:+
−
  shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})"+
−
by (simp_all add: Setcompr_eq_image)+
−
+
−
lemma Max_Segments: +
−
  assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" +
−
  shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}"+
−
using assms+
−
apply(subst KK(1))+
−
apply(subst Max_Union)+
−
apply(auto)[3]+
−
apply(simp add: Setcompr_eq_image)+
−
apply(auto simp add: image_image)+
−
done +
−
+
−
lemma max_cp_readys_max_preced_tG:+
−
  shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R")+
−
proof(cases "readys s = {}")+
−
  case False+
−
  have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)"+
−
    unfolding threads_alt_def1 by simp+
−
  also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"+
−
    apply(subst Max_Segments[symmetric])+
−
    apply (simp add: finite_readys)+
−
    apply (simp add: fsbttGs.finite_subtree)+
−
    apply blast+
−
    using False apply blast+
−
    apply(rule arg_cong)+
−
    back+
−
    apply(blast)+
−
    done +
−
  also have "... = Max {cp s th | th. th \<in> readys s}"+
−
    unfolding cp_alt_def3 ..+
−
  finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"+
−
   by (simp add: Setcompr_eq_image image_def) +
−
qed (auto simp:threads_alt_def)+
−
+
−
+
−
lemma LL:+
−
shows "the_preced s ` threads s = preceds (threads s) s"+
−
using the_preced_def by auto+
−
+
−
+
−
text {*+
−
  The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}+
−
  and @{thm max_cp_eq}:+
−
*}+
−
lemma max_cp_readys_threads:+
−
  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" +
−
    apply(simp add: max_cp_readys_max_preced_tG)+
−
    apply(simp add: max_cp_eq)+
−
    apply(simp add: LL)+
−
    done+
−
+
−
end+
−
+
−
+
−
section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}+
−
+
−
text {*+
−
  As explained in the section where @{term "cntP"},+
−
  @{term "cntV"} and @{term "cntCS"} are defined, +
−
  we need to establish a equation (in lemma @{text "cnp_cnv_cncs"}) +
−
  so that the last can be calculated out of the first two. +
−
+
−
  While the calculation of @{term "cntV"} and @{term "cntCS"}+
−
  are relatively simple, the calculation of @{term "cntCS"} and +
−
  @{term "pvD"} are complicated, because their definitions+
−
  involve a number of other functions such as @{term holdents}, @{term readys}, +
−
  and @{term threads}. To prove  @{text "cnp_cnv_cncs"}, +
−
  we need to investigate how the values of these functions+
−
  are changed with the execution of each kind of system operation.+
−
  Following conventions, such investigation are divided into +
−
  locales corresponding to system operations.+
−
*}+
−
+
−
context valid_trace_p_w+
−
begin+
−
+
−
lemma holding_s_holder: "holding s holder cs"+
−
  by (unfold s_holding_def, unfold wq_s_cs, auto)+
−
+
−
lemma holding_es_holder: "holding (e#s) holder cs"+
−
  by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto)+
−
+
−
lemma holdents_es:+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") +
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L"+
−
    hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def)+
−
    have "holding s th' cs'"+
−
    proof(cases "cs' = cs")+
−
      case True+
−
      from held_unique[OF h[unfolded True] holding_es_holder]+
−
      have "th' = holder" .+
−
      thus ?thesis +
−
        by (unfold True holdents_def, insert holding_s_holder, simp)+
−
    next+
−
      case False+
−
      hence "wq (e#s) cs' = wq s cs'" by simp+
−
      from h[unfolded s_holding_def, folded wq_def, unfolded this]+
−
      show ?thesis+
−
       by (unfold s_holding_def, auto)+
−
    qed +
−
    hence "cs' \<in> ?R" by (auto simp:holdents_def)+
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence h: "holding s th' cs'" by (auto simp:holdents_def)+
−
    have "holding (e#s) th' cs'"+
−
    proof(cases "cs' = cs")+
−
      case True+
−
      from held_unique[OF h[unfolded True] holding_s_holder]+
−
      have "th' = holder" .+
−
      thus ?thesis +
−
        by (unfold True holdents_def, insert holding_es_holder, simp)+
−
    next+
−
      case False+
−
      hence "wq s cs' = wq (e#s) cs'" by simp+
−
      from h[unfolded s_holding_def, folded wq_def, unfolded this]+
−
      show ?thesis+
−
       by (unfold s_holding_def, auto)+
−
    qed +
−
    hence "cs' \<in> ?L" by (auto simp:holdents_def)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'"+
−
 by (unfold cntCS_def holdents_es, simp)+
−
+
−
lemma th_not_ready_es: +
−
  shows "th \<notin> readys (e#s)"+
−
  using waiting_es_th_cs +
−
  by (unfold readys_def, auto)+
−
+
−
end+
−
  +
−
lemma (in valid_trace) finite_holdents: "finite (holdents s th)"+
−
  by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto)+
−
+
−
context valid_trace_p +
−
begin+
−
+
−
lemma live_th_es: "th \<in> threads (e#s)"+
−
  using live_th_s +
−
  by (unfold is_p, simp)+
−
+
−
lemma waiting_neq_th: +
−
  assumes "waiting s t c"+
−
  shows "t \<noteq> th"+
−
  using assms using th_not_waiting by blast +
−
+
−
end+
−
+
−
context valid_trace_p_h+
−
begin+
−
+
−
lemma th_not_waiting':+
−
  "\<not> waiting (e#s) th cs'"+
−
proof(cases "cs' = cs")+
−
  case True+
−
  show ?thesis+
−
    by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto)+
−
next+
−
  case False+
−
  from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def]+
−
  show ?thesis+
−
    by (unfold s_waiting_def, fold wq_def, insert False, simp)+
−
qed+
−
+
−
lemma ready_th_es: +
−
  shows "th \<in> readys (e#s)"+
−
  using th_not_waiting'+
−
  by (unfold readys_def, insert live_th_es, auto)+
−
+
−
lemma holdents_es_th:+
−
  "holdents (e#s) th = (holdents s th) \<union> {cs}" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L" +
−
    hence "holding (e#s) th cs'"+
−
      by (unfold holdents_def, auto)+
−
    hence "cs' \<in> ?R"+
−
     by (cases rule:holding_esE, auto simp:holdents_def)+
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence "holding s th cs' \<or> cs' = cs" +
−
      by (auto simp:holdents_def)+
−
    hence "cs' \<in> ?L"+
−
    proof+
−
      assume "holding s th cs'"+
−
      from holding_kept[OF this]+
−
      show ?thesis by (auto simp:holdents_def)+
−
    next+
−
      assume "cs' = cs"+
−
      thus ?thesis using holding_es_th_cs+
−
        by (unfold holdents_def, auto)+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma not_holding_s_th_cs: "\<not> holding s th cs"+
−
proof+
−
  assume otherwise: "holding s th cs"+
−
  from pip_e[unfolded is_p]+
−
  show False+
−
  proof(cases)+
−
    case (thread_P)+
−
    moreover have "(Cs cs, Th th) \<in> RAG s"+
−
      using otherwise th_not_in_wq+
−
      using s_holding_def wq_def by auto+
−
    ultimately show ?thesis by auto+
−
  qed+
−
qed+
−
+
−
lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1"+
−
proof -+
−
  have "card (holdents s th \<union> {cs}) = card (holdents s th) + 1"+
−
  proof(subst card_Un_disjoint)+
−
    show "holdents s th \<inter> {cs} = {}"+
−
      using not_holding_s_th_cs by (auto simp:holdents_def)+
−
  qed (auto simp:finite_holdents)+
−
  thus ?thesis+
−
   by (unfold cntCS_def holdents_es_th, simp)+
−
qed+
−
+
−
lemma no_holder: +
−
  "\<not> holding s th' cs"+
−
proof+
−
  assume otherwise: "holding s th' cs"+
−
  from this[unfolded s_holding_def, folded wq_def, unfolded we]+
−
  show False by auto+
−
qed+
−
+
−
lemma holdents_es_th':+
−
  assumes "th' \<noteq> th"+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L"+
−
    hence h_e: "holding (e#s) th' cs'" by (auto simp:holdents_def)+
−
    have "cs' \<noteq> cs"+
−
    proof+
−
      assume "cs' = cs"+
−
      from held_unique[OF h_e[unfolded this] holding_es_th_cs]+
−
      have "th' = th" .+
−
      with assms show False by simp+
−
    qed+
−
    from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]+
−
    have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .+
−
    hence "cs' \<in> ?R" +
−
      by (unfold holdents_def s_holding_def, auto)+
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence "holding s th' cs'" by (auto simp:holdents_def)+
−
    from holding_kept[OF this]+
−
    have "holding (e # s) th' cs'" .+
−
    hence "cs' \<in> ?L"+
−
      by (unfold holdents_def, auto)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_es_th'[simp]: +
−
  assumes "th' \<noteq> th"+
−
  shows "cntCS (e#s) th' = cntCS s th'"+
−
  by (unfold cntCS_def holdents_es_th'[OF assms], simp)+
−
+
−
end+
−
+
−
context valid_trace_p+
−
begin+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
        using assms(2)[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      show ?thesis+
−
      proof(cases "wq s cs = []")+
−
        case True+
−
        then interpret vt: valid_trace_p_h+
−
          by (unfold_locales, simp)+
−
        show ?thesis using n_wait wait waiting_kept by auto +
−
      next+
−
        case False+
−
        then interpret vt: valid_trace_p_w by (unfold_locales, simp)+
−
        show ?thesis using n_wait wait waiting_kept by blast +
−
      qed+
−
    qed+
−
  } with assms(2) show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'" +
−
        using assms(2)[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      show ?thesis+
−
      proof(cases "wq s cs = []")+
−
        case True+
−
        then interpret vt: valid_trace_p_h+
−
          by (unfold_locales, simp)+
−
        show ?thesis using n_wait vt.waiting_esE wait by blast +
−
      next+
−
        case False+
−
        then interpret vt: valid_trace_p_w by (unfold_locales, simp)+
−
        show ?thesis using assms(1) n_wait vt.waiting_esE wait by auto +
−
      qed+
−
    qed+
−
  } with assms(2) show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1[OF assms] readys_kept2[OF assms]+
−
  by metis+
−
+
−
lemma cnp_cnv_cncs_kept: (* ddd *)+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof(cases "th' = th")+
−
  case True+
−
  note eq_th' = this+
−
  show ?thesis+
−
  proof(cases "wq s cs = []")+
−
    case True+
−
    then interpret vt: valid_trace_p_h by (unfold_locales, simp)+
−
    show ?thesis+
−
      using assms eq_th' is_p ready_th_s vt.cntCS_es_th vt.ready_th_es pvD_def by auto +
−
  next+
−
    case False+
−
    then interpret vt: valid_trace_p_w by (unfold_locales, simp)+
−
    show ?thesis+
−
      using add.commute add.left_commute assms eq_th' is_p live_th_s +
−
            ready_th_s vt.th_not_ready_es pvD_def+
−
      apply (auto)+
−
      by (fold is_p, simp)+
−
  qed+
−
next+
−
  case False+
−
  note h_False = False+
−
  thus ?thesis+
−
  proof(cases "wq s cs = []")+
−
    case True+
−
    then interpret vt: valid_trace_p_h by (unfold_locales, simp)+
−
    show ?thesis using assms+
−
      by (insert True h_False pvD_def, auto split:if_splits,unfold is_p, auto)+
−
  next+
−
    case False+
−
    then interpret vt: valid_trace_p_w by (unfold_locales, simp)+
−
    show ?thesis using assms+
−
      by (insert False h_False pvD_def, auto split:if_splits,unfold is_p, auto)+
−
  qed+
−
qed+
−
+
−
end+
−
+
−
+
−
context valid_trace_v +
−
begin+
−
+
−
lemma holding_th_cs_s: +
−
  "holding s th cs" +
−
 by  (unfold s_holding_def, unfold wq_s_cs, auto)+
−
+
−
lemma th_ready_s [simp]: "th \<in> readys s"+
−
  using running_th_s+
−
  by (unfold running_def readys_def, auto)+
−
+
−
lemma th_live_s [simp]: "th \<in> threads s"+
−
  using th_ready_s by (unfold readys_def, auto)+
−
+
−
lemma th_ready_es [simp]: "th \<in> readys (e#s)"+
−
  using running_th_s neq_t_th+
−
  by (unfold is_v running_def readys_def, auto)+
−
+
−
lemma th_live_es [simp]: "th \<in> threads (e#s)"+
−
  using th_ready_es by (unfold readys_def, auto)+
−
+
−
lemma pvD_th_s[simp]: "pvD s th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma pvD_th_es[simp]: "pvD (e#s) th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma cntCS_s_th [simp]: "cntCS s th > 0"+
−
proof -+
−
  have "cs \<in> holdents s th" using holding_th_cs_s+
−
    by (unfold holdents_def, simp)+
−
  moreover have "finite (holdents s th)" using finite_holdents +
−
    by simp+
−
  ultimately show ?thesis+
−
    by (unfold cntCS_def, +
−
        auto intro!:card_gt_0_iff[symmetric, THEN iffD1])+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma th_not_waiting: +
−
  "\<not> waiting s th c"+
−
proof -+
−
  have "th \<in> readys s"+
−
    using running_ready running_th_s by blast +
−
  thus ?thesis+
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma waiting_neq_th: +
−
  assumes "waiting s t c"+
−
  shows "t \<noteq> th"+
−
  using assms using th_not_waiting by blast +
−
+
−
end+
−
+
−
context valid_trace_v_n+
−
begin+
−
+
−
lemma not_ready_taker_s[simp]: +
−
  "taker \<notin> readys s"+
−
  using waiting_taker+
−
  by (unfold readys_def, auto)+
−
+
−
lemma taker_live_s [simp]: "taker \<in> threads s"+
−
proof -+
−
  have "taker \<in> set wq'" by (simp add: eq_wq') +
−
  from th'_in_inv[OF this]+
−
  have "taker \<in> set rest" .+
−
  hence "taker \<in> set (wq s cs)" by (simp add: wq_s_cs) +
−
  thus ?thesis using wq_threads by auto +
−
qed+
−
+
−
lemma taker_live_es [simp]: "taker \<in> threads (e#s)"+
−
  using taker_live_s threads_es by blast+
−
+
−
lemma taker_ready_es [simp]:+
−
  shows "taker \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume "waiting (e#s) taker cs'"+
−
    hence False+
−
    proof(cases rule:waiting_esE)+
−
      case 1+
−
      thus ?thesis using waiting_taker waiting_unique by auto +
−
    qed simp+
−
  } thus ?thesis by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma neq_taker_th: "taker \<noteq> th"+
−
  using th_not_waiting waiting_taker by blast +
−
+
−
lemma not_holding_taker_s_cs:+
−
  shows "\<not> holding s taker cs"+
−
  using holding_cs_eq_th neq_taker_th by auto+
−
+
−
lemma holdents_es_taker:+
−
  "holdents (e#s) taker = holdents s taker \<union> {cs}" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L"+
−
    hence "holding (e#s) taker cs'" by (auto simp:holdents_def)+
−
    hence "cs' \<in> ?R"+
−
    proof(cases rule:holding_esE)+
−
      case 2+
−
      thus ?thesis by (auto simp:holdents_def)+
−
    qed auto+
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence "holding s taker cs' \<or> cs' = cs" by (auto simp:holdents_def)+
−
    hence "cs' \<in> ?L" +
−
    proof+
−
      assume "holding s taker cs'"+
−
      hence "holding (e#s) taker cs'" +
−
          using holding_esI2 holding_taker by fastforce +
−
      thus ?thesis by (auto simp:holdents_def)+
−
    next+
−
      assume "cs' = cs"+
−
      with holding_taker+
−
      show ?thesis by (auto simp:holdents_def)+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_es_taker [simp]: "cntCS (e#s) taker = cntCS s taker + 1"+
−
proof -+
−
  have "card (holdents s taker \<union> {cs}) = card (holdents s taker) + 1"+
−
  proof(subst card_Un_disjoint)+
−
    show "holdents s taker \<inter> {cs} = {}"+
−
      using not_holding_taker_s_cs by (auto simp:holdents_def)+
−
  qed (auto simp:finite_holdents)+
−
  thus ?thesis +
−
    by (unfold cntCS_def, insert holdents_es_taker, simp)+
−
qed+
−
+
−
lemma pvD_taker_s[simp]: "pvD s taker = 1"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma pvD_taker_es[simp]: "pvD (e#s) taker = 0"+
−
  by (unfold pvD_def, simp)  +
−
+
−
lemma pvD_th_s[simp]: "pvD s th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma pvD_th_es[simp]: "pvD (e#s) th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma holdents_es_th:+
−
  "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L"+
−
    hence "holding (e#s) th cs'" by (auto simp:holdents_def)+
−
    hence "cs' \<in> ?R"+
−
    proof(cases rule:holding_esE)+
−
      case 2+
−
      thus ?thesis by (auto simp:holdents_def)+
−
    qed (insert neq_taker_th, auto)+
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)+
−
    from holding_esI2[OF this]+
−
    have "cs' \<in> ?L" by (auto simp:holdents_def)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"+
−
proof -+
−
  have "card (holdents s th - {cs}) = card (holdents s th) - 1"+
−
  proof -+
−
    have "cs \<in> holdents s th" using holding_th_cs_s+
−
      by (auto simp:holdents_def)+
−
    moreover have "finite (holdents s th)"+
−
        by (simp add: finite_holdents) +
−
    ultimately show ?thesis by auto+
−
  qed+
−
  thus ?thesis by (unfold cntCS_def holdents_es_th)+
−
qed+
−
+
−
lemma holdents_kept:+
−
  assumes "th' \<noteq> taker"+
−
  and "th' \<noteq> th"+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume h: "cs' \<in> ?L"+
−
    have "cs' \<in> ?R"+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp+
−
      from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)+
−
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]+
−
      show ?thesis+
−
        by (unfold holdents_def s_holding_def, auto)+
−
    next+
−
      case True+
−
      from h[unfolded this]+
−
      have "holding (e#s) th' cs" by (auto simp:holdents_def)+
−
      from held_unique[OF this holding_taker]+
−
      have "th' = taker" .+
−
      with assms show ?thesis by auto+
−
    qed+
−
  } moreover {+
−
    fix cs'+
−
    assume h: "cs' \<in> ?R"+
−
    have "cs' \<in> ?L"+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp+
−
      from h have "holding s th' cs'" by (auto simp:holdents_def)+
−
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]+
−
      show ?thesis+
−
        by (unfold holdents_def s_holding_def, insert eq_wq, simp)+
−
    next+
−
      case True+
−
      from h[unfolded this]+
−
      have "holding s th' cs" by (auto simp:holdents_def)+
−
      from held_unique[OF this holding_th_cs_s]+
−
      have "th' = th" .+
−
      with assms show ?thesis by auto+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_kept [simp]:+
−
  assumes "th' \<noteq> taker"+
−
  and "th' \<noteq> th"+
−
  shows "cntCS (e#s) th' = cntCS s th'"+
−
  by (unfold cntCS_def holdents_kept[OF assms], simp)+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<noteq> taker"+
−
  and "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
        using assms(2)[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" +
−
        using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .+
−
      moreover have "\<not> (th' \<in> set rest \<and> th' \<noteq> hd (taker # rest'))" +
−
        using n_wait[unfolded True s_waiting_def, folded wq_def, +
−
                    unfolded wq_es_cs set_wq', unfolded eq_wq'] .+
−
      ultimately have "th' = taker" by auto+
−
      with assms(1)+
−
      show ?thesis by simp+
−
    qed+
−
  } with assms(2) show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<noteq> taker"+
−
  and "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'" +
−
        using assms(2)[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      have "th' \<in> set rest \<and> th' \<noteq> hd (taker # rest')"+
−
          using  wait [unfolded True s_waiting_def, folded wq_def, +
−
                    unfolded wq_es_cs set_wq', unfolded eq_wq']  .+
−
      moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest))"+
−
          using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .+
−
      ultimately have "th' = taker" using th_not_in_rest by simp+
−
      thm taker_def wq'_def+
−
      with assms(1)+
−
      show ?thesis by simp+
−
    qed+
−
  } with assms(2) show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  assumes "th' \<noteq> taker"+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1[OF assms] readys_kept2[OF assms]+
−
  by metis+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof -+
−
  { assume eq_th': "th' = taker"+
−
    have ?thesis+
−
      apply (unfold eq_th' pvD_taker_es cntCS_es_taker)+
−
      by (insert neq_taker_th assms[unfolded eq_th'], unfold is_v, simp)+
−
  } moreover {+
−
    assume eq_th': "th' = th"+
−
    have ?thesis +
−
      apply (unfold eq_th' pvD_th_es cntCS_es_th)+
−
      by (insert assms[unfolded eq_th'], unfold is_v, simp)+
−
  } moreover {+
−
    assume h: "th' \<noteq> taker" "th' \<noteq> th"+
−
    have ?thesis using assms+
−
      apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)+
−
      by (fold is_v, unfold pvD_def, simp)+
−
  } ultimately show ?thesis by metis+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v_e+
−
begin+
−
+
−
lemma holdents_es_th:+
−
  "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume "cs' \<in> ?L"+
−
    hence "holding (e#s) th cs'" by (auto simp:holdents_def)+
−
    hence "cs' \<in> ?R"+
−
    proof(cases rule:holding_esE)+
−
      case 1+
−
      thus ?thesis by (auto simp:holdents_def)+
−
    qed +
−
  } moreover {+
−
    fix cs'+
−
    assume "cs' \<in> ?R"+
−
    hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)+
−
    from holding_esI2[OF this]+
−
    have "cs' \<in> ?L" by (auto simp:holdents_def)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"+
−
proof -+
−
  have "card (holdents s th - {cs}) = card (holdents s th) - 1"+
−
  proof -+
−
    have "cs \<in> holdents s th" using holding_th_cs_s+
−
      by (auto simp:holdents_def)+
−
    moreover have "finite (holdents s th)"+
−
        by (simp add: finite_holdents) +
−
    ultimately show ?thesis by auto+
−
  qed+
−
  thus ?thesis by (unfold cntCS_def holdents_es_th)+
−
qed+
−
+
−
lemma holdents_kept:+
−
  assumes "th' \<noteq> th"+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume h: "cs' \<in> ?L"+
−
    have "cs' \<in> ?R"+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp+
−
      from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)+
−
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]+
−
      show ?thesis+
−
        by (unfold holdents_def s_holding_def, auto)+
−
    next+
−
      case True+
−
      from h[unfolded this]+
−
      have "holding (e#s) th' cs" by (auto simp:holdents_def)+
−
      from this[unfolded s_holding_def, folded wq_def, +
−
            unfolded wq_es_cs nil_wq']+
−
      show ?thesis by auto+
−
    qed+
−
  } moreover {+
−
    fix cs'+
−
    assume h: "cs' \<in> ?R"+
−
    have "cs' \<in> ?L"+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp+
−
      from h have "holding s th' cs'" by (auto simp:holdents_def)+
−
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]+
−
      show ?thesis+
−
        by (unfold holdents_def s_holding_def, insert eq_wq, simp)+
−
    next+
−
      case True+
−
      from h[unfolded this]+
−
      have "holding s th' cs" by (auto simp:holdents_def)+
−
      from held_unique[OF this holding_th_cs_s]+
−
      have "th' = th" .+
−
      with assms show ?thesis by auto+
−
    qed+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_kept [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "cntCS (e#s) th' = cntCS s th'"+
−
  by (unfold cntCS_def holdents_kept[OF assms], simp)+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
        using assms(1)[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" +
−
        using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . +
−
      hence "th' \<in> set rest" by auto+
−
      with set_wq' have "th' \<in> set wq'" by metis+
−
      with nil_wq' show ?thesis by simp+
−
    qed+
−
  } thus ?thesis using assms+
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'" +
−
        using assms[unfolded readys_def] by auto+
−
    have False+
−
    proof(cases "cs' = cs")+
−
      case False+
−
      with n_wait wait+
−
      show ?thesis +
−
        by (unfold s_waiting_def, fold wq_def, auto)+
−
    next+
−
      case True+
−
      have "th' \<in> set [] \<and> th' \<noteq> hd []"+
−
        using wait[unfolded True s_waiting_def, folded wq_def, +
−
              unfolded wq_es_cs nil_wq'] .+
−
      thus ?thesis by simp+
−
    qed+
−
  } with assms show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1 readys_kept2+
−
  by metis+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof -+
−
  {+
−
    assume eq_th': "th' = th"+
−
    have ?thesis +
−
      apply (unfold eq_th' pvD_th_es cntCS_es_th)+
−
      by (insert assms[unfolded eq_th'], unfold is_v, simp)+
−
  } moreover {+
−
    assume h: "th' \<noteq> th"+
−
    have ?thesis using assms+
−
      apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)+
−
      by (fold is_v, unfold pvD_def, simp)+
−
  } ultimately show ?thesis by metis+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_v+
−
begin+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof(cases "rest = []")+
−
  case True+
−
  then interpret vt: valid_trace_v_e by (unfold_locales, simp)+
−
  show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast +
−
next+
−
  case False+
−
  then interpret vt: valid_trace_v_n by (unfold_locales, simp)+
−
  show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast +
−
qed+
−
+
−
end+
−
+
−
context valid_trace_create+
−
begin+
−
+
−
lemma th_not_live_s [simp]: "th \<notin> threads s"+
−
proof -+
−
  from pip_e[unfolded is_create]+
−
  show ?thesis by (cases, simp)+
−
qed+
−
+
−
lemma th_not_ready_s [simp]: "th \<notin> readys s"+
−
  using th_not_live_s by (unfold readys_def, simp)+
−
+
−
lemma th_live_es [simp]: "th \<in> threads (e#s)"+
−
  by (unfold is_create, simp)+
−
+
−
lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'"+
−
proof+
−
  assume "waiting s th cs'"+
−
  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
  have "th \<in> set (wq s cs')" by auto+
−
  from wq_threads[OF this] have "th \<in> threads s" .+
−
  with th_not_live_s show False by simp+
−
qed+
−
+
−
lemma not_holding_th_s [simp]: "\<not> holding s th cs'"+
−
proof+
−
  assume "holding s th cs'"+
−
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]+
−
  have "th \<in> set (wq s cs')" by auto+
−
  from wq_threads[OF this] have "th \<in> threads s" .+
−
  with th_not_live_s show False by simp+
−
qed+
−
+
−
lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'"+
−
proof+
−
  assume "waiting (e # s) th cs'"+
−
  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
  have "th \<in> set (wq s cs')" by auto+
−
  from wq_threads[OF this] have "th \<in> threads s" .+
−
  with th_not_live_s show False by simp+
−
qed+
−
+
−
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"+
−
proof+
−
  assume "holding (e # s) th cs'"+
−
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]+
−
  have "th \<in> set (wq s cs')" by auto+
−
  from wq_threads[OF this] have "th \<in> threads s" .+
−
  with th_not_live_s show False by simp+
−
qed+
−
+
−
lemma ready_th_es [simp]: "th \<in> readys (e#s)"+
−
  by (simp add:readys_def)+
−
+
−
lemma holdents_th_s: "holdents s th = {}"+
−
  by (unfold holdents_def, auto)+
−
+
−
lemma holdents_th_es: "holdents (e#s) th = {}"+
−
  by (unfold holdents_def, auto)+
−
+
−
lemma cntCS_th_s [simp]: "cntCS s th = 0"+
−
  by (unfold cntCS_def, simp add:holdents_th_s)+
−
+
−
lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"+
−
  by (unfold cntCS_def, simp add:holdents_th_es)+
−
+
−
lemma pvD_th_s [simp]: "pvD s th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma pvD_th_es [simp]: "pvD (e#s) th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma holdents_kept:+
−
  assumes "th' \<noteq> th"+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume h: "cs' \<in> ?L"+
−
    hence "cs' \<in> ?R"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } moreover {+
−
    fix cs'+
−
    assume h: "cs' \<in> ?R"+
−
    hence "cs' \<in> ?L"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_kept [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")+
−
  using holdents_kept[OF assms]+
−
  by (unfold cntCS_def, simp)+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
      using assms by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def]+
−
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
    have False by auto+
−
  } thus ?thesis using assms+
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'"+
−
      using assms(2) by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
         n_wait[unfolded s_waiting_def, folded wq_def]+
−
    have False by auto+
−
  } with assms show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1[OF assms] readys_kept2[OF assms]+
−
  by metis+
−
+
−
lemma pvD_kept [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "pvD (e#s) th' = pvD s th'"+
−
  using assms+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof -+
−
  {+
−
    assume eq_th': "th' = th"+
−
    have ?thesis using assms+
−
      by (unfold eq_th', simp, unfold is_create, simp)+
−
  } moreover {+
−
    assume h: "th' \<noteq> th"+
−
    hence ?thesis using assms+
−
      by (simp, simp add:is_create)+
−
  } ultimately show ?thesis by metis+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_exit+
−
begin+
−
+
−
lemma th_live_s [simp]: "th \<in> threads s"+
−
proof -+
−
  from pip_e[unfolded is_exit]+
−
  show ?thesis+
−
  by (cases, unfold running_def readys_def, simp)+
−
qed+
−
+
−
lemma th_ready_s [simp]: "th \<in> readys s"+
−
proof -+
−
  from pip_e[unfolded is_exit]+
−
  show ?thesis+
−
  by (cases, unfold running_def, simp)+
−
qed+
−
+
−
lemma th_not_live_es [simp]: "th \<notin> threads (e#s)"+
−
  by (unfold is_exit, simp)+
−
+
−
lemma not_holding_th_s [simp]: "\<not> holding s th cs'"+
−
proof -+
−
  from pip_e[unfolded is_exit]+
−
  show ?thesis +
−
   by (cases, unfold holdents_def, auto)+
−
qed+
−
+
−
lemma cntCS_th_s [simp]: "cntCS s th = 0"+
−
proof -+
−
  from pip_e[unfolded is_exit]+
−
  show ?thesis +
−
   by (cases, unfold cntCS_def, simp)+
−
qed+
−
+
−
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"+
−
proof+
−
  assume "holding (e # s) th cs'"+
−
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]+
−
  have "holding s th cs'" +
−
    by (unfold s_holding_def, auto)+
−
  with not_holding_th_s +
−
  show False by simp+
−
qed+
−
+
−
lemma ready_th_es [simp]: "th \<notin> readys (e#s)"+
−
  by (simp add:readys_def)+
−
+
−
lemma holdents_th_s: "holdents s th = {}"+
−
  by (unfold holdents_def, auto)+
−
+
−
lemma holdents_th_es: "holdents (e#s) th = {}"+
−
  by (unfold holdents_def, auto)+
−
+
−
lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"+
−
  by (unfold cntCS_def, simp add:holdents_th_es)+
−
+
−
lemma pvD_th_s [simp]: "pvD s th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma pvD_th_es [simp]: "pvD (e#s) th = 0"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma holdents_kept:+
−
  assumes "th' \<noteq> th"+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume h: "cs' \<in> ?L"+
−
    hence "cs' \<in> ?R"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } moreover {+
−
    fix cs'+
−
    assume h: "cs' \<in> ?R"+
−
    hence "cs' \<in> ?L"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_kept [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")+
−
  using holdents_kept[OF assms]+
−
  by (unfold cntCS_def, simp)+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
      using assms by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def]+
−
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
    have False by auto+
−
  } thus ?thesis using assms+
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<noteq> th"+
−
  and "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'"+
−
      using assms(2) by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
         n_wait[unfolded s_waiting_def, folded wq_def]+
−
    have False by auto+
−
  } with assms show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1[OF assms] readys_kept2[OF assms]+
−
  by metis+
−
+
−
lemma pvD_kept [simp]:+
−
  assumes "th' \<noteq> th"+
−
  shows "pvD (e#s) th' = pvD s th'"+
−
  using assms+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
proof -+
−
  {+
−
    assume eq_th': "th' = th"+
−
    have ?thesis using assms+
−
      by (unfold eq_th', simp, unfold is_exit, simp)+
−
  } moreover {+
−
    assume h: "th' \<noteq> th"+
−
    hence ?thesis using assms+
−
      by (simp, simp add:is_exit)+
−
  } ultimately show ?thesis by metis+
−
qed+
−
+
−
end+
−
+
−
context valid_trace_set+
−
begin+
−
+
−
lemma th_live_s [simp]: "th \<in> threads s"+
−
proof -+
−
  from pip_e[unfolded is_set]+
−
  show ?thesis+
−
  by (cases, unfold running_def readys_def, simp)+
−
qed+
−
+
−
lemma th_ready_s [simp]: "th \<in> readys s"+
−
proof -+
−
  from pip_e[unfolded is_set]+
−
  show ?thesis+
−
  by (cases, unfold running_def, simp)+
−
qed+
−
+
−
lemma th_not_live_es [simp]: "th \<in> threads (e#s)"+
−
  by (unfold is_set, simp)+
−
+
−
+
−
lemma holdents_kept:+
−
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")+
−
proof -+
−
  { fix cs'+
−
    assume h: "cs' \<in> ?L"+
−
    hence "cs' \<in> ?R"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } moreover {+
−
    fix cs'+
−
    assume h: "cs' \<in> ?R"+
−
    hence "cs' \<in> ?L"+
−
      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)+
−
  } ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma cntCS_kept [simp]:+
−
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")+
−
  using holdents_kept+
−
  by (unfold cntCS_def, simp)+
−
+
−
lemma readys_kept1: +
−
  assumes "th' \<in> readys (e#s)"+
−
  shows "th' \<in> readys s"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting s th' cs'"+
−
    have n_wait: "\<not> waiting (e#s) th' cs'" +
−
      using assms by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def]+
−
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
    have False by auto+
−
  } moreover have "th' \<in> threads s" +
−
    using assms[unfolded readys_def] by auto+
−
  ultimately show ?thesis +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_kept2: +
−
  assumes "th' \<in> readys s"+
−
  shows "th' \<in> readys (e#s)"+
−
proof -+
−
  { fix cs'+
−
    assume wait: "waiting (e#s) th' cs'"+
−
    have n_wait: "\<not> waiting s th' cs'"+
−
      using assms by (auto simp:readys_def)+
−
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]+
−
         n_wait[unfolded s_waiting_def, folded wq_def]+
−
    have False by auto+
−
  } with assms show ?thesis  +
−
    by (unfold readys_def, auto)+
−
qed+
−
+
−
lemma readys_simp [simp]:+
−
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"+
−
  using readys_kept1 readys_kept2+
−
  by metis+
−
+
−
lemma pvD_kept [simp]:+
−
  shows "pvD (e#s) th' = pvD s th'"+
−
  by (unfold pvD_def, simp)+
−
+
−
lemma cnp_cnv_cncs_kept:+
−
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"+
−
  using assms+
−
  by (unfold is_set, simp, fold is_set, simp)+
−
+
−
end+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"+
−
proof(induct rule:ind)+
−
  case Nil+
−
  thus ?case +
−
    unfolding cntP_def  cntV_def pvD_def cntCS_def holdents_def s_holding_def+
−
    by(simp add: wq_def)+
−
next+
−
  case (Cons s e)+
−
  interpret vt_e: valid_trace_e s e using Cons by simp+
−
  show ?case+
−
  proof(cases e)+
−
    case (Create th prio)+
−
    interpret vt_create: valid_trace_create s e th prio +
−
      using Create by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_create.cnp_cnv_cncs_kept) +
−
  next+
−
    case (Exit th)+
−
    interpret vt_exit: valid_trace_exit s e th  +
−
        using Exit by (unfold_locales, simp)+
−
   show ?thesis using Cons by (simp add: vt_exit.cnp_cnv_cncs_kept) +
−
  next+
−
    case (P th cs)+
−
    interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_p.cnp_cnv_cncs_kept) +
−
  next+
−
    case (V th cs)+
−
    interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_v.cnp_cnv_cncs_kept) +
−
  next+
−
    case (Set th prio)+
−
    interpret vt_set: valid_trace_set s e th prio+
−
        using Set by (unfold_locales, simp)+
−
    show ?thesis using Cons by (simp add: vt_set.cnp_cnv_cncs_kept) +
−
  qed+
−
qed+
−
+
−
end+
−
+
−
section {* Corollaries of @{thm valid_trace.cnp_cnv_cncs} *}+
−
+
−
context valid_trace+
−
begin+
−
+
−
text {*+
−
  The following two lemmas are purely technical, which says+
−
  a non-living thread can not hold any resource.+
−
*}+
−
lemma not_thread_holdents:+
−
  assumes not_in: "th \<notin> threads s" +
−
  shows "holdents s th = {}"+
−
proof -+
−
  { fix cs+
−
    assume "cs \<in> holdents s th"+
−
    hence "holding s th cs" by (auto simp:holdents_def)+
−
    from this[unfolded s_holding_def, folded wq_def]+
−
    have "th \<in> set (wq s cs)" by auto+
−
    with wq_threads have "th \<in> threads s" by auto+
−
    with assms+
−
    have False by simp+
−
  } thus ?thesis by auto+
−
qed+
−
+
−
lemma not_thread_cncs:+
−
  assumes not_in: "th \<notin> threads s" +
−
  shows "cntCS s th = 0"+
−
  using not_thread_holdents[OF assms]+
−
  by (simp add:cntCS_def)+
−
+
−
text {*+
−
  Starting from the following @{text cnp_cnv_eq}, all +
−
  lemmas in this section concern the meaning of +
−
  condition @{prop "cntP s th = cntV s th"}, i.e.+
−
  when the numbers of resource requesting and resource releasing+
−
  are equal.+
−
*}+
−
+
−
lemma cnp_cnv_eq:+
−
  assumes "th \<notin> threads s"+
−
  shows "cntP s th = cntV s th"+
−
  using assms cnp_cnv_cncs not_thread_cncs pvD_def+
−
  by (auto)+
−
+
−
lemma eq_pv_children:+
−
  assumes eq_pv: "cntP s th = cntV s th"+
−
  shows "children (RAG s) (Th th) = {}"+
−
proof -+
−
    from cnp_cnv_cncs and eq_pv+
−
    have "cntCS s th = 0" +
−
      by (auto split:if_splits)+
−
    from this[unfolded cntCS_def holdents_alt_def]+
−
    have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" .+
−
    have "finite (the_cs ` children (RAG s) (Th th))"+
−
      by (simp add: fsbtRAGs.finite_children)+
−
    from card_0[unfolded card_0_eq[OF this]]+
−
    show ?thesis by auto+
−
qed+
−
+
−
lemma eq_pv_holdents:+
−
  assumes eq_pv: "cntP s th = cntV s th"+
−
  shows "holdents s th = {}"+
−
  by (unfold holdents_alt_def eq_pv_children[OF assms], simp)+
−
+
−
lemma eq_pv_subtree:+
−
  assumes eq_pv: "cntP s th = cntV s th"+
−
  shows "subtree (RAG s) (Th th) = {Th th}"+
−
  using eq_pv_children[OF assms]+
−
  apply(subst subtree_children)+
−
  apply(simp)+
−
  done  +
−
+
−
lemma count_eq_RAG_plus:+
−
  assumes "cntP s th = cntV s th"+
−
  shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"+
−
proof(rule ccontr)+
−
    assume otherwise: "{th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} \<noteq> {}"+
−
    then obtain th' where "(Th th', Th th) \<in> (RAG s)^+" by auto+
−
    from tranclD2[OF this]+
−
    obtain z where "z \<in> children (RAG s) (Th th)" +
−
      by (auto simp:children_def)+
−
    with eq_pv_children[OF assms]+
−
    show False by simp+
−
qed+
−
+
−
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:+
−
  assumes "cntP s th = cntV s th"+
−
  shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"+
−
  using count_eq_RAG_plus_Th[OF assms]+
−
  using tRAG_trancl_eq 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+
−
+
−
subsection {* A notion @{text detached} and its relation with @{term cntP} +
−
  and @{term cntV} *}+
−
+
−
definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"+
−
  where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"+
−
+
−
text {*+
−
  The following lemma shows that a thread is detached means +
−
  it is isolated from @{term RAG}:+
−
*}+
−
+
−
lemma detached_test:+
−
  shows "detached s th = (Th th \<notin> Field (RAG s))"+
−
apply(simp add: detached_def Field_def)+
−
apply(simp add: s_RAG_def)+
−
apply(simp add: s_holding_abv s_waiting_abv)+
−
apply(simp add: Domain_iff Range_iff)+
−
apply(simp add: wq_def)+
−
apply(auto)+
−
done+
−
+
−
lemma detached_cp_the_preced:+
−
  assumes "detached s th"+
−
  shows "cp s th = the_preced s th" (is "?L = ?R")+
−
proof -+
−
  have "?L =  Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"+
−
      by (unfold cp_alt_def, simp)+
−
  moreover have "{th'. Th th' \<in> subtree (RAG s) (Th th)} = {th}" +
−
  proof -+
−
    { fix n+
−
      assume "n \<in> subtree (RAG s) (Th th)"+
−
      hence "n = Th th"+
−
      proof(cases rule:subtreeE)+
−
        case 2+
−
        from 2(2) have "Th th \<in> Range (RAG s)"+
−
          by (elim ancestors_Field, simp)+
−
        moreover from assms[unfolded detached_test] have "Th th \<notin> Field (RAG s)" .+
−
        ultimately have False by (auto simp:Field_def)+
−
        thus ?thesis by simp+
−
      qed simp+
−
    } thus ?thesis by auto+
−
  qed+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
lemma detached_cp_preced:+
−
  assumes "detached s th"+
−
  shows "cp s th = preced th s" +
−
  using detached_cp_the_preced[OF assms] +
−
  by (simp add:the_preced_def)+
−
+
−
context valid_trace+
−
begin+
−
+
−
lemma detached_intro:+
−
  assumes eq_pv: "cntP s th = cntV s th"+
−
  shows "detached s th"+
−
proof -+
−
  from eq_pv cnp_cnv_cncs+
−
  have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:pvD_def)+
−
  thus ?thesis+
−
  proof+
−
    assume "th \<notin> threads s"+
−
    with rg_RAG_threads dm_RAG_threads+
−
    show ?thesis+
−
      by (auto simp add: detached_def s_RAG_def s_waiting_abv +
−
              s_holding_abv wq_def Domain_iff Range_iff)+
−
  next+
−
    assume "th \<in> readys s"+
−
    moreover have "Th th \<notin> Range (RAG s)"+
−
    proof -+
−
      from eq_pv_children[OF assms]+
−
      have "children (RAG s) (Th th) = {}" .+
−
      thus ?thesis+
−
      by (unfold children_def, auto)+
−
    qed+
−
    ultimately show ?thesis+
−
      by (auto simp add: detached_def s_RAG_def s_waiting_abv +
−
              s_holding_abv wq_def readys_def)+
−
  qed+
−
qed+
−
+
−
lemma detached_elim:+
−
  assumes dtc: "detached s th"+
−
  shows "cntP s th = cntV s th"+
−
proof -+
−
  have cncs_z: "cntCS s th = 0"+
−
  proof -+
−
    from dtc have "holdents s th = {}"+
−
      unfolding detached_def holdents_test s_RAG_def+
−
      by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)+
−
    thus ?thesis by (auto simp:cntCS_def)+
−
  qed+
−
  show ?thesis+
−
  proof(cases "th \<in> threads s")+
−
    case True+
−
    with dtc +
−
    have "th \<in> readys s"+
−
      by (unfold readys_def detached_def Field_def Domain_def Range_def, +
−
           auto simp:s_waiting_abv s_RAG_def)+
−
    with cncs_z  show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)+
−
  next+
−
    case False+
−
    with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def)+
−
  qed+
−
qed+
−
+
−
lemma detached_eq:+
−
  shows "(detached s th) = (cntP s th = cntV s th)"+
−
  by (insert vt, auto intro:detached_intro detached_elim)+
−
+
−
end+
−
+
−
section {* Recursive calculation of @{term "cp"} *}+
−
+
−
text {*+
−
  According to the normal definitions, such as @{thm cp_def}, @{thm cp_alt_def}+
−
  and @{thm cp_alt_def1}, the @{term cp}-value of a thread depends +
−
  on the @{term preced}-values of all threads in its subtree. To calculate +
−
  a @{term cp}-value, one needs to traverse a whole subtree. +
−
+
−
  However, in this section, we are going to show that @{term cp}-value +
−
  can be calculate locally (given by the lemma @{text "cp_rec"} in the following).+
−
  According to this lemma,  the @{term cp}-value of a thread can be calculated only from +
−
  the @{term cp}-values of its children in @{term RAG}. +
−
  Therefore, if the @{term cp}-values of one thread's children are not+
−
  changed by an execution step, there is no need to recalculate. This+
−
  is particularly useful to in Implementation.thy to speed up the +
−
  recalculation of @{term cp}-values. +
−
*}+
−
+
−
text {*+
−
  The following function @{text "cp_gen"} is a generalization +
−
  of @{term cp}. Unlike @{term cp} which returns a precedence +
−
  for a thread, @{text "cp_gen"} returns precedence for a node+
−
  in @{term RAG}. When the node represent a thread, @{text cp_gen} is+
−
  coincident with @{term cp} (to be shown in lemma @{text "cp_gen_def_cond"}), +
−
  and this is the only meaningful use of @{text cp_gen}. +
−
+
−
  The introduction of @{text cp_gen} is purely technical to easy some+
−
  of the proofs leading to the finally lemma @{text cp_rec}.+
−
*}+
−
+
−
definition "cp_gen s x =+
−
                  Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"+
−
+
−
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 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+
−
(* ddd *)+
−
lemma cp_gen_rec:+
−
  assumes "x = Th th"+
−
  shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"+
−
proof(cases "children (tRAG s) x = {}")+
−
  case True+
−
  show ?thesis+
−
    apply(subst True)+
−
    apply(subst cp_gen_def)+
−
    apply(subst subtree_children)+
−
    apply(simp add: assms)+
−
    using True assms by auto  +
−
next+
−
  case False+
−
  hence [simp]: "children (tRAG s) x \<noteq> {}" by auto+
−
  note fsbttRAGs.finite_subtree[simp]+
−
  have [simp]: "finite (children (tRAG s) x)"+
−
     by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], +
−
            rule children_subtree)+
−
  { fix r x+
−
    have "subtree r x \<noteq> {}" by (auto simp:subtree_def)+
−
  } note this[simp]+
−
  have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"+
−
  proof -+
−
    from False obtain q where "q \<in> children (tRAG s) x" by blast+
−
    moreover have "subtree (tRAG s) q \<noteq> {}" by simp+
−
    ultimately show ?thesis by blast+
−
  qed+
−
  have h: "Max ((the_preced s \<circ> the_thread) `+
−
                ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =+
−
        Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"+
−
                     (is "?L = ?R")+
−
  proof -+
−
    let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L+
−
    let "Max (_ \<union> (?h ` ?B))" = ?R+
−
    let ?L1 = "?f ` \<Union>(?g ` ?B)"+
−
    have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"+
−
    proof -+
−
      have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp+
−
      also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto+
−
      finally have "Max ?L1 = Max ..." +
−
        by (simp add: \<open>(the_preced s \<circ> the_thread) ` (\<Union>x\<in>children (tRAG s) x. subtree (tRAG s) x) = (\<Union>x\<in>children (tRAG s) x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x)\<close>) +
−
      also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"+
−
        by(subst Max_Union, auto)+
−
      also have "... = Max (cp_gen s ` children (tRAG s) x)"+
−
          by (unfold image_comp cp_gen_alt_def, simp)+
−
      finally show ?thesis .+
−
    qed+
−
    show ?thesis+
−
    proof -+
−
      have "?L = Max (?f ` ?A \<union> ?L1)" by simp+
−
      also have "... = max (the_preced s (the_thread x)) (Max ?L1)"+
−
            by (subst Max_Un, simp+)+
−
      also have "... = max (?f x) (Max (?h ` ?B))"+
−
        by (unfold eq_Max_L1, simp)+
−
      also have "... =?R"+
−
        by (rule max_Max_eq, (simp)+, unfold assms, simp)+
−
      finally show ?thesis .+
−
    qed+
−
  qed  thus ?thesis +
−
          by (fold h subtree_children, unfold cp_gen_def, simp) +
−
qed+
−
+
−
lemma cp_rec:+
−
  "cp s th = Max ({the_preced s th} \<union> +
−
                     (cp s o the_thread) ` children (tRAG s) (Th th))"+
−
proof -+
−
  have "Th th = Th th" by simp+
−
  note h =  cp_gen_def_cond[OF this] cp_gen_rec[OF this]+
−
  show ?thesis +
−
  proof -+
−
    have "cp_gen s ` children (tRAG s) (Th th) = +
−
                (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"+
−
    proof(rule cp_gen_over_set)+
−
      show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"+
−
        by (unfold tRAG_alt_def, auto simp:children_def)+
−
    qed+
−
    thus ?thesis by (subst (1) h(1), unfold h(2), simp)+
−
  qed+
−
qed+
−
+
−
end+
−
+
−
lemma PIP_actorE:+
−
  assumes "PIP s e"+
−
  and "actor e = th"+
−
  and "\<not> isCreate e"+
−
  shows "th \<in> running s"+
−
  using assms+
−
  by (cases, auto)+
−
+
−
+
−
lemma holdents_RAG:+
−
  assumes "holdents s th = {}"+
−
  shows "Th th \<notin> Range (RAG s)"+
−
proof+
−
  assume "Th th \<in> Range (RAG s)"+
−
  thus False+
−
  proof(rule RangeE)+
−
    fix a+
−
    assume "(a, Th th) \<in> RAG s"+
−
    with assms[unfolded holdents_test]+
−
    show False+
−
    using assms children_def holdents_alt_def by fastforce+
−
  qed+
−
qed+
−
+
−
+
−
lemma readys_RAG:+
−
  assumes "th \<in> readys s"+
−
  shows "Th th \<notin> Domain (RAG s)"+
−
proof+
−
  assume "Th th \<in> Domain (RAG s)"+
−
  thus False+
−
  proof(rule DomainE)+
−
    fix b+
−
    assume "(Th th, b) \<in> RAG s"+
−
    with assms[unfolded readys_def s_waiting_def]+
−
    show False+
−
      using Collect_disj_eq s_RAG_def s_waiting_abv s_waiting_def wq_def by fastforce+
−
  qed+
−
qed+
−
+
−
+
−
text {*+
−
  The following two lemmas are general about any valid system state, +
−
  but are used in the derivation in more specific system operations. +
−
*}+
−
+
−
lemma readys_root:+
−
  assumes "th \<in> readys s"+
−
  shows "root (RAG s) (Th th)"+
−
  unfolding root_def ancestors_def+
−
  using readys_RAG assms+
−
by (metis Collect_empty_eq Domain.DomainI trancl_domain)+
−
+
−
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 readys_holdents_detached:+
−
  assumes "th \<in> readys s"+
−
  and "holdents s th = {}"+
−
  shows "detached s th"+
−
proof -+
−
  from readys_RAG[OF assms(1)] holdents_RAG[OF assms(2)]+
−
  show ?thesis+
−
    by (unfold detached_test Field_def, auto)+
−
qed+
−
+
−
lemma len_actions_of_sigma:+
−
  assumes "finite A"+
−
  shows "length (actions_of A t) = (\<Sum> th' \<in> A. length (actions_of {th'} t))"+
−
proof(induct t)+
−
  case h: (Cons e t)+
−
  thus ?case (is "?L = ?R" is "_ = ?T (e#t)") +
−
  proof(cases "actor e \<in> A")+
−
    case True+
−
    have "?L = 1 + ?T t"+
−
      by (fold h, insert True, simp add:actions_of_def)+
−
    moreover have "?R = 1 + ?T t"+
−
    proof -+
−
      have "?R = length (actions_of {actor e} (e # t)) ++
−
                 (\<Sum>th'\<in>A - {actor e}. length (actions_of {th'} (e # t)))"+
−
            (is "_ = ?F (e#t) + ?G (e#t)")+
−
            by (meson True assms sum.remove)      +
−
      moreover have "?F (e#t) = 1 + ?F t" using True+
−
          by  (simp add:actions_of_def)+
−
        moreover have "?G (e#t) = ?G t"+
−
        by (auto simp:actions_of_def) +
−
      moreover have "?F t + ?G t = ?T t"+
−
        by (metis (no_types, lifting) True assms sum.remove) +
−
      ultimately show ?thesis +
−
        by simp+
−
    qed+
−
    ultimately show ?thesis by simp+
−
  next+
−
    case False+
−
    hence "?L = length (actions_of A t)"+
−
      by (simp add:actions_of_def)+
−
    also have "... = (\<Sum>th'\<in>A. length (actions_of {th'} t))" by (simp add: h)+
−
    also have "... = ?R"+
−
      unfolding actions_of_def+
−
      by (metis (no_types, lifting) False filter.simps(2) singletonD sum.cong) +
−
    finally show ?thesis .+
−
  qed+
−
qed (auto simp:actions_of_def)+
−
+
−
lemma threads_Exit:+
−
    assumes "th \<in> threads s"+
−
    and "th \<notin> threads (e#s)"+
−
    shows "e = Exit th"+
−
    using assms+
−
    by (cases e, auto)+
−
+
−
end+
−
+
−