--- a/RTree.thy	Fri Jun 09 15:08:54 2017 +0100
+++ b/RTree.thy	Fri Jun 23 00:27:16 2017 +0100
@@ -693,6 +693,36 @@
   } ultimately show ?thesis by auto
 qed
 
+lemma subset_insert_subtree_outside [simp, intro]: (* ddd *) 
+    assumes "Range r' \<inter> subtree r x = {}" 
+    shows "subtree (r \<union> r') x = (subtree r x)" (is "?L = ?R")
+proof -
+  { have "?L \<subseteq> ?R"
+    proof
+      fix y
+      assume "y \<in> ?L"
+      from this[unfolded subtree_def] have "(y, x) \<in> ( (r \<union> r')^*)" by simp
+      thus "y \<in> ?R"
+      proof(induct rule:converse_rtrancl_induct)
+        case (base)
+        show ?case unfolding subtree_def by auto
+      next
+        case (step x y)
+        moreover have "(x, y) \<in> r"
+        proof - 
+          {  assume "(x, y) \<in> r'"
+             with assms step(3)
+             have False by auto
+          } with step(1) show ?thesis by auto
+        qed
+        ultimately show ?case unfolding subtree_def by auto
+      qed
+    qed
+  } moreover have "?R \<subseteq> ?L" by auto
+  ultimately show ?thesis by auto
+qed
+
+
 lemma subtree_insert_ext [simp, intro]:
     assumes "b \<in> subtree r x"
     shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 
@@ -1806,4 +1836,13 @@
 
 declare RTree.plus_rpath[rule del]
 
+lemma fmap_children:
+  assumes "inj f" 
+  shows  "children ((map_prod f f) ` r) (f s) = f ` (children r s)"
+  using assms
+  apply (unfold children_def map_prod_def, auto)
+  by (drule_tac x = s and y = b in injD, auto)
+
+find_theorems subtree "op \<union>"
+
 end