# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1467937519 -3600
# Node ID 8a13b37b4d95e436dd4f8af0570a43201155f9d0
# Parent  4b717aa162fa59fc42d2c493be6e98c294b1fbc4
updated

diff -r 4b717aa162fa -r 8a13b37b4d95 Implementation.thy
--- a/Implementation.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/Implementation.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -161,7 +161,7 @@
   "ancestors (RAG s) (Cs cs) = {Th th}"
 proof -
   have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th)  \<union>  {Th th}"
-   by (rule rtree_RAG.ancestors_accum[OF edge_of_th])
+   by (rule forest_RAG.ancestors_accum[OF edge_of_th])
   from this[unfolded ancestors_th] show ?thesis by simp
 qed
 
@@ -193,7 +193,7 @@
   "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 
 proof -
   have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
-  proof(rule  rtree_RAG.ancestors_accum)
+  proof(rule  forest_RAG.ancestors_accum)
     from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
   qed
   thus ?thesis using ancestors_th ancestors_cs by auto
@@ -311,7 +311,7 @@
 
 lemma subtree_th: 
   "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)
+proof(unfold RAG_s, fold subtree_cs, rule forest_RAG.subtree_del_inside)
   from edge_of_th
   show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
     by (unfold edges_in_def, auto simp:subtree_def)
@@ -482,7 +482,7 @@
           assume a_in: "a \<in> ?A"
           from 1(2)
           show "?f a = ?g a"
-          proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+          proof(cases rule:vat_es.forest_s.ancestors_childrenE[case_names in_ch out_ch])
              case in_ch
              show ?thesis
              proof(cases "a = u")
@@ -494,7 +494,7 @@
                 proof
                   assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                   have "a = u"
-                  proof(rule vat_es.rtree_s.ancestors_children_unique)
+                  proof(rule vat_es.forest_s.ancestors_children_unique)
                     from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
                                           RTree.children (tRAG (e#s)) x" by auto
                   next 
@@ -528,7 +528,7 @@
               proof
                 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                 have "a = z"
-                proof(rule vat_es.rtree_s.ancestors_children_unique)
+                proof(rule vat_es.forest_s.ancestors_children_unique)
                   from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
                       by (auto simp:ancestors_def)
                   with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
diff -r 4b717aa162fa -r 8a13b37b4d95 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/Journal/Paper.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -184,6 +184,9 @@
   for a process that inherited a higher priority and exits a critical
   section ``{\it it resumes the priority it had at the point of entry
   into the critical section}''.  This error can also be found in the
+  textbook \cite[Section 16.4.1]{LiYao03} where the authors write
+  ``{\it its priority is immediately lowered to the level originally assigned}'';
+  or in the 
   more recent textbook \cite[Page 119]{Laplante11} where the authors
   state: ``{\it when [the task] exits the critical section that caused
   the block, it reverts to the priority it had when it entered that
@@ -207,7 +210,7 @@
   priority.}'' The same error is also repeated later in this textbook.
 
   
-  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+  While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
   formal publications we have found that specify the incorrect
   behaviour, it seems also many informal descriptions of PIP overlook
   the possibility that another high-priority might wait for a
diff -r 4b717aa162fa -r 8a13b37b4d95 Journal/document/root.bib
--- a/Journal/document/root.bib	Thu Jul 07 13:32:09 2016 +0100
+++ b/Journal/document/root.bib	Fri Jul 08 01:25:19 2016 +0100
@@ -23,6 +23,15 @@
   edition =   {3rd}
 }
 
+
+
+@Book{LiYao03,
+  author =    {Q.~Li and C.~Yao},
+  title =        {Real-Time Concepts for Embedded Systems},
+  publisher =    {CRC Press},
+  year =         {2003}
+}
+
 @Book{Laplante11,
   author = 	 {P.~A.~Laplante and S.~J.~Ovaska},
   title = 	 {{R}eal-{T}ime {S}ystems {D}esign and {A}nalysis: {T}ools for the {P}ractitioner},
diff -r 4b717aa162fa -r 8a13b37b4d95 PIPBasics.thy
--- a/PIPBasics.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/PIPBasics.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -2835,16 +2835,16 @@
 context valid_trace
 begin
 
-lemma rtree_RAG: "rtree (RAG s)"
+lemma forest_RAG: "forest (RAG s)"
   using sgv_RAG acyclic_RAG
-  by (unfold rtree_def, auto)
+  by (unfold forest_def, auto)
 
 end
 
-sublocale valid_trace < rtree_RAG?: rtree "RAG s"
-  using rtree_RAG .
-
-sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
+sublocale valid_trace < forest_RAG?: forest "RAG s"
+  using forest_RAG .
+
+sublocale valid_trace < fsbtRAGs?: fforest "RAG s"
 proof
   show "\<And>x. finite (children (RAG s) x)"
     by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) 
@@ -2886,7 +2886,7 @@
   finite-branch relational tree (or forest):  
 *}
 
