--- a/Correctness.thy	Fri Oct 21 14:47:01 2016 +0100
+++ b/Correctness.thy	Fri Dec 09 12:51:29 2016 +0000
@@ -736,87 +736,6 @@
   running thread is exactly @{term "th'"}. *}
 
 
-(*
-lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-  assumes "th \<notin> running (t @ s)"
-  obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
-                    "th' \<in> running (t @ s)"
-proof -
-  -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either 
-        @{term "th"} is in @{term "readys"} or there is path leading from it to 
-        one thread in @{term "readys"}. *}
-  have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (th, th') \<in> (tG (t @ s))\<^sup>+)" 
-    using th_kept vat_t.th_chain_to_ready_tG by blast
-  
-  -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
-       @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *}
-  moreover have "th \<notin> readys (t @ s)" 
-    using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 
-  
-  -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
-        term @{term readys}: *}
-  ultimately obtain th' where th'_readys: "th' \<in> readys (t @ s)"
-                          and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
-
-  -- {* @{text "th'"} is an ancestor of @{term "th"} *}
-  have "th' \<in> ancestors (tG (t @ s)) th" using dp
-    unfolding ancestors_def by simp
-
-  moreover
-  -- {* We are going to show that this @{term th'} is running. *}
-  have "th' \<in> running (t @ s)"
-  proof -
-    -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
-    have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")
-    proof -
-      -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
-            the  @{term cp}-value of @{term th'} is the maximum of 
-            all precedences of all thread nodes in its @{term tRAG}-subtree: *}
-      
-      have "?L =  Max (preceds (subtree (tG (t @ s)) th') (t @ s))"
-            unfolding cp_alt_def2 image_def the_preced_def by meson 
-      also have "... = (preced th (t @ s))"
-      thm subset_Max
-      thm preced_unique
-      proof(rule subset_Max[where ?A="preceds (threads (t @ s)) (t @ s)"])
-        show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
-      next
-        have "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
-          using readys_def th'_readys vat_t.subtree_tG_thread by auto 
-        then show "preceds (subtree (tG (t @ s)) th') (t @ s) \<subseteq> preceds (threads (t @ s)) (t @ s)"
-          by auto
-      next
-        have "th \<in> subtree (tG (t @ s)) th'"
-          by (simp add: dp subtree_def trancl_into_rtrancl)   
-        then show " preced th (t @ s) \<in> preceds (subtree (tG (t @ s)) th') (t @ s)"
-          by blast
-      next
-        have "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
-          apply(simp only: the_preced_def)
-          by simp 
-        show "Max (preceds (threads (t @ s)) (t @ s)) = preced th (t @ s)"
-          thm th_kept max_kept
-          apply(simp del: th_kept)
-          apply(simp only: the_preced_def image_def)
-          apply(simp add: Bex_def_raw)
-          
-      qed
-      also have "... = ?R"
-        using th_cp_max th_cp_preced th_kept 
-              the_preced_def vat_t.max_cp_readys_threads by auto
-      finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
-    qed 
-
-    -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 
-          it is @{term running} by definition. *}
-    then show "th' \<in> running (t @ s)" using th'_readys 
-      unfolding running_def by simp
-  qed
-
-  ultimately show ?thesis using that by metis
-qed
-*)
-
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"
                     "th' \<in> running (t @ s)"

--- 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
 *}
 
 

--- a/Journal/document/root.tex	Fri Oct 21 14:47:01 2016 +0100
+++ b/Journal/document/root.tex	Fri Dec 09 12:51:29 2016 +0000
@@ -18,6 +18,7 @@
 \usepackage{url}
 \usepackage{color}
 \usepackage{courier}
+\usepackage{endnotes}
 \usetikzlibrary{patterns}
 \usepackage{listings}
 \lstset{language=C,

--- a/PIPBasics.thy	Fri Oct 21 14:47:01 2016 +0100
+++ b/PIPBasics.thy	Fri Dec 09 12:51:29 2016 +0000
@@ -3784,14 +3784,14 @@
     unfolding threads_alt_def1 by simp
   also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"
     apply(subst Max_Segments[symmetric])
-    prefer 5  
+    apply (simp add: finite_readys)
+    apply (simp add: fsbttGs.finite_subtree)
+    apply blast
+    using False apply blast
     apply(rule arg_cong)
     back
     apply(blast)
-    apply (simp add: finite_readys)
-    apply (simp add: fsbttGs.finite_subtree)
-    apply blast
-    using False by blast
+    done 
   also have "... = Max {cp s th | th. th \<in> readys s}"
     unfolding cp_alt_def3 ..
   finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"

Binary file journal.pdf has changed