pip: comparison Correctness.thy

equal deleted inserted replaced

-:a88af0e4731f
+:38c6acf03f68
 text {*
 The following lemmas shows that the @{term cp}-value
 of the blocking thread @{text th'} equals to the highest
 precedence in the whole system.
 *}
-lemma runing_preced_inversion:
+lemma running_preced_inversion:
-assumes runing': "th' \<in> runing (t@s)"
+assumes running': "th' \<in> running (t@s)"
 shows "cp (t@s) th' = preced th s" (is "?L = ?R")
 proof -
 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
-by (unfold runing_def, auto)
+by (unfold running_def, auto)
 also have "\<dots> = ?R"
 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
 finally show ?thesis .
 qed
 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.
 On the other hand, since @{text th'} is running, by @{thm
-runing_preced_inversion}, its @{term cp}-value equals to the
+running_preced_inversion}, its @{term cp}-value equals to the
 precedence of @{term th}.
 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
 *}
 lemma eq_pv_blocked: (* ddd *)
 assumes neq_th': "th' \<noteq> th"
 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
-shows "th' \<notin> runing (t@s)"
+shows "th' \<notin> running (t@s)"
 proof
-assume otherwise: "th' \<in> runing (t@s)"
+assume otherwise: "th' \<in> running (t@s)"
 show False
 proof -
 have th'_in: "th' \<in> threads (t@s)"
