--- a/prio/Paper/Paper.thy	Mon Feb 13 04:22:52 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 05:41:53 2012 +0000
@@ -509,7 +509,7 @@
   \noindent
   In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
   Note that in the initial state, that is where the list of events is empty, the set 
-  @{term threads} is empty and therefore there is no thread ready nor a running.
+  @{term threads} is empty and therefore there is neither a thread ready nor running.
   If there is one or more threads ready, then there can only be \emph{one} thread
   running, namely the one whose current precedence is equal to the maximum of all ready 
   threads. We use the set-comprehension to capture both possibilities.
@@ -582,7 +582,7 @@
 
   \noindent
   This completes our formal model of PIP. In the next section we present
-  properties that show our version of PIP is correct.
+  properties that show our model of PIP is correct.
 *}
 
 section {* Correctness Proof *}
@@ -600,7 +600,7 @@
   of the number of critical resources: if there are @{text m} critical
   resources, then a blocked job can only be blocked @{text m} times---that is
   a bounded number of times.
-  For their version of PIP, this is \emph{not} true (as pointed out by 
+  For their version of PIP, this property is \emph{not} true (as pointed out by 
   Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
   blocked an unbounded number of times by creating medium-priority
   threads that block a thread locking a critical resource and having 
@@ -612,11 +612,11 @@
   we show that in every future state (denoted by @{text "s' @ s"}) in which
   @{text th} is still active, either @{text th} is running or it is blocked by a 
   thread that was active in the state @{text s}. Since in @{text s}, as in every 
-  state, the set of active threads is finite, @{text th} can only blocked a
-  finite number of time. We will actually prove a stricter bound. However,
-  this correctness criterion depends on a number of assumptions about the states
+  state, the set of active threads is finite, @{text th} can only be blocked a
+  finite number of times. We will actually prove a stricter bound. However,
+  this correctness criterion hinges on a number of assumptions about the states
   @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
-  in @{text s'}.
+  in @{text s'}. We list them next.
 
   \begin{quote}
   {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
@@ -645,10 +645,10 @@
   
   \begin{quote}
   {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
-  be blocked indefinitely. Of course this can by violated if threads with higher priority
-  than @{text th} are created in @{text s'}. Therefore we have to assume that  
-  events in @{text s'} can only create (respectively set) threads with lower or equal 
-  priority than @{text prio} of @{text th}. We also have to assume that @{text th} does
+  be blocked indefinitely. Of course this can happen if threads with higher priority
+  than @{text th} are continously created in @{text s'}. Therefore we have to assume that  
+  events in @{text s'} can only create (respectively set) threads with equal or lower 
+  priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does
   not get ``exited'' in @{text "s'"}.
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{l}
@@ -674,36 +674,40 @@
   precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} 
   by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
   that means by only finitely many threads. Consequently, indefinite wait of
-  @{text th}, that is Priority Inversion, cannot occur.
+  @{text th}---whcih is Priority Inversion---cannot occur.
+
+  In what follows we will describe properties of PIP that allow us to prove 
+  Theorem~\ref{mainthm}. It is relatively easily to see that
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
+  @{thm[mode=IfThen]  finite_threads}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  where the second property is by induction of @{term vt}. The next three
+  properties are 
 
-   The following are several very basic prioprites:
-  \begin{enumerate}
-  \item All runing threads must be ready (@{text "runing_ready"}):
-          @{thm[display] "runing_ready"}  
-  \item All ready threads must be living (@{text "readys_threads"}):
-          @{thm[display] "readys_threads"} 
-  \item There are finite many living threads at any moment (@{text "finite_threads"}):
-          @{thm[display] "finite_threads"} 
-  \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): 
-          @{thm[display] "wq_distinct"} 
-  \item All threads in waiting queues are living threads (@{text "wq_threads"}): 
-          @{thm[display] "wq_threads"} 
-  \item The event which can get a thread into waiting queue must be @{term "P"}-events
-         (@{text "block_pre"}): 
-          @{thm[display] "block_pre"}   
-  \item A thread may never wait for two different critical resources
-         (@{text "waiting_unique"}): 
-          @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
-  \item Every resource can only be held by one thread
-         (@{text "held_unique"}): 
-          @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
-  \item Every living thread has an unique precedence
-         (@{text "preced_unique"}): 
-          @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
-  \end{enumerate}
-*}
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
+  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
+  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+  \end{tabular}
+  \end{isabelle}
 
-text {* \noindent
+  \noindent
+  The first one states that every waiting thread can only wait for a single
+  resource (because it gets suspended after requesting that resource), and
+  the second that every resource can only be held by a single thread. The
+  third property establishes that in every given valid state, there is
+  at most one running thread.
+
+  TODO
+
+  \noindent
   The following lemmas show how RAG is changed with the execution of events:
   \begin{enumerate}
   \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
@@ -761,8 +765,6 @@
 text {* \noindent
   Some deeper results about the system:
   \begin{enumerate}
-  \item There can only be one running thread (@{text "runing_unique"}):
-  @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
   \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
   @{thm [display] max_cp_eq}
   \item There must be one ready thread having the max @{term "cp"}-value