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
definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}"
definition "tRAG s = wRAG s O hRAG s"
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)
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_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 rtree: rtree "RAG s'"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:unique_RAG[OF assms(1)])
show "acyclic (RAG s')"
by (rule acyclic_RAG[OF assms(1)])
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
lemma readys_root:
assumes "vt s"
and "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(2) 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 "vt s"
and "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,2)]
show ?thesis by (auto simp:root_def)
qed
qed
lemma image_id:
assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x"
shows "f ` A = A"
using assms by (auto simp:image_def)
definition "the_preced s th = preced th s"
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
fun the_thread :: "node \<Rightarrow> thread" where
"the_thread (Th th) = th"
definition "cp_gen s x =
Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
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 threads_set_eq:
"the_thread ` (subtree (tRAG s) (Th th)) =
{th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
proof -
{ fix th'
assume "th' \<in> ?L"
then obtain n where h: "th' = the_thread n" "n \<in> subtree (tRAG s) (Th th)" by auto
from subtree_nodeE[OF this(2)]
obtain th1 where "n = Th th1" by auto
with h have "Th th' \<in> subtree (tRAG s) (Th th)" by auto
hence "Th th' \<in> subtree (RAG s) (Th th)"
proof(cases rule:subtreeE[consumes 1])
case 1
thus ?thesis by (auto simp:subtree_def)
next
case 2
hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
thus ?thesis
proof(induct)
case (step y z)
from this(2)[unfolded tRAG_alt_def]
obtain u where
h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s"
by auto
hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def)
with step(3)
show ?case by (auto simp:subtree_def)
next
case (base y)
from this[unfolded tRAG_alt_def]
show ?case by (auto simp:subtree_def)
qed
qed
hence "th' \<in> ?R" by auto
} moreover {
fix th'
assume "th' \<in> ?R"
hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def)
from star_rpath[OF this]
obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto
hence "Th th' \<in> subtree (tRAG s) (Th th)"
proof(induct xs arbitrary:th' th rule:length_induct)
case (1 xs th' th)
show ?case
proof(cases xs)
case Nil
from rpath_nilE[OF 1(2)[unfolded this]]
have "th' = th" by auto
thus ?thesis by (auto simp:subtree_def)
next
case (Cons x1 xs1) note Cons1 = Cons
show ?thesis
proof(cases "xs1")
case Nil
from 1(2)[unfolded Cons[unfolded this]]
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)
find_theorems rpath "_ = _@[_]"
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 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)" .
from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons]
have "Th th1 \<in> subtree (tRAG s) (Th th)" by simp
moreover have "(Th th', Th th1) \<in> (tRAG s)^*"
proof -
from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto)
qed
ultimately show ?thesis by (auto simp:subtree_def)
qed
qed
qed
from imageI[OF this, of the_thread]
have "th' \<in> ?L" by simp
} ultimately show ?thesis by auto
qed
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
locale valid_trace =
fixes s
assumes vt : "vt s"
context valid_trace
begin
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG[OF vt] show "finite (RAG s)" .
next
from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
qed
end
context valid_trace
begin
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique[OF vt]
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[OF vt] .
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[OF vt] by (auto simp:single_valued_def)
lemma rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG[OF vt]
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
end
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[OF vt]] .
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[OF vt] show "finite (wRAG s)"
by (unfold RAG_split, auto)
qed
next
show "fbranch (hRAG s)"
proof(rule finite_fbranchI)
from finite_RAG[OF vt]
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
lemma eq_dependants: "dependants (wq s) = dependants s"
by (simp add: s_dependants_abv wq_def)
(* obvious lemma *)
lemma not_thread_holdents:
fixes th s
assumes vt: "vt s"
and not_in: "th \<notin> threads s"
shows "holdents s th = {}"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
from stp show ?case
proof(cases)
case (thread_create thread prio)
assume eq_e: "e = Create thread prio"
and not_in': "thread \<notin> threads s"
have "holdents (e # s) th = holdents s th"
apply (unfold eq_e holdents_test)
by (simp add:RAG_create_unchanged)
moreover have "th \<notin> threads s"
proof -
from not_in eq_e show ?thesis by simp
qed
moreover note ih ultimately show ?thesis by auto
next
case (thread_exit thread)
assume eq_e: "e = Exit thread"
and nh: "holdents s thread = {}"
show ?thesis
proof(cases "th = thread")
case True
with nh eq_e
show ?thesis
by (auto simp:holdents_test RAG_exit_unchanged)
next
case False
with not_in and eq_e
have "th \<notin> threads s" by simp
from ih[OF this] False eq_e show ?thesis
by (auto simp:holdents_test RAG_exit_unchanged)
qed
next
case (thread_P thread cs)
assume eq_e: "e = P thread cs"
and is_runing: "thread \<in> runing s"
from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
moreover from is_runing have "thread \<in> threads s"
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
hence "holdents (e # s) th = holdents s th "
apply (unfold cntCS_def holdents_test eq_e)
by (unfold step_RAG_p[OF vtp], auto)
moreover have "holdents s th = {}"
proof(rule ih)
from not_in eq_e show "th \<notin> threads s" by simp
qed
ultimately show ?thesis by simp
next
case (thread_V thread cs)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
have neq_th: "th \<noteq> thread"
proof -
from not_in eq_e have "th \<notin> threads s" by simp
moreover from is_runing have "thread \<in> threads s"
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
from hold obtain rest
where eq_wq: "wq s cs = thread # rest"
by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
from not_in eq_e eq_wq
have "\<not> next_th s thread cs th"
apply (auto simp:next_th_def)
proof -
assume ne: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
have "?t \<in> set rest"
proof(rule someI2)
from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x assume "distinct x \<and> set x = set rest" with ne
show "hd x \<in> set rest" by (cases x, auto)
qed
with eq_wq have "?t \<in> set (wq s cs)" by simp
from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
show False by auto
qed
moreover note neq_th eq_wq
ultimately have "holdents (e # s) th = holdents s th"
by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
moreover have "holdents s th = {}"
proof(rule ih)
from not_in eq_e show "th \<notin> threads s" by simp
qed
ultimately show ?thesis by simp
next
case (thread_set thread prio)
print_facts
assume eq_e: "e = Set thread prio"
and is_runing: "thread \<in> runing s"
from not_in and eq_e have "th \<notin> threads s" by auto
from ih [OF this] and eq_e
show ?thesis
apply (unfold eq_e cntCS_def holdents_test)
by (simp add:RAG_set_unchanged)
qed
next
case vt_nil
show ?case
by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
qed
qed
(* obvious lemma *)
lemma next_th_neq:
assumes vt: "vt s"
and nt: "next_th s th cs th'"
shows "th' \<noteq> th"
proof -
from nt show ?thesis
apply (auto simp:next_th_def)
proof -
fix rest
assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
and ne: "rest \<noteq> []"
have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest"
proof(rule someI2)
from wq_distinct[OF vt, of cs] eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
fix x
assume "distinct x \<and> set x = set rest"
hence eq_set: "set x = set rest" by auto
with ne have "x \<noteq> []" by auto
hence "hd x \<in> set x" by auto
with eq_set show "hd x \<in> set rest" by auto
qed
with wq_distinct[OF vt, of cs] eq_wq show False by auto
qed
qed
(* obvious lemma *)
lemma next_th_unique:
assumes nt1: "next_th s th cs th1"
and nt2: "next_th s th cs th2"
shows "th1 = th2"
using assms by (unfold next_th_def, auto)
lemma wf_RAG:
assumes vt: "vt s"
shows "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG[OF vt] show "finite (RAG s)" .
next
from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
qed
definition child :: "state \<Rightarrow> (node \<times> node) set"
where "child s \<equiv>
{(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
lemma children_def2:
"children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
unfolding child_def children_def by simp
lemma children_dependants:
"children s th \<subseteq> dependants (wq s) th"
unfolding children_def2
unfolding cs_dependants_def
by (auto simp add: eq_RAG)
lemma child_unique:
assumes vt: "vt s"
and ch1: "(Th th, Th th1) \<in> child s"
and ch2: "(Th th, Th th2) \<in> child s"
shows "th1 = th2"
using ch1 ch2
proof(unfold child_def, clarsimp)
fix cs csa
assume h1: "(Th th, Cs cs) \<in> RAG s"
and h2: "(Cs cs, Th th1) \<in> RAG s"
and h3: "(Th th, Cs csa) \<in> RAG s"
and h4: "(Cs csa, Th th2) \<in> RAG s"
from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
from unique_RAG[OF vt h2 this]
show "th1 = th2" by simp
qed
lemma RAG_children:
assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
proof -
from h show ?thesis
proof(induct rule: tranclE)
fix c th2
assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
and h2: "(c, Th th2) \<in> RAG s"
from h2 obtain cs where eq_c: "c = Cs cs"
by (case_tac c, auto simp:s_RAG_def)
show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
proof(rule tranclE[OF h1])
fix ca
assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
and h4: "(ca, c) \<in> RAG s"
show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
proof -
from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
by (case_tac ca, auto simp:s_RAG_def)
from eq_ca h4 h2 eq_c
have "th3 \<in> children s th2" by (auto simp:children_def child_def)
moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
ultimately show ?thesis by auto
qed
next
assume "(Th th1, c) \<in> RAG s"
with h2 eq_c
have "th1 \<in> children s th2"
by (auto simp:children_def child_def)
thus ?thesis by auto
qed
next
assume "(Th th1, Th th2) \<in> RAG s"
thus ?thesis
by (auto simp:s_RAG_def)
qed
qed
lemma sub_child: "child s \<subseteq> (RAG s)^+"
by (unfold child_def, auto)
lemma wf_child:
assumes vt: "vt s"
shows "wf (child s)"
apply(rule wf_subset)
apply(rule wf_trancl[OF wf_RAG[OF vt]])
apply(rule sub_child)
done
lemma RAG_child_pre:
assumes vt: "vt s"
shows
"(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
proof -
from wf_trancl[OF wf_RAG[OF vt]]
have wf: "wf ((RAG s)^+)" .
show ?thesis
proof(rule wf_induct[OF wf, of ?P], clarsimp)
fix th'
assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
(Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
show "(Th th, Th th') \<in> (child s)\<^sup>+"
proof -
from RAG_children[OF h]
have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
thus ?thesis
proof
assume "th \<in> children s th'"
thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
next
assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
then obtain th3 where th3_in: "th3 \<in> children s th'"
and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
qed
qed
qed
qed
lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
by (insert RAG_child_pre, auto)
lemma child_RAG_p:
assumes "(n1, n2) \<in> (child s)^+"
shows "(n1, n2) \<in> (RAG s)^+"
proof -
from assms show ?thesis
proof(induct)
case (base y)
with sub_child show ?case by auto
next
case (step y z)
assume "(y, z) \<in> child s"
with sub_child have "(y, z) \<in> (RAG s)^+" by auto
moreover have "(n1, y) \<in> (RAG s)^+" by fact
ultimately show ?case by auto
qed
qed
text {* (* ddd *)
*}
lemma child_RAG_eq:
assumes vt: "vt s"
shows "(Th th1, Th th2) \<in> (child s)^+ \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
by (auto intro: RAG_child[OF vt] child_RAG_p)
text {* (* ddd *)
*}
lemma children_no_dep:
fixes s th th1 th2 th3
assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"
shows "False"
proof -
from RAG_child[OF vt ch3]
have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
thus ?thesis
proof(rule converse_tranclE)
assume "(Th th1, Th th2) \<in> child s"
from child_unique[OF vt ch1 this] have "th = th2" by simp
with ch2 have "(Th th2, Th th2) \<in> child s" by simp
with wf_child[OF vt] show ?thesis by auto
next
fix c
assume h1: "(Th th1, c) \<in> child s"
and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
with h1 have "(Th th1, Th th3) \<in> child s" by simp
from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
moreover have "wf ((child s)\<^sup>+)"
proof(rule wf_trancl)
from wf_child[OF vt] show "wf (child s)" .
qed
ultimately show False by auto
qed
qed
text {* (* ddd *)
*}
lemma unique_RAG_p:
assumes vt: "vt s"
and dp1: "(n, n1) \<in> (RAG s)^+"
and dp2: "(n, n2) \<in> (RAG s)^+"
and neq: "n1 \<noteq> n2"
shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
proof(rule unique_chain [OF _ dp1 dp2 neq])
from unique_RAG[OF vt]
show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
qed
text {* (* ddd *)
*}
lemma dependants_child_unique:
fixes s th th1 th2 th3
assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and dp1: "th3 \<in> dependants s th1"
and dp2: "th3 \<in> dependants s th2"
shows "th1 = th2"
proof -
{ assume neq: "th1 \<noteq> th2"
from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+"
by (simp add:s_dependants_def eq_RAG)
from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+"
by (simp add:s_dependants_def eq_RAG)
from unique_RAG_p[OF vt dp1 dp2] and neq
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
hence False
proof
assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "
from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
next
assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
qed
} thus ?thesis by auto
qed
lemma RAG_plus_elim:
assumes "vt s"
fixes x
assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
apply (unfold children_def)
by (metis assms(2) children_def RAG_children eq_RAG)
text {* (* ddd *)
*}
lemma dependants_expand:
assumes "vt s"
shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
apply(simp add: image_def)
unfolding cs_dependants_def
apply(auto)
apply (metis assms RAG_plus_elim mem_Collect_eq)
apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
lemma finite_children:
assumes "vt s"
shows "finite (children s th)"
using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
by (metis rev_finite_subset)
lemma finite_dependants:
assumes "vt s"
shows "finite (dependants (wq s) th')"
using dependants_threads[OF assms] finite_threads[OF assms]
by (metis rev_finite_subset)
abbreviation
"preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
abbreviation
"cpreceds s ths \<equiv> (cp s) ` ths"
lemma Un_compr:
"{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
by auto
lemma in_disj:
shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
by metis
lemma UN_exists:
shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
by auto
text {* (* ddd *)
This is the recursive equation used to compute the current precedence of
a thread (the @{text "th"}) here.
*}
lemma cp_rec:
fixes s th
assumes vt: "vt s"
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
proof(cases "children s th = {}")
case True
show ?thesis
unfolding cp_eq_cpreced cpreced_def
by (subst dependants_expand[OF `vt s`]) (simp add: True)
next
case False
show ?thesis (is "?LHS = ?RHS")
proof -
have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
have not_emptyness_facts[simp]:
"dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
using False dependants_expand[OF assms] by(auto simp only: Un_empty)
have finiteness_facts[simp]:
"\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
(* expanding definition *)
have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
unfolding eq_cp by (simp add: Un_compr)
(* moving Max in *)
also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
by (simp add: Max_Un)
(* expanding dependants *)
also have "\<dots> = max (Max {preced th s})
(Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
by (subst dependants_expand[OF `vt s`]) (simp)
(* moving out big Union *)
also have "\<dots> = max (Max {preced th s})
(Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"
by simp
(* moving in small union *)
also have "\<dots> = max (Max {preced th s})
(Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"
by (simp add: in_disj)
(* moving in preceds *)
also have "\<dots> = max (Max {preced th s})
(Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))"
by (simp add: UN_exists)
(* moving in Max *)
also have "\<dots> = max (Max {preced th s})
(Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))"
by (subst Max_Union) (auto simp add: image_image)
(* folding cp + moving out Max *)
also have "\<dots> = ?RHS"
unfolding eq_cp by (simp add: Max_insert)
finally show "?LHS = ?RHS" .
qed
qed
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
lemma next_th_waiting:
assumes vt: "vt s"
and 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 vt, 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 vt: "vt s"
and nxt: "next_th s th cs th'"
shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
using assms next_th_holding next_th_waiting
by (unfold s_RAG_def, simp)
-- {* 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"
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:
fixes th'
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
from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] 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"
context step_v_cps
begin
lemma rtree_RAGs: "rtree (RAG s)"
proof
show "single_valued (RAG s)"
apply (intro_locales)
by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
show "acyclic (RAG s)"
by (rule acyclic_RAG[OF vt_s])
qed
lemma rtree_RAGs': "rtree (RAG s')"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
show "acyclic (RAG s')"
by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
qed
lemmas vt_s' = step_back_vt[OF vt_s[unfolded s_def]]
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 readys_root[OF vt_s' 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 -
find_theorems ancestors
have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \<union> {Th th}"
proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
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 vt_s' 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 RTree.rtree.ancestors_accum[OF rtree_RAGs'])
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}"
proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])
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
find_theorems "_`_" "\<Union> _"
find_theorems "Max" "\<Union> _"
find_theorems wf RAG
thm wf_def
thm image_Union
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 rtree_RAGs: "rtree (RAG s)"
proof
show "single_valued (RAG s)"
apply (intro_locales)
by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
show "acyclic (RAG s)"
by (rule acyclic_RAG[OF vt_s])
qed
lemma rtree_RAGs': "rtree (RAG s')"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
show "acyclic (RAG s')"
by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
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 child_kept_left:
assumes
"(n1, n2) \<in> (child s')^+"
shows "(n1, n2) \<in> (child s)^+"
proof -
from assms show ?thesis
proof(induct rule: converse_trancl_induct)
case (base y)
from base obtain th1 cs1 th2
where h1: "(Th th1, Cs cs1) \<in> RAG s'"
and h2: "(Cs cs1, Th th2) \<in> RAG s'"
and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def)
have "cs1 \<noteq> cs"
proof
assume eq_cs: "cs1 = cs"
with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
with ee show False
by (auto simp:s_RAG_def cs_waiting_def)
qed
with h1 h2 RAG_s have
h1': "(Th th1, Cs cs1) \<in> RAG s" and
h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
thus ?case by auto
next
case (step y z)
have "(y, z) \<in> child s'" by fact
then obtain th1 cs1 th2
where h1: "(Th th1, Cs cs1) \<in> RAG s'"
and h2: "(Cs cs1, Th th2) \<in> RAG s'"
and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
have "cs1 \<noteq> cs"
proof
assume eq_cs: "cs1 = cs"
with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp
with ee show False
by (auto simp:s_RAG_def cs_waiting_def)
qed
with h1 h2 RAG_s have
h1': "(Th th1, Cs cs1) \<in> RAG s" and
h2': "(Cs cs1, Th th2) \<in> RAG s" by auto
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
with eq_y eq_z have "(y, z) \<in> child s" by simp
moreover have "(z, n2) \<in> (child s)^+" by fact
ultimately show ?case by auto
qed
qed
lemma child_kept_right:
assumes
"(n1, n2) \<in> (child s)^+"
shows "(n1, n2) \<in> (child s')^+"
proof -
from assms show ?thesis
proof(induct)
case (base y)
from base and RAG_s
have "(n1, y) \<in> child s'"
apply (auto simp:child_def)
proof -
fix th'
assume "(Th th', Cs cs) \<in> RAG s'"
with ee have "False"
by (auto simp:s_RAG_def cs_waiting_def)
thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto
qed
thus ?case by auto
next
case (step y z)
have "(y, z) \<in> child s" by fact
with RAG_s have "(y, z) \<in> child s'"
apply (auto simp:child_def)
proof -
fix th'
assume "(Th th', Cs cs) \<in> RAG s'"
with ee have "False"
by (auto simp:s_RAG_def cs_waiting_def)
thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto
qed
moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
ultimately show ?case by auto
qed
qed
lemma eq_child: "(child s)^+ = (child s')^+"
by (insert child_kept_left child_kept_right, auto)
lemma eq_cp:
fixes th'
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
apply (unfold cs_dependants_def, unfold eq_RAG)
proof -
from eq_child
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
by auto
with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"
by simp
qed
moreover {
fix th1
assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
next
assume "th1 \<in> dependants (wq s') th'"
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
qed
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
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
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 step_back_vt[OF vt_s[unfolded s_def]] 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 set_prop_split:
"A = {x. x \<in> A \<and> PP x} \<union> {x. x \<in> A \<and> \<not> PP x}"
by auto
lemma f_image_union_eq:
assumes "f ` A = g ` A"
and "f ` B = g ` B"
shows "f ` (A \<union> B) = g ` (A \<union> B)"
using assms by auto
(* ccc *)
lemma cp_gen_update_stop:
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)" sorry
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
(* ccc *)
lemma eq_child_left:
assumes nd: "(Th th, Th th') \<notin> (child s)^+"
shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
proof(induct rule:converse_trancl_induct)
case (base y)
from base obtain th1 cs1
where h1: "(Th th1, Cs cs1) \<in> RAG s"
and h2: "(Cs cs1, Th th') \<in> RAG s"
and eq_y: "y = Th th1" by (auto simp:child_def)
have "th1 \<noteq> th"
proof
assume "th1 = th"
with base eq_y have "(Th th, Th th') \<in> child s" by simp
with nd show False by auto
qed
with h1 h2 RAG_s
have h1': "(Th th1, Cs cs1) \<in> RAG s'" and
h2': "(Cs cs1, Th th') \<in> RAG s'" by auto
with eq_y show ?case by (auto simp:child_def)
next
case (step y z)
have yz: "(y, z) \<in> child s" by fact
then obtain th1 cs1 th2
where h1: "(Th th1, Cs cs1) \<in> RAG s"
and h2: "(Cs cs1, Th th2) \<in> RAG s"
and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
have "th1 \<noteq> th"
proof
assume "th1 = th"
with yz eq_y have "(Th th, z) \<in> child s" by simp
moreover have "(z, Th th') \<in> (child s)^+" by fact
ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
with nd show False by auto
qed
with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"
and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto
with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
moreover have "(z, Th th') \<in> (child s')^+" by fact
ultimately show ?case by auto
qed
lemma eq_child_right:
shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
proof(induct rule:converse_trancl_induct)
case (base y)
with RAG_s show ?case by (auto simp:child_def)
next
case (step y z)
have "(y, z) \<in> child s'" by fact
with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)
moreover have "(z, Th th') \<in> (child s)^+" by fact
ultimately show ?case by auto
qed
lemma eq_child:
assumes nd: "(Th th, Th th') \<notin> (child s)^+"
shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
by (insert eq_child_left[OF nd] eq_child_right, auto)
lemma eq_cp:
assumes nd: "th \<notin> dependants s th'"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
have nd': "(Th th, Th th') \<notin> (child s)^+"
proof
assume "(Th th, Th th') \<in> (child s)\<^sup>+"
with child_RAG_eq[OF vt_s]
have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp
with nd show False
by (simp add:s_dependants_def eq_RAG)
qed
have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"
proof(auto)
fix x assume " x \<in> dependants (wq s) th'"
thus "x \<in> dependants (wq s') th'"
apply (auto simp:cs_dependants_def eq_RAG)
proof -
assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"
with child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp
qed
next
fix x assume "x \<in> dependants (wq s') th'"
thus "x \<in> dependants (wq s) th'"
apply (auto simp:cs_dependants_def eq_RAG)
proof -
assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"
with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
with child_RAG_eq[OF vt_s]
show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp
qed
qed
moreover {
fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
lemma eq_up:
assumes dp1: "th \<in> dependants s th'"
and dp2: "th' \<in> dependants s th''"
and eq_cps: "cp s th' = cp s' th'"
shows "cp s th'' = cp s' th''"
proof -
from dp2
have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
from RAG_child[OF vt_s this[unfolded eq_RAG]]
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
moreover {
fix n th''
have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
(\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
proof(erule trancl_induct, auto)
fix y th''
assume y_ch: "(y, Th th'') \<in> child s"
and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
moreover from child_RAG_p[OF ch'] and eq_y
have "(Th th', Th thy) \<in> (RAG s)^+" by simp
ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
show "cp s th'' = cp s' th''"
apply (subst cp_rec[OF vt_s])
proof -
have "preced th'' s = preced th'' s'"
by (simp add:s_def preced_def)
moreover {
fix th1
assume th1_in: "th1 \<in> children s th''"
have "cp s th1 = cp s' th1"
proof(cases "th1 = thy")
case True
with eq_cpy show ?thesis by simp
next
case False
have neq_th1: "th1 \<noteq> th"
proof
assume eq_th1: "th1 = th"
with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
from children_no_dep[OF vt_s _ _ this] and
th1_in y_ch eq_y show False by (auto simp:children_def)
qed
have "th \<notin> dependants s th1"
proof
assume h:"th \<in> dependants s th1"
from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
from dependants_child_unique[OF vt_s _ _ h this]
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
with False show False by auto
qed
from eq_cp[OF this]
show ?thesis .
qed
}
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
moreover have "children s th'' = children s' th''"
apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
apply (fold s_def, auto simp:RAG_s)
proof -
assume "(Cs cs, Th th'') \<in> RAG s'"
with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
by (auto simp:s_dependants_def eq_RAG)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
by (auto simp:s_RAG_def)
have eq_cs: "cs1 = cs"
proof -
from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
from unique_RAG[OF vt_s this h1]
show ?thesis by simp
qed
have False
proof(rule converse_tranclE[OF h2])
assume "(Cs cs1, Th th') \<in> RAG s"
with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
from unique_RAG[OF vt_s this cs_th']
have "th' = th''" by simp
with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto
with wf_trancl[OF wf_child[OF vt_s]]
show False by auto
next
fix y
assume "(Cs cs1, y) \<in> RAG s"
and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
from unique_RAG[OF vt_s this cs_th']
have "y = Th th''" .
with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
from RAG_child[OF vt_s this]
have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
with wf_trancl[OF wf_child[OF vt_s]]
show False by auto
qed
thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
qed
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
qed
next
fix th''
assume dp': "(Th th', Th th'') \<in> child s"
show "cp s th'' = cp s' th''"
apply (subst cp_rec[OF vt_s])
proof -
have "preced th'' s = preced th'' s'"
by (simp add:s_def preced_def)
moreover {
fix th1
assume th1_in: "th1 \<in> children s th''"
have "cp s th1 = cp s' th1"
proof(cases "th1 = th'")
case True
with eq_cps show ?thesis by simp
next
case False
have neq_th1: "th1 \<noteq> th"
proof
assume eq_th1: "th1 = th"
with dp1 have "(Th th1, Th th') \<in> (RAG s)^+"
by (auto simp:s_dependants_def eq_RAG)
from children_no_dep[OF vt_s _ _ this]
th1_in dp'
show False by (auto simp:children_def)
qed
show ?thesis
proof(rule eq_cp)
show "th \<notin> dependants s th1"
proof
assume "th \<in> dependants s th1"
from dependants_child_unique[OF vt_s _ _ this dp1]
th1_in dp' have "th1 = th'"
by (auto simp:children_def)
with False show False by auto
qed
qed
qed
}
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
moreover have "children s th'' = children s' th''"
apply (unfold children_def child_def s_def RAG_set_unchanged, simp)
apply (fold s_def, auto simp:RAG_s)
proof -
assume "(Cs cs, Th th'') \<in> RAG s'"
with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto
from dp1 have "(Th th, Th th') \<in> (RAG s)^+"
by (auto simp:s_dependants_def eq_RAG)
from converse_tranclE[OF this]
obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"
and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"
by (auto simp:s_RAG_def)
have eq_cs: "cs1 = cs"
proof -
from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp
from unique_RAG[OF vt_s this h1]
show ?thesis by simp
qed
have False
proof(rule converse_tranclE[OF h2])
assume "(Cs cs1, Th th') \<in> RAG s"
with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp
from unique_RAG[OF vt_s this cs_th']
have "th' = th''" by simp
with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto
with wf_trancl[OF wf_child[OF vt_s]]
show False by auto
next
fix y
assume "(Cs cs1, y) \<in> RAG s"
and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"
with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp
from unique_RAG[OF vt_s this cs_th']
have "y = Th th''" .
with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp
from RAG_child[OF vt_s this]
have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
with wf_trancl[OF wf_child[OF vt_s]]
show False by auto
qed
thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto
qed
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
qed
qed
}
ultimately show ?thesis by auto
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"
context step_create_cps
begin
lemma eq_dep: "RAG s = RAG s'"
by (unfold s_def RAG_create_unchanged, auto)
lemma eq_cp:
fixes th'
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
have nd: "th \<notin> dependants s th'"
proof
assume "th \<in> dependants s th'"
hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
from converse_tranclE[OF this]
obtain y where "(Th th, y) \<in> RAG s'" by auto
with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
have in_th: "th \<in> threads s'" by auto
from step_back_step[OF vt_s[unfolded s_def]]
show False
proof(cases)
assume "th \<notin> threads s'"
with in_th show ?thesis by simp
qed
qed
have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
moreover {
fix th1
assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
lemma nil_dependants: "dependants s th = {}"
proof -
from step_back_step[OF vt_s[unfolded s_def]]
show ?thesis
proof(cases)
assume "th \<notin> threads s'"
from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
have hdn: " holdents s' th = {}" .
have "dependants s' th = {}"
proof -
{ assume "dependants s' th \<noteq> {}"
then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"
by (auto simp:s_dependants_def eq_RAG)
from tranclE[OF this] obtain cs' where
"(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def)
with hdn
have False by (auto simp:holdents_test)
} thus ?thesis by auto
qed
thus ?thesis
by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)
qed
qed
lemma eq_cp_th: "cp s th = preced th s"
apply (unfold cp_eq_cpreced cpreced_def)
by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)
end
locale step_exit_cps =
fixes s' th prio s
defines s_def : "s \<equiv> Exit th # s'"
assumes vt_s: "vt s"
context step_exit_cps
begin
lemma eq_dep: "RAG s = RAG s'"
by (unfold s_def RAG_exit_unchanged, auto)
lemma eq_cp:
fixes th'
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
apply (unfold cp_eq_cpreced cpreced_def)
proof -
have nd: "th \<notin> dependants s th'"
proof
assume "th \<in> dependants s th'"
hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)
with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp
from converse_tranclE[OF this]
obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"
by (auto simp:s_RAG_def)
from step_back_step[OF vt_s[unfolded s_def]]
show False
proof(cases)
assume "th \<in> runing s'"
with bk show ?thesis
apply (unfold runing_def readys_def s_waiting_def s_RAG_def)
by (auto simp:cs_waiting_def wq_def)
qed
qed
have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
moreover {
fix th1
assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
hence "preced th1 s = preced th1 s'"
proof
assume "th1 = th'"
with neq_th
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
next
assume "th1 \<in> dependants (wq s') th'"
with nd and eq_dp have "th1 \<noteq> th"
by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
qed
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
by (auto simp:image_def)
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
qed
end
end