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
begin
(* 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 {* (* ??? *)
*}
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 {* (* ??? *)
*}
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 {* (* ??? *)
*}
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 {* (* ??? *)
*}
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 {* (* ??? *)
*}
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 {* (* ??? *)
*}
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
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
locale step_set_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Set th prio#s')"
assumes vt_s: "vt s"
context step_set_cps
begin
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_dep: "RAG s = RAG s'"
by (unfold s_def RAG_set_unchanged, auto)
lemma eq_cp_pre:
fixes th'
assumes neq_th: "th' \<noteq> th"
and nd: "th \<notin> dependants s 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"
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 eq_preced[OF neq_th]
show "preced th1 s = preced th1 s'" by simp
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)
from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
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 no_dependants:
assumes "th' \<noteq> th"
shows "th \<notin> dependants s th'"
proof
assume h: "th \<in> dependants s th'"
from step_back_step [OF vt_s[unfolded s_def]]
have "step s' (Set th prio)" .
hence "th \<in> runing s'" by (cases, simp)
hence rd_th: "th \<in> readys s'"
by (simp add:readys_def runing_def)
from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
from tranclD[OF this]
obtain z where "(Th th, z) \<in> RAG s'" by auto
with rd_th show "False"
apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
by (fold wq_def, blast)
qed
(* Result improved *)
lemma eq_cp:
fixes th'
assumes neq_th: "th' \<noteq> th"
shows "cp s th' = cp s' th'"
proof(rule eq_cp_pre [OF neq_th])
from no_dependants[OF neq_th]
show "th \<notin> dependants s th'" .
qed
lemma eq_up:
fixes th' th''
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'"
proof(rule eq_preced)
show "th'' \<noteq> th"
proof
assume "th'' = th"
with dp_thy y_ch[unfolded eq_y]
have "(Th th, Th th) \<in> (RAG s)^+"
by (auto simp:child_def)
with wf_trancl[OF wf_RAG[OF vt_s]]
show False by auto
qed
qed
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_pre[OF neq_th1 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''"
by (unfold children_def child_def s_def RAG_set_unchanged, simp)
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'"
proof(rule eq_preced)
show "th'' \<noteq> th"
proof
assume "th'' = th"
with dp1 dp'
have "(Th th, Th th) \<in> (RAG s)^+"
by (auto simp:child_def s_dependants_def eq_RAG)
with wf_trancl[OF wf_RAG[OF vt_s]]
show False by auto
qed
qed
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
thus ?thesis
proof(rule eq_cp_pre)
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''"
by (unfold children_def child_def s_def RAG_set_unchanged, simp)
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
lemma eq_up_self:
fixes th' th''
assumes dp: "th \<in> dependants s th''"
and eq_cps: "cp s th = cp s' th"
shows "cp s th'' = cp s' th''"
proof -
from dp
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 child_RAG_p[OF ch'] and eq_y
have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
show "cp s th'' = cp s' th''"
apply (subst cp_rec[OF vt_s])
proof -
have "preced th'' s = preced th'' s'"
proof(rule eq_preced)
show "th'' \<noteq> th"
proof
assume "th'' = th"
with dp_thy y_ch[unfolded eq_y]
have "(Th th, Th th) \<in> (RAG s)^+"
by (auto simp:child_def)
with wf_trancl[OF wf_RAG[OF vt_s]]
show False by auto
qed
qed
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_pre[OF neq_th1 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''"
by (unfold children_def child_def s_def RAG_set_unchanged, simp)
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'"
proof(rule eq_preced)
show "th'' \<noteq> th"
proof
assume "th'' = th"
with dp dp'
have "(Th th, Th th) \<in> (RAG s)^+"
by (auto simp:child_def s_dependants_def eq_RAG)
with wf_trancl[OF wf_RAG[OF vt_s]]
show False by auto
qed
qed
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
assume neq_th1: "th1 \<noteq> th"
thus ?thesis
proof(rule eq_cp_pre)
show "th \<notin> dependants s th1"
proof
assume "th \<in> dependants s th1"
hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
from children_no_dep[OF vt_s _ _ this]
and th1_in dp' show False
by (auto simp:children_def)
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''"
by (unfold children_def child_def s_def RAG_set_unchanged, simp)
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
lemma next_waiting:
assumes vt: "vt s"
and nxt: "next_th s th cs th'"
shows "waiting s th' cs"
proof -
from assms show ?thesis
apply (auto simp:next_th_def s_waiting_def[folded wq_def])
proof -
fix rest
assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
and eq_wq: "wq s cs = th # rest"
and ne: "rest \<noteq> []"
have "set (SOME q. distinct q \<and> set q = set rest) = 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
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
with ni
have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)"
by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from wq_distinct[OF vt, of cs] eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
qed
ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
next
fix rest
assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
and ne: "rest \<noteq> []"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
from wq_distinct[OF vt, of cs] eq_wq
show "distinct rest \<and> set rest = set rest" by auto
next
from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
qed
hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
by auto
moreover have "set (SOME q. distinct q \<and> set q = set rest) = 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
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
qed
ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
with eq_wq and wq_distinct[OF vt, of cs]
show False by auto
qed
qed
locale step_v_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (V th cs#s')"
assumes vt_s: "vt s"
locale step_v_cps_nt = step_v_cps +
fixes th'
assumes nt: "next_th s' th cs th'"
context step_v_cps_nt
begin
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 dependants_kept:
fixes th''
assumes neq1: "th'' \<noteq> th"
and neq2: "th'' \<noteq> th'"
shows "dependants (wq s) th'' = dependants (wq s') th''"
proof(auto)
fix x
assume "x \<in> dependants (wq s) th''"
hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
by (auto simp:cs_dependants_def eq_RAG)
{ fix n
have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s')^+"
proof(induct rule:converse_trancl_induct)
fix y
assume "(y, Th th'') \<in> RAG s"
with RAG_s neq1 neq2
have "(y, Th th'') \<in> RAG s'" by auto
thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
next
fix y z
assume yz: "(y, z) \<in> RAG s"
and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+"
and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+"
have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
proof
show "y \<noteq> Cs cs"
proof
assume eq_y: "y = Cs cs"
with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp
from RAG_s
have cst': "(Cs cs, Th th') \<in> RAG s" by simp
from unique_RAG[OF vt_s this dp_yz]
have eq_z: "z = Th th'" by simp
with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp
from converse_tranclE[OF this]
obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s"
by (auto simp:s_RAG_def)
with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto
from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG s)^+" by auto
moreover have "cs' = cs"
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> RAG s'"
by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
show ?thesis by simp
qed
ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp
moreover note wf_trancl[OF wf_RAG[OF vt_s]]
ultimately show False by auto
qed
next
show "y \<noteq> Th th'"
proof
assume eq_y: "y = Th th'"
with yz have dps: "(Th th', z) \<in> RAG s" by simp
with RAG_s have dps': "(Th th', z) \<in> RAG s'" by auto
have "z = Cs cs"
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> RAG s'"
by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
show ?thesis .
qed
with dps RAG_s show False by auto
qed
qed
with RAG_s yz have "(y, z) \<in> RAG s'" by auto
with ztp'
show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto
qed
}
from this[OF dp]
show "x \<in> dependants (wq s') th''"
by (auto simp:cs_dependants_def eq_RAG)
next
fix x
assume "x \<in> dependants (wq s') th''"
hence dp: "(Th x, Th th'') \<in> (RAG s')^+"
by (auto simp:cs_dependants_def eq_RAG)
{ fix n
have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow> (n, Th th'') \<in> (RAG s)^+"
proof(induct rule:converse_trancl_induct)
fix y
assume "(y, Th th'') \<in> RAG s'"
with RAG_s neq1 neq2
have "(y, Th th'') \<in> RAG s" by auto
thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
next
fix y z
assume yz: "(y, z) \<in> RAG s'"
and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+"
and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+"
have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
proof
show "y \<noteq> Cs cs"
proof
assume eq_y: "y = Cs cs"
with yz have dp_yz: "(Cs cs, z) \<in> RAG s'" by simp
from this have eq_z: "z = Th th"
proof -
from step_back_step[OF vt_s[unfolded s_def]]
have "(Cs cs, Th th) \<in> RAG s'"
by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
show ?thesis by simp
qed
from converse_tranclE[OF ztp]
obtain u where "(z, u) \<in> RAG s'" by auto
moreover
from step_back_step[OF vt_s[unfolded s_def]]
have "th \<in> readys s'" by (cases, simp add:runing_def)
moreover note eq_z
ultimately show False
by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
qed
next
show "y \<noteq> Th th'"
proof
assume eq_y: "y = Th th'"
with yz have dps: "(Th th', z) \<in> RAG s'" by simp
have "z = Cs cs"
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> RAG s'"
by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
show ?thesis .
qed
with ztp have cs_i: "(Cs cs, Th th'') \<in> (RAG s')\<^sup>+" by simp
from step_back_step[OF vt_s[unfolded s_def]]
have cs_th: "(Cs cs, Th th) \<in> RAG s'"
by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)
have "(Cs cs, Th th'') \<notin> RAG s'"
proof
assume "(Cs cs, Th th'') \<in> RAG s'"
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
and neq1 show "False" by simp
qed
with converse_tranclE[OF cs_i]
obtain u where cu: "(Cs cs, u) \<in> RAG s'"
and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto
have "u = Th th"
proof -
from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
show ?thesis .
qed
with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp
from converse_tranclE[OF this]
obtain v where "(Th th, v) \<in> (RAG s')" by auto
moreover from step_back_step[OF vt_s[unfolded s_def]]
have "th \<in> readys s'" by (cases, simp add:runing_def)
ultimately show False
by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
qed
qed
with RAG_s yz have "(y, z) \<in> RAG s" by auto
with ztp'
show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto
qed
}
from this[OF dp]
show "x \<in> dependants (wq s) th''"
by (auto simp:cs_dependants_def eq_RAG)
qed
lemma cp_kept:
fixes th''
assumes neq1: "th'' \<noteq> th"
and neq2: "th'' \<noteq> th'"
shows "cp s th'' = cp s' th''"
proof -
from dependants_kept[OF neq1 neq2]
have "dependants (wq s) th'' = dependants (wq s') th''" .
moreover {
fix th1
assume "th1 \<in> dependants (wq s) th''"
have "preced th1 s = preced th1 s'"
by (unfold s_def, auto simp:preced_def)
}
moreover have "preced th'' s = preced th'' s'"
by (unfold s_def, auto simp: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 ?thesis
by (unfold cp_eq_cpreced cpreced_def, simp)
qed
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 nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"
proof
assume "(Th th1, Cs cs) \<in> RAG s'"
thus "False"
apply (auto simp:s_RAG_def cs_waiting_def)
proof -
assume h1: "th1 \<in> set (wq s' cs)"
and h2: "th1 \<noteq> hd (wq s' cs)"
from step_back_step[OF vt_s[unfolded s_def]]
show "False"
proof(cases)
assume "holding s' th cs"
then obtain rest where
eq_wq: "wq s' cs = th#rest"
apply (unfold s_holding_def wq_def[symmetric])
by (case_tac "(wq s' cs)", auto)
with h1 h2 have ne: "rest \<noteq> []" by auto
with eq_wq
have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
with nnt show ?thesis by auto
qed
qed
qed
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 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 cs1) \<in> RAG s'" by simp
with nw_cs eq_cs 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
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 cs1) \<in> RAG s'" by simp
with nw_cs eq_cs 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
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'"
by (auto simp:child_def)
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'"
by (auto simp:child_def)
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 simp
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
locale step_P_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (P th cs#s')"
assumes vt_s: "vt s"
locale step_P_cps_ne =step_P_cps +
assumes ne: "wq s' cs \<noteq> []"
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
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 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:
fixes th'
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:
fixes th' th''
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