(* 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