Theory Kuratowski

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

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

(* XXX: Replace "parcs (contr_graph G)" by its definition *)
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

(* could be generalized *)
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

(* could be generalized *)
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