
diff -r e3cf792db636 -r 0f124691c191 PIPBasics.thy
--- a/PIPBasics.thy	Tue Jun 14 15:06:16 2016 +0100
+++ b/PIPBasics.thy	Fri Jun 17 09:46:25 2016 +0100
@@ -1,5 +1,5 @@
 theory PIPBasics
-imports PIPDefs
+imports PIPDefs RTree
 begin
 
 text {* (* ddd *)
@@ -147,7 +147,7 @@
   obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"
     by (metis empty_iff hd_in_set list.set(1))
   hence "holding s th' cs" 
-    by (unfold s_holding_def, fold wq_def, auto)
+    unfolding s_holding_def by auto
   from that[OF this] show ?thesis .
 qed
 
@@ -159,7 +159,7 @@
 *}
 lemma children_RAG_alt_def:
   "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
-  by (unfold s_RAG_def, auto simp:children_def holding_eq)
+  by (unfold s_RAG_def, auto simp:children_def s_holding_abv)
 
 text {*
   The following two lemmas relate @{term holdents} and @{term cntCS}
@@ -279,8 +279,8 @@
 lemma in_RAG_E:
   assumes "(n1, n2) \<in> RAG (s::state)"
   obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
-      | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
-  using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
+        | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
+  using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv]
   by auto
 
 text {*
@@ -584,8 +584,8 @@
     thus ?thesis by simp
   qed
   thus ?thesis
-  by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants 
-      f_image_eq the_preced_def) 
+  by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq 
+      s_dependants_abv the_preced_def)
 qed
 
 text {*
@@ -625,7 +625,7 @@
         from h1 have "cs' = cs" by simp
         from assms(2) cs_in[unfolded this]
         have "holding s th'' cs" "holding s th2 cs"
-          by (unfold s_RAG_def, fold holding_eq, auto)
+          by (unfold s_RAG_def, fold s_holding_abv, auto)
         from held_unique[OF this]
         show ?thesis by simp 
       qed
@@ -990,9 +990,9 @@
   obtain rest where eq_wq: "wq s cs = th#rest" by blast
   with otherwise
   have "holding s th cs"
-    by (unfold s_holding_def, fold wq_def, simp)
+    unfolding s_holding_def by auto
   hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
-    by (unfold s_RAG_def, fold holding_eq, auto)
+    by (unfold s_RAG_def, fold s_holding_abv, auto)
   from pip_e[unfolded is_p]
   show False
   proof(cases)
@@ -1033,8 +1033,8 @@
   proof(cases)
     case (thread_V)
     from this(2) show ?thesis
-      by (unfold rest_def s_holding_def, fold wq_def,
-                 metis empty_iff list.collapse list.set(1))
+      unfolding s_holding_def
+      by (metis empty_iff empty_set hd_Cons_tl rest_def) 
   qed
 qed
 
@@ -1168,8 +1168,9 @@
 proof -
   from pip_e[unfolded is_exit]
   show ?thesis
-  by (cases, unfold holdents_def s_holding_def, fold wq_def, 
-             auto elim!:running_wqE)
+  apply(cases)
+  unfolding holdents_def s_holding_def
+  by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE)
 qed
 
 lemma wq_threads_kept:
@@ -1562,7 +1563,7 @@
 proof -
   from assms(1) have "wq (e#s) c = wq s c"  by auto
   from assms(2)[unfolded s_holding_def, folded wq_def, 
-                folded this, unfolded wq_def, folded s_holding_def]
+                folded this, folded s_holding_def]
   show ?thesis .
 qed
 
@@ -1624,7 +1625,7 @@
    
 lemma holding_taker:
   shows "holding (e#s) taker cs"
