--- a/PIPBasics.thy	Tue Jun 14 13:56:51 2016 +0100
+++ b/PIPBasics.thy	Tue Jun 14 15:06:16 2016 +0100
@@ -511,10 +511,12 @@
   } ultimately show ?thesis by blast
 qed
 
+(*
 lemma image_eq:
   assumes "A = B"
   shows "f ` A = f ` B"
   using assms by auto
+*)
 
 lemma tRAG_trancl_eq_Th:
    "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
@@ -907,40 +909,6 @@
   qed
 qed
 
-text {*
-  The following lemma says that if @{text "s"} is a valid state, so 
-  is its any postfix. Where @{term "monent t s"} is the postfix of 
-  @{term "s"} with length @{term "t"}.
-*}
-lemma  vt_moment: "\<And> t. vt (moment t s)"
-proof(induct rule:ind)
-  case Nil
-  thus ?case by (simp add:vt_nil)
-next
-  case (Cons s e t)
-  show ?case
-  proof(cases "t \<ge> length (e#s)")
-    case True
-    from True have "moment t (e#s) = e#s" by simp
-    thus ?thesis using Cons
-      by (simp add:valid_trace_def valid_trace_e_def, auto)
-  next
-    case False
-    from Cons have "vt (moment t s)" by simp
-    moreover have "moment t (e#s) = moment t s"
-    proof -
-      from False have "t \<le> length s" by simp
-      from moment_app [OF this, of "[e]"] 
-      show ?thesis by simp
-    qed
-    ultimately show ?thesis by simp
-  qed
-qed
-
-text {*
-  The following two lemmas are fundamental, because they assure
-  that the numbers of both living and ready threads are finite.
-*}
 
 lemma finite_threads:
   shows "finite (threads s)"
@@ -951,34 +919,6 @@
 
 end
 
-text {*
-  The following locale @{text "valid_moment"} is to inherit the properties 
-  derived on any valid state to the prefix of it, with length @{text "i"}.
-*}
-locale valid_moment = valid_trace + 
-  fixes i :: nat
-
-sublocale valid_moment < vat_moment: valid_trace "(moment i s)"
-  by (unfold_locales, insert vt_moment, auto)
-
-locale valid_moment_e = valid_moment +
-  assumes less_i: "i < length s"
-begin
-  definition "next_e  = hd (moment (Suc i) s)"
-
-  lemma trace_e: 
-    "moment (Suc i) s = next_e#moment i s"
-   proof -
-    from less_i have "Suc i \<le> length s" by auto
-    from moment_plus[OF this, folded next_e_def]
-    show ?thesis .
-   qed
-
-end
-
-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)
 
 section {* Waiting queues are distinct *}
 
@@ -1385,13 +1325,16 @@
 
 end
 
+context valid_trace
+begin
+
 text {*
   The is the main lemma of this section, which is derived
   by induction, case analysis on event @{text e} and 
   assembling the @{text "wq_threads_kept"}-results of 
   all possible cases of @{text "e"}.
 *}
-lemma (in valid_trace) wq_threads: 
+lemma wq_threads: 
   assumes "th \<in> set (wq s cs)"
   shows "th \<in> threads s"
   using assms
@@ -1432,8 +1375,6 @@
 
 subsection {* RAG and threads *}
 
-context valid_trace
-begin
 
 text {*
   As corollaries of @{thm wq_threads}, it is shown in this subsection
@@ -1869,7 +1810,7 @@
   "RAG (e # s) =
    RAG s - {(Cs cs, Th th)} -
      {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
-     {(Cs cs, Th th') |th'.  next_th s th cs th'}" (is "?L = ?R")
+     {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R")
 proof(rule rel_eqI)
   fix n1 n2
   assume "(n1, n2) \<in> ?L"
@@ -3208,14 +3149,15 @@
   qed
 qed
 
-lemma card_running: "card (running s) \<le> 1"
+lemma card_running: 
+  shows "card (running s) \<le> 1"
 proof(cases "running s = {}")
   case True
   thus ?thesis by auto
 next
   case False
-  then obtain th where [simp]: "th \<in> running s" by auto
-  from running_unique[OF this]
+  then obtain th where "th \<in> running s" by auto
+  with running_unique
   have "running s = {th}" by auto
   thus ?thesis by auto
 qed