diff -r 031d2ae9c9b8 -r b620a2a0806a PrioG.thy
--- a/PrioG.thy	Tue Dec 22 23:13:31 2015 +0800
+++ b/PrioG.thy	Wed Jan 06 20:46:14 2016 +0800
@@ -2,6 +2,20 @@
 imports PrioGDef 
 begin
 
+locale valid_trace = 
+  fixes s
+  assumes vt : "vt s"
+
+locale valid_trace_e = valid_trace +
+  fixes e
+  assumes vt_e: "vt (e#s)"
+begin
+
+lemma pip_e: "PIP s e"
+  using vt_e by (cases, simp)  
+
+end
+
 lemma runing_ready: 
   shows "runing s \<subseteq> readys s"
   unfolding runing_def readys_def
@@ -16,8 +30,30 @@
    "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
   by (auto simp:wq_def Let_def cp_def split:list.splits)
 
-lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
-proof(erule_tac vt.induct, simp add:wq_def)
+context valid_trace
+begin
+
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+  assumes "PP []"
+     and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
+                   PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+     shows "PP s"
+proof(rule vt.induct[OF vt])
+  from assms(1) show "PP []" .
+next
+  fix s e
+  assume h: "vt s" "PP s" "PIP s e"
+  show "PP (e # s)"
+  proof(cases rule:assms(2))
+    from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
+  next
+    from h(1,3) have "vt (e#s)" by auto
+    thus "valid_trace (e # s)" by (unfold_locales, simp)
+  qed (insert h, auto)
+qed
+
+lemma wq_distinct: "distinct (wq s cs)"
+proof(rule ind, simp add:wq_def)
   fix s e
   assume h1: "step s e"
   and h2: "distinct (wq s cs)"
@@ -51,6 +87,12 @@
   qed
 qed
 
+end
+
+
+context valid_trace_e
+begin
+
 text {*
   The following lemma shows that only the @{text "P"}
   operation can add new thread into waiting queues. 
@@ -59,9 +101,7 @@
 *}
 
 lemma block_pre: 
-  fixes thread cs s
-  assumes vt_e: "vt (e#s)"
-  and s_ni: "thread \<notin>  set (wq s cs)"
+  assumes s_ni: "thread \<notin>  set (wq s cs)"
   and s_i: "thread \<in> set (wq (e#s) cs)"
   shows "e = P thread cs"
 proof -
@@ -85,7 +125,7 @@
       by (auto simp:wq_def Let_def split:if_splits)
   next
     case (V th cs)
-    with assms show ?thesis
+    with vt_e assms show ?thesis
       apply (auto simp:wq_def Let_def split:if_splits)
     proof -
       fix q qs
@@ -98,7 +138,7 @@
       proof -
         have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
         proof(rule someI2)
-          from wq_distinct [OF step_back_vt[OF vt], of cs]
+          from wq_distinct [of cs]
           and h2[symmetric, folded wq_def]
           show "distinct qs \<and> set qs = set qs" by auto
         next
@@ -112,6 +152,8 @@
   qed
 qed
 