-    by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, 
+    by (unfold s_holding_def, unfold wq_es_cs, 
         auto simp:neq_wq' taker_def)
 
 lemma waiting_esI2:
@@ -1692,7 +1693,7 @@
   case False
   hence "wq (e#s) c = wq s c" by auto
   from assms[unfolded s_holding_def, folded wq_def, 
-             unfolded this, unfolded wq_def, folded s_holding_def]
+             unfolded this, folded s_holding_def]
   have "holding s t c"  .
   from that(2)[OF False this] show ?thesis .
 qed
@@ -1795,7 +1796,7 @@
   case False
   hence "wq (e#s) c = wq s c" by auto
   from assms[unfolded s_holding_def, folded wq_def, 
-             unfolded this, unfolded wq_def, folded s_holding_def]
+             unfolded this, folded s_holding_def]
   have "holding s t c"  .
   from that[OF False this] show ?thesis .
 qed
@@ -1829,13 +1830,13 @@
         with waiting(1,2)
         show ?thesis
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
-             fold waiting_eq, auto)
+             fold s_waiting_abv, auto)
       next
         case 2
         with waiting(1,2)
         show ?thesis
          by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
-             fold waiting_eq, auto)
+             fold s_waiting_abv, auto)
       qed
     next
       case True
@@ -1848,7 +1849,7 @@
         with waiting(1,2)
         show ?thesis
         by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 
-             fold waiting_eq, auto)
+             fold s_waiting_abv, auto)
       qed
     qed
   next
@@ -1865,13 +1866,13 @@
         with holding(1,2)
         show ?thesis
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
-             fold waiting_eq, auto)
+             fold s_waiting_abv, auto)
       next
         case 2
         with holding(1,2)
         show ?thesis
          by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
-             fold holding_eq, auto)
+             fold s_holding_abv, auto)
       qed
     next
       case True
@@ -1884,7 +1885,7 @@
         with holding(1,2)
         show ?thesis
         by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 
-             fold holding_eq, auto)
+             fold s_holding_abv, auto)
       qed
     qed
   qed
@@ -1906,7 +1907,7 @@
       assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
       with h_n.holding_taker
       show ?thesis 
-        by (unfold s_RAG_def, fold holding_eq, auto)
+        by (unfold s_RAG_def, fold s_holding_abv, auto)
    next
     assume h: "(n1, n2) \<in> RAG s \<and>
         (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
@@ -1935,7 +1936,7 @@
         qed
       qed
       thus ?thesis using waiting(1,2)
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
     next
       case (holding th' cs')
       from h this(1,2)
@@ -1951,7 +1952,7 @@
         show ?thesis .
       qed
       thus ?thesis using holding(1,2)
-        by (unfold s_RAG_def, fold holding_eq, auto)
+        by (unfold s_RAG_def, fold s_holding_abv, auto)
     qed
    qed
  next
@@ -1967,7 +1968,7 @@
     case (waiting th' cs')
     from h_e.waiting_esI2[OF this(3)]
     show ?thesis using waiting(1,2)
-      by (unfold s_RAG_def, fold waiting_eq, auto)
+      by (unfold s_RAG_def, fold s_waiting_abv, auto)
    next
     case (holding th' cs')
     with h_s(2)
@@ -1977,12 +1978,12 @@
       assume neq_cs: "cs' \<noteq> cs"
       from holding_esI2[OF this holding(3)]
       show ?thesis using holding(1,2)
-        by (unfold s_RAG_def, fold holding_eq, auto)
+        by (unfold s_RAG_def, fold s_holding_abv, auto)
     next
       assume "th' \<noteq> th"
       from holding_esI1[OF holding(3) this]
       show ?thesis using holding(1,2)
-        by (unfold s_RAG_def, fold holding_eq, auto)
+        by (unfold s_RAG_def, fold s_holding_abv, auto)
     qed
    qed
  qed
@@ -2006,7 +2007,7 @@
 proof(cases "cs' = cs")
   case False
   hence "wq (e#s) cs' = wq s cs'" by simp
-  with assms show ?thesis unfolding holding_raw_def holding_eq by auto 
+  with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto 
 next
   case True
   from assms[unfolded s_holding_def, folded wq_def]
@@ -2015,7 +2016,7 @@
   hence "wq (e#s) cs' = th'#(rest@[th])"
     by (simp add: True wq_es_cs) 
   thus ?thesis
-    by (simp add: holding_raw_def holding_eq) 
+    by (simp add: holding_raw_def s_holding_abv) 
 qed
 end 
 
@@ -2038,11 +2039,11 @@
 proof -
   from wq_es_cs'
   have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
-  thus ?thesis unfolding holding_raw_def holding_eq by blast 
+  thus ?thesis unfolding holding_raw_def s_holding_abv by blast 
 qed
 
 lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
-  by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto)
+  by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto)
 
 lemma waiting_esE:
   assumes "waiting (e#s) th' cs'"
