Theory Ugraph_Lemmas

section‹Lemmas about undirected graphs›

theory Ugraph_Lemmas
imports
  Prob_Lemmas
  Girth_Chromatic.Girth_Chromatic
begin

text‹The complete graph is a graph where all possible edges are present. It is wellformed by
definition.›

definition complete :: "nat set ⇒ ugraph" where
  "complete V = (V, all_edges V)"

lemma complete_wellformed: "uwellformed (complete V)"
  unfolding complete_def uwellformed_def all_edges_def
  by simp

text‹If the set of vertices is finite, the set of edges in the complete graph is finite.›

lemma all_edges_finite: "finite V ⟹ finite (all_edges V)"
  unfolding all_edges_def
  by simp

corollary complete_finite_edges: "finite V ⟹ finite (uedges (complete V))"
  unfolding complete_def using all_edges_finite
  by simp

text‹The sets of possible edges of disjoint sets of vertices are disjoint.›

lemma all_edges_disjoint: "S ∩ T = {} ⟹ all_edges S ∩ all_edges T = {}"
  unfolding all_edges_def
  by force

text‹A graph is called `finite' if its set of edges and its set of vertices are finite.›

definition "finite_graph G ≡ finite (uverts G) ∧ finite (uedges G)"

text‹The complete graph is finite.›

corollary complete_finite: "finite V ⟹ finite_graph (complete V)"
  using complete_finite_edges unfolding finite_graph_def complete_def
  by simp

text‹A graph is called `nonempty' if it contains at least one vertex and at least one edge.›

definition "nonempty_graph G ≡ uverts G ≠ {} ∧ uedges G ≠ {}"

text‹A random graph is both wellformed and finite.›

lemma (in edge_space) wellformed_and_finite:
  assumes "E ∈ Pow S_edges"
  shows "finite_graph (edge_ugraph E)" "uwellformed (edge_ugraph E)"
unfolding finite_graph_def
proof
  show "finite (uverts (edge_ugraph E))"
    unfolding edge_ugraph_def S_verts_def by simp
next
  show "finite (uedges (edge_ugraph E))"
    using assms unfolding edge_ugraph_def S_edges_def by (auto intro: all_edges_finite)
next
  show "uwellformed (edge_ugraph E)"
    using complete_wellformed unfolding edge_ugraph_def S_edges_def complete_def uwellformed_def by force
qed

text‹The probability for a random graph to have $e$ edges is $p ^ e$.›

lemma (in edge_space) cylinder_empty_prob:
  "A ⊆ S_edges ⟹ prob (cylinder S_edges A {}) = p ^ (card A)"
  using cylinder_prob by auto

subsection‹Subgraphs›

definition subgraph :: "ugraph ⇒ ugraph ⇒ bool" where
  "subgraph G' G ≡ uverts G' ⊆ uverts G ∧ uedges G' ⊆ uedges G"

lemma subgraph_refl: "subgraph G G"
  unfolding subgraph_def
  by simp

lemma subgraph_trans: "subgraph G'' G' ⟹ subgraph G' G ⟹ subgraph G'' G"
  unfolding subgraph_def
  by auto

lemma subgraph_antisym: "subgraph G G' ⟹ subgraph G' G ⟹ G = G'"
  unfolding subgraph_def
  by (auto simp add: Product_Type.prod_eqI)

lemma subgraph_complete:
  assumes "uwellformed G"
  shows "subgraph G (complete (uverts G))"
proof -
  {
    fix e
    assume "e ∈ uedges G"
    with assms have "card e = 2" and u: "⋀u. u ∈ e ⟹ u ∈ uverts G"
      unfolding uwellformed_def by auto
    moreover then obtain u v where "e = {u, v}" "u ≠ v"
      by (metis card_2_elements)
    ultimately have "e = mk_uedge (u, v)" "u ∈ uverts G" "v ∈ uverts G"
      by auto
    hence "e ∈ all_edges (uverts G)"
      unfolding all_edges_def using ‹u ≠ v› by fastforce
  }
  thus ?thesis
    unfolding complete_def subgraph_def by auto
qed

corollary wellformed_all_edges: "uwellformed G ⟹ uedges G ⊆ all_edges (uverts G)"
  using subgraph_complete subgraph_def complete_def by simp

corollary max_edges_graph: 
  assumes "uwellformed G" "finite (uverts G)"
  shows "card (uedges G) ≤ (card (uverts G))^2"
proof -
  have "card (uedges G) ≤ card (uverts G) choose 2" 
    by (metis all_edges_finite assms 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

lemma subgraph_finite: "⟦ finite_graph G; subgraph G' G ⟧ ⟹ finite_graph G'"
  unfolding finite_graph_def subgraph_def
  by (metis rev_finite_subset)

corollary wellformed_finite:
  assumes "finite (uverts G)" and "uwellformed G"
  shows "finite_graph G"
proof (rule subgraph_finite[where G = "complete (uverts G)"])
  show "subgraph G (complete (uverts G))"
    using assms by (simp add: subgraph_complete)
next
  have "finite (uedges (complete (uverts G)))"
    using complete_finite_edges[OF assms(1)] .
  thus "finite_graph (complete (uverts G))"
    unfolding finite_graph_def complete_def using assms(1) by auto
qed

definition subgraphs :: "ugraph ⇒ ugraph set" where
"subgraphs G = {G'. subgraph G' G}"

definition nonempty_subgraphs :: "ugraph ⇒ ugraph set" where
"nonempty_subgraphs G = {G'. uwellformed G' ∧ subgraph G' G ∧ nonempty_graph G'}"

lemma subgraphs_finite:
  assumes "finite_graph G"
  shows "finite (subgraphs G)"
proof -
  have "subgraphs G = {(V', E'). V' ⊆ uverts G ∧ E' ⊆ uedges G}"
    unfolding subgraphs_def subgraph_def by force
  moreover have "finite (uverts G)" "finite (uedges G)"
    using assms unfolding finite_graph_def by auto
  ultimately show ?thesis
    by simp
qed

corollary nonempty_subgraphs_finite: "finite_graph G ⟹ finite (nonempty_subgraphs G)"
using subgraphs_finite
unfolding nonempty_subgraphs_def subgraphs_def
by auto

subsection‹Induced subgraphs›

definition induced_subgraph :: "uvert set ⇒ ugraph ⇒ ugraph" where
"induced_subgraph V G = (V, uedges G ∩ all_edges V)"

lemma induced_is_subgraph:
  "V ⊆ uverts G ⟹ subgraph (induced_subgraph V G) G"
  "V ⊆ uverts G ⟹ subgraph (induced_subgraph V G) (complete V)"
unfolding subgraph_def induced_subgraph_def complete_def
by simp+

lemma induced_wellformed: "uwellformed G ⟹ V ⊆ uverts G ⟹ uwellformed (induced_subgraph V G)"
unfolding uwellformed_def induced_subgraph_def all_edges_def
by force

lemma subgraph_union_induced:
  assumes "uverts H1 ⊆ S" and "uverts H2 ⊆ T"
  assumes "uwellformed H1" and "uwellformed H2"
  shows "subgraph H1 (induced_subgraph S G) ∧ subgraph H2 (induced_subgraph T G) ⟷
         subgraph (uverts H1 ∪ uverts H2, uedges H1 ∪ uedges H2) (induced_subgraph (S ∪ T) G)"
unfolding induced_subgraph_def subgraph_def
apply auto
using all_edges_mono apply blast
using all_edges_mono apply blast
using assms(1,2) wellformed_all_edges[OF assms(3)] wellformed_all_edges[OF assms(4)] all_edges_mono[OF assms(1)] all_edges_mono[OF assms(2)]
apply auto
done

lemma (in edge_space) induced_subgraph_prob:
  assumes "uverts H ⊆ V" and "uwellformed H" and "V ⊆ S_verts"
  shows "prob {es ∈ space P. subgraph H (induced_subgraph V (edge_ugraph es))} = p ^ card (uedges H)" (is "prob ?A = _")
proof -
  have "prob ?A = prob (cylinder S_edges (uedges H) {})"
    unfolding cylinder_def space_eq subgraph_def induced_subgraph_def edge_ugraph_def S_edges_def
    by (rule arg_cong[OF Collect_cong]) (metis (no_types) assms(1,2) Pow_iff all_edges_mono fst_conv inf_absorb1 inf_bot_left le_inf_iff snd_conv wellformed_all_edges)
  also have "… = p ^ card (uedges H)"
    proof (rule cylinder_empty_prob)
      have "uedges H ⊆ all_edges (uverts H)"
        by (rule wellformed_all_edges[OF assms(2)])
      also have "all_edges (uverts H) ⊆ all_edges S_verts"
        using assms by (auto simp: all_edges_mono[OF subset_trans])
      finally show "uedges H ⊆ S_edges"
        unfolding S_edges_def .
    qed
  finally show ?thesis
    .
qed

subsection‹Graph isomorphism›

text‹We define graph isomorphism slightly different than in the literature. The usual definition
is that two graphs are isomorphic iff there exists a bijection between the vertex sets which
preserves the adjacency. However, this complicates many proofs.

Instead, we define the intuitive mapping operation on graphs. An isomorphism between two graphs
arises if there is a suitable mapping function from the first to the second graph. Later, we show
that this operation can be inverted.›

fun map_ugraph :: "(nat ⇒ nat) ⇒ ugraph ⇒ ugraph" where
"map_ugraph f (V, E) = (f ` V, (λe. f ` e) ` E)"

definition isomorphism :: "ugraph ⇒ ugraph ⇒ (nat ⇒ nat) ⇒ bool" where
"isomorphism G1 G2 f ≡ bij_betw f (uverts G1) (uverts G2) ∧ G2 = map_ugraph f G1"

abbreviation isomorphic :: "ugraph ⇒ ugraph ⇒ bool" (‹_ ≃ _›) where
"G1 ≃ G2 ≡ uwellformed G1 ∧ uwellformed G2 ∧ (∃f. isomorphism G1 G2 f)"

lemma map_ugraph_id: "map_ugraph id = id"
unfolding fun_eq_iff
by simp

lemma map_ugraph_trans: "map_ugraph (g ∘ f) = (map_ugraph g) ∘ (map_ugraph f)"
  by (simp add: fun_eq_iff image_image)

lemma map_ugraph_wellformed:
  assumes "uwellformed G" and "inj_on f (uverts G)"
  shows "uwellformed (map_ugraph f G)"
unfolding uwellformed_def
proof safe
  fix e'
  assume "e' ∈ uedges (map_ugraph f G)"
  hence "e' ∈ (λe. f ` e) ` (uedges G)"
    by (metis map_ugraph.simps snd_conv surjective_pairing)
  then obtain e where e: "e' = f ` e" "e ∈ uedges G"
    by blast
  hence "card e = 2" "e ⊆ uverts G"
    using assms(1) unfolding uwellformed_def by blast+
  thus "card e' = 2"
    using e(1) by (simp add: card_inj_subs[OF assms(2)])

  fix u'
  assume "u' ∈ e'"
  hence "u' ∈ f ` e"
    using e by force
  then obtain u where u: "u' = f u" "u ∈ e"
    by blast
  hence "u ∈ uverts G"
    using assms(1) e(2) unfolding uwellformed_def by blast
  hence "u' ∈ f ` uverts G"
    using u(1) by simp
  thus "u' ∈ uverts (map_ugraph f G)"
    by (metis map_ugraph.simps fst_conv surjective_pairing)
qed

lemma map_ugraph_finite: "finite_graph G ⟹ finite_graph (map_ugraph f G)"
unfolding finite_graph_def
by (metis finite_imageI fst_conv map_ugraph.simps snd_conv surjective_pairing)

lemma map_ugraph_preserves_sub:
  assumes "subgraph G1 G2"
  shows "subgraph (map_ugraph f G1) (map_ugraph f G2)"
proof -
  have "f ` uverts G1 ⊆ f ` uverts G2" "(λe. f ` e) ` uedges G1 ⊆ (λe. f ` e) ` uedges G2"
    using assms(1) unfolding subgraph_def by auto
  thus ?thesis
    unfolding subgraph_def by (metis map_ugraph.simps fst_conv snd_conv surjective_pairing)
qed

lemma isomorphic_refl: "uwellformed G ⟹ G ≃ G"
unfolding isomorphism_def
by (metis bij_betw_id id_def map_ugraph_id)

lemma isomorphic_trans:
  assumes "G1 ≃ G2" and "G2 ≃ G3"
  shows "G1 ≃ G3"
proof -
  from assms obtain f1 f2 where
    bij: "bij_betw f1 (uverts G1) (uverts G2)" "bij_betw f2 (uverts G2) (uverts G3)" and
    map: "G2 = map_ugraph f1 G1" "G3 = map_ugraph f2 G2"
    unfolding isomorphism_def by blast

  let ?f = "f2 ∘ f1"
  have "bij_betw ?f (uverts G1) (uverts G3)"
    using bij by (simp add: bij_betw_comp_iff)
  moreover have "G3 = map_ugraph ?f G1"
    using map by (simp add: map_ugraph_trans)
  moreover have "uwellformed G1" "uwellformed G3"
    using assms unfolding isomorphism_def by simp+
  ultimately show "G1 ≃ G3"
    unfolding isomorphism_def by blast
qed

lemma isomorphic_sym:
  assumes "G1 ≃ G2"
  shows "G2 ≃ G1"
proof safe
  from assms obtain f where "isomorphism G1 G2 f"
    by blast
  hence bij: "bij_betw f (uverts G1) (uverts G2)" and map: "G2 = map_ugraph f G1"
    unfolding isomorphism_def by auto

  let ?f' = "inv_into (uverts G1) f"
  have bij': "bij_betw ?f' (uverts G2) (uverts G1)"
    by (rule bij_betw_inv_into) fact
  moreover have "uverts G1 = ?f' ` uverts G2"
    using bij' unfolding bij_betw_def by force
  moreover have "uedges G1 = (λe. ?f' ` e) ` uedges G2"
    proof -
      have "uedges G1 = id ` uedges G1"
        by simp
      also have "… = (λe. ?f' ` (f ` e)) ` uedges G1"
        proof (rule image_cong)
          fix a
          assume "a ∈ uedges G1"
          hence "a ⊆ uverts G1"
            using assms unfolding isomorphism_def uwellformed_def by blast
          thus "id a = inv_into (uverts G1) f ` f ` a"
            by (metis (full_types) id_def bij bij_betw_imp_inj_on inv_into_image_cancel)
        qed simp
      also have "… = (λe. ?f' ` e) ` ((λe. f ` e) ` uedges G1)"
        by (rule image_image[symmetric])
      also have "… = (λe. ?f' ` e) ` uedges G2"
        using bij map by (metis map_ugraph.simps prod.collapse snd_eqD)
      finally show ?thesis
        .
    qed
  ultimately have "isomorphism G2 G1 ?f'"
    unfolding isomorphism_def by (metis map_ugraph.simps split_pairs)
  thus "∃f. isomorphism G2 G1 f"
    by blast
qed (auto simp: assms)

lemma isomorphic_cards:
  assumes "G1 ≃ G2"
  shows
    "card (uverts G1) = card (uverts G2)" (is "?V")
    "card (uedges G1) = card (uedges G2)" (is "?E")
proof -
  from assms obtain f where
    bij: "bij_betw f (uverts G1) (uverts G2)" and
    map: "G2 = map_ugraph f G1"
    unfolding isomorphism_def by blast
  from assms have wellformed: "uwellformed G1" "uwellformed G2"
    by simp+

  show ?V
    by (rule bij_betw_same_card[OF bij])

  let ?g = "λe. f ` e"
  have "bij_betw ?g (Pow (uverts G1)) (Pow (uverts G2))"
    by (rule bij_lift[OF bij])
  moreover have "uedges G1 ⊆ Pow (uverts G1)"
    using wellformed(1) unfolding uwellformed_def by blast
  ultimately have "card (?g ` uedges G1) = card (uedges G1)"
    unfolding bij_betw_def by (metis card_inj_subs)
  thus ?E
    by (metis map map_ugraph.simps snd_conv surjective_pairing)
qed

subsection‹Isomorphic subgraphs›

text‹The somewhat sloppy term `isomorphic subgraph' denotes a subgraph which is isomorphic to a
fixed other graph. For example, saying that a graph contains a triangle usually means that it
contains \emph{any} triangle, not the specific triangle with the nodes $1$, $2$ and $3$. Hence, such
a graph would have a triangle as an isomorphic subgraph.›

definition subgraph_isomorphic :: "ugraph ⇒ ugraph ⇒ bool" (‹_ ⊑ _›) where
"G' ⊑ G ≡ uwellformed G ∧ (∃G''. G' ≃ G'' ∧ subgraph G'' G)"

lemma subgraph_is_subgraph_isomorphic: "⟦ uwellformed G'; uwellformed G; subgraph G' G ⟧ ⟹ G' ⊑ G"
unfolding subgraph_isomorphic_def
by (metis isomorphic_refl)

lemma isomorphic_is_subgraph_isomorphic: "G1 ≃ G2 ⟹ G1 ⊑ G2"
unfolding subgraph_isomorphic_def
by (metis subgraph_refl)

lemma subgraph_isomorphic_refl: "uwellformed G ⟹ G ⊑ G"
unfolding subgraph_isomorphic_def
by (metis isomorphic_refl subgraph_refl)

lemma subgraph_isomorphic_pre_iso_closed:
  assumes "G1 ≃ G2" and "G2 ⊑ G3"
  shows "G1 ⊑ G3"
unfolding subgraph_isomorphic_def
proof
  show "uwellformed G3"
    using assms unfolding subgraph_isomorphic_def by blast
next
  from assms(2) obtain G2' where "G2 ≃ G2'" "subgraph G2' G3"
    unfolding subgraph_isomorphic_def by blast
  moreover with assms(1) have "G1 ≃ G2'"
    by (metis isomorphic_trans)
  ultimately show "∃G''. G1 ≃ G'' ∧ subgraph G'' G3"
    by blast
qed

lemma subgraph_isomorphic_pre_subgraph_closed:
  assumes "uwellformed G1" and "subgraph G1 G2" and "G2 ⊑ G3"
  shows "G1 ⊑ G3"
unfolding subgraph_isomorphic_def
proof
  show "uwellformed G3"
    using assms unfolding subgraph_isomorphic_def by blast
next
  from assms(3) obtain G2' where "G2 ≃ G2'" "subgraph G2' G3"
    unfolding subgraph_isomorphic_def by blast
  then obtain f where bij: "bij_betw f (uverts G2) (uverts G2')" "G2' = map_ugraph f G2"
    unfolding isomorphism_def by blast
  let ?G1' = "map_ugraph f G1"

  have "bij_betw f (uverts G1) (f ` uverts G1)"
    using bij(1) assms(2) unfolding subgraph_def by (auto intro: bij_betw_subset)
  moreover hence "uwellformed ?G1'"
    using map_ugraph_wellformed[OF assms(1)] unfolding bij_betw_def ..
  ultimately have "G1 ≃ ?G1'"
    using assms(1) unfolding isomorphism_def by (metis map_ugraph.simps fst_conv surjective_pairing)
  moreover have "subgraph ?G1' G3" (* Yes, I will TOTALLY understand that step tomorrow. *)
    using subgraph_trans[OF map_ugraph_preserves_sub[OF assms(2)]] bij(2) ‹subgraph G2' G3› by simp
  ultimately show "∃G''. G1 ≃ G'' ∧ subgraph G'' G3"
    by blast
qed

lemmas subgraph_isomorphic_pre_closed = subgraph_isomorphic_pre_subgraph_closed subgraph_isomorphic_pre_iso_closed

lemma subgraph_isomorphic_trans[trans]:
  assumes "G1 ⊑ G2" and "G2 ⊑ G3"
  shows "G1 ⊑ G3"
proof -
  from assms(1) obtain G where "G1 ≃ G" "subgraph G G2"
    unfolding subgraph_isomorphic_def by blast
  thus ?thesis
    using assms(2) by (metis subgraph_isomorphic_pre_closed)
qed

lemma subgraph_isomorphic_post_iso_closed: "⟦ H ⊑ G; G ≃ G' ⟧ ⟹ H ⊑ G'"
using isomorphic_is_subgraph_isomorphic subgraph_isomorphic_trans
by blast

lemmas subgraph_isomorphic_post_closed = subgraph_isomorphic_post_iso_closed

lemmas subgraph_isomorphic_closed = subgraph_isomorphic_pre_closed subgraph_isomorphic_post_closed

subsection‹Density›

text‹The density of a graph is the quotient of the number of edges and the number of vertices of
a graph.›

definition density :: "ugraph ⇒ real" where
"density G = card (uedges G) / card (uverts G)"

text‹The maximum density of a graph is the density of its densest nonempty subgraph.›

definition max_density :: "ugraph ⇒ real" where
"max_density G = Lattices_Big.Max (density ` nonempty_subgraphs G)"

text‹We prove some obvious results about the maximum density, such as that there is a subgraph
which has the maximum density and that the (maximum) density is preserved by isomorphisms. The
proofs are a bit complicated by the fact that most facts about @{term Lattices_Big.Max} require
non-emptiness of the target set, but we need that anyway to get a value out of it.›

lemma subgraph_has_max_density:
  assumes "finite_graph G" and "nonempty_graph G" and "uwellformed G"
  shows "∃G'. density G' = max_density G ∧ subgraph G' G ∧ nonempty_graph G' ∧ finite_graph G' ∧ uwellformed G'"
proof -
  have "G ∈ nonempty_subgraphs G"
    unfolding nonempty_subgraphs_def using subgraph_refl assms by simp
  hence "density G ∈ density ` nonempty_subgraphs G"
    by simp
  hence "(density ` nonempty_subgraphs G) ≠ {}"
    by fast
  hence "max_density G ∈ (density ` nonempty_subgraphs G)"
    unfolding max_density_def by (auto simp add: nonempty_subgraphs_finite[OF assms(1)] Max.closed)
  thus ?thesis
    unfolding nonempty_subgraphs_def using subgraph_finite[OF assms(1)] by force
