diff -r 78523b3ae2ad -r ee4611c1e13c prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Jan 30 09:44:33 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 01 08:16:00 2012 +0000
@@ -1,9 +1,9 @@
 (*<*)
 theory Paper
-imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
+imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar
 begin
 ML {*
-  Printer.show_question_marks_default := false;
+  show_question_marks_default := false;
   *}
 (*>*)
 
@@ -507,6 +507,193 @@
 end
 (*>*)
 
+subsection {* Event @{text "V th cs"} *}
+
+(*<*)
+context step_v_cps_nt
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "V th cs"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "V th cs"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  Under such a context, we investigated how the current precedence @{term "cp"} of 
+  threads change from state @{term "s'"} to @{term "s"}. 
+
+
+  Two subcases are considerted, 
+  where the first is that there exits @{term "th'"} 
+  such that 
+  @{thm [display] nt} 
+  holds, which means there exists a thread @{term "th'"} to take over
+  the resource release by thread @{term "th"}. 
+  In this sub-case, the following results are obtained:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}: 
+  @{thm [display] "depend_s"}
+  which shows two edges are removed while one is added. These changes imply how
+  the current precedences should be re-computed.
+  \item First all threads different from @{term "th"} and @{term "th'"} have their
+  @{term "cp"}-value kept, therefore do not need a re-computation
+  (@{text "cp_kept"}): @{thm [display] cp_kept}
+  This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}
+  need to be recomputed.
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+
+context step_v_cps_nnt
+begin
+(*>*)
+
+text {*
+  The other sub-case is when for all @{text "th'"}
+  @{thm [display] nnt}
+  holds, no such thread exists. The following results can be obtained for this 
+  sub-case:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}:
+  @{thm [display] depend_s}
+  which means only one edge is removed.
+  \item In this case, no re-computation is needed (@{text "eq_cp"}):
+  @{thm [display] eq_cp}
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+(*>*)
+
+
+subsection {* Event @{text "P th cs"} *}
+
+(*<*)
+context step_P_cps_e
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "P th cs"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "P th cs"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+
+  This case is further divided into two sub-cases. The first is when @{thm ee} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item No re-computation is needed (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+*}
+
+(*<*)
+end
+
+context step_P_cps_ne
+begin
+(*>*)
+
+text {*
+  The second is when @{thm ne} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item Threads with no dependence relation with @{term "th"} do not need a re-computation
+    of their @{term "cp"}-values (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+    This lemma implies all threads with a dependence relation with @{term "th"} may need 
+    re-computation.
+  \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier
+    (@{text "eq_up"}):
+    @{thm [display] eq_up}
+  \end{enumerate}
+
+  *}
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Create th prio"} *}
+
+(*<*)
+context step_create_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Create th prio"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "Create th prio"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \item The @{term "cp"}-value of @{term "th"} equals its precedence 
+    (@{text "eq_cp_th"}):
+    @{thm [display] eq_cp_th}
+  \end{enumerate}
+
+*}
+
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Exit th"} *}
+
+(*<*)
+context step_exit_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Exit th"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "Exit th"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+  Since @{term th} does not live in state @{term "s"}, there is no need to compute 
+  its @{term cp}-value.
+*}
+
+(*<*)
+end
+(*>*)
+
+
 section {* Related works \label{related} *}
 
 text {*