diff -r 38c6acf03f68 -r 5d8ec128518b PIPBasics.thy
--- 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