Retrofiting of:
CpsG.thy (the parallel copy of PIPBasics.thy),
ExtGG.thy (The paralell copy of Implemenation.thy),
PrioG.thy (The paralell copy of Correctness.thy)
has completed.
The next step is to overwite original copies with the paralell ones.
theory Prio
imports Precedence_ord Moment Lsp Happen_within
begin
type_synonym thread = nat
type_synonym priority = nat
type_synonym cs = nat
datatype event =
Create thread priority |
Exit thread |
P thread cs |
V thread cs |
Set thread priority
datatype node =
Th "thread" |
Cs "cs"
type_synonym state = "event list"
fun threads :: "state \<Rightarrow> thread set"
where
"threads [] = {}" |
"threads (Create thread prio#s) = {thread} \<union> threads s" |
"threads (Exit thread # s) = (threads s) - {thread}" |
"threads (e#s) = threads s"
fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> nat"
where
"original_priority thread [] = 0" |
"original_priority thread (Create thread' prio#s) =
(if thread' = thread then prio else original_priority thread s)" |
"original_priority thread (Set thread' prio#s) =
(if thread' = thread then prio else original_priority thread s)" |
"original_priority thread (e#s) = original_priority thread s"
fun birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"
where
"birthtime thread [] = 0" |
"birthtime thread ((Create thread' prio)#s) = (if (thread = thread') then length s
else birthtime thread s)" |
"birthtime thread ((Set thread' prio)#s) = (if (thread = thread') then length s
else birthtime thread s)" |
"birthtime thread (e#s) = birthtime thread s"
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
where "preced thread s = Prc (original_priority thread s) (birthtime thread s)"
consts holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
depend :: "'b \<Rightarrow> (node \<times> node) set"
dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
defs (overloaded) cs_holding_def: "holding wq thread cs == (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
cs_waiting_def: "waiting wq thread cs == (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
cs_depend_def: "depend (wq::cs \<Rightarrow> thread list) == {(Th t, Cs c) | t c. waiting wq t c} \<union>
{(Cs c, Th t) | c t. holding wq t c}"
cs_dependents_def: "dependents (wq::cs \<Rightarrow> thread list) th == {th' . (Th th', Th th) \<in> (depend wq)^+}"
record schedule_state =
waiting_queue :: "cs \<Rightarrow> thread list"
cur_preced :: "thread \<Rightarrow> precedence"
definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"
where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
fun schs :: "state \<Rightarrow> schedule_state"
where
"schs [] = \<lparr>waiting_queue = \<lambda> cs. [],
cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |
"schs (e#s) = (let ps = schs s in
let pwq = waiting_queue ps in
let pcp = cur_preced ps in
let nwq = case e of
P thread cs \<Rightarrow> pwq(cs:=(pwq cs @ [thread])) |
V thread cs \<Rightarrow> let nq = case (pwq cs) of
[] \<Rightarrow> [] |
(th#pq) \<Rightarrow> case (lsp pcp pq) of
(l, [], r) \<Rightarrow> []
| (l, m#ms, r) \<Rightarrow> m#(l@ms@r)
in pwq(cs:=nq) |
_ \<Rightarrow> pwq
in let ncp = cpreced (e#s) nwq in
\<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
)"
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list"
where "wq s == waiting_queue (schs s)"
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
where "cp s = cur_preced (schs s)"
defs (overloaded) s_holding_def: "holding (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread = hd (wq s cs))"
s_waiting_def: "waiting (s::state) thread cs == (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
s_depend_def: "depend (s::state) == {(Th t, Cs c) | t c. waiting (wq s) t c} \<union>
{(Cs c, Th t) | c t. holding (wq s) t c}"
s_dependents_def: "dependents (s::state) th == {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
definition readys :: "state \<Rightarrow> thread set"
where
"readys s =
{thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}"
definition runing :: "state \<Rightarrow> thread set"
where "runing s = {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
where "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
where
thread_create: "\<lbrakk>prio \<le> max_prio; thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |
thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" |
thread_P: "\<lbrakk>thread \<in> runing s; (Cs cs, Th thread) \<notin> (depend s)^+\<rbrakk> \<Longrightarrow> step s (P thread cs)" |
thread_V: "\<lbrakk>thread \<in> runing s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
inductive vt :: "(state \<Rightarrow> event \<Rightarrow> bool) \<Rightarrow> state \<Rightarrow> bool"
for cs
where
vt_nil[intro]: "vt cs []" |
vt_cons[intro]: "\<lbrakk>vt cs s; cs s e\<rbrakk> \<Longrightarrow> vt cs (e#s)"
lemma runing_ready: "runing s \<subseteq> readys s"
by (auto simp only:runing_def readys_def)
lemma wq_v_eq_nil:
fixes s cs thread rest
assumes eq_wq: "wq s cs = thread # rest"
and eq_lsp: "lsp (cp s) rest = (l, [], r)"
shows "wq (V thread cs#s) cs = []"
proof -
from prems show ?thesis
by (auto simp:wq_def Let_def cp_def split:list.splits)
qed
lemma wq_v_eq:
fixes s cs thread rest
assumes eq_wq: "wq s cs = thread # rest"
and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
shows "wq (V thread cs#s) cs = th'#l@r"
proof -
from prems show ?thesis
by (auto simp:wq_def Let_def cp_def split:list.splits)
qed
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 step 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> (depend s)\<^sup>+"
and h2: "thread \<in> set (waiting_queue (schs s) cs)"
and h3: "thread \<in> runing s"
show "False"
proof -
from h3 have "\<And> cs. thread \<in> set (waiting_queue (schs s) cs) \<Longrightarrow>
thread = hd ((waiting_queue (schs s) cs))"
by (simp add:runing_def readys_def s_waiting_def wq_def)
from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .
with h2
have "(Cs cs, Th thread) \<in> (depend s)"
by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)
with h1 show False by auto
qed
next
fix thread s a list
assume h1: "thread \<in> runing s"
and h2: "holding s thread cs"
and h3: "waiting_queue (schs s) cs = a # list"
and h4: "a \<notin> set list"
and h5: "distinct list"
thus "distinct
((\<lambda>(l, a, r). case a of [] \<Rightarrow> [] | m # ms \<Rightarrow> m # l @ ms @ r)
(lsp (cur_preced (schs s)) list))"
apply (cases "(lsp (cur_preced (schs s)) list)", simp)
apply (case_tac b, simp)
by (drule_tac lsp_set_eq, simp)
qed
qed
lemma block_pre:
fixes thread cs s
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 -
have ee: "\<And> x y. \<lbrakk>x = y\<rbrakk> \<Longrightarrow> set x = set y"
by auto
from s_ni s_i show ?thesis
proof (cases e, auto split:if_splits simp add:Let_def wq_def)
fix uu uub uuc uud uue
assume h: "(uuc, thread # uu, uub) = lsp (cur_preced (schs s)) uud"
and h1 [symmetric]: "uue # uud = waiting_queue (schs s) cs"
and h2: "thread \<notin> set (waiting_queue (schs s) cs)"
from lsp_set [OF h] have "set (uuc @ (thread # uu) @ uub) = set uud" .
hence "thread \<in> set uud" by auto
with h1 have "thread \<in> set (waiting_queue (schs s) cs)" by auto
with h2 show False by auto
next
fix uu uua uub uuc uud uue
assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
and h2: "uue # uud = waiting_queue (schs s) cs"
and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"
and h4: "thread \<in> set uuc"
from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .
with h4 have "thread \<in> set uud" by auto
with h2 have "thread \<in> set (waiting_queue (schs s) cs)"
apply (drule_tac ee) by auto
with h1 show "False" by fast
next
fix uu uua uub uuc uud uue
assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
and h2: "uue # uud = waiting_queue (schs s) cs"
and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"
and h4: "thread \<in> set uu"
from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .
with h4 have "thread \<in> set uud" by auto
with h2 have "thread \<in> set (waiting_queue (schs s) cs)"
apply (drule_tac ee) by auto
with h1 show "False" by fast
next
fix uu uua uub uuc uud uue
assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
and h2: "uue # uud = waiting_queue (schs s) cs"
and h3: "(uuc, uua # uu, uub) = lsp (cur_preced (schs s)) uud"
and h4: "thread \<in> set uub"
from lsp_set [OF h3] have "set (uuc @ (uua # uu) @ uub) = set uud" .
with h4 have "thread \<in> set uud" by auto
with h2 have "thread \<in> set (waiting_queue (schs s) cs)"
apply (drule_tac ee) by auto
with h1 show "False" by fast
qed
qed
lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
thread \<in> runing s \<and> (Cs cs, Th thread) \<notin> (depend s)^+"
apply (ind_cases "vt step ((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 cs (a#s)"
lemma abs2:
assumes vt: "vt step (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 -
have ee: "\<And> uuc thread uu uub s list. (uuc, thread # uu, uub) = lsp (cur_preced (schs s)) list \<Longrightarrow>
lsp (cur_preced (schs s)) list = (uuc, thread # uu, uub)
" by simp
from prems show "False"
apply (cases e)
apply ((simp split:if_splits add:Let_def wq_def)[1])+
apply (insert abs1, fast)[1]
apply ((simp split:if_splits add:Let_def)[1])+
apply (simp split:if_splits list.splits add:Let_def wq_def)
apply (auto dest!:ee)
apply (drule_tac lsp_set_eq, simp)
apply (subgoal_tac "distinct (waiting_queue (schs s) cs)", simp, fold wq_def)
apply (rule_tac wq_distinct, auto)
apply (erule_tac evt_cons, auto)
apply (drule_tac lsp_set_eq, simp)
apply (subgoal_tac "distinct (wq s cs)", simp)
apply (rule_tac wq_distinct, auto)
apply (erule_tac evt_cons, auto)
apply (drule_tac lsp_set_eq, simp)
apply (subgoal_tac "distinct (wq s cs)", simp)
apply (rule_tac wq_distinct, auto)
apply (erule_tac evt_cons, auto)
apply (auto simp:wq_def Let_def split:if_splits prod.splits)
done
qed
lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
proof(induct s, simp)
fix a s t
assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
and vt_a: "vt cs (a # s)"
and le_t: "t \<le> length (a # s)"
show "vt cs (moment t (a # s))"
proof(cases "t = 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
with le_t have le_t1: "t \<le> length s" by simp
from vt_a have "vt cs s"
by (erule_tac evt_cons, simp)
from h [OF this le_t1] have "vt cs (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 (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
*)
lemma waiting_unique_pre:
fixes cs1 cs2 s thread
assumes vt: "vt step 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 step (e#moment t2 s)"
proof -
from vt_moment [OF vt le_t3]
have "vt step (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
from abs2 [OF vt_e True eq_th h2 h1]
show ?thesis by auto
next
case False
from block_pre [OF False h1]
have "e = P thread cs2" .
with vt_e have "vt step ((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 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 step (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
have "vt step (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 False h1]
have "e = P thread cs1" .
with vt_e have "vt step ((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 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 step (e#moment t1 s)"
proof -
from vt_moment [OF vt le_t3]
have "vt step (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 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 step (e#moment t2 s)" by simp
from abs2 [OF this True eq_th h2 h1]
show ?thesis .
next
case False
from block_pre [OF False h1]
have "e = P thread cs2" .
with eq_e1 neq12 show ?thesis by auto
qed
qed
} ultimately show ?thesis by arith
qed
qed
lemma waiting_unique:
assumes "vt step s"
and "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
proof -
from waiting_unique_pre and prems
show ?thesis
by (auto simp add:s_waiting_def)
qed
lemma holded_unique:
assumes "vt step s"
and "holding s th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
proof -
from prems show ?thesis
unfolding s_holding_def
by auto
qed
lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
apply (induct s, auto)
by (case_tac a, auto split:if_splits)
lemma birthtime_unique:
"\<lbrakk>birthtime th1 s = birthtime 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:birthtime_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 "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)
from birthtime_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
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
lemma depend_set_unchanged: "(depend (Set th prio # s)) = depend s"
apply (unfold s_depend_def s_waiting_def wq_def)
by (simp add:Let_def)
lemma depend_create_unchanged: "(depend (Create th prio # s)) = depend s"
apply (unfold s_depend_def s_waiting_def wq_def)
by (simp add:Let_def)
lemma depend_exit_unchanged: "(depend (Exit th # s)) = depend s"
apply (unfold s_depend_def s_waiting_def wq_def)
by (simp add:Let_def)
definition head_of :: "('a \<Rightarrow> 'b::linorder) \<Rightarrow> 'a set \<Rightarrow> 'a set"
where "head_of f A = {a . a \<in> A \<and> f a = Max (f ` A)}"
definition wq_head :: "state \<Rightarrow> cs \<Rightarrow> thread set"
where "wq_head s cs = head_of (cp s) (set (wq s cs))"
lemma f_nil_simp: "\<lbrakk>f cs = []\<rbrakk> \<Longrightarrow> f(cs:=[]) = f"
proof
fix x
assume h:"f cs = []"
show "(f(cs := [])) x = f x"
proof(cases "cs = x")
case True
with h show ?thesis by simp
next
case False
with h show ?thesis by simp
qed
qed
lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"
by(ind_cases "vt ccs (e#s)", simp)
lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"
by(ind_cases "vt ccs (e#s)", simp)
lemma holding_nil:
"\<lbrakk>wq s cs = []; holding (wq s) th cs\<rbrakk> \<Longrightarrow> False"
by (unfold cs_holding_def, auto)
lemma waiting_kept_1: "
\<lbrakk>vt step (V th cs#s); wq s cs = a # list; waiting ((wq s)(cs := ab # aa @ lista @ ca)) t c;
lsp (cp s) list = (aa, ab # lista, ca)\<rbrakk>
\<Longrightarrow> waiting (wq s) t c"
apply (drule_tac step_back_vt, drule_tac wq_distinct[of _ cs])
apply(drule_tac lsp_set_eq)
by (unfold cs_waiting_def, auto split:if_splits)
lemma waiting_kept_2:
"\<And>a list t c aa ca.
\<lbrakk>wq s cs = a # list; waiting ((wq s)(cs := [])) t c; lsp (cp s) list = (aa, [], ca)\<rbrakk>
\<Longrightarrow> waiting (wq s) t c"
apply(drule_tac lsp_set_eq)
by (unfold cs_waiting_def, auto split:if_splits)
lemma holding_nil_simp: "\<lbrakk>holding ((wq s)(cs := [])) t c\<rbrakk> \<Longrightarrow> holding (wq s) t c"
by(unfold cs_holding_def, auto)
lemma step_wq_elim: "\<lbrakk>vt step (V th cs#s); wq s cs = a # list; a \<noteq> th\<rbrakk> \<Longrightarrow> False"
apply(drule_tac step_back_step)
apply(ind_cases "step s (V th cs)")
by(unfold s_holding_def, auto)
lemma holding_cs_neq_simp: "c \<noteq> cs \<Longrightarrow> holding ((wq s)(cs := u)) t c = holding (wq s) t c"
by (unfold cs_holding_def, auto)
lemma holding_th_neq_elim:
"\<And>a list c t aa ca ab lista.
\<lbrakk>\<not> holding (wq s) t c; holding ((wq s)(cs := ab # aa @ lista @ ca)) t c;
ab \<noteq> t\<rbrakk>
\<Longrightarrow> False"
by (unfold cs_holding_def, auto split:if_splits)
lemma holding_nil_abs:
"\<not> holding ((wq s)(cs := [])) th cs"
by (unfold cs_holding_def, auto split:if_splits)
lemma holding_abs: "\<lbrakk>holding ((wq s)(cs := ab # aa @ lista @ c)) th cs; ab \<noteq> th\<rbrakk>
\<Longrightarrow> False"
by (unfold cs_holding_def, auto split:if_splits)
lemma waiting_abs: "\<not> waiting ((wq s)(cs := t # l @ r)) t cs"
by (unfold cs_waiting_def, auto split:if_splits)
lemma waiting_abs_1:
"\<lbrakk>\<not> waiting ((wq s)(cs := [])) t c; waiting (wq s) t c; c \<noteq> cs\<rbrakk>
\<Longrightarrow> False"
by (unfold cs_waiting_def, auto split:if_splits)
lemma waiting_abs_2: "
\<lbrakk>\<not> waiting ((wq s)(cs := ab # aa @ lista @ ca)) t c; waiting (wq s) t c;
c \<noteq> cs\<rbrakk>
\<Longrightarrow> False"
by (unfold cs_waiting_def, auto split:if_splits)
lemma waiting_abs_3:
"\<lbrakk>wq s cs = a # list; \<not> waiting ((wq s)(cs := [])) t c;
waiting (wq s) t c; lsp (cp s) list = (aa, [], ca)\<rbrakk>
\<Longrightarrow> False"
apply(drule_tac lsp_mid_nil, simp)
by(unfold cs_waiting_def, auto split:if_splits)
lemma waiting_simp: "c \<noteq> cs \<Longrightarrow> waiting ((wq s)(cs:=z)) t c = waiting (wq s) t c"
by(unfold cs_waiting_def, auto split:if_splits)
lemma holding_cs_eq:
"\<lbrakk>\<not> holding ((wq s)(cs := [])) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> c = cs"
by(unfold cs_holding_def, auto split:if_splits)
lemma holding_cs_eq_1:
"\<lbrakk>\<not> holding ((wq s)(cs := ab # aa @ lista @ ca)) t c; holding (wq s) t c\<rbrakk>
\<Longrightarrow> c = cs"
by(unfold cs_holding_def, auto split:if_splits)
lemma holding_th_eq:
"\<lbrakk>vt step (V th cs#s); wq s cs = a # list; \<not> holding ((wq s)(cs := [])) t c; holding (wq s) t c;
lsp (cp s) list = (aa, [], ca)\<rbrakk>
\<Longrightarrow> t = th"
apply(drule_tac lsp_mid_nil, simp)
apply(unfold cs_holding_def, auto split:if_splits)
apply(drule_tac step_back_step)
apply(ind_cases "step s (V th cs)")
by (unfold s_holding_def, auto split:if_splits)
lemma holding_th_eq_1:
"\<lbrakk>vt step (V th cs#s);
wq s cs = a # list; \<not> holding ((wq s)(cs := ab # aa @ lista @ ca)) t c; holding (wq s) t c;
lsp (cp s) list = (aa, ab # lista, ca)\<rbrakk>
\<Longrightarrow> t = th"
apply(drule_tac step_back_step)
apply(ind_cases "step s (V th cs)")
apply(unfold s_holding_def cs_holding_def)
by (auto split:if_splits)
lemma holding_th_eq_2: "\<lbrakk>holding ((wq s)(cs := ac # x)) th cs\<rbrakk>
\<Longrightarrow> ac = th"
by (unfold cs_holding_def, auto)
lemma holding_th_eq_3: "
\<lbrakk>\<not> holding (wq s) t c;
holding ((wq s)(cs := ac # x)) t c\<rbrakk>
\<Longrightarrow> ac = t"
by (unfold cs_holding_def, auto)
lemma holding_wq_eq: "holding ((wq s)(cs := th' # l @ r)) th' cs"
by (unfold cs_holding_def, auto)
lemma waiting_th_eq: "
\<lbrakk>waiting (wq s) t c; wq s cs = a # list;
lsp (cp s) list = (aa, ac # lista, ba); \<not> waiting ((wq s)(cs := ac # aa @ lista @ ba)) t c\<rbrakk>
\<Longrightarrow> ac = t"
apply(drule_tac lsp_set_eq, simp)
by (unfold cs_waiting_def, auto split:if_splits)
lemma step_depend_v:
"vt step (V th cs#s) \<Longrightarrow>
depend (V th cs # s) =
depend s - {(Cs cs, Th th)} -
{(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>
{(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"
apply (unfold s_depend_def wq_def,
auto split:list.splits simp:Let_def f_nil_simp holding_wq_eq, fold wq_def cp_def)
apply (auto split:list.splits prod.splits
simp:Let_def f_nil_simp holding_nil_simp holding_cs_neq_simp holding_nil_abs
waiting_abs waiting_simp holding_wq_eq
elim:holding_nil waiting_kept_1 waiting_kept_2 step_wq_elim holding_th_neq_elim
holding_abs waiting_abs_1 waiting_abs_3 holding_cs_eq holding_cs_eq_1
holding_th_eq holding_th_eq_1 holding_th_eq_2 holding_th_eq_3 waiting_th_eq
dest:lsp_mid_length)
done
lemma step_depend_p:
"vt step (P th cs#s) \<Longrightarrow>
depend (P th cs # s) = (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
else depend s \<union> {(Th th, Cs cs)})"
apply(unfold s_depend_def wq_def)
apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)
apply(case_tac "c = cs", auto)
apply(fold wq_def)
apply(drule_tac step_back_step)
by (ind_cases " step s (P (hd (wq s cs)) cs)",
auto simp:s_depend_def wq_def cs_holding_def)
lemma simple_A:
fixes A
assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
shows "A = {} \<or> (\<exists> a. A = {a})"
proof(cases "A = {}")
case True thus ?thesis by simp
next
case False then obtain a where "a \<in> A" by auto
with h have "A = {a}" by auto
thus ?thesis by simp
qed
lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_depend_def, auto)
lemma acyclic_depend:
fixes s
assumes vt: "vt step s"
shows "acyclic (depend s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
assume ih: "acyclic (depend s)"
and stp: "step s e"
and vt: "vt step s"
show ?case
proof(cases e)
case (Create th prio)
with ih
show ?thesis by (simp add:depend_create_unchanged)
next
case (Exit th)
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
from V vt stp have vtt: "vt step (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de: "depend (e # s) =
depend s - {(Cs cs, Th th)} -
{(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>
{(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"
(is "?L = (?A - ?B - ?C) \<union> ?D") by (simp add:V)
from ih have ac: "acyclic (?A - ?B - ?C)" by (auto elim:acyclic_subset)
have "?D = {} \<or> (\<exists> a. ?D = {a})" by (rule simple_A, auto)
thus ?thesis
proof(cases "wq s cs")
case Nil
hence "?D = {}" by simp
with ac and eq_de show ?thesis by simp
next
case (Cons tth rest)
from stp and V have "step s (V th cs)" by simp
hence eq_wq: "wq s cs = th # rest"
proof -
show "step s (V th cs) \<Longrightarrow> wq s cs = th # rest"
apply(ind_cases "step s (V th cs)")
by(insert Cons, unfold s_holding_def, simp)
qed
show ?thesis
proof(cases "lsp (cp s) rest")
fix l b r
assume eq_lsp: "lsp (cp s) rest = (l, b, r) "
show ?thesis
proof(cases "b")
case Nil
with eq_lsp and eq_wq have "?D = {}" by simp
with ac and eq_de show ?thesis by simp
next
case (Cons th' m)
with eq_lsp
have eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
apply simp
by (drule_tac lsp_mid_length, simp)
from eq_wq and eq_lsp
have eq_D: "?D = {(Cs cs, Th th')}" by auto
from eq_wq and eq_lsp
have eq_C: "?C = {(Th th', Cs cs)}" by 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 depend_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_depend_def s_waiting_def cs_waiting_def by simp
hence "cs' = cs"
proof(rule waiting_unique [OF vt])
from eq_wq eq_lsp wq_distinct[OF vt, of cs]
show "waiting s th' cs" by(unfold s_waiting_def, auto dest:lsp_set_eq)
qed
with th'_e eq_x have "(Th th', Cs cs) \<in> ?E" by simp
with eq_C show "False" by simp
qed
with acyclic_insert[symmetric] and ac and eq_D
and eq_de show ?thesis by simp
qed
qed
qed
next
case (P th cs)
from P vt stp have vtt: "vt step (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
depend 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 = depend s \<union> {(Cs cs, Th th)}" by simp
have "(Th th, Cs cs) \<notin> (depend s)\<^sup>*"
proof
assume "(Th th, Cs cs) \<in> (depend s)\<^sup>*"
hence "(Th th, Cs cs) \<in> (depend s)\<^sup>+" by (simp add: rtrancl_eq_or_trancl)
from tranclD2 [OF this]
obtain x where "(x, Cs cs) \<in> depend s" by auto
with True show False by (auto simp:s_depend_def cs_waiting_def)
qed
with acyclic_insert ih eq_r show ?thesis by auto
next
case False
hence eq_r: "?R = depend s \<union> {(Th th, Cs cs)}" by simp
have "(Cs cs, Th th) \<notin> (depend s)\<^sup>*"
proof
assume "(Cs cs, Th th) \<in> (depend s)\<^sup>*"
hence "(Cs cs, Th th) \<in> (depend 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> (depend 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 depend_set_unchanged
show ?thesis by (simp add:depend_set_unchanged)
qed
next
case vt_nil
show "acyclic (depend ([]::state))"
by (auto simp: s_depend_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
qed
qed
lemma finite_depend:
fixes s
assumes vt: "vt step s"
shows "finite (depend s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
assume ih: "finite (depend s)"
and stp: "step s e"
and vt: "vt step s"
show ?case
proof(cases e)
case (Create th prio)
with ih
show ?thesis by (simp add:depend_create_unchanged)
next
case (Exit th)
with ih show ?thesis by (simp add:depend_exit_unchanged)
next
case (V th cs)
from V vt stp have vtt: "vt step (V th cs#s)" by auto
from step_depend_v [OF this]
have eq_de: "depend (e # s) =
depend s - {(Cs cs, Th th)} -
{(Th th', Cs cs) |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))} \<union>
{(Cs cs, Th th') |th'. \<exists>rest. wq s cs = th # rest \<and> (\<exists>l r. lsp (cp s) rest = (l, [th'], r))}"
(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 (rule simple_A, auto)
thus ?thesis
proof
assume h: "?D = {}"
show ?thesis by (unfold h, simp)
next
assume "\<exists> a. ?D = {a}"
thus ?thesis by auto
qed
qed
ultimately show ?thesis by simp
next
case (P th cs)
from P vt stp have vtt: "vt step (P th cs#s)" by auto
from step_depend_p [OF this] P
have "depend (e # s) =
(if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
depend 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 = depend s \<union> {(Cs cs, Th th)}" by simp
with True and ih show ?thesis by auto
next
case False
hence "?R = depend 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:depend_set_unchanged)
qed
next
case vt_nil
show "finite (depend ([]::state))"
by (auto simp: s_depend_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
qed
qed
text {* Several useful lemmas *}
thm wf_trancl
thm finite_acyclic_wf
thm finite_acyclic_wf_converse
thm wf_induct
lemma wf_dep_converse:
fixes s
assumes vt: "vt step s"
shows "wf ((depend s)^-1)"
proof(rule finite_acyclic_wf_converse)
from finite_depend [OF vt]
show "finite (depend s)" .
next
from acyclic_depend[OF vt]
show "acyclic (depend 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> depend (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> depend s"
by (auto simp:s_depend_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 step 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 step 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_depend_def s_holding_def cs_holding_def)
by (fold wq_def, auto)
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 (waiting_queue (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 = waiting_queue (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 "waiting_queue (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: "waiting_queue (schs s) cs' = a # rest"
with h V show ?thesis
proof(cases "(lsp (cur_preced (schs s)) rest)", unfold V)
fix l m r
assume eq_lsp: "lsp (cur_preced (schs s)) rest = (l, m, r)"
and eq_wq: "waiting_queue (schs s) cs' = a # rest"
and th_in_set: "th \<in> set (wq (V th' cs' # s) cs)"
show ?thesis
proof(cases "m")
case Nil
with eq_lsp have "rest = []" using lsp_mid_nil by auto
with eq_wq have "waiting_queue (schs s) cs' = [a]" by simp
with h[unfolded V wq_def] True
show ?thesis
by (simp add:Let_def)
next
case (Cons b rb)
with lsp_mid_length[OF eq_lsp] have eq_m: "m = [b]" by auto
with eq_lsp have "lsp (cur_preced (schs s)) rest = (l, [b], r)" by simp
with h[unfolded V wq_def] True lsp_set_eq [OF this] eq_wq
show ?thesis
apply (auto simp:Let_def, fold wq_def)
by (rule_tac ih [of _ cs'], auto)+
qed
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 step s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_depend_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
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 prems show ?thesis
apply (auto simp:readys_def)
apply (case_tac "cs = csa", simp add:s_waiting_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)
by (auto simp:s_waiting_def wq_def Let_def split:list.splits prod.splits
dest:lsp_set_eq)
qed
lemma readys_v_eq_1:
fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
and neq_th': "th \<noteq> th'"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
proof -
from prems show ?thesis
apply (auto simp:readys_def)
apply (case_tac "cs = csa", simp add:s_waiting_def)
apply (erule_tac x = cs in allE)
apply (simp add:s_waiting_def wq_def Let_def split:prod.splits list.splits)
apply (drule_tac lsp_mid_nil,simp, clarify, fold cp_def, clarsimp)
apply (frule_tac lsp_set_eq, simp)
apply (erule_tac x = csa in allE)
apply (subst (asm) (2) s_waiting_def, unfold wq_def)
apply (auto simp:Let_def split:list.splits prod.splits if_splits
dest:lsp_set_eq)
apply (unfold s_waiting_def)
apply (fold wq_def, clarsimp)
apply (clarsimp)+
apply (case_tac "csa = cs", simp)
apply (erule_tac x = cs in allE, simp)
apply (unfold wq_def)
by (auto simp:Let_def split:list.splits prod.splits if_splits
dest:lsp_set_eq)
qed
lemma readys_v_eq_2:
fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
and neq_th': "th = th'"
and vt: "vt step s"
shows "(th \<in> readys (V thread cs#s))"
proof -
from prems show ?thesis
apply (auto simp:readys_def)
apply (rule_tac wq_threads [of s _ cs], auto dest:lsp_set_eq)
apply (unfold s_waiting_def wq_def)
apply (auto simp:Let_def split:list.splits prod.splits if_splits
dest:lsp_set_eq lsp_mid_nil lsp_mid_length)
apply (fold cp_def, simp+, clarsimp)
apply (frule_tac lsp_set_eq, simp)
apply (fold wq_def)
apply (subgoal_tac "csa = cs", simp)
apply (rule_tac waiting_unique [of s th'], simp)
by (auto simp:s_waiting_def)
qed
lemma chain_building:
assumes vt: "vt step s"
shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)"
proof -
from wf_dep_converse [OF vt]
have h: "wf ((depend s)\<inverse>)" .
show ?thesis
proof(induct rule:wf_induct [OF h])
fix x
assume ih [rule_format]:
"\<forall>y. (y, x) \<in> (depend s)\<inverse> \<longrightarrow>
y \<in> Domain (depend s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (y, Th th') \<in> (depend s)\<^sup>+)"
show "x \<in> Domain (depend s) \<longrightarrow> (\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (depend s)\<^sup>+)"
proof
assume x_d: "x \<in> Domain (depend s)"
show "\<exists>th'. th' \<in> readys s \<and> (x, Th th') \<in> (depend s)\<^sup>+"
proof(cases x)
case (Th th)
from x_d Th obtain cs where x_in: "(Th th, Cs cs) \<in> depend s" by (auto simp:s_depend_def)
with Th have x_in_r: "(Cs cs, x) \<in> (depend s)^-1" by simp
from th_chasing [OF x_in] obtain th' where "(Cs cs, Th th') \<in> depend s" by blast
hence "Cs cs \<in> Domain (depend 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> (depend s)\<^sup>+" by auto
have "(x, Th th') \<in> (depend 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> (depend s)^-1" by (auto simp:s_depend_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 (depend s)"
by (auto simp:readys_def s_waiting_def s_depend_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> (depend s)\<^sup>+" by auto
from th'_d and th''_in
have "(x, Th th'') \<in> (depend s)\<^sup>+" by auto
with th''_r show ?thesis by auto
qed
qed
qed
qed
qed
lemma th_chain_to_ready:
fixes s th
assumes vt: "vt step 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> (depend 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 (depend s)"
by (auto simp:readys_def s_waiting_def s_depend_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, auto)
lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
by (unfold s_holding_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_depend: "\<lbrakk>vt step s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_depend_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 step s"
and th1_d: "(n, Th th1) \<in> (depend s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (depend 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_depend [OF vt]
have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
hence "False"
proof
assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+"
from trancl_split [OF this]
obtain n where dd: "(Th th1, n) \<in> depend s" by auto
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_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_depend_def s_waiting_def cs_waiting_def)
with th1_r show ?thesis by auto
next
assume "(Th th2, Th th1) \<in> (depend s)\<^sup>+"
from trancl_split [OF this]
obtain n where dd: "(Th th2, n) \<in> depend s" by auto
then obtain cs where eq_n: "n = Cs cs"
by (auto simp:s_depend_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 s_depend_def s_waiting_def cs_waiting_def)
with th2_r show ?thesis by auto
qed
} thus ?thesis by auto
qed
definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
where "count Q l = length (filter Q l)"
definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
lemma step_holdents_p_add:
fixes th cs s
assumes vt: "vt step (P th cs#s)"
and "wq s cs = []"
shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
proof -
from prems show ?thesis
unfolding holdents_def step_depend_p[OF vt] by auto
qed
lemma step_holdents_p_eq:
fixes th cs s
assumes vt: "vt step (P th cs#s)"
and "wq s cs \<noteq> []"
shows "holdents (P th cs#s) th = holdents s th"
proof -
from prems show ?thesis
unfolding holdents_def step_depend_p[OF vt] by auto
qed
lemma step_holdents_v_minus:
fixes th cs s
assumes vt: "vt step (V th cs#s)"
shows "holdents (V th cs#s) th = holdents s th - {cs}"
proof -
{ fix rest l r
assume eq_wq: "wq s cs = th # rest"
and eq_lsp: "lsp (cp s) rest = (l, [th], r)"
have "False"
proof -
from lsp_set_eq [OF eq_lsp] have " rest = l @ [th] @ r" .
with eq_wq have "wq s cs = th#\<dots>" by simp
with wq_distinct [OF step_back_vt[OF vt], of cs]
show ?thesis by auto
qed
} thus ?thesis unfolding holdents_def step_depend_v[OF vt] by auto
qed
lemma step_holdents_v_add:
fixes th th' cs s rest l r
assumes vt: "vt step (V th' cs#s)"
and neq_th: "th \<noteq> th'"
and eq_wq: "wq s cs = th' # rest"
and eq_lsp: "lsp (cp s) rest = (l, [th], r)"
shows "holdents (V th' cs#s) th = holdents s th \<union> {cs}"
proof -
from prems show ?thesis
unfolding holdents_def step_depend_v[OF vt] by auto
qed
lemma step_holdents_v_eq:
fixes th th' cs s rest l r th''
assumes vt: "vt step (V th' cs#s)"
and neq_th: "th \<noteq> th'"
and eq_wq: "wq s cs = th' # rest"
and eq_lsp: "lsp (cp s) rest = (l, [th''], r)"
and neq_th': "th \<noteq> th''"
shows "holdents (V th' cs#s) th = holdents s th"
proof -
from prems show ?thesis
unfolding holdents_def step_depend_v[OF vt] by auto
qed
definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntCS s th = card (holdents s th)"
lemma cntCS_v_eq:
fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
and vtv: "vt step (V thread cs#s)"
shows "cntCS (V thread cs#s) th = cntCS s th"
proof -
from prems show ?thesis
apply (unfold cntCS_def holdents_def step_depend_v)
apply auto
apply (subgoal_tac "\<not> (\<exists>l r. lsp (cp s) rest = (l, [th], r))", auto)
by (drule_tac lsp_set_eq, auto)
qed
lemma cntCS_v_eq_1:
fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
and neq_th': "th \<noteq> th'"
and vtv: "vt step (V thread cs#s)"
shows "cntCS (V thread cs#s) th = cntCS s th"
proof -
from prems show ?thesis
apply (unfold cntCS_def holdents_def step_depend_v)
by auto
qed
fun the_cs :: "node \<Rightarrow> cs"
where "the_cs (Cs cs) = cs"
lemma cntCS_v_eq_2:
fixes th thread cs rest
assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
and neq_th': "th = th'"
and vtv: "vt step (V thread cs#s)"
shows "cntCS (V thread cs#s) th = 1 + cntCS s th"
proof -
have "card {csa. csa = cs \<or> (Cs csa, Th th') \<in> depend s} =
Suc (card {cs. (Cs cs, Th th') \<in> depend s})"
(is "card ?A = Suc (card ?B)")
proof -
have h: "?A = insert cs ?B" by auto
moreover have h1: "?B = ?B - {cs}"
proof -
{ assume "(Cs cs, Th th') \<in> depend s"
moreover have "(Th th', Cs cs) \<in> depend s"
proof -
from wq_distinct [OF step_back_vt[OF vtv], of cs]
eq_wq lsp_set_eq [OF eq_lsp] show ?thesis
apply (auto simp:s_depend_def)
by (unfold cs_waiting_def, auto)
qed
moreover note acyclic_depend [OF step_back_vt[OF vtv]]
ultimately have "False"
apply (auto simp:acyclic_def)
apply (erule_tac x="Cs cs" in allE)
apply (subgoal_tac "(Cs cs, Cs cs) \<in> (depend s)\<^sup>+", simp)
by (rule_tac trancl_into_trancl [where b = "Th th'"], auto)
} thus ?thesis by auto
qed
moreover have "card (insert cs ?B) = Suc (card (?B - {cs}))"
proof(rule card_insert)
from finite_depend [OF step_back_vt [OF vtv]]
have fnt: "finite (depend s)" .
show " finite {cs. (Cs cs, Th th') \<in> depend s}" (is "finite ?B")
proof -
have "?B \<subseteq> (\<lambda> (a, b). the_cs a) ` (depend s)"
apply (auto simp:image_def)
by (rule_tac x = "(Cs x, Th th')" in bexI, auto)
with fnt show ?thesis by (auto intro:finite_subset)
qed
qed
ultimately show ?thesis by simp
qed
with prems show ?thesis
apply (unfold cntCS_def holdents_def step_depend_v[OF vtv])
by auto
qed
lemma finite_holding:
fixes s th cs
assumes vt: "vt step s"
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
from finite_depend [OF vt]
have "finite (depend s)" .
hence "finite (?F `(depend s))" by simp
moreover have "{cs . (Cs cs, Th th) \<in> depend 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> depend s"
hence "?F (Cs x, Th th) \<in> ?F `(depend s)" by (rule h)
moreover have "?F (Cs x, Th th) = x" by simp
ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp
} thus ?thesis by auto
qed
ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset)
qed
inductive_cases case_step_v: "step s (V thread cs)"
lemma cntCS_v_dec:
fixes s thread cs
assumes vtv: "vt step (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
have cs_in: "cs \<in> holdents s thread" using step_back_step[OF vtv]
apply (erule_tac case_step_v)
apply (unfold holdents_def s_depend_def, simp)
by (unfold cs_holding_def s_holding_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])
by (unfold holdents_def, unfold step_depend_v[OF vtv],
auto dest:lsp_set_eq)
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
lemma cnp_cnv_cncs:
fixes s th
assumes vt: "vt step 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 step 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 prio max_prio thread)
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_def
by (simp add:depend_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_def
by (simp add:depend_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 (subst (1 2) wq_def)
apply (simp add:Let_def)
apply (subst s_waiting_def, simp)
by (fold wq_def, simp)
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> (depend s)\<^sup>+"
from prems have vtp: "vt step (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, clarify)
apply (intro iffI allI, clarify)
apply (erule_tac x = csa in allE, auto)
apply (subgoal_tac "waiting_queue (schs s) cs \<noteq> []", auto)
apply (erule_tac x = cs in allE, auto)
by (case_tac "(waiting_queue (schs s) cs)", auto)
moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
apply (simp add:cntCS_def holdents_def)
by (unfold step_depend_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_depend_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> depend s} =
Suc (card {cs. (Cs cs, Th thread) \<in> depend 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> depend s}"
by (unfold holdents_def, simp)
qed
moreover have "?R - {cs} = ?R"
proof -
have "cs \<notin> ?R"
proof
assume "cs \<in> {cs. (Cs cs, Th thread) \<in> depend 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_def)
by (unfold step_depend_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)
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_def eq_e step_depend_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 prems have vtv: "vt step (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:s_holding_def)
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
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 -
have "thread \<notin> set (wq (e#s) cs1)"
proof(cases "lsp (cp s) rest")
fix l m r
assume h: "lsp (cp s) rest = (l, m, r)"
show ?thesis
proof(cases "m")
case Nil
from wq_v_eq_nil [OF eq_wq] h Nil eq_e
have " wq (e # s) cs = []" by auto
thus ?thesis using eq_cs by auto
next
case (Cons th' l')
from lsp_mid_length [OF h] and Cons h
have eqh: "lsp (cp s) rest = (l, [th'], r)" by auto
from wq_v_eq [OF eq_wq this]
have "wq (V thread cs # s) cs = th' # l @ r" .
moreover from lsp_set_eq [OF eqh]
have "set rest = set \<dots>" by auto
moreover have "thread \<notin> set rest"
proof -
from wq_distinct [OF step_back_vt[OF vtv], of cs]
and eq_wq show ?thesis by auto
qed
moreover note eq_e eq_cs
ultimately show ?thesis by simp
qed
qed
thus ?thesis by (simp add: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: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)"
by(unfold eq_e, rule readys_v_eq [OF neq_th eq_wq False])
moreover have "cntCS (e#s) th = cntCS s th"
by(unfold eq_e, rule cntCS_v_eq [OF neq_th eq_wq False vtv])
moreover note ih eq_cnp eq_cnv eq_threads
ultimately show ?thesis by auto
next
case True
obtain l m r where eq_lsp: "lsp (cp s) rest = (l, m, r)"
by (cases "lsp (cp s) rest", auto)
with True have "m \<noteq> []" by (auto dest:lsp_mid_nil)
with eq_lsp obtain th' where eq_lsp: "lsp (cp s) rest = (l, [th'], r)"
by (case_tac m, auto dest:lsp_mid_length)
show ?thesis
proof(cases "th = th'")
case False
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
by (unfold eq_e, rule readys_v_eq_1 [OF neq_th eq_wq eq_lsp False])
moreover have "cntCS (e#s) th = cntCS s th"
by (unfold eq_e, rule cntCS_v_eq_1[OF neq_th eq_wq eq_lsp False vtv])
moreover note ih eq_cnp eq_cnv eq_threads
ultimately show ?thesis by auto
next
case True
have "th \<in> readys (e # s)"
by (unfold eq_e, rule readys_v_eq_2 [OF neq_th eq_wq eq_lsp True vt])
moreover have "cntP s th = cntV s th + cntCS s th + 1"
proof -
have "th \<notin> readys s"
proof -
from True eq_wq lsp_set_eq [OF eq_lsp] neq_th
show ?thesis
apply (unfold readys_def s_waiting_def, auto)
by (rule_tac x = cs in exI, auto)
qed
moreover have "th \<in> threads s"
proof -
from True eq_wq lsp_set_eq [OF eq_lsp] neq_th
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 have "cntCS (e # s) th = 1 + cntCS s th"
by (unfold eq_e, rule cntCS_v_eq_2 [OF neq_th eq_wq eq_lsp True vtv])
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_def
by (simp add:depend_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_def s_depend_def wq_def cs_holding_def)
qed
qed
lemma not_thread_cncs:
fixes th s
assumes vt: "vt step 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 step 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 prio max_prio thread)
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_def)
by (simp add:depend_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_def)
by (simp add:depend_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 prems have vtp: "vt step (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_def eq_e)
by (unfold step_depend_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 prems have vtv: "vt step (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:s_holding_def)
have "cntCS (e # s) th = cntCS s th"
proof(unfold eq_e, rule cntCS_v_eq [OF neq_th eq_wq _ vtv])
show "th \<notin> set rest"
proof
assume "th \<in> set rest"
with eq_wq have "th \<in> set (wq s cs)" by simp
from wq_threads [OF vt this] eq_e not_in
show False by simp
qed
qed
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_def)
by (simp add:depend_set_unchanged)
qed
next
case vt_nil
show ?case
by (unfold cntCS_def,
auto simp:count_def holdents_def s_depend_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)
lemma dm_depend_threads:
fixes th s
assumes vt: "vt step s"
and in_dom: "(Th th) \<in> Domain (depend s)"
shows "th \<in> threads s"
proof -
from in_dom obtain n where "(Th th, n) \<in> depend s" by auto
moreover from depend_target_th[OF this] obtain cs where "n = Cs cs" by auto
ultimately have "(Th th, Cs cs) \<in> depend s" by simp
hence "th \<in> set (wq s cs)"
by (unfold s_depend_def, auto simp:cs_waiting_def)
from wq_threads [OF vt this] show ?thesis .
qed
lemma cp_eq_cpreced: "cp s th = cpreced s (wq s) th"
proof(unfold cp_def wq_def, induct s)
case (Cons e s')
show ?case
by (auto simp:Let_def)
next
case Nil
show ?case by (auto simp:Let_def)
qed
fun the_th :: "node \<Rightarrow> thread"
where "the_th (Th th) = th"
lemma runing_unique:
fixes th1 th2 s
assumes vt: "vt step 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"
by (unfold runing_def, simp)
hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)) =
Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependents (wq s) th2))"
(is "Max (?f ` ?A) = Max (?f ` ?B)")
by (unfold cp_eq_cpreced 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 (dependents (wq s) th1)"
proof-
have "finite {th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (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_depend[OF vt] have "finite (depend s)" .
hence "finite ((depend (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_depend_def cs_depend_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependents_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 by (auto intro:that)
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 (dependents (wq s) th2)"
proof-
have "finite {th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (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_depend[OF vt] have "finite (depend s)" .
hence "finite ((depend (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_depend_def cs_depend_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependents_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> dependents (wq s) th1)" by simp
thus "th1' \<in> threads s"
proof
assume "th1' \<in> dependents (wq s) th1"
hence "(Th th1') \<in> Domain ((depend s)^+)"
apply (unfold cs_dependents_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_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> dependents (wq s) th2)" by simp
thus "th2' \<in> threads s"
proof
assume "th2' \<in> dependents (wq s) th2"
hence "(Th th2') \<in> Domain ((depend s)^+)"
apply (unfold cs_dependents_def cs_depend_def s_depend_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (depend s)" by (simp add:trancl_domain)
from dm_depend_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> dependents (wq s) th1" by simp
thus ?thesis
proof
assume eq_th': "th1' = th1"
from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp
next
assume "th2' \<in> dependents (wq s) th2"
with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
hence "(Th th1, Th th2) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
hence "Th th1 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
by auto
hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
from depend_target_th [OF this]
obtain cs' where "n = Cs cs'" by auto
with d have "(Th th1, Cs cs') \<in> depend s" by simp
with runing_1 have "False"
apply (unfold runing_def readys_def s_depend_def)
by (auto simp:eq_waiting)
thus ?thesis by simp
qed
next
assume th1'_in: "th1' \<in> dependents (wq s) th1"
from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
thus ?thesis
proof
assume "th2' = th2"
with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
hence "(Th th2, Th th1) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
hence "Th th2 \<in> Domain ((depend s)^+)" using Domain_def [of "(depend s)^+"]
by auto
hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
from depend_target_th [OF this]
obtain cs' where "n = Cs cs'" by auto
with d have "(Th th2, Cs cs') \<in> depend s" by simp
with runing_2 have "False"
apply (unfold runing_def readys_def s_depend_def)
by (auto simp:eq_waiting)
thus ?thesis by simp
next
assume "th2' \<in> dependents (wq s) th2"
with eq_th12 have "th1' \<in> dependents (wq s) th2" by simp
hence h1: "(Th th1', Th th2) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
from th1'_in have h2: "(Th th1', Th th1) \<in> (depend s)^+"
by (unfold cs_dependents_def s_depend_def cs_depend_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 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 prio max_prio thread)
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 step s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
proof -
from assms show ?thesis
proof(induct)
case (vt_cons s e)
have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
have not_in: "th \<notin> threads (e # s)" by fact
have "step s e" by fact
thus ?case proof(cases)
case (thread_create prio max_prio thread)
assume eq_e: "e = Create thread prio"
hence "thread \<in> threads (e#s)" by simp
with not_in and eq_e have "th \<notin> threads s" by auto
from ih [OF this] show ?thesis using eq_e
by (auto simp:cntP_def cntV_def count_def)
next
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and not_holding: "holdents s thread = {}"
have vt_s: "vt step s" by fact
from finite_holding[OF vt_s] have "finite (holdents s thread)" .
with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
moreover note cnp_cnv_cncs[OF vt_s, of thread]
ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
show ?thesis
proof(cases "th = thread")
case True
with eq_thread eq_e show ?thesis
by (auto simp:cntP_def cntV_def count_def)
next
case False
with not_in and eq_e have "th \<notin> threads s" by simp
from ih[OF this] and eq_e show ?thesis
by (auto simp:cntP_def cntV_def count_def)
qed
next
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
have "thread \<in> runing s" by fact
with not_in eq_e have neq_th: "thread \<noteq> th"
by (auto simp:runing_def readys_def)
from not_in eq_e have "th \<notin> threads s" by simp
from ih[OF this] and neq_th and eq_e show ?thesis
by (auto simp:cntP_def cntV_def count_def)
next
case (thread_V thread cs)
assume eq_e: "e = V thread cs"
have "thread \<in> runing s" by fact
with not_in eq_e have neq_th: "thread \<noteq> th"
by (auto simp:runing_def readys_def)
from not_in eq_e have "th \<notin> threads s" by simp
from ih[OF this] and neq_th and eq_e show ?thesis
by (auto simp:cntP_def cntV_def count_def)
next
case (thread_set thread prio)
assume eq_e: "e = Set thread prio"
and "thread \<in> runing s"
hence "thread \<in> threads (e#s)"
by (simp add:runing_def readys_def)
with not_in and eq_e have "th \<notin> threads s" by auto
from ih [OF this] show ?thesis using eq_e
by (auto simp:cntP_def cntV_def count_def)
qed
next
case vt_nil
show ?case by (auto simp:cntP_def cntV_def count_def)
qed
qed
lemma eq_depend:
"depend (wq s) = depend s"
by (unfold cs_depend_def s_depend_def, auto)
lemma count_eq_dependents:
assumes vt: "vt step s"
and eq_pv: "cntP s th = cntV s th"
shows "dependents (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> depend s}"
proof -
from finite_holding[OF vt, of th] show ?thesis
by (simp add:holdents_def)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
by (unfold cntCS_def holdents_def cs_dependents_def, auto)
show ?thesis
proof(unfold cs_dependents_def)
{ assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto
hence "False"
proof(cases)
assume "(Th th', Th th) \<in> depend (wq s)"
thus "False" by (auto simp:cs_depend_def)
next
fix c
assume "(c, Th th) \<in> depend (wq s)"
with h and eq_depend show "False"
by (cases c, auto simp:cs_depend_def)
qed
} thus "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} = {}" by auto
qed
qed
lemma dependents_threads:
fixes s th
assumes vt: "vt step s"
shows "dependents (wq s) th \<subseteq> threads s"
proof
{ fix th th'
assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (depend (wq s))\<^sup>+}"
have "Th th \<in> Domain (depend s)"
proof -
from h obtain th' where "(Th th, Th th') \<in> (depend (wq s))\<^sup>+" by auto
hence "(Th th) \<in> Domain ( (depend (wq s))\<^sup>+)" by (auto simp:Domain_def)
with trancl_domain have "(Th th) \<in> Domain (depend (wq s))" by simp
thus ?thesis using eq_depend by simp
qed
from dm_depend_threads[OF vt this]
have "th \<in> threads s" .
} note hh = this
fix th1
assume "th1 \<in> dependents (wq s) th"
hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (depend (wq s))\<^sup>+}"
by (unfold cs_dependents_def, simp)
from hh [OF this] show "th1 \<in> threads s" .
qed
lemma finite_threads:
assumes vt: "vt step s"
shows "finite (threads s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
assume vt: "vt step s"
and step: "step s e"
and ih: "finite (threads s)"
from step
show ?case
proof(cases)
case (thread_create prio max_prio thread)
assume eq_e: "e = Create thread prio"
with ih
show ?thesis by (unfold eq_e, auto)
next
case (thread_exit thread)
assume eq_e: "e = Exit thread"
with ih show ?thesis
by (unfold eq_e, auto)
next
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
with ih show ?thesis by (unfold eq_e, auto)
next
case (thread_V thread cs)
assume eq_e: "e = V thread cs"
with ih show ?thesis by (unfold eq_e, auto)
next
case (thread_set thread prio)
from vt_cons thread_set show ?thesis by simp
qed
next
case vt_nil
show ?case by (auto)
qed
qed
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
and np: "A \<noteq> {}"
and fnt: "finite B"
shows "Max (f ` A) \<le> Max (f ` B)"
proof(rule Max_mono)
from seq show "f ` A \<subseteq> f ` B" by auto
next
from np show "f ` A \<noteq> {}" by auto
next
from fnt and seq show "finite (f ` B)" by auto
qed
lemma cp_le:
assumes vt: "vt step 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_dependents_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (depend (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> (depend (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> (depend (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
apply (rule_tac dm_depend_threads[OF vt])
apply (unfold trancl_domain [of "depend s", symmetric])
by (unfold cs_depend_def s_depend_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
assumes vt: "vt step s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (original_priority th s) (birthtime th s)
\<le> Max (insert (Prc (original_priority th s) (birthtime th s))
((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (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> (depend (wq s))\<^sup>+}"
proof -
let ?F = "\<lambda> (x, y). the_th x"
have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (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_depend[OF vt] have "finite (depend s)" .
hence "finite ((depend (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_depend_def cs_depend_def wq_def)
thus ?thesis by auto
qed
ultimately show ?thesis by (auto intro:finite_subset)
qed
thus ?thesis by (simp add:cs_dependents_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 step 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 step 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> (depend s)\<^sup>+)" .
thus ?thesis
proof
assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (depend s)\<^sup>+ "
then obtain th' where th'_in: "th' \<in> readys s"
and tm_chain:"(Th tm, Th th') \<in> (depend s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
from dependents_threads[OF vt] finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th'))"
by (auto intro:finite_subset)
next
fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (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 dependents_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> dependents (wq s) th')"
proof -
from tm_chain
have "tm \<in> dependents (wq s) th'"
by (unfold cs_dependents_def s_depend_def cs_depend_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 dependents_threads [OF vt, of th1] th1_in
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (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> dependents (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> dependents (wq s) tm)"
show "y \<le> preced tm s"
proof -
{ fix y'
assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependents (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
from hy' dependents_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 dependents_threads[OF vt, of tm] finite_threads[OF vt]
show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm))"
by (auto intro:finite_subset)
next
show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (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> dependents (wq s) th1) \<noteq> {}"
by simp
next
from dependents_threads[OF vt, of th1] th1_readys
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (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
lemma max_cp_readys_threads:
assumes vt: "vt step 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 readys_threads:
shows "readys s \<subseteq> threads s"
proof
fix th
assume "th \<in> readys s"
thus "th \<in> threads s"
by (unfold readys_def, auto)
qed
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
apply (unfold s_holding_def cs_holding_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
end