qed

lemma max_density_is_max:
  assumes "finite_graph G" and "finite_graph G'" and "nonempty_graph G'" and "uwellformed G'" and "subgraph G' G"
  shows "density G' ≤ max_density G"
unfolding max_density_def
proof (rule Max_ge)
  show "finite (density ` nonempty_subgraphs G)"
    using assms(1) by (simp add: nonempty_subgraphs_finite)
next
  show "density G' ∈ density ` nonempty_subgraphs G"
    unfolding nonempty_subgraphs_def using assms by blast
qed

lemma max_density_gr_zero:
  assumes "finite_graph G" and "nonempty_graph G" and "uwellformed G"
  shows "0 < max_density G"
proof -
  have "0 < card (uverts G)" "0 < card (uedges G)"
    using assms unfolding finite_graph_def nonempty_graph_def by auto
  hence "0 < density G"
    unfolding density_def by simp
  also have "density G ≤ max_density G"
    using assms by (simp add: max_density_is_max subgraph_refl)
  finally show ?thesis
    .
qed

lemma isomorphic_density:
  assumes "G1 ≃ G2"
  shows "density G1 = density G2"
unfolding density_def
using isomorphic_cards[OF assms]
by simp

lemma isomorphic_max_density:
  assumes "G1 ≃ G2" and "nonempty_graph G1" and "nonempty_graph G2" and "finite_graph G1" and "finite_graph G2"
  shows "max_density G1 = max_density G2"
