--- a/Implementation.thy	Tue Jun 07 13:51:39 2016 +0100
+++ b/Implementation.thy	Thu Jun 09 23:01:36 2016 +0100
@@ -2,14 +2,14 @@
 imports PIPBasics
 begin
 
-section {*
-  This file contains lemmas used to guide the recalculation of current precedence 
-  after every step of execution (or system operation, or event), 
+text {*
+
+  This file contains lemmas used to guide the recalculation of current
+  precedence after every step of execution (or system operation, or event),
   which is the most tricky part in the implementation of PIP.
 
-  Following convention, lemmas are grouped into locales corresponding to 
-  system operations, each explained in a separate section.
-*}
+  Following convention, lemmas are grouped into locales corresponding to
+  system operations, each explained in a separate section. *}
 
 text {*
   The following two lemmas are general about any valid system state, 
@@ -22,17 +22,9 @@
 lemma readys_root:
   assumes "th \<in> readys s"
   shows "root (RAG s) (Th th)"
-proof -
-  { fix x
-    assume "x \<in> ancestors (RAG s) (Th th)"
-    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-    from tranclD[OF this]
-    obtain z where "(Th th, z) \<in> RAG s" by auto
-    with assms(1) have False
-         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw)
-         by (fold wq_def, blast)
-  } thus ?thesis by (unfold root_def, auto)
-qed
+  unfolding root_def ancestors_def
+  using readys_RAG assms
+by (metis Collect_empty_eq Domain.DomainI trancl_domain)
 
 lemma readys_in_no_subtree:
   assumes "th \<in> readys s"
@@ -668,17 +660,18 @@
   have "Th th \<notin> Range (RAG s)"
   proof
     assume "Th th \<in> Range (RAG s)"
-    then obtain cs where "holding_raw (wq s) th cs"
-      by (unfold Range_iff s_RAG_def, auto)
-    with holdents_th_s[unfolded holdents_def]
-    show False by (unfold holding_eq, auto)
+    then obtain cs where "holding s th cs"
+    by (simp add: holdents_RAG holdents_th_s)
+    then show False by (unfold holding_eq, auto)
   qed
   moreover have "Th th \<notin> Domain (RAG s)"
   proof
     assume "Th th \<in> Domain (RAG s)"
-    then obtain cs where "waiting_raw (wq s) th cs"
-      by (unfold Domain_iff s_RAG_def, auto)
-    with th_ready_s show False by (unfold readys_def waiting_eq, auto)
+    then obtain cs where "waiting s th cs"
+    by (simp add: readys_RAG)
+    then show False
+    using RAG_es \<open>Th th \<in> Domain (RAG s)\<close> 
+    th_not_live_es valid_trace.dm_RAG_threads vat_es.valid_trace_axioms by blast
   qed
   ultimately show ?thesis by (auto simp:Field_def)
 qed