--- a/prio/ExtGG.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/ExtGG.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -601,9 +601,11 @@
     have in_thread: "th' \<in> threads (t @ s)"
       and not_holding: "cntP (t @ s) th' = cntV (t @ s) th'" by auto
     from Cons have "extend_highest_gen s th prio tm t" by auto
-    from extend_highest_gen.pv_blocked 
-    [OF this, OF in_thread neq_th' not_holding]
-    have not_runing: "th' \<notin> runing (t @ s)" .
+    then have not_runing: "th' \<notin> runing (t @ s)" 
+      apply(rule extend_highest_gen.pv_blocked) 
+      using Cons(1) in_thread neq_th' not_holding
+      apply(simp_all add: detached_eq)
+      done
     show ?case
     proof(cases e)
       case (V thread cs)
@@ -751,15 +753,16 @@
         next
           from red_moment show "extend_highest_gen s th prio tm (moment (i + k) t)" .
         next
-          from Suc show "cntP (moment (i + k) t @ s) th' = cntV (moment (i + k) t @ s) th'"
-            by (auto)
+          from Suc vt_e show "detached (moment (i + k) t @ s) th'"
+            apply(subst detached_eq)
+            apply(auto intro: vt_e evt_cons)
+            done
         qed
       qed
       from step_back_step[OF vt_e]
       have "step ((moment (i + k) t)@s) e" .
       hence "cntP (e#(moment (i + k) t)@s) th' = cntV (e#(moment (i + k) t)@s) th' \<and>
-        th' \<in> threads (e#(moment (i + k) t)@s)
-        "
+        th' \<in> threads (e#(moment (i + k) t)@s)"
       proof(cases)
         case (thread_create thread prio)
         with Suc show ?thesis by (auto simp:cntP_def cntV_def count_def)
@@ -828,8 +831,11 @@
   from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij
   have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'"
     and h2: "th' \<in> threads ((moment j t)@s)" by auto
-  with extend_highest_gen.pv_blocked [OF  red_moment [of j], OF h2 neq_th' h1]
-  show ?thesis by auto
+  with extend_highest_gen.pv_blocked 
+  show ?thesis 
+    using  red_moment [of j] h2 neq_th' h1
+    apply(auto)
+    by (metis extend_highest_gen.pv_blocked_pre)
 qed
 
 lemma moment_blocked:

--- a/prio/Paper/Paper.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -38,8 +38,9 @@
   original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 
-abbreviation
+(*abbreviation
  "detached s th \<equiv> cntP s th = cntV s th"
+*)
 (*>*)
 
 section {* Introduction *}
@@ -375,6 +376,10 @@
 
 
   {\bf ??? define detached}
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm detached_def}
+  \end{isabelle}
+  
 
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 

--- a/prio/PrioG.thy	Fri Apr 20 11:45:06 2012 +0000
+++ b/prio/PrioG.thy	Fri Apr 20 14:15:36 2012 +0000
@@ -2776,6 +2776,8 @@
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
   where "detached s th \<equiv> (Th th \<notin> Field (depend s))"
 
+thm Field_def
+
 lemma detached_intro:
   fixes s th
   assumes vt: "vt s"
@@ -2803,12 +2805,14 @@
       have "holdents s th = {}"
         by (simp add:cntCS_def)
       thus ?thesis
-        by (auto simp:holdents_def, case_tac x, 
-          auto simp:holdents_def s_depend_def)
+        apply(auto simp:holdents_def)
+        apply(case_tac a)
+        apply(auto simp:holdents_def s_depend_def)
+        done
     qed
     ultimately show ?thesis
       apply (auto simp:detached_def Field_def Domain_def readys_def)
-      apply (case_tac y, auto simp:s_depend_def)
+      apply (case_tac b, auto simp:s_depend_def)
       by (erule_tac x = "nat" in allE, simp add: eq_waiting)
   qed
 qed

Binary file prio/paper.pdf has changed