-sublocale valid_trace < rtree_s?: rtree "tRAG s"
+sublocale valid_trace < forest_s?: forest "tRAG s"
 proof(unfold_locales)
   from sgv_tRAG show "single_valued (tRAG s)" .
 next
@@ -2894,7 +2894,7 @@
 qed
 
 
-sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
+sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
 proof
   fix x
   show "finite (children (tRAG s) x)"
@@ -3210,7 +3210,7 @@
     obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)"
                          "rpath (RAG s) n xs2 (Th th2)" by metis
     hence False
-    proof(cases rule:rtree_RAG.rpath_overlap')
+    proof(cases rule:forest_RAG.rpath_overlap')
       case (less_1 xs3)
       from rpath_star[OF this(3)]
       have "Th th1 \<in> subtree (RAG s) (Th th2)"
diff -r 4b717aa162fa -r 8a13b37b4d95 RTree.thy
--- a/RTree.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/RTree.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -21,7 +21,7 @@
 *}
 
 
-locale rtree = 
+locale forest = 
   fixes r
   assumes sgv: "single_valued r"
   assumes acl: "acyclic r"
@@ -110,7 +110,7 @@
 
 definition "children r x = {y. (y, x) \<in> r}"
 
-locale fgraph = rtree +
+locale fforest = forest +
   assumes fb: "finite (children r x)"
   assumes wf: "wf r"
 begin
@@ -721,7 +721,7 @@
 
 subsubsection {* Properties about relational trees *}
 
-context rtree 
+context forest 
 begin
 
 lemma ancestors_headE:
@@ -1350,7 +1350,7 @@
   qed
 qed
 
-end (* of rtree *)
+end (* of forest *)
 
 lemma subtree_trancl:
   "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")
@@ -1385,7 +1385,7 @@
   "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
   by fast
 
-context fgraph
+context fforest
 begin
   
 lemma finite_subtree:
@@ -1557,19 +1557,6 @@
   } thus ?thesis by (auto simp:acyclic_def)
 qed
 
-lemma relpow_mult: 
-  "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
-proof(induct n arbitrary:m)
-  case (Suc k m)
-  thus ?case
-  proof -
-    have h: "(m * k + m) = (m + m * k)" by auto
-    show ?thesis 
-      apply (simp add:Suc relpow_add[symmetric])
-      by (unfold h, simp)
-  qed
-qed simp
-
 lemma compose_relpow_2 [intro, simp]:
   assumes "r1 \<subseteq> r"
   and "r2 \<subseteq> r"
@@ -1584,6 +1571,19 @@
   } thus ?thesis by (auto simp:numeral_2_eq_2)
 qed
 
+lemma relpow_mult: 
+  "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
+proof(induct n arbitrary:m)
+  case (Suc k m)
+  thus ?case
+  proof -
+    have h: "(m * k + m) = (m + m * k)" by auto
+    show ?thesis 
+      apply (simp add:Suc relpow_add[symmetric])
+      by (unfold h, simp)
+  qed
+qed simp
+
 lemma acyclic_compose [intro, simp]:
   assumes "acyclic r"
   and "r1 \<subseteq> r"
@@ -1623,7 +1623,7 @@
       show "finite (children r1 ` children r2 x)"
       proof(rule finite_imageI)
         from h(2) have "x \<in> Range r2" by auto
-        from assms(2)[unfolded fgraph_def] this
+        from assms(2)[unfolded fforest_def] this
         show "finite (children r2 x)" by auto
       qed
      next
@@ -1637,7 +1637,7 @@
        next
           case False
           hence "y \<in> Range r1" by (unfold children_def, auto)
-          from assms(1)[unfolded fgraph_def] this h1(2)
+          from assms(1)[unfolded fforest_def] this h1(2)
           show ?thesis by auto
        qed
      qed
diff -r 4b717aa162fa -r 8a13b37b4d95 journal.pdf
Binary file journal.pdf has changed