# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1499436614 -3600
# Node ID 42767f6e0ae90d6b55222392f5ac9e56c5c25b3c
# Parent  5067a2ab555727d2fa75b77a049c772c5e48c44f
updated

diff -r 5067a2ab5557 -r 42767f6e0ae9 Implementation.thy
--- a/Implementation.thy	Mon Jul 03 15:29:29 2017 +0100
+++ b/Implementation.thy	Fri Jul 07 15:10:14 2017 +0100
@@ -396,12 +396,12 @@
   the @{text cp}-values for @{text th} and @{text taker}.
 *}
 
-lemma "taker \<notin> children (tG (e#s)) th"
+lemma t1: "taker \<notin> children (tG (e#s)) th"
   by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp
           subtree_ancestorsI taker_ready_es vat_es.root_readys_tG)
   
 
-lemma "th \<notin> children (tG (e#s)) taker"
+lemma t2: "th \<notin> children (tG (e#s)) taker"
   by (metis children_subtree empty_iff  neq_taker_th root_def 
          subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG)
   
diff -r 5067a2ab5557 -r 42767f6e0ae9 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Jul 03 15:29:29 2017 +0100
+++ b/Journal/Paper.thy	Fri Jul 07 15:10:14 2017 +0100
@@ -1960,8 +1960,9 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
-  @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
+  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s} and 
+  @{term "e#s"} with @{text e} being @{term "V th cs"} are both valid. 
+  We have to consider two
   subcases: one where there is a thread to ``take over'' the released
   resource @{text cs}, and one where there is not. Let us consider them
   in turn. Suppose in state @{text s}, the thread @{text th'} takes over
@@ -1969,8 +1970,8 @@
 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm (concl) valid_trace_v_n.RAG_s}\\
-  %@ {thm RAG_s}
+  %@ { thm (concl) valid_trace_v_n.RAG_s}\\
+  @{term "RAG (e#s) = RAG s - {(C cs,T th), (T th',C cs)} \<union> {(C cs, T th')}"}
   \end{isabelle}
   
   \noindent
@@ -1980,38 +1981,50 @@
   can show
 
   \begin{isabelle}\ \ \ \ \ %%%
-  %@ {thm[mode=IfThen] cp_kept}
+  @{text "If"} @{text "th'' \<noteq> th"} and 
+  @{text "th'' \<noteq> th'"}
+  @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]}
   \end{isabelle}
   
   \noindent
   For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
-  recalculate their current precedence since their children have changed. *}
+  recalculate their current precedence since their children have changed. 
+
+  
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm (concl) valid_trace_v_n.t1}\\
+  @{thm (concl) valid_trace_v_n.t2}
+  \end{isabelle}
+*}
 
 text {*
   \noindent
-  In the other case where there is no thread that takes over @{text cs}, we can show how
+  In the other case where there is no thread that takes over @{text cs}, 
+  we can show how
   to recalculate the @{text RAG} and also show that no current precedence needs
   to be recalculated.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  %@ {thm eq_cp}
+  @{thm (concl) valid_trace_v_e.RAG_s}\\
+  @{thm (concl) valid_trace_v_e.eq_cp}
   \end{tabular}
   \end{isabelle}
   *}
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
-  @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
-  the one where @{text cs} is not locked, and one where it is. We treat the former case
+  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s} and 
+  @{term "e#s"} with @{term "e \<equiv> P th cs"} are both valid. 
+  We again have to analyse two subcases, namely
+  the one where @{text cs} is not locked, and one where it is. We 
+  treat the former case
   first by showing that
   
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  %@ {thm RAG_s}\\
-  HERE %@ {thm eq_cp}
+  @{thm valid_trace_p_h.RAG_es}\\
+  %@ { thm valid_trace_p_h.eq_cp}
   \end{tabular}
   \end{isabelle}
 
diff -r 5067a2ab5557 -r 42767f6e0ae9 journal.pdf
Binary file journal.pdf has changed