Theory Graph_Theory.Subdivision

theory Subdivision
imports
  Arc_Walk
  Digraph_Component
  Pair_Digraph
  Bidirected_Digraph
  Auxiliary
begin

section ‹Subdivision on Digraphs›

definition
  subdivision_step :: "('a, 'b) pre_digraph ⇒ ('b ⇒ 'b) ⇒ ('a, 'b) pre_digraph ⇒ ('b ⇒ 'b) ⇒ 'a × 'a × 'a ⇒ 'b × 'b × 'b ⇒ bool"
where
  "subdivision_step G rev_G H rev_H ≡ λ(u, v, w) (uv, uw, vw).
      bidirected_digraph G rev_G
    ∧ bidirected_digraph H rev_H
    ∧ perm_restrict rev_H (arcs G) = perm_restrict rev_G (arcs H)
    ∧ compatible G H

    ∧ verts H = verts G ∪ {w}
    ∧ w ∉ verts G

    ∧ arcs H = {uw, rev_H uw, vw, rev_H vw} ∪ arcs G - {uv, rev_G uv}
    ∧ uv ∈ arcs G
    ∧ distinct [uw, rev_H uw, vw, rev_H vw]
    ∧ arc_to_ends G uv = (u,v)
    ∧ arc_to_ends H uw = (u,w)
    ∧ arc_to_ends H vw = (v,w)
  "

inductive subdivision :: "('a,'b) pre_digraph × ('b ⇒ 'b) ⇒ ('a,'b) pre_digraph × ('b ⇒ 'b) ⇒ bool"
  for biG where
    base: "bidirected_digraph (fst biG) (snd biG) ⟹ subdivision biG biG"
  | divide: "⟦subdivision biG biI; subdivision_step (fst biI) (snd biI) (fst biH) (snd biH) (u,v,w) (uv,uw,vw)⟧ ⟹ subdivision biG biH"

lemma subdivision_induct[case_names base divide, induct pred: subdivision]:
  assumes "subdivision (G, rev_G) (H, rev_H)"
    and "bidirected_digraph G rev_G ⟹ P G rev_G"
    and "⋀I rev_I H rev_H u v w uv uw vw.
            subdivision (G, rev_G) (I, rev_I) ⟹ P I rev_I ⟹ subdivision_step I rev_I H rev_H (u, v, w) (uv, uw, vw) ⟹ P H rev_H"
  shows "P H rev_H"
  using assms(1) by (induct biH≡"(H, rev_H)" arbitrary: H rev_H) (auto intro: assms(2,3))

lemma subdivision_base:
  "bidirected_digraph G rev_G ⟹ subdivision (G, rev_G) (G, rev_G)"
  by (rule subdivision.base) simp

lemma subdivision_step_rev:
  assumes "subdivision_step G rev_G H rev_H (u, v, w) (uv, uw, vw)" "subdivision (H, rev_H) (I, rev_I)"
  shows "subdivision (G, rev_G) (I, rev_I)"
proof -
  have "bidirected_digraph (fst (G, rev_G)) (snd (G, rev_G))" using assms by (auto simp: subdivision_step_def)
  with assms(2,1) show ?thesis
    using assms(2,1) by induct (auto intro: subdivision.intros dest: subdivision_base)
qed

lemma subdivision_trans:
  assumes "subdivision (G, rev_G) (H, rev_H)" "subdivision (H, rev_H) (I, rev_I)"
  shows "subdivision (G, rev_G) (I, rev_I)"
  using assms by induction (auto intro: subdivision_step_rev)

locale subdiv_step =
  fixes G rev_G H rev_H u v w uv uw vw
  assumes subdiv_step: "subdivision_step G rev_G H rev_H (u, v, w) (uv, uw, vw)"

sublocale subdiv_step ⊆ G: bidirected_digraph G rev_G
  using subdiv_step unfolding subdivision_step_def by simp
sublocale subdiv_step ⊆ H: bidirected_digraph H rev_H
  using subdiv_step unfolding subdivision_step_def by simp

