--- a/Journal/Paper.thy	Tue Jun 27 14:49:42 2017 +0100
+++ b/Journal/Paper.thy	Thu Jun 29 14:59:55 2017 +0100
@@ -498,7 +498,7 @@
   \noindent
   Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs} 
   (RAG), which represent the dependencies between threads and resources.
-  We choose to represent RAGs as relations using pairs of the form
+  We choose to represent @{text "RAG"}s as relations using pairs of the form
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
@@ -508,7 +508,7 @@
   \noindent
   where the first stands for a \emph{waiting edge} and the second for a 
   \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 
-  datatype for vertices). Given a waiting queue function, a RAG is defined 
+  datatype for vertices). Given a waiting queue function, a @{text RAG} is defined 
   as the union of the sets of waiting and holding edges, namely
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -555,15 +555,16 @@
   \end{figure}
 
   \noindent
-  If there is no cycle, then every RAG can be pictured as a forrest of trees, as
+  If there is no cycle, then every @{text RAG} can be pictured as a forrest of trees, as
   for example in Figure~\ref{RAGgraph}.
 
-  Because of the RAGs, we will need to formalise some results about
+  Because of the @{text RAG}s, we will need to formalise some results about
   graphs.  While there are few formalisations for graphs already
   implemented in Isabelle, we choose to introduce our own library of
-  graphs for PIP. The justification for this is that we wanted to be able to
-  reason about potentially infinite graphs (in the sense of infinitely
-  branching and infinite size): the property that our RAGs are
+  graphs for PIP. The justification for this is that we wanted 
+  to have a more general theory of graphs which is capable of
+  representing potentially infinite graphs (in the sense of infinitely
+  branching and infinite size): the property that our @{text RAG}s are
   actually forrests of finitely branching trees having only an finite
   depth should be something we can \emph{prove} for our model of
   PIP---it should not be an assumption we build already into our
@@ -573,7 +574,7 @@
   graphs. This relation-based representation is convenient since we
   can use the notions of transitive closure operations @{term "trancl
   DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
-  composition.  A \emph{forrest} is defined as the relation @{text
+  composition.  A \emph{forrest} is defined in our representation as the relation @{text
   rel} that is \emph{single valued} and \emph{acyclic}:
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -614,7 +615,7 @@
   %\endnote{{\bf Lemma about overlapping paths}}
   
   The locking mechanism of PIP ensures that for each thread node,
-  there can be many incoming holding edges in the RAG, but at most one
+  there can be many incoming holding edges in the @{text RAG}, but at most one
   out going waiting edge.  The reason is that when a thread asks for
   resource that is locked already, then the thread is blocked and
   cannot ask for another resource.  Clearly, also every resource can
@@ -623,8 +624,8 @@
   finite, we can always start at a thread waiting for a resource and
   ``chase'' outgoing arrows leading to a single root of a tree.
   
-  The use of relations for representing @{text RAG}s allows us to conveniently define
-  the \emph{thread dependants graph} 
+  The use of relations for representing @{text RAG}s allows us to
+  conveniently define the \emph{Thread Dependants Graph} (TDG):
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm tG_raw_def}\\
@@ -632,9 +633,9 @@
   \end{isabelle}
 
   \noindent This definition represents all threads in a @{text RAG} that wait
-  for a thread to release a resource, but the resource is ``hidden''. 
-  In the
-  picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with
+  for a thread to release a resource, but the corresponding 
+  resource is ``hidden''. 
+  In Figure~\ref{RAGgraph} this means the @{text TDG} connects @{text "th\<^sub>0"} with
   @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
   resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
   cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
@@ -660,8 +661,7 @@
   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 of current precedence is defined as the 
+  precedence of @{text th} \emph{and} all threads in its subtree. Since the notion of current precedence is defined as the 
   transitive closure of the dependent
   threads in the @{text TDG}, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
@@ -798,25 +798,22 @@
   \end{isabelle}
 
   \noindent
-  With these abbreviations in place we can derive for every valid trace @{text s} 
-  the following two facts about  ???????
-  %@ {term dependants} 
-  and @{term cprec} (see \eqref{dependants} 
-  and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def}, 
-  then 
+  With these abbreviations in place we can derive the following two facts 
+  about @{text TDG}s and @{term cprec}, which are more convenient to use in 
+  subsequent proofs. 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
-  @{thm tG_alt_def}\\
-  @{thm cp_s_def}\\
-  \end{tabular}\hfill\numbered{overloaded}
+  @{thm (lhs) tG_alt_def}  & @{text "\<equiv>"} & @{thm (rhs) tG_alt_def}\\
+  @{thm (lhs) cp_s_def}  & @{text "\<equiv>"} & @{thm (rhs) cp_s_def}\\
+  \end{tabular}\\
+  \mbox{}\hfill\numbered{overloaded}
   \end{isabelle}
 
-
-  can introduce 
+  \noindent Next we can introduce 
   the notion of a thread being @{term ready} in a state (i.e.~threads
   that do not wait for any resource, which are the roots of the trees 
-  in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread
+  in the @{text RAG}, see Figure~\ref{RAGgraph}). The @{term running} thread
   is then the thread with the highest current precedence of all ready threads.
 
   \begin{isabelle}\ \ \ \ \ %%%

--- a/PIPDefs.thy	Tue Jun 27 14:49:42 2017 +0100
+++ b/PIPDefs.thy	Thu Jun 29 14:59:55 2017 +0100
@@ -679,8 +679,8 @@
   "tG (s::state) \<equiv> tG_raw (wq s)"
 
 lemma tG_alt_def: 
-  "tG s = {(th1, th2) | th1 th2. 
-                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R")
+  "tG s = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. 
+                  \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th\<^sub>2) \<in> RAG s}" (is "?L = ?R")
   by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp)
 
 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" 

Binary file journal.pdf has changed