-using otherwise readys_threads runing_def by auto
+using otherwise readys_threads running_def by auto
 have "th' = th"
 proof(rule preced_unique)
 -- {* The proof goes like this:
 it is first shown that the @{term preced}-value of @{term th'}
 equals to that of @{term th}, then by uniqueness
 -- {* Since the counts of @{term th'} are balanced, the subtree
 of it contains only itself, so, its @{term cp}-value
 equals its @{term preced}-value: *}
 have "?L = cp (t@s) th'"
 by (unfold cp_eq cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
--- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
+-- {* Since @{term "th'"} is running, by @{thm running_preced_inversion},
 its @{term cp}-value equals @{term "preced th s"},
 which equals to @{term "?R"} by simplification: *}
 also have "... = ?R"
-thm runing_preced_inversion
+thm running_preced_inversion
-using runing_preced_inversion[OF otherwise] by simp
+using running_preced_inversion[OF otherwise] by simp
 finally show ?thesis .
 qed
 qed (auto simp: th'_in th_kept)
 with `th' \<noteq> th` show ?thesis by simp
 qed
 -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}
 assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"
 from cntP_diff_inv[OF this[simplified]]
 obtain cs' where "e = P th' cs'" by auto
 from vat_es.pip_e[unfolded this]
-have "th' \<in> runing (t@s)"
+have "th' \<in> running (t@s)"
 by (cases, simp)
 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
 shows @{term th'} can not be running at moment  @{term "t@s"}: *}
-moreover have "th' \<notin> runing (t@s)"
+moreover have "th' \<notin> running (t@s)"
 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
 -- {* Contradiction is finally derived: *}
 ultimately show False by simp
 qed
 -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change
 proof(rule ccontr) -- {* Proof by contradiction. *}
 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"
 from cntV_diff_inv[OF this[simplified]]
 obtain cs' where "e = V th' cs'" by auto
 from vat_es.pip_e[unfolded this]
-have "th' \<in> runing (t@s)" by (cases, auto)
+have "th' \<in> running (t@s)" by (cases, auto)
-moreover have "th' \<notin> runing (t@s)"
+moreover have "th' \<notin> running (t@s)"
 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
 ultimately show False by simp
 qed
 -- {* Finally, it can be shown that the @{term cntP} and @{term cntV}
 value for @{term th'} are still in balance, so @{term th'}
 it can be derived easily that @{term th'} can not be running in the future:
 *}
 lemma eq_pv_blocked_persist:
 assumes neq_th': "th' \<noteq> th"
 and eq_pv: "cntP s th' = cntV s th'"
-shows "th' \<notin> runing (t@s)"
+shows "th' \<notin> running (t@s)"
 using assms
 by (simp add: eq_pv_blocked eq_pv_persist)
 text {*
 The following lemma shows the blocking thread @{term th'}
 must hold some resource in the very beginning.
 *}
-lemma runing_cntP_cntV_inv: (* ddd *)
+lemma running_cntP_cntV_inv: (* ddd *)
-assumes is_runing: "th' \<in> runing (t@s)"
+assumes is_running: "th' \<in> running (t@s)"
 and neq_th': "th' \<noteq> th"
 shows "cntP s th' > cntV s th'"
 using assms
 proof -
 -- {* First, it can be shown that the number of @{term P} and
 -- {* The proof goes by contradiction, suppose otherwise: *}
 assume otherwise: "cntP s th' = cntV s th'"
 -- {* By applying @{thm  eq_pv_blocked_persist} to this: *}
 from eq_pv_blocked_persist[OF neq_th' otherwise]
 -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}
-have "th' \<notin> runing (t@s)" .
+have "th' \<notin> running (t@s)" .
--- {* This is obvious in contradiction with assumption @{thm is_runing}  *}
+-- {* This is obvious in contradiction with assumption @{thm is_running}  *}
-thus False using is_runing by simp
+thus False using is_running by simp
 qed
 -- {* However, the number of @{term V} is always less or equal to @{term P}: *}
 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
 -- {* Thesis is finally derived by combining the these two results: *}
 ultimately show ?thesis by auto
 The following lemmas shows the blocking thread @{text th'} must be live
 at the very beginning, i.e. the moment (or state) @{term s}.
 The proof is a  simple combination of the results above:
 *}
-lemma runing_threads_inv:
+lemma running_threads_inv:
-assumes runing': "th' \<in> runing (t@s)"
+assumes running': "th' \<in> running (t@s)"
 and neq_th': "th' \<noteq> th"
 shows "th' \<in> threads s"
 proof(rule ccontr) -- {* Proof by contradiction: *}
 assume otherwise: "th' \<notin> threads s"
-have "th' \<notin> runing (t @ s)"
+have "th' \<notin> running (t @ s)"
 proof -
 from vat_s.cnp_cnv_eq[OF otherwise]
 have "cntP s th' = cntV s th'" .
 from eq_pv_blocked_persist[OF neq_th' this]
 show ?thesis .
 qed
-with runing' show False by simp
+with running' show False by simp
 qed
 text {*
 The following lemma summarizes several foregoing
 lemmas to give an overall picture of the blocking thread @{text "th'"}:
 *}
-lemma runing_inversion: (* ddd, one of the main lemmas to present *)
+lemma running_inversion: (* ddd, one of the main lemmas to present *)
-assumes runing': "th' \<in> runing (t@s)"
+assumes running': "th' \<in> running (t@s)"
 and neq_th: "th' \<noteq> th"
 shows "th' \<in> threads s"
 and    "\<not>detached s th'"
 and    "cp (t@s) th' = preced th s"
 proof -
-from runing_threads_inv[OF assms]
+from running_threads_inv[OF assms]
 show "th' \<in> threads s" .
 next
-from runing_cntP_cntV_inv[OF runing' neq_th]
+from running_cntP_cntV_inv[OF running' neq_th]
 show "\<not>detached s th'" using vat_s.detached_eq by simp
 next
-from runing_preced_inversion[OF runing']
+from running_preced_inversion[OF running']
 show "cp (t@s) th' = preced th s" .
 qed
 section {* The existence of `blocking thread` *}
 there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
 Now, since @{term readys}-set is non-empty, there must be
 one in it which holds the highest @{term cp}-value, which, by definition,
-is the @{term runing}-thread. However, we are going to show more: this running thread
+is the @{term running}-thread. However, we are going to show more: this running thread
 is exactly @{term "th'"}.
 *}
 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
-assumes "th \<notin> runing (t@s)"
+assumes "th \<notin> running (t@s)"
 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-"th' \<in> runing (t@s)"
+"th' \<in> running (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"}. *}
+@{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *}
 moreover have "th \<notin> readys (t@s)"
-using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+using assms running_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)"
+have "th' \<in> running (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_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. *}
+it is @{term running} by definition. *}
-with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def)
+with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_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)"
+assumes "th \<notin> running (t @ s)"
 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-"th' \<in> runing (t @ s)"
+"th' \<in> running (t @ s)"
 proof -
 -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is
 in @{term "readys"} or there is path in the @{term RAG} leading from
 it to a thread that is in @{term "readys"}. However, @{term th} cannot
 be in @{term readys}, because otherwise, since @{term th} holds the
-highest @{term cp}-value, it must be @{term "runing"}. This would
+highest @{term cp}-value, it must be @{term "running"}. This would
 violate our assumption. *}
 have "th \<notin> readys (t @ s)"
-using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
+using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto
 then have "\<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
 then 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 first show that this @{term th'} is running. *}
-have "th' \<in> runing (t @ s)"
+have "th' \<in> running (t @ s)"
 proof -
 -- {* For this we need to show that @{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_preced_def vat_t.max_cp_readys_threads by auto
 finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
 qed
 -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
-it is @{term runing} by definition. *}
+it is @{term running} by definition. *}
-with `th' \<in> readys (t @ s)` show "th' \<in> runing (t @ s)" by (simp add: runing_def)
+with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_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 th_blockedE_pretty:
-assumes "th \<notin> runing (t@s)"
+assumes "th \<notin> running (t@s)"
-shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> runing (t@s)"
+shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)"
 using th_blockedE assms by blast
 text {*
 Now it is easy to see there is always a thread to run by case analysis
 on whether thread @{term th} is running: if the answer is Yes, the
 the running thread is obviously @{term th} itself; otherwise, the running
 thread is the @{text th'} given by lemma @{thm th_blockedE}.
 *}
-lemma live: "runing (t@s) \<noteq> {}"
+lemma live: "running (t@s) \<noteq> {}"
-proof(cases "th \<in> runing (t@s)")
+proof(cases "th \<in> running (t@s)")
 case True thus ?thesis by auto
 next
 case False
 thus ?thesis using th_blockedE by auto
 qed
 lemma blockedE:
-assumes "th \<notin> runing (t@s)"
+assumes "th \<notin> running (t@s)"
 obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
-"th' \<in> runing (t@s)"
+"th' \<in> running (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)
+by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
-lemma detached_not_runing:
+lemma detached_not_running:
 assumes "detached (t@s) th'"
 and "th' \<noteq> th"
-shows "th' \<notin> runing (t@s)"
+shows "th' \<notin> running (t@s)"
 proof
-assume otherwise: "th' \<in> runing (t @ s)"
+assume otherwise: "th' \<in> running (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)
+by (simp add:running_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)
+using otherwise by (unfold running_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
 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:
+lemma runningE:
-assumes "th' \<in> runing (t@s)"
+assumes "th' \<in> running (t@s)"
 obtains (is_th) "th' = th"
 | (is_other) "th' \<in> blockers"
-using assms blockers_def runing_inversion(2) by auto
+using assms blockers_def running_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.
 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)
+hence "th' \<in> readys (t@s)" by (auto simp:running_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]
+from et.detached_not_running[OF this] assms[unfolded blockers_def]
-have "th' \<notin> runing (t @ s)" by auto
+have "th' \<notin> running (t @ s)" by auto
 with h(1) show ?thesis by simp
 qed
 } thus ?thesis by auto
 qed
 qed
 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'"
+shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (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)
 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
+have "th \<in> running 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
 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"
+have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (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
+have "th \<in> running (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
 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"
+shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> running (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'" .
+have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t'" .
-moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t"
+moreover have "... \<le> occs (\<lambda>t'. th \<in> running (t' @ s)) t"
 by (unfold Cons, auto)
 ultimately show ?thesis by simp
 qed (auto simp:actions_of_def)
 text {*
 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)")
+proof(cases "actor e \<in> running (t@s)")
 case True
 thus ?thesis
-proof(rule ve.runingE)
+proof(rule ve.runningE)
 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
 the correctness of PIP.
 *}
 theorem bound_priority_inversion:
-"occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+"occs (\<lambda> t'. th \<notin> running (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))"
+let ?Q = "(\<lambda> t'. th \<in> running (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")
+\<le> occs (\<lambda> t'. th \<in> running (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
 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)" .
+have "th' \<in> running (t @ s)" .
-moreover have "th' \<notin> runing (t @ s)"
+moreover have "th' \<notin> running (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
+from extend_highest_gen.detached_not_running[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)
 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>
+"occs (\<lambda> t'. th \<notin> running (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')") .

changeset 127	38c6acf03f68
parent 126	a88af0e4731f
child 130	0f124691c191