Theory Arc_Walk

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