diff -r 30ed212f268a -r b769f43deb30 Implementation.thy
--- a/Implementation.thy	Thu Feb 04 00:43:05 2016 +0000
+++ b/Implementation.thy	Thu Feb 04 14:45:30 2016 +0800
@@ -241,8 +241,6 @@
 context valid_trace_v_e
 begin
 
-find_theorems RAG s e
-
 lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}"
   by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
 
@@ -269,35 +267,29 @@
     by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp)
 
 lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}"
+  (is "?L = ?R")
 proof -
   { fix n
-    have "(Cs cs) \<notin> ancestors (RAG s) n"
-    proof
-      assume "Cs cs \<in> ancestors (RAG s) n"
-      hence "(n, Cs cs) \<in> (RAG s)^+" by (auto simp:ancestors_def)
-      from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s" by auto
-      then obtain th' where "nn = Th th'"
-        by (unfold s_RAG_def, auto)
-      from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s" .
-      from this[unfolded s_RAG_def]
-      have "waiting (wq s) th' cs" by auto
-      from this[unfolded cs_waiting_def]
-      have "1 < length (wq s cs)"
-          by (cases "wq s cs", auto)
-      from holding_next_thI[OF holding_th_cs_s this]
-      obtain th' where "next_th s th cs th'" by auto
-      thus False using no_taker by blast
-    qed
-  } note h = this
-  {  fix n
-     assume "n \<in> subtree (RAG s) (Cs cs)"
-     hence "n = (Cs cs)"
-     by (elim subtreeE, insert h, auto)
-  } moreover have "(Cs cs) \<in> subtree (RAG s) (Cs cs)"
-      by (auto simp:subtree_def)
-  ultimately show ?thesis by auto 
+    assume "n \<in> ?L"
+    hence "n \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 2
+      from this(2) have "(n, Cs cs) \<in> (RAG s)^+"
+        by (auto simp:ancestors_def)
+      from tranclD2[OF this]
+      obtain th' where "waiting s th' cs"
+        by (auto simp:s_RAG_def waiting_eq)
+      with no_waiter_before 
+      show ?thesis by simp
+    qed simp
+  } moreover {
+    fix n
+    assume "n \<in> ?R"
+    hence "n \<in> ?L" by (auto simp:subtree_def)
+  } ultimately show ?thesis by auto
 qed
 
+
 lemma subtree_th: 
   "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
 proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)