Theory Designs_And_Graphs
section ‹Graphs and Designs›
text ‹There are many links between graphs and design - most fundamentally that graphs are designs›
theory Designs_And_Graphs imports Block_Designs Graph_Theory.Digraph Graph_Theory.Digraph_Component
begin
subsection ‹Non-empty digraphs›
text ‹First, we define the concept of a non-empty digraph. This mirrors the idea of a "proper design"
in the design theory library›
locale non_empty_digraph = wf_digraph +
assumes arcs_not_empty: "arcs G ≠ {}"
begin
lemma verts_not_empty: "verts G ≠ {}"
using wf arcs_not_empty head_in_verts by fastforce
end
subsection ‹Arcs to Blocks›
text ‹A digraph uses a pair of points to define an ordered edge. In the case of simple graphs,
both possible orderings will be in the arcs set. Blocks are inherently unordered, and as such
a method is required to convert between the two representations›
context graph
begin
definition arc_to_block :: "'b ⇒ 'a set" where
"arc_to_block e ≡ {tail G e, head G e}"
lemma arc_to_block_to_ends: "{fst (arc_to_ends G e), snd (arc_to_ends G e)} = arc_to_block e"
by (simp add: arc_to_ends_def arc_to_block_def)
lemma arc_to_block_to_ends_swap: "{snd (arc_to_ends G e), fst (arc_to_ends G e)} = arc_to_block e"
using arc_to_block_to_ends
by (simp add: arc_to_block_to_ends insert_commute)
lemma arc_to_ends_to_block: "arc_to_block e = {x, y} ⟹
arc_to_ends G e = (x, y) ∨ arc_to_ends G e = (y, x)"
by (metis arc_to_block_def arc_to_ends_def doubleton_eq_iff)
lemma arc_to_block_sym: "arc_to_ends G e1 = (u, v) ⟹ arc_to_ends G e2 = (v, u) ⟹
arc_to_block e1 = arc_to_block e2"
by (simp add: arc_to_block_def arc_to_ends_def insert_commute)
definition arcs_blocks :: "'a set multiset" where
"arcs_blocks ≡ mset_set (arc_to_block ` (arcs G))"
lemma arcs_blocks_ends: "(x, y) ∈ arcs_ends G ⟹ {x, y} ∈# arcs_blocks"
proof (auto simp add: arcs_ends_def arcs_blocks_def )
fix xa
assume assm1: "(x, y) = arc_to_ends G xa" and assm2: "xa ∈ arcs G"
obtain z where zin: "z ∈ (arc_to_block ` (arcs G))" and "z = arc_to_block xa"
using assm2 by blast
thus "{x, y} ∈ arc_to_block ` (arcs G)" using assm1 arc_to_block_to_ends
by (metis fst_conv snd_conv)
qed
lemma arc_ends_blocks_subset: "E ⊆ arcs G ⟹ (x, y) ∈ ((arc_to_ends G) ` E) ⟹
{x, y} ∈ (arc_to_block ` E)"
by (auto simp add: arc_to_ends_def arc_to_block_def )
lemma arc_blocks_end_subset: assumes "E ⊆ arcs G" and "{x, y} ∈ (arc_to_block ` E)"
shows "(x, y) ∈ ((arc_to_ends G) ` E) ∨ (y, x) ∈ ((arc_to_ends G) ` E)"
proof -
obtain e where "e ∈ E" and "arc_to_block e = {x,y}" using assms
by fastforce
then have "arc_to_ends G e = (x, y) ∨ arc_to_ends G e = (y, x)"
using arc_to_ends_to_block by simp
thus ?thesis
by (metis ‹e ∈ E› image_iff)
qed
lemma arcs_ends_blocks: "{x, y} ∈# arcs_blocks ⟹ (x, y) ∈ arcs_ends G ∧ (y, x) ∈ arcs_ends G"
proof (auto simp add: arcs_ends_def arcs_blocks_def )
fix xa
assume assm1: "{x, y} = arc_to_block xa" and assm2: "xa ∈ (arcs G)"
obtain z where zin: "z ∈ (arc_to_ends G ` (arcs G))" and "z = arc_to_ends G xa"
using assm2 by blast
then have "z = (x, y) ∨ z = (y, x)" using arc_to_block_to_ends assm1
by (metis arc_to_ends_def doubleton_eq_iff fst_conv snd_conv)
thus "(x, y) ∈ arc_to_ends G ` (arcs G)" using assm2
by (metis arcs_ends_def arcs_ends_symmetric sym_arcs zin)
next
fix xa
assume assm1: "{x, y} = arc_to_block xa" and assm2: "xa ∈ (arcs G)"
thus "(y, x) ∈ arc_to_ends G ` arcs G" using arcs_ends_def
by (metis dual_order.refl graph.arc_blocks_end_subset graph_axioms graph_symmetric imageI)
qed
lemma arcs_blocks_iff: "{x, y} ∈# arcs_blocks ⟷ (x, y) ∈ arcs_ends G ∧ (y, x) ∈ arcs_ends G"
using arcs_ends_blocks arcs_blocks_ends by blast
lemma arcs_ends_wf: "(x, y) ∈ arcs_ends G ⟹ x ∈ verts G ∧ y ∈ verts G"
by auto
lemma arcs_blocks_elem: "bl ∈# arcs_blocks ⟹ ∃ x y . bl = {x, y}"
apply (auto simp add: arcs_blocks_def)
by (meson arc_to_block_def)
lemma arcs_ends_blocks_wf:
assumes "bl ∈# arcs_blocks"
shows "bl ⊆ verts G"
proof -
obtain x y where blpair: "bl = {x, y}" using arcs_blocks_elem assms
by fastforce
then have "(x, y) ∈ arcs_ends G" using arcs_ends_blocks assms by simp
thus ?thesis using arcs_ends_wf blpair by auto
qed
lemma arcs_blocks_simple: "bl ∈# arcs_blocks ⟹ count (arcs_blocks) bl = 1"
by (simp add: arcs_blocks_def)
lemma arcs_blocks_ne: "arcs G ≠ {} ⟹ arcs_blocks ≠ {#}"
by (simp add: arcs_blocks_iff arcs_blocks_def mset_set_empty_iff)
end
subsection ‹Graphs are designs›
text ‹Prove that a graph is a number of different types of designs›
sublocale graph ⊆ design "verts G" "arcs_blocks"
using arcs_ends_blocks_wf arcs_blocks_elem by (unfold_locales) (auto)
sublocale graph ⊆ simple_design "verts G" "arcs_blocks"
using arcs_ends_blocks_wf arcs_blocks_elem arcs_blocks_simple by (unfold_locales) (auto)
locale non_empty_graph = graph + non_empty_digraph
sublocale non_empty_graph ⊆ proper_design "verts G" "arcs_blocks"
using arcs_blocks_ne arcs_not_empty by (unfold_locales) simp
lemma (in graph) graph_block_size: assumes "bl ∈# arcs_blocks" shows "card bl = 2"
proof -
obtain x y where blrep: "bl = {x, y}" using assms arcs_blocks_elem
by fastforce
then have "(x, y) ∈ arcs_ends G" using arcs_ends_blocks assms by simp
then have "x ≠ y" using no_loops using adj_not_same by blast
thus ?thesis using blrep by simp
qed
sublocale non_empty_graph ⊆ block_design "verts G" "arcs_blocks" 2
using arcs_not_empty graph_block_size arcs_blocks_ne by (unfold_locales) simp_all
subsection ‹R-regular graphs›
text ‹To reason on r-regular graphs and their link to designs, we require a number of extensions to
lemmas reasoning around the degrees of vertices›
context sym_digraph
begin
lemma in_out_arcs_reflexive: "v ∈ verts G ⟹ (e ∈ (in_arcs G v) ⟹
∃ e' . (e' ∈ (out_arcs G v) ∧ head G e' = tail G e))"
using symmetric_conv sym_arcs by fastforce
lemma out_in_arcs_reflexive: "v ∈ verts G ⟹ (e ∈ (out_arcs G v) ⟹
∃ e' . (e' ∈ (in_arcs G v) ∧ tail G e' = head G e))"
using symmetric_conv sym_arcs by fastforce
end
context nomulti_digraph
begin
lemma in_arcs_single_per_vert:
assumes "v ∈ verts G" and "u ∈ verts G"
assumes "e1 ∈ in_arcs G v" and " e2 ∈ in_arcs G v"
assumes "tail G e1 = u" and "tail G e2 = u"
shows "e1 = e2"
proof -
have in_arcs1: "e1 ∈ arcs G" and in_arcs2: "e2 ∈ arcs G" using assms by auto
have "arc_to_ends G e1 = arc_to_ends G e2" using assms arc_to_ends_def
by (metis in_in_arcs_conv)
thus ?thesis using in_arcs1 in_arcs2 no_multi_arcs by simp
qed
lemma out_arcs_single_per_vert:
assumes "v ∈ verts G" and "u ∈ verts G"
assumes "e1 ∈ out_arcs G v" and " e2 ∈ out_arcs G v"
assumes "head G e1 = u" and "head G e2 = u"
shows "e1 = e2"
proof -
have in_arcs1: "e1 ∈ arcs G" and in_arcs2: "e2 ∈ arcs G" using assms by auto
have "arc_to_ends G e1 = arc_to_ends G e2" using assms arc_to_ends_def
by (metis in_out_arcs_conv)
thus ?thesis using in_arcs1 in_arcs2 no_multi_arcs by simp
qed
end
text ‹Some helpers on the transformation arc definition›
context graph
begin
lemma arc_to_block_is_inj_in_arcs: "inj_on arc_to_block (in_arcs G v)"
apply (auto simp add: arc_to_block_def inj_on_def)
by (metis arc_to_ends_def doubleton_eq_iff no_multi_arcs)
lemma arc_to_block_is_inj_out_arcs: "inj_on arc_to_block (out_arcs G v)"
apply (auto simp add: arc_to_block_def inj_on_def)
by (metis arc_to_ends_def doubleton_eq_iff no_multi_arcs)
lemma in_out_arcs_reflexive_uniq: "v ∈ verts G ⟹ (e ∈ (in_arcs G v) ⟹
∃! e' . (e' ∈ (out_arcs G v) ∧ head G e' = tail G e))"
apply auto
using symmetric_conv apply fastforce
using out_arcs_single_per_vert by (metis head_in_verts in_out_arcs_conv)
lemma out_in_arcs_reflexive_uniq: "v ∈ verts G ⟹ e ∈ (out_arcs G v) ⟹
∃! e' . (e' ∈ (in_arcs G v) ∧ tail G e' = head G e)"
apply auto
using symmetric_conv apply fastforce
using in_arcs_single_per_vert by (metis tail_in_verts in_in_arcs_conv)
lemma in_eq_out_arc_ends: "(u, v) ∈ ((arc_to_ends G) ` (in_arcs G v)) ⟷
(v, u) ∈ ((arc_to_ends G) ` (out_arcs G v))"
using arc_to_ends_def in_in_arcs_conv in_out_arcs_conv
by (smt (z3) Pair_inject adj_in_verts(1) dominatesI image_iff out_in_arcs_reflexive_uniq)
lemma in_degree_eq_card_arc_ends: "in_degree G v = card ((arc_to_ends G) ` (in_arcs G v))"
apply (simp add: in_degree_def)
using no_multi_arcs by (metis card_image in_arcs_in_arcs inj_onI)
lemma in_degree_eq_card_arc_blocks: "in_degree G v = card (arc_to_block ` (in_arcs G v))"
apply (simp add: in_degree_def)
using no_multi_arcs arc_to_block_is_inj_in_arcs by (simp add: card_image)
lemma out_degree_eq_card_arc_blocks: "out_degree G v = card (arc_to_block ` (out_arcs G v))"
apply (simp add: out_degree_def)
using no_multi_arcs arc_to_block_is_inj_out_arcs by (simp add: card_image)
lemma out_degree_eq_card_arc_ends: "out_degree G v = card ((arc_to_ends G) ` (out_arcs G v))"
apply (simp add: out_degree_def)
using no_multi_arcs by (metis card_image out_arcs_in_arcs inj_onI)
lemma bij_betw_in_out_arcs: "bij_betw (λ (u, v) . (v, u)) ((arc_to_ends G) ` (in_arcs G v))
((arc_to_ends G) ` (out_arcs G v))"
apply (auto simp add: bij_betw_def)
apply (simp add: swap_inj_on)
apply (metis Pair_inject arc_to_ends_def image_eqI in_eq_out_arc_ends in_in_arcs_conv)
by (metis arc_to_ends_def imageI in_eq_out_arc_ends in_out_arcs_conv pair_imageI)
lemma in_eq_out_degree: "in_degree G v = out_degree G v"
using bij_betw_in_out_arcs bij_betw_same_card in_degree_eq_card_arc_ends
out_degree_eq_card_arc_ends by auto
lemma in_out_arcs_blocks: "arc_to_block ` (in_arcs G v) = arc_to_block ` (out_arcs G v)"
proof (auto)
fix xa
assume a1: "xa ∈ arcs G" and a2: "v = head G xa"
then have "xa ∈ in_arcs G v" by simp
then obtain e where out: "e ∈ out_arcs G v" and "head G e = tail G xa"
using out_in_arcs_reflexive_uniq by force
then have "arc_to_ends G e = (v, tail G xa)"
by (simp add: arc_to_ends_def)
then have "arc_to_block xa = arc_to_block e"
using arc_to_block_sym by (metis a2 arc_to_ends_def)
then show "arc_to_block xa ∈ arc_to_block ` out_arcs G (head G xa)"
using out a2 by blast
next
fix xa
assume a1: "xa ∈ arcs G" and a2: "v = tail G xa"
then have "xa ∈ out_arcs G v" by simp
then obtain e where ina: "e ∈ in_arcs G v" and "tail G e = head G xa"
using out_in_arcs_reflexive_uniq by force
then have "arc_to_ends G e = (head G xa, v)"
by (simp add: arc_to_ends_def)
then have "arc_to_block xa = arc_to_block e"
using arc_to_block_sym by (metis a2 arc_to_ends_def)
then show "arc_to_block xa ∈ arc_to_block ` in_arcs G (tail G xa)"
using ina a2 by blast
qed
end
text ‹A regular digraph is defined as one where the in degree equals the out degree which in turn
equals some fixed integer $\mathrm{r}$›
locale regular_digraph = wf_digraph +
fixes 𝗋 :: nat
assumes in_deg_r: "v ∈ verts G ⟹ in_degree G v = 𝗋"
assumes out_deg_r: "v ∈ verts G ⟹ out_degree G v = 𝗋"
locale regular_graph = graph + regular_digraph
begin
lemma rep_vertices_in_blocks [simp]:
assumes "x ∈ verts G"
shows "size {# e ∈# arcs_blocks . x ∈ e #} = 𝗋"
proof -
have "⋀ e . e ∈ (arc_to_block ` (arcs G)) ⟹ x ∈ e ⟹ e ∈ (arc_to_block ` in_arcs G x)"
using arc_to_block_def in_in_arcs_conv insert_commute insert_iff singleton_iff sym_arcs
symmetric_conv by fastforce
then have "{ e ∈ (arc_to_block ` (arcs G)) . x ∈ e} = (arc_to_block ` (in_arcs G x))"
using arc_to_block_def by auto
then have "card { e ∈ (arc_to_block ` (arcs G)) . x ∈ e} = 𝗋"
using in_deg_r in_degree_eq_card_arc_blocks assms by auto
thus ?thesis
using arcs_blocks_def finite_arcs by force
qed
end
text ‹Intro rules for regular graphs›
lemma graph_in_degree_r_imp_reg[intro]: assumes "graph G"
assumes "(⋀ v . v ∈ (verts G) ⟹ in_degree G v = 𝗋)"
shows "regular_graph G 𝗋"
proof -
interpret g: graph G using assms by simp
interpret wf: wf_digraph G by (simp add: g.wf_digraph_axioms)
show ?thesis
using assms(2) g.in_eq_out_degree by (unfold_locales) simp_all
qed
lemma graph_out_degree_r_imp_reg[intro]: assumes "graph G"
assumes "(⋀ v . v ∈ (verts G) ⟹ out_degree G v = 𝗋)"
shows "regular_graph G 𝗋"
proof -
interpret g: graph G using assms by simp
interpret wf: wf_digraph G by (simp add: g.wf_digraph_axioms)
show ?thesis
using assms(2) g.in_eq_out_degree by (unfold_locales) simp_all
qed
text ‹Regular graphs (non-empty) can be shown to be a constant rep design›
locale non_empty_regular_graph = regular_graph + non_empty_digraph
sublocale non_empty_regular_graph ⊆ non_empty_graph
by unfold_locales
sublocale non_empty_regular_graph ⊆ constant_rep_design "verts G" "arcs_blocks" 𝗋
using arcs_blocks_ne arcs_not_empty
by (unfold_locales)(simp_all add: point_replication_number_def)
end