# Theory Undirected_Graph_Basics

```(* Graph Theory Library Base
Theory: Undirected_Graph_Basics
Author: Chelsea Edmonds

*)

text ‹ This library aims to present a general theory for undirected graphs. The formalisation
approach models edges as sets with two elements, and is inspired in part by the graph theory
basics defined by Lars Noschinski in \<^cite>‹"noschinski_2012"› which are used in \<^cite>‹"edmonds_szemeredis" and "edmonds_roths"›.
Crucially this library makes the definition more flexible by removing the type synonym from vertices
to natural numbers. This is limiting in more advanced mathematical applications, where it is common
for vertices to represent elements of some other set. It additionally extends significantly on basic
graph definitions.

The approach taken in this formalisation is the "locale-centric" approach for modelling different
graph properties, which has been successfully used in other combinatorial structure formalisations. ›

section ‹ Undirected Graph Theory Basics ›

text ‹This first theory focuses on the basics of graph theory (vertices, edges, degree, incidence,
neighbours etc), as well as defining a number of different types of basic graphs.
This theory draws inspiration from \<^cite>‹"noschinski_2012" and "edmonds_szemeredis" and "edmonds_roths"› ›

theory Undirected_Graph_Basics imports Main "HOL-Library.Multiset" "HOL-Library.Disjoint_Sets"
"HOL-Library.Extended_Real" "Girth_Chromatic.Girth_Chromatic_Misc"
begin

subsection ‹ Miscellaneous Extras ›

text ‹ Useful concepts on lists and sets ›
lemma distinct_tl_rev:
assumes "hd xs = last xs"
shows "distinct (tl xs) ⟷ distinct (tl (rev xs))"
using assms
proof (induct xs)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case proof (cases "xs = []")
case True
then show ?thesis by simp
next
case False
then have "a = last xs"
using Cons.prems by auto
then obtain xs' where "xs = xs' @ [last xs]"
by (metis False append_butlast_last_id)
then have tleq: "tl (rev xs) = rev (xs')"
by (metis butlast_rev butlast_snoc rev_rev_ident)
have "distinct (tl (a # xs)) ⟷ distinct xs"  by simp
also have "... ⟷ distinct (rev xs') ∧ a ∉ set (rev xs')"
by (metis False Nil_is_rev_conv ‹a = last xs› distinct.simps(2) distinct_rev hd_rev list.exhaust_sel tleq)
finally show "distinct (tl (a # xs)) ⟷ distinct (tl (rev (a # xs)))"
using tleq by (simp add: False)
qed
qed

lemma last_in_list_set:  "length xs ≥ 1 ⟹ last xs ∈ set (xs)"
using dual_order.strict_trans1 last_in_set by blast

lemma last_in_list_tl_set:
assumes "length xs ≥ 2"
shows "last xs ∈ set (tl xs)"
using assms by (induct xs) auto

lemma length_list_decomp_lt: "ys ≠ [] ⟹ length (xs @zs) < length (xs@ys@zs)"
using length_append by simp

lemma obtains_Max:
assumes "finite A" and "A ≠ {}"
obtains x where "x ∈ A" and "Max A = x"
using assms Max_in by blast

lemma obtains_MAX:
assumes "finite A" and "A ≠ {}"
obtains x where "x ∈ A" and "Max (f ` A) = f x"
using obtains_Max
by (metis (mono_tags, opaque_lifting) assms(1) assms(2) empty_is_image finite_imageI image_iff)

lemma obtains_Min:
assumes "finite A" and "A ≠ {}"
obtains x where "x ∈ A" and "Min A = x"
using assms Min_in by blast

lemma obtains_MIN:
assumes "finite A" and "A ≠ {}"
obtains x where "x ∈ A" and "Min (f ` A) = f x"
using obtains_Min assms empty_is_image finite_imageI image_iff
by (metis (mono_tags, opaque_lifting))

subsection ‹ Initial Set up ›
text ‹For convenience and readability, some functions and type synonyms are defined outside locale context ›

fun mk_triangle_set :: "('a × 'a × 'a) ⇒ 'a set"
where "mk_triangle_set (x, y, z) = {x,y,z}"

type_synonym 'a edge = "'a set"

