Session Graph_Theory

Theory Rtrancl_On

(* Title:  Rtrancl_On.thy
   Author: Lars Noschinski, TU München
   Author: René Neumann, TU München
*)

theory Rtrancl_On
imports Main
begin

section ‹Reflexive-Transitive Closure on a Domain›

text ‹
  In this section we introduce a variant of the reflexive-transitive closure
  of a relation which is useful to formalize the reachability relation on
  digraphs.
›

inductive_set
  rtrancl_on :: "'a set  'a rel  'a rel"
  for F :: "'a set" and r :: "'a rel"
where
    rtrancl_on_refl [intro!, Pure.intro!, simp]: "a  F  (a, a)  rtrancl_on F r"
  | rtrancl_on_into_rtrancl_on [Pure.intro]:
      "(a, b)  rtrancl_on F r   (b, c)  r  c  F
       (a, c)  rtrancl_on F r"

definition symcl :: "'a rel  'a rel" ("(_s)" [1000] 999) where
  "symcl R = R  (λ(a,b). (b,a)) ` R"

lemma in_rtrancl_on_in_F:
  assumes "(a,b)  rtrancl_on F r" shows "a  F" "b  F"
  using assms by induct auto

lemma rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
  assumes "(a, b)  rtrancl_on F r"
    and "a  F  P a"
        "y z. (a, y)  rtrancl_on F r; (y,z)  r; y  F; z  F; P y  P z"
  shows "P b"
  using assms by (induct a b) (auto dest: in_rtrancl_on_in_F)

lemma rtrancl_on_trans:
  assumes "(a,b)  rtrancl_on F r" "(b,c)  rtrancl_on F r" shows "(a,c)  rtrancl_on F r"
  using assms(2,1)
  by induct (auto intro: rtrancl_on_into_rtrancl_on)

lemma converse_rtrancl_on_into_rtrancl_on:
  assumes "(a,b)  r" "(b, c)  rtrancl_on F r" "a  F"
  shows "(a, c)  rtrancl_on F r"
proof -
  have "b  F" using (b,c)  _ by (rule in_rtrancl_on_in_F)
  show ?thesis
    apply (rule rtrancl_on_trans)
    apply (rule rtrancl_on_into_rtrancl_on)
    apply (rule rtrancl_on_refl)
    by fact+
qed

lemma rtrancl_on_converseI:
  assumes "(y, x)  rtrancl_on F r" shows "(x, y)  rtrancl_on F (r¯)"
  using assms
proof induct
  case (step a b)
  then have "(b,b)  rtrancl_on F (r¯)" "(b,a)  r¯" by auto
  then show ?case using step
    by (metis rtrancl_on_trans rtrancl_on_into_rtrancl_on)
qed auto

theorem rtrancl_on_converseD:
  assumes "(y, x)  rtrancl_on F (r¯)" shows "(x, y)  rtrancl_on F r"
  using assms by - (drule rtrancl_on_converseI, simp)

lemma converse_rtrancl_on_induct[consumes 1, case_names base step, induct set: rtrancl_on]:
  assumes major: "(a, b)  rtrancl_on F r"
    and cases: "b  F  P b"
       "x y. (x,y)  r; (y,b)  rtrancl_on F r; x  F; y  F; P y  P x"
  shows "P a"
  using rtrancl_on_converseI[OF major] cases
  by induct (auto intro: rtrancl_on_converseD)

lemma converse_rtrancl_on_cases:
  assumes "(a, b)  rtrancl_on F r"
  obtains (base) "a = b" "b  F"
    | (step) c where "(a,c)  r" "(c,b)  rtrancl_on F r"
  using assms by induct auto

lemma rtrancl_on_sym:
  assumes "sym r" shows "sym (rtrancl_on F r)"
using assms by (auto simp: sym_conv_converse_eq intro: symI dest: rtrancl_on_converseI)

lemma rtrancl_on_mono:
  assumes "s  r" "F  G" "(a,b)  rtrancl_on F s" shows "(a,b)  rtrancl_on G r"
  using assms(3,1,2)
proof induct
  case (step x y) show ?case
    using step assms by (intro converse_rtrancl_on_into_rtrancl_on[OF _ step(5)]) auto
qed auto

lemma rtrancl_consistent_rtrancl_on:
  assumes "(a,b)  r*"
  and "a  F" "b  F"
  and consistent: "a b.  a  F; (a,b)  r   b  F"
  shows "(a,b)  rtrancl_on F r"
  using assms(1-3)
proof (induction rule: converse_rtrancl_induct)
  case (step y z) then have "z  F" by (rule_tac consistent) simp
  with step have "(z,b)  rtrancl_on F r" by simp
  with step.prems (y,z)  r z  F show ?case
    using converse_rtrancl_on_into_rtrancl_on
    by metis
qed simp

lemma rtrancl_on_rtranclI:
  "(a,b)  rtrancl_on F r  (a,b)  r*"
  by (induct rule: rtrancl_on_induct) simp_all

lemma rtrancl_on_sub_rtrancl:
  "rtrancl_on F r  r^*"
  using rtrancl_on_rtranclI
  by auto



end

Theory Stuff

(* Title:  Stuff.thy
   Author: Lars Noschinski, TU München
*)

theory Stuff
imports
  Main
  "HOL-Library.Extended_Real"

begin

section ‹Additional theorems for base libraries›

text ‹
  This section contains lemmas unrelated to graph theory which might be
  interesting for the Isabelle distribution
›

lemma ereal_Inf_finite_Min:
  fixes S :: "ereal set"
  assumes "finite S" and "S  {}"
  shows "Inf S = Min S"
using assms
by (induct S rule: finite_ne_induct) (auto simp: min_absorb1)

lemma finite_INF_in:
  fixes f :: "'a  ereal"
  assumes "finite S"
  assumes "S  {}"
  shows "(INF s S. f s)  f ` S"
proof -
  from assms
  have "finite (f ` S)" "f ` S  {}" by auto
  then show "Inf (f ` S)  f ` S"
    using ereal_Inf_finite_Min [of "f ` S"]  by simp
qed

lemma not_mem_less_INF:
  fixes f :: "'a  'b :: complete_lattice"
  assumes "f x < (INF s S. f s)"
  assumes "x  S"
  shows "False"
using assms by (metis INF_lower less_le_not_le)

lemma sym_diff:
  assumes "sym A" "sym B" shows "sym (A - B)"
using assms by (auto simp: sym_def)



subsection ‹List›

lemmas list_exhaust2 = list.exhaust[case_product list.exhaust]

lemma list_exhaust_NSC:
  obtains (Nil) "xs = []" | (Single) x where "xs = [x]" | (Cons_Cons) x y ys where "xs = x # y # ys"
by (metis list.exhaust)

lemma tl_rev:
  "tl (rev p) = rev (butlast p)"
by (induct p) auto

lemma butlast_rev:
  "butlast (rev p) = rev (tl p)"
by (induct p) auto

lemma take_drop_take:
   "take n xs @ drop n (take m xs) = take (max n m) xs"
proof cases
  assume "m < n" then show ?thesis by (auto simp: max_def)
next
  assume "¬m < n"
  then have "take n xs = take n (take m xs)" by (auto simp: min_def)
  then show ?thesis by (simp del: take_take add: max_def)
qed

lemma drop_take_drop:
  "drop n (take m xs) @ drop m xs = drop (min n m) xs"
proof cases
  assume A: "¬m < n"
  then show ?thesis
    using drop_append[of n "take m xs" "drop m xs"]
  by (cases "length xs < n") (auto simp: not_less min_def)
qed (auto simp: min_def)

lemma not_distinct_decomp_min_prefix:
  assumes "¬ distinct ws"
  shows " xs ys zs y. ws = xs @ y # ys @ y # zs  distinct xs  y  set xs  y  set ys "
proof -
  obtain xs y ys where "y  set xs" "distinct xs" "ws = xs @ y # ys"
    using assms by (auto simp: not_distinct_conv_prefix)
  moreover then obtain xs' ys' where "xs = xs' @ y # ys'" by (auto simp: in_set_conv_decomp)
  ultimately show ?thesis by auto
qed

lemma not_distinct_decomp_min_not_distinct:
  assumes "¬ distinct ws"
  shows "xs y ys zs. ws = xs @ y # ys @ y # zs  distinct (ys @ [y])"
using assms
proof (induct ws)
  case (Cons w ws)
  show ?case
  proof (cases "distinct ws")
    case True
    then obtain xs ys where "ws = xs @ w # ys" "w  set xs"
      using Cons.prems by (fastforce dest: split_list_first)
    then have "distinct (xs @ [w])" "w # ws = [] @ w # xs @ w # ys"
      using ‹distinct ws by auto
    then show ?thesis by blast
  next
    case False
    then obtain xs y ys zs where "ws = xs @ y # ys @ y # zs  distinct (ys @ [y])"
      using Cons by auto
    then have "w # ws = (w # xs) @ y # ys @ y # zs  distinct (ys @ [y])"
      by simp
    then show ?thesis by blast
  qed
qed simp

lemma card_Ex_subset:
  "k  card M  N. N  M  card N = k"
by (induct rule: inc_induct) (auto simp: card_Suc_eq)

lemma list_set_tl: "x  set (tl xs)  x  set xs"
by (cases xs) auto


section ‹NOMATCH simproc›

text ‹
 The simplification procedure can be used to avoid simplification of terms of a certain form
›

definition NOMATCH :: "'a  'a  bool" where "NOMATCH val pat  True"
lemma NOMATCH_cong[cong]: "NOMATCH val pat = NOMATCH val pat" by (rule refl)

simproc_setup NOMATCH ("NOMATCH val pat") = fn _ => fn ctxt => fn ct =>
  let
    val thy = Proof_Context.theory_of ctxt
    val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
    val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
  in if m then NONE else SOME @{thm NOMATCH_def} end

text ‹
  This setup ensures that a rewrite rule of the form @{term "NOMATCH val pat  t"}
  is only applied, if the pattern @{term pat} does not match the value @{term val}.
›


end

Theory Digraph

(* Title:  Digraph.thy
   Author: Lars Noschinski, TU München
   Author: René Neumann
*)

theory Digraph
imports
  Main
  Rtrancl_On
  Stuff
begin

section ‹Digraphs›

record ('a,'b) pre_digraph =
  verts :: "'a set"
  arcs :: "'b set"
  tail :: "'b  'a"
  head :: "'b  'a"

definition arc_to_ends :: "('a,'b) pre_digraph  'b  'a × 'a" where
  "arc_to_ends G e  (tail G e, head G e)"

locale pre_digraph =
  fixes G :: "('a, 'b) pre_digraph" (structure)

locale wf_digraph = pre_digraph +
  assumes tail_in_verts[simp]: "e  arcs G  tail G e  verts G"
  assumes head_in_verts[simp]: "e  arcs G  head G e  verts G"
begin

lemma wf_digraph: "wf_digraph G" by intro_locales

lemmas wellformed = tail_in_verts head_in_verts

end

definition arcs_ends :: "('a,'b) pre_digraph  ('a × 'a) set" where
  "arcs_ends G  arc_to_ends G ` arcs G"

definition symmetric :: "('a,'b) pre_digraph  bool" where
  "symmetric G  sym (arcs_ends G)"

text ‹
  Matches "pseudo digraphs" from \cite{bangjensen2009digraphs}, except for
  allowing the null graph. For a discussion of that topic,
  see also \cite{harary1974nullgraph}.
›
locale fin_digraph = wf_digraph +
  assumes finite_verts[simp]: "finite (verts G)"
    and finite_arcs[simp]: "finite (arcs G)"

locale loopfree_digraph = wf_digraph +
  assumes no_loops: "e  arcs G  tail G e  head G e"

locale nomulti_digraph = wf_digraph +
  assumes no_multi_arcs: "e1 e2. e1  arcs G; e2  arcs G;
     arc_to_ends G e1 = arc_to_ends G e2  e1 = e2"

locale sym_digraph = wf_digraph +
  assumes sym_arcs[intro]: "symmetric G"

locale digraph = fin_digraph + loopfree_digraph + nomulti_digraph

text ‹
  We model graphs as symmetric digraphs. This is fine for many purposes,
  but not for all. For example, the path $a,b,a$ is considered to be a cycle
  in a digraph (and hence in a symmetric digraph), but not in an undirected
  graph.
›
locale pseudo_graph = fin_digraph + sym_digraph

locale graph = digraph + pseudo_graph

lemma (in wf_digraph) fin_digraphI[intro]:
  assumes "finite (verts G)"
  assumes "finite (arcs G)"
  shows "fin_digraph G"
using assms by unfold_locales

lemma (in wf_digraph) sym_digraphI[intro]:
  assumes "symmetric G"
  shows "sym_digraph G"
using assms by unfold_locales

lemma (in digraph) graphI[intro]:
  assumes "symmetric G"
  shows "graph G"
using assms by unfold_locales



definition (in wf_digraph) arc :: "'b  'a × 'a  bool" where
  "arc e uv  e  arcs G  tail G e = fst uv  head G e = snd uv"


lemma (in fin_digraph) fin_digraph: "fin_digraph G"
  by unfold_locales

lemma (in nomulti_digraph) nomulti_digraph: "nomulti_digraph G" by unfold_locales

lemma arcs_ends_conv: "arcs_ends G = (λe. (tail G e, head G e)) ` arcs G"
  by (auto simp: arc_to_ends_def arcs_ends_def)

lemma symmetric_conv: "symmetric G  (e1  arcs G. e2  arcs G. tail G e1 = head G e2  head G e1 = tail G e2)"
  unfolding symmetric_def arcs_ends_conv sym_def by auto

lemma arcs_ends_symmetric:
  assumes "symmetric G"
  shows "(u,v)  arcs_ends G  (v,u)  arcs_ends G"
  using assms unfolding symmetric_def sym_def by auto

lemma (in nomulti_digraph) inj_on_arc_to_ends:
  "inj_on (arc_to_ends G) (arcs G)"
  by (rule inj_onI) (rule no_multi_arcs)



subsection ‹Reachability›

abbreviation dominates :: "('a,'b) pre_digraph  'a  'a  bool" ("_ ı _" [100,100] 40) where
  "dominates G u v  (u,v)  arcs_ends G"

abbreviation reachable1 :: "('a,'b) pre_digraph  'a  'a  bool" ("_ +ı _" [100,100] 40) where
  "reachable1 G u v  (u,v)  (arcs_ends G)^+"

definition reachable :: "('a,'b) pre_digraph  'a  'a  bool" ("_ *ı _" [100,100] 40) where
  "reachable G u v  (u,v)  rtrancl_on (verts G) (arcs_ends G)"

lemma reachableE[elim]:
  assumes "u G v"
  obtains e where "e  arcs G" "tail G e = u" "head G e = v"
using assms by (auto simp add: arcs_ends_conv)

lemma (in loopfree_digraph) adj_not_same:
  assumes "a  a" shows "False"
  using assms by (rule reachableE) (auto dest: no_loops)

lemma reachable_in_vertsE:
  assumes "u *G v" obtains "u  verts G" "v  verts G"
  using assms unfolding reachable_def by induct auto

lemma symmetric_reachable:
  assumes "symmetric G" "v *G w" shows "w *G v"
proof -
  have "sym (rtrancl_on (verts G) (arcs_ends G))"
    using assms by (auto simp add: symmetric_def dest: rtrancl_on_sym)
  then show ?thesis using assms unfolding reachable_def by (blast elim: symE)
