592   the @{text P}-operation.

   592   the @{text P}-operation.

   593 *}

   593 *}

   594 

   594 

   595 context valid_trace_p_h

   595 context valid_trace_p_h

   596 begin

   596 begin

   598 text {*

   598 text {*

   599   It can be shown that the @{text tG} is not changed by 

   599   It can be shown that the @{text tG} is not changed by 

   600   the @{text P}-action. The reason is that the edge added to @{text RAG}

   600   the @{text P}-action. The reason is that the edge added to @{text RAG}

   601   by the @{text P}-action, namely @{text "(Cs cs, Th th)"},

   601   by the @{text P}-action, namely @{text "(Cs cs, Th th)"},

   602   does not bring any new thread into graph @{text tG}, because 

   602   does not bring any new thread into graph @{text tG}, because 

   603   the node of @{text cs} is isolated from the original @{text RAG}.

   603   the node of @{text cs} is isolated from the original @{text RAG}.

   604 *}

   604 *}

   605 

   605 

   606 lemma tG_es: "tG (e # s) = tG s"

   608 lemma tG_es: "tG (e # s) = tG s"

   607 proof -

   609 proof -

   608   have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"

   610   have [simp]: "\<And> th1. (Th th1, Cs cs) \<notin> RAG s"

   609     by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding)

   611     by (metis in_RAG_E no_holder node.simps(4) the_cs.simps waiting_holding)

   610   show ?thesis

   612   show ?thesis

   638 

   640 

   639 lemma tRAG_s: 

   641 lemma tRAG_s: 

   640   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"

   642   "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}"

   641   using RAG_tRAG_transfer[OF RAG_es cs_held] .

   643   using RAG_tRAG_transfer[OF RAG_es cs_held] .

   642 

   644 

   643 text {*

   651 text {*

   644   The following lemma shows only the ancestors of @{text th} (the initiating 

   652   The following lemma shows only the ancestors of @{text th} (the initiating 

   645   thread of the @{text P}-operation) may possibly 

   653   thread of the @{text P}-operation) may possibly 

   646   need a @{text cp}-recalculation. All other threads (including @{text th} itself)

   654   need a @{text cp}-recalculation. All other threads (including @{text th} itself)

   647   do not need @{text cp}-recalculation. 

   655   do not need @{text cp}-recalculation. 

   648 *}

   656 *}

   649 lemma cp_kept:

   658 lemma cp_kept:

   650   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"

   659   assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)"

   651   shows "cp (e#s) th'' = cp s th''"

   660   shows "cp (e#s) th'' = cp s th''"

   652 proof -

   661 proof -

   653   have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"

   662   have h: "subtree (tRAG (e#s)) (Th th'') = subtree (tRAG s) (Th th'')"

   679     from this[folded tRAG_s] show ?thesis .

   688     from this[folded tRAG_s] show ?thesis .

   680   qed

   689   qed

   681   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)

   690   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)

   682 qed

   691 qed

   683 

   692 

   684 text {*

   699 text {*

   685   Lemma @{thm cp_kept} means that the @{text cp}-recalculation starts from the parent of @{text th},

   700   Lemma @{thm cp_kept} means that the @{text cp}-recalculation starts from the parent of @{text th},

   686   going upwards along the chain of ancestors until one root (which is a thread 

   701   going upwards along the chain of ancestors until one root (which is a thread 

   687   in ready queue) is reached. Actually, recalculation can terminate earlier, as 

   702   in ready queue) is reached. Actually, recalculation can terminate earlier, as 

   688   confirmed by the following two lemmas. 

   703   confirmed by the following two lemmas. 

   815       by (fold cp_gen_rec[OF eq_x], simp)

   830       by (fold cp_gen_rec[OF eq_x], simp)

   816     finally show ?thesis .

   831     finally show ?thesis .

   817   qed

   832   qed

   818 qed

   833 qed

   819 

   834 

   820 text {*

   836 text {*

   821   The following lemma is about the possible early termination of 

   837   The following lemma is about the possible early termination of 

   822   @{text cp}-recalculation. The lemma says that @{text cp}-recalculation 

   838   @{text cp}-recalculation. The lemma says that @{text cp}-recalculation 

   823   can terminate as soon as the recalculation yields an unchanged @{text cp}-value. 

   839   can terminate as soon as the recalculation yields an unchanged @{text cp}-value. 

   824 

   840 

   840     show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis

   856     show "cp_gen (e#s) (Th th') = cp_gen s (Th th')" by metis

   841   qed

   857   qed

   842   with cp_gen_def_cond[OF refl[of "Th th''"]]

   858   with cp_gen_def_cond[OF refl[of "Th th''"]]

   843   show ?thesis by metis

   859   show ?thesis by metis

   844 qed

   860 qed

   845 

   868 

   846 end

   869 end

   847 

   870 

   848 text {* 

   871 text {* 

   849   The following locale deals with the @{text Create}-operation.

   872   The following locale deals with the @{text Create}-operation.