
diff -r b85cfbd58f59 -r 0fd478e14e87 CpsG.thy
--- a/CpsG.thy	Fri Oct 30 20:40:11 2015 +0800
+++ b/CpsG.thy	Thu Dec 03 14:34:00 2015 +0800
@@ -3,9 +3,47 @@
   after every system call (or system operation)
 *}
 theory CpsG
-imports PrioG Max
+imports PrioG Max RTree
+begin
+
+locale pip = 
+  fixes s
+  assumes vt: "vt s"
+
+context pip
 begin
 
+interpretation rtree_RAG: rtree "RAG s"
+proof
+  show "single_valued (RAG s)"
+  apply (intro_locales)
+    by (unfold single_valued_def, auto intro: unique_RAG[OF vt])
+
+  show "acyclic (RAG s)"
+     by (rule acyclic_RAG[OF vt])
+qed
+
+end
+
+
+
+definition "the_preced s th = preced th s"
+
+lemma cp_alt_def:
+  "cp s th =  
+           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+proof -
+  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
+        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
+          (is "Max (_ ` ?L) = Max (_ ` ?R)")
+  proof -
+    have "?L = ?R" 
+    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
+    thus ?thesis by simp
+  qed
+  thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
+qed
+
 lemma eq_dependants: "dependants (wq s) = dependants s"
   by (simp add: s_dependants_abv wq_def)
   
@@ -575,9 +613,11 @@
   qed
 qed
 
+-- {* A useless definition *}
 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
