--- a/RTree.thy	Tue Aug 16 11:49:37 2016 +0100
+++ b/RTree.thy	Wed Aug 24 16:13:20 2016 +0200
@@ -73,12 +73,28 @@
   nodes (including itself) which can reach @{text "x"} by following
   some path in @{text "r"}: *}
 
-definition "subtree r x = {node' . (node', x) \<in> r^*}"
+definition "subtree r x = {y . (y, x) \<in> r^*}"
 
-definition "ancestors r x = {node'. (x, node') \<in> r^+}"
+definition "ancestors r x = {y. (x, y) \<in> r^+}"
 
 definition "root r x = (ancestors r x = {})"
 
+lemma root_indep:
+  assumes "root r x"
+    and "root r y"
+    and "y \<noteq> x"
+  shows "indep r x y"
+proof -
+  { assume "(x, y) \<in> r^*"
+    hence False using assms
+      by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)
+  } moreover {
+    assume "(y, x) \<in> r^*"
+    hence False using assms
+      by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)
+  } ultimately show ?thesis by (auto simp:indep_def)
+qed
+
 text {*
  
   The following @{text "edge_in r x"} is the set of edges contained in
@@ -108,7 +124,7 @@
   shows "(a, b) \<notin> edges_in r x"
   using assms by (unfold edges_in_def subtree_def, auto)
 
-definition "children r x = {node'. (node', x) \<in> r}"
+definition "children r x = {y. (y, x) \<in> r}"
 
 locale fforest = forest +
   assumes fb: "finite (children r x)"
@@ -1067,6 +1083,21 @@
   } thus ?thesis by auto
 qed
 
+lemma root_unique:
+   assumes "x \<in> subtree r y"
+    and "x \<in> subtree r z"
+    and "root r y"
+    and "root r z"
+    shows "y = z" 
+proof -
+  { assume "y \<noteq> z"
+    from root_indep[OF assms(4,3) this]
+    have "indep r z y" .
+    from subtree_disjoint[OF this] and assms
+    have False by auto
+  } thus ?thesis by auto
+qed
+
 text {*
   The following lemma @{text "subtree_del"} characterizes the change of sub-tree of 
   @{text "x"} with the removal of an inside edge @{text "(a, b)"}.