equal
deleted
inserted
replaced
3334 *} |
3334 *} |
3335 |
3335 |
3336 context valid_trace |
3336 context valid_trace |
3337 begin |
3337 begin |
3338 |
3338 |
3339 text {* |
3339 text {* The first lemma is technical, which says out of any node in the |
3340 The first lemma is technical, which says out of any node |
3340 domain of @{term RAG} (no matter whether it is thread node or resource |
3341 in the domain of @{term RAG}, |
3341 node), there is a path leading to a ready thread. |
3342 (no matter whether it is thread node or resource node) |
|
3343 there is a path leading to a ready thread. |
|
3344 *} |
3342 *} |
3345 |
3343 |
3346 lemma chain_building: |
3344 lemma chain_building: |
3347 assumes "node \<in> Domain (RAG s)" |
3345 assumes "node \<in> Domain (RAG s)" |
3348 obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+" |
3346 obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+" |
3407 show ?thesis by auto |
3405 show ?thesis by auto |
3408 qed |
3406 qed |
3409 |
3407 |
3410 lemma th_chain_to_ready_tG: |
3408 lemma th_chain_to_ready_tG: |
3411 assumes th_in: "th \<in> threads s" |
3409 assumes th_in: "th \<in> threads s" |
3412 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (th, th') \<in> (tG s)^+)" |
3410 shows "\<exists>th'\<in> nancestors (tG s) th. th' \<in> readys s" |
3413 proof - |
3411 proof - |
3414 from th_chain_to_ready[OF assms] |
3412 from th_chain_to_ready[OF assms] |
3415 show ?thesis |
3413 show ?thesis |
3416 using dependants_alt_def1 dependants_alt_tG by blast |
3414 using dependants_alt_def1 dependants_alt_tG |
3417 qed |
3415 unfolding nancestors_def ancestors_def |
|
3416 by blast |
|
3417 qed |
|
3418 |
3418 |
3419 |
3419 text {* |
3420 text {* |
3420 The following lemma is a technical one to show |
3421 The following lemma is a technical one to show |
3421 that the set of threads in the subtree of any thread |
3422 that the set of threads in the subtree of any thread |
3422 is finite. |
3423 is finite. |