theory PrioG
imports PrioGDef
begin
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:
"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 wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
proof(erule_tac vt.induct, simp add:wq_def)
fix s e
assume h1: "step s e"
and h2: "distinct (wq s cs)"
thus "distinct (wq (e # s) cs)"
proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
fix thread s
assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
and h2: "thread \<in> set (wq_fun (schs s) cs)"
and h3: "thread \<in> runing s"
show "False"
proof -
from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow>
thread = hd ((wq_fun (schs s) cs))"
by (simp add:runing_def readys_def s_waiting_def wq_def)
from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
with h2
have "(Cs cs, Th thread) \<in> (RAG s)"
by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)
with h1 show False by auto
qed
next
fix thread s a list
assume dst: "distinct list"
show "distinct (SOME q. distinct q \<and> set q = set list)"
proof(rule someI2)
from dst show "distinct list \<and> set list = set list" by auto
next
fix q assume "distinct q \<and> set q = set list"
thus "distinct q" by auto
qed
qed
qed
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 block_pre:
fixes thread cs s
assumes vt_e: "vt (e#s)"
and s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof -
show ?thesis
proof(cases e)
case (P th cs)
with assms
show ?thesis
by (auto simp:wq_def Let_def split:if_splits)
next
case (Create th prio)
with assms show ?thesis
by (auto simp:wq_def Let_def split:if_splits)
next
case (Exit th)
with assms show ?thesis
by (auto simp:wq_def Let_def split:if_splits)
next
case (Set th prio)
with assms show ?thesis
by (auto simp:wq_def Let_def split:if_splits)
next
case (V th cs)
with assms show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
and h2: "q # qs = wq_fun (schs s) cs"
and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
and vt: "vt (V th cs # s)"
from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
moreover have "thread \<in> set qs"
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
from wq_distinct [OF step_back_vt[OF vt], of cs]
and h2[symmetric, folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
fix x assume "distinct x \<and> set x = set qs"
thus "set x = set qs" by auto
qed
with h3 show ?thesis by simp
qed
ultimately show "False" by auto
qed
qed
qed
text {*
The following lemmas is also obvious and shallow. It says
that only running thread can request for a critical resource
and that the requested resource must be one which is
not current held by the thread.
*}
lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (RAG s)^+"
apply (ind_cases "vt ((P thread cs)#s)")
apply (ind_cases "step s (P thread cs)")
by auto
lemma abs1:
fixes e es
assumes ein: "e \<in> set es"
and neq: "hd es \<noteq> hd (es @ [x])"
shows "False"
proof -
from ein have "es \<noteq> []" by auto
then obtain e ess where "es = e # ess" by (cases es, auto)
with neq show ?thesis by auto
qed
lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
by (cases es, auto)
inductive_cases evt_cons: "vt (a#s)"
lemma abs2:
assumes vt: "vt (e#s)"
and inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
and inq': "thread \<in> set (wq (e#s) cs)"
shows "False"
proof -
from assms show "False"
apply (cases e)
apply ((simp split:if_splits add:Let_def wq_def)[1])+
apply (insert abs1, fast)[1]
apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
proof -
fix th qs
assume vt: "vt (V th cs # s)"
and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
proof -
from wq_distinct[OF step_back_vt[OF vt], of cs]
and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
moreover have "thread \<in> set qs"
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
from wq_distinct [OF step_back_vt[OF vt], of cs]
and eq_wq [folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
fix x assume "distinct x \<and> set x = set qs"
thus "set x = set qs" by auto
qed
with th_in show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
qed
qed
lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
proof(induct s, simp)
fix a s t
assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
and vt_a: "vt (a # s)"
show "vt (moment t (a # s))"
proof(cases "t \<ge> length (a#s)")
case True
from True have "moment t (a#s) = a#s" by simp
with vt_a show ?thesis by simp
next
case False
hence le_t1: "t \<le> length s" by simp
from vt_a have "vt s"
by (erule_tac evt_cons, simp)
from h [OF this] have "vt (moment t s)" .
moreover have "moment t (a#s) = moment t s"
proof -
from moment_app [OF le_t1, of "[a]"]
show ?thesis by simp
qed
ultimately show ?thesis by auto
qed
qed
(* Wrong:
lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
*)
text {* (* ??? *)
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 lose 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:
fixes cs1 cs2 s thread
assumes vt: "vt s"
and 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 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>(thread \<in> set (wq (moment t1 s) cs1) \<and>
thread \<noteq> hd (wq (moment t1 s) cs1))"
and nn1: "(\<forall>i'>t1. thread \<in> set (wq (moment i' s) cs1) \<and>
thread \<noteq> hd (wq (moment i' s) cs1))" by auto
from p_split [of "?Q cs2", OF q2 nq2]
obtain t2 where lt2: "t2 < length s"
and np2: "\<not>(thread \<in> set (wq (moment t2 s) cs2) \<and>
thread \<noteq> hd (wq (moment t2 s) cs2))"
and nn2: "(\<forall>i'>t2. thread \<in> set (wq (moment i' s) cs2) \<and>
thread \<noteq> hd (wq (moment i' s) cs2))" by auto
show ?thesis
proof -
{
assume 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: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt]
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
thm abs2
from abs2 [OF vt_e True eq_th h2 h1]
show ?thesis by auto
next
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs2" .
with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
with runing_ready have "thread \<in> readys (moment t2 s)" by auto
with nn1 [rule_format, OF lt12]
show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume lt12: "t2 < t1"
let ?t3 = "Suc t1"
from lt1 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto
have lt_t3: "t1 < ?t3" by simp
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt]
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
from abs2 [OF vt_e True eq_th h2 h1]
show ?thesis by auto
next
case False
from block_pre [OF vt_e False h1]
have "e = P thread cs1" .
with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
with runing_ready have "thread \<in> readys (moment t1 s)" by auto
with nn2 [rule_format, OF lt12]
show ?thesis by (simp add:readys_def wq_def s_waiting_def, auto)
qed
} moreover {
assume eqt12: "t1 = t2"
let ?t3 = "Suc t1"
from lt1 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto
have lt_t3: "t1 < ?t3" by simp
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have vt_e: "vt (e#moment t1 s)"
proof -
from vt_moment [OF vt]
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
from abs2 [OF vt_e True eq_th h2 h1]
show ?thesis by auto
next
case False
from block_pre [OF vt_e False h1]
have eq_e1: "e = P thread cs1" .
have lt_t3: "t1 < ?t3" by simp
with eqt12 have "t2 < ?t3" by simp
from nn2 [rule_format, OF this] and eq_m and eqt12
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
show ?thesis
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
from abs2 [OF this True eq_th h2 h1]
show ?thesis .
next
case False
have vt_e: "vt (e#moment t2 s)"
proof -
from vt_moment [OF vt] eqt12
have "vt (moment (Suc t2) s)" by auto
with eq_m eqt12 show ?thesis by simp
qed
from block_pre [OF vt_e False h1]
have "e = P thread cs2" .
with eq_e1 neq12 show ?thesis by auto
qed
qed
} ultimately show ?thesis by arith
qed
qed
text {*
This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
*}
lemma waiting_unique:
fixes s cs1 cs2
assumes "vt s"
and "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
(* 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:
fixes s::"state"
assumes "holding s th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
using assms
unfolding s_holding_def
by 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:
fixes x y z r
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:
fixes r x y z
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:
fixes r x y z
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)
text {*
The following lemmas are used in the proof of
lemma @{text "step_RAG_v"}, which characterizes how the @{text "RAG"} is changed
by @{text "V"}-events.
However, since our model is very concise, such seemingly obvious lemmas need to be derived from scratch,
starting from the model definitions.
*}
lemma step_v_hold_inv[elim_format]:
"\<And>c t. \<lbrakk>vt (V th cs # s);
\<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow>
next_th s th cs t \<and> c = cs"
proof -
fix c t
assume vt: "vt (V th cs # s)"
and nhd: "\<not> holding (wq s) t c"
and hd: "holding (wq (V th cs # s)) t c"
show "next_th s th cs t \<and> c = cs"
proof(cases "c = cs")
case False
with nhd hd show ?thesis
by (unfold cs_holding_def wq_def, auto simp:Let_def)
next
case True
with step_back_step [OF vt]
have "step s (V th c)" by simp
hence "next_th s th cs t"
proof(cases)
assume "holding s th c"
with nhd hd show ?thesis
apply (unfold s_holding_def cs_holding_def wq_def next_th_def,
auto simp:Let_def split:list.splits if_splits)
proof -
assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"
moreover have "\<dots> = set []"
proof(rule someI2)
show "distinct [] \<and> [] = []" by auto
next
fix x assume "distinct x \<and> x = []"
thus "set x = set []" by auto
qed
ultimately show False by auto
next
assume " hd (SOME q. distinct q \<and> q = []) \<in> set (SOME q. distinct q \<and> q = [])"
moreover have "\<dots> = set []"
proof(rule someI2)
show "distinct [] \<and> [] = []" by auto
next
fix x assume "distinct x \<and> x = []"
thus "set x = set []" by auto
qed
ultimately show False by auto
qed
qed
with True show ?thesis by auto
qed
qed
text {*
The following @{text "step_v_wait_inv"} is also an obvious lemma, which, however, needs to be
derived from scratch, which confirms the correctness of the definition of @{text "next_th"}.
*}
lemma step_v_wait_inv[elim_format]:
"\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
\<rbrakk>
\<Longrightarrow> (next_th s th cs t \<and> cs = c)"
proof -
fix t c
assume vt: "vt (V th cs # s)"
and nw: "\<not> waiting (wq (V th cs # s)) t c"
and wt: "waiting (wq s) t c"
show "next_th s th cs t \<and> cs = c"
proof(cases "cs = c")
case False
with nw wt show ?thesis
by (auto simp:cs_waiting_def wq_def Let_def)
next
case True
from nw[folded True] wt[folded True]
have "next_th s th cs t"
apply (unfold next_th_def, auto simp:cs_waiting_def wq_def Let_def split:list.splits)
proof -
fix a list
assume t_in: "t \<in> set list"
and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
by auto
qed
with t_ni and t_in show "a = th" by auto
next
fix a list
assume t_in: "t \<in> set list"
and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
by auto
qed
with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto
next
fix a list
assume eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step[OF vt]
show "a = th"
proof(cases)
assume "holding s th cs"
with eq_wq show ?thesis
by (unfold s_holding_def wq_def, auto)
qed
qed
with True show ?thesis by simp
qed
qed
lemma step_v_not_wait[consumes 3]:
"\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)
lemma step_v_release:
"\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
proof -
assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
from step_back_step [OF vt] and hd
show "False"
proof(cases)
assume "holding (wq (V th cs # s)) th cs" and "holding s th cs"
thus ?thesis
apply (unfold s_holding_def wq_def cs_holding_def)
apply (auto simp:Let_def split:list.splits)
proof -
fix list
assume eq_wq[folded wq_def]:
"wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
and hd_in: "hd (SOME q. distinct q \<and> set q = set list)
\<in> set (SOME q. distinct q \<and> set q = set list)"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
by auto
qed
moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)"
proof -
from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
show ?thesis by auto
qed
moreover note eq_wq and hd_in
ultimately show "False" by auto
qed
qed
qed
lemma step_v_get_hold:
"\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
apply (unfold cs_holding_def next_th_def wq_def,
auto simp:Let_def)
proof -
fix rest
assume vt: "vt (V th cs # s)"
and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
\<notin> set (SOME q. distinct q \<and> set q = set rest)"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vt], 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"
hence "set x = set rest" by auto
with nrest
show "x \<noteq> []" by (case_tac x, auto)
qed
with ni show "False" by auto
qed
lemma step_v_release_inv[elim_format]:
"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
c = cs \<and> t = th"
apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
proof -
fix a list
assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
show ?thesis
by (unfold s_holding_def wq_def, auto)
qed
next
fix a list
assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step [OF vt] show "a = th"
proof(cases)
assume "holding s th cs" with eq_wq
show ?thesis
by (unfold s_holding_def wq_def, auto)
qed
qed
lemma step_v_waiting_mono:
"\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
proof -
fix t c
let ?s' = "(V th cs # s)"
assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
show "waiting (wq s) t c"
proof(cases "c = cs")
case False
assume neq_cs: "c \<noteq> cs"
hence "waiting (wq ?s') t c = waiting (wq s) t c"
by (unfold cs_waiting_def wq_def, auto simp:Let_def)
with wt show ?thesis by simp
next
case True
with wt show ?thesis
apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)
proof -
fix a list
assume not_in: "t \<notin> set list"
and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
and eq_wq: "wq_fun (schs s) cs = a # list"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
from wq_distinct [OF step_back_vt[OF vt], of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
fix x assume "distinct x \<and> set x = set list"
thus "set x = set list" by auto
qed
with not_in is_in show "t = a" by auto
next
fix list
assume is_waiting: "waiting (wq (V th cs # s)) t cs"
and eq_wq: "wq_fun (schs s) cs = t # list"
hence "t \<in> set list"
apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
proof -
assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
moreover have "\<dots> = set list"
proof(rule someI2)
from wq_distinct [OF step_back_vt[OF vt], of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
fix x assume "distinct x \<and> set x = set list"
thus "set x = set list" by auto
qed
ultimately show "t \<in> set list" by simp
qed
with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
show False by auto
qed
qed
qed
text {* (* ??? *)
The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
with the happening of @{text "V"}-events:
*}
lemma step_RAG_v:
fixes th::thread
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)
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:
fixes s
assumes vt: "vt s"
shows "acyclic (RAG s)"
using assms
proof(induct)
case (vt_cons s e)
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 waiting_unique [OF vt])
from eq_wq wq_distinct[OF vt, 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 wq_distinct[OF vt, 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 wq_distinct[OF vt, 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 wq_distinct[OF vt, 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 wq_distinct[OF vt, 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:
fixes s
assumes vt: "vt s"
shows "finite (RAG s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
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:
fixes s
assumes vt: "vt s"
shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
from finite_RAG [OF vt]
show "finite (RAG s)" .
next
from acyclic_RAG[OF vt]
show "acyclic (RAG s)" .
qed
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)
lemma wq_threads:
fixes s cs
assumes vt: "vt s"
and 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)
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 wq_distinct[OF vt, 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>vt s; (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:
fixes th thread cs rest
assumes vt: "vt s"
and 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 vt, 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:
assumes vt: "vt s"
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 [OF vt]
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 [OF vt] 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:
fixes s th
assumes vt: "vt s"
and 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 vt this]
show ?thesis by auto
qed
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)
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)
lemma unique_RAG: "\<lbrakk>vt s; (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)
lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)
lemma dchain_unique:
assumes vt: "vt s"
and 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 [OF vt]
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
lemma step_holdents_p_add:
fixes th cs s
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:
fixes th cs s
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 finite_holding:
fixes s th cs
assumes vt: "vt s"
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
from finite_RAG [OF vt]
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:
fixes s thread cs
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
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 wq_distinct[OF step_back_vt[OF vtv], 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 finite_holding [OF vtv]
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
text {* (* ??? *) \noindent
The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
of one particular thread.
*}
lemma cnp_cnv_cncs:
fixes s th
assumes vt: "vt s"
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)
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 wq_threads [OF vt 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
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 finite_holding [OF vt, 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 wq_distinct [OF vtp, 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
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 wq_distinct[OF step_back_vt[OF vtv], 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
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 wq_distinct[OF step_back_vt[OF vtv], of cs]
and eq_wq show False by auto
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 (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
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 wq_distinct[OF step_back_vt[OF vtv], 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 wq_distinct[OF step_back_vt[OF vtv], 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 wq_distinct[OF step_back_vt[OF vtv], 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 wq_threads[OF step_back_vt[OF vtv]])
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 wq_distinct[OF step_back_vt[OF vtv], 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 waiting_unique[OF step_back_vt[OF vtv] 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 wq_threads [OF step_back_vt[OF vtv] 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 finite_RAG[OF step_back_vt[OF vtv]]
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:
fixes th s
assumes vt: "vt s"
and 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)
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
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 wq_distinct[OF step_back_vt[OF vtv], 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 "hd x \<in> set rest" by (cases x, auto)
qed
with eq_wq have "?t \<in> set (wq s cs)" by simp
from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
show False by auto
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
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
by (auto simp:s_waiting_def cs_waiting_def wq_def)
lemma dm_RAG_threads:
fixes th s
assumes vt: "vt s"
and 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 vt this] show ?thesis .
qed
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
(* FIXME: NOT NEEDED *)
lemma runing_unique:
fixes th1 th2 s
assumes vt: "vt s"
and 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)")
thm cp_def image_Collect
unfolding cp_eq_cpreced
unfolding cpreced_def .
obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
thm Max_in
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[OF vt] 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
thm Max_in
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[OF vt] 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 vt 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 vt 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:eq_waiting)
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:eq_waiting)
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 vt 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 "vt s \<Longrightarrow> 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
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
lemma length_down_to_in:
assumes le_ij: "i \<le> j"
and le_js: "j \<le> length s"
shows "length (down_to j i s) = j - i"
proof -
have "length (down_to j i s) = length (from_to i j (rev s))"
by (unfold down_to_def, auto)
also have "\<dots> = j - i"
proof(rule length_from_to_in[OF le_ij])
from le_js show "j \<le> length (rev s)" by simp
qed
finally show ?thesis .
qed
lemma moment_head:
assumes le_it: "Suc i \<le> length t"
obtains e where "moment (Suc i) t = e#moment i t"
proof -
have "i \<le> Suc i" by simp
from length_down_to_in [OF this le_it]
have "length (down_to (Suc i) i t) = 1" by auto
then obtain e where "down_to (Suc i) i t = [e]"
apply (cases "(down_to (Suc i) i t)") by auto
moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
by (rule down_to_conc[symmetric], auto)
ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
by (auto simp:down_to_moment)
from that [OF this] show ?thesis .
qed
lemma cnp_cnv_eq:
fixes th s
assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
lemma count_eq_dependants:
assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
shows "dependants (wq s) th = {}"
proof -
from cnp_cnv_cncs[OF vt] 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 vt, 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:
fixes s th
assumes vt: "vt s"
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 vt 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:
assumes vt: "vt s"
shows "finite (threads s)"
using vt
by (induct) (auto elim: step.cases)
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
and np: "A \<noteq> {}"
and fnt: "finite B"
shows "Max (f ` A) \<le> Max (f ` B)"
proof(rule Max_mono)
from seq show "f ` A \<subseteq> f ` B" by auto
next
from np show "f ` A \<noteq> {}" by auto
next
from fnt and seq show "finite (f ` B)" by auto
qed
lemma cp_le:
assumes vt: "vt s"
and 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 [OF vt]
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[OF vt])
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:
assumes vt: "vt s"
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[OF vt] 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:
assumes vt: "vt s"
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[OF vt]
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 vt 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[OF vt]
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 vt, 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[OF vt]
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 vt: "vt s"
and np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(unfold max_cp_eq[OF vt])
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[OF vt] 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 vt 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[OF vt] finite_threads[OF vt]
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[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
from p_in and th'_in and dependants_threads[OF vt, 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 vt, 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[OF vt]
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
next
from finite_threads[OF vt]
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 vt, of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
from finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
} with hy show ?thesis by auto
qed
next
from dependants_threads[OF vt, of tm] finite_threads[OF vt]
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[OF vt]
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[OF vt]
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 vt, 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:
assumes vt: "vt s"
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 vt False])
qed
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
lemma detached_intro:
fixes s th
assumes vt: "vt s"
and eq_pv: "cntP s th = cntV s th"
shows "detached s th"
proof -
from cnp_cnv_cncs[OF vt]
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[OF vt] dm_RAG_threads[OF vt]
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 [OF vt]] 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:
fixes s th
assumes vt: "vt s"
and dtc: "detached s th"
shows "cntP s th = cntV s th"
proof -
from cnp_cnv_cncs[OF vt]
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:eq_waiting 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:
fixes s th
assumes vt: "vt s"
shows "(detached s th) = (cntP s th = cntV s th)"
by (insert vt, auto intro:detached_intro detached_elim)
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.
*}
end