--- a/prio/CpsG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/CpsG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -21,7 +21,7 @@
       assume eq_e: "e = Create thread prio"
         and not_in': "thread \<notin> threads s"
       have "holdents (e # s) th = holdents s th"
-        apply (unfold eq_e holdents_def)
+        apply (unfold eq_e holdents_test)
         by (simp add:depend_create_unchanged)
       moreover have "th \<notin> threads s" 
       proof -
@@ -37,13 +37,13 @@
         case True
         with nh eq_e
         show ?thesis 
-          by (auto simp:holdents_def depend_exit_unchanged)
+          by (auto simp:holdents_test depend_exit_unchanged)
       next
         case False
         with not_in and eq_e
         have "th \<notin> threads s" by simp
         from ih[OF this] False eq_e show ?thesis 
-          by (auto simp:holdents_def depend_exit_unchanged)
+          by (auto simp:holdents_test depend_exit_unchanged)
       qed
     next
       case (thread_P thread cs)
@@ -58,7 +58,7 @@
         ultimately show ?thesis by auto
       qed
       hence "holdents (e # s) th  = holdents s th "
-        apply (unfold cntCS_def holdents_def eq_e)
+        apply (unfold cntCS_def holdents_test eq_e)
         by (unfold step_depend_p[OF vtp], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
@@ -101,7 +101,7 @@
       qed
       moreover note neq_th eq_wq
       ultimately have "holdents (e # s) th  = holdents s th"
-        by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+        by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
       moreover have "holdents s th = {}"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -115,13 +115,13 @@
       from not_in and eq_e have "th \<notin> threads s" by auto
       from ih [OF this] and eq_e
       show ?thesis 
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_set_unchanged)
     qed
     next
       case vt_nil
       show ?case
-      by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+      by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -1919,7 +1919,7 @@
         from tranclE[OF this] obtain cs' where 
           "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
         with hdn
-        have False by (auto simp:holdents_def)
+        have False by (auto simp:holdents_test)
       } thus ?thesis by auto
     qed
     thus ?thesis 

--- a/prio/ExtGG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/ExtGG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -952,6 +952,20 @@
   show ?thesis by auto
 qed
 
+lemma runing_inversion_4:
+  assumes runing': "th' \<in> runing (t@s)"
+  and neq_th: "th' \<noteq> th"
+  shows "th' \<in> threads s"
+  and    "\<not>detached s th'"
+  and    "cp (t@s) th' = preced th s"
+using runing_inversion_3 [OF runing'] 
+  and neq_th 
+  and runing_preced_inversion[OF runing']
+apply(auto simp add: detached_eq[OF vt_s])
+done
+
+
+
 lemma live: "runing (t@s) \<noteq> {}"
 proof(cases "th \<in> runing (t@s)")
   case True thus ?thesis by auto

--- a/prio/Paper/Paper.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -375,13 +375,6 @@
   programmer has to ensure this.
 
 
-  {\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 
   state @{text s}. It is defined as
 
@@ -543,12 +536,22 @@
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use sets to capture both possibilities.
   We can now also conveniently define the set of resources that are locked by a thread in a
-  given state.
+  given state
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm holdents_def}
   \end{isabelle}
 
+  \noindent
+  and also when a thread is detached
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm detached_def}
+  \end{isabelle}
+
+  \noindent
+  which means that @{text th} neither holds nor waits for a resource in @{text s}.
+  
   Finally we can define what a \emph{valid state} is in our model of PIP. For
   example we cannot expect to be able to exit a thread, if it was not
   created yet. 
@@ -1211,6 +1214,18 @@
   be recalculated for an event. This information is provided by the lemmas we proved.
   We confirmened that our observations translate into practice by implementing
   a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. 
+  Our events translate in PINTOS to the following function interface:
+
+  \begin{center}
+  \begin{tabular}{|l|l|}
+  \hline
+  {\bf Event} & {\bf PINTOS function} \\
+  \hline
+  @{text Create} & \\
+  @{text Exit}   & \\
+  \end{tabular}
+  \end{center}
+
 *}
 
 section {* Conclusion *}

--- a/prio/PrioG.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/PrioG.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -1114,7 +1114,7 @@
         apply (ind_cases "step s (Exit th')")
         apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def
                s_depend_def s_holding_def cs_holding_def)
-        by (fold wq_def, auto)
+        done
     next
       case (V th' cs')
       show ?thesis
@@ -1354,7 +1354,7 @@
   shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
 proof -
   from assms show ?thesis
-  unfolding  holdents_def step_depend_p[OF vt] by auto
+  unfolding  holdents_test step_depend_p[OF vt] by (auto)
 qed
 
 lemma step_holdents_p_eq:
@@ -1364,7 +1364,7 @@
   shows "holdents (P th cs#s) th = holdents s th"
 proof -
   from assms show ?thesis
-  unfolding  holdents_def step_depend_p[OF vt] by auto
+  unfolding  holdents_test step_depend_p[OF vt] by auto
 qed
 
 
