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 *Gv  (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 Gx" 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 *Gv  (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