Theory Undirected_Graph_Walks
theory Undirected_Graph_Walks imports Undirected_Graph_Basics
begin
section ‹Walks, Paths and Cycles ›
text ‹ The definition of walks, paths, cycles, and related concepts are foundations of graph theory,
yet there can be some differences in literature between definitions. This formalisation draws inspiration
from Noschinski's Graph Library \<^cite>‹"noschinski_2015"›, however focuses on an undirected graph context
compared to a directed graph context, and extends on some definitions, as required to formalise
Balog Szemeredi Gowers theorem. ›
context ulgraph
begin
subsection ‹ Walks›
text‹This definition is taken from the directed graph library, however edges are undirected›
fun walk_edges :: "'a list ⇒ 'a edge list" where
"walk_edges [] = []"
| "walk_edges [x] = []"
| "walk_edges (x # y # ys) = {x,y} # walk_edges (y # ys)"
lemma walk_edges_app: "walk_edges (xs @ [y, x]) = walk_edges (xs @ [y]) @ [{y, x}]"
by (induct xs rule: walk_edges.induct, simp_all)
lemma walk_edges_tl_ss: "set (walk_edges (tl xs)) ⊆ set (walk_edges xs)"
by (induct xs rule: walk_edges.induct) auto
lemma walk_edges_rev: "rev (walk_edges xs) = walk_edges (rev xs)"
proof (induct xs rule: walk_edges.induct, simp_all)
fix x y ys assume assm: "rev (walk_edges (y # ys)) = walk_edges (rev ys @ [y])"
then show "walk_edges (rev ys @ [y]) @ [{x, y}] = walk_edges (rev ys @ [y, x])"
using walk_edges_app by fastforce
qed
lemma walk_edges_append_ss1: "set (walk_edges (ys)) ⊆ set (walk_edges (xs@ys))"
proof (induct xs rule: walk_edges.induct)
case 1
then show ?case by simp
next
case (2 x)
then show ?case
using walk_edges_tl_ss by fastforce
next
case (3 x y ys)
then show ?case by (simp add: subset_iff)
qed
lemma walk_edges_append_ss2: "set (walk_edges (xs)) ⊆ set (walk_edges (xs@ys))"
by (induct xs rule: walk_edges.induct) auto
lemma walk_edges_singleton_app: "ys ≠ [] ⟹ walk_edges ([x]@ys) = {x, hd ys} # walk_edges ys"
using list.exhaust_sel walk_edges.simps(3) by (metis Cons_eq_appendI eq_Nil_appendI)
lemma walk_edges_append_union: "xs ≠ [] ⟹ ys ≠ [] ⟹
set (walk_edges (xs@ys)) = set (walk_edges (xs)) ∪ set (walk_edges ys) ∪ {{last xs, hd ys}}"
using walk_edges_singleton_app by (induct xs rule: walk_edges.induct) auto
lemma walk_edges_decomp_ss: "set (walk_edges (xs@[y]@zs)) ⊆ set (walk_edges (xs@[y]@ys@[y]@zs))"
proof -
have half_ss: "set (walk_edges (xs@[y])) ⊆ set (walk_edges (xs@[y]@ys@[y]))"
using walk_edges_append_ss2 by fastforce
thus ?thesis proof (cases "zs = []")
case True
then show ?thesis using half_ss by auto
next
case False
then have decomp1: "set (walk_edges (xs@[y]@zs)) = set (walk_edges (xs@[y])) ∪ set (walk_edges (zs)) ∪ {{y, hd zs}}"
using walk_edges_append_union
by (metis append_assoc append_is_Nil_conv last_snoc neq_Nil_conv)
have "set (walk_edges (xs@[y]@ys@[y]@zs)) = set (walk_edges (xs@[y]@ys@[y])) ∪ set (walk_edges (zs)) ∪ {{y, hd zs}}"
using walk_edges_append_union False
by (metis append_assoc append_is_Nil_conv empty_iff empty_set last_snoc list.set_intros(1))
then show ?thesis using decomp1 half_ss by auto
qed
qed
definition walk_length :: "'a list ⇒ nat" where
"walk_length p ≡ length (walk_edges p)"
lemma walk_length_conv: "walk_length p = length p - 1"
by (induct p rule: walk_edges.induct) (auto simp: walk_length_def)
lemma walk_length_rev: "walk_length p = walk_length (rev p)"
using walk_edges_rev walk_length_def
by (metis length_rev)
lemma walk_length_app: "xs ≠ [] ⟹ ys ≠ [] ⟹ walk_length (xs @ ys) = walk_length xs + walk_length ys + 1"
apply (induct xs rule: walk_edges.induct)
apply (simp_all add: walk_length_def)
using walk_edges_singleton_app by force
lemma walk_length_app_ineq: "walk_length (xs @ ys) ≥ walk_length xs + walk_length ys ∧
walk_length (xs @ ys) ≤ walk_length xs + walk_length ys + 1"
proof (cases "xs = [] ∨ ys = []")
case True
then show ?thesis using walk_length_def by auto
next
case False
then show ?thesis
by (simp add: walk_length_app)
qed
text ‹ Note that while the trivial walk is allowed, the empty walk is not ›
definition is_walk :: "'a list ⇒ bool" where
"is_walk xs ≡ set xs ⊆ V ∧ set (walk_edges xs) ⊆ E ∧ xs ≠ []"
lemma is_walkI: "set xs ⊆ V ⟹ set (walk_edges xs) ⊆ E ⟹ xs ≠ [] ⟹ is_walk xs"
using is_walk_def by simp
lemma is_walk_wf: "is_walk xs ⟹ set xs ⊆ V"
by (simp add: is_walk_def)
lemma is_walk_wf_hd: "is_walk xs ⟹ hd xs ∈ V"
using is_walk_wf hd_in_set is_walk_def by blast
lemma is_walk_wf_last: "is_walk xs ⟹ last xs ∈ V"
using is_walk_wf last_in_set is_walk_def by blast
lemma is_walk_singleton: "u ∈ V ⟹ is_walk [u]"
unfolding is_walk_def using walk_edges.simps by simp
lemma is_walk_not_empty: "is_walk xs ⟹ xs ≠ []"
unfolding is_walk_def by simp
lemma is_walk_not_empty2: "is_walk [] = False"
unfolding is_walk_def by simp
text ‹Reasoning on transformations of a walk ›
lemma is_walk_rev: "is_walk xs ⟷ is_walk (rev xs)"
unfolding is_walk_def using walk_edges_rev
by (metis rev_is_Nil_conv set_rev)
lemma is_walk_tl: "length xs ≥ 2 ⟹ is_walk xs ⟹ is_walk (tl xs)"
using walk_edges_tl_ss is_walk_def in_mono list.set_sel(2) tl_Nil by fastforce
lemma is_walk_append:
assumes "is_walk xs"
assumes "is_walk ys"
assumes "last xs = hd ys"
shows "is_walk (xs @ (tl ys))"
proof (intro is_walkI subsetI)
show "xs @ tl ys ≠ []" using is_walk_def assms by auto
show "⋀x. x ∈ set (xs @ tl ys) ⟹ x ∈ V" using assms is_walk_def is_walk_wf
by (metis Un_iff in_mono list_set_tl set_append)
next
fix x assume xin: "x ∈ set (walk_edges (xs @ tl ys))"
show "x ∈ E" proof (cases "tl ys = []")
case True
then show ?thesis using assms(1) is_walk_def xin by auto
next
case False
then have xin2: "x ∈ (set (walk_edges xs) ∪ set (walk_edges (tl ys)) ∪ {{last xs, hd (tl ys)}})"
using walk_edges_append_union is_walk_not_empty assms xin by auto
have 1: "set (walk_edges xs) ⊆ E" using assms(1) is_walk_def
by simp
have 2: "set (walk_edges (tl ys)) ⊆ E" using assms(2) is_walk_def
by (meson dual_order.trans walk_edges_tl_ss)
have "{last xs, hd (tl ys)} ∈ E" using is_walk_def assms(2) assms(3)
by (metis False hd_Cons_tl insert_subset list.simps(15) walk_edges.simps(3))
then show ?thesis using 1 2 xin2 by auto
qed
qed
lemma is_walk_decomp:
assumes "is_walk (xs@[y]@ys@[y]@zs)" (is "is_walk ?w")
shows "is_walk (xs@[y]@zs)"
proof (intro is_walkI)
show "set (xs @ [y] @ zs) ⊆ V" using assms is_walk_def by simp
show "xs @ [y] @ zs ≠ []" by simp
show "set (walk_edges (xs @ [y] @ zs)) ⊆ E"
using walk_edges_decomp_ss assms(1) is_walk_def by blast
qed
lemma is_walk_hd_tl:
assumes "is_walk (y # ys)"
assumes "{x, y} ∈ E"
shows "is_walk (x # y # ys)"
proof (intro is_walkI)
show "set (x # y # ys) ⊆ V"
using assms by (simp add: is_walk_def wellformed_alt_fst)
show "set (walk_edges (x # y # ys)) ⊆ E"
using walk_edges.simps assms is_walk_def by simp
show "x # y # ys ≠ []" by simp
qed
lemma is_walk_drop_hd:
assumes "ys ≠ []"
assumes "is_walk (y # ys)"
shows "is_walk ys"
proof (intro is_walkI)
show "set ys ⊆ V"
using assms is_walk_wf by fastforce
show "set (walk_edges ys) ⊆ E"
using assms is_walk_def walk_edges_tl_ss by force
show "ys ≠ []" using assms by simp
qed
lemma walk_edges_index:
assumes "i ≥ 0" "i < walk_length w"
assumes "is_walk w"
shows "(walk_edges w) ! i ∈ E"
using assms
proof (induct w arbitrary: i rule: walk_edges.induct, simp add: is_walk_not_empty2,
simp add: walk_length_def)
case (3 x y ys)
then show ?case proof (cases "i = 0")
case True
then show ?thesis
using "3.prems"(3) is_walk_def by fastforce
next
case False
have gt: "0 ≤ i -1" using False by simp
have lt: "i - 1 < walk_length (y # ys)"
using "3.prems"(2) False walk_length_conv by auto
have "is_walk (y # ys)"
using "3.prems"(3) is_walk_def by fastforce
then show ?thesis using "3.hyps"[of "i -1"]
by (metis "3.prems"(1) False gt lt le_neq_implies_less nth_Cons_pos walk_edges.simps(3))
qed
qed
lemma is_walk_index:
assumes "i ≥ 0" "Suc i < (length w)"
assumes "is_walk w"
shows "{w ! i, w ! (i + 1)} ∈ E"
using assms proof (induct w arbitrary: i rule: walk_edges.induct, simp, simp)
fix x y ys i
assume IH: "⋀j. 0 ≤ j ⟹ Suc j < length (y # ys) ⟹ is_walk (y # ys) ⟹ {(y # ys) ! j, (y # ys) ! (j + 1)} ∈ E"
assume 1: " 0 ≤ i" and 2: "Suc i < length (x # y # ys)" and 3: "is_walk (x # y # ys)"
show "{(x # y # ys) ! i, (x # y # ys) ! (i + 1)} ∈ E"
proof (cases "i = 0")
case True
then show ?thesis using 3 is_walk_def
by simp
next
case False
have "is_walk (y # ys)" using is_walk_def 3 by fastforce
then show ?thesis using 2 IH[of "i - 1"]
by (simp add: False nat_less_le)
qed
qed
lemma is_walk_take:
assumes "is_walk w"
assumes "n > 0"
assumes "n ≤ length w"
shows "is_walk (take n w)"
using assms proof (induct w arbitrary: n rule: walk_edges.induct)
case 1
then show ?case by simp
next
case (2 x)
then have "n = 1" using 2 by auto
then show ?case by (simp add: "2.prems"(1))
next
case (3 x y ys)
then show ?case proof (cases "n = 1")
case True
then have "take n (x # y # ys) = [x]"
by simp
then show ?thesis using is_walk_def "3.prems"(1) by simp
next
case False
then have ngt: "n ≥ 2" using "3.prems"(2) by auto
then have tk_split1: "take n (x # y # ys) = x # take (n - 1) (y # ys)" using 3
by (simp add: take_Cons')
then have tk_split: "take n (x # y # ys) = x # y # (take (n - 2) ys)"
using 3 ngt take_Cons'[of "n -1" "y" "ys"]
by (metis False diff_diff_left less_one nat_neq_iff one_add_one zero_less_diff)
have w: "is_walk (y # ys)" using is_walk_tl
using "3.prems"(1) is_walk_def by force
have "n - 1 ≤ length (y # ys)" using "3.prems"(3) by simp
then have w_tl: "is_walk (take (n - 1) (y # ys))" using "3.hyps"[of "n - 1"] w "3.prems" ngt
by linarith
have "{x, y} ∈ E" using is_walk_def walk_edges.simps "3.prems"(1) by auto
then show ?thesis using is_walk_hd_tl[of y "(take (n - 2) ys)" x] tk_split
using tk_split1 w_tl by force
qed
qed
lemma is_walk_drop:
assumes "is_walk w"
assumes "n < length w"
shows "is_walk (drop n w)"
using assms proof (induct w arbitrary: n rule: walk_edges.induct)
case 1
then show ?case by simp
next
case (2 x)
then have "n = 0" using 2 by auto
then show ?case by (simp add: "2.prems"(1))
next
case (3 x y ys)
then show ?case proof (cases "n ≥ 2")
case True
then have ngt: "n ≥ 2" using "3.prems"(2) by auto
then have tk_split1: "drop n (x # y # ys) = drop (n - 1) (y # ys)" using 3
by (simp add: drop_Cons')
then have tk_split: "drop n (x # y # ys) = (drop (n - 2) ys)"
using 3 ngt drop_Cons'[of "n -1" "y" "ys"] True
by (metis Suc_1 Suc_le_eq diff_diff_left less_not_refl nat_1_add_1 zero_less_diff)
have w: "is_walk (y # ys)" using is_walk_tl
using "3.prems"(1) is_walk_def by force
have "n - 1 < length (y # ys)" using "3.prems"(2) by simp
then have w_tl: "is_walk (drop (n - 1) (y # ys))" using "3.hyps"[of "n - 1"] w "3.prems" ngt
by linarith
have "{x, y} ∈ E" using is_walk_def walk_edges.simps "3.prems"(1) by auto
then show ?thesis using is_walk_hd_tl[of y "(take (n - 2) ys)" x] tk_split
using tk_split1 w_tl by force
next
case False
then have or: "n = 0 ∨ n = 1"
by auto
have walk: "is_walk (y # ys)" using is_walk_drop_hd 3 by blast
have n0: "n = 0 ⟹ (drop n (x # y # ys)) = (x # y # ys)" by simp
have "n = 1 ⟹ (drop n (x # y # ys)) = y # ys" by simp
then show ?thesis using n0 3 walk or by auto
qed
qed
definition walks :: "'a list set" where
"walks ≡ {p. is_walk p}"
definition is_open_walk :: "'a list ⇒ bool" where
"is_open_walk xs ≡ is_walk xs ∧ hd xs ≠ last xs"
lemma is_open_walk_rev: "is_open_walk xs ⟷ is_open_walk (rev xs)"
unfolding is_open_walk_def using is_walk_rev
by (metis hd_rev last_rev)
definition is_closed_walk :: "'a list ⇒ bool" where
"is_closed_walk xs ≡ is_walk xs ∧ hd xs = last xs"
lemma is_closed_walk_rev: "is_closed_walk xs ⟷ is_closed_walk (rev xs)"
unfolding is_closed_walk_def using is_walk_rev
by (metis hd_rev last_rev)
definition is_trail :: "'a list ⇒ bool" where
"is_trail xs ≡ is_walk xs ∧ distinct (walk_edges xs)"
lemma is_trail_rev: "is_trail xs ⟷ is_trail (rev xs)"
unfolding is_trail_def using is_walk_rev
by (metis distinct_rev walk_edges_rev)
subsection ‹Paths›
text ‹There are two common definitions of a path. The first, given below, excludes the case
where a path is a cycle. Note this also excludes the trivial path $[x]$›
definition is_path :: "'a list ⇒ bool" where
"is_path xs ≡ (is_open_walk xs ∧ distinct (xs))"
lemma is_path_rev: "is_path xs ⟷ is_path (rev xs)"
unfolding is_path_def using is_open_walk_rev
by (metis distinct_rev)
lemma is_path_walk: "is_path xs ⟹ is_walk xs"
unfolding is_path_def is_open_walk_def by auto
definition paths :: "'a list set" where
"paths ≡ {p . is_path p}"
lemma paths_ss_walk: "paths ⊆ walks"
unfolding paths_def walks_def is_path_def is_open_walk_def by auto
text ‹ A more generic definition of a path - used when a cycle is considered a path, and
therefore includes the trivial path $[x]$ ›
definition is_gen_path:: "'a list ⇒ bool" where
"is_gen_path p ≡ is_walk p ∧ ((distinct (tl p) ∧ hd p = last p) ∨ distinct p)"
lemma is_path_gen_path: "is_path p ⟹ is_gen_path p"
unfolding is_path_def is_gen_path_def is_open_walk_def by (auto simp add: distinct_tl)
lemma is_gen_path_rev: "is_gen_path p ⟷ is_gen_path (rev p)"
unfolding is_gen_path_def using is_walk_rev distinct_tl_rev
by (metis distinct_rev hd_rev last_rev)
lemma is_gen_path_distinct: "is_gen_path p ⟹ hd p ≠ last p ⟹ distinct p"
unfolding is_gen_path_def by auto
lemma is_gen_path_distinct_tl:
assumes "is_gen_path p" and "hd p = last p"
shows "distinct (tl p)"
proof (cases "length p > 1")
case True
then show ?thesis
using assms(1) distinct_tl is_gen_path_def by auto
next
case False
then show ?thesis
using assms(1) distinct_tl is_gen_path_def by auto
qed
lemma is_gen_path_trivial: "x ∈ V ⟹ is_gen_path [x]"
unfolding is_gen_path_def is_walk_def by simp
definition gen_paths :: "'a list set" where
"gen_paths ≡ {p . is_gen_path p}"
lemma gen_paths_ss_walks: "gen_paths ⊆ walks"
unfolding gen_paths_def walks_def is_gen_path_def by auto
subsection ‹ Cycles ›
text ‹Note, a cycle must be non trivial (i.e. have an edge), but as we let a loop by a cycle
we broaden the definition in comparison to Noschinski \<^cite>‹"noschinski_2015"› for a cycle to be of
length greater than 1 rather than 3 ›
definition is_cycle :: "'a list ⇒ bool" where
"is_cycle xs ≡ is_closed_walk xs ∧ walk_length xs ≥ 1 ∧ distinct (tl xs)"
lemma is_gen_path_cycle: "is_cycle p ⟹ is_gen_path p"
unfolding is_cycle_def is_gen_path_def is_closed_walk_def by auto
lemma is_cycle_alt_gen_path: "is_cycle xs ⟷ is_gen_path xs ∧ walk_length xs ≥ 1 ∧ hd xs = last xs"
proof (intro iffI)
show "is_cycle xs ⟹ is_gen_path xs ∧ 1 ≤ walk_length xs ∧ hd xs = last xs"
using is_gen_path_cycle is_cycle_def is_closed_walk_def
by auto
show "is_gen_path xs ∧ 1 ≤ walk_length xs ∧ hd xs = last xs ⟹ is_cycle xs"
using distinct_tl is_closed_walk_def is_cycle_def is_gen_path_def by blast
qed
lemma is_cycle_alt: "is_cycle xs ⟷ is_walk xs ∧ distinct (tl xs) ∧ walk_length xs ≥ 1 ∧ hd xs = last xs"
proof (intro iffI)
show "is_cycle xs ⟹ is_walk xs ∧ distinct (tl xs) ∧ 1 ≤ walk_length xs ∧ hd xs = last xs"
using is_cycle_alt_gen_path is_cycle_def is_gen_path_def by blast
show "is_walk xs ∧ distinct (tl xs) ∧ 1 ≤ walk_length xs ∧ hd xs = last xs ⟹ is_cycle xs"
by (simp add: is_cycle_alt_gen_path is_gen_path_def)
qed
lemma is_cycle_rev: "is_cycle xs ⟷ is_cycle (rev xs)"
proof -
have len: "1 ≤ walk_length xs ⟷ 1 ≤ walk_length (rev xs)"
by (metis length_rev walk_edges_rev walk_length_def)
have "hd xs = last xs ⟹ distinct (tl xs) ⟷ distinct (tl (rev xs))"
using distinct_tl_rev by blast
then show ?thesis using len is_cycle_def
using is_closed_walk_def is_closed_walk_rev by auto
qed
lemma cycle_tl_is_path: "is_cycle xs ∧ walk_length xs ≥ 3 ⟹ is_path (tl xs)"
proof (simp add: is_cycle_def is_path_def is_open_walk_def is_closed_walk_def walk_length_conv,
elim conjE, intro conjI, simp add: is_walk_tl)
assume w: "is_walk xs" and eq: "hd xs = last xs" and "3 ≤ length xs - Suc 0" and
dis: "distinct (tl xs)"
then have len: "4 ≤ length xs"
by linarith
then have lentl: "3 ≤ length (tl xs)" by simp
then have lentltl: "2 ≤ length (tl (tl xs))" by simp
have "last (tl (tl xs)) = last (tl xs)"
by (metis One_nat_def Suc_1 ‹3 ≤ length xs - Suc 0› diff_is_0_eq' is_walk_def is_walk_tl last_tl
lentl not_less_eq_eq numeral_le_one_iff one_le_numeral order.trans semiring_norm(70) w)
then have "last (tl xs) ∈ set (tl (tl xs))"
using last_in_list_tl_set lentltl by (metis last_in_set list.sel(2))
moreover have "hd (tl xs) ∉ set (tl (tl xs))" using dis lentltl
by (metis distinct.simps(2) hd_Cons_tl list.sel(2) list.size(3) not_numeral_le_zero)
ultimately show "hd (tl xs) ≠ last (tl xs)" by fastforce
qed
lemma is_gen_path_path:
assumes "is_gen_path p" and "walk_length p > 0" and "(¬ is_cycle p)"
shows "is_path p"
proof (simp add: is_gen_path_def is_path_def is_open_walk_def, intro conjI)
show "is_walk p" using is_gen_path_def assms(1) by simp
show ne: "hd p ≠ last p"
using assms(1) assms(2) assms(3) is_cycle_alt_gen_path by auto
have "((distinct (tl p) ∧ hd p = last p) ∨ distinct p)" using is_gen_path_def assms(1) by auto
thus "distinct p" using ne by auto
qed
lemma is_gen_path_options: "is_gen_path p ⟷ is_cycle p ∨ is_path p ∨ (∃ v ∈ V. p = [v])"
proof (intro iffI)
assume a: "is_gen_path p"
then have "p ≠ []" unfolding is_gen_path_def is_walk_def by auto
then have "(∀ v ∈ V . p ≠ [v]) ⟹ walk_length p > 0" using walk_length_def
by (metis a is_gen_path_def is_walk_wf_hd length_greater_0_conv list.collapse list.distinct(1) walk_edges.simps(3))
then show "is_cycle p ∨ is_path p ∨ (∃ v ∈ V. p = [v])"
using a is_gen_path_path by auto
next
show "is_cycle p ∨ is_path p ∨ (∃ v ∈ V. p = [v]) ⟹ is_gen_path p "
using is_gen_path_cycle is_path_gen_path is_gen_path_trivial by auto
qed
definition cycles :: "'a list set" where
"cycles ≡ {p. is_cycle p}"
lemma cycles_ss_gen_paths: "cycles ⊆ gen_paths"
unfolding cycles_def gen_paths_def using is_gen_path_cycle by auto
lemma gen_paths_ss: "gen_paths ⊆ cycles ∪ paths ∪ {[v] | v. v ∈ V}"
unfolding gen_paths_def cycles_def paths_def using is_gen_path_options by auto
text ‹Walk edges are distinct in a path and cycle ›
lemma distinct_edgesI:
assumes "distinct p" shows "distinct (walk_edges p)"
proof -
from assms have "?thesis" "⋀u. u ∉ set p ⟹ (⋀v. u ≠ v ⟹ {u,v} ∉ set (walk_edges p))"
by (induct p rule: walk_edges.induct) auto
then show ?thesis by simp
qed
lemma scycles_distinct_edges:
assumes "c ∈ cycles" "3 ≤ walk_length c" shows "distinct (walk_edges c)"
proof -
from assms have c_props: "distinct (tl c)" "4 ≤ length c" "hd c = last c"
by (auto simp add: cycles_def is_cycle_def is_closed_walk_def walk_length_conv)
then have "{hd c, hd (tl c)} ∉ set (walk_edges (tl c))"
proof (induct c rule: walk_edges.induct)
case (3 x y ys)
then have "hd ys ≠ last ys" by (cases ys) auto
moreover
from 3 have "walk_edges (y # ys) = {y, hd ys} # walk_edges ys"
by (cases ys) auto
moreover
{ fix xs have "set (walk_edges xs) ⊆ Pow (set xs)"
by (induct xs rule: walk_edges.induct) auto }
ultimately
show ?case using 3 by auto
qed simp_all
moreover
from assms have "distinct (walk_edges (tl c))"
by (intro distinct_edgesI) (simp add: cycles_def is_cycle_def)
ultimately
show ?thesis by(cases c, simp_all)
(metis distinct.simps(1) distinct.simps(2) list.sel(1) list.sel(3) walk_edges.elims)
qed
end
context fin_ulgraph
begin
lemma finite_paths: "finite paths"
proof -
have ss: "paths ⊆ {xs. set xs ⊆ V ∧ length xs ≤ (card (V))}"
proof (rule, simp, intro conjI)
show 1: "⋀x. x ∈ paths ⟹ set x ⊆ V"
unfolding paths_def is_path_def is_open_walk_def is_walk_def by simp
fix x assume a: "x ∈ paths"
then have "distinct x"
using paths_def is_path_def by simp_all
then have eq: "length x = card (set x)"
by (simp add: distinct_card)
then show "length x ≤ gorder" using a 1
by (simp add: card_mono finV)
qed
have "finite {xs. set xs ⊆ V ∧ length xs ≤ (card (V))}"
using finV by (simp add: finite_lists_length_le)
thus ?thesis using ss finite_subset by auto
qed
lemma finite_cycles: "finite (cycles)"
proof -
have "cycles ⊆ {xs. set xs ⊆ V ∧ length xs ≤ Suc (card (V))}"
proof (rule, simp)
fix p assume "p ∈ cycles"
then have "distinct (tl p)" and "set p ⊆ V"
unfolding cycles_def walks_def is_cycle_def is_closed_walk_def is_walk_def
by (simp_all)
then have "set (tl p) ⊆ V"
by (cases p) auto
with finV have "card (set (tl p)) ≤ card (V)"
by (rule card_mono)
then have "length (p) ≤ 1 + card (V)"
using distinct_card[OF ‹distinct (tl p)›] by auto
then show "set p ⊆ V ∧ length p ≤ Suc (card (V))"
by (simp add: ‹set p ⊆ V›)
qed
moreover
have "finite {xs. set xs ⊆ V ∧ length xs ≤ Suc (card (V))}"
using finV by (rule finite_lists_length_le)
ultimately
show ?thesis by (rule finite_subset)
qed
lemma finite_gen_paths: "finite (gen_paths)"
proof -
have "finite ({[v] | v . v ∈ V})" using finV by auto
thus ?thesis using gen_paths_ss finite_cycles finite_paths finite_subset by auto
qed
end
end