--- a/prio/Paper/Paper.thy	Mon Feb 13 03:31:40 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Feb 13 04:22:52 2012 +0000
@@ -660,25 +660,139 @@
   \end{quote}
 
   \noindent
-  Under these assumption we will prove the following property:
+  Under these assumptions we will prove the following property:
 
-  \begin{theorem}
+  \begin{theorem}\label{mainthm}
   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]}
+  the thread @{text th} and the events in @{text "s'"},
+  if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
+  @{text "th' \<in> threads s"}.
   \end{theorem}
 
-  \begin{theorem}
-  @{thm[mode=IfThen] runing_inversion_2}
-  \end{theorem}
+  \noindent
+  This theorem ensures that the thread @{text th}, which has the highest 
+  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.
+
+   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}
+*}
+
+text {* \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}
+  *}
 
- 
-  
+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}
+  *}
+
+text {* \noindent
+  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"}):
+    @{thm [display] chain_building[rule_format]}
+  \item The ready thread chased to is unique (@{text "dchain_unique"}):
+    @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+  \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}
+  *}
 
-TO DO 
+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 
+  (@{text "max_cp_readys_threads"}):
+  @{thm [display] max_cp_readys_threads}
+  \end{enumerate}
+  *}
 
+text {* \noindent
+  The relationship between the count of @{text "P"} and @{text "V"} and the number of 
+  critical resources held by a thread is given as follows:
+  \begin{enumerate}
+  \item The @{term "V"}-operation decreases the number of critical resources 
+    one thread holds (@{text "cntCS_v_dec"})
+     @{thm [display]  cntCS_v_dec}
+  \item The number of @{text "V"} never exceeds the number of @{text "P"} 
+    (@{text "cnp_cnv_cncs"}):
+    @{thm [display]  cnp_cnv_cncs}
+  \item The number of @{text "V"} equals the number of @{text "P"} when 
+    the relevant thread is not living:
+    (@{text "cnp_cnv_eq"}):
+    @{thm [display]  cnp_cnv_eq}
+  \item When a thread is not living, it does not hold any critical resource 
+    (@{text "not_thread_holdents"}):
+    @{thm [display] not_thread_holdents}
+  \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
+    thread does not hold any critical resource, therefore no thread can depend on it
+    (@{text "count_eq_dependents"}):
+    @{thm [display] count_eq_dependents}
+  \end{enumerate}
 *}
 
 (*<*)
@@ -836,123 +950,7 @@
 section {* General properties of Priority Inheritance \label{general} *}
 
 text {*
-  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}
-*}
-
-text {* \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}
-  *}
-
-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}
-  *}
-
-text {* \noindent
-  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"}):
-    @{thm [display] chain_building[rule_format]}
-  \item The ready thread chased to is unique (@{text "dchain_unique"}):
-    @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
-  \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:
-  \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 
-  (@{text "max_cp_readys_threads"}):
-  @{thm [display] max_cp_readys_threads}
-  \end{enumerate}
-  *}
-
-text {* \noindent
-  The relationship between the count of @{text "P"} and @{text "V"} and the number of 
-  critical resources held by a thread is given as follows:
-  \begin{enumerate}
-  \item The @{term "V"}-operation decreases the number of critical resources 
-    one thread holds (@{text "cntCS_v_dec"})
-     @{thm [display]  cntCS_v_dec}
-  \item The number of @{text "V"} never exceeds the number of @{text "P"} 
-    (@{text "cnp_cnv_cncs"}):
-    @{thm [display]  cnp_cnv_cncs}
-  \item The number of @{text "V"} equals the number of @{text "P"} when 
-    the relevant thread is not living:
-    (@{text "cnp_cnv_eq"}):
-    @{thm [display]  cnp_cnv_eq}
-  \item When a thread is not living, it does not hold any critical resource 
-    (@{text "not_thread_holdents"}):
-    @{thm [display] not_thread_holdents}
-  \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
-    thread does not hold any critical resource, therefore no thread can depend on it
-    (@{text "count_eq_dependents"}):
-    @{thm [display] count_eq_dependents}
-  \end{enumerate}
+ 
   *}
 
 section {* Key properties \label{extension} *}

Binary file prio/paper.pdf has changed