
diff -r f70344294e99 -r 10c16b85a839 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Oct 21 14:47:01 2016 +0100
+++ b/Journal/Paper.thy	Fri Dec 09 12:51:29 2016 +0000
@@ -424,7 +424,7 @@
   tasks involved in the inheritance process and thus minimises the number
   of potentially expensive thread-switches. 
 
-  {\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+  \endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
   in a state @{term s}. This can be straightforwardly defined in Isabelle as
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -434,7 +434,7 @@
   \end{tabular}}
   \end{isabelle}
 
-  \noindent using the predefined function @{const count} for lists.
+  \noindent using the predefined function @{const count} for lists.}
 
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
@@ -569,16 +569,17 @@
   forrest} is a forest which is well-founded and every node has 
   finitely many children (is only finitely branching).
 
+  \endnote{
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm rtrancl_path.intros}
   \end{isabelle} 
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm rpath_def}
-  \end{isabelle}
+  \end{isabelle}}
 
 
-  {\bf Lemma about overlapping paths}
+  \endnote{{\bf Lemma about overlapping paths}}
   
 
   We will design our PIP-scheduler  
@@ -619,9 +620,10 @@
   @{thm cpreced_def}\hfill\numbered{cpreced}
   \end{isabelle}
 
+  \endnote{
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm cp_alt_def cp_alt_def1}
-  \end{isabelle}
+  \end{isabelle}}
 
   \noindent
   where the dependants of @{text th} are given by the waiting queue function.
@@ -881,7 +883,7 @@
 (*>*)
 text {*
 
-  In this section we prove facts that immediately follow from
+  \endnote{In this section we prove facts that immediately follow from
   our definitions of valid traces.
 
   \begin{lemma}??\label{precedunique}
@@ -917,7 +919,7 @@
   infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"}
   and @{text "th'\<^sub>2"} are the same threads. However, this also means the
   roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed
-  \end{proof}
+  \end{proof}}
 
   *}
 (*<*)end(*>*)
@@ -1030,9 +1032,9 @@
   Given the assumptions about states @{text "s"} and @{text "s' @ s"},
   the thread @{text th} and the events in @{text "s'"}, then either
   \begin{itemize}
-  \item @{term "th \<in> running (s' @ s)"} or\medskip
+  \item[$\bullet$] @{term "th \<in> running (s' @ s)"} or\medskip
 
-  \item there exists a thread @{term "th'"} with @{term "th' \<noteq> th"}
+  \item[$\bullet$] there exists a thread @{term "th'"} with @{term "th' \<noteq> th"}
   and @{term "th' \<in> running (s' @ s)"} such that @{text "th' \<in> threads
   s"}, @{text "\<not> detached s th'"} and @{term "cp (s' @ s) th' = prec
   th s"}.
@@ -1074,14 +1076,14 @@
 
   Given our assumptions (on @{text th}), the first property we can
   show is that any running thread, say @{text "th'"}, has the same
-  precedence of @{text th}:
+  precedence as @{text th}:
 
   \begin{lemma}\label{runningpreced}
   @{thm [mode=IfThen] running_preced_inversion}
   \end{lemma}
 
   \begin{proof}
-  By definition the running thread has as current precedence the maximum of
+  By definition, the running thread has as current precedence the maximum of
   all ready threads, that is
 
   \begin{center}
@@ -1089,53 +1091,71 @@
   \end{center}
 
   \noindent
-  We also know that this is equal to all threads, that is
+  We also know that this is equal to the current precedences of all threads,
+  that is
 
   \begin{center}
   @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
   \end{center}
 
   \noindent
+  This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum
+  current precedence of the subtree located at @{text "th\<^sub>r"}. All these
+  subtrees together form the set of threads.
   But the maximum of all threads is the @{term "cp"} of @{text "th"},
-  which is the @{term preced} of @{text th}.
+  which is equal to the @{term preced} of @{text th}.\qed
   \end{proof}
 
+  \endnote{
   @{thm "th_blockedE_pretty"} -- thm-blockedE??
   
+  @{text "th_kept"} shows that th is a thread in s'-s
+  }
 
