--- a/PIPBasics.thy Mon Mar 21 14:15:51 2016 +0000
+++ b/PIPBasics.thy Mon Mar 21 14:33:02 2016 +0000
@@ -742,7 +742,7 @@
Because @{term "e#s"} is also a valid trace, properties
derived for valid trace @{term s} also hold on @{term "e#s"}.
*}
-sublocale valid_trace_e < vat_es!: valid_trace "e#s"
+sublocale valid_trace_e < vat_es: valid_trace "e#s"
using vt_e
by (unfold_locales, simp)
@@ -977,7 +977,7 @@
locale valid_moment = valid_trace +
fixes i :: nat
-sublocale valid_moment < vat_moment!: valid_trace "(moment i s)"
+sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
by (unfold_locales, insert vt_moment, auto)
locale valid_moment_e = valid_moment +
@@ -995,7 +995,7 @@
end
-sublocale valid_moment_e < vat_moment_e!: valid_trace_e "moment i s" "next_e"
+sublocale valid_moment_e < vat_moment_e: valid_trace_e "moment i s" "next_e"
using vt_moment[of "Suc i", unfolded trace_e]
by (unfold_locales, simp)
@@ -1468,7 +1468,7 @@
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:cs_waiting_def)
+ by (unfold s_RAG_def, auto simp:cs_waiting_raw)
from wq_threads [OF this] show ?thesis .
qed
@@ -1476,7 +1476,7 @@
assumes "(Th th) \<in> Range (RAG s)"
shows "th \<in> threads s"
using assms
- by (unfold s_RAG_def cs_waiting_def cs_holding_def,
+ by (unfold s_RAG_def cs_waiting_raw cs_holding_raw,
auto intro:wq_threads)
lemma RAG_threads:
@@ -1613,7 +1613,7 @@
have "wq (e#s) c = wq s c" using False
by simp
hence "waiting s t c" using assms
- by (simp add: cs_waiting_def waiting_eq)
+ by (simp add: cs_waiting_raw waiting_eq)
hence "t \<notin> readys s" by (unfold readys_def, auto)
hence "t \<notin> runing s" using runing_ready by auto
with runing_th_s[folded otherwise] show ?thesis by auto
@@ -1628,7 +1628,7 @@
have "wq (e#s) c = wq s c"
using assms(2) by auto
with assms(1) show ?thesis
- using cs_waiting_def waiting_eq by auto
+ unfolding cs_waiting_raw waiting_eq by auto
qed
lemma holding_esI2:
@@ -1716,7 +1716,7 @@
fix x
assume "distinct x \<and> set x = set rest"
moreover have "t \<in> set rest"
- using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto
+ using assms(1) unfolding cs_waiting_raw waiting_eq wq_s_cs by auto
ultimately show "t \<in> set x" by simp
qed
moreover have "t \<noteq> hd wq'"
@@ -1732,7 +1732,7 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
+ with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
@@ -1742,7 +1742,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 cs_waiting_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
+ by (metis cs_waiting_raw insert_iff list.sel(1) s_waiting_abv set_simps(2) 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
@@ -1839,7 +1839,7 @@
shows "waiting (e#s) t c"
proof -
have "c \<noteq> cs" using assms
- using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto
+ using rest_nil wq_s_cs unfolding cs_waiting_raw waiting_eq by auto
from waiting_esI1[OF assms this]
show ?thesis .
qed
@@ -1850,7 +1850,7 @@
proof(cases "c = cs")
case False
hence "wq (e#s) c = wq s c" by auto
- with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto
+ with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
from that(1)[OF False this] show ?thesis .
next
case True
@@ -2071,7 +2071,7 @@
assumes "waiting s th' cs'"
shows "waiting (e#s) th' cs'"
using assms
- unfolding th_not_in_wq waiting_eq cs_waiting_def
+ unfolding th_not_in_wq waiting_eq cs_waiting_raw
by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD
list.distinct(1) split_list wq_es_cs wq_neq_simp)
@@ -2081,7 +2081,7 @@
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
- with assms show ?thesis using cs_holding_def holding_eq by auto
+ with assms show ?thesis unfolding cs_holding_raw holding_eq by auto
next
case True
from assms[unfolded s_holding_def, folded wq_def]
@@ -2090,7 +2090,7 @@
hence "wq (e#s) cs' = th'#(rest@[th])"
by (simp add: True wq_es_cs)
thus ?thesis
- by (simp add: cs_holding_def holding_eq)
+ by (simp add: cs_holding_raw holding_eq)
qed
end
@@ -2113,7 +2113,7 @@
proof -
from wq_es_cs'
have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
- thus ?thesis using cs_holding_def holding_eq by blast
+ thus ?thesis unfolding cs_holding_raw holding_eq by blast
qed
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
@@ -2138,7 +2138,7 @@
next
case False
have "holding s th' cs'" using assms
- using False cs_holding_def holding_eq by auto
+ using False unfolding cs_holding_raw holding_eq by auto
from that(1)[OF False this] show ?thesis .
qed
@@ -2208,7 +2208,7 @@
by (simp add: wq_es_cs wq_s_cs)
lemma waiting_es_th_cs: "waiting (e#s) th cs"
- using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto
+ using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding cs_waiting_raw by auto
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)
@@ -2220,8 +2220,8 @@
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
- with assms show ?thesis
- using cs_holding_def holding_eq that by auto
+ with assms show ?thesis using that
+ unfolding cs_holding_raw holding_eq by auto
next
case True
with assms show ?thesis
@@ -2244,7 +2244,7 @@
next
case False
hence "th' = th \<and> cs' = cs"
- by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2)
+ by (metis assms cs_waiting_raw holder_def list.sel(1) rotate1.simps(2)
set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
with that(2) show ?thesis by metis
qed
@@ -2355,8 +2355,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_def
- cs_holding_def wq_def acyclic_def)
+ by (auto simp: s_RAG_def cs_waiting_raw
+ cs_holding_raw wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
@@ -2788,8 +2788,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_def
- cs_holding_def wq_def acyclic_def)
+ by (auto simp: s_RAG_def cs_waiting_raw
+ cs_holding_raw wq_def acyclic_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
@@ -3078,7 +3078,7 @@
next
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)
+ by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_raw Domain_def)
from chain_building [rule_format, OF this]
show ?thesis by auto
qed
@@ -3628,8 +3628,8 @@
proof(cases)
case (thread_P)
moreover have "(Cs cs, Th th) \<in> RAG s"
- using otherwise cs_holding_def
- holding_eq th_not_in_wq by auto
+ using otherwise th_not_in_wq
+ unfolding cs_holding_raw holding_eq by auto
ultimately show ?thesis by auto
qed
qed