+end
+
 text {*
   The following lemmas is also obvious and shallow. It says
   that only running thread can request for a critical resource 
@@ -126,7 +168,6 @@
 by auto
 
 lemma abs1:
-  fixes e es
   assumes ein: "e \<in> set es"
   and neq: "hd es \<noteq> hd (es @ [x])"
   shows "False"
@@ -141,15 +182,17 @@
 
 inductive_cases evt_cons: "vt (a#s)"
 
+context valid_trace_e
+begin
+
 lemma abs2:
-  assumes vt: "vt (e#s)"
-  and inq: "thread \<in> set (wq s cs)"
+  assumes inq: "thread \<in> set (wq s cs)"
   and nh: "thread = hd (wq s cs)"
   and qt: "thread \<noteq> hd (wq (e#s) cs)"
   and inq': "thread \<in> set (wq (e#s) cs)"
   shows "False"
 proof -
-  from assms show "False"
+  from vt_e assms show "False"
     apply (cases e)
     apply ((simp split:if_splits add:Let_def wq_def)[1])+
     apply (insert abs1, fast)[1]
@@ -161,13 +204,13 @@
       and eq_wq: "wq_fun (schs s) cs = thread # qs"
     show "False"
     proof -
-      from wq_distinct[OF step_back_vt[OF vt], of cs]
+      from wq_distinct[of cs]
         and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
       moreover have "thread \<in> set qs"
       proof -
         have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
         proof(rule someI2)
-          from wq_distinct [OF step_back_vt[OF vt], of cs]
+          from wq_distinct [of cs]
           and eq_wq [folded wq_def]
           show "distinct qs \<and> set qs = set qs" by auto
         next
@@ -181,28 +224,33 @@
   qed
 qed
 
-lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-proof(induct s, simp)
-  fix a s t
-  assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-    and vt_a: "vt (a # s)"
-  show "vt (moment t (a # s))"
-  proof(cases "t \<ge> length (a#s)")
+end
+
+context valid_trace
+begin
+
+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 (a#s) = a#s" by simp
-    with vt_a show ?thesis by simp
+    from True have "moment t (e#s) = e#s" by simp
+    thus ?thesis using Cons
+      by (simp add:valid_trace_def)
   next
     case False
-    hence le_t1: "t \<le> length s" by simp
-    from vt_a have "vt s"
-      by (erule_tac evt_cons, simp)
-    from h [OF this] have "vt (moment t s)" .
-    moreover have "moment t (a#s) = moment t s"
+    from Cons have "vt (moment t s)" by simp
+    moreover have "moment t (e#s) = moment t s"
     proof -
-      from moment_app [OF le_t1, of "[a]"] 
+      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 auto
+    ultimately show ?thesis by simp
   qed
 qed
 
@@ -244,9 +292,7 @@
 *}
 
 lemma waiting_unique_pre:
-  fixes cs1 cs2 s thread
-  assumes vt: "vt s"
-  and h11: "thread \<in> set (wq s cs1)"
+  assumes h11: "thread \<in> set (wq s cs1)"
   and h12: "thread \<noteq> hd (wq s cs1)"
   assumes h21: "thread \<in> set (wq s cs2)"
   and h22: "thread \<noteq> hd (wq s cs2)"
@@ -282,25 +328,26 @@
       from nn2 [rule_format, OF this] and eq_m
       have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
         h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
-      have vt_e: "vt (e#moment t2 s)"
+      have "vt (e#moment t2 s)"
       proof -
-        from vt_moment [OF vt]
+        from vt_moment 
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
+      then interpret vt_e: valid_trace_e "moment t2 s" "e"
+        by (unfold_locales, auto, cases, simp)
       have ?thesis
       proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
         case True
         from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
-          by auto
-          thm abs2
-        from abs2 [OF vt_e True eq_th h2 h1]
+          by auto 
+        from vt_e.abs2 [OF True eq_th h2 h1]
         show ?thesis by auto
       next
         case False
-        from block_pre [OF vt_e False h1]
+        from vt_e.block_pre[OF False h1]
         have "e = P thread cs2" .
-        with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
+        with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
         from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
         with runing_ready have "thread \<in> readys (moment t2 s)" by auto
         with nn1 [rule_format, OF lt12]
@@ -316,24 +363,26 @@
       from nn1 [rule_format, OF this] and eq_m
       have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
-      have vt_e: "vt  (e#moment t1 s)"
+      have "vt  (e#moment t1 s)"
       proof -
-        from vt_moment [OF vt]
+        from vt_moment
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
+      then interpret vt_e: valid_trace_e "moment t1 s" e
+        by (unfold_locales, auto, cases, auto)
       have ?thesis
       proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
         case True
         from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
           by auto
-        from abs2 [OF vt_e True eq_th h2 h1]
+        from vt_e.abs2 True eq_th h2 h1
         show ?thesis by auto
       next
         case False
-        from block_pre [OF vt_e False h1]
+        from vt_e.block_pre [OF False h1]
         have "e = P thread cs1" .
-        with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
+        with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
         from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
         with runing_ready have "thread \<in> readys (moment t1 s)" by auto
         with nn2 [rule_format, OF lt12]
@@ -351,20 +400,22 @@
         h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
       have vt_e: "vt (e#moment t1 s)"
       proof -
-        from vt_moment [OF vt]
+        from vt_moment
         have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
+      then interpret vt_e: valid_trace_e "moment t1 s" e
+        by (unfold_locales, auto, cases, auto)
       have ?thesis
       proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
         case True
         from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
           by auto
-        from abs2 [OF vt_e True eq_th h2 h1]
+        from vt_e.abs2 [OF True eq_th h2 h1]
         show ?thesis by auto
       next
         case False
-        from block_pre [OF vt_e False h1]
+        from vt_e.block_pre [OF False h1]
         have eq_e1: "e = P thread cs1" .
         have lt_t3: "t1 < ?t3" by simp
         with eqt12 have "t2 < ?t3" by simp
@@ -377,17 +428,21 @@
           from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
             by auto
           from vt_e and eqt12 have "vt (e#moment t2 s)" by simp 
-          from abs2 [OF this True eq_th h2 h1]
+          then interpret vt_e2: valid_trace_e "moment t2 s" e
+            by (unfold_locales, auto, cases, auto)
+          from vt_e2.abs2 [OF True eq_th h2 h1]
           show ?thesis .
         next
           case False
-          have vt_e: "vt (e#moment t2 s)"
+          have "vt (e#moment t2 s)"
           proof -
-            from vt_moment [OF vt] eqt12
+            from vt_moment eqt12
             have "vt (moment (Suc t2) s)" by auto
             with eq_m eqt12 show ?thesis by simp
           qed
-          from block_pre [OF vt_e False h1]
+          then interpret vt_e2: valid_trace_e "moment t2 s" e
+            by (unfold_locales, auto, cases, auto)
+          from vt_e2.block_pre [OF False h1]
           have "e = P thread cs2" .
           with eq_e1 neq12 show ?thesis by auto
         qed
@@ -401,15 +456,15 @@
 *}
 
 lemma waiting_unique:
-  fixes s cs1 cs2
-  assumes "vt s"
-  and "waiting s th cs1"
+  assumes "waiting s th cs1"
   and "waiting s th cs2"
   shows "cs1 = cs2"
 using waiting_unique_pre assms
 unfolding wq_def s_waiting_def
 by auto
 
+end
+
 (* not used *)
 text {*
   Every thread can only be blocked on one critical resource, 
@@ -417,13 +472,10 @@
   This fact is much more easier according to our definition. 
 *}
 lemma held_unique:
-  fixes s::"state"
-  assumes "holding s th1 cs"
+  assumes "holding (s::event list) th1 cs"
   and "holding s th2 cs"
   shows "th1 = th2"
-using assms
-unfolding s_holding_def
-by auto
+ by (insert assms, unfold s_holding_def, auto)
 
 
 lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
@@ -642,6 +694,8 @@
   assume vt: "vt (V th cs # s)"
     and nw: "\<not> waiting (wq (V th cs # s)) t c"
     and wt: "waiting (wq s) t c"
+  from vt interpret vt_v: valid_trace_e s "V th cs" 
+    by  (cases, unfold_locales, simp)
   show "next_th s th cs t \<and> cs = c"
   proof(cases "cs = c")
     case False
@@ -659,7 +713,7 @@
         and eq_wq: "wq_fun (schs s) cs = a # list"
       have " set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
-        from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+        from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
         show "distinct list \<and> set list = set list" by auto
       next
         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -673,7 +727,7 @@
         and eq_wq: "wq_fun (schs s) cs = a # list"
       have " set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
