--- a/RTree.thy	Sun Jan 17 22:18:35 2016 +0800
+++ b/RTree.thy	Wed Jan 27 19:26:56 2016 +0800
@@ -980,6 +980,37 @@
   from that[OF this] show ?thesis .
 qed
 
+lemma rpath_overlap_oneside':
+  assumes "rpath r x xs1 x1" 
+  and "rpath r x xs2 x2"
+  and "length xs1 \<le> length xs2"
+  obtains xs3 where 
+    "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"
+proof -
+  from rpath_overlap_oneside[OF assms]
+  obtain xs3 where eq_xs: "xs2 = xs1 @ xs3" by auto
+  show ?thesis
+  proof(cases "xs1 = []")
+    case True
+    from rpath_nilE[OF assms(1)[unfolded this]]
+    have eq_x1: "x1 = x" .
+    have "xs2 = xs3" using True eq_xs by simp
+    from that[OF eq_xs assms(1) assms(2)[folded eq_x1, unfolded this]]
+    show ?thesis .
+  next
+    case False  
+    from rpath_nnl_lastE[OF assms(1) False]
+    obtain xs' where eq_xs1: "xs1 = xs'@[x1]" by auto
+    from assms(2)[unfolded eq_xs this]
+    have "rpath r x (xs' @ [x1] @ xs3) x2" by simp
+    from rpath_appendE[OF this]
+    have "rpath r x (xs' @ [x1]) x1" "rpath r x1 xs3 x2" by auto
+    from that [OF eq_xs this(1)[folded eq_xs1] this(2)]
+    show ?thesis .
+  qed
+qed
+
+
 lemma rpath_overlap [consumes 2, cases pred:rpath]:
   assumes "rpath r x xs1 x1"
   and "rpath r x xs2 x2"
@@ -990,6 +1021,16 @@
   with assms rpath_overlap_oneside that show ?thesis by metis
 qed
 
+lemma rpath_overlap' [consumes 2, cases pred:rpath]:
+  assumes "rpath r x xs1 x1"
+  and "rpath r x xs2 x2"
+  obtains (less_1) xs3 where "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"
+     |    (less_2) xs3 where "xs1 = xs2 @ xs3" "rpath r x xs2 x2" "rpath r x2 xs3 x1"
+proof -
+  have "length xs1 \<le> length xs2 \<or> length xs2 \<le> length xs1" by auto
+  with assms rpath_overlap_oneside' that show ?thesis by metis
+qed
+
 text {*
   As a corollary of @{thm "rpath_overlap_oneside"}, 
   the following two lemmas gives one important property of relation tree, 
@@ -1399,8 +1440,27 @@
   qed
 qed
 
+end (* of rtree *)
 
-end (* of rtree *)
+lemma subtree_trancl:
+  "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")
+proof -
+  { fix z
+    assume "z \<in> ?L"
+    hence "z \<in> ?R"
+    proof(cases rule:subtreeE)
+      case 2
+      thus ?thesis  
+        by (unfold ancestors_def, auto)
+    qed auto
+  } moreover
+  { fix z
+    assume "z \<in> ?R"
+    hence "z \<in> ?L" 
+      by (unfold subtree_def, auto)
+  } ultimately show ?thesis by auto
+qed
+
 
 lemma subtree_children:
   "subtree r x = {x} \<union> (\<Union> (subtree r ` (children r x)))" (is "?L = ?R")
@@ -1742,4 +1802,45 @@
   using assms
   by (auto simp:children_def)
 
+lemma wf_rbase:
+  assumes "wf r"
+  obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"
+proof -
+  from assms
+  have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)"
+  proof(induct) 
+    case (less x)
+    thus ?case
+    proof(cases "\<exists> z. (z, x) \<in> r")
+      case False
+      moreover have "(x, x) \<in> r^*" by auto
+      ultimately show ?thesis by metis
+    next
+      case True
+      then obtain z where h_z: "(z, x) \<in> r" by auto
+      from less[OF this]
+      obtain b where "(b, z) \<in> r^*" "(\<forall>c. (c, b) \<notin> r)"
+        by auto
+      moreover from this(1) h_z have "(b, x) \<in> r^*" by auto
+      ultimately show ?thesis by metis
+    qed
+  qed
+  with that show ?thesis by metis
+qed
+
+lemma wf_base:
+  assumes "wf r"
+  and "a \<in> Range r"
+  obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"
+proof -
+  from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto
+  from wf_rbase[OF assms(1), of a]
+  obtain b where h_b: "(b, a) \<in> r\<^sup>*" "\<forall>c. (c, b) \<notin> r" by auto
+  from rtranclD[OF this(1)]
+  have "b = a \<or>  b \<noteq> a \<and> (b, a) \<in> r\<^sup>+" by auto
+  moreover have "b \<noteq> a" using h_a h_b(2) by auto
+  ultimately have "(b, a) \<in> r\<^sup>+" by auto
+  with h_b(2) and that show ?thesis by metis
+qed
+
 end
\ No newline at end of file