+
 text {* (* ddd *)
   One beauty of our modelling is that we follow the definitional extension tradition of HOL.
   The benefit of such a concise and miniature model is that  large number of intuitively 
@@ -620,6 +660,27 @@
 context step_set_cps 
 begin
 
+interpretation rtree_RAGs: rtree "RAG s"
+proof
+  show "single_valued (RAG s)"
+  apply (intro_locales)
+    by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
+
+  show "acyclic (RAG s)"
+     by (rule acyclic_RAG[OF vt_s])
+qed
+
+interpretation rtree_RAGs': rtree "RAG s'"
+proof
+  show "single_valued (RAG s')"
+  apply (intro_locales)
+    by (unfold single_valued_def, 
+        auto intro: unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+
+  show "acyclic (RAG s')"
+     by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+qed
+
 text {* (* ddd *)
   The following lemma confirms that @{text "Set"}-operating only changes the precedence 
   of initiating thread.
@@ -732,305 +793,73 @@
   shows "cp s th' = cp s' th'"
   by (rule eq_cp_pre[OF assms no_dependants])
 
-
-text {* (* ddd *) \noindent
-   The following @{text "eq_up"} was originally designed to save the recalculations
-   of current precedence going upstream from thread @{text "th"} can stop earlier. 
-   If at a certain point along way, the recalculation results in the same
-   result, the recalculation can stop there. 
-   This lemma is obsolete because we found that @{text "th"} is not contained in 
-   any thread's dependants set. 
+end
 
-   The foregoing lemma says only those threads which 
-*}
-lemma eq_up:
-  fixes th' th''
-  assumes dp1: "th \<in> dependants s th'"
-  and dp2: "th' \<in> dependants s th''"
-  and eq_cps: "cp s th' = cp s' th'"
-  shows "cp s th'' = cp s' th''"
-proof -
-  from dp2
-  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
-  from RAG_child[OF vt_s this[unfolded eq_RAG]]
-  have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
-  moreover { fix n th''
-    have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
-                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
-    proof(erule trancl_induct, auto)
-      fix y th''
-      assume y_ch: "(y, Th th'') \<in> child s"
-        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
-        and ch': "(Th th', y) \<in> (child s)\<^sup>+"
-      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
-      with ih have eq_cpy:"cp s thy = cp s' thy" by blast
-      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
-      moreover from child_RAG_p[OF ch'] and eq_y
-      have "(Th th', Th thy) \<in> (RAG s)^+" by simp
-      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
-      show "cp s th'' = cp s' th''"
-        apply (subst cp_rec[OF vt_s])
-      proof -
-        have "preced th'' s = preced th'' s'"
-        proof(rule eq_preced)
-          show "th'' \<noteq> th"
-          proof
-            assume "th'' = th"
-            with dp_thy y_ch[unfolded eq_y] 
-            have "(Th th, Th th) \<in> (RAG s)^+"
-              by (auto simp:child_def)
-            with wf_trancl[OF wf_RAG[OF vt_s]] 
-            show False by auto
-          qed
-        qed
-        moreover { 
-          fix th1
-          assume th1_in: "th1 \<in> children s th''"
-          have "cp s th1 = cp s' th1"
-          proof(cases "th1 = thy")
-            case True
-            with eq_cpy show ?thesis by simp
-          next
-            case False
-            have neq_th1: "th1 \<noteq> th"
-            proof
-              assume eq_th1: "th1 = th"
-              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
-              from children_no_dep[OF vt_s _ _ this] and 
-              th1_in y_ch eq_y show False by (auto simp:children_def)
-            qed
-            have "th \<notin> dependants s th1"
-            proof
-              assume h:"th \<in> dependants s th1"
-              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
-              from dependants_child_unique[OF vt_s _ _ h this]
-              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
-              with False show False by auto
-            qed
-            from eq_cp_pre[OF neq_th1 this]
-            show ?thesis .
-          qed
-        }
-        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
-          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
-        moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
-        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
-          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
-      qed
-    next
-      fix th''
-      assume dp': "(Th th', Th th'') \<in> child s"
-      show "cp s th'' = cp s' th''"
-        apply (subst cp_rec[OF vt_s])
-      proof -
-        have "preced th'' s = preced th'' s'"
-        proof(rule eq_preced)
-          show "th'' \<noteq> th"
-          proof
-            assume "th'' = th"
-            with dp1 dp'
-            have "(Th th, Th th) \<in> (RAG s)^+"
-              by (auto simp:child_def s_dependants_def eq_RAG)
-            with wf_trancl[OF wf_RAG[OF vt_s]] 
-            show False by auto
-          qed
-        qed
-        moreover { 
-          fix th1
-          assume th1_in: "th1 \<in> children s th''"
-          have "cp s th1 = cp s' th1"
-          proof(cases "th1 = th'")
-            case True
-            with eq_cps show ?thesis by simp
-          next
-            case False
-            have neq_th1: "th1 \<noteq> th"
-            proof
-              assume eq_th1: "th1 = th"
-              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
-                by (auto simp:s_dependants_def eq_RAG)
-              from children_no_dep[OF vt_s _ _ this]
-              th1_in dp'
-              show False by (auto simp:children_def)
-            qed
-            thus ?thesis
-            proof(rule eq_cp_pre)
-              show "th \<notin> dependants s th1"
-              proof
-                assume "th \<in> dependants s th1"
-                from dependants_child_unique[OF vt_s _ _ this dp1]
-                th1_in dp' have "th1 = th'"
-                  by (auto simp:children_def)
-                with False show False by auto
-              qed
-            qed
-          qed
-        }
-        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
-          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
-        moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
-        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
-          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
-      qed     
-    qed
-  }
-  ultimately show ?thesis by auto
-qed
-
-text {* (* ddd *)
-  For those @{text "th''"},  @{text "th \<in> dependants s th''"} means that 
-  the current precedence of such @{text "th''"} might possibly be boosted if the 
-  current precedence of @{text "th"} somehow get raised. The following lemma
-  says that if the resetting of its own priority by thread @{text "th"} does not
-  change its current precedence, then the current precedence of such @{text "th''"}
-  will remain unchanged. The situation such that @{text "th"}'s current 
-  precedence does not change with the resetting of its priority might happen in many
-  different cases. For example, if the current precedence of @{text "th"} is already an inherited one,
-  the lowering of its priority will not change its current precedence, and the increasing 
-  of its priority will not change its current precedence neither, if 
-  incidental rising of its own precedence is not large enough to surpass the inherited precedence. 
+text {*
+  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
 *}
 
-lemma eq_up_self:
-  fixes th' th''
-  assumes dp: "th \<in> dependants s th''"
-  and eq_cps: "cp s th = cp s' th"
-  shows "cp s th'' = cp s' th''"
-proof -
-  from dp
-  have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
-  from RAG_child[OF vt_s this[unfolded eq_RAG]]
-  have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
-  moreover { fix n th''
-    have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
-                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
-    proof(erule trancl_induct, auto)
-      fix y th''
-      assume y_ch: "(y, Th th'') \<in> child s"
-        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
-        and ch': "(Th th, y) \<in> (child s)\<^sup>+"
-      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
-      with ih have eq_cpy:"cp s thy = cp s' thy" by blast
-      from child_RAG_p[OF ch'] and eq_y
-      have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
-      show "cp s th'' = cp s' th''"
-        apply (subst cp_rec[OF vt_s])
-      proof -
-        have "preced th'' s = preced th'' s'"
-        proof(rule eq_preced)
-          show "th'' \<noteq> th"
-          proof
-            assume "th'' = th"
-            with dp_thy y_ch[unfolded eq_y] 
-            have "(Th th, Th th) \<in> (RAG s)^+"
-              by (auto simp:child_def)
-            with wf_trancl[OF wf_RAG[OF vt_s]] 
-            show False by auto
-          qed
-        qed
-        moreover { 
-          fix th1
-          assume th1_in: "th1 \<in> children s th''"
-          have "cp s th1 = cp s' th1"
-          proof(cases "th1 = thy")
-            case True
-            with eq_cpy show ?thesis by simp
-          next
-            case False
-            have neq_th1: "th1 \<noteq> th"
-            proof
-              assume eq_th1: "th1 = th"
-              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
-              from children_no_dep[OF vt_s _ _ this] and 
-              th1_in y_ch eq_y show False by (auto simp:children_def)
-            qed
-            have "th \<notin> dependants s th1"
-            proof
-              assume h:"th \<in> dependants s th1"
-              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
-              from dependants_child_unique[OF vt_s _ _ h this]
-              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
-              with False show False by auto
-            qed
-            from eq_cp_pre[OF neq_th1 this]
-            show ?thesis .
-          qed
-        }
-        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
-          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
-        moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
-        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
-          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
-      qed
-    next
-      fix th''
-      assume dp': "(Th th, Th th'') \<in> child s"
-      show "cp s th'' = cp s' th''"
-        apply (subst cp_rec[OF vt_s])
-      proof -
-        have "preced th'' s = preced th'' s'"
-        proof(rule eq_preced)
-          show "th'' \<noteq> th"
-          proof
-            assume "th'' = th"
-            with dp dp'
-            have "(Th th, Th th) \<in> (RAG s)^+"
-              by (auto simp:child_def s_dependants_def eq_RAG)
-            with wf_trancl[OF wf_RAG[OF vt_s]] 
-            show False by auto
-          qed
-        qed
-        moreover { 
-          fix th1
-          assume th1_in: "th1 \<in> children s th''"
-          have "cp s th1 = cp s' th1"
-          proof(cases "th1 = th")
-            case True
-            with eq_cps show ?thesis by simp
-          next
-            case False
-            assume neq_th1: "th1 \<noteq> th"
-            thus ?thesis
-            proof(rule eq_cp_pre)
-              show "th \<notin> dependants s th1"
-              proof
-                assume "th \<in> dependants s th1"
-                hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
-                from children_no_dep[OF vt_s _ _ this]
-                and th1_in dp' show False
-                  by (auto simp:children_def)
-              qed
-            qed
-          qed
-        }
-        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
-          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
-        moreover have "children s th'' = children s' th''"
-          by (unfold children_def child_def s_def RAG_set_unchanged, simp)
-        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
-          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
-      qed     
-    qed
-  }
-  ultimately show ?thesis by auto
-qed
-end
-
 locale step_v_cps =
-  fixes s' th cs s 
-  defines s_def : "s \<equiv> (V th cs#s')"
+  -- {* @{text "th"} is the initiating thread *}
+  -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}
+  fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}
+  defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
+  -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
   assumes vt_s: "vt s"
 
+text {*
+  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
+  which represents the case when there is another thread @{text "th'"}
+  to take over the critical resource released by the initiating thread @{text "th"}.
+*}
 locale step_v_cps_nt = step_v_cps +
   fixes th'
-  assumes nt: "next_th s' th cs th'"
+  -- {* @{text "th'"} is assumed to take over @{text "cs"} *}
+  assumes nt: "next_th s' th cs th'" 
 
 context step_v_cps_nt
 begin
 
+text {*
+  Lemma @{text "RAG_s"} confirms the change of RAG:
+  two edges removed and one added, as shown by the following diagram.
+*}
+
+(*
+  RAG before the V-operation
+    th1 ----|
+            |
+    th' ----|
+            |----> cs -----|
+    th2 ----|              |
+            |              |
+    th3 ----|              |
+                           |------> th
+    th4 ----|              |
+            |              |
+    th5 ----|              |
+            |----> cs'-----|
+    th6 ----|
+            |
+    th7 ----|
+
+ RAG after the V-operation
+    th1 ----|
+            |
+            |----> cs ----> th'
+    th2 ----|              
+            |              
+    th3 ----|              
+                           
+    th4 ----|              
+            |              
+    th5 ----|              
+            |----> cs'----> th
+    th6 ----|
+            |
+    th7 ----|
+*)
+
 lemma RAG_s:
   "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
                                          {(Cs cs, Th th')}"
@@ -1039,12 +868,16 @@
     and nt show ?thesis  by (auto intro:next_th_unique)
 qed
 
+text {*
+  Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}
+  have their dependants changed.
+*}
 lemma dependants_kept:
   fixes th''
   assumes neq1: "th'' \<noteq> th"
   and neq2: "th'' \<noteq> th'"
   shows "dependants (wq s) th'' = dependants (wq s') th''"
-proof(auto)
+proof(auto) (* ccc *)
   fix x
   assume "x \<in> dependants (wq s) th''"
   hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
@@ -1529,6 +1362,7 @@
   show ?thesis by (simp add:s_def)
 qed
 
+
 lemma eq_child_left:
   assumes nd: "(Th th, Th th') \<notin> (child s)^+"
   shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"




