--- a/CpsG.thy~ Fri Dec 18 19:13:19 2015 +0800
+++ b/CpsG.thy~ Fri Dec 18 22:47:32 2015 +0800
@@ -6,12 +6,21 @@
imports PrioG Max RTree
begin
+definition "the_preced s th = preced th s"
+
+fun the_thread :: "node \<Rightarrow> thread" where
+ "the_thread (Th th) = th"
+
definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}"
definition "tRAG s = wRAG s O hRAG s"
+definition "cp_gen s x =
+ Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
+(* ccc *)
+
lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
s_holding_abv cs_RAG_def, auto)
@@ -126,47 +135,6 @@
} ultimately show ?thesis by auto
qed
-lemma readys_root:
- assumes "vt s"
- and "th \<in> readys s"
- shows "root (RAG s) (Th th)"
-proof -
- { fix x
- assume "x \<in> ancestors (RAG s) (Th th)"
- hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- obtain z where "(Th th, z) \<in> RAG s" by auto
- with assms(2) have False
- apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
- by (fold wq_def, blast)
- } thus ?thesis by (unfold root_def, auto)
-qed
-
-lemma readys_in_no_subtree:
- assumes "vt s"
- and "th \<in> readys s"
- and "th' \<noteq> th"
- shows "Th th \<notin> subtree (RAG s) (Th th')"
-proof
- assume "Th th \<in> subtree (RAG s) (Th th')"
- thus False
- proof(cases rule:subtreeE)
- case 1
- with assms show ?thesis by auto
- next
- case 2
- with readys_root[OF assms(1,2)]
- show ?thesis by (auto simp:root_def)
- qed
-qed
-
-lemma image_id:
- assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x"
- shows "f ` A = A"
- using assms by (auto simp:image_def)
-
-definition "the_preced s th = preced th s"
-
lemma cp_alt_def:
"cp s th =
Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
@@ -182,12 +150,6 @@
thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
qed
-fun the_thread :: "node \<Rightarrow> thread" where
- "the_thread (Th th) = th"
-
-definition "cp_gen s x =
- Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-
lemma cp_gen_alt_def:
"cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"
by (auto simp:cp_gen_def)
@@ -221,45 +183,43 @@
qed
qed
-lemma threads_set_eq:
- "the_thread ` (subtree (tRAG s) (Th th)) =
- {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
+lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"
+proof -
+ have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*"
+ by (rule rtrancl_mono, auto simp:RAG_split)
+ also have "... \<subseteq> ((RAG s)^*)^*"
+ by (rule rtrancl_mono, auto)
+ also have "... = (RAG s)^*" by simp
+ finally show ?thesis by (unfold tRAG_def, simp)
+qed
+
+lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"
proof -
- { fix th'
- assume "th' \<in> ?L"
- then obtain n where h: "th' = the_thread n" "n \<in> subtree (tRAG s) (Th th)" by auto
- from subtree_nodeE[OF this(2)]
- obtain th1 where "n = Th th1" by auto
- with h have "Th th' \<in> subtree (tRAG s) (Th th)" by auto
- hence "Th th' \<in> subtree (RAG s) (Th th)"
- proof(cases rule:subtreeE[consumes 1])
- case 1
- thus ?thesis by (auto simp:subtree_def)
- next
- case 2
- hence "(Th th', Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
- thus ?thesis
- proof(induct)
- case (step y z)
- from this(2)[unfolded tRAG_alt_def]
- obtain u where
- h: "(y, u) \<in> RAG s" "(u, z) \<in> RAG s"
- by auto
- hence "y \<in> subtree (RAG s) z" by (auto simp:subtree_def)
- with step(3)
- show ?case by (auto simp:subtree_def)
- next
- case (base y)
- from this[unfolded tRAG_alt_def]
- show ?case by (auto simp:subtree_def)
- qed
- qed
- hence "th' \<in> ?R" by auto
+ { fix a
+ assume "a \<in> subtree (tRAG s) x"
+ hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
+ with tRAG_star_RAG[of s]
+ have "(a, x) \<in> (RAG s)^*" by auto
+ hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)
+ } thus ?thesis by auto
+qed
+
+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
} moreover {
- fix th'
- assume "th' \<in> ?R"
- hence "(Th th', Th th) \<in> (RAG s)^*" by (auto simp:subtree_def)
- from star_rpath[OF this]
+ fix n
+ assume "n \<in> ?R"
+ 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)
@@ -280,7 +240,6 @@
hence "(Th th', x1) \<in> (RAG s)" by (cases, simp)
then obtain cs where "x1 = Cs cs"
by (unfold s_RAG_def, auto)
- find_theorems rpath "_ = _@[_]"
from rpath_nnl_lastE[OF rp[unfolded this]]
show ?thesis by auto
next
@@ -313,11 +272,16 @@
qed
qed
qed
- from imageI[OF this, of the_thread]
- have "th' \<in> ?L" by simp
+ from this[folded h(1)]
+ have "n \<in> ?L" .
} ultimately show ?thesis by auto
qed
-
+
+lemma threads_set_eq:
+ "the_thread ` (subtree (tRAG s) (Th th)) =
+ {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
+ by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)
+
lemma cp_alt_def1:
"cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
proof -
@@ -344,8 +308,6 @@
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"
@@ -353,6 +315,38 @@
context valid_trace
begin
+lemma readys_root:
+ assumes "th \<in> readys s"
+ shows "root (RAG s) (Th th)"
+proof -
+ { fix x
+ assume "x \<in> ancestors (RAG s) (Th th)"
+ hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
+ from tranclD[OF this]
+ obtain z where "(Th th, z) \<in> RAG s" by auto
+ with assms(1) have False
+ apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
+ by (fold wq_def, blast)
+ } thus ?thesis by (unfold root_def, auto)
+qed
+
+lemma readys_in_no_subtree:
+ assumes "th \<in> readys s"
+ and "th' \<noteq> th"
+ shows "Th th \<notin> subtree (RAG s) (Th th')"
+proof
+ assume "Th th \<in> subtree (RAG s) (Th th')"
+ thus False
+ proof(cases rule:subtreeE)
+ case 1
+ with assms show ?thesis by auto
+ next
+ case 2
+ with readys_root[OF assms(1)]
+ show ?thesis by (auto simp:root_def)
+ qed
+qed
+
lemma not_in_thread_isolated:
assumes "th \<notin> threads s"
shows "(Th th) \<notin> Field (RAG s)"
@@ -566,169 +560,11 @@
end
+(* ccc *)
-lemma eq_dependants: "dependants (wq s) = dependants s"
- by (simp add: s_dependants_abv wq_def)
-
+
(* obvious lemma *)
-lemma not_thread_holdents:
- fixes th s
- assumes vt: "vt s"
- and not_in: "th \<notin> threads s"
- shows "holdents s th = {}"
-proof -
- from vt not_in show ?thesis
- proof(induct arbitrary:th)
- case (vt_cons s e th)
- assume vt: "vt s"
- and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
- and stp: "step s e"
- and not_in: "th \<notin> threads (e # s)"
- from stp show ?case
- proof(cases)
- case (thread_create thread prio)
- assume eq_e: "e = Create thread prio"
- and not_in': "thread \<notin> threads s"
- have "holdents (e # s) th = holdents s th"
- apply (unfold eq_e holdents_test)
- by (simp add:RAG_create_unchanged)
- moreover have "th \<notin> threads s"
- proof -
- from not_in eq_e show ?thesis by simp
- qed
- moreover note ih ultimately show ?thesis by auto
- next
- case (thread_exit thread)
- assume eq_e: "e = Exit thread"
- and nh: "holdents s thread = {}"
- show ?thesis
- proof(cases "th = thread")
- case True
- with nh eq_e
- show ?thesis
- by (auto simp:holdents_test RAG_exit_unchanged)
- next
- case False
- with not_in and eq_e
- have "th \<notin> threads s" by simp
- from ih[OF this] False eq_e show ?thesis
- by (auto simp:holdents_test RAG_exit_unchanged)
- qed
- next
- case (thread_P thread cs)
- assume eq_e: "e = P thread cs"
- and is_runing: "thread \<in> runing s"
- from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto
- have neq_th: "th \<noteq> thread"
- proof -
- from not_in eq_e have "th \<notin> threads s" by simp
- moreover from is_runing have "thread \<in> threads s"
- by (simp add:runing_def readys_def)
- ultimately show ?thesis by auto
- qed
- hence "holdents (e # s) th = holdents s th "
- apply (unfold cntCS_def holdents_test eq_e)
- by (unfold step_RAG_p[OF vtp], auto)
- moreover have "holdents s th = {}"
- proof(rule ih)
- from not_in eq_e show "th \<notin> threads s" by simp
- qed
- ultimately show ?thesis by simp
- next
- case (thread_V thread cs)
- assume eq_e: "e = V thread cs"
- and is_runing: "thread \<in> runing s"
- and hold: "holding s thread cs"
- have neq_th: "th \<noteq> thread"
- proof -
- from not_in eq_e have "th \<notin> threads s" by simp
- moreover from is_runing have "thread \<in> threads s"
- by (simp add:runing_def readys_def)
- ultimately show ?thesis by auto
- qed
- from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto
- from hold obtain rest
- where eq_wq: "wq s cs = thread # rest"
- by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
- from not_in eq_e eq_wq
- have "\<not> next_th s thread cs th"
- apply (auto simp:next_th_def)
- proof -
- assume ne: "rest \<noteq> []"
- and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
- have "?t \<in> set rest"
- proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- fix x assume "distinct x \<and> set x = set rest" with ne
- show "hd x \<in> set rest" by (cases x, auto)
- qed
- with eq_wq have "?t \<in> set (wq s cs)" by simp
- from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
- show False by auto
- qed
- moreover note neq_th eq_wq
- ultimately have "holdents (e # s) th = holdents s th"
- by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
- moreover have "holdents s th = {}"
- proof(rule ih)
- from not_in eq_e show "th \<notin> threads s" by simp
- qed
- ultimately show ?thesis by simp
- next
- case (thread_set thread prio)
- print_facts
- assume eq_e: "e = Set thread prio"
- and is_runing: "thread \<in> runing s"
- from not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] and eq_e
- show ?thesis
- apply (unfold eq_e cntCS_def holdents_test)
- by (simp add:RAG_set_unchanged)
- qed
- next
- case vt_nil
- show ?case
- by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
- qed
-qed
-
-(* obvious lemma *)
-lemma next_th_neq:
- assumes vt: "vt s"
- and nt: "next_th s th cs th'"
- shows "th' \<noteq> th"
-proof -
- from nt show ?thesis
- apply (auto simp:next_th_def)
- proof -
- fix rest
- assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
- and ne: "rest \<noteq> []"
- have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest"
- proof(rule someI2)
- from wq_distinct[OF vt, of cs] eq_wq
- show "distinct rest \<and> set rest = set rest" by auto
- next
- fix x
- assume "distinct x \<and> set x = set rest"
- hence eq_set: "set x = set rest" by auto
- with ne have "x \<noteq> []" by auto
- hence "hd x \<in> set x" by auto
- with eq_set show "hd x \<in> set rest" by auto
- qed
- with wq_distinct[OF vt, of cs] eq_wq show False by auto
- qed
-qed
-
-(* obvious lemma *)
-lemma next_th_unique:
- assumes nt1: "next_th s th cs th1"
- and nt2: "next_th s th cs th2"
- shows "th1 = th2"
-using assms by (unfold next_th_def, auto)
lemma wf_RAG:
assumes vt: "vt s"
@@ -2039,17 +1875,8 @@
proof -
from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
have "(Th th) \<notin> subtree (RAG s') (Th th')" .
- find_theorems subtree tRAG RAG (* ccc *)
- proof
- assume "Th th \<in> subtree (tRAG s') (Th th')"
- thus False
- proof(cases rule:subtreeE)
- case 2
- from ancestors_Field[OF this(2)]
- and th_tRAG[unfolded Field_def]
- show ?thesis by auto
- qed (insert assms, auto)
- qed
+ with tRAG_subtree_RAG[of s' "Th th'"]
+ have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
with a_in[unfolded eq_a] show ?thesis by auto
qed
from preced_kept[OF this]