Theory Hypergraph_Basics.Hypergraph
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