proof -
  ― ‹The proof strategy is not completely straightforward. We first show that if two graphs are
       isomorphic, the maximum density of one graph is less or equal than the maximum density of
       the other graph. The reason is that this proof is quite long and the desired result directly
       follows from the symmetry of the isomorphism relation.\footnote{Some famous mathematician
       once said that if you prove that $a \le b$ and $b \le a$, you know \emph{that} these
       numbers are equal, but not \emph{why}. Since many proofs in this work are mostly opaque to
       me, I can live with that.}›
  {
    fix A B
    assume A: "nonempty_graph A" "finite_graph A"
    assume iso: "A ≃ B"

    then obtain f where f: "B = map_ugraph f A" "bij_betw f (uverts A) (uverts B)"
      unfolding isomorphism_def by blast
    have wellformed: "uwellformed A"
      using iso unfolding isomorphism_def by simp
    ― ‹We observe that the set of densities of the subgraphs does not change if we map the
         subgraphs first.›
    have "density ` nonempty_subgraphs A = density ` (map_ugraph f ` nonempty_subgraphs A)"
      proof (rule image_comp_cong)
        fix G
        assume "G ∈ nonempty_subgraphs A"
        hence "uverts G ⊆ uverts A" "uwellformed G"
          unfolding nonempty_subgraphs_def subgraph_def by simp+
        hence "inj_on f (uverts G)"
          using f(2) unfolding bij_betw_def by (metis subset_inj_on)
        hence "G ≃ map_ugraph f G"
          unfolding isomorphism_def bij_betw_def
          by (metis map_ugraph.simps fst_conv surjective_pairing map_ugraph_wellformed ‹uwellformed G›)
        thus "density G = density (map_ugraph f G)"
          by (fact isomorphic_density)
      qed
    ― ‹Additionally, we show that the operations @{term nonempty_subgraphs} and @{term map_ugraph}
         can be swapped without changing the densities. This is an obvious result, because
         @{term map_ugraph} does not change the structure of a graph. Still, the proof is a bit
         hairy, which is why we only show inclusion in one direction and use symmetry of isomorphism
         later.›
    also have "… ⊆ density ` nonempty_subgraphs (map_ugraph f A)"
      proof (rule image_mono, rule subsetI)
        fix G''
        assume "G'' ∈ map_ugraph f ` nonempty_subgraphs A"
        then obtain G' where G_subst: "G'' = map_ugraph f G'" "G' ∈ nonempty_subgraphs A"
          by blast
        hence G': "subgraph G' A" "nonempty_graph G'" "uwellformed G'"
          unfolding nonempty_subgraphs_def by auto
        hence "inj_on f (uverts G')"
          using f unfolding bij_betw_def subgraph_def by (metis subset_inj_on)
        hence "uwellformed G''"
          using map_ugraph_wellformed G' G_subst by simp
        moreover have "nonempty_graph G''"
          using G' G_subst unfolding nonempty_graph_def by (metis map_ugraph.simps fst_conv snd_conv surjective_pairing empty_is_image)
        moreover have "subgraph G'' (map_ugraph f A)"
          using map_ugraph_preserves_sub G' G_subst by simp
        ultimately show "G'' ∈ nonempty_subgraphs (map_ugraph f A)"
          unfolding nonempty_subgraphs_def by simp
      qed
    finally have "density ` nonempty_subgraphs A ⊆ density ` nonempty_subgraphs (map_ugraph f A)"
      .
    hence "max_density A ≤ max_density (map_ugraph f A)"
      unfolding max_density_def
      proof (rule Max_mono)
        have "A ∈ nonempty_subgraphs A"
          using A iso unfolding nonempty_subgraphs_def by (simp add: subgraph_refl)
        thus "density ` nonempty_subgraphs A ≠ {}"
          by blast
      next
        have "finite (nonempty_subgraphs (map_ugraph f A))"
          by (rule nonempty_subgraphs_finite[OF map_ugraph_finite[OF A(2)]])
        thus "finite (density ` nonempty_subgraphs (map_ugraph f A))"
          by blast
      qed
    hence "max_density A ≤ max_density B"
      by (subst f)
  }
  then show ?thesis
    by (meson assms isomorphic_sym order_antisym_conv)
