diff -r 0a4be67ea7f8 -r f2e0d031a395 prio/PrioG.thy
--- a/prio/PrioG.thy	Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/PrioG.thy	Sun Feb 12 04:45:20 2012 +0000
@@ -9,7 +9,7 @@
    "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 step s \<Longrightarrow> distinct (wq s cs)"
+lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
 proof(erule_tac vt.induct, simp add:wq_def)
   fix s e
   assume h1: "step s e"
@@ -44,15 +44,15 @@
   qed
 qed
 
-lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"
-  by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
+  by(ind_cases "vt (e#s)", simp)
 
-lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"
-  by(ind_cases "vt ccs (e#s)", simp)
+lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
+  by(ind_cases "vt (e#s)", simp)
 
 lemma block_pre: 
   fixes thread cs s
-  assumes vt_e: "vt step (e#s)"
+  assumes vt_e: "vt (e#s)"
   and s_ni: "thread \<notin>  set (wq s cs)"
   and s_i: "thread \<in> set (wq (e#s) cs)"
   shows "e = P thread cs"
@@ -84,7 +84,7 @@
       assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
         and h2: "q # qs = wq_fun (schs s) cs"
         and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
-        and vt: "vt step (V th cs # s)"
+        and vt: "vt (V th cs # s)"
       from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
       moreover have "thread \<in> set qs"
       proof -
@@ -104,9 +104,9 @@
   qed
 qed
 
-lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 
+lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 
   thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (depend s)^+"
-apply (ind_cases "vt step ((P thread cs)#s)")
+apply (ind_cases "vt ((P thread cs)#s)")
 apply (ind_cases "step s (P thread cs)")
 by auto
 
@@ -124,10 +124,10 @@
 lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
   by (cases es, auto)
 
-inductive_cases evt_cons: "vt cs (a#s)"
+inductive_cases evt_cons: "vt (a#s)"
 
 lemma abs2:
-  assumes vt: "vt step (e#s)"
+  assumes vt: "vt (e#s)"
   and inq: "thread \<in> set (wq s cs)"
   and nh: "thread = hd (wq s cs)"
   and qt: "thread \<noteq> hd (wq (e#s) cs)"
@@ -141,7 +141,7 @@
     apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
   proof -
     fix th qs
-    assume vt: "vt step (V th cs # s)"
+    assume vt: "vt (V th cs # s)"
       and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
       and eq_wq: "wq_fun (schs s) cs = thread # qs"
     show "False"
@@ -166,13 +166,13 @@
   qed
 qed
 
-lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
+lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
 proof(induct s, simp)
   fix a s t
-  assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
-    and vt_a: "vt cs (a # s)"
+  assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+    and vt_a: "vt (a # s)"
     and le_t: "t \<le> length (a # s)"
-  show "vt cs (moment t (a # s))"
+  show "vt (moment t (a # s))"
   proof(cases "t = length (a#s)")
     case True
     from True have "moment t (a#s) = a#s" by simp
@@ -180,9 +180,9 @@
   next
     case False
     with le_t have le_t1: "t \<le> length s" by simp
-    from vt_a have "vt cs s"
+    from vt_a have "vt s"
       by (erule_tac evt_cons, simp)
-    from h [OF this le_t1] have "vt cs (moment t s)" .
+    from h [OF this le_t1] have "vt (moment t s)" .
     moreover have "moment t (a#s) = moment t s"
     proof -
       from moment_app [OF le_t1, of "[a]"] 
@@ -198,7 +198,7 @@
 
 lemma waiting_unique_pre:
   fixes cs1 cs2 s thread
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and h11: "thread \<in> set (wq s cs1)"
   and h12: "thread \<noteq> hd (wq s cs1)"
   assumes h21: "thread \<in> set (wq s cs2)"
