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