Theory Graph_Theory_Relations

```section ‹Graph Theory Inheritance›
text ‹ This theory aims to demonstrate the use of locales to transfer theorems between different
graph/combinatorial structure representations ›

theory Graph_Theory_Relations imports Undirected_Graph_Basics Bipartite_Graphs
"Design_Theory.Block_Designs" "Design_Theory.Group_Divisible_Designs"
begin

text ‹A graph is a type of incidence system, and more specifically a type of combinatorial design.
This section demonstrates the correspondence between designs and graphs ›

sublocale graph_system ⊆ inc: incidence_system V "mset_set E"
by (unfold_locales) (metis wellformed elem_mset_set ex_in_conv infinite_set_mset_mset_set)

sublocale fin_graph_system ⊆ finc: finite_incidence_system V "mset_set E"
using finV by unfold_locales

sublocale fin_ulgraph ⊆ d: design V "mset_set E"
using edge_size empty_not_edge fin_edges by unfold_locales auto

sublocale fin_ulgraph ⊆ d: simple_design V "mset_set E"

locale graph_has_edges = graph_system +
assumes edges_nempty: "E ≠ {}"

locale fin_sgraph_wedges = fin_sgraph + graph_has_edges

text ‹The simple graph definition of degree overlaps with the definition of a point replication number ›
sublocale fin_sgraph_wedges ⊆ bd: block_design V "mset_set E" 2
rewrites "point_replication_number (mset_set E) x = degree x"
and "points_index (mset_set E) vs = degree_set vs"
proof (unfold_locales)
show "inc.𝖻 ≠ 0"  by (simp add: edges_nempty fin_edges)
show "⋀bl. bl ∈# mset_set E ⟹ card bl = 2" by (simp add: fin_edges two_edges)
show "mset_set E index vs = degree_set vs"
unfolding degree_set_def points_index_def by (simp add: fin_edges)
next
have "size {#b ∈# (mset_set E) . x ∈ b#} = card (incident_edges x)"
unfolding incident_edges_def vincident_def
then show "mset_set E rep x = degree x" using alt_degree_def point_replication_number_def
by metis
qed

locale fin_bipartite_graph_wedges = fin_bipartite_graph + fin_sgraph_wedges

sublocale fin_bipartite_graph_wedges ⊆ group_design V "mset_set E" "{X, Y}"
by unfold_locales (simp_all add: partition ne)

text ‹ Another common formal representation of graphs is as a vertex set and an adjacency relation
This is a useful representation in some contexts - we use locales to enable the transfer of
results between the two representations, specifically the mutual sublocales approach ›

locale graph_rel =
fixes vertices :: "'a set" ("V")
assumes wf: "⋀ u v. (u, v) ∈ adj_rel ⟹ u ∈ V ∧ v ∈ V"
begin

lemma wf_alt: "adj u v ⟹ (u, v) ∈ V × V"
using wf by blast

end

locale ulgraph_rel = graph_rel +
begin

text ‹ This definition makes sense in the context of an undirected graph ›
definition edge_set:: "'a edge set" where
"edge_set ≡ {{u, v} | u v. adj u v}"

assumes "e ∈ edge_set"
obtains u v where "e = {u, v}" and "adj u v"
using assms edge_set_def mem_Collect_eq
by fastforce

assumes "e ∈ edge_set"
shows "card e = 1 ∨ card e = 2"
proof -
obtain u v where "e = {u, v}" and "adj u v" using obtain_edge_pair_adj assms by blast
then show ?thesis by (cases "u = v", simp_all)
qed

assumes "e ∈ edge_set"
shows "card e > 0 ∧ card e ≤ 2"
proof -
obtain u v where "e = {u, v}" and "adj u v" using obtain_edge_pair_adj assms by blast
then show ?thesis by (cases "u = v", simp_all)
qed

lemma edge_set_wf: "e ∈ edge_set ⟹ e ⊆ V"
using obtain_edge_pair_adj wf by (metis insert_iff singletonD subsetI)

lemma is_graph_system: "graph_system V edge_set"

lemma is_ulgraph: "ulgraph V edge_set"
by (intro_locales) auto

end

context ulgraph
begin

definition adj_relation :: "'a rel" where

text ‹ Temporary interpretation - mutual sublocale setup ›

interpretation ulgraph_rel V adj_relation by (rule is_ulgraph_rel)

assumes "u ∈ V" "v ∈ V"

lemma edges_rel_is: "E = edge_set"
proof -
have "E = {{u, v} | u v . vert_adj u v}"
proof (intro subset_antisym subsetI)
show "⋀x. x ∈ {{u, v} |u v. vert_adj u v} ⟹ x ∈ E"
next
fix x assume "x ∈ E"
then have "x ⊆ V" and "card x > 0" and "card x ≤ 2" using wellformed edge_size by auto
then obtain u v where "x = {u, v}" and "{u, v} ∈ E"
by (metis ‹x ∈ E› alt_edge_size card_1_singletonE card_2_iff insert_absorb2)
then show "x ∈ {{u, v} |u v. vert_adj u v}" unfolding vert_adj_def by blast
qed
then have "E = {{u, v} | u v . adj u v}" using vert_adj_rel_iff Collect_cong
thus ?thesis using edge_set_def by simp
qed

end

context ulgraph_rel
begin

text ‹ Temporary interpretation - mutual sublocale setup ›
interpretation ulgraph V edge_set by (rule is_ulgraph)

proof (intro iffI)
then show "adj u v" using edge_set_def
by (metis (no_types, lifting) doubleton_eq_iff obtain_edge_pair_adj sym_alt)
next
then have "{u, v} ∈ edge_set" using edge_set_def by auto
qed

using rel_item_is by auto

end

sublocale ulgraph_rel ⊆ ulgraph "V" "edge_set"
using local.is_ulgraph rel_edges_is by simp_all

sublocale ulgraph ⊆ ulgraph_rel "V" "adj_relation"
using is_ulgraph_rel edges_rel_is by simp_all

locale sgraph_rel = ulgraph_rel +
begin

lemma irrefl_alt: "adj u v ⟹ u ≠ v"

lemma edge_is_card2:
assumes "e ∈ edge_set"
shows "card e = 2"
proof -
obtain u v where eq: "e = {u, v}" and "adj u v" using assms edge_set_def by blast
then have "u ≠ v" using irrefl_alt by simp
thus ?thesis using eq by simp
qed

lemma is_sgraph: "sgraph V edge_set"
using is_graph_system edge_is_card2 sgraph_axioms_def by (intro_locales) auto

end

context sgraph
begin

lemma is_rel_irrefl_alt:
shows "u ≠ v"
proof -
then have "{u, v} ∈ E" using vert_adj_def by simp
then have "card {u, v} = 2" using two_edges by simp
thus ?thesis by auto
qed

using irrefl_def is_rel_irrefl_alt by auto