-  @{text "th_kept"} shows that th is a thread in s'-s
+  Next we show that a running thread @{text "th'"} must either wait for or
+  hold a resource in state @{text s}.
+
+  \begin{lemma}\label{notdetached}
+  If @{term "th' \<in> running (s' @ s)"} then @{term "\<not>detached s th'"}.
+  \end{lemma}
 
-
+  \begin{proof} Let us assume @{text "th'"} is detached in state
+  @{text "s"}, then, according to the definition of detached, @{text
+  "th’"} does not hold or wait for any resource. Hence the @{text
+  cp}-value of @{text "th'"} in @{text s} is not boosted, that is
+  @{term "cp s th' = prec th s"}, and is therefore lower than the
+  precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
+  means @{text "th'"} will not run as long as @{text "th"} is a
+  live thread. In turn this means @{text "th'"} cannot acquire a reseource
+  and is still detached in state @{text "s' @ s"}.  Consequently
+  @{text "th'"} is also not boosted in state @{text "s' @ s"} and
+  would not run. This contradicts our assumption.\qed
+  \end{proof}
 
 
-  \begin{proof}[of Theorem 1]
-  If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us
-  assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread
-  @{text "th'"} that is an acestor of @{text th} in the @{text "RAG"}
-  and @{text "th'"} is running, that is we know
-
-  \begin{center}
-  @{term "th' \<in> nancestors (tG (s' @ s)) th"} \quad and \quad
-  @{term "th' \<in> running (s' @ s)"}
-  \end{center}
-
-  \noindent We have that @{term "th \<noteq> th'"} since we assumed
-  @{text th} is not running.  By Lem.~\ref{thkept}, we know that
-  @{text "th'"} is also running in state @{text s} and by
-  Lem.~\ref{detached} that @{term "\<not>detached s th'"}.
-  By Lem.~\ref{runningpreced} we have
+  \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"},
+  then there is nothing to show. So let us assume otherwise. Since the
+  @{text "RAG"} is well-founded, we know there exists an ancestor of
+  @{text "th"} that is the root of the corrsponding subtree and
+  therefore is ready. Let us call this thread @{text "th'"}. We know
+  that @{text "th'"} has the highest precedence of all ready threads.
+  Therefore it is running.  We have that @{term "th \<noteq> th'"}
+  since we assumed @{text th} is not running.  By
+  Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}.
+  If @{text "th'"} is not detached in @{text s}, that is either
+  holding or waiting for a resource, it must be that @{term "th' \<in>
+  threads s"}.  By Lem.~\ref{runningpreced} we have
 
   \begin{center}
   @{term "cp (t @ s) th' = preced th s"}
   \end{center}
 
   \noindent
-  This concludes the proof of Theorem 1.
+  This concludes the proof of Theorem 1.\qed
   \end{proof}
 
 
-
-
+  \endnote{
   In what follows we will describe properties of PIP that allow us to
   prove Theorem~\ref{mainthm} and, when instructive, briefly describe
   our argument. Recall we want to prove that in state @{term "s' @ s"}
@@ -1143,7 +1163,6 @@
   "th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
   can show that
 
-  
 
   \begin{lemma}
   If @{thm (prem 2) eq_pv_blocked}
@@ -1153,9 +1172,9 @@
   \begin{lemma}
   If @{thm (prem 2) eq_pv_persist}
   then @{thm (concl) eq_pv_persist}
-  \end{lemma}
+  \end{lemma}}
 
-  \subsection*{\bf OUTLINE}
+  \endnote{{\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
@@ -1218,7 +1237,7 @@
   \end{lemma}
   
   explain tRAG
-  \bigskip
+  \bigskip}
 
   
   Suppose the thread @{term th} is \emph{not} running in state @{term
@@ -1272,10 +1291,7 @@
   Using the lemma \ref{runninginversion} we can say more about the thread th'
   \end{corollary}
 
-  \subsection*{END OUTLINE}
-
-
-
+  \endnote{\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. 
@@ -2009,6 +2025,8 @@
 
   \bibliographystyle{plain}
   \bibliography{root}
+
+  \theendnotes
 *}
 
 




