--- a/CpsG.thy~ Tue Dec 15 15:10:40 2015 +0000
+++ b/CpsG.thy~ Fri Dec 18 19:13:19 2015 +0800
@@ -21,6 +21,22 @@
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
+lemma tRAG_Field:
+ "Field (tRAG s) \<subseteq> Field (RAG s)"
+ by (unfold tRAG_alt_def Field_def, auto)
+
+lemma tRAG_ancestorsE:
+ assumes "x \<in> ancestors (tRAG s) u"
+ obtains th where "x = Th th"
+proof -
+ from assms have "(u, x) \<in> (tRAG s)^+"
+ by (unfold ancestors_def, auto)
+ from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
+ then obtain th where "x = Th th"
+ by (unfold tRAG_alt_def, auto)
+ from that[OF this] show ?thesis .
+qed
+
lemma tRAG_mono:
assumes "RAG s' \<subseteq> RAG s"
shows "tRAG s' \<subseteq> tRAG s"
@@ -337,6 +353,15 @@
context valid_trace
begin
+lemma not_in_thread_isolated:
+ assumes "th \<notin> threads s"
+ shows "(Th th) \<notin> Field (RAG s)"
+proof
+ assume "(Th th) \<in> Field (RAG s)"
+ with dm_RAG_threads[OF vt] and range_in[OF vt] assms
+ show False by (unfold Field_def, blast)
+qed
+
lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
from finite_RAG[OF vt] show "finite (RAG s)" .
@@ -1572,25 +1597,30 @@
context step_P_cps
begin
-lemma rtree_RAGs: "rtree (RAG s)"
-proof
- show "single_valued (RAG s)"
- apply (intro_locales)
- by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
-
- show "acyclic (RAG s)"
- by (rule acyclic_RAG[OF vt_s])
+lemma readys_th: "th \<in> readys s'"
+proof -
+ from step_back_step [OF vt_s[unfolded s_def]]
+ have "PIP s' (P th cs)" .
+ hence "th \<in> runing s'" by (cases, simp)
+ thus ?thesis by (simp add:readys_def runing_def)
qed
-lemma rtree_RAGs': "rtree (RAG s')"
+lemma root_th: "root (RAG s') (Th th)"
+ using readys_root[OF vat_s'.vt readys_th] .
+
+lemma in_no_others_subtree:
+ assumes "th' \<noteq> th"
+ shows "Th th \<notin> subtree (RAG s') (Th th')"
proof
- show "single_valued (RAG s')"
- apply (intro_locales)
- by (unfold single_valued_def,
- auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-
- show "acyclic (RAG s')"
- by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ assume "Th th \<in> subtree (RAG s') (Th th')"
+ thus False
+ proof(cases rule:subtreeE)
+ case 1
+ with assms show ?thesis by auto
+ next
+ case 2
+ with root_th show ?thesis by (auto simp:root_def)
+ qed
qed
lemma preced_kept: "the_preced s = the_preced s'"
@@ -1615,143 +1645,26 @@
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
+lemma subtree_kept:
+ assumes "th' \<noteq> th"
+ shows "subtree (RAG s) (Th th') = subtree (RAG s') (Th th')"
+proof(unfold RAG_s, rule subtree_insert_next)
+ from in_no_others_subtree[OF assms]
+ show "Th th \<notin> subtree (RAG s') (Th th')" .
qed
-lemma child_kept_right:
- assumes
- "(n1, n2) \<in> (child s)^+"
- shows "(n1, n2) \<in> (child s')^+"
+lemma cp_kept:
+ assumes "th' \<noteq> th"
+ shows "cp s th' = cp s' th'"
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
+ have "(the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')}) =
+ (the_preced s' ` {th'a. Th th'a \<in> subtree (RAG s') (Th th')})"
+ by (unfold preced_kept subtree_kept[OF assms], simp)
+ thus ?thesis by (unfold cp_alt_def, simp)
qed
end
-lemma tRAG_ancestorsE:
- assumes "x \<in> ancestors (tRAG s) u"
- obtains th where "x = Th th"
-proof -
- from assms have "(u, x) \<in> (tRAG s)^+"
- by (unfold ancestors_def, auto)
- from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
- then obtain th where "x = Th th"
- by (unfold tRAG_alt_def, auto)
- from that[OF this] show ?thesis .
-qed
-
-
context step_P_cps_ne
begin
@@ -1813,19 +1726,7 @@
show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
qed
-lemma set_prop_split:
- "A = {x. x \<in> A \<and> PP x} \<union> {x. x \<in> A \<and> \<not> PP x}"
- by auto
-
-lemma f_image_union_eq:
- assumes "f ` A = g ` A"
- and "f ` B = g ` B"
- shows "f ` (A \<union> B) = g ` (A \<union> B)"
- using assms by auto
-
-(* ccc *)
-
-lemma cp_gen_update_stop:
+lemma cp_gen_update_stop: (* ddd *)
assumes "u \<in> ancestors (tRAG s) (Th th)"
and "cp_gen s u = cp_gen s' u"
and "y \<in> ancestors (tRAG s) u"
@@ -1842,6 +1743,7 @@
Max ({the_preced s th2} \<union> cp_gen s ` RTree.children (tRAG s) x)" .
also have "... =
Max ({the_preced s' th2} \<union> cp_gen s' ` RTree.children (tRAG s') x)"
+
proof -
from preced_kept have "the_preced s th2 = the_preced s' th2" by simp
moreover have "cp_gen s ` RTree.children (tRAG s) x =
@@ -1918,7 +1820,22 @@
case False
from a_in obtain th_a where eq_a: "a = Th th_a"
by (auto simp:RTree.children_def tRAG_alt_def)
- have "a \<notin> ancestors (tRAG s) (Th th)" sorry
+ have "a \<notin> ancestors (tRAG s) (Th th)"
+ proof
+ assume a_in': "a \<in> ancestors (tRAG s) (Th th)"
+ have "a = z"
+ proof(rule vat_s.rtree_s.ancestors_children_unique)
+ from assms(1) h(1) have "z \<in> ancestors (tRAG s) (Th th)"
+ by (auto simp:ancestors_def)
+ with h(2) show " z \<in> ancestors (tRAG s) (Th th) \<inter>
+ RTree.children (tRAG s) x" by auto
+ next
+ from a_in a_in'
+ show "a \<in> ancestors (tRAG s) (Th th) \<inter> RTree.children (tRAG s) x"
+ by auto
+ qed
+ with False show False by auto
+ qed
from cp_kept[OF this[unfolded eq_a]]
have "cp s th_a = cp s' th_a" .
from this[unfolded cp_gen_def_cond[OF eq_a], folded eq_a]
@@ -1936,316 +1853,19 @@
qed
qed
-
-
-(* ccc *)
-
-lemma eq_child_left:
- assumes nd: "(Th th, Th th') \<notin> (child s)^+"
- shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
-proof(induct rule:converse_trancl_induct)
- case (base y)
- from base obtain th1 cs1
- where h1: "(Th th1, Cs cs1) \<in> RAG s"
- and h2: "(Cs cs1, Th th') \<in> RAG s"
- and eq_y: "y = Th th1" by (auto simp:child_def)
- have "th1 \<noteq> th"
- proof
- assume "th1 = th"
- with base eq_y have "(Th th, Th th') \<in> child s" by simp
- with nd show False by auto
- qed
- with h1 h2 RAG_s
- have h1': "(Th th1, Cs cs1) \<in> RAG s'" and
- h2': "(Cs cs1, Th th') \<in> RAG s'" by auto
- with eq_y show ?case by (auto simp:child_def)
-next
- case (step y z)
- have yz: "(y, z) \<in> child s" by fact
- then obtain th1 cs1 th2
- where h1: "(Th th1, Cs cs1) \<in> RAG s"
- and h2: "(Cs cs1, Th th2) \<in> RAG s"
- and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
- have "th1 \<noteq> th"
- proof
- assume "th1 = th"
- with yz eq_y have "(Th th, z) \<in> child s" by simp
- moreover have "(z, Th th') \<in> (child s)^+" by fact
- ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
- with nd show False by auto
- qed
- with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"
- and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto
- with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
- moreover have "(z, Th th') \<in> (child s')^+" by fact
- ultimately show ?case by auto
-qed
-
-lemma eq_child_right:
- shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
-proof(induct rule:converse_trancl_induct)
- case (base y)
- with RAG_s show ?case by (auto simp:child_def)
-next
- case (step y z)
- have "(y, z) \<in> child s'" by fact
- with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)
- moreover have "(z, Th th') \<in> (child s)^+" by fact
- ultimately show ?case by auto
-qed
-
-lemma eq_child:
- assumes nd: "(Th th, Th th') \<notin> (child s)^+"
- shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
- by (insert eq_child_left[OF nd] eq_child_right, auto)
-
-lemma eq_cp:
- 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'"
+lemma cp_up:
+ assumes "(Th th') \<in> ancestors (tRAG s) (Th th)"
+ and "cp s th' = cp s' th'"
+ and "(Th th'') \<in> ancestors (tRAG s) (Th th')"
shows "cp s th'' = cp s' th''"
proof -
- 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
+ have "cp_gen s (Th th'') = cp_gen s' (Th th'')"
+ proof(rule cp_gen_update_stop[OF assms(1) _ assms(3)])
+ from assms(2) cp_gen_def_cond[OF refl[of "Th th'"]]
+ show "cp_gen s (Th th') = cp_gen s' (Th th')" by metis
+ qed
+ with cp_gen_def_cond[OF refl[of "Th th''"]]
+ show ?thesis by metis
qed
end
@@ -2255,147 +1875,191 @@
defines s_def : "s \<equiv> (Create th prio#s')"
assumes vt_s: "vt s"
+sublocale step_create_cps < vat_s: valid_trace "s"
+ by (unfold_locales, insert vt_s, simp)
+
+sublocale step_create_cps < vat_s': valid_trace "s'"
+ by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
+
context step_create_cps
begin
-lemma eq_dep: "RAG s = RAG s'"
+lemma RAG_kept: "RAG s = RAG s'"
by (unfold s_def RAG_create_unchanged, auto)
+lemma tRAG_kept: "tRAG s = tRAG s'"
+ by (unfold tRAG_alt_def RAG_kept, auto)
+
+lemma preced_kept:
+ assumes "th' \<noteq> th"
+ shows "the_preced s th' = the_preced s' th'"
+ by (unfold s_def the_preced_def preced_def, insert assms, auto)
+
+lemma th_not_in: "Th th \<notin> Field (tRAG s')"
+proof -
+ from vt_s[unfolded s_def]
+ have "PIP s' (Create th prio)" by (cases, simp)
+ hence "th \<notin> threads s'" by(cases, simp)
+ from vat_s'.not_in_thread_isolated[OF this]
+ have "Th th \<notin> Field (RAG s')" .
+ with tRAG_Field show ?thesis by auto
+qed
+
lemma eq_cp:
- 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
+ have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
+ (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
+ proof(unfold tRAG_kept, rule f_image_eq)
+ fix a
+ assume a_in: "a \<in> subtree (tRAG s') (Th th')"
+ then obtain th_a where eq_a: "a = Th th_a"
+ proof(cases rule:subtreeE)
+ case 2
+ from ancestors_Field[OF 2(2)]
+ and that show ?thesis by (unfold tRAG_alt_def, auto)
+ qed auto
+ have neq_th_a: "th_a \<noteq> th"
+ proof -
+ have "(Th th) \<notin> subtree (tRAG s') (Th th')"
+ proof
+ assume "Th th \<in> subtree (tRAG s') (Th th')"
+ thus False
+ proof(cases rule:subtreeE)
+ case 2
+ from ancestors_Field[OF this(2)]
+ and th_not_in[unfolded Field_def]
+ show ?thesis by auto
+ qed (insert assms, auto)
+ qed
+ with a_in[unfolded eq_a] show ?thesis by auto
qed
+ from preced_kept[OF this]
+ show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
+ by (unfold eq_a, simp)
qed
- 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
+ thus ?thesis by (unfold cp_alt_def1, simp)
qed
-lemma nil_dependants: "dependants s th = {}"
+lemma children_of_th: "RTree.children (tRAG s) (Th 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
+ { fix a
+ assume "a \<in> RTree.children (tRAG s) (Th th)"
+ hence "(a, Th th) \<in> tRAG s" by (auto simp:RTree.children_def)
+ with th_not_in have False
+ by (unfold Field_def tRAG_kept, auto)
+ } thus ?thesis by auto
qed
lemma eq_cp_th: "cp s th = preced th s"
- apply (unfold cp_eq_cpreced cpreced_def)
- by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)
+ by (unfold vat_s.cp_rec children_of_th, simp add:the_preced_def)
end
-
locale step_exit_cps =
fixes s' th prio s
defines s_def : "s \<equiv> Exit th # s'"
assumes vt_s: "vt s"
+sublocale step_exit_cps < vat_s: valid_trace "s"
+ by (unfold_locales, insert vt_s, simp)
+
+sublocale step_exit_cps < vat_s': valid_trace "s'"
+ by (unfold_locales, insert step_back_vt[OF vt_s[unfolded s_def]], simp)
+
context step_exit_cps
begin
-lemma eq_dep: "RAG s = RAG s'"
+lemma preced_kept:
+ assumes "th' \<noteq> th"
+ shows "the_preced s th' = the_preced s' th'"
+ by (unfold s_def the_preced_def preced_def, insert assms, auto)
+
+lemma RAG_kept: "RAG s = RAG s'"
by (unfold s_def RAG_exit_unchanged, auto)
+lemma tRAG_kept: "tRAG s = tRAG s'"
+ by (unfold tRAG_alt_def RAG_kept, auto)
+
+lemma th_ready: "th \<in> readys s'"
+proof -
+ from vt_s[unfolded s_def]
+ have "PIP s' (Exit th)" by (cases, simp)
+ hence h: "th \<in> runing s' \<and> holdents s' th = {}" by (cases, metis)
+ thus ?thesis by (unfold runing_def, auto)
+qed
+
+lemma th_holdents: "holdents s' th = {}"
+proof -
+ from vt_s[unfolded s_def]
+ have "PIP s' (Exit th)" by (cases, simp)
+ thus ?thesis by (cases, metis)
+qed
+
+lemma th_RAG: "Th th \<notin> Field (RAG s')"
+proof -
+ have "Th th \<notin> Range (RAG s')"
+ proof
+ assume "Th th \<in> Range (RAG s')"
+ then obtain cs where "holding (wq s') th cs"
+ by (unfold Range_iff s_RAG_def, auto)
+ with th_holdents[unfolded holdents_def]
+ show False by (unfold eq_holding, auto)
+ qed
+ moreover have "Th th \<notin> Domain (RAG s')"
+ proof
+ assume "Th th \<in> Domain (RAG s')"
+ then obtain cs where "waiting (wq s') th cs"
+ by (unfold Domain_iff s_RAG_def, auto)
+ with th_ready show False by (unfold readys_def eq_waiting, auto)
+ qed
+ ultimately show ?thesis by (auto simp:Field_def)
+qed
+
+lemma th_tRAG: "(Th th) \<notin> Field (tRAG s')"
+ using th_RAG tRAG_Field[of s'] by auto
+
lemma eq_cp:
- 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)
+ have "(the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th') =
+ (the_preced s' \<circ> the_thread) ` subtree (tRAG s') (Th th')"
+ proof(unfold tRAG_kept, rule f_image_eq)
+ fix a
+ assume a_in: "a \<in> subtree (tRAG s') (Th th')"
+ then obtain th_a where eq_a: "a = Th th_a"
+ proof(cases rule:subtreeE)
+ case 2
+ from ancestors_Field[OF 2(2)]
+ and that show ?thesis by (unfold tRAG_alt_def, auto)
+ qed auto
+ have neq_th_a: "th_a \<noteq> th"
+ proof -
+ from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+ have "(Th th) \<notin> subtree (RAG s') (Th th')" .
+ find_theorems subtree tRAG RAG (* ccc *)
+ 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_tRAG[unfolded Field_def]
+ show ?thesis by auto
+ qed (insert assms, auto)
+ qed
+ with a_in[unfolded eq_a] show ?thesis by auto
qed
+ from preced_kept[OF this]
+ show "(the_preced s \<circ> the_thread) a = (the_preced s' \<circ> the_thread) a"
+ by (unfold eq_a, simp)
qed
- 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
+ thus ?thesis by (unfold cp_alt_def1, simp)
qed
end
+
end