27 assume "x \<in> ancestors (RAG s) (Th th)" |
27 assume "x \<in> ancestors (RAG s) (Th th)" |
28 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
28 hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
29 from tranclD[OF this] |
29 from tranclD[OF this] |
30 obtain z where "(Th th, z) \<in> RAG s" by auto |
30 obtain z where "(Th th, z) \<in> RAG s" by auto |
31 with assms(1) have False |
31 with assms(1) have False |
32 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def) |
32 apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_raw) |
33 by (fold wq_def, blast) |
33 by (fold wq_def, blast) |
34 } thus ?thesis by (unfold root_def, auto) |
34 } thus ?thesis by (unfold root_def, auto) |
35 qed |
35 qed |
36 |
36 |
37 lemma readys_in_no_subtree: |
37 lemma readys_in_no_subtree: |
666 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
666 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
667 proof - |
667 proof - |
668 have "Th th \<notin> Range (RAG s)" |
668 have "Th th \<notin> Range (RAG s)" |
669 proof |
669 proof |
670 assume "Th th \<in> Range (RAG s)" |
670 assume "Th th \<in> Range (RAG s)" |
671 then obtain cs where "holding (wq s) th cs" |
671 then obtain cs where "holding_raw (wq s) th cs" |
672 by (unfold Range_iff s_RAG_def, auto) |
672 by (unfold Range_iff s_RAG_def, auto) |
673 with holdents_th_s[unfolded holdents_def] |
673 with holdents_th_s[unfolded holdents_def] |
674 show False by (unfold holding_eq, auto) |
674 show False by (unfold holding_eq, auto) |
675 qed |
675 qed |
676 moreover have "Th th \<notin> Domain (RAG s)" |
676 moreover have "Th th \<notin> Domain (RAG s)" |
677 proof |
677 proof |
678 assume "Th th \<in> Domain (RAG s)" |
678 assume "Th th \<in> Domain (RAG s)" |
679 then obtain cs where "waiting (wq s) th cs" |
679 then obtain cs where "waiting_raw (wq s) th cs" |
680 by (unfold Domain_iff s_RAG_def, auto) |
680 by (unfold Domain_iff s_RAG_def, auto) |
681 with th_ready_s show False by (unfold readys_def waiting_eq, auto) |
681 with th_ready_s show False by (unfold readys_def waiting_eq, auto) |
682 qed |
682 qed |
683 ultimately show ?thesis by (auto simp:Field_def) |
683 ultimately show ?thesis by (auto simp:Field_def) |
684 qed |
684 qed |