diff -r 41e4b331ce08 -r 163cd8034e5b prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Feb 14 00:27:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 02:24:09 2012 +0000
@@ -27,6 +27,9 @@
   holdents ("resources") and
   original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
+
+abbreviation
+ "detached s th \<equiv> cntP s th = cntV s th"
 (*>*)
 
 section {* Introduction *}
@@ -592,10 +595,6 @@
 (*<*)
 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 {* 
   Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
@@ -699,11 +698,13 @@
   gives up its resources after a finite amount of time. We found that
   this assumption is awkward to formalise in our model. Therefore we
   leave it out and let the programmer assume the responsibility to
-  program threads in such a benign manner. In this detail, we do not
+  program threads in such a benign manner (in addition to causeing no 
+  circularity in the @{text RAG}). In this detail, we do not
   make any progress in comparison with the work by Sha et al.
 
   In what follows we will describe properties of PIP that allow us to prove 
-  Theorem~\ref{mainthm}. It is relatively easily to see that
+  Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
+  It is relatively easily to see that
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -713,7 +714,7 @@
   \end{isabelle}
 
   \noindent
-  where the second property is by induction of @{term vt}. The next three
+  whereby the second property is by induction of @{term vt}. The next three
   properties are 
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -725,12 +726,12 @@
   \end{isabelle}
 
   \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 having
-  to wait for it); the second that every resource can only be held by a single thread; 
+  The first property states that every waiting thread can only wait for a single
+  resource (because it gets suspended after requesting that resource); 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. We can also show the following properties 
-  about the RAG in @{text "s"}.
+  about the @{term RAG} in @{text "s"}.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -738,47 +739,56 @@
   \hspace{5mm}@{thm (concl) acyclic_depend},
   @{thm (concl) finite_depend} and
   @{thm (concl) wf_dep_converse},\\
-  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}\\
-  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}
+  and\\
+  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
   \end{tabular}
   \end{isabelle}
 
-  TODO
+  \noindent
+  The acyclicity property follow from how we restricted the events in
+  @{text step}; similarly the finiteness and well-foundedness property.
+  The last two properties establish that every thread in a @{text "RAG"}
+  (either holding or waiting for a resource) is a live thread.
+
+  To state the key lemma in our proof, it will be convenient to introduce the notion
+  of a \emph{detached} thread in a state, that is one which does not hold any
+  critical resource nor requests one. 
+
+  \begin{lemma}\label{mainlem}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"},
+  if @{term "th' \<in> treads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
+  then @{text "th' \<notin> running (s' @ s)"}.
+  \end{lemma}
 
   \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"}):
-    @{thm[display] depend_set_unchanged}
-  \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
-    @{thm[display] depend_create_unchanged}
-  \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
-    @{thm[display] depend_exit_unchanged}
-  \item Execution of @{term "P"} (@{text "step_depend_p"}):
-    @{thm[display] step_depend_p}
-  \item Execution of @{term "V"} (@{text "step_depend_v"}):
-    @{thm[display] step_depend_v}
-  \end{enumerate}
-  *}
+  The point of this lemma is that a thread different from @{text th} (which has the highest
+  precedence in @{text s}) not holding any resource cannot be running 
+  in the state @{text "s' @ s"}.
 
-text {* \noindent
-  These properties are used to derive the following important results about RAG:
-  \begin{enumerate}
-  \item RAG is loop free (@{text "acyclic_depend"}):
-  @{thm [display] acyclic_depend}
-  \item RAGs are finite (@{text "finite_depend"}):
-  @{thm [display] finite_depend}
-  \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
-  @{thm [display] wf_dep_converse}
-  \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
-  @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
-  \item All threads in RAG are living threads 
-    (@{text "dm_depend_threads"} and @{text "range_in"}):
-    @{thm [display] dm_depend_threads range_in}
-  \end{enumerate}
-  *}
+  \begin{proof}
+  Since thread @{text "th'"} does not hold any resource, no thread can depend on it. 
+  Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
+  @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the 
+  state @{text "(s' @ s)"} and precedences are distinct among threads, we have
+  @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this 
+  we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
+  Since @{text "prec th (s' @ s)"} is already the highest 
+  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by 
+  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
+  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
+  By defintion of @{text "running"}, @{text "th'"} can not be running in state
+  @{text "s' @ s"}, as we had to show.\qed
+  \end{proof}
 