@@ -2063,7 +2064,7 @@
 next
   case False
   have "holding s th' cs'" using assms
-    using False unfolding holding_raw_def holding_eq by auto
+    using False unfolding holding_raw_def s_holding_abv by auto
   from that(1)[OF False this] show ?thesis .
 qed
 
@@ -2079,7 +2080,7 @@
     proof(cases rule:waiting_esE)
       case 1
       thus ?thesis using waiting(1,2)
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
     qed
   next
     case (holding th' cs')
@@ -2088,7 +2089,7 @@
     proof(cases rule:holding_esE)
       case 1
       with holding(1,2)
-      show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+      show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
     next
       case 2
       with holding(1,2) show ?thesis by auto
@@ -2106,18 +2107,18 @@
       case (waiting th' cs')
       from waiting_kept[OF this(3)]
       show ?thesis using waiting(1,2)
-         by (unfold s_RAG_def, fold waiting_eq, auto)
+         by (unfold s_RAG_def, fold s_waiting_abv, auto)
     next
       case (holding th' cs')
       from holding_kept[OF this(3)]
       show ?thesis using holding(1,2)
-         by (unfold s_RAG_def, fold holding_eq, auto)
+         by (unfold s_RAG_def, fold s_holding_abv, auto)
     qed
   next
     assume "n1 = Cs cs \<and> n2 = Th th"
     with holding_es_th_cs
     show ?thesis 
-      by (unfold s_RAG_def, fold holding_eq, auto)
+      by (unfold s_RAG_def, fold s_holding_abv, auto)
   qed
 qed
 
@@ -2133,11 +2134,12 @@
   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
-  by (simp add: s_waiting_def wq_def wq_es_cs)
+  using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs
+  using Un_iff list.sel(1) list.set_intros(1) s_waiting_def
+   set_append wq_def wq_es_cs 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)
+   by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto)
 
 lemma holding_esE:
   assumes "holding (e#s) th' cs'"
@@ -2187,7 +2189,7 @@
     proof(cases rule:waiting_esE)
       case 1
       thus ?thesis using waiting(1,2)
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
     next
       case 2
       thus ?thesis using waiting(1,2) by auto
@@ -2199,7 +2201,7 @@
     proof(cases rule:holding_esE)
       case 1
       with holding(1,2)
-      show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+      show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
     qed
   qed
 next
@@ -2214,12 +2216,12 @@
       case (waiting th' cs')
       from waiting_kept[OF this(3)]
       show ?thesis using waiting(1,2)
-         by (unfold s_RAG_def, fold waiting_eq, auto)
+         by (unfold s_RAG_def, fold s_waiting_abv, auto)
     next
       case (holding th' cs')
       from holding_kept[OF this(3)]
       show ?thesis using holding(1,2)
-         by (unfold s_RAG_def, fold holding_eq, auto)
+         by (unfold s_RAG_def, fold s_holding_abv, auto)
     qed
   next
     assume "n1 = Th th \<and> n2 = Cs cs"
@@ -2620,7 +2622,7 @@
                           "(Th taker, Cs cs') \<in> RAG s"
         by (unfold s_RAG_def, auto)
       from this(2) have "waiting s taker cs'" 
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
       from waiting_unique[OF this waiting_taker] 
       have "cs' = cs" .
       from h(1)[unfolded this] show False by auto
