--- 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}