Theory Undirected_Graph_Basics
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"
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}"
by (simp add: all_edges_def 1)
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"
by (simp_all add: all_edges_loops_def)
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})"
by (simp add: all_edges_loops_def)
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
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)"
by (simp add: incident_edges_def)
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"
using edge_adj_def by auto
lemma edge_adjacent_alt_def: "e1 ∈ E ⟹ e2 ∈ E ⟹ ∃ x . x ∈ V ∧ x ∈ e1 ∧ x ∈ e2 ⟹ edge_adj e1 e2"
unfolding edge_adj_def by auto
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
"vert_adj v1 v2 ≡ {v1, v2} ∈ E"
lemma vert_adj_sym: "vert_adj v1 v2 ⟷ vert_adj v2 v1"
unfolding vert_adj_def by (simp_all add: insert_commute)
lemma vert_adj_imp_inV: "vert_adj v1 v2 ⟹ v1 ∈ V ∧ v2 ∈ V"
using vert_adj_def wellformed by auto
lemma vert_adj_inc_edge_iff: "vert_adj v1 v2 ⟷ vincident v1 {v1, v2} ∧ vincident v2 {v1, v2} ∧ {v1, v2} ∈ E"
unfolding vert_adj_def vincident_def by auto
lemma not_vert_adj[simp]: "¬ vert_adj v u ⟹ {v, u} ∉ E"
by (simp add: vert_adj_def)
definition neighborhood :: "'a ⇒ 'a set" where
"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}"
lemma vert_adj_edge_iff2:
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)
then show "vert_adj v1 v2" using ein vert_adj_def
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)"
by (simp add: incident_sedges_def)
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"
by (simp add: insert_commute neighborhood_incident)
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
by (simp add: assms)
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
vert_adj_def vert_adj_edge_iff2 vert_adj_imp_inV)
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"
by (simp add: all_edges_between_def)
lemma all_edges_betw_I: "x ∈ X ⟹ y ∈ Y ⟹ {x, y} ∈ E ⟹ (x, y) ∈ all_edges_between X Y"
by (simp add: all_edges_between_def)
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"
by (auto simp add: all_edges_between_def)
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 }"
by (auto simp: vert_adj_def all_edges_between_def)
lemma all_edges_betw_sigma_neighbor:
"all_edges_between X Y = (SIGMA x:X. neighbors_ss x Y)"
by (auto simp add: all_edges_between_def neighbors_ss_def vert_adj_def)
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"
by (simp add: edge_density_def)
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"
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
by (unfold_locales)(simp add: two_edges)
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"
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)
(auto simp add: graph_system.vincident_def graph_system.incident_edge_in_wf)
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"
by (simp add: graph_system_axioms is_subgraphI)
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')"
by (unfold_locales) (simp add: induced_edges_def)
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)
by (simp add: induced_edges_def subset_iff)
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