equal
deleted
inserted
replaced
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 - |
163 have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \<union> {Th th}" |
163 have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th) \<union> {Th th}" |
164 by (rule rtree_RAG.ancestors_accum[OF edge_of_th]) |
164 by (rule forest_RAG.ancestors_accum[OF edge_of_th]) |
165 from this[unfolded ancestors_th] show ?thesis by simp |
165 from this[unfolded ancestors_th] show ?thesis by simp |
166 qed |
166 qed |
167 |
167 |
168 end |
168 end |
169 |
169 |
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}" |
196 proof(rule rtree_RAG.ancestors_accum) |
196 proof(rule forest_RAG.ancestors_accum) |
197 from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto |
197 from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto |
198 qed |
198 qed |
199 thus ?thesis using ancestors_th ancestors_cs by auto |
199 thus ?thesis using ancestors_th ancestors_cs by auto |
200 qed |
200 qed |
201 |
201 |
309 qed |
309 qed |
310 |
310 |
311 |
311 |
312 lemma subtree_th: |
312 lemma subtree_th: |
313 "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" |
313 "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}" |
314 proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside) |
314 proof(unfold RAG_s, fold subtree_cs, rule forest_RAG.subtree_del_inside) |
315 from edge_of_th |
315 from edge_of_th |
316 show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)" |
316 show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)" |
317 by (unfold edges_in_def, auto simp:subtree_def) |
317 by (unfold edges_in_def, auto simp:subtree_def) |
318 qed |
318 qed |
319 |
319 |
480 proof(rule f_image_eq) |
480 proof(rule f_image_eq) |
481 fix a |
481 fix a |
482 assume a_in: "a \<in> ?A" |
482 assume a_in: "a \<in> ?A" |
483 from 1(2) |
483 from 1(2) |
484 show "?f a = ?g a" |
484 show "?f a = ?g a" |
485 proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch]) |
485 proof(cases rule:vat_es.forest_s.ancestors_childrenE[case_names in_ch out_ch]) |
486 case in_ch |
486 case in_ch |
487 show ?thesis |
487 show ?thesis |
488 proof(cases "a = u") |
488 proof(cases "a = u") |
489 case True |
489 case True |
490 from assms(2)[folded this] show ?thesis . |
490 from assms(2)[folded this] show ?thesis . |
492 case False |
492 case False |
493 have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
493 have a_not_in: "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
494 proof |
494 proof |
495 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
495 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
496 have "a = u" |
496 have "a = u" |
497 proof(rule vat_es.rtree_s.ancestors_children_unique) |
497 proof(rule vat_es.forest_s.ancestors_children_unique) |
498 from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
498 from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
499 RTree.children (tRAG (e#s)) x" by auto |
499 RTree.children (tRAG (e#s)) x" by auto |
500 next |
500 next |
501 from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
501 from assms(1) in_ch show "u \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
502 RTree.children (tRAG (e#s)) x" by auto |
502 RTree.children (tRAG (e#s)) x" by auto |
526 by (auto simp:RTree.children_def tRAG_alt_def) |
526 by (auto simp:RTree.children_def tRAG_alt_def) |
527 have "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
527 have "a \<notin> ancestors (tRAG (e#s)) (Th th)" |
528 proof |
528 proof |
529 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
529 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)" |
530 have "a = z" |
530 have "a = z" |
531 proof(rule vat_es.rtree_s.ancestors_children_unique) |
531 proof(rule vat_es.forest_s.ancestors_children_unique) |
532 from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" |
532 from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)" |
533 by (auto simp:ancestors_def) |
533 by (auto simp:ancestors_def) |
534 with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
534 with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter> |
535 RTree.children (tRAG (e#s)) x" by auto |
535 RTree.children (tRAG (e#s)) x" by auto |
536 next |
536 next |