qed

lemma reachable_rtranclI:
  "u *G  v  (u, v)  (arcs_ends G)*"
  unfolding reachable_def by (rule rtrancl_on_rtranclI)


context wf_digraph begin

lemma adj_in_verts:
  assumes "u G v" shows "u  verts G" "v  verts G"
  using assms unfolding arcs_ends_conv by auto

lemma dominatesI: assumes "arc_to_ends G a = (u,v)" "a  arcs G" shows "u G v"
  using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)

lemma reachable_refl [intro!, Pure.intro!, simp]: "v  verts G  v * v"
  unfolding reachable_def by auto

lemma adj_reachable_trans[trans]:
  assumes "a G b" "b *G c" shows "a *G c"
  using assms by (auto simp: reachable_def intro: converse_rtrancl_on_into_rtrancl_on adj_in_verts)

lemma reachable_adj_trans[trans]:
  assumes "a *G b" "b G c" shows "a *G c"
  using assms by (auto simp: reachable_def intro: rtrancl_on_into_rtrancl_on adj_in_verts)

lemma reachable_adjI [intro, simp]: "u  v  u * v"
  by (auto intro: adj_reachable_trans adj_in_verts)

lemma reachable_trans[trans]:
  assumes "u *v" "v * w" shows "u * w"
  using assms unfolding reachable_def by (rule rtrancl_on_trans)

lemma reachable_induct[consumes 1, case_names base step]:
  assumes major: "u *G v"
    and cases: "u  verts G  P u"
       "x y. u *G x; x G y; P x  P y"
  shows "P v"
  using assms unfolding reachable_def by (rule rtrancl_on_induct) auto

lemma converse_reachable_induct[consumes 1, case_names base step, induct pred: reachable]:
  assumes major: "u *G v"
    and cases: "v  verts G  P v"
       "x y. x G y; y *G v; P y  P x"
  shows "P u"
  using assms unfolding reachable_def by (rule converse_rtrancl_on_induct) auto

lemma (in pre_digraph) converse_reachable_cases:
  assumes "u *G v"
  obtains (base) "u = v" "u  verts G"
    | (step) w where "u G w" "w *G v"
  using assms unfolding reachable_def by (cases rule: converse_rtrancl_on_cases) auto

lemma reachable_in_verts:
  assumes "u * v" shows "u  verts G" "v  verts G"
  using assms by induct (simp_all add: adj_in_verts)

lemma reachable1_in_verts:
  assumes "u + v" shows "u  verts G" "v  verts G"
  using assms
  by induct (simp_all add: adj_in_verts)

lemma reachable1_reachable[intro]:
  "v + w  v * w"
  unfolding reachable_def
  by (rule rtrancl_consistent_rtrancl_on) (simp_all add: reachable1_in_verts adj_in_verts)

lemmas reachable1_reachableE[elim] = reachable1_reachable[elim_format]

lemma reachable_neq_reachable1[intro]:
  assumes reach: "v * w"
  and neq: "v  w"
  shows "v + w"
proof -
  from reach have "(v,w)  (arcs_ends G)^*" by (rule reachable_rtranclI)
  with neq show ?thesis by (auto dest: rtranclD)
qed

lemmas reachable_neq_reachable1E[elim] = reachable_neq_reachable1[elim_format]

lemma reachable1_reachable_trans [trans]:
  "u + v  v * w  u + w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_reachable1_trans [trans]:
  "u * v  v + w  u + w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_conv:
  "u * v  (u,v)  (arcs_ends G)^*  (verts G × verts G)"
  apply (auto intro: reachable_in_verts)
  apply (induct rule: rtrancl_induct)
   apply auto
  done

lemma reachable_conv':
  assumes "u  verts G"
  shows "u * v  (u,v)  (arcs_ends G)*" (is "?L = ?R")
proof
  assume "?R" then show "?L" using assms  by induct auto
qed (auto simp: reachable_conv)


end

lemma (in sym_digraph) symmetric_reachable':
  assumes "v *G w" shows "w *G v"
  using sym_arcs assms by (rule symmetric_reachable)




subsection ‹Degrees of vertices›

definition in_arcs :: "('a, 'b) pre_digraph  'a  'b set" where
  "in_arcs G v  {e  arcs G. head G e = v}"

definition out_arcs :: "('a, 'b) pre_digraph  'a  'b set" where
  "out_arcs G v  {e  arcs G. tail G e = v}"

definition in_degree :: "('a, 'b) pre_digraph  'a  nat" where
  "in_degree G v  card (in_arcs G v)"

definition out_degree :: "('a, 'b) pre_digraph  'a  nat" where
  "out_degree G v  card (out_arcs G v)"

lemma (in fin_digraph) finite_in_arcs[intro]:
  "finite (in_arcs G v)"
  unfolding in_arcs_def by auto

lemma (in fin_digraph) finite_out_arcs[intro]:
  "finite (out_arcs G v)"
  unfolding out_arcs_def by auto

lemma in_in_arcs_conv[simp]:
  "e  in_arcs G v  e  arcs G  head G e = v"
  unfolding in_arcs_def by auto

lemma in_out_arcs_conv[simp]:
  "e  out_arcs G v  e  arcs G  tail G e = v"
  unfolding out_arcs_def by auto

lemma inout_arcs_arc_simps[simp]:
  assumes "e  arcs G"
  shows "tail G e = u  out_arcs G u  insert e E = insert e (out_arcs G u  E)"
        "tail G e  u  out_arcs G u  insert e E = out_arcs G u  E"
        "out_arcs G u  {} = {}" (* XXX: should be unnecessary *)
        "head G e = u  in_arcs G u  insert e E = insert e (in_arcs G u  E)"
        "head G e  u  in_arcs G u  insert e E = in_arcs G u  E"
        "in_arcs G u  {} = {}" (* XXX: should be unnecessary *)
  using assms by auto

lemma in_arcs_int_arcs[simp]: "in_arcs G u  arcs G = in_arcs G u" and
      out_arcs_int_arcs[simp]: "out_arcs G u  arcs G = out_arcs G u"
  by auto


lemma in_arcs_in_arcs: "x  in_arcs G u  x  arcs G"
  and out_arcs_in_arcs: "x  out_arcs G u  x  arcs G"
  by (auto simp: in_arcs_def out_arcs_def)



subsection ‹Graph operations›

context pre_digraph begin

definition add_arc :: "'b   ('a,'b) pre_digraph" where
  "add_arc a =  verts = verts G  {tail G a, head G a}, arcs = insert a (arcs G), tail = tail G, head = head G "

definition  del_arc :: "'b  ('a,'b) pre_digraph" where
  "del_arc a =  verts = verts G, arcs = arcs G - {a}, tail = tail G, head = head G "

definition add_vert :: "'a   ('a,'b) pre_digraph" where
  "add_vert v =  verts = insert v (verts G), arcs = arcs G, tail = tail G, head = head G "

definition del_vert :: "'a   ('a,'b) pre_digraph" where
  "del_vert v =  verts = verts G - {v}, arcs = {a  arcs G. tail G a  v  head G a  v}, tail = tail G, head = head G "

lemma
  verts_add_arc: " tail G a  verts G; head G a  verts G   verts (add_arc a) = verts G"  and
  verts_add_arc_conv: "verts (add_arc a) = verts G  {tail G a, head G a}" and
  arcs_add_arc: "arcs (add_arc a) = insert a (arcs G)" and
  tail_add_arc: "tail (add_arc a) = tail G" and
  head_add_arc: "head (add_arc a) = head G"
  by (auto simp: add_arc_def)

lemmas add_arc_simps[simp] = verts_add_arc arcs_add_arc tail_add_arc head_add_arc

lemma
  verts_del_arc: "verts (del_arc a) = verts G"  and
  arcs_del_arc: "arcs (del_arc a) = arcs G - {a}" and
  tail_del_arc: "tail (del_arc a) = tail G" and
  head_del_arc: "head (del_arc a) = head G"
  by (auto simp: del_arc_def)

lemmas del_arc_simps[simp] = verts_del_arc arcs_del_arc tail_del_arc head_del_arc

lemma
    verts_add_vert: "verts (pre_digraph.add_vert G u) = insert u (verts G)" and
    arcs_add_vert: "arcs (pre_digraph.add_vert G u) = arcs G" and
    tail_add_vert: "tail (pre_digraph.add_vert G u) = tail G" and
    head_add_vert: "head (pre_digraph.add_vert G u) = head G"
  by (auto simp: pre_digraph.add_vert_def)

lemmas add_vert_simps = verts_add_vert arcs_add_vert tail_add_vert head_add_vert

lemma
    verts_del_vert: "verts (pre_digraph.del_vert G u) = verts G - {u}" and
    arcs_del_vert: "arcs (pre_digraph.del_vert G u) = {a  arcs G. tail G a  u  head G a  u}" and
    tail_del_vert: "tail (pre_digraph.del_vert G u) = tail G" and
    head_del_vert: "head (pre_digraph.del_vert G u) = head G" and
    ends_del_vert: "arc_to_ends (pre_digraph.del_vert G u) = arc_to_ends G"
  by (auto simp: pre_digraph.del_vert_def arc_to_ends_def)

lemmas del_vert_simps = verts_del_vert arcs_del_vert tail_del_vert head_del_vert

lemma add_add_arc_collapse[simp]: "pre_digraph.add_arc (add_arc a) a = add_arc a"
  by (auto simp: pre_digraph.add_arc_def)

lemma add_del_arc_collapse[simp]: "pre_digraph.add_arc (del_arc a) a = add_arc a"
  by (auto simp: pre_digraph.verts_add_arc_conv pre_digraph.add_arc_simps)

lemma del_add_arc_collapse[simp]:
  " tail G a  verts G; head G a  verts G   pre_digraph.del_arc (add_arc a) a = del_arc a"
  by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

lemma del_del_arc_collapse[simp]: "pre_digraph.del_arc (del_arc a) a = del_arc a"
  by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

lemma add_arc_commute: "pre_digraph.add_arc (add_arc b) a = pre_digraph.add_arc (add_arc a) b"
  by (auto simp: pre_digraph.add_arc_def)

lemma del_arc_commute: "pre_digraph.del_arc (del_arc b) a = pre_digraph.del_arc (del_arc a) b"
  by (auto simp: pre_digraph.del_arc_def)

lemma del_arc_in: "a  arcs G  del_arc a = G"
  by (rule pre_digraph.equality) (auto simp: add_arc_def)

lemma in_arcs_add_arc_iff:
  "in_arcs (add_arc a) u = (if head G a = u then insert a (in_arcs G u) else in_arcs G u)"
  by auto

lemma out_arcs_add_arc_iff:
  "out_arcs (add_arc a) u = (if tail G a = u then insert a (out_arcs G u) else out_arcs G u)"
  by auto

lemma in_arcs_del_arc_iff:
  "in_arcs (del_arc a) u = (if head G a = u then in_arcs G u - {a} else in_arcs G u)"
  by auto

lemma out_arcs_del_arc_iff:
  "out_arcs (del_arc a) u = (if tail G a = u then out_arcs G u - {a} else out_arcs G u)"
  by auto

lemma (in wf_digraph) add_arc_in: "a  arcs G  add_arc a = G"
  by (rule pre_digraph.equality) (auto simp: add_arc_def)

end



context wf_digraph begin

lemma wf_digraph_add_arc[intro]:
  "wf_digraph (add_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

lemma wf_digraph_del_arc[intro]:
  "wf_digraph (del_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

lemma wf_digraph_del_vert: "wf_digraph (del_vert u)"
  by standard (auto simp: del_vert_simps)

lemma wf_digraph_add_vert: "wf_digraph (add_vert u)"
  by standard (auto simp: add_vert_simps)

lemma del_vert_add_vert:
  assumes "u  verts G"
  shows "pre_digraph.del_vert (add_vert u) u = G"
  using assms by (intro pre_digraph.equality) (auto simp: pre_digraph.del_vert_def add_vert_def)

end


context fin_digraph begin

lemma in_degree_add_arc_iff:
  "in_degree (add_arc a) u = (if head G a = u  a  arcs G then in_degree G u + 1 else in_degree G u)"
