--- a/prio/CpsG.thy	Mon Jan 30 09:44:33 2012 +0000
+++ b/prio/CpsG.thy	Wed Feb 01 08:16:00 2012 +0000
@@ -1356,6 +1356,142 @@
 locale step_P_cps_ne =step_P_cps +
   assumes ne: "wq s' cs \<noteq> []"
 
+locale step_P_cps_e =step_P_cps +
+  assumes ee: "wq s' cs = []"
+
+context step_P_cps_e
+begin
+
+lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"
+proof -
+  from ee and  step_depend_p[OF vt_s[unfolded s_def], folded s_def]
+  show ?thesis by auto
+qed
+
+lemma child_kept_left:
+  assumes 
+  "(n1, n2) \<in> (child s')^+"
+  shows "(n1, n2) \<in> (child s)^+"
+proof -
+  from assms show ?thesis 
+  proof(induct rule: converse_trancl_induct)
+    case (base y)
+    from base obtain th1 cs1 th2
+      where h1: "(Th th1, Cs cs1) \<in> depend s'"
+      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)
+    have "cs1 \<noteq> cs"
+    proof
+      assume eq_cs: "cs1 = cs"
+      with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+      with ee show False
+        by (auto simp:s_depend_def cs_waiting_def)
+    qed
+    with h1 h2 depend_s have 
+      h1': "(Th th1, Cs cs1) \<in> depend s" and
+      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+    with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
+    thus ?case by auto
+  next
+    case (step y z)
+    have "(y, z) \<in> child s'" by fact
+    then obtain th1 cs1 th2
+      where h1: "(Th th1, Cs cs1) \<in> depend s'"
+      and h2: "(Cs cs1, Th th2) \<in> depend s'"
+      and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)
+    have "cs1 \<noteq> cs"
+    proof
+      assume eq_cs: "cs1 = cs"
+      with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+      with ee show False 
+        by (auto simp:s_depend_def cs_waiting_def)
+    qed
+    with h1 h2 depend_s have 
+      h1': "(Th th1, Cs cs1) \<in> depend s" and
+      h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+    with eq_y eq_z have "(y, z) \<in> child s" by simp
+    moreover have "(z, n2) \<in> (child s)^+" by fact
+    ultimately show ?case by auto
+  qed
+qed
+
+lemma  child_kept_right:
+  assumes
+  "(n1, n2) \<in> (child s)^+"
+  shows "(n1, n2) \<in> (child s')^+"
+proof -
+  from assms show ?thesis
+  proof(induct)
+    case (base y)
+    from base and depend_s
+    have "(n1, y) \<in> child s'"
+      apply (auto simp:child_def)
+      proof -
+        fix th'
+        assume "(Th th', Cs cs) \<in> depend s'"
+        with ee have "False"
+          by (auto simp:s_depend_def cs_waiting_def)
+        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 
+      qed
+    thus ?case by auto
+  next
+    case (step y z)
+    have "(y, z) \<in> child s" by fact
+    with depend_s have "(y, z) \<in> child s'"
+      apply (auto simp:child_def)
+      proof -
+        fix th'
+        assume "(Th th', Cs cs) \<in> depend s'"
+        with ee have "False"
+          by (auto simp:s_depend_def cs_waiting_def)
+        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto 
+      qed
+    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
+    ultimately show ?case by auto
+  qed
+qed
+
+lemma eq_child: "(child s)^+ = (child s')^+"
+  by (insert child_kept_left child_kept_right, auto)
+
+lemma eq_cp:
+  fixes th' 
+  shows "cp s th' = cp s' th'"
+  apply (unfold cp_eq_cpreced cpreced_def)
+proof -
+  have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+    apply (unfold cs_dependents_def, unfold eq_depend)
+  proof -
+    from eq_child
+    have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
+      by auto
+    with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+    show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+      by simp
+  qed
+  moreover {
+    fix th1 
+    assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+    hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+    hence "preced th1 s = preced th1 s'"
+    proof
+      assume "th1 = th'"
+      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+    next
+      assume "th1 \<in> dependents (wq s') th'"
+      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+    qed
+  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) = 
+                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" 
+    by (auto simp:image_def)
+  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+qed
+
+end
+
 context step_P_cps_ne
 begin
 