-        from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+        from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
         show "distinct list \<and> set list = set list" by auto
       next
         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -704,6 +758,8 @@
 proof -
   assume vt: "vt (V th cs # s)"
     and hd: "holding (wq (V th cs # s)) th cs"
+  from vt interpret vt_v: valid_trace_e s "V th cs"
+    by (cases, unfold_locales, simp+)
   from step_back_step [OF vt] and hd
   show "False"
   proof(cases)
@@ -719,7 +775,7 @@
             \<in> set (SOME q. distinct q \<and> set q = set list)"
       have "set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
-        from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+        from vt_v.wq_distinct[of cs] and eq_wq
         show "distinct list \<and> set list = set list" by auto
       next
         show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
@@ -727,7 +783,7 @@
       qed
       moreover have "distinct  (hd (SOME q. distinct q \<and> set q = set list) # list)"
       proof -
-        from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+        from vt_v.wq_distinct[of cs] and eq_wq
         show ?thesis by auto
       qed
       moreover note eq_wq and hd_in
@@ -747,9 +803,11 @@
     and nrest: "rest \<noteq> []"
     and ni: "hd (SOME q. distinct q \<and> set q = set rest)
             \<notin> set (SOME q. distinct q \<and> set q = set rest)"
+  from vt interpret vt_v: valid_trace_e s "V th cs"
+    by (cases, unfold_locales, simp+)
   have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
   proof(rule someI2)
-    from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+    from vt_v.wq_distinct[of cs] and eq_wq
     show "distinct rest \<and> set rest = set rest" by auto
   next
     fix x assume "distinct x \<and> set x = set rest"
@@ -791,6 +849,8 @@
   let ?s' = "(V th cs # s)"
   assume vt: "vt ?s'" 
     and wt: "waiting (wq ?s') t c"
+  from vt interpret vt_v: valid_trace_e s "V th cs"
+    by (cases, unfold_locales, simp+)
   show "waiting (wq s) t c"
   proof(cases "c = cs")
     case False
@@ -809,7 +869,7 @@
         and eq_wq: "wq_fun (schs s) cs = a # list"
       have "set (SOME q. distinct q \<and> set q = set list) = set list"
       proof(rule someI2)
-        from wq_distinct [OF step_back_vt[OF vt], of cs]
+        from vt_v.wq_distinct [of cs]
         and eq_wq[folded wq_def]
         show "distinct list \<and> set list = set list" by auto
       next
@@ -827,7 +887,7 @@
         assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
         moreover have "\<dots> = set list" 
         proof(rule someI2)
-          from wq_distinct [OF step_back_vt[OF vt], of cs]
+          from vt_v.wq_distinct [of cs]
             and eq_wq[folded wq_def]
           show "distinct list \<and> set list = set list" by auto
         next
@@ -836,7 +896,7 @@
         qed
         ultimately show "t \<in> set list" by simp
       qed
-      with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+      with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
       show False by auto
     qed
   qed
@@ -885,19 +945,22 @@
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
   by (unfold s_RAG_def, auto)
 
+context valid_trace
+begin
+
 text {*
   The following lemma shows that @{text "RAG"} is acyclic.
   The overall structure is by induction on the formation of @{text "vt s"}
   and then case analysis on event @{text "e"}, where the non-trivial cases 
   for those for @{text "V"} and @{text "P"} events.
 *}
-lemma acyclic_RAG: 
-  fixes s
-  assumes vt: "vt s"
+lemma acyclic_RAG:
   shows "acyclic (RAG s)"
-using assms
+using vt
 proof(induct)
   case (vt_cons s e)
+  interpret vt_s: valid_trace s using vt_cons(1)
+    by (unfold_locales, simp)
   assume ih: "acyclic (RAG s)"
     and stp: "step s e"
     and vt: "vt s"
@@ -949,8 +1012,8 @@
           hence wt_th': "waiting s ?th' cs'"
             unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
           hence "cs' = cs"
-          proof(rule waiting_unique [OF vt])
-            from eq_wq wq_distinct[OF vt, of cs]
+          proof(rule vt_s.waiting_unique)
+            from eq_wq vt_s.wq_distinct[of cs]
             show "waiting s ?th' cs" 
               apply (unfold s_waiting_def wq_def, auto)
             proof -
@@ -958,7 +1021,7 @@
                 and eq_wq: "wq_fun (schs s) cs = th # rest"
               have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
               proof(rule someI2)
-                from wq_distinct[OF vt, of cs] and eq_wq
+                from vt_s.wq_distinct[of cs] and eq_wq
                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
               next
                 fix x assume "distinct x \<and> set x = set rest"
@@ -968,7 +1031,7 @@
                 set (SOME q. distinct q \<and> set q = set rest)" by auto
               moreover have "\<dots> = set rest" 
               proof(rule someI2)
-                from wq_distinct[OF vt, of cs] and eq_wq
+                from vt_s.wq_distinct[of cs] and eq_wq
                 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
               next
                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -980,7 +1043,7 @@
                 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
               have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
               proof(rule someI2)
-                from wq_distinct[OF vt, of cs] and eq_wq
+                from vt_s.wq_distinct[of cs] and eq_wq
                 show "distinct rest \<and> set rest = set rest" by auto
               next
                 fix x assume "distinct x \<and> set x = set rest"
@@ -990,7 +1053,7 @@
                 set (SOME q. distinct q \<and> set q = set rest)" by auto
               moreover have "\<dots> = set rest" 
               proof(rule someI2)
-                from wq_distinct[OF vt, of cs] and eq_wq
+                from vt_s.wq_distinct[of cs] and eq_wq
                 show "distinct rest \<and> set rest = set rest" by auto
               next
                 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -1066,14 +1129,14 @@
 qed
 
 
-lemma finite_RAG: 
-  fixes s
-  assumes vt: "vt s"
+lemma finite_RAG:
   shows "finite (RAG s)"
 proof -
   from vt show ?thesis
   proof(induct)
     case (vt_cons s e)
