Theory Graph_Theory.Vertex_Walk

(* Title:  Vertex_Walk.thy
   Author: Lars Noschinski, TU München
*)

theory Vertex_Walk
imports Arc_Walk
begin

section ‹Walks Based on Vertices›

text ‹
  These definitions are here mainly for historical purposes, as they
  do not really work with multigraphs. Consider using Arc Walks
  instead.
›

type_synonym 'a vwalk = "'a list"

text ‹Computes the list of arcs belonging to a list of nodes›
fun vwalk_arcs :: "'a vwalk ⇒ ('a × 'a) list" where
    "vwalk_arcs [] = []"
  | "vwalk_arcs [x] = []"
  | "vwalk_arcs (x#y#xs) = (x,y) # vwalk_arcs (y#xs)"

definition vwalk_length :: "'a vwalk ⇒ nat" where
  "vwalk_length p ≡ length (vwalk_arcs p)"

lemma vwalk_length_simp[simp]:
  shows "vwalk_length p = length p - 1"
by (induct p rule: vwalk_arcs.induct) (auto simp: vwalk_length_def)

definition vwalk :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where
  "vwalk p G ≡ set p ⊆ verts G ∧ set (vwalk_arcs p) ⊆ arcs_ends G ∧ p ≠ []"

definition vpath :: "'a vwalk ⇒ ('a,'b) pre_digraph ⇒ bool" where
  "vpath p G ≡ vwalk p G ∧ distinct p"

text ‹For a given vwalk, compute a vpath with the same tail G and end›
function vwalk_to_vpath :: "'a vwalk ⇒ 'a vwalk" where
    "vwalk_to_vpath [] = []"
  | "vwalk_to_vpath (x # xs) = (if (x ∈ set xs)
      then vwalk_to_vpath (dropWhile (λy. y ≠ x) xs)
      else x # vwalk_to_vpath xs)"
by pat_completeness auto
termination by (lexicographic_order simp add: length_dropWhile_le)


lemma vwalkI[intro]:
  assumes "set p ⊆ verts G"
  assumes "set (vwalk_arcs p) ⊆ arcs_ends G"
  assumes "p ≠ []"
  shows "vwalk p G"
using assms by (auto simp add: vwalk_def)

lemma vwalkE[elim]:
  assumes "vwalk p G"
  assumes "set p ⊆ verts G ⟹
    set (vwalk_arcs p) ⊆ arcs_ends G ∧ p ≠ [] ⟹ P"
  shows "P"
using assms by (simp add: vwalk_def)

lemma vpathI[intro]:
  assumes "vwalk p G"
  assumes "distinct p"
  shows "vpath p G"
using assms by (simp add: vpath_def)

lemma vpathE[elim]:
  assumes "vpath p G"
  assumes "vwalk p G ⟹ distinct p ⟹ P"
  shows "P"
using assms by (simp add: vpath_def)


lemma vwalk_consI:
  assumes "vwalk p G"
  assumes "a ∈ verts G"
  assumes "(a, hd p) ∈ arcs_ends G"
  shows "vwalk (a # p) G"
using assms by (cases p) (auto simp add: vwalk_def)

lemma vwalk_consE:
  assumes "vwalk (a # p) G"
  assumes "p ≠ []"
  assumes "(a, hd p) ∈ arcs_ends G ⟹ vwalk p G ⟹ P"
  shows "P"
using assms by (cases p) (auto simp add: vwalk_def)

lemma vwalk_induct[case_names Base Cons, induct pred: vwalk]:
  assumes "vwalk p G"
  assumes "⋀u. u ∈ verts G ⟹ P [u]"
  assumes "⋀u v es. (u,v) ∈ arcs_ends G ⟹ P (v # es) ⟹ P (u # v # es)"
  shows "P p"
  using assms
proof (induct p)
  case (Cons u es)
  then show ?case
  proof (cases es)
    fix v es' assume "es = v # es'"
    then have "(u,v) ∈ arcs_ends G" and "P (v # es')"
      using Cons by (auto elim: vwalk_consE)
    then show ?thesis using ‹es = v # es'› Cons.prems by auto
  qed auto
