# Theory Bipartite_Graphs

```theory Bipartite_Graphs imports Undirected_Graph_Walks
begin

section ‹Bipartite Graphs ›

text ‹An introductory library for reasoning on bipartite graphs.›

subsection ‹Bipartite Set Up ›
text ‹All "edges", i.e. pairs, between any two sets ›
definition all_bi_edges :: "'a set ⇒ 'a set ⇒ 'a edge set" where
"all_bi_edges X Y ≡ mk_edge ` (X × Y)"

lemma all_bi_edges_alt:
assumes "X ∩ Y = {}"
shows "all_bi_edges X Y = {e . card e = 2 ∧ e ∩ X ≠ {} ∧ e ∩ Y ≠ {}}"
unfolding all_bi_edges_def
proof (intro subset_antisym subsetI)
fix e assume "e ∈ mk_edge ` (X × Y)"
then obtain v1 v2 where "e = { v1, v2}" and  "v1 ∈ X" and "v2 ∈ Y"
by auto
then show "e ∈ {e. card e = 2 ∧ e ∩ X ≠ {} ∧ e ∩ Y ≠ {}}" using assms
using card_2_iff by blast
next
fix e' assume assm: "e' ∈ {e. card e = 2 ∧ e ∩ X ≠ {} ∧ e ∩ Y ≠ {}}"
then obtain v1 where v1in: "v1 ∈ e'" and "v1 ∈ X"
by blast
moreover obtain v2 where v2in: "v2 ∈ e'" and "v2 ∈ Y" using assm by blast
then have ne: "v1 ≠ v2"
using assms calculation(2) by blast
have "card e' = 2" using assm by blast
have "{v1, v2} ⊆ e'" using v1in v2in by blast
then have "e' = {v1, v2}" using assm v1in v2in
by (metis (no_types, opaque_lifting) ‹card e' = 2› card_2_iff' insertCI ne subsetI subset_antisym)
then show "e' ∈ mk_edge ` (X × Y)"
by (simp add: ‹v2 ∈ Y› calculation(2) in_mk_edge_img)
qed

lemma all_bi_edges_alt2:  "all_bi_edges X Y = {{x, y} | x y. x ∈ X ∧ y ∈ Y }"
unfolding all_bi_edges_def
proof (intro subset_antisym subsetI)
fix x assume "x ∈ mk_edge ` (X × Y)"
then obtain a b where "(a, b) ∈ (X × Y)" and xeq: "x = mk_edge (a, b) " by blast
then show "x ∈ {{x, y} |x y. x ∈ X ∧ y ∈ Y}"
by auto
next
fix x assume "x ∈ {{x, y} |x y. x ∈ X ∧ y ∈ Y}"
then obtain a b where xeq: "x = {a, b}" and "a ∈ X" and "b ∈ Y"
by blast
then have "(a, b) ∈ (X × Y)" by auto
then show "x ∈ mk_edge ` (X × Y)"  using in_mk_edge_img xeq by metis
qed

lemma all_bi_edges_wf: "e ∈ all_bi_edges X Y ⟹ e ⊆ X ∪ Y"

lemma all_bi_edges_2: "X ∩ Y = {} ⟹ e ∈ all_bi_edges X Y ⟹ card e = 2"
using card_2_iff by (auto simp add: all_bi_edges_alt2)

lemma all_bi_edges_main: "X ∩ Y = {} ⟹ all_bi_edges X Y ⊆ all_edges (X ∪ Y)"
unfolding  all_edges_def using all_bi_edges_wf all_bi_edges_2 by blast

lemma all_bi_edges_finite: "finite X ⟹ finite Y ⟹ finite (all_bi_edges X Y)"

lemma all_bi_edges_not_ssX: "X ∩ Y = {} ⟹ e ∈ all_bi_edges X Y ⟹ ¬ e ⊆ X"

lemma all_bi_edges_sym: "all_bi_edges X Y = all_bi_edges Y X"

lemma all_bi_edges_not_ssY: "X ∩ Y = {} ⟹ e ∈ all_bi_edges X Y ⟹ ¬ e ⊆ Y"

lemma card_all_bi_edges:
assumes "finite X" "finite Y"
assumes "X ∩ Y = {}"
shows "card (all_bi_edges X Y) = card X * card Y"
proof -
have "card (all_bi_edges X Y) = card (X × Y)"
unfolding all_bi_edges_def using inj_on_mk_edge assms card_image by blast
thus ?thesis using card_cartesian_product by auto
qed

