--- a/PIPBasics.thy Thu Jun 09 23:01:36 2016 +0100
+++ b/PIPBasics.thy Tue Jun 14 13:56:51 2016 +0100
@@ -1448,17 +1448,19 @@
from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)
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: waiting_raw_def)
- from wq_threads [OF this] show ?thesis .
+ then have "th \<in> set (wq s cs)"
+ using in_RAG_E s_waiting_def wq_def by auto
+ then show ?thesis using wq_threads by simp
qed
lemma rg_RAG_threads:
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
using assms
- unfolding s_RAG_def waiting_raw_def holding_raw_def
-using wq_threads by auto
+ apply(erule_tac RangeE)
+ apply(erule_tac in_RAG_E)
+ apply(auto)
+ using s_holding_def wq_def wq_threads by auto
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
@@ -1593,8 +1595,8 @@
case False
have "wq (e#s) c = wq s c" using False
by simp
- hence "waiting s t c" using assms
- by (simp add: waiting_raw_def waiting_eq)
+ hence "waiting s t c" using assms
+ by (simp add: s_waiting_def wq_def)
hence "t \<notin> readys s" by (unfold readys_def, auto)
hence "t \<notin> running s" using running_ready by auto
with running_th_s[folded otherwise] show ?thesis by auto
@@ -1608,8 +1610,8 @@
proof -
have "wq (e#s) c = wq s c"
using assms(2) by auto
- with assms(1) show ?thesis
- unfolding waiting_raw_def waiting_eq by auto
+ with assms(1) show ?thesis
+ by (simp add: s_waiting_def wq_def)
qed
lemma holding_esI2:
@@ -1697,7 +1699,7 @@
fix x
assume "distinct x \<and> set x = set rest"
moreover have "t \<in> set rest"
- using assms(1) unfolding waiting_raw_def waiting_eq wq_s_cs by auto
+ using assms(1) s_waiting_def set_ConsD wq_def wq_s_cs by auto
ultimately show "t \<in> set x" by simp
qed
moreover have "t \<noteq> hd wq'"
@@ -1713,7 +1715,8 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
+ with assms have "waiting s t c"
+ by (simp add: s_waiting_def wq_def)
from that(1)[OF False this] show ?thesis .
next
case True
@@ -1723,7 +1726,7 @@
moreover hence "t \<noteq> th" using assms neq_t_th by blast
moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv)
ultimately have "waiting s t cs"
- by (metis waiting_raw_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
+ by (metis list.sel(1) list.set_sel(2) list.simps(3) rest_def s_waiting_def wq_def wq_s_cs)
show ?thesis using that(2)
using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto
qed
@@ -1817,10 +1820,10 @@
lemma waiting_esI2:
assumes "waiting s t c"
- shows "waiting (e#s) t c"
+ shows "waiting (e # s) t c"
proof -
have "c \<noteq> cs" using assms
- using rest_nil wq_s_cs unfolding waiting_raw_def waiting_eq by auto
+ using no_waiter_before by blast
from waiting_esI1[OF assms this]
show ?thesis .
qed
@@ -1831,7 +1834,8 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
+ with assms have "waiting s t c"
+ by (simp add: s_waiting_def wq_def)
from that(1)[OF False this] show ?thesis .
next
case True
@@ -2052,9 +2056,8 @@
assumes "waiting s th' cs'"
shows "waiting (e#s) th' cs'"
using assms
- unfolding th_not_in_wq waiting_eq waiting_raw_def
- by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD
- list.distinct(1) split_list wq_es_cs wq_neq_simp)
+ by (metis butlast_snoc distinct.simps(2) distinct_singleton hd_append2
+ in_set_butlastD s_waiting_def wq_def wq_es_cs wq_neq_simp)
lemma holding_kept:
assumes "holding s th' cs'"
@@ -2189,7 +2192,8 @@
by (simp add: wq_es_cs wq_s_cs)
lemma waiting_es_th_cs: "waiting (e#s) th cs"
- using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding waiting_raw_def by auto
+ using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs
+ by (simp add: s_waiting_def wq_def wq_es_cs)
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
@@ -2202,7 +2206,7 @@
case False
hence "wq (e#s) cs' = wq s cs'" by simp
with assms show ?thesis using that
- unfolding holding_raw_def holding_eq by auto
+ using s_holding_def wq_def by auto
next
case True
with assms show ?thesis
@@ -2225,8 +2229,8 @@
next
case False
hence "th' = th \<and> cs' = cs"
- by (metis assms waiting_raw_def holder_def list.sel(1) rotate1.simps(2)
- set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
+ by (metis assms hd_append2 insert_iff list.simps(15) rotate1.simps(2)
+ s_waiting_def set_rotate1 wne wq_def wq_es_cs wq_neq_simp)
with that(2) show ?thesis by metis
qed
@@ -3611,7 +3615,7 @@
case (thread_P)
moreover have "(Cs cs, Th th) \<in> RAG s"
using otherwise th_not_in_wq
- unfolding holding_raw_def holding_eq by auto
+ using s_holding_def wq_def by auto
ultimately show ?thesis by auto
qed
qed
@@ -5103,7 +5107,7 @@
assume "(a, Th th) \<in> RAG s"
with assms[unfolded holdents_test]
show False
- by (cases a, auto simp:RAG_raw_def s_RAG_abv)
+ using assms children_def holdents_alt_def by fastforce
qed
qed
@@ -5118,7 +5122,7 @@
assume "(Th th, b) \<in> RAG s"
with assms[unfolded readys_def s_waiting_def]
show False
- by (cases b, auto simp: RAG_raw_def s_RAG_abv waiting_raw_def)
+ using Collect_disj_eq s_RAG_def s_waiting_abv s_waiting_def wq_def by fastforce
qed
qed