--- a/prio/ExtGG.thy	Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/ExtGG.thy	Sun Feb 12 04:45:20 2012 +0000
@@ -29,7 +29,7 @@
 
 locale highest_gen =
   fixes s th prio tm
-  assumes vt_s: "vt step s"
+  assumes vt_s: "vt s"
   and threads_s: "th \<in> threads s"
   and highest: "preced th s = Max ((cp s)`threads s)"
   and preced_th: "preced th s = Prc prio tm"
@@ -88,14 +88,14 @@
 
 locale extend_highest_gen = highest_gen + 
   fixes t 
-  assumes vt_t: "vt step (t@s)"
+  assumes vt_t: "vt (t@s)"
   and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
   and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
   and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 
 lemma step_back_vt_app: 
-  assumes vt_ts: "vt cs (t@s)" 
-  shows "vt cs s"
+  assumes vt_ts: "vt (t@s)" 
+  shows "vt s"
 proof -
   from vt_ts show ?thesis
   proof(induct t)
@@ -103,13 +103,13 @@
     from Nil show ?case by auto
   next
     case (Cons e t)
-    assume ih: " vt cs (t @ s) \<Longrightarrow> vt cs s"
-      and vt_et: "vt cs ((e # t) @ s)"
+    assume ih: " vt (t @ s) \<Longrightarrow> vt s"
+      and vt_et: "vt ((e # t) @ s)"
     show ?case
     proof(rule ih)
-      show "vt cs (t @ s)"
+      show "vt (t @ s)"
       proof(rule step_back_vt)
-        from vt_et show "vt cs (e # t @ s)" by simp
+        from vt_et show "vt (e # t @ s)" by simp
       qed
     qed
   qed
@@ -127,7 +127,7 @@
 lemma ind [consumes 0, case_names Nil Cons, induct type]:
   assumes 
     h0: "R []"
-  and h2: "\<And> e t. \<lbrakk>vt step (t@s); step (t@s) e; 
+  and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 
                     extend_highest_gen s th prio tm t; 
                     extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"
   shows "R t"
@@ -137,11 +137,11 @@
     from h0 show "R []" .
   next
     case (Cons e t')
-    assume ih: "\<lbrakk>vt step (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
-      and vt_e: "vt step ((e # t') @ s)"
+    assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
+      and vt_e: "vt ((e # t') @ s)"
       and et: "extend_highest_gen s th prio tm (e # t')"
     from vt_e and step_back_step have stp: "step (t'@s) e" by auto
-    from vt_e and step_back_vt have vt_ts: "vt step (t'@s)" by auto
+    from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto
     show ?case
     proof(rule h2 [OF vt_ts stp _ _ _ ])
       show "R t'"
@@ -149,7 +149,7 @@
         from et show ext': "extend_highest_gen s th prio tm t'"
           by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)
       next
-        from vt_ts show "vt step (t' @ s)" .
+        from vt_ts show "vt (t' @ s)" .
       qed
     next
       from et show "extend_highest_gen s th prio tm (e # t')" .
@@ -264,7 +264,7 @@
         by (unfold eq_e, simp)
       moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
       proof(rule Max_insert)
-        from Cons have "vt step (t @ s)" by auto
+        from Cons have "vt (t @ s)" by auto
         from finite_threads[OF this]
         show "finite (?f ` (threads (t@s)))" by simp
       next
@@ -310,7 +310,7 @@
 next
     case (Exit thread)
     assume eq_e: "e = Exit thread"
-    from Cons have vt_e: "vt step (e#(t @ s))" by auto
+    from Cons have vt_e: "vt (e#(t @ s))" by auto
     from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
     from stp have thread_ts: "thread \<in> threads (t @ s)"
       by(cases, unfold runing_def readys_def, auto)
@@ -353,7 +353,7 @@
               (is "?t = Max (?g ` ?B)") by simp
             moreover have "?g thread \<le> \<dots>"
             proof(rule Max_ge)
-              have "vt step (t@s)" by fact
+              have "vt (t@s)" by fact
               from finite_threads [OF this]
               show "finite (?g ` ?B)" by simp
             next
@@ -428,7 +428,7 @@
             next
               show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
               proof -
-                from Cons have "vt step (t @ s)" by auto
+                from Cons have "vt (t @ s)" by auto
                 from finite_threads[OF this] show ?thesis by auto
               qed
             qed
@@ -601,7 +601,7 @@
     show ?case
     proof(cases e)
       case (V thread cs)
-      from Cons and V have vt_v: "vt step (V thread cs#(t@s))" by auto
+      from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto
 
       show ?thesis
       proof -
@@ -729,7 +729,7 @@
         by blast
       from red_moment[of "Suc(i+k)"]
       and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp
-      hence vt_e: "vt step (e#(moment (i + k) t)@s)"
+      hence vt_e: "vt (e#(moment (i + k) t)@s)"
         by (unfold extend_highest_gen_def extend_highest_gen_axioms_def 
                           highest_gen_def, auto)
       have not_runing': "th' \<notin>  runing (moment (i + k) t @ s)"
@@ -847,7 +847,7 @@
    eq_me: "moment (Suc i) t = e # moment i t" by blast
   from red_moment[of "Suc i"] and eq_me
   have "extend_highest_gen s th prio tm (e # moment i t)" by simp
-  hence vt_e: "vt step (e#(moment i t)@s)"
+  hence vt_e: "vt (e#(moment i t)@s)"
     by (unfold extend_highest_gen_def extend_highest_gen_axioms_def 
       highest_gen_def, auto)
   from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" .
@@ -858,7 +858,7 @@
   have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
   proof(rule cnp_cnv_eq)
     from step_back_vt [OF vt_e] 
-    show "vt step (moment i t @ s)" .
+    show "vt (moment i t @ s)" .
   next
     from eq_e and stp_i 
     have "step (moment i t @ s) (Create th' prio)" by simp