--- a/CpsG.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/CpsG.thy Wed Jan 06 20:46:14 2016 +0800
@@ -91,15 +91,17 @@
and "(Cs cs, Th th'') \<in> RAG s'"
shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
proof -
+ interpret vt_s': valid_trace "s'" using assms(1)
+ by (unfold_locales, simp)
interpret rtree: rtree "RAG s'"
proof
show "single_valued (RAG s')"
apply (intro_locales)
by (unfold single_valued_def,
- auto intro:unique_RAG[OF assms(1)])
+ auto intro:vt_s'.unique_RAG)
show "acyclic (RAG s')"
- by (rule acyclic_RAG[OF assms(1)])
+ by (rule vt_s'.acyclic_RAG)
qed
{ fix n1 n2
assume "(n1, n2) \<in> ?L"
@@ -152,6 +154,13 @@
} ultimately show ?thesis by auto
qed
+context valid_trace
+begin
+
+lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]
+
+end
+
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
@@ -221,76 +230,133 @@
} thus ?thesis by auto
qed
+lemma tRAG_trancl_eq:
+ "{th'. (Th th', Th th) \<in> (tRAG s)^+} =
+ {th'. (Th th', Th th) \<in> (RAG s)^+}"
+ (is "?L = ?R")
+proof -
+ { fix th'
+ assume "th' \<in> ?L"
+ hence "(Th th', Th th) \<in> (tRAG s)^+" by auto
+ from tranclD[OF this]
+ obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto
+ from tRAG_subtree_RAG[of s] and this(2)
+ have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG)
+ moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto
+ ultimately have "th' \<in> ?R" by auto
+ } moreover
+ { fix th'
+ assume "th' \<in> ?R"
+ hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)
+ from plus_rpath[OF this]
+ obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto
+ hence "(Th th', Th th) \<in> (tRAG s)^+"
+ proof(induct xs arbitrary:th' th rule:length_induct)
+ case (1 xs th' th)
+ then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)
+ show ?case
+ proof(cases "xs1")
+ case Nil
+ from 1(2)[unfolded Cons1 Nil]
+ have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
+ hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
+ then obtain cs where "x1 = Cs cs"
+ by (unfold s_RAG_def, auto)
+ from rpath_nnl_lastE[OF rp[unfolded this]]
+ show ?thesis by auto
+ next
+ case (Cons x2 xs2)
+ from 1(2)[unfolded Cons1[unfolded this]]
+ have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
+ from rpath_edges_on[OF this]
+ have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
+ have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
+ by (simp add: edges_on_unfold)
+ with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
+ then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
+ have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
+ by (simp add: edges_on_unfold)
+ from this eds
+ have rg2: "(x1, x2) \<in> RAG s" by auto
+ from this[unfolded eq_x1]
+ obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
+ from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
+ have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)
+ from rp have "rpath (RAG s) x2 xs2 (Th th)"
+ by (elim rpath_ConsE, simp)
+ from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
+ show ?thesis
+ proof(cases "xs2 = []")
+ case True
+ from rpath_nilE[OF rp'[unfolded this]]
+ have "th1 = th" by auto
+ from rt1[unfolded this] show ?thesis by auto
+ next
+ case False
+ from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]
+ have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp
+ with rt1 show ?thesis by auto
+ qed
+ qed
+ qed
+ hence "th' \<in> ?L" by auto
+ } ultimately show ?thesis by blast
+qed
+
+lemma tRAG_trancl_eq_Th:
+ "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} =
+ {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}"
+ using tRAG_trancl_eq by auto
+
+lemma dependants_alt_def:
+ "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
+ by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
+
+context valid_trace
+begin
+
+lemma count_eq_tRAG_plus:
+ assumes "cntP s th = cntV s th"
+ shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
+ using assms count_eq_dependants dependants_alt_def eq_dependants by auto
+
+lemma count_eq_RAG_plus:
+ assumes "cntP s th = cntV s th"
+ shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+ using assms count_eq_dependants cs_dependants_def eq_RAG by auto
+
+lemma count_eq_RAG_plus_Th:
+ assumes "cntP s th = cntV s th"
+ shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
+ using count_eq_RAG_plus[OF assms] by auto
+
+lemma count_eq_tRAG_plus_Th:
+ assumes "cntP s th = cntV s th"
+ shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
+ using count_eq_tRAG_plus[OF assms] by auto
+
+end
+
lemma tRAG_subtree_eq:
"(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th' \<in> (subtree (RAG s) (Th th))}"
(is "?L = ?R")
proof -
- { fix n
- assume "n \<in> ?L"
- with subtree_nodeE[OF this]
- obtain th' where "n = Th th'" "Th th' \<in> subtree (tRAG s) (Th th)" by auto
- with tRAG_subtree_RAG[of s "Th th"]
- have "n \<in> ?R" by auto
+ { fix n
+ assume h: "n \<in> ?L"
+ hence "n \<in> ?R"
+ by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG)
} moreover {
fix n
assume "n \<in> ?R"
- then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
+ then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
by (auto simp:subtree_def)
- from star_rpath[OF this(2)]
- obtain xs where "rpath (RAG s) (Th th') xs (Th th)" by auto
- hence "Th th' \<in> subtree (tRAG s) (Th th)"
- proof(induct xs arbitrary:th' th rule:length_induct)
- case (1 xs th' th)
- show ?case
- proof(cases xs)
- case Nil
- from rpath_nilE[OF 1(2)[unfolded this]]
- have "th' = th" by auto
- thus ?thesis by (auto simp:subtree_def)
- next
- case (Cons x1 xs1) note Cons1 = Cons
- show ?thesis
- proof(cases "xs1")
- case Nil
- from 1(2)[unfolded Cons[unfolded this]]
- have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
- hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
- then obtain cs where "x1 = Cs cs"
- by (unfold s_RAG_def, auto)
- from rpath_nnl_lastE[OF rp[unfolded this]]
- show ?thesis by auto
- next
- case (Cons x2 xs2)
- from 1(2)[unfolded Cons1[unfolded this]]
- have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
- from rpath_edges_on[OF this]
- have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
- have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
- by (simp add: edges_on_unfold)
- with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
- then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
- have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
- by (simp add: edges_on_unfold)
- from this eds
- have rg2: "(x1, x2) \<in> RAG s" by auto
- from this[unfolded eq_x1]
- obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
- from rp have "rpath (RAG s) x2 xs2 (Th th)"
- by (elim rpath_ConsE, simp)
- from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
- from 1(1)[rule_format, OF _ this, unfolded Cons1 Cons]
- have "Th th1 \<in> subtree (tRAG s) (Th th)" by simp
- moreover have "(Th th', Th th1) \<in> (tRAG s)^*"
- proof -
- from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
- show ?thesis by (unfold RAG_split tRAG_def wRAG_def hRAG_def, auto)
- qed
- ultimately show ?thesis by (auto simp:subtree_def)
- qed
- qed
- qed
- from this[folded h(1)]
- have "n \<in> ?L" .
+ from rtranclD[OF this(2)]
+ have "n \<in> ?L"
+ proof
+ assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
+ with h have "n \<in> {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" by auto
+ thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
+ qed (insert h, auto simp:subtree_def)
} ultimately show ?thesis by auto
qed
@@ -325,13 +391,40 @@
by (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
qed
-locale valid_trace =
- fixes s
- assumes vt : "vt s"
context valid_trace
begin
+lemma RAG_threads:
+ assumes "(Th th) \<in> Field (RAG s)"
+ shows "th \<in> threads s"
+ using assms
+ by (metis Field_def UnE dm_RAG_threads range_in vt)
+
+lemma subtree_tRAG_thread:
+ assumes "th \<in> threads s"
+ shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
+proof -
+ have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+ by (unfold tRAG_subtree_eq, simp)
+ also have "... \<subseteq> ?R"
+ proof
+ fix x
+ assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
+ then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
+ from this(2)
+ show "x \<in> ?R"
+ proof(cases rule:subtreeE)
+ case 1
+ thus ?thesis by (simp add: assms h(1))
+ next
+ case 2
+ thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI)
+ qed
+ qed
+ finally show ?thesis .
+qed
+
lemma readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
@@ -369,19 +462,19 @@
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
+ with dm_RAG_threads and range_in 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)" .
+ from finite_RAG show "finite (RAG s)" .
next
- from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
+ from acyclic_RAG show "acyclic (RAG s)" .
qed
lemma sgv_wRAG: "single_valued (wRAG s)"
- using waiting_unique[OF vt]
+ using waiting_unique
by (unfold single_valued_def wRAG_def, auto)
lemma sgv_hRAG: "single_valued (hRAG s)"
@@ -394,7 +487,7 @@
lemma acyclic_tRAG: "acyclic (tRAG s)"
proof(unfold tRAG_def, rule acyclic_compose)
- show "acyclic (RAG s)" using acyclic_RAG[OF vt] .
+ show "acyclic (RAG s)" using acyclic_RAG .
next
show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
next
@@ -402,11 +495,12 @@
qed
lemma sgv_RAG: "single_valued (RAG s)"
- using unique_RAG[OF vt] by (auto simp:single_valued_def)
+ using unique_RAG by (auto simp:single_valued_def)
lemma rtree_RAG: "rtree (RAG s)"
- using sgv_RAG acyclic_RAG[OF vt]
+ using sgv_RAG acyclic_RAG
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+
end
@@ -415,10 +509,10 @@
show "single_valued (RAG s)"
apply (intro_locales)
by (unfold single_valued_def,
- auto intro:unique_RAG[OF vt])
+ auto intro:unique_RAG)
show "acyclic (RAG s)"
- by (rule acyclic_RAG[OF vt])
+ by (rule acyclic_RAG)
qed
sublocale valid_trace < rtree_s: rtree "tRAG s"
@@ -432,7 +526,7 @@
proof -
show "fsubtree (RAG s)"
proof(intro_locales)
- show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG[OF vt]] .
+ show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
next
show "fsubtree_axioms (RAG s)"
proof(unfold fsubtree_axioms_def)
@@ -450,13 +544,13 @@
proof(unfold tRAG_def, rule fbranch_compose)
show "fbranch (wRAG s)"
proof(rule finite_fbranchI)
- from finite_RAG[OF vt] show "finite (wRAG s)"
+ from finite_RAG show "finite (wRAG s)"
by (unfold RAG_split, auto)
qed
next
show "fbranch (hRAG s)"
proof(rule finite_fbranchI)
- from finite_RAG[OF vt]
+ from finite_RAG
show "finite (hRAG s)" by (unfold RAG_split, auto)
qed
qed
@@ -596,16 +690,18 @@
by (unfold cs_holding_def, auto)
qed
+context valid_trace
+begin
+
lemma next_th_waiting:
- assumes vt: "vt s"
- and nxt: "next_th s th cs th'"
+ assumes nxt: "next_th s th cs th'"
shows "waiting (wq s) th' cs"
proof -
from nxt[unfolded next_th_def]
obtain rest where h: "wq s cs = th # rest"
"rest \<noteq> []"
"th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
- from wq_distinct[OF vt, of cs, unfolded h]
+ from wq_distinct[of cs, unfolded h]
have dst: "distinct (th # rest)" .
have in_rest: "th' \<in> set rest"
proof(unfold h, rule someI2)
@@ -622,11 +718,12 @@
qed
lemma next_th_RAG:
- assumes vt: "vt s"
- and nxt: "next_th s th cs th'"
+ assumes nxt: "next_th (s::event list) th cs th'"
shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
- using assms next_th_holding next_th_waiting
-by (unfold s_RAG_def, simp)
+ using vt assms next_th_holding next_th_waiting
+ by (unfold s_RAG_def, simp)
+
+end
-- {* A useless definition *}
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
@@ -909,7 +1006,7 @@
*)
lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
- using next_th_RAG[OF vat_s'.vt nt] .
+ using next_th_RAG[OF nt] .
lemma ancestors_th':
"ancestors (RAG s') (Th th') = {Th th, Cs cs}"
@@ -1175,7 +1272,7 @@
lemma tRAG_s:
"tRAG s = tRAG s' \<union> {(Th th, Th th')}"
- using RAG_tRAG_transfer[OF step_back_vt[OF vt_s[unfolded s_def]] RAG_s cs_held] .
+ using RAG_tRAG_transfer[OF RAG_s cs_held] .
lemma cp_kept:
assumes "Th th'' \<notin> ancestors (tRAG s) (Th th)"