qed auto

lemma vwalk_arcs_Cons[simp]:
  assumes "p ≠ []"
  shows "vwalk_arcs (u # p) = (u, hd p) # vwalk_arcs p"
using assms by (cases p) simp+

lemma vwalk_arcs_append:
  assumes "p ≠ []" and "q ≠ []"
  shows "vwalk_arcs (p @ q) = vwalk_arcs p @ (last p, hd q) # vwalk_arcs q" 
proof -
  from assms obtain a b p' q' where "p = a # p'" and "q = b # q'"
    by (auto simp add: neq_Nil_conv)
  moreover
  have "vwalk_arcs ((a # p') @ (b # q'))
    = vwalk_arcs (a # p') @ (last (a # p'), b) # vwalk_arcs (b # q')" 
  proof (induct p')
    case Nil show ?case by simp
  next
    case (Cons a' p') then show ?case by (auto simp add: neq_Nil_conv)
  qed
  ultimately
  show ?thesis by auto
qed

lemma set_vwalk_arcs_append1:
  "set (vwalk_arcs p) ⊆ set (vwalk_arcs (p @ q))" 
proof (cases p)
  case (Cons a p') note p_Cons = Cons then show ?thesis
  proof (cases q)
    case (Cons b q')
    with p_Cons  have "p ≠ []" and "q ≠ []" by auto
    then show ?thesis  by (auto simp add: vwalk_arcs_append)
  qed simp
qed simp

lemma set_vwalk_arcs_append2:
  "set (vwalk_arcs q) ⊆ set (vwalk_arcs (p @ q))" 
proof (cases p)
  case (Cons a p') note p_Cons = Cons then show ?thesis
  proof (cases q)
    case (Cons b q')
    with p_Cons have "p ≠ []" and "q ≠ []" by auto
    then show ?thesis by (auto simp add: vwalk_arcs_append)
  qed simp
qed simp

lemma set_vwalk_arcs_cons:
  "set (vwalk_arcs p) ⊆ set (vwalk_arcs (u # p))"
  by (cases p) auto

lemma set_vwalk_arcs_snoc:
  assumes "p ≠ []"
  shows "set (vwalk_arcs (p @ [a]))
    = insert (last p, a) (set (vwalk_arcs p))"
using assms proof (induct p)
  case Nil then show ?case by auto
next
  case (Cons x xs)
  then show ?case
  proof (cases "xs = []")
    case True then show ?thesis by auto
  next
    case False
    have "set (vwalk_arcs ((x # xs) @ [a]))
      = set (vwalk_arcs (x # (xs @ [a])))"
      by auto
    then show ?thesis using Cons and False
      by (auto simp add: set_vwalk_arcs_cons)
  qed
qed

lemma (in wf_digraph) vwalk_wf_digraph_consI:
  assumes "vwalk p G"
  assumes "(a, hd p) ∈ arcs_ends G"
  shows "vwalk (a # p) G"
proof
  show "a # p ≠ []" by simp

  from assms have "a ∈ verts G" and "set p ⊆ verts G" by auto
  then show "set (a # p) ⊆ verts G" by auto

  from ‹vwalk p G› have "p ≠ []" by auto
  then show "set (vwalk_arcs (a # p)) ⊆ arcs_ends G"
    using ‹vwalk p G› and ‹(a, hd p) ∈ arcs_ends G›
    by (auto simp add: set_vwalk_arcs_cons)
qed

lemma vwalkI_append_l:
  assumes "p ≠ []"
  assumes "vwalk (p @ q) G"
  shows "vwalk p G"
proof
  from assms show "p ≠ []" and "set p ⊆ verts G"
    by (auto elim!: vwalkE)
  have "set (vwalk_arcs p) ⊆ set (vwalk_arcs (p @ q))"
    by (auto simp add: set_vwalk_arcs_append1)
  then show "set (vwalk_arcs p) ⊆ arcs_ends G"
    using assms by blast
qed

lemma vwalkI_append_r:
  assumes "q ≠ []"
  assumes "vwalk (p @ q) G"
  shows "vwalk q G"
proof
  from ‹vwalk (p @ q) G› have "set (p @ q) ⊆ verts G" by blast
  then show "set q ⊆ verts G" by simp

  from ‹vwalk (p @ q) G› have "set (vwalk_arcs (p @ q)) ⊆ arcs_ends G"
    by blast
  then show "set (vwalk_arcs q) ⊆ arcs_ends G"
    by (metis set_vwalk_arcs_append2 subset_trans)

  from ‹q ≠ []› show "q ≠ []" by assumption
qed

lemma vwalk_to_vpath_hd: "hd (vwalk_to_vpath xs) = hd xs"
proof (induct xs rule: vwalk_to_vpath.induct)
  case (2 x xs) then show ?case
  proof (cases "x ∈ set xs")
    case True
    then have "hd (dropWhile (λy. y ≠ x) xs) = x"
      using hd_dropWhile[where P="λy. y ≠ x"] by auto
    then show ?thesis using True and 2 by auto
  qed auto
qed auto

lemma vwalk_to_vpath_induct3[consumes 0, case_names base in_set not_in_set]:
  assumes "P []"
  assumes "⋀x xs. x ∈ set xs ⟹ P (dropWhile (λy. y ≠ x) xs)
    ⟹ P (x # xs)"
  assumes "⋀x xs. x ∉ set xs ⟹ P xs ⟹ P (x # xs)"
  shows "P xs"
using assms by (induct xs rule: vwalk_to_vpath.induct) auto

lemma vwalk_to_vpath_nonempty:
  assumes "p ≠ []"
  shows "vwalk_to_vpath p ≠ []"
using assms by (induct p rule: vwalk_to_vpath_induct3) auto

lemma vwalk_to_vpath_last:
  "last (vwalk_to_vpath xs) = last xs"
by (induct xs rule: vwalk_to_vpath_induct3)
   (auto simp add: dropWhile_last vwalk_to_vpath_nonempty)

lemma vwalk_to_vpath_subset:
  assumes "x ∈ set (vwalk_to_vpath xs)"
  shows "x ∈ set xs"
using assms proof (induct xs rule: vwalk_to_vpath.induct)
  case (2 x xs) then show ?case
    by (cases "x ∈ set xs") (auto dest: set_dropWhileD)
qed simp_all

lemma vwalk_to_vpath_cons:
  assumes "x ∉ set xs"
  shows "vwalk_to_vpath (x # xs) = x # vwalk_to_vpath xs"
using assms by auto

lemma vwalk_to_vpath_vpath:
  assumes "vwalk p G"
  shows "vpath (vwalk_to_vpath p) G"
using assms proof (induct p rule: vwalk_to_vpath_induct3)
  case base then show ?case by auto
next
  case (in_set x xs)
  have set_neq: "⋀x xs. x ∉ set xs ⟹ ∀x' ∈ set xs. x' ≠ x" by metis
  from ‹x ∈ set xs› obtain ys zs where "xs = ys @ x # zs" and "x ∉ set ys"
    by (metis in_set_conv_decomp_first)
  then have vwalk_dW: "vwalk (dropWhile (λy. y ≠ x) xs) G"
    using in_set and ‹xs = ys @ x # zs›
    by (auto simp add: dropWhile_append3 set_neq intro: vwalkI_append_r[where p="x # ys"])
  then show ?case using in_set
    by (auto simp add: vwalk_dW)
next
  case (not_in_set x xs)
  then have "x ∈ verts G" and x_notin: "x ∉ set (vwalk_to_vpath xs)"
    by (auto intro: vwalk_to_vpath_subset)

  from not_in_set show ?case
  proof (cases "xs")
    case Nil then show ?thesis using not_in_set.prems by auto
  next
    case (Cons x' xs')
    have "vpath (vwalk_to_vpath xs) G"
      apply (rule not_in_set)
      apply (rule vwalkI_append_r[where p="[x]"])
       using Cons not_in_set by auto
    then have "vwalk (x # vwalk_to_vpath xs) G"
      apply (auto intro!: vwalk_consI simp add: vwalk_to_vpath_hd)
       using not_in_set
       apply -
       apply (erule vwalk_consE)
        using Cons
        apply (auto intro: ‹x ∈ verts G›)
      done
    then have "vpath (x # vwalk_to_vpath xs) G"
      apply (rule vpathI)
      using ‹vpath (vwalk_to_vpath xs) G›
      using x_notin
      by auto
    then show ?thesis using not_in_set
      by (auto simp add: vwalk_to_vpath_cons)
  qed
qed

lemma vwalk_imp_ex_vpath:
  assumes "vwalk p G"
  assumes "hd p = u"
  assumes "last p = v"
  shows "∃q. vpath q G ∧ hd q = u ∧ last q = v"
by (metis assms vwalk_to_vpath_hd vwalk_to_vpath_last vwalk_to_vpath_vpath)


lemma vwalk_arcs_set_nil:
  assumes "x ∈ set (vwalk_arcs p)"
  shows "p ≠ []"
using assms by fastforce

lemma in_set_vwalk_arcs_append1:
  assumes "x ∈ set (vwalk_arcs p) ∨ x ∈ set (vwalk_arcs q)"
  shows "x ∈ set (vwalk_arcs (p @ q))"
using assms proof
  assume "x ∈ set (vwalk_arcs p)"
  then show "x ∈ set (vwalk_arcs (p @ q))"
    by (cases "q = []")
       (auto simp add: vwalk_arcs_append vwalk_arcs_set_nil)
next
  assume "x ∈ set (vwalk_arcs q)"
  then show "x ∈ set (vwalk_arcs (p @ q))"
    by (cases "p = []")
       (auto simp add: vwalk_arcs_append vwalk_arcs_set_nil)
qed

lemma in_set_vwalk_arcs_append2:
  assumes nonempty: "p ≠ []" "q ≠ []"
  assumes disj: "x ∈ set (vwalk_arcs p) ∨ x = (last p, hd q)
    ∨ x ∈ set (vwalk_arcs q)"
  shows "x ∈ set (vwalk_arcs (p @ q))"
using disj proof (elim disjE)
  assume "x = (last p, hd q)"
  then show "x ∈ set (vwalk_arcs (p @ q))"
    by (metis nonempty in_set_conv_decomp vwalk_arcs_append)
qed (auto intro: in_set_vwalk_arcs_append1)

lemma arcs_in_vwalk_arcs:
  assumes "u ∈ set (vwalk_arcs p)"
  shows "u ∈ set p × set p"
using assms by (induct p rule: vwalk_arcs.induct) auto

lemma set_vwalk_arcs_rev:
  "set (vwalk_arcs (rev p)) = {(v, u). (u,v) ∈ set (vwalk_arcs p)}"
proof (induct p)
  case Nil then show ?case by auto
next
  case (Cons x xs)
  then show ?case
  proof (cases "xs = []")
    case True then show ?thesis by auto
  next
    case False
    then have "set (vwalk_arcs (rev (x # xs))) = {(hd xs, x)}
      ∪ {a. case a of (v, u) ⇒ (u, v) ∈ set (vwalk_arcs xs)}"
      by (simp add: set_vwalk_arcs_snoc last_rev Cons)
    also have "… = {a. case a of (v, u) ⇒ (u, v) ∈ set (vwalk_arcs (x # xs))}"
      using False by (auto simp add: set_vwalk_arcs_cons)
    finally show ?thesis by assumption
  qed
qed

lemma vpath_self:
  assumes "u ∈ verts G"
  shows "vpath [u] G"
using assms by (intro vpathI vwalkI, auto)

lemma vwalk_verts_in_verts:
  assumes "vwalk p G"
  assumes "u ∈ set p"
  shows "u ∈ verts G"
using assms by auto

lemma vwalk_arcs_tl:
  "vwalk_arcs (tl xs) = tl (vwalk_arcs xs)"
by (induct xs rule: vwalk_arcs.induct) simp_all

lemma vwalk_arcs_butlast:
  "vwalk_arcs (butlast xs) = butlast (vwalk_arcs xs)"
proof (induct xs rule: rev_induct)
  case (snoc x xs) thus ?case
  proof (cases "xs = []")
    case True with snoc show ?thesis by simp
  next
    case False
    hence "vwalk_arcs (xs @ [x]) = vwalk_arcs xs @ [(last xs, x)]" using vwalk_arcs_append by force
    with snoc show ?thesis by simp
  qed
qed simp

lemma vwalk_arcs_tl_empty:
  "vwalk_arcs xs = [] ⟹ vwalk_arcs (tl xs) = []"
by (induct xs rule: vwalk_arcs.induct) simp_all

lemma vwalk_arcs_butlast_empty:
  "xs ≠ [] ⟹ vwalk_arcs xs = [] ⟹ vwalk_arcs (butlast xs) = []"
by (induct xs rule: vwalk_arcs.induct) simp_all


definition joinable :: "'a vwalk ⇒ 'a vwalk ⇒ bool" where
  "joinable p q ≡ last p = hd q ∧ p ≠ [] ∧ q ≠ []"

definition vwalk_join :: "'a list ⇒ 'a list ⇒ 'a list"
  (infixr "⊕" 65) where
  "p ⊕ q ≡ p @ tl q"

lemma joinable_Nil_l_iff[simp]: "joinable [] p = False"
  and joinable_Nil_r_iff[simp]: "joinable q [] = False"
  by (auto simp: joinable_def)

lemma joinable_Cons_l_iff[simp]: "p ≠ [] ⟹ joinable (v # p) q = joinable p q"
  and joinable_Snoc_r_iff[simp]: "q ≠ [] ⟹ joinable p (q @ [v]) = joinable p q"
   by (auto simp: joinable_def)

lemma joinableI[intro,simp]:
  assumes "last p = hd q" "p ≠ []" "q ≠ []"
  shows "joinable p q"
using assms by (simp add: joinable_def)

lemma vwalk_join_non_Nil[simp]:
  assumes "p ≠ []"
  shows "p ⊕ q ≠ []"
unfolding vwalk_join_def using assms by simp

lemma vwalk_join_Cons[simp]:
  assumes "p ≠ []"
  shows "(u # p) ⊕ q = u # p ⊕ q"
unfolding vwalk_join_def using assms by simp

lemma vwalk_join_def2:
  assumes "joinable p q"
  shows "p ⊕ q = butlast p @ q"
proof -
  from assms have "p ≠ []" and "q ≠ []" by (simp add: joinable_def)+
  then have "vwalk_join p q = butlast p @ last p # tl q"
    unfolding vwalk_join_def by simp
  then show ?thesis using assms by (simp add: joinable_def)
qed

lemma vwalk_join_hd':
  assumes "p ≠ []"
  shows "hd (p ⊕ q) = hd p"
using assms by (auto simp add: vwalk_join_def)

lemma vwalk_join_hd:
  assumes "joinable p q"
  shows "hd (p ⊕ q) = hd p"
using assms by (auto simp add: vwalk_join_def joinable_def)

lemma vwalk_join_last:
  assumes "joinable p q"
  shows "last (p ⊕ q) = last q"
using assms by (auto simp add: vwalk_join_def2 joinable_def)

lemma vwalk_join_Nil[simp]:
  "p ⊕ [] = p"
by (simp add: vwalk_join_def)

lemma vwalk_joinI_vwalk':
  assumes "vwalk p G"
  assumes "vwalk q G"
  assumes "last p = hd q"
  shows "vwalk (p ⊕ q) G"
proof (unfold vwalk_join_def, rule vwalkI)
  have "set p ⊆ verts G" and "set q ⊆ verts G"
    using ‹vwalk p G› and ‹vwalk q G› by blast+
  then show "set (p @ tl q) ⊆ verts G"
    by (cases q) auto
next
  show "p @ tl q ≠ []" using ‹vwalk p G› by auto
next
  have pe_p: "set (vwalk_arcs p) ⊆ arcs_ends G"
    using ‹vwalk p G› by blast
  have pe_q': "set (vwalk_arcs (tl q)) ⊆ arcs_ends G"
  proof -
    have "set (vwalk_arcs (tl q)) ⊆ set (vwalk_arcs q)"
      by (cases q) (simp_all add: set_vwalk_arcs_cons)
    then show ?thesis using ‹vwalk q G› by blast
  qed

  show "set (vwalk_arcs (p @ tl q)) ⊆ arcs_ends G"
  proof (cases "tl q")
    case Nil then show ?thesis using pe_p by auto
  next
    case (Cons x xs)
    then have nonempty: "p ≠ []" "tl q ≠ []"
      using ‹vwalk p G› by auto
    moreover
    have "(hd q, hd (tl q)) ∈ set (vwalk_arcs q)"
      using ‹vwalk q G› Cons by  (cases q) auto
    ultimately show ?thesis
      using ‹vwalk q G›
      by (auto simp: pe_p pe_q' ‹last p = hd q› vwalk_arcs_append)
  qed
qed

lemma vwalk_joinI_vwalk:
  assumes "vwalk p G"
  assumes "vwalk q G"
  assumes "joinable p q"
  shows "vwalk (p ⊕ q) G"
using assms vwalk_joinI_vwalk' by (auto simp: joinable_def)

lemma vwalk_join_split:
  assumes "u ∈ set p"
  shows "∃q r. p = q ⊕ r
  ∧ last q = u ∧ hd r = u ∧ q ≠ [] ∧ r ≠ []"
proof -
  from ‹u ∈ set p›
  obtain pre_p post_p where "p = pre_p @ u # post_p"
    by atomize_elim (auto simp add: split_list)
  then have "p = (pre_p @ [u]) ⊕ (u # post_p)"
    unfolding vwalk_join_def by simp
  then show ?thesis by fastforce
qed

lemma vwalkI_vwalk_join_l:
  assumes "p ≠ []"
  assumes "vwalk (p ⊕ q) G"
  shows "vwalk p G"
using assms unfolding vwalk_join_def
by (auto intro: vwalkI_append_l)

lemma vwalkI_vwalk_join_r:
  assumes "joinable p q"
  assumes "vwalk (p ⊕ q) G"
  shows "vwalk q G"
using assms
by (auto simp add: vwalk_join_def2 joinable_def intro: vwalkI_append_r)

lemma vwalk_join_assoc':
  assumes "p ≠ []" "q ≠ []"
  shows "(p ⊕ q) ⊕ r = p ⊕ q ⊕ r"
using assms by (simp add: vwalk_join_def)

lemma vwalk_join_assoc:
  assumes "joinable p q" "joinable q r"
  shows "(p ⊕ q) ⊕ r = p ⊕ q ⊕ r"
using assms by (simp add: vwalk_join_def joinable_def)

lemma joinable_vwalk_join_r_iff:
  "joinable p (q ⊕ r) ⟷ joinable p q ∨ (q = [] ∧ joinable p (tl r))"
by (cases q) (auto simp add: vwalk_join_def joinable_def)

lemma joinable_vwalk_join_l_iff:
  assumes "joinable p q"
  shows "joinable (p ⊕ q) r ⟷ joinable q r" (is "?L ⟷ ?R")
  using assms by (auto simp: joinable_def vwalk_join_last)

lemmas joinable_simps =
  joinable_vwalk_join_l_iff
  joinable_vwalk_join_r_iff

lemma joinable_cyclic_omit:
  assumes "joinable p q" "joinable q r" "joinable q q"
  shows "joinable p r"
using assms by (metis joinable_def)

lemma joinable_non_Nil:
  assumes "joinable p q"
  shows "p ≠ []" "q ≠ []"
using assms by (simp_all add: joinable_def)

lemma vwalk_join_vwalk_length[simp]:
  assumes "joinable p q"
  shows "vwalk_length (p ⊕ q) = vwalk_length p + vwalk_length q"
using assms unfolding vwalk_join_def
by (simp add: less_eq_Suc_le[symmetric] joinable_non_Nil)

lemma vwalk_join_arcs:
  assumes "joinable p q"
  shows "vwalk_arcs (p ⊕ q) = vwalk_arcs p @ vwalk_arcs q"
  using assms
proof (induct p)
  case (Cons v vs) then show ?case 
    by (cases "vs = []")
       (auto simp: vwalk_join_hd, simp add: joinable_def vwalk_join_def)
qed simp

lemma vwalk_join_arcs1:
  assumes "set (vwalk_arcs p) ⊆ E"
  assumes "p = q ⊕ r"
  shows "set (vwalk_arcs q) ⊆ E"
by (metis assms vwalk_join_def set_vwalk_arcs_append1 subset_trans)

lemma vwalk_join_arcs2:
  assumes "set (vwalk_arcs p) ⊆ E"
  assumes "joinable q r"
  assumes "p = q ⊕ r"
  shows "set (vwalk_arcs r) ⊆ E"
using assms by (simp add: vwalk_join_arcs)


definition concat_vpath :: "'a list ⇒ 'a list ⇒ 'a list" where
  "concat_vpath p q ≡ vwalk_to_vpath (p ⊕ q)"

lemma concat_vpath_is_vpath:
  assumes p_props: "vwalk p G" "hd p = u" "last p = v"
  assumes q_props: "vwalk q G" "hd q = v" "last q = w"
  shows "vpath (concat_vpath p q) G ∧ hd (concat_vpath p q) = u
    ∧ last (concat_vpath p q) = w"
proof (intro conjI)
  have joinable: "joinable p q" using assms by auto

  show "vpath (concat_vpath p q) G"
    unfolding concat_vpath_def using assms and joinable
    by (auto intro: vwalk_to_vpath_vpath vwalk_joinI_vwalk)

  show "hd (concat_vpath p q) = u" "last (concat_vpath p q) = w"
    unfolding concat_vpath_def using assms and joinable
    by (auto simp: vwalk_to_vpath_hd vwalk_to_vpath_last
      vwalk_join_hd vwalk_join_last)
qed

lemma concat_vpath_exists:
  assumes p_props: "vwalk p G" "hd p = u" "last p = v"
  assumes q_props: "vwalk q G" "hd q = v" "last q = w"
  obtains r where "vpath r G" "hd r = u" "last r = w"
using concat_vpath_is_vpath[OF assms] by blast

lemma (in fin_digraph) vpaths_finite:
  shows "finite {p. vpath p G}"
proof -
  have "{p. vpath p G}
    ⊆ {xs. set xs ⊆ verts G ∧ length xs ≤ card (verts G)}"
  proof (clarify, rule conjI)
    fix p assume "vpath p G"
    then show "set p ⊆ verts G" by blast

    from ‹vpath p G› have "length p = card (set p)"
      by (auto simp add: distinct_card)
    also have "… ≤ card (verts G)"
      using ‹vpath p G›
      by (auto intro!: card_mono elim!: vpathE)
    finally show "length p ≤ card (verts G)" .
  qed
  moreover
  have "finite {xs. set xs ⊆ verts G ∧ length xs ≤ card (verts G)}"
    by (intro finite_lists_length_le) auto
  ultimately show ?thesis by (rule finite_subset)
qed

lemma (in wf_digraph) reachable_vwalk_conv:
  "u →⇧*⇘G⇙ v ⟷ (∃p. vwalk p G ∧ hd p = u ∧ last p = v)" (is "?L ⟷ ?R")
proof
  assume ?L then show ?R
  proof (induct rule: converse_reachable_induct)
    case base then show ?case
      by (rule_tac x="[v]" in exI)
         (auto simp: vwalk_def arcs_ends_conv)
  next
    case (step u w)
    then obtain p where "vwalk p G" "hd p = w" "last p = v" by auto
    then have "vwalk (u#p) G ∧ hd (u#p) = u ∧ last (u#p) = v"
      using step by (auto intro!: vwalk_consI intro: adj_in_verts)
    then show ?case ..
  qed
next
  assume ?R
  then obtain p where "vwalk p G" "hd p = u" "last p = v" by auto
  with ‹vwalk p G› show ?L
  proof (induct p arbitrary: u rule: vwalk_induct)
    case (Base u) then show ?case by auto
  next
    case (Cons w x es)
    then have "u →⇘G⇙ x" using Cons by auto
    show ?case
      apply (rule adj_reachable_trans)
      apply fact
      apply (rule Cons)
      using Cons by (auto elim: vwalk_consE)
  qed
qed

lemma (in wf_digraph) reachable_vpath_conv:
  "u →⇧*⇘G⇙ v ⟷ (∃p. vpath p G ∧ hd p = u ∧ last p = v)" (is "?L ⟷ ?R")
proof
  assume ?L then obtain p where "vwalk p G" "hd p = u" "last p = v"
    by (auto simp: reachable_vwalk_conv)
  then show ?R
    by (auto intro: exI[where x="vwalk_to_vpath p"]
      simp: vwalk_to_vpath_hd vwalk_to_vpath_last vwalk_to_vpath_vpath)
qed (auto simp: reachable_vwalk_conv)

lemma in_set_vwalk_arcsE:
  assumes "(u,v) ∈ set (vwalk_arcs p)"
  obtains "u ∈ set p" "v ∈ set p"
using assms
by (induct p rule: vwalk_arcs.induct) auto

lemma vwalk_rev_ex:
  assumes "symmetric G"
  assumes "vwalk p G"
  shows "vwalk (rev p) G"
using assms
proof (induct p)
  case Nil then show ?case by simp
next
  case (Cons x xs)
  then show ?case proof (cases "xs = []")
    case True then show ?thesis using Cons by auto
  next
    case False
    then have "vwalk xs G" using ‹vwalk (x # xs) G›
      by (metis vwalk_consE)
    then have "vwalk (rev xs) G" using Cons by blast
    have "vwalk (rev (x # xs)) G"
    proof (rule vwalkI)
      have "set (x # xs) ⊆ verts G" using ‹vwalk (x # xs) G› by blast
      then show "set (rev (x # xs)) ⊆ verts G" by auto
    next
      have "set (vwalk_arcs (x # xs)) ⊆ arcs_ends G"
        using ‹vwalk (x # xs) G› by auto
      then show "set (vwalk_arcs (rev (x # xs))) ⊆ arcs_ends G"
        using ‹symmetric G›
        by (simp only: set_vwalk_arcs_rev)
           (auto intro: arcs_ends_symmetric)
    next
      show "rev (x # xs) ≠ []" by auto
    qed
    then show "vwalk (rev (x # xs)) G" by auto
  qed
qed

lemma vwalk_singleton[simp]: "vwalk [u] G = (u ∈ verts G)"
  by auto

lemma (in wf_digraph) vwalk_Cons_Cons[simp]:
  "vwalk (u # v # ws) G = ((u,v) ∈ arcs_ends G ∧ vwalk (v # ws) G)"
  by (force elim: vwalk_consE intro: vwalk_consI)

lemma (in wf_digraph) awalk_imp_vwalk:
  assumes "awalk u p v" shows "vwalk (awalk_verts u p) G"
  using assms
  by (induct p arbitrary: u rule: vwalk_arcs.induct)
     (force simp: awalk_simps dest: in_arcs_imp_in_arcs_ends)+

end