+    interpret vt_s: valid_trace s using vt_cons(1)
+      by (unfold_locales, simp)
     assume ih: "finite (RAG s)"
       and stp: "step s e"
       and vt: "vt s"
@@ -1145,32 +1208,35 @@
 text {* Several useful lemmas *}
 
 lemma wf_dep_converse: 
-  fixes s
-  assumes vt: "vt s"
   shows "wf ((RAG s)^-1)"
 proof(rule finite_acyclic_wf_converse)
-  from finite_RAG [OF vt]
+  from finite_RAG 
   show "finite (RAG s)" .
 next
-  from acyclic_RAG[OF vt]
+  from acyclic_RAG
   show "acyclic (RAG s)" .
 qed
 
+end
+
 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
-by (induct l, auto)
+  by (induct l, auto)
 
 lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
   by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
 
+context valid_trace
+begin
+
 lemma wq_threads: 
-  fixes s cs
-  assumes vt: "vt s"
-  and h: "th \<in> set (wq s cs)"
+  assumes h: "th \<in> set (wq s cs)"
   shows "th \<in> threads s"
 proof -
  from vt and h show ?thesis
   proof(induct arbitrary: th cs)
     case (vt_cons s e)
+    interpret vt_s: valid_trace s
+      using vt_cons(1) by (unfold_locales, auto)
     assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
       and stp: "step s e"
       and vt: "vt s"
@@ -1227,7 +1293,7 @@
                 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
                 have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
                 proof(rule someI2)
-                  from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def]
+                  from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
                   show "distinct rest \<and> set rest = set rest" by auto
                 next
                   show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
@@ -1264,14 +1330,13 @@
   qed
 qed
 
-lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
   apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
   by (auto intro:wq_threads)
 
 lemma readys_v_eq:
   fixes th thread cs rest
-  assumes vt: "vt s"
-  and neq_th: "th \<noteq> thread"
+  assumes neq_th: "th \<noteq> thread"
   and eq_wq: "wq s cs = thread#rest"
   and not_in: "th \<notin>  set rest"
   shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
@@ -1292,7 +1357,7 @@
         and eq_wq: "wq_fun (schs s) cs = thread # rest"
       have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
       proof(rule someI2)
-        from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
+        from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
         show "distinct rest \<and> set rest = set rest" by auto
       next
         show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
@@ -1308,10 +1373,9 @@
 *}
 
 lemma chain_building:
-  assumes vt: "vt s"
   shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
 proof -
-  from wf_dep_converse [OF vt]
+  from wf_dep_converse
   have h: "wf ((RAG s)\<inverse>)" .
   show ?thesis
   proof(induct rule:wf_induct [OF h])
@@ -1342,7 +1406,7 @@
           from True and th'_d show ?thesis by auto
         next
           case False
-          from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
+          from th'_d and range_in  have "th' \<in> threads s" by auto
           with False have "Th th' \<in> Domain (RAG s)" 
             by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
           from ih [OF th'_d this]
@@ -1362,9 +1426,7 @@
   The following is just an instance of @{text "chain_building"}.
 *}
 lemma th_chain_to_ready:
-  fixes s th
-  assumes vt: "vt s"
-  and th_in: "th \<in> threads s"
+  assumes th_in: "th \<in> threads s"
   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
 proof(cases "th \<in> readys s")
   case True
@@ -1373,10 +1435,12 @@
   case False
   from False and th_in have "Th th \<in> Domain (RAG s)" 
     by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
-  from chain_building [rule_format, OF vt this]
+  from chain_building [rule_format, OF this]
   show ?thesis by auto
 qed
 
+end
+
 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
   by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
 
@@ -1386,16 +1450,24 @@
 lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
   by (unfold s_holding_def cs_holding_def, auto)
 
-lemma unique_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+context valid_trace
+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)
   by(auto elim:waiting_unique holding_unique)
 
+end
+
+
 lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
 by (induct rule:trancl_induct, auto)
 
+context valid_trace
+begin
+
 lemma dchain_unique:
-  assumes vt: "vt s"
-  and th1_d: "(n, Th th1) \<in> (RAG s)^+"
+  assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
   and th1_r: "th1 \<in> readys s"
   and th2_d: "(n, Th th2) \<in> (RAG s)^+"
   and th2_r: "th2 \<in> readys s"
@@ -1403,7 +1475,7 @@
 proof -
   { assume neq: "th1 \<noteq> th2"
     hence "Th th1 \<noteq> Th th2" by simp
-    from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt]
+    from unique_chain [OF _ th1_d th2_d this] and unique_RAG 
     have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
     hence "False"
     proof
@@ -1427,6 +1499,8 @@
     qed
   } thus ?thesis by auto
 qed
+
+end
              
 
 lemma step_holdents_p_add:
@@ -1450,13 +1524,11 @@
 qed
 
 
-lemma finite_holding:
-  fixes s th cs
-  assumes vt: "vt s"
+lemma (in valid_trace) finite_holding :
   shows "finite (holdents s th)"
 proof -
   let ?F = "\<lambda> (x, y). the_cs x"
-  from finite_RAG [OF vt]
+  from finite_RAG 
   have "finite (RAG s)" .
   hence "finite (?F `(RAG s))" by simp
   moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>" 
@@ -1476,13 +1548,17 @@
   assumes vtv: "vt (V thread cs#s)"
   shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
 proof -
+  from vtv interpret vt_s: valid_trace s
+    by (cases, unfold_locales, simp)
+  from vtv interpret vt_v: valid_trace "V thread cs#s"
+     by (unfold_locales, simp)
   from step_back_step[OF vtv]
   have cs_in: "cs \<in> holdents s thread" 
     apply (cases, unfold holdents_test s_RAG_def, simp)
     by (unfold cs_holding_def s_holding_def wq_def, auto)
   moreover have cs_not_in: 
     "(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
-    apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
+    apply (insert vt_s.wq_distinct[of cs])
     apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
             auto simp:next_th_def)
   proof -
