
diff -r da27bece9575 -r f9e6c4166476 PIPDefs.thy
--- a/PIPDefs.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/PIPDefs.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory PIPDefs
-imports Precedence_ord Max
+imports Precedence_ord Max RTree
 begin
 (*>*)
 
@@ -187,16 +187,13 @@
       {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
 
 text {*
- 
-  \noindent The following @{text "dependants wq th"} represents the set of
-  threads which are waiting on thread @{text "th"} in Resource Allocation
-  Graph @{text "RAG wq"}. Here, "waiting" means waiting directly or
-  indirectly on the critical resource. *}
-
+  The following notion of {\em Thread Graph}, denoted @{text "tG_raw"}, is
+  the graph derived from @{text "RAG_raw"} by hiding all resource nodes. 
+  It is more concise to use in many contexts.
+*}
 definition
-  dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
-where
-  "dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
+  "tG_raw wq = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. 
+                  \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG_raw wq \<and> (Cs cs, Th th\<^sub>2) \<in> RAG_raw wq}" 
 
 text {* 
 
@@ -204,40 +201,15 @@
   precedence} of thread @{text "th"} under state @{text "s"}. The definition
   of @{text "cpreced"} reflects the basic idea of Priority Inheritance that
   the {\em current precedence} of a thread is the precedence inherited from
-  the maximum of all its dependants, i.e. the threads which are waiting
-  directly or indirectly waiting for some resources from it. If no such
-  thread exits, @{text "th"}'s {\em current precedence} equals its original
-  precedence, i.e. @{text "preced th s"}. *}
+  the maximum precedence of all threads in its sub-tree in @{text RAG} 
+  (or the @{text tG}).
+"}. 
+*}
 
 definition 
   cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
   where 
-  "cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
-
-
-
-text {*
-
-  Notice that the current precedence (@{text "cpreced"}) of one thread
-  @{text "th"} can be boosted (increased) by those threads in the @{text
-  "dependants wq th"}-set. If one thread gets boosted, we say it inherits
-  the priority (or, more precisely, the precedence) of its dependants. This
-  is whrere the word "Inheritance" in Priority Inheritance Protocol comes
-  from. *}
-
-lemma cpreced_def2:
-  "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
-  unfolding cpreced_def image_def
-  apply(rule eq_reflection)
-  apply(rule_tac f="Max" in arg_cong)
-  by (auto)
-
-lemma cpreced_def3:
-  "cpreced wq s th \<equiv> Max (preceds ({th} \<union> dependants_raw wq th) s)"
-  unfolding cpreced_def2 image_def
-  apply(rule eq_reflection)
-  apply(rule_tac f="Max" in arg_cong)
-  by (auto)
+  "cpreced wq s th \<equiv> Max (preceds (subtree (tG_raw wq) th) s)"
   
 definition 
   cpreceds :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread set \<Rightarrow> precedence set"
@@ -381,16 +353,18 @@
         let new_wq = wq(cs := release (wq cs)) in
           (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
 
+
 lemma cpreced_initial: 
   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
-apply(rule ext)
-apply(simp add: cpreced_def)
-apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)
-apply(simp add: preced_def)
-done
+proof -
+  have [simp]: "(RAG_raw all_unlocked) = {}"
+    by (unfold RAG_raw_def, auto simp:waiting_raw_def holding_raw_def)
+  have [simp]: "\<forall> x. (subtree {} x) = {x}"
+    by (unfold subtree_def, auto)
+  show ?thesis by (rule ext, auto simp:cpreced_def tG_raw_def preced_def)
+qed
 
 text {* 
-
   \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
   *}
 
@@ -408,7 +382,7 @@
 text {* 
 
   \noindent Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"}
-  and @{text "dependants"} still have the same meaning, but redefined so
+  and @{text "tG"} still have the same meaning, but redefined so
   that they no longer RAG on the fictitious {\em waiting queue function}
   @{text "wq"}, but on system state @{text "s"}. *}
 
@@ -424,10 +398,6 @@
   s_RAG_abv: 
   "RAG (s::state) \<equiv> RAG_raw (wq s)"
   
-definition
-  s_dependants_abv: 
-  "dependants (s::state) \<equiv> dependants_raw (wq s)"
-
 lemma cp_eq: 
   shows "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
@@ -465,11 +435,6 @@
   "RAG_raw (wq s) = RAG s"
   by (unfold RAG_raw_def s_RAG_def, auto)
 
-
-lemma s_dependants_def: 
-  shows "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG s)^+}"
-using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto
-
 text {*
   
   The following function @{text "readys"} calculates the set of ready
@@ -709,38 +674,25 @@
   tRAG, so that it is easier to understand.
 *}
 
-
-definition "tG s = (map_prod the_thread the_thread) `(tRAG s)"
+definition
+  s_tG_abv: 
+  "tG (s::state) \<equiv> tG_raw (wq s)"
 
 lemma tG_alt_def: 
   "tG s = {(th1, th2) | th1 th2. 
                   \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R")
+  by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp)
+
+lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" 
+  by (unfold tRAG_alt_def tG_alt_def, auto)
+
+lemma tG_def_tRAG: "tG s = map_prod the_thread the_thread ` tRAG s"
 proof -
-  { fix th1 th2
-    assume "(th1, th2) \<in> ?L" 
-    hence "(th1, th2) \<in> ?R" by (auto simp:tG_def tRAG_alt_def)
-  } moreover {
-    fix th1 th2
-    assume "(th1, th2) \<in> ?R"
-    then obtain cs where "(Th th1, Cs cs) \<in> RAG s" "(Cs cs, Th th2) \<in> RAG s" by auto
-    hence "(Th th1, Th th2) \<in> (wRAG s O hRAG s)" by (auto simp:RAG_split wRAG_def hRAG_def)
-    hence "(Th th1, Th th2) \<in> tRAG s" by (unfold tRAG_def, simp)
-    hence "(th1, th2) \<in> ?L" by (simp add: tG_def rev_image_eqI)
-  } ultimately show ?thesis by (meson pred_equals_eq2)
+  have [simp]: "(map_prod the_thread the_thread \<circ> map_prod Th Th) = id"
+    by (rule ext, auto)
+  show ?thesis by (unfold tRAG_def_tG image_comp, simp)
 qed
 
-lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" (is "?L = ?R")
-proof -
-  have "?L = (\<lambda> x. x) ` ?L" by simp
-  also have "... = ?R"
-  proof(unfold tG_def image_comp, induct rule:image_cong)
-    case (2 e)
-    thus ?case by (unfold tRAG_alt_def, auto)
-  qed auto
-  finally show ?thesis .
-qed
-
-
 fun actor  where
   "actor (Exit th) = th" |
   "actor (P th cs) = th" |




