--- a/PIPBasics.thy Tue Jul 12 15:09:09 2016 +0100
+++ b/PIPBasics.thy Tue Aug 16 11:49:37 2016 +0100
@@ -376,6 +376,18 @@
using assms
by (auto simp: tRAG_def wRAG_def hRAG_def)
+lemma tRAG_tG:
+ assumes "(n1, n2) \<in> tRAG s"
+ shows "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "(the_thread n1, the_thread n2) \<in> tG s"
+ using assms
+ by (unfold tRAG_def_tG tG_alt_def, auto)
+
+lemma tG_tRAG:
+ assumes "(th1, th2) \<in> tG s"
+ shows "(Th th1, Th th2) \<in> tRAG s"
+ using assms
+ by (unfold tRAG_def_tG, auto)
+
lemma tRAG_ancestorsE:
assumes "x \<in> ancestors (tRAG s) u"
obtains th where "x = Th th"
@@ -388,6 +400,168 @@
from that[OF this] show ?thesis .
qed
+lemma map_prod_RE:
+ assumes "(u, v) \<in> (map_prod f f ` R)"
+ obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R"
+ using assms
+ by auto
+
+lemma map_prod_tranclE:
+ assumes "(u, v) \<in> (map_prod f f ` R)^+"
+ and "inj_on f (Field R)"
+ obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^+"
+proof -
+ from assms(1)
+ have "\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>+"
+ proof(induct rule:trancl_induct)
+ case (base y)
+ thus ?case by auto
+ next
+ case (step y z)
+ then obtain u' v' where h1: "u = f u'" "y = f v'" "(u', v') \<in> R\<^sup>+" by auto
+ from map_prod_RE[OF step(2)] obtain v'' u''
+ where h2: "y = f v''" "z = f u''" "(v'', u'') \<in> R" by auto
+ from h1 h2 have "f v' = f v''" by simp
+ hence eq_v': "v' = v''"
+ proof(cases rule:inj_onD[OF assms(2), consumes 1])
+ case 1
+ from h1(3) show ?case using trancl_subset_Field2[of R] by auto
+ next
+ case 2
+ from h2(3) show ?case by (simp add: Domain.DomainI Field_def)
+ qed
+ let ?u = "u'" and ?v = "u''"
+ have "(?u, ?v) \<in> R^+" using h1(3)[unfolded eq_v'] h2(3) by auto
+ with h1 h2
+ show ?case by auto
+ qed
+ thus ?thesis using that by metis
+qed
+
+lemma map_prod_rtranclE:
+ assumes "(u, v) \<in> (map_prod f f ` R)^*"
+ and "inj_on f (Field R)"
+ obtains (root) "u = v"
+ | (trancl) u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^*"
+proof -
+ from rtranclD[OF assms(1)]
+ have "u = v \<or> (\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>*)"
+ proof
+ assume "u = v" thus ?thesis by auto
+ next
+ assume "u \<noteq> v \<and> (u, v) \<in> (map_prod f f ` R)\<^sup>+"
+ hence "(u, v) \<in> (map_prod f f ` R)\<^sup>+" by auto
+ thus ?thesis
+ by (rule map_prod_tranclE[OF _ assms(2)], auto dest!:trancl_into_rtrancl)
+ qed
+ with that show ?thesis by auto
+qed
+
+lemma Field_tRAGE:
+ assumes "n \<in> (Field (tRAG s))"
+ obtains th where "n = Th th"
+proof -
+ from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def]
+ show ?thesis using that by auto
+qed
+
+lemma trancl_tG_tRAG:
+ assumes "(th1, th2) \<in> (tG s)^+"
+ shows "(Th th1, Th th2) \<in> (tRAG s)^+"
+proof -
+ have "inj_on the_thread (Field (tRAG s))"
+ by (unfold inj_on_def Field_def tRAG_alt_def, auto)
+ from map_prod_tranclE[OF assms[unfolded tG_def] this]
+ obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"
+ by auto
+ hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)
+ from this[unfolded trancl_domain trancl_range]
+ have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)"
+ by (unfold Field_def, auto)
+ then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"
+ by (auto elim!:Field_tRAGE)
+ with h have "th1' = th1" "th2' = th2" by (auto)
+ from h(3)[unfolded h' this]
+ show ?thesis by (auto simp:ancestors_def)
+qed
+
+lemma rtrancl_tG_tRAG:
+ assumes "(th1, th2) \<in> (tG s)^*"
+ shows "(Th th1, Th th2) \<in> (tRAG s)^*"
+proof -
+ from rtranclD[OF assms]
+ show ?thesis
+ proof
+ assume "th1 = th2" thus "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" by auto
+ next
+ assume "th1 \<noteq> th2 \<and> (th1, th2) \<in> (tG s)\<^sup>+"
+ hence "(th1, th2) \<in> (tG s)\<^sup>+" by auto
+ from trancl_into_rtrancl[OF trancl_tG_tRAG[OF this]]
+ show "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" .
+ qed
+qed
+
+lemma trancl_tRAG_tG:
+ assumes "(n1, n2) \<in> (tRAG s)^+"
+ obtains "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)"
+ "(the_thread n1, the_thread n2) \<in> (tG s)^+"
+proof -
+ have inj: "inj_on Th (Field (tG s))"
+ by (unfold inj_on_def Field_def, auto)
+ show ?thesis
+ by (rule map_prod_tranclE[OF assms[unfolded tRAG_def_tG] inj], auto intro!:that)
+qed
+
+lemma rtrancl_tRAG_tG:
+ assumes "(n1, n2) \<in> (tRAG s)^*"
+ obtains "n1 = n2"
+ | "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "the_thread n1 \<noteq> the_thread n2"
+ "(the_thread n1, the_thread n2) \<in> (tG s)^*"
+proof -
+ from rtranclD[OF assms]
+ have "n1 = n2 \<or>
+ n1 = Th (the_thread n1) \<and> n2 = Th (the_thread n2) \<and> the_thread n1 \<noteq> the_thread n2 \<and>
+ (the_thread n1, the_thread n2) \<in> (tG s)^*"
+ proof
+ assume h: "n1 \<noteq> n2 \<and> (n1, n2) \<in> (tRAG s)\<^sup>+"
+ hence "(n1, n2) \<in> (tRAG s)\<^sup>+" by auto
+ from trancl_tRAG_tG[OF this]
+ have "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)"
+ "(the_thread n1, the_thread n2) \<in> (tG s)\<^sup>+" by auto
+ with h
+ show ?thesis by auto
+ qed auto
+ with that show ?thesis by auto
+qed
+
+lemma ancestors_imageE:
+ assumes "u \<in> ancestors ((map_prod f f) ` R) v"
+ and "inj_on f (Field R)"
+ obtains u' v' where "u = (f u')" "v = (f v')" "u' \<in> ancestors R v'"
+ using assms unfolding ancestors_def
+ by (metis map_prod_tranclE mem_Collect_eq)
+
+lemma tRAG_ancestorsE_tG:
+ assumes "x \<in> ancestors (tRAG s) u"
+ obtains "x = Th (the_thread x)" "u = Th (the_thread u)"
+ "the_thread x \<in> ancestors (tG s) (the_thread u)"
+proof -
+ from assms[unfolded ancestors_def]
+ have "(u, x) \<in> (tRAG s)\<^sup>+" by simp
+ from trancl_tRAG_tG[OF this]
+ show ?thesis using that by (auto simp:ancestors_def)
+qed
+
+lemma ancestors_tG_tRAG:
+ assumes "th1 \<in> ancestors (tG s) th2"
+ shows "Th th1 \<in> ancestors (tRAG s) (Th th2)"
+proof -
+ from assms[unfolded ancestors_def]
+ have "(th2, th1) \<in> (tG s)\<^sup>+" by simp
+ from trancl_tG_tRAG[OF this]
+ show ?thesis by (simp add:ancestors_def)
+qed
+
lemma subtree_nodeE:
assumes "n \<in> subtree (tRAG s) (Th th)"
obtains th1 where "n = Th th1"
@@ -411,6 +585,43 @@
qed
qed
+lemma subtree_nodeE_tG:
+ assumes "n \<in> subtree (tRAG s) (Th th)"
+ obtains "n = Th (the_thread n)" "the_thread n \<in> subtree (tG s) th"
+proof -
+ from assms[unfolded subtree_def]
+ have "(n, Th th) \<in> (tRAG s)\<^sup>*" by simp
+ hence "n = Th (the_thread n) \<and> the_thread n \<in> subtree (tG s) th"
+ by (cases rule:rtrancl_tRAG_tG, auto simp:subtree_def)
+ thus ?thesis using that by auto
+qed
+
+lemma subtree_tRAG_tG:
+ "subtree (tRAG s) (Th th) = Th ` (subtree (tG s) th)" (is "?L = ?R")
+proof -
+ { fix n
+ assume "n \<in> ?L"
+ from subtree_nodeE_tG[OF this]
+ have "n \<in> ?R" by auto
+ } moreover {
+ fix n
+ assume "n \<in> ?R"
+ then obtain th' where h: "th' \<in> subtree (tG s) th" "n = Th th'" by auto
+ hence "(th', th) \<in> (tG s)^*" by (auto simp:subtree_def)
+ from rtrancl_tG_tRAG[OF this] and h
+ have "n \<in> ?L" by (auto simp:subtree_def)
+ } ultimately show ?thesis by auto
+qed
+
+lemma subtree_tG_tRAG:
+ "(subtree (tG s) th) = the_thread ` (subtree (tRAG s) (Th th))" (is "?L = ?R")
+proof -
+ have "?R = (the_thread \<circ> Th) ` subtree (tG s) th"
+ by (unfold subtree_tRAG_tG image_comp, simp)
+ also have "... = id ` ?L" by (rule image_cong, auto)
+ finally show ?thesis by simp
+qed
+
text {*
The following lemmas relate @{term tRAG} with
@{term RAG} from different perspectives.
@@ -511,12 +722,6 @@
} ultimately show ?thesis by blast
qed
-(*
-lemma image_eq:
- assumes "A = B"
- shows "f ` A = f ` B"
- using assms by auto
-*)
lemma tRAG_trancl_eq_Th:
"{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} =
@@ -533,6 +738,7 @@
using assms
by (unfold tRAG_alt_def, auto)
+
lemma tRAG_subtree_eq:
"(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}"
(is "?L = ?R")
@@ -600,6 +806,14 @@
thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
qed
+text {*
+ The following is another definition of @{term cp} based on @{term tG}:
+*}
+lemma cp_alt_def2:
+ "cp s th = Max (the_preced s ` (subtree (tG s) th))"
+ by (unfold cp_alt_def1 subtree_tG_tRAG image_comp, simp)
+
+
lemma RAG_tRAG_transfer:
assumes "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
and "(Cs cs, Th th'') \<in> RAG s"
@@ -676,6 +890,36 @@
"dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
using dependants_alt_def tRAG_trancl_eq by auto
+text {*
+ Another definition of dependants based on @{term tG}:
+*}
+lemma dependants_alt_tG:
+ "dependants s th = {th'. (th', th) \<in> (tG s)^+}" (is "?L = ?R")
+proof -
+ have "?L = {th'. (Th th', Th th) \<in> (tRAG s)\<^sup>+}"
+ by (unfold dependants_alt_def, simp)
+ also have "... = ?R" (is "?LL = ?RR")
+ proof -
+ { fix th'
+ assume "th' \<in> ?LL"
+ hence "(Th th', Th th) \<in> (tRAG s)\<^sup>+" by simp
+ from trancl_tRAG_tG[OF this]
+ have "th' \<in> ?RR" by auto
+ } moreover {
+ fix th'
+ assume "th' \<in> ?RR"
+ hence "(th', th) \<in> (tG s)\<^sup>+" by simp
+ from trancl_tG_tRAG[OF this]
+ have "th' \<in> ?LL" by auto
+ } ultimately show ?thesis by auto
+ qed
+ finally show ?thesis .
+qed
+
+lemma dependants_alt_def_tG_ancestors:
+ "dependants s th = {th'. th \<in> ancestors (tG s) th'}"
+ by (unfold dependants_alt_tG ancestors_def, simp)
+
section {* Locales used to investigate the execution of PIP *}
text {*
@@ -1395,6 +1639,15 @@
then show ?thesis using wq_threads by simp
qed
+lemma dm_tG_threads:
+ assumes "th \<in> Domain (tG s)"
+ shows "th \<in> threads s"
+proof -
+ from assms[unfolded tG_alt_def]
+ have "(Th th) \<in> Domain (RAG s)" by (unfold Domain_def, auto)
+ from dm_RAG_threads[OF this] show ?thesis .
+qed
+
lemma rg_RAG_threads:
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
@@ -1404,17 +1657,38 @@
apply(auto)
using s_holding_def wq_def wq_threads by auto
+lemma rg_tG_threads:
+ assumes "th \<in> Range (tG s)"
+ shows "th \<in> threads s"
+proof -
+ from assms[unfolded tG_alt_def]
+ have "(Th th) \<in> Range (RAG s)" by (unfold Range_def, auto)
+ from rg_RAG_threads[OF this] show ?thesis .
+qed
+
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
shows "th \<in> threads s"
using assms
by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
+lemma tG_threads:
+ assumes "th \<in> Field (tG s)"
+ shows "th \<in> threads s"
+ using assms
+ by (metis Field_def UnE dm_tG_threads rg_tG_threads)
+
lemma not_in_thread_isolated:
assumes "th \<notin> threads s"
shows "(Th th) \<notin> Field (RAG s)"
using RAG_threads assms by auto
+lemma not_in_thread_isolated_tG:
+ assumes "th \<notin> threads s"
+ shows "th \<notin> Field (tG s)"
+ using assms
+ using tG_threads by auto
+
text {*
As a corollary, this lemma shows that @{term tRAG}
is also covered by the @{term threads}-set.
@@ -1443,6 +1717,17 @@
finally show ?thesis .
qed
+lemma subtree_tG_thread:
+ assumes "th \<in> threads s"
+ shows "subtree (tG s) th \<subseteq> threads s" (is "?L \<subseteq> ?R")
+proof -
+ from subtree_tRAG_thread[OF assms]
+ have "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" .
+ from this[unfolded subtree_tRAG_tG]
+ have " Th ` subtree (tG s) th \<subseteq> Th ` threads s" .
+ thus ?thesis by auto
+qed
+
end
section {* The formation of @{term RAG} *}
@@ -2316,6 +2601,18 @@
show ?thesis using Cons by simp
qed
qed
+
+lemma finite_tRAG: "finite (tRAG s)"
+proof -
+ from finite_RAG[unfolded RAG_split]
+ have "finite (wRAG s)" "finite (hRAG s)" by auto
+ from finite_relcomp[OF this] tRAG_def
+ show ?thesis by simp
+qed
+
+lemma finite_tG: "finite (tG s)"
+ by (unfold tG_def, insert finite_tRAG, auto)
+
end
subsection {* Uniqueness of waiting *}
@@ -2867,6 +3164,20 @@
show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
qed
+lemma rel_map_alt_def: "rel_map f R = map_prod f f ` R"
+ by (unfold rel_map_def pairself_def map_prod_def, auto)
+
+lemma acyclic_tG: "acyclic (tG s)"
+proof -
+ have "acyclic (rel_map the_thread (tRAG s))"
+ proof(rule rel_map_acyclic [OF acyclic_tRAG])
+ show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))"
+ by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto)
+ qed
+ thus ?thesis
+ by (unfold tG_def, fold rel_map_alt_def, simp)
+qed
+
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
@@ -2879,6 +3190,17 @@
by (unfold tRAG_def, rule single_valued_relcomp,
insert sgv_wRAG sgv_hRAG, auto)
+lemma sgv_tG: "single_valued (tG s)"
+proof -
+ { fix x y z
+ assume h: "(x, y) \<in> tG s" "(x, z) \<in> tG s"
+ from tG_tRAG[OF h(1)] tG_tRAG[OF h(2)]
+ have "(Th x, Th y) \<in> tRAG s" "(Th x, Th z) \<in> tRAG s" by auto
+ from sgv_tRAG[unfolded single_valued_def, rule_format, OF this]
+ have "y = z" by simp
+ } thus ?thesis by (unfold single_valued_def, auto)
+qed
+
end
text {*
@@ -2893,6 +3215,76 @@
from acyclic_tRAG show "acyclic (tRAG s)" .
qed
+sublocale valid_trace < forest_s_tG?: forest "tG s"
+proof(unfold_locales)
+ from sgv_tG show "single_valued (tG s)" .
+next
+ from acyclic_tG show "acyclic (tG s)" .
+qed
+
+context valid_trace
+begin
+
+lemma wf_tRAG: "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
+
+lemma wf_tG: "wf (tG s)"
+proof(rule finite_acyclic_wf)
+ from finite_tG show "finite (tG s)" .
+next
+ from acyclic_tG show "acyclic (tG s)" .
+qed
+
+lemma finite_children_tRAG: "finite (children (tRAG s) x)"
+ proof(unfold tRAG_def, rule fbranch_compose1[rule_format])
+ fix x show "finite (children (wRAG s) x)"
+ proof(rule finite_fbranchI1[rule_format])
+ show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto
+ qed
+ next
+ fix x
+ show "finite (children (hRAG s) x)"
+ proof(rule finite_fbranchI1[rule_format])
+ show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto
+ qed
+ qed
+
+lemma children_map_prod:
+ assumes "inj f"
+ shows " children (map_prod f f ` r) (f x) = f ` (children r x)" (is "?L = ?R")
+proof -
+ { fix e
+ assume "e \<in> ?L"
+ then obtain e' x' where h: "e = f e'" "f x' = f x" "(e', x') \<in> r"
+ by (auto simp:children_def)
+ with assms[unfolded inj_on_def, rule_format]
+ have eq_x': "x' = x" by auto
+ with h
+ have "e \<in> ?R" by (unfold children_def, auto)
+ } moreover {
+ fix e
+ assume "e \<in> ?R"
+ hence "e \<in> ?L" by (auto simp:children_def)
+ } ultimately show ?thesis by auto
+qed
+
+lemma finite_children_tG: "finite (children (tG s) x)"
+proof -
+ have "(children (tRAG s) (Th x)) = Th ` children (tG s) x"
+ by (unfold tRAG_def_tG, subst children_map_prod, auto simp:inj_on_def)
+ from finite_children_tRAG[of "Th x", unfolded this]
+ have "finite (Th ` children (tG s) x)" .
+ from finite_imageD[OF this]
+ show ?thesis by (auto simp:inj_on_def)
+qed
+
+end
sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
proof
@@ -2921,6 +3313,15 @@
qed
qed
+sublocale valid_trace < fsbttGs?: fforest "tG s"
+proof
+ fix x
+ show "finite (children (tG s) x)"
+ by (simp add:finite_children_tG)
+next
+ show "wf (tG s)" by (simp add:wf_tG)
+qed
+
section {* Chain to readys *}
text {*
@@ -3004,6 +3405,15 @@
show ?thesis by auto
qed
+lemma th_chain_to_ready_tG:
+ assumes th_in: "th \<in> threads s"
+ shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (th, th') \<in> (tG s)^+)"
+proof -
+ from th_chain_to_ready[OF assms]
+ show ?thesis
+ using dependants_alt_def1 dependants_alt_tG by blast
+qed
+
text {*
The following lemma is a technical one to show
that the set of threads in the subtree of any thread
@@ -3026,6 +3436,75 @@
ultimately show ?thesis by auto
qed
+(* ccc *)
+
+lemma readys_no_tRAG_chain:
+ assumes "th1 \<in> readys s"
+ and "th2 \<in> readys s"
+ and "th1 \<noteq> th2"
+ shows "(Th th1, Th th2) \<notin> (tRAG s)^*"
+proof
+ assume "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*"
+ from rtranclD[OF this]
+ show False
+ proof
+ assume "Th th1 = Th th2" with assms show ?thesis by simp
+ next
+ assume "Th th1 \<noteq> Th th2 \<and> (Th th1, Th th2) \<in> (tRAG s)\<^sup>+"
+ hence "(Th th1, Th th2) \<in> (tRAG s)\<^sup>+" by auto
+ from tranclD[OF this] obtain cs where "(Th th1, Cs cs) \<in> RAG s"
+ by (unfold tRAG_alt_def, auto)
+ from in_RAG_E[OF this] have "th1 \<notin> readys s" by (unfold readys_def, auto)
+ with assms show ?thesis by simp
+ qed
+qed
+
+lemma readys_indep:
+ assumes "th1 \<in> readys s"
+ and "th2 \<in> readys s"
+ and "th1 \<noteq> th2"
+ shows "indep (tRAG s) (Th th1) (Th th2)"
+ using assms readys_no_tRAG_chain
+ unfolding indep_def by blast
+
+lemma readys_indep_tG:
+ assumes "th1 \<in> readys s"
+ and "th2 \<in> readys s"
+ and "th1 \<noteq> th2"
+ shows "indep (tG s) th1 th2"
+ using assms
+ unfolding indep_def
+ using readys_no_tRAG_chain rtrancl_tG_tRAG by blast
+
+text {*
+ The following lemma @{text "thread_chain"} holds on any living thread,
+ not necessarily a running one.
+*}
+lemma thread_chain:
+ assumes "th \<in> threads s"
+ obtains th' where "th' \<in> subtree (tG s) th" "th' \<in> threads s"
+ "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"
+proof -
+ have "Max (the_preced s ` subtree (tG s) th) \<in> the_preced s ` subtree (tG s) th"
+ proof(rule Max_in)
+ show "finite (the_preced s ` subtree (tG s) th)"
+ by (simp add: fsbttGs.finite_subtree)
+ next
+ show "the_preced s ` subtree (tG s) th \<noteq> {}" using subtree_def by fastforce
+ qed
+ then obtain th' where
+ h: "th' \<in> subtree (tG s) th"
+ "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"
+ by auto
+ moreover have "th' \<in> threads s"
+ proof -
+ from assms have "th \<in> threads s" .
+ from subtree_tG_thread[OF this] and h
+ show ?thesis by auto
+ qed
+ ultimately show ?thesis using that by auto
+qed
+
text {*
The following two lemmas shows there is at most one running thread
in the system.
@@ -3035,6 +3514,80 @@
and running_2: "th2 \<in> running s"
shows "th1 = th2"
proof -
+ -- {* According to lemma @{thm thread_chain},
+ each living threads is chained to a thread in its subtree, and this
+ target thread holds the highest precedence of the subtree.
+
+ The chains for @{term th1} and @{term th2} are established
+ first in the following in @{text "h1"} and @{text "h2"}:
+ *}
+ have "th1 \<in> threads s" using assms
+ by (unfold running_def readys_def, auto)
+ from thread_chain[OF this]
+ obtain th1' where
+ h1: "th1' \<in> subtree (tG s) th1"
+ "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
+ "th1' \<in> threads s"
+ by auto
+ have "th2 \<in> threads s" using assms
+ by (unfold running_def readys_def, auto)
+ from thread_chain[OF this]
+ obtain th2' where
+ h2: "th2' \<in> subtree (tG s) th2"
+ "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
+ "th2' \<in> threads s"
+ by auto
+ -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
+ must be equal:
+ *}
+ have eq_th': "th1' = th2'"
+ proof -
+ have "the_preced s th1' = the_preced s th2'"
+ proof -
+ from running_1 and running_2 have "cp s th1 = cp s th2"
+ unfolding running_def by auto
+ from this[unfolded cp_alt_def2]
+ have eq_max: "Max (the_preced s ` subtree (tG s) th1) =
+ Max (the_preced s ` subtree (tG s) th2)" .
+ with h1(2) h2(2)
+ show ?thesis by metis
+ qed
+ from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
+ show ?thesis .
+ qed
+ -- {* From this, it can be derived that the two sub-trees
+ rooted by @{term th1} and @{term th2} must overlap: *}
+ have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2"
+ using eq_th' h1(1) h2(1) by auto
+ -- {* However, this would be in contradiction with the fact
+ that two independent sub-trees can not overlap,
+ if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
+ Therefore, @{term th1} and @{term th2} must be equal.
+ *}
+ { assume neq: "th1 \<noteq> th2"
+ -- {* According to @{thm readys_indep_tG}, two different threads
+ in ready queue must be independent with each other: *}
+ have "indep (tG s) th1 th2"
+ by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
+ -- {* Therefore, according to lemma @{thm subtree_disjoint},
+ the two sub-trees rooted by them can not overlap:
+ *}
+ from subtree_disjoint[OF this]
+ have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
+ -- {* In contradiction with @{thm overlapping}: *}
+ with overlapping have False by auto
+ } thus ?thesis by auto
+qed
+
+text {*
+ The following two lemmas shows there is at most one running thread
+ in the system.
+*}
+lemma running_unique_old:
+ assumes running_1: "th1 \<in> running s"
+ and running_2: "th2 \<in> running s"
+ shows "th1 = th2"
+proof -
from running_1 and running_2 have "cp s th1 = cp s th2"
unfolding running_def by auto
from this[unfolded cp_alt_def]
@@ -5112,3 +5665,4 @@
by (cases e, auto)
end
+