Theory Hypergraph_Basics.Hypergraph

(* Theory: Hypergraph
   Author: Chelsea Edmonds *)

section ‹Basic Hypergraphs ›

text ‹Converting Design theory to hypergraph notation. Hypergraphs have technically already
been formalised›

theory Hypergraph
  imports 
    "Design_Theory.Block_Designs" 
    "Design_Theory.Sub_Designs" 
    "Fishers_Inequality.Design_Extras"
begin

lemma is_singleton_image: 
  "is_singleton C  is_singleton (f ` C)"
  by (metis image_empty image_insert is_singletonE is_singletonI)

lemma bij_betw_singleton_image: 
  assumes "bij_betw f A B"
  assumes "C  A"
  shows "is_singleton C  is_singleton (f ` C)"
proof (intro iffI)
  show " is_singleton C  is_singleton (f ` C)" by (rule is_singleton_image)
  show "is_singleton (f ` C)  is_singleton C " using assms is_singleton_image
    by (metis bij_betw_def inv_into_image_cancel)
qed

lemma image_singleton: 
  assumes "A  {}"
  assumes " x. x  A  f x = c"
  shows "f ` A = {c}"
  using assms(1) assms(2) by blast

type_synonym colour = nat

type_synonym 'a hyp_edge = "'a set"

