theory CpsG
imports PIPDefs
begin
lemma Max_fg_mono:
assumes "finite A"
and "\<forall> a \<in> A. f a \<le> g a"
shows "Max (f ` A) \<le> Max (g ` A)"
proof(cases "A = {}")
case True
thus ?thesis by auto
next
case False
show ?thesis
proof(rule Max.boundedI)
from assms show "finite (f ` A)" by auto
next
from False show "f ` A \<noteq> {}" by auto
next
fix fa
assume "fa \<in> f ` A"
then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
show "fa \<le> Max (g ` A)"
proof(rule Max_ge_iff[THEN iffD2])
from assms show "finite (g ` A)" by auto
next
from False show "g ` A \<noteq> {}" by auto
next
from h_fa have "g a \<in> g ` A" by auto
moreover have "fa \<le> g a" using h_fa assms(2) by auto
ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
qed
qed
qed
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
and np: "A \<noteq> {}"
and fnt: "finite B"
shows "Max (f ` A) \<le> Max (f ` B)"
proof(rule Max_mono)
from seq show "f ` A \<subseteq> f ` B" by auto
next
from np show "f ` A \<noteq> {}" by auto
next
from fnt and seq show "finite (f ` B)" by auto
qed
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
lemma waiting_holding:
assumes "waiting (s::state) th cs"
obtains th' where "holding s th' cs"
proof -
from assms[unfolded s_waiting_def, folded wq_def]
obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"
by (metis empty_iff hd_in_set list.set(1))
hence "holding s th' cs"
by (unfold s_holding_def, fold wq_def, auto)
from that[OF this] show ?thesis .
qed
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
apply(simp add: Let_def cpreced_initial)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
done
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "Max (_ ` ?L) = Max (_ ` ?R)")
proof -
have "?L = ?R"
by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
thus ?thesis by simp
qed
thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
qed
(* ccc *)
locale valid_trace =
fixes s
assumes vt : "vt s"
locale valid_trace_e = valid_trace +
fixes e
assumes vt_e: "vt (e#s)"
begin
lemma pip_e: "PIP s e"
using vt_e by (cases, simp)
end
locale valid_trace_create = valid_trace_e +
fixes th prio
assumes is_create: "e = Create th prio"
locale valid_trace_exit = valid_trace_e +
fixes th
assumes is_exit: "e = Exit th"
locale valid_trace_p = valid_trace_e +
fixes th cs
assumes is_p: "e = P th cs"
locale valid_trace_v = valid_trace_e +
fixes th cs
assumes is_v: "e = V th cs"
begin
definition "rest = tl (wq s cs)"
definition "wq' = (SOME q. distinct q \<and> set q = set rest)"
end
locale valid_trace_v_n = valid_trace_v +
assumes rest_nnl: "rest \<noteq> []"
locale valid_trace_v_e = valid_trace_v +
assumes rest_nil: "rest = []"
locale valid_trace_set= valid_trace_e +
fixes th prio
assumes is_set: "e = Set th prio"
context valid_trace
begin
lemma ind [consumes 0, case_names Nil Cons, induct type]:
assumes "PP []"
and "(\<And>s e. valid_trace_e s e \<Longrightarrow>
PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
shows "PP s"
proof(induct rule:vt.induct[OF vt, case_names Init Step])
case Init
from assms(1) show ?case .
next
case (Step s e)
show ?case
proof(rule assms(2))
show "valid_trace_e s e" using Step by (unfold_locales, auto)
next
show "PP s" using Step by simp
next
show "PIP s e" using Step by simp
qed
qed
lemma vt_moment: "\<And> t. vt (moment t s)"
proof(induct rule:ind)
case Nil
thus ?case by (simp add:vt_nil)
next
case (Cons s e t)
show ?case
proof(cases "t \<ge> length (e#s)")
case True
from True have "moment t (e#s) = e#s" by simp
thus ?thesis using Cons
by (simp add:valid_trace_def valid_trace_e_def, auto)
next
case False
from Cons have "vt (moment t s)" by simp
moreover have "moment t (e#s) = moment t s"
proof -
from False have "t \<le> length s" by simp
from moment_app [OF this, of "[e]"]
show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
qed
lemma finite_threads:
shows "finite (threads s)"
using vt by (induct) (auto elim: step.cases)
end
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
locale valid_moment = valid_trace +
fixes i :: nat
sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
by (unfold_locales, insert vt_moment, auto)
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 runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
by auto
lemma readys_threads:
shows "readys s \<subseteq> threads s"
unfolding readys_def
by auto
lemma wq_v_neq [simp]:
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
lemma runing_head:
assumes "th \<in> runing s"
and "th \<in> set (wq_fun (schs s) cs)"
shows "th = hd (wq_fun (schs s) cs)"
using assms
by (simp add:runing_def readys_def s_waiting_def wq_def)
context valid_trace
begin
lemma runing_wqE:
assumes "th \<in> runing s"
and "th \<in> set (wq s cs)"
obtains rest where "wq s cs = th#rest"
proof -
from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"
by (meson list.set_cases)
have "th' = th"
proof(rule ccontr)
assume "th' \<noteq> th"
hence "th \<noteq> hd (wq s cs)" using eq_wq by auto
with assms(2)
have "waiting s th cs"
by (unfold s_waiting_def, fold wq_def, auto)
with assms show False
by (unfold runing_def readys_def, auto)
qed
with eq_wq that show ?thesis by metis
qed
end
context valid_trace_create
begin
lemma wq_neq_simp [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_create wq_def
by (auto simp:Let_def)
lemma wq_distinct_kept:
assumes "distinct (wq s cs')"
shows "distinct (wq (e#s) cs')"
using assms by simp
end
context valid_trace_exit
begin
lemma wq_neq_simp [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_exit wq_def
by (auto simp:Let_def)
lemma wq_distinct_kept:
assumes "distinct (wq s cs')"
shows "distinct (wq (e#s) cs')"
using assms by simp
end
context valid_trace_p
begin
lemma wq_neq_simp [simp]:
assumes "cs' \<noteq> cs"
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_p wq_def
by (auto simp:Let_def)
lemma runing_th_s:
shows "th \<in> runing s"
proof -
from pip_e[unfolded is_p]
show ?thesis by (cases, simp)
qed
lemma ready_th_s: "th \<in> readys s"
using runing_th_s
by (unfold runing_def, auto)
lemma live_th_s: "th \<in> threads s"
using readys_threads ready_th_s by auto
lemma live_th_es: "th \<in> threads (e#s)"
using live_th_s
by (unfold is_p, simp)
lemma th_not_waiting:
"\<not> waiting s th c"
proof -
have "th \<in> readys s"
using runing_ready runing_th_s by blast
thus ?thesis
by (unfold readys_def, auto)
qed
lemma waiting_neq_th:
assumes "waiting s t c"
shows "t \<noteq> th"
using assms using th_not_waiting by blast
lemma th_not_in_wq:
shows "th \<notin> set (wq s cs)"
proof
assume otherwise: "th \<in> set (wq s cs)"
from runing_wqE[OF runing_th_s this]
obtain rest where eq_wq: "wq s cs = th#rest" by blast
with otherwise
have "holding s th cs"
by (unfold s_holding_def, fold wq_def, simp)
hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
by (unfold s_RAG_def, fold holding_eq, auto)
from pip_e[unfolded is_p]
show False
proof(cases)
case (thread_P)
with cs_th_RAG show ?thesis by auto
qed
qed
lemma wq_es_cs:
"wq (e#s) cs = wq s cs @ [th]"
by (unfold is_p wq_def, auto simp:Let_def)
lemma wq_distinct_kept:
assumes "distinct (wq s cs')"
shows "distinct (wq (e#s) cs')"
proof(cases "cs' = cs")
case True
show ?thesis using True assms th_not_in_wq
by (unfold True wq_es_cs, auto)
qed (insert assms, simp)
end
context valid_trace_v
begin
lemma wq_neq_simp [simp]:
assumes "cs' \<noteq> cs"
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_v wq_def
by (auto simp:Let_def)
lemma runing_th_s:
shows "th \<in> runing s"
proof -
from pip_e[unfolded is_v]
show ?thesis by (cases, simp)
qed
lemma th_not_waiting:
"\<not> waiting s th c"
proof -
have "th \<in> readys s"
using runing_ready runing_th_s by blast
thus ?thesis
by (unfold readys_def, auto)
qed
lemma waiting_neq_th:
assumes "waiting s t c"
shows "t \<noteq> th"
using assms using th_not_waiting by blast
lemma wq_s_cs:
"wq s cs = th#rest"
proof -
from pip_e[unfolded is_v]
show ?thesis
proof(cases)
case (thread_V)
from this(2) show ?thesis
by (unfold rest_def s_holding_def, fold wq_def,
metis empty_iff list.collapse list.set(1))
qed
qed
lemma wq_es_cs:
"wq (e#s) cs = wq'"
using wq_s_cs[unfolded wq_def]
by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp)
lemma wq_distinct_kept:
assumes "distinct (wq s cs')"
shows "distinct (wq (e#s) cs')"
proof(cases "cs' = cs")
case True
show ?thesis
proof(unfold True wq_es_cs wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
using assms[unfolded True wq_s_cs] by auto
qed simp
qed (insert assms, simp)
end
context valid_trace_set
begin
lemma wq_neq_simp [simp]:
shows "wq (e#s) cs' = wq s cs'"
using assms unfolding is_set wq_def
by (auto simp:Let_def)
lemma wq_distinct_kept:
assumes "distinct (wq s cs')"
shows "distinct (wq (e#s) cs')"
using assms by simp
end
context valid_trace
begin
lemma actor_inv:
assumes "PIP s e"
and "\<not> isCreate e"
shows "actor e \<in> runing s"
using assms
by (induct, auto)
lemma isP_E:
assumes "isP e"
obtains cs where "e = P (actor e) cs"
using assms by (cases e, auto)
lemma isV_E:
assumes "isV e"
obtains cs where "e = V (actor e) cs"
using assms by (cases e, auto)
lemma wq_distinct: "distinct (wq s cs)"
proof(induct rule:ind)
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
show ?case
proof(cases e)
case (Create th prio)
interpret vt_create: valid_trace_create s e th prio
using Create by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_create.wq_distinct_kept)
next
case (Exit th)
interpret vt_exit: valid_trace_exit s e th
using Exit by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_exit.wq_distinct_kept)
next
case (P th cs)
interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_p.wq_distinct_kept)
next
case (V th cs)
interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_v.wq_distinct_kept)
next
case (Set th prio)
interpret vt_set: valid_trace_set s e th prio
using Set by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_set.wq_distinct_kept)
qed
qed (unfold wq_def Let_def, simp)
end
context valid_trace_e
begin
text {*
The following lemma shows that only the @{text "P"}
operation can add new thread into waiting queues.
Such kind of lemmas are very obvious, but need to be checked formally.
This is a kind of confirmation that our modelling is correct.
*}
lemma wq_in_inv:
assumes s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof(cases e)
-- {* This is the only non-trivial case: *}
case (V th cs1)
have False
proof(cases "cs1 = cs")
case True
show ?thesis
proof(cases "(wq s cs1)")
case (Cons w_hd w_tl)
have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"
proof -
have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"
using Cons V by (auto simp:wq_def Let_def True split:if_splits)
moreover have "set ... \<subseteq> set (wq s cs)"
proof(rule someI2)
show "distinct w_tl \<and> set w_tl = set w_tl"
by (metis distinct.simps(2) local.Cons wq_distinct)
qed (insert Cons True, auto)
ultimately show ?thesis by simp
qed
with assms show ?thesis by auto
qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)
qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
thus ?thesis by auto
qed (insert assms, auto simp:wq_def Let_def split:if_splits)
lemma wq_out_inv:
assumes s_in: "thread \<in> set (wq s cs)"
and s_hd: "thread = hd (wq s cs)"
and s_i: "thread \<noteq> hd (wq (e#s) cs)"
shows "e = V thread cs"
proof(cases e)
-- {* There are only two non-trivial cases: *}
case (V th cs1)
show ?thesis
proof(cases "cs1 = cs")
case True
have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .
thus ?thesis
proof(cases)
case (thread_V)
moreover have "th = thread" using thread_V(2) s_hd
by (unfold s_holding_def wq_def, simp)
ultimately show ?thesis using V True by simp
qed
qed (insert assms V, auto simp:wq_def Let_def split:if_splits)
next
case (P th cs1)
show ?thesis
proof(cases "cs1 = cs")
case True
with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"
by (auto simp:wq_def Let_def split:if_splits)
with s_i s_hd s_in have False
by (metis empty_iff hd_append2 list.set(1) wq_def)
thus ?thesis by simp
qed (insert assms P, auto simp:wq_def Let_def split:if_splits)
qed (insert assms, auto simp:wq_def Let_def split:if_splits)
end
context valid_trace
begin
text {* (* ddd *)
The nature of the work is like this: since it starts from a very simple and basic
model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
For instance, the fact
that one thread can not be blocked by two critical resources at the same time
is obvious, because only running threads can make new requests, if one is waiting for
a critical resource and get blocked, it can not make another resource request and get
blocked the second time (because it is not running).
To derive this fact, one needs to prove by contraction and
reason about time (or @{text "moement"}). The reasoning is based on a generic theorem
named @{text "p_split"}, which is about status changing along the time axis. It says if
a condition @{text "Q"} is @{text "True"} at a state @{text "s"},
but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"}
in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history
of events leading to it), such that @{text "Q"} switched
from being @{text "False"} to @{text "True"} and kept being @{text "True"}
till the last moment of @{text "s"}.
Suppose a thread @{text "th"} is blocked
on @{text "cs1"} and @{text "cs2"} in some state @{text "s"},
since no thread is blocked at the very beginning, by applying
@{text "p_split"} to these two blocking facts, there exist
two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that
@{text "th"} got blocked on @{text "cs1"} and @{text "cs2"}
and kept on blocked on them respectively ever since.
Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}.
However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still
in blocked state at moment @{text "t2"} and could not
make any request and get blocked the second time: Contradiction.
*}
lemma waiting_unique_pre: (* ddd *)
assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
and h22: "thread \<noteq> hd (wq s cs2)"
and neq12: "cs1 \<noteq> cs2"
shows "False"
proof -
let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"
from h11 and h12 have q1: "?Q cs1 s" by simp
from h21 and h22 have q2: "?Q cs2 s" by simp
have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)
have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)
from p_split [of "?Q cs1", OF q1 nq1]
obtain t1 where lt1: "t1 < length s"
and np1: "\<not> ?Q cs1 (moment t1 s)"
and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto
from p_split [of "?Q cs2", OF q2 nq2]
obtain t2 where lt2: "t2 < length s"
and np2: "\<not> ?Q cs2 (moment t2 s)"
and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto
{ fix s cs
assume q: "?Q cs s"
have "thread \<notin> runing s"
proof
assume "thread \<in> runing s"
hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and>
thread \<noteq> hd (wq_fun (schs s) cs))"
by (unfold runing_def s_waiting_def readys_def, auto)
from this[rule_format, of cs] q
show False by (simp add: wq_def)
qed
} note q_not_runing = this
{ fix t1 t2 cs1 cs2
assume lt1: "t1 < length s"
and np1: "\<not> ?Q cs1 (moment t1 s)"
and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
and lt2: "t2 < length s"
and np2: "\<not> ?Q cs2 (moment t2 s)"
and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
and lt12: "t1 < t2"
let ?t3 = "Suc t2"
from lt2 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
have "t2 < ?t3" by simp
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
have "vt (e#moment t2 s)"
proof -
from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
then interpret vt_e: valid_trace_e "moment t2 s" "e"
by (unfold_locales, auto, cases, simp)
have ?thesis
proof -
have "thread \<in> runing (moment t2 s)"
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
have "e = V thread cs2"
proof -
have eq_th: "thread = hd (wq (moment t2 s) cs2)"
using True and np2 by auto
from vt_e.wq_out_inv[OF True this h2]
show ?thesis .
qed
thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto
next
case False
have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
with vt_e.actor_inv[OF vt_e.pip_e]
show ?thesis by auto
qed
moreover have "thread \<notin> runing (moment t2 s)"
by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
ultimately show ?thesis by simp
qed
} note lt_case = this
show ?thesis
proof -
{ assume "t1 < t2"
from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
have ?thesis .
} moreover {
assume "t2 < t1"
from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
have ?thesis .
} moreover {
assume eq_12: "t1 = t2"
let ?t3 = "Suc t2"
from lt2 have le_t3: "?t3 \<le> length s" by auto
from moment_plus [OF this]
obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
have lt_2: "t2 < ?t3" by simp
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]
have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have "vt (e#moment t2 s)"
proof -
from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
then interpret vt_e: valid_trace_e "moment t2 s" "e"
by (unfold_locales, auto, cases, simp)
have "e = V thread cs2 \<or> e = P thread cs2"
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
have "e = V thread cs2"
proof -
have eq_th: "thread = hd (wq (moment t2 s) cs2)"
using True and np2 by auto
from vt_e.wq_out_inv[OF True this h2]
show ?thesis .
qed
thus ?thesis by auto
next
case False
have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
thus ?thesis by auto
qed
moreover have "e = V thread cs1 \<or> e = P thread cs1"
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
have eq_th: "thread = hd (wq (moment t1 s) cs1)"
using True and np1 by auto
from vt_e.wq_out_inv[folded eq_12, OF True this g2]
have "e = V thread cs1" .
thus ?thesis by auto
next
case False
have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .
thus ?thesis by auto
qed
ultimately have ?thesis using neq12 by auto
} ultimately show ?thesis using nat_neq_iff by blast
qed
qed
text {*
This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
*}
lemma waiting_unique:
assumes "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
using waiting_unique_pre assms
unfolding wq_def s_waiting_def
by auto
end
(* not used *)
text {*
Every thread can only be blocked on one critical resource,
symmetrically, every critical resource can only be held by one thread.
This fact is much more easier according to our definition.
*}
lemma held_unique:
assumes "holding (s::event list) th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
by (insert assms, unfold s_holding_def, auto)
lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
apply (induct s, auto)
by (case_tac a, auto split:if_splits)
lemma last_set_unique:
"\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
\<Longrightarrow> th1 = th2"
apply (induct s, auto)
by (case_tac a, auto split:if_splits dest:last_set_lt)
lemma preced_unique :
assumes pcd_eq: "preced th1 s = preced th2 s"
and th_in1: "th1 \<in> threads s"
and th_in2: " th2 \<in> threads s"
shows "th1 = th2"
proof -
from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
from last_set_unique [OF this th_in1 th_in2]
show ?thesis .
qed
lemma preced_linorder:
assumes neq_12: "th1 \<noteq> th2"
and th_in1: "th1 \<in> threads s"
and th_in2: " th2 \<in> threads s"
shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"
proof -
from preced_unique [OF _ th_in1 th_in2] and neq_12
have "preced th1 s \<noteq> preced th2 s" by auto
thus ?thesis by auto
qed
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 (in valid_trace_set)
RAG_unchanged: "(RAG (e # s)) = RAG s"
by (unfold is_set RAG_set_unchanged, simp)
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 (in valid_trace_create)
RAG_unchanged: "(RAG (e # s)) = RAG s"
by (unfold is_create RAG_create_unchanged, simp)
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)
lemma (in valid_trace_exit)
RAG_unchanged: "(RAG (e # s)) = RAG s"
by (unfold is_exit RAG_exit_unchanged, simp)
context valid_trace_v
begin
lemma distinct_rest: "distinct rest"
by (simp add: distinct_tl rest_def wq_distinct)
lemma holding_cs_eq_th:
assumes "holding s t cs"
shows "t = th"
proof -
from pip_e[unfolded is_v]
show ?thesis
proof(cases)
case (thread_V)
from held_unique[OF this(2) assms]
show ?thesis by simp
qed
qed
lemma distinct_wq': "distinct wq'"
by (metis (mono_tags, lifting) distinct_rest some_eq_ex wq'_def)
lemma set_wq': "set wq' = set rest"
by (metis (mono_tags, lifting) distinct_rest rest_def
some_eq_ex wq'_def)
lemma th'_in_inv:
assumes "th' \<in> set wq'"
shows "th' \<in> set rest"
using assms set_wq' by simp
lemma neq_t_th:
assumes "waiting (e#s) t c"
shows "t \<noteq> th"
proof
assume otherwise: "t = th"
show False
proof(cases "c = cs")
case True
have "t \<in> set wq'"
using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs]
by simp
from th'_in_inv[OF this] have "t \<in> set rest" .
with wq_s_cs[folded otherwise] wq_distinct[of cs]
show ?thesis by simp
next
case False
have "wq (e#s) c = wq s c" using False
by (unfold is_v, simp)
hence "waiting s t c" using assms
by (simp add: cs_waiting_def waiting_eq)
hence "t \<notin> readys s" by (unfold readys_def, auto)
hence "t \<notin> runing s" using runing_ready by auto
with runing_th_s[folded otherwise] show ?thesis by auto
qed
qed
lemma waiting_esI1:
assumes "waiting s t c"
and "c \<noteq> cs"
shows "waiting (e#s) t c"
proof -
have "wq (e#s) c = wq s c"
using assms(2) is_v by auto
with assms(1) show ?thesis
using cs_waiting_def waiting_eq by auto
qed
lemma holding_esI2:
assumes "c \<noteq> cs"
and "holding s t c"
shows "holding (e#s) t c"
proof -
from assms(1) have "wq (e#s) c = wq s c" using is_v by auto
from assms(2)[unfolded s_holding_def, folded wq_def,
folded this, unfolded wq_def, folded s_holding_def]
show ?thesis .
qed
lemma holding_esI1:
assumes "holding s t c"
and "t \<noteq> th"
shows "holding (e#s) t c"
proof -
have "c \<noteq> cs" using assms using holding_cs_eq_th by blast
from holding_esI2[OF this assms(1)]
show ?thesis .
qed
end
context valid_trace_v_n
begin
lemma neq_wq': "wq' \<noteq> []"
proof (unfold wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
by (simp add: distinct_rest)
next
fix x
assume " distinct x \<and> set x = set rest"
thus "x \<noteq> []" using rest_nnl by auto
qed
definition "taker = hd wq'"
definition "rest' = tl wq'"
lemma eq_wq': "wq' = taker # rest'"
by (simp add: neq_wq' rest'_def taker_def)
lemma next_th_taker:
shows "next_th s th cs taker"
using rest_nnl taker_def wq'_def wq_s_cs
by (auto simp:next_th_def)
lemma taker_unique:
assumes "next_th s th cs taker'"
shows "taker' = taker"
proof -
from assms
obtain rest' where
h: "wq s cs = th # rest'"
"taker' = hd (SOME q. distinct q \<and> set q = set rest')"
by (unfold next_th_def, auto)
with wq_s_cs have "rest' = rest" by auto
thus ?thesis using h(2) taker_def wq'_def by auto
qed
lemma waiting_set_eq:
"{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}"
by (smt all_not_in_conv bot.extremum insertI1 insert_subset
mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)
lemma holding_set_eq:
"{(Cs cs, Th th') |th'. next_th s th cs th'} = {(Cs cs, Th taker)}"
using next_th_taker taker_def waiting_set_eq
by fastforce
lemma holding_taker:
shows "holding (e#s) taker cs"
by (unfold s_holding_def, fold wq_def, unfold wq_es_cs,
auto simp:neq_wq' taker_def)
lemma waiting_esI2:
assumes "waiting s t cs"
and "t \<noteq> taker"
shows "waiting (e#s) t cs"
proof -
have "t \<in> set wq'"
proof(unfold wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
by (simp add: distinct_rest)
next
fix x
assume "distinct x \<and> set x = set rest"
moreover have "t \<in> set rest"
using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto
ultimately show "t \<in> set x" by simp
qed
moreover have "t \<noteq> hd wq'"
using assms(2) taker_def by auto
ultimately show ?thesis
by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)
qed
lemma waiting_esE:
assumes "waiting (e#s) t c"
obtains "c \<noteq> cs" "waiting s t c"
| "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" using is_v by auto
with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]
have "t \<noteq> hd wq'" "t \<in> set wq'" by auto
hence "t \<noteq> taker" by (simp add: taker_def)
moreover hence "t \<noteq> th" using assms neq_t_th by blast
moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv)
ultimately have "waiting s t cs"
by (metis cs_waiting_def list.distinct(2) list.sel(1)
list.set_sel(2) rest_def waiting_eq wq_s_cs)
show ?thesis using that(2)
using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto
qed
lemma holding_esI1:
assumes "c = cs"
and "t = taker"
shows "holding (e#s) t c"
by (unfold assms, simp add: holding_taker)
lemma holding_esE:
assumes "holding (e#s) t c"
obtains "c = cs" "t = taker"
| "c \<noteq> cs" "holding s t c"
proof(cases "c = cs")
case True
from assms[unfolded True, unfolded s_holding_def,
folded wq_def, unfolded wq_es_cs]
have "t = taker" by (simp add: taker_def)
from that(1)[OF True this] show ?thesis .
next
case False
hence "wq (e#s) c = wq s c" using is_v by auto
from assms[unfolded s_holding_def, folded wq_def,
unfolded this, unfolded wq_def, folded s_holding_def]
have "holding s t c" .
from that(2)[OF False this] show ?thesis .
qed
end
context valid_trace_v_e
begin
lemma nil_wq': "wq' = []"
proof (unfold wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
by (simp add: distinct_rest)
next
fix x
assume " distinct x \<and> set x = set rest"
thus "x = []" using rest_nil by auto
qed
lemma no_taker:
assumes "next_th s th cs taker"
shows "False"
proof -
from assms[unfolded next_th_def]
obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []"
by auto
thus ?thesis using rest_def rest_nil by auto
qed
lemma waiting_set_eq:
"{(Th th', Cs cs) |th'. next_th s th cs th'} = {}"
using no_taker by auto
lemma holding_set_eq:
"{(Cs cs, Th th') |th'. next_th s th cs th'} = {}"
using no_taker by auto
lemma no_holding:
assumes "holding (e#s) taker cs"
shows False
proof -
from wq_es_cs[unfolded nil_wq']
have " wq (e # s) cs = []" .
from assms[unfolded s_holding_def, folded wq_def, unfolded this]
show ?thesis by auto
qed
lemma no_waiting:
assumes "waiting (e#s) t cs"
shows False
proof -
from wq_es_cs[unfolded nil_wq']
have " wq (e # s) cs = []" .
from assms[unfolded s_waiting_def, folded wq_def, unfolded this]
show ?thesis by auto
qed
lemma waiting_esI2:
assumes "waiting s t c"
shows "waiting (e#s) t c"
proof -
have "c \<noteq> cs" using assms
using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto
from waiting_esI1[OF assms this]
show ?thesis .
qed
lemma waiting_esE:
assumes "waiting (e#s) t c"
obtains "c \<noteq> cs" "waiting s t c"
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" using is_v by auto
with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
from no_waiting[OF assms[unfolded True]]
show ?thesis by auto
qed
lemma holding_esE:
assumes "holding (e#s) t c"
obtains "c \<noteq> cs" "holding s t c"
proof(cases "c = cs")
case True
from no_holding[OF assms[unfolded True]]
show ?thesis by auto
next
case False
hence "wq (e#s) c = wq s c" using is_v by auto
from assms[unfolded s_holding_def, folded wq_def,
unfolded this, unfolded wq_def, folded s_holding_def]
have "holding s t c" .
from that[OF False this] show ?thesis .
qed
end
lemma rel_eqI:
assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
shows "A = B"
using assms by auto
lemma in_RAG_E:
assumes "(n1, n2) \<in> RAG (s::state)"
obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
| (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
by auto
context valid_trace_v
begin
lemma RAG_es:
"RAG (e # s) =
RAG s - {(Cs cs, Th th)} -
{(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
{(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
proof(rule rel_eqI)
fix n1 n2
assume "(n1, n2) \<in> ?L"
thus "(n1, n2) \<in> ?R"
proof(cases rule:in_RAG_E)
case (waiting th' cs')
show ?thesis
proof(cases "rest = []")
case False
interpret h_n: valid_trace_v_n s e th cs
by (unfold_locales, insert False, simp)
from waiting(3)
show ?thesis
proof(cases rule:h_n.waiting_esE)
case 1
with waiting(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
fold waiting_eq, auto)
next
case 2
with waiting(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
fold waiting_eq, auto)
qed
next
case True
interpret h_e: valid_trace_v_e s e th cs
by (unfold_locales, insert True, simp)
from waiting(3)
show ?thesis
proof(cases rule:h_e.waiting_esE)
case 1
with waiting(1,2)
show ?thesis
by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
fold waiting_eq, auto)
qed
qed
next
case (holding th' cs')
show ?thesis
proof(cases "rest = []")
case False
interpret h_n: valid_trace_v_n s e th cs
by (unfold_locales, insert False, simp)
from holding(3)
show ?thesis
proof(cases rule:h_n.holding_esE)
case 1
with holding(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
fold waiting_eq, auto)
next
case 2
with holding(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
fold holding_eq, auto)
qed
next
case True
interpret h_e: valid_trace_v_e s e th cs
by (unfold_locales, insert True, simp)
from holding(3)
show ?thesis
proof(cases rule:h_e.holding_esE)
case 1
with holding(1,2)
show ?thesis
by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
fold holding_eq, auto)
qed
qed
qed
next
fix n1 n2
assume h: "(n1, n2) \<in> ?R"
show "(n1, n2) \<in> ?L"
proof(cases "rest = []")
case False
interpret h_n: valid_trace_v_n s e th cs
by (unfold_locales, insert False, simp)
from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq]
have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th)
\<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or>
(n2 = Th h_n.taker \<and> n1 = Cs cs)"
by auto
thus ?thesis
proof
assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
with h_n.holding_taker
show ?thesis
by (unfold s_RAG_def, fold holding_eq, auto)
next
assume h: "(n1, n2) \<in> RAG s \<and>
(n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
hence "(n1, n2) \<in> RAG s" by simp
thus ?thesis
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from h and this(1,2)
have "th' \<noteq> h_n.taker \<or> cs' \<noteq> cs" by auto
hence "waiting (e#s) th' cs'"
proof
assume "cs' \<noteq> cs"
from waiting_esI1[OF waiting(3) this]
show ?thesis .
next
assume neq_th': "th' \<noteq> h_n.taker"
show ?thesis
proof(cases "cs' = cs")
case False
from waiting_esI1[OF waiting(3) this]
show ?thesis .
next
case True
from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True]
show ?thesis .
qed
qed
thus ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
next
case (holding th' cs')
from h this(1,2)
have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
hence "holding (e#s) th' cs'"
proof
assume "cs' \<noteq> cs"
from holding_esI2[OF this holding(3)]
show ?thesis .
next
assume "th' \<noteq> th"
from holding_esI1[OF holding(3) this]
show ?thesis .
qed
thus ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
qed
qed
next
case True
interpret h_e: valid_trace_v_e s e th cs
by (unfold_locales, insert True, simp)
from h[unfolded h_e.waiting_set_eq h_e.holding_set_eq]
have h_s: "(n1, n2) \<in> RAG s" "(n1, n2) \<noteq> (Cs cs, Th th)"
by auto
from h_s(1)
show ?thesis
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from h_e.waiting_esI2[OF this(3)]
show ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
next
case (holding th' cs')
with h_s(2)
have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
thus ?thesis
proof
assume neq_cs: "cs' \<noteq> cs"
from holding_esI2[OF this holding(3)]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
next
assume "th' \<noteq> th"
from holding_esI1[OF holding(3) this]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
qed
qed
qed
qed
end
lemma step_RAG_v:
assumes vt:
"vt (V th cs#s)"
shows "
RAG (V th cs # s) =
RAG s - {(Cs cs, Th th)} -
{(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
{(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
proof -
interpret vt_v: valid_trace_v s "V th cs"
using assms step_back_vt by (unfold_locales, auto)
show ?thesis using vt_v.RAG_es .
qed
lemma (in valid_trace_create)
th_not_in_threads: "th \<notin> threads s"
proof -
from pip_e[unfolded is_create]
show ?thesis by (cases, simp)
qed
lemma (in valid_trace_create)
threads_es [simp]: "threads (e#s) = threads s \<union> {th}"
by (unfold is_create, simp)
lemma (in valid_trace_exit)
threads_es [simp]: "threads (e#s) = threads s - {th}"
by (unfold is_exit, simp)
lemma (in valid_trace_p)
threads_es [simp]: "threads (e#s) = threads s"
by (unfold is_p, simp)
lemma (in valid_trace_v)
threads_es [simp]: "threads (e#s) = threads s"
by (unfold is_v, simp)
lemma (in valid_trace_v)
th_not_in_rest[simp]: "th \<notin> set rest"
proof
assume otherwise: "th \<in> set rest"
have "distinct (wq s cs)" by (simp add: wq_distinct)
from this[unfolded wq_s_cs] and otherwise
show False by auto
qed
lemma (in valid_trace_v)
set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"
proof(unfold wq_es_cs wq'_def, rule someI2)
show "distinct rest \<and> set rest = set rest"
by (simp add: distinct_rest)
next
fix x
assume "distinct x \<and> set x = set rest"
thus "set x = set (wq s cs) - {th}"
by (unfold wq_s_cs, simp)
qed
lemma (in valid_trace_exit)
th_not_in_wq: "th \<notin> set (wq s cs)"
proof -
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold holdents_def s_holding_def, fold wq_def,
auto elim!:runing_wqE)
qed
lemma (in valid_trace) wq_threads:
assumes "th \<in> set (wq s cs)"
shows "th \<in> threads s"
using assms
proof(induct rule:ind)
case (Nil)
thus ?case by (auto simp:wq_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
show ?case
proof(cases e)
case (Create th' prio')
interpret vt: valid_trace_create s e th' prio'
using Create by (unfold_locales, simp)
show ?thesis
using Cons.hyps(2) Cons.prems by auto
next
case (Exit th')
interpret vt: valid_trace_exit s e th'
using Exit by (unfold_locales, simp)
show ?thesis
using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto
next
case (P th' cs')
interpret vt: valid_trace_p s e th' cs'
using P by (unfold_locales, simp)
show ?thesis
using Cons.hyps(2) Cons.prems readys_threads
runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv
by fastforce
next
case (V th' cs')
interpret vt: valid_trace_v s e th' cs'
using V by (unfold_locales, simp)
show ?thesis using Cons
using vt.is_v vt.threads_es vt_e.wq_in_inv by blast
next
case (Set th' prio)
interpret vt: valid_trace_set s e th' prio
using Set by (unfold_locales, simp)
show ?thesis using Cons.hyps(2) Cons.prems vt.is_set
by (auto simp:wq_def Let_def)
qed
qed
context valid_trace
begin
lemma dm_RAG_threads:
assumes in_dom: "(Th th) \<in> Domain (RAG s)"
shows "th \<in> threads s"
proof -
from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
hence "th \<in> set (wq s cs)"
by (unfold s_RAG_def, auto simp:cs_waiting_def)
from wq_threads [OF this] show ?thesis .
qed
lemma rg_RAG_threads:
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
using assms
by (unfold s_RAG_def cs_waiting_def cs_holding_def,
auto intro:wq_threads)
end
lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s"
by (unfold preced_def, simp)
lemma (in valid_trace_v)
preced_es: "preced th (e#s) = preced th s"
by (unfold is_v preced_def, simp)
lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
proof
fix th'
show "the_preced (V th cs # s) th' = the_preced s th'"
by (unfold the_preced_def preced_def, simp)
qed
lemma (in valid_trace_v)
the_preced_es: "the_preced (e#s) = the_preced s"
by (unfold is_v preced_def, simp)
context valid_trace_p
begin
lemma not_holding_s_th_cs: "\<not> holding s th cs"
proof
assume otherwise: "holding s th cs"
from pip_e[unfolded is_p]
show False
proof(cases)
case (thread_P)
moreover have "(Cs cs, Th th) \<in> RAG s"
using otherwise cs_holding_def
holding_eq th_not_in_wq by auto
ultimately show ?thesis by auto
qed
qed
lemma waiting_kept:
assumes "waiting s th' cs'"
shows "waiting (e#s) th' cs'"
using assms
by (metis cs_waiting_def hd_append2 list.sel(1) list.set_intros(2)
rotate1.simps(2) self_append_conv2 set_rotate1
th_not_in_wq waiting_eq wq_es_cs wq_neq_simp)
lemma holding_kept:
assumes "holding s th' cs'"
shows "holding (e#s) th' cs'"
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
with assms show ?thesis using cs_holding_def holding_eq by auto
next
case True
from assms[unfolded s_holding_def, folded wq_def]
obtain rest where eq_wq: "wq s cs' = th'#rest"
by (metis empty_iff list.collapse list.set(1))
hence "wq (e#s) cs' = th'#(rest@[th])"
by (simp add: True wq_es_cs)
thus ?thesis
by (simp add: cs_holding_def holding_eq)
qed
end
locale valid_trace_p_h = valid_trace_p +
assumes we: "wq s cs = []"
locale valid_trace_p_w = valid_trace_p +
assumes wne: "wq s cs \<noteq> []"
begin
definition "holder = hd (wq s cs)"
definition "waiters = tl (wq s cs)"
definition "waiters' = waiters @ [th]"
lemma wq_s_cs: "wq s cs = holder#waiters"
by (simp add: holder_def waiters_def wne)
lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
by (simp add: wq_es_cs wq_s_cs)
lemma waiting_es_th_cs: "waiting (e#s) th cs"
using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
lemma holding_esE:
assumes "holding (e#s) th' cs'"
obtains "holding s th' cs'"
using assms
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
with assms show ?thesis
using cs_holding_def holding_eq that by auto
next
case True
with assms show ?thesis
by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that
wq_es_cs' wq_s_cs)
qed
lemma waiting_esE:
assumes "waiting (e#s) th' cs'"
obtains "th' \<noteq> th" "waiting s th' cs'"
| "th' = th" "cs' = cs"
proof(cases "waiting s th' cs'")
case True
have "th' \<noteq> th"
proof
assume otherwise: "th' = th"
from True[unfolded this]
show False by (simp add: th_not_waiting)
qed
from that(1)[OF this True] show ?thesis .
next
case False
hence "th' = th \<and> cs' = cs"
by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2)
set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
with that(2) show ?thesis by metis
qed
lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")
proof(rule rel_eqI)
fix n1 n2
assume "(n1, n2) \<in> ?L"
thus "(n1, n2) \<in> ?R"
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from this(3)
show ?thesis
proof(cases rule:waiting_esE)
case 1
thus ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
next
case 2
thus ?thesis using waiting(1,2) by auto
qed
next
case (holding th' cs')
from this(3)
show ?thesis
proof(cases rule:holding_esE)
case 1
with holding(1,2)
show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
qed
qed
next
fix n1 n2
assume "(n1, n2) \<in> ?R"
hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto
thus "(n1, n2) \<in> ?L"
proof
assume "(n1, n2) \<in> RAG s"
thus ?thesis
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from waiting_kept[OF this(3)]
show ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
qed
next
assume "n1 = Th th \<and> n2 = Cs cs"
thus ?thesis using RAG_edge by auto
qed
qed
end
context valid_trace_p_h
begin
lemma wq_es_cs': "wq (e#s) cs = [th]"
using wq_es_cs[unfolded we] by simp
lemma holding_es_th_cs:
shows "holding (e#s) th cs"
proof -
from wq_es_cs'
have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
thus ?thesis using cs_holding_def holding_eq by blast
qed
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto)
lemma waiting_esE:
assumes "waiting (e#s) th' cs'"
obtains "waiting s th' cs'"
using assms
by (metis cs_waiting_def event.distinct(15) is_p list.sel(1)
set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv)
lemma holding_esE:
assumes "holding (e#s) th' cs'"
obtains "cs' \<noteq> cs" "holding s th' cs'"
| "cs' = cs" "th' = th"
proof(cases "cs' = cs")
case True
from held_unique[OF holding_es_th_cs assms[unfolded True]]
have "th' = th" by simp
from that(2)[OF True this] show ?thesis .
next
case False
have "holding s th' cs'" using assms
using False cs_holding_def holding_eq by auto
from that(1)[OF False this] show ?thesis .
qed
lemma RAG_es: "RAG (e # s) = RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R")
proof(rule rel_eqI)
fix n1 n2
assume "(n1, n2) \<in> ?L"
thus "(n1, n2) \<in> ?R"
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from this(3)
show ?thesis
proof(cases rule:waiting_esE)
case 1
thus ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
qed
next
case (holding th' cs')
from this(3)
show ?thesis
proof(cases rule:holding_esE)
case 1
with holding(1,2)
show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
next
case 2
with holding(1,2) show ?thesis by auto
qed
qed
next
fix n1 n2
assume "(n1, n2) \<in> ?R"
hence "(n1, n2) \<in> RAG s \<or> (n1 = Cs cs \<and> n2 = Th th)" by auto
thus "(n1, n2) \<in> ?L"
proof
assume "(n1, n2) \<in> RAG s"
thus ?thesis
proof(cases rule:in_RAG_E)
case (waiting th' cs')
from waiting_kept[OF this(3)]
show ?thesis using waiting(1,2)
by (unfold s_RAG_def, fold waiting_eq, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
by (unfold s_RAG_def, fold holding_eq, auto)
qed
next
assume "n1 = Cs cs \<and> n2 = Th th"
with holding_es_th_cs
show ?thesis
by (unfold s_RAG_def, fold holding_eq, auto)
qed
qed
end
context valid_trace_p
begin
lemma RAG_es': "RAG (e # s) = (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
else RAG s \<union> {(Th th, Cs cs)})"
proof(cases "wq s cs = []")
case True
interpret vt_p: valid_trace_p_h using True
by (unfold_locales, simp)
show ?thesis by (simp add: vt_p.RAG_es vt_p.we)
next
case False
interpret vt_p: valid_trace_p_w using False
by (unfold_locales, simp)
show ?thesis by (simp add: vt_p.RAG_es vt_p.wne)
qed
end
lemma (in valid_trace_v_n) finite_waiting_set:
"finite {(Th th', Cs cs) |th'. next_th s th cs th'}"
by (simp add: waiting_set_eq)
lemma (in valid_trace_v_n) finite_holding_set:
"finite {(Cs cs, Th th') |th'. next_th s th cs th'}"
by (simp add: holding_set_eq)
lemma (in valid_trace_v_e) finite_waiting_set:
"finite {(Th th', Cs cs) |th'. next_th s th cs th'}"
by (simp add: waiting_set_eq)
lemma (in valid_trace_v_e) finite_holding_set:
"finite {(Cs cs, Th th') |th'. next_th s th cs th'}"
by (simp add: holding_set_eq)
context valid_trace_v
begin
lemma
finite_RAG_kept:
assumes "finite (RAG s)"
shows "finite (RAG (e#s))"
proof(cases "rest = []")
case True
interpret vt: valid_trace_v_e using True
by (unfold_locales, simp)
show ?thesis using assms
by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
next
case False
interpret vt: valid_trace_v_n using False
by (unfold_locales, simp)
show ?thesis using assms
by (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
qed
end
context valid_trace_v_e
begin
lemma
acylic_RAG_kept:
assumes "acyclic (RAG s)"
shows "acyclic (RAG (e#s))"
proof(rule acyclic_subset[OF assms])
show "RAG (e # s) \<subseteq> RAG s"
by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
qed
end
context valid_trace_v_n
begin
lemma waiting_taker: "waiting s taker cs"
apply (unfold s_waiting_def, fold wq_def, unfold wq_s_cs taker_def)
using eq_wq' th'_in_inv wq'_def by fastforce
lemma
acylic_RAG_kept:
assumes "acyclic (RAG s)"
shows "acyclic (RAG (e#s))"
proof -
have "acyclic ((RAG s - {(Cs cs, Th th)} - {(Th taker, Cs cs)}) \<union>
{(Cs cs, Th taker)})" (is "acyclic (?A \<union> _)")
proof -
from assms
have "acyclic ?A"
by (rule acyclic_subset, auto)
moreover have "(Th taker, Cs cs) \<notin> ?A^*"
proof
assume otherwise: "(Th taker, Cs cs) \<in> ?A^*"
hence "(Th taker, Cs cs) \<in> ?A^+"
by (unfold rtrancl_eq_or_trancl, auto)
from tranclD[OF this]
obtain cs' where h: "(Th taker, Cs cs') \<in> ?A"
"(Th taker, Cs cs') \<in> RAG s"
by (unfold s_RAG_def, auto)
from this(2) have "waiting s taker cs'"
by (unfold s_RAG_def, fold waiting_eq, auto)
from waiting_unique[OF this waiting_taker]
have "cs' = cs" .
from h(1)[unfolded this] show False by auto
qed
ultimately show ?thesis by auto
qed
thus ?thesis
by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
qed
end
context valid_trace_p_h
begin
lemma
acylic_RAG_kept:
assumes "acyclic (RAG s)"
shows "acyclic (RAG (e#s))"
proof -
have "acyclic (RAG s \<union> {(Cs cs, Th th)})" (is "acyclic (?A \<union> _)")
proof -
from assms
have "acyclic ?A"
by (rule acyclic_subset, auto)
moreover have "(Th th, Cs cs) \<notin> ?A^*"
proof
assume otherwise: "(Th th, Cs cs) \<in> ?A^*"
hence "(Th th, Cs cs) \<in> ?A^+"
by (unfold rtrancl_eq_or_trancl, auto)
from tranclD[OF this]
obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
by (unfold s_RAG_def, auto)
hence "waiting s th cs'"
by (unfold s_RAG_def, fold waiting_eq, auto)
with th_not_waiting show False by auto
qed
ultimately show ?thesis by auto
qed
thus ?thesis by (unfold RAG_es, simp)
qed
end
context valid_trace_p_w
begin
lemma
acylic_RAG_kept:
assumes "acyclic (RAG s)"
shows "acyclic (RAG (e#s))"
proof -
have "acyclic (RAG s \<union> {(Th th, Cs cs)})" (is "acyclic (?A \<union> _)")
proof -
from assms
have "acyclic ?A"
by (rule acyclic_subset, auto)
moreover have "(Cs cs, Th th) \<notin> ?A^*"
proof
assume otherwise: "(Cs cs, Th th) \<in> ?A^*"
from pip_e[unfolded is_p]
show False
proof(cases)
case (thread_P)
moreover from otherwise have "(Cs cs, Th th) \<in> ?A^+"
by (unfold rtrancl_eq_or_trancl, auto)
ultimately show ?thesis by auto
qed
qed
ultimately show ?thesis by auto
qed
thus ?thesis by (unfold RAG_es, simp)
qed
end
context valid_trace
begin
lemma finite_RAG:
shows "finite (RAG s)"
proof(induct rule:ind)
case Nil
show ?case
by (auto simp: s_RAG_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
show ?case
proof(cases e)
case (Create th prio)
interpret vt: valid_trace_create s e th prio using Create
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
next
case (Exit th)
interpret vt: valid_trace_exit s e th using Exit
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
next
case (P th cs)
interpret vt: valid_trace_p s e th cs using P
by (unfold_locales, simp)
show ?thesis using Cons using vt.RAG_es' by auto
next
case (V th cs)
interpret vt: valid_trace_v s e th cs using V
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.finite_RAG_kept)
next
case (Set th prio)
interpret vt: valid_trace_set s e th prio using Set
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
qed
qed
lemma acyclic_RAG:
shows "acyclic (RAG s)"
proof(induct rule:ind)
case Nil
show ?case
by (auto simp: s_RAG_def cs_waiting_def
cs_holding_def wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
show ?case
proof(cases e)
case (Create th prio)
interpret vt: valid_trace_create s e th prio using Create
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
next
case (Exit th)
interpret vt: valid_trace_exit s e th using Exit
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
next
case (P th cs)
interpret vt: valid_trace_p s e th cs using P
by (unfold_locales, simp)
show ?thesis
proof(cases "wq s cs = []")
case True
then interpret vt_h: valid_trace_p_h s e th cs
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_h.acylic_RAG_kept)
next
case False
then interpret vt_w: valid_trace_p_w s e th cs
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_w.acylic_RAG_kept)
qed
next
case (V th cs)
interpret vt: valid_trace_v s e th cs using V
by (unfold_locales, simp)
show ?thesis
proof(cases "vt.rest = []")
case True
then interpret vt_e: valid_trace_v_e s e th cs
by (unfold_locales, simp)
show ?thesis by (simp add: Cons.hyps(2) vt_e.acylic_RAG_kept)
next
case False
then interpret vt_n: valid_trace_v_n s e th cs
by (unfold_locales, simp)
show ?thesis by (simp add: Cons.hyps(2) vt_n.acylic_RAG_kept)
qed
next
case (Set th prio)
interpret vt: valid_trace_set s e th prio using Set
by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt.RAG_unchanged)
qed
qed
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG show "finite (RAG s)" .
next
from acyclic_RAG show "acyclic (RAG s)" .
qed
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
lemma sgv_hRAG: "single_valued (hRAG s)"
using held_unique
by (unfold single_valued_def hRAG_def, auto)
lemma sgv_tRAG: "single_valued (tRAG s)"
by (unfold tRAG_def, rule single_valued_relcomp,
insert sgv_wRAG sgv_hRAG, auto)
lemma acyclic_tRAG: "acyclic (tRAG s)"
proof(unfold tRAG_def, rule acyclic_compose)
show "acyclic (RAG s)" using acyclic_RAG .
next
show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
next
show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
qed
lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique held_unique)
lemma sgv_RAG: "single_valued (RAG s)"
using unique_RAG by (auto simp:single_valued_def)
lemma rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
end
sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"
proof -
show "fsubtree (RAG s)"
proof(intro_locales)
show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
next
show "fsubtree_axioms (RAG s)"
proof(unfold fsubtree_axioms_def)
from wf_RAG show "wf (RAG s)" .
qed
qed
qed
context valid_trace
begin
lemma finite_subtree_threads:
"finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A")
proof -
have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"
by (auto, insert image_iff, fastforce)
moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"
(is "finite ?B")
proof -
have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}"
by auto
moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto
moreover have "finite ..." by (simp add: finite_subtree)
ultimately show ?thesis by auto
qed
ultimately show ?thesis by auto
qed
lemma le_cp:
shows "preced th s \<le> cp s th"
proof(unfold cp_alt_def, rule Max_ge)
show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
by (simp add: finite_subtree_threads)
next
show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"
by (simp add: subtree_def the_preced_def)
qed
lemma cp_le:
assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max (the_preced s ` threads s)"
proof(unfold cp_alt_def, rule Max_f_mono)
show "finite (threads s)" by (simp add: finite_threads)
next
show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}"
using subtree_def by fastforce
next
show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s"
using assms
by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq
node.inject(1) rtranclD subsetI subtree_def trancl_domain)
qed
lemma max_cp_eq:
shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
(is "?L = ?R")
proof -
have "?L \<le> ?R"
proof(cases "threads s = {}")
case False
show ?thesis
by (rule Max.boundedI,
insert cp_le,
auto simp:finite_threads False)
qed auto
moreover have "?R \<le> ?L"
by (rule Max_fg_mono,
simp add: finite_threads,
simp add: le_cp the_preced_def)
ultimately show ?thesis by auto
qed
lemma max_cp_eq_the_preced:
shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
using max_cp_eq using the_preced_def by presburger
lemma wf_RAG_converse:
shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
from finite_RAG
show "finite (RAG s)" .
next
from acyclic_RAG
show "acyclic (RAG s)" .
qed
lemma chain_building:
assumes "node \<in> Domain (RAG s)"
obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"
proof -
from assms have "node \<in> Range ((RAG s)^-1)" by auto
from wf_base[OF wf_RAG_converse this]
obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto
obtain th' where eq_b: "b = Th th'"
proof(cases b)
case (Cs cs)
from h_b(1)[unfolded trancl_converse]
have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto
from tranclE[OF this]
obtain n where "(n, b) \<in> RAG s" by auto
from this[unfolded Cs]
obtain th1 where "waiting s th1 cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
from waiting_holding[OF this]
obtain th2 where "holding s th2 cs" .
hence "(Cs cs, Th th2) \<in> RAG s"
by (unfold s_RAG_def, fold holding_eq, auto)
with h_b(2)[unfolded Cs, rule_format]
have False by auto
thus ?thesis by auto
qed auto
have "th' \<in> readys s"
proof -
from h_b(2)[unfolded eq_b]
have "\<forall>cs. \<not> waiting s th' cs"
by (unfold s_RAG_def, fold waiting_eq, auto)
moreover have "th' \<in> threads s"
proof(rule rg_RAG_threads)
from tranclD[OF h_b(1), unfolded eq_b]
obtain z where "(z, Th th') \<in> (RAG s)" by auto
thus "Th th' \<in> Range (RAG s)" by auto
qed
ultimately show ?thesis by (auto simp:readys_def)
qed
moreover have "(node, Th th') \<in> (RAG s)^+"
using h_b(1)[unfolded trancl_converse] eq_b by auto
ultimately show ?thesis using that by metis
qed
text {* \noindent
The following is just an instance of @{text "chain_building"}.
*}
lemma th_chain_to_ready:
assumes th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
proof(cases "th \<in> readys s")
case True
thus ?thesis by auto
next
case False
from False and th_in have "Th th \<in> Domain (RAG s)"
by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
from chain_building [rule_format, OF this]
show ?thesis by auto
qed
end
lemma count_rec1 [simp]:
assumes "Q e"
shows "count Q (e#es) = Suc (count Q es)"
using assms
by (unfold count_def, auto)
lemma count_rec2 [simp]:
assumes "\<not>Q e"
shows "count Q (e#es) = (count Q es)"
using assms
by (unfold count_def, auto)
lemma count_rec3 [simp]:
shows "count Q [] = 0"
by (unfold count_def, auto)
lemma cntP_simp1[simp]:
"cntP (P th cs'#s) th = cntP s th + 1"
by (unfold cntP_def, simp)
lemma cntP_simp2[simp]:
assumes "th' \<noteq> th"
shows "cntP (P th cs'#s) th' = cntP s th'"
using assms
by (unfold cntP_def, simp)
lemma cntP_simp3[simp]:
assumes "\<not> isP e"
shows "cntP (e#s) th' = cntP s th'"
using assms
by (unfold cntP_def, cases e, simp+)
lemma cntV_simp1[simp]:
"cntV (V th cs'#s) th = cntV s th + 1"
by (unfold cntV_def, simp)
lemma cntV_simp2[simp]:
assumes "th' \<noteq> th"
shows "cntV (V th cs'#s) th' = cntV s th'"
using assms
by (unfold cntV_def, simp)
lemma cntV_simp3[simp]:
assumes "\<not> isV e"
shows "cntV (e#s) th' = cntV s th'"
using assms
by (unfold cntV_def, cases e, simp+)
lemma cntP_diff_inv:
assumes "cntP (e#s) th \<noteq> cntP s th"
shows "isP e \<and> actor e = th"
proof(cases e)
case (P th' pty)
show ?thesis
by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)",
insert assms P, auto simp:cntP_def)
qed (insert assms, auto simp:cntP_def)
lemma cntV_diff_inv:
assumes "cntV (e#s) th \<noteq> cntV s th"
shows "isV e \<and> actor e = th"
proof(cases e)
case (V th' pty)
show ?thesis
by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)",
insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)
lemma children_RAG_alt_def:
"children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
by (unfold s_RAG_def, auto simp:children_def holding_eq)
fun the_cs :: "node \<Rightarrow> cs" where
"the_cs (Cs cs) = cs"
lemma holdents_alt_def:
"holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
by (unfold children_RAG_alt_def holdents_def, simp add: image_image)
lemma cntCS_alt_def:
"cntCS s th = card (children (RAG s) (Th th))"
apply (unfold children_RAG_alt_def cntCS_def holdents_def)
by (rule card_image[symmetric], auto simp:inj_on_def)
context valid_trace
begin
lemma finite_holdents: "finite (holdents s th)"
by (unfold holdents_alt_def, insert finite_children, auto)
end
context valid_trace_p_w
begin
lemma holding_s_holder: "holding s holder cs"
by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
lemma holding_es_holder: "holding (e#s) holder cs"
by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)
lemma holdents_es:
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def)
have "holding s th' cs'"
proof(cases "cs' = cs")
case True
from held_unique[OF h[unfolded True] holding_es_holder]
have "th' = holder" .
thus ?thesis
by (unfold True holdents_def, insert holding_s_holder, simp)
next
case False
hence "wq (e#s) cs' = wq s cs'" by simp
from h[unfolded s_holding_def, folded wq_def, unfolded this]
show ?thesis
by (unfold s_holding_def, fold wq_def, auto)
qed
hence "cs' \<in> ?R" by (auto simp:holdents_def)
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence h: "holding s th' cs'" by (auto simp:holdents_def)
have "holding (e#s) th' cs'"
proof(cases "cs' = cs")
case True
from held_unique[OF h[unfolded True] holding_s_holder]
have "th' = holder" .
thus ?thesis
by (unfold True holdents_def, insert holding_es_holder, simp)
next
case False
hence "wq s cs' = wq (e#s) cs'" by simp
from h[unfolded s_holding_def, folded wq_def, unfolded this]
show ?thesis
by (unfold s_holding_def, fold wq_def, auto)
qed
hence "cs' \<in> ?L" by (auto simp:holdents_def)
} ultimately show ?thesis by auto
qed
lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'"
by (unfold cntCS_def holdents_es, simp)
lemma th_not_ready_es:
shows "th \<notin> readys (e#s)"
using waiting_es_th_cs
by (unfold readys_def, auto)
end
context valid_trace_p_h
begin
lemma th_not_waiting':
"\<not> waiting (e#s) th cs'"
proof(cases "cs' = cs")
case True
show ?thesis
by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto)
next
case False
from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def]
show ?thesis
by (unfold s_waiting_def, fold wq_def, insert False, simp)
qed
lemma ready_th_es:
shows "th \<in> readys (e#s)"
using th_not_waiting'
by (unfold readys_def, insert live_th_es, auto)
lemma holdents_es_th:
"holdents (e#s) th = (holdents s th) \<union> {cs}" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence "holding (e#s) th cs'"
by (unfold holdents_def, auto)
hence "cs' \<in> ?R"
by (cases rule:holding_esE, auto simp:holdents_def)
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence "holding s th cs' \<or> cs' = cs"
by (auto simp:holdents_def)
hence "cs' \<in> ?L"
proof
assume "holding s th cs'"
from holding_kept[OF this]
show ?thesis by (auto simp:holdents_def)
next
assume "cs' = cs"
thus ?thesis using holding_es_th_cs
by (unfold holdents_def, auto)
qed
} ultimately show ?thesis by auto
qed
lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1"
proof -
have "card (holdents s th \<union> {cs}) = card (holdents s th) + 1"
proof(subst card_Un_disjoint)
show "holdents s th \<inter> {cs} = {}"
using not_holding_s_th_cs by (auto simp:holdents_def)
qed (auto simp:finite_holdents)
thus ?thesis
by (unfold cntCS_def holdents_es_th, simp)
qed
lemma no_holder:
"\<not> holding s th' cs"
proof
assume otherwise: "holding s th' cs"
from this[unfolded s_holding_def, folded wq_def, unfolded we]
show False by auto
qed
lemma holdents_es_th':
assumes "th' \<noteq> th"
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence h_e: "holding (e#s) th' cs'" by (auto simp:holdents_def)
have "cs' \<noteq> cs"
proof
assume "cs' = cs"
from held_unique[OF h_e[unfolded this] holding_es_th_cs]
have "th' = th" .
with assms show False by simp
qed
from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]
have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def, auto)
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence "holding s th' cs'" by (auto simp:holdents_def)
from holding_kept[OF this]
have "holding (e # s) th' cs'" .
hence "cs' \<in> ?L"
by (unfold holdents_def, auto)
} ultimately show ?thesis by auto
qed
lemma cntCS_es_th'[simp]:
assumes "th' \<noteq> th"
shows "cntCS (e#s) th' = cntCS s th'"
by (unfold cntCS_def holdents_es_th'[OF assms], simp)
end
context valid_trace_p
begin
lemma readys_kept1:
assumes "th' \<noteq> th"
and "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms(2)[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
show ?thesis
proof(cases "wq s cs = []")
case True
then interpret vt: valid_trace_p_h
by (unfold_locales, simp)
show ?thesis using n_wait wait waiting_kept by auto
next
case False
then interpret vt: valid_trace_p_w by (unfold_locales, simp)
show ?thesis using n_wait wait waiting_kept by blast
qed
qed
} with assms(2) show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<noteq> th"
and "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2)[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
show ?thesis
proof(cases "wq s cs = []")
case True
then interpret vt: valid_trace_p_h
by (unfold_locales, simp)
show ?thesis using n_wait vt.waiting_esE wait by blast
next
case False
then interpret vt: valid_trace_p_w by (unfold_locales, simp)
show ?thesis using assms(1) n_wait vt.waiting_esE wait by auto
qed
qed
} with assms(2) show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
assumes "th' \<noteq> th"
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1[OF assms] readys_kept2[OF assms]
by metis
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof(cases "th' = th")
case True
note eq_th' = this
show ?thesis
proof(cases "wq s cs = []")
case True
then interpret vt: valid_trace_p_h by (unfold_locales, simp)
show ?thesis
using assms eq_th' is_p ready_th_s vt.cntCS_es_th vt.ready_th_es pvD_def by auto
next
case False
then interpret vt: valid_trace_p_w by (unfold_locales, simp)
show ?thesis
using add.commute add.left_commute assms eq_th' is_p live_th_s
ready_th_s vt.th_not_ready_es pvD_def
apply (auto)
by (fold is_p, simp)
qed
next
case False
note h_False = False
thus ?thesis
proof(cases "wq s cs = []")
case True
then interpret vt: valid_trace_p_h by (unfold_locales, simp)
show ?thesis using assms
by (insert True h_False pvD_def, auto split:if_splits,unfold is_p, auto)
next
case False
then interpret vt: valid_trace_p_w by (unfold_locales, simp)
show ?thesis using assms
by (insert False h_False pvD_def, auto split:if_splits,unfold is_p, auto)
qed
qed
end
context valid_trace_v (* ccc *)
begin
lemma holding_th_cs_s:
"holding s th cs"
by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
lemma th_ready_s [simp]: "th \<in> readys s"
using runing_th_s
by (unfold runing_def readys_def, auto)
lemma th_live_s [simp]: "th \<in> threads s"
using th_ready_s by (unfold readys_def, auto)
lemma th_ready_es [simp]: "th \<in> readys (e#s)"
using runing_th_s neq_t_th
by (unfold is_v runing_def readys_def, auto)
lemma th_live_es [simp]: "th \<in> threads (e#s)"
using th_ready_es by (unfold readys_def, auto)
lemma pvD_th_s[simp]: "pvD s th = 0"
by (unfold pvD_def, simp)
lemma pvD_th_es[simp]: "pvD (e#s) th = 0"
by (unfold pvD_def, simp)
lemma cntCS_s_th [simp]: "cntCS s th > 0"
proof -
have "cs \<in> holdents s th" using holding_th_cs_s
by (unfold holdents_def, simp)
moreover have "finite (holdents s th)" using finite_holdents
by simp
ultimately show ?thesis
by (unfold cntCS_def,
auto intro!:card_gt_0_iff[symmetric, THEN iffD1])
qed
end
context valid_trace_v_n
begin
lemma not_ready_taker_s[simp]:
"taker \<notin> readys s"
using waiting_taker
by (unfold readys_def, auto)
lemma taker_live_s [simp]: "taker \<in> threads s"
proof -
have "taker \<in> set wq'" by (simp add: eq_wq')
from th'_in_inv[OF this]
have "taker \<in> set rest" .
hence "taker \<in> set (wq s cs)" by (simp add: wq_s_cs)
thus ?thesis using wq_threads by auto
qed
lemma taker_live_es [simp]: "taker \<in> threads (e#s)"
using taker_live_s threads_es by blast
lemma taker_ready_es [simp]:
shows "taker \<in> readys (e#s)"
proof -
{ fix cs'
assume "waiting (e#s) taker cs'"
hence False
proof(cases rule:waiting_esE)
case 1
thus ?thesis using waiting_taker waiting_unique by auto
qed simp
} thus ?thesis by (unfold readys_def, auto)
qed
lemma neq_taker_th: "taker \<noteq> th"
using th_not_waiting waiting_taker by blast
lemma not_holding_taker_s_cs:
shows "\<not> holding s taker cs"
using holding_cs_eq_th neq_taker_th by auto
lemma holdents_es_taker:
"holdents (e#s) taker = holdents s taker \<union> {cs}" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence "holding (e#s) taker cs'" by (auto simp:holdents_def)
hence "cs' \<in> ?R"
proof(cases rule:holding_esE)
case 2
thus ?thesis by (auto simp:holdents_def)
qed auto
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence "holding s taker cs' \<or> cs' = cs" by (auto simp:holdents_def)
hence "cs' \<in> ?L"
proof
assume "holding s taker cs'"
hence "holding (e#s) taker cs'"
using holding_esI2 holding_taker by fastforce
thus ?thesis by (auto simp:holdents_def)
next
assume "cs' = cs"
with holding_taker
show ?thesis by (auto simp:holdents_def)
qed
} ultimately show ?thesis by auto
qed
lemma cntCS_es_taker [simp]: "cntCS (e#s) taker = cntCS s taker + 1"
proof -
have "card (holdents s taker \<union> {cs}) = card (holdents s taker) + 1"
proof(subst card_Un_disjoint)
show "holdents s taker \<inter> {cs} = {}"
using not_holding_taker_s_cs by (auto simp:holdents_def)
qed (auto simp:finite_holdents)
thus ?thesis
by (unfold cntCS_def, insert holdents_es_taker, simp)
qed
lemma pvD_taker_s[simp]: "pvD s taker = 1"
by (unfold pvD_def, simp)
lemma pvD_taker_es[simp]: "pvD (e#s) taker = 0"
by (unfold pvD_def, simp)
lemma pvD_th_s[simp]: "pvD s th = 0"
by (unfold pvD_def, simp)
lemma pvD_th_es[simp]: "pvD (e#s) th = 0"
by (unfold pvD_def, simp)
lemma holdents_es_th:
"holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence "holding (e#s) th cs'" by (auto simp:holdents_def)
hence "cs' \<in> ?R"
proof(cases rule:holding_esE)
case 2
thus ?thesis by (auto simp:holdents_def)
qed (insert neq_taker_th, auto)
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)
from holding_esI2[OF this]
have "cs' \<in> ?L" by (auto simp:holdents_def)
} ultimately show ?thesis by auto
qed
lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"
proof -
have "card (holdents s th - {cs}) = card (holdents s th) - 1"
proof -
have "cs \<in> holdents s th" using holding_th_cs_s
by (auto simp:holdents_def)
moreover have "finite (holdents s th)"
by (simp add: finite_holdents)
ultimately show ?thesis by auto
qed
thus ?thesis by (unfold cntCS_def holdents_es_th)
qed
lemma holdents_kept:
assumes "th' \<noteq> taker"
and "th' \<noteq> th"
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume h: "cs' \<in> ?L"
have "cs' \<in> ?R"
proof(cases "cs' = cs")
case False
hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
by (unfold holdents_def s_holding_def, fold wq_def, auto)
next
case True
from h[unfolded this]
have "holding (e#s) th' cs" by (auto simp:holdents_def)
from held_unique[OF this holding_taker]
have "th' = taker" .
with assms show ?thesis by auto
qed
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
have "cs' \<in> ?L"
proof(cases "cs' = cs")
case False
hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
from h have "holding s th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
next
case True
from h[unfolded this]
have "holding s th' cs" by (auto simp:holdents_def)
from held_unique[OF this holding_th_cs_s]
have "th' = th" .
with assms show ?thesis by auto
qed
} ultimately show ?thesis by auto
qed
lemma cntCS_kept [simp]:
assumes "th' \<noteq> taker"
and "th' \<noteq> th"
shows "cntCS (e#s) th' = cntCS s th'"
by (unfold cntCS_def holdents_kept[OF assms], simp)
lemma readys_kept1:
assumes "th' \<noteq> taker"
and "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms(2)[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)"
using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .
moreover have "\<not> (th' \<in> set rest \<and> th' \<noteq> hd (taker # rest'))"
using n_wait[unfolded True s_waiting_def, folded wq_def,
unfolded wq_es_cs set_wq', unfolded eq_wq'] .
ultimately have "th' = taker" by auto
with assms(1)
show ?thesis by simp
qed
} with assms(2) show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<noteq> taker"
and "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2)[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
have "th' \<in> set rest \<and> th' \<noteq> hd (taker # rest')"
using wait [unfolded True s_waiting_def, folded wq_def,
unfolded wq_es_cs set_wq', unfolded eq_wq'] .
moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest))"
using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .
ultimately have "th' = taker" by auto
with assms(1)
show ?thesis by simp
qed
} with assms(2) show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
assumes "th' \<noteq> taker"
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1[OF assms] readys_kept2[OF assms]
by metis
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof -
{ assume eq_th': "th' = taker"
have ?thesis
apply (unfold eq_th' pvD_taker_es cntCS_es_taker)
by (insert neq_taker_th assms[unfolded eq_th'], unfold is_v, simp)
} moreover {
assume eq_th': "th' = th"
have ?thesis
apply (unfold eq_th' pvD_th_es cntCS_es_th)
by (insert assms[unfolded eq_th'], unfold is_v, simp)
} moreover {
assume h: "th' \<noteq> taker" "th' \<noteq> th"
have ?thesis using assms
apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)
by (fold is_v, unfold pvD_def, simp)
} ultimately show ?thesis by metis
qed
end
context valid_trace_v_e
begin
lemma holdents_es_th:
"holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")
proof -
{ fix cs'
assume "cs' \<in> ?L"
hence "holding (e#s) th cs'" by (auto simp:holdents_def)
hence "cs' \<in> ?R"
proof(cases rule:holding_esE)
case 1
thus ?thesis by (auto simp:holdents_def)
qed
} moreover {
fix cs'
assume "cs' \<in> ?R"
hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)
from holding_esI2[OF this]
have "cs' \<in> ?L" by (auto simp:holdents_def)
} ultimately show ?thesis by auto
qed
lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"
proof -
have "card (holdents s th - {cs}) = card (holdents s th) - 1"
proof -
have "cs \<in> holdents s th" using holding_th_cs_s
by (auto simp:holdents_def)
moreover have "finite (holdents s th)"
by (simp add: finite_holdents)
ultimately show ?thesis by auto
qed
thus ?thesis by (unfold cntCS_def holdents_es_th)
qed
lemma holdents_kept:
assumes "th' \<noteq> th"
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume h: "cs' \<in> ?L"
have "cs' \<in> ?R"
proof(cases "cs' = cs")
case False
hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
by (unfold holdents_def s_holding_def, fold wq_def, auto)
next
case True
from h[unfolded this]
have "holding (e#s) th' cs" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def,
unfolded wq_es_cs nil_wq']
show ?thesis by auto
qed
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
have "cs' \<in> ?L"
proof(cases "cs' = cs")
case False
hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
from h have "holding s th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
next
case True
from h[unfolded this]
have "holding s th' cs" by (auto simp:holdents_def)
from held_unique[OF this holding_th_cs_s]
have "th' = th" .
with assms show ?thesis by auto
qed
} ultimately show ?thesis by auto
qed
lemma cntCS_kept [simp]:
assumes "th' \<noteq> th"
shows "cntCS (e#s) th' = cntCS s th'"
by (unfold cntCS_def holdents_kept[OF assms], simp)
lemma readys_kept1:
assumes "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms(1)[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)"
using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .
hence "th' \<in> set rest" by auto
with set_wq' have "th' \<in> set wq'" by metis
with nil_wq' show ?thesis by simp
qed
} thus ?thesis using assms
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms[unfolded readys_def] by auto
have False
proof(cases "cs' = cs")
case False
with n_wait wait
show ?thesis
by (unfold s_waiting_def, fold wq_def, auto)
next
case True
have "th' \<in> set [] \<and> th' \<noteq> hd []"
using wait[unfolded True s_waiting_def, folded wq_def,
unfolded wq_es_cs nil_wq'] .
thus ?thesis by simp
qed
} with assms show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1[OF assms] readys_kept2[OF assms]
by metis
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof -
{
assume eq_th': "th' = th"
have ?thesis
apply (unfold eq_th' pvD_th_es cntCS_es_th)
by (insert assms[unfolded eq_th'], unfold is_v, simp)
} moreover {
assume h: "th' \<noteq> th"
have ?thesis using assms
apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)
by (fold is_v, unfold pvD_def, simp)
} ultimately show ?thesis by metis
qed
end
context valid_trace_v
begin
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof(cases "rest = []")
case True
then interpret vt: valid_trace_v_e by (unfold_locales, simp)
show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast
next
case False
then interpret vt: valid_trace_v_n by (unfold_locales, simp)
show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast
qed
end
context valid_trace_create
begin
lemma th_not_live_s [simp]: "th \<notin> threads s"
proof -
from pip_e[unfolded is_create]
show ?thesis by (cases, simp)
qed
lemma th_not_ready_s [simp]: "th \<notin> readys s"
using th_not_live_s by (unfold readys_def, simp)
lemma th_live_es [simp]: "th \<in> threads (e#s)"
by (unfold is_create, simp)
lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'"
proof
assume "waiting s th cs'"
from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
qed
lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
proof
assume "holding s th cs'"
from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
qed
lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'"
proof
assume "waiting (e # s) th cs'"
from this[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
qed
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
assume "holding (e # s) th cs'"
from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
have "th \<in> set (wq s cs')" by auto
from wq_threads[OF this] have "th \<in> threads s" .
with th_not_live_s show False by simp
qed
lemma ready_th_es [simp]: "th \<in> readys (e#s)"
by (simp add:readys_def)
lemma holdents_th_s: "holdents s th = {}"
by (unfold holdents_def, auto)
lemma holdents_th_es: "holdents (e#s) th = {}"
by (unfold holdents_def, auto)
lemma cntCS_th_s [simp]: "cntCS s th = 0"
by (unfold cntCS_def, simp add:holdents_th_s)
lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"
by (unfold cntCS_def, simp add:holdents_th_es)
lemma pvD_th_s [simp]: "pvD s th = 0"
by (unfold pvD_def, simp)
lemma pvD_th_es [simp]: "pvD (e#s) th = 0"
by (unfold pvD_def, simp)
lemma holdents_kept:
assumes "th' \<noteq> th"
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} ultimately show ?thesis by auto
qed
lemma cntCS_kept [simp]:
assumes "th' \<noteq> th"
shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
using holdents_kept[OF assms]
by (unfold cntCS_def, simp)
lemma readys_kept1:
assumes "th' \<noteq> th"
and "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
have False by auto
} thus ?thesis using assms
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<noteq> th"
and "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2) by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
assumes "th' \<noteq> th"
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1[OF assms] readys_kept2[OF assms]
by metis
lemma pvD_kept [simp]:
assumes "th' \<noteq> th"
shows "pvD (e#s) th' = pvD s th'"
using assms
by (unfold pvD_def, simp)
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof -
{
assume eq_th': "th' = th"
have ?thesis using assms
by (unfold eq_th', simp, unfold is_create, simp)
} moreover {
assume h: "th' \<noteq> th"
hence ?thesis using assms
by (simp, simp add:is_create)
} ultimately show ?thesis by metis
qed
end
context valid_trace_exit
begin
lemma th_live_s [simp]: "th \<in> threads s"
proof -
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold runing_def readys_def, simp)
qed
lemma th_ready_s [simp]: "th \<in> readys s"
proof -
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold runing_def, simp)
qed
lemma th_not_live_es [simp]: "th \<notin> threads (e#s)"
by (unfold is_exit, simp)
lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
proof -
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold holdents_def, auto)
qed
lemma cntCS_th_s [simp]: "cntCS s th = 0"
proof -
from pip_e[unfolded is_exit]
show ?thesis
by (cases, unfold cntCS_def, simp)
qed
lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
assume "holding (e # s) th cs'"
from this[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp]
have "holding s th cs'"
by (unfold s_holding_def, fold wq_def, auto)
with not_holding_th_s
show False by simp
qed
lemma ready_th_es [simp]: "th \<notin> readys (e#s)"
by (simp add:readys_def)
lemma holdents_th_s: "holdents s th = {}"
by (unfold holdents_def, auto)
lemma holdents_th_es: "holdents (e#s) th = {}"
by (unfold holdents_def, auto)
lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"
by (unfold cntCS_def, simp add:holdents_th_es)
lemma pvD_th_s [simp]: "pvD s th = 0"
by (unfold pvD_def, simp)
lemma pvD_th_es [simp]: "pvD (e#s) th = 0"
by (unfold pvD_def, simp)
lemma holdents_kept:
assumes "th' \<noteq> th"
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} ultimately show ?thesis by auto
qed
lemma cntCS_kept [simp]:
assumes "th' \<noteq> th"
shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
using holdents_kept[OF assms]
by (unfold cntCS_def, simp)
lemma readys_kept1:
assumes "th' \<noteq> th"
and "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
have False by auto
} thus ?thesis using assms
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<noteq> th"
and "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms(2) by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
assumes "th' \<noteq> th"
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1[OF assms] readys_kept2[OF assms]
by metis
lemma pvD_kept [simp]:
assumes "th' \<noteq> th"
shows "pvD (e#s) th' = pvD s th'"
using assms
by (unfold pvD_def, simp)
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
proof -
{
assume eq_th': "th' = th"
have ?thesis using assms
by (unfold eq_th', simp, unfold is_exit, simp)
} moreover {
assume h: "th' \<noteq> th"
hence ?thesis using assms
by (simp, simp add:is_exit)
} ultimately show ?thesis by metis
qed
end
context valid_trace_set
begin
lemma th_live_s [simp]: "th \<in> threads s"
proof -
from pip_e[unfolded is_set]
show ?thesis
by (cases, unfold runing_def readys_def, simp)
qed
lemma th_ready_s [simp]: "th \<in> readys s"
proof -
from pip_e[unfolded is_set]
show ?thesis
by (cases, unfold runing_def, simp)
qed
lemma th_not_live_es [simp]: "th \<in> threads (e#s)"
by (unfold is_set, simp)
lemma holdents_kept:
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
by (unfold holdents_def s_holding_def, fold wq_def,
unfold wq_neq_simp, auto)
} ultimately show ?thesis by auto
qed
lemma cntCS_kept [simp]:
shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
using holdents_kept
by (unfold cntCS_def, simp)
lemma threads_kept[simp]:
"threads (e#s) = threads s"
by (unfold is_set, simp)
lemma readys_kept1:
assumes "th' \<in> readys (e#s)"
shows "th' \<in> readys s"
proof -
{ fix cs'
assume wait: "waiting s th' cs'"
have n_wait: "\<not> waiting (e#s) th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def]
n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
have False by auto
} moreover have "th' \<in> threads s"
using assms[unfolded readys_def] by auto
ultimately show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_kept2:
assumes "th' \<in> readys s"
shows "th' \<in> readys (e#s)"
proof -
{ fix cs'
assume wait: "waiting (e#s) th' cs'"
have n_wait: "\<not> waiting s th' cs'"
using assms by (auto simp:readys_def)
from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_neq_simp]
n_wait[unfolded s_waiting_def, folded wq_def]
have False by auto
} with assms show ?thesis
by (unfold readys_def, auto)
qed
lemma readys_simp [simp]:
shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
using readys_kept1 readys_kept2
by metis
lemma pvD_kept [simp]:
shows "pvD (e#s) th' = pvD s th'"
by (unfold pvD_def, simp)
lemma cnp_cnv_cncs_kept:
assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
shows "cntP (e#s) th' = cntV (e#s) th' + cntCS (e#s) th' + pvD (e#s) th'"
using assms
by (unfold is_set, simp, fold is_set, simp)
end
context valid_trace
begin
lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
proof(induct rule:ind)
case Nil
thus ?case
by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def
s_holding_def, simp)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
show ?case
proof(cases e)
case (Create th prio)
interpret vt_create: valid_trace_create s e th prio
using Create by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_create.cnp_cnv_cncs_kept)
next
case (Exit th)
interpret vt_exit: valid_trace_exit s e th
using Exit by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_exit.cnp_cnv_cncs_kept)
next
case (P th cs)
interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_p.cnp_cnv_cncs_kept)
next
case (V th cs)
interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_v.cnp_cnv_cncs_kept)
next
case (Set th prio)
interpret vt_set: valid_trace_set s e th prio
using Set by (unfold_locales, simp)
show ?thesis using Cons by (simp add: vt_set.cnp_cnv_cncs_kept)
qed
qed
lemma not_thread_holdents:
assumes not_in: "th \<notin> threads s"
shows "holdents s th = {}"
proof -
{ fix cs
assume "cs \<in> holdents s th"
hence "holding s th cs" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def]
have "th \<in> set (wq s cs)" by auto
with wq_threads have "th \<in> threads s" by auto
with assms
have False by simp
} thus ?thesis by auto
qed
lemma not_thread_cncs:
assumes not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
using not_thread_holdents[OF assms]
by (simp add:cntCS_def)
lemma cnp_cnv_eq:
assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
using assms cnp_cnv_cncs not_thread_cncs pvD_def
by (auto)
end
end