--- a/CpsG.thy	Sat Oct 17 16:14:30 2015 +0800
+++ b/CpsG.thy	Fri Oct 30 20:40:11 2015 +0800
@@ -6,6 +6,9 @@
 imports PrioG Max
 begin
 
+lemma eq_dependants: "dependants (wq s) = dependants s"
+  by (simp add: s_dependants_abv wq_def)
+  
 (* obvious lemma *)
 lemma not_thread_holdents:
   fixes th s
@@ -312,14 +315,14 @@
   qed
 qed
 
-text {* (* ??? *)
+text {* (* ddd *)
 *}
 lemma child_RAG_eq: 
   assumes vt: "vt s"
   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
   by (auto intro: RAG_child[OF vt] child_RAG_p)
 
-text {* (* ??? *)
+text {* (* ddd *)
 *}
 lemma children_no_dep:
   fixes s th th1 th2 th3
@@ -354,7 +357,7 @@
   qed
 qed
 
-text {* (* ??? *)
+text {* (* ddd *)
 *}
 lemma unique_RAG_p:
   assumes vt: "vt s"
@@ -367,7 +370,7 @@
   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 
-text {* (* ??? *)
+text {* (* ddd *)
 *}
 lemma dependants_child_unique:
   fixes s th th1 th2 th3
@@ -405,7 +408,7 @@
   apply (unfold children_def)
   by (metis assms(2) children_def RAG_children eq_RAG)
 
-text {* (* ??? *)
+text {* (* ddd *)
 *}
 lemma dependants_expand:
   assumes "vt s"
@@ -447,7 +450,9 @@
   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
 by auto
 
-text {* (* ??? *)
+text {* (* ddd *)
+  This is the recursive equation used to compute the current precedence of 
+  a thread (the @{text "th"}) here. 
 *}
 lemma cp_rec:
   fixes s th
@@ -514,17 +519,112 @@
   qed
 qed
 
+lemma next_waiting:
+  assumes vt: "vt s"
+  and nxt: "next_th s th cs th'"
+  shows "waiting s th' cs"
+proof -
+  from assms show ?thesis
+    apply (auto simp:next_th_def s_waiting_def[folded wq_def])
+  proof -
+    fix rest
+    assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+      and eq_wq: "wq s cs = th # rest"
+      and ne: "rest \<noteq> []"
+    have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    with ni
+    have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
+      by simp
+    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+    qed
+    ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
+  next
+    fix rest
+    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
+      and ne: "rest \<noteq> []"
+    have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+    qed
+    hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
+      by auto
+    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
+    proof(rule someI2)
+      from wq_distinct[OF vt, of cs] eq_wq
+      show "distinct rest \<and> set rest = set rest" by auto
+    next
+      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+    qed
+    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
+    with eq_wq and wq_distinct[OF vt, of cs]
+    show False by auto
+  qed
+qed
+
 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 
+  obvious facts are derived as lemmas, rather than asserted as axioms.
+*}
+
+text {*
+  However, the lemmas in the forthcoming several locales are no longer 
+  obvious. These lemmas show how the current precedences should be recalculated 
+  after every execution step (in our model, every step is represented by an event, 
+  which in turn, represents a system call, or operation). Each operation is 
+  treated in a separate locale.
+
+  The complication of current precedence recalculation comes 
+  because the changing of RAG needs to be taken into account, 
+  in addition to the changing of precedence. 
+  The reason RAG changing affects current precedence is that,
+  according to the definition, current precedence 
+  of a thread is the maximum of the precedences of its dependants, 
+  where the dependants are defined in terms of RAG.
+
+  Therefore, each operation, lemmas concerning the change of the precedences 
+  and RAG are derived first, so that the lemmas about
+  current precedence recalculation can be based on.
+*}
+
+text {* (* ddd *)
+  The following locale @{text "step_set_cps"} investigates the recalculation 
+  after the @{text "Set"} operation.
+*}
 locale step_set_cps =
   fixes s' th prio s 
-  defines s_def : "s \<equiv> (Set th prio#s')"
+  -- {* @{text "s'"} is the system state before the operation *}
+  -- {* @{text "s"} is the system state after the operation *}
+  defines s_def : "s \<equiv> (Set th prio#s')" 
+  -- {* @{text "s"} is assumed to be a legitimate state, from which
+         the legitimacy of @{text "s"} can be derived. *}
   assumes vt_s: "vt s"
 
 context step_set_cps 
 begin
 
+text {* (* ddd *)
+  The following lemma confirms that @{text "Set"}-operating only changes the precedence 
+  of initiating thread.
+*}
+
 lemma eq_preced:
   fixes th'
   assumes "th' \<noteq> th"
@@ -534,69 +634,115 @@
     by (unfold s_def, auto simp:preced_def)
 qed
 
+text {* (* ddd *)
+  The following lemma assures that the resetting of priority does not change the RAG. 
+*}
+
 lemma eq_dep: "RAG s = RAG s'"
   by (unfold s_def RAG_set_unchanged, auto)
 
+text {*
+  Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation.
+  It says, thread other than the initiating thread @{text "th"} does not need recalculation
+  unless it lies upstream of @{text "th"} in the RAG. 
+
+  The reason behind this lemma is that: 
+  the change of precedence of one thread can only affect it's upstream threads, according to 
+  lemma @{text "eq_preced"}. Since the only thread which might change precedence is
+  @{text "th"}, so only @{text "th"} and its upstream threads need recalculation.
+  (* ccc *)
+*}
+
 lemma eq_cp_pre:
   fixes th' 
   assumes neq_th: "th' \<noteq> th"
   and nd: "th \<notin> dependants s th'"
   shows "cp s th' = cp s' th'"
-  apply (unfold cp_eq_cpreced cpreced_def)
 proof -
-  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"
-    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
-  moreover {
-    fix th1 
-    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"
-    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto
-    hence "preced th1 s = preced th1 s'"
-    proof
-      assume "th1 = th'"
-      with eq_preced[OF neq_th]
-      show "preced th1 s = preced th1 s'" by simp
-    next
-      assume "th1 \<in> dependants (wq s') th'"
-      with nd and eq_dp have "th1 \<noteq> th"
-        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)
-      from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
-    qed
-  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = 
-                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" 
-    by (auto simp:image_def)
-  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
-        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp
+  -- {* This is what we need to prove after expanding the definition of @{text "cp"} *}
+  have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =
+        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"
+   (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))") 
+  proof -
+      -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of 
+            any threads are not changed, this is one of key facts underpinning this 
+            lemma *}
+      have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)
+      have "(?f1 ` ({th'} \<union> ?A)) =  (?f2 ` ({th'} \<union> ?B))"
+      proof(rule image_cong)
+        show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab)
+      next  
+        fix x
+        assume x_in: "x \<in> {th'} \<union> ?B"
+        show "?f1 x = ?f2 x"
+        proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *}
+          from x_in[folded eq_ab, unfolded eq_dependants]
+          have "x \<in> {th'} \<union> dependants s th'" .
+          thus "x \<noteq> th"
+          proof
+            assume "x \<in> {th'}" 
+            with `th' \<noteq> th` show ?thesis by simp
+          next
+            assume "x \<in> dependants s th'"
+            with `th \<notin> dependants s th'` show ?thesis by auto
+          qed 
+        qed 
+      qed
+      thus ?thesis by simp
+  qed 
+  thus ?thesis by (unfold cp_eq_cpreced cpreced_def)
 qed
 
