690 assume "c \<in> subtree (r - r') x" |
690 assume "c \<in> subtree (r - r') x" |
691 moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto) |
691 moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto) |
692 ultimately have "c \<in> (subtree r x)" by auto |
692 ultimately have "c \<in> (subtree r x)" by auto |
693 } ultimately show ?thesis by auto |
693 } ultimately show ?thesis by auto |
694 qed |
694 qed |
|
695 |
|
696 lemma subset_insert_subtree_outside [simp, intro]: (* ddd *) |
|
697 assumes "Range r' \<inter> subtree r x = {}" |
|
698 shows "subtree (r \<union> r') x = (subtree r x)" (is "?L = ?R") |
|
699 proof - |
|
700 { have "?L \<subseteq> ?R" |
|
701 proof |
|
702 fix y |
|
703 assume "y \<in> ?L" |
|
704 from this[unfolded subtree_def] have "(y, x) \<in> ( (r \<union> r')^*)" by simp |
|
705 thus "y \<in> ?R" |
|
706 proof(induct rule:converse_rtrancl_induct) |
|
707 case (base) |
|
708 show ?case unfolding subtree_def by auto |
|
709 next |
|
710 case (step x y) |
|
711 moreover have "(x, y) \<in> r" |
|
712 proof - |
|
713 { assume "(x, y) \<in> r'" |
|
714 with assms step(3) |
|
715 have False by auto |
|
716 } with step(1) show ?thesis by auto |
|
717 qed |
|
718 ultimately show ?case unfolding subtree_def by auto |
|
719 qed |
|
720 qed |
|
721 } moreover have "?R \<subseteq> ?L" by auto |
|
722 ultimately show ?thesis by auto |
|
723 qed |
|
724 |
695 |
725 |
696 lemma subtree_insert_ext [simp, intro]: |
726 lemma subtree_insert_ext [simp, intro]: |
697 assumes "b \<in> subtree r x" |
727 assumes "b \<in> subtree r x" |
698 shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" |
728 shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" |
699 using assms by (auto simp:subtree_def rtrancl_insert) |
729 using assms by (auto simp:subtree_def rtrancl_insert) |