@@ -235,10 +235,10 @@
       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 step (e#moment t2 s)"
+      have vt_e: "vt (e#moment t2 s)"
       proof -
         from vt_moment [OF vt le_t3]
-        have "vt step (moment ?t3 s)" .
+        have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
       have ?thesis
@@ -252,11 +252,11 @@
         case False
         from block_pre [OF vt_e False h1]
         have "e = P thread cs2" .
-        with vt_e have "vt step ((P thread cs2)# moment t2 s)" by simp
+        with 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]
-        show ?thesis  by (simp add:readys_def s_waiting_def, auto)
+        show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
       qed
     } moreover {
       assume lt12: "t2 < t1"
@@ -268,10 +268,10 @@
       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 step (e#moment t1 s)"
+      have vt_e: "vt  (e#moment t1 s)"
       proof -
         from vt_moment [OF vt le_t3]
-        have "vt step (moment ?t3 s)" .
+        have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
       have ?thesis
@@ -285,11 +285,11 @@
         case False
         from block_pre [OF vt_e False h1]
         have "e = P thread cs1" .
-        with vt_e have "vt step ((P thread cs1)# moment t1 s)" by simp
+        with 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]
-        show ?thesis  by (simp add:readys_def s_waiting_def, auto)
+        show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
       qed
     } moreover {
       assume eqt12: "t1 = t2"
@@ -301,10 +301,10 @@
       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 step (e#moment t1 s)"
+      have vt_e: "vt (e#moment t1 s)"
       proof -
         from vt_moment [OF vt le_t3]
-        have "vt step (moment ?t3 s)" .
+        have "vt (moment ?t3 s)" .
         with eq_m show ?thesis by simp
       qed
       have ?thesis
@@ -328,15 +328,15 @@
           case True
           from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
             by auto
-          from vt_e and eqt12 have "vt step (e#moment t2 s)" by simp 
+          from vt_e and eqt12 have "vt (e#moment t2 s)" by simp 
           from abs2 [OF this True eq_th h2 h1]
           show ?thesis .
         next
           case False
-          have vt_e: "vt step (e#moment t2 s)"
+          have vt_e: "vt (e#moment t2 s)"
           proof -
             from vt_moment [OF vt le_t3] eqt12
-            have "vt step (moment (Suc t2) s)" by auto
+            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]
@@ -350,18 +350,18 @@
 
 lemma waiting_unique:
   fixes s cs1 cs2
-  assumes "vt step s"
+  assumes "vt s"
   and "waiting s th cs1"
   and "waiting s th cs2"
   shows "cs1 = cs2"
 proof -
   from waiting_unique_pre and prems
   show ?thesis
-    by (auto simp add:s_waiting_def)
+    by (auto simp add: wq_def s_waiting_def)
 qed
 
 lemma held_unique:
-  assumes "vt step s"
+  assumes "vt s"
   and "holding s th1 cs"
   and "holding s th2 cs"
   shows "th1 = th2"
@@ -512,11 +512,11 @@
 
 
 lemma step_v_hold_inv[elim_format]:
-  "\<And>c t. \<lbrakk>vt step (V th cs # s); 
+  "\<And>c t. \<lbrakk>vt (V th cs # s); 
   \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
 proof -
   fix c t
-  assume vt: "vt step (V th cs # s)"
+  assume vt: "vt (V th cs # s)"
     and nhd: "\<not> holding (wq s) t c"
     and hd: "holding (wq (V th cs # s)) t c"
   show "next_th s th cs t \<and> c = cs"
@@ -561,12 +561,12 @@
 qed
 
 lemma step_v_wait_inv[elim_format]:
-    "\<And>t c. \<lbrakk>vt step (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
+    "\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
            \<rbrakk>
           \<Longrightarrow> (next_th s th cs t \<and> cs = c)"
 proof -
   fix t c 
-  assume vt: "vt step (V th cs # s)"
+  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"
   show "next_th s th cs t \<and> cs = c"
@@ -623,13 +623,13 @@
 qed
 
 lemma step_v_not_wait[consumes 3]:
-  "\<lbrakk>vt step (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
+  "\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
   by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)
 
 lemma step_v_release:
-  "\<lbrakk>vt step (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
+  "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
 proof -
-  assume vt: "vt step (V th cs # s)"
+  assume vt: "vt (V th cs # s)"
     and hd: "holding (wq (V th cs # s)) th cs"
   from step_back_step [OF vt] and hd
   show "False"
@@ -664,12 +664,12 @@
 qed
 
 lemma step_v_get_hold:
-  "\<And>th'. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
+  "\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
   apply (unfold cs_holding_def next_th_def wq_def,
          auto simp:Let_def)
 proof -
   fix rest
-  assume vt: "vt step (V th cs # s)"
+  assume vt: "vt (V th cs # s)"
     and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
     and nrest: "rest \<noteq> []"
     and ni: "hd (SOME q. distinct q \<and> set q = set rest)
@@ -688,12 +688,12 @@
 qed
 
 lemma step_v_release_inv[elim_format]:
-"\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> 
+"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow> 
   c = cs \<and> t = th"
   apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
   proof -
     fix a list
-    assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+    assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
     from step_back_step [OF vt] show "a = th"
     proof(cases)
       assume "holding s th cs" with eq_wq
@@ -702,7 +702,7 @@
     qed
   next
     fix a list
-    assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+    assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
     from step_back_step [OF vt] show "a = th"
     proof(cases)
       assume "holding s th cs" with eq_wq
@@ -712,11 +712,11 @@
   qed
 
 lemma step_v_waiting_mono:
-  "\<And>t c. \<lbrakk>vt step (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
+  "\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
 proof -
   fix t c
   let ?s' = "(V th cs # s)"
-  assume vt: "vt step ?s'" 
+  assume vt: "vt ?s'" 
     and wt: "waiting (wq ?s') t c"
   show "waiting (wq s) t c"
   proof(cases "c = cs")
@@ -772,7 +772,7 @@
 lemma step_depend_v:
 fixes th::thread
 assumes vt:
-  "vt step (V th cs#s)"
+  "vt (V th cs#s)"
 shows "
   depend (V th cs # s) =
   depend s - {(Cs cs, Th th)} -
@@ -787,7 +787,7 @@
   done
 
 lemma step_depend_p:
-  "vt step (P th cs#s) \<Longrightarrow>
+  "vt (P th cs#s) \<Longrightarrow>
   depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
                                              else depend s \<union> {(Th th, Cs cs)})"
   apply(simp only: s_depend_def wq_def)
@@ -816,7 +816,7 @@
 
 lemma acyclic_depend: 
   fixes s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "acyclic (depend s)"
 proof -
   from vt show ?thesis
@@ -824,7 +824,7 @@
     case (vt_cons s e)
     assume ih: "acyclic (depend s)"
       and stp: "step s e"
-      and vt: "vt step s"
+      and vt: "vt s"
     show ?case
     proof(cases e)
       case (Create th prio)
@@ -835,7 +835,7 @@
       with ih show ?thesis by (simp add:depend_exit_unchanged)
     next
       case (V th cs)
-      from V vt stp have vtt: "vt step (V th cs#s)" by auto
+      from V vt stp have vtt: "vt (V th cs#s)" by auto
       from step_depend_v [OF this]
       have eq_de: 
         "depend (e # s) = 
@@ -849,7 +849,7 @@
       proof(cases)
         assume "holding s th cs"
         hence th_in: "th \<in> set (wq s cs)" and
-          eq_hd: "th = hd (wq s cs)" by (unfold s_holding_def, auto)
+          eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
         then obtain rest where
           eq_wq: "wq s cs = th#rest"
           by (cases "wq s cs", auto)
@@ -871,19 +871,19 @@
             obtain cs' where eq_x: "x = Cs cs'" by auto
             with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
             hence wt_th': "waiting s ?th' cs'"
