
diff -r 71a3300d497b -r 95e7933968f8 Correctness.thy
--- a/Correctness.thy	Fri Apr 15 14:44:09 2016 +0100
+++ b/Correctness.thy	Thu Jun 02 13:15:03 2016 +0100
@@ -52,6 +52,13 @@
 sublocale highest_gen < vat_s?: valid_trace "s"
   by (unfold_locales, insert vt_s, simp)
 
+fun occs where
+  "occs Q [] = (if Q [] then 1 else 0::nat)" |
+  "occs Q (x#xs) = (if Q (x#xs) then (1 + occs Q xs) else occs Q xs)"
+
+lemma occs_le: "occs Q t + occs (\<lambda> e. \<not> Q e) t \<le> (1 + length t)"
+  by  (induct t, auto)
+
 context highest_gen
 begin
 
@@ -68,6 +75,7 @@
   @{text "th"} and @{text th} is among these threads, 
   its @{term cp} must equal to its precedence:
 *}
+
 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
 proof -
   have "?L \<le> ?R"
@@ -742,6 +750,9 @@
     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
     proof -
+      -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
+            the  @{term cp}-value of @{term th'} is the maximum of 
+            all precedences of all thread nodes in its @{term tRAG}-subtree: *}
       have "?L =  Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
         by (unfold cp_alt_def1, simp)
       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
@@ -762,9 +773,82 @@
           thus ?thesis using max_preced the_preced_def by auto
         qed
       qed
+      thm the_preced_def
       also have "... = ?R"
         using th_cp_max th_cp_preced th_kept 
               the_preced_def vat_t.max_cp_readys_threads by auto