+text {*
+  The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. 
+  The reason for this is that only no-blocked thread can initiate 
+  a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any 
+  critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG.
+  Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}.
+*}
 lemma no_dependants:
-  assumes "th' \<noteq> th"
   shows "th \<notin> dependants s th'"
 proof
-  assume h: "th \<in> dependants s th'"
-  from step_back_step [OF vt_s[unfolded s_def]]
-  have "step s' (Set th prio)" .
-  hence "th \<in> runing s'" by (cases, simp)
-  hence rd_th: "th \<in> readys s'" 
-    by (simp add:readys_def runing_def)
-  from h have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
+  assume "th \<in> dependants s th'"
+  from `th \<in> dependants s th'` have "(Th th, Th th') \<in> (RAG s')\<^sup>+"
     by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)
   from tranclD[OF this]
   obtain z where "(Th th, z) \<in> RAG s'" by auto
-  with rd_th show "False"
+  moreover have "th \<in> readys s'"
+  proof -
+    from step_back_step [OF vt_s[unfolded s_def]]
+    have "step s' (Set th prio)" .
+    hence "th \<in> runing s'" by (cases, simp)
+    thus ?thesis by (simp add:readys_def runing_def)
+  qed
+  ultimately show "False"
     apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
     by (fold wq_def, blast)
 qed
 
 (* Result improved *)
