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 *Gw"
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 *Gv"
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