theory Implementation
imports PIPBasics
begin
text {*
This file contains lemmas used to guide the recalculation of current
precedence after every step of execution (or system operation, or event),
which is the most tricky part in the implementation of PIP.
Following convention, lemmas are grouped into locales corresponding to
system operations, each explained in a separate section. *}
text {*
The following two lemmas are general about any valid system state,
but are used in the derivation in more specific system operations.
*}
context valid_trace
begin
lemma readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
unfolding root_def ancestors_def
using readys_RAG assms
by (metis Collect_empty_eq Domain.DomainI trancl_domain)
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
end
section {* The @{term Set} operation *}
context valid_trace_set
begin
text {* (* ddd *)
The following two lemmas confirm that @{text "Set"}-operation
only changes the precedence of the initiating thread (or actor)
of the operation (or event).
*}
lemma eq_preced:
assumes "th' \<noteq> th"
shows "preced th' (e#s) = preced th' s"
proof -
from assms show ?thesis
by (unfold is_set, auto simp:preced_def)
qed
lemma eq_the_preced:
assumes "th' \<noteq> th"
shows "the_preced (e#s) th' = the_preced s th'"
using assms
by (unfold the_preced_def, intro eq_preced, simp)
text {* (* ddd *)
Th following lemma @{text "eq_cp_pre"} says that 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:
assumes nd: "Th th \<notin> subtree (RAG s) (Th th')"
shows "cp (e#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 (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#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 RAG_es 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 (e#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 -
from readys_in_no_subtree[OF th_ready_s 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:
assumes "th' \<noteq> th"
shows "cp (e#s) th' = cp s th'"
by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])
end
section {* The @{term V} operation *}
text {*
The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
*}
context valid_trace_v
begin
lemma ancestors_th: "ancestors (RAG s) (Th th) = {}"
proof -
from readys_root[OF th_ready_s]
show ?thesis
by (unfold root_def, simp)
qed
lemma edge_of_th:
"(Cs cs, Th th) \<in> RAG s"
proof -
from holding_th_cs_s
show ?thesis
by (unfold s_RAG_def s_holding_abv, 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}"
by (rule forest_RAG.ancestors_accum[OF edge_of_th])
from this[unfolded ancestors_th] show ?thesis by simp
qed
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"}.
*}
lemma (in valid_trace_v)
the_preced_es: "the_preced (e#s) = the_preced s"
proof
fix th'
show "the_preced (e # s) th' = the_preced s th'"
by (unfold the_preced_def preced_def is_v, simp)
qed
context valid_trace_v_n
begin
lemma sub_RAGs':
"{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s"
using waiting_taker holding_th_cs_s
by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto)
lemma ancestors_th':
"ancestors (RAG s) (Th taker) = {Th th, Cs cs}"
proof -
have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
proof(rule forest_RAG.ancestors_accum)
from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
qed
thus ?thesis using ancestors_th ancestors_cs by auto
qed
lemma RAG_s:
"RAG (e#s) = (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) \<union>
{(Cs cs, Th taker)}"
by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
lemma subtree_kept: (* ddd *)
assumes "th1 \<notin> {th, taker}"
shows "subtree (RAG (e#s)) (Th th1) =
subtree (RAG s) (Th th1)" (is "_ = ?R")
proof -
let ?RAG' = "(RAG s - {(Cs cs, Th th), (Th taker, Cs cs)})"
let ?RAG'' = "?RAG' \<union> {(Cs cs, Th taker)}"
have "subtree ?RAG' (Th th1) = ?R"
proof(rule subset_del_subtree_outside)
show "Range {(Cs cs, Th th), (Th taker, 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 taker \<notin> subtree (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th th1)"
proof(rule subtree_refute)
show "Th th1 \<notin> ancestors (RAG s - {(Cs cs, Th th), (Th taker, Cs cs)}) (Th taker)"
(is "_ \<notin> ?R")
proof -
have "?R \<subseteq> ancestors (RAG s) (Th taker)" 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 taker" by simp
qed
qed
ultimately show ?thesis by (unfold RAG_s, simp)
qed
lemma cp_kept:
assumes "th1 \<notin> {th, taker}"
shows "cp (e#s) th1 = cp s th1"
by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
end
context valid_trace_v_e
begin
lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"
by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
lemma subtree_kept:
assumes "th1 \<noteq> th"
shows "subtree (RAG (e#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 (e#s) th1 = cp s th1"
by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}"
(is "?L = ?R")
proof -
{ fix n
assume "n \<in> ?L"
hence "n \<in> ?R"
proof(cases rule:subtreeE)
case 2
from this(2) have "(n, Cs cs) \<in> (RAG s)^+"
by (auto simp:ancestors_def)
from tranclD2[OF this]
obtain th' where "waiting s th' cs"
by (auto simp:s_RAG_def s_waiting_abv)
with no_waiter_before
show ?thesis by simp
qed simp
} moreover {
fix n
assume "n \<in> ?R"
hence "n \<in> ?L" by (auto simp:subtree_def)
} ultimately show ?thesis by auto
qed
lemma subtree_th:
"subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
proof(unfold RAG_s, fold subtree_cs, rule forest_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 (e#s) th = cp s th"
by (unfold cp_alt_def subtree_th the_preced_es, auto)
lemma eq_cp:
shows "cp (e#s) th' = cp s th'"
using cp_kept_1 cp_kept_2
by (cases "th' = th", auto)
end
section {* The @{term P} operation *}
context valid_trace_p
begin
lemma root_th: "root (RAG s) (Th th)"
by (simp add: ready_th_s readys_root)
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 (e#s) = the_preced s"
proof
fix th'
show "the_preced (e # s) th' = the_preced s th'"
by (unfold the_preced_def is_p preced_def, simp)
qed
end
context valid_trace_p_h
begin
lemma subtree_kept:
assumes "th' \<noteq> th"
shows "subtree (RAG (e#s)) (Th th') = subtree (RAG s) (Th th')"
proof(unfold RAG_es, 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 (e#s) th' = cp s th'"
proof -
have "(the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#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 valid_trace_p_w
begin
lemma cs_held: "(Cs cs, Th holder) \<in> RAG s"
using holding_s_holder
by (unfold s_RAG_def, fold s_holding_abv, auto)
lemma tRAG_s:
"tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"
using RAG_tRAG_transfer[OF RAG_es cs_held] .
lemma cp_kept:
assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"
shows "cp (e#s) th'' = cp s th''"
proof -
have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"
proof -
have "Th holder \<notin> subtree (tRAG s) (Th th'')"
proof
assume "Th holder \<in> subtree (tRAG s) (Th th'')"
thus False
proof(rule subtreeE)
assume "Th holder = Th th''"
from assms[unfolded tRAG_s ancestors_def, folded this]
show ?thesis by auto
next
assume "Th th'' \<in> ancestors (tRAG s) (Th holder)"
moreover have "... \<subseteq> ancestors (tRAG (e#s)) (Th holder)"
proof(rule ancestors_mono)
show "tRAG s \<subseteq> tRAG (e#s)" by (unfold tRAG_s, auto)
qed
ultimately have "Th th'' \<in> ancestors (tRAG (e#s)) (Th holder)" by auto
moreover have "Th holder \<in> ancestors (tRAG (e#s)) (Th th)"
by (unfold tRAG_s, auto simp:ancestors_def)
ultimately have "Th th'' \<in> ancestors (tRAG (e#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 holder)}) (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 (e#s)) (Th th)"
and "cp_gen (e#s) u = cp_gen s u"
and "y \<in> ancestors (tRAG (e#s)) u"
shows "cp_gen (e#s) y = cp_gen s y"
using assms(3)
proof(induct rule:wf_induct[OF vat_es.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_es.cp_gen_rec[OF this]
have "?L =
Max ({the_preced (e#s) th2} \<union> cp_gen (e#s) ` RTree.children (tRAG (e#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 (e#s) th2 = the_preced s th2" by simp
moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
cp_gen s ` RTree.children (tRAG s) x"
proof -
have "RTree.children (tRAG (e#s)) x = RTree.children (tRAG s) x"
proof(unfold tRAG_s, rule children_union_kept)
have start: "(Th th, Th holder) \<in> tRAG (e#s)"
by (unfold tRAG_s, auto)
note x_u = 1(2)
show "x \<notin> Range {(Th th, Th holder)}"
proof
assume "x \<in> Range {(Th th, Th holder)}"
hence eq_x: "x = Th holder" using RangeE by auto
show False
proof(cases rule:vat_es.ancestors_headE[OF assms(1) start])
case 1
from x_u[folded this, unfolded eq_x] vat_es.acyclic_tRAG
show ?thesis by (auto simp:ancestors_def acyclic_def)
next
case 2
with x_u[unfolded eq_x]
have "(Th holder, Th holder) \<in> (tRAG (e#s))^+" by (auto simp:ancestors_def)
with vat_es.acyclic_tRAG show ?thesis by (auto simp:acyclic_def)
qed
qed
qed
moreover have "cp_gen (e#s) ` RTree.children (tRAG (e#s)) x =
cp_gen s ` RTree.children (tRAG (e#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_es.forest_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 (e#s)) (Th th)"
proof
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
have "a = u"
proof(rule vat_es.forest_s.ancestors_children_unique)
from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
RTree.children (tRAG (e#s)) x" by auto
next
from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
RTree.children (tRAG (e#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 (e#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 (e#s)) u" "z \<in> RTree.children (tRAG (e#s)) x" by auto
show ?thesis
proof(cases "a = z")
case True
from h(2) have zx_in: "(z, x) \<in> (tRAG (e#s))" by (auto simp:RTree.children_def)
from 1(1)[rule_format, OF this h(1)]
have eq_cp_gen: "cp_gen (e#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 (e#s)) (Th th)"
proof
assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
have "a = z"
proof(rule vat_es.forest_s.ancestors_children_unique)
from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
by (auto simp:ancestors_def)
with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter>
RTree.children (tRAG (e#s)) x" by auto
next
from a_in a_in'
show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> RTree.children (tRAG (e#s)) x"
by auto
qed
with False show False by auto
qed
from cp_kept[OF this[unfolded eq_a]]
have "cp (e#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 cp_gen_rec[OF eq_x], simp)
finally show ?thesis .
qed
qed
lemma cp_up:
assumes "(Th th') \<in> ancestors (tRAG (e#s)) (Th th)"
and "cp (e#s) th' = cp s th'"
and "(Th th'') \<in> ancestors (tRAG (e#s)) (Th th')"
shows "cp (e#s) th'' = cp s th''"
proof -
have "cp_gen (e#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 (e#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
section {* The @{term Create} operation *}
context valid_trace_create
begin
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
by (unfold tRAG_alt_def RAG_es, auto)
lemma preced_kept:
assumes "th' \<noteq> th"
shows "the_preced (e#s) th' = the_preced s th'"
by (unfold the_preced_def preced_def is_create, insert assms, auto)
lemma th_not_in: "Th th \<notin> Field (tRAG s)"
by (meson not_in_thread_isolated subsetCE tRAG_Field th_not_live_s)
lemma eq_cp:
assumes neq_th: "th' \<noteq> th"
shows "cp (e#s) th' = cp s th'"
proof -
have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#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 (e#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 (e#s)) (Th th) = {}"
proof -
{ fix a
assume "a \<in> RTree.children (tRAG (e#s)) (Th th)"
hence "(a, Th th) \<in> tRAG (e#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 (e#s) th = preced th (e#s)"
by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def)
end
context valid_trace_exit
begin
lemma preced_kept:
assumes "th' \<noteq> th"
shows "the_preced (e#s) th' = the_preced s th'"
using assms
by (unfold the_preced_def is_exit preced_def, simp)
lemma tRAG_kept: "tRAG (e#s) = tRAG s"
by (unfold tRAG_alt_def RAG_es, auto)
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 s th cs"
by (simp add: holdents_RAG holdents_th_s)
then show False by (unfold s_holding_abv, auto)
qed
moreover have "Th th \<notin> Domain (RAG s)"
proof
assume "Th th \<in> Domain (RAG s)"
then obtain cs where "waiting s th cs"
by (simp add: readys_RAG)
then show False
using RAG_es \<open>Th th \<in> Domain (RAG s)\<close>
th_not_live_es valid_trace.dm_RAG_threads vat_es.valid_trace_axioms by blast
qed
ultimately show ?thesis by (auto simp:Field_def)
qed
lemma th_tRAG: "(Th th) \<notin> Field (tRAG s)"
using th_RAG tRAG_Field by auto
lemma eq_cp:
assumes neq_th: "th' \<noteq> th"
shows "cp (e#s) th' = cp s th'"
proof -
have "(the_preced (e#s) \<circ> the_thread) ` subtree (tRAG (e#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 -
from readys_in_no_subtree[OF th_ready_s 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 (e#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