-text {* \noindent
+  \noindent
+  Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to 
+  issue a {text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
+  one step further, @{text "th'"} still cannot hold any resource. The situation will 
+  not change in further extensions as long as @{text "th"} holds the highest precedence.
+
+
   The following lemmas show how every node in RAG can be chased to ready threads:
   \begin{enumerate}
   \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
@@ -788,17 +798,6 @@
   \end{enumerate}
   *}
 
-text {* \noindent
-  Properties about @{term "next_th"}:
-  \begin{enumerate}
-  \item The thread taking over is different from the thread which is releasing
-  (@{text "next_th_neq"}):
-  @{thm [display] next_th_neq}
-  \item The thread taking over is unique
-  (@{text "next_th_unique"}):
-  @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  
-  \end{enumerate}
-  *}
 
 text {* \noindent
   Some deeper results about the system:
@@ -833,23 +832,13 @@
     (@{text "count_eq_dependents"}):
     @{thm [display] count_eq_dependents}
   \end{enumerate}
-*}
+
 
-(*<*)
-end
-(*>*)
+  @{thm[display] live}
+*}
 
 subsection {* Proof idea *}
 
-(*<*)
-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 {*
 The reason that only threads which already held some resoures
 can be runing and block @{text "th"} is that if , otherwise, one thread 
@@ -869,48 +858,68 @@
   then after a while, only thread @{text "th"} is left running. This shows how indefinite 
   priority inversion can be avoided. 
 
-  So, the key of the proof is to establish the correctness of @{text "moment_blocked"}.
-  We are going to show how this lemma is proved. At the heart of this proof, is 
-  lemma @{text "pv_blocked"}:
-  @{thm [display] pv_blocked}
-  This lemma says: for any @{text "s"}-extension {text "t"}, if thread @{text "th'"}
-  does not hold any resource, it can not be running at @{text "t@s"}.
+*}
+
+section {* Key properties \label{extension} *}
 
 
-  \noindent Proof: 
+text {* \noindent
+  All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
+  It can be proved that @{term "extend_highest_gen"} holds 
+  for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
+  @{thm [display] red_moment}
+  
+  From this, an induction principle can be derived for @{text "t"}, so that 
+  properties already derived for @{term "t"} can be applied to any prefix 
+  of @{text "t"} in the proof of new properties 
+  about @{term "t"} (@{text "ind"}):
+  \begin{center}
+  @{thm[display] ind}
+  \end{center}
+
+  The following properties can be proved about @{term "th"} in @{term "t"}:
   \begin{enumerate}
-  \item Since thread @{text "th'"} does not hold any resource, no thread may depend on it, 
-    so its current precedence @{text "cp (t@s) th'"} equals to its own precedence
-   @{text "preced th' (t@s)"}.  \label{arg_1}
-  \item Since @{text "th"} has the highest precedence in the system and 
-    precedences are distinct among threads, we have
-    @{text "preced th' (t@s) < preced th (t@s)"}. From this and item \ref{arg_1}, 
-    we have @{text "cp (t@s) th' < preced th (t@s)"}.
-  \item Since @{text "preced th (t@s)"} is already the highest in the system, 
-    @{text "cp (t@s) th"} can not be higher than this and can not be lower neither (by 
-    the definition of @{text "cp"}), we have @{text "preced th (t@s) = cp (t@s) th"}.
-  \item Finally we have @{text "cp (t@s) th' < cp (t@s) th"}.
-  \item By defintion of @{text "running"}, @{text "th'"} can not be runing at 
-    @{text "t@s"}.
+  \item In @{term "t"}, thread @{term "th"} is kept live and its 
+    precedence is preserved as well
+    (@{text "th_kept"}): 
+    @{thm [display] th_kept}
+  \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
+    all living threads
+    (@{text "max_preced"}): 
+    @{thm [display] max_preced}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
+    among all living threads
+    (@{text "th_cp_max_preced"}): 
+    @{thm [display] th_cp_max_preced}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
+    precedence among all living threads
+    (@{text "th_cp_max"}): 
+    @{thm [display] th_cp_max}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
+    @{term "s"}
+    (@{text "th_cp_preced"}): 
+    @{thm [display] th_cp_preced}
   \end{enumerate}
-  Since @{text "th'"} is not able to run at state @{text "t@s"}, it is not able to 
-  make either {text "P"} or @{text "V"} action, so if @{text "t@s"} is extended
-  one step further, @{text "th'"} still does not hold any resource. 
-  The situation will not unchanged in further extensions as long as 
-  @{text "th"} holds the highest precedence. Since this @{text "t"} is arbitarily chosen 
-  except being constrained by predicate @{text "extend_highest_gen"} and 
-  this predicate has the property that if it holds for @{text "t"}, it also holds
-  for any moment @{text "i"} inside @{text "t"}, as shown by lemma @{text "red_moment"}:
-@{thm [display] "extend_highest_gen.red_moment"}
-  so @{text "pv_blocked"} can be applied to any @{text "moment i t"}. 
-  From this, lemma @{text "moment_blocked"} follows.
-*}
+  *}
+
+text {* \noindent
+  The main theorem of this part is to characterizing the running thread during @{term "t"} 
+  (@{text "runing_inversion_2"}):
+  @{thm [display] runing_inversion_2}
+  According to this, if a thread is running, it is either @{term "th"} or was
+  already live and held some resource 
+  at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
+
+  Since there are only finite many threads live and holding some resource at any moment,
+  if every such thread can release all its resources in finite duration, then after finite
+  duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
+  then.
+  *}
 
 (*<*)
 end
 (*>*)
 