-              unfolding s_depend_def s_waiting_def cs_waiting_def by simp
+              unfolding s_depend_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]
               show "waiting s ?th' cs" 
-                apply (unfold s_waiting_def, auto)
+                apply (unfold s_waiting_def wq_def, auto)
               proof -
                 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
-                and eq_wq: "wq s cs = th # rest"
+                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
-                  show "distinct rest \<and> set rest = set rest" by auto
+                  show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
                 next
                   fix x assume "distinct x \<and> set x = set rest"
                   with False show "x \<noteq> []" by auto
@@ -893,7 +893,7 @@
                 moreover have "\<dots> = set rest" 
                 proof(rule someI2)
                   from wq_distinct[OF vt, of cs] and eq_wq
-                  show "distinct rest \<and> set rest = set rest" by auto
+                  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
                 qed
@@ -940,7 +940,7 @@
       qed
   next
     case (P th cs)
-    from P vt stp have vtt: "vt step (P th cs#s)" by auto
+    from P vt stp have vtt: "vt (P th cs#s)" by auto
     from step_depend_p [OF this] P
     have "depend (e # s) = 
       (if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else 
@@ -992,7 +992,7 @@
 
 lemma finite_depend: 
   fixes s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "finite (depend s)"
 proof -
   from vt show ?thesis
@@ -1000,7 +1000,7 @@
     case (vt_cons s e)
     assume ih: "finite (depend s)"
       and stp: "step s e"
-      and vt: "vt step s"
+      and vt: "vt s"
     show ?case
     proof(cases e)
       case (Create th prio)
@@ -1011,7 +1011,7 @@
       with ih show ?thesis by (simp add:depend_exit_unchanged)
     next
       case (V th cs)
-      from V vt stp have vtt: "vt step (V th cs#s)" by auto
+      from V vt stp have vtt: "vt (V th cs#s)" by auto
       from step_depend_v [OF this]
       have eq_de: "depend (e # s) = 
                    depend s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
@@ -1035,7 +1035,7 @@
       ultimately show ?thesis by simp
     next
       case (P th cs)
-      from P vt stp have vtt: "vt step (P th cs#s)" by auto
+      from P vt stp have vtt: "vt (P th cs#s)" by auto
       from step_depend_p [OF this] P
       have "depend (e # s) = 
               (if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else 
@@ -1069,7 +1069,7 @@
 
 lemma wf_dep_converse: 
   fixes s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "wf ((depend s)^-1)"
 proof(rule finite_acyclic_wf_converse)
   from finite_depend [OF vt]
@@ -1087,7 +1087,7 @@
 
 lemma wq_threads: 
   fixes s cs
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and h: "th \<in> set (wq s cs)"
   shows "th \<in> threads s"
 proof -
@@ -1096,7 +1096,7 @@
     case (vt_cons s e)
     assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
       and stp: "step s e"
-      and vt: "vt step s"
+      and vt: "vt s"
       and h: "th \<in> set (wq (e # s) cs)"
     show ?case
     proof(cases e)
@@ -1187,13 +1187,13 @@
   qed
 qed
 
-lemma range_in: "\<lbrakk>vt step s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
   apply(unfold s_depend_def cs_waiting_def cs_holding_def)
   by (auto intro:wq_threads)
 
 lemma readys_v_eq:
   fixes th thread cs rest
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and neq_th: "th \<noteq> thread"
   and eq_wq: "wq s cs = thread#rest"
   and not_in: "th \<notin>  set rest"
@@ -1201,19 +1201,21 @@
 proof -
   from prems show ?thesis
     apply (auto simp:readys_def)
-    apply (case_tac "cs = csa", simp add:s_waiting_def)
+    apply(simp add:s_waiting_def[folded wq_def])
     apply (erule_tac x = csa in allE)
     apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
     apply (case_tac "csa = cs", simp)
     apply (erule_tac x = cs in allE)
+    apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
+    apply(auto simp add: wq_def)
     apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
     proof -
-      assume th_nin: "th \<notin> set rest"
+       assume th_nin: "th \<notin> set rest"
         and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
         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] and eq_wq[folded wq_def]
+        from wq_distinct[OF vt, 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
@@ -1223,7 +1225,7 @@
 qed
 
 lemma chain_building:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)"
 proof -
   from wf_dep_converse [OF vt]
@@ -1259,7 +1261,7 @@
           case False
           from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
           with False have "Th th' \<in> Domain (depend s)" 
-            by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+            by (auto simp:readys_def wq_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
           from ih [OF th'_d this]
           obtain th'' where 
             th''_r: "th'' \<in> readys s" and 
@@ -1275,7 +1277,7 @@
 
 lemma th_chain_to_ready:
   fixes s th
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and th_in: "th \<in> threads s"
   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (depend s)^+)"
 proof(cases "th \<in> readys s")
@@ -1284,21 +1286,21 @@
 next
   case False
   from False and th_in have "Th th \<in> Domain (depend s)" 
-    by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+    by (auto simp:readys_def s_waiting_def s_depend_def wq_def cs_waiting_def Domain_def)
   from chain_building [rule_format, OF vt this]
   show ?thesis by auto
 qed
 
 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
-  by  (unfold s_waiting_def cs_waiting_def, auto)
+  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
 
 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
-  by (unfold s_holding_def cs_holding_def, simp)
+  by (unfold s_holding_def wq_def cs_holding_def, simp)
 
 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_depend: "\<lbrakk>vt step s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
+lemma unique_depend: "\<lbrakk>vt s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
   apply(unfold s_depend_def, auto, fold waiting_eq holding_eq)
   by(auto elim:waiting_unique holding_unique)
 
@@ -1306,7 +1308,7 @@
 by (induct rule:trancl_induct, auto)
 
 lemma dchain_unique:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and th1_d: "(n, Th th1) \<in> (depend s)^+"
   and th1_r: "th1 \<in> readys s"
   and th2_d: "(n, Th th2) \<in> (depend s)^+"
@@ -1325,7 +1327,7 @@
       then obtain cs where eq_n: "n = Cs cs"
         by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
       from dd eq_n have "th1 \<notin> readys s"
-        by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+        by (auto simp:readys_def s_depend_def wq_def s_waiting_def cs_waiting_def)
       with th1_r show ?thesis by auto
     next
       assume "(Th th2, Th th1) \<in> (depend s)\<^sup>+"
@@ -1334,7 +1336,7 @@
       then obtain cs where eq_n: "n = Cs cs"
         by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
       from dd eq_n have "th2 \<notin> readys s"
-        by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+        by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
       with th2_r show ?thesis by auto
     qed
   } thus ?thesis by auto
@@ -1343,7 +1345,7 @@
 
 lemma step_holdents_p_add:
   fixes th cs s
-  assumes vt: "vt step (P th cs#s)"
+  assumes vt: "vt (P th cs#s)"
   and "wq s cs = []"
   shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
 proof -
@@ -1353,7 +1355,7 @@
 
 lemma step_holdents_p_eq:
   fixes th cs s
-  assumes vt: "vt step (P th cs#s)"
+  assumes vt: "vt (P th cs#s)"
   and "wq s cs \<noteq> []"
   shows "holdents (P th cs#s) th = holdents s th"
 proof -
@@ -1364,7 +1366,7 @@
 
 lemma finite_holding:
   fixes s th cs
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "finite (holdents s th)"
 proof -
   let ?F = "\<lambda> (x, y). the_cs x"
@@ -1385,13 +1387,13 @@
 
 lemma cntCS_v_dec: 
   fixes s thread cs
-  assumes vtv: "vt step (V thread cs#s)"
+  assumes vtv: "vt (V thread cs#s)"
   shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
 proof -
   from step_back_step[OF vtv]
   have cs_in: "cs \<in> holdents s thread" 
     apply (cases, unfold holdents_def s_depend_def, simp)
-    by (unfold cs_holding_def s_holding_def, auto)
+    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])
@@ -1458,14 +1460,14 @@
 
 lemma cnp_cnv_cncs:
   fixes s th
