diff --git a/thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy b/thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy --- a/thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy +++ b/thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy @@ -1,664 +1,656 @@ 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)" + "complete V = (V, all_edges V)" lemma complete_wellformed: "uwellformed (complete V)" -unfolding complete_def uwellformed_def all_edges_def -by simp + 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 + 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 + 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 + 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 + 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 + using cylinder_prob by auto subsection\Subgraphs\ definition subgraph :: "ugraph \ ugraph \ bool" where -"subgraph G' G \ uverts G' \ uverts G \ uedges G' \ uedges G" + "subgraph G' G \ uverts G' \ uverts G \ uedges G' \ uedges G" lemma subgraph_refl: "subgraph G G" -unfolding subgraph_def -by simp + unfolding subgraph_def + by simp lemma subgraph_trans: "subgraph G'' G' \ subgraph G' G \ subgraph G'' G" -unfolding subgraph_def -by auto + 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) + 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 + 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) + 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 H\<^sub>1 \ S" and "uverts H\<^sub>2 \ T" assumes "uwellformed H\<^sub>1" and "uwellformed H\<^sub>2" shows "subgraph H\<^sub>1 (induced_subgraph S G) \ subgraph H\<^sub>2 (induced_subgraph T G) \ subgraph (uverts H\<^sub>1 \ uverts H\<^sub>2, uedges H\<^sub>1 \ uedges H\<^sub>2) (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 G\<^sub>1 G\<^sub>2 f \ bij_betw f (uverts G\<^sub>1) (uverts G\<^sub>2) \ G\<^sub>2 = map_ugraph f G\<^sub>1" abbreviation isomorphic :: "ugraph \ ugraph \ bool" ("_ \ _") where "G\<^sub>1 \ G\<^sub>2 \ uwellformed G\<^sub>1 \ uwellformed G\<^sub>2 \ (\f. isomorphism G\<^sub>1 G\<^sub>2 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 G\<^sub>1 G\<^sub>2" shows "subgraph (map_ugraph f G\<^sub>1) (map_ugraph f G\<^sub>2)" proof - have "f ` uverts G\<^sub>1 \ f ` uverts G\<^sub>2" "(\e. f ` e) ` uedges G\<^sub>1 \ (\e. f ` e) ` uedges G\<^sub>2" 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 "G\<^sub>1 \ G\<^sub>2" and "G\<^sub>2 \ G\<^sub>3" shows "G\<^sub>1 \ G\<^sub>3" proof - from assms obtain f\<^sub>1 f\<^sub>2 where bij: "bij_betw f\<^sub>1 (uverts G\<^sub>1) (uverts G\<^sub>2)" "bij_betw f\<^sub>2 (uverts G\<^sub>2) (uverts G\<^sub>3)" and map: "G\<^sub>2 = map_ugraph f\<^sub>1 G\<^sub>1" "G\<^sub>3 = map_ugraph f\<^sub>2 G\<^sub>2" unfolding isomorphism_def by blast let ?f = "f\<^sub>2 \ f\<^sub>1" have "bij_betw ?f (uverts G\<^sub>1) (uverts G\<^sub>3)" using bij by (simp add: bij_betw_comp_iff) moreover have "G\<^sub>3 = map_ugraph ?f G\<^sub>1" using map by (simp add: map_ugraph_trans) moreover have "uwellformed G\<^sub>1" "uwellformed G\<^sub>3" using assms unfolding isomorphism_def by simp+ ultimately show "G\<^sub>1 \ G\<^sub>3" unfolding isomorphism_def by blast qed lemma isomorphic_sym: assumes "G\<^sub>1 \ G\<^sub>2" shows "G\<^sub>2 \ G\<^sub>1" proof safe from assms obtain f where "isomorphism G\<^sub>1 G\<^sub>2 f" by blast hence bij: "bij_betw f (uverts G\<^sub>1) (uverts G\<^sub>2)" and map: "G\<^sub>2 = map_ugraph f G\<^sub>1" unfolding isomorphism_def by auto let ?f' = "inv_into (uverts G\<^sub>1) f" have bij': "bij_betw ?f' (uverts G\<^sub>2) (uverts G\<^sub>1)" by (rule bij_betw_inv_into) fact moreover have "uverts G\<^sub>1 = ?f' ` uverts G\<^sub>2" using bij' unfolding bij_betw_def by force moreover have "uedges G\<^sub>1 = (\e. ?f' ` e) ` uedges G\<^sub>2" proof - have "uedges G\<^sub>1 = id ` uedges G\<^sub>1" by simp also have "\ = (\e. ?f' ` (f ` e)) ` uedges G\<^sub>1" proof (rule image_cong) fix a assume "a \ uedges G\<^sub>1" hence "a \ uverts G\<^sub>1" using assms unfolding isomorphism_def uwellformed_def by blast thus "id a = inv_into (uverts G\<^sub>1) 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 G\<^sub>1)" by (rule image_image[symmetric]) also have "\ = (\e. ?f' ` e) ` uedges G\<^sub>2" using bij map by (metis map_ugraph.simps prod.collapse snd_eqD) finally show ?thesis . qed ultimately have "isomorphism G\<^sub>2 G\<^sub>1 ?f'" unfolding isomorphism_def by (metis map_ugraph.simps split_pairs) thus "\f. isomorphism G\<^sub>2 G\<^sub>1 f" by blast qed (auto simp: assms) lemma isomorphic_cards: assumes "G\<^sub>1 \ G\<^sub>2" shows "card (uverts G\<^sub>1) = card (uverts G\<^sub>2)" (is "?V") "card (uedges G\<^sub>1) = card (uedges G\<^sub>2)" (is "?E") proof - from assms obtain f where bij: "bij_betw f (uverts G\<^sub>1) (uverts G\<^sub>2)" and map: "G\<^sub>2 = map_ugraph f G\<^sub>1" unfolding isomorphism_def by blast from assms have wellformed: "uwellformed G\<^sub>1" "uwellformed G\<^sub>2" by simp+ show ?V by (rule bij_betw_same_card[OF bij]) let ?g = "\e. f ` e" have "bij_betw ?g (Pow (uverts G\<^sub>1)) (Pow (uverts G\<^sub>2))" by (rule bij_lift[OF bij]) moreover have "uedges G\<^sub>1 \ Pow (uverts G\<^sub>1)" using wellformed(1) unfolding uwellformed_def by blast ultimately have "card (?g ` uedges G\<^sub>1) = card (uedges G\<^sub>1)" 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: "G\<^sub>1 \ G\<^sub>2 \ G\<^sub>1 \ G\<^sub>2" 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 "G\<^sub>1 \ G\<^sub>2" and "G\<^sub>2 \ G\<^sub>3" shows "G\<^sub>1 \ G\<^sub>3" unfolding subgraph_isomorphic_def proof show "uwellformed G\<^sub>3" using assms unfolding subgraph_isomorphic_def by blast next from assms(2) obtain G\<^sub>2' where "G\<^sub>2 \ G\<^sub>2'" "subgraph G\<^sub>2' G\<^sub>3" unfolding subgraph_isomorphic_def by blast moreover with assms(1) have "G\<^sub>1 \ G\<^sub>2'" by (metis isomorphic_trans) ultimately show "\G''. G\<^sub>1 \ G'' \ subgraph G'' G\<^sub>3" by blast qed lemma subgraph_isomorphic_pre_subgraph_closed: assumes "uwellformed G\<^sub>1" and "subgraph G\<^sub>1 G\<^sub>2" and "G\<^sub>2 \ G\<^sub>3" shows "G\<^sub>1 \ G\<^sub>3" unfolding subgraph_isomorphic_def proof show "uwellformed G\<^sub>3" using assms unfolding subgraph_isomorphic_def by blast next from assms(3) obtain G\<^sub>2' where "G\<^sub>2 \ G\<^sub>2'" "subgraph G\<^sub>2' G\<^sub>3" unfolding subgraph_isomorphic_def by blast then obtain f where bij: "bij_betw f (uverts G\<^sub>2) (uverts G\<^sub>2')" "G\<^sub>2' = map_ugraph f G\<^sub>2" unfolding isomorphism_def by blast let ?G\<^sub>1' = "map_ugraph f G\<^sub>1" have "bij_betw f (uverts G\<^sub>1) (f ` uverts G\<^sub>1)" using bij(1) assms(2) unfolding subgraph_def by (auto intro: bij_betw_subset) moreover hence "uwellformed ?G\<^sub>1'" using map_ugraph_wellformed[OF assms(1)] unfolding bij_betw_def .. ultimately have "G\<^sub>1 \ ?G\<^sub>1'" using assms(1) unfolding isomorphism_def by (metis map_ugraph.simps fst_conv surjective_pairing) moreover have "subgraph ?G\<^sub>1' G\<^sub>3" (* Yes, I will TOTALLY understand that step tomorrow. *) using subgraph_trans[OF map_ugraph_preserves_sub[OF assms(2)]] bij(2) \subgraph G\<^sub>2' G\<^sub>3\ by simp ultimately show "\G''. G\<^sub>1 \ G'' \ subgraph G'' G\<^sub>3" by blast qed lemmas subgraph_isomorphic_pre_closed = subgraph_isomorphic_pre_subgraph_closed subgraph_isomorphic_pre_iso_closed lemma subgraph_isomorphic_trans[trans]: assumes "G\<^sub>1 \ G\<^sub>2" and "G\<^sub>2 \ G\<^sub>3" shows "G\<^sub>1 \ G\<^sub>3" proof - from assms(1) obtain G where "G\<^sub>1 \ G" "subgraph G G\<^sub>2" 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 "G\<^sub>1 \ G\<^sub>2" shows "density G\<^sub>1 = density G\<^sub>2" unfolding density_def using isomorphic_cards[OF assms] by simp lemma isomorphic_max_density: assumes "G\<^sub>1 \ G\<^sub>2" and "nonempty_graph G\<^sub>1" and "nonempty_graph G\<^sub>2" and "finite_graph G\<^sub>1" and "finite_graph G\<^sub>2" shows "max_density G\<^sub>1 = max_density G\<^sub>2" 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) } - note le = this - - show ?thesis - using le[OF assms(2) assms(4) assms(1)] le[OF assms(3) assms(5) isomorphic_sym[OF assms(1)]] - by (fact antisym) + 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" -proof - - have post: "H \ f V" "uverts (f V) = V" - using assms unfolding is_fixed_selector_def by auto - - have "H \ f V" - by (rule isomorphic_is_subgraph_isomorphic) - (simp add: post) - also have "f V \ induced_subgraph V G" - by (rule subgraph_is_subgraph_isomorphic) - (auto simp: induced_wellformed[OF G V] post sub) - also have "\ \ G" - by (rule subgraph_is_subgraph_isomorphic[OF induced_wellformed]) - (auto simp: G V induced_is_subgraph(1)[OF V]) - finally show "H \ G" - . -qed + by (meson G V assms induced_is_subgraph(1) is_fixed_selector_def sub subgraph_isomorphic_def subgraph_trans) end diff --git a/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy --- a/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy +++ b/thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy @@ -1,1563 +1,1539 @@ section\Roth's Theorem on Arithmetic Progressions\ theory Roth_Arithmetic_Progressions imports Szemeredi_Regularity.Szemeredi "Random_Graph_Subgraph_Threshold.Subgraph_Threshold" "Ergodic_Theory.Asymptotic_Density" "HOL-Library.Ramsey" "HOL-Library.Nat_Bijection" begin subsection \Miscellaneous Preliminaries\ lemma sum_prod_le_prod_sum: fixes a :: "'a \ 'b::linordered_idom" assumes "\i. i \ I \ a i \ 0 \ b i \ 0" shows "(\i\I. \j\I. a i * b j) \ (\i\I. a i) * (\i\I. b i)" using assms by (induction I rule: infinite_finite_induct) (auto simp add: algebra_simps sum.distrib sum_distrib_left) lemma real_mult_gt_cube: "A \ (X ::real) \ B \ X \ C \ X \ X \ 0 \ A * B * C \ X^3" by (simp add: mult_mono' power3_eq_cube) lemma triple_sigma_rewrite_card: assumes "finite X" "finite Y" "finite Z" shows "card {(x,y,z) . x \ X \ (y,z) \ Y \ Z \ P x y z} = (\x\ X . card {(y,z) \ Y \ Z. P x y z})" proof - define W where "W \ \x. {(y,z) \ Y \ Z. P x y z}" have "W x \ Y \ Z" for x by (auto simp: W_def) then have [simp]: "finite (W x)" for x by (meson assms finite_SigmaI infinite_super) have eq: "{(x,y,z) . x \ X \ (y,z) \ Y \ Z \ P x y z} = (\x\X. \(y,z)\W x. {(x,y,z)})" by (auto simp: W_def) show ?thesis unfolding eq by (simp add: disjoint_iff assms card_UN_disjoint) (simp add: W_def) qed lemma all_edges_between_mono1: "Y \ Z \ all_edges_between Y X G \ all_edges_between Z X G" by (auto simp: all_edges_between_def) lemma all_edges_between_mono2: "Y \ Z \ all_edges_between X Y G \ all_edges_between X Z G" by (auto simp: all_edges_between_def) lemma uwellformed_alt_fst: assumes "uwellformed G" "{x, y} \ uedges G" shows "x \ uverts G" using uwellformed_def assms by simp lemma uwellformed_alt_snd: assumes "uwellformed G" "{x, y} \ uedges G" shows "y \ uverts G" using uwellformed_def assms by simp lemma all_edges_between_subset_times: "all_edges_between X Y G \ (X \ \(uedges G)) \ (Y \ \(uedges G))" by (auto simp: all_edges_between_def) lemma finite_all_edges_between': assumes "finite (uverts G)" "uwellformed G" shows "finite (all_edges_between X Y G)" proof - have "finite (\(uedges G))" by (meson Pow_iff all_edges_subset_Pow assms finite_Sup subsetD wellformed_all_edges) with all_edges_between_subset_times show ?thesis by (metis finite_Int finite_SigmaI finite_subset) qed -lemma 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 all_edges_between_ss_uedges: "mk_uedge ` (all_edges_between X Y G) \ uedges G" - by (auto simp: all_edges_between_def) - -lemma all_edges_betw_D3: "(x, y) \ all_edges_between X Y G \ {x, y} \ uedges G" - by (simp add: all_edges_between_def) - -lemma all_edges_betw_I: "x \ X \ y \ Y \ {x, y} \ uedges G \ (x, y) \ all_edges_between X Y G" - by (simp add: all_edges_between_def) - lemma all_edges_between_E_diff: "all_edges_between X Y (V,E-E') = all_edges_between X Y (V,E) - all_edges_between X Y (V,E')" by (auto simp: all_edges_between_def) lemma all_edges_between_E_Un: "all_edges_between X Y (V,E\E') = all_edges_between X Y (V,E) \ all_edges_between X Y (V,E')" by (auto simp: all_edges_between_def) lemma all_edges_between_E_UN: "all_edges_between X Y (V, \i\I. E i) = (\i\I. all_edges_between X Y (V,E i))" by (auto simp: all_edges_between_def) lemma all_edges_preserved: "\all_edges_between A B G' = all_edges_between A B G; X \ A; Y \ B\ \ all_edges_between X Y G' = all_edges_between X Y G" by (auto simp: all_edges_between_def) lemma subgraph_edge_wf: assumes "uwellformed G" "uverts H = uverts G" "uedges H \ uedges G" shows "uwellformed H" by (metis assms subsetD uwellformed_def) subsection \Preliminaries on Neighbors in Graphs\ definition neighbor_in_graph:: " uvert \ uvert \ ugraph \ bool" where "neighbor_in_graph x y G \ (x \ (uverts G) \ y \ (uverts G) \ {x,y} \ (uedges G))" definition neighbors :: "uvert \ ugraph \ uvert set" where "neighbors x G \ {y \ uverts G . neighbor_in_graph x y G}" definition neighbors_ss:: "uvert \ uvert set \ ugraph \ uvert set" where "neighbors_ss x Y G \ {y \ Y . neighbor_in_graph x y G}" lemma all_edges_betw_sigma_neighbor: "uwellformed G \ all_edges_between X Y G = (SIGMA x:X. neighbors_ss x Y G)" by (auto simp add: all_edges_between_def neighbors_ss_def neighbor_in_graph_def uwellformed_alt_fst uwellformed_alt_snd) lemma card_all_edges_betw_neighbor: assumes "finite X" "finite Y" "uwellformed G" shows "card (all_edges_between X Y G) = (\x\X. card (neighbors_ss x Y G))" using all_edges_betw_sigma_neighbor assms by (simp add: neighbors_ss_def) subsection \Preliminaries on Triangles in Graphs\ definition triangle_in_graph:: "uvert \ uvert \ uvert \ ugraph \ bool" where "triangle_in_graph x y z G \ ({x,y} \ uedges G) \ ({y,z} \ uedges G) \ ({x,z} \ uedges G)" definition triangle_triples where "triangle_triples X Y Z G \ {(x,y,z) \ X \ Y \ Z. triangle_in_graph x y z G}" lemma triangle_commu1: assumes "triangle_in_graph x y z G" shows "triangle_in_graph y x z G" using assms triangle_in_graph_def by (auto simp add: insert_commute) lemma triangle_vertices_distinct1: assumes wf: "uwellformed G" assumes tri: "triangle_in_graph x y z G" shows "x \ y" proof (rule ccontr) assume a: "\ x \ y" have "card {x, y} = 2" using tri wf triangle_in_graph_def using uwellformed_def by blast thus False using a by simp qed lemma triangle_vertices_distinct2: assumes "uwellformed G" "triangle_in_graph x y z G" shows "y \ z" by (metis assms triangle_vertices_distinct1 triangle_in_graph_def) lemma triangle_in_graph_edge_point: assumes "uwellformed G" shows "triangle_in_graph x y z G \ {y, z} \ uedges G \ neighbor_in_graph x y G \ neighbor_in_graph x z G" by (auto simp add: triangle_in_graph_def neighbor_in_graph_def assms uwellformed_alt_fst uwellformed_alt_snd) definition "unique_triangles G \ \e \ uedges G. \!T. \x y z. T = {x,y,z} \ triangle_in_graph x y z G \ e \ T" definition triangle_free_graph:: "ugraph \ bool" where "triangle_free_graph G \ \(\ x y z. triangle_in_graph x y z G )" lemma triangle_free_graph_empty: "uedges G = {} \ triangle_free_graph G" by (simp add: triangle_free_graph_def triangle_in_graph_def) lemma edge_vertices_not_equal: assumes "uwellformed G" "{x,y} \ uedges G" shows "x \ y" using assms triangle_in_graph_def triangle_vertices_distinct1 by blast lemma triangle_in_graph_verts: assumes "uwellformed G" "triangle_in_graph x y z G" shows "x \ uverts G" "y \ uverts G" "z\ uverts G" proof - have 1: "{x, y} \ uedges G" using triangle_in_graph_def using assms(2) by auto then show "x \ uverts G" using uwellformed_alt_fst assms by blast then show "y \ uverts G" using 1 uwellformed_alt_snd assms by blast have "{x, z} \ uedges G" using triangle_in_graph_def assms(2) by auto then show "z \ uverts G" using uwellformed_alt_snd assms by blast qed definition triangle_set :: "ugraph \ uvert set set" where "triangle_set G \ { {x,y,z} | x y z. triangle_in_graph x y z G}" fun mk_triangle_set :: "(uvert \ uvert \ uvert) \ uvert set" where "mk_triangle_set (x,y,z) = {x,y,z}" lemma finite_triangle_set: assumes fin: "finite (uverts G)" and wf: "uwellformed G" shows "finite (triangle_set G)" proof - have "triangle_set G \ Pow (uverts G)" using PowI local.wf triangle_in_graph_def triangle_set_def uwellformed_def by auto then show ?thesis by (meson fin finite_Pow_iff infinite_super) qed lemma card_triangle_3: assumes "t \ triangle_set G" "uwellformed G" shows "card t = 3" using assms by (auto simp: triangle_set_def edge_vertices_not_equal triangle_in_graph_def) lemma triangle_set_power_set_ss: "uwellformed G \ triangle_set G \ Pow (uverts G)" by (auto simp add: triangle_set_def triangle_in_graph_def uwellformed_alt_fst uwellformed_alt_snd) lemma triangle_in_graph_ss: assumes "uedges Gnew \ uedges G" assumes "triangle_in_graph x y z Gnew" shows "triangle_in_graph x y z G" using assms triangle_in_graph_def by auto lemma triangle_set_graph_edge_ss: assumes "uedges Gnew \ uedges G" assumes "uverts Gnew = uverts G" shows "triangle_set Gnew \ triangle_set G" using assms unfolding triangle_set_def by (blast intro: triangle_in_graph_ss) lemma triangle_set_graph_edge_ss_bound: fixes G :: "ugraph" and Gnew :: "ugraph" assumes "uwellformed G" "finite (uverts G)" "uedges Gnew \ uedges G" "uverts Gnew = uverts G" shows "card (triangle_set G) \ card (triangle_set Gnew)" by (simp add: assms card_mono finite_triangle_set triangle_set_graph_edge_ss) subsection \The Triangle Counting Lemma and the Triangle Removal Lemma\ text\We begin with some more auxiliary material to be used in the main lemmas.\ lemma regular_pair_neighbor_bound: fixes \::real assumes finG: "finite (uverts G)" assumes xss: "X \ uverts G" and yss: "Y \ uverts G" and "card X > 0" and wf: "uwellformed G" and eg0: "\ > 0" and "regular_pair X Y G \" and ed: "edge_density X Y G \ 2*\" defines "X' \ {x \ X. card (neighbors_ss x Y G) < (edge_density X Y G - \) * card (Y)}" shows "card X' < \ * card X" (is "card (?X') < \ * _") proof (cases "?X' = {}") case False \\Following Gowers's proof - more in depth with reasoning on contradiction\ let ?rxy = "1/(card X' * card Y)" show ?thesis proof (rule ccontr) assume "\ (card (X') < \ * card X) " then have a: "(card(X') \ \ * card X) " by simp have fin: "finite X" "finite Y" using assms finite_subset by auto have ebound: "\ \ 1/2" by (metis ed edge_density_le1 le_divide_eq_numeral1(1) mult.commute order_trans) have finx: "finite X'" using fin X'_def by simp have "\ x. x \ X'\ (card (neighbors_ss x Y G)) < (edge_density X Y G - \) * (card Y)" unfolding X'_def by blast then have "(\x\X'. card (neighbors_ss x Y G)) < (\x\X'. ((edge_density X Y G - \) * (card Y)))" using False sum_strict_mono X'_def by (smt (verit, del_insts) finx of_nat_sum) then have upper: "(\x\X'. card (neighbors_ss x Y G)) < (card X') * ((edge_density X Y G - \) * (card Y))" by (simp add: sum_bounded_above) have yge0: "card Y > 0" by (metis gr0I mult_eq_0_iff of_nat_0 of_nat_less_0_iff upper) have "?rxy > 0" using card_0_eq finx False yge0 X'_def by fastforce then have upper2: "?rxy * (\x\X'. card (neighbors_ss x Y G)) < ?rxy * (card X') * ((edge_density X Y G - \) * (card Y))" by (smt (verit) mult.assoc mult_le_cancel_left upper) have "?rxy * (card X') * ((edge_density X Y G - \) * (card Y)) = edge_density X Y G - \" using False X'_def finx by force with \\ > 0\ upper2 have con: "edge_density X Y G - ?rxy * (\x\X'. card (neighbors_ss x Y G)) > \" by linarith have "\edge_density X Y G - ?rxy * (\x\X'. card (neighbors_ss x Y G))\ = \?rxy * (card (all_edges_between X' Y G)) - edge_density X Y G\" using card_all_edges_betw_neighbor fin wf by (simp add: X'_def) also have "... = \edge_density X' Y G - edge_density X Y G\" by (simp add: edge_density_def) also have "... \ \" using assms ebound yge0 a by (force simp add: X'_def regular_pair_def) finally show False using con by linarith qed qed (simp add: \card X > 0\ eg0) lemma neighbor_set_meets_e_reg_cond: fixes \::real assumes "edge_density X Y G \ 2*\" and "card (neighbors_ss x Y G) \ (edge_density X Y G - \) * card Y" shows "card (neighbors_ss x Y G) \ \ * card (Y)" by (smt (verit) assms mult_right_mono of_nat_0_le_iff) lemma all_edges_btwn_neighbour_sets_lower_bound: fixes \::real assumes rp2: "regular_pair Y Z G \" and ed1: "edge_density X Y G \ 2*\" and ed2: "edge_density X Z G \ 2*\" and cond1: "card (neighbors_ss x Y G) \ (edge_density X Y G - \) * card Y" and cond2: "card (neighbors_ss x Z G) \ (edge_density X Z G - \) * card Z" shows "card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G) \ (edge_density Y Z G - \) * card (neighbors_ss x Y G) * card (neighbors_ss x Z G)" (is "card (all_edges_between ?Y' ?Z' G) \ (edge_density Y Z G - \) * card ?Y' * card ?Z'") proof - have yss': "?Y' \ Y" using neighbors_ss_def by simp have zss': "?Z' \ Z" using neighbors_ss_def by simp have min_sizeY: "card ?Y' \ \ * card Y" using cond1 ed1 neighbor_set_meets_e_reg_cond by blast have min_sizeZ: "card ?Z' \ \ * card Z" using cond2 ed2 neighbor_set_meets_e_reg_cond by blast then have "\ edge_density ?Y' ?Z' G - edge_density Y Z G \ \ \" using min_sizeY yss' zss' assms by (force simp add: regular_pair_def) then have "edge_density Y Z G - \ \ (card (all_edges_between ?Y' ?Z' G)/(card ?Y' * card ?Z'))" using edge_density_def by simp then have "(card ?Y' * card ?Z') * (edge_density Y Z G - \) \ (card (all_edges_between ?Y' ?Z' G))" by (metis abs_of_nat division_ring_divide_zero le_divide_eq mult_of_nat_commute of_nat_0_le_iff times_divide_eq_right zero_less_abs_iff) then show ?thesis by (metis (no_types, lifting) ab_semigroup_mult_class.mult_ac(1) mult_of_nat_commute of_nat_mult) qed text\We are now ready to show the Triangle Counting Lemma:\ theorem triangle_counting_lemma: fixes \::real assumes xss: "X \ uverts G" and yss: "Y \ uverts G" and zss: "Z \ uverts G" and en0: "\ > 0" and finG: "finite (uverts G)" and wf: "uwellformed G" and rp1: "regular_pair X Y G \" and rp2: "regular_pair Y Z G \" and rp3: "regular_pair X Z G \" and ed1: "edge_density X Y G \ 2*\" and ed2: "edge_density X Z G \ 2*\" and ed3: "edge_density Y Z G \ 2*\" shows "card (triangle_triples X Y Z G) \ (1-2*\) * (edge_density X Y G - \) * (edge_density X Z G - \) * (edge_density Y Z G - \)* card X * card Y * card Z" proof - let ?T_all = "{(x,y,z) \ X \ Y \ Z. (triangle_in_graph x y z G)}" let ?ediff = "\X Y. edge_density X Y G - \" define XF where "XF \ \Y. {x \ X. card(neighbors_ss x Y G) < ?ediff X Y * card Y}" have fin: "finite X" "finite Y" "finite Z" using finG rev_finite_subset xss yss zss by auto then have "card X > 0" using card_0_eq ed1 edge_density_def en0 by fastforce text\ Obtain a subset of @{term X} where all elements meet minimum numbers for neighborhood size in @{term Y} and @{term Z}.\ define X2 where "X2 \ X - (XF Y \ XF Z)" have xss: "X2 \ X" and finx2: "finite X2" by (auto simp add: X2_def fin) text \Reasoning on the minimum size of @{term X2}:\ have part1: "(XF Y \ XF Z) \ X2 = X" by (auto simp: XF_def X2_def) have card_XFY: "card (XF Y) < \ * card X" using regular_pair_neighbor_bound assms \card X > 0\ by (simp add: XF_def) text\ We now repeat the same argument as above to the regular pair @{term X} @{term Z} in @{term G}.\ have card_XFZ: "card (XF Z) < \ * card X" using regular_pair_neighbor_bound assms \card X > 0\ by (simp add: XF_def) have "card (XF Y \ XF Z) \ 2 * \ * (card X)" by (smt (verit) card_XFY card_XFZ card_Un_le comm_semiring_class.distrib of_nat_add of_nat_mono) then have "card X2 \ card X - 2 * \ * card X" using part1 by (smt (verit, del_insts) card_Un_le of_nat_add of_nat_mono) then have minx2: "card X2 \ (1 - 2 * \) * card X" by (metis mult.commute mult_cancel_left2 right_diff_distrib) text \Reasoning on the minimum number of edges between neighborhoods of @{term X} in @{term Y} and @{term Z}.\ have edyzgt0: "?ediff Y Z > 0" and edxygt0: "?ediff X Y > 0" using ed1 ed3 \\ > 0\ by linarith+ have card_y_bound: "card (neighbors_ss x Y G) \ ?ediff X Y * card Y" and card_z_bound: "card (neighbors_ss x Z G) \ ?ediff X Z * card Z" if "x \ X2" for x using that by (auto simp: XF_def X2_def) have card_y_bound': "(\x\ X2. ?ediff Y Z * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) \ (\x\ X2. ?ediff Y Z * ?ediff X Y * (card Y) * (card (neighbors_ss x Z G)))" by (rule sum_mono) (smt (verit, best) mult.left_commute card_y_bound edyzgt0 mult.commute mult_right_mono of_nat_0_le_iff) have card_z_bound': "(\x\ X2. ?ediff Y Z * ?ediff X Y * (card Y) * (card (neighbors_ss x Z G))) \ (\x\ X2. ?ediff Y Z * ?ediff X Y * (card Y) * ?ediff X Z * (card Z))" using card_z_bound mult_left_mono edxygt0 edyzgt0 by (fastforce intro!: sum_mono) have eq_set: "\x. {(y,z). y \ Y \ z \ Z \ {y, z} \ uedges G \ neighbor_in_graph x y G \ neighbor_in_graph x z G } = {(y,z). y \ (neighbors_ss x Y G) \ z \ (neighbors_ss x Z G) \ {y, z} \ uedges G }" by (auto simp: neighbors_ss_def) have "card ?T_all = (\x\ X . card {(y,z) \ Y \ Z. triangle_in_graph x y z G})" using triple_sigma_rewrite_card fin by force also have "\ = (\x\ X . card {(y,z). y \ Y \ z \ Z \ {y, z} \ uedges G \ neighbor_in_graph x y G \ neighbor_in_graph x z G })" using triangle_in_graph_edge_point assms by auto also have "... = (\x \ X. card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))" using all_edges_between_def eq_set by presburger finally have l: "card ?T_all \ (\x\ X2 . card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G))" by (simp add: fin xss sum_mono2) have "(\x\ X2. ?ediff Y Z * (card (neighbors_ss x Y G)) * (card (neighbors_ss x Z G))) \ (\x\ X2. real (card (all_edges_between (neighbors_ss x Y G) (neighbors_ss x Z G) G)))" (is "sum ?F _ \ sum ?G _") proof (rule sum_mono) show "\x. x \ X2 \ ?F x \ ?G x" using all_edges_btwn_neighbour_sets_lower_bound card_y_bound card_z_bound ed1 ed2 rp2 by blast qed then have "card ?T_all \ card X2 * ?ediff Y Z * ?ediff X Y * card Y * ?ediff X Z * card Z" using card_z_bound' card_y_bound' l of_nat_le_iff [symmetric, where 'a=real] by force then have "real (card ?T_all) \ ((1 - 2 * \) * card X) * ?ediff Y Z * ?ediff X Y * (card Y) * ?ediff X Z * (card Z)" by (smt (verit, best) ed2 edxygt0 edyzgt0 en0 minx2 mult_right_mono of_nat_0_le_iff) then show ?thesis by (simp add: triangle_triples_def mult.commute mult.left_commute) qed definition regular_graph :: "uvert set set \ ugraph \ real \ bool" where "regular_graph P G \ \ \R S. R\P \ S\P \ regular_pair R S G \" for \::real text \A minimum density, but empty edge sets are excluded.\ definition edge_dense :: "nat set \ nat set \ ugraph \ real \ bool" where "edge_dense X Y G \ \ all_edges_between X Y G = {} \ edge_density X Y G \ \" definition dense_graph :: "uvert set set \ ugraph \ real \ bool" where "dense_graph P G \ \ \R S. R\P \ S\P \ edge_dense R S G \" for \::real definition decent :: "nat set \ nat set \ ugraph \ real \ bool" where "decent X Y G \ \ all_edges_between X Y G = {} \ (card X \ \ \ card Y \ \)" for \::real definition decent_graph :: "uvert set set \ ugraph \ real \ bool" where "decent_graph P G \ \ \R S. R\P \ S\P \ decent R S G \" text \The proof of the triangle counting lemma requires ordered triples. For each unordered triple there are six permutations, hence the factor of $1/6$ here.\ lemma card_convert_triangle_rep: fixes G :: "ugraph" assumes "X \ uverts G" and "Y \ uverts G" and "Z \ uverts G" and fin: "finite (uverts G)" and wf: "uwellformed G" shows "card (triangle_set G) \ 1/6 * card {(x,y,z) \ X \ Y \ Z . (triangle_in_graph x y z G)}" (is "_ \ 1/6 * card ?TT") proof - define tofl where "tofl \ \l::nat list. (hd l, hd(tl l), hd(tl(tl l)))" have in_tofl: "(x,y,z) \ tofl ` permutations_of_set {x,y,z}" if "x\y" "y\z" "x\z" for x y z proof - have "distinct[x,y,z]" using that by simp then show ?thesis unfolding tofl_def image_iff by (smt (verit, best) list.sel(1) list.sel(3) list.simps(15) permutations_of_setI set_empty) qed have "?TT \ {(x,y,z). (triangle_in_graph x y z G)}" by auto also have "\ \ (\t \ triangle_set G. tofl ` permutations_of_set t)" using edge_vertices_not_equal [OF wf] in_tofl by (clarsimp simp add: triangle_set_def triangle_in_graph_def) metis finally have "?TT \ (\t \ triangle_set G. tofl ` permutations_of_set t)" . then have "card ?TT \ card(\t \ triangle_set G. tofl ` permutations_of_set t)" by (intro card_mono finite_UN_I finite_triangle_set) (auto simp: assms) also have "\ \ (\t \ triangle_set G. card (tofl ` permutations_of_set t))" using card_UN_le fin finite_triangle_set local.wf by blast also have "\ \ (\t \ triangle_set G. card (permutations_of_set t))" by (meson card_image_le finite_permutations_of_set sum_mono) also have "\ \ (\t \ triangle_set G. fact 3)" by (rule sum_mono) (metis card.infinite card_permutations_of_set card_triangle_3 eq_refl local.wf nat.case numeral_3_eq_3) also have "\ = 6 * card (triangle_set G)" by (simp add: eval_nat_numeral) finally have "card ?TT \ 6 * card (triangle_set G)" . then show ?thesis by (simp add: divide_simps) qed lemma card_convert_triangle_rep_bound: fixes G :: "ugraph" and t :: real assumes "X \ uverts G" and "Y \ uverts G" and "Z \ uverts G" and fin: "finite (uverts G)" and wf: "uwellformed G" assumes "card {(x,y,z) \ X \ Y \ Z . (triangle_in_graph x y z G)} \ t" shows "card (triangle_set G) \ 1/6 *t" proof - define t' where "t' \ card {(x,y,z) \ X \ Y \ Z . (triangle_in_graph x y z G)}" have "t' \ t" using assms t'_def by simp then have tgt: "1/6 * t' \ 1/6 * t" by simp have "card (triangle_set G) \ 1/6 *t'" using t'_def card_convert_triangle_rep assms by simp thus ?thesis using tgt by linarith qed lemma edge_density_eq0: assumes "all_edges_between A B G = {}" and "X \ A" "Y \ B" shows "edge_density X Y G = 0" proof - have "all_edges_between X Y G = {}" by (metis all_edges_between_mono1 all_edges_between_mono2 assms subset_empty) then show ?thesis by (auto simp: edge_density_def) qed text\The following is the Triangle Removal Lemma.\ theorem triangle_removal_lemma: fixes \ :: real assumes egt: "\ > 0" shows "\\::real > 0. \G. card(uverts G) > 0 \ uwellformed G \ card (triangle_set G) \ \ * card(uverts G) ^ 3 \ (\G'. triangle_free_graph G' \ uverts G' = uverts G \ uedges G' \ uedges G \ card (uedges G - uedges G') \ \ * (card (uverts G))\<^sup>2)" (is "\\::real > 0. \G. _ \ _ \ _ \ (\Gnew. ?\ G Gnew)") proof (cases "\ < 1") case False show ?thesis proof (intro exI conjI strip) fix G define Gnew where "Gnew \ ((uverts G), {}::uedge set)" assume G: "uwellformed G" "card(uverts G) > 0" then show "triangle_free_graph Gnew" "uverts Gnew = uverts G" "uedges Gnew \ uedges G" by (auto simp: Gnew_def triangle_free_graph_empty) have "real (card (uedges G)) \ (card (uverts G))\<^sup>2" by (meson G card_gt_0_iff max_edges_graph of_nat_le_iff) also have "\ \ \ * (card (uverts G))\<^sup>2" using False mult_le_cancel_right1 by fastforce finally show "real (card (uedges G - uedges Gnew)) \ \ * ((card (uverts G))\<^sup>2)" by (simp add: Gnew_def) qed (rule zero_less_one) next case True have e4gt: "\/4 > 0" using \\ > 0\ by auto then obtain M0 where M0: "\G. card (uverts G) > 0 \ \P. regular_partition (\/4) G P \ card P \ M0" and "M0>0" by (metis Szemeredi_Regularity_Lemma le0 neq0_conv not_le not_numeral_le_zero) define D0 where "D0 \ 1/6 *(1-(\/2))*((\/4)^3)*((\ /(4*M0))^3)" have "D0 > 0" using \0 < \\ \\ < 1\ \M0 > 0\ by (simp add: D0_def zero_less_mult_iff) then obtain \:: "real" where \: "0 < \" "\ < D0" by (meson dense) show ?thesis proof (rule exI, intro conjI strip) fix G assume "card(uverts G) > 0" and wf: "uwellformed G" then have fin: "finite (uverts G)" by (simp add: card_gt_0_iff) text\Assume that, for a yet to be determined $\delta$, we have:\ assume ineq: "real (card (triangle_set G)) \ \ * card (uverts G) ^ 3" text\Step 1: Partition: Using Szemer\'{e}di's Regularity Lemma, we get an $\epsilon/4$ partition. \ let ?n = "card (uverts G)" have vne: "uverts G \ {}" using \0 < card (uverts G)\ by force then have ngt0: "?n > 0" by (simp add: fin card_gt_0_iff) with M0 obtain P where M: "regular_partition (\/4) G P" and "card P \ M0" by blast define M where "M \ card P" have "finite P" by (meson M fin finite_elements regular_partition_def) with M0 have "M > 0" unfolding M_def by (metis M card_gt_0_iff partition_onD1 partition_on_empty regular_partition_def vne) let ?e4M = "\ / (4 * real M)" define D where "D \ 1/6 *(1-(\/2)) * ((\/4)^3) * ?e4M^3" have "D > 0" using \0 < \\ \\ < 1\ \M > 0\ by (simp add: D_def zero_less_mult_iff) have "D0 \ D" unfolding D0_def D_def using \0 < \\ \\ < 1\ \card P \ M0\ \M > 0\ by (intro mult_mono) (auto simp: frac_le M_def) have fin_part: "finite_graph_partition (uverts G) P M" using M unfolding regular_partition_def finite_graph_partition_def by (metis M_def \0 < M\ card_gt_0_iff) then have fin_P: "finite R" and card_P_gt0: "card R > 0" if "R\P" for R using fin finite_graph_partition_finite finite_graph_partition_gt0 that by auto have card_P_le: "card R \ ?n" if "R\P" for R by (meson card_mono fin fin_part finite_graph_partition_subset that) have P_disjnt: "\R S. \R \ S; R \ P; S \ P\ \ R \ S = {}" using fin_part by (metis disjnt_def finite_graph_partition_def insert_absorb pairwise_insert partition_on_def) have sum_card_P: "(\R\P. card R) = ?n" using card_finite_graph_partition fin fin_part by meson text\Step 2. Cleaning. For each ordered pair of parts $(P_i,P_j)$, remove all edges between $P_i$ and $P_j$ if (a) it is an irregular pair, (b) its edge density ${} < \epsilon/2$, (c) either $P_i$ or $P_j$ is small (${}\le(\epsilon/4M)n$) Process (a) removes at most $(\epsilon/4)n^2$ edges. Process (b) removes at most $(\epsilon/2)n^2$ edges. Process (c) removes at most $(\epsilon/4)n^2$ edges. The remaining graph is triangle-free for some choice of $\delta$. \ define edge where "edge \ \R S. mk_uedge ` (all_edges_between R S G)" have edge_commute: "edge R S = edge S R" for R S by (force simp add: edge_def all_edges_between_swap [of S] split: prod.split) have card_edge_le_card: "card (edge R S) \ card (all_edges_between R S G)" for R S by (simp add: card_image_le edge_def fin finite_all_edges_between' local.wf) have card_edge_le: "card (edge R S) \ card R * card S" if "R\P" "S\P" for R S by (meson card_edge_le_card fin_P le_trans max_all_edges_between that) text \Obtain the set of edges meeting condition (a).\ define irreg_pairs where "irreg_pairs \ {(R,S). R \ P \ S \ P \ \ regular_pair R S G (\/4)}" define Ea where "Ea \ (\(R,S) \ irreg_pairs. edge R S)" text \Obtain the set of edges meeting condition (b).\ define low_density_pairs where "low_density_pairs \ {(R,S). R \ P \ S \ P \ \ edge_dense R S G (\/2)}" define Eb where "Eb \ (\(i,j) \ low_density_pairs. edge i j)" text \Obtain the set of edges meeting condition (c).\ define small where "small \ \R. R \ P \ card R \ ?e4M * ?n" let ?SMALL = "Collect small" define small_pairs where "small_pairs \ {(R,S). R \ P \ S \ P \ (small R \ small S)}" define Ec where "Ec \ (\R \ ?SMALL. \S \ P. edge R S)" have Ec_def': "Ec = (\(i,j) \ small_pairs. edge i j)" by (force simp: edge_commute small_pairs_def small_def Ec_def) have eabound: "card Ea \ (\/4) * ?n^2" \\Count the edge bound for @{term Ea}\ proof - have \
: "\R S. \R \ P; S \ P\ \ card (edge R S) \ card R * card S" unfolding edge_def by (meson card_image_le fin_P finite_all_edges_between max_all_edges_between order_trans) have "irreg_pairs \ P \ P" by (auto simp: irreg_pairs_def) then have "finite irreg_pairs" by (meson \finite P\ finite_SigmaI finite_subset) have "card Ea \ (\(R,S)\irreg_pairs. card (edge R S))" by (simp add: Ea_def card_UN_le [OF \finite irreg_pairs\] case_prod_unfold) also have "\ \ (\(R,S) \ {(R,S). R\P \ S\P \ \ regular_pair R S G (\/4)}. card R * card S)" unfolding irreg_pairs_def using \
by (force intro: sum_mono) also have "\ = (\(R,S) \ irregular_set (\/4) G P. card R * card S)" by (simp add: irregular_set_def) finally have "card Ea \ (\(R,S) \ irregular_set (\/4) G P. card R * card S)" . with M show ?thesis unfolding regular_partition_def by linarith qed have ebbound: "card Eb \ (\/2) * (?n^2)" \\Count the edge bound for @{term Eb}.\ proof - have \
: "\R S. \R \ P; S \ P; \ edge_dense R S G (\ / 2)\ \ real (card (edge R S)) * 2 \ \ * real (card R) * real (card S)" by (simp add: divide_simps edge_dense_def edge_density_def card_P_gt0) (smt (verit, best) card_edge_le_card of_nat_le_iff mult.assoc) have subs: "low_density_pairs \ P \ P" by (auto simp: low_density_pairs_def) then have "finite low_density_pairs" by (metis \finite P\ finite_SigmaI finite_subset) have "real (card Eb) \ (\(i,j)\low_density_pairs. real (card (edge i j)))" unfolding Eb_def by (smt (verit, ccfv_SIG) \finite low_density_pairs\ card_UN_le of_nat_mono of_nat_sum case_prod_unfold sum_mono) also have "\ \ (\(R,S)\low_density_pairs. \/2 * card R * card S)" unfolding low_density_pairs_def by (force intro: sum_mono \
) also have "\ \ (\(R,S)\P \ P. \/2 * card R * card S)" using subs \\ > 0\ by (intro sum_mono2) (auto simp: \finite P\) also have "\ = \/2 * (\(R,S)\P \ P. card R * card S)" by (simp add: sum_distrib_left case_prod_unfold mult_ac) also have "\ \ (\/2) * (?n^2)" using \\>0\ sum_prod_le_prod_sum by (simp add: power2_eq_square sum_product flip: sum.cartesian_product sum_card_P) finally show ?thesis . qed have ecbound: "card Ec \ (\/4) * (?n^2)" \\Count the edge bound for @{term Ec}.\ proof - have edge_bound: "(card (edge R S)) \ ?e4M * ?n^2" if "S \ P" "small R" for R S proof - have "real (card R) \ \ * ?n / (4 * real M)" using that by (simp add: small_def) with card_P_le [OF \S\P\] have *: "real (card R) * real (card S) \ \ * card (uverts G) / (4 * real M) * ?n" by (meson mult_mono of_nat_0_le_iff of_nat_mono order.trans) also have "\ = ?e4M * ?n^2" by (simp add: power2_eq_square) finally show ?thesis by (smt (verit) card_edge_le of_nat_mono of_nat_mult small_def that) qed have subs: "?SMALL \ P" by (auto simp: small_def) then obtain card_sp: "card (?SMALL) \ M" and "finite ?SMALL" using M_def \finite P\ card_mono by (metis finite_subset) have "real (card Ec) \ (\R \ ?SMALL. real (card (\S \ P. edge R S)))" unfolding Ec_def by (smt (verit, ccfv_SIG) \finite ?SMALL\ card_UN_le of_nat_mono of_nat_sum case_prod_unfold sum_mono) also have "\ \ (\R \ ?SMALL. ?e4M * ?n^2)" proof (intro sum_mono) fix R assume i: "R \ Collect small" then have "R\P" and card_Pi: "card R \ ?e4M * ?n" by (auto simp: small_def) let ?UE = "\(edge R ` (P))" have *: "real (card ?UE) \ real (card R * ?n)" proof - have "?UE \ mk_uedge ` (all_edges_between R (uverts G) G)" apply (simp add: edge_def UN_subset_iff Ball_def) by (meson all_edges_between_mono2 fin_part finite_graph_partition_subset image_mono) then have "card ?UE \ card (all_edges_between R (uverts G) G)" by (meson card_image_le card_mono fin finite_all_edges_between' finite_imageI wf le_trans) then show ?thesis by (meson of_nat_mono fin fin_P max_all_edges_between order.trans \R\P\) qed also have "\ \ ?e4M * real (?n\<^sup>2)" using card_Pi \M > 0\ \?n > 0\ by (force simp add: divide_simps power2_eq_square) finally show "real (card ?UE) \ ?e4M * real (?n\<^sup>2)" . qed also have "\ \ card ?SMALL * (?e4M * ?n^2)" by simp also have "\ \ M * (?e4M * ?n^2)" using egt by (intro mult_right_mono) (auto simp add: card_sp) also have "\ \ (\/4) * (?n^2)" using \M > 0\ by simp finally show ?thesis . qed \\total count\ have prev1: "card (Ea \ Eb \ Ec) \ card (Ea \ Eb) + card Ec" by (simp add: card_Un_le) also have "\ \ card Ea + card Eb + card Ec" by (simp add: card_Un_le) also have prev: "\ \ (\/4)*(?n^2) + (\/2)*(?n^2) + (\/4)*(?n^2)" using eabound ebbound ecbound by linarith finally have cutedgesbound: "card (Ea \ Eb \ Ec) \ \ * (?n^2)" by simp define Gnew where "Gnew \ (uverts G, uedges G - (Ea \ Eb \ Ec))" show "\Gnew. ?\ G Gnew" proof (intro exI conjI) show verts: "uverts Gnew = uverts G" by (simp add: Gnew_def) - have allij: "\R S. edge R S \ uedges G" - using all_edges_between_ss_uedges edge_def by presburger - then have eae: "Ea \ uedges G" by (auto simp: Ea_def) - have eab: "Eb \ uedges G" using allij by (auto simp: Eb_def) - have "Ec \ uedges G" using allij by (auto simp: Ec_def) - then have diffedges: "(Ea \ Eb \ Ec) \ uedges G" - using eae eab by auto + have diffedges: "(Ea \ Eb \ Ec) \ uedges G" + by (auto simp: Ea_def Eb_def Ec_def all_edges_between_def edge_def) then show edges: "uedges Gnew \ uedges G" by (simp add: Gnew_def) then have "uedges G - (uedges Gnew) = uedges G \ (Ea \ Eb \ Ec) " by (simp add: Gnew_def Diff_Diff_Int) then have "uedges G - (uedges Gnew) = (Ea \ Eb \ Ec)" using diffedges by (simp add: Int_absorb1) then have cardbound: "card (uedges G - uedges Gnew) \ \ * (?n^2)" using cutedgesbound by simp have graph_partition_new: "finite_graph_partition (uverts Gnew) P M" using verts by (simp add: fin_part) have new_wf: "uwellformed Gnew" using subgraph_edge_wf verts edges wf by simp have new_fin: "finite (uverts Gnew)" using verts fin by simp text\ The notes by Bell and Grodzicki are quite useful for understanding the lines below. See pg 4 in the middle after the summary of the min edge counts.\ have irreg_pairs_swap: "(R,S) \ irreg_pairs \ (S, R) \ irreg_pairs" for R S by (auto simp: irreg_pairs_def regular_pair_commute) have low_density_pairs_swap: "(R,S) \ low_density_pairs \ (S,R) \ low_density_pairs" for R S by (simp add: low_density_pairs_def edge_density_commute edge_dense_def) (use all_edges_between_swap in blast) have small_pairs_swap: "(R,S) \ small_pairs \ (S,R) \ small_pairs" for R S by (auto simp: small_pairs_def) have all_edges_if: "all_edges_between R S Gnew = (if (R,S) \ irreg_pairs \ low_density_pairs \ small_pairs then {} else all_edges_between R S G)" (is "?lhs = ?rhs") if ij: "R \ P" "S \ P" for R S proof show "?lhs \ ?rhs" using that fin_part unfolding Gnew_def Ea_def Eb_def Ec_def' apply (simp add: all_edges_between_E_diff all_edges_between_E_Un all_edges_between_E_UN) apply (auto simp: edge_def in_mk_uedge_img_iff all_edges_between_def) done next have Ea: "all_edges_between R S (V, Ea) = {}" if "(R,S) \ irreg_pairs" for V using ij that P_disjnt by (auto simp: Ea_def doubleton_eq_iff edge_def all_edges_between_def irreg_pairs_def; metis regular_pair_commute disjoint_iff_not_equal) have Eb: "all_edges_between R S (V, Eb) = {}" if "(R,S) \ low_density_pairs" for V using ij that apply (auto simp: Eb_def edge_def all_edges_between_def low_density_pairs_def edge_dense_def) apply metis by (metis IntI P_disjnt doubleton_eq_iff edge_density_commute equals0D) have Ec: "all_edges_between R S (V, Ec) = {}" if "(R,S) \ small_pairs" for V using ij that by (auto simp: Ec_def' doubleton_eq_iff edge_def all_edges_between_def small_pairs_def; metis P_disjnt disjoint_iff) show "?rhs \ ?lhs" by (auto simp add: Gnew_def Ea Eb Ec all_edges_between_E_diff all_edges_between_E_Un) qed have rp: "regular_pair R S Gnew (\/4)" if ij: "R \ P" "S \ P" for R S proof (cases "(R,S) \ irreg_pairs") case False have ed: "edge_density X Y Gnew = (if (R,S) \ irreg_pairs \ low_density_pairs \ small_pairs then 0 else edge_density X Y G)" if "X \ R" "Y \ S" for X Y using all_edges_if that ij False by (smt (verit) all_edges_preserved edge_density_eq0 edge_density_def) show ?thesis using that False \\ > 0\ by (auto simp add: irreg_pairs_def regular_pair_def less_le ed) next case True then have ed: "edge_density X Y Gnew = 0" if "X \ R" "Y \ S" for X Y by (meson edge_density_eq0 all_edges_if that \R \ P\ \S \ P\ UnCI) with egt that show ?thesis by (auto simp: regular_pair_def ed) qed then have reg_pairs: "regular_graph P Gnew (\/4)" by (meson regular_graph_def) have "edge_dense R S Gnew (\/2)" if "R \ P" "S \ P" for R S proof (cases "(R,S) \ low_density_pairs") case False have ed: "edge_density R S Gnew = (if (R,S) \ irreg_pairs \ low_density_pairs \ small_pairs then 0 else edge_density R S G)" using all_edges_if that that by (simp add: edge_density_def) with that \\ > 0\ False show ?thesis by (auto simp: low_density_pairs_def edge_dense_def all_edges_if) next case True then have "edge_density R S Gnew = 0" by (simp add: all_edges_if edge_density_def that) with \\ > 0\ that show ?thesis by (simp add: True all_edges_if edge_dense_def) qed then have density_bound: "dense_graph P Gnew (\/2)" by (meson dense_graph_def) have min_subset_size: "decent_graph P Gnew (?e4M * ?n)" using \\ > 0\ by (auto simp: decent_graph_def small_pairs_def small_def decent_def all_edges_if) show "triangle_free_graph Gnew" proof (rule ccontr) assume non: "\?thesis" then obtain x y z where trig_ex: "triangle_in_graph x y z Gnew" using triangle_free_graph_def non by auto then have xin: "x \ (uverts Gnew)" and yin: "y \ (uverts Gnew)" and zin: "z \ (uverts Gnew)" using triangle_in_graph_verts new_wf by auto then obtain R S T where xinp: "x \ R" and ilt: "R\P" and yinp: "y \ S" and jlt: "S\P" and zinp: "z \ T" and klt: "T\P" by (metis graph_partition_new xin Union_iff finite_graph_partition_equals) then have finitesubsets: "finite R" "finite S" "finite T" using new_fin fin_part finite_graph_partition_finite fin by auto have subsets: "R \ uverts Gnew" "S \ uverts Gnew" "T \ uverts Gnew" using finite_graph_partition_subset ilt jlt klt graph_partition_new by auto have min_sizes: "card R \ ?e4M*?n" "card S \ ?e4M*?n" "card T \ ?e4M*?n" using trig_ex min_subset_size xinp yinp zinp ilt jlt klt by (auto simp: triangle_in_graph_def decent_graph_def decent_def all_edges_between_def) have min_dens: "edge_density R S Gnew \ \/2" "edge_density R T Gnew \ \/2" "edge_density S T Gnew \ \/2" - using density_bound subsets ilt jlt klt xinp yinp zinp unfolding dense_graph_def edge_dense_def - by (metis all_edges_betw_I equals0D triangle_in_graph_def trig_ex)+ + using density_bound ilt jlt klt xinp yinp zinp trig_ex + by (auto simp: dense_graph_def edge_dense_def all_edges_between_def triangle_in_graph_def) then have min_dens_diff: "edge_density R S Gnew - \/4 \ \/4" "edge_density R T Gnew - \/4 \ \/4" "edge_density S T Gnew - \/4 \ \/4" by auto have mincard0: "(card R) * (card S) * (card T) \ 0" by simp have gtcube: "((edge_density R S Gnew) - \/4)*((edge_density R T Gnew) - \/4) *((edge_density S T Gnew) - \/4) \ (\/4)^3" using min_dens_diff e4gt real_mult_gt_cube by auto then have c1: "((edge_density R S Gnew) - \/4)*((edge_density R T Gnew) - \/4) *((edge_density S T Gnew) - \/4) \ 0" by (smt (verit) e4gt zero_less_power) have "?e4M * ?n \ 0" using egt by force then have "card R * card S * card T \ (?e4M * ?n)^3" by (metis min_sizes of_nat_mult real_mult_gt_cube) then have cardgtbound:"card R * card S * card T \ ?e4M^ 3 * ?n^3" by (metis of_nat_power power_mult_distrib) have "(1-\/2) * (\/4)^3 * (\/(4*M))^3 * ?n^3 \ (1-\/2) * (\/4)^3 * card R * card S * card T" using cardgtbound ordered_comm_semiring_class.comm_mult_left_mono True e4gt by fastforce also have "... \ (1-2*(\/4)) * (edge_density R S Gnew - \/4)*(edge_density R T Gnew - \/4) * (edge_density S T Gnew - \/4) * card R * card S * card T" using gtcube c1 \\ < 1\ mincard0 by (simp add: mult.commute mult.left_commute mult_left_mono) also have "... \ card (triangle_triples R S T Gnew)" by (smt (verit, best) e4gt ilt jlt klt min_dens_diff new_fin new_wf rp subsets triangle_counting_lemma) finally have "card (triangle_set Gnew) \ D * ?n^3" using card_convert_triangle_rep_bound new_wf new_fin subsets by (auto simp: triangle_triples_def D_def) then have g_tset_bound: "card (triangle_set G) \ D * ?n^3" using triangle_set_graph_edge_ss_bound by (smt (verit) edges fin local.wf of_nat_mono verts) have "card (triangle_set G) > \ * ?n^3" proof - have "?n^3 > 0" by (simp add: \uverts G \ {}\ card_gt_0_iff fin) with \ \D0 \ D\ have "D * ?n^3 > \ * ?n^3" by force thus "card (triangle_set G) > \ * ?n ^3" using g_tset_bound unfolding D_def by linarith qed thus False using ineq by linarith qed show "real (card (uedges G - uedges Gnew)) \ \ * real ((card (uverts G))\<^sup>2)" using cardbound edges verts by blast qed qed (rule \0 < \\) qed subsection \Roth's Theorem\ text\We will first need the following corollary of the Triangle Removal Lemma.\ text \See \<^url>\https://en.wikipedia.org/wiki/Ruzsa–Szemerédi_problem\. Suggested by Yaël Dillies \ corollary Diamond_free: fixes \ :: real assumes "0 < \" shows "\N>0. \G. card(uverts G) > N \ uwellformed G \ unique_triangles G \ card (uedges G) \ \ * (card (uverts G))\<^sup>2" proof - have "\/3 > 0" using assms by auto then obtain \::real where "\ > 0" and \: "\G. \card(uverts G) > 0; uwellformed G; card (triangle_set G) \ \ * card(uverts G) ^ 3\ \ (\Gnew. triangle_free_graph Gnew \ uverts Gnew = uverts G \ (uedges Gnew \ uedges G) \ card (uedges G - uedges Gnew) \ \/3 * (card (uverts G))\<^sup>2)" using triangle_removal_lemma by metis obtain N::nat where N: "real N \ 1 / (3*\)" by (meson real_arch_simple) show ?thesis proof (intro exI conjI strip) show "N > 0" using N \0 < \\ zero_less_iff_neq_zero by fastforce fix G let ?n = "card (uverts G)" assume G_gt_N: "N < ?n" and wf: "uwellformed G" and uniq: "unique_triangles G" have G_ne: "?n > 0" using G_gt_N by linarith obtain TF where TF: "\e. e \ uedges G \ \x y z. TF e = {x,y,z} \ triangle_in_graph x y z G \ e \ TF e" using uniq unfolding unique_triangles_def by metis let ?TWO = "(\t. [t]\<^bsup>2\<^esup>)" have tri_nsets_2: "[{x,y,z}]\<^bsup>2\<^esup> = {{x,y},{y,z},{x,z}}" if "triangle_in_graph x y z G" for x y z using that unfolding nsets_def triangle_in_graph_def card_2_iff doubleton_eq_iff by (blast dest!: edge_vertices_not_equal [OF wf]) have tri_nsets_3: "{{x,y},{y,z},{x,z}} \ [uedges G]\<^bsup>3\<^esup>" if "triangle_in_graph x y z G" for x y z using that by (simp add: nsets_def card_3_iff triangle_in_graph_def) (metis doubleton_eq_iff edge_vertices_not_equal [OF wf]) have sub: "?TWO ` triangle_set G \ [uedges G]\<^bsup>3\<^esup>" using tri_nsets_2 tri_nsets_3 triangle_set_def by auto have "\i. i \ triangle_set G \ ?TWO i \ {}" using tri_nsets_2 triangle_set_def by auto moreover have dfam: "disjoint_family_on ?TWO (triangle_set G)" using sub [unfolded image_subset_iff] uniq unfolding disjoint_family_on_def triangle_set_def nsets_def unique_triangles_def by (smt (verit) disjoint_iff_not_equal insert_subset mem_Collect_eq mk_disjoint_insert ) ultimately have inj: "inj_on ?TWO (triangle_set G)" by (simp add: disjoint_family_on_iff_disjoint_image) have \
: "\T\triangle_set G. e \ [T]\<^bsup>2\<^esup>" if "e \ uedges G" for e using uniq [unfolded unique_triangles_def] that local.wf apply (simp add: triangle_set_def triangle_in_graph_def nsets_def uwellformed_def) by (metis (mono_tags, lifting) finite.emptyI finite.insertI finite_subset) with sub have "\(?TWO ` triangle_set G) = uedges G" by (auto simp: image_subset_iff nsets_def) then have "card (\(?TWO ` triangle_set G)) = card (uedges G)" by simp moreover have "card (\(?TWO ` triangle_set G)) = 3 * card (triangle_set G)" proof (subst card_UN_disjoint' [OF dfam]) show "finite ([i]\<^bsup>2\<^esup>)" if "i \ triangle_set G" for i using that tri_nsets_2 triangle_set_def by fastforce show "finite (triangle_set G)" by (meson G_ne card_gt_0_iff local.wf finite_triangle_set) have "card ([i]\<^bsup>2\<^esup>) = 3" if "i \ triangle_set G" for i using that wf nsets_def tri_nsets_2 tri_nsets_3 triangle_set_def by fastforce then show "(\i\triangle_set G. card ([i]\<^bsup>2\<^esup>)) = 3 * card (triangle_set G)" by simp qed ultimately have A: "3 * card (triangle_set G) = card (uedges G)" by auto have "card (uedges G) \ card (all_edges(uverts G))" by (meson G_ne all_edges_finite card_gt_0_iff card_mono local.wf wellformed_all_edges) also have "\ = card (uverts G) choose 2" by (metis G_ne card_all_edges card_eq_0_iff not_less0) also have "\ = card (uverts G) * (card (uverts G) - 1) div 2" by (meson n_choose_2_nat) also have "\ < (card (uverts G))\<^sup>2" by (simp add: G_ne less_imp_diff_less less_mult_imp_div_less power2_eq_square) finally have B: "card (uedges G) < (card (uverts G))\<^sup>2" . have "card (triangle_set G) \ (card (uverts G))\<^sup>2 / 3" using A B by linarith also have "\ \ \ * card(uverts G) ^ 3" proof - have "1 \ 3 * \ * N" using N \\ > 0\ by (simp add: field_simps) also have "\ \ 3 * \ * ?n" using G_gt_N \0 < \\ by force finally have "1 * ?n^2 \ (3 * \ * ?n) * ?n^2" by (simp add: G_ne) then show ?thesis by (simp add: eval_nat_numeral mult_ac) qed finally have "card (triangle_set G) \ \ * ?n ^ 3" . then obtain Gnew where Gnew: "triangle_free_graph Gnew" "uverts Gnew = uverts G" "uedges Gnew \ uedges G" and card_edge_diff: "card (uedges G - uedges Gnew) \ \/3 * ?n\<^sup>2" using G_ne \ local.wf by meson text\Deleting an edge removes at most one triangle from the graph by assumption, so the number of edges removed in this process is at least the number of triangles.\ have False if non: "\e. e \ uedges G - uedges Gnew \ {x,y,z} \ TF e" and tri: "triangle_in_graph x y z G" for x y z proof - have "\ triangle_in_graph x y z Gnew" using Gnew triangle_free_graph_def by blast with tri obtain e where eG: "e \ uedges G - uedges Gnew" and esub: "e \ {x,y,z}" using insert_commute triangle_in_graph_def by auto then show False by (metis DiffD1 TF tri uniq unique_triangles_def non [OF eG]) qed then have "triangle_set G \ TF ` (uedges G - uedges Gnew)" unfolding triangle_set_def by blast moreover have "finite (uedges G - uedges Gnew)" by (meson G_ne card_gt_0_iff finite_Diff finite_graph_def wf wellformed_finite) ultimately have "card (triangle_set G) \ card (uedges G - uedges Gnew)" by (meson surj_card_le) then show "card (uedges G) \ \ * ?n\<^sup>2" using A card_edge_diff by linarith qed qed text\We are now ready to proceed to the proof of Roth's Theorem for Arithmetic Progressions. \ definition progression3 :: "'a::comm_monoid_add \ 'a \ 'a set" where "progression3 k d \ {k, k+d, k+d+d}" lemma p3_int_iff: "progression3 (int k) (int d) \ int ` A \ progression3 k d \ A" apply (simp add: progression3_def image_iff) by (smt (verit, best) int_plus of_nat_eq_iff) text\We assume that a set of naturals $A \subseteq \{... lemma RothArithmeticProgressions_aux: fixes \::real assumes "\ > 0" obtains X where "\N \ X. \A \ {..k d. d>0 \ progression3 k d \ A) \ card A < \ * real N" proof - obtain X where "X>0" and X: "\G. \card(uverts G) > X; uwellformed G; unique_triangles G\ \ card (uedges G) \ \/12 * (card (uverts G))\<^sup>2" by (metis assms Diamond_free less_divide_eq_numeral1(1) mult_eq_0_iff) show thesis proof (intro strip that) fix N A assume "X \ N" and A: "A \ {..k d. 0 < d \ progression3 k d \ A" then have "N > 0" using \0 < X\ by linarith define M where "M \ Suc (2*N)" have M_mod_bound[simp]: "x mod M < M" for x by (simp add: M_def) have "odd M" "M>0" "N {..k d. d > 0 \ progression3 k d \ int ` A" by (metis imageE insert_subset non p3_int_iff pos_int_cases progression3_def) text\Construct a tripartite graph @{term G} whose three parts are copies of @{text"\/M\"}.\ define part_of where "part_of \ \\. (\i. prod_encode (\,i)) ` {.. \p. fst (prod_decode p)" define from_part where "from_part \ \p. snd (prod_decode p)" have enc_iff [simp]: "prod_encode (a,i) \ part_of a' \ a'=a \ i0 < M\ by (clarsimp simp: part_of_def image_iff Bex_def) presburger have part_of_M: "p \ part_of a \ from_part p < M" for a p using from_part_def part_of_def by fastforce have disjnt_part_of: "a \ b \ disjnt (part_of a) (part_of b)" for a b by (auto simp: part_of_def disjnt_iff) have from_enc [simp]: "from_part (prod_encode (a,i)) = i" for a i by (simp add: from_part_def) have finpart [iff]: "finite (part_of a)" for a by (simp add: part_of_def \0 < M\) have cardpart [simp]: "card (part_of a) = M" for a using \0 < M\ by (simp add: part_of_def eq_nat_nat_iff inj_on_def card_image) let ?X = "part_of 0" let ?Y = "part_of (Suc 0)" let ?Z = "part_of (Suc (Suc 0))" define diff where "diff \ \a b. (int a - int b) mod (int M)" have inj_on_diff: "inj_on (\x. diff x a) {.. x mod int M = x' mod int M" for x x' y by (simp add: mod_eq_dvd_iff) have diff_invert: "diff y x = int a \ y = (x + a) mod M" if "y < M" "a\A" for x y a proof - have "a < M" using A \N < M\ that by auto show ?thesis proof assume "diff y x = int a" with that \a have "int y = int (x+a) mod int M" unfolding diff_def by (smt (verit, ccfv_SIG) eq_mod_M mod_less of_nat_add zmod_int) with that show "y = (x + a) mod M" by (metis nat_int zmod_int) qed (simp add: \a < M\ diff_def mod_diff_left_eq zmod_int) qed define diff2 where "diff2 \ \a b. ((int a - int b) * int(Suc N)) mod (int M)" have inj_on_diff2: "inj_on (\x. diff2 x a) {..0 < N\ by auto have diff2_by2: "(diff2 a b * 2) mod M = diff a b" for a b proof - have "int M dvd ((int a - int b) * int M)" by simp then have "int M dvd ((int a - int b) * int (Suc N) * 2 - (int a - int b))" by (auto simp: M_def algebra_simps) then show ?thesis by (metis diff2_def diff_def mod_eq_dvd_iff mod_mult_left_eq) qed have diff2_invert: "diff2 (((x + a) mod M + a) mod M) x = int a" if "a\A" for x a proof - have 1: "((x + a) mod M + a) mod M = (x + 2*a) mod M" by (metis group_cancel.add1 mod_add_left_eq mult_2) have "(int ((x + 2*a) mod M) - int x) * (1 + int N) mod int M = (int (x + 2*a) - int x) * (1 + int N) mod int M" by (metis mod_diff_left_eq mod_mult_cong of_nat_mod) also have "\ = int (a * (Suc M)) mod int M" by (simp add: algebra_simps M_def) also have "\ = int a mod int M" by simp also have "\ = int a" using A M_def subsetD that by auto finally show ?thesis using that by (auto simp: 1 diff2_def) qed define Edges where "Edges \ \X Y df. {{x,y}| x y. x \ X \ y \ Y \ df(from_part y) (from_part x) \ int ` A}" have Edges_subset: "Edges X Y df \ Pow (X \ Y)" for X Y df by (auto simp: Edges_def) define XY where "XY \ Edges ?X ?Y diff" define YZ where "YZ \ Edges ?Y ?Z diff" define XZ where "XZ \ Edges ?X ?Z diff2" obtain [simp]: "finite XY" "finite YZ" "finite XZ" using Edges_subset unfolding XY_def YZ_def XZ_def by (metis finite_Pow_iff finite_UnI finite_subset finpart) define G where "G \ (?X \ ?Y \ ?Z, XY \ YZ \ XZ)" have finG: "finite (uverts G)" and cardG: "card (uverts G) = 3*M" by (simp_all add: G_def card_Un_disjnt disjnt_part_of) then have "card(uverts G) > X" using M_def \X \ N\ by linarith have "uwellformed G" by (fastforce simp: card_insert_if part_of_def G_def XY_def YZ_def XZ_def Edges_def uwellformed_def) have [simp]: "{prod_encode (\,x), prod_encode (\,y)} \ XY" "{prod_encode (\,x), prod_encode (\,y)} \ YZ" "{prod_encode (\,x), prod_encode (\,y)} \ XZ" for x y \ by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff) have label_ne_XY [simp]: "label_of_part p \ label_of_part q" if "{p,q} \ XY" for p q using that by (auto simp add: XY_def part_of_def Edges_def doubleton_eq_iff label_of_part_def) then have [simp]: "{p} \ XY" for p by (metis insert_absorb2) have label_ne_YZ [simp]: "label_of_part p \ label_of_part q" if "{p,q} \ YZ" for p q using that by (auto simp add: YZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def) then have [simp]: "{p} \ YZ" for p by (metis insert_absorb2) have label_ne_XZ [simp]: "label_of_part p \ label_of_part q" if "{p,q} \ XZ" for p q using that by (auto simp add: XZ_def part_of_def Edges_def doubleton_eq_iff label_of_part_def) then have [simp]: "{p} \ XZ" for p by (metis insert_absorb2) have label012: "label_of_part v < 3" if "v \ uverts G" for v using that by (auto simp add: G_def eval_nat_numeral part_of_def label_of_part_def) have Edges_distinct: "\p q r \ \ \ \ df df'. \{p,q} \ Edges (part_of \) (part_of \) df; {q,r} \ Edges (part_of \) (part_of \) df; {p,r} \ Edges (part_of \) (part_of \) df'; \ \ \; \ \ \\ \ False" apply (auto simp: disjnt_iff Edges_def doubleton_eq_iff conj_disj_distribR ex_disj_distrib) apply (metis disjnt_iff disjnt_part_of)+ done have uniq: "\id\A. \x \ {p,q,r}. \y \ {p,q,r}. \z \ {p,q,r}. x = prod_encode(0, i) \ y = prod_encode(1, (i+d) mod M) \ z = prod_encode(2, (i+d+d) mod M)" if T: "triangle_in_graph p q r G" for p q r proof - obtain x y z where xy: "{x,y} \ XY" and yz: "{y,z} \ YZ" and xz: "{x,z} \ XZ" and x: "x \ {p,q,r}" and y: "y \ {p,q,r}" and z: "z \ {p,q,r}" using T apply (simp add: triangle_in_graph_def G_def XY_def YZ_def XZ_def) by (smt (verit, ccfv_SIG) Edges_distinct Zero_not_Suc insert_commute n_not_Suc_n) then have "x \ ?X" "y \ ?Y" "z \ ?Z" by (auto simp: XY_def YZ_def XZ_def Edges_def doubleton_eq_iff; metis disjnt_iff disjnt_part_of)+ then obtain i j k where i: "x = prod_encode(0,i)" and j: "y = prod_encode(1,j)" and k: "z = prod_encode(2,k)" by (metis One_nat_def Suc_1 enc_iff prod_decode_aux.cases prod_decode_inverse) obtain a1 where "a1 \ A" and a1: "(int j - int i) mod int M = int a1" using xy \x \ ?X\ i j by (auto simp add: XY_def Edges_def doubleton_eq_iff diff_def) obtain a3 where "a3 \ A" and a3: "(int k - int j) mod int M = int a3" using yz \x \ ?X\ j k by (auto simp add: YZ_def Edges_def doubleton_eq_iff diff_def) obtain a2 where "a2 \ A" and a2: "(int k - int i) mod int M = int (a2 * 2) mod int M" using xz \x \ ?X\ i k apply (auto simp add: XZ_def Edges_def doubleton_eq_iff) by (metis diff2_by2 diff_def int_plus mult_2_right) obtain "a1a1 \ A\ \a2 \ A\ \a3 \ A\ by blast then obtain "a1+a3 < M" "a2 * 2 < M" by (simp add: M_def) then have "int (a2 * 2) = int (a2 * 2) mod M" by force also have "\ = int (a1 + a3) mod int M" using a1 a2 a3 by (smt (verit, del_insts) int_plus mod_add_eq) also have "\ = int (a1+a3)" using \a1 + a3 < M\ by force finally have "a2*2 = a1+a3" by presburger then obtain equal: "a3 - a2 = a2 - a1" "a2 - a3 = a1 - a2" by (metis Nat.diff_cancel diff_cancel2 mult_2_right) with \a1 \ A\ \a2 \ A\ \a3 \ A\ have "progression3 a1 (a2 - a1) \ A" apply (clarsimp simp: progression3_def) by (metis diff_is_0_eq' le_add_diff_inverse nle_le) with non equal have "a2 = a1" unfolding progression3_def by (metis \a2 \ A\ \a3 \ A\ add.right_neutral diff_is_0_eq insert_subset le_add_diff_inverse not_gr_zero) then have "a3 = a2" using \a2 * 2 = a1 + a3\ by force have k_minus_j: "(int k - int j) mod int M = int a1" by (simp add: \a2 = a1\ \a3 = a2\ a3) have i_to_j: "j mod M = (i+a1) mod M" by (metis a1 add_diff_cancel_left' add_diff_eq mod_add_right_eq nat_int of_nat_add of_nat_mod) have j_to_k: "k mod M = (j+a1) mod M" by (metis \a2 = a1\ \a3 = a2\ a3 add_diff_cancel_left' add_diff_eq mod_add_right_eq nat_int of_nat_add of_nat_mod) have "ix \ ?X\ i by simp then show ?thesis using i j k x y z \a1 \ A\ by (metis \y \ ?Y\ \z \?Z\ enc_iff i_to_j j_to_k mod_add_left_eq mod_less) qed text\Every edge of the graph G lies in exactly one triangle.\ have "unique_triangles G" unfolding unique_triangles_def proof (intro strip) fix e assume "e \ uedges G" then consider "e \ XY" | "e \ YZ" | "e \ XZ" using G_def by fastforce then show "\!T. \x y z. T = {x, y, z} \ triangle_in_graph x y z G \ e \ T" proof cases case 1 then obtain i j a where eeq: "e = {prod_encode(0,i), prod_encode(1,j)}" and "i A" by (auto simp: XY_def Edges_def part_of_def) let ?x = "prod_encode (0, i)" let ?y = "prod_encode (1, j)" let ?z = "prod_encode (2, (j+a) mod M)" have yeq: "j = (i+a) mod M" using diff_invert using \a \ A\ df \j by blast with \a \ A\ \j have "{?y,?z} \ YZ" by (fastforce simp: YZ_def Edges_def image_iff diff_invert) moreover have "{?x,?z} \ XZ" using \a \ A\ by (fastforce simp: XZ_def Edges_def yeq diff2_invert \i) ultimately have T: "triangle_in_graph ?x ?y ?z G" using \e \ uedges G\ by (force simp add: G_def eeq triangle_in_graph_def) show ?thesis proof (intro ex1I) show "\x y z. {?x,?y,?z} = {x, y, z} \ triangle_in_graph x y z G \ e \ {?x,?y,?z}" using T eeq by blast fix T assume "\p q r. T = {p, q, r} \ triangle_in_graph p q r G \ e \ T" then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e \ T" by blast with uniq obtain i' a' x y z where "i' A" and x: "x \ {p,q,r}" and y: "y \ {p,q,r}" and z: "z \ {p,q,r}" and xeq: "x = prod_encode(0, i')" and yeq: "y = prod_encode(1, (i'+a') mod M)" and zeq: "z = prod_encode(2, (i'+a'+a') mod M)" by metis then have sets_eq: "{x,y,z} = {p,q,r}" by auto with Teq \e \ T\ have esub': "e \ {x,y,z}" by blast have "a' < M" using A \N < M\ \a' \ A\ by auto obtain "?x \ e" "?y \ e" using eeq by force then have "x = ?x" using esub' eeq yeq zeq by simp then have "y = ?y" using esub' eeq zeq by simp obtain eq': "i' = i" "(i'+a') mod M = j" using \x = ?x\ xeq using \y =?y\ yeq by auto then have "diff (i'+a') i' = int a'" by (simp add: diff_def \a' < M\) then have "a' = a" by (metis eq' df diff_def mod_diff_left_eq nat_int zmod_int) then have "z = ?z" by (metis \y = ?y\ mod_add_left_eq prod_encode_eq snd_conv yeq zeq) then show "T = {?x,?y,?z}" using Teq \x = ?x\ \y = ?y\ sets_eq by presburger qed next case 2 then obtain j k a where eeq: "e = {prod_encode(1,j), prod_encode(2,k)}" and "j A" by (auto simp: YZ_def Edges_def part_of_def numeral_2_eq_2) let ?x = "prod_encode (0, (M+j-a) mod M)" let ?y = "prod_encode (1, j)" let ?z = "prod_encode (2, k)" have zeq: "k = (j+a) mod M" using diff_invert using \a \ A\ df \k by blast with \a \ A\ \k have "{?x,?z} \ XZ" unfolding XZ_def Edges_def image_iff apply (clarsimp simp: mod_add_left_eq doubleton_eq_iff conj_disj_distribR ex_disj_distrib) apply (smt (verit, ccfv_threshold) A \N < M\ diff2_invert le_add_diff_inverse2 lessThan_iff linorder_not_less mod_add_left_eq mod_add_self1 not_add_less1 order.strict_trans subsetD) done moreover have "a < N" using A \a \ A\ by blast with \N < M\ have "((M + j - a) mod M + a) mod M = j mod M" by (simp add: mod_add_left_eq) then have "{?x,?y} \ XY" using \a \ A\ \j unfolding XY_def Edges_def by (force simp add: zeq image_iff diff_invert doubleton_eq_iff ex_disj_distrib) ultimately have T: "triangle_in_graph ?x ?y ?z G" using \e \ uedges G\ by (auto simp: G_def eeq triangle_in_graph_def) show ?thesis proof (intro ex1I) show "\x y z. {?x,?y,?z} = {x, y, z} \ triangle_in_graph x y z G \ e \ {?x,?y,?z}" using T eeq by blast fix T assume "\p q r. T = {p, q, r} \ triangle_in_graph p q r G \ e \ T" then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e \ T" by blast with uniq obtain i' a' x y z where "i' A" and x: "x \ {p,q,r}" and y: "y \ {p,q,r}" and z: "z \ {p,q,r}" and xeq: "x = prod_encode(0, i')" and yeq: "y = prod_encode(1, (i'+a') mod M)" and zeq: "z = prod_encode(2, (i'+a'+a') mod M)" by metis then have sets_eq: "{x,y,z} = {p,q,r}" by auto with Teq \e \ T\ have esub': "e \ {x,y,z}" by blast have "a' < M" using A \N < M\ \a' \ A\ by auto obtain "?y \ e" "?z \ e" using eeq by force then have "y = ?y" using esub' eeq xeq zeq by simp then have "z = ?z" using esub' eeq xeq by simp obtain eq': "(i'+a') mod M = j" "(i'+a'+a') mod M = k" using \y = ?y\ yeq using \z =?z\ zeq by auto then have "diff (i'+a'+a') (i'+a') = int a'" by (simp add: diff_def \a' < M\) then have "a' = a" by (metis M_mod_bound \a' \ A\ df diff_invert eq' mod_add_eq mod_if of_nat_eq_iff) have "(M + ((i'+a') mod M) - a') mod M = (M + (i' + a') - a') mod M" by (metis Nat.add_diff_assoc2 \a' < M\ less_imp_le_nat mod_add_right_eq) with \i' < M\ have "(M + ((i'+a') mod M) - a') mod M = i'" by force with \a' = a\ eq' have "(M + j - a) mod M = i'" by force with xeq have "x = ?x" by blast then show "T = {?x,?y,?z}" using Teq \z = ?z\ \y = ?y\ sets_eq by presburger qed next case 3 then obtain i k a where eeq: "e = {prod_encode(0,i), prod_encode(2,k)}" and "i A" by (auto simp: XZ_def Edges_def part_of_def eval_nat_numeral) let ?x = "prod_encode (0, i)" let ?y = "prod_encode (1, (i+a) mod M)" let ?z = "prod_encode (2, k)" have keq: "k = (i+a+a) mod M" using diff2_invert [OF \a \ A\, of i] df \k using inj_on_diff2 [of i] by (simp add: inj_on_def Ball_def mod_add_left_eq) with \a \ A\ have "{?x,?y} \ XY" using \a \ A\ \i \k apply (auto simp: XY_def Edges_def) by (metis M_mod_bound diff_invert enc_iff from_enc imageI) moreover have "{?y,?z} \ YZ" apply (auto simp: YZ_def Edges_def image_iff eval_nat_numeral) by (metis M_mod_bound \a \ A\ diff_invert enc_iff from_enc mod_add_left_eq keq) ultimately have T: "triangle_in_graph ?x ?y ?z G" using \e \ uedges G\ by (force simp add: G_def eeq triangle_in_graph_def) show ?thesis proof (intro ex1I) show "\x y z. {?x,?y,?z} = {x, y, z} \ triangle_in_graph x y z G \ e \ {?x,?y,?z}" using T eeq by blast fix T assume "\p q r. T = {p, q, r} \ triangle_in_graph p q r G \ e \ T" then obtain p q r where Teq: "T = {p,q,r}" and tri: "triangle_in_graph p q r G" and "e \ T" by blast with uniq obtain i' a' x y z where "i' A" and x: "x \ {p,q,r}" and y: "y \ {p,q,r}" and z: "z \ {p,q,r}" and xeq: "x = prod_encode(0, i')" and yeq: "y = prod_encode(1, (i'+a') mod M)" and zeq: "z = prod_encode(2, (i'+a'+a') mod M)" by metis then have sets_eq: "{x,y,z} = {p,q,r}" by auto with Teq \e \ T\ have esub': "e \ {x,y,z}" by blast have "a' < M" using A \N < M\ \a' \ A\ by auto obtain "?x \ e" "?z \ e" using eeq by force then have "x = ?x" using esub' eeq yeq zeq by simp then have "z = ?z" using esub' eeq yeq by simp obtain eq': "i' = i" "(i'+a'+a') mod M = k" using \x = ?x\ xeq using \z =?z\ zeq by auto then have "diff (i'+a') i' = int a'" by (simp add: diff_def \a' < M\) then have "a' = a" by (metis \a' \ A\ add.commute df diff2_invert eq' mod_add_right_eq nat_int) then have "y = ?y" by (metis \x = ?x\ prod_encode_eq snd_conv yeq xeq) then show "T = {?x,?y,?z}" using Teq \x = ?x\ \z = ?z\ sets_eq by presburger qed qed qed have *: "card (uedges G) \ \/12 * (card (uverts G))\<^sup>2" using X \X < card (uverts G)\ \unique_triangles G\ \uwellformed G\ by blast have diff_cancel: "\j A" for i a proof - have "int a < int M" using A M_def that by auto then have "(int ((i + a) mod M) - int i) mod int M = int a" by (simp add: mod_diff_left_eq of_nat_mod) then show ?thesis using \0 < M\ diff_def mod_less_divisor by blast qed have diff2_cancel: "\j A" "i = 2 * int a * (1 + int N) mod int M" by (smt (verit) mod_diff_left_eq mod_mult_eq mod_mult_right_eq) also have "\ = int a mod int M" proof - have "(2 * int a * (1 + int N) - int a) = M * a" by (simp add: M_def algebra_simps) then have "M dvd (2 * int a * (1 + int N) - int a)" by simp then show ?thesis using mod_eq_dvd_iff by blast qed also have "\ = a" by (simp add: \a < M\) finally show ?thesis by (metis \0 < M\ diff2_def mod_less_divisor of_nat_Suc) qed have card_Edges: "card (Edges (part_of \) (part_of \) df) = M * card A" (is "card ?E = _") if "\ \ \" and df_cancel: "\a\A. \ija. inj_on (\x. df x a) {.. \ df proof - define R where "R \ \\ Y df u p. \x y i a. u = {x,y} \ p = (i,a) \ x = prod_encode (\,i) \ y \ Y \ a \ A \ df(from_part y) (from_part x) = int a" have R_uniq: "\R \ (part_of \) df u p; R \ (part_of \) df u p'; \ \ \\ \ p' = p" for u p p' \ \ df by (auto simp add: R_def doubleton_eq_iff) define f where "f \ \\ Y df u. @p. R \ Y df u p" have f_if_R: "f \ (part_of \) df u = p" if "R \ (part_of \) df u p" "\ \ \" for u p \ \ df using R_uniq f_def that by blast have "bij_betw (f \ (part_of \) df) ?E ({.. A)" unfolding bij_betw_def inj_on_def proof (intro conjI strip) fix u u' assume "u \ ?E" and "u' \ ?E" and eq: "f \ (part_of \) df u = f \ (part_of \) df u'" obtain x y a where u: "u = {x,y}" "x \ part_of \" "y \ part_of \" "a \ A" and df: "df (from_part y) (from_part x) = int a" using \u \ ?E\ by (force simp add: Edges_def image_iff) then obtain i where i: "x = prod_encode (\,i)" using part_of_def by blast with u df R_def f_if_R that have fu: "f \ (part_of \) df u = (i,a)" by blast obtain x' y' a' where u': "u' = {x',y'}" "x' \ part_of \" "y' \ part_of \" "a'\A" and df': "df (from_part y') (from_part x') = int a'" using \u' \ ?E\ by (force simp add: Edges_def image_iff) then obtain i' where i': "x' = prod_encode (\,i')" using part_of_def by blast with u' df' R_def f_if_R that have fu': "f \ (part_of \) df u' = (i',a')" by blast have "i'=i" "a' = a" using fu fu' eq by auto with i i' have "x = x'" by meson moreover have "from_part y = from_part y'" using df df' \x = x'\ \a' = a\ df_inj u'(3) u(3) by (clarsimp simp add: inj_on_def) (metis part_of_M lessThan_iff) then have "y = y'" using part_of_def u'(3) u(3) by fastforce ultimately show "u = u'" using u'(1) u(1) by force next have "f \ (part_of \) df ` ?E \ {.. A" proof (clarsimp simp: Edges_def) fix i a x y b assume "x \ part_of \" "y \ part_of \" "df (from_part y) (from_part x) = int b" "b \ A" and feq: "(i, a) = f \ (part_of \) df {x, y}" then have "R \ (part_of \) df {x,y} (from_part x, b)" by (auto simp: R_def doubleton_eq_iff part_of_def) then have "(from_part x, b) = (i, a)" by (simp add: f_if_R feq from_part_def that) then show "i < M \ a \ A" using \x \ part_of \\ \b \ A\ part_of_M by fastforce qed moreover have "{.. A \ f \ (part_of \) df ` ?E" proof clarsimp fix i a assume "a \ A" and "i < M" then obtain j where "j (part_of \) df {prod_encode (\, i), prod_encode (\, j)} = (i,a)" by (metis R_def \a \ A\ enc_iff f_if_R from_enc \\ \ \\) then have "{prod_encode (\,i), prod_encode (\, j mod M)} \ Edges (part_of \) (part_of \) df" apply (clarsimp simp: Edges_def doubleton_eq_iff) by (metis \a \ A\ \i < M\ \j < M\ enc_iff from_enc image_eqI j mod_if) then show "(i,a) \ f \ (part_of \) df ` Edges (part_of \) (part_of \) df" using \j < M\ fj image_iff by fastforce qed ultimately show "f \ (part_of \) df ` ?E = {.. A" by blast qed then show ?thesis by (simp add: bij_betw_same_card card_cartesian_product) qed have [simp]: "disjnt XY YZ" "disjnt XY XZ" "disjnt YZ XZ" using disjnt_part_of unfolding XY_def YZ_def XZ_def Edges_def disjnt_def by (clarsimp simp add: disjoint_iff doubleton_eq_iff, meson disjnt_iff n_not_Suc_n nat.discI)+ have [simp]: "card XY = M * card A" "card YZ = M * card A" by (simp_all add: XY_def YZ_def card_Edges diff_cancel inj_on_diff) have [simp]: "card XZ = M * card A" by (simp_all add: XZ_def card_Edges diff2_cancel inj_on_diff2) have card_edges: "card (uedges G) = 3 * M * card A" by (simp add: G_def card_Un_disjnt) have "card A \ \ * (real M / 4)" using * \0 < M\ by (simp add: cardG card_edges power2_eq_square) also have "\ < \ * N" using \N>0\ by (simp add: M_def assms) finally show "card A < \ * N" . qed qed text\We finally present the main statement formulated using the upper asymptotic density condition.\ theorem RothArithmeticProgressions: assumes "upper_asymptotic_density A > 0" shows "\k d. d>0 \ progression3 k d \ A" proof (rule ccontr) assume non: "\k d. 0 < d \ progression3 k d \ A" obtain X where X: "\N \ X. \A' \ {..k d. d>0 \ progression3 k d \ A') \ card A' < upper_asymptotic_density A / 2 * real N" by (metis half_gt_zero RothArithmeticProgressions_aux assms) then have "\N \ X. card (A \ {.. upper_asymptotic_density A / 2" by (force simp add: eventually_sequentially less_eq_real_def intro!: upper_asymptotic_densityI) with assms show False by linarith qed end