--- a/Journal/Paper.thy	Wed Jan 06 20:46:14 2016 +0800
+++ b/Journal/Paper.thy	Wed Jan 06 16:34:26 2016 +0000
@@ -1,6 +1,8 @@
 (*<*)
 theory Paper
-imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
+imports "../Implementation" 
+        "../Correctness" 
+        "~~/src/HOL/Library/LaTeXsugar"
 begin
 
 
@@ -19,7 +21,7 @@
   Cs ("C") and
   readys ("ready") and
   preced ("prec") and
-  preceds ("precs") and
+(*  preceds ("precs") and*)
   cpreced ("cprec") and
   cp ("cprec") and
   holdents ("resources") and
@@ -361,7 +363,7 @@
   We also use the abbreviation 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{abbrev "preceds s ths"}
+  ???preceds s ths
   \end{isabelle}
 
   \noindent
@@ -898,6 +900,53 @@
   However, we are able to combine their two separate bounds into a
   single theorem improving their bound.
 
+  \subsection*{\bf OUTLINE}
+
+  Since @{term "th"} is the most urgent thread, if it is somehow
+  blocked, people want to know why and wether this blocking is
+  reasonable.
+
+  @{thm [source] th_blockedE} @{thm th_blockedE}
+
+  if @{term "th"} is blocked, then there is a path leading from 
+  @{term "th"} to @{term "th'"}, which means:
+  there is a chain of demand leading from @{term th} to @{term th'}.
+
+  %%% in other words
+  %%% th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. 
+  %%% 
+  %%% We says that th is blocked by "th'".
+
+  THEN
+
+  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
+
+  It is basic propery with non-trival proof. 
+
+  THEN
+
+  @{thm [source] max_preced} @{thm max_preced}
+
+  which says @{term "th"} holds the max precedence.
+
+  THEN
+ 
+  @{thm [source] th_cp_max th_cp_preced th_kept}
+  @{thm th_cp_max th_cp_preced th_kept}
+
+  THENTHEN
+
+  @{thm [source] runing_inversion_4} @{thm runing_inversion_4}
+
+  which explains what the @{term "th'"} looks like. Now, we have found the 
+  @{term "th'"} which blocks @{term th}, we need to know more about it.
+  To see what kind of thread can block @{term th}.
+
+  From these two lemmas we can see the correctness of PIP, which is
+  that: the blockage of th is reasonable and under control.
+
+  \subsection*{END OUTLINE}
+
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
   It is relatively easy to see that:
@@ -915,9 +964,10 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
-  @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
-  @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
+  HERE??
+  %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+  %@ {thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+  %@ {thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
   \end{tabular}
   \end{isabelle}
 
@@ -931,13 +981,13 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{text If}~@{thm (prem 1) acyclic_RAG}~@{text "then"}:\\
+  HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\
   \hspace{5mm}@{thm (concl) acyclic_RAG},
   @{thm (concl) finite_RAG} and
   @{thm (concl) wf_dep_converse},\\
-  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads}
+  %\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads}
   and\\
-  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
+  %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
   \end{tabular}
   \end{isabelle}
 
@@ -1136,7 +1186,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm children_def2}
+  HERE?? %%@ {thm children_def2}
   \end{tabular}
   \end{isabelle}
 
@@ -1146,9 +1196,9 @@
   a resource). We can prove the following lemma.
 
   \begin{lemma}\label{childrenlem}
-  @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
+  HERE %@{text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
   \begin{center}
-  @{thm (concl) cp_rec}.
+  %@ {thm (concl) cp_rec}.
   \end{center}
   \end{lemma}
   
@@ -1184,7 +1234,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm eq_dep},\\
+  HERE ?? %@ {thm eq_dep},\\
   @{thm eq_cp_th}, and\\
   @{thm[mode=IfThen] eq_cp}
   \end{tabular}
@@ -1208,7 +1258,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm eq_dep}, and\\
+  HERE %@ {thm eq_dep}, and\\
   @{thm[mode=IfThen] eq_cp}
   \end{tabular}
   \end{isabelle}
@@ -1257,9 +1307,9 @@
   %
   %\begin{isabelle}\ \ \ \ \ %%%
   %\begin{tabular}{@ {}l}
-  %@{thm[mode=IfThen] eq_up_self}\\
-  %@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
-  %@{text "then"} @{thm (concl) eq_up}.
+  %@ {thm[mode=IfThen] eq_up_self}\\
+  %@{text "If"} @ {thm (prem 1) eq_up}, @ {thm (prem 2) eq_up} and @ {thm (prem 3) eq_up}\\
+  %@{text "then"} @ {thm (concl) eq_up}.
   %\end{tabular}
   %\end{isabelle}
   %
@@ -1330,7 +1380,7 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm RAG_s}\\
-  @{thm eq_cp}
+  HERE %@ {thm eq_cp}
   \end{tabular}
   \end{isabelle}
 
@@ -1343,7 +1393,7 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   @{thm RAG_s}\\
-  @{thm[mode=IfThen] eq_cp}
+  HERE %@ {thm[mode=IfThen] eq_cp}
   \end{tabular}
   \end{isabelle}
 
@@ -1362,8 +1412,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
   %%@ {t hm[mode=IfThen] eq_up_self}\\
-  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
-  @{text "then"} @{thm (concl) eq_up}.
+  HERE
+  %@{text "If"} @ {thm (prem 1) eq_up}, @ {thm (prem 2) eq_up} and @ {thm (prem 3) eq_up}\\
+  %@{text "then"} @ {thm (concl) eq_up}.
   \end{tabular}
   \end{isabelle}