-  assumes vt: "vt step s"
+  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)
-    assume vt: "vt step s"
+    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)"
     and stp: "step s e"
@@ -1519,10 +1521,9 @@
           (th \<in> readys (s) \<or> th \<notin> threads (s))" 
           apply (simp add:threads.simps readys_def)
           apply (subst s_waiting_def)
-          apply (subst (1 2) wq_def)
           apply (simp add:Let_def)
           apply (subst s_waiting_def, simp)
-          by (fold wq_def, simp)
+          done
         with eq_cnp eq_cnv eq_cncs ih
         have ?thesis by simp
       } moreover {
@@ -1539,7 +1540,7 @@
       assume eq_e: "e = P thread cs"
         and is_runing: "thread \<in> runing s"
         and no_dep: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
-      from prems have vtp: "vt step (P thread cs#s)" by auto
+      from prems have vtp: "vt (P thread cs#s)" by auto
       show ?thesis 
       proof -
         { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
@@ -1621,7 +1622,7 @@
                 hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def)
                 from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" .
                 hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)" 
-                  by (simp add:s_waiting_def)
+                  by (simp add:s_waiting_def wq_def)
                 moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto
                 ultimately have "th = hd (wq (e#s) cs)" by blast
                 with eq_wq have "th = hd (wq s cs @ [th])" by simp
