section {*
This file contains lemmas used to guide the recalculation of current precedence
after every system call (or system operation)
*}
theory CpsG
imports PrioG Max RTree
begin
text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
difference is the order of arguemts. *}
definition "the_preced s th = preced th s"
lemma inj_the_preced:
"inj_on (the_preced s) (threads s)"
by (metis inj_onI preced_unique the_preced_def)
text {* @{term "the_thread"} extracts thread out of RAG node. *}
fun the_thread :: "node \<Rightarrow> thread" where
"the_thread (Th th) = th"
text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}"
text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
s_holding_abv cs_RAG_def, auto)
text {*
The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
It characterizes the dependency between threads when calculating current
precedences. It is defined as the composition of the above two sub-graphs,
names @{term "wRAG"} and @{term "hRAG"}.
*}
definition "tRAG s = wRAG s O hRAG s"
(* ccc *)
definition "cp_gen s x =
Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
lemma tRAG_Field:
"Field (tRAG s) \<subseteq> Field (RAG s)"
by (unfold tRAG_alt_def Field_def, auto)
lemma tRAG_ancestorsE:
assumes "x \<in> ancestors (tRAG s) u"
obtains th where "x = Th th"
proof -
from assms have "(u, x) \<in> (tRAG s)^+"
by (unfold ancestors_def, auto)
from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
then obtain th where "x = Th th"
by (unfold tRAG_alt_def, auto)
from that[OF this] show ?thesis .
qed
lemma tRAG_mono:
assumes "RAG s' \<subseteq> RAG s"
shows "tRAG s' \<subseteq> tRAG s"
using assms
by (unfold tRAG_alt_def, auto)
lemma holding_next_thI:
assumes "holding s th cs"
and "length (wq s cs) > 1"
obtains th' where "next_th s th cs th'"
proof -
from assms(1)[folded eq_holding, unfolded cs_holding_def]
have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" .
then obtain rest where h1: "wq s cs = th#rest"
by (cases "wq s cs", auto)
with assms(2) have h2: "rest \<noteq> []" by auto
let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
have "next_th s th cs ?th'" using h1(1) h2
by (unfold next_th_def, auto)
from that[OF this] show ?thesis .
qed
lemma RAG_tRAG_transfer:
assumes "vt s'"
assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
and "(Cs cs, Th th'') \<in> RAG s'"
shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
proof -
interpret vt_s': valid_trace "s'" using assms(1)
by (unfold_locales, simp)
interpret rtree: rtree "RAG s'"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:vt_s'.unique_RAG)
show "acyclic (RAG s')"
by (rule vt_s'.acyclic_RAG)
qed
{ fix n1 n2
assume "(n1, n2) \<in> ?L"
from this[unfolded tRAG_alt_def]
obtain th1 th2 cs' where
h: "n1 = Th th1" "n2 = Th th2"
"(Th th1, Cs cs') \<in> RAG s"
"(Cs cs', Th th2) \<in> RAG s" by auto
from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto
from h(3) and assms(2)
have "(Th th1, Cs cs') = (Th th, Cs cs) \<or>
(Th th1, Cs cs') \<in> RAG s'" by auto
hence "(n1, n2) \<in> ?R"
proof
assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
hence eq_th1: "th1 = th" by simp
moreover have "th2 = th''"
proof -
from h1 have "cs' = cs" by simp
from assms(3) cs_in[unfolded this] rtree.sgv
show ?thesis
by (unfold single_valued_def, auto)
qed
ultimately show ?thesis using h(1,2) by auto
next
assume "(Th th1, Cs cs') \<in> RAG s'"
with cs_in have "(Th th1, Th th2) \<in> tRAG s'"
by (unfold tRAG_alt_def, auto)
from this[folded h(1, 2)] show ?thesis by auto
qed
} moreover {
fix n1 n2
assume "(n1, n2) \<in> ?R"
hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto
hence "(n1, n2) \<in> ?L"
proof
assume "(n1, n2) \<in> tRAG s'"
moreover have "... \<subseteq> ?L"
proof(rule tRAG_mono)
show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)
qed
ultimately show ?thesis by auto
next
assume eq_n: "(n1, n2) = (Th th, Th th'')"
from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto
moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto
ultimately show ?thesis
by (unfold eq_n tRAG_alt_def, auto)
qed
} ultimately show ?thesis by auto
qed
context valid_trace
begin
lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
end
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
(is "Max (_ ` ?L) = Max (_ ` ?R)")
proof -
have "?L = ?R"
by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
thus ?thesis by simp
qed
thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
qed
lemma cp_gen_alt_def:
"cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
by (auto simp:cp_gen_def)
lemma tRAG_nodeE:
assumes "(n1, n2) \<in> tRAG s"
obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
using assms
by (auto simp: tRAG_def wRAG_def hRAG_def tRAG_def)
lemma subtree_nodeE:
assumes "n \<in> subtree (tRAG s) (Th th)"
obtains th1 where "n = Th th1"
proof -
show ?thesis
proof(rule subtreeE[OF assms])
assume "n = Th th"
from that[OF this] show ?thesis .
next
assume "Th th \<in> ancestors (tRAG s) n"
hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
hence "\<exists> th1. n = Th th1"
proof(induct)
case (base y)
from tRAG_nodeE[OF this] show ?case by metis
next
case (step y z)
thus ?case by auto
qed
with that show ?thesis by auto
qed
qed
lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"
proof -
have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*"
by (rule rtrancl_mono, auto simp:RAG_split)
also have "... \<subseteq> ((RAG s)^*)^*"
by (rule rtrancl_mono, auto)
also have "... = (RAG s)^*" by simp
finally show ?thesis by (unfold tRAG_def, simp)
qed
lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"
proof -
{ fix a
assume "a \<in> subtree (tRAG s) x"
hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
with tRAG_star_RAG[of s]
have "(a, x) \<in> (RAG s)^*" by auto
hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)
} thus ?thesis by auto
qed
lemma tRAG_trancl_eq:
"{th'. (Th th', Th th) \<in> (tRAG s)^+} =
{th'. (Th th', Th th) \<in> (RAG s)^+}"
(is "?L = ?R")
proof -
{ fix th'
assume "th' \<in> ?L"
hence "(Th th', Th th) \<in> (tRAG s)^+" by auto
from tranclD[OF this]
obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto
from tRAG_subtree_RAG[of s] and this(2)
have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG)
moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto
ultimately have "th' \<in> ?R" by auto
} moreover
{ fix th'
assume "th' \<in> ?R"
hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)
from plus_rpath[OF this]
obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto
hence "(Th th', Th th) \<in> (tRAG s)^+"
proof(induct xs arbitrary:th' th rule:length_induct)
case (1 xs th' th)
then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)
show ?case
proof(cases "xs1")
case Nil
from 1(2)[unfolded Cons1 Nil]
have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
then obtain cs where "x1 = Cs cs"
by (unfold s_RAG_def, auto)
from rpath_nnl_lastE[OF rp[unfolded this]]
show ?thesis by auto
next
case (Cons x2 xs2)
from 1(2)[unfolded Cons1[unfolded this]]
have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
from rpath_edges_on[OF this]
have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
by (simp add: edges_on_unfold)
with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
by (simp add: edges_on_unfold)
from this eds
have rg2: "(x1, x2) \<in> RAG s" by auto
from this[unfolded eq_x1]
obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)
from rp have "rpath (RAG s) x2 xs2 (Th th)"
by (elim rpath_ConsE, simp)
from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
show ?thesis
proof(cases "xs2 = []")
case True
from rpath_nilE[OF rp'[unfolded this]]
have "th1 = th" by auto
from rt1[unfolded this] show ?thesis by auto
next
case False
from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]
have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp
with rt1 show ?thesis by auto
qed
qed
qed
hence "th' \<in> ?L" by auto
} ultimately show ?thesis by blast
qed
lemma tRAG_trancl_eq_Th:
"{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} =
{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}"
using tRAG_trancl_eq by auto
lemma dependants_alt_def:
"dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
context valid_trace
begin
lemma count_eq_tRAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using assms count_eq_dependants dependants_alt_def eq_dependants by auto
lemma count_eq_RAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
using assms count_eq_dependants cs_dependants_def eq_RAG by auto
lemma count_eq_RAG_plus_Th:
assumes "cntP s th = cntV s th"
shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
using count_eq_RAG_plus[OF assms] by auto
lemma count_eq_tRAG_plus_Th:
assumes "cntP s th = cntV s th"
shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
using count_eq_tRAG_plus[OF assms] by auto
end
lemma tRAG_subtree_eq:
"(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}"
(is "?L = ?R")
proof -
{ fix n
assume h: "n \<in> ?L"
hence "n \<in> ?R"
by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG)
} moreover {
fix n
assume "n \<in> ?R"
then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
by (auto simp:subtree_def)
from rtranclD[OF this(2)]
have "n \<in> ?L"
proof
assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto
thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
qed (insert h, auto simp:subtree_def)
} ultimately show ?thesis by auto
qed
lemma threads_set_eq:
"the_thread ` (subtree (tRAG s) (Th th)) =
{th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
lemma cp_alt_def1:
"cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
proof -
have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
by auto
thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
qed
lemma cp_gen_def_cond:
assumes "x = Th th"
shows "cp s th = cp_gen s (Th th)"
by (unfold cp_alt_def1 cp_gen_def, simp)
lemma cp_gen_over_set:
assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
proof(rule f_image_eq)
fix a
assume "a \<in> A"
from assms[rule_format, OF this]
obtain th where eq_a: "a = Th th" by auto
show "cp_gen s a = (cp s \<circ> the_thread) a"
by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
qed
context valid_trace
begin
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
shows "th \<in> threads s"
using assms
by (metis Field_def UnE dm_RAG_threads range_in vt)
lemma subtree_tRAG_thread:
assumes "th \<in> threads s"
shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
proof -
have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
by (unfold tRAG_subtree_eq, simp)
also have "... \<subseteq> ?R"
proof
fix x
assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
from this(2)
show "x \<in> ?R"
proof(cases rule:subtreeE)
case 1
thus ?thesis by (simp add: assms h(1))
next
case 2
thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI)
qed
qed
finally show ?thesis .
qed
lemma readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
proof -
{ fix x
assume "x \<in> ancestors (RAG s) (Th th)"
hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
from tranclD[OF this]
obtain z where "(Th th, z) \<in> RAG s" by auto
with assms(1) have False
apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
by (fold wq_def, blast)
} thus ?thesis by (unfold root_def, auto)
qed
lemma readys_in_no_subtree:
assumes "th \<in> readys s"
and "th' \<noteq> th"
shows "Th th \<notin> subtree (RAG s) (Th th')"
proof
assume "Th th \<in> subtree (RAG s) (Th th')"
thus False
proof(cases rule:subtreeE)
case 1
with assms show ?thesis by auto
next
case 2
with readys_root[OF assms(1)]
show ?thesis by (auto simp:root_def)
qed
qed
lemma not_in_thread_isolated:
assumes "th \<notin> threads s"
shows "(Th th) \<notin> Field (RAG s)"
proof
assume "(Th th) \<in> Field (RAG s)"
with dm_RAG_threads and range_in assms
show False by (unfold Field_def, blast)
qed
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG show "finite (RAG s)" .
next
from acyclic_RAG show "acyclic (RAG s)" .
qed
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
lemma sgv_hRAG: "single_valued (hRAG s)"
using holding_unique
by (unfold single_valued_def hRAG_def, auto)
lemma sgv_tRAG: "single_valued (tRAG s)"
by (unfold tRAG_def, rule single_valued_relcomp,
insert sgv_wRAG sgv_hRAG, auto)
lemma acyclic_tRAG: "acyclic (tRAG s)"
proof(unfold tRAG_def, rule acyclic_compose)
show "acyclic (RAG s)" using acyclic_RAG .
next
show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
next
show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
qed
lemma sgv_RAG: "single_valued (RAG s)"
using unique_RAG by (auto simp:single_valued_def)
lemma rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
end
sublocale valid_trace < rtree_RAG: rtree "RAG s"
proof
show "single_valued (RAG s)"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:unique_RAG)
show "acyclic (RAG s)"
by (rule acyclic_RAG)
qed
sublocale valid_trace < rtree_s: rtree "tRAG s"
proof(unfold_locales)
from sgv_tRAG show "single_valued (tRAG s)" .
next
from acyclic_tRAG show "acyclic (tRAG s)" .
qed
sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"
proof -
show "fsubtree (RAG s)"
proof(intro_locales)
show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
next
show "fsubtree_axioms (RAG s)"
proof(unfold fsubtree_axioms_def)
find_theorems wf RAG
from wf_RAG show "wf (RAG s)" .
qed
qed
qed
sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"
proof -
have "fsubtree (tRAG s)"
proof -
have "fbranch (tRAG s)"
proof(unfold tRAG_def, rule fbranch_compose)
show "fbranch (wRAG s)"
proof(rule finite_fbranchI)
from finite_RAG show "finite (wRAG s)"
by (unfold RAG_split, auto)
qed
next
show "fbranch (hRAG s)"
proof(rule finite_fbranchI)
from finite_RAG
show "finite (hRAG s)" by (unfold RAG_split, auto)
qed
qed
moreover have "wf (tRAG s)"
proof(rule wf_subset)
show "wf (RAG s O RAG s)" using wf_RAG
by (fold wf_comp_self, simp)
next
show "tRAG s \<subseteq> (RAG s O RAG s)"
by (unfold tRAG_alt_def, auto)
qed
ultimately show ?thesis
by (unfold fsubtree_def fsubtree_axioms_def,auto)
qed
from this[folded tRAG_def] show "fsubtree (tRAG s)" .
qed
lemma Max_UNION:
assumes "finite A"
and "A \<noteq> {}"
and "\<forall> M \<in> f ` A. finite M"
and "\<forall> M \<in> f ` A. M \<noteq> {}"
shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
using assms[simp]
proof -
have "?L = Max (\<Union>(f ` A))"
by (fold Union_image_eq, simp)
also have "... = ?R"
by (subst Max_Union, simp+)
finally show ?thesis .
qed
lemma max_Max_eq:
assumes "finite A"
and "A \<noteq> {}"
and "x = y"
shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
proof -
have "?R = Max (insert y A)" by simp
also from assms have "... = ?L"
by (subst Max.insert, simp+)
finally show ?thesis by simp
qed
context valid_trace
begin
(* ddd *)
lemma cp_gen_rec:
assumes "x = Th th"
shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
proof(cases "children (tRAG s) x = {}")
case True
show ?thesis
by (unfold True cp_gen_def subtree_children, simp add:assms)
next
case False
hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
note fsbttRAGs.finite_subtree[simp]
have [simp]: "finite (children (tRAG s) x)"
by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree],
rule children_subtree)
{ fix r x
have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
} note this[simp]
have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
proof -
from False obtain q where "q \<in> children (tRAG s) x" by blast
moreover have "subtree (tRAG s) q \<noteq> {}" by simp
ultimately show ?thesis by blast
qed
have h: "Max ((the_preced s \<circ> the_thread) `
({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
(is "?L = ?R")
proof -
let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
let "Max (_ \<union> (?h ` ?B))" = ?R
let ?L1 = "?f ` \<Union>(?g ` ?B)"
have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
proof -
have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
finally have "Max ?L1 = Max ..." by simp
also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
by (subst Max_UNION, simp+)
also have "... = Max (cp_gen s ` children (tRAG s) x)"
by (unfold image_comp cp_gen_alt_def, simp)
finally show ?thesis .
qed
show ?thesis
proof -
have "?L = Max (?f ` ?A \<union> ?L1)" by simp
also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
by (subst Max_Un, simp+)
also have "... = max (?f x) (Max (?h ` ?B))"
by (unfold eq_Max_L1, simp)
also have "... =?R"
by (rule max_Max_eq, (simp)+, unfold assms, simp)
finally show ?thesis .
qed
qed thus ?thesis
by (fold h subtree_children, unfold cp_gen_def, simp)
qed
lemma cp_rec:
"cp s th = Max ({the_preced s th} \<union>
(cp s o the_thread) ` children (tRAG s) (Th th))"
proof -
have "Th th = Th th" by simp
note h = cp_gen_def_cond[OF this] cp_gen_rec[OF this]
show ?thesis
proof -
have "cp_gen s ` children (tRAG s) (Th th) =
(cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
proof(rule cp_gen_over_set)
show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
by (unfold tRAG_alt_def, auto simp:children_def)
qed
thus ?thesis by (subst (1) h(1), unfold h(2), simp)
qed
qed
end
(* keep *)
lemma next_th_holding:
assumes vt: "vt s"
and nxt: "next_th s th cs th'"
shows "holding (wq s) th cs"
proof -
from nxt[unfolded next_th_def]
obtain rest where h: "wq s cs = th # rest"
"rest \<noteq> []"
"th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
thus ?thesis
by (unfold cs_holding_def, auto)
qed
context valid_trace
begin
lemma next_th_waiting:
assumes nxt: "next_th s th cs th'"
shows "waiting (wq s) th' cs"
proof -
from nxt[unfolded next_th_def]
obtain rest where h: "wq s cs = th # rest"
"rest \<noteq> []"
"th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
from wq_distinct[of cs, unfolded h]
have dst: "distinct (th # rest)" .
have in_rest: "th' \<in> set rest"
proof(unfold h, rule someI2)
show "distinct rest \<and> set rest = set rest" using dst by auto
next
fix x assume "distinct x \<and> set x = set rest"
with h(2)
show "hd x \<in> set (rest)" by (cases x, auto)
qed
hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
moreover have "th' \<noteq> hd (wq s cs)"
by (unfold h(1), insert in_rest dst, auto)
ultimately show ?thesis by (auto simp:cs_waiting_def)
qed
lemma next_th_RAG:
assumes nxt: "next_th (s::event list) th cs th'"
shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
using vt assms next_th_holding next_th_waiting
by (unfold s_RAG_def, simp)
end
-- {* A useless definition *}
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
text {* (* ddd *)
One beauty of our modelling is that we follow the definitional extension tradition of HOL.
The benefit of such a concise and miniature model is that large number of intuitively
obvious facts are derived as lemmas, rather than asserted as axioms.
*}
text {*
However, the lemmas in the forthcoming several locales are no longer
obvious. These lemmas show how the current precedences should be recalculated
after every execution step (in our model, every step is represented by an event,
which in turn, represents a system call, or operation). Each operation is
treated in a separate locale.
The complication of current precedence recalculation comes
because the changing of RAG needs to be taken into account,
in addition to the changing of precedence.
The reason RAG changing affects current precedence is that,
according to the definition, current precedence
of a thread is the maximum of the precedences of its dependants,
where the dependants are defined in terms of RAG.
Therefore, each operation, lemmas concerning the change of the precedences
and RAG are derived first, so that the lemmas about
current precedence recalculation can be based on.
*}
text {* (* ddd *)
The following locale @{text "step_set_cps"} investigates the recalculation
after the @{text "Set"} operation.
*}
locale step_set_cps =
fixes s' th prio s
-- {* @{text "s'"} is the system state before the operation *}
-- {* @{text "s"} is the system state after the operation *}
defines s_def : "s \<equiv> (Set th prio#s')"
-- {* @{text "s"} is assumed to be a legitimate state, from which
the legitimacy of @{text "s"} can be derived. *}
assumes vt_s: "vt s"
sublocale step_set_cps < vat_s : valid_trace "s"
proof
from vt_s show "vt s" .
qed
sublocale step_set_cps < vat_s' : valid_trace "s'"
proof
from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
qed
context step_set_cps
begin
text {* (* ddd *)
The following two lemmas confirm that @{text "Set"}-operating only changes the precedence
of the initiating thread.
*}
lemma eq_preced:
assumes "th' \<noteq> th"
shows "preced th' s = preced th' s'"
proof -
from assms show ?thesis
by (unfold s_def, auto simp:preced_def)
qed
lemma eq_the_preced:
fixes th'
assumes "th' \<noteq> th"
shows "the_preced s th' = the_preced s' th'"
using assms
by (unfold the_preced_def, intro eq_preced, simp)
text {*
The following lemma assures that the resetting of priority does not change the RAG.
*}
lemma eq_dep: "RAG s = RAG s'"
by (unfold s_def RAG_set_unchanged, auto)
text {* (* ddd *)
Th following lemma @{text "eq_cp_pre"} says the priority change of @{text "th"}
only affects those threads, which as @{text "Th th"} in their sub-trees.
The proof of this lemma is simplified by using the alternative definition of @{text "cp"}.
*}
lemma eq_cp_pre:
fixes th'
assumes nd: "Th th \<notin> subtree (RAG s') (Th th')"
shows "cp s th' = cp s' th'"
proof -
-- {* After unfolding using the alternative definition, elements
affecting the @{term "cp"}-value of threads become explicit.
We only need to prove the following: *}
have "Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =
Max (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"
(is "Max (?f ` ?S1) = Max (?g ` ?S2)")
proof -
-- {* The base sets are equal. *}
have "?S1 = ?S2" using eq_dep by simp
-- {* The function values on the base set are equal as well. *}
moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"
proof
fix th1
assume "th1 \<in> ?S2"
with nd have "th1 \<noteq> th" by (auto)
from eq_the_preced[OF this]
show "the_preced s th1 = the_preced s' th1" .
qed
-- {* Therefore, the image of the functions are equal. *}
ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)
thus ?thesis by simp
qed
thus ?thesis by (simp add:cp_alt_def)
qed
text {*
The following lemma shows that @{term "th"} is not in the
sub-tree of any other thread.
*}
lemma th_in_no_subtree:
assumes "th' \<noteq> th"
shows "Th th \<notin> subtree (RAG s') (Th th')"
proof -
have "th \<in> readys s'"
proof -
from step_back_step [OF vt_s[unfolded s_def]]
have "step s' (Set th prio)" .
hence "th \<in> runing s'" by (cases, simp)
thus ?thesis by (simp add:readys_def runing_def)
qed
find_theorems readys subtree
from vat_s'.readys_in_no_subtree[OF this assms(1)]
show ?thesis by blast
qed
text {*
By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"},
it is obvious that the change of priority only affects the @{text "cp"}-value
of the initiating thread @{text "th"}.
*}
lemma eq_cp:
fixes th'
assumes "th' \<noteq> th"
shows "cp s th' = cp s' th'"
by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
end
text {*
The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
*}
locale step_v_cps =
-- {* @{text "th"} is the initiating thread *}
-- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}
fixes s' th cs s -- {* @{text "s'"} is the state before operation*}
defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
-- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
assumes vt_s: "vt s"
sublocale step_v_cps < vat_s : valid_trace "s"
proof
from vt_s show "vt s" .
qed
sublocale step_v_cps < vat_s' : valid_trace "s'"
proof
from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
qed
context step_v_cps
begin
lemma ready_th_s': "th \<in> readys s'"
using step_back_step[OF vt_s[unfolded s_def]]
by (cases, simp add:runing_def)
lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"
proof -
from vat_s'.readys_root[OF ready_th_s']
show ?thesis
by (unfold root_def, simp)
qed
lemma holding_th: "holding s' th cs"
proof -
from vt_s[unfolded s_def]
have " PIP s' (V th cs)" by (cases, simp)
thus ?thesis by (cases, auto)
qed
lemma edge_of_th:
"(Cs cs, Th th) \<in> RAG s'"
proof -
from holding_th
show ?thesis
by (unfold s_RAG_def holding_eq, auto)
qed
lemma ancestors_cs:
"ancestors (RAG s') (Cs cs) = {Th th}"
proof -
have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \<union> {Th th}"
proof(rule vat_s'.rtree_RAG.ancestors_accum)
from vt_s[unfolded s_def]
have " PIP s' (V th cs)" by (cases, simp)
thus "(Cs cs, Th th) \<in> RAG s'"
proof(cases)
assume "holding s' th cs"
from this[unfolded holding_eq]
show ?thesis by (unfold s_RAG_def, auto)
qed
qed
from this[unfolded ancestors_th] show ?thesis by simp
qed
lemma preced_kept: "the_preced s = the_preced s'"
by (auto simp: s_def the_preced_def preced_def)
end
text {*
The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
which represents the case when there is another thread @{text "th'"}
to take over the critical resource released by the initiating thread @{text "th"}.
*}
locale step_v_cps_nt = step_v_cps +
fixes th'
-- {* @{text "th'"} is assumed to take over @{text "cs"} *}
assumes nt: "next_th s' th cs th'"
context step_v_cps_nt
begin
text {*
Lemma @{text "RAG_s"} confirms the change of RAG:
two edges removed and one added, as shown by the following diagram.
*}
(*
RAG before the V-operation
th1 ----|
|
th' ----|
|----> cs -----|
th2 ----| |
| |
th3 ----| |
|------> th
th4 ----| |
| |
th5 ----| |
|----> cs'-----|
th6 ----|
|
th7 ----|
RAG after the V-operation
th1 ----|
|
|----> cs ----> th'
th2 ----|
|
th3 ----|
th4 ----|
|
th5 ----|
|----> cs'----> th
th6 ----|
|
th7 ----|
*)
lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
using next_th_RAG[OF nt] .
lemma ancestors_th':
"ancestors (RAG s') (Th th') = {Th th, Cs cs}"
proof -
have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"
proof(rule vat_s'.rtree_RAG.ancestors_accum)
from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto
qed
thus ?thesis using ancestors_th ancestors_cs by auto
qed
lemma RAG_s:
"RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
{(Cs cs, Th th')}"
proof -
from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
and nt show ?thesis by (auto intro:next_th_unique)
qed
lemma subtree_kept:
assumes "th1 \<notin> {th, th'}"
shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)" (is "_ = ?R")
proof -
let ?RAG' = "(RAG s' - {(Cs cs, Th th), (Th th', Cs cs)})"
let ?RAG'' = "?RAG' \<union> {(Cs cs, Th th')}"
have "subtree ?RAG' (Th th1) = ?R"
proof(rule subset_del_subtree_outside)
show "Range {(Cs cs, Th th), (Th th', Cs cs)} \<inter> subtree (RAG s') (Th th1) = {}"
proof -
have "(Th th) \<notin> subtree (RAG s') (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s') (Th th)"
by (unfold ancestors_th, simp)
next
from assms show "Th th1 \<noteq> Th th" by simp
qed
moreover have "(Cs cs) \<notin> subtree (RAG s') (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s') (Cs cs)"
by (unfold ancestors_cs, insert assms, auto)
qed simp
ultimately have "{Th th, Cs cs} \<inter> subtree (RAG s') (Th th1) = {}" by auto
thus ?thesis by simp
qed
qed
moreover have "subtree ?RAG'' (Th th1) = subtree ?RAG' (Th th1)"
proof(rule subtree_insert_next)
show "Th th' \<notin> subtree (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) (Th th')"
(is "_ \<notin> ?R")
proof -
have "?R \<subseteq> ancestors (RAG s') (Th th')" by (rule ancestors_mono, auto)
moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp
ultimately show ?thesis by auto
qed
next
from assms show "Th th1 \<noteq> Th th'" by simp
qed
qed
ultimately show ?thesis by (unfold RAG_s, simp)
qed
lemma cp_kept:
assumes "th1 \<notin> {th, th'}"
shows "cp s th1 = cp s' th1"
by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)
end
locale step_v_cps_nnt = step_v_cps +
assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
context step_v_cps_nnt
begin
lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"
proof -
from nnt and step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
show ?thesis by auto
qed
lemma subtree_kept:
assumes "th1 \<noteq> th"
shows "subtree (RAG s) (Th th1) = subtree (RAG s') (Th th1)"
proof(unfold RAG_s, rule subset_del_subtree_outside)
show "Range {(Cs cs, Th th)} \<inter> subtree (RAG s') (Th th1) = {}"
proof -
have "(Th th) \<notin> subtree (RAG s') (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s') (Th th)"
by (unfold ancestors_th, simp)
next
from assms show "Th th1 \<noteq> Th th" by simp
qed
thus ?thesis by auto
qed
qed
lemma cp_kept_1:
assumes "th1 \<noteq> th"
shows "cp s th1 = cp s' th1"
by (unfold cp_alt_def preced_kept subtree_kept[OF assms], simp)
lemma subtree_cs: "subtree (RAG s') (Cs cs) = {Cs cs}"
proof -
{ fix n
have "(Cs cs) \<notin> ancestors (RAG s') n"
proof
assume "Cs cs \<in> ancestors (RAG s') n"
hence "(n, Cs cs) \<in> (RAG s')^+" by (auto simp:ancestors_def)
from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s'" by auto
then obtain th' where "nn = Th th'"
by (unfold s_RAG_def, auto)
from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s'" .
from this[unfolded s_RAG_def]
have "waiting (wq s') th' cs" by auto
from this[unfolded cs_waiting_def]
have "1 < length (wq s' cs)"
by (cases "wq s' cs", auto)
from holding_next_thI[OF holding_th this]
obtain th' where "next_th s' th cs th'" by auto
with nnt show False by auto
qed
} note h = this
{ fix n
assume "n \<in> subtree (RAG s') (Cs cs)"
hence "n = (Cs cs)"
by (elim subtreeE, insert h, auto)
} moreover have "(Cs cs) \<in> subtree (RAG s') (Cs cs)"
by (auto simp:subtree_def)
ultimately show ?thesis by auto
qed
lemma subtree_th:
"subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"
find_theorems "subtree" "_ - _" RAG
proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)
from edge_of_th
show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"
by (unfold edges_in_def, auto simp:subtree_def)
qed
lemma cp_kept_2:
shows "cp s th = cp s' th"
by (unfold cp_alt_def subtree_th preced_kept, auto)
lemma eq_cp:
fixes th'
shows "cp s th' = cp s' th'"
using cp_kept_1 cp_kept_2
by (cases "th' = th", auto)
end
locale step_P_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (P th cs#s')"
assumes vt_s: "vt s"
sublocale step_P_cps < vat_s : valid_trace "s"
proof
from vt_s show "vt s" .
qed
sublocale step_P_cps < vat_s' : valid_trace "s'"
proof
from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
qed
context step_P_cps
begin
lemma readys_th: "th \<in> readys s'"
proof -
from step_back_step [OF vt_s[unfolded s_def]]
have "PIP s' (P th cs)" .
hence "th \<in> runing s'" by (cases, simp)
thus ?thesis by (simp add:readys_def runing_def)
qed
lemma root_th: "root (RAG s') (Th th)"
using readys_root[OF readys_th] .
lemma in_no_others_subtree:
assumes "th' \<noteq> th"
shows "Th th \<notin> subtree (RAG s') (Th th')"
proof
assume "Th th \<in> subtree (RAG s') (Th th')"
thus False
proof(cases rule:subtreeE)
case 1
with assms show ?thesis by auto
next
case 2
with root_th show ?thesis by (auto simp:root_def)
qed
qed
lemma preced_kept: "the_preced s = the_preced s'"
by (auto simp: s_def the_preced_def preced_def)
end
locale step_P_cps_ne =step_P_cps +
fixes th'
assumes ne: "wq s' cs \<noteq> []"
defines th'_def: "th' \<equiv> hd (wq s' cs)"
locale step_P_cps_e =step_P_cps +
assumes ee: "wq s' cs = []"
context step_P_cps_e
begin
lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"
proof -
from ee and step_RAG_p[OF vt_s[unfolded s_def], folded s_def]
show ?thesis by auto
qed
lemma subtree_kept:
assumes "th' \<noteq> th"
shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"
proof(unfold RAG_s, rule subtree_insert_next)
from in_no_others_subtree[OF assms]
show "Th th \<notin> subtree (RAG s') (Th th')" .
qed
lemma cp_kept:
assumes "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof -
have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =
(the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"
by (unfold preced_kept subtree_kept[OF assms], simp)
thus ?thesis by (unfold cp_alt_def, simp)
qed
end
context step_P_cps_ne
begin
lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
proof -
from step_RAG_p[OF vt_s[unfolded s_def]] and ne
show ?thesis by (simp add:s_def)
qed
lemma cs_held: "(Cs cs, Th th') \<in> RAG s'"
proof -
have "(Cs cs, Th th') \<in> hRAG s'"
proof -
from ne
have " holding s' th' cs"
by (unfold th'_def holding_eq cs_holding_def, auto)
thus ?thesis
by (unfold hRAG_def, auto)
qed
thus ?thesis by (unfold RAG_split, auto)
qed
lemma tRAG_s:
"tRAG s = tRAG s' \<union> {(Th th, Th th')}"
using RAG_tRAG_transfer[OF RAG_s cs_held] .
lemma cp_kept:
assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)"
shows "cp s th'' = cp s' th''"
proof -
have h: "subtree (tRAG s) (Th th'') = subtree (tRAG s') (Th th'')"
proof -
have "Th th' \<notin> subtree (tRAG s') (Th th'')"
proof
assume "Th th' \<in> subtree (tRAG s') (Th th'')"
thus False
proof(rule subtreeE)
assume "Th th' = Th th''"
from assms[unfolded tRAG_s ancestors_def, folded this]
show ?thesis by auto
next
assume "Th th'' \<in> ancestors (tRAG s') (Th th')"
moreover have "... \<subseteq> ancestors (tRAG s) (Th th')"
proof(rule ancestors_mono)
show "tRAG s' \<subseteq> tRAG s" by (unfold tRAG_s, auto)
qed
ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th')" by auto
moreover have "Th th' \<in> ancestors (tRAG s) (Th th)"
by (unfold tRAG_s, auto simp:ancestors_def)
ultimately have "Th th'' \<in> ancestors (tRAG s) (Th th)"
by (auto simp:ancestors_def)
with assms show ?thesis by auto
qed
qed
from subtree_insert_next[OF this]
have "subtree (tRAG s' \<union> {(Th th, Th th')}) (Th th'') = subtree (tRAG s') (Th th'')" .
from this[folded tRAG_s] show ?thesis .
qed
show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
qed
lemma cp_gen_update_stop: (* ddd *)
assumes "u \<in> ancestors (tRAG s) (Th th)"
and "cp_gen s u = cp_gen s' u"
and "y \<in> ancestors (tRAG s) u"
shows "cp_gen s y = cp_gen s' y"
using assms(3)
proof(induct rule:wf_induct[OF vat_s.fsbttRAGs.wf])
case (1 x)
show ?case (is "?L = ?R")
proof -
from tRAG_ancestorsE[OF 1(2)]
obtain th2 where eq_x: "x = Th th2" by blast
from vat_s.cp_gen_rec[OF this]
have "?L =
Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .
also have "... =
Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
proof -
from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
moreover have "cp_gen s ` RTree.children (tRAG s) x =
cp_gen s' ` RTree.children (tRAG s') x"
proof -
have "RTree.children (tRAG s) x = RTree.children (tRAG s') x"
proof(unfold tRAG_s, rule children_union_kept)
have start: "(Th th, Th th') \<in> tRAG s"
by (unfold tRAG_s, auto)
note x_u = 1(2)
show "x \<notin> Range {(Th th, Th th')}"
proof
assume "x \<in> Range {(Th th, Th th')}"
hence eq_x: "x = Th th'" using RangeE by auto
show False
proof(cases rule:vat_s.rtree_s.ancestors_headE[OF assms(1) start])
case 1
from x_u[folded this, unfolded eq_x] vat_s.acyclic_tRAG
show ?thesis by (auto simp:ancestors_def acyclic_def)
next
case 2
with x_u[unfolded eq_x]
have "(Th th', Th th') \<in> (tRAG s)^+" by (auto simp:ancestors_def)
with vat_s.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
qed
qed
qed
moreover have "cp_gen s ` RTree.children (tRAG s) x =
cp_gen s' ` RTree.children (tRAG s) x" (is "?f ` ?A = ?g ` ?A")
proof(rule f_image_eq)
fix a
assume a_in: "a \<in> ?A"
from 1(2)
show "?f a = ?g a"
proof(cases rule:vat_s.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
case in_ch
show ?thesis
proof(cases "a = u")
case True
from assms(2)[folded this] show ?thesis .
next
case False
have a_not_in: "a \<notin> ancestors (tRAG s) (Th th)"
proof
assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
have "a = u"
proof(rule vat_s.rtree_s.ancestors_children_unique)
from a_in' a_in show "a \<in> ancestors (tRAG s) (Th th) \<inter>
RTree.children (tRAG s) x" by auto
next
from assms(1) in_ch show "u \<in> ancestors (tRAG s) (Th th) \<inter>
RTree.children (tRAG s) x" by auto
qed
with False show False by simp
qed
from a_in obtain th_a where eq_a: "a = Th th_a"
by (unfold RTree.children_def tRAG_alt_def, auto)
from cp_kept[OF a_not_in[unfolded eq_a]]
have "cp s th_a = cp s' th_a" .
from this [unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
show ?thesis .
qed
next
case (out_ch z)
hence h: "z \<in> ancestors (tRAG s) u" "z \<in> RTree.children (tRAG s) x" by auto
show ?thesis
proof(cases "a = z")
case True
from h(2) have zx_in: "(z, x) \<in> (tRAG s)" by (auto simp:RTree.children_def)
from 1(1)[rule_format, OF this h(1)]
have eq_cp_gen: "cp_gen s z = cp_gen s' z" .
with True show ?thesis by metis
next
case False
from a_in obtain th_a where eq_a: "a = Th th_a"
by (auto simp:RTree.children_def tRAG_alt_def)
have "a \<notin> ancestors (tRAG s) (Th th)"
proof
assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
have "a = z"
proof(rule vat_s.rtree_s.ancestors_children_unique)
from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)"
by (auto simp:ancestors_def)
with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter>
RTree.children (tRAG s) x" by auto
next
from a_in a_in'
show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x"
by auto
qed
with False show False by auto
qed
from cp_kept[OF this[unfolded eq_a]]
have "cp s th_a = cp s' th_a" .
from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
show ?thesis .
qed
qed
qed
ultimately show ?thesis by metis
qed
ultimately show ?thesis by simp
qed
also have "... = ?R"
by (fold vat_s'.cp_gen_rec[OF eq_x], simp)
finally show ?thesis .
qed
qed
lemma cp_up:
assumes "(Th th') \<in> ancestors (tRAG s) (Th th)"
and "cp s th' = cp s' th'"
and "(Th th'') \<in> ancestors (tRAG s) (Th th')"
shows "cp s th'' = cp s' th''"
proof -
have "cp_gen s (Th th'') = cp_gen s' (Th th'')"
proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])
from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]
show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis
qed
with cp_gen_def_cond[OF refl[of "Th th''"]]
show ?thesis by metis
qed
end
locale step_create_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Create th prio#s')"
assumes vt_s: "vt s"
sublocale step_create_cps < vat_s: valid_trace "s"
by (unfold_locales, insert vt_s, simp)
sublocale step_create_cps < vat_s': valid_trace "s'"
by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
context step_create_cps
begin
lemma RAG_kept: "RAG s = RAG s'"
by (unfold s_def RAG_create_unchanged, auto)
lemma tRAG_kept: "tRAG s = tRAG s'"
by (unfold tRAG_alt_def RAG_kept, auto)
lemma preced_kept:
assumes "th' \<noteq> th"
shows "the_preced s th' = the_preced s' th'"
by (unfold s_def the_preced_def preced_def, insert assms, auto)
lemma th_not_in: "Th th \<notin> Field (tRAG s')"
proof -
from vt_s[unfolded s_def]
have "PIP s' (Create th prio)" by (cases, simp)
hence "th \<notin> threads s'" by(cases, simp)
from vat_s'.not_in_thread_isolated[OF this]
have "Th th \<notin> Field (RAG s')" .
with tRAG_Field show ?thesis by auto
qed
lemma eq_cp:
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof -
have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
(the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
proof(unfold tRAG_kept, rule f_image_eq)
fix a
assume a_in: "a \<in> subtree (tRAG s') (Th th')"
then obtain th_a where eq_a: "a = Th th_a"
proof(cases rule:subtreeE)
case 2
from ancestors_Field[OF 2(2)]
and that show ?thesis by (unfold tRAG_alt_def, auto)
qed auto
have neq_th_a: "th_a \<noteq> th"
proof -
have "(Th th) \<notin> subtree (tRAG s') (Th th')"
proof
assume "Th th \<in> subtree (tRAG s') (Th th')"
thus False
proof(cases rule:subtreeE)
case 2
from ancestors_Field[OF this(2)]
and th_not_in[unfolded Field_def]
show ?thesis by auto
qed (insert assms, auto)
qed
with a_in[unfolded eq_a] show ?thesis by auto
qed
from preced_kept[OF this]
show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
by (unfold eq_a, simp)
qed
thus ?thesis by (unfold cp_alt_def1, simp)
qed
lemma children_of_th: "RTree.children (tRAG s) (Th th) = {}"
proof -
{ fix a
assume "a \<in> RTree.children (tRAG s) (Th th)"
hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def)
with th_not_in have False
by (unfold Field_def tRAG_kept, auto)
} thus ?thesis by auto
qed
lemma eq_cp_th: "cp s th = preced th s"
by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)
end
locale step_exit_cps =
fixes s' th prio s
defines s_def : "s \<equiv> Exit th # s'"
assumes vt_s: "vt s"
sublocale step_exit_cps < vat_s: valid_trace "s"
by (unfold_locales, insert vt_s, simp)
sublocale step_exit_cps < vat_s': valid_trace "s'"
by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
context step_exit_cps
begin
lemma preced_kept:
assumes "th' \<noteq> th"
shows "the_preced s th' = the_preced s' th'"
by (unfold s_def the_preced_def preced_def, insert assms, auto)
lemma RAG_kept: "RAG s = RAG s'"
by (unfold s_def RAG_exit_unchanged, auto)
lemma tRAG_kept: "tRAG s = tRAG s'"
by (unfold tRAG_alt_def RAG_kept, auto)
lemma th_ready: "th \<in> readys s'"
proof -
from vt_s[unfolded s_def]
have "PIP s' (Exit th)" by (cases, simp)
hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis)
thus ?thesis by (unfold runing_def, auto)
qed
lemma th_holdents: "holdents s' th = {}"
proof -
from vt_s[unfolded s_def]
have "PIP s' (Exit th)" by (cases, simp)
thus ?thesis by (cases, metis)
qed
lemma th_RAG: "Th th \<notin> Field (RAG s')"
proof -
have "Th th \<notin> Range (RAG s')"
proof
assume "Th th \<in> Range (RAG s')"
then obtain cs where "holding (wq s') th cs"
by (unfold Range_iff s_RAG_def, auto)
with th_holdents[unfolded holdents_def]
show False by (unfold eq_holding, auto)
qed
moreover have "Th th \<notin> Domain (RAG s')"
proof
assume "Th th \<in> Domain (RAG s')"
then obtain cs where "waiting (wq s') th cs"
by (unfold Domain_iff s_RAG_def, auto)
with th_ready show False by (unfold readys_def eq_waiting, auto)
qed
ultimately show ?thesis by (auto simp:Field_def)
qed
lemma th_tRAG: "(Th th) \<notin> Field (tRAG s')"
using th_RAG tRAG_Field[of s'] by auto
lemma eq_cp:
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof -
have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
(the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
proof(unfold tRAG_kept, rule f_image_eq)
fix a
assume a_in: "a \<in> subtree (tRAG s') (Th th')"
then obtain th_a where eq_a: "a = Th th_a"
proof(cases rule:subtreeE)
case 2
from ancestors_Field[OF 2(2)]
and that show ?thesis by (unfold tRAG_alt_def, auto)
qed auto
have neq_th_a: "th_a \<noteq> th"
proof -
find_theorems readys subtree s'
from vat_s'.readys_in_no_subtree[OF th_ready assms]
have "(Th th) \<notin> subtree (RAG s') (Th th')" .
with tRAG_subtree_RAG[of s' "Th th'"]
have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
with a_in[unfolded eq_a] show ?thesis by auto
qed
from preced_kept[OF this]
show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
by (unfold eq_a, simp)
qed
thus ?thesis by (unfold cp_alt_def1, simp)
qed
end
end