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