ExtGG.thy finished, but more comments are needed.
--- 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)"
--- a/CpsG.thy~ Tue Dec 22 23:13:31 2015 +0800
+++ b/CpsG.thy~ Wed Jan 06 20:46:14 2016 +0800
@@ -10,6 +10,10 @@
difference is the order of arguemts. *}
definition "the_preced s th = preced th s"
+lemma inj_the_preced:
+ "inj_on (the_preced s) (threads s)"
+ by (metis inj_onI preced_unique the_preced_def)
+
text {* @{term "the_thread"} extracts thread out of RAG node. *}
fun the_thread :: "node \<Rightarrow> thread" where
"the_thread (Th th) = th"
@@ -87,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"
@@ -148,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))})"
@@ -217,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
@@ -321,13 +391,17 @@
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 readys_root:
assumes "th \<in> readys s"
shows "root (RAG s) (Th th)"
@@ -365,19 +439,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)"
@@ -390,7 +464,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
@@ -398,11 +472,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
@@ -411,10 +486,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"
@@ -428,7 +503,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)
@@ -446,13 +521,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
@@ -592,16 +667,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)
@@ -618,11 +695,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"
@@ -905,7 +983,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}"
@@ -1171,7 +1249,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)"
--- a/ExtGG.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/ExtGG.thy Wed Jan 06 20:46:14 2016 +0800
@@ -2,67 +2,93 @@
imports PrioG CpsG
begin
-lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
- apply (induct s, simp)
-proof -
- fix a s
- assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
- and eq_as: "a # s \<noteq> []"
- show "last_set th (a # s) < length (a # s)"
- proof(cases "s \<noteq> []")
- case False
- from False show ?thesis
- by (cases a, auto simp:last_set.simps)
- next
- case True
- from ih [OF True] show ?thesis
- by (cases a, auto simp:last_set.simps)
- qed
+text {*
+ The following two auxiliary lemmas are used to reason about @{term Max}.
+*}
+lemma image_Max_eqI:
+ assumes "finite B"
+ and "b \<in> B"
+ and "\<forall> x \<in> B. f x \<le> f b"
+ shows "Max (f ` B) = f b"
+ using assms
+ using Max_eqI by blast
+
+lemma image_Max_subset:
+ assumes "finite A"
+ and "B \<subseteq> A"
+ and "a \<in> B"
+ and "Max (f ` A) = f a"
+ shows "Max (f ` B) = f a"
+proof(rule image_Max_eqI)
+ show "finite B"
+ using assms(1) assms(2) finite_subset by auto
+next
+ show "a \<in> B" using assms by simp
+next
+ show "\<forall>x\<in>B. f x \<le> f a"
+ by (metis Max_ge assms(1) assms(2) assms(4)
+ finite_imageI image_eqI subsetCE)
qed
-lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
- by (induct s, auto simp:threads.simps)
-
-lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
- apply (drule_tac th_in_ne)
- by (unfold preced_def, auto intro: birth_time_lt)
-
+text {*
+ The following locale @{text "highest_gen"} sets the basic context for our
+ investigation: supposing thread @{text th} holds the highest @{term cp}-value
+ in state @{text s}, which means the task for @{text th} is the
+ most urgent. We want to show that
+ @{text th} is treated correctly by PIP, which means
+ @{text th} will not be blocked unreasonably by other less urgent
+ threads.
+*}
locale highest_gen =
fixes s th prio tm
assumes vt_s: "vt s"
and threads_s: "th \<in> threads s"
and highest: "preced th s = Max ((cp s)`threads s)"
- and preced_th: "preced th s = Prc prio tm"
+ -- {* The internal structure of @{term th}'s precedence is exposed:*}
+ and preced_th: "preced th s = Prc prio tm"
+-- {* @{term s} is a valid trace, so it will inherit all results derived for
+ a valid trace: *}
sublocale highest_gen < vat_s: valid_trace "s"
by (unfold_locales, insert vt_s, simp)
context highest_gen
begin
+text {*
+ @{term tm} is the time when the precedence of @{term th} is set, so
+ @{term tm} must be a valid moment index into @{term s}.
+*}
lemma lt_tm: "tm < length s"
by (insert preced_tm_lt[OF threads_s preced_th], simp)
+text {*
+ Since @{term th} holds the highest precedence and @{text "cp"}
+ is the highest precedence of all threads in the sub-tree of
+ @{text "th"} and @{text th} is among these threads,
+ its @{term cp} must equal to its precedence:
+*}
lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
proof -
have "?L \<le> ?R"
by (unfold highest, rule Max_ge,
- auto simp:threads_s finite_threads[OF vt_s])
+ auto simp:threads_s finite_threads)
moreover have "?R \<le> ?L"
by (unfold vat_s.cp_rec, rule Max_ge,
auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
ultimately show ?thesis by auto
qed
+(* ccc *)
lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
- by (fold max_cp_eq[OF vt_s], unfold eq_cp_s_th, insert highest, simp)
+ by (fold max_cp_eq, unfold eq_cp_s_th, insert highest, simp)
lemma highest_preced_thread: "preced th s = Max ((\<lambda> th'. preced th' s) ` threads s)"
by (fold eq_cp_s_th, unfold highest_cp_preced, simp)
lemma highest': "cp s th = Max (cp s ` threads s)"
proof -
- from highest_cp_preced max_cp_eq[OF vt_s, symmetric]
+ from highest_cp_preced max_cp_eq[symmetric]
show ?thesis by simp
qed
@@ -75,6 +101,9 @@
and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
+sublocale extend_highest_gen < vat_t: valid_trace "t@s"
+ by (unfold_locales, insert vt_t, simp)
+
lemma step_back_vt_app:
assumes vt_ts: "vt (t@s)"
shows "vt s"
@@ -110,14 +139,6 @@
context extend_highest_gen
begin
-(*
- lemma red_moment:
- "extend_highest_gen s th prio tm (moment i t)"
- apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
- apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
- by (unfold highest_gen_def, auto dest:step_back_vt_app)
-*)
-
lemma ind [consumes 0, case_names Nil Cons, induct type]:
assumes
h0: "R []"
@@ -218,48 +239,21 @@
qed
qed
-lemma Max_remove_less:
- assumes "finite A"
- and "a \<in> A"
- and "b \<in> A"
- and "a \<noteq> b"
- and "inj_on f A"
- and "f a = Max (f ` A)"
- shows "Max (f ` (A - {b})) = (Max (f ` A))"
-proof -
- have "Max (f ` (A - {b})) = Max (f`A - {f b})"
- proof -
- have "f ` (A - {b}) = f ` A - f ` {b}"
- by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto)
- thus ?thesis by simp
- qed
- also have "... =
- (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))"
- proof(subst Max.remove)
- from assms show "f a \<in> f ` A - {f b}"
- by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff)
- next
- from assms(1) show "finite (f ` A - {f b})" by auto
- qed auto
- also have "... = Max (f ` A)" (is "?L = ?R")
- proof(cases "f ` A - {f b} - {f a} = {}")
- case True
- with assms show ?thesis by auto
- next
- case False
- hence "?L = max (f a) (Max (f ` A - {f b} - {f a}))"
- by simp
- also have "... = ?R"
- proof -
- from assms False
- have "(Max (f ` A - {f b} - {f a})) \<le> f a" by auto
- thus ?thesis by (simp add: assms(6) max_def)
- qed
- finally show ?thesis .
- qed
- finally show ?thesis .
-qed
+text {*
+ According to @{thm th_kept}, thread @{text "th"} has its living status
+ and precedence kept along the way of @{text "t"}. The following lemma
+ shows that this preserved precedence of @{text "th"} remains as the highest
+ along the way of @{text "t"}.
+ The proof goes by induction over @{text "t"} using the specialized
+ induction rule @{thm ind}, followed by case analysis of each possible
+ operations of PIP. All cases follow the same pattern rendered by the
+ generalized introduction rule @{thm "image_Max_eqI"}.
+
+ The very essence is to show that precedences, no matter whether they are newly introduced
+ or modified, are always lower than the one held by @{term "th"},
+ which by @{thm th_kept} is preserved along the way.
+*}
lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
proof(induct rule:ind)
case Nil
@@ -273,62 +267,74 @@
show ?case
proof(cases e)
case (Create thread prio')
- from Cons(2)[unfolded this]
- have thread_not_in: "thread \<notin> threads (t@s)" by (cases, simp)
show ?thesis (is "Max (?f ` ?A) = ?t")
proof -
- have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))"
- by (unfold Create, simp)
- moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
- proof(rule Max.insert)
- from finite_threads[OF Cons(1)]
- show "finite (?f ` (threads (t@s)))" by simp
- qed (insert h_t.th_kept, auto)
- moreover have "(Max (?f ` (threads (t@s)))) = ?t"
- proof -
- have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) =
- (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"
- by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def)
- with Cons show ?thesis by (auto simp:the_preced_def)
+ -- {* The following is the common pattern of each branch of the case analysis. *}
+ -- {* The major part is to show that @{text "th"} holds the highest precedence: *}
+ have "Max (?f ` ?A) = ?f th"
+ proof(rule image_Max_eqI)
+ show "finite ?A" using h_e.finite_threads by auto
+ next
+ show "th \<in> ?A" using h_e.th_kept by auto
+ next
+ show "\<forall>x\<in>?A. ?f x \<le> ?f th"
+ proof
+ fix x
+ assume "x \<in> ?A"
+ hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)
+ thus "?f x \<le> ?f th"
+ proof
+ assume "x = thread"
+ thus ?thesis
+ apply (simp add:Create the_preced_def preced_def, fold preced_def)
+ using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 preced_th by force
+ next
+ assume h: "x \<in> threads (t @ s)"
+ from Cons(2)[unfolded Create]
+ have "x \<noteq> thread" using h by (cases, auto)
+ hence "?f x = the_preced (t@s) x"
+ by (simp add:Create the_preced_def preced_def)
+ hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"
+ by (simp add: h_t.finite_threads h)
+ also have "... = ?f th"
+ by (metis Cons.hyps(5) h_e.th_kept the_preced_def)
+ finally show ?thesis .
+ qed
+ qed
qed
- moreover have "?f thread < ?t"
- proof -
- from h_e.create_low and Create
- have "prio' \<le> prio" by auto
- thus ?thesis
- by (unfold preced_th, unfold Create, insert lt_tm,
- auto simp:preced_def precedence_less_def preced_th the_preced_def)
- qed
- ultimately show ?thesis by (auto simp:max_def)
- qed
+ -- {* The minor part is to show that the precedence of @{text "th"}
+ equals to preserved one, given by the foregoing lemma @{thm th_kept} *}
+ also have "... = ?t" using h_e.th_kept the_preced_def by auto
+ -- {* Then it follows trivially that the precedence preserved
+ for @{term "th"} remains the maximum of all living threads along the way. *}
+ finally show ?thesis .
+ qed
next
case (Exit thread)
- show ?thesis
+ show ?thesis (is "Max (?f ` ?A) = ?t")
proof -
- have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) =
- Max (the_preced (t @ s) ` (threads (t @ s)))"
- proof(rule Max_remove_less)
- show "th \<noteq> thread" using Exit h_e.exit_diff by auto
+ have "Max (?f ` ?A) = ?f th"
+ proof(rule image_Max_eqI)
+ show "finite ?A" using h_e.finite_threads by auto
next
- from Cons(2)[unfolded Exit]
- show "thread \<in> threads (t @ s)"
- by (cases, simp add: readys_def runing_def)
- next
- show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t)
+ show "th \<in> ?A" using h_e.th_kept by auto
next
- show "th \<in> threads (t @ s)" by (simp add: h_t.th_kept)
- next
- show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced)
- next
- show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))"
- by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def)
+ show "\<forall>x\<in>?A. ?f x \<le> ?f th"
+ proof
+ fix x
+ assume "x \<in> ?A"
+ hence "x \<in> threads (t@s)" by (simp add: Exit)
+ hence "?f x \<le> Max (?f ` threads (t@s))"
+ by (simp add: h_t.finite_threads)
+ also have "... \<le> ?f th"
+ apply (simp add:Exit the_preced_def preced_def, fold preced_def)
+ using Cons.hyps(5) h_t.th_kept the_preced_def by auto
+ finally show "?f x \<le> ?f th" .
+ qed
qed
- from this[unfolded Cons(5)]
- have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" .
- moreover have "the_preced ((e # t) @ s) = the_preced (t@s)"
- by (auto simp:Exit the_preced_def preced_def)
- ultimately show ?thesis by (simp add:Exit)
- qed
+ also have "... = ?t" using h_e.th_kept the_preced_def by auto
+ finally show ?thesis .
+ qed
next
case (P thread cs)
with Cons
@@ -337,202 +343,158 @@
case (V thread cs)
with Cons
show ?thesis by (auto simp:preced_def the_preced_def)
- next (* ccc *)
+ next
case (Set thread prio')
- show ?thesis
- apply (unfold Set, simp, insert Cons(5)) (* ccc *)
- find_theorems priority Set
- find_theorems preced Set
+ show ?thesis (is "Max (?f ` ?A) = ?t")
proof -
- let ?B = "threads (t@s)"
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.set_diff_low[OF this] and Set
- have neq_thread: "thread \<noteq> th" and le_p: "prio' \<le> prio" by auto
- from Set have "Max (?f ` ?A) = Max (?f ` ?B)" by simp
- also have "\<dots> = ?t"
- proof(rule Max_eqI)
- fix y
- assume y_in: "y \<in> ?f ` ?B"
- then obtain th1 where
- th1_in: "th1 \<in> ?B" and eq_y: "y = ?f th1" by auto
- show "y \<le> ?t"
- proof(cases "th1 = thread")
- case True
- with neq_thread le_p eq_y Set
- show ?thesis
- apply (subst preced_th, insert lt_tm)
- by (auto simp:preced_def precedence_le_def)
- next
- case False
- with Set eq_y
- have "y = preced th1 (t@s)"
- by (simp add:preced_def)
- moreover have "\<dots> \<le> ?t"
- proof -
- from Cons
- have "?t = Max ((\<lambda> th'. preced th' (t@s)) ` (threads (t@s)))"
- by auto
- moreover have "preced th1 (t@s) \<le> \<dots>"
- proof(rule Max_ge)
- from th1_in
- show "preced th1 (t @ s) \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"
- by simp
- next
- show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
- proof -
- from Cons have "vt (t @ s)" by auto
- from finite_threads[OF this] show ?thesis by auto
- qed
+ have "Max (?f ` ?A) = ?f th"
+ proof(rule image_Max_eqI)
+ show "finite ?A" using h_e.finite_threads by auto
+ next
+ show "th \<in> ?A" using h_e.th_kept by auto
+ next
+ show "\<forall>x\<in>?A. ?f x \<le> ?f th"
+ proof
+ fix x
+ assume h: "x \<in> ?A"
+ show "?f x \<le> ?f th"
+ proof(cases "x = thread")
+ case True
+ moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"
+ proof -
+ have "the_preced (t @ s) th = Prc prio tm"
+ using h_t.th_kept preced_th by (simp add:the_preced_def)
+ moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto
+ ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)
qed
- ultimately show ?thesis by auto
+ ultimately show ?thesis
+ by (unfold Set, simp add:the_preced_def preced_def)
+ next
+ case False
+ then have "?f x = the_preced (t@s) x"
+ by (simp add:the_preced_def preced_def Set)
+ also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"
+ using Set h h_t.finite_threads by auto
+ also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def)
+ finally show ?thesis .
qed
- ultimately show ?thesis by auto
- qed
- next
- from Cons and finite_threads
- show "finite (?f ` ?B)" by auto
- next
- from Cons have "extend_highest_gen s th prio tm t" by auto
- from extend_highest_gen.th_kept [OF this]
- have h: "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .
- show "?t \<in> (?f ` ?B)"
- proof -
- from neq_thread Set h
- have "?t = ?f th" by (auto simp:preced_def)
- with h show ?thesis by auto
qed
qed
+ also have "... = ?t" using h_e.th_kept the_preced_def by auto
finally show ?thesis .
- qed
+ qed
qed
qed
-lemma max_preced: "preced th (t@s) = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))"
+lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"
by (insert th_kept max_kept, auto)
-lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))"
- (is "?L = ?R")
+text {*
+ The reason behind the following lemma is that:
+ Since @{term "cp"} is defined as the maximum precedence
+ of those threads contained in the sub-tree of node @{term "Th th"}
+ in @{term "RAG (t@s)"}, and all these threads are living threads, and
+ @{term "th"} is also among them, the maximum precedence of
+ them all must be the one for @{text "th"}.
+*}
+lemma th_cp_max_preced:
+ "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R")
proof -
- have "?L = cpreced (wq (t@s)) (t@s) th"
- by (unfold cp_eq_cpreced, simp)
- also have "\<dots> = ?R"
- proof(unfold cpreced_def)
- show "Max ((\<lambda>th. preced th (t @ s)) ` ({th} \<union> dependants (wq (t @ s)) th)) =
- Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
- (is "Max (?f ` ({th} \<union> ?A)) = Max (?f ` ?B)")
- proof(cases "?A = {}")
- case False
- have "Max (?f ` ({th} \<union> ?A)) = Max (insert (?f th) (?f ` ?A))" by simp
- moreover have "\<dots> = max (?f th) (Max (?f ` ?A))"
- proof(rule Max_insert)
- show "finite (?f ` ?A)"
- proof -
- from dependants_threads[OF vt_t]
- have "?A \<subseteq> threads (t@s)" .
- moreover from finite_threads[OF vt_t] have "finite \<dots>" .
- ultimately show ?thesis
- by (auto simp:finite_subset)
- qed
+ let ?f = "the_preced (t@s)"
+ have "?L = ?f th"
+ proof(unfold cp_alt_def, rule image_Max_eqI)
+ show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
+ proof -
+ have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} =
+ the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>
+ (\<exists> th'. n = Th th')}"
+ by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)
+ moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree)
+ ultimately show ?thesis by simp
+ qed
+ next
+ show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
+ by (auto simp:subtree_def)
+ next
+ show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.
+ the_preced (t @ s) x \<le> the_preced (t @ s) th"
+ proof
+ fix th'
+ assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
+ hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto
+ moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"
+ by (meson subtree_Field)
+ ultimately have "Th th' \<in> ..." by auto
+ hence "th' \<in> threads (t@s)"
+ proof
+ assume "Th th' \<in> {Th th}"
+ thus ?thesis using th_kept by auto
next
- from False show "(?f ` ?A) \<noteq> {}" by simp
+ assume "Th th' \<in> Field (RAG (t @ s))"
+ thus ?thesis using vat_t.not_in_thread_isolated by blast
qed
- moreover have "\<dots> = Max (?f ` ?B)"
- proof -
- from max_preced have "?f th = Max (?f ` ?B)" .
- moreover have "Max (?f ` ?A) \<le> \<dots>"
- proof(rule Max_mono)
- from False show "(?f ` ?A) \<noteq> {}" by simp
- next
- show "?f ` ?A \<subseteq> ?f ` ?B"
- proof -
- have "?A \<subseteq> ?B" by (rule dependants_threads[OF vt_t])
- thus ?thesis by auto
- qed
- next
- from finite_threads[OF vt_t]
- show "finite (?f ` ?B)" by simp
- qed
- ultimately show ?thesis
- by (auto simp:max_def)
- qed
- ultimately show ?thesis by auto
- next
- case True
- with max_preced show ?thesis by auto
+ thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"
+ by (metis Max_ge finite_imageI finite_threads image_eqI
+ max_kept th_kept the_preced_def)
qed
qed
+ also have "... = ?R" by (simp add: max_preced the_preced_def)
finally show ?thesis .
qed
lemma th_cp_max: "cp (t@s) th = Max (cp (t@s) ` threads (t@s))"
- by (unfold max_cp_eq[OF vt_t] th_cp_max_preced, simp)
+ using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger
lemma th_cp_preced: "cp (t@s) th = preced th s"
by (fold max_kept, unfold th_cp_max_preced, simp)
lemma preced_less:
- fixes th'
assumes th'_in: "th' \<in> threads s"
and neq_th': "th' \<noteq> th"
shows "preced th' s < preced th s"
-proof -
- have "preced th' s \<le> Max ((\<lambda>th'. preced th' s) ` threads s)"
- proof(rule Max_ge)
- from finite_threads [OF vt_s]
- show "finite ((\<lambda>th'. preced th' s) ` threads s)" by simp
- next
- from th'_in show "preced th' s \<in> (\<lambda>th'. preced th' s) ` threads s"
- by simp
- qed
- moreover have "preced th' s \<noteq> preced th s"
- proof
- assume "preced th' s = preced th s"
- from preced_unique[OF this th'_in] neq_th' threads_s
- show "False" by (auto simp:readys_def)
- qed
- ultimately show ?thesis using highest_preced_thread
- by auto
-qed
+ using assms
+by (metis Max.coboundedI finite_imageI highest not_le order.trans
+ preced_linorder rev_image_eqI threads_s vat_s.finite_threads
+ vat_s.le_cp)
+
+text {*
+ Counting of the number of @{term "P"} and @{term "V"} operations
+ is the cornerstone of a large number of the following proofs.
+ The reason is that this counting is quite easy to calculate and
+ convenient to use in the reasoning.
+
+ The following lemma shows that the counting controls whether
+ a thread is running or not.
+*}
lemma pv_blocked_pre:
- fixes th'
assumes th'_in: "th' \<in> threads (t@s)"
and neq_th': "th' \<noteq> th"
and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
shows "th' \<notin> runing (t@s)"
proof
- assume "th' \<in> runing (t@s)"
- hence "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))"
- by (auto simp:runing_def)
- with max_cp_readys_threads [OF vt_t]
- have "cp (t @ s) th' = Max (cp (t@s) ` threads (t@s))"
- by auto
- moreover from th_cp_max have "cp (t @ s) th = \<dots>" by simp
- ultimately have "cp (t @ s) th' = cp (t @ s) th" by simp
- moreover from th_cp_preced and th_kept have "\<dots> = preced th (t @ s)"
- by simp
- finally have h: "cp (t @ s) th' = preced th (t @ s)" .
+ assume otherwise: "th' \<in> runing (t@s)"
show False
proof -
- have "dependants (wq (t @ s)) th' = {}"
- by (rule count_eq_dependants [OF vt_t eq_pv])
- moreover have "preced th' (t @ s) \<noteq> preced th (t @ s)"
- proof
- assume "preced th' (t @ s) = preced th (t @ s)"
- hence "th' = th"
- proof(rule preced_unique)
- from th_kept show "th \<in> threads (t @ s)" by simp
- next
- from th'_in show "th' \<in> threads (t @ s)" by simp
+ have "th' = th"
+ proof(rule preced_unique)
+ show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
+ proof -
+ have "?L = cp (t@s) th'"
+ by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
+ also have "... = cp (t @ s) th" using otherwise
+ by (metis (mono_tags, lifting) mem_Collect_eq
+ runing_def th_cp_max vat_t.max_cp_readys_threads)
+ also have "... = ?R" by (metis th_cp_preced th_kept)
+ finally show ?thesis .
qed
- with assms show False by simp
- qed
- ultimately show ?thesis
- by (insert h, unfold cp_eq_cpreced cpreced_def, simp)
- qed
+ qed (auto simp: th'_in th_kept)
+ moreover have "th' \<noteq> th" using neq_th' .
+ ultimately show ?thesis by simp
+ qed
qed
-lemmas pv_blocked = pv_blocked_pre[folded detached_eq [OF vt_t]]
+lemmas pv_blocked = pv_blocked_pre[folded detached_eq]
lemma runing_precond_pre:
fixes th'
@@ -541,113 +503,102 @@
and neq_th': "th' \<noteq> th"
shows "th' \<in> threads (t@s) \<and>
cntP (t@s) th' = cntV (t@s) th'"
-proof -
- show ?thesis
- proof(induct rule:ind)
- case (Cons e t)
- from Cons
- have in_thread: "th' \<in> threads (t @ s)"
- and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
- from Cons have "extend_highest_gen s th prio tm t" by auto
- then have not_runing: "th' \<notin> runing (t @ s)"
- apply(rule extend_highest_gen.pv_blocked)
- using Cons(1) in_thread neq_th' not_holding
- apply(simp_all add: detached_eq)
- done
+proof(induct rule:ind)
+ case (Cons e t)
+ interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
+ interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
show ?case
proof(cases e)
- case (V thread cs)
- from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto
-
+ case (P thread cs)
show ?thesis
proof -
- from Cons and V have "step (t@s) (V thread cs)" by auto
- hence neq_th': "thread \<noteq> th'"
- proof(cases)
- assume "thread \<in> runing (t@s)"
- moreover have "th' \<notin> runing (t@s)" by fact
- ultimately show ?thesis by auto
+ have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
+ proof -
+ have "thread \<noteq> th'"
+ proof -
+ have "step (t@s) (P thread cs)" using Cons P by auto
+ thus ?thesis
+ proof(cases)
+ assume "thread \<in> runing (t@s)"
+ moreover have "th' \<notin> runing (t@s)" using Cons(5)
+ by (metis neq_th' vat_t.pv_blocked_pre)
+ ultimately show ?thesis by auto
+ qed
+ qed with Cons show ?thesis
+ by (unfold P, simp add:cntP_def cntV_def count_def)
qed
- with not_holding have cnt_eq: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
- by (unfold V, simp add:cntP_def cntV_def count_def)
- moreover from in_thread
- have in_thread': "th' \<in> threads ((e # t) @ s)" by (unfold V, simp)
+ moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp)
ultimately show ?thesis by auto
qed
next
- case (P thread cs)
- from Cons and P have "step (t@s) (P thread cs)" by auto
- hence neq_th': "thread \<noteq> th'"
- proof(cases)
- assume "thread \<in> runing (t@s)"
- moreover note not_runing
- ultimately show ?thesis by auto
- qed
- with Cons and P have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
- by (auto simp:cntP_def cntV_def count_def)
- moreover from Cons and P have in_thread': "th' \<in> threads ((e # t) @ s)"
- by auto
- ultimately show ?thesis by auto
- next
- case (Create thread prio')
- from Cons and Create have "step (t@s) (Create thread prio')" by auto
- hence neq_th': "thread \<noteq> th'"
- proof(cases)
- assume "thread \<notin> threads (t @ s)"
- moreover have "th' \<in> threads (t@s)" by fact
+ case (V thread cs)
+ show ?thesis
+ proof -
+ have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
+ proof -
+ have "thread \<noteq> th'"
+ proof -
+ have "step (t@s) (V thread cs)" using Cons V by auto
+ thus ?thesis
+ proof(cases)
+ assume "thread \<in> runing (t@s)"
+ moreover have "th' \<notin> runing (t@s)" using Cons(5)
+ by (metis neq_th' vat_t.pv_blocked_pre)
+ ultimately show ?thesis by auto
+ qed
+ qed with Cons show ?thesis
+ by (unfold V, simp add:cntP_def cntV_def count_def)
+ qed
+ moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp)
ultimately show ?thesis by auto
qed
- with Cons and Create
- have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
- by (auto simp:cntP_def cntV_def count_def)
- moreover from Cons and Create
- have in_thread': "th' \<in> threads ((e # t) @ s)" by auto
- ultimately show ?thesis by auto
+ next
+ case (Create thread prio')
+ show ?thesis
+ proof -
+ have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
+ proof -
+ have "thread \<noteq> th'"
+ proof -
+ have "step (t@s) (Create thread prio')" using Cons Create by auto
+ thus ?thesis using Cons(5) by (cases, auto)
+ qed with Cons show ?thesis
+ by (unfold Create, simp add:cntP_def cntV_def count_def)
+ qed
+ moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp)
+ ultimately show ?thesis by auto
+ qed
next
case (Exit thread)
- from Cons and Exit have "step (t@s) (Exit thread)" by auto
- hence neq_th': "thread \<noteq> th'"
- proof(cases)
- assume "thread \<in> runing (t @ s)"
- moreover note not_runing
+ show ?thesis
+ proof -
+ have neq_thread: "thread \<noteq> th'"
+ proof -
+ have "step (t@s) (Exit thread)" using Cons Exit by auto
+ thus ?thesis apply (cases) using Cons(5)
+ by (metis neq_th' vat_t.pv_blocked_pre)
+ qed
+ hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons
+ by (unfold Exit, simp add:cntP_def cntV_def count_def)
+ moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread
+ by (unfold Exit, simp)
ultimately show ?thesis by auto
qed
- with Cons and Exit
- have eq_cnt: "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'"
- by (auto simp:cntP_def cntV_def count_def)
- moreover from Cons and Exit and neq_th'
- have in_thread': "th' \<in> threads ((e # t) @ s)"
- by auto
- ultimately show ?thesis by auto
next
case (Set thread prio')
with Cons
show ?thesis
by (auto simp:cntP_def cntV_def count_def)
qed
- next
- case Nil
- with assms
- show ?case by auto
- qed
+next
+ case Nil
+ with assms
+ show ?case by auto
qed
-(*
-lemma runing_precond:
- fixes th'
- assumes th'_in: "th' \<in> threads s"
- and eq_pv: "cntP s th' = cntV s th'"
- and neq_th': "th' \<noteq> th"
- shows "th' \<notin> runing (t@s)"
-proof -
- from runing_precond_pre[OF th'_in eq_pv neq_th']
- have h1: "th' \<in> threads (t @ s)" and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
- from pv_blocked[OF h1 neq_th' h2]
- show ?thesis .
-qed
-*)
-
-lemmas runing_precond_pre_dtc = runing_precond_pre[folded detached_eq[OF vt_t] detached_eq[OF vt_s]]
+text {* Changing counting balance to detachedness *}
+lemmas runing_precond_pre_dtc = runing_precond_pre
+ [folded vat_t.detached_eq vat_s.detached_eq]
lemma runing_precond:
fixes th'
@@ -655,18 +606,11 @@
and neq_th': "th' \<noteq> th"
and is_runing: "th' \<in> runing (t@s)"
shows "cntP s th' > cntV s th'"
+ using assms
proof -
have "cntP s th' \<noteq> cntV s th'"
- proof
- assume eq_pv: "cntP s th' = cntV s th'"
- from runing_precond_pre[OF th'_in eq_pv neq_th']
- have h1: "th' \<in> threads (t @ s)"
- and h2: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
- from pv_blocked_pre[OF h1 neq_th' h2] have " th' \<notin> runing (t @ s)" .
- with is_runing show "False" by simp
- qed
- moreover from cnp_cnv_cncs[OF vt_s, of th']
- have "cntV s th' \<le> cntP s th'" by auto
+ by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in)
+ moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
ultimately show ?thesis by auto
qed
@@ -676,95 +620,44 @@
and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'"
shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and>
th' \<in> threads ((moment (i+j) t)@s)"
-proof(induct j)
- case (Suc k)
- show ?case
- proof -
- { assume True: "Suc (i+k) \<le> length t"
- from moment_head [OF this]
- obtain e where
- eq_me: "moment (Suc(i+k)) t = e#(moment (i+k) t)"
- by blast
- from red_moment[of "Suc(i+k)"]
- and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp
- hence vt_e: "vt (e#(moment (i + k) t)@s)"
- by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
- highest_gen_def, auto)
- have not_runing': "th' \<notin> runing (moment (i + k) t @ s)"
- proof -
- show "th' \<notin> runing (moment (i + k) t @ s)"
- proof(rule extend_highest_gen.pv_blocked)
- from Suc show "th' \<in> threads (moment (i + k) t @ s)"
- by simp
- next
- from neq_th' show "th' \<noteq> th" .
- next
- from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" .
- next
- from Suc vt_e show "detached (moment (i + k) t @ s) th'"
- apply(subst detached_eq)
- apply(auto intro: vt_e evt_cons)
- done
- qed
- qed
- from step_back_step[OF vt_e]
- have "step ((moment (i + k) t)@s) e" .
- hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and>
- th' \<in> threads (e#(moment (i + k) t)@s)"
- proof(cases)
- case (thread_create thread prio)
- with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_exit thread)
- moreover have "thread \<noteq> th'"
- proof -
- have "thread \<in> runing (moment (i + k) t @ s)" by fact
- moreover note not_runing'
- ultimately show ?thesis by auto
- qed
- moreover note Suc
- ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_P thread cs)
- moreover have "thread \<noteq> th'"
- proof -
- have "thread \<in> runing (moment (i + k) t @ s)" by fact
- moreover note not_runing'
- ultimately show ?thesis by auto
- qed
- moreover note Suc
- ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_V thread cs)
- moreover have "thread \<noteq> th'"
- proof -
- have "thread \<in> runing (moment (i + k) t @ s)" by fact
- moreover note not_runing'
- ultimately show ?thesis by auto
- qed
- moreover note Suc
- ultimately show ?thesis by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_set thread prio')
- with Suc show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- qed
- with eq_me have ?thesis using eq_me by auto
- } note h = this
- show ?thesis
- proof(cases "Suc (i+k) \<le> length t")
- case True
- from h [OF this] show ?thesis .
- next
- case False
- with moment_ge
- have eq_m: "moment (i + Suc k) t = moment (i+k) t" by auto
- with Suc show ?thesis by auto
- qed
+proof -
+ interpret h_i: red_extend_highest_gen _ _ _ _ _ i
+ by (unfold_locales)
+ interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j"
+ by (unfold_locales)
+ interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)"
+ proof(unfold_locales)
+ show "vt (moment i t @ s)" by (metis h_i.vt_t)
+ next
+ show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept)
+ next
+ show "preced th (moment i t @ s) =
+ Max (cp (moment i t @ s) ` threads (moment i t @ s))"
+ by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept)
+ next
+ show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th)
+ next
+ show "vt (moment j (restm i t) @ moment i t @ s)"
+ using moment_plus_split by (metis add.commute append_assoc h_j.vt_t)
+ next
+ fix th' prio'
+ assume "Create th' prio' \<in> set (moment j (restm i t))"
+ thus "prio' \<le> prio" using assms
+ by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append)
+ next
+ fix th' prio'
+ assume "Set th' prio' \<in> set (moment j (restm i t))"
+ thus "th' \<noteq> th \<and> prio' \<le> prio"
+ by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append)
+ next
+ fix th'
+ assume "Exit th' \<in> set (moment j (restm i t))"
+ thus "th' \<noteq> th"
+ by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append)
qed
-next
- case 0
- from assms show ?case by auto
+ show ?thesis
+ by (metis add.commute append_assoc eq_pv h.runing_precond_pre
+ moment_plus_split neq_th' th'_in)
qed
lemma moment_blocked_eqpv:
@@ -778,14 +671,19 @@
proof -
from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
- and h2: "th' \<in> threads ((moment j t)@s)" by auto
- with extend_highest_gen.pv_blocked
- show ?thesis
- using red_moment [of j] h2 neq_th' h1
- apply(auto)
- by (metis extend_highest_gen.pv_blocked_pre)
+ and h2: "th' \<in> threads ((moment j t)@s)" by auto
+ moreover have "th' \<notin> runing ((moment j t)@s)"
+ proof -
+ interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
+ show ?thesis
+ using h.pv_blocked_pre h1 h2 neq_th' by auto
+ qed
+ ultimately show ?thesis by auto
qed
+(* The foregoing two lemmas are preparation for this one, but
+ in long run can be combined. Maybe I am wrong.
+*)
lemma moment_blocked:
assumes neq_th': "th' \<noteq> th"
and th'_in: "th' \<in> threads ((moment i t)@s)"
@@ -795,71 +693,119 @@
th' \<in> threads ((moment j t)@s) \<and>
th' \<notin> runing ((moment j t)@s)"
proof -
- from vt_moment[OF vt_t, of "i+length s"] moment_prefix[of i t s]
- have vt_i: "vt (moment i t @ s)" by auto
- from vt_moment[OF vt_t, of "j+length s"] moment_prefix[of j t s]
- have vt_j: "vt (moment j t @ s)" by auto
- from moment_blocked_eqpv [OF neq_th' th'_in detached_elim [OF vt_i dtc] le_ij,
- folded detached_eq[OF vt_j]]
- show ?thesis .
+ interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
+ interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales)
+ have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'"
+ by (metis dtc h_i.detached_elim)
+ from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]
+ show ?thesis by (metis h_j.detached_intro)
qed
-lemma runing_inversion_1:
+lemma runing_preced_inversion:
+ assumes runing': "th' \<in> runing (t@s)"
+ shows "cp (t@s) th' = preced th s" (is "?L = ?R")
+proof -
+ have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
+ by (unfold runing_def, auto)
+ also have "\<dots> = ?R"
+ by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
+ finally show ?thesis .
+qed
+
+text {*
+ The situation when @{term "th"} is blocked is analyzed by the following lemmas.
+*}
+
+text {*
+ The following lemmas shows the running thread @{text "th'"}, if it is different from
+ @{term th}, must be live at the very beginning. By the term {\em the very beginning},
+ we mean the moment where the formal investigation starts, i.e. the moment (or state)
+ @{term s}.
+*}
+
+lemma runing_inversion_0:
assumes neq_th': "th' \<noteq> th"
and runing': "th' \<in> runing (t@s)"
- shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
-proof(cases "th' \<in> threads s")
- case True
- with runing_precond [OF this neq_th' runing'] show ?thesis by simp
-next
- case False
- let ?Q = "\<lambda> t. th' \<in> threads (t@s)"
- let ?q = "moment 0 t"
- from moment_eq and False have not_thread: "\<not> ?Q ?q" by simp
- from runing' have "th' \<in> threads (t@s)" by (simp add:runing_def readys_def)
- from p_split_gen [of ?Q, OF this not_thread]
- obtain i where lt_its: "i < length t"
- and le_i: "0 \<le> i"
- and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")
- and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by auto
- from lt_its have "Suc i \<le> length t" by auto
- from moment_head[OF this] obtain e where
- eq_me: "moment (Suc i) t = e # moment i t" by blast
- from red_moment[of "Suc i"] and eq_me
- have "extend_highest_gen s th prio tm (e # moment i t)" by simp
- hence vt_e: "vt (e#(moment i t)@s)"
- by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
- highest_gen_def, auto)
- from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" .
- from post[rule_format, of "Suc i"] and eq_me
- have not_in': "th' \<in> threads (e # moment i t@s)" by auto
- from create_pre[OF stp_i pre this]
- obtain prio where eq_e: "e = Create th' prio" .
- have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
- proof(rule cnp_cnv_eq)
- from step_back_vt [OF vt_e]
- show "vt (moment i t @ s)" .
- next
- from eq_e and stp_i
- have "step (moment i t @ s) (Create th' prio)" by simp
- thus "th' \<notin> threads (moment i t @ s)" by (cases, simp)
- qed
- with eq_e
- have "cntP ((e#moment i t)@s) th' = cntV ((e#moment i t)@s) th'"
- by (simp add:cntP_def cntV_def count_def)
- with eq_me[symmetric]
- have h1: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"
- by simp
- from eq_e have "th' \<in> threads ((e#moment i t)@s)" by simp
- with eq_me [symmetric]
- have h2: "th' \<in> threads (moment (Suc i) t @ s)" by simp
- from moment_blocked_eqpv [OF neq_th' h2 h1, of "length t"] and lt_its
- and moment_ge
- have "th' \<notin> runing (t @ s)" by auto
- with runing'
- show ?thesis by auto
+ shows "th' \<in> threads s"
+proof -
+ -- {* The proof is by contradiction: *}
+ { assume otherwise: "\<not> ?thesis"
+ have "th' \<notin> runing (t @ s)"
+ proof -
+ -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *}
+ have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def)
+ -- {* However, @{text "th'"} does not exist at very beginning. *}
+ have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise
+ by (metis append.simps(1) moment_zero)
+ -- {* Therefore, there must be a moment during @{text "t"}, when
+ @{text "th'"} came into being. *}
+ -- {* Let us suppose the moment being @{text "i"}: *}
+ from p_split_gen[OF th'_in th'_notin]
+ obtain i where lt_its: "i < length t"
+ and le_i: "0 \<le> i"
+ and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre")
+ and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto)
+ interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales)
+ interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales)
+ from lt_its have "Suc i \<le> length t" by auto
+ -- {* Let us also suppose the event which makes this change is @{text e}: *}
+ from moment_head[OF this] obtain e where
+ eq_me: "moment (Suc i) t = e # moment i t" by blast
+ hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t)
+ hence "PIP (moment i t @ s) e" by (cases, simp)
+ -- {* It can be derived that this event @{text "e"}, which
+ gives birth to @{term "th'"} must be a @{term "Create"}: *}
+ from create_pre[OF this, of th']
+ obtain prio where eq_e: "e = Create th' prio"
+ by (metis append_Cons eq_me lessI post pre)
+ have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto
+ have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'"
+ proof -
+ have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
+ by (metis h_i.cnp_cnv_eq pre)
+ thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def)
+ qed
+ show ?thesis
+ using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge
+ by auto
+ qed
+ with `th' \<in> runing (t@s)`
+ have False by simp
+ } thus ?thesis by auto
qed
+text {*
+ The second lemma says, if the running thread @{text th'} is different from
+ @{term th}, then this @{text th'} must in the possession of some resources
+ at the very beginning.
+
+ To ease the reasoning of resource possession of one particular thread,
+ we used two auxiliary functions @{term cntV} and @{term cntP},
+ which are the counters of @{term P}-operations and
+ @{term V}-operations respectively.
+ If the number of @{term V}-operation is less than the number of
+ @{term "P"}-operations, the thread must have some unreleased resource.
+*}
+
+lemma runing_inversion_1: (* ddd *)
+ assumes neq_th': "th' \<noteq> th"
+ and runing': "th' \<in> runing (t@s)"
+ -- {* thread @{term "th'"} is a live on in state @{term "s"} and
+ it has some unreleased resource. *}
+ shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
+proof -
+ -- {* The proof is a simple composition of @{thm runing_inversion_0} and
+ @{thm runing_precond}: *}
+ -- {* By applying @{thm runing_inversion_0} to assumptions,
+ it can be shown that @{term th'} is live in state @{term s}: *}
+ have "th' \<in> threads s" using runing_inversion_0[OF assms(1,2)] .
+ -- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}
+ with runing_precond [OF this neq_th' runing'] show ?thesis by simp
+qed
+
+text {*
+ The following lemma is just a rephrasing of @{thm runing_inversion_1}:
+*}
lemma runing_inversion_2:
assumes runing': "th' \<in> runing (t@s)"
shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
@@ -868,37 +814,11 @@
show ?thesis by auto
qed
-lemma runing_preced_inversion:
- assumes runing': "th' \<in> runing (t@s)"
- shows "cp (t@s) th' = preced th s"
-proof -
- from runing' have "cp (t@s) th' = Max (cp (t @ s) ` readys (t @ s))"
- by (unfold runing_def, auto)
- also have "\<dots> = preced th s"
- proof -
- from max_cp_readys_threads[OF vt_t]
- have "\<dots> = Max (cp (t @ s) ` threads (t @ s))" .
- also have "\<dots> = preced th s"
- proof -
- from max_kept
- and max_cp_eq [OF vt_t]
- show ?thesis by auto
- qed
- finally show ?thesis .
- qed
- finally show ?thesis .
-qed
-
lemma runing_inversion_3:
assumes runing': "th' \<in> runing (t@s)"
and neq_th: "th' \<noteq> th"
shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
-proof -
- from runing_inversion_2 [OF runing']
- and neq_th
- and runing_preced_inversion[OF runing']
- show ?thesis by auto
-qed
+ by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)
lemma runing_inversion_4:
assumes runing': "th' \<in> runing (t@s)"
@@ -906,83 +826,93 @@
shows "th' \<in> threads s"
and "\<not>detached s th'"
and "cp (t@s) th' = preced th s"
-using runing_inversion_3 [OF runing']
- and neq_th
- and runing_preced_inversion[OF runing']
-apply(auto simp add: detached_eq[OF vt_s])
-done
+ apply (metis neq_th runing' runing_inversion_2)
+ apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
+ by (metis neq_th runing' runing_inversion_3)
+
+
+text {*
+ Suppose @{term th} is not running, it is first shown that
+ there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
+ in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
+ Now, since @{term readys}-set is non-empty, there must be
+ one in it which holds the highest @{term cp}-value, which, by definition,
+ is the @{term runing}-thread. However, we are going to show more: this running thread
+ is exactly @{term "th'"}.
+ *}
+lemma th_blockedE: (* ddd *)
+ assumes "th \<notin> runing (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> runing (t@s)"
+proof -
+ -- {* According to @{thm vat_t.th_chain_to_ready}, either
+ @{term "th"} is in @{term "readys"} or there is path leading from it to
+ one thread in @{term "readys"}. *}
+ have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
+ using th_kept vat_t.th_chain_to_ready by auto
+ -- {* However, @{term th} can not be in @{term readys}, because otherwise, since
+ @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
+ moreover have "th \<notin> readys (t@s)"
+ using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+ -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
+ term @{term readys}: *}
+ ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
+ and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+ -- {* We are going to show that this @{term th'} is running. *}
+ have "th' \<in> runing (t@s)"
+ proof -
+ -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
+ have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+ proof -
+ have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
+ by (unfold cp_alt_def1, simp)
+ also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
+ proof(rule image_Max_subset)
+ show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
+ next
+ show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
+ by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread)
+ next
+ show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
+ by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+ next
+ show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
+ (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")
+ proof -
+ have "?L = the_preced (t @ s) ` threads (t @ s)"
+ by (unfold image_comp, rule image_cong, auto)
+ thus ?thesis using max_preced the_preced_def by auto
+ qed
+ qed
+ also have "... = ?R"
+ using th_cp_max th_cp_preced th_kept
+ the_preced_def vat_t.max_cp_readys_threads by auto
+ finally show ?thesis .
+ qed
+ -- {* Now, since @{term th'} holds the highest @{term cp}
+ and we have already show it is in @{term readys},
+ it is @{term runing} by definition. *}
+ with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def)
+ qed
+ -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
+ moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
+ ultimately show ?thesis using that by metis
+qed
+
+text {*
+ Now it is easy to see there is always a thread to run by case analysis
+ on whether thread @{term th} is running: if the answer is Yes, the
+ the running thread is obviously @{term th} itself; otherwise, the running
+ thread is the @{text th'} given by lemma @{thm th_blockedE}.
+*}
lemma live: "runing (t@s) \<noteq> {}"
-proof(cases "th \<in> runing (t@s)")
+proof(cases "th \<in> runing (t@s)")
case True thus ?thesis by auto
next
case False
- then have not_ready: "th \<notin> readys (t@s)"
- apply (unfold runing_def,
- insert th_cp_max max_cp_readys_threads[OF vt_t, symmetric])
- by auto
- from th_kept have "th \<in> threads (t@s)" by auto
- from th_chain_to_ready[OF vt_t this] and not_ready
- obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
- have "th' \<in> runing (t@s)"
- proof -
- have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"
- proof -
- have " Max ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')) =
- preced th (t@s)"
- proof(rule Max_eqI)
- fix y
- assume "y \<in> (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
- then obtain th1 where
- h1: "th1 = th' \<or> th1 \<in> dependants (wq (t @ s)) th'"
- and eq_y: "y = preced th1 (t@s)" by auto
- show "y \<le> preced th (t @ s)"
- proof -
- from max_preced
- have "preced th (t @ s) = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" .
- moreover have "y \<le> \<dots>"
- proof(rule Max_ge)
- from h1
- have "th1 \<in> threads (t@s)"
- proof
- assume "th1 = th'"
- with th'_in show ?thesis by (simp add:readys_def)
- next
- assume "th1 \<in> dependants (wq (t @ s)) th'"
- with dependants_threads [OF vt_t]
- show "th1 \<in> threads (t @ s)" by auto
- qed
- with eq_y show " y \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" by simp
- next
- from finite_threads[OF vt_t]
- show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))" by simp
- qed
- ultimately show ?thesis by auto
- qed
- next
- from finite_threads[OF vt_t] dependants_threads [OF vt_t, of th']
- show "finite ((\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th'))"
- by (auto intro:finite_subset)
- next
- from dp
- have "th \<in> dependants (wq (t @ s)) th'"
- by (unfold cs_dependants_def, auto simp:eq_RAG)
- thus "preced th (t @ s) \<in>
- (\<lambda>th. preced th (t @ s)) ` ({th'} \<union> dependants (wq (t @ s)) th')"
- by auto
- qed
- moreover have "\<dots> = Max (cp (t @ s) ` readys (t @ s))"
- proof -
- from max_preced and max_cp_eq[OF vt_t, symmetric]
- have "preced th (t @ s) = Max (cp (t @ s) ` threads (t @ s))" by simp
- with max_cp_readys_threads[OF vt_t] show ?thesis by simp
- qed
- ultimately show ?thesis by (unfold cp_eq_cpreced cpreced_def, simp)
- qed
- with th'_in show ?thesis by (auto simp:runing_def)
- qed
- thus ?thesis by auto
+ thus ?thesis using th_blockedE by auto
qed
end
--- a/Precedence_ord.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/Precedence_ord.thy Wed Jan 06 20:46:14 2016 +0800
@@ -14,6 +14,19 @@
(Prc fx sx, Prc fy sy) \<Rightarrow>
fx < fy \<or> (fx \<le> fy \<and> sy \<le> sx))"
+lemma preced_leI1[intro]:
+ assumes "fx < fy"
+ shows "Prc fx sx \<le> Prc fy sy"
+ using assms
+ by (simp add: precedence_le_def)
+
+lemma preced_leI2[intro]:
+ assumes "fx \<le> fy"
+ and "sy \<le> sx"
+ shows "Prc fx sx \<le> Prc fy sy"
+ using assms
+ by (simp add: precedence_le_def)
+
definition
precedence_less_def: "x < y \<longleftrightarrow> (case (x, y) of
(Prc fx sx, Prc fy sy) \<Rightarrow>
--- a/PrioG.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/PrioG.thy Wed Jan 06 20:46:14 2016 +0800
@@ -2,6 +2,20 @@
imports PrioGDef
begin
+locale valid_trace =
+ fixes s
+ assumes vt : "vt s"
+
+locale valid_trace_e = valid_trace +
+ fixes e
+ assumes vt_e: "vt (e#s)"
+begin
+
+lemma pip_e: "PIP s e"
+ using vt_e by (cases, simp)
+
+end
+
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -16,8 +30,30 @@
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
-proof(erule_tac vt.induct, simp add:wq_def)
+context valid_trace
+begin
+
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+ assumes "PP []"
+ and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
+ PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+ shows "PP s"
+proof(rule vt.induct[OF vt])
+ from assms(1) show "PP []" .
+next
+ fix s e
+ assume h: "vt s" "PP s" "PIP s e"
+ show "PP (e # s)"
+ proof(cases rule:assms(2))
+ from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
+ next
+ from h(1,3) have "vt (e#s)" by auto
+ thus "valid_trace (e # s)" by (unfold_locales, simp)
+ qed (insert h, auto)
+qed
+
+lemma wq_distinct: "distinct (wq s cs)"
+proof(rule ind, simp add:wq_def)
fix s e
assume h1: "step s e"
and h2: "distinct (wq s cs)"
@@ -51,6 +87,12 @@
qed
qed
+end
+
+
+context valid_trace_e
+begin
+
text {*
The following lemma shows that only the @{text "P"}
operation can add new thread into waiting queues.
@@ -59,9 +101,7 @@
*}
lemma block_pre:
- fixes thread cs s
- assumes vt_e: "vt (e#s)"
- and s_ni: "thread \<notin> set (wq s cs)"
+ assumes s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof -
@@ -85,7 +125,7 @@
by (auto simp:wq_def Let_def split:if_splits)
next
case (V th cs)
- with assms show ?thesis
+ with vt_e assms show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
@@ -98,7 +138,7 @@
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and h2[symmetric, folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -112,6 +152,8 @@
qed
qed
+end
+
text {*
The following lemmas is also obvious and shallow. It says
that only running thread can request for a critical resource
@@ -126,7 +168,6 @@
by auto
lemma abs1:
- fixes e es
assumes ein: "e \<in> set es"
and neq: "hd es \<noteq> hd (es @ [x])"
shows "False"
@@ -141,15 +182,17 @@
inductive_cases evt_cons: "vt (a#s)"
+context valid_trace_e
+begin
+
lemma abs2:
- assumes vt: "vt (e#s)"
- and inq: "thread \<in> set (wq s cs)"
+ assumes inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
and inq': "thread \<in> set (wq (e#s) cs)"
shows "False"
proof -
- from assms show "False"
+ from vt_e assms show "False"
apply (cases e)
apply ((simp split:if_splits add:Let_def wq_def)[1])+
apply (insert abs1, fast)[1]
@@ -161,13 +204,13 @@
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs]
+ from wq_distinct[of cs]
and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
moreover have "thread \<in> set qs"
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and eq_wq [folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -181,28 +224,33 @@
qed
qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-proof(induct s, simp)
- fix a s t
- assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
- and vt_a: "vt (a # s)"
- show "vt (moment t (a # s))"
- proof(cases "t \<ge> length (a#s)")
+end
+
+context valid_trace
+begin
+
+lemma vt_moment: "\<And> t. vt (moment t s)"
+proof(induct rule:ind)
+ case Nil
+ thus ?case by (simp add:vt_nil)
+next
+ case (Cons s e t)
+ show ?case
+ proof(cases "t \<ge> length (e#s)")
case True
- from True have "moment t (a#s) = a#s" by simp
- with vt_a show ?thesis by simp
+ from True have "moment t (e#s) = e#s" by simp
+ thus ?thesis using Cons
+ by (simp add:valid_trace_def)
next
case False
- hence le_t1: "t \<le> length s" by simp
- from vt_a have "vt s"
- by (erule_tac evt_cons, simp)
- from h [OF this] have "vt (moment t s)" .
- moreover have "moment t (a#s) = moment t s"
+ from Cons have "vt (moment t s)" by simp
+ moreover have "moment t (e#s) = moment t s"
proof -
- from moment_app [OF le_t1, of "[a]"]
+ from False have "t \<le> length s" by simp
+ from moment_app [OF this, of "[e]"]
show ?thesis by simp
qed
- ultimately show ?thesis by auto
+ ultimately show ?thesis by simp
qed
qed
@@ -244,9 +292,7 @@
*}
lemma waiting_unique_pre:
- fixes cs1 cs2 s thread
- assumes vt: "vt s"
- and h11: "thread \<in> set (wq s cs1)"
+ assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
and h22: "thread \<noteq> hd (wq s cs2)"
@@ -282,25 +328,26 @@
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- have vt_e: "vt (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t2 s" "e"
+ by (unfold_locales, auto, cases, simp)
have ?thesis
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
- by auto
- thm abs2
- from abs2 [OF vt_e True eq_th h2 h1]
+ by auto
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre[OF False h1]
have "e = P thread cs2" .
- with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
+ with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
with runing_ready have "thread \<in> readys (moment t2 s)" by auto
with nn1 [rule_format, OF lt12]
@@ -316,24 +363,26 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt (e#moment t1 s)"
+ have "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 True eq_th h2 h1
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have "e = P thread cs1" .
- with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
+ with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
with runing_ready have "thread \<in> readys (moment t1 s)" by auto
with nn2 [rule_format, OF lt12]
@@ -351,20 +400,22 @@
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have vt_e: "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have eq_e1: "e = P thread cs1" .
have lt_t3: "t1 < ?t3" by simp
with eqt12 have "t2 < ?t3" by simp
@@ -377,17 +428,21 @@
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
- from abs2 [OF this True eq_th h2 h1]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.abs2 [OF True eq_th h2 h1]
show ?thesis .
next
case False
- have vt_e: "vt (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt] eqt12
+ from vt_moment eqt12
have "vt (moment (Suc t2) s)" by auto
with eq_m eqt12 show ?thesis by simp
qed
- from block_pre [OF vt_e False h1]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.block_pre [OF False h1]
have "e = P thread cs2" .
with eq_e1 neq12 show ?thesis by auto
qed
@@ -401,15 +456,15 @@
*}
lemma waiting_unique:
- fixes s cs1 cs2
- assumes "vt s"
- and "waiting s th cs1"
+ assumes "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
using waiting_unique_pre assms
unfolding wq_def s_waiting_def
by auto
+end
+
(* not used *)
text {*
Every thread can only be blocked on one critical resource,
@@ -417,13 +472,10 @@
This fact is much more easier according to our definition.
*}
lemma held_unique:
- fixes s::"state"
- assumes "holding s th1 cs"
+ assumes "holding (s::event list) th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
-using assms
-unfolding s_holding_def
-by auto
+ by (insert assms, unfold s_holding_def, auto)
lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
@@ -642,6 +694,8 @@
assume vt: "vt (V th cs # s)"
and nw: "\<not> waiting (wq (V th cs # s)) t c"
and wt: "waiting (wq s) t c"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp)
show "next_th s th cs t \<and> cs = c"
proof(cases "cs = c")
case False
@@ -659,7 +713,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -673,7 +727,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -704,6 +758,8 @@
proof -
assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
from step_back_step [OF vt] and hd
show "False"
proof(cases)
@@ -719,7 +775,7 @@
\<in> set (SOME q. distinct q \<and> set q = set list)"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -727,7 +783,7 @@
qed
moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show ?thesis by auto
qed
moreover note eq_wq and hd_in
@@ -747,9 +803,11 @@
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
\<notin> set (SOME q. distinct q \<and> set q = set rest)"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[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"
@@ -791,6 +849,8 @@
let ?s' = "(V th cs # s)"
assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
show "waiting (wq s) t c"
proof(cases "c = cs")
case False
@@ -809,7 +869,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -827,7 +887,7 @@
assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
moreover have "\<dots> = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -836,7 +896,7 @@
qed
ultimately show "t \<in> set list" by simp
qed
- with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+ with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
show False by auto
qed
qed
@@ -885,19 +945,22 @@
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
+context valid_trace
+begin
+
text {*
The following lemma shows that @{text "RAG"} is acyclic.
The overall structure is by induction on the formation of @{text "vt s"}
and then case analysis on event @{text "e"}, where the non-trivial cases
for those for @{text "V"} and @{text "P"} events.
*}
-lemma acyclic_RAG:
- fixes s
- assumes vt: "vt s"
+lemma acyclic_RAG:
shows "acyclic (RAG s)"
-using assms
+using vt
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "acyclic (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -949,8 +1012,8 @@
hence wt_th': "waiting s ?th' cs'"
unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
hence "cs' = cs"
- proof(rule waiting_unique [OF vt])
- from eq_wq wq_distinct[OF vt, of cs]
+ proof(rule vt_s.waiting_unique)
+ from eq_wq vt_s.wq_distinct[of cs]
show "waiting s ?th' cs"
apply (unfold s_waiting_def wq_def, auto)
proof -
@@ -958,7 +1021,7 @@
and eq_wq: "wq_fun (schs s) cs = th # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -968,7 +1031,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -980,7 +1043,7 @@
and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[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"
@@ -990,7 +1053,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and 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
@@ -1066,14 +1129,14 @@
qed
-lemma finite_RAG:
- fixes s
- assumes vt: "vt s"
+lemma finite_RAG:
shows "finite (RAG s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "finite (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -1145,32 +1208,35 @@
text {* Several useful lemmas *}
lemma wf_dep_converse:
- fixes s
- assumes vt: "vt s"
shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
- from finite_RAG [OF vt]
+ from finite_RAG
show "finite (RAG s)" .
next
- from acyclic_RAG[OF vt]
+ from acyclic_RAG
show "acyclic (RAG s)" .
qed
+end
+
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
-by (induct l, auto)
+ by (induct l, auto)
lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
+context valid_trace
+begin
+
lemma wq_threads:
- fixes s cs
- assumes vt: "vt s"
- and h: "th \<in> set (wq s cs)"
+ assumes h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
from vt and h show ?thesis
proof(induct arbitrary: th cs)
case (vt_cons s e)
+ interpret vt_s: valid_trace s
+ using vt_cons(1) by (unfold_locales, auto)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
and vt: "vt s"
@@ -1227,7 +1293,7 @@
assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def]
+ from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
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"
@@ -1264,14 +1330,13 @@
qed
qed
-lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
- assumes vt: "vt s"
- and neq_th: "th \<noteq> thread"
+ assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
@@ -1292,7 +1357,7 @@
and eq_wq: "wq_fun (schs s) cs = thread # rest"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
+ from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
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
@@ -1308,10 +1373,9 @@
*}
lemma chain_building:
- assumes vt: "vt s"
shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
proof -
- from wf_dep_converse [OF vt]
+ from wf_dep_converse
have h: "wf ((RAG s)\<inverse>)" .
show ?thesis
proof(induct rule:wf_induct [OF h])
@@ -1342,7 +1406,7 @@
from True and th'_d show ?thesis by auto
next
case False
- from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
+ from th'_d and range_in have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (RAG s)"
by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
@@ -1362,9 +1426,7 @@
The following is just an instance of @{text "chain_building"}.
*}
lemma th_chain_to_ready:
- fixes s th
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
proof(cases "th \<in> readys s")
case True
@@ -1373,10 +1435,12 @@
case False
from False and th_in have "Th th \<in> Domain (RAG s)"
by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
- from chain_building [rule_format, OF vt this]
+ from chain_building [rule_format, OF this]
show ?thesis by auto
qed
+end
+
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
by (unfold s_waiting_def cs_waiting_def wq_def, auto)
@@ -1386,16 +1450,24 @@
lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
by (unfold s_holding_def cs_holding_def, auto)
-lemma unique_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+context valid_trace
+begin
+
+lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique holding_unique)
+end
+
+
lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)
+context valid_trace
+begin
+
lemma dchain_unique:
- assumes vt: "vt s"
- and th1_d: "(n, Th th1) \<in> (RAG s)^+"
+ assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (RAG s)^+"
and th2_r: "th2 \<in> readys s"
@@ -1403,7 +1475,7 @@
proof -
{ assume neq: "th1 \<noteq> th2"
hence "Th th1 \<noteq> Th th2" by simp
- from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt]
+ from unique_chain [OF _ th1_d th2_d this] and unique_RAG
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
hence "False"
proof
@@ -1427,6 +1499,8 @@
qed
} thus ?thesis by auto
qed
+
+end
lemma step_holdents_p_add:
@@ -1450,13 +1524,11 @@
qed
-lemma finite_holding:
- fixes s th cs
- assumes vt: "vt s"
+lemma (in valid_trace) finite_holding :
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
- from finite_RAG [OF vt]
+ from finite_RAG
have "finite (RAG s)" .
hence "finite (?F `(RAG s))" by simp
moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>"
@@ -1476,13 +1548,17 @@
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
+ from vtv interpret vt_s: valid_trace s
+ by (cases, unfold_locales, simp)
+ from vtv interpret vt_v: valid_trace "V thread cs#s"
+ by (unfold_locales, simp)
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_test s_RAG_def, simp)
by (unfold cs_holding_def s_holding_def wq_def, auto)
moreover have cs_not_in:
"(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
- apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
+ apply (insert vt_s.wq_distinct[of cs])
apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
auto simp:next_th_def)
proof -
@@ -1536,7 +1612,7 @@
moreover have "card \<dots> =
Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vtv]
+ from vt_v.finite_holding
show " finite (holdents (V thread cs # s) thread)" .
qed
moreover from cs_not_in
@@ -1544,20 +1620,22 @@
ultimately show ?thesis by (simp add:cntCS_def)
qed
+context valid_trace
+begin
+
text {* (* ddd *) \noindent
The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
of one particular thread.
*}
lemma cnp_cnv_cncs:
- fixes s th
- assumes vt: "vt s"
shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
then cntCS s th else cntCS s th + 1)"
proof -
from vt show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. cntP s th = cntV s th +
(if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
@@ -1571,7 +1649,7 @@
proof -
{ fix cs
assume "thread \<in> set (wq s cs)"
- from wq_threads [OF vt this] have "thread \<in> threads s" .
+ from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
with not_in have "False" by simp
} with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
by (auto simp:readys_def threads.simps s_waiting_def
@@ -1632,6 +1710,8 @@
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
+ then interpret vt_p: valid_trace "(P thread cs#s)"
+ by (unfold_locales, simp)
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1679,7 +1759,7 @@
have "?L = insert cs ?R" by auto
moreover have "card \<dots> = Suc (card (?R - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vt, of thread]
+ from vt_s.finite_holding [of thread]
show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
by (unfold holdents_test, simp)
qed
@@ -1718,7 +1798,7 @@
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
hence "th = hd (wq s cs)" using False by auto
- with False eq_wq wq_distinct [OF vtp, of cs]
+ with False eq_wq vt_p.wq_distinct [of cs]
show False by (fold eq_e, auto)
qed
moreover from is_runing have "th \<in> threads (e#s)"
@@ -1737,6 +1817,7 @@
next
case (thread_V thread cs)
from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
@@ -1746,8 +1827,9 @@
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = 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
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
@@ -1782,8 +1864,9 @@
proof -
assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
with eq_set have "thread \<in> set rest" by simp
- with wq_distinct[OF step_back_vt[OF vtv], of cs]
- and eq_wq show False by auto
+ with vt_v.wq_distinct[of cs]
+ and eq_wq show False
+ by (metis distinct.simps(2) vt_s.wq_distinct)
qed
thus ?thesis by (simp add:wq_def s_waiting_def)
qed
@@ -1819,7 +1902,7 @@
case False
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
apply (insert step_back_vt[OF vtv])
- by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
+ by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
moreover have "cntCS (e#s) th = cntCS s th"
apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
proof -
@@ -1838,7 +1921,7 @@
" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+ from vt_s.wq_distinct[ 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"
@@ -1870,7 +1953,7 @@
have "\<not> th \<in> readys s"
apply (auto simp:readys_def s_waiting_def)
apply (rule_tac x = cs in exI, auto)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
+ by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
@@ -1885,7 +1968,7 @@
apply (unfold eq_e step_RAG_v[OF vtv],
auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def
Let_def cs_holding_def)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
+ by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
thus ?thesis by (simp add:cntCS_def)
qed
moreover note ih eq_cnp eq_cnv eq_threads
@@ -1902,7 +1985,7 @@
assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
show "?t \<in> threads s"
- proof(rule wq_threads[OF step_back_vt[OF vtv]])
+ proof(rule vt_s.wq_threads)
from eq_wq and t_in
show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
qed
@@ -1915,7 +1998,7 @@
show "?t = hd (wq_fun (schs s) csa)"
proof -
{ assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and
+ from vt_s.wq_distinct[of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto
with eq_wq and t_in
@@ -1924,7 +2007,7 @@
from t_in' neq_hd'
have w2: "waiting s ?t csa"
by (auto simp:s_waiting_def wq_def)
- from waiting_unique[OF step_back_vt[OF vtv] w1 w2]
+ from vt_s.waiting_unique[OF w1 w2]
and neq_cs have "False" by auto
} thus ?thesis by auto
qed
@@ -1942,7 +2025,7 @@
proof -
from th_in eq_wq
have "th \<in> set (wq s cs)" by simp
- from wq_threads [OF step_back_vt[OF vtv] this]
+ from vt_s.wq_threads [OF this]
show ?thesis .
qed
ultimately show ?thesis using ih by auto
@@ -1961,7 +2044,7 @@
have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)"
apply (auto simp:image_def)
by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
- with finite_RAG[OF step_back_vt[OF vtv]]
+ with vt_s.finite_RAG
show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
next
show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
@@ -2022,14 +2105,14 @@
qed
lemma not_thread_cncs:
- fixes th s
- assumes vt: "vt s"
- and not_in: "th \<notin> threads s"
+ assumes not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
@@ -2097,7 +2180,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
+ from assms thread_V vt stp ih
+ have vtv: "vt (V thread cs#s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs#s)"
+ by (unfold_locales, simp)
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)
@@ -2109,15 +2195,18 @@
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
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
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
+ from vt_s.wq_threads[OF this] and ni
+ show False
+ using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)`
+ ni vt_s.wq_threads by blast
qed
moreover note neq_th eq_wq
ultimately have "cntCS (e # s) th = cntCS s th"
@@ -2146,13 +2235,16 @@
qed
qed
+end
+
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
by (auto simp:s_waiting_def cs_waiting_def wq_def)
+context valid_trace
+begin
+
lemma dm_RAG_threads:
- fixes th s
- assumes vt: "vt s"
- and in_dom: "(Th th) \<in> Domain (RAG s)"
+ assumes in_dom: "(Th th) \<in> Domain (RAG s)"
shows "th \<in> threads s"
proof -
from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
@@ -2160,9 +2252,11 @@
ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
hence "th \<in> set (wq s cs)"
by (unfold s_RAG_def, auto simp:cs_waiting_def)
- from wq_threads [OF vt this] show ?thesis .
+ from wq_threads [OF this] show ?thesis .
qed
+end
+
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
@@ -2177,11 +2271,11 @@
apply(simp add: Let_def)
done
-(* FIXME: NOT NEEDED *)
+context valid_trace
+begin
+
lemma runing_unique:
- fixes th1 th2 s
- assumes vt: "vt s"
- and runing_1: "th1 \<in> runing s"
+ assumes runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
proof -
@@ -2210,7 +2304,7 @@
by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2254,7 +2348,7 @@
by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2289,7 +2383,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th1' = th1"
with runing_1 show ?thesis
@@ -2304,7 +2398,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th2' = th2"
with runing_2 show ?thesis
@@ -2366,7 +2460,7 @@
from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
show ?thesis
- proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
+ proof(rule dchain_unique[OF h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
qed
@@ -2375,7 +2469,7 @@
qed
-lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+lemma "card (runing s) \<le> 1"
apply(subgoal_tac "finite (runing s)")
prefer 2
apply (metis finite_nat_set_iff_bounded lessI runing_unique)
@@ -2389,6 +2483,9 @@
apply(auto)
done
+end
+
+
lemma create_pre:
assumes stp: "step s e"
and not_in: "th \<notin> threads s"
@@ -2447,28 +2544,35 @@
from that [OF this] show ?thesis .
qed
+context valid_trace
+begin
+
lemma cnp_cnv_eq:
- fixes th s
- assumes "vt s"
- and "th \<notin> threads s"
+ assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
- by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+ using assms
+ using cnp_cnv_cncs not_thread_cncs by auto
+
+end
+
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
+context valid_trace
+begin
+
lemma count_eq_dependants:
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "dependants (wq s) th = {}"
proof -
- from cnp_cnv_cncs[OF vt] and eq_pv
+ from cnp_cnv_cncs and eq_pv
have "cntCS s th = 0"
by (auto split:if_splits)
moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
proof -
- from finite_holding[OF vt, of th] show ?thesis
+ from finite_holding[of th] show ?thesis
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
@@ -2492,8 +2596,6 @@
qed
lemma dependants_threads:
- fixes s th
- assumes vt: "vt s"
shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
@@ -2505,7 +2607,7 @@
with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
thus ?thesis using eq_RAG by simp
qed
- from dm_RAG_threads[OF vt this]
+ from dm_RAG_threads[OF this]
have "th \<in> threads s" .
} note hh = this
fix th1
@@ -2516,10 +2618,10 @@
qed
lemma finite_threads:
- assumes vt: "vt s"
shows "finite (threads s)"
-using vt
-by (induct) (auto elim: step.cases)
+using vt by (induct) (auto elim: step.cases)
+
+end
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
@@ -2534,9 +2636,11 @@
from fnt and seq show "finite (f ` B)" by auto
qed
+context valid_trace
+begin
+
lemma cp_le:
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
@@ -2545,20 +2649,19 @@
proof(rule Max_f_mono)
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
next
- from finite_threads [OF vt]
+ from finite_threads
show "finite (threads s)" .
next
from th_in
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
- apply (rule_tac dm_RAG_threads[OF vt])
+ apply (rule_tac dm_RAG_threads)
apply (unfold trancl_domain [of "RAG s", symmetric])
by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
- assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (priority th s) (last_set th s)
@@ -2579,7 +2682,7 @@
by (rule_tac x = "(Th x, Th th)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2599,7 +2702,6 @@
qed
lemma max_cp_eq:
- assumes vt: "vt s"
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
@@ -2609,26 +2711,26 @@
case False
have "?l \<in> ((cp s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
next
from False show "cp s ` threads s \<noteq> {}" by auto
qed
then obtain th
where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
- have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in])
+ have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
proof -
have "?r \<in> (?f ` ?A)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
qed
then obtain th' where
th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
- from le_cp [OF vt, of th'] eq_r
+ from le_cp [of th'] eq_r
have "?r \<le> cp s th'" by auto
moreover have "\<dots> \<le> cp s th"
proof(fold eq_l)
@@ -2637,7 +2739,7 @@
from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
qed
qed
@@ -2647,23 +2749,22 @@
qed
lemma max_cp_readys_threads_pre:
- assumes vt: "vt s"
- and np: "threads s \<noteq> {}"
+ assumes np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
-proof(unfold max_cp_eq[OF vt])
+proof(unfold max_cp_eq)
show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
proof -
let ?p = "Max ((\<lambda>th. preced th s) ` threads s)"
let ?f = "(\<lambda>th. preced th s)"
have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt] show "finite (?f ` threads s)" by simp
+ from finite_threads show "finite (?f ` threads s)" by simp
next
from np show "?f ` threads s \<noteq> {}" by simp
qed
then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
by (auto simp:Image_def)
- from th_chain_to_ready [OF vt tm_in]
+ from th_chain_to_ready [OF tm_in]
have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
thus ?thesis
proof
@@ -2672,7 +2773,7 @@
and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
- from dependants_threads[OF vt] finite_threads[OF vt]
+ from dependants_threads finite_threads
show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
@@ -2680,10 +2781,10 @@
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- from p_in and th'_in and dependants_threads[OF vt, of th']
+ from p_in and th'_in and dependants_threads[of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
@@ -2710,18 +2811,18 @@
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
- from dependants_threads [OF vt, of th1] th1_in
+ from dependants_threads [of th1] th1_in
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
from th'_in
@@ -2741,16 +2842,16 @@
assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
- from hy' dependants_threads[OF vt, of tm]
+ from hy' dependants_threads[of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
} with hy show ?thesis by auto
qed
next
- from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+ from dependants_threads[of tm] finite_threads
show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
@@ -2761,7 +2862,7 @@
proof(rule Max_eqI)
from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
fix y assume "y \<in> cp s ` readys s"
@@ -2771,13 +2872,13 @@
apply(unfold cp_eq_p h)
apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
proof -
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
- from dependants_threads[OF vt, of th1] th1_readys
+ from dependants_threads[of th1] th1_readys
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
@@ -2794,7 +2895,6 @@
there must be one inside it has the maximum precedence of the whole system.
*}
lemma max_cp_readys_threads:
- assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
@@ -2802,9 +2902,10 @@
by (auto simp:readys_def)
next
case False
- show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
+ show ?thesis by (rule max_cp_readys_threads_pre[OF False])
qed
+end
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
apply (unfold s_holding_def cs_holding_def wq_def, simp)
@@ -2836,13 +2937,14 @@
apply(auto)
done
+context valid_trace
+begin
+
lemma detached_intro:
- fixes s th
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "detached s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_cnt: "cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
hence cncs_zero: "cntCS s th = 0"
@@ -2852,14 +2954,14 @@
thus ?thesis
proof
assume "th \<notin> threads s"
- with range_in[OF vt] dm_RAG_threads[OF vt]
+ with range_in dm_RAG_threads
show ?thesis
by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
next
assume "th \<in> readys s"
moreover have "Th th \<notin> Range (RAG s)"
proof -
- from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+ from card_0_eq [OF finite_holding] and cncs_zero
have "holdents s th = {}"
by (simp add:cntCS_def)
thus ?thesis
@@ -2874,12 +2976,10 @@
qed
lemma detached_elim:
- fixes s th
- assumes vt: "vt s"
- and dtc: "detached s th"
+ assumes dtc: "detached s th"
shows "cntP s th = cntV s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_pv: " cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
have cncs_z: "cntCS s th = 0"
@@ -2904,11 +3004,11 @@
qed
lemma detached_eq:
- fixes s th
- assumes vt: "vt s"
shows "(detached s th) = (cntP s th = cntV s th)"
by (insert vt, auto intro:detached_intro detached_elim)
+end
+
text {*
The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
from the concise and miniature model of PIP given in PrioGDef.thy.
@@ -2923,5 +3023,29 @@
shows "th1 = th2"
using assms by (unfold next_th_def, auto)
-
+lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+ apply (induct s, simp)
+proof -
+ fix a s
+ assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+ and eq_as: "a # s \<noteq> []"
+ show "last_set th (a # s) < length (a # s)"
+ proof(cases "s \<noteq> []")
+ case False
+ from False show ?thesis
+ by (cases a, auto simp:last_set.simps)
+ next
+ case True
+ from ih [OF True] show ?thesis
+ by (cases a, auto simp:last_set.simps)
+ qed
+qed
+
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+ by (induct s, auto simp:threads.simps)
+
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+ apply (drule_tac th_in_ne)
+ by (unfold preced_def, auto intro: birth_time_lt)
+
end
--- a/PrioG.thy~ Tue Dec 22 23:13:31 2015 +0800
+++ b/PrioG.thy~ Wed Jan 06 20:46:14 2016 +0800
@@ -2,6 +2,20 @@
imports PrioGDef
begin
+locale valid_trace =
+ fixes s
+ assumes vt : "vt s"
+
+locale valid_trace_e = valid_trace +
+ fixes e
+ assumes vt_e: "vt (e#s)"
+begin
+
+lemma pip_e: "PIP s e"
+ using vt_e by (cases, simp)
+
+end
+
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -16,8 +30,30 @@
"cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
-proof(erule_tac vt.induct, simp add:wq_def)
+context valid_trace
+begin
+
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+ assumes "PP []"
+ and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
+ PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+ shows "PP s"
+proof(rule vt.induct[OF vt])
+ from assms(1) show "PP []" .
+next
+ fix s e
+ assume h: "vt s" "PP s" "PIP s e"
+ show "PP (e # s)"
+ proof(cases rule:assms(2))
+ from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
+ next
+ from h(1,3) have "vt (e#s)" by auto
+ thus "valid_trace (e # s)" by (unfold_locales, simp)
+ qed (insert h, auto)
+qed
+
+lemma wq_distinct: "distinct (wq s cs)"
+proof(rule ind, simp add:wq_def)
fix s e
assume h1: "step s e"
and h2: "distinct (wq s cs)"
@@ -51,6 +87,12 @@
qed
qed
+end
+
+
+context valid_trace_e
+begin
+
text {*
The following lemma shows that only the @{text "P"}
operation can add new thread into waiting queues.
@@ -59,9 +101,7 @@
*}
lemma block_pre:
- fixes thread cs s
- assumes vt_e: "vt (e#s)"
- and s_ni: "thread \<notin> set (wq s cs)"
+ assumes s_ni: "thread \<notin> set (wq s cs)"
and s_i: "thread \<in> set (wq (e#s) cs)"
shows "e = P thread cs"
proof -
@@ -85,7 +125,7 @@
by (auto simp:wq_def Let_def split:if_splits)
next
case (V th cs)
- with assms show ?thesis
+ with vt_e assms show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
@@ -98,7 +138,7 @@
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and h2[symmetric, folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -112,6 +152,8 @@
qed
qed
+end
+
text {*
The following lemmas is also obvious and shallow. It says
that only running thread can request for a critical resource
@@ -126,7 +168,6 @@
by auto
lemma abs1:
- fixes e es
assumes ein: "e \<in> set es"
and neq: "hd es \<noteq> hd (es @ [x])"
shows "False"
@@ -141,15 +182,17 @@
inductive_cases evt_cons: "vt (a#s)"
+context valid_trace_e
+begin
+
lemma abs2:
- assumes vt: "vt (e#s)"
- and inq: "thread \<in> set (wq s cs)"
+ assumes inq: "thread \<in> set (wq s cs)"
and nh: "thread = hd (wq s cs)"
and qt: "thread \<noteq> hd (wq (e#s) cs)"
and inq': "thread \<in> set (wq (e#s) cs)"
shows "False"
proof -
- from assms show "False"
+ from vt_e assms show "False"
apply (cases e)
apply ((simp split:if_splits add:Let_def wq_def)[1])+
apply (insert abs1, fast)[1]
@@ -161,13 +204,13 @@
and eq_wq: "wq_fun (schs s) cs = thread # qs"
show "False"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs]
+ from wq_distinct[of cs]
and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
moreover have "thread \<in> set qs"
proof -
have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from wq_distinct [of cs]
and eq_wq [folded wq_def]
show "distinct qs \<and> set qs = set qs" by auto
next
@@ -181,28 +224,33 @@
qed
qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-proof(induct s, simp)
- fix a s t
- assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
- and vt_a: "vt (a # s)"
- show "vt (moment t (a # s))"
- proof(cases "t \<ge> length (a#s)")
+end
+
+context valid_trace
+begin
+
+lemma vt_moment: "\<And> t. vt (moment t s)"
+proof(induct rule:ind)
+ case Nil
+ thus ?case by (simp add:vt_nil)
+next
+ case (Cons s e t)
+ show ?case
+ proof(cases "t \<ge> length (e#s)")
case True
- from True have "moment t (a#s) = a#s" by simp
- with vt_a show ?thesis by simp
+ from True have "moment t (e#s) = e#s" by simp
+ thus ?thesis using Cons
+ by (simp add:valid_trace_def)
next
case False
- hence le_t1: "t \<le> length s" by simp
- from vt_a have "vt s"
- by (erule_tac evt_cons, simp)
- from h [OF this] have "vt (moment t s)" .
- moreover have "moment t (a#s) = moment t s"
+ from Cons have "vt (moment t s)" by simp
+ moreover have "moment t (e#s) = moment t s"
proof -
- from moment_app [OF le_t1, of "[a]"]
+ from False have "t \<le> length s" by simp
+ from moment_app [OF this, of "[e]"]
show ?thesis by simp
qed
- ultimately show ?thesis by auto
+ ultimately show ?thesis by simp
qed
qed
@@ -244,9 +292,7 @@
*}
lemma waiting_unique_pre:
- fixes cs1 cs2 s thread
- assumes vt: "vt s"
- and h11: "thread \<in> set (wq s cs1)"
+ assumes h11: "thread \<in> set (wq s cs1)"
and h12: "thread \<noteq> hd (wq s cs1)"
assumes h21: "thread \<in> set (wq s cs2)"
and h22: "thread \<noteq> hd (wq s cs2)"
@@ -282,25 +328,26 @@
from nn2 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
- have vt_e: "vt (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t2 s" "e"
+ by (unfold_locales, auto, cases, simp)
have ?thesis
proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
case True
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
- by auto
- thm abs2
- from abs2 [OF vt_e True eq_th h2 h1]
+ by auto
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre[OF False h1]
have "e = P thread cs2" .
- with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
+ with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
with runing_ready have "thread \<in> readys (moment t2 s)" by auto
with nn1 [rule_format, OF lt12]
@@ -316,24 +363,26 @@
from nn1 [rule_format, OF this] and eq_m
have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
- have vt_e: "vt (e#moment t1 s)"
+ have "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 True eq_th h2 h1
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have "e = P thread cs1" .
- with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
+ with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
with runing_ready have "thread \<in> readys (moment t1 s)" by auto
with nn2 [rule_format, OF lt12]
@@ -351,20 +400,22 @@
h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
have vt_e: "vt (e#moment t1 s)"
proof -
- from vt_moment [OF vt]
+ from vt_moment
have "vt (moment ?t3 s)" .
with eq_m show ?thesis by simp
qed
+ then interpret vt_e: valid_trace_e "moment t1 s" e
+ by (unfold_locales, auto, cases, auto)
have ?thesis
proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
case True
from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
by auto
- from abs2 [OF vt_e True eq_th h2 h1]
+ from vt_e.abs2 [OF True eq_th h2 h1]
show ?thesis by auto
next
case False
- from block_pre [OF vt_e False h1]
+ from vt_e.block_pre [OF False h1]
have eq_e1: "e = P thread cs1" .
have lt_t3: "t1 < ?t3" by simp
with eqt12 have "t2 < ?t3" by simp
@@ -377,17 +428,21 @@
from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
by auto
from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
- from abs2 [OF this True eq_th h2 h1]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.abs2 [OF True eq_th h2 h1]
show ?thesis .
next
case False
- have vt_e: "vt (e#moment t2 s)"
+ have "vt (e#moment t2 s)"
proof -
- from vt_moment [OF vt] eqt12
+ from vt_moment eqt12
have "vt (moment (Suc t2) s)" by auto
with eq_m eqt12 show ?thesis by simp
qed
- from block_pre [OF vt_e False h1]
+ then interpret vt_e2: valid_trace_e "moment t2 s" e
+ by (unfold_locales, auto, cases, auto)
+ from vt_e2.block_pre [OF False h1]
have "e = P thread cs2" .
with eq_e1 neq12 show ?thesis by auto
qed
@@ -401,15 +456,15 @@
*}
lemma waiting_unique:
- fixes s cs1 cs2
- assumes "vt s"
- and "waiting s th cs1"
+ assumes "waiting s th cs1"
and "waiting s th cs2"
shows "cs1 = cs2"
using waiting_unique_pre assms
unfolding wq_def s_waiting_def
by auto
+end
+
(* not used *)
text {*
Every thread can only be blocked on one critical resource,
@@ -417,13 +472,10 @@
This fact is much more easier according to our definition.
*}
lemma held_unique:
- fixes s::"state"
- assumes "holding s th1 cs"
+ assumes "holding (s::event list) th1 cs"
and "holding s th2 cs"
shows "th1 = th2"
-using assms
-unfolding s_holding_def
-by auto
+ by (insert assms, unfold s_holding_def, auto)
lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
@@ -642,6 +694,8 @@
assume vt: "vt (V th cs # s)"
and nw: "\<not> waiting (wq (V th cs # s)) t c"
and wt: "waiting (wq s) t c"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp)
show "next_th s th cs t \<and> cs = c"
proof(cases "cs = c")
case False
@@ -659,7 +713,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -673,7 +727,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have " set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+ from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -704,6 +758,8 @@
proof -
assume vt: "vt (V th cs # s)"
and hd: "holding (wq (V th cs # s)) th cs"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
from step_back_step [OF vt] and hd
show "False"
proof(cases)
@@ -719,7 +775,7 @@
\<in> set (SOME q. distinct q \<and> set q = set list)"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show "distinct list \<and> set list = set list" by auto
next
show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -727,7 +783,7 @@
qed
moreover have "distinct (hd (SOME q. distinct q \<and> set q = set list) # list)"
proof -
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[of cs] and eq_wq
show ?thesis by auto
qed
moreover note eq_wq and hd_in
@@ -747,9 +803,11 @@
and nrest: "rest \<noteq> []"
and ni: "hd (SOME q. distinct q \<and> set q = set rest)
\<notin> set (SOME q. distinct q \<and> set q = set rest)"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+ from vt_v.wq_distinct[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"
@@ -791,6 +849,8 @@
let ?s' = "(V th cs # s)"
assume vt: "vt ?s'"
and wt: "waiting (wq ?s') t c"
+ from vt interpret vt_v: valid_trace_e s "V th cs"
+ by (cases, unfold_locales, simp+)
show "waiting (wq s) t c"
proof(cases "c = cs")
case False
@@ -809,7 +869,7 @@
and eq_wq: "wq_fun (schs s) cs = a # list"
have "set (SOME q. distinct q \<and> set q = set list) = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -827,7 +887,7 @@
assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
moreover have "\<dots> = set list"
proof(rule someI2)
- from wq_distinct [OF step_back_vt[OF vt], of cs]
+ from vt_v.wq_distinct [of cs]
and eq_wq[folded wq_def]
show "distinct list \<and> set list = set list" by auto
next
@@ -836,7 +896,7 @@
qed
ultimately show "t \<in> set list" by simp
qed
- with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+ with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
show False by auto
qed
qed
@@ -885,19 +945,22 @@
lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_RAG_def, auto)
+context valid_trace
+begin
+
text {*
The following lemma shows that @{text "RAG"} is acyclic.
The overall structure is by induction on the formation of @{text "vt s"}
and then case analysis on event @{text "e"}, where the non-trivial cases
for those for @{text "V"} and @{text "P"} events.
*}
-lemma acyclic_RAG:
- fixes s
- assumes vt: "vt s"
+lemma acyclic_RAG:
shows "acyclic (RAG s)"
-using assms
+using vt
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "acyclic (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -949,8 +1012,8 @@
hence wt_th': "waiting s ?th' cs'"
unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
hence "cs' = cs"
- proof(rule waiting_unique [OF vt])
- from eq_wq wq_distinct[OF vt, of cs]
+ proof(rule vt_s.waiting_unique)
+ from eq_wq vt_s.wq_distinct[of cs]
show "waiting s ?th' cs"
apply (unfold s_waiting_def wq_def, auto)
proof -
@@ -958,7 +1021,7 @@
and eq_wq: "wq_fun (schs s) cs = th # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
fix x assume "distinct x \<and> set x = set rest"
@@ -968,7 +1031,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and eq_wq
show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -980,7 +1043,7 @@
and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[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"
@@ -990,7 +1053,7 @@
set (SOME q. distinct q \<and> set q = set rest)" by auto
moreover have "\<dots> = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs] and eq_wq
+ from vt_s.wq_distinct[of cs] and 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
@@ -1066,14 +1129,14 @@
qed
-lemma finite_RAG:
- fixes s
- assumes vt: "vt s"
+lemma finite_RAG:
shows "finite (RAG s)"
proof -
from vt show ?thesis
proof(induct)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume ih: "finite (RAG s)"
and stp: "step s e"
and vt: "vt s"
@@ -1145,32 +1208,35 @@
text {* Several useful lemmas *}
lemma wf_dep_converse:
- fixes s
- assumes vt: "vt s"
shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
- from finite_RAG [OF vt]
+ from finite_RAG
show "finite (RAG s)" .
next
- from acyclic_RAG[OF vt]
+ from acyclic_RAG
show "acyclic (RAG s)" .
qed
+end
+
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
-by (induct l, auto)
+ by (induct l, auto)
lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
+context valid_trace
+begin
+
lemma wq_threads:
- fixes s cs
- assumes vt: "vt s"
- and h: "th \<in> set (wq s cs)"
+ assumes h: "th \<in> set (wq s cs)"
shows "th \<in> threads s"
proof -
from vt and h show ?thesis
proof(induct arbitrary: th cs)
case (vt_cons s e)
+ interpret vt_s: valid_trace s
+ using vt_cons(1) by (unfold_locales, auto)
assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
and stp: "step s e"
and vt: "vt s"
@@ -1227,7 +1293,7 @@
assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def]
+ from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
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"
@@ -1264,14 +1330,13 @@
qed
qed
-lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
by (auto intro:wq_threads)
lemma readys_v_eq:
fixes th thread cs rest
- assumes vt: "vt s"
- and neq_th: "th \<noteq> thread"
+ assumes neq_th: "th \<noteq> thread"
and eq_wq: "wq s cs = thread#rest"
and not_in: "th \<notin> set rest"
shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
@@ -1292,7 +1357,7 @@
and eq_wq: "wq_fun (schs s) cs = thread # rest"
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
proof(rule someI2)
- from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
+ from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
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
@@ -1308,10 +1373,9 @@
*}
lemma chain_building:
- assumes vt: "vt s"
shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
proof -
- from wf_dep_converse [OF vt]
+ from wf_dep_converse
have h: "wf ((RAG s)\<inverse>)" .
show ?thesis
proof(induct rule:wf_induct [OF h])
@@ -1342,7 +1406,7 @@
from True and th'_d show ?thesis by auto
next
case False
- from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
+ from th'_d and range_in have "th' \<in> threads s" by auto
with False have "Th th' \<in> Domain (RAG s)"
by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
from ih [OF th'_d this]
@@ -1362,9 +1426,7 @@
The following is just an instance of @{text "chain_building"}.
*}
lemma th_chain_to_ready:
- fixes s th
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes th_in: "th \<in> threads s"
shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
proof(cases "th \<in> readys s")
case True
@@ -1373,10 +1435,12 @@
case False
from False and th_in have "Th th \<in> Domain (RAG s)"
by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
- from chain_building [rule_format, OF vt this]
+ from chain_building [rule_format, OF this]
show ?thesis by auto
qed
+end
+
lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
by (unfold s_waiting_def cs_waiting_def wq_def, auto)
@@ -1386,16 +1450,24 @@
lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
by (unfold s_holding_def cs_holding_def, auto)
-lemma unique_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+context valid_trace
+begin
+
+lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
by(auto elim:waiting_unique holding_unique)
+end
+
+
lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
by (induct rule:trancl_induct, auto)
+context valid_trace
+begin
+
lemma dchain_unique:
- assumes vt: "vt s"
- and th1_d: "(n, Th th1) \<in> (RAG s)^+"
+ assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
and th1_r: "th1 \<in> readys s"
and th2_d: "(n, Th th2) \<in> (RAG s)^+"
and th2_r: "th2 \<in> readys s"
@@ -1403,7 +1475,7 @@
proof -
{ assume neq: "th1 \<noteq> th2"
hence "Th th1 \<noteq> Th th2" by simp
- from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt]
+ from unique_chain [OF _ th1_d th2_d this] and unique_RAG
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
hence "False"
proof
@@ -1427,6 +1499,8 @@
qed
} thus ?thesis by auto
qed
+
+end
lemma step_holdents_p_add:
@@ -1450,13 +1524,11 @@
qed
-lemma finite_holding:
- fixes s th cs
- assumes vt: "vt s"
+lemma (in valid_trace) finite_holding :
shows "finite (holdents s th)"
proof -
let ?F = "\<lambda> (x, y). the_cs x"
- from finite_RAG [OF vt]
+ from finite_RAG
have "finite (RAG s)" .
hence "finite (?F `(RAG s))" by simp
moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>"
@@ -1476,13 +1548,17 @@
assumes vtv: "vt (V thread cs#s)"
shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
proof -
+ from vtv interpret vt_s: valid_trace s
+ by (cases, unfold_locales, simp)
+ from vtv interpret vt_v: valid_trace "V thread cs#s"
+ by (unfold_locales, simp)
from step_back_step[OF vtv]
have cs_in: "cs \<in> holdents s thread"
apply (cases, unfold holdents_test s_RAG_def, simp)
by (unfold cs_holding_def s_holding_def wq_def, auto)
moreover have cs_not_in:
"(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
- apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
+ apply (insert vt_s.wq_distinct[of cs])
apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
auto simp:next_th_def)
proof -
@@ -1536,7 +1612,7 @@
moreover have "card \<dots> =
Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vtv]
+ from vt_v.finite_holding
show " finite (holdents (V thread cs # s) thread)" .
qed
moreover from cs_not_in
@@ -1544,20 +1620,22 @@
ultimately show ?thesis by (simp add:cntCS_def)
qed
+context valid_trace
+begin
+
text {* (* ddd *) \noindent
The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
of one particular thread.
*}
lemma cnp_cnv_cncs:
- fixes s th
- assumes vt: "vt s"
shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
then cntCS s th else cntCS s th + 1)"
proof -
from vt show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e)
+ interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. cntP s th = cntV s th +
(if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
@@ -1571,7 +1649,7 @@
proof -
{ fix cs
assume "thread \<in> set (wq s cs)"
- from wq_threads [OF vt this] have "thread \<in> threads s" .
+ from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
with not_in have "False" by simp
} with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
by (auto simp:readys_def threads.simps s_waiting_def
@@ -1632,6 +1710,8 @@
and is_runing: "thread \<in> runing s"
and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
from thread_P vt stp ih have vtp: "vt (P thread cs#s)" by auto
+ then interpret vt_p: valid_trace "(P thread cs#s)"
+ by (unfold_locales, simp)
show ?thesis
proof -
{ have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1679,7 +1759,7 @@
have "?L = insert cs ?R" by auto
moreover have "card \<dots> = Suc (card (?R - {cs}))"
proof(rule card_insert)
- from finite_holding [OF vt, of thread]
+ from vt_s.finite_holding [of thread]
show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
by (unfold holdents_test, simp)
qed
@@ -1718,7 +1798,7 @@
ultimately have "th = hd (wq (e#s) cs)" by blast
with eq_wq have "th = hd (wq s cs @ [th])" by simp
hence "th = hd (wq s cs)" using False by auto
- with False eq_wq wq_distinct [OF vtp, of cs]
+ with False eq_wq vt_p.wq_distinct [of cs]
show False by (fold eq_e, auto)
qed
moreover from is_runing have "th \<in> threads (e#s)"
@@ -1737,6 +1817,7 @@
next
case (thread_V thread cs)
from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
assume eq_e: "e = V thread cs"
and is_runing: "thread \<in> runing s"
and hold: "holding s thread cs"
@@ -1746,8 +1827,9 @@
have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = 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
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
next
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
@@ -1782,8 +1864,9 @@
proof -
assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
with eq_set have "thread \<in> set rest" by simp
- with wq_distinct[OF step_back_vt[OF vtv], of cs]
- and eq_wq show False by auto
+ with vt_v.wq_distinct[of cs]
+ and eq_wq show False
+ by (metis distinct.simps(2) vt_s.wq_distinct)
qed
thus ?thesis by (simp add:wq_def s_waiting_def)
qed
@@ -1819,7 +1902,7 @@
case False
have "(th \<in> readys (e # s)) = (th \<in> readys s)"
apply (insert step_back_vt[OF vtv])
- by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
+ by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
moreover have "cntCS (e#s) th = cntCS s th"
apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
proof -
@@ -1838,7 +1921,7 @@
" by simp
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+ from vt_s.wq_distinct[ 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"
@@ -1870,7 +1953,7 @@
have "\<not> th \<in> readys s"
apply (auto simp:readys_def s_waiting_def)
apply (rule_tac x = cs in exI, auto)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
+ by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
moreover
from eq_wq and th_in and neq_hd
have "\<not> (th \<in> readys (e # s))"
@@ -1885,7 +1968,7 @@
apply (unfold eq_e step_RAG_v[OF vtv],
auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def
Let_def cs_holding_def)
- by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
+ by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
thus ?thesis by (simp add:cntCS_def)
qed
moreover note ih eq_cnp eq_cnv eq_threads
@@ -1902,7 +1985,7 @@
assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
show "?t \<in> threads s"
- proof(rule wq_threads[OF step_back_vt[OF vtv]])
+ proof(rule vt_s.wq_threads)
from eq_wq and t_in
show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
qed
@@ -1915,7 +1998,7 @@
show "?t = hd (wq_fun (schs s) csa)"
proof -
{ assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and
+ from vt_s.wq_distinct[of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto
with eq_wq and t_in
@@ -1924,7 +2007,7 @@
from t_in' neq_hd'
have w2: "waiting s ?t csa"
by (auto simp:s_waiting_def wq_def)
- from waiting_unique[OF step_back_vt[OF vtv] w1 w2]
+ from vt_s.waiting_unique[OF w1 w2]
and neq_cs have "False" by auto
} thus ?thesis by auto
qed
@@ -1942,7 +2025,7 @@
proof -
from th_in eq_wq
have "th \<in> set (wq s cs)" by simp
- from wq_threads [OF step_back_vt[OF vtv] this]
+ from vt_s.wq_threads [OF this]
show ?thesis .
qed
ultimately show ?thesis using ih by auto
@@ -1961,7 +2044,7 @@
have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)"
apply (auto simp:image_def)
by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
- with finite_RAG[OF step_back_vt[OF vtv]]
+ with vt_s.finite_RAG
show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
next
show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
@@ -2022,14 +2105,14 @@
qed
lemma not_thread_cncs:
- fixes th s
- assumes vt: "vt s"
- and not_in: "th \<notin> threads s"
+ assumes not_in: "th \<notin> threads s"
shows "cntCS s th = 0"
proof -
from vt not_in show ?thesis
proof(induct arbitrary:th)
case (vt_cons s e th)
+ interpret vt_s: valid_trace s using vt_cons(1)
+ by (unfold_locales, simp)
assume vt: "vt s"
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
and stp: "step s e"
@@ -2097,7 +2180,10 @@
by (simp add:runing_def readys_def)
ultimately show ?thesis by auto
qed
- from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
+ from assms thread_V vt stp ih
+ have vtv: "vt (V thread cs#s)" by auto
+ then interpret vt_v: valid_trace "(V thread cs#s)"
+ by (unfold_locales, simp)
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)
@@ -2109,15 +2195,18 @@
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
+ from vt_v.wq_distinct[of cs] and eq_wq
+ show "distinct rest \<and> set rest = set rest"
+ by (metis distinct.simps(2) vt_s.wq_distinct)
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
+ from vt_s.wq_threads[OF this] and ni
+ show False
+ using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)`
+ ni vt_s.wq_threads by blast
qed
moreover note neq_th eq_wq
ultimately have "cntCS (e # s) th = cntCS s th"
@@ -2146,13 +2235,16 @@
qed
qed
+end
+
lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
by (auto simp:s_waiting_def cs_waiting_def wq_def)
+context valid_trace
+begin
+
lemma dm_RAG_threads:
- fixes th s
- assumes vt: "vt s"
- and in_dom: "(Th th) \<in> Domain (RAG s)"
+ assumes in_dom: "(Th th) \<in> Domain (RAG s)"
shows "th \<in> threads s"
proof -
from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
@@ -2160,9 +2252,11 @@
ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
hence "th \<in> set (wq s cs)"
by (unfold s_RAG_def, auto simp:cs_waiting_def)
- from wq_threads [OF vt this] show ?thesis .
+ from wq_threads [OF this] show ?thesis .
qed
+end
+
lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
@@ -2177,11 +2271,11 @@
apply(simp add: Let_def)
done
-(* FIXME: NOT NEEDED *)
+context valid_trace
+begin
+
lemma runing_unique:
- fixes th1 th2 s
- assumes vt: "vt s"
- and runing_1: "th1 \<in> runing s"
+ assumes runing_1: "th1 \<in> runing s"
and runing_2: "th2 \<in> runing s"
shows "th1 = th2"
proof -
@@ -2210,7 +2304,7 @@
by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2254,7 +2348,7 @@
by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2289,7 +2383,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th1' = th1"
with runing_1 show ?thesis
@@ -2304,7 +2398,7 @@
apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
by (auto simp:Domain_def)
hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
- from dm_RAG_threads[OF vt this] show ?thesis .
+ from dm_RAG_threads[OF this] show ?thesis .
next
assume "th2' = th2"
with runing_2 show ?thesis
@@ -2366,7 +2460,7 @@
from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
show ?thesis
- proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
+ proof(rule dchain_unique[OF h1 _ h2, symmetric])
from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
qed
@@ -2375,7 +2469,7 @@
qed
-lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+lemma "card (runing s) \<le> 1"
apply(subgoal_tac "finite (runing s)")
prefer 2
apply (metis finite_nat_set_iff_bounded lessI runing_unique)
@@ -2389,6 +2483,9 @@
apply(auto)
done
+end
+
+
lemma create_pre:
assumes stp: "step s e"
and not_in: "th \<notin> threads s"
@@ -2447,28 +2544,35 @@
from that [OF this] show ?thesis .
qed
+context valid_trace
+begin
+
lemma cnp_cnv_eq:
- fixes th s
- assumes "vt s"
- and "th \<notin> threads s"
+ assumes "th \<notin> threads s"
shows "cntP s th = cntV s th"
- by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+ using assms
+ using cnp_cnv_cncs not_thread_cncs by auto
+
+end
+
lemma eq_RAG:
"RAG (wq s) = RAG s"
by (unfold cs_RAG_def s_RAG_def, auto)
+context valid_trace
+begin
+
lemma count_eq_dependants:
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "dependants (wq s) th = {}"
proof -
- from cnp_cnv_cncs[OF vt] and eq_pv
+ from cnp_cnv_cncs and eq_pv
have "cntCS s th = 0"
by (auto split:if_splits)
moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
proof -
- from finite_holding[OF vt, of th] show ?thesis
+ from finite_holding[of th] show ?thesis
by (simp add:holdents_test)
qed
ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
@@ -2492,8 +2596,6 @@
qed
lemma dependants_threads:
- fixes s th
- assumes vt: "vt s"
shows "dependants (wq s) th \<subseteq> threads s"
proof
{ fix th th'
@@ -2505,7 +2607,7 @@
with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
thus ?thesis using eq_RAG by simp
qed
- from dm_RAG_threads[OF vt this]
+ from dm_RAG_threads[OF this]
have "th \<in> threads s" .
} note hh = this
fix th1
@@ -2516,10 +2618,10 @@
qed
lemma finite_threads:
- assumes vt: "vt s"
shows "finite (threads s)"
-using vt
-by (induct) (auto elim: step.cases)
+using vt by (induct) (auto elim: step.cases)
+
+end
lemma Max_f_mono:
assumes seq: "A \<subseteq> B"
@@ -2534,9 +2636,11 @@
from fnt and seq show "finite (f ` B)" by auto
qed
+context valid_trace
+begin
+
lemma cp_le:
- assumes vt: "vt s"
- and th_in: "th \<in> threads s"
+ assumes th_in: "th \<in> threads s"
shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
@@ -2545,20 +2649,19 @@
proof(rule Max_f_mono)
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
next
- from finite_threads [OF vt]
+ from finite_threads
show "finite (threads s)" .
next
from th_in
show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
apply (auto simp:Domain_def)
- apply (rule_tac dm_RAG_threads[OF vt])
+ apply (rule_tac dm_RAG_threads)
apply (unfold trancl_domain [of "RAG s", symmetric])
by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
qed
qed
lemma le_cp:
- assumes vt: "vt s"
shows "preced th s \<le> cp s th"
proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
show "Prc (priority th s) (last_set th s)
@@ -2579,7 +2682,7 @@
by (rule_tac x = "(Th x, Th th)" in bexI, auto)
moreover have "finite \<dots>"
proof -
- from finite_RAG[OF vt] have "finite (RAG s)" .
+ from finite_RAG have "finite (RAG s)" .
hence "finite ((RAG (wq s))\<^sup>+)"
apply (unfold finite_trancl)
by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2599,7 +2702,6 @@
qed
lemma max_cp_eq:
- assumes vt: "vt s"
shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
(is "?l = ?r")
proof(cases "threads s = {}")
@@ -2609,26 +2711,26 @@
case False
have "?l \<in> ((cp s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
next
from False show "cp s ` threads s \<noteq> {}" by auto
qed
then obtain th
where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
- have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in])
+ have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
proof -
have "?r \<in> (?f ` ?A)"
proof(rule Max_in)
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
next
from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
qed
then obtain th' where
th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
- from le_cp [OF vt, of th'] eq_r
+ from le_cp [of th'] eq_r
have "?r \<le> cp s th'" by auto
moreover have "\<dots> \<le> cp s th"
proof(fold eq_l)
@@ -2637,7 +2739,7 @@
from th_in' show "cp s th' \<in> cp s ` threads s"
by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` threads s)" by auto
qed
qed
@@ -2647,23 +2749,22 @@
qed
lemma max_cp_readys_threads_pre:
- assumes vt: "vt s"
- and np: "threads s \<noteq> {}"
+ assumes np: "threads s \<noteq> {}"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
-proof(unfold max_cp_eq[OF vt])
+proof(unfold max_cp_eq)
show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
proof -
let ?p = "Max ((\<lambda>th. preced th s) ` threads s)"
let ?f = "(\<lambda>th. preced th s)"
have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
proof(rule Max_in)
- from finite_threads[OF vt] show "finite (?f ` threads s)" by simp
+ from finite_threads show "finite (?f ` threads s)" by simp
next
from np show "?f ` threads s \<noteq> {}" by simp
qed
then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
by (auto simp:Image_def)
- from th_chain_to_ready [OF vt tm_in]
+ from th_chain_to_ready [OF tm_in]
have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
thus ?thesis
proof
@@ -2672,7 +2773,7 @@
and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
have "cp s th' = ?f tm"
proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
- from dependants_threads[OF vt] finite_threads[OF vt]
+ from dependants_threads finite_threads
show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
by (auto intro:finite_subset)
next
@@ -2680,10 +2781,10 @@
from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
moreover have "p \<le> \<dots>"
proof(rule Max_ge)
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
- from p_in and th'_in and dependants_threads[OF vt, of th']
+ from p_in and th'_in and dependants_threads[of th']
show "p \<in> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
qed
@@ -2710,18 +2811,18 @@
apply (unfold cp_eq_cpreced cpreced_def)
apply (rule Max_mono)
proof -
- from dependants_threads [OF vt, of th1] th1_in
+ from dependants_threads [of th1] th1_in
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
(\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
from th'_in
@@ -2741,16 +2842,16 @@
assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
have "y' \<le> preced tm s"
proof(unfold tm_max, rule Max_ge)
- from hy' dependants_threads[OF vt, of tm]
+ from hy' dependants_threads[of tm]
show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
qed
} with hy show ?thesis by auto
qed
next
- from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+ from dependants_threads[of tm] finite_threads
show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
by (auto intro:finite_subset)
next
@@ -2761,7 +2862,7 @@
proof(rule Max_eqI)
from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
next
- from finite_threads[OF vt]
+ from finite_threads
show "finite (cp s ` readys s)" by (auto simp:readys_def)
next
fix y assume "y \<in> cp s ` readys s"
@@ -2771,13 +2872,13 @@
apply(unfold cp_eq_p h)
apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
proof -
- from finite_threads[OF vt]
+ from finite_threads
show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
next
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
by simp
next
- from dependants_threads[OF vt, of th1] th1_readys
+ from dependants_threads[of th1] th1_readys
show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
\<subseteq> (\<lambda>th. preced th s) ` threads s"
by (auto simp:readys_def)
@@ -2794,7 +2895,6 @@
there must be one inside it has the maximum precedence of the whole system.
*}
lemma max_cp_readys_threads:
- assumes vt: "vt s"
shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
proof(cases "threads s = {}")
case True
@@ -2802,9 +2902,10 @@
by (auto simp:readys_def)
next
case False
- show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
+ show ?thesis by (rule max_cp_readys_threads_pre[OF False])
qed
+end
lemma eq_holding: "holding (wq s) th cs = holding s th cs"
apply (unfold s_holding_def cs_holding_def wq_def, simp)
@@ -2836,13 +2937,14 @@
apply(auto)
done
+context valid_trace
+begin
+
lemma detached_intro:
- fixes s th
- assumes vt: "vt s"
- and eq_pv: "cntP s th = cntV s th"
+ assumes eq_pv: "cntP s th = cntV s th"
shows "detached s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_cnt: "cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
hence cncs_zero: "cntCS s th = 0"
@@ -2852,14 +2954,14 @@
thus ?thesis
proof
assume "th \<notin> threads s"
- with range_in[OF vt] dm_RAG_threads[OF vt]
+ with range_in dm_RAG_threads
show ?thesis
by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
next
assume "th \<in> readys s"
moreover have "Th th \<notin> Range (RAG s)"
proof -
- from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+ from card_0_eq [OF finite_holding] and cncs_zero
have "holdents s th = {}"
by (simp add:cntCS_def)
thus ?thesis
@@ -2874,12 +2976,10 @@
qed
lemma detached_elim:
- fixes s th
- assumes vt: "vt s"
- and dtc: "detached s th"
+ assumes dtc: "detached s th"
shows "cntP s th = cntV s th"
proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
have eq_pv: " cntP s th =
cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
have cncs_z: "cntCS s th = 0"
@@ -2904,11 +3004,11 @@
qed
lemma detached_eq:
- fixes s th
- assumes vt: "vt s"
shows "(detached s th) = (cntP s th = cntV s th)"
by (insert vt, auto intro:detached_intro detached_elim)
+end
+
text {*
The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
from the concise and miniature model of PIP given in PrioGDef.thy.
@@ -2923,6 +3023,4 @@
shows "th1 = th2"
using assms by (unfold next_th_def, auto)
-
-
end
--- a/RTree.thy Tue Dec 22 23:13:31 2015 +0800
+++ b/RTree.thy Wed Jan 06 20:46:14 2016 +0800
@@ -597,6 +597,23 @@
with that[unfolded ancestors_def] show ?thesis by auto
qed
+
+lemma subtree_Field:
+ "subtree r x \<subseteq> Field r \<union> {x}"
+proof
+ fix y
+ assume "y \<in> subtree r x"
+ thus "y \<in> Field r \<union> {x}"
+ proof(cases rule:subtreeE)
+ case 1
+ thus ?thesis by auto
+ next
+ case 2
+ thus ?thesis apply (auto simp:ancestors_def)
+ using Field_def tranclD by fastforce
+ qed
+qed
+
lemma subtree_ancestorsI:
assumes "a \<in> subtree r b"
and "a \<noteq> b"