@@ -1536,7 +1612,7 @@
   moreover have "card \<dots> = 
                     Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
   proof(rule card_insert)
-    from finite_holding [OF vtv]
+    from vt_v.finite_holding
     show " finite (holdents (V thread cs # s) thread)" .
   qed
   moreover from cs_not_in 
@@ -1544,20 +1620,22 @@
   ultimately show ?thesis by (simp add:cntCS_def)
 qed 
 
+context valid_trace
+begin
+
 text {* (* ddd *) \noindent
   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 
   of one particular thread. 
 *} 
 
 lemma cnp_cnv_cncs:
-  fixes s th
-  assumes vt: "vt s"
   shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s) 
                                        then cntCS s th else cntCS s th + 1)"
 proof -
   from vt show ?thesis
   proof(induct arbitrary:th)
     case (vt_cons s e)
+    interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
     assume vt: "vt s"
     and ih: "\<And>th. cntP s th  = cntV s th +
                (if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
@@ -1571,7 +1649,7 @@
       proof -
         { fix cs 
           assume "thread \<in> set (wq s cs)"
-          from wq_threads [OF vt this] have "thread \<in> threads s" .
+          from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
           with not_in have "False" by simp
         } with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
           by (auto simp:readys_def threads.simps s_waiting_def 
@@ -1632,6 +1710,8 @@
         and is_runing: "thread \<in> runing s"
         and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
       from thread_P vt stp ih  have vtp: "vt (P thread cs#s)" by auto
+      then interpret vt_p: valid_trace "(P thread cs#s)"
+        by (unfold_locales, simp)
       show ?thesis 
       proof -
         { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1679,7 +1759,7 @@
                   have "?L = insert cs ?R" by auto
                   moreover have "card \<dots> = Suc (card (?R - {cs}))" 
                   proof(rule card_insert)
-                    from finite_holding [OF vt, of thread]
+                    from vt_s.finite_holding [of thread]
                     show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
                       by (unfold holdents_test, simp)
                   qed
@@ -1718,7 +1798,7 @@
                 ultimately have "th = hd (wq (e#s) cs)" by blast
                 with eq_wq have "th = hd (wq s cs @ [th])" by simp
                 hence "th = hd (wq s cs)" using False by auto
-                with False eq_wq wq_distinct [OF vtp, of cs]
+                with False eq_wq vt_p.wq_distinct [of cs]
                 show False by (fold eq_e, auto)
               qed
               moreover from is_runing have "th \<in> threads (e#s)" 
@@ -1737,6 +1817,7 @@
     next
       case (thread_V thread cs)
       from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
+      then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
       assume eq_e: "e = V thread cs"
         and is_runing: "thread \<in> runing s"
         and hold: "holding s thread cs"
@@ -1746,8 +1827,9 @@
       have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
       have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest"
       proof(rule someI2)
-        from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
-        show "distinct rest \<and> set rest = set rest" by auto
+        from vt_v.wq_distinct[of cs] and eq_wq
+        show "distinct rest \<and> set rest = set rest"
+          by (metis distinct.simps(2) vt_s.wq_distinct)
       next
         show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
           by auto
@@ -1782,8 +1864,9 @@
                   proof -
                     assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
                     with eq_set have "thread \<in> set rest" by simp
-                    with wq_distinct[OF step_back_vt[OF vtv], of cs]
-                    and eq_wq show False by auto
+                    with vt_v.wq_distinct[of cs]
+                    and eq_wq show False
+                        by (metis distinct.simps(2) vt_s.wq_distinct)
                   qed
                   thus ?thesis by (simp add:wq_def s_waiting_def)
                 qed
@@ -1819,7 +1902,7 @@
             case False
             have "(th \<in> readys (e # s)) = (th \<in> readys s)"
               apply (insert step_back_vt[OF vtv])
-              by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
+              by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
             moreover have "cntCS (e#s) th = cntCS s th"
               apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
               proof -
@@ -1838,7 +1921,7 @@
                                   " by simp
                     moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
                     proof(rule someI2)
-                      from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+                      from vt_s.wq_distinct[ of cs] and eq_wq
                       show "distinct rest \<and> set rest = set rest" by auto
                     next
                       fix x assume "distinct x \<and> set x = set rest"
@@ -1870,7 +1953,7 @@
                 have "\<not> th \<in> readys s"
                   apply (auto simp:readys_def s_waiting_def)
                   apply (rule_tac x = cs in exI, auto)
-                  by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
+                  by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
                 moreover 
                 from eq_wq and th_in and neq_hd
                 have "\<not> (th \<in> readys (e # s))"
@@ -1885,7 +1968,7 @@
                   apply (unfold eq_e step_RAG_v[OF vtv], 
                          auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def
                                    Let_def cs_holding_def)
-                  by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
+                  by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
                 thus ?thesis by (simp add:cntCS_def)
               qed
               moreover note ih eq_cnp eq_cnv eq_threads
@@ -1902,7 +1985,7 @@
                 assume eq_wq: "wq_fun (schs s) cs = thread # rest"
                   and t_in: "?t \<in> set rest"
                 show "?t \<in> threads s"
-                proof(rule wq_threads[OF step_back_vt[OF vtv]])
+                proof(rule vt_s.wq_threads)
                   from eq_wq and t_in
                   show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
                 qed
@@ -1915,7 +1998,7 @@
                 show "?t = hd (wq_fun (schs s) csa)"
                 proof -
                   { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
-                    from wq_distinct[OF step_back_vt[OF vtv], of cs] and 
+                    from vt_s.wq_distinct[of cs] and 
                     eq_wq[folded wq_def] and t_in eq_wq
                     have "?t \<noteq> thread" by auto
                     with eq_wq and t_in
@@ -1924,7 +2007,7 @@
                     from t_in' neq_hd'
                     have w2: "waiting s ?t csa"
                       by (auto simp:s_waiting_def wq_def)
-                    from waiting_unique[OF step_back_vt[OF vtv] w1 w2]
+                    from vt_s.waiting_unique[OF w1 w2]
                     and neq_cs have "False" by auto
                   } thus ?thesis by auto
                 qed
@@ -1942,7 +2025,7 @@
                 proof -
                   from th_in eq_wq
                   have "th \<in> set (wq s cs)" by simp
-                  from wq_threads [OF step_back_vt[OF vtv] this] 
+                  from vt_s.wq_threads [OF this] 
                   show ?thesis .
                 qed
                 ultimately show ?thesis using ih by auto
@@ -1961,7 +2044,7 @@
                     have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)" 
                       apply (auto simp:image_def)
                       by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
-                    with finite_RAG[OF step_back_vt[OF vtv]]
+                    with vt_s.finite_RAG
                     show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
                   next
                     show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
@@ -2022,14 +2105,14 @@
 qed
 
 lemma not_thread_cncs:
-  fixes th s
-  assumes vt: "vt s"
-  and not_in: "th \<notin> threads s" 
+  assumes not_in: "th \<notin> threads s" 
   shows "cntCS s th = 0"
 proof -
   from vt not_in show ?thesis
   proof(induct arbitrary:th)
     case (vt_cons s e th)
+    interpret vt_s: valid_trace s using vt_cons(1)
+       by (unfold_locales, simp)
     assume vt: "vt s"
       and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
       and stp: "step s e"
@@ -2097,7 +2180,10 @@
           by (simp add:runing_def readys_def)
         ultimately show ?thesis by auto
       qed
-      from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
+      from assms thread_V vt stp ih 
+      have vtv: "vt (V thread cs#s)" by auto
+      then interpret vt_v: valid_trace "(V thread cs#s)"
+        by (unfold_locales, simp)
       from hold obtain rest 
         where eq_wq: "wq s cs = thread # rest"
         by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
@@ -2109,15 +2195,18 @@
           and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
         have "?t \<in> set rest"
         proof(rule someI2)
-          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
-          show "distinct rest \<and> set rest = set rest" by auto
+          from vt_v.wq_distinct[of cs] and eq_wq
+          show "distinct rest \<and> set rest = set rest"
+            by (metis distinct.simps(2) vt_s.wq_distinct) 
         next
           fix x assume "distinct x \<and> set x = set rest" with ne
           show "hd x \<in> set rest" by (cases x, auto)
         qed
         with eq_wq have "?t \<in> set (wq s cs)" by simp
-        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
-        show False by auto
+        from vt_s.wq_threads[OF this] and ni
+        show False
+          using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)` 
+            ni vt_s.wq_threads by blast 
       qed
       moreover note neq_th eq_wq
       ultimately have "cntCS (e # s) th  = cntCS s th"
@@ -2146,13 +2235,16 @@
   qed
 qed
 
+end
+
 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
   by (auto simp:s_waiting_def cs_waiting_def wq_def)
 
+context valid_trace
+begin
+
 lemma dm_RAG_threads:
-  fixes th s
-  assumes vt: "vt s"
-  and in_dom: "(Th th) \<in> Domain (RAG s)"
+  assumes in_dom: "(Th th) \<in> Domain (RAG s)"
   shows "th \<in> threads s"
 proof -
   from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
@@ -2160,9 +2252,11 @@
   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:cs_waiting_def)
-  from wq_threads [OF vt this] show ?thesis .
+  from wq_threads [OF this] show ?thesis .
 qed
 
+end
+
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
@@ -2177,11 +2271,11 @@
 apply(simp add: Let_def)
 done
 
-(* FIXME: NOT NEEDED *)
+context valid_trace
+begin
+
 lemma runing_unique:
-  fixes th1 th2 s
-  assumes vt: "vt s"
-  and runing_1: "th1 \<in> runing s"
+  assumes runing_1: "th1 \<in> runing s"
   and runing_2: "th2 \<in> runing s"
   shows "th1 = th2"
 proof -
@@ -2210,7 +2304,7 @@
               by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
             moreover have "finite \<dots>"
             proof -
-              from finite_RAG[OF vt] have "finite (RAG s)" .
+              from finite_RAG have "finite (RAG s)" .
               hence "finite ((RAG (wq s))\<^sup>+)"
                 apply (unfold finite_trancl)
                 by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2254,7 +2348,7 @@
               by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
             moreover have "finite \<dots>"
             proof -
-              from finite_RAG[OF vt] have "finite (RAG s)" .
+              from finite_RAG have "finite (RAG s)" .
               hence "finite ((RAG (wq s))\<^sup>+)"
                 apply (unfold finite_trancl)
                 by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2289,7 +2383,7 @@
         apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
         by (auto simp:Domain_def)
       hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
-      from dm_RAG_threads[OF vt this] show ?thesis .
+      from dm_RAG_threads[OF this] show ?thesis .
     next
       assume "th1' = th1"
       with runing_1 show ?thesis
@@ -2304,7 +2398,7 @@
         apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
         by (auto simp:Domain_def)
       hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
-      from dm_RAG_threads[OF vt this] show ?thesis .
+      from dm_RAG_threads[OF this] show ?thesis .
     next
       assume "th2' = th2"
       with runing_2 show ?thesis
@@ -2366,7 +2460,7 @@
       from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
         by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
       show ?thesis
-      proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
+      proof(rule dchain_unique[OF h1 _ h2, symmetric])
         from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
         from runing_2 show "th2 \<in> readys s" by (simp add:runing_def) 
       qed
@@ -2375,7 +2469,7 @@
 qed
 
 
-lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+lemma "card (runing s) \<le> 1"
 apply(subgoal_tac "finite (runing s)")
 prefer 2
 apply (metis finite_nat_set_iff_bounded lessI runing_unique)
@@ -2389,6 +2483,9 @@
 apply(auto) 
 done
 
+end
+
+
 lemma create_pre:
   assumes stp: "step s e"
   and not_in: "th \<notin> threads s"
@@ -2447,28 +2544,35 @@
   from that [OF this] show ?thesis .
 qed
 
+context valid_trace
+begin
+
 lemma cnp_cnv_eq:
-  fixes th s
-  assumes "vt s"
-  and "th \<notin> threads s"
+  assumes "th \<notin> threads s"
   shows "cntP s th = cntV s th"
- by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+  using assms
+  using cnp_cnv_cncs not_thread_cncs by auto
+
+end
+
 
 lemma eq_RAG: 
   "RAG (wq s) = RAG s"
 by (unfold cs_RAG_def s_RAG_def, auto)
 
+context valid_trace
+begin
+
 lemma count_eq_dependants:
-  assumes vt: "vt s"
-  and eq_pv: "cntP s th = cntV s th"
+  assumes eq_pv: "cntP s th = cntV s th"
   shows "dependants (wq s) th = {}"
 proof -
-  from cnp_cnv_cncs[OF vt] and eq_pv
+  from cnp_cnv_cncs and eq_pv
   have "cntCS s th = 0" 
     by (auto split:if_splits)
   moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
   proof -
-    from finite_holding[OF vt, of th] show ?thesis
+    from finite_holding[of th] show ?thesis
       by (simp add:holdents_test)
   qed
   ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
@@ -2492,8 +2596,6 @@
 qed
 
 lemma dependants_threads:
-  fixes s th
-  assumes vt: "vt s"
   shows "dependants (wq s) th \<subseteq> threads s"
 proof
   { fix th th'
@@ -2505,7 +2607,7 @@
       with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
       thus ?thesis using eq_RAG by simp
     qed
-    from dm_RAG_threads[OF vt this]
+    from dm_RAG_threads[OF this]
     have "th \<in> threads s" .
   } note hh = this
   fix th1 
@@ -2516,10 +2618,10 @@
 qed
 
 lemma finite_threads:
-  assumes vt: "vt s"
   shows "finite (threads s)"
-using vt
-by (induct) (auto elim: step.cases)
+using vt by (induct) (auto elim: step.cases)
+
+end
 
 lemma Max_f_mono:
   assumes seq: "A \<subseteq> B"
@@ -2534,9 +2636,11 @@
   from fnt and seq show "finite (f ` B)" by auto
 qed
 
