Theory Hypergraph_Colourings
section ‹Hypergraph Colourings ›
theory Hypergraph_Colourings imports "Card_Partitions.Card_Partitions"
"Hypergraph_Basics.Hypergraph_Variations" "HOL-Library.Extended_Real"
"Girth_Chromatic.Girth_Chromatic_Misc"
begin
subsection ‹Function and Number extras ›
lemma surj_PiE:
assumes "f ∈ A →⇩E B"
assumes "f ` A = B"
assumes "b ∈ B"
obtains a where "a ∈ A" and "f a = b"
using assms(2) assms(3) by blast
lemma Stirling_gt_0: "n ≥ k ⟹ k ≠ 0 ⟹ Stirling n k > 0"
apply (induct n k rule: Stirling.induct, simp_all)
using Stirling_same Suc_lessI gr0I zero_neq_one by (metis Suc_leI)
lemma card_partition_on_ne:
assumes "card A ≥ n" "n≠ 0"
shows "{P. partition_on A P ∧ card P = n} ≠ {}"
proof -
have "finite A" using assms
using card_eq_0_iff by force
then have "card {P. partition_on A P ∧ card P = n} > 0"
using card_partition_on Stirling_gt_0 assms by fastforce
thus ?thesis using card.empty
by fastforce
qed
lemma enat_lt_INF:
fixes f :: "'a ⇒ enat"
assumes "(INF x∈ S. f x) < t"
obtains x where "x ∈ S" and "f x < t"
proof -
from assms have "(INF x∈ S. f x) ≠ top"
by fastforce
then obtain y where " y ∈ S" and "f y = (INF x ∈ S . f x)" using enat_in_INF
by metis
thus ?thesis using assms
by (simp add: that)
qed
subsection ‹Basic Definitions ›
context hypergraph
begin
text ‹Edge colourings - using older partition approach ›
definition edge_colouring :: "('a hyp_edge ⇒ colour) ⇒ colour set ⇒ bool" where
"edge_colouring f C ≡ partition_on_mset E {# {#h ∈# E . f h = c#} . c ∈# (mset_set C)#}"
definition proper_edge_colouring :: "('a hyp_edge ⇒ colour) ⇒ colour set ⇒ bool" where
"proper_edge_colouring f C ≡ edge_colouring f C ∧
(∀ e1 e2 c. e1 ∈# E ∧ e2 ∈# E - {#e1#} ∧ c ∈ C ∧ f e1 = c ∧ f e2 = c ⟶ e1 ∩ e2 = {})"
text ‹A vertex colouring function with no edge monochromatic requirements ›
abbreviation vertex_colouring :: "('a ⇒ colour) ⇒ nat ⇒ bool" where
"vertex_colouring f n ≡ f ∈ 𝒱 →⇩E {0..<n}"
lemma vertex_colouring_union:
assumes "vertex_colouring f n"
shows "⋃ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}} = 𝒱"
using assms by (intro subset_antisym subsetI) blast+
lemma vertex_colouring_disj:
assumes "vertex_colouring f n"
assumes "p ∈ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}}"
assumes "p' ∈ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}}"
assumes "p ≠ p'"
shows "p ∩ p' = {}"
proof (rule ccontr)
assume a: "p ∩ p' ≠ {} "
obtain c c' where "c ∈ {0..<n}" and "c' ∈ {0..<n}" "p = {v ∈ 𝒱. f v = c}" and
"p' = {v ∈ 𝒱. f v = c}" and "c ≠ c'"
using assms(4) assms(2) assms(3) a by blast
then obtain v where "v ∈ 𝒱" and "v ∈ p" and "v ∈ p'" using a by blast
then show False using Fun.apply_inverse
using ‹p = {v ∈ 𝒱. f v = c}› ‹p' = {v ∈ 𝒱. f v = c}› assms(4) by blast
qed
lemma vertex_colouring_n0: "𝒱 ≠ {} ⟹ ¬ vertex_colouring f 0"
by auto
lemma vertex_colouring_image: "vertex_colouring f n ⟹ v ∈ 𝒱 ⟹ f v ∈ {0..<n}"
using funcset_mem by blast
lemma vertex_colouring_image_edge_ss: "vertex_colouring f n ⟹ e ∈# E ⟹ f ` e ⊆ {0..<n}"
using wellformed vertex_colouring_image by blast
lemma vertex_colour_edge_map_ne: "vertex_colouring f n ⟹ e ∈# E ⟹ f ` e ≠ {}"
using blocks_nempty by simp
lemma vertex_colouring_ne: "vertex_colouring f n ⟹ f u ≠ f v ⟹ u ≠ v"
by auto
lemma vertex_colour_one: "𝒱 ≠ {} ⟹ vertex_colouring f 1 ⟹ v ∈ 𝒱 ⟹ f v = (0::nat)"
using atLeastLessThan_iff less_one vertex_colouring_image by simp
lemma vertex_colour_one_alt:
assumes "𝒱 ≠ {}"
shows "vertex_colouring f (1::nat) ⟷ f = (λ v ∈ 𝒱 . 0::nat)"
proof (intro iffI)
assume a: "vertex_colouring f 1"
show "f = (λv∈𝒱. 0::nat) "
proof (rule ccontr)
assume "f ≠ (λv∈𝒱. 0)"
then have "∃ v∈ 𝒱 . f v ≠ 0"
using a by auto
thus False using vertex_colour_one assms a
by meson
qed
next
show "f = (λv∈𝒱. 0) ⟹ f ∈ 𝒱 →⇩E {0..<1}" using PiE_eq_singleton by auto
qed
lemma vertex_colouring_partition:
assumes "vertex_colouring f n"
assumes "f ` 𝒱 = {0..<n}"
shows "partition_on 𝒱 { {v ∈ 𝒱 . f v = c} | c. c∈ {0..<n}}"
proof (intro partition_onI)
fix p assume "p ∈ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}}"
then obtain c where peq: "p = {v ∈ 𝒱 . f v = c}" and cin: "c ∈ {0..<n}" by blast
have "f ∈ 𝒱 →⇩E {0..<n}" using assms(1) by presburger
then obtain v where "v ∈ 𝒱" and "f v = c"
using surj_PiE[of f 𝒱 "{0..<n}" c] cin assms(2) by auto
then show "p ≠ {}" using peq by auto
next
show " ⋃ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}} = 𝒱" using vertex_colouring_union assms by auto
next
show "⋀p p'. p ∈ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}} ⟹
p' ∈ {{v ∈ 𝒱. f v = c} |c. c ∈ {0..<n}} ⟹ p ≠ p' ⟹ p ∩ p' = {}"
by auto
qed
subsection ‹ Monochromatic Edges ›
definition mono_edge :: "('a ⇒ colour) ⇒ 'a hyp_edge ⇒ bool" where
"mono_edge f e ≡ ∃ c. ∀ v ∈ e. f v = c"
lemma mono_edge_single:
assumes "e ∈# E"
shows "mono_edge f e ⟷ is_singleton (f ` e)"
unfolding mono_edge_def
proof (intro iffI)
assume "∃c. ∀v∈e. f v = c"
then obtain c where ceq: "⋀ v . v ∈ e ⟹ f v = c" by blast
then have "f ` e = {c}" using image_singleton assms blocks_nempty by metis
then show "is_singleton (f ` e)" by simp
next
assume "is_singleton (f ` e)"
then obtain c where "f ` e = {c}" by (meson is_singletonE)
then show "∃c. ∀v∈e. f v = c" by auto
qed
definition mono_edge_col :: "('a ⇒ colour) ⇒ 'a hyp_edge ⇒ colour ⇒ bool" where
"mono_edge_col f e c ≡ ∀ v ∈ e. f v = c"
lemma mono_edge_colI: "(⋀ v. v ∈ e ⟹ f v = c) ⟹ mono_edge_col f e c"
unfolding mono_edge_col_def by simp
lemma mono_edge_colD: "mono_edge_col f e c ⟹ (⋀ v. v ∈ e ⟹ f v = c)"
unfolding mono_edge_col_def by simp
lemma mono_edge_alt_col: "mono_edge f e ≡ ∃ c. mono_edge_col f e c"
unfolding mono_edge_def mono_edge_col_def by auto
subsection ‹Proper colourings ›
text ‹A proper vertex colouring brings in the monochromatic edge decision. Note that
this allows for a colouring of up to $n$ colours, not precisely $n$ colours›
definition is_proper_colouring :: "('a ⇒ colour) ⇒ nat ⇒ bool" where
"is_proper_colouring f n ≡ vertex_colouring f n ∧ (∀ e ∈# E. ∀ c ∈ {0..<n}. f ` e ≠ {c})"
lemma is_proper_colouring_alt: "is_proper_colouring f n ⟷ vertex_colouring f n ∧(∀ e ∈# E. ¬ is_singleton (f ` e))"
unfolding is_proper_colouring_def using vertex_colouring_image_edge_ss
by (auto) (metis insert_subset is_singleton_def)
lemma is_proper_colouring_alt2: "is_proper_colouring f n ⟷ vertex_colouring f n ∧(∀ e ∈# E. ¬ mono_edge f e)"
unfolding is_proper_colouring_def using vertex_colouring_image_edge_ss mono_edge_single
is_proper_colouring_alt is_proper_colouring_def by force
lemma is_proper_colouringI[intro]: "vertex_colouring f n ⟹ (⋀ e .e ∈# E ⟹
¬ is_singleton (f ` e)) ⟹ is_proper_colouring f n"
using is_proper_colouring_alt by simp
lemma is_proper_colouringI2[intro]: "vertex_colouring f n ⟹ (⋀ e .e ∈# E ⟹ ¬ mono_edge f e)
⟹ is_proper_colouring f n"
using is_proper_colouring_alt2 by simp
lemma is_proper_colouring_n0: "𝒱 ≠ {} ⟹ ¬ is_proper_colouring f 0"
unfolding is_proper_colouring_def using vertex_colouring_n0 by auto
lemma is_proper_colouring_empty:
assumes "𝒱 = {}"
shows "is_proper_colouring f n ⟷ f = (λ x . undefined)"
unfolding is_proper_colouring_def using PiE_empty_domain assms
using vertex_colouring_image_edge_ss by fastforce
lemma is_proper_colouring_n1:
assumes "𝒱 ≠ {}" "E ≠ {#}"
shows "¬ is_proper_colouring f 1"
proof (rule ccontr)
assume "¬ ¬ is_proper_colouring f 1"
then have vc: "vertex_colouring f 1" and em: "(∀ e ∈# E. ¬ mono_edge f e)"
using is_proper_colouring_alt2 by auto
then obtain e where ein: "e ∈# E" using assms by blast
have "f ∈ 𝒱 →⇩E {0}" using vc by auto
then have "∀ v∈ 𝒱. f v = 0"
by simp
then have "∀ v ∈ e. f v = 0" using wellformed‹e ∈# E› by blast
then have "mono_edge f e" using ein mono_edge_def by auto
then show False using em ein by simp
qed
lemma (in fin_hypergraph) is_proper_colouring_image_card:
assumes "𝒱 ≠ {}" "E ≠ {#}"
assumes "n > 1"
assumes "is_proper_colouring f n"
shows "card (f ` 𝒱) > 1"
proof (rule ccontr)
assume "¬ 1 < card (f ` 𝒱)"
then have a: "card (f ` 𝒱) = 1"
using assms by (meson card_0_eq finite_imageI finite_sets image_is_empty less_one linorder_neqE_nat)
then obtain c where ceq: "f ` 𝒱 = {c}"
using card_1_singletonE by blast
then obtain e where ein: "e ∈# E" using assms(2) by blast
then have ss: "e ⊆ 𝒱" using wellformed by auto
then have "∀ v ∈ e. f v = c" using ceq
by blast
then have "mono_edge f e" using ein mono_edge_def by auto
then show False using is_proper_colouring_alt2 ein
using assms(4) by blast
qed
text ‹ More monochromatic edges ›
lemma no_monochomatic_is_colouring:
assumes "∀ e ∈# E . ¬ mono_edge f e"
assumes "vertex_colouring f n"
shows "is_proper_colouring f n"
using assms mono_edge_single is_proper_colouringI by (auto)
lemma ex_monochomatic_not_colouring:
assumes "∃ e ∈# E . mono_edge f e"
assumes "vertex_colouring f n"
shows "¬ is_proper_colouring f n"
using assms(1) by (simp add: mono_edge_single is_proper_colouring_alt)
lemma mono_edge_colour_obtain:
assumes "mono_edge f e"
assumes "vertex_colouring f n"
assumes "e ∈# E"
obtains c where "c ∈ {0..<n}" and "mono_edge_col f e c"
proof -
have ss: "f ` e ⊆ {0..<n}" using vertex_colouring_image_edge_ss assms by simp
obtain c where all: "∀ v ∈ e. f v = c" using mono_edge_def
using assms(1) by fastforce
have "f ` e ≠ {}" using blocks_nempty by (simp add: assms(3))
then have "c ∈ f ` e" using all
by fastforce
thus ?thesis using ss that all mono_edge_col_def by blast
qed
text ‹ Complete proper colourings - i.e. when n colours are required ›
definition is_complete_proper_colouring:: "('a ⇒ colour) ⇒ nat ⇒ bool" where
"is_complete_proper_colouring f n ≡ is_proper_colouring f n ∧ f ` 𝒱 = {0..<n}"
lemma is_complete_proper_colouring_part:
assumes "is_complete_proper_colouring f n"
shows "partition_on 𝒱 { {v ∈ 𝒱 . f v = c} | c. c∈ {0..<n}}"
using vertex_colouring_partition assms is_complete_proper_colouring_def is_proper_colouring_def
by auto
lemma is_complete_proper_colouring_n0: "𝒱 ≠ {} ⟹ ¬ is_complete_proper_colouring f 0"
unfolding is_complete_proper_colouring_def using is_proper_colouring_n0 by simp
lemma is_complete_proper_colouring_n1:
assumes "𝒱 ≠ {}" "E ≠ {#}"
shows "¬ is_complete_proper_colouring f 1"
unfolding is_complete_proper_colouring_def using is_proper_colouring_n1 assms by simp
lemma (in fin_hypergraph) is_proper_colouring_reduce:
assumes "is_proper_colouring f n"
obtains f' where "is_complete_proper_colouring f' (card (f ` 𝒱))"
proof (cases "f ` 𝒱 = {0..<(n::nat)}")
case True
then have "card (f ` 𝒱) = n" by simp
then show ?thesis using is_complete_proper_colouring_def assms
using True that by auto
next
case False
obtain g :: "nat ⇒ nat" where bij: "bij_betw g (f ` 𝒱) {0..<(card (f ` 𝒱))}"
using ex_bij_betw_finite_nat finite_sets by blast
let ?f' = "λ x . if x ∈ 𝒱 then (g ∘ f) x else undefined"
have img: "?f' ` 𝒱 = {0..<card (f ` 𝒱)}" using bij bij_betw_imp_surj_on image_comp
by (smt (verit) image_cong)
have "is_proper_colouring ?f' (card (f ` 𝒱))"
proof (intro is_proper_colouringI)
show "vertex_colouring ?f' (card (f ` 𝒱))"
using img by auto
next
fix e assume ein: "e ∈# E"
then have ns: "¬ is_singleton (f ` e)" using assms is_proper_colouring_alt by blast
have ss: "(f ` e) ⊆ (f ` 𝒱)" using wellformed
by (simp add: ein image_mono)
have "e ⊆ 𝒱" using wellformed ein by simp
then have "?f' ` e = g ` (f ` e)" by auto
then show "¬ is_singleton (?f' ` e)" using bij ns ss bij_betw_singleton_image by metis
qed
then show ?thesis using is_complete_proper_colouring_def img
by (meson that)
qed
lemma (in fin_hypergraph) two_colouring_is_complete:
assumes "𝒱 ≠ {}"
assumes "E ≠ {#}"
assumes "is_proper_colouring f 2"
shows "is_complete_proper_colouring f 2"
proof -
have gt: "card (f ` 𝒱) > 1" using is_proper_colouring_image_card assms
using one_less_numeral_iff semiring_norm(76) by blast
have "f ∈ 𝒱 →⇩E {0..<2}" using is_proper_colouring_def assms(3) by auto
then have "f ` 𝒱 ⊆ {0..<2}" by blast
then have "card (f ` 𝒱) = 2"
by (metis Nat.le_diff_conv2 gt leI less_one less_zeroE nat_1_add_1 order_antisym_conv
subset_eq_atLeast0_lessThan_card zero_less_diff)
thus ?thesis using is_complete_proper_colouring_def assms
by (metis ‹f ` 𝒱 ⊆ {0..<2}› plus_nat.add_0 subset_card_intvl_is_intvl)
qed
subsection ‹n vertex colourings ›
definition is_n_colourable :: "nat ⇒ bool" where
"is_n_colourable n ≡ ∃ f . is_proper_colouring f n"
definition is_n_edge_colourable :: "nat ⇒ bool" where
"is_n_edge_colourable n ≡ ∃ f C . card C = n ⟶ proper_edge_colouring f C"
definition all_n_vertex_colourings :: "nat ⇒ ('a ⇒ colour) set" where
"all_n_vertex_colourings n ≡ {f . vertex_colouring f n}"
notation all_n_vertex_colourings ("(𝒞⇧_)" [502] 500)
lemma all_n_vertex_colourings_alt: "𝒞⇧n = 𝒱 →⇩E {0..<n}"
unfolding all_n_vertex_colourings_def by auto
lemma vertex_colourings_empty: "𝒱 ≠ {} ⟹ all_n_vertex_colourings 0 = {}"
unfolding all_n_vertex_colourings_def using vertex_colouring_n0
by simp
lemma (in fin_hypergraph) vertex_colourings_fin : "finite (𝒞⇧n) "
using all_n_vertex_colourings_alt finite_PiE finite_sets by (metis finite_atLeastLessThan)
lemma (in fin_hypergraph) count_vertex_colourings: "card (𝒞⇧n) = n ^ horder"
using all_n_vertex_colourings_alt card_funcsetE
by (metis card_atLeastLessThan finite_sets minus_nat.diff_0)
lemma vertex_colourings_nempty:
assumes "card 𝒱 ≥ n"
assumes "n ≠ 0"
shows "𝒞⇧n ≠ {}"
using all_n_vertex_colourings_alt assms
by (simp add: PiE_eq_empty_iff)
lemma vertex_colourings_one:
assumes "𝒱 ≠ {}"
shows "𝒞⇧1 = {λ v∈ 𝒱 . 0}"
using vertex_colour_one_alt assms
by (simp add: all_n_vertex_colourings_def)
lemma mono_edge_set_union:
assumes "e ∈# E"
shows "{f ∈ 𝒞⇧n . mono_edge f e} = (⋃c ∈ {0..<n}. {f ∈ 𝒞⇧n . mono_edge_col f e c})"
proof (intro subset_antisym subsetI)
fix g assume a1: "g ∈ {f ∈ 𝒞⇧n. mono_edge f e}"
then have "vertex_colouring g n" using all_n_vertex_colourings_def by blast
then obtain c where "c ∈ {0..<n}" and "mono_edge_col g e c" using a1 assms mono_edge_colour_obtain
by blast
then show "g ∈ (⋃c∈{0..<n}. {f ∈ 𝒞⇧n. mono_edge_col f e c})"
using ‹vertex_colouring g n› all_n_vertex_colourings_def by auto
next
fix h assume "h ∈ (⋃c∈{0..<n}. {f ∈ 𝒞⇧n. mono_edge_col f e c})"
then obtain c where "c ∈ {0..<n}" and "h ∈ {f ∈ 𝒞⇧n. mono_edge_col f e c}"
by blast
then show "h ∈ {f ∈ 𝒞⇧n. mono_edge f e}"
using mono_edge_alt_col by blast
qed
end
text ‹ Property B set up ›
abbreviation (in hypergraph) has_property_B :: "bool" where
"has_property_B ≡ is_n_colourable 2"
abbreviation hyp_graph_order:: "'a hyp_graph ⇒ nat" where
"hyp_graph_order h ≡ card (hyp_verts h)"
definition not_col_n_uni_hyps:: "nat ⇒ 'a hyp_graph set"
where "not_col_n_uni_hyps n ≡ { h . fin_kuniform_hypergraph_nt (hyp_verts h) (hyp_edges h) n ∧
¬ (hypergraph.has_property_B (hyp_verts h) (hyp_edges h)) }"
definition min_edges_colouring :: "nat ⇒ 'a itself ⇒ enat" where
"min_edges_colouring n _ ≡ INF h ∈ ((not_col_n_uni_hyps n) :: 'a hyp_graph set) . enat (size (hyp_edges h))"
lemma obtains_min_edge_colouring:
fixes z :: "'a itself"
assumes "min_edges_colouring n z < x"
obtains h :: "'a hyp_graph" where "h ∈ not_col_n_uni_hyps n" and "enat (size (hyp_edges h)) < x"
proof -
have "(INF h ∈ ((not_col_n_uni_hyps n) :: 'a hyp_graph set) . enat (size (hyp_edges h))) < x"
using min_edges_colouring_def[of "n" z] assms by auto
thus ?thesis using enat_lt_INF[of "λ h. enat (size (hyp_edges h))" "not_col_n_uni_hyps n" "x"]
using that by blast
qed
subsection ‹Alternate Partition Definition.›
text ‹Note that the indexed definition should be used most of the time instead ›
context hypergraph
begin
definition is_proper_colouring_part :: "'a set set ⇒ bool" where
"is_proper_colouring_part C ≡ partition_on 𝒱 C ∧ (∀ c ∈ C. ∀ e ∈# E. ¬ e ⊆ c)"
definition is_n_colourable_part :: "nat ⇒ bool" where
"is_n_colourable_part n ≡ ∃ C . card C = n ⟶ is_proper_colouring_part C"
abbreviation has_property_B_part :: "bool" where
"has_property_B_part ≡ is_n_colourable_part 2"
definition mono_edge_ss :: "'a set set ⇒ 'a hyp_edge ⇒ bool" where
"mono_edge_ss C e ≡ ∃ c ∈ C. e ⊆ c"
lemma is_proper_colouring_partI: "partition_on 𝒱 C ⟹ (∀ c ∈ C. ∀ e ∈# E. ¬ e ⊆ c) ⟹
is_proper_colouring_part C"
by (simp add: is_proper_colouring_part_def)
lemma no_monochomatic_is_colouring_part:
assumes "∀ e ∈# E . ¬ mono_edge_ss C e"
assumes "partition_on 𝒱 C"
shows "is_proper_colouring_part C"
using assms(1) mono_edge_ss_def by(intro is_proper_colouring_partI) (simp_all add: assms)
lemma ex_monochomatic_not_colouring_part:
assumes "∃ e ∈# E . mono_edge_ss C e"
assumes "partition_on 𝒱 C"
shows "¬ is_proper_colouring_part C"
using assms(1) mono_edge_ss_def is_proper_colouring_part_def by auto
definition all_n_vertex_colourings_part :: "nat ⇒ 'a set set set" where
"all_n_vertex_colourings_part n ≡ {C . partition_on 𝒱 C ∧ card C = n}"
lemma (in fin_hypergraph) all_vertex_colourings_part_fin: "finite (all_n_vertex_colourings_part n)"
unfolding all_n_vertex_colourings_part_def is_proper_colouring_part_def
using finitely_many_partition_on finite_sets by fastforce
lemma all_vertex_colourings_part_nempty: "card 𝒱 ≥ n ⟹ n ≠ 0 ⟹ all_n_vertex_colourings_part n ≠ {}"
unfolding all_n_vertex_colourings_part_def using card_partition_on_ne by blast
lemma disjoint_family_on_colourings:
assumes "e ∈# E"
shows "disjoint_family_on (λ c. {f ∈ 𝒞⇧n . mono_edge_col f e c}) {0..<n}"
using blocks_nempty mono_edge_col_def assms by (auto intro: disjoint_family_onI)
end
end