lemma (in sgraph) all_edges_between_bi_subset: "mk_edge ` all_edges_between X Y ⊆ all_bi_edges X Y"
by (auto simp: all_edges_between_def all_bi_edges_def)

subsection ‹ Bipartite Graph Locale ›

text ‹For reasoning purposes, it is useful to explicitly label the two sets of vertices as X and Y.
These are parameters in the locale›

locale bipartite_graph = graph_system +
fixes X Y :: "'a set"
assumes partition: "partition_on V {X, Y}"
assumes ne: "X ≠ Y"
assumes edge_betw: "e ∈ E ⟹ e ∈ all_bi_edges X Y"
begin

lemma part_intersect_empty: "X ∩ Y = {}"
using partition_onD2 partition disjointD ne
by blast

lemma X_not_empty: "X ≠ {}"
using partition partition_onD3 by auto

lemma Y_not_empty: "Y ≠ {}"
using partition partition_onD3 by auto

lemma XY_union: "X ∪ Y = V"
using partition partition_onD1 by auto

lemma card_edges_two: "e ∈ E ⟹ card e = 2"
using edge_betw all_bi_edges_alt part_intersect_empty by auto

lemma partitions_ss: "X ⊆ V" "Y ⊆ V"
using XY_union by auto

end

text ‹ By definition, we say an edge must be between X and Y, i.e. contains two vertices ›
sublocale bipartite_graph ⊆ sgraph
using card_edges_two by (unfold_locales)

context bipartite_graph
begin

abbreviation "density ≡ edge_density X Y"

lemma bipartite_sym: "bipartite_graph V E Y X"
using partition ne edge_betw all_bi_edges_sym
by (unfold_locales) (auto simp add: insert_commute)

assumes "x1 ∈ X" "x2 ∈ X"
assume "{x1, x2} ∈ E"
then have "¬ {x1, x2} ⊆ X"
using all_bi_edges_not_ssX edge_betw part_intersect_empty by auto
then show False using assms by auto
qed

assumes "y1 ∈ Y" "y2 ∈ Y"
proof -
interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
qed

lemma X_vert_adj_Y: "x ∈X ⟹ vert_adj x y ⟹ y ∈ Y"

lemma Y_vert_adj_X: "y ∈Y ⟹ vert_adj y x ⟹ x ∈ X"

lemma neighbors_ss_eq_neighborhoodX: "v ∈ X ⟹ neighborhood v = neighbors_ss v Y"
unfolding neighborhood_def neighbors_ss_def

lemma neighbors_ss_eq_neighborhoodY: "v ∈ Y ⟹ neighborhood v = neighbors_ss v X"
unfolding neighborhood_def neighbors_ss_def

lemma neighborhood_subset_oppX: "v ∈ X ⟹ neighborhood v ⊆ Y"
using neighbors_ss_eq_neighborhoodX neighbors_ss_def by auto

lemma neighborhood_subset_oppY: "v ∈ Y ⟹ neighborhood v ⊆ X"
using neighbors_ss_eq_neighborhoodY neighbors_ss_def by auto

lemma degree_neighbors_ssX: "v ∈ X ⟹ degree v = card (neighbors_ss v Y)"
using neighbors_ss_eq_neighborhoodX alt_deg_neighborhood by auto

lemma degree_neighbors_ssY: "v ∈ Y ⟹ degree v = card (neighbors_ss v X)"
using neighbors_ss_eq_neighborhoodY alt_deg_neighborhood by auto

definition is_bicomplete:: "bool" where
"is_bicomplete ≡ E = all_bi_edges X Y"

lemma edge_betw_indiv:
assumes "e ∈ E"
obtains x y where "x ∈ X ∧ y ∈ Y ∧ e = {x, y}"
proof -
have "e ∈ {{x, y} | x y. x ∈ X ∧ y ∈ Y }"
using edge_betw all_bi_edges_alt2 assms by blast
thus ?thesis
using that by auto
qed

lemma edges_between_equals_edge_set: "mk_edge ` (all_edges_between X Y) = E"
by (simp add: all_edges_between_set, intro subset_antisym subsetI, auto) (metis edge_betw_indiv)

text ‹ Lemmas for reasoning on walks and paths in a bipartite graph ›
lemma walk_alternates:
assumes "is_walk w"
assumes "Suc i < length w" "i ≥ 0"
shows "w ! i ∈ X ⟷ w ! (i + 1) ∈ Y"
proof -
have "{w ! i, w ! (i +1)} ∈ E" using is_walk_index assms by auto
then show ?thesis
qed

