Theory Hypergraph_Variations
section ‹Hypergraph Variations›
text ‹This section presents many different types of hypergraphs, introducing conditions such as
non-triviality, regularity, and uniform. Additionally, it briefly formalises decompositions ›
theory Hypergraph_Variations
imports
Hypergraph
Undirected_Graph_Theory.Bipartite_Graphs
begin
subsection ‹Non-trivial hypergraphs›
text ‹Non empty (ne) implies that the vertex (and edge) set is not empty. Non trivial typically
requires at least two edges ›
locale hyper_system_vne = hypersystem +
assumes V_nempty: "𝒱 ≠ {}"
locale hyper_system_ne = hyper_system_vne +
assumes E_nempty: "E ≠ {#}"
locale hypergraph_ne = hypergraph +
assumes E_nempty: "E ≠ {#}"
begin
lemma V_nempty: "𝒱 ≠ {}"
using wellformed E_nempty blocks_nempty by fastforce
lemma sizeE_not_zero: "size E ≠ 0"
using E_nempty by auto
end
sublocale hypergraph_ne ⊆ hyper_system_ne
by (unfold_locales) (simp_all add: V_nempty E_nempty)
locale hyper_system_ns = hypersystem +
assumes V_not_single: "¬ is_singleton 𝒱"
locale hypersystem_nt = hyper_system_ne + hyper_system_ns
locale hypergraph_nt = hypergraph_ne + hyper_system_ns
sublocale hypergraph_nt ⊆ hypersystem_nt
by (unfold_locales)
locale fin_hypersystem_vne = fin_hypersystem + hyper_system_vne
begin
lemma order_gt_zero: "horder > 0"
using V_nempty finite_sets by auto
lemma order_ge_one: "horder ≥ 1"
using order_gt_zero by auto
end
locale fin_hypersystem_nt = fin_hypersystem_vne + hypersystem_nt
begin
lemma order_gt_one: "horder > 1"
using V_nempty V_not_single
by (simp add: finite_sets is_singleton_altdef nat_neq_iff)
lemma order_ge_two: "horder ≥ 2"
using order_gt_one by auto
end
locale fin_hypergraph_ne = fin_hypergraph + hypergraph_ne
sublocale fin_hypergraph_ne ⊆ fin_hypersystem_vne
by unfold_locales
locale fin_hypergraph_nt = fin_hypergraph + hypergraph_nt
sublocale fin_hypergraph_nt ⊆ fin_hypersystem_nt
by (unfold_locales)
sublocale fin_hypergraph_ne ⊆ proper_design 𝒱 E
using blocks_nempty sizeE_not_zero by unfold_locales simp
sublocale proper_design ⊆ fin_hypergraph_ne 𝒱 ℬ
using blocks_nempty design_blocks_nempty by unfold_locales simp
subsection ‹Regular and Uniform Hypergraphs›
locale dregular_hypergraph = hypergraph +
fixes d
assumes const_degree: "⋀ x. x ∈ 𝒱 ⟹ hdegree x = d"
locale fin_dregular_hypergraph = dregular_hypergraph + fin_hypergraph
locale kuniform_hypergraph = hypergraph +
fixes k :: nat
assumes uniform: "⋀ e . e ∈# E ⟹ card e = k"
locale fin_kuniform_hypergraph = kuniform_hypergraph + fin_hypergraph
locale almost_regular_hypergraph = hypergraph +
assumes "⋀ x y . x ∈ 𝒱 ⟹ y ∈ 𝒱 ⟹ ¦ hdegree x - hdegree y ¦ ≤ 1"
locale kuniform_regular_hypgraph = kuniform_hypergraph 𝒱 E k + dregular_hypergraph 𝒱 E k
for 𝒱 E k
locale fin_kuniform_regular_hypgraph_nt = kuniform_regular_hypgraph 𝒱 E k + fin_hypergraph_nt 𝒱 E
for 𝒱 E k
sublocale fin_kuniform_regular_hypgraph_nt ⊆ fin_kuniform_hypergraph 𝒱 E k
by unfold_locales
sublocale fin_kuniform_regular_hypgraph_nt ⊆ fin_dregular_hypergraph 𝒱 E k
by unfold_locales
locale block_balanced_design = block_design + t_wise_balance
locale regular_block_design = block_design + constant_rep_design
sublocale t_design ⊆ block_balanced_design
by unfold_locales
locale fin_kuniform_hypergraph_nt = fin_kuniform_hypergraph + fin_hypergraph_nt
sublocale fin_kuniform_regular_hypgraph_nt ⊆ fin_kuniform_hypergraph_nt 𝒱 E k
by unfold_locales
text ‹Note that block designs are defined as non-trivial and finite as they automatically build on
the proper design locale ›
sublocale fin_kuniform_hypergraph_nt ⊆ block_design 𝒱 E k
rewrites "point_replication_number E v = hdegree v" and "points_index E vs = hdegree_set vs"
using uniform by (unfold_locales)
(simp_all add: point_replication_number_def hdegree_def hdegree_set_def points_index_def E_nempty)
sublocale fin_kuniform_regular_hypgraph_nt ⊆ regular_block_design 𝒱 E k k
rewrites "point_replication_number E v =hdegree v" and "points_index E vs = hdegree_set vs"
using const_degree by (unfold_locales)
(simp_all add: point_replication_number_def hdegree_def hdegree_set_def points_index_def)
subsection ‹Factorisations›
locale d_factor = spanning_hypergraph + dregular_hypergraph 𝒱H EH d for d
context hypergraph
begin
definition is_d_factor :: "'a hyp_graph ⇒ bool" where
"is_d_factor H ≡ (∃ d. d_factor (hyp_verts H) (hyp_edges H) 𝒱 E d)"
definition d_factorisation :: "'a hyp_graph multiset ⇒ bool" where
"d_factorisation S ≡ hypergraph_decomposition S ∧ (∀ h ∈# S. is_d_factor h)"
end
subsection ‹Sample Graph Theory Connections›
sublocale fin_graph_system ⊆ fin_hypersystem V "mset_set E"
rewrites "hedge_adjacent = edge_adj"
proof (unfold_locales)
show "⋀b. b ∈# mset_set E ⟹ b ⊆ V" using wellformed fin_edges by simp
then interpret hs: hypersystem V "mset_set E"
by unfold_locales (simp add: fin_edges)
show "hs.hedge_adjacent = edge_adj"
unfolding hs.hedge_adjacent_def edge_adj_def
by (simp add: fin_edges)
qed(simp add: finV)
sublocale fin_bipartite_graph ⊆ fin_hypersystem_vne V "mset_set E"
using X_not_empty Y_not_empty partitions_ss(2) by unfold_locales (auto)
end