equal
deleted
inserted
replaced
655 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} |
655 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} |
656 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
656 lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)" |
657 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
657 by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv |
658 s_holding_abv cs_RAG_def, auto) |
658 s_holding_abv cs_RAG_def, auto) |
659 |
659 |
|
660 lemma tRAG_alt_def: |
|
661 "tRAG s = {(Th th1, Th th2) | th1 th2. |
|
662 \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" |
|
663 by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def) |
|
664 |
660 definition "cp_gen s x = |
665 definition "cp_gen s x = |
661 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
666 Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)" |
662 |
667 |
663 (*<*) |
668 (*<*) |
664 |
669 |