+text {* 
+  A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"}
+  gives the main lemma of this locale, which shows that
+  only the initiating thread needs a recalculation of current precedence.
+*}
 lemma eq_cp:
- fixes th' 
-  assumes neq_th: "th' \<noteq> th"
+  fixes th' 
+  assumes "th' \<noteq> th"
   shows "cp s th' = cp s' th'"
-proof(rule eq_cp_pre [OF neq_th])
-  from no_dependants[OF neq_th] 
-  show "th \<notin> dependants s th'" .
-qed
+  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. 
+
+   The foregoing lemma says only those threads which 
+*}
 lemma eq_up:
   fixes th' th''
   assumes dp1: "th \<in> dependants s th'"
@@ -733,6 +879,20 @@
   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. 
+*}
+
 lemma eq_up_self:
   fixes th' th''
   assumes dp: "th \<in> dependants s th''"
@@ -859,63 +1019,6 @@
 qed
 end
 
-lemma next_waiting:
-  assumes vt: "vt s"
-  and nxt: "next_th s th cs th'"
-  shows "waiting s th' cs"
-proof -
-  from assms show ?thesis
-    apply (auto simp:next_th_def s_waiting_def[folded wq_def])
-  proof -
-    fix rest
-    assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
-      and eq_wq: "wq s cs = th # rest"
-      and ne: "rest \<noteq> []"
-    have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
-    proof(rule someI2)
-      from wq_distinct[OF vt, of cs] eq_wq
-      show "distinct rest \<and> set rest = set rest" by auto
-    next
-      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
-    qed
-    with ni
-    have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"
-      by simp
-    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
-    proof(rule someI2)
-      from wq_distinct[OF vt, of cs] eq_wq
-      show "distinct rest \<and> set rest = set rest" by auto
-    next
-      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
-    qed
-    ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
-  next
-    fix rest
-    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
-      and ne: "rest \<noteq> []"
-    have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
-    proof(rule someI2)
-      from wq_distinct[OF vt, of cs] eq_wq
-      show "distinct rest \<and> set rest = set rest" by auto
-    next
-      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
-    qed
-    hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
-      by auto
-    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" 
-    proof(rule someI2)
-      from wq_distinct[OF vt, of cs] eq_wq
-      show "distinct rest \<and> set rest = set rest" by auto
-    next
-      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
-    qed
-    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
-    with eq_wq and wq_distinct[OF vt, of cs]
-    show False by auto
-  qed
-qed
-
-
 locale step_v_cps =
   fixes s' th cs s 
   defines s_def : "s \<equiv> (V th cs#s')"

--- a/PrioG.thy	Sat Oct 17 16:14:30 2015 +0800
+++ b/PrioG.thy	Fri Oct 30 20:40:11 2015 +0800
@@ -210,7 +210,7 @@
     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 *)
 
-text {* (* ??? *)
+text {* (* ddd *)
   The nature of the work is like this: since it starts from a very simple and basic 
   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.
   For instance, the fact 
@@ -842,7 +842,7 @@
   qed
 qed
 
-text {* (* ??? *) 
+text {* (* ddd *) 
   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed
   with the happening of @{text "V"}-events:
 *}
@@ -1544,7 +1544,7 @@
   ultimately show ?thesis by (simp add:cntCS_def)
 qed 
 
-text {* (* ??? *) \noindent
+text {* (* ddd *) \noindent
   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 
   of one particular thread. 
 *}