diff -r 170e59f2d645 -r 675416b1defd Journal/Paper.thy
--- a/Journal/Paper.thy	Tue May 23 15:10:48 2017 +0100
+++ b/Journal/Paper.thy	Fri Jun 02 14:36:44 2017 +0100
@@ -1588,7 +1588,7 @@
   resource also a corresponding unlocking request.  Second, we need to
   distinghish 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 a loop in between the locking and
+  it forever (there might be an unbounded loop in between the locking and
   unlocking requests).
 
   Because of these problems, we decided in our earlier paper
@@ -1601,24 +1601,25 @@
   Priority Inversion measured by the number of events.  The events can
   be seen as a \textit{rough(!)} abstraction of the ``runtime
   behaviour'' of threads and also as an abstract notion of
-  ``time''---when a new event happened, some time must have passed.
+  ``time''---when a new event happens, some time must have passed.
 
 
   What we will establish in this section is that there can only be a
   finite number of states after state @{term s} in which the thread
-  @{term th} is blocked.  For this finiteness bound to exist, Sha et
-  al.~informally make two assumtions: first, there is a finite pool of
-  threads (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 in our model we can create or exit threads
+  @{term th} is blocked (recall for this that a state is a list of
+  events).  For this finiteness bound to exist, Sha et al.~informally
+  make two assumtions: first, there is a finite pool of threads
+  (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
+  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 put up an upper bound on the number of threads that
-  have been created upto any valid future state after @{term
-  s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
-  "Create"}-requests.  So our first assumption states:
+  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:
 
   \begin{quote} {\bf Assumption on the number of threads created 
   after the state {\boldmath@{text s}}:} Given the
@@ -1638,7 +1639,7 @@
   This ensures that no matter which ``future'' state is reached, the
   number of @{text "Create"}-events is finite. We use @{text "es @ s"}
   to stand for \emph{future states} after @{text s}---it is @{text s}
-  extended with some list of events.
+  extended with some list @{text es} of events.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about
@@ -1651,9 +1652,10 @@
   \noindent This set contains all treads that are not detached in
   state @{text s}. According to our definiton of @{text "detached"},
   this means a thread in @{text "blockers"} either holds or waits for
-  some resource. Our Theorem~1 implies that they can all potentially
-  block @{text th} after state @{text s}. We need to make the
-  following assumption about the threads in this set:
+  some resource in state @{text s} . Our Them~1 implies that any of
+  those threads can all potentially block @{text th} after state
+  @{text s}. We need to make the following assumption about the
+  threads in the @{text "blockers"}-set:
 
   \begin{quote}
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
@@ -1671,19 +1673,20 @@
   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
-  thread. Our @{text "BND(th')"} binds the number of these ``calls''.
+  a thread. Our @{text "BND(th')"} binds 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
   @{text th} is not running (that is where Priority Inversion occurs)
   can be bounded by the number of actions the threads in @{text
-  blockers} perform and how many threads are newly created.  To state
-  our bound formally, we need to make a definition of what we mean by
-  intermediate states; it will be the list of states starting from
-  @{text s} upto the state @{text "es @ s"}. For example, suppose
-  $\textit{es} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
-  \textit{e}_1]$, then the intermediate states from @{text s} upto
-  @{text "es @ s"} are
+  blockers} perform (i.e.~events) and how many threads are newly
+  created.  To state our bound formally, we need to make a definition
+  of what we mean by intermediate states between a state @{text s} and
+  a future state after @{text s}; they will be the list of states
+  starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For
+  example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1},
+  \ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states
+  from @{text s} upto @{text "es @ s"} are
 
   \begin{center}
   \begin{tabular}{l}
@@ -1711,59 +1714,77 @@
 
   \begin{theorem}
   Given our assumptions about bounds, we have that 
-
   \[
   @{text "len"}\,[@{text "s'"} 
   \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \;\;\leq\;\; 
   @{text "BC"} + \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}\;. 
   \]
+  \end{theorem}
 