context subdiv_step begin

  (*XXX*)
  abbreviation (input) "vu ≡ rev_G uv"
  abbreviation (input) "wu ≡ rev_H uw"
  abbreviation (input) "wv ≡ rev_H vw"

  lemma subdiv_compat: "compatible G H"
    using subdiv_step by (simp add: subdivision_step_def)

  lemma arc_to_ends_eq: "arc_to_ends H = arc_to_ends G"
    using subdiv_compat by (simp add: compatible_def arc_to_ends_def fun_eq_iff)

  lemma head_eq: "head H = head G"
    using subdiv_compat by (simp add: compatible_def fun_eq_iff)

  lemma tail_eq: "tail H = tail G"
    using subdiv_compat by (simp add: compatible_def fun_eq_iff)

  lemma verts_H: "verts H = verts G ∪ {w}"
    using subdiv_step by (simp add: subdivision_step_def)

  lemma verts_G: "verts G = verts H - {w}"
    using subdiv_step by (auto simp: subdivision_step_def)

  lemma arcs_H: "arcs H = {uw, wu, vw, wv} ∪ arcs G - {uv, vu}"
    using subdiv_step by (simp add: subdivision_step_def)

  lemma not_in_verts_G: "w ∉ verts G"
    using subdiv_step by (simp add: subdivision_step_def)

  lemma in_arcs_G: "{uv, vu} ⊆ arcs G"
    using subdiv_step by (simp add: subdivision_step_def)

  lemma not_in_arcs_H: "{uv,vu} ∩ arcs H = {}"
    using arcs_H by auto

  lemma subdiv_ate:
      "arc_to_ends G uv = (u,v)"
      "arc_to_ends H uv = (u,v)"
      "arc_to_ends H uw = (u,w)"
      "arc_to_ends H vw = (v,w)"
    using subdiv_step subdiv_compat by (auto simp: subdivision_step_def arc_to_ends_def compatible_def)

  lemma subdiv_ends[simp]:
    "tail G uv = u" "head G uv = v" "tail H uv = u" "head H uv = v"
    "tail H uw = u" "head H uw = w" "tail H vw = v" "head H vw = w"
    using subdiv_ate by (auto simp: arc_to_ends_def)

  lemma subdiv_ends_G_rev[simp]:
    "tail G (vu) = v" "head G (vu) = u" "tail H (vu) = v" "head H (vu) = u"
    using in_arcs_G by (auto simp: tail_eq head_eq)

  lemma subdiv_distinct_verts0: "u ≠ w" "v ≠ w"
      using in_arcs_G not_in_verts_G using subdiv_ate by (auto simp: arc_to_ends_def dest: G.wellformed)

  lemma in_arcs_H: "{uw, wu, vw, wv} ⊆ arcs H"
  proof -
    { assume "uv = uw"
      then have "arc_to_ends H uv = arc_to_ends H uw" by simp
      then have "v = w" by (simp add: arc_to_ends_def)
    } moreover
    { assume "uv = vw"
      then have "arc_to_ends H uv = arc_to_ends H vw" by simp
      then have "v = w" by (simp add: arc_to_ends_def)
    } moreover
    { assume "vu = uw"
      then have "arc_to_ends H (vu) = arc_to_ends H uw" by simp
      then have "u = w" by (simp add: arc_to_ends_def)
    } moreover
    { assume "vu = vw"
      then have "arc_to_ends H (vu) = arc_to_ends H vw" by simp
      then have "u = w" by (simp add: arc_to_ends_def)
    } ultimately
    have "{uw,vw} ⊆ arcs H" unfolding arcs_H using subdiv_distinct_verts0 by auto
    then show ?thesis by auto
  qed

  lemma subdiv_ends_H_rev[simp]:
    "tail H (wu) = w" "tail H (wv) = w"
    "head H (wu) = u" "head H (wv) = v"
    using in_arcs_H subdiv_ate by simp_all

  lemma in_verts_G: "{u,v} ⊆ verts G"
    using in_arcs_G by (auto dest: G.wellformed)

  lemma not_in_arcs_G: "{uw, wu, vw, wv} ∩ arcs G = {}"
  proof -
    note X = G.wellformed[simplified tail_eq[symmetric] head_eq[symmetric]]
    show ?thesis using not_in_verts_G in_arcs_H by (auto dest: X )
  qed

  lemma subdiv_distinct_arcs: "distinct [uv, vu, uw, wu, vw, wv]"
  proof -
    have "distinct [uw, wu, vw, wv]"
      using subdiv_step by (simp add: subdivision_step_def)
    moreover
    have "distinct [uv, vu]" using in_arcs_G G.arev_dom by auto
    moreover
    have "{uv, vu} ∩ {uw, wu, vw, wv} = {}"
      using arcs_H in_arcs_H by auto
    ultimately show ?thesis by auto
  qed

  lemma arcs_G: "arcs G = arcs H ∪ {uv, vu} - {uw, wu, vw, wv}"
    using in_arcs_G not_in_arcs_G unfolding arcs_H by auto

  lemma subdiv_ate_H_rev:
    "arc_to_ends H (wu) = (w,u)"
    "arc_to_ends H (wv) = (w,v)"
    using in_arcs_H subdiv_ate by simp_all

  lemma adj_with_w: "u →⇘H⇙ w" "w →⇘H⇙ u" "v →⇘H⇙ w" "w →⇘H⇙ v"
    using in_arcs_H subdiv_ate by (auto intro: H.dominatesI[rotated])

  lemma w_reach: "u →⇧*⇘H⇙ w" "w →⇧*⇘H⇙ u" "v →⇧*⇘H⇙ w" "w →⇧*⇘H⇙ v"
    using adj_with_w by auto

  lemma G_reach: "v →⇧*⇘G⇙ u" "u →⇧*⇘G⇙ v"
    using subdiv_ate in_arcs_G by (simp add: G.dominatesI G.symmetric_reachable')+

  lemma out_arcs_w: "out_arcs H w = {wu, wv}"
    using subdiv_distinct_verts0 in_arcs_H
    by (auto simp: arcs_H) (auto simp: tail_eq verts_G dest: G.tail_in_verts)

  lemma out_degree_w: "out_degree H w = 2"
    using subdiv_distinct_arcs by (auto simp: out_degree_def out_arcs_w card_insert_if)

end

lemma subdivision_compatible:
  assumes "subdivision (G, rev_G) (H, rev_H)" shows "compatible G H"
  using assms by induct (auto simp: compatible_def subdivision_step_def)

lemma subdivision_bidir:
  assumes "subdivision (G, rev_G) (H, rev_H)"
  shows "bidirected_digraph H rev_H"
  using assms by induct (auto simp: subdivision_step_def)

lemma subdivision_choose_rev:
  assumes "subdivision (G, rev_G) (H, rev_H)" "bidirected_digraph H rev_H'"
  shows "∃rev_G'. subdivision (G, rev_G') (H, rev_H')"
  using assms
proof (induction arbitrary: rev_H')
  case base
  then show ?case by (auto dest: subdivision_base)
next
  case (divide I rev_I H rev_H u v w uv uw vw)

  interpret subdiv_step I rev_I H rev_H u v w uv uw vw using divide by unfold_locales
  interpret H': bidirected_digraph H rev_H' by fact

  define rev_I' where "rev_I' x =
    (if x = uv then rev_I uv else if x = rev_I uv then uv else if x ∈ arcs I then rev_H' x else x)"
    for x

  have rev_H_injD: "⋀x y z. rev_H' x = z ⟹ rev_H' y = z ⟹ x ≠ y ⟹ False"
    by (metis H'.arev_eq_iff)

  have rev_H'_simps: "rev_H' uw = rev_H uw ∧ rev_H' vw = rev_H vw
    ∨ rev_H' uw = rev_H vw ∧ rev_H' vw = rev_H uw"
  proof -
    have "arc_to_ends H (rev_H' uw) = (w,u)" "arc_to_ends H (rev_H' vw) = (w,v)"
      using in_arcs_H by (auto simp: subdiv_ate)
    moreover
    have "⋀x. x ∈ arcs H ⟹ tail H x = w ⟹ x ∈ {rev_H uw, rev_H vw}"
      using subdiv_distinct_verts0 not_in_verts_G by (auto simp: arcs_H) (simp add: tail_eq)
    ultimately
    have "rev_H' uw ∈ {rev_H uw, rev_H vw}" "rev_H' vw ∈ {rev_H uw, rev_H vw}"
      using in_arcs_H by auto
    then show ?thesis using in_arcs_H by (auto dest: rev_H_injD)
  qed

  have rev_H_uv: "rev_H' uv = uv" "rev_H' (rev_I uv) = rev_I uv"
    using not_in_arcs_H by (auto simp: H'.arev_eq)

  have bd_I': "bidirected_digraph I rev_I'"
  proof
    fix a
    have "⋀a. a ≠ uv ⟹ a ≠ rev_I uv ⟹ a ∈ arcs I ⟹ a ∈ arcs H"
      by (auto simp: arcs_H)
    then show "(a ∈ arcs I) = (rev_I' a ≠ a)"
      using in_arcs_G by (auto simp: rev_I'_def dest: G.arev_neq H'.arev_neq)
  next
    fix a
    have *: "⋀a. rev_H' a = rev_I uv ⟷ a = rev_I uv"
      by (metis H'.arev_arev H'.arev_dom insert_disjoint(1) not_in_arcs_H)
    have **: "⋀a. uv = rev_H' a ⟷ a = uv" using H'.arev_eq not_in_arcs_H by force
    have ***: "⋀a. a ∈ arcs I ⟹ rev_H' a ∈ arcs I"
      using rev_H'_simps  by (case_tac "a ∈ {uv,vu}") (fastforce simp: rev_H_uv, auto simp: arcs_G dest: rev_H_injD)
    show "rev_I' (rev_I' a) = a"
      by (auto simp: rev_I'_def H'.arev_eq rev_H_uv * ** ***)
  next
    fix a assume "a ∈ arcs I"
    then show "tail I (rev_I' a) = head I a"
      using in_arcs_G by (auto simp: rev_I'_def tail_eq[symmetric] head_eq[symmetric] arcs_H)
  qed
  moreover
  have "⋀x. rev_H' x = uv ⟷ x = uv" "⋀x. rev_H' x = rev_I uv ⟷ x = rev_I uv"
    using not_in_arcs_H by (auto dest: H'.arev_eq) (metis H'.arev_arev H'.arev_eq)
  then have "perm_restrict rev_H' (arcs I) = perm_restrict rev_I' (arcs H)"
    using not_in_arcs_H by (auto simp: rev_I'_def perm_restrict_def H'.arev_eq)
  ultimately
  have sds_I'H': "subdivision_step I rev_I' H rev_H' (u, v, w) (uv, uw, vw)"
    using divide(2,4) rev_H'_simps unfolding subdivision_step_def
    by (fastforce simp:  rev_I'_def)
  then have "subdivision (I, rev_I') (H, rev_H')" "∃rev_G'. subdivision (G, rev_G') (I, rev_I')"
    using bd_I' divide by (auto intro: subdivision.intros dest: subdivision_base)
  then show ?case by (blast intro: subdivision_trans)
qed

lemma subdivision_verts_subset:
  assumes "subdivision (G,rev_G) (H,rev_H)" "x ∈ verts G"
  shows "x ∈ verts H"
  using assms by induct (auto simp: subdiv_step.verts_H subdiv_step_def)


subsection ‹Subdivision on Pair Digraphs›

text ‹
  In this section, we introduce specialized rules for pair digraphs.
›

abbreviation "subdivision_pair G H ≡ subdivision (with_proj G, swap_in (parcs G)) (with_proj H, swap_in (parcs H))"

lemma arc_to_ends_with_proj[simp]: "arc_to_ends (with_proj G) = id"
  by (auto simp: arc_to_ends_def)

context
begin

  text ‹
    We use the @{verbatim inductive} command to define an inductive definition pair graphs.
    This is proven to be equivalent to @{const subdivision}.
    This allows us to transfer the rules proven by @{verbatim inductive} to @{const subdivision}.
    To spare the user confusion, we hide this new constant.
  ›

  private inductive pair_sd :: "'a pair_pre_digraph ⇒ 'a pair_pre_digraph ⇒ bool"
    for G where
      base: "pair_bidirected_digraph G ⟹ pair_sd G G"
    | divide: "⋀e w H. ⟦e ∈ parcs H; w ∉ pverts H; pair_sd G H⟧
        ⟹ pair_sd G (subdivide H e w)"

  private lemma bidirected_digraphI_pair_sd:
    assumes "pair_sd G H" shows "pair_bidirected_digraph H"
    using assms
  proof induct
    case base
    then show ?case by auto
  next
    case (divide e w H)
    interpret H: pair_bidirected_digraph H by fact
    from divide show ?case by (intro H.pair_bidirected_digraph_subdivide)
  qed

  private lemma subdivision_with_projI:
    assumes "pair_sd G H"
    shows "subdivision_pair G H"
    using assms
  proof induct
    case base
    then show ?case by (blast intro: pair_bidirected_digraph.bidirected_digraph subdivision_base)
  next
    case (divide e w H)

    obtain u v where "e = (u,v)" by (cases e)

    interpret H: pair_bidirected_digraph H
      using divide(3) by (rule bidirected_digraphI_pair_sd)
    interpret I: pair_bidirected_digraph "subdivide H e w"
      using divide(1,2) by (rule H.pair_bidirected_digraph_subdivide)

    have uvw: "u ≠ v" "u ≠ w" "v ≠ w"
      using divide by (auto simp: ‹e = _› dest: H.adj_not_same H.wellformed)

    have "subdivision (with_proj G, swap_in (parcs G)) (H, swap_in (parcs H))"
      using divide by auto
    moreover
    have *: "perm_restrict (swap_in (parcs (subdivide H e w))) (parcs H) = perm_restrict (swap_in (parcs H)) (parcs (subdivide H e w))"
      by (auto simp: perm_restrict_def fun_eq_iff swap_in_def)
    have "subdivision_step (with_proj H) (swap_in (arcs H)) (with_proj (subdivide H e w)) (swap_in (arcs (subdivide H e w)))
        (u, v, w) (e, (u,w), (v,w))"
      unfolding subdivision_step_def
      unfolding prod.simps with_proj_simps
      using divide uvw
      by (intro conjI H.bidirected_digraph I.bidirected_digraph *)
         (auto simp add: swap_in_def ‹e = _› compatibleI_with_proj)
    ultimately
    show ?case by (auto intro: subdivision.divide)
  qed

  private lemma subdivision_with_projD:
    assumes "subdivision_pair G H"
    shows "pair_sd G H"
    using assms
  proof (induct "with_proj H" "swap_in (parcs H)" arbitrary: H rule: subdivision_induct)
    case base
    interpret bidirected_digraph "with_proj G" "swap_in (parcs G)" by fact
    from base have "G = H" by (simp add: with_proj_def)
    with base show ?case
      by (auto intro: pair_sd.base pair_bidirected_digraphI_bidirected_digraph)
  next
    case (divide I rev_I u v w uv uw vw)
    define I' where "I' = ⦇ pverts = verts I, parcs = arcs I ⦈"
    have "compatible G I " using ‹subdivision (with_proj G, _) (I, _)›
      by (rule subdivision_compatible)
    then have "tail I = fst" "head I = snd" by (auto simp: compatible_def)
    then have I: "I = I'" by (auto simp: I'_def)
    moreover
    from I have "rev_I = swap_in (parcs I')"
      using ‹subdivision_step _ _ _ _ _ _›
      by (simp add: subdivision_step_def bidirected_digraph_rev_conv_pair)
    ultimately
    have pd_sd: "pair_sd G I'" by (auto intro: divide.hyps)

    interpret sd: subdiv_step I' "swap_in (parcs I')" H "swap_in (parcs H)" u v w uv uw vw
      using ‹subdivision_step _ _ _ _ _ _› unfolding ‹I = _› ‹rev_I = _› by unfold_locales

    have ends: "uv = (u,v)" "uw = (u,w)" "vw = (v,w)"
      using sd.subdiv_ate by simp_all
    then have si_ends: "swap_in (parcs H) (u,w) = (w,u)" "swap_in (parcs H) (v,w) = (w,v)"
        "swap_in (parcs I') (u,v) = (v,u)"
      using sd.subdiv_ends_H_rev sd.subdiv_ends_G_rev by (auto simp: swap_in_def)

    have "parcs H = parcs I' - {(u, v), (v, u)} ∪ {(u, w), (w, u), (w, v), (v, w)}"
      using sd.in_arcs_G sd.not_in_arcs_G sd.arcs_H by (auto simp: si_ends ends)
    then have "H = subdivide I' uv w" using sd.verts_H by (simp add: ends subdivide.simps)
    then show ?case
      using sd.in_arcs_G sd.not_in_verts_G by (auto intro: pd_sd pair_sd.divide)
  qed

  private lemma subdivision_pair_conv:
    "pair_sd G H = subdivision_pair G H "
    by (metis subdivision_with_projD subdivision_with_projI)

  lemmas subdivision_pair_induct = pair_sd.induct[
      unfolded subdivision_pair_conv, case_names base divide, induct pred: pair_sd]

  lemmas subdivision_pair_base = pair_sd.base[unfolded subdivision_pair_conv]
  lemmas subdivision_pair_divide = pair_sd.divide[unfolded subdivision_pair_conv]

  lemmas subdivision_pair_intros = pair_sd.intros[unfolded subdivision_pair_conv]
  lemmas subdivision_pair_cases = pair_sd.cases[unfolded subdivision_pair_conv]

  lemmas subdivision_pair_simps = pair_sd.simps[unfolded subdivision_pair_conv]

  lemmas bidirected_digraphI_subdivision = bidirected_digraphI_pair_sd[unfolded subdivision_pair_conv]

end

lemma (in pair_graph) pair_graph_subdivision:
  assumes "subdivision_pair G H"
  shows "pair_graph H"
  using assms
by (induct rule: subdivision_pair_induct) (blast intro: pair_graph.pair_graph_subdivide divide)+


end