# 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
›

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'"
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
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›
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))"
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)

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
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
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 = []")
next
assume "x ∈ set (vwalk_arcs q)"
then show "x ∈ set (vwalk_arcs (p @ q))"
by (cases "p = []")
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"

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

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)"
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 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
```