# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1458570782 0
# Node ID b3b8735c7c0211ca8fca891278ce9ebc54f8f414
# Parent  8d8ed7b9680f85c1aa0e4de30aad4c65b34e4123
updated to Isabelle 2016

diff -r 8d8ed7b9680f -r b3b8735c7c02 PIPBasics.thy
--- 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