updated
authorChristian Urban <urbanc@in.tum.de>
Tue, 27 Jun 2017 14:49:42 +0100
changeset 179 f9e6c4166476
parent 178 da27bece9575
child 180 cfd17cb339d1
updated
Correctness.thy
Implementation.thy
Journal/Paper.thy
PIPBasics.thy
PIPDefs.thy
journal.pdf
--- a/Correctness.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Correctness.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -2,6 +2,8 @@
 imports PIPBasics
 begin
 
+(* hg cat -r 176 Correctness.thy *)
+
 lemma actions_of_len_cons [iff]: 
     "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1"
       by  (unfold actions_of_def, simp)
@@ -521,21 +523,27 @@
   @{term "P"}-count equals its @{term "V"}-count (which means it no
   longer has any resource in its possession), it cannot be a running
   thread.
+  
+  (* eee *)
+  The proof is by contradiction:
+  If @{text th'} is running, it can be derived that @{text "th' = th"} which 
+  is in contradiction with the assume @{text "th' \<noteq> th"}.
 
-  The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
-  The key is the use of @{thm eq_pv_dependants} to derive the
-  emptiness of @{text th'}s @{term dependants}-set from the balance of
-  its @{term P} and @{term V} counts.  From this, it can be shown
-  @{text th'}s @{term cp}-value equals to its own precedence.
+  The derivation of @{text "th' = th"} uses @{thm preced_unique}, according to which
+  we need to show the @{text th'} and @{text th} have the same precedence. The proof
+  of this is based on the combination of the following two facts:
 
-  On the other hand, since @{text th'} is running, by @{thm
-  running_preced_inversion}, its @{term cp}-value equals to the
-  precedence of @{term th}.
+  From @{thm vat_t.detached_intro} and assume 
+  @{text "cntP (t@s) th' = cntV (t@s) th'"} it can be derived that 
+  @{text th'} is detached. From this and @{thm detached_cp_preced}
+  it following the precedence of @{text th'} equals to its own @{text cp}-value.
 
-  Combining the above two resukts we have that @{text th'} and @{term
-  th} have the same precedence. By uniqueness of precedences, we have
-  @{text "th' = th"}, which is in contradiction with the assumption
-  @{text "th' \<noteq> th"}.
+  Since @{text th'} is running, from this and @{thm
+  running_preced_inversion}, the precedence of @{text th'} equals to
+  the precedence of @{term th}.
+
+  By combining the above two results we have that @{text th'} and @{term
+  th} have the same precedence. 
 
 *} 
                       
@@ -567,7 +575,6 @@
               its @{term cp}-value equals @{term "preced th s"}, 
               which equals to @{term "?R"} by simplification: *}
         also have "... = ?R" 
-        thm running_preced_inversion
             using running_preced_inversion[OF otherwise] by simp
         finally show ?thesis .
       qed
@@ -1689,5 +1696,4 @@
 
 end
 
-
 end
--- a/Implementation.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Implementation.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -7,7 +7,7 @@
   The use of dependants has been abandoned. Through a series of lemma 
   named xxx_alt_def, lemma originally expressed using dependants 
   is now expressed in terms of RAG, tRAG and tG.
-*)
+*)                                            
 
 text {*
 
@@ -863,7 +863,7 @@
   by (unfold tRAG_alt_def RAG_es, auto)
 
 lemma tG_kept: "tG (e#s) = tG s"
-  by (unfold tG_def tRAG_kept, simp)
+  by (unfold tG_def_tRAG tRAG_kept, simp)
 
 text {*
   The following lemma shows that @{text th} is completely isolated 
@@ -971,7 +971,7 @@
   Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.
 *}
 lemma tG_kept: "tG (e#s) = tG s"
-  by (unfold tG_def tRAG_kept, simp)
+  by (unfold tG_def_tRAG tRAG_kept, simp)
 
 lemma th_RAG: "Th th \<notin> Field (RAG s)"
 proof -
@@ -1016,7 +1016,7 @@
   shows "cp (e#s) th' = cp s th'"
 proof -
   have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
-        (the_preced s ` subtree (tG s) th')"
+          (the_preced s ` subtree (tG s) th')"
   proof -
     { fix a
       assume "a \<in> subtree (tG s) th'"
--- a/Journal/Paper.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Journal/Paper.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -36,8 +36,8 @@
   holding ("holds") and
   waiting_raw ("waits") and
   waiting ("waits") and
-  dependants_raw ("dependants") and
-  dependants ("dependants") and
+  tG_raw ("TDG") and
+  tG ("TDG") and
   RAG_raw ("RAG") and
   RAG ("RAG") and
   Th ("T") and
@@ -459,8 +459,8 @@
   %
   %\begin{isabelle}\ \ \ \ \ %%%
   %\mbox{\begin{tabular}{@ {}l}
-  %@{thm cntP_def}\\
-  %@{thm cntV_def}
+  %@ {thm cntP_def}\\
+  %@ {thm cntV_def}
   %\end{tabular}}
   %\end{isabelle}
   % 
@@ -623,24 +623,26 @@
   finite, we can always start at a thread waiting for a resource and
   ``chase'' outgoing arrows leading to a single root of a tree.
   
-  The use of relations for representing RAGs allows us to conveniently define
-  the notion of the \emph{dependants} of a thread
+  The use of relations for representing @{text RAG}s allows us to conveniently define
+  the \emph{thread dependants graph} 
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm dependants_raw_def}\hfill\numbered{dependants}
+  @{thm tG_raw_def}\\
+  \mbox{}\hfill\numbered{dependants}
   \end{isabelle}
 
-  \noindent This definition needs to account for all threads that wait
-  for a thread to release a resource. This means we need to include
-  threads that transitively wait for a resource to be released (in the
-  picture above this means the dependants of @{text "th\<^sub>0"} are
-  @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
-  resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
-  cannot make any progress unless @{text "th\<^sub>2"} makes progress,
-  which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
-  there is a circle of dependencies in a RAG, then clearly we have a
+  \noindent This definition represents all threads in a @{text RAG} that wait
+  for a thread to release a resource, but the resource is ``hidden''. 
+  In the
+  picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with
+  @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
+  resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
+  cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
+  Similarly for the other threads.
+  If
+  there is a circle of dependencies in a @{text RAG} (and thus @{text TDG}), then clearly we have a
   deadlock. Therefore when a thread requests a resource, we must
-  ensure that the resulting RAG is not circular. In practice, the
+  ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
   programmer has to ensure this. Our model will enforce that critical 
   resources can only be requested provided no circularity can arise.
 
@@ -648,19 +650,20 @@
   state @{text s}. It is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def3}\hfill\numbered{cpreced}
+  @{thm cpreced_def}
+  \hfill\numbered{cpreced}
   \end{isabelle}
 
-   \noindent where the dependants of @{text th} are given by the
-  waiting queue function.  While the precedence @{term prec} of any
+   \noindent 
+  While the precedence @{term prec} of any
   thread is determined statically (for example when the thread is
   created), the point of the current precedence is to dynamically
   increase this precedence, if needed according to PIP. Therefore the
   current precedence of @{text th} is given as the maximum of the
   precedence of @{text th} \emph{and} all threads that are dependants
-  of @{text th} in the state @{text s}. Since the notion @{term
-  "dependants"} is defined as the transitive closure of all dependent
-  threads, we deal correctly with the problem in the informal
+  of @{text th} in the state @{text s}. Since the notion of current precedence is defined as the 
+  transitive closure of the dependent
+  threads in the @{text TDG}, we deal correctly with the problem in the informal
   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
   lowered prematurely (see Introduction). We again introduce an abbreviation for current
   precedeces of a set of threads, written @{text "cprecs wq s ths"}.
@@ -781,27 +784,31 @@
 
   Having the scheduler function @{term schs} at our disposal, we can
   ``lift'', or overload, the notions @{term waiting}, @{term holding},
-  @{term RAG}, @{term dependants} and @{term cp} to operate on states
-  only.
+  @{term RAG}, %%@ {term dependants} 
+  and @{term cp} to operate on states only.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
   @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\
   @{thm (lhs) s_waiting_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv[simplified wq_def]}\\
   @{thm (lhs) s_RAG_abv}      & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv[simplified wq_def]}\\
-  @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv[simplified wq_def]}\\
+  @{thm (lhs) s_tG_abv}& @{text "\<equiv>"} & @{thm (rhs) s_tG_abv[simplified wq_def]}\\
   @{thm (lhs) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\  
   \end{tabular}
   \end{isabelle}
 
   \noindent
   With these abbreviations in place we can derive for every valid trace @{text s} 
-  the following two facts about  @{term dependants} and @{term cprec} (see \eqref{dependants} 
-  and \eqref{cpreced}): Given @{thm (prem 1) valid_trace.cp_alt_def}, then 
+  the following two facts about  ???????
+  %@ {term dependants} 
+  and @{term cprec} (see \eqref{dependants} 
+  and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def}, 
+  then 
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
-  @{thm (concl) valid_trace.cp_alt_def3}\\
+  @{thm tG_alt_def}\\
+  @{thm cp_s_def}\\
   \end{tabular}\hfill\numbered{overloaded}
   \end{isabelle}
 
@@ -1839,11 +1846,11 @@
 
   \begin{center}
   @{thm tG_alt_def}\\
-  @{thm dependants_alt_tG} 
+  ???? %@ {thm dependants_alt_tG} 
   \end{center}
 
   \begin{center}
-  @{thm valid_trace.cp_alt_def3} 
+  ???? %@ {thm valid_trace.cp_alt_def3} 
   \end{center}
 
 
--- a/PIPBasics.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/PIPBasics.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -396,25 +396,17 @@
   show ?thesis using that by auto
 qed
 
+
 lemma trancl_tG_tRAG:
   assumes "(th1, th2) \<in> (tG s)^+"
   shows "(Th th1, Th th2) \<in> (tRAG s)^+"
-proof -
-  have "inj_on the_thread (Field (tRAG s))"
-    by (unfold inj_on_def Field_def tRAG_alt_def, auto)
-  from map_prod_tranclE[OF assms[unfolded tG_def] this]
-  obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"
-    by auto
-  hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)
-  from this[unfolded trancl_domain trancl_range]
-  have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" 
-    by (unfold Field_def, auto)
-  then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"
-    by (auto elim!:Field_tRAGE)
-  with h have "th1' = th1" "th2' = th2" by (auto)
-  from h(3)[unfolded h' this]
-  show ?thesis by (auto simp:ancestors_def)
-qed
+  using assms unfolding tRAG_def_tG
+proof(induct rule:trancl_induct)
+  case (step y z)
+  from step(2) have "(Th y, Th z) \<in> map_prod Th Th ` (tG s)" by auto
+  with step(3)
+  show ?case by auto
+qed auto
 
 lemma rtrancl_tG_tRAG:
   assumes "(th1, th2) \<in> (tG s)^*"
@@ -706,24 +698,14 @@
   (and specifically {\em relational tree} and {\em relational forest})
   are in place.
 *}
+
+lemma cp_s_def: "cp s th = Max (preceds (subtree (tG s) th) s)"
+  by (unfold cp_eq cpreced_def s_tG_abv, simp)
+
 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 s th)) =
-        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
-          (is "Max (_ ` ?L) = Max (_ ` ?R)")
-  proof -
-    have "?L = ?R" 
-    unfolding subtree_def
-    apply(auto)
-    apply (simp add: s_RAG_abv s_dependants_def wq_def)
-    by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def)
-    thus ?thesis by simp
-  qed
-  thus ?thesis
-  by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq 
-      s_dependants_abv the_preced_def)
-qed
+  apply (unfold cp_s_def subtree_tG_tRAG threads_set_eq)
+  by (smt Collect_cong Setcompr_eq_image the_preced_def)
 
 text {*
   The following is another definition of @{term cp}.
@@ -803,56 +785,6 @@
   } ultimately show ?thesis by auto
 qed
 
