983 lemma rpath_overlap_oneside':

   984   assumes "rpath r x xs1 x1" 

   985   and "rpath r x xs2 x2"

   986   and "length xs1 \<le> length xs2"

   987   obtains xs3 where 

   988     "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"

   989 proof -

   990   from rpath_overlap_oneside[OF assms]

   991   obtain xs3 where eq_xs: "xs2 = xs1 @ xs3" by auto

   992   show ?thesis

   993   proof(cases "xs1 = []")

   994     case True

   995     from rpath_nilE[OF assms(1)[unfolded this]]

   996     have eq_x1: "x1 = x" .

   997     have "xs2 = xs3" using True eq_xs by simp

   998     from that[OF eq_xs assms(1) assms(2)[folded eq_x1, unfolded this]]

   999     show ?thesis .

  1000   next

  1001     case False  

  1002     from rpath_nnl_lastE[OF assms(1) False]

  1003     obtain xs' where eq_xs1: "xs1 = xs'@[x1]" by auto

  1004     from assms(2)[unfolded eq_xs this]

  1005     have "rpath r x (xs' @ [x1] @ xs3) x2" by simp

  1006     from rpath_appendE[OF this]

  1007     have "rpath r x (xs' @ [x1]) x1" "rpath r x1 xs3 x2" by auto

  1008     from that [OF eq_xs this(1)[folded eq_xs1] this(2)]

  1009     show ?thesis .

  1010   qed

  1011 qed

  1012 

  1013 

  1022 qed

  1023 

  1024 lemma rpath_overlap' [consumes 2, cases pred:rpath]:

  1025   assumes "rpath r x xs1 x1"

  1026   and "rpath r x xs2 x2"

  1027   obtains (less_1) xs3 where "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"

  1028      |    (less_2) xs3 where "xs1 = xs2 @ xs3" "rpath r x xs2 x2" "rpath r x2 xs3 x1"

  1029 proof -

  1030   have "length xs1 \<le> length xs2 \<or> length xs2 \<le> length xs1" by auto

  1031   with assms rpath_overlap_oneside' that show ?thesis by metis

  1444 

  1445 lemma subtree_trancl:

  1446   "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")

  1447 proof -

  1448   { fix z

  1449     assume "z \<in> ?L"

  1450     hence "z \<in> ?R"

  1451     proof(cases rule:subtreeE)

  1452       case 2

  1453       thus ?thesis  

  1454         by (unfold ancestors_def, auto)

  1455     qed auto

  1456   } moreover

  1457   { fix z

  1458     assume "z \<in> ?R"

  1459     hence "z \<in> ?L" 

  1460       by (unfold subtree_def, auto)

  1461   } ultimately show ?thesis by auto

  1462 qed

  1463 

  1805 lemma wf_rbase:

  1806   assumes "wf r"

  1807   obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"

  1808 proof -

  1809   from assms

  1810   have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)"

  1811   proof(induct) 

  1812     case (less x)

  1813     thus ?case

  1814     proof(cases "\<exists> z. (z, x) \<in> r")

  1815       case False

  1816       moreover have "(x, x) \<in> r^*" by auto

  1817       ultimately show ?thesis by metis

  1818     next

  1819       case True

  1820       then obtain z where h_z: "(z, x) \<in> r" by auto

  1821       from less[OF this]

  1822       obtain b where "(b, z) \<in> r^*" "(\<forall>c. (c, b) \<notin> r)"

  1823         by auto

  1824       moreover from this(1) h_z have "(b, x) \<in> r^*" by auto

  1825       ultimately show ?thesis by metis

  1826     qed

  1827   qed

  1828   with that show ?thesis by metis

  1829 qed

  1830 

  1831 lemma wf_base:

  1832   assumes "wf r"

  1833   and "a \<in> Range r"

  1834   obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"

  1835 proof -

  1836   from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto

  1837   from wf_rbase[OF assms(1), of a]

  1838   obtain b where h_b: "(b, a) \<in> r\<^sup>*" "\<forall>c. (c, b) \<notin> r" by auto

  1839   from rtranclD[OF this(1)]

  1840   have "b = a \<or>  b \<noteq> a \<and> (b, a) \<in> r\<^sup>+" by auto

  1841   moreover have "b \<noteq> a" using h_a h_b(2) by auto

  1842   ultimately have "(b, a) \<in> r\<^sup>+" by auto

  1843   with h_b(2) and that show ?thesis by metis

  1844 qed

  1845