--- a/Journal/Paper.thy	Fri Dec 09 15:18:19 2016 +0000
+++ b/Journal/Paper.thy	Mon Dec 19 23:43:54 2016 +0000
@@ -47,7 +47,7 @@
   preceds ("precs") and
   cpreced ("cprec") and
   wq_fun ("wq") and
-  cprec_fun ("cp") and
+  cprec_fun ("cp'_fun") and
   holdents ("resources") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
   cntP ("c\<^bsub>P\<^esub>") and
@@ -611,14 +611,14 @@
   there is a circle of dependencies in a RAG, then clearly we have a
   deadlock. Therefore when a thread requests a resource, we must
   ensure that the resulting RAG is not circular. In practice, the
-  programmer has to ensure this. Our model will assume that critical 
+  programmer has to ensure this. Our model will enforce that critical 
   resources can only be requested provided no circularity can arise.
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def}\hfill\numbered{cpreced}
+  @{thm cpreced_def3}\hfill\numbered{cpreced}
   \end{isabelle}
 
   \endnote{
@@ -626,18 +626,19 @@
   @{thm cp_alt_def cp_alt_def1}
   \end{isabelle}}
 
-  \noindent
-  where the dependants of @{text th} are given by the waiting queue function.
-  While the precedence @{term prec} of any thread is determined statically 
-  (for example when the thread is
-  created), the point of the current precedence is to let the scheduler increase this
-  precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
-  given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
-  threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
-  defined as the transitive closure of all dependent threads, we deal correctly with the 
-  problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
-  lowered prematurely. We again introduce an abbreviation for current precedeces of
-  a set of threads, written @{term "cprecs wq s ths"}.
+  \noindent where the dependants of @{text th} are given by the
+  waiting queue function.  While the precedence @{term prec} of any
+  thread is determined statically (for example when the thread is
+  created), the point of the current precedence is to dynamically
+  increase this precedence, if needed according to PIP. Therefore the
+  current precedence of @{text th} is given as the maximum of the
+  precedence of @{text th} \emph{and} all threads that are dependants
+  of @{text th} in the state @{text s}. Since the notion @{term
+  "dependants"} is defined as the transitive closure of all dependent
+  threads, we deal correctly with the problem in the informal
+  algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
+  lowered prematurely (see Introduction). We again introduce an abbreviation for current
+  precedeces of a set of threads, written @{term "cprecs wq s ths"}.
   
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cpreceds_def}
@@ -649,7 +650,7 @@
   functions:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "\<lparr>wq, cp\<rparr>"}
+  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
   \end{isabelle}
 
   \noindent
@@ -696,7 +697,7 @@
   \end{isabelle}
 
   \noindent 
-  More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
+  More interesting are the cases where a resource, say @{text cs}, is requested or released. In these cases
   we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
   the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} 
   appended to the end of that list (remember the head of this list is assigned to be in the possession of this
@@ -738,10 +739,11 @@
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
-  choice for the next waiting list. It just has to be a list of distinctive threads and
-  contains the same elements as @{text "qs"}. This gives for @{term V} the clause:
+  \noindent where @{text "SOME"} stands for Hilbert's epsilon and
+  implements an arbitrary choice for the next waiting list. It just
+  has to be a list of distinctive threads and contains the same
+  elements as @{text "qs"} (essentially @{text "qs'"} can be any
+  reordering of the list @{text "qs"}). This gives for @{term V} the clause:
  
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}

--- a/PIPDefs.thy	Fri Dec 09 15:18:19 2016 +0000
+++ b/PIPDefs.thy	Mon Dec 19 23:43:54 2016 +0000
@@ -232,6 +232,13 @@
   apply(rule_tac f="Max" in arg_cong)
   by (auto)
 
+lemma cpreced_def3:
+  "cpreced wq s th \<equiv> Max (preceds ({th} \<union> dependants_raw wq th) s)"
+  unfolding cpreced_def2 image_def
+  apply(rule eq_reflection)
+  apply(rule_tac f="Max" in arg_cong)
+  by (auto)
+  
 definition 
   cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set"
   where 

Binary file journal.pdf has changed