--- a/prio/Paper/Paper.thy	Mon Jan 30 09:44:33 2012 +0000
+++ b/prio/Paper/Paper.thy	Wed Feb 01 08:16:00 2012 +0000
@@ -1,9 +1,9 @@
 (*<*)
 theory Paper
-imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
+imports CpsG ExtGG (* "~~/src/HOL/Library/LaTeXsugar" *) LaTeXsugar
 begin
 ML {*
-  Printer.show_question_marks_default := false;
+  show_question_marks_default := false;
   *}
 (*>*)
 
@@ -507,6 +507,193 @@
 end
 (*>*)
 
+subsection {* Event @{text "V th cs"} *}
+
+(*<*)
+context step_v_cps_nt
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "V th cs"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "V th cs"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  Under such a context, we investigated how the current precedence @{term "cp"} of 
+  threads change from state @{term "s'"} to @{term "s"}. 
+
+
+  Two subcases are considerted, 
+  where the first is that there exits @{term "th'"} 
+  such that 
+  @{thm [display] nt} 
+  holds, which means there exists a thread @{term "th'"} to take over
+  the resource release by thread @{term "th"}. 
+  In this sub-case, the following results are obtained:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}: 
+  @{thm [display] "depend_s"}
+  which shows two edges are removed while one is added. These changes imply how
+  the current precedences should be re-computed.
+  \item First all threads different from @{term "th"} and @{term "th'"} have their
+  @{term "cp"}-value kept, therefore do not need a re-computation
+  (@{text "cp_kept"}): @{thm [display] cp_kept}
+  This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}
+  need to be recomputed.
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+
+context step_v_cps_nnt
+begin
+(*>*)
+
+text {*
+  The other sub-case is when for all @{text "th'"}
+  @{thm [display] nnt}
+  holds, no such thread exists. The following results can be obtained for this 
+  sub-case:
+  \begin{enumerate}
+  \item The change of RAG is given by lemma @{text "depend_s"}:
+  @{thm [display] depend_s}
+  which means only one edge is removed.
+  \item In this case, no re-computation is needed (@{text "eq_cp"}):
+  @{thm [display] eq_cp}
+  \end{enumerate}
+  *}
+
+(*<*)
+end
+(*>*)
+
+
+subsection {* Event @{text "P th cs"} *}
+
+(*<*)
+context step_P_cps_e
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "P th cs"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "P th cs"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+
+  This case is further divided into two sub-cases. The first is when @{thm ee} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item No re-computation is needed (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+*}
+
+(*<*)
+end
+
+context step_P_cps_ne
+begin
+(*>*)
+
+text {*
+  The second is when @{thm ne} holds.
+  The following results can be obtained:
+  \begin{enumerate}
+  \item One edge is added to the RAG (@{text "depend_s"}):
+    @{thm [display] depend_s}
+  \item Threads with no dependence relation with @{term "th"} do not need a re-computation
+    of their @{term "cp"}-values (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+    This lemma implies all threads with a dependence relation with @{term "th"} may need 
+    re-computation.
+  \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier
+    (@{text "eq_up"}):
+    @{thm [display] eq_up}
+  \end{enumerate}
+
+  *}
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Create th prio"} *}
+
+(*<*)
+context step_create_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Create th prio"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "Create th prio"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \item The @{term "cp"}-value of @{term "th"} equals its precedence 
+    (@{text "eq_cp_th"}):
+    @{thm [display] eq_cp_th}
+  \end{enumerate}
+
+*}
+
+
+(*<*)
+end
+(*>*)
+
+subsection {* Event @{text "Exit th"} *}
+
+(*<*)
+context step_exit_cps
+begin
+(*>*)
+
+text {*
+  The context under which event @{text "Exit th"} happens is formalized as follows:
+  \begin{enumerate}
+    \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.
+    \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 
+      event @{text "Exit th"} is eligible to happen under state @{term "s'"} and
+      state @{term "s'"} is a valid state.
+  \end{enumerate}
+  The following results can be obtained under this context:
+  \begin{enumerate}
+  \item The RAG does not change (@{text "eq_dep"}):
+    @{thm [display] eq_dep}
+  \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):
+    @{thm [display] eq_cp}
+  \end{enumerate}
+  Since @{term th} does not live in state @{term "s"}, there is no need to compute 
+  its @{term cp}-value.
+*}
+
+(*<*)
+end
+(*>*)
+
+
 section {* Related works \label{related} *}
 
 text {*

Binary file prio/paper.pdf has changed