--- a/Test.thy Fri May 23 15:19:32 2014 +0100
+++ b/Test.thy Sat May 24 12:39:12 2014 +0100
@@ -72,7 +72,7 @@
abbreviation
"release qs \<equiv> case qs of
[] => []
- | (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
+ | (_ # qs) => SOME q. distinct q \<and> set q = set qs"
fun schs :: "state \<Rightarrow> schedule_state"
where
@@ -122,6 +122,9 @@
definition holding :: "state \<Rightarrow> thread \<Rightarrow> cs set"
where "holding s th \<equiv> {cs . holds2 s th cs}"
+abbreviation
+ "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"
+
lemma holding_RAG:
"holding s th = {cs . (Cs cs, Th th) \<in> RAG2 s}"
unfolding holding_def
@@ -191,41 +194,41 @@
lemma RAG_p1:
assumes "wq s cs = []"
- shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Cs cs, Th th)}"
- using assms
- apply(auto simp add: RAG2_def RAG_def wq_def Let_def waits_def holds_def)
- apply (metis in_set_insert insert_Nil list.distinct(1))
- done
+ shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Cs cs, Th th)}"
+using assms
+unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
lemma RAG_p2:
- assumes "vt (P th cs#s)" "wq s cs \<noteq> []"
- shows "RAG2 (P th cs # s) = RAG2 s \<union> {(Th th, Cs cs)}"
- using assms
- apply(simp add: RAG2_def Let_def)
- apply(erule_tac vt.cases)
- apply(simp)
- apply(clarify)
- apply(simp)
- apply(erule_tac step.cases)
- apply(simp_all)
- apply(simp add: wq_def RAG_def RAG2_def)
- apply(simp add: waits_def holds_def)
- apply(auto)
- done
+ assumes "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" "wq s cs \<noteq> []"
+ shows "RAG2 (P th cs # s) \<subseteq> RAG2 s \<union> {(Th th, Cs cs)}"
+using assms
+unfolding RAG2_def RAG_def wq_def Let_def waits_def holds_def
+by (auto simp add: Let_def)
+
+lemma [simp]: "(SOME q. distinct q \<and> q = []) = []"
+by auto
+
+lemma [simp]: "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
+apply auto
+apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
-definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
- where "next_th s th cs t =
- (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> t = hd (SOME q. distinct q \<and> set q = set rest))"
+lemma RAG_v1:
+assumes vt: "wq s cs = [th]"
+shows "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}"
+using assms
+unfolding RAG2_def RAG_def waits_def holds_def wq_def
+by (auto simp add: Let_def)
-lemma RAG_v:
-assumes vt:"vt (V th cs#s)"
-shows "
- RAG2 (V th cs # s) =
- RAG2 s - {(Cs cs, Th th)} -
- {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
- {(Cs cs, Th th') |th'. next_th s th cs th'}"
- apply (insert vt, unfold RAG2_def RAG_def)
- sorry
+lemma RAG_v2:
+assumes vt:"vt s" "wq s cs = th # wts \<and> wts \<noteq> []"
+shows "RAG2 (V th cs # s) \<subseteq>
+ RAG2 s - {(Cs cs, Th th)} - {(Th (next_to_run wts), Cs cs)} \<union> {(Cs cs, Th (next_to_run wts))}"
+unfolding RAG2_def RAG_def waits_def holds_def
+using assms wq_distinct[OF vt(1), of"cs"]
+by (auto simp add: Let_def wq_def)
lemma waiting_unique:
assumes "vt s"
@@ -234,11 +237,6 @@
shows "cs1 = cs2"
sorry
-lemma singleton_Un:
- shows "A \<union> {x} = insert x A"
-by simp
-
-
lemma acyclic_RAG_step:
assumes vt: "vt s"
and stp: "step s e"
@@ -247,11 +245,8 @@
using stp vt ac
proof (induct)
case (step_P th s cs)
- have vt: "vt s" by fact
have ac: "acyclic (RAG2 s)" by fact
- have rn: "th \<in> runing s" by fact
have ds: "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>+" by fact
- have vtt: "vt (P th cs#s)" using vt rn ds by (metis step.step_P vt_cons)
{ assume a: "wq s cs = []" -- "case waiting queue is empty"
have "(Th th, Cs cs) \<notin> (RAG2 s)\<^sup>*"
proof
@@ -262,14 +257,16 @@
qed
with acyclic_insert ac
have "acyclic (RAG2 s \<union> {(Cs cs, Th th)})" by simp
- then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a] by simp
+ then have "acyclic (RAG2 (P th cs # s))" using RAG_p1[OF a]
+ by (rule acyclic_subset)
}
moreover
{ assume a: "wq s cs \<noteq> []" -- "case waiting queue is not empty"
from ds have "(Cs cs, Th th) \<notin> (RAG2 s)\<^sup>*" by (metis node.distinct(1) rtranclD)
with acyclic_insert ac
have "acyclic (RAG2 s \<union> {(Th th, Cs cs)})" by auto
- then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF vtt a] by simp
+ then have "acyclic (RAG2 (P th cs # s))" using RAG_p2[OF ds a]
+ by (rule acyclic_subset)
}
ultimately show "acyclic (RAG2 (P th cs # s))" by metis
next
@@ -278,89 +275,53 @@
have ac: "acyclic (RAG2 s)" by fact
have rn: "th \<in> runing s" by fact
have hd: "holds2 s th cs" by fact
- from hd
- have th_in: "th \<in> set (wq s cs)" and
- eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
- then obtain rest where
- eq_wq: "wq s cs = th # rest" by (cases "wq s cs") (auto)
- show ?case
- apply(subst RAG_v)
- apply(rule vt_cons)
- apply(rule vt)
- apply(rule step.step_V)
- apply(rule rn)
- apply(rule hd)
- using eq_wq
- apply(cases "rest = []")
- apply(subgoal_tac "{(Cs cs, Th th') |th'. next_th s th cs th'} = {}")
- apply(simp)
- apply(rule acyclic_subset)
- apply(rule ac)
- apply(auto)[1]
- apply(auto simp add: next_th_def)[1]
- -- "case wq more than a singleton"
- apply(subgoal_tac "{(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest)))} =
- {(Cs cs, Th th') |th'. next_th s th cs th'}")
- apply(rotate_tac 2)
- apply(drule sym)
- apply(simp only: singleton_Un)
- apply(simp only: acyclic_insert)
- apply(rule conjI)
- apply(rule acyclic_subset)
- apply(rule ac)
- apply(auto)[1]
- apply(rotate_tac 2)
- apply(thin_tac "?X")
- defer
- apply(simp add: next_th_def)
- apply(clarify)
- apply(simp add: rtrancl_eq_or_trancl)
- apply(drule tranclD)
- apply(erule exE)
- apply(drule conjunct1)
- apply(subgoal_tac "(Th (hd (SOME q. distinct q \<and> set q = set rest)), z) \<in> RAG2 s")
- prefer 2
- apply(simp)
- apply(case_tac z)
- apply(simp add: RAG2_def RAG_def)
- apply(clarify)
- apply(simp)
- apply(simp add: next_th_def)
- apply(rule waiting_unique)
- apply(rule vt)
- apply(simp add: RAG2_def RAG_def waits2_def waits_def wq_def)
- apply(rotate_tac 2)
- apply(thin_tac "?X")
- apply(subgoal_tac "distinct (wq s cs)")
- prefer 2
- apply(rule wq_distinct)
- apply(rule vt)
- apply (unfold waits2_def waits_def wq_def, auto)
- apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
- prefer 2
- apply (metis (mono_tags) set_empty tfl_some)
- apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in>
- set (SOME q. distinct q \<and> set q = set rest)")
- prefer 2
- apply(auto)[1]
- apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest")
- prefer 2
- apply(rule someI2)
- apply(auto)[2]
- apply(auto)[1]
- apply(subgoal_tac "(SOME q. distinct q \<and> set q = set rest) \<noteq> []")
- prefer 2
- apply (metis (mono_tags) set_empty tfl_some)
- apply(subgoal_tac "hd (SOME q. distinct q \<and> set q = set rest) \<in>
- set (SOME q. distinct q \<and> set q = set rest)")
- prefer 2
- apply(auto)[1]
- apply(subgoal_tac "set (SOME q. distinct q \<and> set q = set rest) = set rest")
- prefer 2
- apply(rule someI2)
- apply(auto)[2]
- apply(auto)[1]
- done
+ from hd have th_in: "th \<in> set (wq s cs)" and
+ eq_hd: "th = hd (wq s cs)" unfolding holds2_def holds_def wq_def by auto
+ then obtain wts where
+ eq_wq: "wq s cs = th # wts" by (cases "wq s cs") (auto)
+ { assume "wts = []" -- "case no thread present to take over"
+ with eq_wq have "wq s cs = [th]" by simp
+ then have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)}" by (rule RAG_v1)
+ moreover have "acyclic (RAG2 s - {(Cs cs, Th th)})" using ac by (auto intro: acyclic_subset)
+ ultimately
+ have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+ }
+ moreover
+ { def nth \<equiv> "next_to_run wts"
+ assume aa: "wts \<noteq> []" -- "at least one thread present to take over"
+ with vt eq_wq
+ have "RAG2 (V th cs # s) \<subseteq> RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)} \<union> {(Cs cs, Th nth)}"
+ unfolding nth_def by (rule_tac RAG_v2) (auto)
+ moreover
+ have "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
+ proof -
+ have "acyclic (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})" using ac by (auto intro: acyclic_subset)
+ moreover
+ have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
+ proof
+ assume "(Th nth, Cs cs) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>+"
+ then obtain z where a: "(Th nth, z) \<in> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})"
+ by (metis converse_tranclE)
+ then have "(Th nth, z) \<in> RAG2 s" by simp
+ then obtain cs' where b: "z = Cs cs'" "(Th nth, Cs cs') \<in> RAG2 s"
+ unfolding RAG2_def RAG_def by auto
+ then have "cs = cs'"
+ apply(rule_tac waiting_unique[OF vt])
+ using eq_wq aa
+ apply(auto simp add: nth_def RAG2_def RAG_def waits2_def waits_def wq_def)
+ apply (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.inject set_empty2 tfl_some vt wq_def wq_distinct)
+ by (metis (mono_tags, lifting) `\<And>thesis. (\<And>wts. wq s cs = th # wts \<Longrightarrow> thesis) \<Longrightarrow> thesis` distinct.simps(2) hd_in_set list.sel(1) set_empty2 tfl_some vt wq_def wq_distinct)
+ then show "False" using a b by simp
+ qed
+ then have "(Th nth, Cs cs) \<notin> (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)})\<^sup>*"
+ by (metis node.distinct(1) rtranclD)
+ ultimately
+ show "acyclic (insert (Cs cs, Th nth) (RAG2 s - {(Cs cs, Th th)} - {(Th nth, Cs cs)}))"
+ by (simp add: acyclic_insert)
+ qed
+ ultimately have "acyclic (RAG2 (V th cs # s))" by (auto intro: acyclic_subset)
+ }
+ ultimately show "acyclic (RAG2 (V th cs # s))" by metis
qed (simp_all)