239 |
239 |
240 |
240 |
241 context valid_trace_v_e |
241 context valid_trace_v_e |
242 begin |
242 begin |
243 |
243 |
244 find_theorems RAG s e |
|
245 |
|
246 lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" |
244 lemma RAG_s: "RAG (e#s) = RAG s - {(Cs cs, Th th)}" |
247 by (unfold RAG_es waiting_set_eq holding_set_eq, simp) |
245 by (unfold RAG_es waiting_set_eq holding_set_eq, simp) |
248 |
246 |
249 lemma subtree_kept: |
247 lemma subtree_kept: |
250 assumes "th1 \<noteq> th" |
248 assumes "th1 \<noteq> th" |
267 assumes "th1 \<noteq> th" |
265 assumes "th1 \<noteq> th" |
268 shows "cp (e#s) th1 = cp s th1" |
266 shows "cp (e#s) th1 = cp s th1" |
269 by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) |
267 by (unfold cp_alt_def the_preced_es subtree_kept[OF assms], simp) |
270 |
268 |
271 lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" |
269 lemma subtree_cs: "subtree (RAG s) (Cs cs) = {Cs cs}" |
|
270 (is "?L = ?R") |
272 proof - |
271 proof - |
273 { fix n |
272 { fix n |
274 have "(Cs cs) \<notin> ancestors (RAG s) n" |
273 assume "n \<in> ?L" |
275 proof |
274 hence "n \<in> ?R" |
276 assume "Cs cs \<in> ancestors (RAG s) n" |
275 proof(cases rule:subtreeE) |
277 hence "(n, Cs cs) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
276 case 2 |
278 from tranclE[OF this] obtain nn where h: "(nn, Cs cs) \<in> RAG s" by auto |
277 from this(2) have "(n, Cs cs) \<in> (RAG s)^+" |
279 then obtain th' where "nn = Th th'" |
278 by (auto simp:ancestors_def) |
280 by (unfold s_RAG_def, auto) |
279 from tranclD2[OF this] |
281 from h[unfolded this] have "(Th th', Cs cs) \<in> RAG s" . |
280 obtain th' where "waiting s th' cs" |
282 from this[unfolded s_RAG_def] |
281 by (auto simp:s_RAG_def waiting_eq) |
283 have "waiting (wq s) th' cs" by auto |
282 with no_waiter_before |
284 from this[unfolded cs_waiting_def] |
283 show ?thesis by simp |
285 have "1 < length (wq s cs)" |
284 qed simp |
286 by (cases "wq s cs", auto) |
285 } moreover { |
287 from holding_next_thI[OF holding_th_cs_s this] |
286 fix n |
288 obtain th' where "next_th s th cs th'" by auto |
287 assume "n \<in> ?R" |
289 thus False using no_taker by blast |
288 hence "n \<in> ?L" by (auto simp:subtree_def) |
290 qed |
289 } ultimately show ?thesis by auto |
291 } note h = this |
290 qed |
292 { fix n |
291 |
293 assume "n \<in> subtree (RAG s) (Cs cs)" |
|
294 hence "n = (Cs cs)" |
|
295 by (elim subtreeE, insert h, auto) |
|
296 } moreover have "(Cs cs) \<in> subtree (RAG s) (Cs cs)" |
|
297 by (auto simp:subtree_def) |
|
298 ultimately show ?thesis by auto |
|
299 qed |
|
300 |
292 |
301 lemma subtree_th: |
293 lemma subtree_th: |
302 "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" |
294 "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" |
303 proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) |
295 proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) |
304 from edge_of_th |
296 from edge_of_th |