--- a/prio/Paper/Paper.thy	Wed Feb 08 16:35:49 2012 +0000
+++ b/prio/Paper/Paper.thy	Thu Feb 09 13:05:51 2012 +0000
@@ -14,6 +14,11 @@
   birthtime ("last'_set") and
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
   Prc ("'(_, _')") and
+  holding ("holds") and
+  waiting ("waits") and
+  Th ("_") and
+  Cs ("_") and
+  readys ("ready") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -156,7 +161,7 @@
   later to the case of PIP on multi-processor systems.} Our model of
   PIP is based on Paulson's inductive approach to protocol
   verification \cite{Paulson98}, where the \emph{state} of a system is
-  given by a list of events that happened so far.  \emph{Events} fall
+  given by a list of events that happened so far.  \emph{Events} in PIP fall
   into five categories defined as the datatype
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -192,7 +197,7 @@
   \end{isabelle}
 
   \noindent
-  Another calculates the priority for a thread @{text "th"}, defined as
+  Another function calculates the priority for a thread @{text "th"}, defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -224,18 +229,18 @@
   \end{tabular}}
   \end{isabelle}
 
-  \footnote{Can Precedence be the real birth-time / or must be time precedence last set?}
-
   \noindent
-  A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of
-  natural numbers defined as
+  In this definition @{term "length s"} stands for the length of the list
+  of events @{text s}. Again the default value in this function is @{text 0}
+  for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
+  state @{text s} is a pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm (rhs) preced_def[where thread="th"]}
   \end{isabelle}
 
   \noindent
-  The point of precedences is to schedule threads not according to priorities (what should
+  The point of precedences is to schedule threads not according to priorities (because what should
   we do in case two threads have the same priority), but according to precedences. 
   Precedences allow us to always discriminate two threads with equal priority by 
   tacking into account the time when the priority was last set. We order precedences so 
@@ -251,18 +256,40 @@
   functions, below abbreviated as @{text wq}, taking a resource as
   argument and returning a list of threads.  This allows us to define
   when a thread \emph{holds}, respectively \emph{waits}, for a
-  resource @{text cs}.
+  resource @{text cs} given a waiting queue function.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm s_holding_def[where thread="th"]}\\
+  @{thm s_waiting_def[where thread="th"]}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  In this definition we assume @{text "set"} converts a list into a set.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm cs_holding_def[where thread="th"]}\\
-  @{thm cs_waiting_def[where thread="th"]}
+  @{thm s_depend_def}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm readys_def}\\
+  \end{tabular}
+  \end{isabelle}
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm runing_def}\\
   \end{tabular}
   \end{isabelle}
 
 
+  resources
 
-  resources
+  done: threads     not done: running
 
   step relation:
 
@@ -271,6 +298,7 @@
   @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
   @{thm[mode=Rule] thread_exit[where thread=th]}\medskip\\
 
+  @{thm[mode=Rule] thread_set[where thread=th]}\medskip\\
   @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
   @{thm[mode=Rule] thread_V[where thread=th]}\\
   \end{tabular}

--- a/prio/PrioG.thy	Wed Feb 08 16:35:49 2012 +0000
+++ b/prio/PrioG.thy	Thu Feb 09 13:05:51 2012 +0000
@@ -791,11 +791,12 @@
                                              else depend s \<union> {(Th th, Cs cs)})"
   apply(unfold s_depend_def wq_def)
   apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def)
-  apply(case_tac "c = cs", auto)
+  apply(case_tac "csa = cs", auto)
   apply(fold wq_def)
   apply(drule_tac step_back_step)
-  by (ind_cases " step s (P (hd (wq s cs)) cs)", 
-    auto simp:s_depend_def wq_def cs_holding_def)
+  apply(ind_cases " step s (P (hd (wq s cs)) cs)")
+  apply(auto simp:s_depend_def wq_def cs_holding_def)
+  done
 
 lemma simple_A:
   fixes A

--- a/prio/PrioGDef.thy	Wed Feb 08 16:35:49 2012 +0000
+++ b/prio/PrioGDef.thy	Thu Feb 09 13:05:51 2012 +0000
@@ -159,7 +159,7 @@
   *}
   cs_depend_def: 
   "depend (wq::cs \<Rightarrow> thread list) \<equiv>
-      {(Th t, Cs c) | t c. waiting wq t c} \<union> {(Cs c, Th t) | c t. holding wq t c}"
+      {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
   -- {* 
   \begin{minipage}{0.9\textwidth}
   The following @{text "dependents wq th"} represents the set of threads which are depending on
@@ -264,7 +264,7 @@
   "waiting (s::state) thread cs \<equiv> (thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs))"
   s_depend_def: 
   "depend (s::state) \<equiv> 
-    {(Th t, Cs c) | t c. waiting (wq s) t c} \<union> {(Cs c, Th t) | c t. holding (wq s) t c}"
+    {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
   s_dependents_def: 
   "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
 
@@ -273,7 +273,7 @@
   for running if it is a live thread and it is not waiting for any critical resource.
   *}
 definition readys :: "state \<Rightarrow> thread set"
-  where "readys s = {thread . thread \<in> threads s \<and> (\<forall> cs. \<not> waiting s thread cs)}"
+  where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
 
 text {* \noindent
   The following function @{text "runing"} calculates the set of running thread, which is the ready 

Binary file prio/paper.pdf has changed