diff -r 2aa37de77f31 -r b6ea51cd2e88 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jan 14 03:29:22 2016 +0000
+++ b/Journal/Paper.thy	Fri Jan 15 02:05:29 2016 +0000
@@ -23,7 +23,9 @@
   cpreced ("cprec") and
   cp ("cprec") and
   holdents ("resources") and
-  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
+  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
+  cntP ("c\<^bsub>P\<^esub>") and
+  cntV ("c\<^bsub>V\<^esub>")
  
 (*>*)
 
@@ -178,17 +180,18 @@
   priority.}'' The same error is also repeated later in this textbook.
 
   
-  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have 
-  found that specify the incorrect behaviour, it seems also many
-  informal descriptions of PIP overlook the possibility that another
-  high-priority might wait for a low-priority process to finish.
-  A notable exception is the texbook \cite{buttazzo}, which gives the correct 
-  behaviour of resetting the priority of a thread to the highest remaining priority of the 
-  threads it blocks. This textbook also gives an informal proof for 
-  the correctness of PIP in the style of Sha et al. Unfortunately, this informal 
-  proof is too vague to be useful for formalising the correctness of PIP
-  and the specification leaves out nearly all details in order 
-  to implement PIP efficiently.\medskip\smallskip
+  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+  formal publications we have found that specify the incorrect
+  behaviour, it seems also many informal descriptions of PIP overlook
+  the possibility that another high-priority might wait for a
+  low-priority process to finish.  A notable exception is the texbook
+  \cite{buttazzo}, which gives the correct behaviour of resetting the
+  priority of a thread to the highest remaining priority of the
+  threads it blocks. This textbook also gives an informal proof for
+  the correctness of PIP in the style of Sha et al. Unfortunately,
+  this informal proof is too vague to be useful for formalising the
+  correctness of PIP and the specification leaves out nearly all
+  details in order to implement PIP efficiently.\medskip\smallskip
   %
   %The advantage of formalising the
   %correctness of a high-level specification of PIP in a theorem prover
@@ -196,27 +199,29 @@
   %informal reasoning (since we have to analyse all possible behaviours
   %of threads, i.e.~\emph{traces}, that could possibly happen).
 
-  \noindent
-  {\bf Contributions:} There have been earlier formal investigations
-  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
-  checking techniques. This paper presents a formalised and
-  mechanically checked proof for the correctness of PIP. For this we 
-  needed to design a new correctness criterion for PIP. In contrast to model checking, our
-  formalisation provides insight into why PIP is correct and allows us
-  to prove stronger properties that, as we will show, can help with an
-  efficient implementation of PIP in the educational PINTOS operating
-  system \cite{PINTOS}.  For example, we found by ``playing'' with the
-  formalisation that the choice of the next thread to take over a lock
-  when a resource is released is irrelevant for PIP being correct---a
-  fact that has not been mentioned in the literature and not been used
-  in the reference implementation of PIP in PINTOS.  This fact, however, is important
-  for an efficient implementation of PIP, because we can give the lock
-  to the thread with the highest priority so that it terminates more
-  quickly.  We were also being able to generalise the scheduler of Sha
-  et al.~\cite{Sha90} to the practically relevant case where critical 
-  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of 
-  this restriction. %In the existing literature there is no 
-  %proof and also no proving method that cover this generalised case.
+  \noindent {\bf Contributions:} There have been earlier formal
+  investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
+  employ model checking techniques. This paper presents a formalised
+  and mechanically checked proof for the correctness of PIP. For this
+  we needed to design a new correctness criterion for PIP. In contrast
+  to model checking, our formalisation provides insight into why PIP
+  is correct and allows us to prove stronger properties that, as we
+  will show, can help with an efficient implementation of PIP. We
+  illustrate this with an implementation of PIP in the educational
+  PINTOS operating system \cite{PINTOS}.  For example, we found by
+  ``playing'' with the formalisation that the choice of the next
+  thread to take over a lock when a resource is released is irrelevant
+  for PIP being correct---a fact that has not been mentioned in the
+  literature and not been used in the reference implementation of PIP
+  in PINTOS.  This fact, however, is important for an efficient
+  implementation of PIP, because we can give the lock to the thread
+  with the highest priority so that it terminates more quickly.  We
+  were also being able to generalise the scheduler of Sha et
+  al.~\cite{Sha90} to the practically relevant case where critical
+  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+  an example of this restriction. In the existing literature there is
+  no proof and also no proving method that cover this generalised
+  case.
 
   \begin{figure}
   \begin{center}
@@ -382,6 +387,18 @@
   tasks involved in the inheritance process and thus minimises the number
   of potentially expensive thread-switches. 
 
+  We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+  in a state @{term s}. This can be straightforwardly defined in Isabelle as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{@ {}l}
+  @{thm cntP_def}\\
+  @{thm cntV_def}
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent using the predefined function @{const count} for lists.
+
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
   this list (i.e.~the head, or short @{term hd}) is chosen to be the one 
@@ -943,8 +960,39 @@
   From these two lemmas we can see the correctness of PIP, which is
   that: the blockage of th is reasonable and under control.
 
+  Lemmas we want to describe:
+
+  \begin{lemma}
+  @{thm eq_pv_persist}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm eq_pv_blocked}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm runing_cntP_cntV_inv}
+  \end{lemma}
+
+  \noindent
+  Remember we do not have the well-nestedness restriction in our
+  proof, which means the difference between the counters @{const cntV}
+  and @{const cntP} can be larger than @{term 1}.
+
+  \begin{lemma}
+  @{thm runing_inversion}
+  \end{lemma}
+  
+
+  \begin{lemma}
+  @{thm th_blockedE}
+  \end{lemma}
+
   \subsection*{END OUTLINE}
 
+
+
+
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
   It is relatively easy to see that:
@@ -957,7 +1005,7 @@
   \end{isabelle}
 
   \noindent
-  The second property is by induction of @{term vt}. The next three
+  The second property is by induction on @{term vt}. The next three
   properties are: 
 
   \begin{isabelle}\ \ \ \ \ %%%