--- a/Journal/Paper.thy Fri Apr 15 13:52:07 2016 +0100
+++ b/Journal/Paper.thy Fri Apr 15 14:44:09 2016 +0100
@@ -411,8 +411,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm cs_holding_def[where thread="th"]}\\
- @{thm cs_waiting_def[where thread="th"]}
+ @{thm cs_holding_raw[where thread="th"]}\\
+ @{thm cs_waiting_raw[where thread="th"]}
\end{tabular}
\end{isabelle}
@@ -445,7 +445,7 @@
as the union of the sets of waiting and holding edges, namely
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_RAG_def}
+ @{thm cs_RAG_raw}
\end{isabelle}
@@ -1034,9 +1034,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
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"]}
+ %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\
+ %@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\
+ %@ {thm[mode=IfThen] runing_unique[of _ "th1" "th2"]}
\end{tabular}
\end{isabelle}
@@ -1053,10 +1053,10 @@
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},\\
+ %@ {thm (concl) wf_dep_converse},\\
%\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}
@@ -1135,7 +1135,7 @@
%\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
% @ {thm [display] chain_building[rule_format]}
%\item The ready thread chased to is unique (@{text "dchain_unique"}):
- % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]}
+ % @ {thm [display] dchain_unique[of _ _ "th1" "th2"]}
%\end{enumerate}
%Some deeper results about the system:
@@ -1305,10 +1305,6 @@
kind of events.\smallskip
*}
-(*<*)
-context step_create_cps
-begin
-(*>*)
text {*
\noindent
\colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and
@@ -1318,8 +1314,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
HERE ?? %@ {thm eq_dep},\\
- @{thm eq_cp_th}, and\\
- @{thm[mode=IfThen] eq_cp}
+ @{thm valid_trace_create.eq_cp_th}, and\\
+ @{thm[mode=IfThen] valid_trace_create.eq_cp}
\end{tabular}
\end{isabelle}
@@ -1329,11 +1325,7 @@
thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
\smallskip
*}
-(*<*)
-end
-context step_exit_cps
-begin
-(*>*)
+
text {*
\noindent
\colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and
@@ -1341,8 +1333,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- HERE %@ {thm eq_dep}, and\\
- @{thm[mode=IfThen] eq_cp}
+ HERE %@ {thm valid_trace_create.eq_dep}, and\\
+ @{thm[mode=IfThen] valid_trace_create.eq_cp}
\end{tabular}
\end{isabelle}
@@ -1353,11 +1345,7 @@
current precedence.
\smallskip
*}
-(*<*)
-end
-context step_set_cps
-begin
-(*>*)
+
text {*
\noindent
\colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and
@@ -1365,8 +1353,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm[mode=IfThen] eq_dep}, and\\
- @{thm[mode=IfThen] eq_cp_pre}
+ %@ {thm[mode=IfThen] eq_dep}, and\\
+ %@ {thm[mode=IfThen] valid_trace_create.eq_cp_pre}
\end{tabular}
\end{isabelle}
@@ -1404,11 +1392,7 @@
%have their current precedence changed.
\smallskip
*}
-(*<*)
-end
-context step_v_cps_nt
-begin
-(*>*)
+
text {*
\noindent
\colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and
@@ -1420,7 +1404,7 @@
\begin{isabelle}\ \ \ \ \ %%%
- @{thm RAG_s}
+ %@ {thm RAG_s}
\end{isabelle}
\noindent
@@ -1430,12 +1414,14 @@
can show
\begin{isabelle}\ \ \ \ \ %%%
- @{thm[mode=IfThen] cp_kept}
+ %@ {thm[mode=IfThen] cp_kept}
\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. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
+ recalculate their current precedence since their children have changed. *}
+
+text {*
\noindent
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
@@ -1443,16 +1429,12 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm RAG_s}\\
- @{thm eq_cp}
+ %@ {thm RAG_s}\\
+ %@ {thm eq_cp}
\end{tabular}
\end{isabelle}
*}
-(*<*)
-end
-context step_P_cps_e
-begin
-(*>*)
+
text {*
\noindent
\colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and
@@ -1462,20 +1444,22 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm RAG_s}\\
+ %@ {thm RAG_s}\\
HERE %@ {thm eq_cp}
\end{tabular}
\end{isabelle}
\noindent
This means we need to add a holding edge to the @{text RAG} and no
- current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
+ current precedence needs to be recalculated.*}
+
+text {*
\noindent
In the second case we know that resource @{text cs} is locked. We can show that
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm RAG_s}\\
+ %@ {thm RAG_s}\\
HERE %@ {thm[mode=IfThen] eq_cp}
\end{tabular}
\end{isabelle}
@@ -1505,7 +1489,9 @@
This lemma states that if an intermediate @{term cp}-value does not change, then
the procedure can also stop, because none of its dependent threads will
have their current precedence changed.
- *}(*<*)end(*>*)text {*
+ *}
+
+text {*
As can be seen, a pleasing byproduct of our formalisation is that the properties in
this section closely inform an implementation of PIP, namely whether the
RAG needs to be reconfigured or current precedences need to