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" by (auto simp add: all_bi_edges_alt2) 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)" by (simp add: all_bi_edges_def) lemma all_bi_edges_not_ssX: "X ∩ Y = {} ⟹ e ∈ all_bi_edges X Y ⟹ ¬ e ⊆ X" by (auto simp add: all_bi_edges_alt) lemma all_bi_edges_sym: "all_bi_edges X Y = all_bi_edges Y X" by (auto simp add: all_bi_edges_alt2) lemma all_bi_edges_not_ssY: "X ∩ Y = {} ⟹ e ∈ all_bi_edges X Y ⟹ ¬ e ⊆ Y" by (auto simp add: all_bi_edges_alt) 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) lemma X_verts_not_adj: assumes "x1 ∈ X" "x2 ∈ X" shows "¬ vert_adj x1 x2" proof (rule ccontr, simp add: vert_adj_def) 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 lemma Y_verts_not_adj: assumes "y1 ∈ Y" "y2 ∈ Y" shows "¬ vert_adj y1 y2" proof - interpret sym: bipartite_graph V E Y X using bipartite_sym by simp show ?thesis using sym.X_verts_not_adj by (simp add: assms(1) assms(2)) qed lemma X_vert_adj_Y: "x ∈X ⟹ vert_adj x y ⟹ y ∈ Y" using X_verts_not_adj XY_union vert_adj_imp_inV by blast lemma Y_vert_adj_X: "y ∈Y ⟹ vert_adj y x ⟹ x ∈ X" using Y_verts_not_adj XY_union vert_adj_imp_inV by blast lemma neighbors_ss_eq_neighborhoodX: "v ∈ X ⟹ neighborhood v = neighbors_ss v Y" unfolding neighborhood_def neighbors_ss_def by(auto simp add: X_vert_adj_Y vert_adj_imp_inV) lemma neighbors_ss_eq_neighborhoodY: "v ∈ Y ⟹ neighborhood v = neighbors_ss v X" unfolding neighborhood_def neighbors_ss_def by(auto simp add: Y_vert_adj_X vert_adj_imp_inV) 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 using X_vert_adj_Y not_vert_adj Y_vert_adj_X vert_adj_sym by blast 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 by (metis add_0 add_diff_cancel_right' less_2_cases_iff list.size(3) nat_1_add_1 step.prems(1) 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 by (simp add: w2) have "last w = w ! (n + 1)" using step last_conv_nth is_walk_not_empty by (metis add.left_commute diff_add_inverse nat_1_add_1) 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 by (simp add: False w1n) 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 numeral_1_eq_Suc_0 numerals(1) plus_nat.add_0) 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 by (simp add: card_edges_between_set) qed lemma edge_size_degree_sumX: "card E = (∑y ∈ X . degree y)" proof - interpret sym: fin_bipartite_graph V E Y X using fin_bipartite_sym by simp show ?thesis using sym.edge_size_degree_sumY by simp qed end end