@@ -1386,7 +1386,7 @@
       ultimately have "x \<in> (\<lambda>(x, y). the_cs x) ` depend s" by simp 
     } thus ?thesis by auto
   qed
-  ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset)
+  ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset)
 qed
 
 lemma cntCS_v_dec: 
@@ -1396,12 +1396,12 @@
 proof -
   from step_back_step[OF vtv]
   have cs_in: "cs \<in> holdents s thread" 
-    apply (cases, unfold holdents_def s_depend_def, simp)
+    apply (cases, unfold holdents_test s_depend_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 (unfold holdents_def, unfold step_depend_v[OF vtv],
+    apply (unfold holdents_test, unfold step_depend_v[OF vtv],
             auto simp:next_th_def)
   proof -
     fix rest
@@ -1492,7 +1492,7 @@
         from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
         from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
         have eq_cncs: "cntCS (e#s) th = cntCS s th"
-          unfolding cntCS_def holdents_def
+          unfolding cntCS_def holdents_test
           by (simp add:depend_create_unchanged eq_e)
         { assume "th \<noteq> thread"
           with eq_readys eq_e
@@ -1517,7 +1517,7 @@
       from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
       from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
       have eq_cncs: "cntCS (e#s) th = cntCS s th"
-        unfolding cntCS_def holdents_def
+        unfolding cntCS_def holdents_test
         by (simp add:depend_exit_unchanged eq_e)
       { assume "th \<noteq> thread"
         with eq_e
@@ -1559,7 +1559,7 @@
             apply (erule_tac x = cs in allE, auto)
             by (case_tac "(wq_fun (schs s) cs)", auto)
           moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
-            apply (simp add:cntCS_def holdents_def)
+            apply (simp add:cntCS_def holdents_test)
             by (unfold  step_depend_p [OF vtp], auto)
           moreover from eq_e neq_th have "cntP (e # s) th = cntP s th"
             by (simp add:cntP_def count_def)
@@ -1594,7 +1594,7 @@
                   proof(rule card_insert)
                     from finite_holding [OF vt, of thread]
                     show " finite {cs. (Cs cs, Th thread) \<in> depend s}"
-                      by (unfold holdents_def, simp)
+                      by (unfold holdents_test, simp)
                   qed
                   moreover have "?R - {cs} = ?R"
                   proof -
@@ -1609,7 +1609,7 @@
                 qed
                 thus ?thesis
                   apply (unfold eq_e eq_th cntCS_def)
-                  apply (simp add: holdents_def)
+                  apply (simp add: holdents_test)
                   by (unfold step_depend_p [OF vtp], auto simp:True)
               qed
               moreover from is_runing have "th \<in> readys s"
@@ -1637,7 +1637,7 @@
               moreover from is_runing have "th \<in> threads (e#s)" 
                 by (unfold eq_e, auto simp:runing_def readys_def eq_th)
               moreover have "cntCS (e # s) th = cntCS s th"
-                apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp])
+                apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp])
                 by (auto simp:False)
               moreover note eq_cnp eq_cnv ih[of th]
               moreover from is_runing have "th \<in> readys s"
@@ -1734,7 +1734,7 @@
               apply (insert step_back_vt[OF vtv])
               by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
             moreover have "cntCS (e#s) th = cntCS s th"
-              apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+              apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
               proof -
                 have "{csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs \<and> next_th s thread cs th} =
                       {cs. (Cs cs, Th th) \<in> depend s}"
@@ -1796,7 +1796,7 @@
                 from eq_wq and  th_in and neq_hd
                 have "(holdents (e # s) th) = (holdents s th)"
                   apply (unfold eq_e step_depend_v[OF vtv], 
-                         auto simp:next_th_def eq_set s_depend_def holdents_def wq_def
+                         auto simp:next_th_def eq_set s_depend_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)
                 thus ?thesis by (simp add:cntCS_def)
@@ -1861,7 +1861,7 @@
                 ultimately show ?thesis using ih by auto
               qed
               moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th"
-                apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto)
+                apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto)
               proof -
                 show "card {csa. (Cs csa, Th th) \<in> depend s \<or> csa = cs} =
                                Suc (card {cs. (Cs cs, Th th) \<in> depend s})"
@@ -1903,7 +1903,7 @@
         from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
         from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def)
         have eq_cncs: "cntCS (e#s) th = cntCS s th"
