--- a/prio/Paper/Paper.thy	Mon Feb 13 00:06:59 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 03:31:40 2012 +0000
@@ -587,56 +587,93 @@
 
 section {* Correctness Proof *}
 
-
 (*<*)
 context extend_highest_gen
 begin
-(*>*)
-
 print_locale extend_highest_gen
 thm extend_highest_gen_def
 thm extend_highest_gen_axioms_def
 thm highest_gen_def
+(*>*)
 text {* 
-  Main lemma
+  Sha et al.~\cite{Sha90} state their correctness criterion of PIP in terms
+  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 
+  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 
+  a too low priority. In the way we have set up our formal model of PIP, 
+  their proof idea, even when fixed, does not seem to go through.
+
+  The idea behind our correctness criterion of PIP is as follows: for all states
+  @{text s}, we know the corresponding thread @{text th} with the highest precedence;
+  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
+  @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
+  in @{text s'}.
+
+  \begin{quote}
+  {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
+  any meaningful statement, we need to require that @{text "s"} and 
+  @{text "s' @ s"} are valid states, namely
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  @{term "vt s"}\\
+  @{term "vt (s' @ s)"} 
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
 
-  \begin{enumerate}
-  \item @{term "s"} is a valid state (@{text "vt_s"}):
-    @{thm  vt_s}.
-  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
-    @{thm threads_s}.
-  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
-    @{thm highest}.
-  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
-    @{thm preced_th}.
- 
-  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
-  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
-    its precedence can not be higher than @{term "th"},  therefore
-    @{term "th"} remain to be the one with the highest precedence
-    (@{text "create_low"}):
-    @{thm [display] create_low}
-  \item Any adjustment of priority in 
-    @{term "t"} does not happen to @{term "th"} and 
-    the priority set is no higher than @{term "prio"}, therefore
-    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
-    @{thm [display] set_diff_low}
-  \item Since we are investigating what happens to @{term "th"}, it is assumed 
-    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
-    @{thm [display] exit_diff}
-  \end{enumerate}
+  \begin{quote}
+  {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be active in @{text s} and 
+  has the highest precedence of all active threads in @{text s}. Furthermore the
+  priority of @{text th} is @{text prio}.
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  @{term "th \<in> threads s"}\\
+  @{term "prec th s = Max (cprec s ` threads s)"}\\
+  @{term "prec th s = (prio, DUMMY)"}
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
+  
+  \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
+  not get ``exited'' in @{text "s'"}.
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{l}
+  {If}~~@{text "Create _ prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
+  {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
+  {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
+  \end{tabular}
+  \end{isabelle}
+  \end{quote}
 
-  \begin{lemma}
-  @{thm[mode=IfThen] moment_blocked}
-  \end{lemma}
+  \noindent
+  Under these assumption we will prove the following property:
+
+  \begin{theorem}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"}.
+  @{thm[mode=IfThen] runing_inversion_3[where ?th'="th'", THEN
+  conjunct1]}
+  \end{theorem}
 
   \begin{theorem}
   @{thm[mode=IfThen] runing_inversion_2}
   \end{theorem}
 
-  \begin{theorem}
-  @{thm[mode=IfThen] runing_inversion_3}
-  \end{theorem}
+