123   assumed more urgent to finish. *}

   123   assumed more urgent to finish. *}

   124 

   124 

   125 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

   125 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"

   126   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"

   126   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"

   127 

   127 

   129   where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"

   129   where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"

   130 

   130 

   131 text {*

   131 text {*

   132 

   132 

   133   \noindent A number of important notions in PIP are represented as the

   133   \noindent A number of important notions in PIP are represented as the

   225   is whrere the word "Inheritance" in Priority Inheritance Protocol comes

   225   is whrere the word "Inheritance" in Priority Inheritance Protocol comes

   226   from. *}

   226   from. *}

   227 

   227 

   228 lemma cpreced_def2:

   228 lemma cpreced_def2:

   229   "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"

   229   "cpreced wq s th \<equiv> Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"

   231   apply(rule eq_reflection)

   231   apply(rule eq_reflection)

   232   apply(rule_tac f="Max" in arg_cong)

   232   apply(rule_tac f="Max" in arg_cong)

   233   by (auto)

   233   by (auto)

   234 

   234 

   235 definition 

   235 definition 

   377 lemma cpreced_initial: 

   377 lemma cpreced_initial: 

   378   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"

   378   "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"

   379 apply(rule ext)

   379 apply(rule ext)

   380 apply(simp add: cpreced_def)

   380 apply(simp add: cpreced_def)

   381 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)

   381 apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)

   383 done

   383 done

   384 

   384 

   385 text {* 

   385 text {* 

   386 

   386 

   387   \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.

   387   \noindent The following @{text "wq"} is a shorthand for @{text "wq_fun"}.