-
 section {* Properties for an Implementation\label{implement} *}
 
 text {*
@@ -1227,122 +1236,7 @@
   \bibliography{root}
 *}
 
-section {* Key properties \label{extension} *}
-
-(*<*)
-context extend_highest_gen
-begin
-(*>*)
-
-text {*
-  The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this 
-  purpose, we need to investigate what happens after one thread takes the highest precedence. 
-  A locale is used to describe such a situation, which assumes:
-  \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}.
-  \end{enumerate}
-  *}
-
-text {* \noindent
-  Under these assumptions, some basic priority can be derived for @{term "th"}:
-  \begin{enumerate}
-  \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
-    @{thm [display] eq_cp_s_th}
-  \item The current precedence of @{term "th"} is the highest precedence in 
-    the system (@{text "highest_cp_preced"}):
-    @{thm [display] highest_cp_preced}
-  \item The precedence of @{term "th"} is the highest precedence 
-    in the system (@{text "highest_preced_thread"}):
-    @{thm [display] highest_preced_thread}
-  \item The current precedence of @{term "th"} is the highest current precedence 
-    in the system (@{text "highest'"}):
-    @{thm [display] highest'}
-  \end{enumerate}
-  *}
-
-text {* \noindent
-  To analysis what happens after state @{term "s"} a sub-locale is defined, which 
-  assumes:
-  \begin{enumerate}
-  \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}
-*}
-
-text {* \noindent
-  All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
-  It can be proved that @{term "extend_highest_gen"} holds 
-  for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
-  @{thm [display] red_moment}
-  
-  From this, an induction principle can be derived for @{text "t"}, so that 
-  properties already derived for @{term "t"} can be applied to any prefix 
-  of @{text "t"} in the proof of new properties 
-  about @{term "t"} (@{text "ind"}):
-  \begin{center}
-  @{thm[display] ind}
-  \end{center}
-
-  The following properties can be proved about @{term "th"} in @{term "t"}:
-  \begin{enumerate}
-  \item In @{term "t"}, thread @{term "th"} is kept live and its 
-    precedence is preserved as well
-    (@{text "th_kept"}): 
-    @{thm [display] th_kept}
-  \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
-    all living threads
-    (@{text "max_preced"}): 
-    @{thm [display] max_preced}
-  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
-    among all living threads
-    (@{text "th_cp_max_preced"}): 
-    @{thm [display] th_cp_max_preced}
-  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
-    precedence among all living threads
-    (@{text "th_cp_max"}): 
-    @{thm [display] th_cp_max}
-  \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
-    @{term "s"}
-    (@{text "th_cp_preced"}): 
-    @{thm [display] th_cp_preced}
-  \end{enumerate}
-  *}
-
-text {* \noindent
-  The main theorem of this part is to characterizing the running thread during @{term "t"} 
-  (@{text "runing_inversion_2"}):
-  @{thm [display] runing_inversion_2}
-  According to this, if a thread is running, it is either @{term "th"} or was
-  already live and held some resource 
-  at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
-
-  Since there are only finite many threads live and holding some resource at any moment,
-  if every such thread can release all its resources in finite duration, then after finite
-  duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
-  then.
-  *}
 
 (*<*)
 end
-
-end
 (*>*)
\ No newline at end of file