CpsG.thy updated. It is a copy of PIPBasics.thy under drastic improvement.
theory CpsG
imports PIPDefs
begin
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
(* I am going to use this file as a start point to retrofiting
PIPBasics.thy, which is originally called CpsG.ghy *)
locale valid_trace =
fixes s
assumes vt : "vt s"
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
by (unfold s_waiting_def cs_waiting_def wq_def, auto)
lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
by (unfold s_holding_def wq_def cs_holding_def, simp)
thm s_waiting_def cs_waiting_def wq_def
locale valid_trace_e = valid_trace +
fixes e
assumes vt_e: "vt (e#s)"
begin
lemma pip_e: "PIP s e"
using vt_e by (cases, simp)
end
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
by auto
lemma readys_threads:
shows "readys s \<subseteq> threads s"
unfolding readys_def
by auto
lemma wq_v_neq [simp]:
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
lemma runing_head:
assumes "th \<in> runing s"
and "th \<in> set (wq_fun (schs s) cs)"
shows "th = hd (wq_fun (schs s) cs)"
using assms
by (simp add:runing_def readys_def s_waiting_def wq_def)
context valid_trace
begin
lemma actor_inv:
assumes "PIP s e"
and "\<not> isCreate e"
shows "actor e \<in> runing s"
using assms
by (induct, auto)
lemma isP_E:
assumes "isP e"
obtains cs where "e = P (actor e) cs"
using assms by (cases e, auto)
lemma isV_E:
assumes "isV e"
obtains cs where "e = V (actor e) cs"
using assms by (cases e, auto)
lemma ind [consumes 0, case_names Nil Cons, induct type]:
assumes "PP []"
and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
shows "PP s"
proof(rule vt.induct[OF vt])
from assms(1) show "PP []" .
next
fix s e
assume h: "vt s" "PP s" "PIP s e"
show "PP (e # s)"
proof(cases rule:assms(2))
from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
next
from h(1,3) have "vt (e#s)" by auto
thus "valid_trace (e # s)" by (unfold_locales, simp)
qed (insert h, auto)
qed
lemma wq_distinct: "distinct (wq s cs)"
proof(induct rule:ind)
case (Cons s e)
from Cons(4,3)
show ?case
proof(induct)
case (thread_P th s cs1)
show ?case
proof(cases "cs = cs1")
case True
thus ?thesis (is "distinct ?L")
proof -
have "?L = wq_fun (schs s) cs1 @ [th]" using True
by (simp add:wq_def wf_def Let_def split:list.splits)
moreover have "distinct ..."
proof -
have "th \<notin> set (wq_fun (schs s) cs1)"
proof
assume otherwise: "th \<in> set (wq_fun (schs s) cs1)"
from runing_head[OF thread_P(1) this]
have "th = hd (wq_fun (schs s) cs1)" .
hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise
by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
with thread_P(2) show False by auto
qed
moreover have "distinct (wq_fun (schs s) cs1)"
using True thread_P wq_def by auto
ultimately show ?thesis by auto
qed
ultimately show ?thesis by simp
qed
next
case False
with thread_P(3)
show ?thesis
by (auto simp:wq_def wf_def Let_def split:list.splits)
qed
next
case (thread_V th s cs1)
thus ?case
proof(cases "cs = cs1")
case True
show ?thesis (is "distinct ?L")
proof(cases "(wq s cs)")
case Nil
thus ?thesis
by (auto simp:wq_def wf_def Let_def split:list.splits)
next
case (Cons w_hd w_tl)
moreover have "distinct (SOME q. distinct q \<and> set q = set w_tl)"
proof(rule someI2)
from thread_V(3)[unfolded Cons]
show "distinct w_tl \<and> set w_tl = set w_tl" by auto
qed auto
ultimately show ?thesis
by (auto simp:wq_def wf_def Let_def True split:list.splits)
qed
next
case False
with thread_V(3)
show ?thesis
by (auto simp:wq_def wf_def Let_def split:list.splits)
qed
qed (insert Cons, auto simp: wq_def Let_def split:list.splits)
qed (unfold wq_def Let_def, simp)
end
context valid_trace_e
begin
text {*
The following lemma shows that only the @{text "P"}
operation can add new thread into waiting queues.
Such kind of lemmas are very obvious, but need to be checked formally.
This is a kind of confirmation that our modelling is correct.
*}
lemma wq_in_inv:
assumes s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof(cases e)
-- {* This is the only non-trivial case: *}
case (V th cs1)
have False
proof(cases "cs1 = cs")
case True
show ?thesis
proof(cases "(wq s cs1)")
case (Cons w_hd w_tl)
have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"
proof -
have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"
using Cons V by (auto simp:wq_def Let_def True split:if_splits)
moreover have "set ... \<subseteq> set (wq s cs)"
proof(rule someI2)
show "distinct w_tl \<and> set w_tl = set w_tl"
by (metis distinct.simps(2) local.Cons wq_distinct)
qed (insert Cons True, auto)
ultimately show ?thesis by simp
qed
with assms show ?thesis by auto
qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)
qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
thus ?thesis by auto
qed (insert assms, auto simp:wq_def Let_def split:if_splits)
lemma wq_out_inv:
assumes s_in: "thread \<in> set (wq s cs)"
and s_hd: "thread = hd (wq s cs)"
and s_i: "thread \<noteq> hd (wq (e#s) cs)"
shows "e = V thread cs"
proof(cases e)
-- {* There are only two non-trivial cases: *}
case (V th cs1)
show ?thesis
proof(cases "cs1 = cs")
case True
have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .
thus ?thesis
proof(cases)
case (thread_V)
moreover have "th = thread" using thread_V(2) s_hd
by (unfold s_holding_def wq_def, simp)
ultimately show ?thesis using V True by simp
qed
qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
next
case (P th cs1)
show ?thesis
proof(cases "cs1 = cs")
case True
with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"
by (auto simp:wq_def Let_def split:if_splits)
with s_i s_hd s_in have False
by (metis empty_iff hd_append2 list.set(1) wq_def)
thus ?thesis by simp
qed (insert assms P, auto simp:wq_def Let_def split:if_splits)
qed (insert assms, auto simp:wq_def Let_def split:if_splits)
end
context valid_trace
begin
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)
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
end
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)
context valid_trace
begin
text {* (* ddd *)
The nature of the work is like this: since it starts from a very simple and basic
model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
For instance, the fact
that one thread can not be blocked by two critical resources at the same time
is obvious, because only running threads can make new requests, if one is waiting for
a critical resource and get blocked, it can not make another resource request and get
blocked the second time (because it is not running).
To derive this fact, one needs to prove by contraction and
reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
named @{text "p_split"}, which is about status changing along the time axis. It says if
a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"}
in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history
of events leading to it), such that @{text "Q"} switched
from being @{text "False"} to @{text "True"} and kept being @{text "True"}
till the last moment of @{text "s"}.
Suppose a thread @{text "th"} is blocked
on @{text "cs1"} and @{text "cs2"} in some state @{text "s"},
since no thread is blocked at the very beginning, by applying
@{text "p_split"} to these two blocking facts, there exist
two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that
@{text "th"} got blocked on @{text "cs1"} and @{text "cs2"}
and kept on blocked on them respectively ever since.
Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
in blocked state at moment @{text "t2"} and could not
make any request and get blocked the second time: Contradiction.
*}
lemma waiting_unique_pre: (* ddd *)
assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
and h22: "thread \<noteq> hd (wq s cs2)"
and neq12: "cs1 \<noteq> cs2"
shows "False"
proof -
let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"
from h11 and h12 have q1: "?Q cs1 s" by simp
from h21 and h22 have q2: "?Q cs2 s" by simp
have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)
have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)
from p_split [of "?Q cs1", OF q1 nq1]
obtain t1 where lt1: "t1 < length s"
and np1: "\<not> ?Q cs1 (moment t1 s)"
and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto
from p_split [of "?Q cs2", OF q2 nq2]
obtain t2 where lt2: "t2 < length s"
and np2: "\<not> ?Q cs2 (moment t2 s)"
and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto
{ fix s cs
assume q: "?Q cs s"
have "thread \<notin> runing s"
proof
assume "thread \<in> runing s"
hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and>
thread \<noteq> hd (wq_fun (schs s) cs))"
by (unfold runing_def s_waiting_def readys_def, auto)
from this[rule_format, of cs] q
show False by (simp add: wq_def)
qed
} note q_not_runing = this
{ fix t1 t2 cs1 cs2
assume lt1: "t1 < length s"
and np1: "\<not> ?Q cs1 (moment t1 s)"
and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
and lt2: "t2 < length s"
and np2: "\<not> ?Q cs2 (moment t2 s)"
and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
and lt12: "t1 < t2"
let ?t3 = "Suc t2"
from lt2 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
have "t2 < ?t3" by simp
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
have "vt (e#moment t2 s)"
proof -
from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
then interpret vt_e: valid_trace_e "moment t2 s" "e"
by (unfold_locales, auto, cases, simp)
have ?thesis
proof -
have "thread \<in> runing (moment t2 s)"
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
have "e = V thread cs2"
proof -
have eq_th: "thread = hd (wq (moment t2 s) cs2)"
using True and np2 by auto
from vt_e.wq_out_inv[OF True this h2]
show ?thesis .
qed
thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto
next
case False
have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
with vt_e.actor_inv[OF vt_e.pip_e]
show ?thesis by auto
qed
moreover have "thread \<notin> runing (moment t2 s)"
by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
ultimately show ?thesis by simp
qed
} note lt_case = this
show ?thesis
proof -
{ assume "t1 < t2"
from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
have ?thesis .
} moreover {
assume "t2 < t1"
from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
have ?thesis .
} moreover {
assume eq_12: "t1 = t2"
let ?t3 = "Suc t2"
from lt2 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
have lt_2: "t2 < ?t3" by simp
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]
have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have "vt (e#moment t2 s)"
proof -
from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
then interpret vt_e: valid_trace_e "moment t2 s" "e"
by (unfold_locales, auto, cases, simp)
have "e = V thread cs2 \<or> e = P thread cs2"
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
have "e = V thread cs2"
proof -
have eq_th: "thread = hd (wq (moment t2 s) cs2)"
using True and np2 by auto
from vt_e.wq_out_inv[OF True this h2]
show ?thesis .
qed
thus ?thesis by auto
next
case False
have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
thus ?thesis by auto
qed
moreover have "e = V thread cs1 \<or> e = P thread cs1"
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
have eq_th: "thread = hd (wq (moment t1 s) cs1)"
using True and np1 by auto
from vt_e.wq_out_inv[folded eq_12, OF True this g2]
have "e = V thread cs1" .
thus ?thesis by auto
next
case False
have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .
thus ?thesis by auto
qed
ultimately have ?thesis using neq12 by auto
} ultimately show ?thesis using nat_neq_iff by blast
qed
qed
text {*
This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
*}
lemma waiting_unique:
assumes "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
using waiting_unique_pre assms
unfolding wq_def s_waiting_def
by auto
end
(* not used *)
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)
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
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
(* An aux lemma used later *)
lemma unique_minus:
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r"
and xz: "(x, z) \<in> r^+"
and neq: "y \<noteq> z"
shows "(y, z) \<in> r^+"
proof -
from xz and neq show ?thesis
proof(induct)
case (base ya)
have "(x, ya) \<in> r" by fact
from unique [OF xy this] have "y = ya" .
with base show ?case by auto
next
case (step ya z)
show ?case
proof(cases "y = ya")
case True
from step True show ?thesis by simp
next
case False
from step False
show ?thesis by auto
qed
qed
qed
lemma unique_base:
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r"
and xz: "(x, z) \<in> r^+"
and neq_yz: "y \<noteq> z"
shows "(y, z) \<in> r^+"
proof -
from xz neq_yz show ?thesis
proof(induct)
case (base ya)
from xy unique base show ?case by auto
next
case (step ya z)
show ?case
proof(cases "y = ya")
case True
from True step show ?thesis by auto
next
case False
from False step
have "(y, ya) \<in> r\<^sup>+" by auto
with step show ?thesis by auto
qed
qed
qed
lemma unique_chain:
assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"
and xy: "(x, y) \<in> r^+"
and xz: "(x, z) \<in> r^+"
and neq_yz: "y \<noteq> z"
shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"
proof -
from xy xz neq_yz show ?thesis
proof(induct)
case (base y)
have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto
from unique_base [OF _ h1 h2 h3] and unique show ?case by auto
next
case (step y za)
show ?case
proof(cases "y = z")
case True
from True step show ?thesis by auto
next
case False
from False step have "(y, z) \<in> r\<^sup>+ \<or> (z, y) \<in> r\<^sup>+" by auto
thus ?thesis
proof
assume "(z, y) \<in> r\<^sup>+"
with step have "(z, za) \<in> r\<^sup>+" by auto
thus ?thesis by auto
next
assume h: "(y, z) \<in> r\<^sup>+"
from step have yza: "(y, za) \<in> r" by simp
from step have "za \<noteq> z" by simp
from unique_minus [OF _ yza h this] and unique
have "(za, z) \<in> r\<^sup>+" by auto
thus ?thesis by auto
qed
qed
qed
qed
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 RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)
lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)
lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)
context valid_trace
begin
lemma finite_threads:
shows "finite (threads s)"
using vt by (induct) (auto elim: step.cases)
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
thm cpreced_initial
apply(simp add: Let_def cpreced_initial)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
done
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
lemma wq_threads:
assumes h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
from vt and h show ?thesis
proof(induct arbitrary: th cs)
case (vt_cons s e)
interpret vt_s: valid_trace s
using vt_cons(1) by (unfold_locales, auto)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
and vt: "vt s"
and h: "th \<in> set (wq (e # s) cs)"
show ?case
proof(cases e)
case (Create th' prio)
with ih h show ?thesis
by (auto simp:wq_def Let_def)
next
case (Exit th')
with stp ih h show ?thesis
apply (auto simp:wq_def Let_def)
apply (ind_cases "step s (Exit th')")
apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
s_RAG_def s_holding_def cs_holding_def)
done
next
case (V th' cs')
show ?thesis
proof(cases "cs' = cs")
case False
with h
show ?thesis
apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def)
by (drule_tac ih, simp)
next
case True
from h
show ?thesis
proof(unfold V wq_def)
assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
show "th \<in> threads (V th' cs' # s)"
proof(cases "cs = cs'")
case False
hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
with th_in have " th \<in> set (wq s cs)"
by (fold wq_def, simp)
from ih [OF this] show ?thesis by simp
next
case True
show ?thesis
proof(cases "wq_fun (schs s) cs'")
case Nil
with h V show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
by (fold wq_def, drule_tac ih, simp)
next
case (Cons a rest)
assume eq_wq: "wq_fun (schs s) cs' = a # rest"
with h V show ?thesis
apply (auto simp:Let_def wq_def split:if_splits)
proof -
assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
qed
with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
from ih[OF this[folded wq_def]] show "th \<in> threads s" .
next
assume th_in: "th \<in> set (wq_fun (schs s) cs)"
from ih[OF this[folded wq_def]]
show "th \<in> threads s" .
qed
qed
qed
qed
qed
next
case (P th' cs')
from h stp
show ?thesis
apply (unfold P wq_def)
apply (auto simp:Let_def split:if_splits, fold wq_def)
apply (auto intro:ih)
apply(ind_cases "step s (P th' cs')")
by (unfold runing_def readys_def, auto)
next
case (Set thread prio)
with ih h show ?thesis
by (auto simp:wq_def Let_def)
qed
next
case vt_nil
thus ?case by (auto simp:wq_def)
qed
qed
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 from RAG_target_th[OF this] obtain cs where "n = Cs cs" by 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:cs_waiting_def)
from wq_threads [OF this] show ?thesis .
qed
lemma cp_le:
assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
\<le> Max ((\<lambda>th. preced th s) ` threads s)"
(is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
proof(rule Max_f_mono)
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
next
from finite_threads
show "finite (threads s)" .
next
from th_in
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
apply (rule_tac dm_RAG_threads)
apply (unfold trancl_domain [of "RAG s", symmetric])
by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (priority th s) (last_set th s)
\<le> Max (insert (Prc (priority th s) (last_set th s))
((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
(is "?l \<le> Max (insert ?l ?A)")
proof(cases "?A = {}")
case False
have "finite ?A" (is "finite (?f ` ?B)")
proof -
have "finite ?B"
proof-
have "finite {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
apply (auto simp:image_def)
by (rule_tac x = "(Th x, Th th)" in bexI, auto)
moreover have "finite \<dots>"
proof -
from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
from Max_insert [OF this False, of ?l] show ?thesis by auto
next
case True
thus ?thesis by auto
qed
qed
lemma max_cp_eq:
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
case True
thus ?thesis by auto
next
case False
have "?l \<in> ((cp s) ` threads s)"
proof(rule Max_in)
from finite_threads
show "finite (cp s ` threads s)" by auto
next
from False show "cp s ` threads s \<noteq> {}" by auto
qed
then obtain th
where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
proof -
have "?r \<in> (?f ` ?A)"
proof(rule Max_in)
from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
qed
then obtain th' where
th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
from le_cp [of th'] eq_r
have "?r \<le> cp s th'" by auto
moreover have "\<dots> \<le> cp s th"
proof(fold eq_l)
show " cp s th' \<le> Max (cp s ` threads s)"
proof(rule Max_ge)
from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
next
from finite_threads
show "finite (cp s ` threads s)" by auto
qed
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis using eq_l by auto
qed
lemma max_cp_eq_the_preced:
shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
using max_cp_eq using the_preced_def by presburger
end
lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s"
by (unfold preced_def, simp)
lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
proof
fix th'
show "the_preced (V th cs # s) th' = the_preced s th'"
by (unfold the_preced_def preced_def, simp)
qed
locale valid_trace_v = valid_trace_e +
fixes th cs
assumes is_v: "e = V th cs"
context valid_trace_v
begin
definition "rest = tl (wq s cs)"
definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
lemma distinct_rest: "distinct rest"
by (simp add: distinct_tl rest_def wq_distinct)
lemma runing_th_s:
shows "th \<in> runing s"
proof -
from pip_e[unfolded is_v]
show ?thesis by (cases, simp)
qed
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 th_not_waiting:
"\<not> waiting s th c"
proof -
have "th \<in> readys s"
using runing_ready runing_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
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 distinct_wq': "distinct wq'"
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
by (metis (mono_tags, lifting) distinct.simps(2)
rest_def some_eq_ex wq'_def wq_distinct wq_s_cs)
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 (unfold is_v, simp)
hence "waiting s t c" using assms
by (simp add: cs_waiting_def waiting_eq)
hence "t \<notin> readys s" by (unfold readys_def, auto)
hence "t \<notin> runing s" using runing_ready by auto
with runing_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) is_v by auto
with assms(1) show ?thesis
using cs_waiting_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" using is_v by auto
from assms(2)[unfolded s_holding_def, folded wq_def,
folded this, unfolded wq_def, folded s_holding_def]
show ?thesis .
qed
end
locale valid_trace_v_n = valid_trace_v +
assumes rest_nnl: "rest \<noteq> []"
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
definition "taker = hd wq'"
definition "rest' = tl wq'"
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) cs_waiting_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" using is_v by auto
with assms have "waiting s t c" using cs_waiting_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 cs_waiting_def list.distinct(2) list.sel(1)
list.set_sel(2) rest_def waiting_eq 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" using is_v 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
locale valid_trace_v_e = valid_trace_v +
assumes rest_nil: "rest = []"
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_waiting:
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_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" using is_v by auto
with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
from no_waiting[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" using is_v 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 (* ccc *)
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 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
context valid_trace_v
begin
lemma
"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')
thus ?thesis
qed
qed
qed
qed
end
lemma step_RAG_v: (* ccc *)
assumes vt:
"vt (V th cs#s)"
shows "
RAG (V th cs # 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"
show "(n1, n2) \<in> ?R" sorry
next
fix n1 n2
assume "(n1, n2) \<in> ?R"
show "(n1, n2) \<in> ?L" sorry
qed
text {* (* ddd *)
The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
with the happening of @{text "V"}-events:
*}
lemma step_RAG_v:
assumes vt:
"vt (V th cs#s)"
shows "
RAG (V th cs # 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'}"
apply (insert vt, unfold s_RAG_def)
apply (auto split:if_splits list.splits simp:Let_def)
apply (auto elim: step_v_waiting_mono step_v_hold_inv
step_v_release step_v_wait_inv
step_v_get_hold step_v_release_inv)
apply (erule_tac step_v_not_wait, auto)
done
text {*
The following @{text "step_RAG_p"} lemma charaterizes how @{text "RAG"} is changed
with the happening of @{text "P"}-events:
*}
lemma step_RAG_p:
"vt (P th cs#s) \<Longrightarrow>
RAG (P th cs # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
else RAG s \<union> {(Th th, Cs cs)})"
apply(simp only: s_RAG_def wq_def)
apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
apply(case_tac "csa = cs", auto)
apply(fold wq_def)
apply(drule_tac step_back_step)
apply(ind_cases " step s (P (hd (wq s cs)) cs)")
apply(simp add:s_RAG_def wq_def cs_holding_def)
apply(auto)
done
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
context valid_trace
begin
text {*
The following lemma shows that @{text "RAG"} is acyclic.
The overall structure is by induction on the formation of @{text "vt s"}
and then case analysis on event @{text "e"}, where the non-trivial cases
for those for @{text "V"} and @{text "P"} events.
*}
lemma acyclic_RAG:
shows "acyclic (RAG s)"
using vt
proof(induct)
case (vt_cons s e)
interpret vt_s: valid_trace s using vt_cons(1)
by (unfold_locales, simp)
assume ih: "acyclic (RAG s)"
and stp: "step s e"
and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
with ih
show ?thesis by (simp add:RAG_create_unchanged)
next
case (Exit th)
with ih show ?thesis by (simp add:RAG_exit_unchanged)
next
case (V th cs)
from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_RAG_v [OF this]
have eq_de:
"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 = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
from step_back_step [OF vtt]
have "step s (V th cs)" .
thus ?thesis
proof(cases)
assume "holding s th cs"
hence th_in: "th \<in> set (wq s cs)" and
eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
then obtain rest where
eq_wq: "wq s cs = th#rest"
by (cases "wq s cs", auto)
show ?thesis
proof(cases "rest = []")
case False
let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
from eq_wq False have eq_D: "?D = {(Cs cs, Th ?th')}"
by (unfold next_th_def, auto)
let ?E = "(?A - ?B - ?C)"
have "(Th ?th', Cs cs) \<notin> ?E\<^sup>*"
proof
assume "(Th ?th', Cs cs) \<in> ?E\<^sup>*"
hence " (Th ?th', Cs cs) \<in> ?E\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
from tranclD [OF this]
obtain x where th'_e: "(Th ?th', x) \<in> ?E" by blast
hence th_d: "(Th ?th', x) \<in> ?A" by simp
from RAG_target_th [OF this]
obtain cs' where eq_x: "x = Cs cs'" by auto
with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
hence wt_th': "waiting s ?th' cs'"
unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
hence "cs' = cs"
proof(rule vt_s.waiting_unique)
from eq_wq vt_s.wq_distinct[of cs]
show "waiting s ?th' cs"
apply (unfold s_waiting_def wq_def, auto)
proof -
assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
and eq_wq: "wq_fun (schs s) cs = th # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
with False show "x \<noteq> []" by auto
qed
hence "hd (SOME q. distinct q \<and> set q = set rest) \<in>
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
moreover note hd_in
ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
next
assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest"
with False show "x \<noteq> []" by auto
qed
hence "hd (SOME q. distinct q \<and> set q = set rest) \<in>
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
moreover note hd_in
ultimately show False by auto
qed
qed
with th'_e eq_x have "(Th ?th', Cs cs) \<in> ?E" by simp
with False
show "False" by (auto simp: next_th_def eq_wq)
qed
with acyclic_insert[symmetric] and ac
and eq_de eq_D show ?thesis by auto
next
case True
with eq_wq
have eq_D: "?D = {}"
by (unfold next_th_def, auto)
with eq_de ac
show ?thesis by auto
qed
qed
next
case (P th cs)
from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_RAG_p [OF this] P
have "RAG (e # s) =
(if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else
RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R")
by simp
moreover have "acyclic ?R"
proof(cases "wq s cs = []")
case True
hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp
have "(Th th, Cs cs) \<notin> (RAG s)\<^sup>*"
proof
assume "(Th th, Cs cs) \<in> (RAG s)\<^sup>*"
hence "(Th th, Cs cs) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
from tranclD2 [OF this]
obtain x where "(x, Cs cs) \<in> RAG s" by auto
with True show False by (auto simp:s_RAG_def cs_waiting_def)
qed
with acyclic_insert ih eq_r show ?thesis by auto
next
case False
hence eq_r: "?R = RAG s \<union> {(Th th, Cs cs)}" by simp
have "(Cs cs, Th th) \<notin> (RAG s)\<^sup>*"
proof
assume "(Cs cs, Th th) \<in> (RAG s)\<^sup>*"
hence "(Cs cs, Th th) \<in> (RAG s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
moreover from step_back_step [OF vtt] have "step s (P th cs)" .
ultimately show False
proof -
show " \<lbrakk>(Cs cs, Th th) \<in> (RAG s)\<^sup>+; step s (P th cs)\<rbrakk> \<Longrightarrow> False"
by (ind_cases "step s (P th cs)", simp)
qed
qed
with acyclic_insert ih eq_r show ?thesis by auto
qed
ultimately show ?thesis by simp
next
case (Set thread prio)
with ih
thm RAG_set_unchanged
show ?thesis by (simp add:RAG_set_unchanged)
qed
next
case vt_nil
show "acyclic (RAG ([]::state))"
by (auto simp: s_RAG_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
qed
lemma finite_RAG:
shows "finite (RAG s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
interpret vt_s: valid_trace s using vt_cons(1)
by (unfold_locales, simp)
assume ih: "finite (RAG s)"
and stp: "step s e"
and vt: "vt s"
show ?case
proof(cases e)
case (Create th prio)
with ih
show ?thesis by (simp add:RAG_create_unchanged)
next
case (Exit th)
with ih show ?thesis by (simp add:RAG_exit_unchanged)
next
case (V th cs)
from V vt stp have vtt: "vt (V th cs#s)" by auto
from step_RAG_v [OF this]
have eq_de: "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 = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
moreover from ih have ac: "finite (?A - ?B - ?C)" by simp
moreover have "finite ?D"
proof -
have "?D = {} \<or> (\<exists> a. ?D = {a})"
by (unfold next_th_def, auto)
thus ?thesis
proof
assume h: "?D = {}"
show ?thesis by (unfold h, simp)
next
assume "\<exists> a. ?D = {a}"
thus ?thesis
by (metis finite.simps)
qed
qed
ultimately show ?thesis by simp
next
case (P th cs)
from P vt stp have vtt: "vt (P th cs#s)" by auto
from step_RAG_p [OF this] P
have "RAG (e # s) =
(if wq s cs = [] then RAG s \<union> {(Cs cs, Th th)} else
RAG s \<union> {(Th th, Cs cs)})" (is "?L = ?R")
by simp
moreover have "finite ?R"
proof(cases "wq s cs = []")
case True
hence eq_r: "?R = RAG s \<union> {(Cs cs, Th th)}" by simp
with True and ih show ?thesis by auto
next
case False
hence "?R = RAG s \<union> {(Th th, Cs cs)}" by simp
with False and ih show ?thesis by auto
qed
ultimately show ?thesis by auto
next
case (Set thread prio)
with ih
show ?thesis by (simp add:RAG_set_unchanged)
qed
next
case vt_nil
show "finite (RAG ([]::state))"
by (auto simp: s_RAG_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
qed
qed
text {* Several useful lemmas *}
lemma wf_dep_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
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
by (induct l, auto)
lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
context valid_trace
begin
lemma wq_threads:
assumes h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
from vt and h show ?thesis
proof(induct arbitrary: th cs)
case (vt_cons s e)
interpret vt_s: valid_trace s
using vt_cons(1) by (unfold_locales, auto)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
and vt: "vt s"
and h: "th \<in> set (wq (e # s) cs)"
show ?case
proof(cases e)
case (Create th' prio)
with ih h show ?thesis
by (auto simp:wq_def Let_def)
next
case (Exit th')
with stp ih h show ?thesis
apply (auto simp:wq_def Let_def)
apply (ind_cases "step s (Exit th')")
apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
s_RAG_def s_holding_def cs_holding_def)
done
next
case (V th' cs')
show ?thesis
proof(cases "cs' = cs")
case False
with h
show ?thesis
apply(unfold wq_def V, auto simp:Let_def V split:prod.splits, fold wq_def)
by (drule_tac ih, simp)
next
case True
from h
show ?thesis
proof(unfold V wq_def)
assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
show "th \<in> threads (V th' cs' # s)"
proof(cases "cs = cs'")
case False
hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
with th_in have " th \<in> set (wq s cs)"
by (fold wq_def, simp)
from ih [OF this] show ?thesis by simp
next
case True
show ?thesis
proof(cases "wq_fun (schs s) cs'")
case Nil
with h V show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
by (fold wq_def, drule_tac ih, simp)
next
case (Cons a rest)
assume eq_wq: "wq_fun (schs s) cs' = a # rest"
with h V show ?thesis
apply (auto simp:Let_def wq_def split:if_splits)
proof -
assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
qed
with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
from ih[OF this[folded wq_def]] show "th \<in> threads s" .
next
assume th_in: "th \<in> set (wq_fun (schs s) cs)"
from ih[OF this[folded wq_def]]
show "th \<in> threads s" .
qed
qed
qed
qed
qed
next
case (P th' cs')
from h stp
show ?thesis
apply (unfold P wq_def)
apply (auto simp:Let_def split:if_splits, fold wq_def)
apply (auto intro:ih)
apply(ind_cases "step s (P th' cs')")
by (unfold runing_def readys_def, auto)
next
case (Set thread prio)
with ih h show ?thesis
by (auto simp:wq_def Let_def)
qed
next
case vt_nil
thus ?case by (auto simp:wq_def)
qed
qed
lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
proof -
from assms show ?thesis
apply (auto simp:readys_def)
apply(simp add:s_waiting_def[folded wq_def])
apply (erule_tac x = csa in allE)
apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
apply (case_tac "csa = cs", simp)
apply (erule_tac x = cs in allE)
apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
apply(auto simp add: wq_def)
apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
proof -
assume th_nin: "th \<notin> set rest"
and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
and eq_wq: "wq_fun (schs s) cs = thread # rest"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
with th_nin th_in show False by auto
qed
qed
text {* \noindent
The following lemmas shows that: starting from any node in @{text "RAG"},
by chasing out-going edges, it is always possible to reach a node representing a ready
thread. In this lemma, it is the @{text "th'"}.
*}
lemma chain_building:
shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
proof -
from wf_dep_converse
have h: "wf ((RAG s)\<inverse>)" .
show ?thesis
proof(induct rule:wf_induct [OF h])
fix x
assume ih [rule_format]:
"\<forall>y. (y, x) \<in> (RAG s)\<inverse> \<longrightarrow>
y \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (y, Th th') \<in> (RAG s)\<^sup>+)"
show "x \<in> Domain (RAG s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+)"
proof
assume x_d: "x \<in> Domain (RAG s)"
show "\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (RAG s)\<^sup>+"
proof(cases x)
case (Th th)
from x_d Th obtain cs where x_in: "(Th th, Cs cs) \<in> RAG s" by (auto simp:s_RAG_def)
with Th have x_in_r: "(Cs cs, x) \<in> (RAG s)^-1" by simp
from th_chasing [OF x_in] obtain th' where "(Cs cs, Th th') \<in> RAG s" by blast
hence "Cs cs \<in> Domain (RAG s)" by auto
from ih [OF x_in_r this] obtain th'
where th'_ready: " th' \<in> readys s" and cs_in: "(Cs cs, Th th') \<in> (RAG s)\<^sup>+" by auto
have "(x, Th th') \<in> (RAG s)\<^sup>+" using Th x_in cs_in by auto
with th'_ready show ?thesis by auto
next
case (Cs cs)
from x_d Cs obtain th' where th'_d: "(Th th', x) \<in> (RAG s)^-1" by (auto simp:s_RAG_def)
show ?thesis
proof(cases "th' \<in> readys s")
case True
from True and th'_d show ?thesis by auto
next
case False
from th'_d and range_in have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (RAG s)"
by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
obtain th'' where
th''_r: "th'' \<in> readys s" and
th''_in: "(Th th', Th th'') \<in> (RAG s)\<^sup>+" by auto
from th'_d and th''_in
have "(x, Th th'') \<in> (RAG s)\<^sup>+" by auto
with th''_r show ?thesis by auto
qed
qed
qed
qed
qed
text {* \noindent
The following is just an instance of @{text "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 cs_waiting_def Domain_def)
from chain_building [rule_format, OF this]
show ?thesis by auto
qed
end
lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
by (unfold s_holding_def cs_holding_def, auto)
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 holding_unique)
end
lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)
context valid_trace
begin
lemma dchain_unique:
assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (RAG s)^+"
and th2_r: "th2 \<in> readys s"
shows "th1 = th2"
proof -
{ assume neq: "th1 \<noteq> th2"
hence "Th th1 \<noteq> Th th2" by simp
from unique_chain [OF _ th1_d th2_d this] and unique_RAG
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
hence "False"
proof
assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+"
from trancl_split [OF this]
obtain n where dd: "(Th th1, n) \<in> RAG s" by auto
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th1 \<notin> readys s"
by (auto simp:readys_def s_RAG_def wq_def s_waiting_def cs_waiting_def)
with th1_r show ?thesis by auto
next
assume "(Th th2, Th th1) \<in> (RAG s)\<^sup>+"
from trancl_split [OF this]
obtain n where dd: "(Th th2, n) \<in> RAG s" by auto
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
from dd eq_n have "th2 \<notin> readys s"
by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
with th2_r show ?thesis by auto
qed
} thus ?thesis by auto
qed
end
lemma step_holdents_p_add:
assumes vt: "vt (P th cs#s)"
and "wq s cs = []"
shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
proof -
from assms show ?thesis
unfolding holdents_test step_RAG_p[OF vt] by (auto)
qed
lemma step_holdents_p_eq:
assumes vt: "vt (P th cs#s)"
and "wq s cs \<noteq> []"
shows "holdents (P th cs#s) th = holdents s th"
proof -
from assms show ?thesis
unfolding holdents_test step_RAG_p[OF vt] by auto
qed
lemma (in valid_trace) finite_holding :
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
from finite_RAG
have "finite (RAG s)" .
hence "finite (?F `(RAG s))" by simp
moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>"
proof -
{ have h: "\<And> a A f. a \<in> A \<Longrightarrow> f a \<in> f ` A" by auto
fix x assume "(Cs x, Th th) \<in> RAG s"
hence "?F (Cs x, Th th) \<in> ?F `(RAG s)" by (rule h)
moreover have "?F (Cs x, Th th) = x" by simp
ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` RAG s" by simp
} thus ?thesis by auto
qed
ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset)
qed
lemma cntCS_v_dec:
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
from vtv interpret vt_s: valid_trace s
by (cases, unfold_locales, simp)
from vtv interpret vt_v: valid_trace "V thread cs#s"
by (unfold_locales, simp)
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_test s_RAG_def, simp)
by (unfold cs_holding_def s_holding_def wq_def, auto)
moreover have cs_not_in:
"(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
apply (insert vt_s.wq_distinct[of cs])
apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
auto simp:next_th_def)
proof -
fix rest
assume dst: "distinct (rest::thread list)"
and ne: "rest \<noteq> []"
and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from dst show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
set (SOME q. distinct q \<and> set q = set rest)" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from dst show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume " distinct x \<and> set x = set rest" with ne
show "x \<noteq> []" by auto
qed
ultimately
show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s"
by auto
next
fix rest
assume dst: "distinct (rest::thread list)"
and ne: "rest \<noteq> []"
and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from dst show "distinct rest \<and> set rest = set rest" by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
set (SOME q. distinct q \<and> set q = set rest)" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from dst show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume " distinct x \<and> set x = set rest" with ne
show "x \<noteq> []" by auto
qed
ultimately show "False" by auto
qed
ultimately
have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
by auto
moreover have "card \<dots> =
Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
proof(rule card_insert)
from vt_v.finite_holding
show " finite (holdents (V thread cs # s) thread)" .
qed
moreover from cs_not_in
have "cs \<notin> (holdents (V thread cs#s) thread)" by auto
ultimately show ?thesis by (simp add:cntCS_def)
qed
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_diff_inv:
assumes "cntP (e#s) th \<noteq> cntP s th"
shows "isP e \<and> actor e = th"
proof(cases e)
case (P th' pty)
show ?thesis
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"
shows "isV e \<and> actor e = th"
proof(cases e)
case (V th' pty)
show ?thesis
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)
context valid_trace
begin
text {* (* ddd *) \noindent
The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
of one particular thread.
*}
lemma cnp_cnv_cncs:
shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
then cntCS s th else cntCS s th + 1)"
proof -
from vt show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e)
interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. cntP s th = cntV s th +
(if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
and stp: "step s e"
from stp show ?case
proof(cases)
case (thread_create thread prio)
assume eq_e: "e = Create thread prio"
and not_in: "thread \<notin> threads s"
show ?thesis
proof -
{ fix cs
assume "thread \<in> set (wq s cs)"
from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
with not_in have "False" by simp
} with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
by (auto simp:readys_def threads.simps s_waiting_def
wq_def cs_waiting_def Let_def)
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
unfolding cntCS_def holdents_test
by (simp add:RAG_create_unchanged eq_e)
{ assume "th \<noteq> thread"
with eq_readys eq_e
have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) =
(th \<in> readys (s) \<or> th \<notin> threads (s))"
by (simp add:threads.simps)
with eq_cnp eq_cnv eq_cncs ih not_in
have ?thesis by simp
} moreover {
assume eq_th: "th = thread"
with not_in ih have " cntP s th = cntV s th + cntCS s th" by simp
moreover from eq_th and eq_readys have "th \<in> readys (e#s)" by simp
moreover note eq_cnp eq_cnv eq_cncs
ultimately have ?thesis by auto
} ultimately show ?thesis by blast
qed
next
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and is_runing: "thread \<in> runing s"
and no_hold: "holdents s thread = {}"
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
unfolding cntCS_def holdents_test
by (simp add:RAG_exit_unchanged eq_e)
{ assume "th \<noteq> thread"
with eq_e
have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) =
(th \<in> readys (s) \<or> th \<notin> threads (s))"
apply (simp add:threads.simps readys_def)
apply (subst s_waiting_def)
apply (simp add:Let_def)
apply (subst s_waiting_def, simp)
done
with eq_cnp eq_cnv eq_cncs ih
have ?thesis by simp
} moreover {
assume eq_th: "th = thread"
with ih is_runing have " cntP s th = cntV s th + cntCS s th"
by (simp add:runing_def)
moreover from eq_th eq_e have "th \<notin> threads (e#s)"
by simp
moreover note eq_cnp eq_cnv eq_cncs
ultimately have ?thesis by auto
} ultimately show ?thesis by blast
next
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
then interpret vt_p: valid_trace "(P thread cs#s)"
by (unfold_locales, simp)
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
assume neq_th: "th \<noteq> thread"
with eq_e
have eq_readys: "(th \<in> readys (e#s)) = (th \<in> readys (s))"
apply (simp add:readys_def s_waiting_def wq_def Let_def)
apply (rule_tac hh)
apply (intro iffI allI, clarify)
apply (erule_tac x = csa in allE, auto)
apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
apply (erule_tac x = cs in allE, auto)
by (case_tac "(wq_fun (schs s) cs)", auto)
moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
apply (simp add:cntCS_def holdents_test)
by (unfold step_RAG_p [OF vtp], auto)
moreover from eq_e neq_th have "cntP (e # s) th = cntP s th"
by (simp add:cntP_def count_def)
moreover from eq_e neq_th have "cntV (e#s) th = cntV s th"
by (simp add:cntV_def count_def)
moreover from eq_e neq_th have "threads (e#s) = threads s" by simp
moreover note ih [of th]
ultimately have ?thesis by simp
} moreover {
assume eq_th: "th = thread"
have ?thesis
proof -
from eq_e eq_th have eq_cnp: "cntP (e # s) th = 1 + (cntP s th)"
by (simp add:cntP_def count_def)
from eq_e eq_th have eq_cnv: "cntV (e#s) th = cntV s th"
by (simp add:cntV_def count_def)
show ?thesis
proof (cases "wq s cs = []")
case True
with is_runing
have "th \<in> readys (e#s)"
apply (unfold eq_e wq_def, unfold readys_def s_RAG_def)
apply (simp add: wq_def[symmetric] runing_def eq_th s_waiting_def)
by (auto simp:readys_def wq_def Let_def s_waiting_def wq_def)
moreover have "cntCS (e # s) th = 1 + cntCS s th"
proof -
have "card {csa. csa = cs \<or> (Cs csa, Th thread) \<in> RAG s} =
Suc (card {cs. (Cs cs, Th thread) \<in> RAG s})" (is "card ?L = Suc (card ?R)")
proof -
have "?L = insert cs ?R" by auto
moreover have "card \<dots> = Suc (card (?R - {cs}))"
proof(rule card_insert)
from vt_s.finite_holding [of thread]
show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
by (unfold holdents_test, simp)
qed
moreover have "?R - {cs} = ?R"
proof -
have "cs \<notin> ?R"
proof
assume "cs \<in> {cs. (Cs cs, Th thread) \<in> RAG s}"
with no_dep show False by auto
qed
thus ?thesis by auto
qed
ultimately show ?thesis by auto
qed
thus ?thesis
apply (unfold eq_e eq_th cntCS_def)
apply (simp add: holdents_test)
by (unfold step_RAG_p [OF vtp], auto simp:True)
qed
moreover from is_runing have "th \<in> readys s"
by (simp add:runing_def eq_th)
moreover note eq_cnp eq_cnv ih [of th]
ultimately show ?thesis by auto
next
case False
have eq_wq: "wq (e#s) cs = wq s cs @ [th]"
by (unfold eq_th eq_e wq_def, auto simp:Let_def)
have "th \<notin> readys (e#s)"
proof
assume "th \<in> readys (e#s)"
hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def)
from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" .
hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)"
by (simp add:s_waiting_def wq_def)
moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
hence "th = hd (wq s cs)" using False by auto
with False eq_wq vt_p.wq_distinct [of cs]
show False by (fold eq_e, auto)
qed
moreover from is_runing have "th \<in> threads (e#s)"
by (unfold eq_e, auto simp:runing_def readys_def eq_th)
moreover have "cntCS (e # s) th = cntCS s th"
apply (unfold cntCS_def holdents_test eq_e step_RAG_p[OF vtp])
by (auto simp:False)
moreover note eq_cnp eq_cnv ih[of th]
moreover from is_runing have "th \<in> readys s"
by (simp add:runing_def eq_th)
ultimately show ?thesis by auto
qed
qed
} ultimately show ?thesis by blast
qed
next
case (thread_V thread cs)
from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
from vt_v.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest"
by (metis distinct.simps(2) vt_s.wq_distinct)
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
qed
show ?thesis
proof -
{ assume eq_th: "th = thread"
from eq_th have eq_cnp: "cntP (e # s) th = cntP s th"
by (unfold eq_e, simp add:cntP_def count_def)
moreover from eq_th have eq_cnv: "cntV (e#s) th = 1 + cntV s th"
by (unfold eq_e, simp add:cntV_def count_def)
moreover from cntCS_v_dec [OF vtv]
have "cntCS (e # s) thread + 1 = cntCS s thread"
by (simp add:eq_e)
moreover from is_runing have rd_before: "thread \<in> readys s"
by (unfold runing_def, simp)
moreover have "thread \<in> readys (e # s)"
proof -
from is_runing
have "thread \<in> threads (e#s)"
by (unfold eq_e, auto simp:runing_def readys_def)
moreover have "\<forall> cs1. \<not> waiting (e#s) thread cs1"
proof
fix cs1
{ assume eq_cs: "cs1 = cs"
have "\<not> waiting (e # s) thread cs1"
proof -
from eq_wq
have "thread \<notin> set (wq (e#s) cs1)"
apply(unfold eq_e wq_def eq_cs s_holding_def)
apply (auto simp:Let_def)
proof -
assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
with eq_set have "thread \<in> set rest" by simp
with vt_v.wq_distinct[of cs]
and eq_wq show False
by (metis distinct.simps(2) vt_s.wq_distinct)
qed
thus ?thesis by (simp add:wq_def s_waiting_def)
qed
} moreover {
assume neq_cs: "cs1 \<noteq> cs"
have "\<not> waiting (e # s) thread cs1"
proof -
from wq_v_neq [OF neq_cs[symmetric]]
have "wq (V thread cs # s) cs1 = wq s cs1" .
moreover have "\<not> waiting s thread cs1"
proof -
from runing_ready and is_runing
have "thread \<in> readys s" by auto
thus ?thesis by (simp add:readys_def)
qed
ultimately show ?thesis
by (auto simp:wq_def s_waiting_def eq_e)
qed
} ultimately show "\<not> waiting (e # s) thread cs1" by blast
qed
ultimately show ?thesis by (simp add:readys_def)
qed
moreover note eq_th ih
ultimately have ?thesis by auto
} moreover {
assume neq_th: "th \<noteq> thread"
from neq_th eq_e have eq_cnp: "cntP (e # s) th = cntP s th"
by (simp add:cntP_def count_def)
from neq_th eq_e have eq_cnv: "cntV (e # s) th = cntV s th"
by (simp add:cntV_def count_def)
have ?thesis
proof(cases "th \<in> set rest")
case False
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
apply (insert step_back_vt[OF vtv])
by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
moreover have "cntCS (e#s) th = cntCS s th"
apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
proof -
have "{csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} =
{cs. (Cs cs, Th th) \<in> RAG s}"
proof -
from False eq_wq
have " next_th s thread cs th \<Longrightarrow> (Cs cs, Th th) \<in> RAG s"
apply (unfold next_th_def, auto)
proof -
assume ne: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
and eq_wq: "wq s cs = thread # rest"
from eq_set ni have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
set (SOME q. distinct q \<and> set q = set rest)
" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from vt_s.wq_distinct[ of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest"
with ne show "x \<noteq> []" by auto
qed
ultimately show
"(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> RAG s"
by auto
qed
thus ?thesis by auto
qed
thus "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} =
card {cs. (Cs cs, Th th) \<in> RAG s}" by simp
qed
moreover note ih eq_cnp eq_cnv eq_threads
ultimately show ?thesis by auto
next
case True
assume th_in: "th \<in> set rest"
show ?thesis
proof(cases "next_th s thread cs th")
case False
with eq_wq and th_in have
neq_hd: "th \<noteq> hd (SOME q. distinct q \<and> set q = set rest)" (is "th \<noteq> hd ?rest")
by (auto simp:next_th_def)
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
proof -
from eq_wq and th_in
have "\<not> th \<in> readys s"
apply (auto simp:readys_def s_waiting_def)
apply (rule_tac x = cs in exI, auto)
by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
apply (auto simp:readys_def s_waiting_def eq_e wq_def Let_def split:list.splits)
by (rule_tac x = cs in exI, auto simp:eq_set)
ultimately show ?thesis by auto
qed
moreover have "cntCS (e#s) th = cntCS s th"
proof -
from eq_wq and th_in and neq_hd
have "(holdents (e # s) th) = (holdents s th)"
apply (unfold eq_e step_RAG_v[OF vtv],
auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def
Let_def cs_holding_def)
by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
thus ?thesis by (simp add:cntCS_def)
qed
moreover note ih eq_cnp eq_cnv eq_threads
ultimately show ?thesis by auto
next
case True
let ?rest = " (SOME q. distinct q \<and> set q = set rest)"
let ?t = "hd ?rest"
from True eq_wq th_in neq_th
have "th \<in> readys (e # s)"
apply (auto simp:eq_e readys_def s_waiting_def wq_def
Let_def next_th_def)
proof -
assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
show "?t \<in> threads s"
proof(rule vt_s.wq_threads)
from eq_wq and t_in
show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
qed
next
fix csa
assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
and neq_cs: "csa \<noteq> cs"
and t_in': "?t \<in> set (wq_fun (schs s) csa)"
show "?t = hd (wq_fun (schs s) csa)"
proof -
{ assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
from vt_s.wq_distinct[of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto
with eq_wq and t_in
have w1: "waiting s ?t cs"
by (auto simp:s_waiting_def wq_def)
from t_in' neq_hd'
have w2: "waiting s ?t csa"
by (auto simp:s_waiting_def wq_def)
from vt_s.waiting_unique[OF w1 w2]
and neq_cs have "False" by auto
} thus ?thesis by auto
qed
qed
moreover have "cntP s th = cntV s th + cntCS s th + 1"
proof -
have "th \<notin> readys s"
proof -
from True eq_wq neq_th th_in
show ?thesis
apply (unfold readys_def s_waiting_def, auto)
by (rule_tac x = cs in exI, auto simp add: wq_def)
qed
moreover have "th \<in> threads s"
proof -
from th_in eq_wq
have "th \<in> set (wq s cs)" by simp
from vt_s.wq_threads [OF this]
show ?thesis .
qed
ultimately show ?thesis using ih by auto
qed
moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th"
apply (unfold cntCS_def holdents_test eq_e step_RAG_v[OF vtv], auto)
proof -
show "card {csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs} =
Suc (card {cs. (Cs cs, Th th) \<in> RAG s})"
(is "card ?A = Suc (card ?B)")
proof -
have "?A = insert cs ?B" by auto
hence "card ?A = card (insert cs ?B)" by simp
also have "\<dots> = Suc (card ?B)"
proof(rule card_insert_disjoint)
have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)"
apply (auto simp:image_def)
by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
with vt_s.finite_RAG
show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
next
show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
proof
assume "cs \<in> {cs. (Cs cs, Th th) \<in> RAG s}"
hence "(Cs cs, Th th) \<in> RAG s" by simp
with True neq_th eq_wq show False
by (auto simp:next_th_def s_RAG_def cs_holding_def)
qed
qed
finally show ?thesis .
qed
qed
moreover note eq_cnp eq_cnv
ultimately show ?thesis by simp
qed
qed
} ultimately show ?thesis by blast
qed
next
case (thread_set thread prio)
assume eq_e: "e = Set thread prio"
and is_runing: "thread \<in> runing s"
show ?thesis
proof -
from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
have eq_cncs: "cntCS (e#s) th = cntCS s th"
unfolding cntCS_def holdents_test
by (simp add:RAG_set_unchanged eq_e)
from eq_e have eq_readys: "readys (e#s) = readys s"
by (simp add:readys_def cs_waiting_def s_waiting_def wq_def,
auto simp:Let_def)
{ assume "th \<noteq> thread"
with eq_readys eq_e
have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) =
(th \<in> readys (s) \<or> th \<notin> threads (s))"
by (simp add:threads.simps)
with eq_cnp eq_cnv eq_cncs ih is_runing
have ?thesis by simp
} moreover {
assume eq_th: "th = thread"
with is_runing ih have " cntP s th = cntV s th + cntCS s th"
by (unfold runing_def, auto)
moreover from eq_th and eq_readys is_runing have "th \<in> readys (e#s)"
by (simp add:runing_def)
moreover note eq_cnp eq_cnv eq_cncs
ultimately have ?thesis by auto
} ultimately show ?thesis by blast
qed
qed
next
case vt_nil
show ?case
by (unfold cntP_def cntV_def cntCS_def,
auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
qed
qed
lemma not_thread_cncs:
assumes not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
interpret vt_s: valid_trace s using vt_cons(1)
by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
from stp show ?case
proof(cases)
case (thread_create thread prio)
assume eq_e: "e = Create thread prio"
and not_in': "thread \<notin> threads s"
have "cntCS (e # s) th = cntCS s th"
apply (unfold eq_e cntCS_def holdents_test)
by (simp add:RAG_create_unchanged)
moreover have "th \<notin> threads s"
proof -
from not_in eq_e show ?thesis by simp
qed
moreover note ih ultimately show ?thesis by auto
next
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and nh: "holdents s thread = {}"
have eq_cns: "cntCS (e # s) th = cntCS s th"
apply (unfold eq_e cntCS_def holdents_test)
by (simp add:RAG_exit_unchanged)
show ?thesis
proof(cases "th = thread")
case True
have "cntCS s th = 0" by (unfold cntCS_def, auto simp:nh True)
with eq_cns show ?thesis by simp
next
case False
with not_in and eq_e
have "th \<notin> threads s" by simp
from ih[OF this] and eq_cns show ?thesis by simp
qed
next
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
from assms thread_P ih vt stp thread_P have vtp: "vt (P thread cs#s)" by auto
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
moreover from is_runing have "thread \<in> threads s"
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
hence "cntCS (e # s) th = cntCS s th "
apply (unfold cntCS_def holdents_test eq_e)
by (unfold step_RAG_p[OF vtp], auto)
moreover have "cntCS s th = 0"
proof(rule ih)
from not_in eq_e show "th \<notin> threads s" by simp
qed
ultimately show ?thesis by simp
next
case (thread_V thread cs)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
moreover from is_runing have "thread \<in> threads s"
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
from assms thread_V vt stp ih
have vtv: "vt (V thread cs#s)" by auto
then interpret vt_v: valid_trace "(V thread cs#s)"
by (unfold_locales, simp)
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
from not_in eq_e eq_wq
have "\<not> next_th s thread cs th"
apply (auto simp:next_th_def)
proof -
assume ne: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
have "?t \<in> set rest"
proof(rule someI2)
from vt_v.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest"
by (metis distinct.simps(2) vt_s.wq_distinct)
next
fix x assume "distinct x \<and> set x = set rest" with ne
show "hd x \<in> set rest" by (cases x, auto)
qed
with eq_wq have "?t \<in> set (wq s cs)" by simp
from vt_s.wq_threads[OF this] and ni
show False
using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)`
ni vt_s.wq_threads by blast
qed
moreover note neq_th eq_wq
ultimately have "cntCS (e # s) th = cntCS s th"
by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
moreover have "cntCS s th = 0"
proof(rule ih)
from not_in eq_e show "th \<notin> threads s" by simp
qed
ultimately show ?thesis by simp
next
case (thread_set thread prio)
print_facts
assume eq_e: "e = Set thread prio"
and is_runing: "thread \<in> runing s"
from not_in and eq_e have "th \<notin> threads s" by auto
from ih [OF this] and eq_e
show ?thesis
apply (unfold eq_e cntCS_def holdents_test)
by (simp add:RAG_set_unchanged)
qed
next
case vt_nil
show ?case
by (unfold cntCS_def,
auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
qed
qed
end
context valid_trace
begin
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 from RAG_target_th[OF this] obtain cs where "n = Cs cs" by 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:cs_waiting_def)
from wq_threads [OF this] show ?thesis .
qed
end
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
thm cpreced_initial
apply(simp add: Let_def cpreced_initial)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
done
context valid_trace
begin
lemma runing_unique:
assumes runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
proof -
from runing_1 and runing_2 have "cp s th1 = cp s th2"
unfolding runing_def
apply(simp)
done
hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
(is "Max (?f ` ?A) = Max (?f ` ?B)")
unfolding cp_eq_cpreced
unfolding cpreced_def .
obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
proof -
have h1: "finite (?f ` ?A)"
proof -
have "finite ?A"
proof -
have "finite (dependants (wq s) th1)"
proof-
have "finite {th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
apply (auto simp:image_def)
by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
moreover have "finite \<dots>"
proof -
from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
thus ?thesis by auto
qed
moreover have h2: "(?f ` ?A) \<noteq> {}"
proof -
have "?A \<noteq> {}" by simp
thus ?thesis by simp
qed
from Max_in [OF h1 h2]
have "Max (?f ` ?A) \<in> (?f ` ?A)" .
thus ?thesis
thm cpreced_def
unfolding cpreced_def[symmetric]
unfolding cp_eq_cpreced[symmetric]
unfolding cpreced_def
using that[intro] by (auto)
qed
obtain th2' where th2_in: "th2' \<in> ?B" and eq_f_th2: "?f th2' = Max (?f ` ?B)"
proof -
have h1: "finite (?f ` ?B)"
proof -
have "finite ?B"
proof -
have "finite (dependants (wq s) th2)"
proof-
have "finite {th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
apply (auto simp:image_def)
by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
moreover have "finite \<dots>"
proof -
from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
thus ?thesis by auto
qed
moreover have h2: "(?f ` ?B) \<noteq> {}"
proof -
have "?B \<noteq> {}" by simp
thus ?thesis by simp
qed
from Max_in [OF h1 h2]
have "Max (?f ` ?B) \<in> (?f ` ?B)" .
thus ?thesis by (auto intro:that)
qed
from eq_f_th1 eq_f_th2 eq_max
have eq_preced: "preced th1' s = preced th2' s" by auto
hence eq_th12: "th1' = th2'"
proof (rule preced_unique)
from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp
thus "th1' \<in> threads s"
proof
assume "th1' \<in> dependants (wq s) th1"
hence "(Th th1') \<in> Domain ((RAG s)^+)"
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
from dm_RAG_threads[OF this] show ?thesis .
next
assume "th1' = th1"
with runing_1 show ?thesis
by (unfold runing_def readys_def, auto)
qed
next
from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp
thus "th2' \<in> threads s"
proof
assume "th2' \<in> dependants (wq s) th2"
hence "(Th th2') \<in> Domain ((RAG s)^+)"
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
from dm_RAG_threads[OF this] show ?thesis .
next
assume "th2' = th2"
with runing_2 show ?thesis
by (unfold runing_def readys_def, auto)
qed
qed
from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp
thus ?thesis
proof
assume eq_th': "th1' = th1"
from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp
next
assume "th2' \<in> dependants (wq s) th2"
with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp
hence "(Th th1, Th th2) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
hence "Th th1 \<in> Domain ((RAG s)^+)"
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "Th th1 \<in> Domain (RAG s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th1, n) \<in> RAG s" by (auto simp:Domain_def)
from RAG_target_th [OF this]
obtain cs' where "n = Cs cs'" by auto
with d have "(Th th1, Cs cs') \<in> RAG s" by simp
with runing_1 have "False"
apply (unfold runing_def readys_def s_RAG_def)
by (auto simp:waiting_eq)
thus ?thesis by simp
qed
next
assume th1'_in: "th1' \<in> dependants (wq s) th1"
from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2"
with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp
hence "(Th th2, Th th1) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
hence "Th th2 \<in> Domain ((RAG s)^+)"
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "Th th2 \<in> Domain (RAG s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th2, n) \<in> RAG s" by (auto simp:Domain_def)
from RAG_target_th [OF this]
obtain cs' where "n = Cs cs'" by auto
with d have "(Th th2, Cs cs') \<in> RAG s" by simp
with runing_2 have "False"
apply (unfold runing_def readys_def s_RAG_def)
by (auto simp:waiting_eq)
thus ?thesis by simp
next
assume "th2' \<in> dependants (wq s) th2"
with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp
hence h1: "(Th th1', Th th2) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
show ?thesis
proof(rule dchain_unique[OF h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
qed
qed
qed
qed
lemma "card (runing s) \<le> 1"
apply(subgoal_tac "finite (runing s)")
prefer 2
apply (metis finite_nat_set_iff_bounded lessI runing_unique)
apply(rule ccontr)
apply(simp)
apply(case_tac "Suc (Suc 0) \<le> card (runing s)")
apply(subst (asm) card_le_Suc_iff)
apply(simp)
apply(auto)[1]
apply (metis insertCI runing_unique)
apply(auto)
done
end
lemma create_pre:
assumes stp: "step s e"
and not_in: "th \<notin> threads s"
and is_in: "th \<in> threads (e#s)"
obtains prio where "e = Create th prio"
proof -
from assms
show ?thesis
proof(cases)
case (thread_create thread prio)
with is_in not_in have "e = Create th prio" by simp
from that[OF this] show ?thesis .
next
case (thread_exit thread)
with assms show ?thesis by (auto intro!:that)
next
case (thread_P thread)
with assms show ?thesis by (auto intro!:that)
next
case (thread_V thread)
with assms show ?thesis by (auto intro!:that)
next
case (thread_set thread)
with assms show ?thesis by (auto intro!:that)
qed
qed
context valid_trace
begin
lemma cnp_cnv_eq:
assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
using assms
using cnp_cnv_cncs not_thread_cncs by auto
end
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
context valid_trace
begin
lemma count_eq_dependants:
assumes eq_pv: "cntP s th = cntV s th"
shows "dependants (wq s) th = {}"
proof -
from cnp_cnv_cncs and eq_pv
have "cntCS s th = 0"
by (auto split:if_splits)
moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
proof -
from finite_holding[of th] show ?thesis
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
by (unfold cntCS_def holdents_test cs_dependants_def, auto)
show ?thesis
proof(unfold cs_dependants_def)
{ assume "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}"
then obtain th' where "(Th th', Th th) \<in> (RAG (wq s))\<^sup>+" by auto
hence "False"
proof(cases)
assume "(Th th', Th th) \<in> RAG (wq s)"
thus "False" by (auto simp:cs_RAG_def)
next
fix c
assume "(c, Th th) \<in> RAG (wq s)"
with h and eq_RAG show "False"
by (cases c, auto simp:cs_RAG_def)
qed
} thus "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} = {}" by auto
qed
qed
lemma dependants_threads:
shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (RAG (wq s))\<^sup>+}"
have "Th th \<in> Domain (RAG s)"
proof -
from h obtain th' where "(Th th, Th th') \<in> (RAG (wq s))\<^sup>+" by auto
hence "(Th th) \<in> Domain ( (RAG (wq s))\<^sup>+)" by (auto simp:Domain_def)
with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
thus ?thesis using eq_RAG by simp
qed
from dm_RAG_threads[OF this]
have "th \<in> threads s" .
} note hh = this
fix th1
assume "th1 \<in> dependants (wq s) th"
hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (RAG (wq s))\<^sup>+}"
by (unfold cs_dependants_def, simp)
from hh [OF this] show "th1 \<in> threads s" .
qed
lemma finite_threads:
shows "finite (threads s)"
using vt by (induct) (auto elim: step.cases)
end
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
context valid_trace
begin
lemma cp_le:
assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
\<le> Max ((\<lambda>th. preced th s) ` threads s)"
(is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
proof(rule Max_f_mono)
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
next
from finite_threads
show "finite (threads s)" .
next
from th_in
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
apply (rule_tac dm_RAG_threads)
apply (unfold trancl_domain [of "RAG s", symmetric])
by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (priority th s) (last_set th s)
\<le> Max (insert (Prc (priority th s) (last_set th s))
((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
(is "?l \<le> Max (insert ?l ?A)")
proof(cases "?A = {}")
case False
have "finite ?A" (is "finite (?f ` ?B)")
proof -
have "finite ?B"
proof-
have "finite {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
apply (auto simp:image_def)
by (rule_tac x = "(Th x, Th th)" in bexI, auto)
moreover have "finite \<dots>"
proof -
from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependants_def)
qed
thus ?thesis by simp
qed
from Max_insert [OF this False, of ?l] show ?thesis by auto
next
case True
thus ?thesis by auto
qed
qed
lemma max_cp_eq:
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
case True
thus ?thesis by auto
next
case False
have "?l \<in> ((cp s) ` threads s)"
proof(rule Max_in)
from finite_threads
show "finite (cp s ` threads s)" by auto
next
from False show "cp s ` threads s \<noteq> {}" by auto
qed
then obtain th
where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
proof -
have "?r \<in> (?f ` ?A)"
proof(rule Max_in)
from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
qed
then obtain th' where
th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
from le_cp [of th'] eq_r
have "?r \<le> cp s th'" by auto
moreover have "\<dots> \<le> cp s th"
proof(fold eq_l)
show " cp s th' \<le> Max (cp s ` threads s)"
proof(rule Max_ge)
from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
next
from finite_threads
show "finite (cp s ` threads s)" by auto
qed
qed
ultimately show ?thesis by auto
qed
ultimately show ?thesis using eq_l by auto
qed
lemma max_cp_readys_threads_pre:
assumes np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(unfold max_cp_eq)
show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
proof -
let ?p = "Max ((\<lambda>th. preced th s) ` threads s)"
let ?f = "(\<lambda>th. preced th s)"
have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
proof(rule Max_in)
from finite_threads show "finite (?f ` threads s)" by simp
next
from np show "?f ` threads s \<noteq> {}" by simp
qed
then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
by (auto simp:Image_def)
from th_chain_to_ready [OF tm_in]
have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
thus ?thesis
proof
assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+ "
then obtain th' where th'_in: "th' \<in> readys s"
and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
from dependants_threads finite_threads
show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
from p_in and th'_in and dependants_threads[of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
ultimately show "p \<le> preced tm s" by auto
next
show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
proof -
from tm_chain
have "tm \<in> dependants (wq s) th'"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, auto)
thus ?thesis by auto
qed
qed
with tm_max
have h: "cp s th' = Max ((\<lambda>th. preced th s) ` threads s)" by simp
show ?thesis
proof (fold h, rule Max_eqI)
fix q
assume "q \<in> cp s ` readys s"
then obtain th1 where th1_in: "th1 \<in> readys s"
and eq_q: "q = cp s th1" by auto
show "q \<le> cp s th'"
apply (unfold h eq_q)
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
from dependants_threads [of th1] th1_in
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
next
from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
from th'_in
show "cp s th' \<in> cp s ` readys s" by simp
qed
next
assume tm_ready: "tm \<in> readys s"
show ?thesis
proof(fold tm_max)
have cp_eq_p: "cp s tm = preced tm s"
proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
fix y
assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
show "y \<le> preced tm s"
proof -
{ fix y'
assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
from hy' dependants_threads[of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
} with hy show ?thesis by auto
qed
next
from dependants_threads[of tm] finite_threads
show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
by simp
qed
moreover have "Max (cp s ` readys s) = cp s tm"
proof(rule Max_eqI)
from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
next
from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
fix y assume "y \<in> cp s ` readys s"
then obtain th1 where th1_readys: "th1 \<in> readys s"
and h: "y = cp s th1" by auto
show "y \<le> cp s tm"
apply(unfold cp_eq_p h)
apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
proof -
from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
from dependants_threads[of th1] th1_readys
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
qed
ultimately show " Max (cp s ` readys s) = preced tm s" by simp
qed
qed
qed
qed
text {* (* ccc *) \noindent
Since the current precedence of the threads in ready queue will always be boosted,
there must be one inside it has the maximum precedence of the whole system.
*}
lemma max_cp_readys_threads:
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
thus ?thesis
by (auto simp:readys_def)
next
case False
show ?thesis by (rule max_cp_readys_threads_pre[OF False])
qed
end
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
apply (unfold s_holding_def cs_holding_def wq_def, simp)
done
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
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))"
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
context valid_trace
begin
lemma detached_intro:
assumes eq_pv: "cntP s th = cntV s th"
shows "detached s th"
proof -
from cnp_cnv_cncs
have eq_cnt: "cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
hence cncs_zero: "cntCS s th = 0"
by (auto simp:eq_pv split:if_splits)
with eq_cnt
have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv)
thus ?thesis
proof
assume "th \<notin> threads s"
with range_in 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 card_0_eq [OF finite_holding] and cncs_zero
have "holdents s th = {}"
by (simp add:cntCS_def)
thus ?thesis
apply(auto simp:holdents_test)
apply(case_tac a)
apply(auto simp:holdents_test s_RAG_def)
done
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 -
from cnp_cnv_cncs
have eq_pv: " cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
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 and eq_pv show ?thesis by simp
next
case False
with cncs_z and eq_pv show ?thesis by simp
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
text {*
The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
from the concise and miniature model of PIP given in PrioGDef.thy.
*}
lemma eq_dependants: "dependants (wq s) = dependants s"
by (simp add: s_dependants_abv wq_def)
lemma next_th_unique:
assumes nt1: "next_th s th cs th1"
and nt2: "next_th s th cs th2"
shows "th1 = th2"
using assms by (unfold next_th_def, auto)
lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
apply (induct s, simp)
proof -
fix a s
assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
and eq_as: "a # s \<noteq> []"
show "last_set th (a # s) < length (a # s)"
proof(cases "s \<noteq> []")
case False
from False show ?thesis
by (cases a, auto simp:last_set.simps)
next
case True
from ih [OF True] show ?thesis
by (cases a, auto simp:last_set.simps)
qed
qed
lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
by (induct s, auto simp:threads.simps)
lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
apply (drule_tac th_in_ne)
by (unfold preced_def, auto intro: birth_time_lt)
lemma inj_the_preced:
"inj_on (the_preced s) (threads s)"
by (metis inj_onI preced_unique the_preced_def)
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
lemma tRAG_Field:
"Field (tRAG s) \<subseteq> Field (RAG s)"
by (unfold tRAG_alt_def Field_def, auto)
lemma tRAG_ancestorsE:
assumes "x \<in> ancestors (tRAG s) u"
obtains th where "x = Th th"
proof -
from assms have "(u, x) \<in> (tRAG s)^+"
by (unfold ancestors_def, auto)
from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
then obtain th where "x = Th th"
by (unfold tRAG_alt_def, auto)
from that[OF this] show ?thesis .
qed
lemma tRAG_mono:
assumes "RAG s' \<subseteq> RAG s"
shows "tRAG s' \<subseteq> tRAG s"
using assms
by (unfold tRAG_alt_def, auto)
lemma holding_next_thI:
assumes "holding s th cs"
and "length (wq s cs) > 1"
obtains th' where "next_th s th cs th'"
proof -
from assms(1)[folded eq_holding, unfolded cs_holding_def]
have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" .
then obtain rest where h1: "wq s cs = th#rest"
by (cases "wq s cs", auto)
with assms(2) have h2: "rest \<noteq> []" by auto
let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
have "next_th s th cs ?th'" using h1(1) h2
by (unfold next_th_def, auto)
from that[OF this] show ?thesis .
qed
lemma RAG_tRAG_transfer:
assumes "vt s'"
assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
and "(Cs cs, Th th'') \<in> RAG s'"
shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
proof -
interpret vt_s': valid_trace "s'" using assms(1)
by (unfold_locales, simp)
interpret rtree: rtree "RAG s'"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:vt_s'.unique_RAG)
show "acyclic (RAG s')"
by (rule vt_s'.acyclic_RAG)
qed
{ fix n1 n2
assume "(n1, n2) \<in> ?L"
from this[unfolded tRAG_alt_def]
obtain th1 th2 cs' where
h: "n1 = Th th1" "n2 = Th th2"
"(Th th1, Cs cs') \<in> RAG s"
"(Cs cs', Th th2) \<in> RAG s" by auto
from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto
from h(3) and assms(2)
have "(Th th1, Cs cs') = (Th th, Cs cs) \<or>
(Th th1, Cs cs') \<in> RAG s'" by auto
hence "(n1, n2) \<in> ?R"
proof
assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
hence eq_th1: "th1 = th" by simp
moreover have "th2 = th''"
proof -
from h1 have "cs' = cs" by simp
from assms(3) cs_in[unfolded this] rtree.sgv
show ?thesis
by (unfold single_valued_def, auto)
qed
ultimately show ?thesis using h(1,2) by auto
next
assume "(Th th1, Cs cs') \<in> RAG s'"
with cs_in have "(Th th1, Th th2) \<in> tRAG s'"
by (unfold tRAG_alt_def, auto)
from this[folded h(1, 2)] show ?thesis by auto
qed
} moreover {
fix n1 n2
assume "(n1, n2) \<in> ?R"
hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto
hence "(n1, n2) \<in> ?L"
proof
assume "(n1, n2) \<in> tRAG s'"
moreover have "... \<subseteq> ?L"
proof(rule tRAG_mono)
show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)
qed
ultimately show ?thesis by auto
next
assume eq_n: "(n1, n2) = (Th th, Th th'')"
from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto
moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto
ultimately show ?thesis
by (unfold eq_n tRAG_alt_def, auto)
qed
} ultimately show ?thesis by auto
qed
context valid_trace
begin
lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
end
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "Max (_ ` ?L) = Max (_ ` ?R)")
proof -
have "?L = ?R"
by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
thus ?thesis by simp
qed
thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
qed
lemma cp_gen_alt_def:
"cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
by (auto simp:cp_gen_def)
lemma tRAG_nodeE:
assumes "(n1, n2) \<in> tRAG s"
obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
using assms
by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)
lemma subtree_nodeE:
assumes "n \<in> subtree (tRAG s) (Th th)"
obtains th1 where "n = Th th1"
proof -
show ?thesis
proof(rule subtreeE[OF assms])
assume "n = Th th"
from that[OF this] show ?thesis .
next
assume "Th th \<in> ancestors (tRAG s) n"
hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
hence "\<exists> th1. n = Th th1"
proof(induct)
case (base y)
from tRAG_nodeE[OF this] show ?case by metis
next
case (step y z)
thus ?case by auto
qed
with that show ?thesis by auto
qed
qed
lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"
proof -
have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*"
by (rule rtrancl_mono, auto simp:RAG_split)
also have "... \<subseteq> ((RAG s)^*)^*"
by (rule rtrancl_mono, auto)
also have "... = (RAG s)^*" by simp
finally show ?thesis by (unfold tRAG_def, simp)
qed
lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"
proof -
{ fix a
assume "a \<in> subtree (tRAG s) x"
hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
with tRAG_star_RAG[of s]
have "(a, x) \<in> (RAG s)^*" by auto
hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)
} thus ?thesis by auto
qed
lemma tRAG_trancl_eq:
"{th'. (Th th', Th th) \<in> (tRAG s)^+} =
{th'. (Th th', Th th) \<in> (RAG s)^+}"
(is "?L = ?R")
proof -
{ fix th'
assume "th' \<in> ?L"
hence "(Th th', Th th) \<in> (tRAG s)^+" by auto
from tranclD[OF this]
obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto
from tRAG_subtree_RAG[of s] and this(2)
have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG)
moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto
ultimately have "th' \<in> ?R" by auto
} moreover
{ fix th'
assume "th' \<in> ?R"
hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)
from plus_rpath[OF this]
obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto
hence "(Th th', Th th) \<in> (tRAG s)^+"
proof(induct xs arbitrary:th' th rule:length_induct)
case (1 xs th' th)
then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)
show ?case
proof(cases "xs1")
case Nil
from 1(2)[unfolded Cons1 Nil]
have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
then obtain cs where "x1 = Cs cs"
by (unfold s_RAG_def, auto)
from rpath_nnl_lastE[OF rp[unfolded this]]
show ?thesis by auto
next
case (Cons x2 xs2)
from 1(2)[unfolded Cons1[unfolded this]]
have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
from rpath_edges_on[OF this]
have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
by (simp add: edges_on_unfold)
with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
by (simp add: edges_on_unfold)
from this eds
have rg2: "(x1, x2) \<in> RAG s" by auto
from this[unfolded eq_x1]
obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)
from rp have "rpath (RAG s) x2 xs2 (Th th)"
by (elim rpath_ConsE, simp)
from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
show ?thesis
proof(cases "xs2 = []")
case True
from rpath_nilE[OF rp'[unfolded this]]
have "th1 = th" by auto
from rt1[unfolded this] show ?thesis by auto
next
case False
from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]
have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp
with rt1 show ?thesis by auto
qed
qed
qed
hence "th' \<in> ?L" by auto
} ultimately show ?thesis by blast
qed
lemma tRAG_trancl_eq_Th:
"{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} =
{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}"
using tRAG_trancl_eq by auto
lemma dependants_alt_def:
"dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
context valid_trace
begin
lemma count_eq_tRAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using assms count_eq_dependants dependants_alt_def eq_dependants by auto
lemma count_eq_RAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
using assms count_eq_dependants cs_dependants_def eq_RAG by auto
lemma count_eq_RAG_plus_Th:
assumes "cntP s th = cntV s th"
shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
using count_eq_RAG_plus[OF assms] by auto
lemma count_eq_tRAG_plus_Th:
assumes "cntP s th = cntV s th"
shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using count_eq_tRAG_plus[OF assms] by auto
end
lemma tRAG_subtree_eq:
"(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}"
(is "?L = ?R")
proof -
{ fix n
assume h: "n \<in> ?L"
hence "n \<in> ?R"
by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG)
} moreover {
fix n
assume "n \<in> ?R"
then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
by (auto simp:subtree_def)
from rtranclD[OF this(2)]
have "n \<in> ?L"
proof
assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto
thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
qed (insert h, auto simp:subtree_def)
} ultimately show ?thesis by auto
qed
lemma threads_set_eq:
"the_thread ` (subtree (tRAG s) (Th th)) =
{th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
lemma cp_alt_def1:
"cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
proof -
have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
by auto
thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
qed
lemma cp_gen_def_cond:
assumes "x = Th th"
shows "cp s th = cp_gen s (Th th)"
by (unfold cp_alt_def1 cp_gen_def, simp)
lemma cp_gen_over_set:
assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
proof(rule f_image_eq)
fix a
assume "a \<in> A"
from assms[rule_format, OF this]
obtain th where eq_a: "a = Th th" by auto
show "cp_gen s a = (cp s \<circ> the_thread) a"
by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
qed
context valid_trace
begin
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
shows "th \<in> threads s"
using assms
by (metis Field_def UnE dm_RAG_threads range_in vt)
lemma subtree_tRAG_thread:
assumes "th \<in> threads s"
shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
proof -
have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
by (unfold tRAG_subtree_eq, simp)
also have "... \<subseteq> ?R"
proof
fix x
assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
from this(2)
show "x \<in> ?R"
proof(cases rule:subtreeE)
case 1
thus ?thesis by (simp add: assms h(1))
next
case 2
thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI)
qed
qed
finally show ?thesis .
qed
lemma readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
proof -
{ fix x
assume "x \<in> ancestors (RAG s) (Th th)"
hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
from tranclD[OF this]
obtain z where "(Th th, z) \<in> RAG s" by auto
with assms(1) have False
apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
by (fold wq_def, blast)
} thus ?thesis by (unfold root_def, auto)
qed
lemma readys_in_no_subtree:
assumes "th \<in> readys s"
and "th' \<noteq> th"
shows "Th th \<notin> subtree (RAG s) (Th th')"
proof
assume "Th th \<in> subtree (RAG s) (Th th')"
thus False
proof(cases rule:subtreeE)
case 1
with assms show ?thesis by auto
next
case 2
with readys_root[OF assms(1)]
show ?thesis by (auto simp:root_def)
qed
qed
lemma not_in_thread_isolated:
assumes "th \<notin> threads s"
shows "(Th th) \<notin> Field (RAG s)"
proof
assume "(Th th) \<in> Field (RAG s)"
with dm_RAG_threads and range_in assms
show False by (unfold Field_def, blast)
qed
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG show "finite (RAG s)" .
next
from acyclic_RAG show "acyclic (RAG s)" .
qed
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
lemma sgv_hRAG: "single_valued (hRAG s)"
using holding_unique
by (unfold single_valued_def hRAG_def, auto)
lemma sgv_tRAG: "single_valued (tRAG s)"
by (unfold tRAG_def, rule single_valued_relcomp,
insert sgv_wRAG sgv_hRAG, auto)
lemma acyclic_tRAG: "acyclic (tRAG s)"
proof(unfold tRAG_def, rule acyclic_compose)
show "acyclic (RAG s)" using acyclic_RAG .
next
show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
next
show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
qed
lemma sgv_RAG: "single_valued (RAG s)"
using unique_RAG by (auto simp:single_valued_def)
lemma rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
end
sublocale valid_trace < rtree_RAG: rtree "RAG s"
proof
show "single_valued (RAG s)"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:unique_RAG)
show "acyclic (RAG s)"
by (rule acyclic_RAG)
qed
sublocale valid_trace < rtree_s: rtree "tRAG s"
proof(unfold_locales)
from sgv_tRAG show "single_valued (tRAG s)" .
next
from acyclic_tRAG show "acyclic (tRAG s)" .
qed
sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"
proof -
show "fsubtree (RAG s)"
proof(intro_locales)
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
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
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
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
(* keep *)
lemma next_th_holding:
assumes vt: "vt s"
and nxt: "next_th s th cs th'"
shows "holding (wq s) th cs"
proof -
from nxt[unfolded next_th_def]
obtain rest where h: "wq s cs = th # rest"
"rest \<noteq> []"
"th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
thus ?thesis
by (unfold cs_holding_def, auto)
qed
context valid_trace
begin
lemma next_th_waiting:
assumes nxt: "next_th s th cs th'"
shows "waiting (wq s) th' cs"
proof -
from nxt[unfolded next_th_def]
obtain rest where h: "wq s cs = th # rest"
"rest \<noteq> []"
"th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
from wq_distinct[of cs, unfolded h]
have dst: "distinct (th # rest)" .
have in_rest: "th' \<in> set rest"
proof(unfold h, rule someI2)
show "distinct rest \<and> set rest = set rest" using dst by auto
next
fix x assume "distinct x \<and> set x = set rest"
with h(2)
show "hd x \<in> set (rest)" by (cases x, auto)
qed
hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
moreover have "th' \<noteq> hd (wq s cs)"
by (unfold h(1), insert in_rest dst, auto)
ultimately show ?thesis by (auto simp:cs_waiting_def)
qed
lemma next_th_RAG:
assumes nxt: "next_th (s::event list) th cs th'"
shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
using vt assms next_th_holding next_th_waiting
by (unfold s_RAG_def, simp)
end
-- {* A useless definition *}
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
find_theorems release
lemma "wq (V th cs # s) cs1 = ttt"
apply (unfold wq_def, auto simp:Let_def)
end