qed

subsection‹Fixed selectors›

text‹\label{sec:selector}
In the proof of the main theorem in the lecture notes, the concept of a ``fixed copy'' of a graph is
fundamental.

Let $H$ be a fixed graph. A `fixed selector' is basically a function mapping a set with the same
size as the vertex set of $H$ to a new graph which is isomorphic to $H$ and its vertex set is the
same as the input set.\footnote{We call such a selector \emph{fixed} because its result is
deterministic.}›

definition "is_fixed_selector H f = (∀V. finite V ∧ card (uverts H) = card V ⟶ H ≃ f V ∧ uverts (f V) = V)"

text‹Obviously, there may be many possible fixed selectors for a given graph. First, we show
that there is always at least one. This is sufficient, because we can always obtain that one and
use its properties without knowing exactly which one we chose.›

lemma ex_fixed_selector:
  assumes "uwellformed H" and "finite_graph H"
  obtains f where "is_fixed_selector H f"
proof
  ― ‹I guess this is the only place in the whole work where we make use of a nifty little HOL
       feature called \emph{SOME}, which is basically Hilbert's choice operator. The reason is that
       any bijection between the the vertex set of @{term H} and the input set gives rise to a
       fixed selector function. In the lecture notes, a specific bijection was defined, but this
       is shorter and more elegant.›
  let ?bij = "λV. SOME g. bij_betw g (uverts H) V"
  let ?f = "λV. map_ugraph (?bij V) H"
  {
    fix V :: "uvert set"
    assume "finite V" "card (uverts H) = card V"
    moreover have "finite (uverts H)"
      using assms unfolding finite_graph_def by simp
    ultimately have "bij_betw (?bij V) (uverts H) V"
      by (metis finite_same_card_bij someI_ex)
    moreover hence *: "uverts (?f V) = V ∧ uwellformed (?f V)"
      using map_ugraph_wellformed[OF assms(1)]
      by (metis bij_betw_def map_ugraph.simps fst_conv surjective_pairing)
    ultimately have **: "H ≃ ?f V"
      unfolding isomorphism_def using assms(1) by auto
    note * **
  }
  thus "is_fixed_selector H ?f"
    unfolding is_fixed_selector_def by blast
qed

lemma fixed_selector_induced_subgraph:
  assumes "is_fixed_selector H f" and "card (uverts H) = card V" and "finite V"
  assumes sub: "subgraph (f V) (induced_subgraph V G)" and V: "V ⊆ uverts G" and G: "uwellformed G"
  shows "H ⊑ G"
  by (meson G V assms induced_is_subgraph(1) is_fixed_selector_def sub subgraph_isomorphic_def subgraph_trans)

end