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

(* 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)"
  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 ― ‹ Neighbor in graph from Roth \cite{edmonds_roths}›
"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 ― ‹ 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}"

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  eE. vincident v1 e  vincident v2 e" using vert_adj_inc_edge_iff by blast
  assume "eE. 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) = (xX. 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) = (yY. card (all_edges_between X {y}))"
proof -
  have "all_edges_between X Y = (yY. 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 
  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 "VH :: 'a set" EH + G: graph_system "VG :: 'a set" EG for "VH" "EH" "VG" "EG" +
  assumes verts_ss: "VH  VG"
  assumes edges_ss: "EH  EG"

(* 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) 
    (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 VG EG"
  shows "ulgraph VH EH"
  using assms ulgraph.edge_size[ of VG EG] edges_ss by (unfold_locales) auto

lemma is_simp_subgraph:
  assumes "sgraph VG EG"
  shows "sgraph VH EH"
  using assms sgraph.two_edges edges_ss by (unfold_locales) auto

lemma is_finite_subgraph:
  assumes "fin_graph_system VG EG"
  shows "fin_graph_system VH EH"
  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