--- a/Journal/Paper.thy	Fri Sep 22 09:40:54 2017 +0100
+++ b/Journal/Paper.thy	Mon Dec 18 14:52:48 2017 +0000
@@ -491,13 +491,13 @@
   \end{tabular}
   \end{isabelle}
 
-  \noindent
-  In this definition we assume that @{text "set"} converts a list into a set.
-  Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
-  from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL. 
-  At the beginning, that is in the state where no thread is created yet, 
-  the waiting queue function will be the function that returns the
-  empty list for every resource.
+  \noindent In this definition we assume that @{text "set"} converts a
+  list into a set.  Note that in the first definition the condition
+  about @{text "th \<in> set (wq cs)"} does not follow from @{text "th
+  = hd (set (wq cs))"}, since the head of an empty list is undefined
+  in Isabelle/HOL.  At the beginning, that is in the state where no
+  thread is created yet, the waiting queue function will be the
+  function that returns the empty list for every resource.
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{abbrev all_unlocked}\hfill\numbered{allunlocked}
@@ -563,27 +563,30 @@
   \end{figure}
 
   \noindent
-  If there is no cycle, then every @{text RAG} can be pictured as a forrest of trees, as
+  If there is no cycle, then every @{text RAG} can be pictured as a forest of trees, as
   for example in Figure~\ref{RAGgraph}.
 
-  Because of the @{text RAG}s, we will need to formalise some results about
-  graphs.  While there are few formalisations for graphs already
+  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 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
-  model. It seemed for our purposes the most convenient
-  represeantation of graphs are binary relations given by sets of
-  pairs shown in \eqref{pairs}. The pairs stand for the edges in
-  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 in our representation as the relation @{text
-  rel} that is \emph{single valued} and \emph{acyclic}:
+  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
+  forests 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 model. It
+  seemed for our purposes the most convenient represeantation of
+  graphs are binary relations given by sets of pairs shown in
+  \eqref{pairs}. The pairs stand for the edges in graphs. This
+  relation-based representation has the advantage that the notions
+  @{text "waiting"} and @{text "holiding"} are already defined in
+  terms of relations amongst theads and resources. Also, we can easily
+  re-use the standard notions for transitive closure operations @{term
+  "trancl DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
+  composition for our graphs.  A \emph{forest} is defined in our
+  representation as the relation @{text rel} that is \emph{single
+  valued} and \emph{acyclic}:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -605,10 +608,13 @@
   \mbox{}\hfill\numbered{children}
   \end{isabelle}
   
-  \noindent Note that forrests can have trees with infinte depth and
+  \noindent Note that forests can have trees with infinte depth and
   containing nodes with infinitely many children.  A \emph{finite
-  forrest} is a forrest which is well-founded and every node has 
-  finitely many children (is only finitely branching).
+  forest} is a forest whose underlying relation is
+  well-founded\footnote{For \emph{well-founded} we use the quite natural
+  definition from Isabelle.}
+  and every node has finitely many children (is only finitely
+  branching).
 
   %\endnote{
   %\begin{isabelle}\ \ \ \ \ %%%
@@ -1185,7 +1191,7 @@
   \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"},
   then there is nothing to show. So let us assume otherwise. Since the
   @{text "RAG"} is well-founded, we know there exists an ancestor of
-  @{text "th"} that is the root of the corrsponding subtree and
+  @{text "th"} that is the root of the corresponding subtree and
   therefore is ready (it does not request any resources). Let us call
   this thread @{text "th'"}.  Since in PIP the @{term "cpreced"}-value
   of any thread equals the maximum precedence of all threads in its
@@ -1612,7 +1618,7 @@
   for machine instructions. Therefore we cannot characterise what are
   ``good'' programs that contain for every locking request for a
   resource also a corresponding unlocking request.  Second, we need to
-  distinghish between a thread that ``just'' locks a resource for a
+  distinguish between a thread that ``just'' locks a resource for a
   finite amount of time (even if it is very long) and one that locks
   it forever (there might be an unbounded loop in between the locking and
   unlocking requests).
@@ -1638,14 +1644,15 @@
   (active or hibernating) and second, each of them giving up its
   resources after a finite amount of time.  However, we do not have
   this concept of active or hibernating threads in our model.  In fact
-  we can dispence with the first assumption altogether and allow that
+  we can dispense with the first assumption altogether and allow that
   in our model we can create new threads or exit existing threads
   arbitrarily. Consequently, the avoidance of indefinite priority
   inversion we are trying to establish is in our model not true,
   unless we stipulate an upper bound on the number of threads that
   have been created during the time leading to any future state
   after @{term s}. Otherwise our PIP scheduler could be ``swamped''
-  with @{text "Create"}-requests.  So our first assumption states:
+  with @{text "Create"}-requests from of lower priority threads.  
+So our first assumption states:
 
   \begin{quote} {\bf Assumption on the number of threads created 
   after the state {\boldmath@{text s}}:} Given the
@@ -1699,7 +1706,7 @@
   s}. The bound reflects how each thread @{text "th'"} is programmed:
   Though we cannot express what instructions a thread is executing,
   the events in our model correspond to the system calls made by
-  a thread. Our @{text "BND(th')"} binds the number of these ``calls''.
+  a thread. Our @{text "BND(th')"} bounds the number of these ``calls''.
   
   The main reason for these two assumptions is that we can prove the
   following: The number of states after @{text s} in which the thread

Binary file journal.pdf has changed