-text {* 
-  The following lemmas gives an alternative definition @{term dependants}
-  in terms of @{term tRAG}.
-*}
-
-lemma dependants_alt_def:
-  "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
-  by (metis eq_RAG s_dependants_def tRAG_trancl_eq)
-
-text {* 
-  The following lemmas gives another alternative definition @{term dependants}
-  in terms of @{term RAG}.
-*}
-
-lemma dependants_alt_def1:
-  "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
-  using dependants_alt_def tRAG_trancl_eq by auto
-
-text {*
-  Another definition of dependants based on @{term tG}:
-*}
-lemma dependants_alt_tG:
-  "dependants s th = {th'. (th', th) \<in> (tG s)^+}" (is "?L = ?R")
-proof -
-  have "?L = {th'. (Th th', Th th) \<in> (tRAG s)\<^sup>+}"
-    by (unfold dependants_alt_def, simp)
-  also have "... = ?R" (is "?LL = ?RR")
-  proof -
-    { fix th'
-      assume "th' \<in> ?LL"
-      hence "(Th th', Th th) \<in> (tRAG s)\<^sup>+" by simp
-      from trancl_tRAG_tG[OF this]
-      have "th' \<in> ?RR" by auto
-    } moreover {
-      fix th'
-      assume "th' \<in> ?RR"
-      hence "(th', th) \<in> (tG s)\<^sup>+" by simp
-      from trancl_tG_tRAG[OF this]
-      have "th' \<in> ?LL" by auto
-    } ultimately show ?thesis by auto
-  qed
-  finally show ?thesis .
-qed
-
-lemma dependants_alt_def_tG_ancestors:
-  "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
-  by (unfold dependants_alt_tG ancestors_def, simp)
-
-
-
 section {* Locales used to investigate the execution of PIP *}
 
 text {* 
@@ -2543,8 +2475,22 @@
   show ?thesis by simp
 qed
 
+find_theorems inj finite "_ ` _"
+
+find_theorems tG tRAG
+
+thm tRAG_def_tG
+
+find_theorems "finite (?f ` ?A)" "finite ?A"
+
 lemma finite_tG: "finite (tG s)"
-  by (unfold tG_def, insert finite_tRAG, auto)
+proof(rule finite_imageD)
+  from finite_tRAG[unfolded tRAG_def_tG]
+  show "finite (map_prod Th Th ` tG s)" .
+next
+  show "inj_on (map_prod Th Th) (tG s)"
+    using inj_on_def by fastforce
+qed
 
 end
 
@@ -3108,7 +3054,7 @@
       by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto)
   qed
   thus ?thesis