-  \end{theorem}
+  \noindent This theorem uses Isabelle's list-comprehension notation,
+  which lists all intermediate states between @{text s} and @{text "es
+  @ s"}, and then filters this list according to states in which
+  @{text th} is not running. By calculating the number of elements in
+  the filtered list using the function @{text len}, we have the number
+  of intermediate states in which @{text th} is not running and which
+  by the theorem is bounded by the term on the right-hand side.
 
   \begin{proof} There are two characterisations for the number of
-  events in @{text es}: First, for each corresponding state in @{text
-  "s upto es"}, either @{text th} is running or not running. That
-  means
- 
-  \begin{equation}\label{firsteq}
-  @{text "len es"} = 
-  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}] +
-  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] 
+  events in @{text es}: First, in each state in
+  @{text "s upto es"}, clearly either @{text th} is running or
+  not running. Together with @{text "len es = len (s upto es)"}, that
+  implies %
+
+  \begin{equation}
+  \label{firsteq}
+  \begin{array}{lcl}
+  @{text "len es"} & \;=\; &
+  @{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]\\ 
+  & & +\;
+  @{text len}\, [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+  \end{array} 
   \end{equation}
 
   \noindent Second by Thm~\ref{mainthm}, the events are either the
   actions of @{text th} or @{text "Create"}-events or actions of the
   threads in blockers. That is
-
+  %
   \begin{equation}\label{secondeq}
-  @{text "len es"} = @{text "len (actions_of {th} es)"} +
-                     @{text "len (filter isCreate es)"} + 
-                      @{text "len (actions_of blockers es)"}
+  \begin{array}{lcl}
+  @{text "len es"} & \;=\; & @{text "len (actions_of {th} es)"}\\
+  & & +\; @{text "len (filter isCreate es)"}\\ 
+  & & +\; @{text "len (actions_of blockers es)"}
+  \end{array}
   \end{equation}
 
-  \noindent
-  Further we know that an action of @{text th} can only be taken when @{text th} is running. Therefore
-
+  \noindent Furthermore we know that an action of @{text th} in the
+  intermediate states @{text "s upto es"} can only be taken when
+  @{text th} is running. Therefore
+  %
   \[
-  @{text "len (actions_of {th} es)"} \leq 
-  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
+  @{text "len (actions_of {th} es)"} \;\leq\; 
+  @{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
   \]
   
-  \noindent Substituting this into \eqref{firsteq} gives
-
+  \noindent holds. Substituting this into \eqref{firsteq} gives
+  %
   \[
-  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] 
-  \leq @{text "len es"} - @{text "len (actions_of {th} es)"}
+  @{text len}\,[@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] 
+  \;\leq\; @{text "len es"} - @{text "len (actions_of {th} es)"}
   \]
 
+  \noindent
   into which we can substitute \eqref{secondeq} yielding
-
+  %
   \[
-  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq
-  @{text "len (filter isCreate es)"} + @{text "len (actions_of blockers es)"}
+  \begin{array}{rcl}
+  @{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] & \;\;\leq\;\; &
+  @{text "len (filter isCreate es)"}\\
+  & & \quad + @{text "len (actions_of blockers es)"}
+  \end{array}
   \]
 
-  \noindent By our first assumption we know that the @{text
+  \noindent By our first assumption we know that the number of @{text
   "Create"}-events are bounded by the bound @{text BC}.  By our second
   assumption we can prove that the actions of all blockers is bounded
   by the sum of bounds of the individual blocking threads, that is
@@ -1777,16 +1798,15 @@
   \end{proof}
 
   \noindent This theorem is the main conclusion we obtain for the
-  Priority Inheritance Protocol: it shows that the set of @{text blockers}
-  is fixed at state @{text s} when @{text th} becomes the thread with
-  highest priority. Then no additional blocker of @{text th} can
-  appear after the state @{text s}. And in this way we can bound the
-  number of states where the thread @{text th} with the highest
-  priority is prevented from running.
-*}
-(*<*)
-end
-(*>*)
+  Priority Inheritance Protocol. It is based on the fact that the set of
+  @{text blockers} is fixed at state @{text s} when @{text th} becomes
+  the thread with highest priority. Then no additional blocker of
+  @{text th} can appear after the state @{text s}. And in this way we
+  can bound the number of states where the thread @{text th} with the
+  highest priority is prevented from running.
+  Our bound does not depend on the restriction of well-nested critical 
+  sections in the Priority Inheritance Protocol as imposed by Sha et al.  
+  *} (*<*) end (*>*)
 
 section {* Properties for an Implementation\label{implement} *}
 
@@ -1803,7 +1823,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  HERE?? %%@ {thm children_def2}
+  ?? @{thm children_def}
   \end{tabular}
   \end{isabelle}
 
@@ -1813,7 +1833,7 @@
   a resource). We can prove the following lemma.
 
   \begin{lemma}\label{childrenlem}
-  HERE %@{text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
+  HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
   \begin{center}
   %@ {thm (concl) cp_rec}.
   \end{center}