@@ -1644,13 +1645,13 @@
       qed
     next
       case (thread_V thread cs)
-      from prems have vtv: "vt step (V thread cs # s)" by auto
+      from prems have vtv: "vt (V thread cs # s)" by auto
       assume eq_e: "e = V thread cs"
         and is_runing: "thread \<in> runing s"
         and hold: "holding s thread cs"
       from hold obtain rest 
         where eq_wq: "wq s cs = thread # rest"
-        by (case_tac "wq s cs", auto simp:s_holding_def)
+        by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
       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)
@@ -1693,7 +1694,7 @@
                     with wq_distinct[OF step_back_vt[OF vtv], of cs]
                     and eq_wq show False by auto
                   qed
-                  thus ?thesis by (simp add:s_waiting_def)
+                  thus ?thesis by (simp add:wq_def s_waiting_def)
                 qed
               } moreover {
                 assume neq_cs: "cs1 \<noteq> cs"
@@ -1708,7 +1709,7 @@
                       thus ?thesis by (simp add:readys_def)
                     qed
                     ultimately show ?thesis 
-                      by (auto simp:s_waiting_def eq_e)
+                      by (auto simp:wq_def s_waiting_def eq_e)
                   qed
               } ultimately show "\<not> waiting (e # s) thread cs1" by blast
             qed
@@ -1778,7 +1779,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)
+                  by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
                 moreover 
                 from eq_wq and th_in and neq_hd
                 have "\<not> (th \<in> readys (e # s))"
@@ -1844,7 +1845,7 @@
                   from True eq_wq neq_th th_in
                   show ?thesis
                     apply (unfold readys_def s_waiting_def, auto)
-                    by (rule_tac x = cs in exI, auto)
+                    by (rule_tac x = cs in exI, auto simp add: wq_def)
                 qed
                 moreover have "th \<in> threads s"
                 proof -
@@ -1931,14 +1932,14 @@
 
 lemma not_thread_cncs:
   fixes th s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and 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)
-    assume vt: "vt step s"
+    assume vt: "vt s"
       and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
       and stp: "step s e"
       and not_in: "th \<notin> threads (e # s)"
@@ -1977,7 +1978,7 @@
       case (thread_P thread cs)
       assume eq_e: "e = P thread cs"
       and is_runing: "thread \<in> runing s"