-  by (unfold tG_def, fold rel_map_alt_def, simp)
+  by (unfold tG_def_tRAG, fold rel_map_alt_def, simp) 
 qed
 
 lemma sgv_wRAG: "single_valued (wRAG s)"
@@ -3344,9 +3290,20 @@
 proof -
   from th_chain_to_ready[OF assms]
   show ?thesis
-  using dependants_alt_def1 dependants_alt_tG 
-  unfolding nancestors_def ancestors_def
-  by blast 
+  proof
+    assume "th \<in> readys s"
+    thus ?thesis by (unfold nancestors_def, auto)
+  next
+    assume "\<exists>th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)\<^sup>+"
+    then obtain th' where h: "th' \<in> readys s" "(Th th, Th th') \<in> (RAG s)\<^sup>+" by auto
+    from h(2) tRAG_trancl_eq
+    have "(Th th, Th th') \<in> (tRAG s)^+" by auto
+    hence "(th, th') \<in> (tG s)^+"
+      by (metis the_thread.simps trancl_tRAG_tG)
+    with h(1)
+    show ?thesis
+      using ancestors_def mem_Collect_eq nancestors2 by fastforce
+  qed
 qed
 
 
@@ -3754,7 +3711,6 @@
   over the union of subtrees, the following equation can be derived:
 *}
 
-
 lemma cp_alt_def3:
   shows "cp s th = Max (preceds (subtree (tG s) th) s)"
 unfolding cp_alt_def2
@@ -5173,19 +5129,13 @@
   shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
   using count_eq_RAG_plus[OF assms] by auto
 
-lemma eq_pv_dependants:
-  assumes eq_pv: "cntP s th = cntV s th"
-  shows "dependants s th = {}"
-proof -
-  from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
-  show ?thesis .
-qed
 
 lemma count_eq_tRAG_plus:
   assumes "cntP s th = cntV s th"
   shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
-  using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast
-
+  using count_eq_RAG_plus_Th[OF assms]
+  using tRAG_trancl_eq by auto
+  
 lemma count_eq_tRAG_plus_Th:
   assumes "cntP s th = cntV s th"
   shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
--- 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" |
Binary file journal.pdf has changed