type_synonym 'a hyp_graph = "('a set) × ('a hyp_edge multiset)"

abbreviation hyp_edges :: "'a hyp_graph  'a hyp_edge multiset" where
  "hyp_edges H  snd H"

abbreviation hyp_verts :: "'a hyp_graph  'a set" where
  "hyp_verts H  fst H"

locale hypersystem = incidence_system "vertices :: 'a set" "edges :: 'a hyp_edge multiset" 
  for "vertices" ("𝒱") and "edges" ("E") 

begin

text‹Basic definitions using hypergraph language›

abbreviation horder :: "nat" where
"horder  card (𝒱)"

definition hdegree :: "'a  nat" where
"hdegree v  size {#e ∈# E . v  e #}"

lemma hdegree_rep_num: "hdegree v = point_replication_number E v"
  unfolding hdegree_def point_replication_number_def by simp

definition hdegree_set :: "'a set  nat" where
"hdegree_set vs  size {#e ∈# E. vs  e#}"

lemma hdegree_set_points_index: "hdegree_set vs = points_index E vs"
  unfolding hdegree_set_def points_index_def by simp

definition hvert_adjacent :: "'a  'a  bool" where
"hvert_adjacent v1 v2   e . e ∈# E  v1  e  v2  e  v1  𝒱  v2  𝒱"

definition hedge_adjacent :: "'a hyp_edge  'a hyp_edge  bool" where
"hedge_adjacent e1 e2  e1  e2  {}  e1 ∈# E  e2 ∈# E"

lemma edge_adjacent_alt_def: "e1 ∈# E  e2 ∈# E   x . x  𝒱  x  e1  x  e2  
    hedge_adjacent e1 e2"
  unfolding hedge_adjacent_def by auto

definition hneighborhood :: "'a  'a set" where
"hneighborhood x  {v  𝒱 . hvert_adjacent x v}"

definition hmax_degree :: "nat" where
"hmax_degree  Max {hdegree v | v. v  𝒱}"

definition hrank :: "nat" where
"hrank  Max {card e | e . e ∈# E}"

definition hcorank :: "nat" where
"hcorank = Min {card e | e . e ∈# E}"

definition hedge_neighbourhood :: "'a  'a hyp_edge multiset" where
"hedge_neighbourhood x  {# e ∈# E . x  e #}"

lemma degree_alt_neigbourhood: "hdegree x = size (hedge_neighbourhood x)"
  using hedge_neighbourhood_def by (simp add: hdegree_def) 

definition hinduced_edges:: "'a set  'a hyp_edge multiset" where
"hinduced_edges V' = {#e ∈# E . e  V'#}"

end

text‹Sublocale for rewriting definition purposes rather than inheritance›
sublocale hypersystem  incidence_system 𝒱 E
  rewrites "point_replication_number E v = hdegree v" and "points_index E vs = hdegree_set vs"
  by (unfold_locales) (simp_all add: hdegree_rep_num hdegree_set_points_index)

text ‹Reverse sublocale to establish equality ›
sublocale incidence_system  hypersystem 𝒱 
  rewrites "hdegree v = point_replication_number  v" and "hdegree_set vs = points_index  vs"
proof (unfold_locales)
  interpret hs: hypersystem 𝒱  by (unfold_locales)
  show "hs.hdegree v =  rep v" using hs.hdegree_rep_num by simp
  show " hs.hdegree_set vs =  index vs" using hs.hdegree_set_points_index by simp
qed

text‹Missing design identified in the design theory hierarchy ›
locale inf_design = incidence_system + 
  assumes blocks_nempty: "bl ∈#   bl  {}"

sublocale design  inf_design
  by unfold_locales (simp add: blocks_nempty)

locale fin_hypersystem = hypersystem + finite_incidence_system 𝒱 E

sublocale finite_incidence_system  fin_hypersystem 𝒱 
  by unfold_locales

locale hypergraph = hypersystem + inf_design 𝒱 E

sublocale inf_design  hypergraph 𝒱 
  by unfold_locales (simp add: wellformed)

locale fin_hypergraph = hypergraph + fin_hypersystem

sublocale design  fin_hypergraph 𝒱 
  by unfold_locales

sublocale fin_hypergraph  design 𝒱 E
  using blocks_nempty by (unfold_locales) simp

subsection ‹Sub hypergraphs›
text ‹Sub hypergraphs and related concepts (spanning hypergraphs etc)›

locale sub_hypergraph = sub: hypergraph 𝒱H EH + orig: hypergraph "𝒱 :: 'a set" E + 
  sub_set_system 𝒱H EH 𝒱 E for 𝒱H EH 𝒱 E 

locale spanning_hypergraph = sub_hypergraph + 
  assumes "𝒱 = 𝒱H"

lemma spanning_hypergraphI:  "sub_hypergraph VH EH V E  V = VH  spanning_hypergraph VH EH V E"
  using spanning_hypergraph_def spanning_hypergraph_axioms_def by blast

context hypergraph
begin

definition is_subhypergraph :: "'a hyp_graph  bool" where
"is_subhypergraph H  sub_hypergraph (hyp_verts H) (hyp_edges H) 𝒱 E"

lemma is_subhypergraphI: 
  assumes "(hyp_verts H  𝒱)"
  assumes "(hyp_edges H ⊆# E)"
  assumes "hypergraph (hyp_verts H) (hyp_edges H)"
  shows "is_subhypergraph H"
  unfolding is_subhypergraph_def 
proof -
  interpret h: hypergraph "hyp_verts H" "hyp_edges H"
    using assms(3) by simp
  show "sub_hypergraph (hyp_verts H) (hyp_edges H) 𝒱 E"
    by (unfold_locales) (simp_all add: assms)
qed

definition hypergraph_decomposition :: "'a hyp_graph multiset  bool" where
"hypergraph_decomposition S  ( h ∈# S . is_subhypergraph  h)  
  partition_on_mset E {#hyp_edges h . h ∈# S#}"

definition is_spanning_subhypergraph :: "'a hyp_graph  bool" where
"is_spanning_subhypergraph H  spanning_hypergraph (hyp_verts H) (hyp_edges H) 𝒱 E"

lemma is_spanning_subhypergraphI: "is_subhypergraph H  (hyp_verts H) = 𝒱  
    is_spanning_subhypergraph H"
  unfolding is_subhypergraph_def is_spanning_subhypergraph_def using spanning_hypergraphI by blast

lemma spanning_subhypergraphI:  "(hyp_verts H) = 𝒱  (hyp_edges H) ⊆# E 
  hypergraph (hyp_verts H) (hyp_edges H)  is_spanning_subhypergraph H"
  using is_spanning_subhypergraphI by (simp add: is_subhypergraphI)

end
end