theory PIPBasics
imports PIPDefs
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
lemma Max_fg_mono:
assumes "finite A"
and "\<forall> a \<in> A. f a \<le> g a"
shows "Max (f ` A) \<le> Max (g ` A)"
proof(cases "A = {}")
case True
thus ?thesis by auto
next
case False
show ?thesis
proof(rule Max.boundedI)
from assms show "finite (f ` A)" by auto
next
from False show "f ` A \<noteq> {}" by auto
next
fix fa
assume "fa \<in> f ` A"
then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
show "fa \<le> Max (g ` A)"
proof(rule Max_ge_iff[THEN iffD2])
from assms show "finite (g ` A)" by auto
next
from False show "g ` A \<noteq> {}" by auto
next
from h_fa have "g a \<in> g ` A" by auto
moreover have "fa \<le> g a" using h_fa assms(2) by auto
ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
qed
qed
qed
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
and np: "A \<noteq> {}"
and fnt: "finite B"
shows "Max (f ` A) \<le> Max (f ` B)"
proof(rule Max_mono)
from seq show "f ` A \<subseteq> f ` B" by auto
next
from np show "f ` A \<noteq> {}" by auto
next
from fnt and seq show "finite (f ` B)" by auto
qed
lemma Max_UNION:
assumes "finite A"
and "A \<noteq> {}"
and "\<forall> M \<in> f ` A. finite M"
and "\<forall> M \<in> f ` A. M \<noteq> {}"
shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
using assms[simp]
proof -
have "?L = Max (\<Union>(f ` A))"
by (fold Union_image_eq, simp)
also have "... = ?R"
by (subst Max_Union, simp+)
finally show ?thesis .
qed
lemma max_Max_eq:
assumes "finite A"
and "A \<noteq> {}"
and "x = y"
shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
proof -
have "?R = Max (insert y A)" by simp
also from assms have "... = ?L"
by (subst Max.insert, simp+)
finally show ?thesis by simp
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"
by (unfold s_holding_def, fold wq_def, 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 holding_eq)
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 waiting_eq holding_eq]
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_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 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
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 image_eq:
assumes "A = B"
shows "f ` A = f ` B"
using assms by auto
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_alt_def:
"cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
have "Max (the_preced s ` ({th} \<union> dependants s th)) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "Max (_ ` ?L) = Max (_ ` ?R)")
proof -
have "?L = ?R"
unfolding subtree_def
apply(auto)
apply (simp add: s_RAG_abv s_dependants_def wq_def)
by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def)
thus ?thesis by simp
qed
thus ?thesis
by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants
f_image_eq the_preced_def)
qed
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
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 holding_eq, 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
text {*
The following lemmas gives an alternative definition @{term dependants}
in terms of @{term tRAG}.
*}
lemma dependants_alt_def:
"dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
text {*
The following lemmas gives another alternative definition @{term dependants}
in terms of @{term RAG}.
*}
lemma dependants_alt_def1:
"dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
using dependants_alt_def tRAG_trancl_eq by auto
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
text {*
The following lemma says that if @{text "s"} is a valid state, so
is its any postfix. Where @{term "monent t s"} is the postfix of
@{term "s"} with length @{term "t"}.
*}
lemma vt_moment: "\<And> t. vt (moment t s)"
proof(induct rule:ind)
case Nil
thus ?case by (simp add:vt_nil)
next
case (Cons s e t)
show ?case
proof(cases "t \<ge> length (e#s)")
case True
from True have "moment t (e#s) = e#s" by simp
thus ?thesis using Cons
by (simp add:valid_trace_def valid_trace_e_def, auto)
next
case False
from Cons have "vt (moment t s)" by simp
moreover have "moment t (e#s) = moment t s"
proof -
from False have "t \<le> length s" by simp
from moment_app [OF this, of "[e]"]
show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
qed
text {*
The following two lemmas are fundamental, because they assure
that the numbers of both living and ready threads are finite.
*}
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
text {*
The following locale @{text "valid_moment"} is to inherit the properties
derived on any valid state to the prefix of it, with length @{text "i"}.
*}
locale valid_moment = valid_trace +
fixes i :: nat
sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
by (unfold_locales, insert vt_moment, auto)
locale valid_moment_e = valid_moment +
assumes less_i: "i < length s"
begin
definition "next_e = hd (moment (Suc i) s)"
lemma trace_e:
"moment (Suc i) s = next_e#moment i s"
proof -
from less_i have "Suc i \<le> length s" by auto
from moment_plus[OF this, folded next_e_def]
show ?thesis .
qed
end
sublocale valid_moment_e < vat_moment_e: valid_trace_e "moment i s" "next_e"
using vt_moment[of "Suc i", unfolded trace_e]
by (unfold_locales, simp)
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'"
using assms 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'"
using assms 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"
by (unfold s_holding_def, fold wq_def, simp)
hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
by (unfold s_RAG_def, fold holding_eq, 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
by (unfold rest_def s_holding_def, fold wq_def,
metis empty_iff list.collapse list.set(1))
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'"
using assms 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
by (cases, unfold holdents_def s_holding_def, fold wq_def,
auto elim!: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
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 (in valid_trace) 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 *}
context valid_trace
begin
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
hence "th \<in> set (wq s cs)"
by (unfold s_RAG_def, auto simp: waiting_raw_def)
from wq_threads [OF this] show ?thesis .
qed
lemma rg_RAG_threads:
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
using assms
unfolding s_RAG_def waiting_raw_def holding_raw_def
using wq_threads by auto
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 not_in_thread_isolated:
assumes "th \<notin> threads s"
shows "(Th th) \<notin> Field (RAG s)"
using RAG_threads assms 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
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: waiting_raw_def waiting_eq)
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
unfolding waiting_raw_def waiting_eq by auto
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, unfolded wq_def, 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, fold wq_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) unfolding waiting_raw_def waiting_eq 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" unfolding waiting_raw_def waiting_eq by auto
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 waiting_raw_def insert_iff list.sel(1) s_waiting_abv set_simps(2) 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, unfolded wq_def, 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 rest_nil wq_s_cs unfolding waiting_raw_def waiting_eq by auto
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" unfolding waiting_raw_def waiting_eq by auto
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, unfolded wq_def, 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 waiting_eq, 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 waiting_eq, 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 waiting_eq, 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 waiting_eq, 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 holding_eq, 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 holding_eq, 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 holding_eq, 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 waiting_eq, 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 holding_eq, 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 waiting_eq, 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 holding_eq, 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 holding_eq, 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
unfolding th_not_in_wq waiting_eq waiting_raw_def
by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD
list.distinct(1) split_list 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 holding_eq 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 holding_eq)
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 holding_eq by blast
qed
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold holding_eq, 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 holding_eq 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 waiting_eq, 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 holding_eq, 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 waiting_eq, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
qed
next
assume "n1 = Cs cs \<and> n2 = Th th"
with holding_es_th_cs
show ?thesis
by (unfold s_RAG_def, fold holding_eq, 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 waiting_eq wq_es_cs' wq_s_cs unfolding waiting_raw_def by auto
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold waiting_eq, 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
unfolding holding_raw_def holding_eq 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 waiting_raw_def holder_def list.sel(1) rotate1.simps(2)
set_ConsD set_rotate1 waiting_eq wq_es_cs 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 waiting_eq, 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 holding_eq, 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 waiting_eq, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, 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
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 waiting_eq, 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 waiting_eq, 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 waiting_eq holding_eq)
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 rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
end
sublocale valid_trace < rtree_RAG?: rtree "RAG s"
using rtree_RAG .
sublocale valid_trace < fsbtRAGs?: fsubtree "RAG s"
proof -
show "fsubtree (RAG s)"
proof(intro_locales)
show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
next
show "fsubtree_axioms (RAG s)"
proof(unfold fsubtree_axioms_def)
from wf_RAG show "wf (RAG s)" .
qed
qed
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 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)
end
text {*
It can be shown that @{term tRAG} is also a
finite-branch relational tree (or forest):
*}
sublocale valid_trace < rtree_s?: rtree "tRAG s"
proof(unfold_locales)
from sgv_tRAG show "single_valued (tRAG s)" .
next
from acyclic_tRAG show "acyclic (tRAG s)" .
qed
sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s"
proof -
have "fsubtree (tRAG s)"
proof -
have "fbranch (tRAG s)"
proof(unfold tRAG_def, rule fbranch_compose)
show "fbranch (wRAG s)"
proof(rule finite_fbranchI)
from finite_RAG show "finite (wRAG s)"
by (unfold RAG_split, auto)
qed
next
show "fbranch (hRAG s)"
proof(rule finite_fbranchI)
from finite_RAG
show "finite (hRAG s)" by (unfold RAG_split, auto)
qed
qed
moreover have "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
ultimately show ?thesis
by (unfold fsubtree_def fsubtree_axioms_def,auto)
qed
from this[folded tRAG_def] show "fsubtree (tRAG s)" .
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 waiting_eq, 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 holding_eq, 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 waiting_eq, 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
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
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 -
from running_1 and running_2 have "cp s th1 = cp s th2"
unfolding running_def by auto
from this[unfolded cp_alt_def]
have eq_max:
"Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})"
(is "Max ?L = Max ?R") .
have "Max ?L \<in> ?L"
proof(rule Max_in)
show "finite ?L" by (simp add: finite_subtree_threads)
next
show "?L \<noteq> {}" using subtree_def by fastforce
qed
then obtain th1' where
h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
by auto
have "Max ?R \<in> ?R"
proof(rule Max_in)
show "finite ?R" by (simp add: finite_subtree_threads)
next
show "?R \<noteq> {}" using subtree_def by fastforce
qed
then obtain th2' where
h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
by auto
have "th1' = th2'"
proof(rule preced_unique)
from h_1(1)
show "th1' \<in> threads s"
proof(cases rule:subtreeE)
case 1
hence "th1' = th1" by simp
with running_1 show ?thesis by (auto simp:running_def readys_def)
next
case 2
from this(2)
have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
from tranclD[OF this]
have "(Th th1') \<in> Domain (RAG s)" by auto
from dm_RAG_threads[OF this] show ?thesis .
qed
next
from h_2(1)
show "th2' \<in> threads s"
proof(cases rule:subtreeE)
case 1
hence "th2' = th2" by simp
with running_2 show ?thesis by (auto simp:running_def readys_def)
next
case 2
from this(2)
have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
from tranclD[OF this]
have "(Th th2') \<in> Domain (RAG s)" by auto
from dm_RAG_threads[OF this] show ?thesis .
qed
next
have "the_preced s th1' = the_preced s th2'"
using eq_max h_1(2) h_2(2) by metis
thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
qed
from h_1(1)[unfolded this]
have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
from h_2(1)[unfolded this]
have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
from star_rpath[OF star1] obtain xs1
where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
by auto
from star_rpath[OF star2] obtain xs2
where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
by auto
from rp1 rp2
show ?thesis
proof(cases)
case (less_1 xs')
moreover have "xs' = []"
proof(rule ccontr)
assume otherwise: "xs' \<noteq> []"
from rpath_plus[OF less_1(3) this]
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
from tranclD[OF this]
obtain cs where "waiting s th1 cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
with running_1 show False
by (unfold running_def readys_def, auto)
qed
ultimately have "xs2 = xs1" by simp
from rpath_dest_eq[OF rp1 rp2[unfolded this]]
show ?thesis by simp
next
case (less_2 xs')
moreover have "xs' = []"
proof(rule ccontr)
assume otherwise: "xs' \<noteq> []"
from rpath_plus[OF less_2(3) this]
have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
from tranclD[OF this]
obtain cs where "waiting s th2 cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
with running_2 show False
by (unfold running_def readys_def, auto)
qed
ultimately have "xs2 = xs1" by simp
from rpath_dest_eq[OF rp1 rp2[unfolded this]]
show ?thesis by simp
qed
qed
lemma card_running: "card (running s) \<le> 1"
proof(cases "running s = {}")
case True
thus ?thesis by auto
next
case False
then obtain th where [simp]: "th \<in> running s" by auto
from running_unique[OF this]
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 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 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:rtree_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:waiting_eq)
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:waiting_eq)
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 max_cp_readys_max_preced:
shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
proof(cases "readys s = {}")
case False
have "?R =
Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
by (simp add: threads_alt_def)
also have "... =
Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
by (unfold image_UN, simp)
also have "... =
Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)"
proof(rule Max_UNION)
show "\<forall>M\<in>(\<lambda>x. the_preced s `
{th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
using finite_subtree_threads by auto
qed (auto simp:False subtree_def finite_readys)
also have "... =
Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) `
readys s)"
by (simp add: image_comp)
also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
proof -
have "(?f ` ?A) = (?g ` ?A)"
proof(rule f_image_eq)
fix th1
assume "th1 \<in> ?A"
thus "?f th1 = ?g th1"
by (unfold cp_alt_def, simp)
qed
thus ?thesis by simp
qed
finally show ?thesis by simp
qed (auto simp:threads_alt_def)
text {*
The following lemma is simply a corollary of @{thm max_cp_readys_max_preced}
and @{thm max_cp_eq}:
*}
lemma max_cp_readys_threads:
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
using max_cp_readys_max_preced max_cp_eq by auto
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, fold wq_def, unfold wq_s_cs, auto)
lemma holding_es_holder: "holding (e#s) holder cs"
by (unfold s_holding_def, fold wq_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, fold wq_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, fold wq_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
unfolding holding_raw_def holding_eq 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, fold wq_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, fold wq_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, fold wq_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, fold wq_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, fold wq_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, fold wq_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[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' = 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, fold wq_def,
unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_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, fold wq_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, fold wq_def,
unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_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, fold wq_def,
unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_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
by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def
s_holding_def, simp)
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]
by (unfold subtree_children, simp)
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 eq_pv_dependants:
assumes eq_pv: "cntP s th = cntV s th"
shows "dependants s th = {}"
proof -
from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
show ?thesis .
qed
lemma count_eq_tRAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using assms eq_pv_dependants dependants_alt_def eq_dependants 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:waiting_eq 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
by (unfold True cp_gen_def subtree_children, simp add:assms)
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
also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
by (subst Max_UNION, simp+)
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
by (cases a, auto simp:RAG_raw_def s_RAG_abv)
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
by (cases b, auto simp: RAG_raw_def s_RAG_abv waiting_raw_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 (subst comm_monoid_add_class.setsum.remove[where x = "actor e",
OF assms True], simp)
moreover have "?F (e#t) = 1 + ?F t" using True
by (simp add:actions_of_def)
moreover have "?G (e#t) = ?G t"
by (rule setsum.cong, auto simp:actions_of_def)
moreover have "?F t + ?G t = ?T t"
by (subst comm_monoid_add_class.setsum.remove[where x = "actor e",
OF assms True], simp)
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"
by (rule setsum.cong; insert False, auto simp:actions_of_def)
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