+              thm th_cp_max th_cp_preced th_kept 
+              the_preced_def vat_t.max_cp_readys_threads
+      finally show ?thesis .
+    qed 
+    -- {* Now, since @{term th'} holds the highest @{term cp} 
+          and we have already show it is in @{term readys},
+          it is @{term runing} by definition. *}
+    with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) 
+  qed
+  -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
+  moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
+    using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
+  ultimately show ?thesis using that by metis
+qed
+
+lemma (* new proof of th_blockedE *)
+  assumes "th \<notin> runing (t@s)"
+  obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+                    "th' \<in> runing (t@s)"
+proof -
+  -- {* According to @{thm vat_t.th_chain_to_ready}, either 
+        @{term "th"} is in @{term "readys"} or there is path leading from it to 
+        one thread in @{term "readys"}. *}
+  have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" 
+    using th_kept vat_t.th_chain_to_ready by auto
+  -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
+       @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
+  moreover have "th \<notin> readys (t@s)" 
+    using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
+  -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
+        term @{term readys}: *}
+  ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
+                          and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+  -- {* We are going to show that this @{term th'} is running. *}
+  have "th' \<in> runing (t@s)"
+  proof -
+    -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
+    have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+    proof -
+      -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
+            the  @{term cp}-value of @{term th'} is the maximum of 
+            all precedences of all thread nodes in its @{term tRAG}-subtree: *}
+      have "?L =  Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"
+      proof -
+        have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =
+              the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"
+                by fastforce
+        thus ?thesis by (unfold cp_alt_def1, simp)
+      qed
+      also have "... = (the_preced (t @ s) th)"
+      proof(rule image_Max_subset)
+        show "finite (threads (t@s))" by (simp add: vat_t.finite_threads)
+      next
+        show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
+          by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 
+                the_thread.simps vat_t.subtree_tRAG_thread)
+      next
+        show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
+        proof -
+          have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
+                    by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+          thus ?thesis by force
+        qed
+      next
+        show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+          by simp
+      qed
+      also have "... = ?R"
+        using th_cp_max th_cp_preced th_kept 
+              the_preced_def vat_t.max_cp_readys_threads by auto
+              thm th_cp_max th_cp_preced th_kept 
+              the_preced_def vat_t.max_cp_readys_threads
       finally show ?thesis .
     qed 
     -- {* Now, since @{term th'} holds the highest @{term cp} 
@@ -792,5 +876,588 @@
   thus ?thesis using th_blockedE by auto
 qed
 
+lemma blockedE:
+  assumes "th \<notin> runing (t@s)"
+  obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+                    "th' \<in> runing (t@s)"
+                    "th' \<in> threads s"
+                    "\<not>detached s th'"
+                    "cp (t@s) th' = preced th s"
+                    "th' \<noteq> th"
+by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE)
+
+lemma detached_not_runing:
+  assumes "detached (t@s) th'"
+  and "th' \<noteq> th"
+  shows "th' \<notin> runing (t@s)"
+proof
+    assume otherwise: "th' \<in> runing (t @ s)"
+    have "cp (t@s) th' = cp (t@s) th"
+    proof -
+      have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise
+          by (simp add:runing_def)
+      moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads)
+      ultimately show ?thesis by simp
+    qed
+    moreover have "cp (t@s) th' = preced th' (t@s)" using assms(1)
+      by (simp add: detached_cp_preced)
+    moreover have "cp (t@s) th = preced th (t@s)" by simp
+    ultimately have "preced th' (t@s) = preced th (t@s)" by simp
+    from preced_unique[OF this] 
+    have "th' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .
+    moreover have "th' \<in> threads (t@s)" 
+      using otherwise by (unfold runing_def readys_def, auto)
+    moreover have "th \<in> threads (t@s)" by (simp add: th_kept) 
+    ultimately have "th' = th" by metis
+    with assms(2) show False by simp
+qed
+
+section {* The correctness theorem of PIP *}
+
+text {*
+  In this section, we identify two more conditions in addition to the ones already 
+  specified in the forgoing locales, based on which the correctness of PIP is 
+  formally proved. 
+
+  Note that Priority Inversion refers to the phenomenon where the thread with highest priority 
+  is blocked by one with lower priority because the resource it is requesting is 
+  currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion}, 
+  i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large. 
+
+  For PIP to be correct, a finite upper bound needs to be found for the occurrence number, 
+  and the existence. This section makes explicit two more conditions so that the existence 
+  of such a upper bound can be proved to exist. 
+*}
+
+text {*
+  The following set @{text "blockers"} characterizes the set of threads which 
+  might block @{term th} in @{term t}:
+*}
+
+definition "blockers = {th'. \<not>detached s th' \<and> th' \<noteq> th}"
+
+text {*
+  The following lemma shows that the definition of @{term "blockers"} is correct, 
+  i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.
+*}
+lemma runingE:
+  assumes "th' \<in> runing (t@s)"
+  obtains (is_th) "th' = th"
+        | (is_other) "th' \<in> blockers"
+  using assms blockers_def runing_inversion(2) by auto
+
+text {*
+  The following lemma shows that the number of blockers are finite.
+  The reason is simple, because blockers are subset of thread set, which
+  has been shown finite.
+*}
+
+lemma finite_blockers: "finite blockers"
+proof -
+  have "finite {th'. \<not>detached s th'}"
+  proof -
+    have "finite {th'. Th th' \<in> Field (RAG s)}"
+    proof -
+      have "{th'. Th th' \<in> Field (RAG s)} \<subseteq> threads s"
+      proof
+        fix x
+        assume "x \<in> {th'. Th th' \<in> Field (RAG s)}"
+        thus "x \<in> threads s" using vat_s.RAG_threads by auto
+      qed
+      moreover have "finite ..." by (simp add: vat_s.finite_threads) 
+      ultimately show ?thesis using rev_finite_subset by auto 
+    qed
+    thus ?thesis by (unfold detached_test, auto)
+  qed
+  thus ?thesis unfolding blockers_def by simp
+qed
+
+text {*
+  The following lemma shows that a blocker may never die
+  as long as the highest thread @{term th} is living. 
+
+  The reason for this is that, before a thread can execute an @{term Exit} operation,
+  it must give up all its resource. However, the high priority inherited by a blocker 
+  thread also goes with the resources it once held, and the consequence is the lost of 
+  right to run, the other precondition for it to execute its own  @{term Exit} operation.
+  For this reason, a blocker may never exit before the exit of the highest thread @{term th}.
+*}
+
+lemma blockers_kept:
+  assumes "th' \<in> blockers"
+  shows "th' \<in> threads (t@s)"
+proof(induct rule:ind)
+  case Nil
+  from assms[unfolded blockers_def detached_test]
+  have "Th th' \<in> Field (RAG s)" by simp
+  from vat_s.RAG_threads[OF this]
+  show ?case by simp
+next
+  case h: (Cons e t)
+  interpret et: extend_highest_gen s th prio tm t
+    using h by simp
+  show ?case
+  proof -
+    { assume otherwise: "th' \<notin> threads ((e # t) @ s)"
+      from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto
+      from h(2)[unfolded this]
+      have False
+      proof(cases)
+        case h: (thread_exit)
+        hence "th' \<in> readys (t@s)" by (auto simp:runing_def)
+        from readys_holdents_detached[OF this h(2)]
+        have "detached (t @ s) th'" .
+        from et.detached_not_runing[OF this] assms[unfolded blockers_def]
+        have "th' \<notin> runing (t @ s)" by auto
+        with h(1) show ?thesis by simp
+      qed
+    } thus ?thesis by auto
+  qed
+qed
+
+text {*
+  The following lemma shows that a blocker may never execute its @{term Create}-operation
+  during the period of @{term t}. The reason is that for a thread to be created 
+  (or executing its @{term Create} operation), it must be non-existing (or dead). 
+  However, since lemma @{thm blockers_kept} shows that blockers are always living, 
+  it can not be created. 
+
+  A thread is created only when there is some external reason, there is need for it to run. 
+  The precondition for this is that it has already died (or get out of existence).
+*}
+
+lemma blockers_no_create:
+  assumes "th' \<in> blockers"
+  and "e \<in> set t"
+  and "actor e = th'"
+  shows "\<not> isCreate e"
+  using assms(2,3)
+proof(induct rule:ind)
+  case h: (Cons e' t)
+  interpret et: extend_highest_gen s th prio tm t
+    using h by simp
+  { assume eq_e: "e = e'"
+    from et.blockers_kept assms
+    have "th' \<in> threads (t @ s)" by auto
+    with h(2,7)
+    have ?case 
+      by (unfold eq_e, cases, auto simp:blockers_def)
+  } with h
+  show ?case by auto
+qed auto
+
+text {*
+  The following lemma shows that, same as blockers, 
+  the highest thread @{term th} also can not execute its @{term Create}-operation.
+  And the reason is similar: since @{thm th_kept} says that thread @{term th} is kept live
+  during @{term t}, it can not (or need not) be created another time.
+*}
+lemma th_no_create:
+  assumes "e \<in> set t"
+  and "actor e = th"
+  shows "\<not> isCreate e"
+  using assms
+proof(induct rule:ind)
+  case h:(Cons e' t)
+  interpret et: extend_highest_gen s th prio tm t
+    using h by simp
+  { assume eq_e: "e = e'"
+    from et.th_kept have "th \<in> threads (t @ s)" by simp
+    with h(2,7)
+    have ?case by (unfold eq_e, cases, auto)
+  } with h
+  show ?case by auto
+qed auto
+
+text {*
+  The following is a preliminary lemma in order to show that the number of 
+  actions (or operations) taken by the highest thread @{term th} is 
+  less or equal to the number of occurrences when @{term th} is in running
+  state. What is proved in this lemma is essentially a strengthening, which 
+  says the inequality holds even if the occurrence at the very beginning is
+  ignored.
+
+  The reason for this lemma is that for every operation to be executed, its actor must
+  be in running state. Therefore, there is one occurrence of running state
+  behind every action. 
+
+  However, this property does not hold in general, because, for 
+  the execution of @{term Create}-operation, the actor does not have to be in running state. 
+  Actually, the actor must be in dead state, in order to be created. For @{term th}, this 
+  property holds because, according to lemma @{thm th_no_create}, @{term th} can not execute
+  any @{term Create}-operation during the period of @{term t}.
+*}
+lemma actions_th_occs_pre:
+  assumes "t = e'#t'"
+  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t'"
+  using assms
+proof(induct arbitrary: e' t' rule:ind)
+  case h: (Cons e t e' t')
+  interpret vt: valid_trace "(t@s)" using h(1)
+    by (unfold_locales, simp)
+  interpret ve:  extend_highest_gen s th prio tm t using h by simp
+  interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
+  show ?case (is "?L \<le> ?R")
+  proof(cases t)
+    case Nil
+    show ?thesis
+    proof(cases "actor e = th")
+      case True
+      from ve'.th_no_create[OF _ this]
+      have "\<not> isCreate e" by auto
+      from PIP_actorE[OF h(2) True this] Nil
+      have "th \<in> runing s" by simp
+      hence "?R = 1" using Nil h by simp
+      moreover have "?L = 1" using True Nil by (simp add:actions_of_def)
+      ultimately show ?thesis by simp
+    next
+      case False
+      with Nil
+      show ?thesis by (auto simp:actions_of_def)
+    qed
+  next
+    case h1: (Cons e1 t1)
+    hence eq_t': "t' = e1#t1" using h by simp
+    from h(5)[OF h1]
+    have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t1" 
+      (is "?F t \<le> ?G t1") .
+    show ?thesis 
+    proof(cases "actor e = th")
+      case True
+      from ve'.th_no_create[OF _ this]
+      have "\<not> isCreate e" by auto
+      from PIP_actorE[OF h(2) True this]
+      have "th \<in> runing (t@s)" by simp
+      hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)
+      moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)
+      ultimately show ?thesis using le by simp
+    next
+      case False
+      with le
+      show ?thesis by (unfold h1 eq_t', simp add:actions_of_def)
+    qed
+  qed
+qed auto
+
+text {*
+  The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the
+  lemma really needed in later proofs.
+*}
+lemma actions_th_occs:
+  shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
+proof(cases t)
+  case (Cons e' t')
+  from actions_th_occs_pre[OF this]
+  have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t'" .
+  moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t" 
+    by (unfold Cons, auto)
+  ultimately show ?thesis by simp
+qed (auto simp:actions_of_def)
+
+text {*
+  The following lemma splits all the operations in @{term t} into three
+  disjoint sets, namely the operations of @{term th}, the operations of 
+  blockers and @{term Create}-operations. These sets are mutually disjoint
+  because: @{term "{th}"} and @{term blockers} are disjoint by definition, 
+  and neither @{term th} nor any blocker can execute @{term Create}-operation
+  (according to lemma @{thm th_no_create} and @{thm blockers_no_create}).
+
+  One important caveat noted by this lemma is that: 
+  Although according to assumption @{thm create_low}, each thread created in 
+  @{term t} has precedence lower than @{term th}, therefore, will get no
+  change to run after creation, therefore, can not acquire any resource 
+  to become a blocker, the @{term Create}-operations of such 
+  lower threads may still consume overall execution time of duration @{term t}, therefore,
+  may compete for execution time with the most urgent thread @{term th}.
+  For PIP to be correct, the number of such competing operations needs to be 
+  bounded somehow.
+*}
+
+lemma actions_split:
+  "length t = length (actions_of {th} t) + 
+              length (actions_of blockers t) + 
+              length (filter (isCreate) t)"
+proof(induct rule:ind)
+  case h: (Cons e t)
+  interpret ve :  extend_highest_gen s th prio tm t using h by simp
+  interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
+  show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)")
+  proof(cases "actor e \<in> runing (t@s)")
+    case True
+    thus ?thesis
+    proof(rule ve.runingE)
+      assume 1: "actor e = th"
+      have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def)
+      moreover have "?O (e#t) = ?O t" 
+      proof -
+        have "actor e \<notin> blockers" using 1
+          by (simp add:actions_of_def blockers_def)
+        thus ?thesis by (simp add:actions_of_def)
+      qed
+      moreover have "?C (e#t) = ?C t"
+      proof -
+        from ve'.th_no_create[OF _ 1]
+        have "\<not> isCreate e" by auto
+        thus ?thesis by (simp add:actions_of_def)
+      qed
+      ultimately show ?thesis using h by simp
+    next
+      assume 2: "actor e \<in> ve'.blockers"
+      have "?T (e#t) = ?T (t)"
+      proof -
+        from 2 have "actor e \<noteq> th" by (auto simp:blockers_def)
+        thus ?thesis by (auto simp:actions_of_def)
+      qed
+      moreover have "?O (e#t) = 1 + ?O(t)" using 2
+        by (auto simp:actions_of_def)
+      moreover have "?C (e#t) = ?C(t)"
+      proof -
+        from ve'.blockers_no_create[OF 2, of e]
+        have "\<not> isCreate e" by auto
+        thus ?thesis by (simp add:actions_of_def)
+      qed
+      ultimately show ?thesis using h by simp
+    qed
+  next
+    case False
+    from h(2)
+    have is_create: "isCreate e"
+      by (cases; insert False, auto)
+    have "?T (e#t) = ?T t"
+    proof -
+      have "actor e \<noteq> th"
+      proof
+        assume "actor e = th"
+        from ve'.th_no_create[OF _ this]
+        have "\<not> isCreate e" by auto
+        with is_create show False by simp
+      qed
+      thus ?thesis by (auto simp:actions_of_def)
+    qed
+    moreover have "?O (e#t) = ?O t"
+    proof -
+      have "actor e \<notin> blockers"
+      proof
+        assume "actor e \<in> blockers"
+        from ve'.blockers_no_create[OF this, of e]
+        have "\<not> isCreate e" by simp
+        with is_create show False by simp
+      qed
+      thus ?thesis by (simp add:actions_of_def)
+    qed
+    moreover have "?C (e#t) = 1 + ?C t" using is_create
+        by (auto simp:actions_of_def)
+    ultimately show ?thesis using h by simp
+  qed
+qed (auto simp:actions_of_def)
+
+text {*
+  By combining several of forging lemmas, this lemma gives a upper bound
+  of the occurrence number when the most urgent thread @{term th} is blocked.
+
+  It says, the occasions when @{term th} is blocked during period @{term t} 
+  is no more than the number of @{term Create}-operations and 
+  the operations taken by blockers plus one. 
+
+  Since the length of @{term t} may extend indefinitely, if @{term t} is full
+  of the above mentioned blocking operations, @{term th} may have not chance to run. 
+  And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely 
+  with the growth of @{term t}. Therefore, this lemma alone does not ensure 
+  the correctness of PIP. 
+
+*}
+
+theorem bound_priority_inversion:
+  "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
+          1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
+   (is "?L \<le> ?R")
+proof - 
+  let ?Q = "(\<lambda> t'. th \<in> runing (t'@s))"
+  from occs_le[of ?Q t] 
+  have "?L \<le> (1 + length t) - occs ?Q t" by simp
+  also have "... \<le> ?R"
+  proof -
+    have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
+              \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t" (is "?L1 \<le> ?R1")
+    proof -
+      have "?L1 = length (actions_of {th} t)" using actions_split by arith
+      also have "... \<le> ?R1" using actions_th_occs by simp
+      finally show ?thesis .
+    qed            
+    thus ?thesis by simp
+  qed
+  finally show ?thesis .
+qed
+
 end
