Theory Hypergraph_Basics.Hypergraph_Variations

(* Theory: Hypergraph_Variations
   Author: Chelsea Edmonds *)

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