+context valid_trace
+begin
+
 lemma cp_le:
-  assumes vt: "vt s"
-  and th_in: "th \<in> threads s"
+  assumes th_in: "th \<in> threads s"
   shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
   show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
@@ -2545,20 +2649,19 @@
   proof(rule Max_f_mono)
     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
   next
-    from finite_threads [OF vt]
+    from finite_threads
     show "finite (threads s)" .
   next
     from th_in
     show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
       apply (auto simp:Domain_def)
-      apply (rule_tac dm_RAG_threads[OF vt])
+      apply (rule_tac dm_RAG_threads)
       apply (unfold trancl_domain [of "RAG s", symmetric])
       by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
   qed
 qed
 
 lemma le_cp:
-  assumes vt: "vt s"
   shows "preced th s \<le> cp s th"
 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
   show "Prc (priority th s) (last_set th s)
@@ -2579,7 +2682,7 @@
             by (rule_tac x = "(Th x, Th th)" in bexI, auto)
           moreover have "finite \<dots>"
           proof -
-            from finite_RAG[OF vt] have "finite (RAG s)" .
+            from finite_RAG have "finite (RAG s)" .
             hence "finite ((RAG (wq s))\<^sup>+)"
               apply (unfold finite_trancl)
               by (auto simp: s_RAG_def cs_RAG_def wq_def)