+
+text {*
+  As explained before, lemma @{text bound_priority_inversion} alone does not
+  ensure the correctness of PIP. For PIP to be correct, the number of blocking operations 
+  (by {\em blocking operation}, we mean the @{term Create}-operations and 
+           operations taken by blockers) has to be bounded somehow.
+
+  And the following lemma is for this purpose.
+*}
+
+locale bounded_extend_highest = extend_highest_gen + 
+  -- {*
+    To bound operations of blockers, the locale specifies that each blocker 
+    releases all resources and becomes detached after a certain number 
+    of operations. In the assumption, this number is given by the 
+    existential variable @{text span}. Notice that this number is fixed for each 
+    blocker regardless of any particular instance of @{term t} in which it operates.
+    
+    This assumption is reasonable, because it is a common sense that 
+    the total number of operations take by any standalone thread (or process) 
+    is only determined by its own input, and should not be affected by 
+    the particular environment in which it operates. In this particular case,
+    we regard the @{term t} as the environment of thread @{term th}.
+  *}
+  assumes finite_span: 
+          "th' \<in> blockers \<Longrightarrow>
+                 (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+                                length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"
+  -- {* The following @{text BC} is bound of @{term Create}-operations *}
+  fixes BC
+  -- {* 
+  The following assumption requires the number of @{term Create}-operations is 
+  less or equal to @{term BC} regardless of any particular extension of @{term t}.
+
+   Although this assumption might seem doubtful at first sight, it is necessary 
+   to ensure the occasions when @{term th} is blocked to be finite. Just consider
+   the extreme case when @{term Create}-operations consume all the time in duration 
+   @{term "t"} and leave no space for neither @{term "th"} nor blockers to operate.
+   An investigate of the precondition for @{term Create}-operation in the definition 
+   of @{term PIP} may reveal that such extreme cases are well possible, because it 
+   is only required the thread to be created be a fresh (or dead one), and there 
+   are infinitely many such threads. 
+
+   However, if we relax the correctness criterion of PIP, allowing @{term th} to be 
+   blocked indefinitely while still attaining a certain portion of @{term t} to complete 
+   its task, then this bound @{term BC} can be lifted to function depending on @{term t}
+   where @{text "BC t"} is of a certain proportion of @{term "length t"}.
+  *}
+  assumes finite_create: 
+          "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"
+begin 
+
+text {*
+  The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:
+*}
+
+lemma create_bc: 
+  shows "length (filter isCreate t) \<le> BC"
+    by (meson extend_highest_gen_axioms finite_create)
+
+text {*
+  The following @{term span}-function gives the upper bound of 
+  operations take by each particular blocker.
+*}
+definition "span th' = (SOME span.
+         \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+              length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')"
+
+text {*
+  The following lemmas shows the correctness of @{term span}, i.e. 
+  the number of operations of taken by @{term th'} is given by 
+  @{term "span th"}.
+
+  The reason for this lemma is that since @{term th'} gives up all resources 
+  after @{term "span th'"} operations and becomes detached,
+  its inherited high priority is lost, with which the right to run goes as well.
+*}
+lemma le_span:
+  assumes "th' \<in> blockers"
+  shows "length (actions_of {th'} t) \<le> span th'"
+proof -
+  from finite_span[OF assms(1)] obtain span' 
+  where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+                     length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
+                     by auto
+  have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
+  proof(rule someI2[where a = span'])
+    fix span
+    assume fs: "?P span" 
+    show "length (actions_of {th'} t) \<le> span"
+    proof(induct rule:ind)
+      case h: (Cons e t)
+        interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
+      show ?case
+      proof(cases "length (actions_of {th'} t) < span")
+        case True
+        thus ?thesis by (simp add:actions_of_def)
+      next
+        case False
+        have "actor e \<noteq> th'"
+        proof
+          assume otherwise: "actor e = th'"
+          from ve'.blockers_no_create [OF assms _ this]
+          have "\<not> isCreate e" by auto
+          from PIP_actorE[OF h(2) otherwise this]
+          have "th' \<in> runing (t @ s)" .
+          moreover have "th' \<notin> runing (t @ s)"
+          proof -
+            from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
+            from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
+            from extend_highest_gen.detached_not_runing[OF h(3) this] assms
+            show ?thesis by (auto simp:blockers_def)
+          qed
+          ultimately show False by simp
+        qed
+        with h show ?thesis by (auto simp:actions_of_def)
+      qed
+    qed (simp add: actions_of_def)
+  next
+    from span'
+    show "?P span'" .
+  qed
+  thus ?thesis by (unfold span_def, auto)
+qed
+
+text {*
+  The following lemma is a corollary of @{thm le_span}, which says 
+  the total operations of blockers is bounded by the 
+  sum of @{term span}-values of all blockers.
+*}
+lemma len_action_blockers: 
+  "length (actions_of blockers t) \<le> (\<Sum> th' \<in> blockers . span th')"
+    (is "?L \<le> ?R")
+proof -
+  from len_actions_of_sigma[OF finite_blockers]
+  have "?L  = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
+  also have "... \<le> ?R"
+    by (rule Groups_Big.setsum_mono, insert le_span, auto)
+  finally show ?thesis .
+qed
+
+text {*
+  By combining forgoing lemmas, it is proved that the number of 
+  blocked occurrences of the most urgent thread @{term th} is finitely bounded:
+*}
+theorem priority_inversion_is_finite:
+  "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
+          1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
+proof -
+  from bound_priority_inversion
+  have "?L \<le> 1 + (length (actions_of blockers t) + length (filter isCreate t))" 
+      (is "_ \<le> 1 + (?A' + ?B')") .
+  moreover have "?A' \<le> ?A" using len_action_blockers .
+  moreover have "?B' \<le> ?B" using create_bc .
+  ultimately show ?thesis by simp
+qed
+
+text {*
+  The following lemma says the most urgent thread @{term th} will get as many 
+  as operations it wishes, provided @{term t} is long enough. 
+  Similar result can also be obtained under the slightly weaker assumption where
+  @{term BC} is lifted to a function and @{text "BC t"} is a portion of 
+  @{term "length t"}.
+*}
+theorem enough_actions_for_the_highest:
+  "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
+  using actions_split create_bc len_action_blockers by linarith
+
 end
+
+end




