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 ≤ order" 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