@@ -2599,7 +2702,6 @@
 qed
 
 lemma max_cp_eq: 
-  assumes vt: "vt s"
   shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
   (is "?l = ?r")
 proof(cases "threads s = {}")
@@ -2609,26 +2711,26 @@
   case False
   have "?l \<in> ((cp s) ` threads s)"
   proof(rule Max_in)
-    from finite_threads[OF vt] 
+    from finite_threads
     show "finite (cp s ` threads s)" by auto
   next
     from False show "cp s ` threads s \<noteq> {}" by auto
   qed
   then obtain th 
     where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
-  have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in])
+  have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
   moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
   proof -
     have "?r \<in> (?f ` ?A)"
     proof(rule Max_in)
-      from finite_threads[OF vt]
+      from finite_threads
       show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
     next
       from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
     qed
     then obtain th' where 
       th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
-    from le_cp [OF vt, of th']  eq_r
+    from le_cp [of th']  eq_r
     have "?r \<le> cp s th'" by auto
     moreover have "\<dots> \<le> cp s th"
     proof(fold eq_l)
@@ -2637,7 +2739,7 @@
         from th_in' show "cp s th' \<in> cp s ` threads s"
           by auto
       next
-        from finite_threads[OF vt]
+        from finite_threads
         show "finite (cp s ` threads s)" by auto
       qed
     qed
@@ -2647,23 +2749,22 @@
 qed
 
 lemma max_cp_readys_threads_pre:
-  assumes vt: "vt s"
-  and np: "threads s \<noteq> {}"
+  assumes np: "threads s \<noteq> {}"
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
-proof(unfold max_cp_eq[OF vt])
+proof(unfold max_cp_eq)
   show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
   proof -
     let ?p = "Max ((\<lambda>th. preced th s) ` threads s)" 
     let ?f = "(\<lambda>th. preced th s)"
     have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
     proof(rule Max_in)
-      from finite_threads[OF vt] show "finite (?f ` threads s)" by simp
+      from finite_threads show "finite (?f ` threads s)" by simp
     next
       from np show "?f ` threads s \<noteq> {}" by simp
     qed
     then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
       by (auto simp:Image_def)
-    from th_chain_to_ready [OF vt tm_in]
+    from th_chain_to_ready [OF tm_in]
     have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
     thus ?thesis
     proof
@@ -2672,7 +2773,7 @@
         and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
       have "cp s th' = ?f tm"
       proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
-        from dependants_threads[OF vt] finite_threads[OF vt]
+        from dependants_threads finite_threads
         show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))" 
           by (auto intro:finite_subset)
       next