text ‹A useful reasoning pattern to mimic "wlog" statements for properties that are symmetric
is to interpret the symmetric bipartite graph and then directly apply the lemma proven earlier›
lemma walk_alternates_sym:
assumes "is_walk w"
assumes "Suc i < length w" "i ≥ 0"
shows "w ! i ∈ Y ⟷ w ! (i + 1) ∈ X"
proof -
interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
show ?thesis using sym.walk_alternates assms by simp
qed

lemma walk_length_even:
assumes "is_walk w"
assumes "hd w ∈ X" and "last w ∈ X"
shows "even (walk_length w)"
using assms
proof (induct "length w" arbitrary: w rule: nat_induct2)
case 0
then show ?case by (auto simp add: is_walk_def)
next
case 1
then have "walk_length w = 0" using walk_length_conv by auto
then show ?case by simp
next
case (step n)
then show ?case proof (cases "n = 0")
case True
then have "length w = 2" using step by simp
then have "hd w ∈ X ⟹ last w ∈ Y" using walk_alternates hd_conv_nth last_conv_nth
zero_le zero_neq_numeral)
then show ?thesis
using part_intersect_empty step.prems(2) step.prems(3) by blast
next
case False
have IH: "(⋀w. n = length w ⟹ is_walk w ⟹ hd w ∈ X ⟹ last w ∈ X ⟹ even (walk_length w))"
using step by simp
obtain w1 w2 where weq: "w = w1@w2" and w1: "w1 = take n w" and w2: "w2 = drop n w"
by simp
then have ne: "w1 ≠ []" using False is_walk_not_empty2 step.prems(1) by fastforce
then have w1_walk: "is_walk w1" using w1 is_walk_take False
by (metis nat_le_linear neq0_conv step.prems(1) take_all)
have hdw1: "hd w1 ∈ X" using step ne weq by auto
then have w1n: "length w1 = n" using step length_take w1 by auto
then have "length w2 = 2" using step length_drop
have "last w = w ! (n + 1)" using step last_conv_nth is_walk_not_empty
then have "w ! n ∈ Y" using step by (simp add: walk_alternates_sym)
then have "w ! (n - 1) ∈ X" using False walk_alternates step by simp
then have "last w1 ∈ X" using step last_conv_nth[of w1] ne w1n
by (metis last_list_update list_update_id take_update_swap w1)
then have "even (walk_length w1)" using w1_walk w1n hdw1 IH[of w1] by simp
then have "even (walk_length w1 + 2)" by simp
then show ?thesis using walk_length_conv weq step
qed
qed

lemma walk_length_even_sym:
assumes "is_walk w"
assumes "hd w ∈ Y"
assumes "last w ∈ Y"
shows "even (walk_length w)"
proof -
interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
show ?thesis using sym.walk_length_even assms by auto
qed