@@ -2655,7 +2657,7 @@
       obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
         by (unfold s_RAG_def, auto)
       hence "waiting s th cs'" 
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
       with th_not_waiting show False by auto 
     qed
     ultimately show ?thesis by auto
@@ -2784,7 +2786,7 @@
 begin
 
 lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
-  apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
+  apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv)
   by(auto elim:waiting_unique held_unique)
 
 lemma sgv_RAG: "single_valued (RAG s)"
@@ -2962,11 +2964,11 @@
     obtain n where "(n, b) \<in> RAG s" by auto
     from this[unfolded Cs]
     obtain th1 where "waiting s th1 cs"
-      by (unfold s_RAG_def, fold waiting_eq, auto)
+      by (unfold s_RAG_def, fold s_waiting_abv, auto)
     from waiting_holding[OF this]
     obtain th2 where "holding s th2 cs" .
     hence "(Cs cs, Th th2) \<in> RAG s"
-      by (unfold s_RAG_def, fold holding_eq, auto)
+      by (unfold s_RAG_def, fold s_holding_abv, auto)
     with h_b(2)[unfolded Cs, rule_format]
     have False by auto
     thus ?thesis by auto
@@ -2975,7 +2977,7 @@
   proof -
     from h_b(2)[unfolded eq_b]
     have "\<forall>cs. \<not> waiting s th' cs"
-      by (unfold s_RAG_def, fold waiting_eq, auto)
+      by (unfold s_RAG_def, fold s_waiting_abv, auto)
     moreover have "th' \<in> threads s"
     proof(rule rg_RAG_threads)
       from tranclD[OF h_b(1), unfolded eq_b]
@@ -3123,7 +3125,7 @@
       have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
       from tranclD[OF this]
       obtain cs where "waiting s th1 cs"
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
       with running_1 show False
         by (unfold running_def readys_def, auto)
     qed
@@ -3139,7 +3141,7 @@
       have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
       from tranclD[OF this]
       obtain cs where "waiting s th2 cs"
-        by (unfold s_RAG_def, fold waiting_eq, auto)
+        by (unfold s_RAG_def, fold s_waiting_abv, auto)
       with running_2 show False
         by (unfold running_def readys_def, auto)
     qed
@@ -3232,7 +3234,7 @@
         obtain z where "(Th th1, z) \<in> RAG s" by auto
         from this[unfolded s_RAG_def, folded wq_def]
         obtain cs' where "waiting s th1 cs'"
-          by (auto simp:waiting_eq)
+          by (auto simp:s_waiting_abv)
         with assms(1) show False by (auto simp:readys_def)
       qed
     next
@@ -3251,7 +3253,7 @@
         obtain z where "(Th th2, z) \<in> RAG s" by auto
         from this[unfolded s_RAG_def, folded wq_def]
         obtain cs' where "waiting s th2 cs'"
-          by (auto simp:waiting_eq)
+          by (auto simp:s_waiting_abv)
         with assms(2) show False by (auto simp:readys_def)
       qed
     qed
@@ -3425,10 +3427,10 @@
 begin
 
 lemma holding_s_holder: "holding s holder cs"
-  by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+  by (unfold s_holding_def, unfold wq_s_cs, auto)
 
 lemma holding_es_holder: "holding (e#s) holder cs"
-  by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)
+  by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto)
 
 lemma holdents_es:
   shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") 
@@ -3448,7 +3450,7 @@
       hence "wq (e#s) cs' = wq s cs'" by simp
       from h[unfolded s_holding_def, folded wq_def, unfolded this]
       show ?thesis