@@ -2680,10 +2781,10 @@
         from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
         moreover have "p \<le> \<dots>"
         proof(rule Max_ge)
-          from finite_threads[OF vt]
+          from finite_threads
           show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
         next
-          from p_in and th'_in and dependants_threads[OF vt, of th']
+          from p_in and th'_in and dependants_threads[of th']
           show "p \<in> (\<lambda>th. preced th s) ` threads s"
             by (auto simp:readys_def)
         qed
@@ -2710,18 +2811,18 @@
           apply (unfold cp_eq_cpreced cpreced_def)
           apply (rule Max_mono)
         proof -
-          from dependants_threads [OF vt, of th1] th1_in
+          from dependants_threads [of th1] th1_in
           show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq> 
                  (\<lambda>th. preced th s) ` threads s"
             by (auto simp:readys_def)
         next
           show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
         next
-          from finite_threads[OF vt] 
+          from finite_threads 
           show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
         qed
       next
-        from finite_threads[OF vt]
+        from finite_threads
         show "finite (cp s ` readys s)" by (auto simp:readys_def)
       next
         from th'_in
@@ -2741,16 +2842,16 @@
               assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
               have "y' \<le> preced tm s"
               proof(unfold tm_max, rule Max_ge)
-                from hy' dependants_threads[OF vt, of tm]
+                from hy' dependants_threads[of tm]
                 show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
               next
-                from finite_threads[OF vt] 
+                from finite_threads
                 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
               qed
             } with hy show ?thesis by auto
           qed
         next
-          from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+          from dependants_threads[of tm] finite_threads
           show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
             by (auto intro:finite_subset)
         next
@@ -2761,7 +2862,7 @@
         proof(rule Max_eqI)
           from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
         next
-          from finite_threads[OF vt]
+          from finite_threads
           show "finite (cp s ` readys s)" by (auto simp:readys_def)
         next
           fix y assume "y \<in> cp s ` readys s"
@@ -2771,13 +2872,13 @@
             apply(unfold cp_eq_p h)
             apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
           proof -
-            from finite_threads[OF vt]
+            from finite_threads
             show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
           next
             show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
               by simp
           next
-            from dependants_threads[OF vt, of th1] th1_readys
+            from dependants_threads[of th1] th1_readys
             show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) 
                     \<subseteq> (\<lambda>th. preced th s) ` threads s"
               by (auto simp:readys_def)
@@ -2794,7 +2895,6 @@
   there must be one inside it has the maximum precedence of the whole system. 
 *}
 lemma max_cp_readys_threads:
-  assumes vt: "vt s"
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 proof(cases "threads s = {}")
   case True
@@ -2802,9 +2902,10 @@
     by (auto simp:readys_def)
 next
   case False
-  show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
+  show ?thesis by (rule max_cp_readys_threads_pre[OF False])
 qed
 
+end
 
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
   apply (unfold s_holding_def cs_holding_def wq_def, simp)
@@ -2836,13 +2937,14 @@
 apply(auto)
 done
 
+context valid_trace
+begin
+
 lemma detached_intro:
-  fixes s th
-  assumes vt: "vt s"
-  and eq_pv: "cntP s th = cntV s th"
+  assumes eq_pv: "cntP s th = cntV s th"
   shows "detached s th"
 proof -
- from cnp_cnv_cncs[OF vt]
+ from cnp_cnv_cncs
   have eq_cnt: "cntP s th =
     cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
   hence cncs_zero: "cntCS s th = 0"
@@ -2852,14 +2954,14 @@
   thus ?thesis
   proof
     assume "th \<notin> threads s"
-    with range_in[OF vt] dm_RAG_threads[OF vt]
+    with range_in dm_RAG_threads
     show ?thesis
       by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
   next
     assume "th \<in> readys s"
     moreover have "Th th \<notin> Range (RAG s)"
     proof -
-      from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+      from card_0_eq [OF finite_holding] and cncs_zero
       have "holdents s th = {}"
         by (simp add:cntCS_def)
       thus ?thesis
@@ -2874,12 +2976,10 @@
 qed
 
 lemma detached_elim:
-  fixes s th
-  assumes vt: "vt s"
-  and dtc: "detached s th"
+  assumes dtc: "detached s th"
   shows "cntP s th = cntV s th"
 proof -
-  from cnp_cnv_cncs[OF vt]
+  from cnp_cnv_cncs
   have eq_pv: " cntP s th =
     cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
   have cncs_z: "cntCS s th = 0"
@@ -2904,11 +3004,11 @@
 qed
 
 lemma detached_eq:
-  fixes s th
-  assumes vt: "vt s"
   shows "(detached s th) = (cntP s th = cntV s th)"
   by (insert vt, auto intro:detached_intro detached_elim)
 
+end
+
 text {* 
   The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
   from the concise and miniature model of PIP given in PrioGDef.thy.
@@ -2923,5 +3023,29 @@
   shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
 
- 
+lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+  apply (induct s, simp)
+proof -
+  fix a s
+  assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+    and eq_as: "a # s \<noteq> []"
+  show "last_set th (a # s) < length (a # s)"
+  proof(cases "s \<noteq> []")
+    case False
+    from False show ?thesis
+      by (cases a, auto simp:last_set.simps)
+  next
+    case True
+    from ih [OF True] show ?thesis
+      by (cases a, auto simp:last_set.simps)
+  qed
+qed
+
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+  by (induct s, auto simp:threads.simps)
+
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+  apply (drule_tac th_in_ne)
+  by (unfold preced_def, auto intro: birth_time_lt)
+
 end