equal
deleted
inserted
replaced
593 proof - |
593 proof - |
594 from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def) |
594 from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def) |
595 from rtranclD[OF this] |
595 from rtranclD[OF this] |
596 have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" . |
596 have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" . |
597 with that[unfolded ancestors_def] show ?thesis by auto |
597 with that[unfolded ancestors_def] show ?thesis by auto |
|
598 qed |
|
599 |
|
600 |
|
601 lemma subtree_Field: |
|
602 "subtree r x \<subseteq> Field r \<union> {x}" |
|
603 proof |
|
604 fix y |
|
605 assume "y \<in> subtree r x" |
|
606 thus "y \<in> Field r \<union> {x}" |
|
607 proof(cases rule:subtreeE) |
|
608 case 1 |
|
609 thus ?thesis by auto |
|
610 next |
|
611 case 2 |
|
612 thus ?thesis apply (auto simp:ancestors_def) |
|
613 using Field_def tranclD by fastforce |
|
614 qed |
598 qed |
615 qed |
599 |
616 |
600 lemma subtree_ancestorsI: |
617 lemma subtree_ancestorsI: |
601 assumes "a \<in> subtree r b" |
618 assumes "a \<in> subtree r b" |
602 and "a \<noteq> b" |
619 and "a \<noteq> b" |