diff -r 0a4be67ea7f8 -r f2e0d031a395 prio/CpsG.thy
--- a/prio/CpsG.thy	Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/CpsG.thy	Sun Feb 12 04:45:20 2012 +0000
@@ -4,14 +4,14 @@
 
 lemma not_thread_holdents:
   fixes th s
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and not_in: "th \<notin> threads s" 
   shows "holdents s th = {}"
 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> holdents s th = {}"
       and stp: "step s e"
       and not_in: "th \<notin> threads (e # s)"
@@ -49,7 +49,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
@@ -77,10 +77,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)
@@ -128,7 +128,7 @@
 
 
 lemma next_th_neq: 
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and nt: "next_th s th cs th'"
   shows "th' \<noteq> th"
 proof -
@@ -167,7 +167,7 @@
   by auto
 
 lemma wf_depend:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "wf (depend s)"
 proof(rule finite_acyclic_wf)
   from finite_depend[OF vt] show "finite (depend s)" .
@@ -256,7 +256,7 @@
   by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
 
 lemma child_unique:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and ch1: "(Th th, Th th1) \<in> child s"
   and ch2: "(Th th, Th th2) \<in> child s"
   shows "th1 = th2"
@@ -329,7 +329,7 @@
   by (unfold child_def, auto)
 
 lemma wf_child: 
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "wf (child s)"
 proof(rule wf_subset)
   from wf_trancl[OF wf_depend[OF vt]]
@@ -339,7 +339,7 @@
 qed
 
 lemma depend_child_pre:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows
   "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
 proof -
@@ -371,7 +371,7 @@
   qed
 qed
 
-lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
   by (insert depend_child_pre, auto)
 
 lemma child_depend_p:
@@ -392,7 +392,7 @@
 qed
 
 lemma child_depend_eq: 
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows 
   "((Th th1, Th th2) \<in> (child s)^+) = 
    ((Th th1, Th th2) \<in> (depend s)^+)"
@@ -400,7 +400,7 @@
 
 lemma children_no_dep:
   fixes s th th1 th2 th3
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and ch1: "(Th th1, Th th) \<in> child s"
   and ch2: "(Th th2, Th th) \<in> child s"
   and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
@@ -433,7 +433,7 @@
 qed
 
 lemma unique_depend_p:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and dp1: "(n, n1) \<in> (depend s)^+"
   and dp2: "(n, n2) \<in> (depend s)^+"
   and neq: "n1 \<noteq> n2"
@@ -445,7 +445,7 @@
 
 lemma dependents_child_unique:
   fixes s th th1 th2 th3
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and ch1: "(Th th1, Th th) \<in> child s"
   and ch2: "(Th th2, Th th) \<in> child s"
   and dp1: "th3 \<in> dependents s th1"
@@ -472,7 +472,7 @@
 
 lemma cp_rec:
   fixes s th
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
 proof(unfold cp_eq_cpreced_f cpreced_def)
   let ?f = "(\<lambda>th. preced th s)"
@@ -625,7 +625,7 @@
 locale step_set_cps =
   fixes s' th prio s 
   defines s_def : "s \<equiv> (Set th prio#s')"
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
 
 context step_set_cps 
 begin
@@ -936,12 +936,12 @@
 end
 
 lemma next_waiting:
-  assumes vt: "vt step s"
+  assumes vt: "vt s"
   and nxt: "next_th s th cs th'"
   shows "waiting s th' cs"
 proof -
   from assms show ?thesis
-    apply (auto simp:next_th_def s_waiting_def)
+    apply (auto simp:next_th_def s_waiting_def[folded wq_def])
   proof -
     fix rest
     assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
@@ -994,7 +994,7 @@
 locale step_v_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (V th cs#s')"
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
 
 locale step_v_cps_nt = step_v_cps +
   fixes th'
@@ -1054,7 +1054,7 @@
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
             have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
             show ?thesis by simp
           qed
@@ -1072,7 +1072,7 @@
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
             have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
             show ?thesis .
           qed
@@ -1115,7 +1115,7 @@
           proof -
             from step_back_step[OF vt_s[unfolded s_def]]
             have "(Cs cs, Th th) \<in> depend s'"
-              by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+              by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
             show ?thesis by simp
           qed
@@ -1126,7 +1126,7 @@
           have "th \<in> readys s'" by (cases, simp add:runing_def)
           moreover note eq_z
           ultimately show False 
-            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)
         qed
       next
         show "y \<noteq> Th th'"
@@ -1137,14 +1137,14 @@
           proof -
             from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
             have "(Th th', Cs cs) \<in> depend s'"
-              by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+              by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
             from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
             show ?thesis .
           qed
           with ztp have cs_i: "(Cs cs, Th th'') \<in>  (depend s')\<^sup>+" by simp
           from step_back_step[OF vt_s[unfolded s_def]]
           have cs_th: "(Cs cs, Th th) \<in> depend s'"
-            by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+            by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
           have "(Cs cs, Th th'') \<notin>  depend s'"
           proof
             assume "(Cs cs, Th th'') \<in> depend s'"
@@ -1165,7 +1165,7 @@
           moreover from step_back_step[OF vt_s[unfolded s_def]]
           have "th \<in> readys s'" by (cases, simp add:runing_def)
           ultimately show False 
-            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)
         qed
       qed
       with depend_s yz have "(y, z) \<in> depend s" by auto
@@ -1223,7 +1223,7 @@
       assume "holding s' th cs" 
       then obtain rest where
         eq_wq: "wq s' cs = th#rest"
-        apply (unfold s_holding_def)
+        apply (unfold s_holding_def wq_def[symmetric])
         by (case_tac "(wq s' cs)", auto)
       with h1 h2 have ne: "rest \<noteq> []" by auto
       with eq_wq
@@ -1351,7 +1351,7 @@
 locale step_P_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (P th cs#s')"
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
 
 locale step_P_cps_ne =step_P_cps +
   assumes ne: "wq s' cs \<noteq> []"
@@ -1814,7 +1814,7 @@
 locale step_create_cps =
   fixes s' th prio s 
   defines s_def : "s \<equiv> (Create th prio#s')"
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
 
 context step_create_cps
 begin
@@ -1902,7 +1902,7 @@
 locale step_exit_cps =
   fixes s' th prio s 
   defines s_def : "s \<equiv> (Exit th#s')"
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
 
 context step_exit_cps
 begin
@@ -1930,7 +1930,7 @@
       assume "th \<in> runing s'"
       with bk show ?thesis
         apply (unfold runing_def readys_def s_waiting_def s_depend_def)
-        by (auto simp:cs_waiting_def)
+        by (auto simp:cs_waiting_def wq_def)
     qed
   qed
   have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"