diff -r c1028969401a -r 1b72810a2d61 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu May 18 15:11:49 2017 +0100
+++ b/Journal/Paper.thy	Tue May 23 15:08:47 2017 +0100
@@ -1133,8 +1133,9 @@
   % @{text "th_kept"} shows that th is a thread in s'-s
   % }
 
-  Given our assumptions (on @{text th}), the first property we show that a running thread @{text "th'"} must either wait for or
-  hold a resource in state @{text s}.
+  Given our assumptions (on @{text th}), the first property we show
+  that a running thread @{text "th'"} must either wait for or hold a
+  resource in state @{text s}.
 
   \begin{lemma}\label{notdetached}
   If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
@@ -1621,19 +1622,23 @@
 
   \begin{quote} {\bf Assumption on the number of threads created 
   after the state {\boldmath@{text s}}:} Given the
-  state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
+  state @{text s}, in every ``future'' valid state @{text "es @ s"}, we
   require that the number of created threads is less than
   a bound @{text "BC"}, that is 
 
-  \[@{text "len (filter isCreate t) < BC"}\;.\]  
+  \[@{text "len (filter isCreate es) < BC"}\;\]  
+  
+  wherby @{text es} is a list of events.
   \end{quote}
 
   \noindent Note that it is not enough to just to state that there are
   only finite number of threads created up until a single state @{text
   "s' @ s"} after @{text s}.  Instead, we need to put this bound on
   the @{text "Create"} events for all valid states after @{text s}.
-  This ensures that no matter which ``future'' state is reached, the number
-  of @{text "Create"}-events is finite.
+  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.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about
@@ -1654,14 +1659,14 @@
   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 
   For each such @{text "th'"} there exists a finite bound @{text "BND(th')"} 
   such that for all future 
-  valid states @{text "t @ s"},
-  we have that if \mbox{@{term "\<not>(detached (t @ s) th')"}}, then 
-  \[@{text "len (actions_of {th'} t) < BND(th')"}\] 
+  valid states @{text "es @ s"},
+  we have that if \mbox{@{term "\<not>(detached (es @ s) th')"}}, then 
+  \[@{text "len (actions_of {th'} es) < BND(th')"}\] 
   \end{quote} 
 
   \noindent By this assumption we enforce that any thread potentially
   blocking @{term th} must become detached (that is lock no resource
-  anymore) after a finite number of events in @{text "t @ s"}. Again
+  anymore) after a finite number of events in @{text "es @ s"}. Again
   we have to state this bound to hold in all valid states after @{text
   s}. The bound reflects how each thread @{text "th'"} is programmed:
   Though we cannot express what instructions a thread is executing,
@@ -1675,10 +1680,10 @@
   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 "t @ s"}. For example, suppose
-  $\textit{t} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
+  @{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 "t @ s"} are
+  @{text "es @ s"} are
 
   \begin{center}
   \begin{tabular}{l}
@@ -1697,82 +1702,87 @@
   \begin{center}
   \begin{tabular}{lcl}
   @{text "s upto []"} & $\dn$ & $[]$\\
-  @{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
+  @{text "s upto (_::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
   \end{tabular}
   \end{center}
   
-
-  \noindent Assume you have an extension @{text t}, this essentially 
-  defines in out list representation of states all the postfixes of 
-  @{text t}.
+  \noindent
+  Our theorem can then be stated as follows:
 
   \begin{theorem}
   Given our assumptions about bounds, we have that 
 
   \[
   @{text "len"}\,[@{text "s'"} 
-  \leftarrow @{text "s upto t"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq 1 + 
+  \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \;\;\leq\;\; 
+  @{text "BC"} + \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}\;. 
   \]
 
-  \[@{thm bounded_extend_highest.priority_inversion_is_finite_upto}\]
   \end{theorem}
 
-
-  Theorem: 
+  \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'"}] 
+  \end{equation}
 
-  \begin{isabelle}\ \ \ \ \ %%%
-  @{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le>
-  1 + len (actions_of blockers t) + len (filter isCreate t)"}
-  \end{isabelle}
+  \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
 
-  Proof:
+  \begin{equation}\label{secondeq}
+  @{text "len es"} = @{text "len (actions_of {th} es)"} +
+                     @{text "len (filter isCreate es)"} + 
+                      @{text "len (actions_of blockers es)"}
+  \end{equation}
+
+  \noindent
+  Further we know that an action of @{text th} 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'"}]
+  \]
   
-  Consider the states @{text "s upto t"}. It holds that all the states where
-  @{text "th"} runs and all the states where @{text "th"} does not run is 
-  equalt to @{text "len t"}. That means
-
-  \begin{center}
-  @{text "states where th does not run = len t - states where th runs"} (*)
-  \end{center}
-
-  It also holds that all the actions of @{text "th"} are less or equal to 
-  the states where @{text th} runs. That is
-
-  \begin{center}
-  @{text "len (actions_of {th} t) \<le> states where th runs"}
-  \end{center}
-  
-  That means in $(*)$ we have 
+  \noindent Substituting this into \eqref{firsteq} gives
 
-  \begin{center}
-  @{text "states where th does not run \<le> len t - len (actions_of {th} t)"}
-  \end{center}
-
-  If we look at all the events that can occur in @{text "s upto t"}, we have that
+  \[
+  @{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)"}
+  \]
 
-  \begin{center}
-  @{text "len t = len (action_of {th}) + len (action_of blockers t) + 
-  len (filter isCreate t)"}
-  \end{center}
+  into which we can substitute \eqref{secondeq} yielding
 
-  This gives us finally our theorem. \hfill\qed\medskip
+  \[
+  @{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)"}
+  \]
 
-  \noindent In order to now show the absence of indefinite Priority
-  Inversion, we need to show that the number of actions of the @{text
-  "blockers"} is bounded---the number of @{text "Creates"} is clearly
-  bounded by our first assumption. The number of actions of each
-  individual thread in @{text "blockers"} is bound by our second
-  assumption.  Since there can only be a finite number of @{text
-  blockers} in state @{text s} their overall sum is also bounded.
-  This is actually the main conclusion we obtain for the Priority
-  Inheritance Protocol: this above theorem shows is that set of @{text
-  blockers} is fixed at state @{text s} when the Priority Inversion
-  occured and 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
-  fropm running.
+  \noindent By our first assumption we know that the @{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
+
+  \[
+  @{text "len (actions_of blockers es)"} \;\;\leq\;\;
+  \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}
+  \]
 
+  \noindent With this in place we can conclude our theorem.\hfill\qed
+  \end{proof}
 
+  \noindent This theorem is the main conclusion we obtain for the
+  Priority Inheritance Protocol: it shows that 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