proof -
  have "a  arcs G  a  in_arcs G u" by (auto simp: in_arcs_def)
  with finite_in_arcs show ?thesis
    unfolding in_degree_def by (auto simp: in_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

lemma out_degree_add_arc_iff:
  "out_degree (add_arc a) u = (if tail G a = u  a  arcs G then out_degree G u + 1 else out_degree G u)"
proof -
  have "a  arcs G  a  out_arcs G u" by (auto simp: out_arcs_def)
  with finite_out_arcs show ?thesis
    unfolding out_degree_def by (auto simp: out_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

lemma in_degree_del_arc_iff:
  "in_degree (del_arc a) u = (if head G a = u  a  arcs G then in_degree G u - 1 else in_degree G u)"
proof -
  have "a  arcs G  a  in_arcs G u" by (auto simp: in_arcs_def)
  with finite_in_arcs show ?thesis
    unfolding in_degree_def by (auto simp: in_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma out_degree_del_arc_iff:
  "out_degree (del_arc a) u = (if tail G a = u  a  arcs G then out_degree G u - 1 else out_degree G u)"
proof -
  have "a  arcs G  a  out_arcs G u" by (auto simp: out_arcs_def)
  with finite_out_arcs show ?thesis
    unfolding out_degree_def by (auto simp: out_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma fin_digraph_del_vert: "fin_digraph (del_vert u)"
  by standard (auto simp: del_vert_simps)

lemma fin_digraph_del_arc: "fin_digraph (del_arc a)"
  by standard (auto simp: del_vert_simps)

end

end

Theory Bidirected_Digraph

theory Bidirected_Digraph
imports
  Digraph
  "HOL-Combinatorics.Permutations"
begin

section ‹Bidirected Graphs›

locale bidirected_digraph = wf_digraph G for G +
  fixes arev :: "'b  'b"
  assumes arev_dom: "a. a  arcs G  arev a  a"
  assumes arev_arev_raw: "a. a  arcs G  arev (arev a) = a"
  assumes tail_arev[simp]: "a. a  arcs G  tail G (arev a) = head G a"

lemma (in wf_digraph) bidirected_digraphI:
  assumes arev_eq: "a. a  arcs G  arev a = a"
  assumes arev_neq: "a. a  arcs G  arev a  a"
  assumes arev_arev_raw: "a. a  arcs G  arev (arev a) = a"
  assumes tail_arev: "a. a  arcs G  tail G (arev a) = head G a"
  shows "bidirected_digraph G arev"
  using assms by unfold_locales (auto simp: permutes_def)

context bidirected_digraph begin

  lemma bidirected_digraph[intro!]: "bidirected_digraph G arev"
    by unfold_locales

  lemma arev_arev[simp]: "arev (arev a) = a"
    using arev_dom by (cases "a  arcs G") (auto simp: arev_arev_raw)

  lemma arev_o_arev[simp]: "arev o arev = id"
    by (simp add: fun_eq_iff)

  lemma arev_eq: "a  arcs G  arev a = a"
    by (simp add: arev_dom)

  lemma arev_neq: "a  arcs G  arev a  a"
    by (simp add: arev_dom)

  lemma arev_in_arcs[simp]: "a  arcs G  arev a  arcs G"
    by (metis arev_arev arev_dom)

  lemma head_arev[simp]:
    assumes "a  arcs G" shows "head G (arev a) = tail G a"
  proof -
    from assms have "head G (arev a) = tail G (arev (arev a)) "
      by (simp only: tail_arev arev_in_arcs)
    then show ?thesis by simp
  qed

  lemma ate_arev[simp]:
    assumes "a  arcs G" shows "arc_to_ends G (arev a) = prod.swap (arc_to_ends G a)"
    using assms by (auto simp: arc_to_ends_def)

  lemma bij_arev: "bij arev"
    using arev_arev by (metis bij_betw_imageI inj_on_inverseI surjI)

  lemma arev_permutes_arcs: "arev permutes arcs G"
    using arev_dom bij_arev by (auto simp: permutes_def bij_iff)

  lemma arev_eq_iff: "x y. arev x = arev y  x = y"
    by (metis arev_arev)

  lemma in_arcs_eq: "in_arcs G w = arev ` out_arcs G w"
    by auto (metis arev_arev arev_in_arcs image_eqI in_out_arcs_conv tail_arev)

  lemma inj_on_arev[intro!]: "inj_on arev S"
    by (metis arev_arev inj_on_inverseI)

  lemma even_card_loops:
    "even (card (in_arcs G w  out_arcs G w))" (is "even (card ?S)")
  proof -
    { assume "¬finite ?S"
      then have ?thesis by simp
    }
    moreover
    { assume A:"finite ?S"
      have "card ?S = card ({{a,arev a} | a. a  ?S})" (is "_ = card ( ?T)")
        by (rule arg_cong[where f=card]) (auto intro!: exI[where x="{x, arev x}" for x])
      also have "= sum card ?T"
      proof (rule card_Union_disjoint)
        show "A. A{{a, arev a} |a. a  ?S}  finite A" by auto
        show "pairwise disjnt {{a, arev a} |a. a  in_arcs G w  out_arcs G w}"
          unfolding pairwise_def disjnt_def
           by safe (simp_all add: arev_eq_iff)
      qed
      also have " = sum (λa. 2) ?T"
        by (intro sum.cong) (auto simp: card_insert_if dest: arev_neq)
      also have " = 2 * card ?T" by simp
      finally have ?thesis by simp
    }
    ultimately
    show ?thesis by blast
  qed

end

(*XXX*)
sublocale bidirected_digraph  sym_digraph
proof (unfold_locales, unfold symmetric_def, intro symI)
  fix u v assume "u G v"
  then obtain a where "a  arcs G" "arc_to_ends G a = (u,v)" by (auto simp: arcs_ends_def)
  then have "arev a  arcs G" "arc_to_ends G (arev a) = (v,u)"
    by (auto simp: arc_to_ends_def)
  then show "v G u" by (auto simp: arcs_ends_def intro: rev_image_eqI)
qed



end

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

Theory Pair_Digraph

(* Title:  Pair_Digraph.thy
   Author: Lars Noschinski, TU München
*)

theory Pair_Digraph
imports
  Digraph
  Bidirected_Digraph
  Arc_Walk
begin

section ‹Digraphs without Parallel Arcs›

text ‹
  If no parallel arcs are desired, arcs can be accurately described as pairs of
  This is the natural representation for Digraphs without multi-arcs.
  and @{term "head G"}, making it easier to deal with multiple related graphs
  and to modify a graph by adding edges.

  This theory introduces such a specialisation of digraphs.
›

record 'a pair_pre_digraph = pverts :: "'a set" parcs :: "'a rel"

definition with_proj :: "'a pair_pre_digraph  ('a, 'a × 'a) pre_digraph" where
  "with_proj G =  verts = pverts G, arcs = parcs G, tail = fst, head = snd "

declare [[coercion with_proj]]

primrec pawalk_verts :: "'a  ('a × 'a) awalk  'a list" where
  "pawalk_verts u [] = [u]" |
  "pawalk_verts u (e # es) = fst e # pawalk_verts (snd e) es"

fun pcas :: "'a  ('a × 'a) awalk  'a  bool" where
  "pcas u [] v = (u = v)" |
  "pcas u (e # es) v = (fst e = u  pcas (snd e) es v)"

lemma with_proj_simps[simp]:
  "verts (with_proj G) = pverts G"
  "arcs (with_proj G) = parcs G"
  "arcs_ends (with_proj G) = parcs G"
  "tail (with_proj G) = fst"
  "head (with_proj G) = snd"
  by (auto simp: with_proj_def arcs_ends_conv)

lemma cas_with_proj_eq: "pre_digraph.cas (with_proj G) = pcas"
proof (unfold fun_eq_iff, intro allI)
  fix u es v show "pre_digraph.cas (with_proj G) u es v = pcas u es v"
    by (induct es arbitrary: u) (auto simp:  pre_digraph.cas.simps)
qed

lemma awalk_verts_with_proj_eq: "pre_digraph.awalk_verts (with_proj G) = pawalk_verts"
proof (unfold fun_eq_iff, intro allI)
  fix u es show "pre_digraph.awalk_verts (with_proj G) u es = pawalk_verts u es"
    by (induct es arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps)
qed



locale pair_pre_digraph = fixes G :: "'a pair_pre_digraph"
begin

lemmas [simp] = cas_with_proj_eq awalk_verts_with_proj_eq

end



locale pair_wf_digraph = pair_pre_digraph +
  assumes arc_fst_in_verts: "e. e  parcs G  fst e  pverts G"
  assumes arc_snd_in_verts: "e. e  parcs G  snd e  pverts G"
begin

lemma in_arcsD1: "(u,v)  parcs G  u  pverts G"
  and in_arcsD2: "(u,v)  parcs G  v  pverts G"
  by (auto dest: arc_fst_in_verts arc_snd_in_verts)

lemmas wellformed' = in_arcsD1 in_arcsD2

end

locale pair_fin_digraph = pair_wf_digraph +
  assumes pair_finite_verts: "finite (pverts G)"
    and pair_finite_arcs: "finite (parcs G)"

locale pair_sym_digraph = pair_wf_digraph +
  assumes pair_sym_arcs: "symmetric G"

locale pair_loopfree_digraph = pair_wf_digraph  +
  assumes pair_no_loops: "e  parcs G  fst e  snd e"

locale pair_bidirected_digraph = pair_sym_digraph + pair_loopfree_digraph

locale pair_pseudo_graph = pair_fin_digraph + pair_sym_digraph

locale pair_digraph = pair_fin_digraph  + pair_loopfree_digraph

locale pair_graph = pair_digraph + pair_pseudo_graph

sublocale pair_pre_digraph  pre_digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  by unfold_locales auto

sublocale pair_wf_digraph  wf_digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  by unfold_locales (auto simp: arc_fst_in_verts arc_snd_in_verts)

sublocale pair_fin_digraph  fin_digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  using pair_finite_verts pair_finite_arcs by unfold_locales auto

sublocale pair_sym_digraph  sym_digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  using pair_sym_arcs by unfold_locales auto

sublocale pair_pseudo_graph  pseudo_graph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  by unfold_locales auto

sublocale pair_loopfree_digraph  loopfree_digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  using pair_no_loops by unfold_locales auto

sublocale pair_digraph  digraph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  by unfold_locales (auto simp: arc_to_ends_def)

sublocale pair_graph  graph "with_proj G"
  rewrites "verts G = pverts G" and "arcs G = parcs G" and "tail G = fst" and "head G = snd"
    and "arcs_ends G = parcs G"
    and "pre_digraph.awalk_verts G = pawalk_verts"
    and "pre_digraph.cas G = pcas"
  by unfold_locales auto

sublocale pair_graph  pair_bidirected_digraph by unfold_locales

lemma wf_digraph_wp_iff: "wf_digraph (with_proj G) = pair_wf_digraph G" (is "?L  ?R")
proof
  assume ?L then interpret wf_digraph "with_proj G" .
  show ?R using wellformed by unfold_locales auto
next
  assume ?R then interpret pair_wf_digraph G .
  show ?L by unfold_locales
qed

lemma (in pair_fin_digraph) pair_fin_digraph[intro!]: "pair_fin_digraph G" ..

context pair_digraph begin

lemma pair_wf_digraph[intro!]: "pair_wf_digraph G" by intro_locales

lemma pair_digraph[intro!]: "pair_digraph G" ..

lemma (in pair_loopfree_digraph) no_loops':
  "(u,v)  parcs G  u  v"
  by (auto dest: no_loops)

end

lemma (in pair_wf_digraph) apath_succ_decomp:
  assumes "apath u p v"
  assumes "(x,y)  set p"
  assumes "y  v"
  shows "p1 z p2. p = p1 @ (x,y) # (y,z) # p2  x  z  y  z"
proof -
  from (x,y)  set p obtain p1 p2 where p_decomp: "p = p1 @ (x,y) # p2"
    by (metis (no_types) in_set_conv_decomp_first)
  from p_decomp ‹apath u p v y  v have "p2  []" "awalk y p2 v"
    by (auto simp: apath_def awalk_Cons_iff)
  then obtain z p2' where p2_decomp: "p2 = (y,z) # p2'"
    by atomize_elim (cases p2, auto simp: awalk_Cons_iff)
  then have "x  z  y  z" using p_decomp p2_decomp ‹apath u p v
    by (auto simp: apath_append_iff apath_simps hd_in_awalk_verts)
  with p_decomp p2_decomp have "p = p1 @ (x,y) # (y,z) # p2'  x  z  y  z"
    by auto
  then show ?thesis by blast
qed


lemma (in pair_sym_digraph) arcs_symmetric:
  "(a,b)  parcs G  (b,a)  parcs G"
  using sym_arcs by (auto simp: symmetric_def elim: symE)

lemma (in pair_pseudo_graph) pair_pseudo_graph[intro]: "pair_pseudo_graph G" ..

lemma (in pair_graph) pair_graph[intro]: "pair_graph G" by unfold_locales
lemma (in pair_graph) pair_graphD_graph: "graph G" by unfold_locales

lemma pair_graphI_graph:
  assumes "graph (with_proj G)" shows "pair_graph G"
proof -
  interpret G: graph "with_proj G" by fact
  show ?thesis
    using G.wellformed G.finite_arcs G.finite_verts G.no_loops
    by unfold_locales auto
qed

lemma pair_loopfreeI_loopfree:
  assumes "loopfree_digraph (with_proj G)" shows "pair_loopfree_digraph G"
proof -
  interpret loopfree_digraph "with_proj G" by fact
  show ?thesis using wellformed no_loops by unfold_locales auto
qed



subsection ‹Path reversal for Pair Digraphs›

text ‹This definition is only meaningful in @{term Pair_Digraph}

primrec rev_path :: "('a × 'a) awalk  ('a × 'a) awalk" where
  "rev_path [] = []" |
  "rev_path (e # es) = rev_path es @ [(snd e, fst e)]"

lemma rev_path_append[simp]: "rev_path (p @ q) = rev_path q @ rev_path p"
  by (induct p) auto

lemma rev_path_rev_path[simp]:
  "rev_path (rev_path p) = p"
  by (induct p) auto

lemma rev_path_empty[simp]:
  "rev_path p = []  p = []"
  by (induct p) auto 

lemma rev_path_eq: "rev_path p = rev_path q  p = q"
  by (metis rev_path_rev_path)

lemma (in pair_sym_digraph)
  assumes "awalk u p v"
  shows awalk_verts_rev_path: "awalk_verts v (rev_path p) = rev (awalk_verts u p)"
    and awalk_rev_path': "awalk v (rev_path p) u"
using assms
proof (induct p arbitrary: u)
  case Nil case 1 then show ?case by auto
next
  case Nil case 2 then show ?case by (auto simp: awalk_Nil_iff)
next
  case (Cons e es) case 1
  with Cons have walks: "awalk v (rev_path es) (snd e)"
        "awalk (snd e) [(snd e, fst e)] u"
      and verts: "awalk_verts v (rev_path es) = rev (awalk_verts (snd e) es)"
    by (auto simp: awalk_simps intro: arcs_symmetric)

  from walks have "awalk v (rev_path es @ [(snd e, fst e)]) u"
    by simp
  moreover
  have "tl (awalk_verts (awlast v (rev_path es)) [(snd e, fst e)]) = [fst e]"
    by auto
  ultimately
  show ?case using 1 verts by (auto simp: awalk_verts_append)
next
  case (Cons e es) case 2
  with Cons have "awalk v (rev_path es) (snd e)"
    by (auto simp: awalk_Cons_iff)
  moreover
  have "rev_path (e # es) = rev_path es @ [(snd e, fst e)]"
    by auto
  moreover
  from Cons 2 have "awalk (snd e) [(snd e, fst e)] u"
    by (auto simp: awalk_simps intro: arcs_symmetric)
  ultimately show "awalk v (rev_path (e # es)) u"
    by simp
qed

lemma (in pair_sym_digraph) awalk_rev_path[simp]:
  "awalk v (rev_path p) u = awalk u p v" (is "?L = ?R")
by (metis awalk_rev_path' rev_path_rev_path)

lemma (in pair_sym_digraph) apath_rev_path[simp]:
  "apath v (rev_path p) u = apath u p v"
by (auto simp: awalk_verts_rev_path apath_def)


subsection ‹Subdividing Edges›

text ‹subdivide an edge (=two associated arcs) in graph›
fun subdivide :: "'a pair_pre_digraph  'a × 'a  'a  'a pair_pre_digraph" where
  "subdivide G (u,v) w = 
    pverts = pverts G  {w},
    parcs = (parcs G - {(u,v),(v,u)})  {(u,w), (w,u), (w, v), (v, w)}"

declare subdivide.simps[simp del]

text ‹subdivide an arc in a path›
fun sd_path :: "'a × 'a  'a  ('a × 'a) awalk  ('a × 'a) awalk" where
    "sd_path _ _ [] = []"
  | "sd_path (u,v) w (e # es) = (if e = (u,v)
                                 then [(u,w),(w,v)]
                                 else if e = (v,u)
                                 then [(v,w),(w,u)]
                                 else [e]) @ sd_path (u,v) w es"

text ‹contract an arc in a path›
fun co_path :: "'a × 'a  'a  ('a × 'a) awalk  ('a × 'a) awalk" where
    "co_path _ _ [] = []"
  | "co_path _ _ [e] = [e]"
  | "co_path (u,v) w (e1 # e2 # es) = (if e1 = (u,w)  e2 = (w,v)
      then (u,v) # co_path (u,v) w es
      else if e1 = (v,w)  e2 = (w,u)
      then (v,u) # co_path (u,v) w es
      else e1 # co_path (u,v) w (e2 # es))"

lemma co_path_simps[simp]:
  "e1  (fst e, w); e1  (snd e,w)  co_path e w (e1 # es) = e1 # co_path e w es" 
  "e1 = (fst e, w); e2 = (w, snd e)  co_path e w (e1 # e2 # es) = e # co_path e w es"
  "e1 = (snd e, w); e2 = (w, fst e)
     co_path e w (e1 # e2 # es) = (snd e, fst e) # co_path e w es"
  "e1  (fst e, w)  e2  (w, snd e); e1  (snd e, w)  e2  (w, fst e)
     co_path e w (e1 # e2 # es) = e1 # co_path e w (e2 # es)"
  apply (cases es; auto)
  apply (cases e; auto)
  apply (cases e; auto)
  apply (cases e; cases "fst e = snd e"; auto)
  apply (cases e; cases "fst e = snd e"; auto)
  done

lemma co_path_nonempty[simp]: "co_path e w p = []  p = []"
  by (cases e) (cases p rule: list_exhaust_NSC, auto)

declare co_path.simps(3)[simp del]

lemma verts_subdivide[simp]: "pverts (subdivide G e w) = pverts G  {w}"
  by (cases e) (auto simp: subdivide.simps)

lemma arcs_subdivide[simp]:
  shows "parcs (subdivide G (u,v) w) = (parcs G - {(u,v),(v,u)})  {(u,w), (w,u), (w, v), (v, w)}"
  by (auto simp: subdivide.simps)

lemmas subdivide_simps = verts_subdivide arcs_subdivide

lemma sd_path_induct[case_names empty pass sd sdrev]:
  assumes A: "P e []"
    and B: "e' es. e'  e  e'  (snd e , fst e)  P e es  P e (e' # es)"
      "es. P e es  P e (e # es)"
      "es. fst e  snd e  P e es  P e ((snd e, fst e) # es)"
  shows "P e es"
  by (induct es) (rule A, metis B prod.collapse)

lemma co_path_induct[case_names empty single co corev pass]:
  fixes e :: "'a × 'a"
    and w :: "'a"
    and p :: "('a × 'a) awalk"
  assumes Nil: "P e w []"
    and ConsNil:"e'. P e w [e']"
    and ConsCons1: "e1 e2 es. e1 = (fst e, w)  e2 = (w, snd e)  P e w es 
            P e w (e1 # e2 # es)"
    and ConsCons2: "e1 e2 es. ¬(e1 = (fst e, w)  e2 = (w, snd e)) 
            e1 = (snd e, w)  e2 = (w, fst e)  P e w es 
            P e w (e1 # e2 # es)"
    and ConsCons3: "e1 e2 es.
            ¬ (e1 = (fst e, w)  e2 = (w, snd e)) 
             ¬ (e1 = (snd e, w)  e2 = (w, fst e))  P e w (e2 # es) 
            P e w (e1 # e2 # es)"
  shows "P e w p"
proof (induct p rule: length_induct)
  case (1 p) then show ?case
  proof (cases p rule: list_exhaust_NSC)
    case (Cons_Cons e1 e2 es)
    then have "P e w es" "P e w (e2 # es)"using 1 by auto
    then show ?thesis unfolding Cons_Cons by (blast intro: ConsCons1 ConsCons2 ConsCons3)
  qed (auto intro: Nil ConsNil)
qed

lemma co_sd_id:
  assumes "(u,w)  set p" "(v,w)  set p"
  shows "co_path (u,v) w (sd_path (u,v) w p) = p"
using assms by (induct p) auto

lemma sd_path_id:
  assumes "(x,y)  set p" "(y,x)  set p"
  shows "sd_path (x,y) w p = p"
using assms by (induct p) auto

lemma (in pair_wf_digraph) pair_wf_digraph_subdivide:
  assumes props: "e  parcs G" "w  pverts G"
  shows "pair_wf_digraph (subdivide G e w)" (is "pair_wf_digraph ?sG")
proof
  obtain u v where [simp]: "e = (u,v)" by (cases e) auto
  fix e' assume "e'  parcs ?sG"
  then show "fst e'  pverts ?sG" "snd e'  pverts ?sG"
    using props by (auto dest: wellformed)
qed

lemma (in pair_sym_digraph) pair_sym_digraph_subdivide:
  assumes props: "e  parcs G" "w  pverts G"
  shows "pair_sym_digraph (subdivide G e w)" (is "pair_sym_digraph ?sG")
proof -
  interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide)
  obtain u v where [simp]: "e = (u,v)" by (cases e) auto
  show ?thesis
  proof
    have "a b. (a, b)  parcs (subdivide G e w)  (b, a)  parcs (subdivide G e w)"
      unfolding e = _ arcs_subdivide
      by (elim UnE, rule UnI1, rule_tac [2] UnI2) (blast intro: arcs_symmetric)+
    then show "symmetric ?sG"
      unfolding symmetric_def with_proj_simps by (rule symI)
  qed
qed

lemma (in pair_loopfree_digraph) pair_loopfree_digraph_subdivide:
  assumes props: "e  parcs G" "w  pverts G"
  shows "pair_loopfree_digraph (subdivide G e w)" (is "pair_loopfree_digraph ?sG")
proof -
  interpret sdG: pair_wf_digraph "subdivide G e w" using assms by (rule pair_wf_digraph_subdivide)
  from assms show ?thesis
    by unfold_locales (cases e, auto dest: wellformed no_loops)
qed

lemma (in pair_bidirected_digraph) pair_bidirected_digraph_subdivide:
  assumes props: "e  parcs G" "w  pverts G"
  shows "pair_bidirected_digraph (subdivide G e w)" (is "pair_bidirected_digraph ?sG")
proof -
  interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide)
  interpret sdG: pair_loopfree_digraph "subdivide G e w" using assms by (rule pair_loopfree_digraph_subdivide)
  show ?thesis by unfold_locales
qed

lemma (in pair_pseudo_graph) pair_pseudo_graph_subdivide:
  assumes props: "e  parcs G" "w  pverts G"
  shows "pair_pseudo_graph (subdivide G e w)" (is "pair_pseudo_graph ?sG")
proof -
  interpret sdG: pair_sym_digraph "subdivide G e w" using assms by (rule pair_sym_digraph_subdivide)
  obtain u v where [simp]: "e = (u,v)" by (cases e) auto
  show ?thesis by unfold_locales (cases e, auto)
qed

lemma (in pair_graph) pair_graph_subdivide:
  assumes "e  parcs G" "w  pverts G"
  shows "pair_graph (subdivide G e w)" (is "pair_graph ?sG")
proof -
  interpret PPG: pair_pseudo_graph "subdivide G e w"
    using assms by (rule pair_pseudo_graph_subdivide)
  interpret PPG: pair_loopfree_digraph "subdivide G e w"
    using assms by (rule pair_loopfree_digraph_subdivide)
  from assms show ?thesis by unfold_locales
qed

lemma arcs_subdivideD:
  assumes "x  parcs (subdivide G e w)" "fst x  w" "snd x  w"
  shows "x  parcs G"
using assms by (cases e) auto

context pair_sym_digraph begin

lemma
  assumes path: "apath u p v"
  assumes elems: "e  parcs G" "w  pverts G"
  shows apath_sd_path: "pre_digraph.apath (subdivide G e w) u (sd_path e w p) v" (is ?A)
    and set_awalk_verts_sd_path: "set (awalk_verts u (sd_path e w p))
       set (awalk_verts u p)  {w}" (is ?B)
proof -
  obtain x y where e_conv: "e = (x,y)" by (cases e) auto
  define sG where "sG = subdivide G e w"
  interpret S: pair_sym_digraph sG
    unfolding sG_def using elems by (rule pair_sym_digraph_subdivide)

  have ev_sG: "S.awalk_verts = awalk_verts"
    by (auto simp: fun_eq_iff pre_digraph.awalk_verts_conv)
  have w_sG: "{(x,w), (y,w), (w,x), (w,y)}  parcs sG"
    by (auto simp: sG_def e_conv)

  from path have "S.apath u (sd_path (x,y) w p) v"
    and "set (S.awalk_verts u (sd_path (x,y) w p))  set (awalk_verts u p)  {w}"
  proof (induct p arbitrary: u rule: sd_path_induct)
    case empty case 1
    moreover have "pverts sG = pverts G  {w}" by (simp add: sG_def)
    ultimately show ?case by (auto simp: apath_Nil_iff S.apath_Nil_iff)
  next
    case empty case 2 then show ?case by simp
  next
    case (pass e' es)
    { case 1
      then have "S.apath (snd e') (sd_path (x,y) w es) v" "u  w" "fst e' = u"
          "u  set (S.awalk_verts (snd e') (sd_path (x,y) w es))"
        using pass elems by (fastforce simp: apath_Cons_iff)+
      moreover then have "e'  parcs sG"
        using 1 pass by (auto simp: e_conv sG_def S.apath_Cons_iff apath_Cons_iff)
      ultimately show ?case using pass by (auto simp: S.apath_Cons_iff) }
    note case1 = this
    { case 2 with pass 2 show ?case by (simp add: apath_Cons_iff) blast }
  next
    { fix u es a b
      assume A: "apath u ((a,b) # es) v"
        and ab: "(a,b) = (x,y)  (a,b) = (y,x)"
        and hyps: "u. apath u es v  S.apath u (sd_path (x, y) w es) v"
          "u. apath u es v  set (awalk_verts u (sd_path (x, y) w es))  set (awalk_verts u es)  {w}"

      from ab A have "(x,y)  set es" "(y,x)  set es"
        by (auto simp: apath_Cons_iff dest!: awalkI_apath dest: awalk_verts_arc1 awalk_verts_arc2)
      then have ev_sd: "set (S.awalk_verts b (sd_path (x,y) w es)) = set (awalk_verts b es)"
        by (simp add: sd_path_id)

      from A ab have [simp]: "x  y"
        by (simp add: apath_Cons_iff) (metis awalkI_apath awalk_verts_non_Nil awhd_of_awalk hd_in_set)
 
      from A have "S.apath b (sd_path (x,y) w es) v" "u = a" "u  w"
        using ab hyps elems by (auto simp: apath_Cons_iff wellformed')
      moreover
      then have "S.awalk u (sd_path (x, y) w ((a, b) # es)) v "
        using ab w_sG by (auto simp: S.apath_def S.awalk_simps S.wellformed')
      then have "u  set (S.awalk_verts w ((w,b) # sd_path (x,y) w es))"
        using ab u  w ev_sd A by (auto simp: apath_Cons_iff S.awalk_def)
      moreover
      have "w  set (awalk_verts b (sd_path (x, y) w es))"
        using ab ev_sd A elems by (auto simp: awalk_Cons_iff apath_def)
      ultimately
      have path: "S.apath u (sd_path (x, y) w ((a, b) # es)) v "
        using ab hyps w_sG u = a by (auto simp: S.apath_Cons_iff ) }
    note path = this
    { case (sd es)
      { case 1 with sd show ?case by (intro path) auto }
      { case 2 show ?case using 2 sd
          by (auto simp: apath_Cons_iff) } }
    { case (sdrev es)
      { case 1 with sdrev show ?case by (intro path) auto }
      { case 2 show ?case using 2 sdrev
          by (auto simp: apath_Cons_iff) } }
  qed
  then show ?A ?B unfolding sG_def e_conv .
qed

lemma
  assumes elems: "e  parcs G" "w  pverts G" "u  pverts G" "v  pverts G"
  assumes path: "pre_digraph.apath (subdivide G e w) u p v"
  shows apath_co_path: "apath u (co_path e w p) v" (is ?thesis_path)
    and set_awalk_verts_co_path: "set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}" (is ?thesis_set)
proof -
  obtain x y where e_conv: "e = (x,y)" by (cases e) auto
  interpret S: pair_sym_digraph "subdivide G e w"
    using elems(1,2) by (rule pair_sym_digraph_subdivide)

  have e_w: "fst e  w" "snd e  w" using elems by auto

  have "S.apath u p v" "u  w" using elems path by auto
  then have co_path: "apath u (co_path e w p) v
     set (awalk_verts u (co_path e w p)) = set (awalk_verts u p) - {w}"
  proof (induction p arbitrary: u rule: co_path_induct)
    case empty with elems show ?case
      by (simp add: apath_Nil_iff S.apath_Nil_iff)
  next
    case (single e') with elems show ?case
     by (auto simp: apath_Cons_iff S.apath_Cons_iff apath_Nil_iff S.apath_Nil_iff
        dest: arcs_subdivideD)
  next
    case (co e1 e2 es)
    then have "apath u (co_path e w (e1 # e2 # es)) v" using co e_w elems
      by (auto simp: apath_Cons_iff S.apath_Cons_iff)
    moreover
    have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
      using co e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff)
    ultimately
    show ?case by fast
  next
    case (corev e1 e2 es)
    have "apath u (co_path e w (e1 # e2 # es)) v" using corev(1-3) e_w(1) elems(1)
      by (auto simp: apath_Cons_iff S.apath_Cons_iff  intro: arcs_symmetric)
    moreover
    have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
      using corev e_w by (auto simp: apath_Cons_iff S.apath_Cons_iff)
    ultimately
    show ?case by fast
  next
    case (pass e1 e2 es)
    have "fst e1  w" using elems pass.prems by (auto simp: S.apath_Cons_iff)
    have "snd e1  w"
    proof
      assume "snd e1 = w"
      then have "e1  parcs G" using elems by auto
      then have "e1  parcs (subdivide G e w) - parcs G"
        using pass by (auto simp: S.apath_Cons_iff)
      then have "e1 = (x,w)  e1 = (y,w)"
        using ‹fst e1  w e_w by (auto simp add: e_conv)
      moreover
      have "fst e2 = w" using ‹snd e1 = w pass.prems by (auto simp: S.apath_Cons_iff)
      then have "e2  parcs G" using elems by auto
      then have "e2  parcs (subdivide G e w) - parcs G"
        using pass by (auto simp: S.apath_Cons_iff)
      then have "e2 = (w,x)  e2 = (w,y)"
        using ‹fst e2 = w e_w by (cases e2) (auto simp add: e_conv)
      ultimately
      have "e1 = (x,w)  e2 = (w,x)  e1 = (y,w)  e2 = (w,y)"
        using pass.hyps[simplified e_conv] by auto
      then show False
        using pass.prems by (cases es) (auto simp: S.apath_Cons_iff)
    qed
    then have "e1  parcs G"
      using ‹fst e1  w pass.prems by (auto simp: S.apath_Cons_iff dest: arcs_subdivideD)

    have ih: "apath (snd e1) (co_path e w (e2 # es)) v  set (awalk_verts (snd e1) (co_path e w (e2 # es))) = set (awalk_verts (snd e1) (e2 # es)) - {w}"
      using pass.prems ‹snd e1  w by (intro pass.IH) (auto simp: apath_Cons_iff S.apath_Cons_iff)
    then have "fst e1  set (awalk_verts (snd e1) (co_path e w (e2 # es)))" "fst e1 = u"
      using pass.prems by (clarsimp simp: S.apath_Cons_iff)+
    then have "apath u (co_path e w (e1 # e2 # es)) v"
      using ih pass e1  parcs G by (auto simp: apath_Cons_iff S.apath_Cons_iff)[]
    moreover
    have "set (awalk_verts u (co_path e w (e1 # e2 # es))) = set (awalk_verts u (e1 # e2 # es)) - {w}"
      using pass.hyps ih ‹fst e1  w by auto
    ultimately show ?case by fast
  qed
  then show ?thesis_set ?thesis_path by blast+
qed

end



subsection ‹Bidirected Graphs›

definition (in -) swap_in :: "('a × 'a) set  'a × 'a  'a × 'a" where
  "swap_in S x = (if x  S then prod.swap x else x)"

lemma bidirected_digraph_rev_conv_pair:
  assumes "bidirected_digraph (with_proj G) rev_G"
  shows "rev_G = swap_in (parcs G)"
proof -
  interpret bidirected_digraph G rev_G by fact
  have "a b. (a, b)  parcs G  rev_G (a, b) = (b, a)"
    using tail_arev[simplified with_proj_simps] head_arev[simplified with_proj_simps]
    by (metis fst_conv prod.collapse snd_conv)
  then show ?thesis by (auto simp: swap_in_def fun_eq_iff arev_eq)
qed

lemma (in pair_bidirected_digraph) bidirected_digraph:
  "bidirected_digraph (with_proj G) (swap_in (parcs G))"
  using no_loops' arcs_symmetric
  by unfold_locales (auto simp: swap_in_def)

lemma pair_bidirected_digraphI_bidirected_digraph:
  assumes "bidirected_digraph (with_proj G) (swap_in (parcs G))"
  shows "pair_bidirected_digraph G"
proof -
  interpret bidirected_digraph "with_proj G" "swap_in (parcs G)" by fact
  {
    fix a assume "a  parcs G" then have "fst a  snd a"
      using arev_neq[of a] bidirected_digraph_rev_conv_pair[OF assms(1)]
      by (cases a) (auto simp: swap_in_def)
  }
  then show ?thesis
    using tail_in_verts head_in_verts by unfold_locales auto
qed

end

Theory Digraph_Component

(* Title:  Digraph_Component.thy
   Author: Lars Noschinski, TU München
*)

theory Digraph_Component
imports
  Digraph
  Arc_Walk
  Pair_Digraph
begin

section ‹Components of (Symmetric) Digraphs›

definition compatible :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  bool" where
  "compatible G H  tail G = tail H  head G = head H"

(* Require @{term "wf_digraph G"}? *)
definition subgraph :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  bool" where
  "subgraph H G  verts H  verts G  arcs H  arcs G  wf_digraph G  wf_digraph H  compatible G H"

definition induced_subgraph :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  bool" where
  "induced_subgraph H G  subgraph H G  arcs H = {e  arcs G. tail G e  verts H  head G e  verts H}"

definition spanning :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  bool" where
  "spanning H G  subgraph H G  verts G = verts H"

definition strongly_connected :: "('a,'b) pre_digraph  bool" where
  "strongly_connected G  verts G  {}  (u  verts G. v  verts G. u *G v)"


text ‹
  The following function computes underlying symmetric graph of a digraph
  and removes parallel arcs.
›

definition mk_symmetric :: "('a,'b) pre_digraph  'a pair_pre_digraph" where
  "mk_symmetric G   pverts = verts G, parcs = earcs G. {(tail G e, head G e), (head G e, tail G e)}"

definition connected :: "('a,'b) pre_digraph  bool" where
  "connected G  strongly_connected (mk_symmetric G)"

definition forest :: "('a,'b) pre_digraph  bool" where
  "forest G  ¬(p. pre_digraph.cycle G p)"

definition tree :: "('a,'b) pre_digraph  bool" where
  "tree G  connected G  forest G"

definition spanning_tree :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  bool" where
  "spanning_tree H G  tree H  spanning H G"

definition (in pre_digraph)
  max_subgraph :: "(('a,'b) pre_digraph  bool)  ('a,'b) pre_digraph   bool"
where
  "max_subgraph P H  subgraph H G  P H  (H'. H'  H  subgraph H H'  ¬(subgraph H' G  P H'))"

definition (in pre_digraph) sccs :: "('a,'b) pre_digraph set" where
  "sccs  {H. induced_subgraph H G  strongly_connected H  ¬(H'. induced_subgraph H' G
       strongly_connected H'  verts H  verts H')}"

definition (in pre_digraph) sccs_verts :: "'a set set" where
  "sccs_verts = {S. S  {}  (u  S. v  S. u *G v)  (u  S. v. v  S  ¬u *G v  ¬v *G u)}"
(*XXX:  "sccs_verts = verts ` sccs" *)

definition (in pre_digraph) scc_of :: "'a  'a set" where
  "scc_of u  {v. u * v  v * u}"

definition union :: "('a,'b) pre_digraph  ('a,'b) pre_digraph  ('a,'b) pre_digraph" where
  "union G H   verts = verts G  verts H, arcs = arcs G  arcs H, tail = tail G, head = head G"

definition (in pre_digraph) Union :: "('a,'b) pre_digraph set  ('a,'b) pre_digraph" where
  "Union gs =  verts = (G  gs. verts G), arcs = (G  gs. arcs G),
    tail = tail G , head = head G  "



subsection ‹Compatible Graphs›

lemma compatible_tail:
  assumes "compatible G H" shows "tail G = tail H"
  using assms by (simp add: fun_eq_iff compatible_def)

lemma compatible_head:
  assumes "compatible G H" shows "head G = head H"
  using assms by (simp add: fun_eq_iff compatible_def)

lemma compatible_cas:
  assumes "compatible G H" shows "pre_digraph.cas G = pre_digraph.cas H"
proof (unfold fun_eq_iff, intro allI)
  fix u es v show "pre_digraph.cas G u es v = pre_digraph.cas H u es v"
    using assms
    by (induct es arbitrary: u)
       (simp_all add: pre_digraph.cas.simps compatible_head compatible_tail)
qed

lemma compatible_awalk_verts:
  assumes "compatible G H" shows "pre_digraph.awalk_verts G = pre_digraph.awalk_verts H"
proof (unfold fun_eq_iff, intro allI)
  fix u es show "pre_digraph.awalk_verts G u es = pre_digraph.awalk_verts H u es"
    using assms
    by (induct es arbitrary: u)
       (simp_all add: pre_digraph.awalk_verts.simps compatible_head compatible_tail)
qed

lemma compatibleI_with_proj[intro]:
  shows "compatible (with_proj G) (with_proj H)"
  by (auto simp: compatible_def)



subsection ‹Basic lemmas›

lemma (in sym_digraph) graph_symmetric:
  shows "(u,v)  arcs_ends G  (v,u)  arcs_ends G"
  using sym_arcs by (auto simp add: symmetric_def sym_def)

lemma strongly_connectedI[intro]:
  assumes "verts G  {}" "u v. u  verts G  v  verts G  u *G v"
  shows "strongly_connected G"
using assms by (simp add: strongly_connected_def)

lemma strongly_connectedE[elim]:
  assumes "strongly_connected G"
  assumes "(u v. u  verts G  v  verts G  u *G v)  P"
  shows "P"
using assms by (auto simp add: strongly_connected_def)

lemma subgraph_imp_subverts:
  assumes "subgraph H G"
  shows "verts H  verts G"
using assms by (simp add: subgraph_def)

lemma induced_imp_subgraph:
  assumes "induced_subgraph H G"
  shows "subgraph H G"
using assms by (simp add: induced_subgraph_def)

lemma (in pre_digraph) in_sccs_imp_induced:
  assumes "c  sccs"
  shows "induced_subgraph c G"
using assms by (auto simp: sccs_def)

lemma spanning_tree_imp_tree[dest]:
  assumes "spanning_tree H G"
  shows "tree H"
using assms by (simp add: spanning_tree_def)

lemma tree_imp_connected[dest]:
  assumes "tree G"
  shows "connected G"
using assms by (simp add: tree_def)

lemma spanning_treeI[intro]:
  assumes "spanning H G"
  assumes "tree H"
  shows "spanning_tree H G"
using assms by (simp add: spanning_tree_def)

lemma spanning_treeE[elim]:
  assumes "spanning_tree H G"
  assumes "tree H  spanning H G  P"
  shows "P"
using assms by (simp add: spanning_tree_def)

lemma spanningE[elim]:
  assumes "spanning H G"
  assumes "subgraph H G  verts G = verts H  P"
  shows "P"
using assms by (simp add: spanning_def)

lemma (in pre_digraph) in_sccsI[intro]:
  assumes "induced_subgraph c G"
  assumes "strongly_connected c"
  assumes "¬(c'. induced_subgraph c' G  strongly_connected c' 
    verts c  verts c')"
  shows "c  sccs"
using assms by (auto simp add: sccs_def)

lemma (in pre_digraph) in_sccsE[elim]:
  assumes "c  sccs"
  assumes "induced_subgraph c G  strongly_connected c  ¬ (d.
    induced_subgraph d G  strongly_connected d  verts c  verts d)  P"
  shows "P"
using assms by (simp add: sccs_def)

lemma subgraphI:
  assumes "verts H  verts G"
  assumes "arcs H  arcs G"
  assumes "compatible G H"
  assumes "wf_digraph H"
  assumes "wf_digraph G"
  shows "subgraph H G"
using assms by (auto simp add: subgraph_def)

lemma subgraphE[elim]:
  assumes "subgraph H G"
  obtains "verts H  verts G" "arcs H  arcs G" "compatible G H" "wf_digraph H" "wf_digraph G"
using assms by (simp add: subgraph_def)

lemma induced_subgraphI[intro]:
  assumes "subgraph H G"
  assumes "arcs H = {e  arcs G. tail G e  verts H  head G e  verts H}"
  shows "induced_subgraph H G"
using assms unfolding induced_subgraph_def by safe

lemma induced_subgraphE[elim]:
  assumes "induced_subgraph H G"
  assumes "subgraph H G; arcs H = {e  arcs G. tail G e  verts H  head G e  verts H}  P"
  shows "P"
using assms by (auto simp add: induced_subgraph_def)

lemma pverts_mk_symmetric[simp]: "pverts (mk_symmetric G) = verts G"
  and parcs_mk_symmetric:
    "parcs (mk_symmetric G) = (earcs G. {(tail G e, head G e), (head G e, tail G e)})"
  by (auto simp: mk_symmetric_def arcs_ends_conv image_UN)

lemma arcs_ends_mono:
  assumes "subgraph H G"
  shows "arcs_ends H  arcs_ends G"
  using assms by (auto simp add: subgraph_def arcs_ends_conv compatible_tail compatible_head)

lemma (in wf_digraph) subgraph_refl: "subgraph G G"
  by (auto simp: subgraph_def compatible_def) unfold_locales

lemma (in wf_digraph) induced_subgraph_refl: "induced_subgraph G G"
  by (rule induced_subgraphI) (auto simp: subgraph_refl)




subsection ‹The underlying symmetric graph of a digraph›

lemma (in wf_digraph) wellformed_mk_symmetric[intro]: "pair_wf_digraph (mk_symmetric G)"
  by unfold_locales (auto simp: parcs_mk_symmetric)

lemma (in fin_digraph) pair_fin_digraph_mk_symmetric[intro]: "pair_fin_digraph (mk_symmetric G)"
proof -
  have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
  also have "?X = {(a, b). (b, a)  arcs_ends G}" by auto
  finally have X: "finite ..." .
  then show ?thesis
    by unfold_locales (auto simp: mk_symmetric_def arcs_ends_conv)
qed

lemma (in digraph) digraph_mk_symmetric[intro]: "pair_digraph (mk_symmetric G)"
proof -
  have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
  also have "?X = {(a, b). (b, a)  arcs_ends G}" by auto
  finally have "finite ..." .
  then show ?thesis
    by unfold_locales (auto simp: mk_symmetric_def arc_to_ends_def dest: no_loops)
qed

lemma (in wf_digraph) reachable_mk_symmetricI:
  assumes "u * v" shows "u *mk_symmetric G v"
proof -
  have "arcs_ends G  parcs (mk_symmetric G)"
       "(u, v)  rtrancl_on (pverts (mk_symmetric G)) (arcs_ends G)"
    using assms unfolding reachable_def by (auto simp: parcs_mk_symmetric)
  then show ?thesis unfolding reachable_def by (auto intro: rtrancl_on_mono)
qed

lemma (in wf_digraph) adj_mk_symmetric_eq:
  "symmetric G  parcs (mk_symmetric G) = arcs_ends G"
  by (auto simp: parcs_mk_symmetric in_arcs_imp_in_arcs_ends arcs_ends_symmetric)

lemma (in wf_digraph) reachable_mk_symmetric_eq:
  assumes "symmetric G" shows "u *mk_symmetric G v  u * v" (is "?L  ?R")
  using adj_mk_symmetric_eq[OF assms] unfolding reachable_def by auto

lemma (in wf_digraph) mk_symmetric_awalk_imp_awalk:
  assumes sym: "symmetric G"
  assumes walk: "pre_digraph.awalk (mk_symmetric G) u p v"
  obtains q where "awalk u q v"
proof -
  interpret S: pair_wf_digraph "mk_symmetric G" ..
  from walk have "u *mk_symmetric G v"
    by (simp only: S.reachable_awalk) rule
  then have "u * v" by (simp only: reachable_mk_symmetric_eq[OF sym])
  then show ?thesis by (auto simp: reachable_awalk intro: that)
qed

lemma symmetric_mk_symmetric:
  "symmetric (mk_symmetric G)"
  by (auto simp: symmetric_def parcs_mk_symmetric intro: symI)



subsection ‹Subgraphs and Induced Subgraphs›

lemma subgraph_trans:
  assumes "subgraph G H" "subgraph H I" shows "subgraph G I"
  using assms by (auto simp: subgraph_def compatible_def)

text ‹
  The @{term digraph} and @{term fin_digraph} properties are preserved under
  the (inverse) subgraph relation
›
lemma (in fin_digraph) fin_digraph_subgraph:
  assumes "subgraph H G" shows "fin_digraph H"
proof (intro_locales)
  from assms show "wf_digraph H" by auto

  have HG: "arcs H  arcs G" "verts H  verts G"
    using assms by auto
  then have "finite (verts H)" "finite (arcs H)"
    using finite_verts finite_arcs by (blast intro: finite_subset)+
  then show "fin_digraph_axioms H"
    by unfold_locales
qed

lemma (in digraph) digraph_subgraph:
  assumes "subgraph H G" shows "digraph H"
proof
  fix e assume e: "e  arcs H"
  with assms show "tail H e  verts H" "head H e  verts H"
    by (auto simp: subgraph_def intro: wf_digraph.wellformed)
  from e and assms have "e  arcs H  arcs G" by auto
  with assms show "tail H e  head H e"
    using no_loops by (auto simp: subgraph_def compatible_def arc_to_ends_def)
next
  have "arcs H  arcs G" "verts H  verts G" using assms by auto
  then show "finite (arcs H)" "finite (verts H)"
    using finite_verts finite_arcs by (blast intro: finite_subset)+
next
  fix e1 e2 assume "e1  arcs H" "e2  arcs H"
    and eq: "arc_to_ends H e1 = arc_to_ends H e2"
  with assms have "e1  arcs H  arcs G" "e2  arcs H  arcs G"
    by auto
  with eq show "e1 = e2"
    using no_multi_arcs assms
    by (auto simp: subgraph_def compatible_def arc_to_ends_def)
qed

lemma (in pre_digraph) adj_mono:
  assumes "u H v" "subgraph H G"
  shows "u  v"
  using assms by (blast dest: arcs_ends_mono)

lemma (in pre_digraph) reachable_mono:
  assumes walk: "u *H v" and sub: "subgraph H G"
  shows "u * v"
proof -
  have "verts H  verts G" using sub by auto
  with assms show ?thesis
    unfolding reachable_def by (metis arcs_ends_mono rtrancl_on_mono)
qed


text ‹
  Arc walks and paths are preserved under the subgraph relation.
›
lemma (in wf_digraph) subgraph_awalk_imp_awalk:
  assumes walk: "pre_digraph.awalk H u p v"
  assumes sub: "subgraph H G"
  shows "awalk u p v"
  using assms by (auto simp: pre_digraph.awalk_def compatible_cas)

lemma (in wf_digraph) subgraph_apath_imp_apath:
  assumes path: "pre_digraph.apath H u p v"
  assumes sub: "subgraph H G"
  shows "apath u p v"
  using assms unfolding pre_digraph.apath_def
  by (auto intro: subgraph_awalk_imp_awalk simp: compatible_awalk_verts)

lemma subgraph_mk_symmetric:
  assumes "subgraph H G"
  shows "subgraph (mk_symmetric H) (mk_symmetric G)"
proof (rule subgraphI)
  let ?wpms = "λG. mk_symmetric G"
  from assms have "compatible G H" by auto
  with assms
  show "verts (?wpms H)   verts (?wpms G)"
    and "arcs (?wpms H)  arcs (?wpms G)"
    by (auto simp: parcs_mk_symmetric compatible_head compatible_tail)
  show "compatible (?wpms G) (?wpms H)" by rule
  interpret H: pair_wf_digraph "mk_symmetric H"
    using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
  interpret G: pair_wf_digraph "mk_symmetric G"
    using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
  show "wf_digraph (?wpms H)"
    by unfold_locales
  show "wf_digraph (?wpms G)" by unfold_locales
qed

lemma (in fin_digraph) subgraph_in_degree:
  assumes "subgraph H G"
  shows "in_degree H v  in_degree G v"
proof -
  have "finite (in_arcs G v)" by auto
  moreover
  have "in_arcs H v  in_arcs G v"
    using assms by (auto simp: subgraph_def in_arcs_def compatible_head compatible_tail)
  ultimately
  show ?thesis unfolding in_degree_def by (rule card_mono)
qed

lemma (in wf_digraph) subgraph_cycle:
  assumes "subgraph H G" "pre_digraph.cycle H p " shows "cycle p"
proof -
  from assms have "compatible G H" by auto
  with assms show ?thesis
    by (auto simp: pre_digraph.cycle_def compatible_awalk_verts intro: subgraph_awalk_imp_awalk)
qed

lemma (in wf_digraph) subgraph_del_vert: "subgraph (del_vert u) G"
  by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales

lemma (in wf_digraph) subgraph_del_arc: "subgraph (del_arc a) G"
  by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales



subsection ‹Induced subgraphs›

lemma wf_digraphI_induced:
  assumes "induced_subgraph H G"
  shows "wf_digraph H"
proof -
  from assms have "compatible G H" by auto
  with assms show ?thesis by unfold_locales (auto simp: compatible_tail compatible_head)
qed

lemma (in digraph) digraphI_induced:
  assumes "induced_subgraph H G"
  shows "digraph H"
proof -
  interpret W: wf_digraph H using assms by (rule wf_digraphI_induced)
  from assms have "compatible G H" by auto
  from assms have arcs: "arcs H  arcs G" by blast
  show ?thesis
  proof
    from assms have "verts H  verts G" by blast
    then show "finite (verts H)" using finite_verts by (rule finite_subset)
  next
    from arcs show "finite (arcs H)" using finite_arcs by (rule finite_subset)
  next
    fix e assume "e  arcs H"
    with arcs ‹compatible G H show "tail H e  head H e"
      by (auto dest: no_loops simp: compatible_tail[symmetric] compatible_head[symmetric])
  next
    fix e1 e2 assume "e1  arcs H" "e2  arcs H" and ate: "arc_to_ends H e1 = arc_to_ends H e2"
    with arcs ‹compatible G H show "e1 = e2" using ate
      by (auto intro: no_multi_arcs simp: compatible_tail[symmetric] compatible_head[symmetric] arc_to_ends_def)
  qed
qed

text ‹Computes the subgraph of @{term G} induced by @{term vs}
definition induce_subgraph :: "('a,'b) pre_digraph  'a set  ('a,'b) pre_digraph" (infix "" 67) where
  "G  vs =  verts = vs, arcs = {e  arcs G. tail G e  vs  head G e  vs},
    tail = tail G, head = head G "

lemma induce_subgraph_verts[simp]:
 "verts (G  vs) = vs"
by (auto simp add: induce_subgraph_def)

lemma induce_subgraph_arcs[simp]:
 "arcs (G  vs) = {e  arcs G. tail G e  vs  head G e  vs}"
by (auto simp add: induce_subgraph_def)

lemma induce_subgraph_tail[simp]:
  "tail (G  vs) = tail G"
by (auto simp: induce_subgraph_def)

lemma induce_subgraph_head[simp]:
  "head (G  vs) = head G"
by (auto simp: induce_subgraph_def)

lemma compatible_induce_subgraph: "compatible (G  S) G"
  by (auto simp: compatible_def)

lemma (in wf_digraph) induced_induce[intro]:
  assumes "vs  verts G"
  shows "induced_subgraph (G  vs) G"
using assms
by (intro subgraphI induced_subgraphI)
   (auto simp: arc_to_ends_def induce_subgraph_def wf_digraph_def compatible_def)

lemma (in wf_digraph) wellformed_induce_subgraph[intro]:
  "wf_digraph (G  vs)"
  by unfold_locales auto

lemma induced_graph_imp_symmetric:
  assumes "symmetric G"
  assumes "induced_subgraph H G"
  shows "symmetric H"
proof (unfold symmetric_conv, safe)
  from assms have "compatible G H" by auto

  fix e1 assume "e1  arcs H"
  then obtain e2 where "tail G e1 = head G e2"  "head G e1 = tail G e2" "e2  arcs G"
    using assms by (auto simp add: symmetric_conv)
  moreover
  then have "e2  arcs H"
    using assms and e1  arcs H by auto
  ultimately
  show "e2arcs H. tail H e1 = head H e2  head H e1 = tail H e2"
    using assms e1  arcs H ‹compatible G H
    by (auto simp: compatible_head compatible_tail)
qed

lemma (in sym_digraph) induced_graph_imp_graph:
  assumes "induced_subgraph H G"
  shows "sym_digraph H"
proof (rule wf_digraph.sym_digraphI)
  from assms show "wf_digraph H" by (rule wf_digraphI_induced)
next
  show "symmetric H"
    using assms sym_arcs by (auto intro: induced_graph_imp_symmetric)
qed

lemma (in wf_digraph) induce_reachable_preserves_paths:
  assumes "u *G v"
  shows "u *G  {w. u *G w} v"
  using assms
proof induct
  case base then show ?case by (auto simp: reachable_def)
next
  case (step u w)
  interpret iG: wf_digraph "G  {w. u *G w}"
    by (rule wellformed_induce_subgraph)
  from u  w have "u G  {wa. u *G wa} w"
    by (auto simp: arcs_ends_conv reachable_def intro: wellformed rtrancl_on_into_rtrancl_on)
  then have "u *G  {wa. u *G wa} w"
    by (rule iG.reachable_adjI)
  moreover
  from step have "{x. w * x}  {x. u * x}"
    by (auto intro: adj_reachable_trans)
  then have "subgraph (G  {wa. w * wa}) (G  {wa. u * wa})"
    by (intro subgraphI) (auto simp: arcs_ends_conv compatible_def)
  then have "w *G  {wa. u * wa} v"
    by (rule iG.reachable_mono[rotated]) fact
  ultimately show ?case by (rule iG.reachable_trans)
qed

lemma induce_subgraph_ends[simp]:
  "arc_to_ends (G  S) = arc_to_ends G"
  by (auto simp: arc_to_ends_def)

lemma dominates_induce_subgraphD:
  assumes "u G  S v" shows "u G v"
  using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)

context wf_digraph begin

  lemma reachable_induce_subgraphD:
    assumes "u *G  S v" "S  verts G" shows "u *G v"
  proof -
    interpret GS: wf_digraph "G  S" by auto
    show ?thesis
      using assms by induct (auto dest: dominates_induce_subgraphD intro: adj_reachable_trans)
  qed

  lemma dominates_induce_ss:
    assumes "u G  S v" "S  T" shows "u G  T v"
    using assms by (auto simp: arcs_ends_def)

  lemma reachable_induce_ss:
    assumes "u *G  S v" "S  T" shows "u *G  T v"
    using assms unfolding reachable_def
    by induct (auto intro: dominates_induce_ss converse_rtrancl_on_into_rtrancl_on)

  lemma awalk_verts_induce:
    "pre_digraph.awalk_verts (G  S) = awalk_verts"
  proof (intro ext)
    fix u p show "pre_digraph.awalk_verts (G  S) u p = awalk_verts u p"
      by (induct p arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps)
  qed

  lemma (in -) cas_subset:
    assumes "pre_digraph.cas G u p v" "subgraph G H"
    shows "pre_digraph.cas H u p v"
    using assms
    by (induct p arbitrary: u) (auto simp: pre_digraph.cas.simps subgraph_def compatible_def)

  lemma cas_induce:
    assumes "cas u p v" "set (awalk_verts u p)  S"
    shows "pre_digraph.cas (G  S) u p v"
    using assms
  proof (induct p arbitrary: u S)
    case Nil then show ?case by (auto simp: pre_digraph.cas.simps)
  next
    case (Cons a as)
    have "pre_digraph.cas (G  set (awalk_verts (head G a) as)) (head G a) as v"
      using Cons by auto
    then have "pre_digraph.cas (G  S) (head G a) as v"
      using _  S by (rule_tac cas_subset) (auto simp: subgraph_def compatible_def)
    then show ?case using Cons by (auto simp: pre_digraph.cas.simps)
  qed

  lemma awalk_induce:
    assumes "awalk u p v" "set (awalk_verts u p)  S"
    shows "pre_digraph.awalk (G  S) u p v"
  proof -
    interpret GS: wf_digraph "G  S" by auto
    show ?thesis
      using assms by (auto simp: pre_digraph.awalk_def cas_induce GS.cas_induce set_awalk_verts)
  qed

  lemma subgraph_induce_subgraphI:
    assumes "V  verts G" shows "subgraph (G  V) G"
    by (metis assms induced_imp_subgraph induced_induce)

end

lemma induced_subgraphI':
  assumes subg:"subgraph H G"
  assumes max: "H'. subgraph H' G  (verts H'  verts H  arcs H'  arcs H)"
  shows "induced_subgraph H G"
proof -
  interpret H: wf_digraph H using ‹subgraph H G ..
  define H' where "H' = G  verts H"
  then have H'_props: "subgraph H' G" "verts H' = verts H"
    using subg by (auto intro: wf_digraph.subgraph_induce_subgraphI)
  moreover
  have "arcs H' = arcs H"
  proof
    show "arcs H'  arcs H" using max H'_props by auto
    show "arcs H  arcs H'" using subg by (auto simp: H'_def compatible_def)
  qed
  then show "induced_subgraph H G" by (auto simp: induced_subgraph_def H'_def subg) 
qed

lemma (in pre_digraph) induced_subgraph_altdef:
  "induced_subgraph H G  subgraph H G  (H'. subgraph H' G  (verts H'  verts H  arcs H'  arcs H))" (is "?L  ?R")
proof -
  { fix H' :: "('a,'b) pre_digraph"
    assume A: "verts H' = verts H" "subgraph H' G"
    interpret H': wf_digraph H' using ‹subgraph H' G ..
    from ‹subgraph H' G
    have comp: "tail G = tail H'" "head G = head H'" by (auto simp: compatible_def)
    then have "a. a  arcs H'  tail G a  verts H" "a. a  arcs H'  tail G a  verts H"
      by (auto dest: H'.wellformed simp: A)
    then have "arcs H'  {e  arcs G. tail G e  verts H  head G e  verts H}"
      using ‹subgraph H' G by (auto simp: subgraph_def comp A(1)[symmetric])
  }
  then show ?thesis using induced_subgraphI'[of H G] by (auto simp: induced_subgraph_def)
qed



subsection ‹Unions of Graphs›

lemma
  verts_union[simp]: "verts (union G H) = verts G  verts H" and
  arcs_union[simp]: "arcs (union G H) = arcs G  arcs H" and
  tail_union[simp]: "tail (union G H) = tail G" and
  head_union[simp]: "head (union G H) = head G"
  by (auto simp: union_def)

lemma wellformed_union:
  assumes "wf_digraph G" "wf_digraph H" "compatible G H"
  shows "wf_digraph (union G H)"
  using assms
  by unfold_locales
     (auto simp: union_def compatible_tail compatible_head dest: wf_digraph.wellformed)

lemma subgraph_union_iff:
  assumes "wf_digraph H1" "wf_digraph H2" "compatible H1 H2"
  shows "subgraph (union H1 H2) G  subgraph H1 G  subgraph H2 G"
  using assms by (fastforce simp: compatible_def intro!: subgraphI wellformed_union)

lemma subgraph_union[intro]:
  assumes "subgraph H1 G" "compatible H1 G"
  assumes "subgraph H2 G" "compatible H2 G"
  shows "subgraph (union H1 H2) G"
proof -
  from assms have "wf_digraph (union H1 H2)"
    by (auto intro: wellformed_union simp: compatible_def)
  with assms show ?thesis
    by (auto simp add: subgraph_def union_def arc_to_ends_def compatible_def)
qed

lemma union_fin_digraph:
  assumes "fin_digraph G" "fin_digraph H" "compatible G H"
  shows "fin_digraph (union G H)"
proof intro_locales
  interpret G: fin_digraph G by (rule assms)
  interpret H: fin_digraph H by (rule assms)
  show "wf_digraph (union G H)" using assms
    by (intro wellformed_union) intro_locales
  show "fin_digraph_axioms (union G H)"
    using assms by unfold_locales (auto simp: union_def)
qed

lemma subgraphs_of_union:
  assumes "wf_digraph G" "wf_digraph G'" "compatible G G'"
  shows "subgraph G (union G G')"
    and "subgraph G' (union G G')"
  using assms by (auto intro!: subgraphI wellformed_union simp: compatible_def)


subsection ‹Maximal Subgraphs›

lemma (in pre_digraph) max_subgraph_mp:
  assumes "max_subgraph Q x" "x. P x  Q x" "P x" shows "max_subgraph P x"
  using assms by (auto simp: max_subgraph_def)

lemma (in pre_digraph) max_subgraph_prop: "max_subgraph P x  P x"
  by (simp add: max_subgraph_def)

lemma (in pre_digraph) max_subgraph_subg_eq:
  assumes "max_subgraph P H1" "max_subgraph P H2" "subgraph H1 H2"
  shows "H1 = H2"
  using assms by (auto simp: max_subgraph_def)

lemma subgraph_induce_subgraphI2:
  assumes "subgraph H G" shows "subgraph H (G  verts H)"
  using assms by (auto simp: subgraph_def compatible_def wf_digraph.wellformed wf_digraph.wellformed_induce_subgraph)

definition arc_mono :: "(('a,'b) pre_digraph  bool)  bool" where
  "arc_mono P  (H1 H2. P H1  subgraph H1 H2  verts H1 = verts H2  P H2)"

lemma (in pre_digraph) induced_subgraphI_arc_mono:
  assumes "max_subgraph P H"
  assumes "arc_mono P"
  shows "induced_subgraph H G"
proof -
  interpret wf_digraph G using assms by (auto simp: max_subgraph_def)
  have "subgraph H (G  verts H)" "subgraph (G  verts H) G" "verts H = verts (G  verts H)" "P H"
    using assms by (auto simp: max_subgraph_def subgraph_induce_subgraphI2 subgraph_induce_subgraphI)
  moreover
  then have "P (G  verts  H)"
    using assms by (auto simp: arc_mono_def)
  ultimately
  have "max_subgraph P (G  verts H)"
    using assms by (auto simp: max_subgraph_def) metis
  then have "H = G  verts H"
    using ‹max_subgraph P H ‹subgraph H _
    by (intro max_subgraph_subg_eq)
  show ?thesis using assms by (subst H = _) (auto simp: max_subgraph_def)
qed

lemma (in pre_digraph) induced_subgraph_altdef2:
  "induced_subgraph H G  max_subgraph (λH'. verts H' = verts H) H" (is "?L  ?R")
proof
  assume ?L
  moreover
  { fix H' assume "induced_subgraph H G" "subgraph H H'" "H  H'"
    then have "¬(subgraph H' G  verts H' = verts H)"
      by (auto simp: induced_subgraph_altdef compatible_def elim!: allE[where x=H'])
  }
  ultimately show "max_subgraph (λH'. verts H' = verts H) H" by (auto simp: max_subgraph_def)
next
  assume ?R
  moreover have "arc_mono (λH'. verts H' = verts H)" by (auto simp: arc_mono_def)
  ultimately show ?L by (rule induced_subgraphI_arc_mono)
qed

(*XXX*)
lemma (in pre_digraph) max_subgraphI:
  assumes "P x" "subgraph x G" "y. x  y; subgraph x y; subgraph y G  ¬P y"
  shows "max_subgraph P x"
  using assms by (auto simp: max_subgraph_def)

lemma (in pre_digraph) subgraphI_max_subgraph: "max_subgraph P x  subgraph x G"
  by (simp add: max_subgraph_def)


subsection ‹Connected and Strongly Connected Graphs›

context wf_digraph begin

  lemma in_sccs_verts_conv_reachable:
    "S  sccs_verts  S  {}  (u  S. v  S. u *G v)  (u  S. v. v  S  ¬u *G v  ¬v *G u)"
    by (simp add: sccs_verts_def)

  lemma sccs_verts_disjoint:
    assumes "S  sccs_verts" "T  sccs_verts" "S  T" shows "S  T = {}"
    using assms unfolding in_sccs_verts_conv_reachable by safe meson+

  lemma strongly_connected_spanning_imp_strongly_connected:
    assumes "spanning H G"
    assumes "strongly_connected H"
    shows "strongly_connected G"
  proof (unfold strongly_connected_def, intro ballI conjI)
    from assms show "verts G  {}" unfolding strongly_connected_def spanning_def by auto
  next
    fix u v assume "u  verts G" and "v  verts G"
    then have "u *H v" "subgraph H G"
      using assms by (auto simp add: strongly_connected_def)
    then show "u * v" by (rule reachable_mono)
  qed

  lemma strongly_connected_imp_induce_subgraph_strongly_connected:
    assumes subg: "subgraph H G"
    assumes sc: "strongly_connected H"
    shows "strongly_connected (G  (verts H))"
  proof -
    let ?is_H = "G  (verts H)"

    interpret H: wf_digraph H
      using subg by (rule subgraphE)
    interpret GrH: wf_digraph "?is_H"
      by (rule wellformed_induce_subgraph)

    have "verts H  verts G" using assms by auto

    have "subgraph H (G  verts H)"
      using subg by (intro subgraphI) (auto simp: compatible_def)
    then show ?thesis
      using induced_induce[OF ‹verts H  verts G]
        and sc GrH.strongly_connected_spanning_imp_strongly_connected
      unfolding spanning_def by auto
  qed

  lemma in_sccs_vertsI_sccs:
    assumes "S  verts ` sccs" shows "S  sccs_verts"
    unfolding sccs_verts_def
  proof (intro CollectI conjI allI ballI impI)
    show "S  {}" using assms by (auto simp: sccs_verts_def sccs_def strongly_connected_def)

    from assms have sc: "strongly_connected (G  S)" "S  verts G"
      apply (auto simp: sccs_verts_def sccs_def)
      by (metis induced_imp_subgraph subgraphE wf_digraph.strongly_connected_imp_induce_subgraph_strongly_connected)

    {
      fix u v assume A: "u  S" "v  S"
      with sc have "u *G  S v" by auto
      then show "u *G v" using S  verts G by (rule reachable_induce_subgraphD)
    next
      fix u v assume A: "u  S" "v  S"
      { assume B: "u *G v" "v *G u"
        from B obtain p_uv where p_uv: "awalk u p_uv v" by (metis reachable_awalk)
        from B obtain p_vu where p_vu: "awalk v p_vu u" by (metis reachable_awalk)
        define T where "T = S  set (awalk_verts u p_uv)  set (awalk_verts v p_vu)"
        have "S  T" by (auto simp: T_def)
        have "v  T" using p_vu by (auto simp: T_def set_awalk_verts)
        then have "T  S" using v  S by auto

        interpret T: wf_digraph "G  T" by auto

        from p_uv have T_p_uv: "T.awalk u p_uv v"
          by (rule awalk_induce) (auto simp: T_def)
        from p_vu have T_p_vu: "T.awalk v p_vu u"
          by (rule awalk_induce) (auto simp: T_def)

        have uv_reach: "u *G  T v" "v *G  T u"
          using T_p_uv T_p_vu A by (metis T.reachable_awalk)+

        { fix x y assume "x  S" "y  S"
          then have "x *G  S y" "y *G  S x"
            using sc by auto
          then have "x *G  T y" "y *G  T x"
            using S  T by (auto intro: reachable_induce_ss)
        } note A1 = this

        { fix x assume "x  T"
          moreover
          { assume "x  S" then have "x *G  T v"
              using uv_reach A1 A by (auto intro: T.reachable_trans[rotated])
          } moreover
          { assume "x  set (awalk_verts u p_uv)" then have "x *G  T v"
              using T_p_uv by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_to)
          } moreover
          { assume "x  set (awalk_verts v p_vu)" then have "x *G  T v"
              using T_p_vu by (rule_tac T.reachable_trans)
                (auto simp: uv_reach awalk_verts_induce dest: T.awalk_verts_reachable_to)
          } ultimately
          have "x *G  T v" by (auto simp: T_def)
        } note xv_reach = this

        { fix x assume "x  T"
          moreover
          { assume "x  S" then have "v *G  T x"
              using uv_reach A1 A by (auto intro: T.reachable_trans)
          } moreover
          { assume "x  set (awalk_verts v p_vu)" then have "v *G  T x"
              using T_p_vu by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_from)
          } moreover
          { assume "x  set (awalk_verts u p_uv)" then have "v *G  T x"
              using T_p_uv by (rule_tac T.reachable_trans[rotated])
                (auto intro: T.awalk_verts_reachable_from uv_reach simp: awalk_verts_induce)
          } ultimately
          have "v *G  T x" by (auto simp: T_def)
        } note vx_reach = this

        { fix x y assume "x  T" "y  T" then have "x *G  T y"
            using xv_reach vx_reach by (blast intro: T.reachable_trans)
        }
        then have "strongly_connected (G  T)"
          using S  {} S  T by auto
        moreover have "induced_subgraph (G  T) G"
          using S  verts G
          by (auto simp: T_def intro: awalk_verts_reachable_from p_uv p_vu reachable_in_verts(2))
        ultimately
        have "T. induced_subgraph (G  T) G  strongly_connected (G  T)  verts (G  S)  verts (G  T)"
          using S  T T  S by auto
        then have "G  S  sccs" unfolding sccs_def by blast
        then have "S  verts ` sccs"
          by (metis (erased, hide_lams) S  T T  S ‹induced_subgraph (G  T) G ‹strongly_connected (G  T)
            dual_order.order_iff_strict image_iff in_sccsE induce_subgraph_verts)
        then have False using assms by metis
      }
      then show "¬u *G v  ¬v *G u" by metis
    }
  qed

end

lemma arc_mono_strongly_connected[intro,simp]: "arc_mono strongly_connected"
  by (auto simp: arc_mono_def) (metis spanning_def subgraphE wf_digraph.strongly_connected_spanning_imp_strongly_connected)

lemma (in pre_digraph) sccs_altdef2:
  "sccs = {H. max_subgraph strongly_connected H}" (is "?L = ?R")
proof -
  { fix H H' :: "('a, 'b) pre_digraph" 
    assume a1: "strongly_connected H'"
    assume a2: "induced_subgraph H' G"
    assume a3: "max_subgraph strongly_connected H"
    assume a4: "verts H  verts H'"
    have sg: "subgraph H G" and ends_G: "tail G = tail H " "head G = head H"
      using a3 by (auto simp: max_subgraph_def compatible_def)
    then interpret H: wf_digraph H by blast
    have "arcs H  arcs H'" using a2 a4 sg by (fastforce simp: ends_G)
    then have "H = H'"
      using a1 a2 a3 a4
      by (metis (no_types) compatible_def induced_imp_subgraph max_subgraph_def subgraph_def)
  } note X = this

  { fix H
    assume a1: "induced_subgraph H G"
    assume a2: "strongly_connected H"
    assume a3: "H'. strongly_connected H'  induced_subgraph H' G  ¬ verts H  verts H'"
    interpret G: wf_digraph G using a1 by auto
    { fix y assume "H  y" and subg: "subgraph H y" "subgraph y G"
      then have "verts H  verts y"
        using a1 by (auto simp: induced_subgraph_altdef2 max_subgraph_def)
      then have "¬strongly_connected y"
        using subg a1 a2 a3[THEN spec, of "G  verts y"]
        by (auto simp: G.induced_induce G.strongly_connected_imp_induce_subgraph_strongly_connected)
    }
    then have "max_subgraph strongly_connected H"
      using a1 a2 by (auto intro: max_subgraphI)
  } note Y = this

  show ?thesis unfolding sccs_def
    by (auto dest: max_subgraph_prop X intro: induced_subgraphI_arc_mono Y)
qed

locale max_reachable_set = wf_digraph +
  fixes S assumes S_in_sv: "S  sccs_verts"
begin

  lemma reach_in: "u v. u  S; v  S  u *G v"
    and not_reach_out: "u v. u  S; v  S  ¬u *G v  ¬v *G u"
    and not_empty: "S  {}"
    using S_in_sv by (auto simp: sccs_verts_def)

  lemma reachable_induced:
    assumes conn: "u  S" "v  S" "u *G v"
    shows "u *G  S v"
  proof -
    let ?H = "G  S"
    have "S  verts G" using reach_in by (auto dest: reachable_in_verts)
    then have "induced_subgraph ?H G"
        by (rule induced_induce)
    then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)

    from conn obtain p where p: "awalk u p v" by (metis reachable_awalk)
    show ?thesis
    proof (cases "set p  arcs (G  S)")
      case True
      with p conn have "H.awalk u p v"
        by (auto simp: pre_digraph.awalk_def compatible_cas[OF compatible_induce_subgraph])
      then show ?thesis by (metis H.reachable_awalk)
    next
      case False
      then obtain a where "a  set p" "a  arcs (G  S)" by auto
      moreover
      then have "tail G a  S  head G a  S" using p by auto
      ultimately
      obtain w where "w  set (awalk_verts u p)" "w  S" using p by (auto simp: set_awalk_verts)
      then have "u *G w" "w *G v"
        using p by (auto intro: awalk_verts_reachable_from awalk_verts_reachable_to)
      moreover have "v *G u" using conn reach_in by auto
      ultimately have "u *G w" "w *G u" by (auto intro: reachable_trans)
      with w  S conn not_reach_out have False by blast
      then show ?thesis ..
    qed
  qed

  lemma strongly_connected:
    shows "strongly_connected (G  S)"
    using not_empty by (intro strongly_connectedI) (auto intro: reachable_induced reach_in)

  lemma induced_in_sccs: "G  S  sccs"
  proof -
    let ?H = "G  S"
    have "S  verts G" using reach_in by (auto dest: reachable_in_verts)
    then have "induced_subgraph ?H G"
        by (rule induced_induce)
    then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)

    { fix T assume "S  T" "T  verts G" "strongly_connected (G  T)"
      from S  T obtain v where "v  T" "v  S" by auto
      from not_empty obtain u where "u  S" by auto
      then have "u  T" using S  T by auto

      from u  S v  S have "¬u *G v  ¬v *G u" by (rule not_reach_out)
      moreover
      from ‹strongly_connected _ have "u *G  T v" "v *G  T u"
        using v  T u  T by (auto simp: strongly_connected_def)
      then have "u *G v" "v *G u"
        using T  verts G by (auto dest: reachable_induce_subgraphD)
      ultimately have False by blast
    } note psuper_not_sc = this

    have "¬ (c'. induced_subgraph c' G  strongly_connected c'  verts (G  S)  verts c')"
      by (metis induce_subgraph_verts induced_imp_subgraph psuper_not_sc subgraphE
        strongly_connected_imp_induce_subgraph_strongly_connected)
    with S  _ not_empty show "?H  sccs" by (intro in_sccsI induced_induce strongly_connected)
  qed
end

context wf_digraph begin

  lemma in_verts_sccsD_sccs:
    assumes "S  sccs_verts"
    shows "G  S  sccs"
  proof -
    from assms interpret max_reachable_set by unfold_locales
    show ?thesis by (auto simp: sccs_verts_def intro: induced_in_sccs)
  qed

  lemma sccs_verts_conv: "sccs_verts = verts ` sccs"
    by (auto intro: in_sccs_vertsI_sccs rev_image_eqI dest: in_verts_sccsD_sccs)

  lemma induce_eq_iff_induced:
    assumes "induced_subgraph H G" shows "G  verts H = H"
    using assms by (auto simp: induced_subgraph_def induce_subgraph_def compatible_def)

  lemma sccs_conv_sccs_verts: "sccs = induce_subgraph G ` sccs_verts"
    by (auto intro!: rev_image_eqI in_sccs_vertsI_sccs dest: in_verts_sccsD_sccs
      simp: sccs_def induce_eq_iff_induced)

end


lemma connected_conv:
  shows "connected G  verts G  {}  (u  verts G. v  verts G. (u,v)  rtrancl_on (verts G) ((arcs_ends G)s))"
proof -
  have "symcl (arcs_ends G) = parcs (mk_symmetric G)"
    by (auto simp: parcs_mk_symmetric symcl_def arcs_ends_conv)
  then show ?thesis by (auto simp: connected_def strongly_connected_def reachable_def)
qed

lemma (in wf_digraph) symmetric_connected_imp_strongly_connected:
  assumes "symmetric G" "connected G"
  shows "strongly_connected G"
proof
  from ‹connected G show "verts G  {}" unfolding connected_def strongly_connected_def by auto
next
  from ‹connected G
  have sc_mks: "strongly_connected (mk_symmetric G)"
    unfolding connected_def by simp

  fix u v assume "u  verts G" "v  verts G"
  with sc_mks have "u *mk_symmetric G v"
    unfolding strongly_connected_def by auto
  then show "u * v" using assms by (simp only: reachable_mk_symmetric_eq)
qed

lemma (in wf_digraph) connected_spanning_imp_connected:
  assumes "spanning H G"
  assumes "connected H"
  shows "connected G"
proof (unfold connected_def strongly_connected_def, intro conjI ballI)
  from assms show "verts (mk_symmetric G ) {}"
    unfolding spanning_def connected_def strongly_connected_def by auto
next
  fix u v
  assume "u  verts (mk_symmetric G)" and "v  verts (mk_symmetric G)"
  then have "u  pverts (mk_symmetric H)" and "v  pverts (mk_symmetric H)"
    using ‹spanning H G by (auto simp: mk_symmetric_def)
  with ‹connected H
  have "u *with_proj (mk_symmetric H) v" "subgraph (mk_symmetric H) (mk_symmetric G)"
    using ‹spanning H G unfolding connected_def
    by (auto simp: spanning_def dest: subgraph_mk_symmetric)
  then show "u *mk_symmetric G v" by (rule pre_digraph.reachable_mono)
qed

lemma (in wf_digraph) spanning_tree_imp_connected:
  assumes "spanning_tree H G"
  shows "connected G"
using assms by (auto intro: connected_spanning_imp_connected)

term "LEAST x. P x"

lemma (in sym_digraph) induce_reachable_is_in_sccs:
  assumes "u  verts G"
  shows "(G  {v. u * v})  sccs"
proof -
  let ?c = "(G  {v. u * v})"
  have isub_c: "induced_subgraph ?c G"
    by (auto elim: reachable_in_vertsE)
  then interpret c: wf_digraph ?c by (rule wf_digraphI_induced)

  have sym_c: "symmetric (G  {v. u * v})"
    using sym_arcs isub_c by (rule induced_graph_imp_symmetric)

  note ‹induced_subgraph ?c G
  moreover
  have "strongly_connected ?c"
  proof (rule strongly_connectedI)
    show "verts ?c  {}" using assms by auto
  next
    fix v w assume l_assms: "v  verts ?c" "w  verts ?c"
    have "u *G  {v. u * v} v"
      using l_assms by (intro induce_reachable_preserves_paths) auto
    then have "v *G  {v. u * v} u" by (rule symmetric_reachable[OF sym_c])
    also have "u *G  {v. u * v} w"
      using l_assms by (intro induce_reachable_preserves_paths) auto
    finally show "v *G  {v. u * v} w" .
  qed
  moreover
  have "¬(d. induced_subgraph d G  strongly_connected d 
    verts ?c  verts d)"
  proof
    assume "d. induced_subgraph d G  strongly_connected d 
      verts ?c  verts d"
    then obtain d where "induced_subgraph d G" "strongly_connected d"
      "verts ?c  verts d" by auto
    then obtain v where "v  verts d" and "v  verts ?c"
      by auto

    have "u  verts ?c" using u  verts G by auto
    then have "u  verts d" using ‹verts ?c  verts d by auto 
    then have "u *d v"
      using ‹strongly_connected d u  verts d v  verts d by auto
    then have "u * v"
      using ‹induced_subgraph d G
      by (auto intro: pre_digraph.reachable_mono)
    then have "v  verts ?c" by (auto simp: reachable_awalk)
    then show False using v  verts ?c by auto
  qed
  ultimately show ?thesis unfolding sccs_def by auto
qed

lemma induced_eq_verts_imp_eq:
  assumes "induced_subgraph G H"
  assumes "induced_subgraph G' H"
  assumes "verts G = verts G'"
  shows "G = G'"
  using assms by (auto simp: induced_subgraph_def subgraph_def compatible_def)

lemma (in pre_digraph) in_sccs_subset_imp_eq:
  assumes "c  sccs"
  assumes "d  sccs"
  assumes "verts c  verts d"
  shows "c = d"
using assms by (blast intro: induced_eq_verts_imp_eq)

context wf_digraph begin

  lemma connectedI:
    assumes "verts G  {}" "u v. u  verts G  v  verts G  u *mk_symmetric G v"
    shows "connected G"
    using assms by (auto simp: connected_def)
  
  lemma connected_awalkE:
    assumes "connected G" "u  verts G" "v  verts G"
    obtains p where "pre_digraph.awalk (mk_symmetric G) u p v"
  proof -
    interpret sG: pair_wf_digraph "mk_symmetric G" ..
    from assms have "u *mk_symmetric G v" by (auto simp: connected_def)
    then obtain p where "sG.awalk u p v" by (auto simp: sG.reachable_awalk)
    then show ?thesis ..
  qed

  lemma inj_on_verts_sccs: "inj_on verts sccs"
    by (rule inj_onI) (metis in_sccs_imp_induced induced_eq_verts_imp_eq)

  lemma card_sccs_verts: "card sccs_verts = card sccs"
    by (auto simp: sccs_verts_conv intro: inj_on_verts_sccs card_image)

end


lemma strongly_connected_non_disj:
  assumes wf: "wf_digraph G" "wf_digraph H" "compatible G H"
  assumes sc: "strongly_connected G" "strongly_connected H"
  assumes not_disj: "verts G  verts H  {}"
  shows "strongly_connected (union G H)"
proof
  from sc show "verts (union G H)  {}"
    unfolding strongly_connected_def by simp
next
  let ?x = "union G H"
  fix u v w assume "u  verts ?x" and "v  verts ?x"
  obtain w where w_in_both: "w  verts G" "w  verts H"
    using not_disj by auto

  interpret x: wf_digraph ?x
    by (rule wellformed_union) fact+
  have subg: "subgraph G ?x" "subgraph H ?x"
    by (rule subgraphs_of_union[OF _ _ ], fact+)+
  have reach_uw: "u *?x w"
    using u  verts ?x subg w_in_both sc
    by (auto intro: pre_digraph.reachable_mono)
  also have reach_wv: "w *?x v"
    using v  verts ?x subg w_in_both sc
    by (auto intro: pre_digraph.reachable_mono)
  finally (x.reachable_trans) show "u *?x v" .
qed

context wf_digraph begin

  lemma scc_disj:
    assumes scc: "c  sccs" "d  sccs"
    assumes "c  d"
    shows "verts c  verts d = {}"
  proof (rule ccontr)
    assume contr: "¬?thesis"

    let ?x = "union c d"

    have comp1: "compatible G c" "compatible G d"
      using scc by (auto simp: sccs_def)
    then have comp: "compatible c d" by (auto simp: compatible_def)

    have wf: "wf_digraph c" "wf_digraph d"
      and sc: "strongly_connected c" "strongly_connected d"
      using scc by (auto intro: in_sccs_imp_induced)
    have "compatible c d"
      using comp by (auto simp: sccs_def compatible_def)
    from wf comp sc have union_conn: "strongly_connected ?x"
      using contr by (rule strongly_connected_non_disj)

    have sg: "subgraph ?x G"
      using scc comp1 by (intro subgraph_union) (auto simp: compatible_def)
    then have v_cd: "verts c  verts G"  "verts d  verts G" by (auto elim!: subgraphE)
    have "wf_digraph ?x" by (rule wellformed_union) fact+
    with v_cd sg union_conn
    have induce_subgraph_conn: "strongly_connected (G  verts ?x)"
        "induced_subgraph (G  verts ?x) G"
      by - (intro strongly_connected_imp_induce_subgraph_strongly_connected,
        auto simp: subgraph_union_iff)

    from assms have "¬verts c  verts d" and "¬ verts d  verts c"
      by (metis in_sccs_subset_imp_eq)+
    then have psub: "verts c  verts ?x"
      by (auto simp: union_def)
    then show False using induce_subgraph_conn
      by (metis c  sccs› in_sccsE induce_subgraph_verts)
  qed

  lemma in_sccs_verts_conv:
    "S  sccs_verts  G  S  sccs"
    by (auto simp: sccs_verts_conv intro: rev_image_eqI)
      (metis in_sccs_imp_induced induce_subgraph_verts induced_eq_verts_imp_eq induced_imp_subgraph induced_induce subgraphE)

end

lemma (in wf_digraph) in_scc_of_self: "u  verts G  u  scc_of u"
  by (auto simp: scc_of_def)

lemma (in wf_digraph) scc_of_empty_conv: "scc_of u = {}  u  verts G"
  using in_scc_of_self by (auto simp: scc_of_def reachable_in_verts)

lemma (in wf_digraph) scc_of_in_sccs_verts:
  assumes "u  verts G" shows "scc_of u  sccs_verts"
  using assms by (auto simp: in_sccs_verts_conv_reachable scc_of_def intro: reachable_trans exI[where x=u])

lemma (in wf_digraph) sccs_verts_subsets: "S  sccs_verts  S  verts G"
  by (auto simp: sccs_verts_conv)

lemma (in fin_digraph) finite_sccs_verts: "finite sccs_verts"
proof -
  have "finite (Pow (verts G))" by auto
  moreover with sccs_verts_subsets have "sccs_verts  Pow (verts G)" by auto
  ultimately show ?thesis by (rule rev_finite_subset)
qed

lemma (in wf_digraph) sccs_verts_conv_scc_of:
  "sccs_verts = scc_of ` verts G" (is "?L = ?R")
proof (intro set_eqI iffI)
  fix S assume "S  ?R" then show "S  ?L"
    by (auto simp: in_sccs_verts_conv_reachable scc_of_empty_conv) (auto simp: scc_of_def intro: reachable_trans)
next
  fix S assume "S  ?L"
  moreover
  then obtain u where "u  S" by (auto simp: in_sccs_verts_conv_reachable)
  moreover
  then have "u  verts G" using S  ?L by (metis sccs_verts_subsets subsetCE)
  then have "scc_of u  sccs_verts" "u  scc_of u"
    by (auto intro: scc_of_in_sccs_verts in_scc_of_self)
  ultimately
  have "scc_of u = S" using sccs_verts_disjoint by blast
  then show "S  ?R" using ‹scc_of u  _ u  verts G by auto
qed

lemma (in sym_digraph) scc_ofI_reachable:
  assumes "u * v" shows "u  scc_of v"
  using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])

lemma (in sym_digraph) scc_ofI_reachable':
  assumes "v * u" shows "u  scc_of v"
  using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])

lemma (in sym_digraph) scc_ofI_awalk:
  assumes "awalk u p v" shows "u  scc_of v"
  using assms by (metis reachable_awalk scc_ofI_reachable)

lemma (in sym_digraph) scc_ofI_apath:
  assumes "apath u p v" shows "u  scc_of v"
  using assms by (metis reachable_apath scc_ofI_reachable)

lemma (in wf_digraph) scc_of_eq: "u  scc_of v  scc_of u = scc_of v"
  by (auto simp: scc_of_def intro: reachable_trans)

lemma (in wf_digraph) strongly_connected_eq_iff:
  "strongly_connected G  sccs = {G}" (is "?L  ?R")
proof
  assume ?L
  then have "G  sccs" by (auto simp: sccs_def induced_subgraph_refl)
  moreover
  { fix H assume "H  sccs" "G  H"
    with G  sccs› have "verts G  verts H = {}" by (rule scc_disj)
    moreover
    from H  sccs› have "verts H  verts G" by auto
    ultimately
    have "verts H = {}" by auto
    with H  sccs› have "False" by (auto simp: sccs_def strongly_connected_def)
  } ultimately
  show ?R by auto
qed (auto simp: sccs_def)




subsection ‹Components›

lemma (in sym_digraph) exists_scc:
  assumes "verts G  {}" shows "c. c  sccs"
proof -
  from assms obtain u where "u  verts G" by auto
  then show ?thesis by (blast dest: induce_reachable_is_in_sccs)
qed

theorem (in sym_digraph) graph_is_union_sccs:
  shows "Union sccs = G"
proof -
  have "(c  sccs. verts c) = verts G"
    by (auto intro: induce_reachable_is_in_sccs)
  moreover
  have "(c  sccs. arcs c) = arcs G"
  proof
    show "(c  sccs. arcs c)  arcs G"
      by safe (metis in_sccsE induced_imp_subgraph subgraphE subsetD)
    show "arcs G  (c  sccs. arcs c)"
    proof (safe)
      fix e assume "e  arcs G"
      define a b where [simp]: "a = tail G e" and [simp]: "b = head G e"

      have "e  (x  sccs. arcs x)"
      proof cases
        assume "xsccs. {a,b }  verts x"
        then obtain c where "c  sccs" and "{a,b}  verts c"
          by auto
        then have "e  {e  arcs G. tail G e  verts c
           head G e  verts c}" using e  arcs G by auto
        then have "e  arcs c" using c  sccs› by blast
        then show ?thesis using c  sccs› by auto
      next
        assume l_assm: "¬(xsccs. {a,b}  verts x)"

        have "a * b" using e  arcs G 
          by (metis a_def b_def reachable_adjI in_arcs_imp_in_arcs_ends)
        then have "{a,b}  verts (G  {v. a * v})" "a  verts G"
          by (auto elim: reachable_in_vertsE)
        moreover
        have "(G  {v. a * v})  sccs"
          using a  verts G by (auto intro: induce_reachable_is_in_sccs)
        ultimately
        have False using l_assm by blast
        then show ?thesis by simp
      qed
      then show "e  (c  sccs. arcs c)" by auto
    qed
  qed
  ultimately show ?thesis
    by (auto simp add: Union_def)
qed

lemma (in sym_digraph) scc_for_vert_ex:
  assumes "u  verts G"
  shows "c. csccs  u  verts c"
using assms by (auto intro: induce_reachable_is_in_sccs)



lemma (in sym_digraph) scc_decomp_unique:
  assumes "S  sccs" "verts (Union S) = verts G" shows "S = sccs"
proof (rule ccontr)
  assume "S  sccs"
  with assms obtain c where "c  sccs" and "c  S" by auto
  with assms have "d. d  S  verts c  verts d = {}"
    by (intro scc_disj) auto
  then have "verts c  verts (Union S) = {}"
    by (auto simp: Union_def)
  with assms have "verts c  verts G = {}" by auto
  moreover from c  sccs› obtain u where "u  verts c  verts G"
    by (auto simp: sccs_def strongly_connected_def)
  ultimately show False by blast
qed


end

Theory Vertex_Walk

(* Title:  Vertex_Walk.thy
   Author: Lars Noschinski, TU München
*)

theory Vertex_Walk
imports Arc_Walk
begin

section ‹Walks Based on Vertices›

text ‹
  These definitions are here mainly for historical purposes, as they
  do not really work with multigraphs. Consider using Arc Walks
  instead.
›

type_synonym 'a vwalk = "'a list"

text ‹Computes the list of arcs belonging to a list of nodes›
fun vwalk_arcs :: "'a vwalk  ('a × 'a) list" where
    "vwalk_arcs [] = []"
  | "vwalk_arcs [x] = []"
  | "vwalk_arcs (x#y#xs) = (x,y) # vwalk_arcs (y#xs)"

definition vwalk_length :: "'a vwalk  nat" where
  "vwalk_length p  length (vwalk_arcs p)"

lemma vwalk_length_simp[simp]:
  shows "vwalk_length p = length p - 1"
by (induct p rule: vwalk_arcs.induct) (auto simp: vwalk_length_def)

definition vwalk :: "'a vwalk  ('a,'b) pre_digraph  bool" where
  "vwalk p G  set p  verts G  set (vwalk_arcs p)  arcs_ends G  p  []"

definition vpath :: "'a vwalk  ('a,'b) pre_digraph  bool" where
  "vpath p G  vwalk p G  distinct p"

text ‹For a given vwalk, compute a vpath with the same tail G and end›
function vwalk_to_vpath :: "'a vwalk  'a vwalk" where
    "vwalk_to_vpath [] = []"
  | "vwalk_to_vpath (x # xs) = (if (x  set xs)
      then vwalk_to_vpath (dropWhile (λy. y  x) xs)
      else x # vwalk_to_vpath xs)"
by p