diff -r 6a7a8c51d42f -r d9974794436a RTree.thy
--- a/RTree.thy	Mon Jun 27 14:08:21 2016 +0100
+++ b/RTree.thy	Mon Jul 04 14:04:11 2016 +0100
@@ -110,9 +110,10 @@
 
 definition "children r x = {y. (y, x) \<in> r}"
 
-locale fbranch =
+locale fgraph =
   fixes r
   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
+  assumes wf: "wf r"
 begin
 
 lemma finite_children: "finite (children r x)"
@@ -120,8 +121,6 @@
 
 end
 
-locale fsubtree = fbranch + 
-   assumes wf: "wf r"
 
 subsection {* Auxiliary lemmas *}
 
@@ -1387,7 +1386,7 @@
   "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
   by fast
 
-context fsubtree 
+context fgraph
 begin
   
 lemma finite_subtree:
@@ -1613,9 +1612,9 @@
   by (auto simp:children_def)
 
 lemma fbranch_compose [intro, simp]:
-  assumes "fbranch r1"
-  and "fbranch r2"
-  shows "fbranch (r1 O r2)"
+  assumes "\<forall> x \<in> Range r1 . finite (children r1 x)"
+  and "\<forall> x \<in> Range r2 . finite (children r2 x)"
+  shows "\<forall> x \<in> Range (r1 O r2) . finite (children (r1 O r2) x)"
 proof -
   {  fix x
      assume "x\<in>Range (r1 O r2)"
@@ -1625,8 +1624,8 @@
       show "finite (children r1 ` children r2 x)"
       proof(rule finite_imageI)
         from h(2) have "x \<in> Range r2" by auto
-        from assms(2)[unfolded fbranch_def, rule_format, OF this]
-        show "finite (children r2 x)" .
+        from assms(2)[unfolded fgraph_def] this
+        show "finite (children r2 x)" by auto
       qed
      next
        fix M
@@ -1639,16 +1638,16 @@
        next
           case False
           hence "y \<in> Range r1" by (unfold children_def, auto)
-          from assms(1)[unfolded fbranch_def, rule_format, OF this, folded h1(2)]
-          show ?thesis .
+          from assms(1)[unfolded fgraph_def] this h1(2)
+          show ?thesis by auto
        qed
      qed
-  } thus ?thesis by (unfold fbranch_def, auto)
+  } thus ?thesis using assms by auto
 qed
 
 lemma finite_fbranchI [intro]:
   assumes "finite r"
-  shows "fbranch r"
+  shows "\<forall> x \<in> Range r . finite (children r x)"
 proof -
   { fix x 
     assume "x \<in>Range r"
@@ -1659,25 +1658,25 @@
       have "finite {y. (y, x) \<in> r}" .
       thus ?thesis by (unfold children_def, simp)
     qed
-  } thus ?thesis by (auto simp:fbranch_def)
+  } thus ?thesis by auto
 qed
 
 lemma subset_fbranchI [intro]:
-  assumes "fbranch r1"
+  assumes "\<forall> x \<in> Range r1 . finite (children r1 x)"
   and "r2 \<subseteq> r1"
-  shows "fbranch r2"
+  shows "\<forall> x \<in> Range r2 . finite (children r2 x)"
 proof -
   { fix x
     assume "x \<in>Range r2"
     with assms(2) have "x \<in> Range r1" by auto
-    from assms(1)[unfolded fbranch_def, rule_format, OF this]
+    from assms(1)[rule_format, OF this]
     have "finite (children r1 x)" .
     hence "finite (children r2 x)"
     proof(rule rev_finite_subset)
       from assms(2)
       show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def)
     qed
-  } thus ?thesis by (auto simp:fbranch_def)
+  } thus ?thesis by auto
 qed
 
 lemma children_subtree [simp, intro]: