# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1467637451 -3600
# Node ID d9974794436a2d34b0e8ff6458e991354e699e37
# Parent  6a7a8c51d42ff8ef595d10a27ef4d1c8604ab6b1
added version with fgraphs

diff -r 6a7a8c51d42f -r d9974794436a PIPBasics.thy
--- a/PIPBasics.thy	Mon Jun 27 14:08:21 2016 +0100
+++ b/PIPBasics.thy	Mon Jul 04 14:04:11 2016 +0100
@@ -2844,17 +2844,12 @@
 sublocale valid_trace < rtree_RAG?: rtree "RAG s"
   using rtree_RAG .
 
-sublocale valid_trace < fsbtRAGs?: fsubtree "RAG s"
-proof -
-  show "fsubtree (RAG s)"
-  proof(intro_locales)
-    show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
-  next
-    show "fsubtree_axioms (RAG s)"
-    proof(unfold fsubtree_axioms_def)
-      from wf_RAG show "wf (RAG s)" .
-    qed
-  qed
+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])
+next
+  show "wf (RAG s)" using wf_RAG .
 qed
 
 subsection {* Derived properties for sub-graphs of RAG *}
@@ -2897,36 +2892,31 @@
   from acyclic_tRAG show "acyclic (tRAG s)" .
 qed
 
-sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s"
-proof -
-  have "fsubtree (tRAG s)"
-  proof -
-    have "fbranch (tRAG s)"
-    proof(unfold tRAG_def, rule fbranch_compose)
-        show "fbranch (wRAG s)"
+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 "fbranch (hRAG s)"
+        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
-    qed
-    moreover have "wf (tRAG s)"
-    proof(rule wf_subset)
+  qed
+next
+  show "wf (tRAG s)"
+  proof(rule wf_subset)
       show "wf (RAG s O RAG s)" using wf_RAG
         by (fold wf_comp_self, simp)
-    next
+  next
       show "tRAG s \<subseteq> (RAG s O RAG s)"
         by (unfold tRAG_alt_def, auto)
-    qed
-    ultimately show ?thesis
-      by (unfold fsubtree_def fsubtree_axioms_def,auto)
   qed
-  from this[folded tRAG_def] show "fsubtree (tRAG s)" .
 qed
 
 section {* Chain to readys *}
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]: