Theory Book
section ‹The book algorithm›
theory Book imports
Neighbours
"HOL-Library.Disjoint_Sets" "HOL-Decision_Procs.Approximation"
"HOL-Real_Asymp.Real_Asymp"
begin
hide_const Bseq
subsection ‹Locale for the parameters of the construction›
text ‹The epsilon of the paper, outside the locale›
definition eps :: "nat ⇒ real"
where "eps ≡ λk. real k powr (-1/4)"
lemma eps_eq_sqrt: "eps k = 1 / sqrt (sqrt (real k))"
by (simp add: eps_def powr_minus_divide powr_powr flip: powr_half_sqrt)
lemma eps_ge0: "eps k ≥ 0"
by (simp add: eps_def)
lemma eps_gt0: "k>0 ⟹ eps k > 0"
by (simp add: eps_def)
lemma eps_le1:
assumes "k>0" shows "eps k ≤ 1"
proof -
have "eps 1 = 1"
by (simp add: eps_def)
moreover have "eps n ≤ eps m" if "0<m" "m ≤ n" for m n
using that by (simp add: eps_def powr_minus powr_mono2 divide_simps)
ultimately show ?thesis
using assms by (metis less_one nat_neq_iff not_le)
qed
lemma eps_less1:
assumes "k>1" shows "eps k < 1"
by (smt (verit) assms eps_def less_imp_of_nat_less of_nat_1 powr_less_one zero_le_divide_iff)
definition qfun_base :: "[nat, nat] ⇒ real"
where "qfun_base ≡ λk h. ((1 + eps k)^h - 1) / k"
definition "hgt_maximum ≡ λk. 2 * ln (real k) / eps k"
text ‹The first of many "bigness assumptions"›
definition "Big_height_upper_bound ≡ λk. qfun_base k (nat ⌊hgt_maximum k⌋) > 1"
lemma Big_height_upper_bound:
shows "∀⇧∞k. Big_height_upper_bound k"
unfolding Big_height_upper_bound_def hgt_maximum_def eps_def qfun_base_def
by real_asymp
type_synonym 'a config = "'a set × 'a set × 'a set × 'a set"
locale P0_min =
fixes p0_min :: real
assumes p0_min: "0 < p0_min" "p0_min < 1"
locale Book_Basis = fin_sgraph + P0_min +
assumes complete: "E = all_edges V"
assumes infinite_UNIV: "infinite (UNIV::'a set)"
begin
abbreviation "nV ≡ card V"
lemma graph_size: "graph_size = (nV choose 2)"
using card_all_edges complete finV by blast
lemma in_E_iff [iff]: "{v,w} ∈ E ⟷ v∈V ∧ w∈V ∧ v≠w"
by (auto simp: complete all_edges_alt doubleton_eq_iff)
lemma all_edges_betw_un_iff_clique: "K ⊆ V ⟹ all_edges_betw_un K K ⊆ F ⟷ clique K F"
unfolding clique_def all_edges_betw_un_def doubleton_eq_iff subset_iff
by blast
lemma clique_Un:
assumes "clique A F" "clique B F" "all_edges_betw_un A B ⊆ F" "A ⊆ V" "B ⊆ V"
shows "clique (A ∪ B) F"
using assms by (simp add: all_uedges_betw_I clique_Un subset_iff)
lemma clique_insert:
assumes "clique A F" "all_edges_betw_un {x} A ⊆ F" "A ⊆ V" "x ∈ V"
shows "clique (insert x A) F"
using assms
by (metis Un_subset_iff clique_def insert_is_Un insert_subset clique_Un singletonD)
lemma less_RN_Red_Blue:
fixes l k
assumes nV: "nV < RN k l"
obtains Red Blue :: "'a set set"
where "Red ⊆ E" "Blue = E∖Red" "¬ (∃K. size_clique k K Red)" "¬ (∃K. size_clique l K Blue)"
proof -
have "¬ is_Ramsey_number k l nV"
using RN_le assms leD by blast
then obtain f where f: "f ∈ nsets {..<nV} 2 → {..<2}"
and noclique: "⋀i. i<2 ⟹ ¬ monochromatic {..<nV} ([k,l] ! i) 2 f i"
by (auto simp: partn_lst_def eval_nat_numeral)
obtain φ where φ: "bij_betw φ {..<nV} V"
using bij_betw_from_nat_into_finite finV by blast
define θ where "θ ≡ inv_into {..<nV} φ"
have θ: "bij_betw θ V {..<nV}"
using φ θ_def bij_betw_inv_into by blast
have emap: "bij_betw (λe. φ`e) (nsets {..<nV} 2) E"
by (metis φ bij_betw_nsets complete nsets2_eq_all_edges)
define Red where "Red ≡ (λe. φ`e) ` ((f -` {0}) ∩ nsets {..<nV} 2)"
define Blue where "Blue ≡ (λe. φ`e) ` ((f -` {1}) ∩ nsets {..<nV} 2)"
have "Red ⊆ E"
using bij_betw_imp_surj_on[OF emap] by (auto simp: Red_def)
have "Blue = E-Red"
using emap f
by (auto simp: Red_def Blue_def bij_betw_def inj_on_eq_iff image_iff Pi_iff)
have no_Red_K: False if "size_clique k K Red" for K
proof -
have KR: "clique K Red" and Kk: "card K = k" and "K⊆V"
using that by (auto simp: size_clique_def)
have "f {θ v, θ w} = 0"
if eq: "θ v ≠ θ w" and "v ∈ K" "w ∈ K" for v w
proof -
have "∃e∈f -` {0} ∩ [{..<nV}]⇗2⇖. {v, w} = φ ` e"
using that KR by (fastforce simp: clique_def Red_def)
then show ?thesis
using bij_betw_inv_into_left [OF φ]
by (auto simp: θ_def doubleton_eq_iff insert_commute elim!: nsets2_E)
qed
then have "f ` [θ`K]⇗2⇖ ⊆ {0}" by (auto elim!: nsets2_E)
moreover have "θ`K ∈ [{..<nV}]⇗card K⇖"
by (smt (verit) ‹K⊆V› θ bij_betwE bij_betw_nsets finV mem_Collect_eq nsets_def finite_subset)
ultimately show False
using noclique [of 0] Kk
by (simp add: size_clique_def monochromatic_def)
qed
have no_Blue_K: False if "size_clique l K Blue" for K
proof -
have KB: "clique K Blue" and Kl: "card K = l" and "K⊆V"
using that by (auto simp: size_clique_def)
have "f {θ v, θ w} = 1"
if eq: "θ v ≠ θ w" and "v ∈ K" "w ∈ K" for v w
proof -
have "∃e∈f -` {1} ∩ [{..<nV}]⇗2⇖. {v, w} = φ ` e"
using that KB by (fastforce simp: clique_def Blue_def)
then show ?thesis
using bij_betw_inv_into_left [OF φ]
by (auto simp: θ_def doubleton_eq_iff insert_commute elim!: nsets2_E)
qed
then have "f ` [θ`K]⇗2⇖ ⊆ {1}" by (auto elim!: nsets2_E)
moreover have "θ`K ∈ [{..<nV}]⇗card K⇖"
by (smt (verit) ‹K⊆V› θ bij_betwE bij_betw_nsets finV mem_Collect_eq nsets_def finite_subset)
ultimately show False
using noclique [of 1] Kl
by (simp add: size_clique_def monochromatic_def)
qed
show thesis
using ‹Blue = E ∖ Red› ‹Red ⊆ E› no_Blue_K no_Red_K that by presburger
qed
end
locale No_Cliques = Book_Basis + P0_min +
fixes Red Blue :: "'a set set"
assumes Red_E: "Red ⊆ E"
assumes Blue_def: "Blue = E-Red"
fixes l::nat
fixes k::nat
assumes l_le_k: "l ≤ k"
assumes no_Red_clique: "¬ (∃K. size_clique k K Red)"
assumes no_Blue_clique: "¬ (∃K. size_clique l K Blue)"
locale Book = Book_Basis + No_Cliques +
fixes μ::real
assumes μ01: "0 < μ" "μ < 1"
fixes X0 :: "'a set" and Y0 :: "'a set"
assumes XY0: "disjnt X0 Y0" "X0 ⊆ V" "Y0 ⊆ V"
assumes density_ge_p0_min: "gen_density Red X0 Y0 ≥ p0_min"
locale Book' = Book_Basis + No_Cliques +
fixes γ::real
assumes γ_def: "γ = real l / (real k + real l)"
fixes X0 :: "'a set" and Y0 :: "'a set"
assumes XY0: "disjnt X0 Y0" "X0 ⊆ V" "Y0 ⊆ V"
assumes density_ge_p0_min: "gen_density Red X0 Y0 ≥ p0_min"
context No_Cliques
begin
lemma ln0: "l>0"
using no_Blue_clique by (force simp: size_clique_def clique_def)
lemma kn0: "k > 0"
using l_le_k ln0 by auto
lemma Blue_E: "Blue ⊆ E"
by (simp add: Blue_def)
lemma disjnt_Red_Blue: "disjnt Red Blue"
by (simp add: Blue_def disjnt_def)
lemma Red_Blue_all: "Red ∪ Blue = all_edges V"
using Blue_def Red_E complete by blast
lemma Blue_eq: "Blue = all_edges V - Red"
using Blue_def complete by auto
lemma Red_eq: "Red = all_edges V - Blue"
using Blue_eq Red_Blue_all by blast
lemma disjnt_Red_Blue_Neighbours: "disjnt (Neighbours Red x ∩ X) (Neighbours Blue x ∩ X')"
using disjnt_Red_Blue by (auto simp: disjnt_def Neighbours_def)
lemma indep_Red_iff_clique_Blue: "K ⊆ V ⟹ indep K Red ⟷ clique K Blue"
using Blue_eq by auto
lemma Red_Blue_RN:
fixes X :: "'a set"
assumes "card X ≥ RN m n" "X⊆V"
shows "∃K ⊆ X. size_clique m K Red ∨ size_clique n K Blue"
using partn_lst_imp_is_clique_RN [OF is_Ramsey_number_RN [of m n]] assms indep_Red_iff_clique_Blue
unfolding is_clique_RN_def size_clique_def clique_indep_def
by (metis finV finite_subset subset_eq)
end
context Book
begin
lemma Red_edges_XY0: "Red ∩ all_edges_betw_un X0 Y0 ≠ {}"
using density_ge_p0_min p0_min
by (auto simp: gen_density_def edge_card_def)
lemma finite_X0: "finite X0" and finite_Y0: "finite Y0"
using XY0 finV finite_subset by blast+
lemma Red_nonempty: "Red ≠ {}"
using Red_edges_XY0 by blast
lemma gorder_ge2: "gorder ≥ 2"
using Red_nonempty
by (metis Red_E card_mono equals0I finV subset_empty two_edges wellformed)
lemma nontriv: "E ≠ {}"
using Red_E Red_nonempty by force
lemma no_singleton_Blue [simp]: "{a} ∉ Blue"
using Blue_E by auto
lemma no_singleton_Red [simp]: "{a} ∉ Red"
using Red_E by auto
lemma not_Red_Neighbour [simp]: "x ∉ Neighbours Red x" and not_Blue_Neighbour [simp]: "x ∉ Neighbours Blue x"
using Red_E Blue_E not_own_Neighbour by auto
lemma Neighbours_RB:
assumes "a ∈ V" "X⊆V"
shows "Neighbours Red a ∩ X ∪ Neighbours Blue a ∩ X = X - {a}"
using assms Red_Blue_all complete singleton_not_edge
by (fastforce simp: Neighbours_def)
lemma Neighbours_Red_Blue:
assumes "x ∈ V"
shows "Neighbours Red x = V - insert x (Neighbours Blue x)"
using Red_E assms by (auto simp: Blue_eq Neighbours_def complete all_edges_def)
abbreviation "red_density X Y ≡ gen_density Red X Y"
abbreviation "blue_density X Y ≡ gen_density Blue X Y"
definition Weight :: "['a set, 'a set, 'a, 'a] ⇒ real" where
"Weight ≡ λX Y x y. inverse (card Y) * (card (Neighbours Red x ∩ Neighbours Red y ∩ Y)
- red_density X Y * card (Neighbours Red x ∩ Y))"
definition weight :: "'a set ⇒ 'a set ⇒ 'a ⇒ real" where
"weight ≡ λX Y x. ∑y ∈ X-{x}. Weight X Y x y"
definition p0 :: "real"
where "p0 ≡ red_density X0 Y0"
definition qfun :: "nat ⇒ real"
where "qfun ≡ λh. p0 + qfun_base k h"
lemma qfun_eq: "qfun ≡ λh. p0 + ((1 + eps k)^h - 1) / k"
by (simp add: qfun_def qfun_base_def)
definition hgt :: "real ⇒ nat"
where "hgt ≡ λp. LEAST h. p ≤ qfun h ∧ h>0"
lemma qfun0 [simp]: "qfun 0 = p0"
by (simp add: qfun_eq)
lemma p0_ge: "p0 ≥ p0_min"
using density_ge_p0_min by (simp add: p0_def)
lemma card_XY0: "card X0 > 0" "card Y0 > 0"
using Red_edges_XY0 finite_X0 finite_Y0 by force+
lemma finite_Red [simp]: "finite Red"
by (metis Red_Blue_all complete fin_edges finite_Un)
lemma finite_Blue [simp]: "finite Blue"
using Blue_E fin_edges finite_subset by blast
lemma Red_edges_nonzero: "edge_card Red X0 Y0 > 0"
using Red_edges_XY0
using Red_E edge_card_def fin_edges finite_subset by fastforce
lemma p0_01: "0 < p0" "p0 ≤ 1"
proof -
show "0 < p0"
using Red_edges_nonzero card_XY0
by (auto simp: p0_def gen_density_def divide_simps mult_less_0_iff)
show "p0 ≤ 1"
by (simp add: gen_density_le1 p0_def)
qed
lemma qfun_strict_mono: "h'<h ⟹ qfun h' < qfun h"
by (simp add: divide_strict_right_mono eps_gt0 kn0 qfun_eq)
lemma qfun_mono: "h'≤h ⟹ qfun h' ≤ qfun h"
by (metis less_eq_real_def nat_less_le qfun_strict_mono)
lemma q_Suc_diff: "qfun (Suc h) - qfun h = eps k * (1 + eps k)^h / k"
by (simp add: qfun_eq field_split_simps)
lemma height_exists':
obtains h where "p ≤ qfun_base k h ∧ h>0"
proof -
have 1: "1 + eps k ≥ 1"
by (auto simp: eps_def)
have "∀⇧∞h. p ≤ real h * eps k / real k"
using p0_01 kn0 unfolding eps_def by real_asymp
then obtain h where "p ≤ real h * eps k / real k"
by (meson eventually_sequentially order.refl)
also have "… ≤ ((1 + eps k) ^ h - 1) / real k"
using linear_plus_1_le_power [of "eps k" h]
by (intro divide_right_mono add_mono) (auto simp: eps_def add_ac)
also have "… ≤ ((1 + eps k) ^ Suc h - 1) / real k"
using power_increasing [OF le_SucI [OF order_refl] 1]
by (simp add: divide_right_mono)
finally have "p ≤ qfun_base k (Suc h)"
unfolding qfun_base_def using p0_01 by blast
then show thesis
using that by blast
qed
lemma height_exists:
obtains h where "p ≤ qfun h" "h>0"
proof -
obtain h' where "p ≤ qfun_base k h' ∧ h'>0"
using height_exists' by blast
then show thesis
using p0_01 qfun_def that
by (metis add_strict_increasing less_eq_real_def)
qed
lemma hgt_gt0: "hgt p > 0"
unfolding hgt_def
by (smt (verit, best) LeastI height_exists kn0)
lemma hgt_works: "p ≤ qfun (hgt p)"
by (metis (no_types, lifting) LeastI height_exists hgt_def)
lemma hgt_Least:
assumes "0<h" "p ≤ qfun h"
shows "hgt p ≤ h"
by (simp add: Suc_leI assms hgt_def Least_le)
lemma real_hgt_Least:
assumes "real h ≤ r" "0<h" "p ≤ qfun h"
shows "real (hgt p) ≤ r"
using assms by (meson assms order.trans hgt_Least of_nat_mono)
lemma hgt_greater:
assumes "p > qfun h"
shows "hgt p > h"
by (meson assms hgt_works kn0 not_less order.trans qfun_mono)
lemma hgt_less_imp_qfun_less:
assumes "0<h" "h < hgt p"
shows "p > qfun h"
by (metis assms hgt_Least not_le)
lemma hgt_le_imp_qfun_ge:
assumes "hgt p ≤ h"
shows "p ≤ qfun h"
by (meson assms hgt_greater not_less)
text ‹This gives us an upper bound for heights, namely @{term "hgt 1"}, but it's not explicit.›
lemma hgt_mono:
assumes "p ≤ q"
shows "hgt p ≤ hgt q"
by (meson assms order.trans hgt_Least hgt_gt0 hgt_works)
lemma hgt_mono':
assumes "hgt p < hgt q"
shows "p < q"
by (smt (verit) assms hgt_mono leD)
text ‹The upper bound of the height $h(p)$ appears just below (5) on page 9.
Although we can bound all Heights by monotonicity (since @{term "p≤1"}),
we need to exhibit a specific $o(k)$ function.›
lemma height_upper_bound:
assumes "p ≤ 1" and big: "Big_height_upper_bound k"
shows "hgt p ≤ 2 * ln k / eps k"
using assms real_hgt_Least big nat_floor_neg not_gr0 of_nat_floor
unfolding Big_height_upper_bound_def hgt_maximum_def
by (smt (verit, ccfv_SIG) p0_01(1) power.simps(1) qfun_def qfun_eq zero_less_divide_iff)
definition alpha :: "nat ⇒ real" where "alpha ≡ λh. qfun h - qfun (h-1)"
lemma alpha_ge0: "alpha h ≥ 0"
by (simp add: alpha_def qfun_eq divide_le_cancel eps_gt0)
lemma alpha_Suc_ge: "alpha (Suc h) ≥ eps k / k"
proof -
have "(1 + eps k) ^ h ≥ 1"
by (simp add: eps_def)
then show ?thesis
by (simp add: alpha_def qfun_eq eps_gt0 field_split_simps)
qed
lemma alpha_ge: "h>0 ⟹ alpha h ≥ eps k / k"
by (metis Suc_pred alpha_Suc_ge)
lemma alpha_gt0: "h>0 ⟹ alpha h > 0"
by (metis alpha_ge alpha_ge0 eps_gt0 kn0 nle_le not_le of_nat_0_less_iff zero_less_divide_iff)
lemma alpha_Suc_eq: "alpha (Suc h) = eps k * (1 + eps k) ^ h / k"
by (simp add: alpha_def q_Suc_diff)
lemma alpha_eq:
assumes "h>0" shows "alpha h = eps k * (1 + eps k) ^ (h-1) / k"
by (metis Suc_pred' alpha_Suc_eq assms)
lemma alpha_hgt_eq: "alpha (hgt p) = eps k * (1 + eps k) ^ (hgt p -1) / k"
using alpha_eq hgt_gt0 by presburger
lemma alpha_mono: "⟦h' ≤ h; 0 < h'⟧ ⟹ alpha h' ≤ alpha h"
by (simp add: alpha_eq eps_ge0 divide_right_mono mult_left_mono power_increasing)
definition all_incident_edges :: "'a set ⇒ 'a set set" where
"all_incident_edges ≡ λA. ⋃v∈A. incident_edges v"
lemma all_incident_edges_Un [simp]: "all_incident_edges (A∪B) = all_incident_edges A ∪ all_incident_edges B"
by (auto simp: all_incident_edges_def)
end
context Book
begin
subsection ‹State invariants›
definition "V_state ≡ λ(X,Y,A,B). X⊆V ∧ Y⊆V ∧ A⊆V ∧ B⊆V"
definition "disjoint_state ≡ λ(X,Y,A,B). disjnt X Y ∧ disjnt X A ∧ disjnt X B ∧ disjnt Y A ∧ disjnt Y B ∧ disjnt A B"
text ‹previously had all edges incident to A, B›
definition "RB_state ≡ λ(X,Y,A,B). all_edges_betw_un A A ⊆ Red ∧ all_edges_betw_un A (X ∪ Y) ⊆ Red
∧ all_edges_betw_un B (B ∪ X) ⊆ Blue"
definition "valid_state ≡ λU. V_state U ∧ disjoint_state U ∧ RB_state U"
definition "termination_condition ≡ λX Y. card X ≤ RN k (nat ⌈real l powr (3/4)⌉) ∨ red_density X Y ≤ 1/k"
lemma
assumes "V_state(X,Y,A,B)"
shows finX: "finite X" and finY: "finite Y" and finA: "finite A" and finB: "finite B"
using V_state_def assms finV finite_subset by auto
lemma
assumes "valid_state(X,Y,A,B)"
shows A_Red_clique: "clique A Red" and B_Blue_clique: "clique B Blue"
using assms
by (auto simp: valid_state_def V_state_def RB_state_def all_edges_betw_un_iff_clique all_edges_betw_un_Un2)
lemma A_less_k:
assumes valid: "valid_state(X,Y,A,B)"
shows "card A < k"
using assms A_Red_clique[OF valid] no_Red_clique unfolding valid_state_def V_state_def
by (metis nat_neq_iff prod.case size_clique_def size_clique_smaller)
lemma B_less_l:
assumes valid: "valid_state(X,Y,A,B)"
shows "card B < l"
using assms B_Blue_clique[OF valid] no_Blue_clique unfolding valid_state_def V_state_def
by (metis nat_neq_iff prod.case size_clique_def size_clique_smaller)
subsection ‹Degree regularisation›
definition "red_dense ≡ λY p x. card (Neighbours Red x ∩ Y) ≥ (p - eps k powr (-1/2) * alpha (hgt p)) * card Y"
definition "X_degree_reg ≡ λX Y. {x ∈ X. red_dense Y (red_density X Y) x}"
definition "degree_reg ≡ λ(X,Y,A,B). (X_degree_reg X Y, Y, A, B)"
lemma X_degree_reg_subset: "X_degree_reg X Y ⊆ X"
by (auto simp: X_degree_reg_def)
lemma degree_reg_V_state: "V_state U ⟹ V_state (degree_reg U)"
by (auto simp: degree_reg_def X_degree_reg_def V_state_def)
lemma degree_reg_disjoint_state: "disjoint_state U ⟹ disjoint_state (degree_reg U)"
by (auto simp: degree_reg_def X_degree_reg_def disjoint_state_def disjnt_iff)
lemma degree_reg_RB_state: "RB_state U ⟹ RB_state (degree_reg U)"
apply (simp add: degree_reg_def RB_state_def all_edges_betw_un_Un2 split: prod.split prod.split_asm)
by (meson X_degree_reg_subset all_edges_betw_un_mono2 order.trans)
lemma degree_reg_valid_state: "valid_state U ⟹ valid_state (degree_reg U)"
by (simp add: degree_reg_RB_state degree_reg_V_state degree_reg_disjoint_state valid_state_def)
lemma not_red_dense_sum_less:
assumes "⋀x. x ∈ X ⟹ ¬ red_dense Y p x" and "X≠{}" "finite X"
shows "(∑x∈X. card (Neighbours Red x ∩ Y)) < p * real (card Y) * card X"
proof -
have "⋀x. x ∈ X ⟹ card (Neighbours Red x ∩ Y) < p * real (card Y)"
using assms
unfolding red_dense_def
by (smt (verit) alpha_ge0 mult_right_mono of_nat_0_le_iff powr_ge_pzero zero_le_mult_iff)
with ‹X≠{}› show ?thesis
by (smt (verit) ‹finite X› of_nat_sum sum_strict_mono mult_of_nat_commute sum_constant)
qed
lemma red_density_X_degree_reg_ge:
assumes "disjnt X Y"
shows "red_density (X_degree_reg X Y) Y ≥ red_density X Y"
proof (cases "X={} ∨ infinite X ∨ infinite Y")
case True
then show ?thesis
by (force simp: gen_density_def X_degree_reg_def)
next
case False
then have "finite X" "finite Y"
by auto
{ assume "⋀x. x ∈ X ⟹ ¬ red_dense Y (red_density X Y) x"
with False have "(∑x∈X. card (Neighbours Red x ∩ Y)) < red_density X Y * real (card Y) * card X"
using ‹finite X› not_red_dense_sum_less by blast
with Red_E have "edge_card Red Y X < (red_density X Y * real (card Y)) * card X"
by (metis False assms disjnt_sym edge_card_eq_sum_Neighbours)
then have False
by (simp add: gen_density_def edge_card_commute split: if_split_asm)
}
then obtain x where x: "x ∈ X" "red_dense Y (red_density X Y) x"
by blast
define X' where "X' ≡ {x ∈ X. ¬ red_dense Y (red_density X Y) x}"
have X': "finite X'" "disjnt Y X'"
using assms ‹finite X› by (auto simp: X'_def disjnt_iff)
have eq: "X_degree_reg X Y = X - X'"
by (auto simp: X_degree_reg_def X'_def)
show ?thesis
proof (cases "X'={}")
case True
then show ?thesis
by (simp add: eq)
next
case False
show ?thesis
unfolding eq
proof (rule gen_density_below_avg_ge)
have "(∑x∈X'. card (Neighbours Red x ∩ Y)) < red_density X Y * real (card Y) * card X'"
proof (intro not_red_dense_sum_less)
fix x
assume "x ∈ X'"
show "¬ red_dense Y (red_density X Y) x"
using ‹x ∈ X'› by (simp add: X'_def)
qed (use False X' in auto)
then have "card X * (∑x∈X'. card (Neighbours Red x ∩ Y)) < card X' * edge_card Red Y X"
by (simp add: gen_density_def mult.commute divide_simps edge_card_commute
flip: of_nat_sum of_nat_mult split: if_split_asm)
then have "card X * (∑x∈X'. card (Neighbours Red x ∩ Y)) ≤ card X' * (∑x∈X. card (Neighbours Red x ∩ Y))"
using assms Red_E
by (metis ‹finite X› disjnt_sym edge_card_eq_sum_Neighbours nless_le)
then have "red_density Y X' ≤ red_density Y X"
using assms X' False ‹finite X›
apply (simp add: gen_density_def edge_card_eq_sum_Neighbours disjnt_commute Red_E)
apply (simp add: X'_def field_split_simps flip: of_nat_sum of_nat_mult)
done
then show "red_density X' Y ≤ red_density X Y"
by (simp add: X'_def gen_density_commute)
qed (use assms x ‹finite X› ‹finite Y› X'_def in auto)
qed
qed
subsection ‹Big blue steps: code›
definition bluish :: "['a set,'a] ⇒ bool" where
"bluish ≡ λX x. card (Neighbours Blue x ∩ X) ≥ μ * real (card X)"
definition many_bluish :: "'a set ⇒ bool" where
"many_bluish ≡ λX. card {x∈X. bluish X x} ≥ RN k (nat ⌈l powr (2/3)⌉)"
definition good_blue_book :: "['a set, 'a set × 'a set] ⇒ bool" where
"good_blue_book ≡ λX. λ(S,T). book S T Blue ∧ S⊆X ∧ T⊆X ∧ card T ≥ (μ ^ card S) * card X / 2"
lemma ex_good_blue_book: "good_blue_book X ({}, X)"
by (simp add: good_blue_book_def book_def)
lemma bounded_good_blue_book: "⟦good_blue_book X (S,T); finite X⟧ ⟹ card S ≤ card X"
by (simp add: card_mono finX good_blue_book_def)
definition best_blue_book_card :: "'a set ⇒ nat" where
"best_blue_book_card ≡ λX. GREATEST s. ∃S T. good_blue_book X (S,T) ∧ s = card S"
lemma best_blue_book_is_best: "⟦good_blue_book X (S,T); finite X⟧ ⟹ card S ≤ best_blue_book_card X"
unfolding best_blue_book_card_def
by (smt (verit) Greatest_le_nat bounded_good_blue_book)
lemma ex_best_blue_book: "finite X ⟹ ∃S T. good_blue_book X (S,T) ∧ card S = best_blue_book_card X"
unfolding best_blue_book_card_def
by (smt (verit) GreatestI_ex_nat bounded_good_blue_book ex_good_blue_book)
definition "choose_blue_book ≡ λ(X,Y,A,B). @(S,T). good_blue_book X (S,T) ∧ card S = best_blue_book_card X"
lemma choose_blue_book_works:
"⟦finite X; (S,T) = choose_blue_book (X,Y,A,B)⟧
⟹ good_blue_book X (S,T) ∧ card S = best_blue_book_card X"
unfolding choose_blue_book_def
using someI_ex [OF ex_best_blue_book]
by (metis (mono_tags, lifting) case_prod_conv someI_ex)
lemma choose_blue_book_subset:
"⟦finite X; (S,T) = choose_blue_book (X,Y,A,B)⟧ ⟹ S ⊆ X ∧ T ⊆ X ∧ disjnt S T"
using choose_blue_book_works good_blue_book_def book_def by fastforce
text ‹expressing the complicated preconditions inductively›
inductive big_blue
where "⟦many_bluish X; good_blue_book X (S,T); card S = best_blue_book_card X⟧ ⟹ big_blue (X,Y,A,B) (T, Y, A, B∪S)"
lemma big_blue_V_state: "⟦big_blue U U'; V_state U⟧ ⟹ V_state U'"
by (force simp: good_blue_book_def V_state_def elim!: big_blue.cases)
lemma big_blue_disjoint_state: "⟦big_blue U U'; disjoint_state U⟧ ⟹ disjoint_state U'"
by (force simp: book_def disjnt_iff good_blue_book_def disjoint_state_def elim!: big_blue.cases)
lemma big_blue_RB_state: "⟦big_blue U U'; RB_state U⟧ ⟹ RB_state U'"
apply (clarsimp simp add: good_blue_book_def book_def RB_state_def all_edges_betw_un_Un1 all_edges_betw_un_Un2 elim!: big_blue.cases)
by (metis all_edges_betw_un_commute all_edges_betw_un_mono1 le_supI2 sup.orderE)
lemma big_blue_valid_state: "⟦big_blue U U'; valid_state U⟧ ⟹ valid_state U'"
by (meson big_blue_RB_state big_blue_V_state big_blue_disjoint_state valid_state_def)
subsection ‹The central vertex›
definition central_vertex :: "['a set,'a] ⇒ bool" where
"central_vertex ≡ λX x. x ∈ X ∧ card (Neighbours Blue x ∩ X) ≤ μ * real (card X)"
lemma ex_central_vertex:
assumes "¬ termination_condition X Y" "¬ many_bluish X"
shows "∃x. central_vertex X x"
proof -
have "l ≠ 0"
using linorder_not_less assms unfolding many_bluish_def by force
then have *: "real l powr (2/3) ≤ real l powr (3/4)"
using powr_mono by force
then have "card {x ∈ X. bluish X x} < card X"
using assms RN_mono
unfolding termination_condition_def many_bluish_def not_le
by (smt (verit, ccfv_SIG) linorder_not_le nat_ceiling_le_eq of_nat_le_iff)
then obtain x where "x ∈ X" "¬ bluish X x"
by (metis (mono_tags, lifting) mem_Collect_eq nat_neq_iff subsetI subset_antisym)
then show ?thesis
by (meson bluish_def central_vertex_def linorder_linear)
qed
lemma finite_central_vertex_set: "finite X ⟹ finite {x. central_vertex X x}"
by (simp add: central_vertex_def)
definition max_central_vx :: "['a set,'a set] ⇒ real" where
"max_central_vx ≡ λX Y. Max (weight X Y ` {x. central_vertex X x})"
lemma central_vx_is_best:
"⟦central_vertex X x; finite X⟧ ⟹ weight X Y x ≤ max_central_vx X Y"
unfolding max_central_vx_def by (simp add: finite_central_vertex_set)
lemma ex_best_central_vx:
"⟦¬ termination_condition X Y; ¬ many_bluish X; finite X⟧
⟹ ∃x. central_vertex X x ∧ weight X Y x = max_central_vx X Y"
unfolding max_central_vx_def
by (metis empty_iff ex_central_vertex finite_central_vertex_set mem_Collect_eq obtains_MAX)
text ‹it's necessary to make a specific choice; a relational treatment might allow different vertices
to be chosen, making a nonsense of the choice between steps 4 and 5›
definition "choose_central_vx ≡ λ(X,Y,A,B). @x. central_vertex X x ∧ weight X Y x = max_central_vx X Y"
lemma choose_central_vx_works:
"⟦¬ termination_condition X Y; ¬ many_bluish X; finite X⟧
⟹ central_vertex X (choose_central_vx (X,Y,A,B)) ∧ weight X Y (choose_central_vx (X,Y,A,B)) = max_central_vx X Y"
unfolding choose_central_vx_def
using someI_ex [OF ex_best_central_vx] by force
lemma choose_central_vx_X:
"⟦¬ many_bluish X; ¬ termination_condition X Y; finite X⟧ ⟹ choose_central_vx (X,Y,A,B) ∈ X"
using central_vertex_def choose_central_vx_works by fastforce
subsection ‹Red step›
definition "reddish ≡ λk X Y p x. red_density (Neighbours Red x ∩ X) (Neighbours Red x ∩ Y) ≥ p - alpha (hgt p)"
inductive red_step
where "⟦reddish k X Y (red_density X Y) x; x = choose_central_vx (X,Y,A,B)⟧
⟹ red_step (X,Y,A,B) (Neighbours Red x ∩ X, Neighbours Red x ∩ Y, insert x A, B)"
lemma red_step_V_state:
assumes "red_step (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "V_state (X,Y,A,B)"
shows "V_state U'"
proof -
have "X ⊆ V"
using assms by (auto simp: V_state_def)
then have "choose_central_vx (X, Y, A, B) ∈ V"
using assms choose_central_vx_X by (fastforce simp: finX)
with assms show ?thesis
by (auto simp: V_state_def elim!: red_step.cases)
qed
lemma red_step_disjoint_state:
assumes "red_step (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "V_state (X,Y,A,B)" "disjoint_state (X,Y,A,B)"
shows "disjoint_state U'"
proof -
have "choose_central_vx (X, Y, A, B) ∈ X"
using assms by (metis choose_central_vx_X finX)
with assms show ?thesis
by (auto simp: disjoint_state_def disjnt_iff not_own_Neighbour elim!: red_step.cases)
qed
lemma red_step_RB_state:
assumes "red_step (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "V_state (X,Y,A,B)" "RB_state (X,Y,A,B)"
shows "RB_state U'"
proof -
define x where "x ≡ choose_central_vx (X, Y, A, B)"
have [simp]: "finite X"
using assms by (simp add: finX)
have "x ∈ X"
using assms choose_central_vx_X by (metis ‹finite X› x_def)
have A: "all_edges_betw_un (insert x A) (insert x A) ⊆ Red"
if "all_edges_betw_un A A ⊆ Red" "all_edges_betw_un A (X ∪ Y) ⊆ Red"
using that ‹x ∈ X› all_edges_betw_un_commute
by (auto simp: all_edges_betw_un_insert2 all_edges_betw_un_Un2 intro!: all_uedges_betw_I)
have B1: "all_edges_betw_un (insert x A) (Neighbours Red x ∩ X) ⊆ Red"
if "all_edges_betw_un A X ⊆ Red"
using that ‹x ∈ X› by (force simp: all_edges_betw_un_def in_Neighbours_iff)
have B2: "all_edges_betw_un (insert x A) (Neighbours Red x ∩ Y) ⊆ Red"
if "all_edges_betw_un A Y ⊆ Red"
using that ‹x ∈ X› by (force simp: all_edges_betw_un_def in_Neighbours_iff)
from assms A B1 B2 show ?thesis
apply (clarsimp simp: RB_state_def simp flip: x_def elim!: red_step.cases)
by (metis Int_Un_eq(2) Un_subset_iff all_edges_betw_un_Un2)
qed
lemma red_step_valid_state:
assumes "red_step (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "valid_state (X,Y,A,B)"
shows "valid_state U'"
by (meson assms red_step_RB_state red_step_V_state red_step_disjoint_state valid_state_def)
subsection ‹Density-boost step›
inductive density_boost
where "⟦¬ reddish k X Y (red_density X Y) x; x = choose_central_vx (X,Y,A,B)⟧
⟹ density_boost (X,Y,A,B) (Neighbours Blue x ∩ X, Neighbours Red x ∩ Y, A, insert x B)"
lemma density_boost_V_state:
assumes "density_boost (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "V_state (X,Y,A,B)"
shows "V_state U'"
proof -
have "X ⊆ V"
using assms by (auto simp: V_state_def)
then have "choose_central_vx (X, Y, A, B) ∈ V"
using assms choose_central_vx_X finX by fastforce
with assms show ?thesis
by (auto simp: V_state_def elim!: density_boost.cases)
qed
lemma density_boost_disjoint_state:
assumes "density_boost (X,Y,A,B) U'" "¬ termination_condition X Y"
"¬ many_bluish X" "V_state (X,Y,A,B)" "disjoint_state (X,Y,A,B)"
shows "disjoint_state U'"
proof -
have "X ⊆ V"
using assms by (auto simp: V_state_def)
then have "choose_central_vx (X, Y, A, B) ∈ X"
using assms by (metis choose_central_vx_X finX)
with assms show ?thesis
by (auto simp: disjoint_state_def disjnt_iff not_own_Neighbour elim!: density_boost.cases)
qed
lemma density_boost_RB_state:
assumes "density_boost (X,Y,A,B) U'" "¬ termination_condition X Y" "¬ many_bluish X" "V_state (X,Y,A,B)"
and rb: "RB_state (X,Y,A,B)"
shows "RB_state U'"
proof -
define x where "x ≡ choose_central_vx (X, Y, A, B)"
have "x ∈ X"
using assms by (metis choose_central_vx_X finX x_def)
have "all_edges_betw_un A (Neighbours Blue x ∩ X ∪ Neighbours Red x ∩ Y) ⊆ Red"
if "all_edges_betw_un A (X ∪ Y) ⊆ Red"
using that by (metis Int_Un_eq(4) Un_subset_iff all_edges_betw_un_Un2)
moreover
have "all_edges_betw_un (insert x B) (insert x B) ⊆ Blue"
if "all_edges_betw_un B (B ∪ X) ⊆ Blue"
using that ‹x ∈ X› by (auto simp: subset_iff set_eq_iff all_edges_betw_un_def)
moreover
have "all_edges_betw_un (insert x B) (Neighbours Blue x ∩ X) ⊆ Blue"
if "all_edges_betw_un B (B ∪ X) ⊆ Blue"
using ‹x ∈ X› that by (auto simp: all_edges_betw_un_def subset_iff in_Neighbours_iff)
ultimately show ?thesis
using assms
by (auto simp: RB_state_def all_edges_betw_un_Un2 x_def [symmetric] elim!: density_boost.cases)
qed
lemma density_boost_valid_state:
assumes "density_boost (X,Y,A,B) U'" "¬ termination_condition X Y" "¬ many_bluish X" "valid_state (X,Y,A,B)"
shows "valid_state U'"
by (meson assms density_boost_RB_state density_boost_V_state density_boost_disjoint_state valid_state_def)
subsection ‹Execution steps 2--5 as a function›
definition next_state :: "'a config ⇒ 'a config" where
"next_state ≡ λ(X,Y,A,B).
if many_bluish X
then let (S,T) = choose_blue_book (X,Y,A,B) in (T, Y, A, B∪S)
else let x = choose_central_vx (X,Y,A,B) in
if reddish k X Y (red_density X Y) x
then (Neighbours Red x ∩ X, Neighbours Red x ∩ Y, insert x A, B)
else (Neighbours Blue x ∩ X, Neighbours Red x ∩ Y, A, insert x B)"
lemma next_state_valid:
assumes "valid_state (X,Y,A,B)" "¬ termination_condition X Y"
shows "valid_state (next_state (X,Y,A,B))"
proof (cases "many_bluish X")
case True
with finX have "big_blue (X,Y,A,B) (next_state (X,Y,A,B))"
apply (simp add: next_state_def split: prod.split)
by (metis assms(1) big_blue.intros choose_blue_book_works valid_state_def)
then show ?thesis
using assms big_blue_valid_state by blast
next
case non_bluish: False
define x where "x = choose_central_vx (X,Y,A,B)"
show ?thesis
proof (cases "reddish k X Y (red_density X Y) x")
case True
with non_bluish have "red_step (X,Y,A,B) (next_state (X,Y,A,B))"
by (simp add: next_state_def Let_def x_def red_step.intros split: prod.split)
then show ?thesis
using assms non_bluish red_step_valid_state by blast
next
case False
with non_bluish have "density_boost (X,Y,A,B) (next_state (X,Y,A,B))"
by (simp add: next_state_def Let_def x_def density_boost.intros split: prod.split)
then show ?thesis
using assms density_boost_valid_state non_bluish by blast
qed
qed
primrec stepper :: "nat ⇒ 'a config" where
"stepper 0 = (X0,Y0,{},{})"
| "stepper (Suc n) =
(let (X,Y,A,B) = stepper n in
if termination_condition X Y then (X,Y,A,B)
else if even n then degree_reg (X,Y,A,B) else next_state (X,Y,A,B))"
lemma degree_reg_subset:
assumes "degree_reg (X,Y,A,B) = (X',Y',A',B')"
shows "X' ⊆ X ∧ Y' ⊆ Y"
using assms by (auto simp: degree_reg_def X_degree_reg_def)
lemma next_state_subset:
assumes "next_state (X,Y,A,B) = (X',Y',A',B')" "finite X"
shows "X' ⊆ X ∧ Y' ⊆ Y"
using assms choose_blue_book_subset
apply (clarsimp simp: next_state_def valid_state_def Let_def split: if_split_asm prod.split_asm)
by (smt (verit) choose_blue_book_subset subset_eq)
lemma valid_state0: "valid_state (X0, Y0, {}, {})"
using XY0 by (simp add: valid_state_def V_state_def disjoint_state_def RB_state_def)
lemma valid_state_stepper [simp]: "valid_state (stepper n)"
proof (induction n)
case 0
then show ?case
by (simp add: stepper_def valid_state0)
next
case (Suc n)
then show ?case
by (force simp: next_state_valid degree_reg_valid_state split: prod.split)
qed
lemma V_state_stepper: "V_state (stepper n)"
using valid_state_def valid_state_stepper by force
lemma RB_state_stepper: "RB_state (stepper n)"
using valid_state_def valid_state_stepper by force
lemma
assumes "stepper n = (X,Y,A,B)"
shows stepper_A: "clique A Red ∧ A⊆V" and stepper_B: "clique B Blue ∧ B⊆V"
proof -
have "A⊆V" "B⊆V"
using V_state_stepper[of n] assms by (auto simp: V_state_def)
moreover
have "all_edges_betw_un A A ⊆ Red" "all_edges_betw_un B B ⊆ Blue"
using RB_state_stepper[of n] assms by (auto simp: RB_state_def all_edges_betw_un_Un2)
ultimately show "clique A Red ∧ A⊆V" "clique B Blue ∧ B⊆V"
using all_edges_betw_un_iff_clique by auto
qed
lemma card_B_limit:
assumes "stepper n = (X,Y,A,B)" shows "card B < l"
by (metis B_less_l assms valid_state_stepper)
definition "Xseq ≡ (λ(X,Y,A,B). X) ∘ stepper"
definition "Yseq ≡ (λ(X,Y,A,B). Y) ∘ stepper"
definition "Aseq ≡ (λ(X,Y,A,B). A) ∘ stepper"
definition "Bseq ≡ (λ(X,Y,A,B). B) ∘ stepper"
definition "pseq ≡ λn. red_density (Xseq n) (Yseq n)"
definition "pee ≡ λi. red_density (Xseq i) (Yseq i)"
lemma Xseq_0 [simp]: "Xseq 0 = X0"
by (simp add: Xseq_def)
lemma Xseq_Suc_subset: "Xseq (Suc i) ⊆ Xseq i" and Yseq_Suc_subset: "Yseq (Suc i) ⊆ Yseq i"
apply (simp_all add: Xseq_def Yseq_def split: if_split_asm prod.split)
by (metis V_state_stepper degree_reg_subset finX next_state_subset)+
lemma Xseq_antimono: "j ≤ i ⟹ Xseq i ⊆ Xseq j"
by (simp add: lift_Suc_antimono_le[of UNIV] Xseq_Suc_subset)
lemma Xseq_subset_V: "Xseq i ⊆ V"
using XY0 Xseq_0 Xseq_antimono by blast
lemma finite_Xseq: "finite (Xseq i)"
by (meson Xseq_subset_V finV finite_subset)
lemma Yseq_0 [simp]: "Yseq 0 = Y0"
by (simp add: Yseq_def)
lemma Yseq_antimono: "j ≤ i ⟹ Yseq i ⊆ Yseq j"
by (simp add: Yseq_Suc_subset lift_Suc_antimono_le[of UNIV])
lemma Yseq_subset_V: "Yseq i ⊆ V"
using XY0 Yseq_0 Yseq_antimono by blast
lemma finite_Yseq: "finite (Yseq i)"
by (meson Yseq_subset_V finV finite_subset)
lemma Xseq_Yseq_disjnt: "disjnt (Xseq i) (Yseq i)"
by (metis XY0(1) Xseq_0 Xseq_antimono Yseq_0 Yseq_antimono disjnt_subset1 disjnt_sym zero_le)
lemma edge_card_eq_pee:
"edge_card Red (Xseq i) (Yseq i) = pee i * card (Xseq i) * card (Yseq i)"
by (simp add: pee_def gen_density_def finite_Xseq finite_Yseq)
lemma valid_state_seq: "valid_state(Xseq i, Yseq i, Aseq i, Bseq i)"
using valid_state_stepper[of i]
by (force simp: Xseq_def Yseq_def Aseq_def Bseq_def simp del: valid_state_stepper split: prod.split)
lemma Aseq_less_k: "card (Aseq i) < k"
by (meson A_less_k valid_state_seq)
lemma Aseq_0 [simp]: "Aseq 0 = {}"
by (simp add: Aseq_def)
lemma Aseq_Suc_subset: "Aseq i ⊆ Aseq (Suc i)" and Bseq_Suc_subset: "Bseq i ⊆ Bseq (Suc i)"
by (auto simp: Aseq_def Bseq_def next_state_def degree_reg_def Let_def split: prod.split)
lemma
assumes "j ≤ i"
shows Aseq_mono: "Aseq j ⊆ Aseq i" and Bseq_mono: "Bseq j ⊆ Bseq i"
using assms by (auto simp: Aseq_Suc_subset Bseq_Suc_subset lift_Suc_mono_le[of UNIV])
lemma Aseq_subset_V: "Aseq i ⊆ V"
using stepper_A[of i] by (simp add: Aseq_def split: prod.split)
lemma Bseq_subset_V: "Bseq i ⊆ V"
using stepper_B[of i] by (simp add: Bseq_def split: prod.split)
lemma finite_Aseq: "finite (Aseq i)" and finite_Bseq: "finite (Bseq i)"
by (meson Aseq_subset_V Bseq_subset_V finV finite_subset)+
lemma Bseq_less_l: "card (Bseq i) < l"
by (meson B_less_l valid_state_seq)
lemma Bseq_0 [simp]: "Bseq 0 = {}"
by (simp add: Bseq_def)
lemma pee_eq_p0: "pee 0 = p0"
by (simp add: pee_def p0_def)
lemma pee_ge0: "pee i ≥ 0"
by (simp add: gen_density_ge0 pee_def)
lemma pee_le1: "pee i ≤ 1"
using gen_density_le1 pee_def by presburger
lemma pseq_0: "p0 = pseq 0"
by (simp add: p0_def pseq_def Xseq_def Yseq_def)
text ‹The central vertex at each step (though only defined in some cases),
@{term "x_i"} in the paper›
definition "cvx ≡ λi. choose_central_vx (stepper i)"
text ‹the indexing of @{term beta} is as in the paper --- and different from that of @{term Xseq}›
definition
"beta ≡ λi. let (X,Y,A,B) = stepper i in card(Neighbours Blue (cvx i) ∩ X) / card X"
lemma beta_eq: "beta i = card(Neighbours Blue (cvx i) ∩ Xseq i) / card (Xseq i)"
by (simp add: beta_def cvx_def Xseq_def split: prod.split)
lemma beta_ge0: "beta i ≥ 0"
by (simp add: beta_eq)
subsection ‹The classes of execution steps›
text ‹For R, B, S, D›