Theory Check_Non_Planarity_Verification
section "Verification of a Non-Planarity Checker"
theory Check_Non_Planarity_Verification imports
Check_Non_Planarity_Impl
"../Planarity/Kuratowski_Combinatorial"
"HOL-Library.Rewrite"
"HOL-Eisbach.Eisbach"
begin
subsection ‹Graph Basics and Implementation›
context pre_digraph begin
lemma cas_nonempty_ends:
assumes "p ≠ []" "cas u p v" "cas u' p v'"
shows "u = u'" "v = v'"
using assms apply (metis cas_simp)
using assms by (metis append_Nil2 cas.simps(1) cas_append_iff cas_simp)
lemma awalk_nonempty_ends:
assumes "p ≠ []" "awalk u p v" "awalk u' p v'"
shows "u = u'" "v = v'"
using assms by (auto simp: awalk_def intro: cas_nonempty_ends)
end
lemma (in pair_graph) verts2_awalk_distinct:
assumes V: "verts3 G ⊆ V" "V ⊆ pverts G" "u ∈ V"
assumes p: "awalk u p v" "set (inner_verts p) ∩ V = {}" "progressing p"
shows "distinct (inner_verts p)"
using p
proof (induct p arbitrary: v rule: rev_induct)
case Nil then show ?case by auto
next
case (snoc e es)
have "distinct (inner_verts es)"
apply (rule snoc.hyps)
using snoc.prems apply (auto dest: progressing_appendD1)
apply (metis (opaque_lifting, no_types) disjoint_iff_not_equal in_set_inner_verts_appendI_l)
done
show ?case
proof (rule ccontr)
assume A: "¬?thesis"
then obtain es' e' where "es = es' @ [e']" "es ≠ []"
by (cases es rule: rev_cases) auto
have "fst e ∈ set (inner_verts es)"
using A ‹distinct (inner_verts es)› ‹es ≠ []›
by (auto simp: inner_verts_def)
moreover
have "fst e' ≠ fst e" "snd e' = fst e"
using ‹es = es' @ [e']› snoc.prems(1)
by (auto simp: awalk_Cons_iff dest: no_loops)
ultimately
obtain es'' e'' where "es' = es'' @ [e'']"
by (cases es' rule: rev_cases) (auto simp: ‹es = es' @ [e']› inner_verts_def)
then have "fst e'' ≠ fst e"
using ‹snd e' = fst e›[symmetric] snoc.prems(1,3) unfolding ‹es = _›
by (simp add: ‹es = _› awalk_Cons_iff progressing_append_iff progressing_Cons)
have "fst e' ∈ set (inner_verts es)"
using ‹es = es' @ [e']› ‹es' = es'' @ [e'']›
by (cases es'') (auto simp: inner_verts_def)
have "fst e ∈ set (inner_verts es')"
using ‹es = es' @ [e']› ‹fst e ∈ set (inner_verts es)› ‹fst e' ≠ fst e›
by (cases es') (auto simp: inner_verts_def)
then obtain q e'2 e'3 r where Z: "es' = q @ [e'2, e'3] @ r" "snd e'2 = fst e" "fst e'3 = fst e"
proof -
obtain e'3' where "e'3' ∈ set (tl es')" "fst e'3' = fst e"
using ‹fst e ∈ set (inner_verts es')›
by (cases es') (auto simp: inner_verts_def)
then obtain q r where "tl es' = q @ e'3' # r"
by (metis split_list)
then have F2: "snd (last (hd es' # q)) = fst e"
using ‹es = es' @ [e']› snoc.prems(1) ‹fst e'3' = fst e›
apply (cases es')
apply (case_tac [2] q rule: rev_cases)
apply auto
done
then have "es' = (butlast (hd es' # q)) @ [last (hd es' # q), e'3'] @ r"
using ‹tl es' = q @ e'3' # r› by (cases es') auto
then show ?thesis using F2 ‹fst e'3' = fst e› by fact
qed
then have "fst e'2 ≠ snd e'3"
using snoc.prems(3) unfolding ‹es = _›
by (simp add: progressing_append_iff progressing_Cons)
moreover
from Z have B: "fst e'2 = u ∨ fst e'2 ∈ set (inner_verts es')"
using ‹es = es' @ [e']› snoc.prems(1)
by (cases q) (auto simp: inner_verts_def)
then have "fst e'2 ≠ fst e'"
proof
assume "fst e'2 = u"
then have "fst e'2 ∉ set (inner_verts es)"
using V ‹es = es' @ [e']› snoc.prems(2)
by (cases es') (auto simp: inner_verts_def)
moreover
have "fst e' ∈ set (inner_verts es)"
using ‹es = es' @ [e']› ‹es' = es'' @ [e'']›
by (cases es'') (auto simp: inner_verts_def)
ultimately show ?thesis by auto
next
assume "fst e'2 ∈ set (inner_verts es')"
moreover
have "fst e' ∈ set (inner_verts es)"
using ‹es = es' @ [e']› ‹es' = es'' @ [e'']›
by (cases es'') (auto simp: inner_verts_def)
ultimately
show ?thesis
using ‹distinct (inner_verts es)› unfolding ‹es = es' @ [e']›
by (cases es') (fastforce simp: inner_verts_def)+
qed
moreover
have "snd e'3 ≠ fst e'"
proof (rule notI, cases)
assume "r = []" "snd e'3 = fst e'"
then show False using Z ‹es = es' @ [e']› snoc.prems(3) ‹snd e' = fst e›
by (simp add: progressing_append_iff progressing_Cons)
next
assume A: "r ≠ []" "snd e'3 = fst e'"
then obtain r0 rs where "r = r0 # rs" by (cases r) auto
then have "snd e'3 = fst r0"
using Z ‹es = es' @ [e']› snoc.prems(1)
by (auto simp: awalk_Cons_iff)
with A have "fst r0 = fst e'" by auto
have "¬distinct (inner_verts es)"
by (cases q) (auto simp add: Z(1) ‹es = es' @ [e']›
‹r = r0 # rs› ‹fst r0 = fst e'› inner_verts_def)
then show False using ‹distinct (inner_verts es)› by auto
qed
ultimately
have card_to_fst_e: "card {e'2, (snd e'3, fst e'3), e'} = 3"
by (auto simp: card_insert_if)
moreover
have "e'3 ∈ parcs G"
using Z using snoc.prems(1) ‹es = es' @ [e']›
by (auto intro: arcs_symmetric)
then have "(snd e'3, fst e'3) ∈ parcs G"
by (auto intro: arcs_symmetric)
then have "{e'2, (snd e'3, fst e'3), e'} ⊆ {ed ∈ parcs G. snd ed = fst e}"
using snoc.prems(1) ‹es = es' @ [e']› Z by auto
moreover
have "fst e ∈ pverts G" using snoc.prems(1) by auto
then have card_to_fst_e_abs: "card {ed ∈ parcs G. snd ed = fst e} ≤ 2"
using ‹fst e ∈ set (inner_verts es)› V snoc.prems(2)
unfolding verts3_def in_degree_def
by (cases es) (auto simp: inner_verts_def in_arcs_def)
ultimately
have "{e'2, (snd e'3, fst e'3), e'} = {ed ∈ parcs G. snd ed = fst e}"
by (intro card_seteq) auto
then show False
using card_to_fst_e card_to_fst_e_abs by auto
qed
qed
lemma (in wf_digraph) inner_verts_conv':
assumes "awalk u p v" "2 ≤ length p" shows "inner_verts p = awalk_verts (head G (hd p)) (butlast (tl p))"
using assms
apply (cases p)
apply (auto simp: awalk_Cons_iff; fail)
apply (match premises in "p = _ # as" for as ⇒ ‹cases as rule: rev_cases›)
apply (auto simp: inner_verts_def awalk_verts_conv)
done
lemma verts3_in_verts:
assumes "x ∈ verts3 G" shows "x ∈ verts G"
using assms unfolding verts3_def by auto
lemma (in pair_graph) deg2_awalk_is_iapath:
assumes V: "verts3 G ⊆ V" "V ⊆ pverts G"
assumes p: "awalk u p v" "set (inner_verts p) ∩ V = {}" "progressing p"
assumes in_V: "u ∈ V" "v ∈ V"
assumes "u ≠ v"
shows "gen_iapath V u p v"
proof (cases p)
case Nil then show ?thesis using p(1) in_V ‹u ≠ v› by (auto simp: apath_def gen_iapath_def)
next
case (Cons p0 ps)
then have ev_p: "awalk_verts u p = u # butlast (tl (awalk_verts u p)) @ [v]"
using p(1) by (cases p) auto
have "u ∉ set (inner_verts p)" "v ∉ set (inner_verts p)"
using p(2) in_V by auto
with verts2_awalk_distinct[OF V in_V(1) p] have "distinct (awalk_verts u p)"
using p(1) ‹u ≠ v› by (subst ev_p) (auto simp: inner_verts_conv[of p u] verts3_def)
then show ?thesis using p(1-2) in_V ‹u ≠ v› by (auto simp: apath_def gen_iapath_def)
qed
lemma (in pair_graph) inner_verts_min_degree:
assumes walk_p: "awalk u p v" and progress: "progressing p"
and w_p: "w ∈ set (inner_verts p)"
shows "2 ≤in_degree G w"
proof -
from w_p have "2 ≤ length p" using not_le by fastforce
moreover
then obtain e1 es e2 where p_decomp: "p = e1 # es @ [e2]"
by (metis One_nat_def Suc_1 Suc_eq_plus1 le0 list.size(3) list.size(4) neq_Nil_conv not_less_eq_eq rev_cases)
ultimately
have w_es: "w ∈ set (awalk_verts (snd e1) es)"
using walk_p w_p by (auto simp: apath_def inner_verts_conv')
have walk_es: "awalk (snd e1) es (fst e2)"
using walk_p by (auto simp: p_decomp awalk_simps)
obtain q r where es_decomp: "es = q @ r" "awalk (snd e1) q w" "awalk w r (fst e2)"
using awalk_decomp[OF walk_es w_es] by auto
define xs x y ys
where "xs = butlast (e1 # q)" and "x = last (e1 # q)"
and "y = hd (r @ [e2])" and "ys = tl (r @ [e2])"
then have "p = xs @ x # y # ys"
by (auto simp: p_decomp es_decomp)
moreover
have "awalk u (e1 # q) w" "awalk w (r @ [e2]) v"
using walk_p es_decomp p_decomp by (auto simp: awalk_Cons_iff)
then have inc_w: "snd x = w" "fst y = w"
unfolding x_def y_def
apply -
apply (auto simp: awalk_Cons_iff awalk_verts_conv; fail)
apply (cases r)
apply auto
done
ultimately have "fst x ≠ snd y"
using progress by (auto simp: progressing_append_iff progressing_Cons)
have "x ∈ parcs G" "y ∈ parcs G"
using walk_p ‹p = xs @ x # y # ys› by auto
then have "{x, (snd y, w)} ⊆ {e ∈ parcs G. snd e = w}"
using inc_w by auto (metis arcs_symmetric surjective_pairing)
then have "card {x, (snd y, w)} ≤ in_degree G w"
unfolding in_degree_def by (intro card_mono) auto
then show ?thesis using ‹fst x ≠ snd y› inc_w
by (auto simp: card_insert_if split: if_split_asm)
qed
lemma (in pair_pseudo_graph) gen_iapath_same2E:
assumes "verts3 G ⊆ V" "V ⊆ pverts G"
and "gen_iapath V u p v" "gen_iapath V w q x"
and "e ∈ set p" "e ∈ set q"
obtains "p = q"
using assms same_gen_iapath_by_common_arc by metis
definition mk_graph' :: "IGraph ⇒ ig_vertex pair_pre_digraph" where
"mk_graph' IG ≡ ⦇ pverts = set (ig_verts IG), parcs = set (ig_arcs IG)⦈"
definition mk_graph :: "IGraph ⇒ ig_vertex pair_pre_digraph" where
"mk_graph IG ≡ mk_symmetric (mk_graph' IG)"
lemma verts_mkg': "pverts (mk_graph' G) = set (ig_verts G)"
unfolding mk_graph'_def by simp
lemma arcs_mkg': "parcs (mk_graph' G) = set (ig_arcs G)"
unfolding mk_graph'_def by simp
lemmas mkg'_simps = verts_mkg' arcs_mkg'
lemma verts_mkg: "pverts (mk_graph G) = set (ig_verts G)"
unfolding mk_graph_def by (simp add: mkg'_simps )
lemma parcs_mk_symmetric_symcl: "parcs (mk_symmetric G) = (arcs_ends G)⇧s"
by (auto simp: parcs_mk_symmetric symcl_def arcs_ends_conv)
lemma arcs_mkg: "parcs (mk_graph G) = (set (ig_arcs G))⇧s"
unfolding mk_graph_def parcs_mk_symmetric_symcl by (simp add: arcs_mkg')
lemmas mkg_simps = verts_mkg arcs_mkg
definition iadj :: "IGraph ⇒ ig_vertex ⇒ ig_vertex ⇒ bool" where
"iadj G u v ≡ (u,v) ∈ set (ig_arcs G) ∨ (v,u) ∈ set (ig_arcs G)"
definition "loop_free G ≡ (∀e ∈ parcs G. fst e ≠ snd e)"
lemma ig_opposite_simps:
"ig_opposite G (u,v) u = v" "ig_opposite G (v,u) u = v"
unfolding ig_opposite_def by auto
lemma distinct_ig_verts:
"distinct (ig_verts G)"
by (cases G) (auto simp: ig_verts_def Abs_IGraph_inverse)
lemma set_ig_arcs_verts:
assumes "IGraph_inv G" "(u,v) ∈ set (ig_arcs G)" shows "u ∈ set (ig_verts G)" "v ∈ set (ig_verts G)"
using assms unfolding IGraph_inv_def
by (auto simp: mkg'_simps dest: all_nth_imp_all_set)
lemma IGraph_inv_conv:
"IGraph_inv G ⟷ pair_fin_digraph (mk_graph' G)"
proof -
{ assume "∀e∈set (ig_arcs G). fst e ∈ set (ig_verts G) ∧ snd e ∈ set (ig_verts G)"
then have "pair_fin_digraph (mk_graph' G)"
by unfold_locales (auto simp: mkg'_simps) }
moreover
{ assume "pair_fin_digraph (mk_graph' G)"
then interpret pair_fin_digraph "mk_graph' G" .
have "∀e∈set (ig_arcs G). fst e ∈ set (ig_verts G) ∧ snd e ∈ set (ig_verts G)"
using tail_in_verts head_in_verts
by (fastforce simp: mkg'_simps in_set_conv_nth) }
ultimately
show ?thesis unfolding IGraph_inv_def by blast
qed
lemma IGraph_inv_conv':
"IGraph_inv G ⟷ pair_pseudo_graph (mk_graph G)"
unfolding IGraph_inv_conv
proof
assume "pair_fin_digraph (mk_graph' G)"
interpret ppd: pair_fin_digraph "mk_graph' G" by fact
interpret pd: pair_fin_digraph "mk_graph G"
unfolding mk_graph_def ..
show "pair_pseudo_graph (mk_graph G)"
by unfold_locales (auto simp: mk_graph_def symmetric_mk_symmetric)
next
assume A: "pair_pseudo_graph (mk_graph G)"
interpret ppg: pair_pseudo_graph "mk_graph G" by fact
show "pair_fin_digraph (mk_graph' G)"
using ppg.wellformed'
by unfold_locales (auto simp: mkg_simps mkg'_simps symcl_def, auto)
qed
lemma iadj_io_edge:
assumes "u ∈ set (ig_verts G)" "e ∈ set (ig_in_out_arcs G u)"
shows "iadj G u (ig_opposite G e u)"
proof -
from assms obtain v where e: "e = (u,v) ∨ e = (v,u)" "e ∈ set (ig_arcs G)"
unfolding ig_in_out_arcs_def by (cases e) auto
then have *: "ig_opposite G e u = v" by safe (auto simp: ig_opposite_def)
show ?thesis using e unfolding iadj_def * by auto
qed
lemma All_set_ig_verts: "(∀v ∈ set (ig_verts G). P v) ⟷ (∀i < ig_verts_cnt G. P (ig_verts G ! i))"
by (metis in_set_conv_nth ig_verts_cnt_def)
lemma IGraph_imp_ppd_mkg':
assumes "IGraph_inv G" shows "pair_fin_digraph (mk_graph' G)"
using assms unfolding IGraph_inv_conv by auto
lemma finite_symcl_iff: "finite (R⇧s) ⟷ finite R"
unfolding symcl_def by blast
lemma (in pair_fin_digraph) pair_pseudo_graphI_mk_symmetric:
"pair_pseudo_graph (mk_symmetric G)"
by unfold_locales
(auto simp: parcs_mk_symmetric symmetric_mk_symmetric wellformed')
lemma IGraph_imp_ppg_mkg:
assumes "IGraph_inv G" shows "pair_pseudo_graph (mk_graph G)"
using assms unfolding mk_graph_def
by (intro pair_fin_digraph.pair_pseudo_graphI_mk_symmetric IGraph_imp_ppd_mkg')
lemma IGraph_lf_imp_pg_mkg:
assumes "IGraph_inv G" "loop_free (mk_graph G)" shows "pair_graph (mk_graph G)"
proof -
interpret ppg: pair_pseudo_graph "mk_graph G"
using assms(1) by (rule IGraph_imp_ppg_mkg)
show "pair_graph (mk_graph G)"
using assms by unfold_locales (auto simp: loop_free_def)
qed
lemma set_ig_arcs_imp_verts:
assumes "(u,v) ∈ set (ig_arcs G)" "IGraph_inv G" shows "u ∈ set (ig_verts G)" "v ∈ set (ig_verts G)"
proof -
interpret pair_pseudo_graph "mk_graph G"
using assms by (auto intro: IGraph_imp_ppg_mkg)
from assms have "(u,v) ∈ parcs (mk_graph G)" by (simp add: mkg_simps symcl_def)
then have "u ∈ pverts (mk_graph G)" "v ∈ pverts (mk_graph G)" by (auto dest: wellformed')
then show "u ∈ set (ig_verts G)" "v ∈ set (ig_verts G)" by (auto simp: mkg_simps)
qed
lemma iadj_imp_verts:
assumes "iadj G u v" "IGraph_inv G" shows "u ∈ set (ig_verts G)" "v ∈ set (ig_verts G)"
using assms unfolding iadj_def by (auto dest: set_ig_arcs_imp_verts)
lemma card_ig_neighbors_indegree:
assumes "IGraph_inv G"
shows "card (ig_neighbors G u) = in_degree (mk_graph G) u"
proof -
have inj2: "inj_on (λe. ig_opposite G e u) {e ∈ parcs (mk_graph G). snd e = u}"
unfolding ig_opposite_def by (rule inj_onI) (fastforce split: if_split_asm)
have "ig_neighbors G u = (λe. ig_opposite G e u) ` {e ∈ parcs (mk_graph G). snd e = u}"
using assms unfolding ig_neighbors_def
by (auto simp: ig_opposite_simps symcl_def mkg_simps set_ig_arcs_verts intro!: rev_image_eqI)
then have "card (ig_neighbors G u) = card ((λe. ig_opposite G e u) ` {e ∈ parcs (mk_graph G). snd e = u})"
by simp
also have "… = in_degree (mk_graph G) u"
unfolding in_degree_def in_arcs_def with_proj_simps
using inj2 by (rule card_image)
finally show ?thesis .
qed
lemma iadjD:
assumes "iadj G u v"
shows "∃e ∈ set (ig_in_out_arcs G u). (e = (u,v) ∨ e = (v,u))"
proof -
from assms obtain e where "e ∈ set (ig_arcs G)" "e = (u,v) ∨ e = (v,u)"
unfolding iadj_def by auto
then show ?thesis unfolding ig_in_out_arcs_def by auto
qed
lemma
ig_verts_empty[simp]: "ig_verts ig_empty = []" and
ig_verts_add_e[simp]: "ig_verts (ig_add_e G u v) = ig_verts G" and
ig_verts_add_v[simp]: "ig_verts (ig_add_v G v) = ig_verts G @ (if v ∈ set (ig_verts G) then [] else [v])"
unfolding ig_verts_def ig_empty_def ig_add_e_def ig_add_v_def
by (auto simp: Abs_IGraph_inverse distinct_ig_verts[simplified ig_verts_def])
lemma
ig_arcs_empty[simp]: "ig_arcs ig_empty = []" and
ig_arcs_add_e[simp]: "ig_arcs (ig_add_e G u v) = ig_arcs G @ [(u,v)]" and
ig_arcs_add_v[simp]: "ig_arcs (ig_add_v G v) = ig_arcs G"
unfolding ig_arcs_def ig_empty_def ig_add_e_def ig_add_v_def
by (auto simp: Abs_IGraph_inverse distinct_ig_verts)
subsection ‹Total Correctness›
subsubsection ‹Procedure @{term is_subgraph}›
definition is_subgraph_verts_inv :: "IGraph ⇒ IGraph ⇒ nat ⇒ bool" where
"is_subgraph_verts_inv G H i ≡ set (take i (ig_verts G)) ⊆ set (ig_verts H)"
definition is_subgraph_arcs_inv :: "IGraph ⇒ IGraph ⇒ nat ⇒ bool" where
"is_subgraph_arcs_inv G H i ≡ ∀j < i. let (u,v) = ig_arcs G ! j in
((u,v) ∈ set (ig_arcs H) ∨ (v,u) ∈ set (ig_arcs H))
∧ u ∈ set (ig_verts G) ∧ v ∈ set (ig_verts G)"
lemma is_subgraph_verts_0: "is_subgraph_verts_inv G H 0"
unfolding is_subgraph_verts_inv_def by auto
lemma is_subgraph_verts_step:
assumes "is_subgraph_verts_inv G H i" "ig_verts G ! i ∈ set (ig_verts H)"
assumes "i < length (ig_verts G)"
shows "is_subgraph_verts_inv G H (Suc i)"
using assms by (auto simp: is_subgraph_verts_inv_def take_Suc_conv_app_nth)
lemma is_subgraph_verts_last:
"is_subgraph_verts_inv G H (length (ig_verts G)) ⟷ pverts (mk_graph G) ⊆ pverts (mk_graph H)"
apply (auto simp: is_subgraph_verts_inv_def mkg_simps)
done
lemma is_subgraph_arcs_0: "is_subgraph_arcs_inv G H 0"
unfolding is_subgraph_arcs_inv_def by auto
lemma is_subgraph_arcs_step:
assumes "is_subgraph_arcs_inv G H i"
"e ∈ set (ig_arcs H) ∨ (snd e, fst e) ∈ set (ig_arcs H)"
"fst e ∈ set (ig_verts G)" "snd e ∈ set (ig_verts G)"
assumes "e = ig_arcs G ! i"
assumes "i < length (ig_arcs G)"
shows "is_subgraph_arcs_inv G H (Suc i)"
using assms by (auto simp: is_subgraph_arcs_inv_def less_Suc_eq)
lemma wellformed_pseudo_graph_mkg:
shows "pair_wf_digraph (mk_graph G) = pair_pseudo_graph(mk_graph G)" (is "?L = ?R")
proof
assume ?R
then interpret ppg: pair_pseudo_graph "mk_graph G" .
show ?L by unfold_locales
next
assume ?L
moreover have "symmetric (mk_graph G)"
unfolding mk_graph_def by (simp add: symmetric_mk_symmetric)
ultimately show ?R
unfolding pair_wf_digraph_def
by unfold_locales (auto simp: mkg_simps finite_symcl_iff)
qed
lemma is_subgraph_arcs_last:
"is_subgraph_arcs_inv G H (length (ig_arcs G)) ⟷ parcs (mk_graph G) ⊆ parcs (mk_graph H) ∧ pair_pseudo_graph (mk_graph G)"
proof -
have "is_subgraph_arcs_inv G H (length (ig_arcs G))
= (∀(u,v) ∈ set (ig_arcs G). ((u,v) ∈ set (ig_arcs H) ∨ (v,u) ∈ set (ig_arcs H))
∧ u ∈ set (ig_verts G) ∧ v ∈ set (ig_verts G))"
unfolding is_subgraph_arcs_inv_def
by (metis (lifting, no_types) all_nth_imp_all_set nth_mem)
also have "... ⟷ parcs (mk_graph G) ⊆ parcs (mk_graph H) ∧ pair_pseudo_graph (mk_graph G)"
unfolding wellformed_pseudo_graph_mkg[symmetric]
by (auto simp: mkg_simps pair_wf_digraph_def symcl_def)
finally show ?thesis .
qed
lemma is_subgraph_verts_arcs_last:
assumes "is_subgraph_verts_inv G H (ig_verts_cnt G)"
assumes "is_subgraph_arcs_inv G H (ig_arcs_cnt G)"
assumes "IGraph_inv H"
shows "subgraph (mk_graph G) (mk_graph H)" (is ?T1)
"pair_pseudo_graph (mk_graph G)" (is ?T2)
proof -
interpret ppg: pair_pseudo_graph "mk_graph G"
using assms by (simp add: is_subgraph_arcs_last)
interpret ppgH: pair_pseudo_graph "mk_graph H" using assms by (intro IGraph_imp_ppg_mkg)
have "wf_digraph (with_proj (mk_graph G))" by unfold_locales
with assms show ?T1 ?T2
by (auto simp: is_subgraph_verts_last is_subgraph_arcs_last subgraph_def ppgH.wf_digraph)
qed
lemma is_subgraph_false:
assumes "subgraph (mk_graph G) (mk_graph H)"
obtains "∀i < length (ig_verts G). ig_verts G ! i ∈ set (ig_verts H)"
"∀i < length (ig_arcs G). let (u,v) = ig_arcs G ! i in
((u,v)∈ set (ig_arcs H) ∨ (v,u) ∈ set (ig_arcs H))
∧ u ∈ set (ig_verts G) ∧ v ∈ set (ig_verts G)"
proof
from assms
show "∀i < length (ig_verts G). ig_verts G ! i ∈ set (ig_verts H)"
unfolding subgraph_def by (auto simp: mkg_simps)
next
from assms have "is_subgraph_arcs_inv G H (length (ig_arcs G))"
unfolding is_subgraph_arcs_last subgraph_def wellformed_pseudo_graph_mkg[symmetric]
by (auto simp: wf_digraph_wp_iff)
then show "∀i < length (ig_arcs G). let (u,v) = ig_arcs G ! i in
((u,v)∈ set (ig_arcs H) ∨ (v,u) ∈ set (ig_arcs H))
∧ u ∈ set (ig_verts G) ∧ v ∈ set (ig_verts G)"
by (auto simp: is_subgraph_arcs_inv_def)
qed
lemma (in is_subgraph_impl) is_subgraph_spec:
"∀σ. Γ ⊢⇩t ⦃σ. IGraph_inv ´H ⦄ ´R :== PROC is_subgraph(´G, ´H) ⦃ ´G = ⇗σ⇖G ∧ ´H = ⇗σ⇖H ∧ ´R = (subgraph (mk_graph ´G) (mk_graph ´H) ∧ IGraph_inv ´G)⦄"
apply (vcg_step spec=none)
apply (rewrite
at "whileAnno _ (named_loop ''verts'') _ _"
in for (σ)
to "whileAnno _
⦃ is_subgraph_verts_inv ´G ´H ´i ∧ ´G = ⇗σ⇖G ∧ ´H = ⇗σ⇖H ∧ ´i ≤ ig_verts_cnt ´G
∧ IGraph_inv ´H⦄
(MEASURE ig_verts_cnt ´G - ´i)
_"
annotate_named_loop_var)
apply (rewrite
at "whileAnno _ (named_loop ''arcs'') _ _"
in for (σ)
to "whileAnno _
⦃ is_subgraph_arcs_inv ´G ´H ´i ∧ ´G = ⇗σ⇖G ∧ ´H = ⇗σ⇖H ∧ ´i ≤ ig_arcs_cnt ´G
∧ is_subgraph_verts_inv ´G ´H (length (ig_verts ´G)) ∧ IGraph_inv ´H ⦄
(MEASURE ig_arcs_cnt ´G - ´i)
_"
annotate_named_loop_var)
apply vcg
apply (fastforce simp: is_subgraph_verts_0)
apply (fastforce simp: is_subgraph_verts_step elim: is_subgraph_false)
apply (fastforce simp: is_subgraph_arcs_0 not_less)
apply (auto simp: is_subgraph_arcs_step elim!: is_subgraph_false; fastforce)
apply (fastforce simp: IGraph_inv_conv' is_subgraph_verts_arcs_last)
done
subsubsection ‹Procedure @{term is_loop_free}›
definition "is_loopfree_inv G k ≡ ∀j<k. fst (ig_arcs G ! j) ≠ snd (ig_arcs G ! j)"
lemma is_loopfree_0:
"is_loopfree_inv G 0"
by (auto simp: is_loopfree_inv_def)
lemma is_loopfree_step1:
assumes "is_loopfree_inv G n"
assumes "fst (ig_arcs G ! n) ≠ snd (ig_arcs G ! n)"
assumes "n < ig_arcs_cnt G"
shows "is_loopfree_inv G (Suc n)"
using assms unfolding is_loopfree_inv_def
by (auto intro: less_SucI elim: less_SucE)
lemma is_loopfree_step2:
assumes "loop_free (mk_graph G)"
assumes "n < ig_arcs_cnt G"
shows "fst (ig_arcs G ! n) ≠ snd (ig_arcs G ! n)"
using assms unfolding is_loopfree_inv_def loop_free_def
by (auto simp: mkg_simps symcl_def)
lemma is_loopfree_last:
assumes "is_loopfree_inv G (ig_arcs_cnt G)"
shows "loop_free (mk_graph G)"
using assms apply (auto simp: is_loopfree_inv_def loop_free_def mkg_simps in_set_conv_nth symcl_def)
apply (metis fst_eqD snd_eqD)+
done
lemma (in is_loopfree_impl) is_loopfree_spec:
"∀σ. Γ ⊢⇩t ⦃σ. IGraph_inv ´G ⦄ ´R :== PROC is_loopfree(´G) ⦃ ´G = ⇗σ⇖G ∧ ´R = loop_free (mk_graph ´G) ⦄"
apply (vcg_step spec=none)
apply (rewrite
at "whileAnno _ (named_loop ''loop'') _ _"
in for (σ)
to "whileAnno _
⦃ is_loopfree_inv ´G ´i ∧ ´G = ⇗σ⇖G ∧ ´i ≤ ig_arcs_cnt ´G ⦄
(MEASURE ig_arcs_cnt ´G - ´i)
_"
annotate_named_loop_var)
apply vcg
apply (fastforce simp: is_loopfree_0)
apply (fastforce intro: is_loopfree_step1 dest: is_loopfree_step2)
apply (fastforce simp: is_loopfree_last)
done
subsubsection ‹Procedure @{term select_nodes}›
definition select_nodes_inv :: "IGraph ⇒ IGraph ⇒ nat ⇒ bool" where
"select_nodes_inv G H i ≡ set (ig_verts H) = {v ∈ set (take i (ig_verts G)). card (ig_neighbors G v) ≥ 3} ∧ IGraph_inv H"
lemma select_nodes_inv_step:
fixes G H i
defines "v ≡ ig_verts G ! i"
assumes G_inv: "IGraph_inv G"
assumes sni_inv: "select_nodes_inv G H i"
assumes less: "i < ig_verts_cnt G"
assumes H': "H' = (if 3 ≤ card (ig_neighbors G v) then ig_add_v H v else H)"
shows "select_nodes_inv G H' (Suc i)"
proof -
have *: "IGraph_inv H'" using sni_inv H'
unfolding IGraph_inv_def select_nodes_inv_def by auto
have take_Suc_i: "take (Suc i) (ig_verts G) = take i (ig_verts G) @ [v]"
using less unfolding v_def by (auto simp: take_Suc_conv_app_nth)
have X: "v ∉ set (take i (ig_verts G))"
using G_inv less distinct_ig_verts unfolding v_def IGraph_inv_conv
by (auto simp: distinct_conv_nth in_set_conv_nth)
show ?thesis
unfolding select_nodes_inv_def using X sni_inv
by (simp only: *) (auto simp: take_Suc_i select_nodes_inv_def H')
qed
definition select_nodes_prop :: "IGraph ⇒ IGraph ⇒ bool" where
"select_nodes_prop G H ≡ pverts (mk_graph H) = verts3 (mk_graph G)"
lemma (in select_nodes_impl) select_nodes_spec:
"∀σ. Γ ⊢⇩t ⦃σ. IGraph_inv ´G⦄ ´R :== PROC select_nodes(´G)
⦃ select_nodes_prop ⇗σ⇖G ´R ∧ IGraph_inv ´R ∧ set (ig_arcs ´R) = {}⦄"
apply vcg_step
apply (rewrite
at "whileAnno _ (named_loop ''loop'') _ _"
in for (σ)
to "whileAnno _
⦃ select_nodes_inv ´G ´R ´i ∧ ´i ≤ ig_verts_cnt ´G ∧ ´G = ⇗σ⇖G ∧ IGraph_inv ´G ∧ set (ig_arcs ´R) = {}⦄
(MEASURE ig_verts_cnt ´G - ´i)
_"
annotate_named_loop_var)
apply vcg
apply (fastforce simp: select_nodes_inv_def IGraph_inv_def mkg'_simps)
apply (fastforce simp add: select_nodes_inv_step)
apply (fastforce simp add: select_nodes_inv_def select_nodes_prop_def card_ig_neighbors_indegree verts3_def mkg_simps)
done
subsubsection ‹Procedure @{term find_endpoint}›
definition find_endpoint_path_inv where
"find_endpoint_path_inv G H len u v w x ≡
∃p. pre_digraph.awalk (mk_graph G) u p x ∧ length p = len ∧
hd p = (u,v) ∧ last p = (w, x) ∧
set (pre_digraph.inner_verts (mk_graph G) p) ∩ set (ig_verts H) = {} ∧
progressing p "
definition find_endpoint_arcs_inv where
"find_endpoint_arcs_inv G found k v0 v1 v0' v1' ≡
(found ⟶ (∃i < k. v1' = ig_opposite G (ig_in_out_arcs G v1 ! i) v1 ∧ v0' = v1 ∧ v0 ≠ v1')) ∧
(¬found ⟶ (∀i < k. v0 = ig_opposite G (ig_in_out_arcs G v1 ! i) v1) ∧ v0 = v0' ∧ v1 = v1')"
lemma find_endpoint_path_first:
assumes "iadj G u v" "u ≠ v" "IGraph_inv G"
shows "find_endpoint_path_inv G H (Suc 0) u v u v"
proof -
interpret ppg: pair_pseudo_graph "mk_graph G"
using assms by (auto intro: IGraph_imp_ppg_mkg)
have "(u,v) ∈ parcs (mk_graph G)"
using assms by (auto simp: iadj_def mkg_simps symcl_def)
then have "ppg.awalk u [(u,v)] v" "length [(u,v)] = Suc 0" "hd [(u,v)] = (u,v)" "last [(u,v)] = (u,v)" "progressing [(u,v)]"
using assms by (auto simp: ppg.awalk_simps iadj_imp_verts mkg_simps progressing_Cons)
moreover
have "set (ppg.inner_verts [(u,v)]) ∩ set (ig_verts H) = {}"
by (auto simp: ppg.inner_verts_def)
ultimately
show ?thesis unfolding find_endpoint_path_inv_def by blast
qed
lemma find_endpoint_arcs_0:
"find_endpoint_arcs_inv G False 0 v0 v1 v0 v1"
unfolding find_endpoint_arcs_inv_def by auto
lemma find_endpoint_path_lastE:
assumes "find_endpoint_path_inv G H len u v w x"
assumes ig: "IGraph_inv G" and lf: "loop_free (mk_graph G)"
assumes snp: "select_nodes_prop G H"
assumes "0 < len"
assumes u: "u ∈ set (ig_verts H)"
obtains p where "pre_digraph.awalk (mk_graph G) u ((u,v) # p) x"
and "progressing ((u,v) # p)"
and "set (pre_digraph.inner_verts (mk_graph G) ((u,v) # p)) ∩ set (ig_verts H) = {}"
and "len ≤ ig_verts_cnt G"
proof -
from ig and lf interpret pair_graph "mk_graph G"
by (rule IGraph_lf_imp_pg_mkg)
have [simp]: "verts3 (mk_graph G) = set (ig_verts H)"
using assms unfolding select_nodes_prop_def by (auto simp: mkg_simps)
from assms obtain q where q: "awalk u q x" "length q = len" "hd q = (u,v)"
and iv: "set (inner_verts q) ∩ verts3 (mk_graph G) = {}"
and prg: "progressing q"
unfolding find_endpoint_path_inv_def by auto
moreover then obtain q0 qs where "q = q0 # qs" using ‹0 < len› by (cases q) auto
moreover
have "len ≤ ig_verts_cnt G"
proof -
have ev_q: "awalk_verts u q = u # inner_verts q @ [x]"
unfolding inner_verts_conv[of q u] using q ‹q = q0 # qs› by auto
then have len_ev: "length (awalk_verts u q) = 2 + length (inner_verts q)"
by auto
have set_av: "set (awalk_verts u q) ⊆ pverts (mk_graph G)"
using q(1) by auto
from snp u have "u ∈ verts3 (mk_graph G)" by simp
moreover
with _ _ have "distinct (inner_verts q)"
using q(1) iv prg by (rule verts2_awalk_distinct) (auto simp: verts3_def)
ultimately
have "distinct (u # inner_verts q)" using iv by auto
moreover
have "set (u # inner_verts q) ⊆ pverts (mk_graph G)"
using ev_q set_av by auto
ultimately
have "length (u # inner_verts q) ≤ card (pverts (mk_graph G))"
by (metis card_mono distinct_card finite_set verts_mkg)
then have "length (awalk_verts u q) ≤ 1 + card (pverts (mk_graph G))"
by (simp add: len_ev)
then have "length q ≤ card (pverts (mk_graph G))"
by (auto simp: length_awalk_verts)
also have "… ≤ ig_verts_cnt G" by (auto simp: mkg_simps card_length)
finally show ?thesis by (simp add: q)
qed
ultimately show ?thesis by (intro that) auto
qed
lemma find_endpoint_path_last1:
assumes "find_endpoint_path_inv G H len u v w x"
assumes ig: "IGraph_inv G" and lf: "loop_free (mk_graph G)"
assumes snp: "select_nodes_prop G H"
assumes "0 < len"
assumes mem: "u ∈ set (ig_verts H)" "x ∈ set (ig_verts H)" "u ≠ x"
shows "∃p. pre_digraph.iapath (mk_graph G) u ((u,v) # p) x"
proof -
from ig and lf interpret pair_graph "mk_graph G"
by (rule IGraph_lf_imp_pg_mkg)
have [simp]: "verts3 (mk_graph G) = set (ig_verts H)"
"⋀x. x ∈ set (ig_verts H) ⟹ x ∈ pverts (mk_graph G)"
using assms unfolding select_nodes_prop_def by (auto simp: mkg_simps verts3_def)
show ?thesis
apply (rule find_endpoint_path_lastE[OF assms(1-5) mem(1)])
by (drule deg2_awalk_is_iapath[rotated 2]) (auto simp: mem)
qed
lemma find_endpoint_path_last2D:
assumes path: "find_endpoint_path_inv G H len u v w u"
assumes ig: "IGraph_inv G" and lf: "loop_free (mk_graph G)"
assumes snp: "select_nodes_prop G H"
assumes "0 < len"
assumes mem: "u ∈ set (ig_verts H)"
assumes iapath: "pre_digraph.iapath (mk_graph G) u ((u,v) # p) x"
shows False
proof -
from ig and lf interpret pair_graph "mk_graph G"
by (rule IGraph_lf_imp_pg_mkg)
have [simp]: "verts3 (mk_graph G) = set (ig_verts H)"
using assms unfolding select_nodes_prop_def by (auto simp: mkg_simps)
have V: "verts3 (mk_graph G) ⊆ verts3 (mk_graph G)" "verts3 (mk_graph G) ⊆ pverts (mk_graph G)"
using verts3_in_verts[where G="mk_graph G"] by auto
obtain q where walk_q: "awalk u ((u, v) # q) u" and
progress_q: "progressing ((u, v) # q)" and
iv_q: "set (inner_verts ((u, v) # q)) ∩ verts3 (mk_graph G) = {}"
by (rule find_endpoint_path_lastE[OF path ig lf snp ‹0 < len› mem]) auto
from iapath have walk_p: "awalk u ((u,v) # p) x" and
iv_p: "set (inner_verts ((u, v) # p)) ∩ verts3 (mk_graph G) = {}" and
uv_verts3: "u ∈ verts3 (mk_graph G)" "x ∈ verts3 (mk_graph G)"
unfolding gen_iapath_def apath_def by auto
from iapath have progress_p: "progressing ((u,v) # p)"
unfolding gen_iapath_def by (auto intro: apath_imp_progressing)
from V walk_q walk_p progress_q progress_p iv_q iv_p
have "(u,v) # q = (u,v) # p"
apply (rule same_awalk_by_common_arc[where e="(u,v)"])
using uv_verts3
apply auto
done
then show False
by (metis iapath apath_nonempty_ends gen_iapath_def awalk_nonempty_ends(2) walk_p walk_q)
qed
lemma find_endpoint_arcs_last:
assumes arcs: "find_endpoint_arcs_inv G False (length (ig_in_out_arcs G v1)) v0 v1 v0a v1a"
assumes path: "find_endpoint_path_inv G H len v_tail v_next v0 v1"
assumes ig: "IGraph_inv G" and lf: "loop_free (mk_graph G)"
assumes snp: "select_nodes_prop G H"
assumes mem: "v_tail ∈ set (ig_verts H)"
assumes "0 < len"
shows "¬ pre_digraph.iapath (mk_graph G) v_tail ((v_tail, v_next) # p) x"
proof
let "¬?A" = "?thesis"
assume ?A
interpret pair_graph "mk_graph G" using ig lf by (rule IGraph_lf_imp_pg_mkg)
have v3G_eq: "verts3 (mk_graph G) = set (ig_verts H)"
using assms unfolding select_nodes_prop_def by (auto simp: mkg_simps)
txt ‹
If no extending edge was found (as implied by @{thm arcs}), the last vertex of the walk
computed (as implied by @{thm path}) is of degree 1. Hence we consider all vertices
except the degree-2 nodes.
›
define V where "V = {v ∈ pverts (mk_graph G). in_degree (mk_graph G) v ≠ 2}"
have V: "verts3 (mk_graph G) ⊆ V" "V ⊆ pverts (mk_graph G)"
unfolding verts3_def V_def by auto
from ‹?A› have walk_p: "awalk v_tail ((v_tail, v_next) # p) x" and
progress_p: "progressing ((v_tail, v_next) # p)"
by (auto simp: gen_iapath_def apath_def intro: apath_imp_progressing)
have iapath_V_p: "gen_iapath V v_tail ((v_tail, v_next) # p) x"
proof -
{ fix u assume A: "u ∈ set (inner_verts ((v_tail, v_next) # p))"
then have "u ∈ pverts (mk_graph G)" using ‹?A›
by (auto 2 4 simp: set_inner_verts gen_iapath_def apath_Cons_iff dest: awalkI_apath)
with A ‹?A› inner_verts_min_degree[OF walk_p progress_p A] have "u ∉ V"
unfolding gen_iapath_def verts3_def V_def by auto }
with ‹?A› V show ?thesis by (auto simp: gen_iapath_def)
qed
have arcs_p: "(v_tail, v_next) ∈ set ((v_tail, v_next) # p)"
unfolding gen_iapath_def apath_def by auto
have id_x: "2 < in_degree (mk_graph G) x"
using ‹?A› unfolding gen_iapath_def verts3_def by auto
from arcs have edge_no_pr: "⋀e. e ∈ set (ig_in_out_arcs G v1) ⟹
v0 = ig_opposite G e v1" and"v0 = v0a" "v1 = v1a"
by (auto simp: find_endpoint_arcs_inv_def in_set_conv_nth)
have "{e ∈ parcs (mk_graph G). snd e = v1} ⊆ {(v0,v1)}" (is "?L ⊆ ?R")
proof
fix e assume "e ∈ ?L"
then have "fst e ≠ snd e" by (auto dest: no_loops)
moreover
from ‹e ∈ ?L› have "e ∈ set (ig_in_out_arcs G v1) ∨ (snd e, fst e) ∈ set (ig_in_out_arcs G v1)"
by (auto simp: mkg_simps ig_in_out_arcs_def symcl_def)
then have "v0 = ig_opposite G e v1 ∨ v0 = ig_opposite G (snd e, fst e) v1"
by (auto intro: edge_no_pr)
ultimately show "e ∈ ?R" using ‹e ∈ ?L› by (auto simp: ig_opposite_def)
qed
then have id_v1: "in_degree (mk_graph G) v1 ≤ card {(v0,v1)}"
unfolding in_degree_def in_arcs_def by (intro card_mono) auto
from path obtain q where walk_q: "awalk v_tail q v1" and
q_props: "length q = len" "hd q = (v_tail, v_next)" and
iv_q': "set (inner_verts q) ∩ verts3 (mk_graph G) = {}" and
progress_q: "progressing q"
by (auto simp: find_endpoint_path_inv_def v3G_eq)
then have "v1 ∈ pverts (mk_graph G)"
by (metis awalk_last_in_verts)
then have "v1 ∈ V" using id_v1 unfolding V_def by auto
{ fix u assume A: "u ∈ set (inner_verts q)"
then have "u ∈ set (pawalk_verts v_tail q)" using walk_q
by (auto simp: inner_verts_conv[where u=v_tail] awalk_def dest: in_set_butlastD list_set_tl)
then have "u ∈ pverts (mk_graph G)" using walk_q by auto
with A iv_q' inner_verts_min_degree[OF walk_q progress_q A] have "u ∉ V"
unfolding verts3_def V_def by auto }
then have iv_q: "set (inner_verts q) ∩ V = {}" by auto
have arcs_q: "(v_tail, v_next) ∈ set q"
using q_props ‹0 < len› by (cases q) auto
have neq: "v_tail ≠ v1"
using find_endpoint_path_last2D[OF _ ig lf snp ‹0 < len› ‹v_tail ∈ _› ‹?A›] path by auto
have in_V: "v_tail ∈ V" using iapath_V_p unfolding gen_iapath_def by auto
have iapath_V_q: "gen_iapath V v_tail q v1"
using V walk_q iv_q progress_q in_V ‹v1 ∈ V› neq by (rule deg2_awalk_is_iapath)
have "((v_tail, v_next) # p) = q"
using V iapath_V_p iapath_V_q arcs_p arcs_q
by (rule same_gen_iapath_by_common_arc)
then have "v1 = x" using walk_p walk_q by auto
then show False using id_v1 id_x by auto
qed
lemma find_endpoint_arcs_step1E:
assumes "find_endpoint_arcs_inv G False k v0 v1 v0' v1'"
assumes "ig_opposite G (ig_in_out_arcs G v1 ! k) v1' ≠ v0'"
obtains "v0 = v0'" "v1 = v1'" "find_endpoint_arcs_inv G True (Suc k) v0 v1 v1 (ig_opposite G (ig_in_out_arcs G v1 ! k) v1)"
using assms unfolding find_endpoint_arcs_inv_def
by (auto intro: less_SucI elim: less_SucE)
lemma find_endpoint_arcs_step2E:
assumes "find_endpoint_arcs_inv G False k v0 v1 v0' v1'"
assumes "ig_opposite G (ig_in_out_arcs G v1 ! k) v1' = v0'"
obtains "v0 = v0'" "v1 = v1'" "find_endpoint_arcs_inv G False (Suc k) v0 v1 v0 v1"
using assms unfolding find_endpoint_arcs_inv_def
by (auto intro: less_SucI elim: less_SucE)
lemma find_endpoint_path_step:
assumes path: "find_endpoint_path_inv G H len u v w x" and "0 < len"
assumes arcs: "find_endpoint_arcs_inv G True k w x w' x'"
"k ≤ length (ig_in_out_arcs G x)"
assumes ig: "IGraph_inv G"
assumes not_end: "x ∉ set (ig_verts H)"
shows "find_endpoint_path_inv G H (Suc len) u v w' x'"
proof -
interpret pg: pair_pseudo_graph "mk_graph G"
using ig by (auto intro: IGraph_imp_ppg_mkg)
from path obtain p where awalk: "pg.awalk u p x" and
p: "length p = len" "hd p = (u, v)" "last p = (w, x)" and
iv: "set (pg.inner_verts p) ∩ set (ig_verts H) = {}" and
progress: "progressing p"
by (auto simp: find_endpoint_path_inv_def)
define p' where "p' = p @ [(x,x')]"
from path have "x ∈ set (ig_verts G)"
by (metis awalk pg.awalk_last_in_verts verts_mkg)
with arcs have "iadj G x x'" "x = w'" "w ≠ x'"
using ‹x ∈ set (ig_verts G)› unfolding find_endpoint_arcs_inv_def
by (auto intro: iadj_io_edge)
then have "(x,x') ∈ parcs (mk_graph G)" "x' ∈ set (ig_verts G)"
using ig unfolding iadj_def by (auto simp: mkg_simps set_ig_arcs_imp_verts symcl_def)
then have "pg.awalk u p' x'"
unfolding p'_def using awalk by (auto simp: pg.awalk_simps mkg_simps)
moreover
have "length p' = Suc len" "hd p' = (u,v)" "last p' = (w',x')"
using ‹x = w'› ‹0 < len› p by (auto simp: p'_def)
moreover
have "set (pg.inner_verts p') ∩ set (ig_verts H) = {}"
using iv not_end p ‹0 < len› unfolding p'_def by (auto simp: pg.inner_verts_def)
moreover
{ fix ys y z zs have "p' ≠ ys @ [(y,z), (z,y)] @ zs"
proof
let "¬?A" = "?thesis"
assume ?A
from progress have "⋀zs. p ≠ ys @ (y,z) # (z,y) # zs"
by (auto simp: progressing_append_iff progressing_Cons)
with ‹?A› have "zs = []" unfolding p'_def by (cases zs rule: rev_cases) auto
then show False using ‹?A› using ‹w ≠ x'› ‹last p = (w,x)› unfolding p'_def by auto
qed }
then have "progressing p'" by (auto simp: progressing_def)
ultimately show ?thesis unfolding find_endpoint_path_inv_def by blast
qed
lemma no_loop_path:
assumes "u = v" and ig: "IGraph_inv G"
shows "¬ (∃p w. pre_digraph.iapath (mk_graph G) u ((u, v) # p) w)"
proof -
interpret ppg: pair_pseudo_graph "mk_graph G"
using ig by (rule IGraph_imp_ppg_mkg)
from ‹u = v› show ?thesis
by (auto simp: ppg.gen_iapath_def ppg.apath_Cons_iff)
(metis hd_in_set ppg.awalk_verts_non_Nil ppg.awhd_of_awalk pre_digraph.awalkI_apath)
qed
lemma (in find_endpoint_impl) find_endpoint_spec:
"∀σ. Γ ⊢⇩t ⦃σ. select_nodes_prop ´G ´H ∧ loop_free (mk_graph ´G) ∧ ´v_tail ∈ set (ig_verts ´H) ∧ iadj ´G ´v_tail ´v_next ∧ IGraph_inv ´G⦄
´R :== PROC find_endpoint(´G, ´H, ´v_tail, ´v_next)
⦃case ´R of None ⇒ ¬(∃p w. pre_digraph.iapath (mk_graph ⇗σ⇖G) ⇗σ⇖v_tail ((⇗σ⇖v_tail, ⇗σ⇖v_next) # p) w)
| Some w ⇒ (∃p. pre_digraph.iapath (mk_graph ⇗σ⇖G) ⇗σ⇖v_tail ((⇗σ⇖v_tail, ⇗σ⇖v_next) # p) w) ⦄"
apply vcg_step
apply (rewrite
at "whileAnno _ (named_loop ''path'') _ _"
in for (σ)
to "whileAnno _
⦃ find_endpoint_path_inv ´G ´H ´len ´v_tail ´v_next ´v0 ´v1
∧ ´v_tail = ⇗σ⇖v_tail ∧ ´v_next = ⇗σ⇖v_next ∧ ´G = ⇗σ⇖G ∧ ´H = ⇗σ⇖H
∧ 0 < ´ len
∧ ´v_tail ∈ set (ig_verts ´H) ∧ select_nodes_prop ´G ´H ∧ IGraph_inv ´G ∧ loop_free (mk_graph ´G) ⦄
(MEASURE Suc (ig_verts_cnt ´G) - ´len)
_"
annotate_named_loop_var)
apply (rewrite
at "whileAnno _ (named_loop ''arcs'') _ _"
in for (σ)
to "whileAnnoFix _
(λ(v0,v1,len). ⦃ find_endpoint_arcs_inv ´G ´found ´i v0 v1 ´v0 ´v1
∧ ´i ≤ length (ig_in_out_arcs ´G v1) ∧ ´io_arcs = ig_in_out_arcs ´G v1
∧ ´v_tail = ⇗σ⇖v_tail ∧ ´v_next = ⇗σ⇖v_next ∧ ´G = ⇗σ⇖G ∧ ´H = ⇗σ⇖ H
∧ ´len = len
∧ ´v_tail ∈ set (ig_verts ´H) ∧ select_nodes_prop ´G ´H ∧ IGraph_inv ´G ⦄)
(λ_. (MEASURE length ´io_arcs - ´i))
_"
annotate_named_loop_var_fix)
apply vcg
apply (fastforce simp: find_endpoint_path_first no_loop_path)
apply (match premises in "find_endpoint_path_inv _ _ _ _ _ v0 v1" for v0 v1
⇒ ‹rule exI[where x=v0], rule exI[where x=v1]›)
apply (fastforce simp: find_endpoint_arcs_last find_endpoint_arcs_0 find_endpoint_path_step elim: find_endpoint_path_lastE)
apply (fastforce elim: find_endpoint_arcs_step1E find_endpoint_arcs_step2E)
apply (fastforce dest: find_endpoint_path_last1 find_endpoint_path_last2D)
done
subsubsection ‹Procedure @{term contract}›
definition contract_iter_nodes_inv where
"contract_iter_nodes_inv G H k ≡
set (ig_arcs H) = (⋃i<k. {(u,v). u = (ig_verts H ! i) ∧ (∃p. pre_digraph.iapath (mk_graph G) u p v)})"
definition contract_iter_adj_inv :: "IGraph ⇒ IGraph ⇒ IGraph ⇒ nat ⇒ nat ⇒ bool" where
"contract_iter_adj_inv G H0 H u l ≡ (set (ig_arcs H) - ({u} × UNIV) = set (ig_arcs H0)) ∧
ig_verts H = ig_verts H0 ∧
(∀v. (u,v) ∈ set (ig_arcs H) ⟷
((∃j<l. ∃p. pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v)))"
lemma contract_iter_adj_invE:
assumes "contract_iter_adj_inv G H0 H u l"
obtains "set (ig_arcs H) - ({u} × UNIV) = set (ig_arcs H0)" "ig_verts H = ig_verts H0"
"⋀v. (u,v) ∈ set (ig_arcs H) ⟷ ((∃j<l. ∃p. pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v))"
using assms unfolding contract_iter_adj_inv_def by auto
lemma contract_iter_adj_inv_def':
"contract_iter_adj_inv G H0 H u l ⟷ (
set (ig_arcs H) - ({u} × UNIV) = set (ig_arcs H0)) ∧ ig_verts H = ig_verts H0 ∧
(∀v. ((∃j<l. ∃p. pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v) ⟶ (u,v) ∈ set (ig_arcs H)) ∧
((u,v) ∈ set (ig_arcs H) ⟶ ((∃j<l. ∃p. pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v))))"
unfolding contract_iter_adj_inv_def by metis
lemma select_nodes_prop_add_e[simp]:
"select_nodes_prop G (ig_add_e H u v) = select_nodes_prop G H"
by (simp add: select_nodes_prop_def mkg_simps)
lemma contract_iter_adj_inv_step1:
assumes "pair_pseudo_graph (mk_graph G)"
assumes ciai: "contract_iter_adj_inv G H0 H u l"
assumes iapath: "pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! l) u) # p) w"
shows "contract_iter_adj_inv G H0 (ig_add_e H u w) u (Suc l)"
proof -
interpret pair_pseudo_graph "mk_graph G" by fact
{ fix v j assume *: "j < Suc l" "∃p. iapath u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v"
then have "(u, v) ∈ set (ig_arcs (ig_add_e H u w))"
proof (cases "j < l")
case True with * ciai show ?thesis
by (auto simp: contract_iter_adj_inv_def)[]
next
case False with * have "j = l" by arith
with *(2) obtain q where **: "iapath u ((u, ig_opposite G (ig_in_out_arcs G u ! l) u) # q) v"
by metis
with iapath have "p = q"
using verts3_in_verts[where G="mk_graph G"]
by (auto elim: gen_iapath_same2E[rotated 2])
with ** iapath have "v = w"
by (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def elim: pre_digraph.awalk_nonempty_ends[rotated])
then show ?thesis by simp
qed }
moreover
{ fix v assume *: "(u,v) ∈ set (ig_arcs (ig_add_e H u w))"
have "(∃j<Suc l. ∃p. gen_iapath (verts3 (mk_graph G)) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v)"
proof cases
assume "v = w" then show ?thesis using iapath by auto
next
assume "v ≠ w" then show ?thesis using ciai *
unfolding contract_iter_adj_inv_def by (auto intro: less_SucI)
qed }
moreover
have "set (ig_arcs (ig_add_e H u w)) - ({u} × UNIV) = set (ig_arcs H0)"
"ig_verts (ig_add_e H u w) = ig_verts H0"
using ciai unfolding contract_iter_adj_inv_def by auto
ultimately
show ?thesis unfolding contract_iter_adj_inv_def by metis
qed
lemma contract_iter_adj_inv_step2:
assumes ciai: "contract_iter_adj_inv G H0 H u l"
assumes iapath: "⋀p w. ¬pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! l) u) # p) w"
shows "contract_iter_adj_inv G H0 H u (Suc l)"
proof -
{ fix v j assume *: "j < Suc l" "∃p. pre_digraph.iapath (mk_graph G) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v"
then have "(u, v) ∈ set (ig_arcs H)"
proof (cases "j < l")
case True with * ciai show ?thesis
by (auto simp: contract_iter_adj_inv_def)
next
case False with * have "j = l" by auto
with * show ?thesis using iapath by metis
qed }
moreover
{ fix v assume *: "(u,v) ∈ set (ig_arcs H)"
then have "(∃j<Suc l. ∃p. pre_digraph.gen_iapath (mk_graph G) (verts3 (mk_graph G)) u ((u, ig_opposite G (ig_in_out_arcs G u ! j) u) # p) v)"
using ciai unfolding contract_iter_adj_inv_def by (auto intro: less_SucI) }
moreover
have "set (ig_arcs H) - ({u} × UNIV) = set (ig_arcs H0)" "ig_verts H = ig_verts H0"
using ciai unfolding contract_iter_adj_inv_def by (auto simp:)
ultimately
show ?thesis unfolding contract_iter_adj_inv_def by metis
qed
definition contract_iter_adj_prop where
"contract_iter_adj_prop G H0 H u ≡ ig_verts H = ig_verts H0
∧ set (ig_arcs H) = set (ig_arcs H0) ∪ ({u} × {v. ∃p. pre_digraph.iapath (mk_graph G) u p v})"
lemma contract_iter_adj_propI:
assumes nodes: "contract_iter_nodes_inv G H i"
assumes ciai: "contract_iter_adj_inv G H H' u (length (ig_in_out_arcs G u))"
assumes u: "u = ig_verts H ! i"
shows "contract_iter_adj_prop G H H' u"
proof -
have "ig_verts H' = ig_verts H"
using ciai unfolding contract_iter_adj_inv_def by auto
moreover
have "set (ig_arcs H') ⊆ set (ig_arcs H) ∪({u} × {v. ∃p. pre_digraph.iapath (mk_graph G) u p v})"
using ciai unfolding contract_iter_adj_inv_def by auto
moreover
{ fix v p assume path: "pre_digraph.iapath (mk_graph G) u p v"
then obtain e es where "p = e # es" by (cases p) (auto simp: pre_digraph.gen_iapath_def)
then have "e ∈ parcs (mk_graph G)" using path
by (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def pre_digraph.awalk_def)
moreover
then obtain w where "e = (u,w)" using ‹p = e # es› path
by (cases e) (auto simp: pre_digraph.gen_iapath_def pre_digraph.apath_def pre_digraph.awalk_def pre_digraph.cas.simps)
ultimately
have "(u,w) ∈ set (ig_arcs G) ∨ (w,u) ∈ set (ig_arcs G)"
unfolding mk_graph_def by (auto simp: parcs_mk_symmetric mkg'_simps)
then obtain e' where H1: "e' = (u,w) ∨ e' = (w,u)" and "e' ∈ set (ig_arcs G)"
by auto
then have "e' ∈ set (ig_in_out_arcs G u)"
unfolding ig_in_out_arcs_def by auto
then obtain k where H2: "ig_in_out_arcs G u ! k = e'" "k < length (ig_in_out_arcs G u)"
by (auto simp: in_set_conv_nth)
have opp_e': "ig_opposite G e' u = w" using H1 unfolding ig_opposite_def by auto
have "(u,v) ∈ set (ig_arcs H')"
using ciai unfolding contract_iter_adj_inv_def'
apply safe
apply (erule allE[where x=v])
apply safe
apply (erule notE)
apply (rule exI[where x=k])
apply (simp add: H2 opp_e')
using path ‹e = (u,w)› ‹p = e # es› by auto }
then have "set (ig_arcs H) ∪({u} × {v. ∃p. pre_digraph.iapath (mk_graph G) u p v}) ⊆ set (ig_arcs H')"
using ciai unfolding contract_iter_adj_inv_def by auto
ultimately
show ?thesis unfolding contract_iter_adj_prop_def by blast
qed
lemma contract_iter_nodes_inv_step:
assumes nodes: "contract_iter_nodes_inv G H i"
assumes adj: "contract_iter_adj_inv G H H' (ig_verts H ! i) (length (ig_in_out_arcs G (ig_verts H ! i)))"
assumes snp: "select_nodes_prop G H"
shows "contract_iter_nodes_inv G H' (Suc i)"
proof -
have ciap: "contract_iter_adj_prop G H H' (ig_verts H ! i)"
using nodes adj by (rule contract_iter_adj_propI) simp
then have ie_H': "set (ig_arcs H') = set (ig_arcs H) ∪ {(u,v). u = ig_verts H' ! i ∧ (∃p. pre_digraph.gen_iapath (mk_graph G) (verts3 (mk_graph G)) u p v)}"
and [simp]: "ig_verts H' = ig_verts H"
unfolding contract_iter_adj_prop_def by auto
have ie_H: "set (ig_arcs H) = (⋃ j<i. {(u, v). u = ig_verts H' ! j ∧ (∃p. pre_digraph.gen_iapath (mk_graph G) (verts3 (mk_graph G)) u p v)})"
using nodes unfolding contract_iter_nodes_inv_def by simp
have *: "⋀S k. (⋃i < Suc k. S i) = (⋃i < k. S i) ∪ S k"
by (metis UN_insert lessThan_Suc sup_commute)
show ?thesis by (simp only: contract_iter_nodes_inv_def ie_H ie_H' *)
qed
lemma contract_iter_nodes_0:
assumes "set (ig_arcs H) = {}" shows "contract_iter_nodes_inv G H 0"
using assms unfolding contract_iter_nodes_inv_def by simp
lemma contract_iter_adj_0:
assumes nodes: "contract_iter_nodes_inv G H i"
assumes i: "i < ig_verts_cnt H"
shows "contract_iter_adj_inv G H H (ig_verts H ! i) 0"
using assms distinct_ig_verts
unfolding contract_iter_adj_inv_def contract_iter_nodes_inv_def
by (auto simp: distinct_conv_nth)
lemma snp_vertexes:
assumes "select_nodes_prop G H" "u ∈ set (ig_verts H)" shows "u ∈ set (ig_verts G)"
using assms unfolding select_nodes_prop_def by (auto simp: verts3_def mkg_simps)
lemma igraph_ig_add_eI:
assumes "IGraph_inv G"
assumes "u ∈ set (ig_verts G)" "v ∈ set (ig_verts G)"
shows "IGraph_inv (ig_add_e G u v)"
using assms unfolding IGraph_inv_def by auto
lemma snp_iapath_ends_in:
assumes "select_nodes_prop G H"
assumes "pre_digraph.iapath (mk_graph G) u p v"
shows "u ∈ set (ig_verts H)" "v ∈ set (ig_verts H)"
using assms unfolding pre_digraph.gen_iapath_def select_nodes_prop_def verts3_def
by (auto simp: mkg_simps)
lemma contract_iter_nodes_last:
assumes nodes: "contract_iter_nodes_inv G H (ig_verts_cnt H)"
assumes snp: "select_nodes_prop G H"
assumes igraph: "IGraph_inv G"
shows "mk_graph' H = contr_graph (mk_graph G)" (is ?t1)
and "symmetric (mk_graph' H)" (is ?t2)
proof -
interpret ppg_mkG: pair_pseudo_graph "mk_graph G"
using igraph by (rule IGraph_imp_ppg_mkg)
{ fix u v p assume "pre_digraph.iapath (mk_graph G) u p v"
then have "∃p. pre_digraph.iapath (mk_graph G) v p u"
using ppg_mkG.gen_iapath_rev_path[where u=u and v=v, symmetric] by auto }
then have ie_sym: "⋀u v. (∃p. pre_digraph.iapath (mk_graph G) u p v) ⟷ (∃p. pre_digraph.iapath (mk_graph G) v p u)"
by auto
from nodes have "set (ig_arcs H) = {(u, v). u ∈ set (ig_verts H) ∧ (∃p. pre_digraph.gen_iapath (mk_graph G) (verts3 (mk_graph G)) u p v)}"
unfolding contract_iter_nodes_inv_def by (auto simp: in_set_conv_nth)
then have *: "set (ig_arcs H) = {(u,v). (∃p. pre_digraph.iapath (mk_graph G) u p v)}"
using snp by (auto simp: snp_iapath_ends_in(1))
then have **: "set (ig_arcs H) = (λ(a,b). (b,a)) ` {(u,v). (∃p. pre_digraph.iapath (mk_graph G) u p v)}"
using ie_sym by fastforce
have sym: "symmetric (mk_graph' H)"
unfolding symmetric_conv by (auto simp: mkg'_simps * ie_sym)
have "pverts (mk_graph' H) = verts3 (mk_graph G)"
using snp unfolding select_nodes_prop_def by (simp add: mkg_simps mkg'_simps)
moreover
have "parcs (mk_graph' H) = {(u,v). (∃p. ppg_mkG.iapath u p v)}"
using * by (auto simp: mkg_simps mkg'_simps)
ultimately show ?t1 ?t2
using snp sym unfolding gen_contr_graph_def select_nodes_prop_def by auto
qed
lemma (in contract_impl) contract_spec:
"∀σ. Γ ⊢⇩t ⦃σ. select_nodes_prop ´G ´H ∧ IGraph_inv ´G ∧ loop_free (mk_graph ´G) ∧ IGraph_inv ´H ∧ set (ig_arcs ´H) = {}⦄
´R :== PROC contract(´G, ´H)
⦃´G = ⇗σ⇖G ∧ mk_graph' ´R = contr_graph (mk_graph ´G) ∧ symmetric (mk_graph' ´R) ∧ IGraph_inv ´R⦄"
apply vcg_step
apply (rewrite
at "whileAnno _ (named_loop ''iter_nodes'') _ _"
in for (σ)
to "whileAnno _
⦃contract_iter_nodes_inv ´G ´H ´i
∧ select_nodes_prop ´G ´H ∧ ´i ≤ ig_verts_cnt ´H ∧ IGraph_inv ´G ∧ loop_free (mk_graph ´G)
∧ IGraph_inv ´H ∧ ´G = ⇗σ⇖G⦄
(MEASURE ig_verts_cnt ´H - ´i)
_"
annotate_named_loop_var)
apply (rewrite
at "whileAnno _ (named_loop ''iter_adj'') _ _"
in for (σ)
to "whileAnnoFix _
(λ(H, u, i). ⦃contract_iter_adj_inv ´G H ´H u ´j
∧ select_nodes_prop ´G ´H ∧ ´u = u ∧ ´j ≤ length (ig_in_out_arcs ´G ´u) ∧ ´io_arcs = ig_in_out_arcs ´G ´u
∧ u ∈ set (ig_verts ´H) ∧ IGraph_inv ´G ∧ loop_free (mk_graph ´G) ∧ IGraph_inv ´H ∧ ´G = ⇗σ⇖G ∧ ´i = i⦄)
(λ_. (MEASURE length ´io_arcs - ´j))
_"
annotate_named_loop_var_fix)
apply vcg
apply (fastforce simp: contract_iter_nodes_0)
apply (match premises in "select_nodes_prop _ H" for H ⇒ ‹rule exI[where x=H]›)
apply (fastforce simp: contract_iter_adj_0 contract_iter_nodes_inv_step elim: contract_iter_adj_invE)
apply (fastforce simp: contract_iter_adj_inv_step2 contract_iter_adj_inv_step1
IGraph_imp_ppg_mkg igraph_ig_add_eI snp_iapath_ends_in iadj_io_edge snp_vertexes)
apply (fastforce simp: not_less intro: contract_iter_nodes_last)
done
subsubsection ‹Procedure @{term is_K33}›
definition is_K33_colorize_inv :: "IGraph ⇒ ig_vertex ⇒ nat ⇒ (ig_vertex ⇒ bool) ⇒ bool" where
"is_K33_colorize_inv G u k blue ≡ ∀v ∈ set (ig_verts G). blue v ⟷
(∃i < k. v = ig_opposite G (ig_in_out_arcs G u ! i) u)"
definition is_K33_component_size_inv :: "IGraph ⇒ nat ⇒ (ig_vertex ⇒ bool) ⇒ nat ⇒ bool" where
"is_K33_component_size_inv G k blue cnt ≡ cnt = card {i. i < k ∧ blue (ig_verts G ! i)}"
definition is_K33_outer_inv :: "IGraph ⇒ nat ⇒ (ig_vertex ⇒ bool) ⇒ bool" where
"is_K33_outer_inv G k blue ≡ ∀i < k. ∀v ∈ set (ig_verts G).
blue (ig_verts G ! i) = blue v ⟷ (ig_verts G ! i, v) ∉ set (ig_arcs G)"
definition is_K33_inner_inv :: "IGraph ⇒ nat ⇒ nat ⇒ (ig_vertex ⇒ bool) ⇒ bool" where
"is_K33_inner_inv G k l blue ≡ ∀j < l.
blue (ig_verts G ! k) = blue (ig_verts G ! j) ⟷ (ig_verts G ! k, ig_verts G ! j) ∉ set (ig_arcs G)"
lemma is_K33_colorize_0: "is_K33_colorize_inv G u 0 (λ_. False)"
unfolding is_K33_colorize_inv_def by auto
lemma is_K33_component_size_0: "is_K33_component_size_inv G 0 blue 0"
unfolding is_K33_component_size_inv_def by auto
lemma is_K33_outer_0: "is_K33_outer_inv G 0 blue"
unfolding is_K33_outer_inv_def by auto
lemma is_K33_inner_0: "is_K33_inner_inv G k 0 blue"
unfolding is_K33_inner_inv_def by auto
lemma is_K33_colorize_last:
assumes "u ∈ set (ig_verts G)"
shows "is_K33_colorize_inv G u (length (ig_in_out_arcs G u)) blue
= (∀v ∈ set (ig_verts G). blue v ⟷ iadj G u v)" (is "?L = ?R")
proof -
{ fix v
have "(∃i<length (ig_in_out_arcs G u). v = ig_opposite G (ig_in_out_arcs G u ! i) u)
⟷ (∃e ∈ set (ig_in_out_arcs G u). v = ig_opposite G e u)" (is "?A ⟷ _")
by auto (auto simp: in_set_conv_nth)
also have "… ⟷ iadj G u v"
using assms by (force simp: iadj_io_edge ig_opposite_simps dest: iadjD)
finally have "?A ⟷ iadj G u v" . }
then show ?thesis unfolding is_K33_colorize_inv_def by auto
qed
lemma is_K33_component_size_last:
assumes "k = ig_verts_cnt G"
shows "is_K33_component_size_inv G k blue cnt ⟷ card {u ∈ set (ig_verts G). blue u} = cnt"
proof -
have *: "{u ∈ set (ig_verts G). blue u} = (λn. ig_verts G ! n) ` {i. i < ig_verts_cnt G ∧ blue (ig_verts G ! i)}"
by (auto simp: in_set_conv_nth )
have "inj_on (λn. ig_verts G ! n) {i. i < ig_verts_cnt G ∧ blue (ig_verts G ! i)}"
using distinct_ig_verts by (auto simp: nth_eq_iff_index_eq intro: inj_onI)
with assms show ?thesis
unfolding * is_K33_component_size_inv_def
by (auto intro: card_image)
qed
lemma is_K33_outer_last:
"is_K33_outer_inv G (ig_verts_cnt G) blue ⟷ (∀u ∈ set (ig_verts G). ∀v ∈ set (ig_verts G).
blue u = blue v ⟷ (u,v) ∉ set (ig_arcs G))"
unfolding is_K33_outer_inv_def by (simp add: All_set_ig_verts)
lemma is_K33_inner_last:
"is_K33_inner_inv G k (ig_verts_cnt G) blue ⟷ (∀v ∈ set (ig_verts G).
blue (ig_verts G ! k) = blue v ⟷ (ig_verts G ! k, v) ∉ set (ig_arcs G))"
unfolding is_K33_inner_inv_def by (simp add: All_set_ig_verts)
lemma is_K33_colorize_step:
fixes G u i blue
assumes colorize: "is_K33_colorize_inv G u k blue"
shows " is_K33_colorize_inv G u (Suc k) (blue (ig_opposite G (ig_in_out_arcs G u ! k) u := True))"
using assms by (auto simp: is_K33_colorize_inv_def elim: less_SucE intro: less_SucI)
lemma is_K33_component_size_step1:
assumes comp:"is_K33_component_size_inv G k blue blue_cnt"
assumes blue: "blue (ig_verts G ! k)"
shows "is_K33_component_size_inv G (Suc k) blue (Suc blue_cnt)"
proof -
have "{i. i < Suc k ∧ blue (ig_verts G ! i)}
= insert k {i. i < k ∧ blue (ig_verts G ! i)}"
using blue by auto
with comp show ?thesis
unfolding is_K33_component_size_inv_def by auto
qed
lemma is_K33_component_size_step2:
assumes comp:"is_K33_component_size_inv G k blue blue_cnt"
assumes blue: "¬blue (ig_verts G ! k)"
shows "is_K33_component_size_inv G (Suc k) blue blue_cnt"
proof -
have "{i. i < Suc k ∧ blue (ig_verts G ! i)} = {i. i < k ∧ blue (ig_verts G ! i)}"
using blue by (auto elim: less_SucE)
with comp show ?thesis
unfolding is_K33_component_size_inv_def by auto
qed
lemma is_K33_outer_step:
assumes "is_K33_outer_inv G i blue"
assumes "is_K33_inner_inv G i (ig_verts_cnt G) blue"
shows "is_K33_outer_inv G (Suc i) blue"
using assms unfolding is_K33_outer_inv_def is_K33_inner_last
by (auto intro: less_SucI elim: less_SucE)
lemma is_K33_inner_step:
assumes "is_K33_inner_inv G i j blue"
assumes "(blue (ig_verts G ! i) = blue (ig_verts G ! j)) ⟷ (ig_verts G ! i, ig_verts G ! j) ∉ set (ig_arcs G)"
shows "is_K33_inner_inv G i (Suc j) blue"
using assms by (auto simp: is_K33_inner_inv_def elim: less_SucE)
lemma K33_mkg'I:
fixes G col cnt
defines "u ≡ ig_verts G ! 0"
assumes ig: "IGraph_inv G"
assumes iv_cnt: "ig_verts_cnt G = 6" and c1_cnt: "cnt = 3"
assumes colorize: "is_K33_colorize_inv G u (length (ig_in_out_arcs G u)) blue"
assumes comp: "is_K33_component_size_inv G (ig_verts_cnt G) blue cnt"
assumes outer: "is_K33_outer_inv G (ig_verts_cnt G) blue"
shows "K⇘3,3⇙ (mk_graph' G)"
proof -
have "u ∈ set (ig_verts G)" unfolding u_def using iv_cnt by auto
then have "(∀v∈set (ig_verts G). blue v ⟷ iadj G u v)"
using colorize by (rule is_K33_colorize_last[THEN iffD1])
define U V where "U = {u ∈ set (ig_verts G). ¬blue u}" and "V = {v ∈ set (ig_verts G). blue v}"
then have UV_set: "U ⊆ set (ig_verts G)" "V ⊆ set (ig_verts G)" "U ∪ V = set (ig_verts G)" "U ∩ V = {}"
and fin_UV: "finite U" "finite V" by auto
have card_verts: "card (set (ig_verts G)) = 6"
using iv_cnt distinct_ig_verts by (simp add: distinct_card)
from ig comp c1_cnt have "card V = 3" by (simp add: is_K33_component_size_last V_def)
moreover have "card (U ∪ V) = 6" using UV_set distinct_ig_verts iv_cnt
by (auto simp: distinct_card)
ultimately have "card U = 3"
by (simp add: card_Un_disjoint[OF fin_UV UV_set(4)])
note cards = ‹card V = 3› ‹card U = 3› card_verts
from is_K33_outer_last[THEN iffD1, OF outer]
have "(∀u∈U. ∀v∈V. (u, v) ∈ set (ig_arcs G) ∧ (v, u) ∈ set (ig_arcs G))
∧ (∀u∈U. ∀u'∈U. (u, u') ∉ set (ig_arcs G))
∧ (∀v∈V. ∀v'∈V. (v, v') ∉ set (ig_arcs G))"
unfolding U_def V_def by auto
then have "U × V ⊆ set (ig_arcs G)" "V × U ⊆ set (ig_arcs G)"
"U × U ∩ set (ig_arcs G) = {}" "V × V ∩ set (ig_arcs G) = {}"
by auto
moreover have "set (ig_arcs G) ⊆ (U ∪ V) × (U ∪ V)"
unfolding ‹U ∪ V = _› by (auto simp: ig set_ig_arcs_verts)
ultimately
have conn: "set (ig_arcs G) = U × V ∪ V × U"
by blast
interpret ppg_mkg': pair_fin_digraph "mk_graph' G"
using ig by (auto intro: IGraph_imp_ppd_mkg')
show ?thesis
unfolding complete_bipartite_digraph_pair_def mkg'_simps
using cards UV_set conn by simp metis
qed
lemma K33_mkg'E:
assumes K33: "K⇘3,3⇙ (mk_graph' G)"
assumes ig: "IGraph_inv G"
assumes colorize: "is_K33_colorize_inv G u (length (ig_in_out_arcs G u)) blue"
and u: "u ∈ set (ig_verts G)"
obtains "is_K33_component_size_inv G (ig_verts_cnt G) blue 3"
"is_K33_outer_inv G (ig_verts_cnt G) blue"
proof -
from K33 obtain U V where
verts_G: "set (ig_verts G) = U ∪ V" and
arcs_G: "set (ig_arcs G) = U × V ∪ V × U" and
disj_UV: "U ∩ V = {}" and
card: "card U = 3" "card V = 3"
unfolding complete_bipartite_digraph_pair_def mkg'_simps by auto
from colorize u have col_adj: "⋀v. v ∈ set (ig_verts G) ⟹ blue v ⟷ iadj G u v"
using is_K33_colorize_last by auto
have iadj_conv: "⋀u v. iadj G u v ⟷ (u,v) ∈ U × V ∪ V × U"
unfolding iadj_def arcs_G by auto
{ assume "u ∈ U"
then have "V = {v ∈ set (ig_verts G). blue v}"
using disj_UV by (auto simp: iadj_conv verts_G col_adj)
then have "is_K33_component_size_inv G (ig_verts_cnt G) blue 3"
using ig card by (simp add: is_K33_component_size_last)
moreover
have "⋀v. v ∈ U ∪ V ⟹ blue v ⟷ v ∈ V"
using ‹u ∈ U› disj_UV by (auto simp: verts_G col_adj iadj_conv)
then have "is_K33_outer_inv G (ig_verts_cnt G) blue"
using ‹U ∩ V = {}› by (subst is_K33_outer_last) (auto simp: arcs_G verts_G )
ultimately have ?thesis by (rule that) }
moreover
{ assume "u ∈ V"
then have "U = {v ∈ set (ig_verts G). blue v}"
using disj_UV by (auto simp: iadj_conv verts_G col_adj)
then have "is_K33_component_size_inv G (ig_verts_cnt G) blue 3"
using ig card by (simp add: is_K33_component_size_last)
moreover
have "⋀v. v ∈ U ∪ V ⟹ blue v ⟷ v ∈ U"
using ‹u ∈ V› disj_UV by (auto simp: verts_G col_adj iadj_conv)
then have "is_K33_outer_inv G (ig_verts_cnt G) blue"
using ‹U ∩ V = {}› by (subst is_K33_outer_last) (auto simp: arcs_G verts_G )
ultimately have ?thesis by (rule that) }
ultimately show ?thesis using verts_G u by blast
qed
lemma K33_card:
assumes "K⇘3,3⇙ (mk_graph' G)" shows "ig_verts_cnt G = 6"
proof -
from assms have "card (verts (mk_graph' G)) = 6"
unfolding complete_bipartite_digraph_pair_def by (auto simp: card_Un_disjoint)
then show ?thesis
using distinct_ig_verts by (auto simp: mkg'_simps distinct_card)
qed
abbreviation (input) is_K33_colorize_inv_last :: "IGraph ⇒ (ig_vertex ⇒ bool) ⇒ bool" where
"is_K33_colorize_inv_last G blue ≡ is_K33_colorize_inv G (ig_verts G ! 0) (length (ig_in_out_arcs G (ig_verts G ! 0))) blue"
abbreviation (input) is_K33_component_size_inv_last :: "IGraph ⇒ (ig_vertex ⇒ bool) ⇒ bool" where
"is_K33_component_size_inv_last G blue ≡ is_K33_component_size_inv G (ig_verts_cnt G) blue 3"
lemma is_K33_outerD:
assumes "is_K33_outer_inv G (ig_verts_cnt G) blue"
assumes "i < ig_verts_cnt G" "j < ig_verts_cnt G"
shows "(blue (ig_verts G ! i) = blue (ig_verts G ! j)) ⟷ (ig_verts G ! i, ig_verts G ! j) ∉ set (ig_arcs G)"
using assms unfolding is_K33_outer_last by auto
lemma (in is_K33_impl) is_K33_spec:
"∀σ. Γ ⊢⇩t ⦃σ. IGraph_inv ´G ∧ symmetric (mk_graph' ´G)⦄
´R :== PROC is_K33(´G)
⦃ ´G = ⇗σ⇖G ∧ ´R = K⇘3,3⇙(mk_graph' ´G) ⦄"
apply vcg_step
apply (rewrite
at "whileAnno _ (named_loop ''colorize'') _ _"
in for (σ)
to "whileAnno _
⦃ is_K33_colorize_inv ´G ´u ´i ´blue ∧ ´i ≤ length ´io_arcs
∧ ´io_arcs = ig_in_out_arcs ´G ´u ∧ ´u = ig_verts ´G ! 0 ∧ ´G = ⇗σ⇖G ∧ IGraph_inv ´G
∧ ´u = ig_verts ´G ! 0 ∧ ig_verts_cnt ´G = 6⦄
(MEASURE length ´io_arcs - ´i)
_"
annotate_named_loop_var)
apply (rewrite
at "whileAnno _ (named_loop ''component_size'') _ _"
in for (σ)
to "whileAnnoFix _
(λblue. ⦃ is_K33_component_size_inv ´G ´i ´blue ´blue_cnt
∧ ´i ≤ ig_verts_cnt ´G ∧ ´blue = blue ∧ ´G = ⇗σ⇖G ∧ IGraph_inv ´G
∧ ig_verts_cnt ´G = 6 ∧ is_K33_colorize_inv_last ´G ´blue ⦄)
(λ_. (MEASURE ig_verts_cnt ´G - ´i))
_"
annotate_named_loop_var_fix)
apply (rewrite
at "whileAnno _ (named_loop ''connected_outer'') _ _"
in for (σ)
to "whileAnnoFix _
(λblue. ⦃ is_K33_outer_inv ´G ´i ´blue ∧ ´i ≤ ig_verts_cnt ´G
∧ ´blue = blue ∧ ´G = ⇗σ⇖G ∧ IGraph_inv ´G
∧ ig_verts_cnt ´G = 6 ∧ is_K33_colorize_inv_last ´G ´blue ∧ is_K33_component_size_inv_last ´G ´blue ⦄)
(λ_. (MEASURE ig_verts_cnt ´G - ´i))
_"
annotate_named_loop_var_fix)
apply (rewrite
at "whileAnno _ (named_loop ''connected_inner'') _ _"
in for (σ)
to "whileAnnoFix _
(λ(i,blue). ⦃ is_K33_inner_inv ´G ´i ´j ´blue ∧ ´j ≤ ig_verts_cnt ´G
∧ ´i = i ∧´i < ig_verts_cnt ´G ∧ ´blue = blue ∧ ´G = ⇗σ⇖G ∧ IGraph_inv ´G ∧ ´u = ig_verts ´G ! ´i
∧ ig_verts_cnt ´G = 6 ∧ is_K33_colorize_inv_last ´G ´blue ∧ is_K33_component_size_inv_last ´G ´blue ⦄)
(λ_. (MEASURE ig_verts_cnt ´G - ´j))
_"
annotate_named_loop_var_fix)
apply vcg
apply (fastforce simp: is_K33_colorize_0 is_K33_component_size_0 is_K33_outer_0 is_K33_component_size_last
elim: K33_mkg'E dest: K33_card intro: K33_mkg'I)
apply (fastforce simp add: is_K33_colorize_step)
apply (fastforce simp: is_K33_colorize_0 is_K33_component_size_0 is_K33_outer_0 is_K33_component_size_last
elim: K33_mkg'E intro: K33_mkg'I)
apply (fastforce simp: is_K33_component_size_step1 is_K33_component_size_step2)
apply (fastforce simp: is_K33_inner_0 is_K33_outer_step)
apply (simp only: simp_thms)
apply (intro conjI allI impI notI)
apply (fastforce elim: K33_mkg'E dest: is_K33_outerD)
apply (fastforce elim: K33_mkg'E dest: is_K33_outerD)
apply (simp add: is_K33_inner_step; fail)
apply linarith
done
subsubsection ‹Procedure @{term is_K5}›
definition
"is_K5_outer_inv G k ≡ ∀i<k. ∀v ∈ set (ig_verts G). ig_verts G ! i ≠ v
⟷ (ig_verts G ! i, v) ∈ set (ig_arcs G)"
definition
"is_K5_inner_inv G k l ≡ ∀j < l. ig_verts G ! k ≠ ig_verts G ! j
⟷ (ig_verts G ! k, ig_verts G ! j) ∈ set (ig_arcs G)"
lemma K5_card:
assumes "K⇘5⇙ (mk_graph' G)" shows "ig_verts_cnt G = 5"
using assms distinct_ig_verts unfolding complete_digraph_pair_def
by (auto simp add: mkg'_simps distinct_card)
lemma is_K5_inner_0: "is_K5_inner_inv G k 0"
unfolding is_K5_inner_inv_def by auto
lemma is_K5_inner_last:
assumes "l = ig_verts_cnt G"
shows "is_K5_inner_inv G k l ⟷ (∀v ∈ set (ig_verts G). ig_verts G ! k ≠ v
⟷ (ig_verts G ! k, v) ∈ set (ig_arcs G))"
proof -
have "⋀v. v ∈ set (ig_verts G) ⟹ ∃j<ig_verts_cnt G. ig_verts G ! j = v"
by (auto simp: in_set_conv_nth)
then show ?thesis using assms unfolding is_K5_inner_inv_def
by auto metis
qed
lemma is_K5_outer_step:
assumes "is_K5_outer_inv G k"
assumes "is_K5_inner_inv G k (ig_verts_cnt G)"
shows "is_K5_outer_inv G (Suc k)"
using assms unfolding is_K5_outer_inv_def
by (auto simp: is_K5_inner_last elim: less_SucE)
lemma is_K5_outer_last:
assumes "is_K5_outer_inv G (ig_verts_cnt G)"
assumes "IGraph_inv G" "ig_verts_cnt G = 5" "symmetric (mk_graph' G)"
shows "K⇘5⇙ (mk_graph' G)"
proof -
interpret ppg_mkg': pair_fin_digraph "mk_graph' G"
using assms(2) by (auto intro: IGraph_imp_ppd_mkg')
have "⋀u v. (u, v) ∈ set (ig_arcs G) ⟹ u ≠ v"
using assms(1,2) unfolding is_K5_outer_inv_def ig_verts_cnt_def
by (metis in_set_conv_nth set_ig_arcs_verts(2))
then interpret ppg_mkg': pair_graph "(mk_graph' G)"
using assms(4) by unfold_locales (auto simp: mkg'_simps arc_to_ends_def)
have "⋀a b. a ∈ pverts (mk_graph' G) ⟹
b ∈ pverts (mk_graph' G) ⟹ a ≠ b ⟹ (a, b) ∈ parcs (mk_graph' G)"
using assms(1) unfolding is_K5_outer_inv_def mkg'_simps
by (metis in_set_conv_nth ig_verts_cnt_def)
moreover
have "card (pverts (mk_graph' G)) = 5"
using ‹ig_verts_cnt G = 5› distinct_ig_verts by (auto simp: mkg'_simps distinct_card)
ultimately
show ?thesis
unfolding complete_digraph_pair_def
by (auto dest: ppg_mkg'.in_arcsD1 ppg_mkg'.in_arcsD2 ppg_mkg'.no_loops')
qed
lemma is_K5_inner_step:
assumes "is_K5_inner_inv G k l"
assumes "k < ig_verts_cnt G"
assumes "k ≠ l ⟷ (ig_verts G ! k, ig_verts G ! l) ∈ set (ig_arcs G)"
shows "is_K5_inner_inv G k (Suc l)"
using assms distinct_ig_verts unfolding is_K5_inner_inv_def
apply (auto elim: less_SucE)
by (metis (opaque_lifting, no_types) Suc_lessD less_SucE less_trans_Suc linorder_neqE_nat nth_eq_iff_index_eq)
lemma iK5E:
assumes "K⇘5⇙ (mk_graph' G)"
obtains "ig_verts_cnt G = 5" "⟦i < ig_verts_cnt G; j < ig_verts_cnt G⟧ ⟹ i ≠ j ⟷ (ig_verts G ! i, ig_verts G ! j) ∈ set (ig_arcs G)"
proof
show "ig_verts_cnt G = 5"
"i < ig_verts_cnt G ⟹ j < ig_verts_cnt G ⟹
(i ≠ j) = ((ig_verts G ! i, ig_verts G ! j) ∈ set (ig_arcs G))"
using assms distinct_ig_verts
by (auto simp: complete_digraph_pair_def mkg'_simps distinct_card nth_eq_iff_index_eq)
qed
lemma (in is_K5_impl) is_K5_spec:
"∀σ. Γ ⊢⇩t ⦃σ. IGraph_inv ´G ∧ symmetric (mk_graph' ´G)⦄
´R :== PROC is_K5(´G)
⦃ ´G = ⇗σ⇖G ∧ ´R = K⇘5⇙(mk_graph' ´G) ⦄"
apply vcg_step
apply (rewrite
at "whileAnno _ (named_loop ''outer_loop'') _ _"
in for (σ)
to "whileAnno _
⦃ is_K5_outer_inv ´G ´i ∧´i ≤ 5 ∧ IGraph_inv ´G ∧ symmetric (mk_graph' ´G) ∧ ´G = ⇗σ⇖G ∧ ig_verts_cnt ´G = 5 ⦄
(MEASURE 5 - ´i)
_"
annotate_named_loop_var)
apply (rewrite
at "whileAnno _ (named_loop ''inner_loop'') _ _"
in for (σ)
to "whileAnnoFix _
(λi. ⦃ is_K5_inner_inv ´G ´i ´j
∧ ´j ≤ 5 ∧ ´i < 5 ∧ IGraph_inv ´G ∧ symmetric (mk_graph' ´G) ∧ ´G = ⇗σ⇖G ∧ ´i = i
∧ ig_verts_cnt ´G = 5 ∧ ´u = ig_verts ´G ! ´i⦄)
(λ_. (MEASURE 5 - ´j))
_"
annotate_named_loop_var_fix)
apply vcg
apply (fastforce simp: is_K5_outer_inv_def intro: K5_card)
apply (fastforce simp add: is_K5_inner_0 is_K5_outer_step)
apply (fastforce simp: is_K5_inner_step elim: iK5E)
apply (fastforce simp: is_K5_outer_last)
done
subsubsection ‹Soundness of the Checker›
lemma planar_theorem:
assumes "pair_pseudo_graph G" "pair_pseudo_graph K"
and "subgraph K G"
and "K⇘3,3⇙ (contr_graph K) ∨ K⇘5⇙ (contr_graph K)"
shows "¬kuratowski_planar G"
using assms
by (auto dest: pair_pseudo_graph.kuratowski_contr)
definition witness :: "'a pair_pre_digraph ⇒ 'a pair_pre_digraph ⇒ bool" where
"witness G K ≡ loop_free K ∧ pair_pseudo_graph K ∧ subgraph K G
∧ (K⇘3,3⇙ (contr_graph K) ∨ K⇘5⇙ (contr_graph K))"
lemma "witness (mk_graph G) (mk_graph K) ⟷ pair_pre_digraph.certify (mk_graph G) (mk_graph K) ∧ loop_free (mk_graph K)"
by (auto simp: witness_def pair_pre_digraph.certify_def Let_def wf_digraph_wp_iff wellformed_pseudo_graph_mkg)
lemma pwd_imp_ppg_mkg:
assumes "pair_wf_digraph (mk_graph G)"
shows "pair_pseudo_graph (mk_graph G)"
proof -
interpret pair_wf_digraph "mk_graph G" by fact
show ?thesis
apply unfold_locales
apply (auto simp: mkg_simps finite_symcl_iff)
apply (auto simp: mk_graph_def symmetric_mk_symmetric)
done
qed
theorem (in check_kuratowski_impl) check_kuratowski_spec:
"∀σ. Γ ⊢⇩t ⦃σ. pair_wf_digraph (mk_graph ´G)⦄
´R :== PROC check_kuratowski(´G, ´K)
⦃ ´G = ⇗σ⇖G ∧ ´K = ⇗σ⇖K ∧ ´R ⟷ witness (mk_graph ´G) (mk_graph ´K)⦄"
by vcg (auto simp: witness_def IGraph_inv_conv' pwd_imp_ppg_mkg)
lemma check_kuratowski_correct:
assumes "pair_pseudo_graph G"
assumes "witness G K"
shows "¬kuratowski_planar G"
using assms
by (intro planar_theorem[where K=K]) (auto simp: witness_def)
lemma check_kuratowski_correct_comb:
assumes "pair_pseudo_graph G"
assumes "witness G K"
shows "¬comb_planar G"
using assms by (metis check_kuratowski_correct comb_planar_compat)
lemma check_kuratowski_complete:
assumes "pair_pseudo_graph G" "pair_pseudo_graph K" "loop_free K"
assumes "subgraph K G"
assumes "subdivision_pair H K" "K⇘3,3⇙ H ∨ K⇘5⇙ H"
shows "witness G K"
using assms by (auto simp: witness_def intro: K33_contractedI K5_contractedI)
end