Theory Graph_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