Theory Undirected_Graph_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

subsection ‹ Design Inheritance ›
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"
  by unfold_locales (simp add: fin_edges) 

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
    by (simp add: fin_edges) 
  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)


subsection ‹Adjacency Relation Definition ›

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")
  fixes adj_rel :: "'a rel"
  assumes wf: "⋀ u v. (u, v) ∈ adj_rel ⟹ u ∈ V ∧ v ∈ V"
begin 

abbreviation "adj u v ≡ (u, v) ∈ adj_rel"

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

end


locale ulgraph_rel = graph_rel + 
  assumes sym_adj: "sym adj_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}"

lemma obtain_edge_pair_adj:
  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 

lemma adj_to_edge_set_card: 
  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

lemma adj_to_edge_set_card_lim: 
  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"
  by (unfold_locales) (simp add: edge_set_wf)

lemma sym_alt: "adj u v ⟷ adj v u"
  using sym_adj by (meson symE)

lemma is_ulgraph: "ulgraph V edge_set"
  using ulgraph_axioms_def is_graph_system adj_to_edge_set_card_lim 
  by (intro_locales) auto

end

context ulgraph
begin

definition adj_relation :: "'a rel" where
"adj_relation ≡ {(u, v) | u v . vert_adj u v}"

lemma adj_relation_wf: "(u, v) ∈ adj_relation ⟹ {u, v} ⊆ V"
  unfolding adj_relation_def using vert_adj_imp_inV by auto

lemma adj_relation_sym: "sym adj_relation"
  unfolding adj_relation_def sym_def using vert_adj_sym by auto

lemma is_ulgraph_rel: "ulgraph_rel V adj_relation"
  using adj_relation_wf adj_relation_sym by (unfold_locales) auto

text ‹ Temporary interpretation - mutual sublocale setup ›

interpretation ulgraph_rel V adj_relation by (rule is_ulgraph_rel)

lemma vert_adj_rel_iff: 
  assumes "u ∈ V" "v ∈ V"
  shows "vert_adj u v ⟷ adj u v"
  using adj_relation_def by auto

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"
      using vert_adj_def by fastforce
  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
    by (smt (verit) local.wf vert_adj_imp_inV) 
  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)

lemma rel_vert_adj_iff:  "vert_adj u v ⟷ adj u v"
proof (intro iffI)
  assume "vert_adj u v"
  then have "{u, v} ∈ edge_set" by (simp add: vert_adj_def)
  then show "adj u v" using edge_set_def
    by (metis (no_types, lifting) doubleton_eq_iff obtain_edge_pair_adj sym_alt) 
next
  assume "adj u v"
  then have "{u, v} ∈ edge_set" using edge_set_def by auto
  then show "vert_adj u v" by (simp add: vert_adj_def)
qed

lemma rel_item_is: "(u, v) ∈ adj_rel ⟷ (u, v) ∈ adj_relation"
  unfolding adj_relation_def using rel_vert_adj_iff by auto

lemma rel_edges_is: "adj_rel = adj_relation"
  using rel_item_is by auto

end

sublocale ulgraph_rel ⊆ ulgraph "V" "edge_set"
  rewrites "ulgraph.adj_relation edge_set = adj_rel"
  using local.is_ulgraph rel_edges_is by simp_all

sublocale ulgraph ⊆ ulgraph_rel "V" "adj_relation"
  rewrites "ulgraph_rel.edge_set adj_relation = E"
  using is_ulgraph_rel edges_rel_is by simp_all

locale sgraph_rel = ulgraph_rel +
  assumes irrefl_adj: "irrefl adj_rel"
begin

lemma irrefl_alt: "adj u v ⟹ u ≠ v"
  using irrefl_adj irrefl_def by fastforce 

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: 
  assumes "(u, v) ∈ adj_relation"
  shows "u ≠ v"
proof -
  have "vert_adj u v" using adj_relation_def assms by blast
  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

lemma is_rel_irrefl: "irrefl adj_relation"
  using irrefl_def is_rel_irrefl_alt by auto

lemma is_sgraph_rel: "sgraph_rel V adj_relation"
  by (unfold_locales) (simp add: is_rel_irrefl)

end

sublocale sgraph_rel ⊆ sgraph V "edge_set"
  rewrites "ulgraph.adj_relation edge_set = adj_rel"
  using is_sgraph rel_edges_is by simp_all

sublocale sgraph ⊆ sgraph_rel V "adj_relation"
  rewrites "ulgraph_rel.edge_set adj_relation = E"
  using is_sgraph_rel edges_rel_is by simp_all

end