--- a/PIPBasics.thy	Mon Jul 04 14:04:11 2016 +0100
+++ b/PIPBasics.thy	Thu Jul 07 13:32:09 2016 +0100
@@ -2846,8 +2846,9 @@
 
 sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
 proof
-  show "\<forall>x\<in>Range (RAG s). finite (children (RAG s) x)" 
-    by (rule finite_fbranchI[OF finite_RAG])
+  show "\<And>x. finite (children (RAG s) x)"
+    by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) 
+    (*by (rule finite_fbranchI[OF finite_RAG])*)
 next
   show "wf (RAG s)" using wf_RAG .
 qed
@@ -2892,21 +2893,22 @@
   from acyclic_tRAG show "acyclic (tRAG s)" .
 qed
 
+
 sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
 proof
-  show "\<forall>x\<in>Range (tRAG s). finite (children (tRAG s) x)"
-  proof(unfold tRAG_def, rule fbranch_compose)
-        show "\<forall>x\<in>Range (wRAG s). finite (children (wRAG s) x)"
-        proof(rule finite_fbranchI)
-           from finite_RAG show "finite (wRAG s)"
-           by (unfold RAG_split, auto)
-        qed
-    next
-        show "\<forall>x\<in>Range (hRAG s). finite (children (hRAG s) x)"
-        proof(rule finite_fbranchI)
-           from finite_RAG 
-           show "finite (hRAG s)" by (unfold RAG_split, auto)
-        qed
+  fix x
+  show "finite (children (tRAG s) x)"
+  proof(unfold tRAG_def, rule fbranch_compose1[rule_format])
+    fix x show "finite (children (wRAG s) x)" 
+    proof(rule finite_fbranchI1[rule_format])
+      show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto
+    qed
+  next
+    fix x
+    show "finite (children (hRAG s) x)"
+    proof(rule finite_fbranchI1[rule_format])
+      show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto
+    qed
   qed
 next
   show "wf (tRAG s)"

--- a/RTree.thy	Mon Jul 04 14:04:11 2016 +0100
+++ b/RTree.thy	Thu Jul 07 13:32:09 2016 +0100
@@ -110,9 +110,8 @@
 
 definition "children r x = {y. (y, x) \<in> r}"
 
-locale fgraph =
-  fixes r
-  assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
+locale fgraph = rtree +
+  assumes fb: "finite (children r x)"
   assumes wf: "wf r"
 begin
 
@@ -1402,7 +1401,7 @@
     next
       case False
       hence "x \<in> Range r" by (auto simp:children_def)
-      from fb[rule_format, OF this] 
+      from fb 
       have "finite (children r x)" .
       thus ?thesis by (rule finite_imageI)
     qed
@@ -1645,6 +1644,14 @@
   } thus ?thesis using assms by auto
 qed
 
+lemma fbranch_compose1 [intro, simp]:
+  assumes "\<forall>x. finite (children r1 x)"
+  and "\<forall>x. finite (children r2 x)"
+  shows "\<forall>x. finite (children (r1 O r2) x)"
+by (metis (no_types, lifting) Collect_empty_eq Range.intros assms(1) 
+         assms(2) children_def fbranch_compose finite.emptyI)
+
+
 lemma finite_fbranchI [intro]:
   assumes "finite r"
   shows "\<forall> x \<in> Range r . finite (children r x)"
@@ -1661,6 +1668,12 @@
   } thus ?thesis by auto
 qed
 
+lemma finite_fbranchI1 [intro]:
+  assumes "finite r"
+  shows "\<forall> x . finite (children r x)"
+  by (metis (no_types, lifting) Collect_empty_eq Range.intros assms 
+      children_def finite.emptyI finite_fbranchI)
+
 lemma subset_fbranchI [intro]:
   assumes "\<forall> x \<in> Range r1 . finite (children r1 x)"
   and "r2 \<subseteq> r1"