(* This is preferably not needed, but may be a helpful abbreviation when working outside a locale context *)
type_synonym 'a pregraph = "('a set) × ('a edge set)"

abbreviation gverts :: "'a pregraph ⇒ 'a set" where
"gverts H ≡ fst H"

abbreviation gedges :: "'a pregraph ⇒ 'a edge set" where
"gedges H ≡ snd H"

fun mk_edge :: "'a × 'a ⇒ 'a edge" where
"mk_edge (u,v) = {u,v}"

text ‹All edges is simply the set of subsets of a set S of size 2›
definition "all_edges S ≡ {e . e ⊆ S ∧ card e = 2}"
text ‹ Note, this is a different definition to Noschinski's \<^cite>‹"noschinski_2012"› ugraph which uses
the @{term "mk_edge"} function unnecessarily ›

text ‹ Basic properties of these functions ›
lemma all_edges_mono:
"vs ⊆ ws ⟹ all_edges vs ⊆ all_edges ws"
unfolding all_edges_def by auto

lemma all_edges_alt: "all_edges S = {{x, y} | x y . x ∈ S ∧ y ∈ S ∧ x ≠ y}"
unfolding all_edges_def
proof (intro subset_antisym subsetI)
fix x assume "x ∈ {e. e ⊆ S ∧ card e = 2}"
then obtain u v where "x = {u, v}" and "card {u, v} = 2" and "{u, v} ⊆ S"
by (metis (mono_tags, lifting) card_2_iff mem_Collect_eq)
then show "x ∈ {{x, y} |x y. x ∈ S ∧ y ∈ S ∧ x ≠ y}"
by fastforce
next
show "⋀x. x ∈ {{x, y} |x y. x ∈ S ∧ y ∈ S ∧ x ≠ y} ⟹ x ∈ {e. e ⊆ S ∧ card e = 2}"
by auto
qed

lemma all_edges_alt_pairs: "all_edges S = mk_edge ` {uv ∈ S × S. fst uv ≠ snd uv}"
unfolding all_edges_alt
proof (intro subset_antisym)
have img: "mk_edge ` {uv ∈ S × S. fst uv ≠ snd uv} = {mk_edge (u, v) | u v. (u, v) ∈ S × S ∧ u ≠v}"
by (smt (z3) Collect_cong fst_conv prod.collapse setcompr_eq_image snd_conv)
then show " mk_edge ` {uv ∈ S × S. fst uv ≠ snd uv} ⊆ {{x, y} |x y. x ∈ S ∧ y ∈ S ∧ x ≠ y}"
by auto
show  "{{x, y} |x y. x ∈ S ∧ y ∈ S ∧ x ≠ y} ⊆ mk_edge ` {uv ∈ S × S. fst uv ≠ snd uv}"
using img by simp
qed

lemma all_edges_subset_Pow: "all_edges A ⊆ Pow A"
by (auto simp: all_edges_def)

lemma all_edges_disjoint:  "S ∩ T = {} ⟹ all_edges S ∩ all_edges T = {}"
by (auto simp add: all_edges_def disjoint_iff subset_eq)

lemma card_all_edges: "finite A ⟹ card (all_edges A) = card A choose 2"
using all_edges_def by (metis (full_types) n_subsets)

lemma finite_all_edges: "finite S ⟹ finite (all_edges S)"
by (meson all_edges_subset_Pow finite_Pow_iff finite_subset)

lemma in_mk_edge_img: "(a,b) ∈ A ∨ (b,a) ∈ A ⟹ {a,b} ∈ mk_edge ` A"
by (auto intro: rev_image_eqI)

thm in_mk_edge_img
lemma in_mk_uedge_img_iff: "{a,b} ∈ mk_edge ` A ⟷ (a,b) ∈ A ∨ (b,a) ∈ A"
by (auto simp: doubleton_eq_iff intro: rev_image_eqI)

lemma inj_on_mk_edge: "X ∩ Y = {} ⟹ inj_on mk_edge (X × Y)"
by (auto simp: inj_on_def doubleton_eq_iff)

definition complete_graph :: "'a set ⇒ 'a pregraph" where
"complete_graph S ≡ (S, all_edges S)"

definition all_edges_loops:: "'a set ⇒ 'a edge set"where
"all_edges_loops S ≡ all_edges S ∪ {{v} | v. v ∈ S}"

lemma all_edges_loops_alt: "all_edges_loops S = {e . e ⊆ S ∧ (card e = 2 ∨ card e = 1)}"
proof -
have 1: " {{v} | v. v ∈ S} = {e . e ⊆ S ∧ card e = 1}"
by (metis One_nat_def card.empty card_Suc_eq empty_iff empty_subsetI insert_subset is_singleton_altdef is_singleton_the_elem )
have "{e . e ⊆ S ∧ (card e = 2 ∨ card e = 1)} = {e . e ⊆ S ∧ card e = 2} ∪ {e . e ⊆ S ∧ card e = 1}"
by auto
then have "{e . e ⊆ S ∧ (card e = 2 ∨ card e = 1)} = all_edges S ∪ {{v} | v. v ∈ S}"
then show ?thesis unfolding all_edges_loops_def by simp
qed

lemma loops_disjoint: "all_edges S ∩ {{v} | v. v ∈ S} = {}"
unfolding all_edges_def using card_2_iff
by fastforce

lemma all_edges_loops_ss: "all_edges S ⊆ all_edges_loops S" "{{v} | v. v ∈ S} ⊆ all_edges_loops S"

lemma finite_singletons: "finite S ⟹ finite ({{v} | v. v ∈ S})"
by (auto)

lemma card_singletons:
assumes "finite S" shows "card {{v} | v. v ∈ S} = card S"
using assms
proof (induct S rule: finite_induct)
case empty
then show ?case by simp
next
case (insert x F)
then have disj: "{{x}} ∩ {{v} |v. v ∈ F} = {}" by auto
have "{{v} |v. v ∈ insert x F} = ({{x}} ∪ {{v} |v. v ∈ F})" by auto
then have "card {{v} |v. v ∈ insert x F} = card ({{x}} ∪ {{v} |v. v ∈ F})" by simp
also have "... = card {{x}} + card {{v} |v. v ∈ F}" using card_Un_disjoint disj assms finite_subset
using insert.hyps(1) by force
also have "... = 1 + card {{v} |v. v ∈ F}" using is_singleton_altdef by simp
also have "... = 1 + card F" using insert.hyps by auto
finally show ?case using insert.hyps(1) insert.hyps(2) by force
qed

lemma finite_all_edges_loops: "finite S ⟹ finite (all_edges_loops S)"
unfolding all_edges_loops_def using finite_all_edges finite_singletons by auto

lemma card_all_edges_loops:
assumes "finite S"
shows "card (all_edges_loops S) = (card S) choose 2 + card S"
proof -
have "card (all_edges_loops S) = card (all_edges S ∪ {{v} | v. v ∈ S})"
also have "... = card (all_edges S) + card {{v} | v. v ∈ S}"
using loops_disjoint assms card_Un_disjoint[of "all_edges S" "{{v} | v. v ∈ S}"]
all_edges_loops_ss finite_all_edges_loops finite_subset by fastforce
also have "... = (card S) choose 2 + card {{v} | v. v ∈ S}" by(simp add: card_all_edges assms)
finally show ?thesis using assms card_singletons by auto
qed

subsection ‹ Graph System Locale ›
text ‹ A generic incidence set system re-labeled to graph notation, where repeated edges are not allowed.
All the definitions here do not need the "edge" size to be constrained to make sense. ›

locale graph_system =
fixes vertices :: "'a set" ("V")
fixes edges :: "'a edge set" ("E")
assumes wellformed: "e ∈ E ⟹ e ⊆ V"
begin

(* Basic incidence and adjacency definitions *)
abbreviation gorder :: "nat" where
"gorder ≡ card (V)"

abbreviation graph_size :: "nat" where
"graph_size ≡ card E"

definition vincident :: "'a ⇒ 'a edge ⇒ bool" where
"vincident v e ≡ v ∈ e"

lemma incident_edge_in_wf: "e ∈ E ⟹ vincident v e ⟹ v ∈ V"
using wellformed vincident_def by auto

definition incident_edges :: "'a ⇒ 'a edge set" where
"incident_edges v ≡{e . e ∈ E ∧ vincident v e}"

lemma incident_edges_empty: "¬ (v ∈ V) ⟹ incident_edges v = {}"
using incident_edges_def incident_edge_in_wf by auto

lemma finite_incident_edges: "finite E ⟹ finite (incident_edges v)"

definition edge_adj :: "'a edge ⇒ 'a edge ⇒ bool" where
"edge_adj e1 e2 ≡ e1 ∩ e2 ≠ {} ∧ e1 ∈ E ∧ e2 ∈ E"

lemma edge_adj_inE: "edge_adj e1 e2 ⟹ e1 ∈ E ∧ e2 ∈ E"

lemma edge_adjacent_alt_def: "e1 ∈ E ⟹ e2 ∈ E ⟹ ∃ x . x ∈ V ∧ x ∈ e1 ∧ x ∈ e2 ⟹ edge_adj e1 e2"

lemma wellformed_alt_fst:  "{x, y} ∈ E ⟹ x ∈ V"
using wellformed by auto

lemma wellformed_alt_snd:  "{x, y} ∈ E ⟹ y ∈ V"
using wellformed  by auto
end

text ‹Simple constraints on a graph system may include finite and non-empty constraints ›
locale fin_graph_system = graph_system +
assumes finV: "finite V"
begin

lemma fin_edges: "finite E"
using wellformed finV
by (meson PowI finite_Pow_iff finite_subset subsetI)

end

locale ne_graph_system = graph_system +
assumes not_empty: "V ≠ {}"

subsection ‹ Undirected Graph with Loops ›
text ‹ This formalisation models a loop by a singleton set. In this case a graph has the edge
size criteria if it has edges of size 1 or 2. Notably this removes the option for an edge to be empty ›
locale ulgraph = graph_system +
assumes edge_size: "e ∈ E ⟹ card e > 0 ∧ card e ≤ 2"

begin

lemma alt_edge_size: "e ∈ E ⟹ card e = 1 ∨ card e = 2"
using edge_size by fastforce

definition is_loop:: "'a edge ⇒ bool" where
"is_loop e ≡ card e = 1"

definition is_sedge :: "'a edge ⇒ bool" where
"is_sedge e ≡ card e = 2"

lemma is_edge_or_loop: "e ∈ E ⟹ is_loop e ∨ is_sedge e"
using alt_edge_size is_loop_def is_sedge_def by simp

lemma edges_split_loop: "E = {e ∈ E . is_loop e } ∪ {e ∈ E . is_sedge e}"
using is_edge_or_loop by auto

lemma edges_split_loop_inter_empty: "{} = {e ∈ E . is_loop e } ∩ {e ∈ E . is_sedge e}"
unfolding is_loop_def is_sedge_def by auto

definition vert_adj :: "'a ⇒ 'a ⇒ bool" where ― ‹ Neighbor in graph from Roth \cite{edmonds_roths}›
"vert_adj v1 v2 ≡ {v1, v2} ∈ E"

lemma vert_adj_imp_inV: "vert_adj v1 v2 ⟹ v1 ∈ V ∧ v2 ∈ V"

lemma vert_adj_inc_edge_iff: "vert_adj v1 v2 ⟷ vincident v1 {v1, v2} ∧ vincident v2 {v1, v2} ∧ {v1, v2} ∈ E"

definition neighborhood :: "'a ⇒ 'a set" where ― ‹ Neighbors in Roth Development \cite{edmonds_roths}›
"neighborhood x ≡ {v ∈ V . vert_adj x v}"

lemma neighborhood_incident: "u ∈ neighborhood v ⟷ {u, v} ∈ incident_edges v"
unfolding neighborhood_def incident_edges_def
by (smt (verit) vincident_def insert_commute insert_subset mem_Collect_eq subset_insertI vert_adj_def wellformed)

definition neighbors_ss :: "'a ⇒ 'a set ⇒ 'a set" where
"neighbors_ss x Y ≡ {y ∈ Y . vert_adj x y}"

assumes "v1 ≠ v2"
shows "vert_adj v1 v2 ⟷ (∃ e ∈ E . vincident v1 e ∧ vincident v2 e)"
proof (intro iffI)
show "vert_adj v1 v2 ⟹ ∃e∈E. vincident v1 e ∧ vincident v2 e" using vert_adj_inc_edge_iff by blast
assume "∃e∈E. vincident v1 e ∧ vincident v2 e"
then obtain e where ein: "e ∈ E" and "vincident v1 e" and "vincident v2 e"
using vert_adj_inc_edge_iff assms alt_edge_size by auto
then have "e = {v1, v2}" using alt_edge_size assms
by (smt (verit) card_1_singletonE card_2_iff vincident_def insertE insert_commute singletonD)
by simp
qed

text ‹Incident simple edges, i.e. excluding loops ›
definition incident_sedges :: "'a ⇒ 'a edge set" where
"incident_sedges v ≡ {e ∈ E . vincident v e ∧ card e = 2}"

lemma finite_inc_sedges: "finite E ⟹ finite (incident_sedges v)"

lemma incident_sedges_empty[simp]: "v ∉ V ⟹ incident_sedges v = {}"
unfolding incident_sedges_def using vincident_def wellformed by fastforce

definition has_loop :: "'a ⇒ bool" where
"has_loop v ≡ {v} ∈ E"

lemma has_loop_in_verts: "has_loop v ⟹ v ∈ V"
using has_loop_def wellformed by auto

lemma is_loop_set_alt: "{{v} | v . has_loop v} = {e ∈ E . is_loop e}"
proof (intro subset_antisym subsetI)
fix x assume "x ∈ {{v} |v. has_loop v}"
then obtain v where "x = {v}" and "has_loop v"
by blast
then show "x ∈ {e ∈ E. is_loop e}" using has_loop_def is_loop_def by auto
next
fix x assume a: "x ∈{e ∈ E. is_loop e}"
then have "is_loop x" by blast
then obtain v where "x = {v}" and "{v} ∈ E" using is_loop_def a
by (metis card_1_singletonE mem_Collect_eq)
thus "x ∈ {{v} |v. has_loop v}" using has_loop_def by simp
qed

definition incident_loops :: "'a ⇒ 'a edge set" where
"incident_loops v ≡ {e ∈ E. e = {v}}"

lemma card1_incident_imp_vert: "vincident v e ∧ card e = 1 ⟹ e = {v}"
by (metis card_1_singletonE vincident_def singleton_iff)

lemma incident_loops_alt: "incident_loops v = {e ∈ E. vincident v e ∧ card e = 1}"
unfolding incident_loops_def using card1_incident_imp_vert vincident_def by auto

lemma incident_loops_simp: "has_loop v ⟹ incident_loops v = {{v}}" "¬ has_loop v ⟹ incident_loops v = {}"
unfolding incident_loops_def has_loop_def by auto

lemma incident_loops_union: "⋃ (incident_loops ` V) = {e ∈ E . is_loop e}"
proof -
have "V = {v ∈ V. has_loop v} ∪ {v ∈ V . ¬ has_loop v}"
by auto
then have "⋃ (incident_loops ` V) = ⋃ (incident_loops ` {v ∈ V. has_loop v}) ∪
⋃ (incident_loops ` {v ∈ V. ¬ has_loop v})" by auto
also have "... = ⋃ (incident_loops ` {v ∈ V. has_loop v})" using incident_loops_simp(2) by simp
also have "... = ⋃ ({{{v}} | v . has_loop v})" using has_loop_in_verts incident_loops_simp(1) by auto
also have "... = ({{v} | v . has_loop v})" by auto
finally show ?thesis using is_loop_set_alt by simp
qed

lemma finite_incident_loops: "finite (incident_loops v)"
using incident_loops_simp by (cases "has_loop v") auto

lemma incident_loops_card: "card (incident_loops v) ≤ 1"
by (cases "has_loop v") (simp_all add: incident_loops_simp)

lemma incident_edges_union: "incident_edges v = incident_sedges v ∪ incident_loops v"
unfolding incident_edges_def incident_sedges_def incident_loops_alt using alt_edge_size
by auto

lemma incident_edges_sedges[simp]: "¬ has_loop v ⟹ incident_edges v = incident_sedges v"
using incident_edges_union incident_loops_simp by auto

lemma incident_sedges_union: "⋃ (incident_sedges ` V) = {e ∈ E . is_sedge e}"
proof (intro subset_antisym subsetI)
fix x assume "x ∈ ⋃ (incident_sedges ` V)"
then obtain v where "x ∈ incident_sedges v" by blast
then show "x ∈ {e ∈ E. is_sedge e}" using incident_sedges_def is_sedge_def by auto
next
fix x assume "x ∈ {e ∈ E. is_sedge e}"
then have xin: "x ∈ E" and c2: "card x = 2" using is_sedge_def by auto
then obtain v where "v ∈ x" and vin: "v ∈ V" using wellformed
by (meson card_2_iff' subsetD)
then have "x ∈ incident_sedges v" unfolding incident_sedges_def vincident_def using xin c2 by auto
then show "x ∈ ⋃ (incident_sedges ` V)" using vin by auto
qed

lemma empty_not_edge: "{} ∉ E"
using edge_size by fastforce

text ‹ The degree definition is complicated by loops - each loop contributes two to degree.
This is required for basic counting properties on the degree to hold›
definition degree :: "'a ⇒ nat" where
"degree v ≡ card (incident_sedges v) + 2 * (card (incident_loops v))"

lemma degree_no_loops[simp]: "¬ has_loop v ⟹ degree v = card (incident_edges v)"
using incident_edges_sedges degree_def incident_loops_simp(2) by auto

lemma degree_none[simp]: "¬ v  ∈ V ⟹ degree v = 0"
using degree_def degree_no_loops has_loop_in_verts incident_edges_sedges incident_sedges_empty by auto

lemma degree0_inc_edges_empt_iff:
assumes "finite E"
shows "degree v = 0 ⟷ incident_edges v = {}"
proof (intro iffI)
assume "degree v = 0"
then have "card (incident_sedges v) + 2 * (card (incident_loops v)) = 0" using degree_def by simp
then have "incident_sedges v = {}" and "incident_loops v = {}"
using degree_def incident_edges_union assms finite_incident_edges finite_incident_loops by auto
thus "incident_edges v = {}" using incident_edges_union by auto
next
show "incident_edges v = {} ⟹ degree v = 0" using incident_edges_union degree_def
by simp
qed

lemma incident_edges_neighbors_img: "incident_edges v = (λ u . {v, u}) ` (neighborhood v)"
proof (intro subset_antisym subsetI)
fix x assume a: "x ∈ incident_edges v"
then have xE: "x ∈ E" and vx: "v ∈ x" using incident_edges_def vincident_def by auto
then obtain u where "x = {u, v}" using alt_edge_size
by (smt (verit, best) card_1_singletonE card_2_iff insertE insert_absorb2 insert_commute singletonD)
then have "u ∈ neighborhood v"
using a neighborhood_incident by blast
then show "x ∈ (λu. {v, u}) ` neighborhood v" using ‹x = {u, v}› by blast
next
fix x assume "x ∈ (λu. {v, u}) ` neighborhood v"
then obtain u' where "x = {v, u'}" and "u' ∈ neighborhood v"
by blast
then show "x ∈ incident_edges v"
qed

lemma card_incident_sedges_neighborhood: "card (incident_edges v) = card (neighborhood v)"
proof -
have "bij_betw (λ u . {v, u}) (neighborhood v) (incident_edges v)"
by(intro bij_betw_imageI inj_onI, simp_all add:incident_edges_neighbors_img)(metis doubleton_eq_iff)
thus ?thesis
by (metis bij_betw_same_card)
qed

lemma degree0_neighborhood_empt_iff:
assumes "finite E"
shows "degree v = 0 ⟷ neighborhood v = {}"
using degree0_inc_edges_empt_iff incident_edges_neighbors_img

definition is_isolated_vertex:: "'a ⇒ bool" where
"is_isolated_vertex v ≡ v ∈ V ∧ (∀ u ∈ V . ¬ vert_adj u v)"

lemma is_isolated_vertex_edge: "is_isolated_vertex v ⟹ (⋀ e. e ∈ E ⟹ ¬ (vincident v e))"
unfolding is_isolated_vertex_def
by (metis (full_types) all_not_in_conv vincident_def insert_absorb insert_iff mk_disjoint_insert

lemma is_isolated_vertex_no_loop: "is_isolated_vertex v ⟹ ¬ has_loop v"
unfolding has_loop_def is_isolated_vertex_def vert_adj_def by auto

lemma is_isolated_vertex_degree0: "is_isolated_vertex v ⟹ degree v = 0"
proof -
assume assm: "is_isolated_vertex v"
then have "¬ has_loop v" using is_isolated_vertex_no_loop by simp
then have "degree v = card (incident_edges v)" using degree_no_loops by auto
moreover have "⋀ e. e ∈ E ⟹ ¬ (vincident v e)"
using is_isolated_vertex_edge assm by auto
then have "(incident_edges v) = {}" unfolding incident_edges_def by auto
ultimately show "degree v = 0" by simp
qed

lemma iso_vertex_empty_neighborhood: "is_isolated_vertex v ⟹ neighborhood v = {}"
using is_isolated_vertex_def neighborhood_def
by (metis (mono_tags, lifting) Collect_empty_eq is_isolated_vertex_edge vert_adj_inc_edge_iff)

definition max_degree :: "nat" where
"max_degree ≡ Max {degree v | v. v ∈ V}"

definition min_degree :: "nat" where
"min_degree ≡ Min {degree v | v . v ∈ V}"

definition is_edge_between :: "'a set ⇒ 'a set ⇒ 'a edge ⇒ bool" where
"is_edge_between X Y e ≡ ∃ x y. e = {x, y} ∧ x ∈ X ∧ y ∈ Y"

text ‹All edges between two sets of vertices, @{term X} and @{term Y}, in a graph, @{term G}.
Inspired by Szemeredi development \<^cite>‹"edmonds_szemeredis"› and generalised here ›

definition all_edges_between :: "'a set ⇒ 'a set ⇒ ('a × 'a) set" where
"all_edges_between X Y ≡ {(x, y) . x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"

lemma all_edges_betw_D3: "(x, y) ∈ all_edges_between X Y ⟹ {x, y} ∈ E"

lemma all_edges_betw_I: "x ∈ X ⟹ y ∈ Y ⟹ {x, y} ∈ E ⟹ (x, y) ∈ all_edges_between X Y"

lemma all_edges_between_subset: "all_edges_between X Y ⊆ X×Y"
by (auto simp: all_edges_between_def)

lemma all_edges_between_E_ss: "mk_edge ` all_edges_between X Y ⊆ E"

lemma all_edges_between_rem_wf: "all_edges_between X Y = all_edges_between (X ∩ V) (Y ∩ V)"
using wellformed by (simp add: all_edges_between_def) blast

lemma all_edges_between_empty [simp]:
"all_edges_between {} Z = {}" "all_edges_between Z {} = {}"
by (auto simp: all_edges_between_def)

lemma all_edges_between_disjnt1: "disjnt X Y ⟹ disjnt (all_edges_between X Z) (all_edges_between Y Z)"
by (auto simp: all_edges_between_def disjnt_iff)

lemma all_edges_between_disjnt2: "disjnt Y Z ⟹ disjnt (all_edges_between X Y) (all_edges_between X Z)"
by (auto simp: all_edges_between_def disjnt_iff)

lemma max_all_edges_between:
assumes "finite X" "finite Y"
shows "card (all_edges_between X Y) ≤ card X * card Y"
by (metis assms card_mono finite_SigmaI all_edges_between_subset card_cartesian_product)

lemma all_edges_between_Un1:
"all_edges_between (X ∪ Y) Z = all_edges_between X Z ∪ all_edges_between Y Z"
by (auto simp: all_edges_between_def)

lemma all_edges_between_Un2:
"all_edges_between X (Y ∪ Z) = all_edges_between X Y ∪ all_edges_between X Z"
by (auto simp: all_edges_between_def)

lemma finite_all_edges_between:
assumes "finite X" "finite Y"
shows "finite (all_edges_between X Y)"
by (meson all_edges_between_subset assms finite_cartesian_product finite_subset)

lemma all_edges_between_Union1:
"all_edges_between (Union 𝒳) Y = (⋃X∈𝒳. all_edges_between X Y)"
by (auto simp: all_edges_between_def)

lemma all_edges_between_Union2:
"all_edges_between X (Union 𝒴) = (⋃Y∈𝒴. all_edges_between X Y)"
by (auto simp: all_edges_between_def)

lemma all_edges_between_disjoint1:
assumes "disjoint R"
shows "disjoint ((λX. all_edges_between X Y) ` R)"
using assms by (auto simp: all_edges_between_def disjoint_def)

lemma all_edges_between_disjoint2:
assumes "disjoint R"
shows "disjoint ((λY. all_edges_between X Y) ` R)"
using assms by (auto simp: all_edges_between_def disjoint_def)

lemma all_edges_between_disjoint_family_on1:
assumes "disjoint R"
shows "disjoint_family_on (λX. all_edges_between X Y) R"
by (metis (no_types, lifting) all_edges_between_disjnt1 assms disjnt_def disjoint_family_on_def pairwiseD)

lemma all_edges_between_disjoint_family_on2:
assumes "disjoint R"
shows "disjoint_family_on (λY. all_edges_between X Y) R"
by (metis (no_types, lifting) all_edges_between_disjnt2 assms disjnt_def disjoint_family_on_def pairwiseD)

lemma all_edges_between_mono1:
"Y ⊆ Z ⟹ all_edges_between Y X ⊆ all_edges_between Z X"
by (auto simp: all_edges_between_def)

lemma all_edges_between_mono2:
"Y ⊆ Z ⟹ all_edges_between X Y ⊆ all_edges_between X Z"
by (auto simp: all_edges_between_def)

lemma inj_on_mk_edge: "X ∩ Y = {} ⟹ inj_on mk_edge (all_edges_between X Y)"
by (auto simp: inj_on_def doubleton_eq_iff all_edges_between_def)

lemma all_edges_between_subset_times: "all_edges_between X Y ⊆ (X ∩ ⋃E) × (Y ∩ ⋃E)"
by (auto simp: all_edges_between_def)

lemma all_edges_betw_prod_def_neighbors: "all_edges_between X Y = {(x, y) ∈ X × Y . vert_adj x y }"

lemma all_edges_betw_sigma_neighbor:
"all_edges_between X Y = (SIGMA x:X. neighbors_ss x Y)"

lemma card_all_edges_betw_neighbor:
assumes "finite X" "finite Y"
shows "card (all_edges_between X Y) = (∑x∈X. card (neighbors_ss x Y))"
using all_edges_betw_sigma_neighbor assms by (simp add: neighbors_ss_def)

lemma all_edges_between_swap:
"all_edges_between X Y = (λ(x,y). (y,x)) ` (all_edges_between Y X)"
unfolding all_edges_between_def
by (auto simp add: insert_commute image_iff split: prod.split)

lemma card_all_edges_between_commute:
"card (all_edges_between X Y) = card (all_edges_between Y X)"
proof -
have "inj_on (λ(x, y). (y, x)) A" for A :: "(nat*nat)set"
by (auto simp: inj_on_def)
then show ?thesis using all_edges_between_swap [of X Y] card_image
by (metis swap_inj_on)
qed

lemma all_edges_between_set: "mk_edge ` all_edges_between X Y = {{x, y}| x y. x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"
unfolding all_edges_between_def
proof (intro subset_antisym subsetI)
fix e assume "e ∈ mk_edge ` {(x, y). x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"
then obtain x y where "e = mk_edge (x, y)" and "x ∈ X" and "y ∈ Y" and "{x, y} ∈ E"
by blast
then show "e ∈ {{x, y} |x y. x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"
by auto
next
fix e assume "e ∈ {{x, y} |x y. x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"
then obtain x y where "e ={x, y}" and "x ∈ X" and "y ∈ Y" and "{x, y} ∈ E"
by blast
then have "e = mk_edge (x, y)"
by auto
then show "e ∈ mk_edge ` {(x, y). x ∈ X ∧ y ∈ Y ∧ {x, y} ∈ E}"
using ‹x ∈ X› ‹y ∈ Y› ‹{x, y} ∈ E› by blast
qed

subsection ‹Edge Density›

text ‹The edge density between two sets of vertices, @{term X} and @{term Y}, in @{term G}.
This is the same definition as taken in the Szemeredi development, generalised here \<^cite>‹"edmonds_szemeredis"››

definition "edge_density X Y ≡ card (all_edges_between X Y)/(card X * card Y)"
lemma edge_density_ge0: "edge_density X Y ≥ 0"
by (auto simp: edge_density_def)

lemma edge_density_le1: "edge_density X Y ≤ 1"
proof (cases "finite X ∧ finite Y")
case True
then show ?thesis
using of_nat_mono [OF max_all_edges_between, of X Y]
by (fastforce simp add: edge_density_def divide_simps)
qed (auto simp: edge_density_def)

lemma edge_density_zero:  "Y = {} ⟹ edge_density X Y = 0"

lemma edge_density_commute: "edge_density X Y = edge_density Y X"
by (simp add: edge_density_def card_all_edges_between_commute mult.commute)

lemma edge_density_Un:
assumes "disjnt X1 X2" "finite X1" "finite X2" "finite Y"
shows "edge_density (X1 ∪ X2) Y = (edge_density X1 Y * card X1 + edge_density X2 Y * card X2) / (card X1 + card X2)"
using assms unfolding edge_density_def
by (simp add: all_edges_between_disjnt1 all_edges_between_Un1 finite_all_edges_between card_Un_disjnt divide_simps)

lemma edge_density_eq0:
assumes "all_edges_between A B = {}" and "X ⊆ A" "Y ⊆ B"
shows "edge_density X Y  = 0"
proof -
have "all_edges_between X Y = {}"
by (metis all_edges_between_mono1 all_edges_between_mono2 assms subset_empty)
then show ?thesis
by (auto simp: edge_density_def)
qed

end

text ‹A number of lemmas are limited to a finite graph ›
locale fin_ulgraph = ulgraph + fin_graph_system
begin

lemma card_is_has_loop_eq: "card {e ∈ E . is_loop e} = card {v ∈ V . has_loop v}"
proof -
have "⋀ e . e ∈ E ⟹ is_loop e ⟷ (∃ v. e = {v})" using is_loop_def
using is_singleton_altdef is_singleton_def by blast
define f :: "'a ⇒ 'a set"  where "f = (λ v . {v})"
have feq: "f ` {v ∈ V . has_loop v} = {{v} | v . has_loop v}" using has_loop_in_verts f_def by auto
have "inj_on f {v ∈ V . has_loop v}" by (simp add: f_def)
then have "card {v ∈ V . has_loop v} = card (f ` {v ∈ V . has_loop v})"
using card_image by fastforce
also have "... = card {{v} | v . has_loop v}" using feq by simp
finally have "card {v ∈ V . has_loop v} = card {e ∈ E . is_loop e}" using is_loop_set_alt by simp
thus "card {e ∈ E . is_loop e} = card {v ∈ V . has_loop v}" by simp
qed

lemma finite_all_edges_between': "finite (all_edges_between X Y)"
using finV wellformed
by (metis all_edges_between_rem_wf finite_Int finite_all_edges_between)

lemma card_all_edges_between:
assumes "finite Y"
shows "card (all_edges_between X Y) = (∑y∈Y. card (all_edges_between X {y}))"
proof -
have "all_edges_between X Y = (⋃y∈Y. all_edges_between X {y})"
by (auto simp: all_edges_between_def)
moreover have "disjoint_family_on (λy. all_edges_between X {y}) Y"
unfolding disjoint_family_on_def
by (auto simp: disjoint_family_on_def all_edges_between_def)
ultimately show ?thesis
by (simp add: card_UN_disjoint' assms finite_all_edges_between')
qed

end

subsection ‹Simple Graphs ›

text ‹ A simple graph (or sgraph) constrains edges to size of two. This is the classic definition
of an undirected graph ›

locale sgraph = graph_system +
assumes two_edges: "e ∈ E ⟹ card e = 2"
begin

lemma wellformed_all_edges: "E ⊆ all_edges V"
unfolding all_edges_def using wellformed two_edges by auto

lemma e_in_all_edges: "e ∈ E ⟹ e ∈ all_edges V"
using wellformed_all_edges by auto

lemma e_in_all_edges_ss: "e ∈ E ⟹ e ⊆ V' ⟹ V' ⊆ V ⟹ e ∈ all_edges V'"
unfolding all_edges_def using wellformed two_edges by auto

lemma singleton_not_edge: "{x} ∉ E" ― ‹ Suggested by Mantas Baksys ›
using two_edges by fastforce

end

text ‹ It is easy to proof that @{term "sgraph"} is a sublocale of @{term "ulgraph"}. By using indirect inheritance,
we avoid two unneeded cardinality conditions ›
sublocale sgraph ⊆ ulgraph V E

locale fin_sgraph = sgraph + fin_graph_system
begin

lemma fin_neighbourhood: "finite (neighborhood x)"
unfolding neighborhood_def using finV by simp

lemma fin_all_edges: "finite (all_edges V)"
unfolding all_edges_def by (simp add: finV)

lemma max_edges_graph:  "card E ≤ (card V)^2"
proof -
have "card E ≤ card V choose 2"
by (metis fin_all_edges finV card_all_edges card_mono wellformed_all_edges)
thus ?thesis
by (metis binomial_le_pow le0 neq0_conv order.trans zero_less_binomial_iff)
qed

end

sublocale fin_sgraph ⊆ fin_ulgraph
by (unfold_locales)

context sgraph
begin

lemma no_loops: "v ∈ V ⟹ ¬ has_loop v"
using has_loop_def two_edges by fastforce

text ‹Ideally, we'd redefine degree in the context of a simple graph. However, this requires
a named loop locale, which complicates notation unnecessarily. This is the lemma that should always
be used when unfolding the degree definition in a simple graph context ›
lemma alt_degree_def[simp]: "degree v = card (incident_edges v)"
using no_loops degree_no_loops  degree_none incident_edges_empty by (cases "v ∈ V") simp_all

lemma alt_deg_neighborhood: "degree v = card (neighborhood v)"
using card_incident_sedges_neighborhood by simp

definition degree_set :: "'a set ⇒ nat" where
"degree_set vs ≡ card {e ∈ E. vs ⊆ e}"

definition is_complete_n_graph:: "nat ⇒ bool" where
"is_complete_n_graph n ≡ gorder = n ∧ E = all_edges V"

text ‹ The complement of a graph is a basic concept ›

definition is_complement :: "'a pregraph ⇒ bool" where
"is_complement G ≡ V = gverts G ∧ gedges G = all_edges V - E"

definition complement_edges :: "'a edge set" where
"complement_edges ≡ all_edges V - E"

lemma is_complement_edges: "is_complement (V', E')  ⟷ V = V' ∧ complement_edges = E'"
unfolding is_complement_def complement_edges_def by auto

interpretation G_comp: sgraph V "complement_edges"
by (unfold_locales)(auto simp add: complement_edges_def all_edges_def)

lemma is_complement_edge_iff: "e ⊆ V ⟹ e ∈ complement_edges ⟷ e ∉ E ∧ card e = 2"
unfolding complement_edges_def all_edges_def by auto

end

text ‹A complete graph is a simple graph ›

lemma complete_sgraph: "sgraph S (all_edges S)"
unfolding all_edges_def by (unfold_locales) (simp_all)

interpretation comp_sgraph: sgraph S "(all_edges S)"
using complete_sgraph by auto

lemma complete_fin_sgraph: "finite S ⟹ fin_sgraph S (all_edges S)"
using complete_sgraph
by (intro_locales) (auto simp add: sgraph.axioms(1) sgraph_def fin_graph_system_axioms_def)

subsection ‹ Subgraph Basics ›

text ‹ A subgraph is defined as a graph where the vertex and edge sets are subsets of the original graph.
Note that using the locale approach, we require each graph to be wellformed. This is interestingly
omitted in a number of other formal definitions.  ›
locale subgraph = H: graph_system "V⇩H :: 'a set" E⇩H + G: graph_system "V⇩G :: 'a set" E⇩G for "V⇩H" "E⇩H" "V⇩G" "E⇩G" +
assumes verts_ss: "V⇩H ⊆ V⇩G"
assumes edges_ss: "E⇩H ⊆ E⇩G"

(* An intro rule *)
lemma is_subgraphI[intro]: "V' ⊆ V ⟹ E' ⊆ E ⟹ graph_system V' E' ⟹ graph_system V E ⟹ subgraph V' E' V E"
using graph_system_def by (unfold_locales)

context subgraph
begin

text ‹ Note: it could also be useful to have similar rules in @{term "ulgraph"} locale etc with
subgraph assumption ›
lemma is_subgraph_ulgraph:
assumes "ulgraph V⇩G E⇩G"
shows "ulgraph V⇩H E⇩H"
using assms ulgraph.edge_size[ of V⇩G E⇩G] edges_ss by (unfold_locales) auto

lemma is_simp_subgraph:
assumes "sgraph V⇩G E⇩G"
shows "sgraph V⇩H E⇩H"
using assms sgraph.two_edges edges_ss by (unfold_locales) auto

lemma is_finite_subgraph:
assumes "fin_graph_system V⇩G E⇩G"
shows "fin_graph_system V⇩H E⇩H"
using assms verts_ss
by (unfold_locales) (simp add: fin_graph_system.finV finite_subset)

lemma (in graph_system) subgraph_refl: "subgraph V E V E"

lemma subgraph_trans:
assumes "graph_system V E"
assumes "graph_system V' E'"
assumes "graph_system V'' E''"
shows "subgraph V'' E'' V' E' ⟹ subgraph V' E' V E ⟹ subgraph V'' E'' V E"
by (meson assms(1) assms(3) is_subgraphI subgraph.edges_ss subgraph.verts_ss subset_trans)

lemma subgraph_antisym: "subgraph V' E' V E ⟹ subgraph V E V' E' ⟹ V = V' ∧ E = E'"
by (simp add: dual_order.eq_iff subgraph.edges_ss subgraph.verts_ss)

end

lemma (in sgraph) subgraph_complete: "subgraph V E V (all_edges V)"
proof -
interpret comp: sgraph V "(all_edges V)"
using complete_sgraph by auto
show ?thesis by (unfold_locales) (simp_all add: wellformed_all_edges)
qed

text ‹ We are often interested in the set of subgraphs. This is still very possible using locale definitions.
Interesting Note - random graphs \<^cite>‹"Hupel_Random"› has a different definition for the well formed
constraint to be added in here instead of in the main subgraph definition›

definition (in graph_system) subgraphs:: "'a pregraph set" where
"subgraphs ≡ {G . subgraph (gverts G) (gedges G) V E}"

text ‹ Induced subgraph - really only affects edges ›
definition (in graph_system) induced_edges:: "'a set ⇒ 'a edge set" where
"induced_edges V' ≡ {e ∈ E. e ⊆ V'}"

lemma (in sgraph) induced_edges_alt: "induced_edges V' = E ∩ all_edges V'"
unfolding induced_edges_def all_edges_def using two_edges by blast

lemma (in sgraph) induced_edges_self: "induced_edges V = E"
unfolding induced_edges_def
by (simp add: subsetI subset_antisym wellformed)

context graph_system
begin

lemma induced_edges_ss: "V' ⊆ V ⟹ induced_edges V' ⊆ E"
unfolding induced_edges_def by auto

lemma induced_is_graph_sys: "graph_system V' (induced_edges V')"

interpretation induced_graph: graph_system V' "(induced_edges V')"
using induced_is_graph_sys by simp

lemma induced_is_subgraph: "V' ⊆ V ⟹ subgraph V' (induced_edges V') V E"
using induced_edges_ss by (unfold_locales) auto

lemma induced_edges_union:
assumes "VH1 ⊆ S" "VH2 ⊆ T"
assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
assumes "EH1 ∪ EH2 ⊆ (induced_edges (S ∪ T))"
shows "EH1 ⊆ (induced_edges S)"
proof (intro subsetI, simp add: induced_edges_def, intro conjI)
show "⋀x. x ∈ EH1 ⟹ x ∈ E" using assms(5)
show "⋀x. x ∈ EH1 ⟹ x ⊆ S"
using assms(1) assms(3) graph_system.wellformed by blast
qed

lemma induced_edges_union_subgraph_single:
assumes "VH1 ⊆ S" "VH2 ⊆ T"
assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
assumes "subgraph (VH1 ∪ VH2) (EH1 ∪ EH2) (S ∪ T) (induced_edges (S ∪ T))"
shows "subgraph VH1 EH1 S (induced_edges S)"
proof -
interpret ug: subgraph "(VH1 ∪ VH2)" "(EH1 ∪ EH2)" "(S ∪ T)" "(induced_edges (S ∪ T))"
using assms(5) by simp
show "subgraph VH1 EH1 S (induced_edges S)"
using assms(3) graph_system_def
by (unfold_locales) (blast, simp add: assms(1), meson assms induced_edges_union ug.edges_ss)
qed

lemma induced_union_subgraph:
assumes "VH1 ⊆ S" and "VH2 ⊆ T"
assumes "graph_system VH1 EH1" "graph_system VH2 EH2"
shows "subgraph VH1 EH1 S (induced_edges S) ∧ subgraph VH2 EH2 T (induced_edges T) ⟷
subgraph (VH1 ∪ VH2) (EH1 ∪ EH2) (S ∪ T) (induced_edges (S ∪ T))"
proof (intro iffI conjI, elim conjE)
show "subgraph (VH1 ∪ VH2) (EH1 ∪ EH2) (S ∪ T) (induced_edges (S ∪ T))
⟹ subgraph VH1 EH1 S (induced_edges S)"
using induced_edges_union_subgraph_single assms by simp
show "subgraph (VH1 ∪ VH2) (EH1 ∪ EH2) (S ∪ T) (induced_edges (S ∪ T))
⟹ subgraph VH2 EH2 T (induced_edges T)"
using induced_edges_union_subgraph_single assms by (simp add: Un_commute)
assume a1: "subgraph VH1 EH1 S (induced_edges S)" and a2: "subgraph VH2 EH2 T (induced_edges T)"
then interpret h1: subgraph VH1 EH1 S "(induced_edges S)"
by simp
interpret h2: subgraph VH2 EH2 T "(induced_edges T)" using a2 by simp
show "subgraph (VH1 ∪ VH2) (EH1 ∪ EH2) (S ∪ T) (induced_edges (S ∪ T))"
using h1.H.wellformed h2.H.wellformed h1.verts_ss h2.verts_ss h1.edges_ss h2.edges_ss
by (unfold_locales) (auto simp add: induced_edges_def)
qed

end
end```