-       by (unfold s_holding_def, fold wq_def, auto)
+       by (unfold s_holding_def, auto)
     qed 
     hence "cs' \<in> ?R" by (auto simp:holdents_def)
   } moreover {
@@ -3467,7 +3469,7 @@
       hence "wq s cs' = wq (e#s) cs'" by simp
       from h[unfolded s_holding_def, folded wq_def, unfolded this]
       show ?thesis
-       by (unfold s_holding_def, fold wq_def, auto)
+       by (unfold s_holding_def, auto)
     qed 
     hence "cs' \<in> ?L" by (auto simp:holdents_def)
   } ultimately show ?thesis by auto
@@ -3598,7 +3600,7 @@
     from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]
     have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .
     hence "cs' \<in> ?R" 
-      by (unfold holdents_def s_holding_def, fold wq_def, auto)
+      by (unfold holdents_def s_holding_def, auto)
   } moreover {
     fix cs'
     assume "cs' \<in> ?R"
@@ -3738,7 +3740,7 @@
 
 lemma holding_th_cs_s: 
   "holding s th cs" 
- by  (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+ by  (unfold s_holding_def, unfold wq_s_cs, auto)
 
 lemma th_ready_s [simp]: "th \<in> readys s"
   using running_th_s
@@ -3931,7 +3933,7 @@
       from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
       from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
       show ?thesis
-        by (unfold holdents_def s_holding_def, fold wq_def, auto)
+        by (unfold holdents_def s_holding_def, auto)
     next
       case True
       from h[unfolded this]
@@ -3950,7 +3952,7 @@
       from h have "holding s th' cs'" by (auto simp:holdents_def)
       from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
       show ?thesis
-        by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+        by (unfold holdents_def s_holding_def, insert eq_wq, simp)
     next
       case True
       from h[unfolded this]
@@ -4107,7 +4109,7 @@
       from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
       from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
       show ?thesis
-        by (unfold holdents_def s_holding_def, fold wq_def, auto)
+        by (unfold holdents_def s_holding_def, auto)
     next
       case True
       from h[unfolded this]
@@ -4126,7 +4128,7 @@
       from h have "holding s th' cs'" by (auto simp:holdents_def)
       from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
       show ?thesis
-        by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+        by (unfold holdents_def s_holding_def, insert eq_wq, simp)
     next
       case True
       from h[unfolded this]
@@ -4315,14 +4317,12 @@
   { fix cs'
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -4432,7 +4432,7 @@
   assume "holding (e # s) th cs'"
   from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
   have "holding s th cs'" 
-    by (unfold s_holding_def, fold wq_def, auto)
+    by (unfold s_holding_def, auto)
   with not_holding_th_s 
   show False by simp
 qed
@@ -4462,14 +4462,12 @@
   { fix cs'
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -4567,14 +4565,12 @@
   { fix cs'
     assume h: "cs' \<in> ?L"
     hence "cs' \<in> ?R"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } moreover {
     fix cs'
     assume h: "cs' \<in> ?R"
     hence "cs' \<in> ?L"
-      by (unfold holdents_def s_holding_def, fold wq_def, 
-             unfold wq_kept, auto)
+      by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
   } ultimately show ?thesis by auto
 qed
 
@@ -4639,8 +4635,8 @@
 proof(induct rule:ind)
   case Nil
   thus ?case 
-    by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def 
-              s_holding_def, simp)
+    unfolding cntP_def  cntV_def pvD_def cntCS_def holdents_def s_holding_def
+    by(simp add: wq_def)
 next
   case (Cons s e)
   interpret vt_e: valid_trace_e s e using Cons by simp
@@ -4772,7 +4768,7 @@
 lemma count_eq_tRAG_plus:
   assumes "cntP s th = cntV s th"
   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
-  using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 
+  using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast
 
 lemma count_eq_tRAG_plus_Th:
   assumes "cntP s th = cntV s th"
@@ -4880,7 +4876,7 @@
     with dtc 
     have "th \<in> readys s"
       by (unfold readys_def detached_def Field_def Domain_def Range_def, 
-           auto simp:waiting_eq s_RAG_def)
+           auto simp:s_waiting_abv s_RAG_def)
     with cncs_z  show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)
   next
     case False




