--- a/RTree.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/RTree.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -21,7 +21,7 @@
 *}
 
 
-locale rtree = 
+locale forest = 
   fixes r
   assumes sgv: "single_valued r"
   assumes acl: "acyclic r"
@@ -110,7 +110,7 @@
 
 definition "children r x = {y. (y, x) \<in> r}"
 
-locale fgraph = rtree +
+locale fforest = forest +
   assumes fb: "finite (children r x)"
   assumes wf: "wf r"
 begin
@@ -721,7 +721,7 @@
 
 subsubsection {* Properties about relational trees *}
 
-context rtree 
+context forest 
 begin
 
 lemma ancestors_headE:
@@ -1350,7 +1350,7 @@
   qed
 qed
 
-end (* of rtree *)
+end (* of forest *)
 
 lemma subtree_trancl:
   "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")
@@ -1385,7 +1385,7 @@
   "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
   by fast
 
-context fgraph
+context fforest
 begin
   
 lemma finite_subtree:
@@ -1557,19 +1557,6 @@
   } thus ?thesis by (auto simp:acyclic_def)
 qed
 
-lemma relpow_mult: 
-  "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
-proof(induct n arbitrary:m)
-  case (Suc k m)
-  thus ?case
-  proof -
-    have h: "(m * k + m) = (m + m * k)" by auto
-    show ?thesis 
-      apply (simp add:Suc relpow_add[symmetric])
-      by (unfold h, simp)
-  qed
-qed simp
-
 lemma compose_relpow_2 [intro, simp]:
   assumes "r1 \<subseteq> r"
   and "r2 \<subseteq> r"
@@ -1584,6 +1571,19 @@
   } thus ?thesis by (auto simp:numeral_2_eq_2)
 qed
 
+lemma relpow_mult: 
+  "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
+proof(induct n arbitrary:m)
+  case (Suc k m)
+  thus ?case
+  proof -
+    have h: "(m * k + m) = (m + m * k)" by auto
+    show ?thesis 
+      apply (simp add:Suc relpow_add[symmetric])
+      by (unfold h, simp)
+  qed
+qed simp
+
 lemma acyclic_compose [intro, simp]:
   assumes "acyclic r"
   and "r1 \<subseteq> r"
@@ -1623,7 +1623,7 @@
       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 fgraph_def] this
+        from assms(2)[unfolded fforest_def] this
         show "finite (children r2 x)" by auto
       qed
      next
@@ -1637,7 +1637,7 @@
        next
           case False
           hence "y \<in> Range r1" by (unfold children_def, auto)
-          from assms(1)[unfolded fgraph_def] this h1(2)
+          from assms(1)[unfolded fforest_def] this h1(2)
           show ?thesis by auto
        qed
      qed