lemma walk_length_odd:
assumes "is_walk w"
assumes "hd w ∈ X" and "last w ∈ Y"
shows "odd (walk_length w)"
using assms
proof (cases "length w ≥ 2")
case True
then have hdin: "hd (tl w) ∈ Y" using walk_alternates hd_conv_nth
by (metis (mono_tags, lifting) Suc_1 Suc_less_eq2 assms(1) assms(2) is_walk_not_empty2 is_walk_tl
le_neq_implies_less le_numeral_extra(3) length_greater_0_conv less_Suc_eq nth_tl
have w: "is_walk (tl w)" using assms True is_walk_tl by auto
have last: "last (tl w) ∈ Y" using assms(3) by (simp add: is_walk_not_empty last_tl w)
then have ev: "even (walk_length (tl w))" using hdin w  walk_length_even_sym[of "tl w"] by auto
then have "walk_length w = walk_length (tl w) + 1" using True walk_length_conv by auto
then show ?thesis using ev by simp
next
case False
have "length w ≠ 0" using is_walk_not_empty assms by simp
then have "length w = 1" using False by linarith
then have "hd w = last w"
using ‹length w ≠ 0› hd_conv_nth last_conv_nth by fastforce
then have "hd w ∈ X ⟹ last w ∉ Y" using part_intersect_empty by auto
then show ?thesis using assms by simp
qed

lemma walk_length_odd_sym:
assumes "is_walk w"
assumes "hd w ∈ Y" and "last w ∈ X"
shows "odd (walk_length w)"
proof -
interpret sym: bipartite_graph V E Y X using bipartite_sym by simp
show ?thesis using assms sym.walk_length_odd by simp
qed

lemma walk_length_even_iff:
assumes "is_walk w"
shows "even (walk_length w) ⟷ (hd w ∈ X ∧ last w ∈ X) ∨ (hd w ∈ Y ∧ last w ∈ Y)"
proof (intro iffI)
assume ev: "even (walk_length w)"
show "hd w ∈ X ∧ last w ∈ X ∨ hd w ∈ Y ∧ last w ∈ Y"
proof (rule ccontr)
assume "¬ ((hd w ∈ X ∧ last w ∈ X) ∨ (hd w ∈ Y ∧ last w ∈ Y))"
then have "(hd w ∉ X ∨ last w ∉ X) ∧ (hd w ∉ Y ∨ last w ∉ Y)" by simp
then have "(hd w ∈ Y ∨ last w ∈ Y) ∧ (hd w ∈ X ∨ last w ∈ X)" using part_intersect_empty
using XY_union assms is_walk_wf_hd is_walk_wf_last by auto
then have split: "(hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X)"
using part_intersect_empty by auto
have o1: "(hd w ∈ X ∧ last w ∈ Y) ⟹ odd (walk_length w)" using walk_length_odd assms by auto
have "(hd w ∈ Y ∧ last w ∈ X) ⟹ odd (walk_length w)" using walk_length_odd_sym assms by auto
then show False using split ev o1 by auto
qed
next
show "(hd w ∈ X ∧ last w ∈ X) ∨ (hd w ∈ Y ∧ last w ∈ Y) ⟹ even (walk_length w)"
using walk_length_even walk_length_even_sym assms by auto
qed

lemma walk_length_odd_iff:
assumes "is_walk w"
shows "odd (walk_length w) ⟷ (hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X)"
proof (intro iffI)
assume o: "odd (walk_length w)"
show "(hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X)"
proof (rule ccontr)
assume "¬ ((hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X))"
then have "(hd w ∉ X ∨ last w ∉ Y) ∧ (hd w ∉ Y ∨ last w ∉ X)" by simp
then have "(hd w ∈ Y ∨ last w ∈ X) ∧ (hd w ∈ X ∨ last w ∈ Y)" using part_intersect_empty
using XY_union assms is_walk_wf_hd is_walk_wf_last by auto
then have split: "(hd w ∈ X ∧ last w ∈ X) ∨ (hd w ∈ Y ∧ last w ∈ Y)"
using part_intersect_empty by auto
have e1: "(hd w ∈ X ∧ last w ∈ X) ⟹ even (walk_length w)" using walk_length_even assms by auto
have "(hd w ∈ Y ∧ last w ∈ Y) ⟹ even (walk_length w)" using walk_length_even_sym assms by auto
then show False using split o e1 by auto
qed
next
show "(hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X) ⟹ odd (walk_length w)"
using walk_length_odd walk_length_odd_sym assms by auto
qed

text ‹ Classic basic theorem that a bipartite graph must not have any cycles with an odd length ›
lemma no_odd_cycles:
assumes "is_walk w"
assumes "odd (walk_length w)"
shows "¬ is_cycle w"
proof -
have "(hd w ∈ X ∧ last w ∈ Y) ∨ (hd w ∈ Y ∧ last w ∈ X)" using assms walk_length_odd_iff by auto
then have "hd w ≠ last w" using part_intersect_empty by auto
thus ?thesis using is_cycle_def is_closed_walk_def by simp
qed

end

text ‹ A few properties rely on cardinality definitions that require the vertex sets to be finite ›

locale fin_bipartite_graph = bipartite_graph + fin_graph_system
begin

lemma fin_bipartite_sym: "fin_bipartite_graph V E Y X"
by (intro_locales) (simp add: bipartite_sym bipartite_graph.axioms(2))

lemma partitions_finite: "finite X" "finite Y"
using partitions_ss finite_subset finV by auto

lemma card_edges_between_set: "card (all_edges_between X Y) = card E"
proof -
have "card (all_edges_between X Y) = card (mk_edge ` (all_edges_between X Y))"
using inj_on_mk_edge using partitions_finite card_image
by (metis inj_on_mk_edge part_intersect_empty)
then show ?thesis by (simp add: edges_between_equals_edge_set)
qed

lemma density_simp: "density = card (E) / ((card X) * (card Y))"
unfolding edge_density_def using card_edges_between_set by auto

lemma edge_size_degree_sumY: "card E = (∑y ∈ Y . degree y)"
proof -
have "(∑y ∈ Y . degree y) = (∑y ∈ Y . card(neighbors_ss y X))"
using degree_neighbors_ssY by (simp)
also have "... = card (all_edges_between X Y)"
using card_all_edges_betw_neighbor
by (metis card_all_edges_between_commute partitions_finite(1) partitions_finite(2))
finally show ?thesis