Theory Graph_Theory.Kuratowski
theory Kuratowski
imports
Arc_Walk
Digraph_Component
Subdivision
"HOL-Library.Rewrite"
begin
section ‹Kuratowski Subgraphs›
text ‹
We consider the underlying undirected graphs. The underlying undirected graph is represented as a
symmetric digraph.
›
subsection ‹Public definitions›
definition complete_digraph :: "nat ⇒ ('a,'b) pre_digraph ⇒ bool" ("K⇘_⇙") where
"complete_digraph n G ≡ graph G ∧ card (verts G) = n ∧ arcs_ends G = {(u,v). (u,v) ∈ verts G × verts G ∧ u ≠ v}"
definition complete_bipartite_digraph :: "nat ⇒ nat ⇒ ('a, 'b) pre_digraph ⇒ bool" ("K⇘_,_⇙") where
"complete_bipartite_digraph m n G ≡ graph G ∧ (∃U V. verts G = U ∪ V ∧ U ∩ V = {}
∧ card U = m ∧ card V = n ∧ arcs_ends G = U × V ∪ V × U)"
definition kuratowski_planar :: "('a,'b) pre_digraph ⇒ bool" where
"kuratowski_planar G ≡ ¬(∃H. subgraph H G ∧ (∃K rev_K rev_H. subdivision (K, rev_K) (H, rev_H) ∧ (K⇘3,3⇙ K ∨ K⇘5⇙ K)))"
lemma complete_digraph_pair_def: "K⇘n⇙ (with_proj G)
⟷ finite (pverts G) ∧ card (pverts G) = n ∧ parcs G = {(u,v). (u,v) ∈ (pverts G × pverts G) ∧ u ≠ v}" (is "_ = ?R")
proof
assume A: "K⇘n⇙ G"
then interpret graph "with_proj G" by (simp add: complete_digraph_def)
show ?R using A finite_verts by (auto simp: complete_digraph_def)
next
assume A: ?R
moreover
then have "finite (pverts G × pverts G)" "parcs G ⊆ pverts G × pverts G"
by auto
then have "finite (parcs G)" by (rule rev_finite_subset)
ultimately interpret pair_graph G
by unfold_locales (auto simp: symmetric_def split: prod.splits intro: symI)
show "K⇘n⇙ G" using A finite_verts by (auto simp: complete_digraph_def)
qed
lemma complete_bipartite_digraph_pair_def: "K⇘m,n⇙ (with_proj G) ⟷ finite (pverts G)
∧ (∃U V. pverts G = U ∪ V ∧ U ∩ V = {} ∧ card U = m ∧ card V = n ∧ parcs G = U × V ∪ V × U)" (is "_ = ?R")
proof
assume A: "K⇘m,n⇙ G"
then interpret graph G by (simp add: complete_bipartite_digraph_def)
show ?R using A finite_verts by (auto simp: complete_bipartite_digraph_def)
next
assume A: ?R
then interpret pair_graph G
by unfold_locales (fastforce simp: complete_bipartite_digraph_def symmetric_def split: prod.splits intro: symI)+
show "K⇘m,n⇙ G" using A by (auto simp: complete_bipartite_digraph_def)
qed
lemma pair_graphI_complete:
assumes "K⇘n⇙ (with_proj G)"
shows "pair_graph G"
proof -
from assms interpret graph "with_proj G" by (simp add: complete_digraph_def)
show "pair_graph G"
using finite_arcs finite_verts sym_arcs wellformed no_loops by unfold_locales simp_all
qed
lemma pair_graphI_complete_bipartite:
assumes "K⇘m,n⇙ (with_proj G)"
shows "pair_graph G"
proof -
from assms interpret graph "with_proj G" by (simp add: complete_bipartite_digraph_def)
show "pair_graph G"
using finite_arcs finite_verts sym_arcs wellformed no_loops by unfold_locales simp_all
qed
subsection ‹Inner vertices of a walk›
context pre_digraph begin
definition (in pre_digraph) inner_verts :: "'b awalk ⇒ 'a list" where
"inner_verts p ≡ tl (map (tail G) p)"
lemma inner_verts_Nil[simp]: "inner_verts [] = []" by (auto simp: inner_verts_def)
lemma inner_verts_singleton[simp]: "inner_verts [x] = []" by (auto simp: inner_verts_def)
lemma (in wf_digraph) inner_verts_Cons:
assumes "awalk u (e # es) v"
shows "inner_verts (e # es) = (if es ≠ [] then head G e # inner_verts es else [])"
using assms by (induct es) (auto simp: inner_verts_def)
lemma (in - ) inner_verts_with_proj_def:
"pre_digraph.inner_verts (with_proj G) p = tl (map fst p)"
unfolding pre_digraph.inner_verts_def by simp
lemma inner_verts_conv: "inner_verts p = butlast (tl (awalk_verts u p))"
unfolding inner_verts_def awalk_verts_conv by simp
lemma (in pre_digraph) inner_verts_empty[simp]:
assumes "length p < 2" shows "inner_verts p = []"
using assms by (cases p) (auto simp: inner_verts_def)
lemma (in wf_digraph) set_inner_verts:
assumes "apath u p v"
shows "set (inner_verts p) = set (awalk_verts u p) - {u,v}"
proof (cases "length p < 2")
case True with assms show ?thesis
by (cases p) (auto simp: inner_verts_conv[of _ u] apath_def)
next
case False
have "awalk_verts u p = u # inner_verts p @ [v]"
using assms False length_awalk_verts[of u p] inner_verts_conv[of p u]
by (cases "awalk_verts u p") (auto simp: apath_def awalk_conv)
then show ?thesis using assms by (auto simp: apath_def)
qed
lemma in_set_inner_verts_appendI_l:
assumes "u ∈ set (inner_verts p)"
shows "u ∈ set (inner_verts (p @ q))"
using assms
by (induct p) (auto simp: inner_verts_def)
lemma in_set_inner_verts_appendI_r:
assumes "u ∈ set (inner_verts q)"
shows "u ∈ set (inner_verts (p @ q))"
using assms
by (induct p) (auto simp: inner_verts_def dest: list_set_tl)
end
subsection ‹Progressing Walks›
text ‹
We call a walk \emph{progressing} if it does not contain the sequence
@{term "[(x,y), (y,x)]"}. This concept is relevant in particular
for @{term iapath}s: If all of the inner vertices have degree at
most 2 this implies that such a walk is a trail and even a path.
›
definition progressing :: "('a × 'a) awalk ⇒ bool" where
"progressing p ≡ ∀xs x y ys. p ≠ xs @ (x,y) # (y,x) # ys"
lemma progressing_Nil: "progressing []"
by (auto simp: progressing_def)
lemma progressing_single: "progressing [e]"
by (auto simp: progressing_def)
lemma progressing_ConsD:
assumes "progressing (e # es)" shows "progressing es"
using assms unfolding progressing_def by (metis (no_types) append_eq_Cons_conv)
lemma progressing_Cons:
"progressing (x # xs) ⟷ (xs = [] ∨ (xs ≠ [] ∧ ¬(fst x = snd (hd xs) ∧ snd x = fst (hd xs)) ∧ progressing xs))" (is "?L = ?R")
proof
assume ?L
show ?R
proof (cases xs)
case Nil then show ?thesis by auto
next
case (Cons x' xs')
then have "⋀u v. (x # x' # xs') ≠ [] @ (u,v) # (v,u) # xs'" using ‹?L› unfolding progressing_def by metis
then have "¬(fst x = snd x' ∧ snd x = fst x')" by (cases x) (cases x', auto)
with Cons show ?thesis using ‹?L› by (auto dest: progressing_ConsD)
qed
next
assume ?R then show ?L unfolding progressing_def
by (auto simp add: Cons_eq_append_conv)
qed
lemma progressing_Cons_Cons:
"progressing ((u,v) # (v,w) # es) ⟷ u ≠ w ∧ progressing ((v,w) # es)" (is "?L ⟷ ?R")
by (auto simp: progressing_Cons)
lemma progressing_appendD1:
assumes "progressing (p @ q)" shows "progressing p"
using assms unfolding progressing_def by (metis append_Cons append_assoc)
lemma progressing_appendD2:
assumes "progressing (p @ q)" shows "progressing q"
using assms unfolding progressing_def by (metis append_assoc)
lemma progressing_rev_path:
"progressing (rev_path p) = progressing p" (is "?L = ?R")
proof
assume ?L
show ?R unfolding progressing_def
proof (intro allI notI)
fix xs x y ys l1 l2 assume "p = xs @ (x,y) # (y,x) # ys"
then have "rev_path p = rev_path ys @ (x,y) # (y,x) # rev_path xs"
by simp
then show False using ‹?L› unfolding progressing_def by auto
qed
next
assume ?R
show ?L unfolding progressing_def
proof (intro allI notI)
fix xs x y ys l1 l2 assume "rev_path p = xs @ (x,y) # (y,x) # ys"
then have "rev_path (rev_path p) = rev_path ys @ (x,y) # (y,x) # rev_path xs"
by simp
then show False using ‹?R› unfolding progressing_def by auto
qed
qed
lemma progressing_append_iff:
shows "progressing (xs @ ys) ⟷ progressing xs ∧ progressing ys
∧ (xs ≠ [] ∧ ys ≠ [] ⟶ (fst (last xs) ≠ snd (hd ys) ∨ snd (last xs) ≠ fst (hd ys)))"
proof (induct ys arbitrary: xs)
case Nil then show ?case by (auto simp: progressing_Nil)
next
case (Cons y' ys')
let "_ = ?R" = ?case
have *: "xs ≠ [] ⟹ hd (rev_path xs) = prod.swap (last xs)" by (induct xs) auto
have "progressing (xs @ y' # ys') ⟷ progressing ((xs @ [y']) @ ys')"
by simp
also have "… ⟷ progressing (xs @ [y']) ∧ progressing ys' ∧ (ys' ≠ [] ⟶ (fst y' ≠ snd (hd ys') ∨ snd y' ≠ fst (hd ys')))"
by (subst Cons) simp
also have "… ⟷ ?R"
by (auto simp: progressing_Cons progressing_Nil progressing_rev_path[where p="xs @ _",symmetric] * progressing_rev_path prod.swap_def)
finally show ?case .
qed
subsection ‹Walks with Restricted Vertices›
definition verts3 :: "('a, 'b) pre_digraph ⇒ 'a set" where
"verts3 G ≡ {v ∈ verts G. 2 < in_degree G v}"
text ‹A path were only the end nodes may be in @{term V}›
definition (in pre_digraph) gen_iapath :: "'a set ⇒ 'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"gen_iapath V u p v ≡ u ∈ V ∧ v ∈ V ∧ apath u p v ∧ set (inner_verts p) ∩ V = {} ∧ p ≠ []"
abbreviation (in pre_digraph) (input) iapath :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"iapath u p v ≡ gen_iapath (verts3 G) u p v"
definition gen_contr_graph :: "('a,'b) pre_digraph ⇒ 'a set ⇒ 'a pair_pre_digraph" where
"gen_contr_graph G V ≡ ⦇
pverts = V,
parcs = {(u,v). ∃p. pre_digraph.gen_iapath G V u p v}
⦈"
abbreviation (input) contr_graph :: "'a pair_pre_digraph ⇒ 'a pair_pre_digraph" where
"contr_graph G ≡ gen_contr_graph G (verts3 G)"
subsection ‹Properties of subdivisions›
lemma (in pair_sym_digraph) verts3_subdivide:
assumes "e ∈ parcs G" "w ∉ pverts G"
shows"verts3 (subdivide G e w) = verts3 G"
proof -
let ?sG = "subdivide G e w"
obtain u v where e_conv[simp]: "e = (u,v)" by (cases e) auto
from ‹w ∉ pverts G›
have w_arcs: "(u,w) ∉ parcs G" "(v,w) ∉ parcs G" "(w,u) ∉ parcs G" "(w,v) ∉ parcs G"
by (auto dest: wellformed)
have G_arcs: "(u,v) ∈ parcs G" "(v,u) ∈ parcs G"
using ‹e ∈ parcs G› by (auto simp: arcs_symmetric)
have "{v ∈ pverts G. 2 < in_degree G v} = {v ∈ pverts G. 2 < in_degree ?sG v}"
proof -
{ fix x assume "x ∈ pverts G"
define card_eq where "card_eq x ⟷ in_degree ?sG x = in_degree G x" for x
have "in_arcs ?sG u = (in_arcs G u - {(v,u)}) ∪ {(w,u)}"
"in_arcs ?sG v = (in_arcs G v - {(u,v)}) ∪ {(w,v)}"
using w_arcs G_arcs by auto
then have "card_eq u" "card_eq v"
unfolding card_eq_def in_degree_def using w_arcs G_arcs
apply -
apply (cases "finite (in_arcs G u)"; simp add: card_Suc_Diff1 del: card_Diff_insert)
apply (cases "finite (in_arcs G v)"; simp add: card_Suc_Diff1 del: card_Diff_insert)
done
moreover
have "x ∉ {u,v} ⟹ in_arcs ?sG x = in_arcs G x"
using ‹x ∈ pverts G› ‹w ∉ pverts G› by auto
then have "x ∉ {u,v} ⟹ card_eq x" by (simp add: in_degree_def card_eq_def)
ultimately have "card_eq x" by fast
then have "in_degree G x = in_degree ?sG x"
unfolding card_eq_def by simp }
then show ?thesis by auto
qed
also have "… = {v∈pverts ?sG. 2 < in_degree ?sG v}"
proof -
have "in_degree ?sG w ≤ 2"
proof -
have "in_arcs ?sG w = {(u,w), (v,w)}"
using ‹w ∉ pverts G› G_arcs(1) by (auto simp: wellformed')
then show ?thesis
unfolding in_degree_def by (auto simp: card_insert_if)
qed
then show ?thesis using G_arcs assms by auto
qed
finally show ?thesis by (simp add: verts3_def)
qed
lemma sd_path_Nil_iff:
"sd_path e w p = [] ⟷ p = []"
by (cases "(e,w,p)" rule: sd_path.cases) auto
lemma (in pair_sym_digraph) gen_iapath_sd_path:
fixes e :: "'a × 'a" and w :: 'a
assumes elems: "e ∈ parcs G" "w ∉ pverts G"
assumes V: "V ⊆ pverts G"
assumes path: "gen_iapath V u p v"
shows "pre_digraph.gen_iapath (subdivide G e w) V u (sd_path e w p) v"
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 by (auto intro: pair_sym_digraph_subdivide)
from path have "apath u p v" by (auto simp: gen_iapath_def)
then have apath_sd: "S.apath u (sd_path e w p) v" and
set_ev_sd: "set (S.awalk_verts u (sd_path e w p)) ⊆ set (awalk_verts u p) ∪ {w}"
using elems by (rule apath_sd_path set_awalk_verts_sd_path)+
have "w ∉ {u,v}" using elems ‹apath u p v›
by (auto simp: apath_def awalk_hd_in_verts awalk_last_in_verts)
have "set (S.inner_verts (sd_path e w p)) = set (S.awalk_verts u (sd_path e w p)) - {u,v}"
using apath_sd by (rule S.set_inner_verts)
also have "… ⊆ set (awalk_verts u p) ∪ {w} - {u,v}"
using set_ev_sd by auto
also have "… = set (inner_verts p) ∪ {w}"
using set_inner_verts[OF ‹apath u p v›] ‹w ∉ {u,v}› by blast
finally have "set (S.inner_verts (sd_path e w p)) ∩ V ⊆ (set (inner_verts p) ∪ {w}) ∩ V"
using V by blast
also have "… ⊆ {}"
using path elems V unfolding gen_iapath_def by auto
finally show ?thesis
using apath_sd elems path by (auto simp: gen_iapath_def S.gen_iapath_def sd_path_Nil_iff)
qed
lemma (in pair_sym_digraph)
assumes elems: "e ∈ parcs G" "w ∉ pverts G"
assumes V: "V ⊆ pverts G"
assumes path: "pre_digraph.gen_iapath (subdivide G e w) V u p v"
shows gen_iapath_co_path: "gen_iapath V 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 -
interpret S: pair_sym_digraph "subdivide G e w"
using elems by (rule pair_sym_digraph_subdivide)
have uv: "u ∈ pverts G" "v ∈ pverts G" "S.apath u p v" using V path by (auto simp: S.gen_iapath_def)
note co = apath_co_path[OF elems uv] set_awalk_verts_co_path[OF elems uv]
show ?thesis_set by (fact co)
show ?thesis_path using co path unfolding gen_iapath_def S.gen_iapath_def using elems
by (clarsimp simp add: set_inner_verts[of u] S.set_inner_verts[of u]) blast
qed
subsection ‹Pair Graphs›
context pair_sym_digraph begin
lemma gen_iapath_rev_path:
"gen_iapath V v (rev_path p) u = gen_iapath V u p v" (is "?L = ?R")
proof -
{ fix u p v assume "gen_iapath V u p v"
then have "butlast (tl (awalk_verts v (rev_path p))) = rev (butlast (tl (awalk_verts u p)))"
by (auto simp: tl_rev butlast_rev butlast_tl awalk_verts_rev_path gen_iapath_def apath_def)
with ‹gen_iapath V u p v› have "gen_iapath V v (rev_path p) u"
by (auto simp: gen_iapath_def apath_def inner_verts_conv[symmetric] awalk_verts_rev_path) }
note RL = this
show ?thesis by (auto dest: RL intro: RL)
qed
lemma inner_verts_rev_path:
assumes "awalk u p v"
shows "inner_verts (rev_path p) = rev (inner_verts p)"
by (metis assms butlast_rev butlast_tl awalk_verts_rev_path inner_verts_conv tl_rev)
end
context pair_pseudo_graph begin
lemma apath_imp_progressing:
assumes "apath u p v" shows "progressing p"
proof (rule ccontr)
assume "¬?thesis"
then obtain xs x y ys where *: "p = xs @ (x,y) # (y,x) # ys"
unfolding progressing_def by auto
then have "¬apath u p v"
by (simp add: apath_append_iff apath_simps hd_in_awalk_verts)
then show False using assms by auto
qed
lemma awalk_Cons_deg2_unique:
assumes "awalk u p v" "p ≠ []"
assumes "in_degree G u ≤ 2"
assumes "awalk u1 (e1 # p) v" "awalk u2 (e2 # p) v"
assumes "progressing (e1 # p)" "progressing (e2 # p)"
shows "e1 = e2"
proof (cases p)
case (Cons e es)
show ?thesis
proof (rule ccontr)
assume "e1 ≠ e2"
define x where "x = snd e"
then have e_unf:"e = (u,x)" using ‹awalk u p v› Cons by (auto simp: awalk_simps)
then have ei_unf: "e1 = (u1, u)" "e2 = (u2, u)"
using Cons assms by (auto simp: apath_simps prod_eqI)
with Cons assms ‹e = (u,x)› ‹e1 ≠ e2› have "u1 ≠ u2" "x ≠ u1" "x ≠ u2"
by (auto simp: progressing_Cons_Cons)
moreover have "{(u1, u), (u2, u), (x,u)} ⊆ parcs G"
using e_unf ei_unf Cons assms by (auto simp: awalk_simps intro: arcs_symmetric)
then have "finite (in_arcs G u)"
and "{(u1, u), (u2, u), (x,u)} ⊆ in_arcs G u" by auto
then have "card ({(u1, u), (u2, u), (x,u)}) ≤ in_degree G u"
unfolding in_degree_def by (rule card_mono)
ultimately show "False" using ‹in_degree G u ≤ 2› by auto
qed
qed (simp add: ‹p ≠ []›)
lemma same_awalk_by_same_end:
assumes V: "verts3 G ⊆ V" "V ⊆ pverts G"
and walk: "awalk u p v" "awalk u q w" "hd p = hd q" "p ≠ []" "q ≠ []"
and progress: "progressing p" "progressing q"
and tail: "v ∈ V" "w ∈ V"
and inner_verts: "set (inner_verts p) ∩ V = {}"
"set (inner_verts q) ∩ V = {}"
shows "p = q"
using walk progress inner_verts
proof (induct p q arbitrary: u rule: list_induct2'[case_names Nil_Nil Cons_Nil Nil_Cons Cons_Cons])
case (Cons_Cons a as b bs)
from ‹hd (a # _) = hd _› have "a = b" by simp
{ fix a as v b bs w
assume A: "awalk u (a # as) v" "awalk u (b # bs) w"
"set (inner_verts (b # bs)) ∩ V = {}" "v ∈ V" "a = b" "as = []"
then have "bs = []" by - (rule ccontr, auto simp: inner_verts_Cons awalk_simps)
} note Nil_imp_Nil = this
show ?case
proof (cases "as = []")
case True
then have "bs = []" using Cons_Cons.prems ‹a = b› tail by (metis Nil_imp_Nil)
then show ?thesis using True ‹a = b› by simp
next
case False
then have "bs ≠ []" using Cons_Cons.prems ‹a = b› tail by (metis Nil_imp_Nil)
obtain a' as' where "as = a' # as'" using ‹as ≠ []› by (cases as) simp
obtain b' bs' where "bs = b' # bs'" using ‹bs ≠ []› by (cases bs) simp
let ?arcs = "{(fst a, snd a), (snd a', snd a), (snd b', snd a)}"
have "card {fst a, snd a', snd b'} = card (fst ` ?arcs)" by auto
also have "… = card ?arcs" by (rule card_image) (cases a, auto)
also have "… ≤ in_degree G (snd a)"
proof -
have "?arcs ⊆ in_arcs G (snd a)"
using ‹progressing (a # as)› ‹progressing (b # bs)› ‹awalk _ (a # as) _› ‹awalk _ (b # bs) _›
unfolding ‹a = b› ‹as = _› ‹bs = _›
by (cases b; cases a') (auto simp: progressing_Cons_Cons awalk_simps intro: arcs_symmetric)
with _show ?thesis unfolding in_degree_def by (rule card_mono) auto
qed
also have "… ≤ 2"
proof -
have "snd a ∉ V" "snd a ∈ pverts G"
using Cons_Cons.prems ‹as ≠ []› by (auto simp: inner_verts_Cons)
then show ?thesis using V by (auto simp: verts3_def)
qed
finally have "fst a = snd a' ∨ fst a = snd b' ∨ snd a' = snd b'"
by (auto simp: card_insert_if split: if_splits)
then have "hd as = hd bs"
using ‹progressing (a # as)› ‹progressing (b # bs)› ‹awalk _ (a # as) _› ‹awalk _ (b # bs) _›
unfolding ‹a = b› ‹as = _› ‹bs = _›
by (cases b, cases a', cases b') (auto simp: progressing_Cons_Cons awalk_simps)
then show ?thesis
using ‹as ≠ []› ‹bs ≠ []› Cons_Cons.prems
by (auto dest: progressing_ConsD simp: awalk_simps inner_verts_Cons intro!: Cons_Cons)
qed
qed simp_all
lemma same_awalk_by_common_arc:
assumes V: "verts3 G ⊆ V" "V ⊆ pverts G"
assumes walk: "awalk u p v" "awalk w q x"
assumes progress: "progressing p" "progressing q"
assumes iv_not_in_V: "set (inner_verts p) ∩ V = {}" "set (inner_verts q) ∩ V = {}"
assumes ends_in_V: "{u,v,w,x} ⊆ V"
assumes arcs: "e ∈ set p" "e ∈ set q"
shows "p = q"
proof -
from arcs obtain p1 p2 where p_decomp: "p = p1 @ e # p2" by (metis in_set_conv_decomp_first)
from arcs obtain q1 q2 where q_decomp: "q = q1 @ e # q2" by (metis in_set_conv_decomp_first)
{ define p1' q1' where "p1' = rev_path (p1 @ [e])" and "q1' = rev_path (q1 @ [e])"
then have decomp: "p = rev_path p1' @ p2" "q = rev_path q1' @ q2"
and "awlast u (rev_path p1') = snd e" "awlast w (rev_path q1') = snd e"
using p_decomp q_decomp walk by (auto simp: awlast_append awalk_verts_rev_path)
then have walk': "awalk (snd e) p1' u" "awalk (snd e) q1' w"
using walk by auto
moreover have "hd p1' = hd q1'" "p1' ≠ []" "q1' ≠ []" by (auto simp: p1'_def q1'_def)
moreover have "progressing p1'" "progressing q1'"
using progress unfolding decomp by (auto dest: progressing_appendD1 simp: progressing_rev_path)
moreover
have "set (inner_verts (rev_path p1')) ∩ V = {}" "set (inner_verts (rev_path q1')) ∩ V = {}"
using iv_not_in_V unfolding decomp
by (auto intro: in_set_inner_verts_appendI_l in_set_inner_verts_appendI_r)
then have "u ∈ V" "w ∈ V" "set (inner_verts p1') ∩ V = {}" "set (inner_verts q1') ∩ V = {}"
using ends_in_V iv_not_in_V walk unfolding decomp
by (auto simp: inner_verts_rev_path)
ultimately have "p1' = q1'" by (rule same_awalk_by_same_end[OF V]) }
moreover
{ define p2' q2' where "p2' = e # p2" and "q2' = e # q2"
then have decomp: "p = p1 @ p2'" "q = q1 @ q2'"
using p_decomp q_decomp by (auto simp: awlast_append)
moreover
have "awlast u p1 = fst e" "awlast w q1 = fst e"
using p_decomp q_decomp walk by auto
ultimately
have *: "awalk (fst e) p2' v" "awalk (fst e) q2' x"
using walk by auto
moreover have "hd p2' = hd q2'" "p2' ≠ []" "q2' ≠ []" by (auto simp: p2'_def q2'_def)
moreover have "progressing p2'" "progressing q2'"
using progress unfolding decomp by (auto dest: progressing_appendD2)
moreover
have "v ∈ V" "x ∈ V" "set (inner_verts p2') ∩ V = {}" "set (inner_verts q2') ∩ V = {}"
using ends_in_V iv_not_in_V unfolding decomp
by (auto intro: in_set_inner_verts_appendI_l in_set_inner_verts_appendI_r)
ultimately have "p2' = q2'" by (rule same_awalk_by_same_end[OF V]) }
ultimately
show "p = q" using p_decomp q_decomp by (auto simp: rev_path_eq)
qed
lemma same_gen_iapath_by_common_arc:
assumes V: "verts3 G ⊆ V" "V ⊆ pverts G"
assumes path: "gen_iapath V u p v" "gen_iapath V w q x"
assumes arcs: "e ∈ set p" "e ∈ set q"
shows "p = q"
proof -
from path have awalk: "awalk u p v" "awalk w q x" "progressing p" "progressing q"
and in_V: "set (inner_verts p) ∩ V = {}" "set (inner_verts q) ∩ V = {}" "{u,v,w,x} ⊆ V"
by (auto simp: gen_iapath_def apath_imp_progressing apath_def)
from V awalk in_V arcs show ?thesis by (rule same_awalk_by_common_arc)
qed
end
subsection ‹Slim graphs›
text ‹
We define the notion of a slim graph. The idea is that for a slim graph @{term G}, @{term G}
is a subdivision of @{term "contr_graph G"}.
›
context pair_pre_digraph begin
definition (in pair_pre_digraph) is_slim :: "'a set ⇒ bool" where
"is_slim V ≡
(∀v ∈ pverts G. v ∈ V ∨
in_degree G v ≤ 2 ∧ (∃x p y. gen_iapath V x p y ∧ v ∈ set (awalk_verts x p))) ∧
(∀e ∈ parcs G. fst e ≠ snd e ∧ (∃x p y. gen_iapath V x p y ∧ e ∈ set p)) ∧
(∀u v p q. (gen_iapath V u p v ∧ gen_iapath V u q v) ⟶ p = q) ∧
V ⊆ pverts G"
definition direct_arc :: "'a × 'a ⇒ 'a × 'a" where
"direct_arc uv ≡ SOME e. {fst uv , snd uv} = {fst e, snd e}"
definition choose_iapath :: "'a ⇒ 'a ⇒ ('a × 'a) awalk" where
"choose_iapath u v ≡ (let
chosen_path = (λu v. SOME p. iapath u p v)
in if direct_arc (u,v) = (u,v) then chosen_path u v else rev_path (chosen_path v u))"
definition slim_paths :: "('a × ('a × 'a) awalk × 'a) set" where
"slim_paths ≡ (λe. (fst e, choose_iapath (fst e) (snd e), snd e)) ` parcs (contr_graph G)"
definition slim_verts :: "'a set" where
"slim_verts ≡ verts3 G ∪ (⋃(u,p,_) ∈ slim_paths. set (awalk_verts u p))"
definition slim_arcs :: "'a rel" where
"slim_arcs ≡ ⋃(_,p,_) ∈ slim_paths. set p"
text ‹Computes a slim subgraph for an arbitrary @{term pair_digraph}›
definition slim :: "'a pair_pre_digraph" where
"slim ≡ ⦇ pverts = slim_verts, parcs = slim_arcs ⦈"
end
lemma (in wf_digraph) iapath_dist_ends: "⋀u p v. iapath u p v ⟹ u ≠ v"
unfolding pre_digraph.gen_iapath_def by (metis apath_ends)
context pair_sym_digraph begin
lemma choose_iapath:
assumes "∃p. iapath u p v"
shows "iapath u (choose_iapath u v) v"
proof (cases "direct_arc (u,v) = (u,v)")
define chosen where "chosen u v = (SOME p. iapath u p v)" for u v
{ case True
have "iapath u (chosen u v) v"
unfolding chosen_def by (rule someI_ex) (rule assms)
then show ?thesis using True by (simp add: choose_iapath_def chosen_def) }
{ case False
from assms obtain p where "iapath u p v" by auto
then have "iapath v (rev_path p) u"
by (simp add: gen_iapath_rev_path)
then have "iapath v (chosen v u) u"
unfolding chosen_def by (rule someI)
then show ?thesis using False
by (simp add: choose_iapath_def chosen_def gen_iapath_rev_path) }
qed
lemma slim_simps: "pverts slim = slim_verts" "parcs slim = slim_arcs"
by (auto simp: slim_def)
lemma slim_paths_in_G_E:
assumes "(u,p,v) ∈ slim_paths" obtains "iapath u p v" "u ≠ v"
using assms choose_iapath
by (fastforce simp: gen_contr_graph_def slim_paths_def dest: iapath_dist_ends)
lemma verts_slim_in_G: "pverts slim ⊆ pverts G"
by (auto simp: slim_simps slim_verts_def verts3_def gen_iapath_def apath_def
elim!: slim_paths_in_G_E elim!: awalkE)
lemma verts3_in_slim_G[simp]:
assumes "x ∈ verts3 G" shows "x ∈ pverts slim"
using assms by (auto simp: slim_simps slim_verts_def)
lemma arcs_slim_in_G: "parcs slim ⊆ parcs G"
by (auto simp: slim_simps slim_arcs_def gen_iapath_def apath_def
elim!: slim_paths_in_G_E elim!: awalkE)
lemma slim_paths_in_slimG:
assumes "(u,p,v) ∈ slim_paths"
shows "pre_digraph.gen_iapath slim (verts3 G) u p v ∧ p ≠ []"
proof -
from assms have arcs: "⋀e. e ∈ set p ⟹ e ∈ parcs slim"
by (auto simp: slim_simps slim_arcs_def)
moreover
from assms have "gen_iapath (verts3 G) u p v" and "p ≠ []"
by (auto simp: gen_iapath_def elim!: slim_paths_in_G_E)
ultimately show ?thesis
by (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def pre_digraph.awalk_def
inner_verts_with_proj_def)
qed
lemma direct_arc_swapped:
"direct_arc (u,v) = direct_arc (v,u)"
by (simp add: direct_arc_def insert_commute)
lemma direct_arc_chooses:
fixes u v :: 'a shows "direct_arc (u,v) = (u,v) ∨ direct_arc (u,v) = (v,u)"
proof -
define f :: "'a set ⇒ 'a × 'a"
where "f X = (SOME e. X = {fst e,snd e})" for X
have "∃p::'a × 'a. {u,v} = {fst p, snd p}" by (rule exI[where x="(u,v)"]) auto
then have "{u,v} = {fst (f {u,v}), snd (f {u,v})}"
unfolding f_def by (rule someI_ex)
then have "f {u,v} = (u,v) ∨ f {u,v} = (v,u)"
by (auto simp: doubleton_eq_iff prod_eq_iff)
then show ?thesis by (auto simp: direct_arc_def f_def)
qed
lemma rev_path_choose_iapath:
assumes "u ≠ v"
shows "rev_path (choose_iapath u v) = choose_iapath v u"
using assms direct_arc_chooses[of u v]
by (auto simp: choose_iapath_def direct_arc_swapped)
lemma no_loops_in_iapath: "gen_iapath V u p v ⟹ a ∈ set p ⟹ fst a ≠ snd a"
by (auto simp: gen_iapath_def no_loops_in_apath)
lemma pair_bidirected_digraph_slim: "pair_bidirected_digraph slim"
proof
fix e assume A: "e ∈ parcs slim"
then obtain u p v where "(u,p,v) ∈ slim_paths" "e ∈ set p" by (auto simp: slim_simps slim_arcs_def)
with A have "iapath u p v" by (auto elim: slim_paths_in_G_E)
with ‹e ∈ set p› have "fst e ∈ set (awalk_verts u p)" "snd e ∈ set (awalk_verts u p)"
by (auto simp: set_awalk_verts gen_iapath_def apath_def)
moreover
from ‹_ ∈ slim_paths› have "set (awalk_verts u p) ⊆ pverts slim"
by (auto simp: slim_simps slim_verts_def)
ultimately
show "fst e ∈ pverts slim" "snd e ∈ pverts slim" by auto
show "fst e ≠ snd e"
using ‹iapath u p v› ‹e ∈ set p › by (auto dest: no_loops_in_iapath)
next
{ fix e assume "e ∈ parcs slim"
then obtain u p v where "(u,p,v) ∈ slim_paths" and "e ∈ set p"
by (auto simp: slim_simps slim_arcs_def)
moreover
then have "iapath u p v" and "p ≠ []" and "u ≠ v" by (auto elim: slim_paths_in_G_E)
then have "iapath v (rev_path p) u" and "rev_path p ≠ []" and "v ≠ u"
by (auto simp: gen_iapath_rev_path)
then have "(v,u) ∈ parcs (contr_graph G)"
by (auto simp: gen_contr_graph_def)
moreover
from ‹iapath u p v› have "u ≠ v"
by (auto simp: gen_iapath_def dest: apath_nonempty_ends)
ultimately
have "(v, rev_path p, u) ∈ slim_paths"
by (auto simp: slim_paths_def rev_path_choose_iapath intro: rev_image_eqI)
moreover
from ‹e ∈ set p› have "(snd e, fst e) ∈ set (rev_path p)"
by (induct p) auto
ultimately have "(snd e, fst e) ∈ parcs slim"
by (auto simp: slim_simps slim_arcs_def) }
then show "symmetric slim"
unfolding symmetric_conv by simp (metis fst_conv snd_conv)
qed
lemma (in pair_pseudo_graph) pair_graph_slim: "pair_graph slim"
proof -
interpret slim: pair_bidirected_digraph slim by (rule pair_bidirected_digraph_slim)
show ?thesis
proof
show "finite (pverts slim)"
using verts_slim_in_G finite_verts by (rule finite_subset)
show "finite (parcs slim)"
using arcs_slim_in_G finite_arcs by (rule finite_subset)
qed
qed
lemma subgraph_slim: "subgraph slim G"
proof (rule subgraphI)
interpret H: pair_bidirected_digraph "slim"
by (rule pair_bidirected_digraph_slim) intro_locales
show "verts slim ⊆ verts G" "arcs slim ⊆ arcs G"
by (auto simp: verts_slim_in_G arcs_slim_in_G)
show "compatible G slim" ..
show "wf_digraph slim" "wf_digraph G"
by unfold_locales
qed
lemma giapath_if_slim_giapath:
assumes "pre_digraph.gen_iapath slim (verts3 G) u p v"
shows "gen_iapath (verts3 G) u p v"
using assms verts_slim_in_G arcs_slim_in_G
by (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def pre_digraph.awalk_def
inner_verts_with_proj_def)
lemma slim_giapath_if_giapath:
assumes "gen_iapath (verts3 G) u p v"
shows "∃p. pre_digraph.gen_iapath slim (verts3 G) u p v" (is "∃p. ?P p")
proof
from assms have choose_arcs: "⋀e. e ∈ set (choose_iapath u v) ⟹ e ∈ parcs slim"
by (fastforce simp: slim_simps slim_arcs_def slim_paths_def gen_contr_graph_def)
moreover
from assms have choose: "iapath u (choose_iapath u v) v"
by (intro choose_iapath) (auto simp: gen_iapath_def)
ultimately show "?P (choose_iapath u v)"
by (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def pre_digraph.awalk_def
inner_verts_with_proj_def)
qed
lemma contr_graph_slim_eq:
"gen_contr_graph slim (verts3 G) = contr_graph G"
using giapath_if_slim_giapath slim_giapath_if_giapath by (fastforce simp: gen_contr_graph_def)
end
context pair_pseudo_graph begin
lemma verts3_slim_in_verts3:
assumes "v ∈ verts3 slim" shows "v ∈ verts3 G"
proof -
from assms have "2 < in_degree slim v" by (auto simp: verts3_def)
also have "… ≤ in_degree G v" using subgraph_slim by (rule subgraph_in_degree)
finally show ?thesis using assms subgraph_slim by (fastforce simp: verts3_def)
qed
lemma slim_is_slim:
"pair_pre_digraph.is_slim slim (verts3 G)"
proof (unfold pair_pre_digraph.is_slim_def, safe)
interpret S: pair_graph slim by (rule pair_graph_slim)
{ fix v assume "v ∈ pverts slim" "v ∉ verts3 G"
then have "in_degree G v ≤ 2"
using verts_slim_in_G by (auto simp: verts3_def)
then show "in_degree slim v ≤ 2"
using subgraph_in_degree[OF subgraph_slim, of v] by fastforce
next
fix w assume "w ∈ pverts slim" "w ∉ verts3 G"
then obtain u p v where upv: "(u, p, v) ∈ slim_paths" "w ∈ set (awalk_verts u p)"
by (auto simp: slim_simps slim_verts_def)
moreover
then have "S.gen_iapath (verts3 G) u p v"
using slim_paths_in_slimG by auto
ultimately
show "∃x q y. S.gen_iapath (verts3 G) x q y
∧ w ∈ set (awalk_verts x q)"
by auto
next
fix u v assume "(u,v) ∈ parcs slim"
then obtain x p y where "(x, p, y) ∈ slim_paths" "(u,v) ∈ set p"
by (auto simp: slim_simps slim_arcs_def)
then have "S.gen_iapath (verts3 G) x p y ∧ (u,v) ∈ set p"
using slim_paths_in_slimG by auto
then show "∃x p y. S.gen_iapath (verts3 G) x p y ∧ (u,v) ∈ set p"
by blast
next
fix u v assume "(u,v) ∈ parcs slim" "fst (u,v) = snd (u,v)"
then show False by (auto simp: S.no_loops')
next
fix u v p q
assume paths: "S.gen_iapath (verts3 G) u p v"
"S.gen_iapath (verts3 G) u q v"
have V: "verts3 slim ⊆ verts3 G" "verts3 G ⊆ pverts slim"
by (auto simp: verts3_slim_in_verts3)
have "p = [] ∨ q = [] ⟹ p = q" using paths
by (auto simp: S.gen_iapath_def dest: S.apath_ends)
moreover
{ assume "p ≠ []" "q ≠ []"
{ fix u p v assume "p ≠ []" and path: "S.gen_iapath (verts3 G) u p v"
then obtain e where "e ∈ set p" by (metis last_in_set)
then have "e ∈ parcs slim" using path by (auto simp: S.gen_iapath_def S.apath_def)
then obtain x r y where "(x,r,y) ∈ slim_paths" "e ∈ set r"
by (auto simp: slim_simps slim_arcs_def)
then have "S.gen_iapath (verts3 G) x r y" by (metis slim_paths_in_slimG)
with ‹e ∈ set r› ‹e ∈ set p› path have "p = r"
by (auto intro: S.same_gen_iapath_by_common_arc[OF V])
then have "x = u" "y = v" using path ‹S.gen_iapath (verts3 G) x r y› ‹p = r› ‹p ≠ []›
by (auto simp: S.gen_iapath_def S.apath_def dest: S.awalk_ends)
then have "(u,p,v) ∈ slim_paths" using ‹p = r› ‹(x,r,y) ∈ slim_paths› by simp }
note obt = this
from ‹p ≠ []› ‹q ≠ []› paths have "(u,p,v) ∈ slim_paths" "(u,q,v) ∈ slim_paths"
by (auto intro: obt)
then have "p = q" by (auto simp: slim_paths_def)
}
ultimately show "p = q" by metis
}
qed auto
end
context pair_sym_digraph begin
lemma
assumes p: "gen_iapath (pverts G) u p v"
shows gen_iapath_triv_path: "p = [(u,v)]"
and gen_iapath_triv_arc: "(u,v) ∈ parcs G"
proof -
have "set (inner_verts p) = {}"
proof -
have *: "⋀A B :: 'a set. ⟦A ⊆ B; A ∩ B = {}⟧ ⟹ A = {}" by blast
have "set (inner_verts p) = set (awalk_verts u p) - {u, v}"
using p by (simp add: set_inner_verts gen_iapath_def)
also have "… ⊆ pverts G"
using p unfolding gen_iapath_def apath_def awalk_conv by auto
finally show ?thesis
using p by (rule_tac *) (auto simp: gen_iapath_def)
qed
then have "inner_verts p = []" by simp
then show "p = [(u,v)]" using p
by (cases p) (auto simp: gen_iapath_def apath_def inner_verts_def split: if_split_asm)
then show "(u,v) ∈ parcs G"
using p by (auto simp: gen_iapath_def apath_def)
qed
lemma gen_contr_triv:
assumes "is_slim V" "pverts G = V" shows "gen_contr_graph G V = G"
proof -
let ?gcg = "gen_contr_graph G V"
from assms have "pverts ?gcg = pverts G"
by (auto simp: gen_contr_graph_def is_slim_def)
moreover
have "parcs ?gcg = parcs G"
proof (rule set_eqI, safe)
fix u v assume "(u,v) ∈ parcs ?gcg"
then obtain p where "gen_iapath V u p v"
by (auto simp: gen_contr_graph_def)
then show "(u,v) ∈ parcs G"
using gen_iapath_triv_arc ‹pverts G = V› by auto
next
fix u v assume "(u,v) ∈ parcs G"
with assms obtain x p y where path: "gen_iapath V x p y" "(u,v) ∈ set p" "u ≠ v"
by (auto simp: is_slim_def)
with ‹pverts G = V› have "p = [(x,y)]" by (intro gen_iapath_triv_path) auto
then show "(u,v) ∈ parcs ?gcg"
using path by (auto simp: gen_contr_graph_def)
qed
ultimately
show "?gcg = G" by auto
qed
lemma is_slim_no_loops:
assumes "is_slim V" "a ∈ arcs G" shows "fst a ≠ snd a"
using assms by (auto simp: is_slim_def)
end
subsection ‹Contraction Preserves Kuratowski-Subgraph-Property›
lemma (in pair_pseudo_graph) in_degree_contr:
assumes "v ∈ V" and V: "verts3 G ⊆ V" "V ⊆ verts G"
shows "in_degree (gen_contr_graph G V) v ≤ in_degree G v"
proof -
have fin: "finite {(u, p). gen_iapath V u p v}"
proof -
have "{(u, p). gen_iapath V u p v} ⊆ (λ(u,p,_). (u,p)) ` {(u,p,v). apath u p v}"
by (force simp: gen_iapath_def)
with apaths_finite_triple show ?thesis by (rule finite_surj)
qed
have io_snd: "inj_on snd {(u,p). gen_iapath V u p v}"
by (rule inj_onI) (auto simp: gen_iapath_def apath_def dest: awalk_ends)
have io_last: "inj_on last {p. ∃u. gen_iapath V u p v}"
proof (rule inj_onI, safe)
fix u1 u2 p1 p2
assume A: "last p1 = last p2" and B: "gen_iapath V u1 p1 v" "gen_iapath V u2 p2 v"
from B have "last p1 ∈ set p1" "last p2 ∈ set p2" by (auto simp: gen_iapath_def)
with A have "last p1 ∈ set p1" "last p1 ∈ set p2" by simp_all
with V[simplified] B show "p1 = p2" by (rule same_gen_iapath_by_common_arc)
qed
have "in_degree (gen_contr_graph G V) v = card ((λ(u,_). (u,v)) ` {(u,p). gen_iapath V u p v})"
proof -
have "in_arcs (gen_contr_graph G V) v = (λ(u,_). (u,v)) ` {(u,p). gen_iapath V u p v}"
by (auto simp: gen_contr_graph_def)
then show ?thesis unfolding in_degree_def by simp
qed
also have "… ≤ card {(u,p). gen_iapath V u p v}"
using fin by (rule card_image_le)
also have "… = card (snd ` {(u,p). gen_iapath V u p v})"
using io_snd by (rule card_image[symmetric])
also have "snd ` {(u,p). gen_iapath V u p v} = {p. ∃u. gen_iapath V u p v}"
by (auto intro: rev_image_eqI)
also have "card … = card (last ` ...)"
using io_last by (rule card_image[symmetric])
also have "… ≤ in_degree G v"
unfolding in_degree_def
proof (rule card_mono)
show "last ` {p. ∃u. gen_iapath V u p v} ⊆ in_arcs G v"
proof -
have "⋀u p. awalk u p v ⟹ p ≠ [] ⟹ last p ∈ parcs G"
by (auto simp: awalk_def)
moreover
{ fix u p assume "awalk u p v" "p ≠ []"
then have "snd (last p) = v" by (induct p arbitrary: u) (auto simp: awalk_simps) }
ultimately
show ?thesis unfolding in_arcs_def by (auto simp: gen_iapath_def apath_def)
qed
qed auto
finally show ?thesis .
qed
lemma (in pair_graph) contracted_no_degree2_simp:
assumes subd: "subdivision_pair G H"
assumes two_less_deg2: "verts3 G = pverts G"
shows "contr_graph H = G"
using subd
proof (induct rule: subdivision_pair_induct)
case base
{ fix e assume "e ∈ parcs G"
then have "gen_iapath (pverts G) (fst e) [(fst e, snd e)] (snd e)" "e ∈ set [(fst e, snd e)]"
using no_loops[of "(fst e, snd e)"] by (auto simp: gen_iapath_def apath_simps )
then have "∃u p v. gen_iapath (pverts G) u p v ∧ e ∈ set p" by blast }
moreover
{ fix u p v assume "gen_iapath (pverts G) u p v"
from ‹gen_iapath _ u p v› have "p = [(u,v)]"
unfolding gen_iapath_def apath_def
by safe (cases p, case_tac [2] list, auto simp: awalk_simps inner_verts_def) }
ultimately have "is_slim (verts3 G)" unfolding is_slim_def two_less_deg2
by (blast dest: no_loops_in_iapath)
then show ?case by (simp add: gen_contr_triv two_less_deg2)
next
case (divide e w H)
let ?sH = "subdivide H e w"
from ‹subdivision_pair G H› interpret H: pair_bidirected_digraph H
by (rule bidirected_digraphI_subdivision)
from divide(1,2) interpret S: pair_sym_digraph ?sH by (rule H.pair_sym_digraph_subdivide)
obtain u v where e_conv:"e = (u,v)" by (cases e) auto
have "contr_graph ?sH = contr_graph H"
proof -
have V_cond: "verts3 H ⊆ pverts H" by (auto simp: verts3_def)
have "verts3 H = verts3 ?sH"
using divide by (simp add: H.verts3_subdivide)
then have v: "pverts (contr_graph ?sH) = pverts (contr_graph H)"
by (auto simp: gen_contr_graph_def)
moreover
then have "parcs (contr_graph ?sH) = parcs (contr_graph H)"
unfolding gen_contr_graph_def
by (auto dest: H.gen_iapath_co_path[OF divide(1,2) V_cond]
H.gen_iapath_sd_path[OF divide(1,2) V_cond])
ultimately show ?thesis by auto
qed
then show ?case using divide by simp
qed
lemma verts3_K33:
assumes "K⇘3,3⇙ (with_proj G)"
shows "verts3 G = verts G"
proof -
{ fix v assume "v ∈ pverts G"
from assms obtain U V where cards: "card U = 3" "card V=3"
and UV: "U ∩ V = {}" "pverts G = U ∪ V" "parcs G = U × V ∪ V × U"
unfolding complete_bipartite_digraph_pair_def by blast
have "2 < in_degree G v"
proof (cases "v ∈ U")
case True
then have "in_arcs G v = V × {v}" using UV by fastforce
then show ?thesis using cards by (auto simp: card_cartesian_product in_degree_def)
next
case False
then have "in_arcs G v = U × {v}" using ‹v ∈ _› UV by fastforce
then show ?thesis using cards by (auto simp: card_cartesian_product in_degree_def)
qed }
then show ?thesis by (auto simp: verts3_def)
qed
lemma verts3_K5:
assumes "K⇘5⇙ (with_proj G)"
shows "verts3 G = verts G"
proof -
interpret pgG: pair_graph G using assms by (rule pair_graphI_complete)
{ fix v assume "v ∈ pverts G"
have "2 < (4 :: nat)" by simp
also have "4 = card (pverts G - {v})"
using assms ‹v ∈ pverts G› unfolding complete_digraph_def by auto
also have "pverts G - {v} = {u ∈ pverts G. u ≠ v}"
by auto
also have "card … = card ({u ∈ pverts G. u ≠ v} × {v})" (is "_ = card ?A")
by auto
also have "?A = in_arcs G v"
using assms ‹v ∈ pverts G› unfolding complete_digraph_def by safe auto
also have "card … = in_degree G v"
unfolding in_degree_def ..
finally have "2 < in_degree G v" . }
then show ?thesis unfolding verts3_def by auto
qed
lemma K33_contractedI:
assumes subd: "subdivision_pair G H"
assumes k33: "K⇘3,3⇙ G"
shows "K⇘3,3⇙ (contr_graph H)"
proof -
interpret pgG: pair_graph G using k33 by (rule pair_graphI_complete_bipartite)
show ?thesis
using assms by (auto simp: pgG.contracted_no_degree2_simp verts3_K33)
qed
lemma K5_contractedI:
assumes subd: "subdivision_pair G H"
assumes k5: "K⇘5⇙ G"
shows "K⇘5⇙ (contr_graph H)"
proof -
interpret pgG: pair_graph G using k5 by (rule pair_graphI_complete)
show ?thesis
using assms by (auto simp add: pgG.contracted_no_degree2_simp verts3_K5)
qed
subsection ‹Final proof›
context pair_sym_digraph begin
lemma gcg_subdivide_eq:
assumes mem: "e ∈ parcs G" "w ∉ pverts G"
assumes V: "V ⊆ pverts G"
shows "gen_contr_graph (subdivide G e w) V = gen_contr_graph G V"
proof -
interpret sdG: pair_sym_digraph "subdivide G e w"
using mem by (rule pair_sym_digraph_subdivide)
{ fix u p v assume "sdG.gen_iapath V u p v"
have "gen_iapath V u (co_path e w p) v"
using mem V ‹sdG.gen_iapath V u p v› by (rule gen_iapath_co_path)
then have "∃p. gen_iapath V u p v" ..
} note A = this
moreover
{ fix u p v assume "gen_iapath V u p v"
have "sdG.gen_iapath V u (sd_path e w p) v"
using mem V ‹gen_iapath V u p v› by (rule gen_iapath_sd_path)
then have "∃p. sdG.gen_iapath V u p v" ..
} note B = this
ultimately show ?thesis using assms by (auto simp: gen_contr_graph_def)
qed
lemma co_path_append:
assumes "[last p1, hd p2] ∉ {[(fst e,w),(w,snd e)], [(snd e,w),(w,fst e)]}"
shows "co_path e w (p1 @ p2) = co_path e w p1 @ co_path e w p2"
using assms
proof (induct p1 rule: co_path_induct)
case single then show ?case by (cases p2) auto
next
case (co e1 e2 es) then show ?case by (cases es) auto
next
case (corev e1 e2 es) then show ?case by (cases es) auto
qed auto
lemma exists_co_path_decomp1:
assumes mem: "e ∈ parcs G" "w ∉ pverts G"
assumes p: "pre_digraph.apath (subdivide G e w) u p v" "(fst e, w) ∈ set p" "w ≠ v"
shows "∃p1 p2. p = p1 @ (fst e, w) # (w, snd e) # p2"
proof -
let ?sdG = "subdivide G e w"
interpret sdG: pair_sym_digraph ?sdG
using mem by (rule pair_sym_digraph_subdivide)
obtain p1 p2 z where p_decomp: "p = p1 @ (fst e, w) # (w, z) # p2" "fst e ≠ z" "w ≠ z"
by atomize_elim (rule sdG.apath_succ_decomp[OF p])
then have "(fst e,w) ∈ parcs ?sdG" "(w, z) ∈ parcs ?sdG"
using p by (auto simp: sdG.apath_def)
with ‹fst e ≠ z› have "z = snd e"
using mem by (cases e) (auto simp: wellformed')
with p_decomp show ?thesis by fast
qed
lemma is_slim_if_subdivide:
assumes "pair_pre_digraph.is_slim (subdivide G e w) V"
assumes mem1: "e ∈ parcs G" "w ∉ pverts G" and mem2: "w ∉ V"
shows "is_slim V"
proof -
let ?sdG = "subdivide G e w"
interpret sdG: pair_sym_digraph "subdivide G e w"
using mem1 by (rule pair_sym_digraph_subdivide)
obtain u v where "e = (u,v)" by (cases e) auto
with mem1 have "u ∈ pverts G" "v ∈ pverts G" by (auto simp: wellformed')
with mem1 have "u ≠ w" "v ≠ w" by auto
let ?w_parcs = "{(u,w), (v,w), (w,u), (w, v)}"
have sdg_new_parcs: "?w_parcs ⊆ parcs ?sdG"
using ‹e = (u,v)› by auto
have sdg_no_parcs: "(u,v) ∉ parcs ?sdG" "(v,u) ∉ parcs ?sdG"
using ‹e = (u,v)› ‹u ≠ w› ‹v ≠ w› by auto
{ fix z assume A: "z ∈ pverts G"
have "in_degree ?sdG z = in_degree G z"
proof -
{ assume "z ≠ u" "z ≠ v"
then have "in_arcs ?sdG z = in_arcs G z"
using ‹e = (u,v)› mem1 A by auto
then have "in_degree ?sdG z = in_degree G z" by (simp add: in_degree_def) }
moreover
{ assume "z = u"
then have "in_arcs G z = in_arcs ?sdG z ∪ {(v,u)} - {(w,u)}"
using ‹e = (u,v)› mem1 by (auto simp: intro: arcs_symmetric wellformed')
moreover
have "card (in_arcs ?sdG z ∪ {(v,u)} - {(w,u)}) = card (in_arcs ?sdG z)"
using sdg_new_parcs sdg_no_parcs ‹z = u› by (cases "finite (in_arcs ?sdG z)") (auto simp: in_arcs_def)
ultimately have "in_degree ?sdG z= in_degree G z" by (simp add: in_degree_def) }
moreover
{ assume "z = v"
then have "in_arcs G z = in_arcs ?sdG z ∪ {(u,v)} - {(w,v)}"
using ‹e = (u,v)› mem1 A by (auto simp: wellformed')
moreover
have "card (in_arcs ?sdG z ∪ {(u,v)} - {(w,v)}) = card (in_arcs ?sdG z)"
using sdg_new_parcs sdg_no_parcs ‹z = v› by (cases "finite (in_arcs ?sdG z)") (auto simp: in_arcs_def)
ultimately have "in_degree ?sdG z= in_degree G z" by (simp add: in_degree_def) }
ultimately show ?thesis by metis
qed }
note in_degree_same = this
have V_G: "V ⊆ pverts G" "verts3 G ⊆ V"
proof -
have "V ⊆ pverts ?sdG" "pverts ?sdG = pverts G ∪ {w}" "verts3 ?sdG ⊆ V" "verts3 G ⊆ verts3 ?sdG"
using ‹sdG.is_slim V› ‹e = (u,v)› in_degree_same mem1
unfolding sdG.is_slim_def verts3_def
by (fast, simp, fastforce, force)
then show "V ⊆ pverts G" "verts3 G ⊆ V" using ‹w ∉ V› by auto
qed
have pverts: "∀v∈pverts G. v ∈ V ∨ in_degree G v ≤ 2 ∧ (∃x p y. gen_iapath V x p y ∧ v ∈ set (awalk_verts x p))"
proof -
{ fix z assume A: "z ∈ pverts G" "z ∉ V"
have "z ∈ pverts ?sdG" using ‹e = (u,v)› A mem1 by auto
then have "in_degree ?sdG z ≤ 2"
using ‹sdG.is_slim V› A by (auto simp: sdG.is_slim_def)
with in_degree_same[OF ‹z ∈ pverts G›] have idg: "in_degree G z ≤ 2" by auto
from A have "z ∈ pverts ?sdG" "z ∉ V" using ‹e = (u,v)› mem1 by auto
then obtain x' q y' where "sdG.gen_iapath V x' q y'" "z ∈ set (sdG.awalk_verts x' q)"
using ‹sdG.is_slim V› unfolding sdG.is_slim_def by metis
then have "gen_iapath V x' (co_path e w q) y'" "z ∈ set (awalk_verts x' (co_path e w q))"
using A mem1 V_G by (auto simp: set_awalk_verts_co_path' intro: gen_iapath_co_path)
with idg have "in_degree G z ≤ 2 ∧ (∃x p y. gen_iapath V x p y ∧ z ∈ set (awalk_verts x p))"
by metis }
then show ?thesis by auto
qed
have parcs: "∀e∈parcs G. fst e ≠ snd e ∧ (∃x p y. gen_iapath V x p y ∧ e ∈ set p)"
proof (intro ballI conjI)
fix e' assume "e' ∈ parcs G"
show "(∃x p y. gen_iapath V x p y ∧ e' ∈ set p)"
proof (cases "e' ∈ parcs ?sdG")
case True
then obtain x p y where "sdG.gen_iapath V x p y" "e' ∈ set p"
using ‹sdG.is_slim V› by (auto simp: sdG.is_slim_def)
with ‹e ∈ parcs G› ‹w ∉ pverts G› V_G have "gen_iapath V x (co_path e w p) y"
by (auto intro: gen_iapath_co_path)
from ‹e' ∈ parcs G› have "e' ∉ ?w_parcs" using mem1 by (auto simp: wellformed')
with ‹e' ∈ set p› have "e' ∈ set (co_path e w p)"
by (induct p rule: co_path_induct) (force simp: ‹e = (u,v)›)+
then show "∃x p y. gen_iapath V x p y ∧ e' ∈ set p "
using ‹gen_iapath V x (co_path e w p) y› by fast
next
assume "e' ∉ parcs ?sdG"
define a b where "a = fst e'" and "b = snd e'"
then have "e' = (a,b)" and ab: "(a,b) = (u,v) ∨ (a,b) = (v,u)"
using ‹e' ∈ parcs G› ‹e' ∉ parcs ?sdG› ‹e = (u,v)› mem1 by auto
obtain x p y where "sdG.gen_iapath V x p y" "(a,w) ∈ set p"
using ‹sdG.is_slim V› sdg_new_parcs ab by (auto simp: sdG.is_slim_def)
with ‹e ∈ parcs G› ‹w ∉ pverts G› V_G have "gen_iapath V x (co_path e w p) y"
by (auto intro: gen_iapath_co_path)
have "(a,b) ∈ parcs G" "subdivide G (a,b) w = subdivide G e w"
using mem1 ‹e = (u,v)› ‹e' = (a,b)› ab
by (auto intro: arcs_symmetric simp: subdivide.simps)
then have "pre_digraph.apath (subdivide G (a,b) w) x p y" "w ≠ y"
using mem2 ‹sdG.gen_iapath V x p y› by (auto simp: sdG.gen_iapath_def)
then obtain p1 p2 where p: "p = p1 @ (a,w) # (w,b) # p2"
using exists_co_path_decomp1 ‹(a,b) ∈ parcs G› ‹w ∉ pverts G› ‹(a,w) ∈ set p› ‹w ≠ y›
by atomize_elim auto
moreover
from p have "co_path e w ((a,w) # (w,b) # p2) = (a,b) # co_path e w p2"
unfolding ‹e = (u,v)› using ab by auto
ultimately
have "(a,b) ∈ set (co_path e w p)"
unfolding ‹e = (u,v)› using ab ‹u ≠ w› ‹v ≠ w›
by (induct p rule: co_path_induct) (auto simp: co_path_append)
then show ?thesis
using ‹gen_iapath V x (co_path e w p) y› ‹e' = (a,b)› by fast
qed
then show "fst e' ≠ snd e'" by (blast dest: no_loops_in_iapath)
qed
have unique: "∀u v p q. (gen_iapath V u p v ∧ gen_iapath V u q v) ⟶ p = q"
proof safe
fix x y p q assume A: "gen_iapath V x p y" "gen_iapath V x q y"
then have "set p ⊆ parcs G" "set q ⊆ parcs G"
by (auto simp: gen_iapath_def apath_def)
then have w_p: "(u,w) ∉ set p" "(v,w) ∉ set p" and w_q: "(u,w) ∉ set q" "(v,w) ∉ set q"
using mem1 by (auto simp: wellformed')
from A have "sdG.gen_iapath V x (sd_path e w p) y" "sdG.gen_iapath V x (sd_path e w q) y"
using mem1 V_G by (auto intro: gen_iapath_sd_path)
then have "sd_path e w p = sd_path e w q"
using ‹sdG.is_slim V› unfolding sdG.is_slim_def by metis
then have "co_path e w (sd_path e w p) = co_path e w (sd_path e w q)" by simp
then show "p = q" using w_p w_q ‹e = (u,v)› by (simp add: co_sd_id)
qed
from pverts parcs V_G unique show ?thesis by (auto simp: is_slim_def)
qed
end
context pair_pseudo_graph begin
lemma subdivision_gen_contr:
assumes "is_slim V"
shows "subdivision_pair (gen_contr_graph G V) G"
using assms using pair_pseudo_graph
proof (induct "card (pverts G - V)" arbitrary: G)
case 0
interpret G: pair_pseudo_graph G by fact
have "pair_bidirected_digraph G"
using G.pair_sym_arcs 0 by unfold_locales (auto simp: G.is_slim_def)
with 0 show ?case
by (auto intro: subdivision_pair_intros simp: G.gen_contr_triv G.is_slim_def)
next
case (Suc n)
interpret G: pair_pseudo_graph G by fact
from ‹Suc n = card (pverts G - V)›
have "pverts G - V ≠ {}"
by (metis Nat.diff_le_self Suc_n_not_le_n card_Diff_subset_Int diff_Suc_Suc empty_Diff finite.emptyI inf_bot_left)
then obtain w where "w ∈ pverts G - V" by auto
then obtain x q y where q: "G.gen_iapath V x q y" "w ∈ set (G.awalk_verts x q)" "in_degree G w ≤ 2"
using ‹G.is_slim V› by (auto simp: G.is_slim_def)
then have "w ≠ x" "w ≠ y" "w ∉ V" using ‹w ∈ pverts G - V› by (auto simp: G.gen_iapath_def)
then obtain e where "e ∈ set q" "snd e = w"
using ‹w ∈ pverts G - V› q
unfolding G.gen_iapath_def G.apath_def G.awalk_conv
by (auto simp: G.awalk_verts_conv')
moreover define u where "u = fst e"
ultimately obtain q1 q2 v where q_decomp: "q = q1 @ (u, w) # (w, v) # q2" "u ≠ v" "w ≠ v"
using q ‹w ≠ y› unfolding G.gen_iapath_def by atomize_elim (rule G.apath_succ_decomp, auto)
with q have qi_walks: "G.awalk x q1 u" "G.awalk v q2 y"
by (auto simp: G.gen_iapath_def G.apath_def G.awalk_Cons_iff)
from q q_decomp have uvw_arcs1: "(u,w) ∈ parcs G" "(w,v) ∈ parcs G"
by (auto simp: G.gen_iapath_def G.apath_def)
then have uvw_arcs2: "(w,u) ∈ parcs G" "(v,w) ∈ parcs G"
by (blast intro: G.arcs_symmetric)+
have "u ≠ w" "v ≠ w" using q_decomp q
by (auto simp: G.gen_iapath_def G.apath_append_iff G.apath_simps)
have in_arcs: "in_arcs G w = {(u,w), (v,w)}"
proof -
have "{(u,w), (v,w)} ⊆ in_arcs G w"
using uvw_arcs1 uvw_arcs2 by auto
moreover note ‹in_degree G w ≤ 2›
moreover have "card {(u,w), (v,w)} = 2" using ‹u ≠ v› by auto
ultimately
show ?thesis by - (rule card_seteq[symmetric], auto simp: in_degree_def)
qed
have out_arcs: "out_arcs G w ⊆ {(w,u), (w,v)}" (is "?L ⊆ ?R")
proof
fix e assume "e ∈ out_arcs G w"
then have "(snd e, fst e) ∈ in_arcs G w"
by (auto intro: G.arcs_symmetric)
then show "e ∈ {(w, u), (w, v)}" using in_arcs by auto
qed
have "(u,v) ∉ parcs G"
proof
assume "(u,v) ∈ parcs G"
have "G.gen_iapath V x (q1 @ (u,v) # q2) y"
proof -
have awalk': "G.awalk x (q1 @ (u,v) # q2) y"
using qi_walks ‹(u,v) ∈ parcs G›
by (auto simp: G.awalk_simps)
have "G.awalk x q y" using ‹G.gen_iapath V x q y› by (auto simp: G.gen_iapath_def G.apath_def)
have "distinct (G.awalk_verts x (q1 @ (u,v) # q2))"
using awalk' ‹G.gen_iapath V x q y› unfolding q_decomp
by (auto simp: G.gen_iapath_def G.apath_def G.awalk_verts_append)
moreover
have "set (G.inner_verts (q1 @ (u,v) # q2)) ⊆ set (G.inner_verts q)"
using awalk' ‹G.awalk x q y› unfolding q_decomp
by (auto simp: butlast_append G.inner_verts_conv[of _ x] G.awalk_verts_append
intro: in_set_butlast_appendI)
then have "set (G.inner_verts (q1 @ (u,v) # q2)) ∩ V = {}"
using ‹G.gen_iapath V x q y› by (auto simp: G.gen_iapath_def)
ultimately show ?thesis using awalk' ‹G.gen_iapath V x q y› by (simp add: G.gen_iapath_def G.apath_def)
qed
then have "(q1 @ (u,v) # q2) = q"
using ‹G.gen_iapath V x q y› ‹G.is_slim V› unfolding G.is_slim_def by metis
then show False unfolding q_decomp by simp
qed
then have "(v,u) ∉ parcs G" by (auto intro: G.arcs_symmetric)
define G' where "G' = ⦇pverts = pverts G - {w},
parcs = {(u,v), (v,u)} ∪ (parcs G - {(u,w), (w,u), (v,w), (w,v)})⦈"
have mem_G': "(u,v) ∈ parcs G'" "w ∉ pverts G'" by (auto simp: G'_def)
interpret pd_G': pair_fin_digraph G'
proof
fix e assume A: "e ∈ parcs G'"
have "e ∈ parcs G ∧ e ≠ (u, w) ∧ e ≠ (w, u) ∧ e ≠ (v, w) ∧ e ≠ (w, v) ⟹ fst e ≠ w"
"e ∈ parcs G ∧ e ≠ (u, w) ∧ e ≠ (w, u) ∧ e ≠ (v, w) ∧ e ≠ (w, v) ⟹ snd e ≠ w"
using out_arcs in_arcs by auto
with A uvw_arcs1 show "fst e ∈ pverts G'" "snd e ∈ pverts G'"
using ‹u ≠ w› ‹v ≠ w› by (auto simp: G'_def G.wellformed')
next
qed (auto simp: G'_def arc_to_ends_def)
interpret spd_G': pair_pseudo_graph G'
proof (unfold_locales, simp add: symmetric_def)
have "sym {(u,v), (v,u)}" "sym (parcs G)" "sym {(u, w), (w, u), (v, w), (w, v)}"
using G.sym_arcs by (auto simp: symmetric_def sym_def)
then have "sym ({(u,v), (v,u)} ∪ (parcs G - {(u,w), (w,u), (v,w), (w,v)}))"
by (intro sym_Un) (auto simp: sym_diff)
then show "sym (parcs G')" unfolding G'_def by simp
qed
have card_G': "n = card (pverts G' - V)"
proof -
have "pverts G - V = insert w (pverts G' - V)"
using ‹w ∈ pverts G - V› by (auto simp: G'_def)
then show ?thesis using ‹Suc n = card (pverts G - V)› mem_G' by simp
qed
have G_is_sd: "G = subdivide G' (u,v) w" (is "_ = ?sdG'")
using ‹w ∈ pverts G - V› ‹(u,v) ∉ parcs G› ‹(v,u) ∉ parcs G› uvw_arcs1 uvw_arcs2
by (intro pair_pre_digraph.equality) (auto simp: G'_def)
have gcg_sd: "gen_contr_graph (subdivide G' (u,v) w) V = gen_contr_graph G' V"
proof -
have "V ⊆ pverts G"
using ‹G.is_slim V› by (auto simp: G.is_slim_def verts3_def)
moreover
have "verts3 G' = verts3 G"
by (simp only: G_is_sd spd_G'.verts3_subdivide[OF ‹(u,v) ∈ parcs G'› ‹w ∉ pverts G'›])
ultimately
have V: "V ⊆ pverts G'"
using ‹w ∈ pverts G - V› by (auto simp: G'_def)
with mem_G' show ?thesis by (rule spd_G'.gcg_subdivide_eq)
qed
have is_slim_G': "pd_G'.is_slim V" using ‹G.is_slim V› mem_G' ‹w ∉ V›
unfolding G_is_sd by (rule spd_G'.is_slim_if_subdivide)
with mem_G' have "subdivision_pair (gen_contr_graph G' V) (subdivide G' (u, v) w)"
by (intro Suc card_G' subdivision_pair_intros) auto
then show ?case by (simp add: gcg_sd G_is_sd)
qed
lemma contr_is_subgraph_subdivision:
shows "∃H. subgraph (with_proj H) G ∧ subdivision_pair (contr_graph G) H"
proof -
interpret sG: pair_graph slim by (rule pair_graph_slim)
have "subdivision_pair (gen_contr_graph slim (verts3 G)) slim "
by (rule sG.subdivision_gen_contr) (rule slim_is_slim)
then show ?thesis unfolding contr_graph_slim_eq by (blast intro: subgraph_slim)
qed
theorem kuratowski_contr:
fixes K :: "'a pair_pre_digraph"
assumes subgraph_K: "subgraph K G"
assumes spd_K: "pair_pseudo_graph K"
assumes kuratowski: "K⇘3,3⇙ (contr_graph K) ∨ K⇘5⇙ (contr_graph K)"
shows "¬kuratowski_planar G"
proof -
interpret spd_K: pair_pseudo_graph K by (fact spd_K)
obtain H where subgraph_H: "subgraph (with_proj H) K"
and subdiv_H:"subdivision_pair (contr_graph K) H"
by atomize_elim (rule spd_K.contr_is_subgraph_subdivision)
have grI: "⋀K. (K⇘3,3⇙ K ∨ K⇘5⇙ K) ⟹ graph K"
by (auto simp: complete_digraph_def complete_bipartite_digraph_def)
from subdiv_H and kuratowski
have "∃K. subdivision_pair K H ∧ (K⇘3,3⇙ K ∨ K⇘5⇙ K)" by blast
then have "∃K rev_K rev_H. subdivision (K, rev_K) (H, rev_H) ∧ (K⇘3,3⇙ K ∨ K⇘5⇙ K)"
by (auto intro: grI pair_graphI_graph)
then show ?thesis using subgraph_H subgraph_K
unfolding kuratowski_planar_def by (auto intro: subgraph_trans)
qed
theorem certificate_characterization:
defines "kuratowski ≡ λG :: 'a pair_pre_digraph. K⇘3,3⇙ G ∨ K⇘5⇙ G"
shows "kuratowski (contr_graph G)
⟷ (∃H. kuratowski H ∧ subdivision_pair H slim ∧ verts3 G = verts3 slim)" (is "?L ⟷ ?R")
proof
assume ?L
interpret S: pair_graph slim by (rule pair_graph_slim)
have "subdivision_pair (contr_graph G) slim"
proof -
have *: "S.is_slim (verts3 G)" by (rule slim_is_slim)
show ?thesis using contr_graph_slim_eq S.subdivision_gen_contr[OF *] by auto
qed
moreover
have "verts3 slim = verts3 G" (is "?l = ?r")
proof safe
fix v assume "v ∈ ?l" then show "v ∈ ?r"
using verts_slim_in_G verts3_slim_in_verts3 by auto
next
fix v assume "v ∈ ?r"
have "v ∈ verts3 (contr_graph G)"
proof -
have "v ∈ verts (contr_graph G)"
using ‹v ∈ ?r› by (auto simp: verts3_def gen_contr_graph_def)
then show ?thesis
using ‹?L› unfolding kuratowski_def by (auto simp: verts3_K33 verts3_K5)
qed
then have "v ∈ verts3 (gen_contr_graph slim (verts3 G))" unfolding contr_graph_slim_eq .
then have "2 < in_degree (gen_contr_graph slim (verts3 G)) v"
unfolding verts3_def by auto
also have "… ≤ in_degree slim v"
using ‹v ∈ ?r› verts3_slim_in_verts3 by (auto intro: S.in_degree_contr)
finally show "v ∈ verts3 slim"
using verts3_in_slim_G ‹v ∈ ?r› unfolding verts3_def by auto
qed
ultimately show ?R using ‹?L› by auto
next
assume ?R
then have "kuratowski (gen_contr_graph slim (verts3 G))"
unfolding kuratowski_def
by (auto intro: K33_contractedI K5_contractedI)
then show ?L unfolding contr_graph_slim_eq .
qed
definition (in pair_pre_digraph) certify :: "'a pair_pre_digraph ⇒ bool" where
"certify cert ≡ let C = contr_graph cert in subgraph cert G ∧ (K⇘3,3⇙ C ∨ K⇘5⇙C)"
theorem certify_complete:
assumes "pair_pseudo_graph cert"
assumes "subgraph cert G"
assumes "∃H. subdivision_pair H cert ∧ (K⇘3,3⇙ H ∨ K⇘5⇙ H)"
shows "certify cert"
unfolding certify_def
using assms by (auto simp: Let_def intro: K33_contractedI K5_contractedI)
theorem certify_sound:
assumes "pair_pseudo_graph cert"
assumes "certify cert"
shows" ¬kuratowski_planar G"
using assms by (intro kuratowski_contr) (auto simp: certify_def Let_def)
theorem certify_characterization:
assumes "pair_pseudo_graph cert"
shows "certify cert ⟷ subgraph cert G ∧ verts3 cert = verts3 (pair_pre_digraph.slim cert)
∧(∃H. (K⇘3,3⇙ (with_proj H) ∨ K⇘5⇙ H) ∧ subdivision_pair H (pair_pre_digraph.slim cert))"
(is "?L ⟷ ?R")
by (auto simp only: simp_thms certify_def Let_def pair_pseudo_graph.certificate_characterization[OF assms])
end
end