-      from prems have vtp: "vt step (P thread cs#s)" by auto
+      from prems have vtp: "vt (P thread cs#s)" by auto
       have neq_th: "th \<noteq> thread" 
       proof -
         from not_in eq_e have "th \<notin> threads s" by simp
@@ -2005,10 +2006,10 @@
           by (simp add:runing_def readys_def)
         ultimately show ?thesis by auto
       qed
-      from prems have vtv: "vt step (V thread cs#s)" by auto
+      from prems have vtv: "vt (V thread cs#s)" by auto
       from hold obtain rest 
         where eq_wq: "wq s cs = thread # rest"
-        by (case_tac "wq s cs", auto simp:s_holding_def)
+        by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
       from not_in eq_e eq_wq
       have "\<not> next_th s thread cs th"
         apply (auto simp:next_th_def)
@@ -2055,11 +2056,11 @@
 qed
 
 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
-  by (auto simp:s_waiting_def cs_waiting_def)
+  by (auto simp:s_waiting_def cs_waiting_def wq_def)
 
 lemma dm_depend_threads:
   fixes th s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and in_dom: "(Th th) \<in> Domain (depend s)"
   shows "th \<in> threads s"
 proof -
@@ -2087,7 +2088,7 @@
 
 lemma runing_unique:
   fixes th1 th2 s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and runing_1: "th1 \<in> runing s"
   and runing_2: "th2 \<in> runing s"
   shows "th1 = th2"
@@ -2331,7 +2332,7 @@
 
 lemma cnp_cnv_eq:
   fixes th s
-  assumes "vt step s"
+  assumes "vt s"
   and "th \<notin> threads s"
   shows "cntP s th = cntV s th"
 proof -
@@ -2352,7 +2353,7 @@
       case (thread_exit thread)
       assume eq_e: "e = Exit thread"
         and not_holding: "holdents s thread = {}"
-      have vt_s: "vt step s" by fact
+      have vt_s: "vt s" by fact
       from finite_holding[OF vt_s] have "finite (holdents s thread)" .
       with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
       moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
@@ -2408,7 +2409,7 @@
 by (unfold cs_depend_def s_depend_def, auto)
 
 lemma count_eq_dependents:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and eq_pv: "cntP s th = cntV s th"
   shows "dependents (wq s) th = {}"
 proof -
@@ -2442,7 +2443,7 @@
 
 lemma dependents_threads:
   fixes s th
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "dependents (wq s) th \<subseteq> threads s"
 proof
   { fix th th'
@@ -2465,13 +2466,13 @@
 qed
 
 lemma finite_threads:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "finite (threads s)"
 proof -
   from vt show ?thesis
   proof(induct)
     case (vt_cons s e)
-    assume vt: "vt step s"
+    assume vt: "vt s"
     and step: "step s e"
     and ih: "finite (threads s)"
     from step
@@ -2518,7 +2519,7 @@
 qed
 
 lemma cp_le:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and 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_dependents_def)
@@ -2541,7 +2542,7 @@
 qed
 
 lemma le_cp:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "preced th s \<le> cp s th"
 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
   show "Prc (original_priority th s) (birthtime th s)
@@ -2582,7 +2583,7 @@
 qed
 
 lemma max_cp_eq: 
-  assumes vt: "vt step s"
+  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 = {}")
@@ -2630,7 +2631,7 @@
 qed
 
 lemma max_cp_readys_threads_pre:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and np: "threads s \<noteq> {}"
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 proof(unfold max_cp_eq[OF vt])
@@ -2773,7 +2774,7 @@
 qed
 
 lemma max_cp_readys_threads:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 proof(cases "threads s = {}")
   case True
@@ -2794,7 +2795,7 @@
 qed
 
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
-  apply (unfold s_holding_def cs_holding_def, simp)
+  apply (unfold s_holding_def cs_holding_def wq_def, simp)
   done
 
 lemma f_image_eq: