(* Title: Arc_Walk.thy Author: Lars Noschinski, TU München *) theory Arc_Walk imports Digraph begin section ‹Arc Walks› text ‹ We represent a walk in a graph by the list of its arcs. › type_synonym 'b awalk = "'b list" context pre_digraph begin text ‹ The list of vertices of a walk. The additional vertex argument is there to deal with the case of empty walks. › primrec awalk_verts :: "'a ⇒ 'b awalk ⇒ 'a list" where "awalk_verts u [] = [u]" | "awalk_verts u (e # es) = tail G e # awalk_verts (head G e) es" abbreviation awhd :: "'a ⇒ 'b awalk ⇒ 'a" where "awhd u p ≡ hd (awalk_verts u p)" abbreviation awlast:: "'a ⇒ 'b awalk ⇒ 'a" where "awlast u p ≡ last (awalk_verts u p)" text ‹ Tests whether a list of arcs is a consistent arc sequence, i.e. a list of arcs, where the head G node of each arc is the tail G node of the following arc. › fun cas :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "cas u [] v = (u = v)" | "cas u (e # es) v = (tail G e = u ∧ cas (head G e) es v)" lemma cas_simp: assumes "es ≠ []" shows "cas u es v ⟷ tail G (hd es) = u ∧ cas (head G (hd es)) (tl es) v" using assms by (cases es) auto definition awalk :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "awalk u p v ≡ u ∈ verts G ∧ set p ⊆ arcs G ∧ cas u p v" (* XXX: rename to atrail? *) definition (in pre_digraph) trail :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where "trail u p v ≡ awalk u p v ∧ distinct p" definition apath :: "'a ⇒'b awalk ⇒ 'a ⇒ bool" where "apath u p v ≡ awalk u p v ∧ distinct (awalk_verts u p)" end subsection ‹Basic Lemmas› lemma (in pre_digraph) awalk_verts_conv: "awalk_verts u p = (if p = [] then [u] else map (tail G) p @ [head G (last p)])" by (induct p arbitrary: u) auto lemma (in pre_digraph) awalk_verts_conv': assumes "cas u p v" shows "awalk_verts u p = (if p = [] then [u] else tail G (hd p) # map (head G) p)" using assms by (induct u p v rule: cas.induct) (auto simp: cas_simp) lemma (in pre_digraph) length_awalk_verts: "length (awalk_verts u p) = Suc (length p)" by (simp add: awalk_verts_conv) lemma (in pre_digraph) awalk_verts_ne_eq: assumes "p ≠ []" shows "awalk_verts u p = awalk_verts v p" using assms by (auto simp: awalk_verts_conv) lemma (in pre_digraph) awalk_verts_non_Nil[simp]: "awalk_verts u p ≠ []" by (simp add: awalk_verts_conv) context wf_digraph begin lemma assumes "cas u p v" shows awhd_if_cas: "awhd u p = u" and awlast_if_cas: "awlast u p = v" using assms by (induct p arbitrary: u) auto lemma awalk_verts_in_verts: assumes "u ∈ verts G" "set p ⊆ arcs G" "v ∈ set (awalk_verts u p)" shows "v ∈ verts G" using assms by (induct p arbitrary: u) (auto intro: wellformed) lemma assumes "u ∈ verts G" "set p ⊆ arcs G" shows awhd_in_verts: "awhd u p ∈ verts G" and awlast_in_verts: "awlast u p ∈ verts G" using assms by (auto elim: awalk_verts_in_verts) lemma awalk_conv: "awalk u p v = (set (awalk_verts u p) ⊆ verts G ∧ set p ⊆ arcs G ∧ awhd u p = u ∧ awlast u p = v ∧ cas u p v)" unfolding awalk_def using hd_in_set[OF awalk_verts_non_Nil, of u p] by (auto intro: awalk_verts_in_verts awhd_if_cas awlast_if_cas simp del: hd_in_set) lemma awalkI: assumes "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" shows "awalk u p v" using assms by (auto simp: awalk_conv awhd_if_cas awlast_if_cas) lemma awalkE[elim]: assumes "awalk u p v" obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" "awhd u p = u" "awlast u p = v" using assms by (auto simp add: awalk_conv) lemma awalk_Nil_iff: "awalk u [] v ⟷ u = v ∧ u ∈ verts G" unfolding awalk_def by auto lemma trail_Nil_iff: "trail u [] v ⟷ u = v ∧ u ∈ verts G" by (auto simp: trail_def awalk_Nil_iff) lemma apath_Nil_iff: "apath u [] v ⟷ u = v ∧ u ∈ verts G" by (auto simp: apath_def awalk_Nil_iff) lemma awalk_hd_in_verts: "awalk u p v ⟹ u ∈ verts G" by (cases p) auto lemma awalk_last_in_verts: "awalk u p v ⟹ v ∈ verts G" unfolding awalk_conv by auto lemma hd_in_awalk_verts: "awalk u p v ⟹ u ∈ set (awalk_verts u p)" "apath u p v ⟹ u ∈ set (awalk_verts u p)" by (case_tac [!]p) (auto simp: apath_def) lemma awalk_Cons_iff: "awalk u (e # es) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ awalk (head G e) es w" by (auto simp: awalk_def) lemma trail_Cons_iff: "trail u (e # es ) w ⟷ e ∈ arcs G ∧ u = tail G e ∧ e ∉ set es ∧ trail (head G e) es w" by (auto simp: trail_def awalk_Cons_iff) lemma apath_Cons_iff: "apath u (e # es) w ⟷ e ∈ arcs G ∧ tail G e = u ∧ apath (head G e) es w ∧ tail G e ∉ set (awalk_verts (head G e) es)" (is "?L ⟷ ?R") by (auto simp: apath_def awalk_Cons_iff) lemmas awalk_simps = awalk_Nil_iff awalk_Cons_iff lemmas trail_simps = trail_Nil_iff trail_Cons_iff lemmas apath_simps = apath_Nil_iff apath_Cons_iff lemma arc_implies_awalk: "e ∈ arcs G ⟹ awalk (tail G e) [e] (head G e)" by (simp add: awalk_simps) lemma apath_nonempty_ends: assumes "apath u p v" assumes "p ≠ []" shows "u ≠ v" using assms proof (induct p arbitrary: u) case (Cons e es) then have "apath (head G e) es v" "u ∉ set (awalk_verts (head G e) es)" by (auto simp: apath_Cons_iff) moreover then have "v ∈ set (awalk_verts (head G e) es)" by (auto simp: apath_def) ultimately show "u ≠ v" by auto qed simp (* replace by awalk_Cons_iff?*) lemma awalk_ConsI: assumes "awalk v es w" assumes "e ∈ arcs G" and "arc_to_ends G e = (u,v)" shows "awalk u (e # es) w" using assms by (cases es) (auto simp: awalk_def arc_to_ends_def) lemma (in pre_digraph) awalkI_apath: assumes "apath u p v" shows "awalk u p v" using assms by (simp add: apath_def) lemma arcE: assumes "arc e (u,v)" assumes "⟦e ∈ arcs G; tail G e = u; head G e = v⟧ ⟹ P" shows "P" using assms by (auto simp: arc_def) lemma in_arcs_imp_in_arcs_ends: assumes "e ∈ arcs G" shows "(tail G e, head G e) ∈ arcs_ends G" using assms by (auto simp: arcs_ends_conv) lemma set_awalk_verts_cas: assumes "cas u p v" shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)" using assms proof (induct p arbitrary: u) case Nil then show ?case by simp next case (Cons e es) then have "set (awalk_verts (head G e) es) = {head G e} ∪ set (map (tail G) es) ∪ set (map (head G) es)" by (auto simp: awalk_Cons_iff) with Cons.prems show ?case by auto qed lemma set_awalk_verts_not_Nil_cas: assumes "cas u p v" "p ≠ []" shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)" proof - have "u ∈ set (map (tail G) p)" using assms by (cases p) auto with assms show ?thesis by (auto simp: set_awalk_verts_cas) qed lemma set_awalk_verts: assumes "awalk u p v" shows "set (awalk_verts u p) = {u} ∪ set (map (tail G) p) ∪ set (map (head G) p)" using assms by (intro set_awalk_verts_cas) blast lemma set_awalk_verts_not_Nil: assumes "awalk u p v" "p ≠ []" shows "set (awalk_verts u p) = set (map (tail G) p) ∪ set (map (head G) p)" using assms by (intro set_awalk_verts_not_Nil_cas) blast lemma awhd_of_awalk: "awalk u p v ⟹ awhd u p = u" and awlast_of_awalk: "awalk u p v ⟹ NOMATCH (awlast u p) v ⟹ awlast u p = v" unfolding NOMATCH_def by auto lemmas awends_of_awalk[simp] = awhd_of_awalk awlast_of_awalk lemma awalk_verts_arc1: assumes "e ∈ set p" shows "tail G e ∈ set (awalk_verts u p)" using assms by (auto simp: awalk_verts_conv) lemma awalk_verts_arc2: assumes "awalk u p v" "e ∈ set p" shows "head G e ∈ set (awalk_verts u p)" using assms by (simp add: set_awalk_verts) lemma awalk_induct_raw[case_names Base Cons(*, induct pred: awalk*)]: assumes "awalk u p v" assumes "⋀w1. w1 ∈ verts G ⟹ P w1 [] w1" assumes "⋀w1 w2 e es. e ∈ arcs G ⟹ arc_to_ends G e = (w1, w2) ⟹ P w2 es v ⟹ P w1 (e # es) v" shows "P u p v" using assms proof (induct p arbitrary: u v) case Nil then show ?case using Nil.prems by auto next case (Cons e es) from Cons.prems(1) show ?case by (intro Cons) (auto intro: Cons(2-) simp: arc_to_ends_def awalk_Cons_iff) qed subsection ‹Appending awalks› lemma (in pre_digraph) cas_append_iff[simp]: "cas u (p @ q) v ⟷ cas u p (awlast u p) ∧ cas (awlast u p) q v" by (induct u p v rule: cas.induct) auto lemma cas_ends: assumes "cas u p v" "cas u' p v'" shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms by (induct u p v arbitrary: u u' rule: cas.induct) auto lemma awalk_ends: assumes "awalk u p v" "awalk u' p v'" shows "(p ≠ [] ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms by (simp add: awalk_def cas_ends) lemma awalk_ends_eqD: assumes "awalk u p u" "awalk v p w" shows "v = w" using awalk_ends[OF assms(1,2)] by auto lemma awalk_empty_ends: assumes "awalk u [] v" shows "u = v" using assms by (auto simp: awalk_def) lemma apath_ends: assumes "apath u p v" and "apath u' p v'" shows "(p ≠ [] ∧ u ≠ v ∧ u = u' ∧ v = v') ∨ (p = [] ∧ u = v ∧ u' = v')" using assms unfolding apath_def by (metis assms(2) apath_nonempty_ends awalk_ends) lemma awalk_append_iff[simp]: "awalk u (p @ q) v ⟷ awalk u p (awlast u p) ∧ awalk (awlast u p) q v" (is "?L ⟷ ?R") by (auto simp: awalk_def intro: awlast_in_verts) lemma awlast_append: "awlast u (p @ q) = awlast (awlast u p) q" by (simp add: awalk_verts_conv) lemma awhd_append: "awhd u (p @ q) = awhd (awhd u q) p" by (simp add: awalk_verts_conv) declare awalkE[rule del] lemma awalkE'[elim]: assumes "awalk u p v" obtains "set (awalk_verts u p) ⊆ verts G" "set p ⊆ arcs G" "cas u p v" "awhd u p = u" "awlast u p = v" "u ∈ verts G" "v ∈ verts G" proof - have "u ∈ set (awalk_verts u p)" "v ∈ set (awalk_verts u p)" using assms by (auto simp: hd_in_awalk_verts elim: awalkE) then show ?thesis using assms by (auto elim: awalkE intro: that) qed lemma awalk_appendI: assumes "awalk u p v" assumes "awalk v q w" shows "awalk u (p @ q) w" using assms proof (induct p arbitrary: u) case Nil then show ?case by auto next case (Cons e es) from Cons.prems have ee_e: "arc_to_ends G e = (u, head G e)" unfolding arc_to_ends_def by auto have "awalk (head G e) es v" using ee_e Cons(2) awalk_Cons_iff by auto then show ?case using Cons ee_e by (auto simp: awalk_Cons_iff) qed lemma awalk_verts_append_cas: assumes "cas u (p @ q) v" shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)" using assms proof (induct p arbitrary: u) case Nil then show ?case by (cases q) auto qed (auto simp: awalk_Cons_iff) lemma awalk_verts_append: assumes "awalk u (p @ q) v" shows "awalk_verts u (p @ q) = awalk_verts u p @ tl (awalk_verts (awlast u p) q)" using assms by (intro awalk_verts_append_cas) blast lemma awalk_verts_append2: assumes "awalk u (p @ q) v" shows "awalk_verts u (p @ q) = butlast (awalk_verts u p) @ awalk_verts (awlast u p) q" using assms by (auto simp: awalk_verts_conv) lemma apath_append_iff: "apath u (p @ q) v ⟷ apath u p (awlast u p) ∧ apath (awlast u p) q v ∧ set (awalk_verts u p) ∩ set (tl (awalk_verts (awlast u p) q)) = {}" (is "?L ⟷ ?R") proof assume ?L then have "distinct (awalk_verts (awlast u p) q)" by (auto simp: apath_def awalk_verts_append2) with ‹?L› show ?R by (auto simp: apath_def awalk_verts_append) next assume ?R then show ?L by (auto simp: apath_def awalk_verts_append dest: distinct_tl) qed lemma (in wf_digraph) set_awalk_verts_append_cas: assumes "cas u p v" "cas v q w" shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)" proof - from assms have cas_pq: "cas u (p @ q) w" by (simp add: awlast_if_cas) moreover from assms have "v ∈ set (awalk_verts u p)" by (metis awalk_verts_non_Nil awlast_if_cas last_in_set) ultimately show ?thesis using assms by (auto simp: set_awalk_verts_cas) qed lemma (in wf_digraph) set_awalk_verts_append: assumes "awalk u p v" "awalk v q w" shows "set (awalk_verts u (p @ q)) = set (awalk_verts u p) ∪ set (awalk_verts v q)" proof - from assms have "awalk u (p @ q) w" by auto moreover with assms have "v ∈ set (awalk_verts u (p @ q))" by (auto simp: awalk_verts_append) ultimately show ?thesis using assms by (auto simp: set_awalk_verts) qed lemma cas_takeI: assumes "cas u p v" "awlast u (take n p) = v'" shows "cas u (take n p) v'" proof - from assms have "cas u (take n p @ drop n p) v" by simp with assms show ?thesis unfolding cas_append_iff by simp qed lemma cas_dropI: assumes "cas u p v" "awlast u (take n p) = u'" shows "cas u' (drop n p) v" proof - from assms have "cas u (take n p @ drop n p) v" by simp with assms show ?thesis unfolding cas_append_iff by simp qed lemma awalk_verts_take_conv: assumes "cas u p v" shows "awalk_verts u (take n p) = take (Suc n) (awalk_verts u p)" proof - from assms have "cas u (take n p) (awlast u (take n p))" by (auto intro: cas_takeI) with assms show ?thesis by (cases n p rule: nat.exhaust[case_product list.exhaust]) (auto simp: awalk_verts_conv' take_map simp del: awalk_verts.simps) qed lemma awalk_verts_drop_conv: assumes "cas u p v" shows "awalk_verts u' (drop n p) = (if n < length p then drop n (awalk_verts u p) else [u'])" using assms by (auto simp: awalk_verts_conv drop_map) lemma awalk_decomp_verts: assumes cas: "cas u p v" and ev_decomp: "awalk_verts u p = xs @ y # ys" obtains q r where "cas u q y" "cas y r v" "p = q @ r" "awalk_verts u q = xs @ [y]" "awalk_verts y r = y # ys" using assms proof - define q r where "q = take (length xs) p" and "r = drop (length xs) p" then have p: "p = q @ r" by simp moreover from p have "cas u q (awlast u q)" "cas (awlast u q) r v" using ‹cas u p v› by auto moreover have "awlast u q = y" using q_def and assms by (auto simp: awalk_verts_take_conv) moreover have *: "awalk_verts u q = xs @ [awlast u q]" using assms q_def by (auto simp: awalk_verts_take_conv) moreover from * have "awalk_verts y r = y # ys" unfolding q_def r_def using assms by (auto simp: awalk_verts_drop_conv not_less) ultimately show ?thesis by (intro that) auto qed lemma awalk_decomp: assumes "awalk u p v" assumes "w ∈ set (awalk_verts u p)" shows "∃q r. p = q @ r ∧ awalk u q w ∧ awalk w r v" proof - from assms have "cas u p v" by auto moreover from assms obtain xs ys where "awalk_verts u p = xs @ w # ys" by (auto simp: in_set_conv_decomp) ultimately obtain q r where "cas u q w" "cas w r v" "p = q @ r" "awalk_verts u q = xs @ [w]" by (auto intro: awalk_decomp_verts) with assms show ?thesis by auto qed lemma awalk_not_distinct_decomp: assumes "awalk u p v" assumes "¬ distinct (awalk_verts u p)" shows "∃q r s. p = q @ r @ s ∧ distinct (awalk_verts u q) ∧ 0 < length r ∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)" proof - from assms obtain xs ys zs y where pv_decomp: "awalk_verts u p = xs @ y # ys @ y # zs" and xs_y_props: "distinct xs" "y ∉ set xs" "y ∉ set ys" using not_distinct_decomp_min_prefix by blast obtain q p' where "cas u q y" "p = q @ p'" "awalk_verts u q = xs @ [y]" and p'_props: "cas y p' v" "awalk_verts y p' = (y # ys) @ y # zs" using assms pv_decomp by - (rule awalk_decomp_verts, auto) obtain r s where "cas y r y" "cas y s v" "p' = r @ s" "awalk_verts y r = y # ys @ [y]" "awalk_verts y s = y # zs" using p'_props by (rule awalk_decomp_verts) auto have "p = q @ r @ s" using ‹p = q @ p'› ‹p' = r @ s› by simp moreover have "distinct (awalk_verts u q)" using ‹awalk_verts u q = xs @ [y]› and xs_y_props by simp moreover have "0 < length r" using ‹awalk_verts y r = y # ys @ [y]› by auto moreover from pv_decomp assms have "y ∈ verts G" by auto then have "awalk u q y" "awalk y r y" "awalk y s v" using ‹awalk u p v› ‹cas u q y› ‹cas y r y› ‹cas y s v› unfolding ‹p = q @ r @ s› by (auto simp: awalk_def) ultimately show ?thesis by blast qed lemma apath_decomp_disjoint: assumes "apath u p v" assumes "p = q @ r" assumes "x ∈ set (awalk_verts u q)" "x ∈ set (tl (awalk_verts (awlast u q) r))" shows False using assms by (auto simp: apath_def awalk_verts_append) subsection ‹Cycles› definition closed_w :: "'b awalk ⇒ bool" where "closed_w p ≡ ∃u. awalk u p u ∧ 0 < length p" text ‹ The definitions of cycles in textbooks vary w.r.t to the minimial length of a cycle. The definition given here matches \<^cite>‹"diestel2010graph"›. \<^cite>‹"bangjensen2009digraphs"› excludes loops from being cycles. Volkmann (Lutz Volkmann: Graphen an allen Ecken und Kanten, 2006 (?)) places no restriction on the length in the definition, but later usage assumes cycles to be non-empty. › definition (in pre_digraph) cycle :: "'b awalk ⇒ bool" where "cycle p ≡ ∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ p ≠ []" lemma cycle_altdef: "cycle p ⟷ closed_w p ∧ (∃u. distinct (tl (awalk_verts u p)))" by (cases p) (auto simp: closed_w_def cycle_def) lemma (in wf_digraph) distinct_tl_verts_imp_distinct: assumes "awalk u p v" assumes "distinct (tl (awalk_verts u p))" shows "distinct p" proof (rule ccontr) assume "¬distinct p" then obtain e xs ys zs where p_decomp: "p = xs @ e # ys @ e # zs" by (blast dest: not_distinct_decomp_min_prefix) then show False using assms p_decomp by (auto simp: awalk_verts_append awalk_Cons_iff set_awalk_verts) qed lemma (in wf_digraph) distinct_verts_imp_distinct: assumes "awalk u p v" assumes "distinct (awalk_verts u p)" shows "distinct p" using assms by (blast intro: distinct_tl_verts_imp_distinct distinct_tl) lemma (in wf_digraph) cycle_conv: "cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ distinct p ∧ p ≠ [])" unfolding cycle_def by (auto intro: distinct_tl_verts_imp_distinct) lemma (in loopfree_digraph) cycle_digraph_conv: "cycle p ⟷ (∃u. awalk u p u ∧ distinct (tl (awalk_verts u p)) ∧ 2 ≤ length p)" (is "?L ⟷ ?R") proof assume "cycle p" then obtain u where *: "awalk u p u" "distinct (tl (awalk_verts u p))" "p ≠ []" unfolding cycle_def by auto have "2 ≤ length p" proof (rule ccontr) assume "¬?thesis" with * obtain e where "p=[e]" by (cases p) (auto simp: not_le) then show False using * by (auto simp: awalk_simps dest: no_loops) qed then show ?R using * by auto qed (auto simp: cycle_def) lemma (in wf_digraph) closed_w_imp_cycle: assumes "closed_w p" shows "∃p. cycle p" using assms proof (induct "length p" arbitrary: p rule: less_induct) case less then obtain u where *: "awalk u p u" "p ≠ []" by (auto simp: closed_w_def) show ?thesis proof cases assume "distinct (tl (awalk_verts u p))" with less show ?thesis by (auto simp: closed_w_def cycle_altdef) next assume A: "¬distinct (tl (awalk_verts u p))" then obtain e es where "p = e # es" by (cases p) auto with A * have **: "awalk (head G e) es u" "¬distinct (awalk_verts (head G e) es)" by (auto simp: awalk_Cons_iff) obtain q r s where "es = q @ r @ s" "∃w. awalk w r w" "closed_w r" using awalk_not_distinct_decomp[OF **] by (auto simp: closed_w_def) then have "length r < length p" using ‹p = _› by auto then show ?thesis using ‹closed_w r› by (rule less) qed qed subsection ‹Reachability› lemma reachable1_awalk: "u →⇧^{+}v ⟷ (∃p. awalk u p v ∧ p ≠ [])" proof assume "u →⇧^{+}v" then show "∃p. awalk u p v ∧ p ≠ []" proof (induct rule: converse_trancl_induct) case (base y) then obtain e where "e ∈ arcs G" "tail G e = y" "head G e = v" by auto with arc_implies_awalk show ?case by auto next case (step x y) then obtain p where "awalk y p v" "p ≠ []" by auto moreover from ‹x → y› obtain e where "tail G e = x" "head G e = y" "e ∈ arcs G" by auto ultimately have "awalk x (e # p) v" by (auto simp: awalk_Cons_iff) then show ?case by auto qed next assume "∃p. awalk u p v ∧ p ≠ []" then obtain p where "awalk u p v" "p ≠ []" by auto thus "u →⇧^{+}v" proof (induct p arbitrary: u) case (Cons a as) then show ?case by (cases "as = []") (auto simp: awalk_simps trancl_into_trancl2 dest: in_arcs_imp_in_arcs_ends) qed simp qed lemma reachable_awalk: "u →⇧^{*}v ⟷ (∃p. awalk u p v)" proof cases assume "u = v" have "u →⇧^{*}u ⟷ awalk u [] u" by (auto simp: awalk_Nil_iff reachable_in_verts) also have "… ⟷ (∃p. awalk u p u)" by (metis awalk_Nil_iff awalk_hd_in_verts) finally show ?thesis using ‹u = v› by simp next assume "u ≠ v" then have "u →⇧^{*}v ⟷ u →⇧^{+}v" by auto also have "… ⟷ (∃p. awalk u p v)" using ‹u ≠ v› unfolding reachable1_awalk by force finally show ?thesis . qed lemma reachable_awalkI[intro?]: assumes "awalk u p v" shows "u →⇧^{*}v" unfolding reachable_awalk using assms by auto lemma reachable1_awalkI: "awalk v p w ⟹ p ≠ [] ⟹ v →⇧^{+}w" by (auto simp add: reachable1_awalk) lemma reachable_arc_trans: assumes "u →⇧^{*}v" "arc e (v,w)" shows "u →⇧^{*}w" proof - from ‹u →⇧^{*}v› obtain p where "awalk u p v" by (auto simp: reachable_awalk) moreover have "awalk v [e] w" using ‹arc e (v,w)› by (auto simp: arc_def awalk_def) ultimately have "awalk u (p @ [e]) w" by (rule awalk_appendI) then show ?thesis .. qed lemma awalk_verts_reachable_from: assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "u →⇧^{*}⇘G⇙ w" proof - obtain s where "awalk u s w" using awalk_decomp[OF assms] by blast then show ?thesis by (metis reachable_awalk) qed lemma awalk_verts_reachable_to: assumes "awalk u p v" "w ∈ set (awalk_verts u p)" shows "w →⇧^{*}⇘G⇙ v" proof - obtain s where "awalk w s v" using awalk_decomp[OF assms] by blast then show ?thesis by (metis reachable_awalk) qed subsection ‹Paths› lemma (in fin_digraph) length_apath_less: assumes "apath u p v" shows "length p < card (verts G)" proof - have "length p < length (awalk_verts u p)" unfolding awalk_verts_conv by (auto simp: awalk_verts_conv) also have "length (awalk_verts u p) = card (set (awalk_verts u p))" using ‹apath u p v› by (auto simp: apath_def distinct_card) also have "… ≤ card (verts G)" using ‹apath u p v› unfolding apath_def awalk_conv by (auto intro: card_mono) finally show ?thesis . qed lemma (in fin_digraph) length_apath: assumes "apath u p v" shows "length p ≤ card (verts G)" using length_apath_less[OF assms] by auto lemma (in fin_digraph) apaths_finite_triple: shows "finite {(u,p,v). apath u p v}" proof - have "⋀u p v. awalk u p v ⟹ distinct (awalk_verts u p) ⟹length p ≤ card (verts G)" by (rule length_apath) (auto simp: apath_def) then have "{(u,p,v). apath u p v} ⊆ verts G × {es. set es ⊆ arcs G ∧ length es ≤ card (verts G)} × verts G" by (auto simp: apath_def) moreover have "finite ..." using finite_verts finite_arcs by (intro finite_cartesian_product finite_lists_length_le) ultimately show ?thesis by (rule finite_subset) qed lemma (in fin_digraph) apaths_finite: shows "finite {p. apath u p v}" proof - have "{p. apath u p v} ⊆ (fst o snd) ` {(u,p,v). apath u p v}" by force with apaths_finite_triple show ?thesis by (rule finite_surj) qed fun is_awalk_cyc_decomp :: "'b awalk => ('b awalk × 'b awalk × 'b awalk) ⇒ bool" where "is_awalk_cyc_decomp p (q,r,s) ⟷ p = q @ r @ s ∧ (∃u v w. awalk u q v ∧ awalk v r v ∧ awalk v s w) ∧ 0 <length r ∧ (∃u. distinct (awalk_verts u q))" definition awalk_cyc_decomp :: "'b awalk ⇒ 'b awalk × 'b awalk × 'b awalk" where "awalk_cyc_decomp p = (SOME qrs. is_awalk_cyc_decomp p qrs)" function awalk_to_apath :: "'b awalk ⇒ 'b awalk" where "awalk_to_apath p = (if ¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v) then (let (q,r,s) = awalk_cyc_decomp p in awalk_to_apath (q @ s)) else p)" by auto lemma awalk_cyc_decomp_has_prop: assumes "awalk u p v" and "¬distinct (awalk_verts u p)" shows "is_awalk_cyc_decomp p (awalk_cyc_decomp p)" proof - obtain q r s where *: "p = q @ r @ s ∧ distinct (awalk_verts u q) ∧ 0 < length r ∧ (∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v)" by (atomize_elim) (rule awalk_not_distinct_decomp[OF assms]) then have "∃x. is_awalk_cyc_decomp p x" by (intro exI[where x="(q,r,s)"]) auto then show ?thesis unfolding awalk_cyc_decomp_def .. qed lemma awalk_cyc_decompE: assumes dec: "awalk_cyc_decomp p = (q,r,s)" assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)" obtains "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" proof show "p = q @ r @ s" "distinct (awalk_verts u q)" "closed_w r" using awalk_cyc_decomp_has_prop[OF p_props] and dec by (auto simp: closed_w_def awalk_verts_conv) then have "p ≠ []" by (auto simp: closed_w_def) (* TODO: Can we find some general rules to prove the last property?*) obtain u' w' v' where obt_awalk: "awalk u' q w'" "awalk w' r w'" "awalk w' s v'" using awalk_cyc_decomp_has_prop[OF p_props] and dec by auto then have "awalk u' p v'" using ‹p = q @ r @ s› by simp then have "u = u'" and "v = v'" using ‹p ≠ []› ‹awalk u p v› by (metis awalk_ends)+ then have "awalk u q w'" "awalk w' r w'" "awalk w' s v" using obt_awalk by auto then show "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" by auto qed lemma awalk_cyc_decompE': assumes p_props: "awalk u p v" "¬distinct (awalk_verts u p)" obtains q r s where "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" proof - obtain q r s where "awalk_cyc_decomp p = (q,r,s)" by (cases "awalk_cyc_decomp p") auto then have "p = q @ r @ s" "distinct (awalk_verts u q)" "∃w. awalk u q w ∧ awalk w r w ∧ awalk w s v" "closed_w r" using assms by (auto elim: awalk_cyc_decompE) then show ?thesis .. qed termination awalk_to_apath proof (relation "measure length") fix G p qrs rs q r s have X: "⋀x y. closed_w r ⟹ awalk x r y ⟹ x = y" unfolding closed_w_def by (blast dest: awalk_ends) assume "¬(∃u. distinct (awalk_verts u p)) ∧(∃u v. awalk u p v)" and **:"qrs = awalk_cyc_decomp p" "(q, rs) = qrs" "(r, s) = rs" then obtain u v where *: "awalk u p v" "¬distinct (awalk_verts u p)" by (cases p) auto then have "awalk_cyc_decomp p = (q,r,s)" using ** by simp then have "is_awalk_cyc_decomp p (q,r,s)" apply (rule awalk_cyc_decompE[OF _ *]) using X[of "awlast u q" "awlast (awlast u q) r"] *(1) by (auto simp: closed_w_def) then show "(q @ s, p) ∈ measure length" by (auto simp: closed_w_def) qed simp declare awalk_to_apath.simps[simp del] lemma awalk_to_apath_induct[consumes 1, case_names path decomp]: assumes awalk: "awalk u p v" assumes dist: "⋀p. awalk u p v ⟹ distinct (awalk_verts u p) ⟹ P p" assumes dec: "⋀p q r s. ⟦awalk u p v; awalk_cyc_decomp p = (q,r,s); ¬distinct (awalk_verts u p); P (q @ s)⟧ ⟹ P p" shows "P p" using awalk proof (induct "length p" arbitrary: p rule: less_induct) case less show ?case proof (cases "distinct (awalk_verts u p)") case True then show ?thesis by (auto intro: dist less.prems) next case False obtain q r s where p_cdecomp: "awalk_cyc_decomp p = (q,r,s)" by (cases "awalk_cyc_decomp p") auto then have "is_awalk_cyc_decomp p (q,r,s)" "p = q @ r @ s" using awalk_cyc_decomp_has_prop[OF less.prems(1) False] by auto then have "length (q @ s) < length p" "awalk u (q @ s) v" using less.prems by (auto dest!: awalk_ends_eqD) then have "P (q @ s)" by (auto intro: less) with p_cdecomp False show ?thesis by (auto intro: dec less.prems) qed qed lemma step_awalk_to_apath: assumes awalk: "awalk u p v" and decomp: "awalk_cyc_decomp p = (q, r, s)" and dist: "¬ distinct (awalk_verts u p)" shows "awalk_to_apath p = awalk_to_apath (q @ s)" proof - from dist have "¬(∃u. distinct (awalk_verts u p))" by (auto simp: awalk_verts_conv) with awalk and decomp show "awalk_to_apath p = awalk_to_apath (q @ s)" by (auto simp: awalk_to_apath.simps) qed lemma apath_awalk_to_apath: assumes "awalk u p v" shows "apath u (awalk_to_apath p) v" using assms proof (induct rule: awalk_to_apath_induct) case (path p) then have "awalk_to_apath p = p" by (auto simp: awalk_to_apath.simps) then show ?case using path by (auto simp: apath_def) next case (decomp p q r s) then show ?case using step_awalk_to_apath[of _ p _ q r s] by simp qed lemma (in wf_digraph) awalk_to_apath_subset: assumes "awalk u p v" shows "set (awalk_to_apath p) ⊆ set p" using assms proof (induct rule: awalk_to_apath_induct) case (path p) then have "awalk_to_apath p = p" by (auto simp: awalk_to_apath.simps) then show ?case by simp next case (decomp p q r s) have *: "¬(∃u. distinct (awalk_verts u p)) ∧ (∃u v. awalk u p v)" using decomp by (cases p) auto have "set (awalk_to_apath (q @ s)) ⊆ set p" using decomp by (auto elim!: awalk_cyc_decompE) then show ?case by (subst awalk_to_apath.simps) (simp only: * simp_thms if_True decomp Let_def prod.simps) qed lemma reachable_apath: "u →⇧^{*}v ⟷ (∃p. apath u p v)" by (auto intro: awalkI_apath apath_awalk_to_apath simp: reachable_awalk) lemma no_loops_in_apath: assumes "apath u p v" "a ∈ set p" shows "tail G a ≠ head G a" proof - from ‹a ∈ set p› obtain p1 p2 where "p = p1 @ a # p2" by (auto simp: in_set_conv_decomp) with ‹apath u p v› have "apath (tail G a) ([a] @ p2) (v)" by (auto simp: apath_append_iff apath_Cons_iff apath_Nil_iff) then have "apath (tail G a) [a] (head G a)" by - (drule apath_append_iff[THEN iffD1], simp) then show ?thesis by (auto simp: apath_Cons_iff) qed end end