equal
deleted
inserted
replaced
152 lemma edge_of_th: |
152 lemma edge_of_th: |
153 "(Cs cs, Th th) \<in> RAG s" |
153 "(Cs cs, Th th) \<in> RAG s" |
154 proof - |
154 proof - |
155 from holding_th_cs_s |
155 from holding_th_cs_s |
156 show ?thesis |
156 show ?thesis |
157 by (unfold s_RAG_def holding_eq, auto) |
157 by (unfold s_RAG_def s_holding_abv, auto) |
158 qed |
158 qed |
159 |
159 |
160 lemma ancestors_cs: |
160 lemma ancestors_cs: |
161 "ancestors (RAG s) (Cs cs) = {Th th}" |
161 "ancestors (RAG s) (Cs cs) = {Th th}" |
162 proof - |
162 proof - |
185 begin |
185 begin |
186 |
186 |
187 lemma sub_RAGs': |
187 lemma sub_RAGs': |
188 "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s" |
188 "{(Cs cs, Th th), (Th taker, Cs cs)} \<subseteq> RAG s" |
189 using waiting_taker holding_th_cs_s |
189 using waiting_taker holding_th_cs_s |
190 by (unfold s_RAG_def, fold waiting_eq holding_eq, auto) |
190 by (unfold s_RAG_def, fold s_waiting_abv s_holding_abv, auto) |
191 |
191 |
192 lemma ancestors_th': |
192 lemma ancestors_th': |
193 "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" |
193 "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" |
194 proof - |
194 proof - |
195 have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}" |
195 have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}" |
295 case 2 |
295 case 2 |
296 from this(2) have "(n, Cs cs) \<in> (RAG s)^+" |
296 from this(2) have "(n, Cs cs) \<in> (RAG s)^+" |
297 by (auto simp:ancestors_def) |
297 by (auto simp:ancestors_def) |
298 from tranclD2[OF this] |
298 from tranclD2[OF this] |
299 obtain th' where "waiting s th' cs" |
299 obtain th' where "waiting s th' cs" |
300 by (auto simp:s_RAG_def waiting_eq) |
300 by (auto simp:s_RAG_def s_waiting_abv) |
301 with no_waiter_before |
301 with no_waiter_before |
302 show ?thesis by simp |
302 show ?thesis by simp |
303 qed simp |
303 qed simp |
304 } moreover { |
304 } moreover { |
305 fix n |
305 fix n |
388 context valid_trace_p_w |
388 context valid_trace_p_w |
389 begin |
389 begin |
390 |
390 |
391 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" |
391 lemma cs_held: "(Cs cs, Th holder) \<in> RAG s" |
392 using holding_s_holder |
392 using holding_s_holder |
393 by (unfold s_RAG_def, fold holding_eq, auto) |
393 by (unfold s_RAG_def, fold s_holding_abv, auto) |
394 |
394 |
395 lemma tRAG_s: |
395 lemma tRAG_s: |
396 "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" |
396 "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" |
397 using RAG_tRAG_transfer[OF RAG_es cs_held] . |
397 using RAG_tRAG_transfer[OF RAG_es cs_held] . |
398 |
398 |
660 have "Th th \<notin> Range (RAG s)" |
660 have "Th th \<notin> Range (RAG s)" |
661 proof |
661 proof |
662 assume "Th th \<in> Range (RAG s)" |
662 assume "Th th \<in> Range (RAG s)" |
663 then obtain cs where "holding s th cs" |
663 then obtain cs where "holding s th cs" |
664 by (simp add: holdents_RAG holdents_th_s) |
664 by (simp add: holdents_RAG holdents_th_s) |
665 then show False by (unfold holding_eq, auto) |
665 then show False by (unfold s_holding_abv, auto) |
666 qed |
666 qed |
667 moreover have "Th th \<notin> Domain (RAG s)" |
667 moreover have "Th th \<notin> Domain (RAG s)" |
668 proof |
668 proof |
669 assume "Th th \<in> Domain (RAG s)" |
669 assume "Th th \<in> Domain (RAG s)" |
670 then obtain cs where "waiting s th cs" |
670 then obtain cs where "waiting s th cs" |