-          unfolding cntCS_def holdents_def
+          unfolding cntCS_def holdents_test
           by (simp add:depend_set_unchanged eq_e)
         from eq_e have eq_readys: "readys (e#s) = readys s" 
           by (simp add:readys_def cs_waiting_def s_waiting_def wq_def,
@@ -1930,7 +1930,7 @@
     case vt_nil
     show ?case 
       by (unfold cntP_def cntV_def cntCS_def, 
-        auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+        auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -1953,7 +1953,7 @@
       assume eq_e: "e = Create thread prio"
         and not_in': "thread \<notin> threads s"
       have "cntCS (e # s) th = cntCS s th"
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_create_unchanged)
       moreover have "th \<notin> threads s" 
       proof -
@@ -1965,7 +1965,7 @@
       assume eq_e: "e = Exit thread"
       and nh: "holdents s thread = {}"
       have eq_cns: "cntCS (e # s) th = cntCS s th"
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_exit_unchanged)
       show ?thesis
       proof(cases "th = thread")
@@ -1991,7 +1991,7 @@
         ultimately show ?thesis by auto
       qed
       hence "cntCS (e # s) th  = cntCS s th "
-        apply (unfold cntCS_def holdents_def eq_e)
+        apply (unfold cntCS_def holdents_test eq_e)
         by (unfold step_depend_p[OF vtp], auto)
       moreover have "cntCS s th = 0"
       proof(rule ih)
@@ -2034,7 +2034,7 @@
       qed
       moreover note neq_th eq_wq
       ultimately have "cntCS (e # s) th  = cntCS s th"
-        by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+        by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto)
       moreover have "cntCS s th = 0"
       proof(rule ih)
         from not_in eq_e show "th \<notin> threads s" by simp
@@ -2048,14 +2048,14 @@
       from not_in and eq_e have "th \<notin> threads s" by auto
       from ih [OF this] and eq_e
       show ?thesis 
-        apply (unfold eq_e cntCS_def holdents_def)
+        apply (unfold eq_e cntCS_def holdents_test)
         by (simp add:depend_set_unchanged)
     qed
     next
       case vt_nil
       show ?case
       by (unfold cntCS_def, 
-        auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+        auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)
   qed
 qed
 
@@ -2425,10 +2425,10 @@
   moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}"
   proof -
     from finite_holding[OF vt, of th] show ?thesis
-      by (simp add:holdents_def)
+      by (simp add:holdents_test)
   qed
   ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
-    by (unfold cntCS_def holdents_def cs_dependents_def, auto)
+    by (unfold cntCS_def holdents_test cs_dependents_def, auto)
   show ?thesis
   proof(unfold cs_dependents_def)
     { assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
@@ -2773,10 +2773,20 @@
    by (rule image_subsetI, auto intro:h[symmetric])
 qed
 
+
 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
-  where "detached s th \<equiv> (Th th \<notin> Field (depend s))"
+  where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"
+
 
-thm Field_def
+lemma detached_test:
+  shows "detached s th = (Th th \<notin> Field (depend s))"
+apply(simp add: detached_def Field_def)
+apply(simp add: s_depend_def)
+apply(simp add: s_holding_abv s_waiting_abv)
+apply(simp add: Domain_iff Range_iff)
+apply(simp add: wq_def)
+apply(auto)
+done
 
 lemma detached_intro:
   fixes s th
@@ -2796,7 +2806,7 @@
     assume "th \<notin> threads s"
     with range_in[OF vt] dm_depend_threads[OF vt]
     show ?thesis
-      by (auto simp:detached_def Field_def Domain_def Range_def)
+      by (auto simp add: detached_def s_depend_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 (depend s)"
@@ -2805,15 +2815,13 @@
       have "holdents s th = {}"
         by (simp add:cntCS_def)
       thus ?thesis
-        apply(auto simp:holdents_def)
+        apply(auto simp:holdents_test)
         apply(case_tac a)
-        apply(auto simp:holdents_def s_depend_def)
+        apply(auto simp:holdents_test s_depend_def)
         done
     qed
     ultimately show ?thesis
-      apply (auto simp:detached_def Field_def Domain_def readys_def)
-      apply (case_tac b, auto simp:s_depend_def)
-      by (erule_tac x = "nat" in allE, simp add: eq_waiting)
+      by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def)
   qed
 qed
 
@@ -2829,7 +2837,8 @@
   have cncs_z: "cntCS s th = 0"
   proof -
     from dtc have "holdents s th = {}"
-      by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def)
+      unfolding detached_def holdents_test s_depend_def
+      by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)
     thus ?thesis by (auto simp:cntCS_def)
   qed
   show ?thesis

--- a/prio/PrioGDef.thy	Mon Apr 23 08:01:37 2012 +0000
+++ b/prio/PrioGDef.thy	Mon Apr 30 15:32:34 2012 +0000
@@ -361,7 +361,15 @@
   @{text "th"} in state @{text "s"}.
   *}
 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
-  where "holdents s th \<equiv> {cs . (Cs cs, Th th) \<in> depend s}"
+  where "holdents s th \<equiv> {cs . holding s th cs}"
+
+lemma holdents_test: 
+  "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+unfolding holdents_def
+unfolding s_depend_def
+unfolding s_holding_abv
+unfolding wq_def
+by (simp)
 
 text {* \noindent
   @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in

Binary file prio/paper.pdf has changed