diff --git a/thys/Clique_and_Monotone_Circuits/Assumptions_and_Approximations.thy b/thys/Clique_and_Monotone_Circuits/Assumptions_and_Approximations.thy --- a/thys/Clique_and_Monotone_Circuits/Assumptions_and_Approximations.thy +++ b/thys/Clique_and_Monotone_Circuits/Assumptions_and_Approximations.thy @@ -1,472 +1,467 @@ section \Simplied Version of Gordeev's Proof for Monotone Circuits\ subsection \Setup of Global Assumptions and Proofs of Approximations\ theory Assumptions_and_Approximations imports "HOL-Real_Asymp.Real_Asymp" Stirling_Formula.Stirling_Formula Preliminaries begin locale first_assumptions = fixes l p k :: nat assumes l2: "l > 2" and pl: "p > l" and kp: "k > p" begin lemma k2: "k > 2" using pl l2 kp by auto lemma p: "p > 2" using pl l2 kp by auto lemma k: "k > l" using pl l2 kp by auto definition "m = k^4" lemma km: "k < m" using power_strict_increasing_iff[of k 1 4] k2 unfolding m_def by auto lemma lm: "l + 1 < m" using km k by simp lemma m2: "m > 2" using k2 km by auto lemma mp: "m > p" using km k kp by simp -definition "L = fact l * (p - 1) ^ l + 1" +definition "L = fact l * (p - 1) ^ l" lemma kml: "k \ m - l" proof - have "k \ k * k - k" using k2 by (cases k, auto) also have "\ \ (k * k) * 1 - l" using k by simp also have "\ \ (k * k) * (k * k) - l" by (intro diff_le_mono mult_left_mono, insert k2, auto) also have "(k * k) * (k * k) = m" unfolding m_def by algebra finally show ?thesis . qed end locale second_assumptions = first_assumptions + assumes kl2: "k = l^2" and l8: "l \ 8" begin lemma Lm: "L \ m" proof - have "m \ l ^ l" unfolding L_def m_def unfolding kl2 power_mult[symmetric] by (intro power_increasing, insert l8, auto) also have "\ \ (p - 1) ^ l" by (rule power_mono, insert pl, auto) also have "\ \ fact l * (p - 1) ^ l" by simp also have "\ \ L" unfolding L_def by simp finally show ?thesis . qed lemma Lp: "L > p" using Lm mp by auto lemma L3: "L > 3" using p Lp by auto end definition "eps = 1/(1000 :: real)" lemma eps: "eps > 0" unfolding eps_def by simp definition L0 :: nat where "L0 = (SOME l0. \l\l0. 1 / 3 < (1 + - 1 / real l) ^ l)" definition M0 :: nat where "M0 = (SOME y. \ x. x \ y \ (root 8 (real x) * log 2 (real x) + 1) / real x powr (1 / 8 + eps) \ 1)" definition L0' :: nat where "L0' = (SOME l0. \ n \ l0. 6 * (real n)^16 * fact n < real (n\<^sup>2 ^ 4) powr (1 / 8 * real (n\<^sup>2 ^ 4) powr (1 / 8)))" definition L0'' :: nat where "L0'' = (SOME l0. \ l \ l0. real l * log 2 (real (l\<^sup>2 ^ 4)) + 1 < real (l\<^sup>2))" lemma L0'': assumes "l \ L0''" shows "real l * log 2 (real (l\<^sup>2 ^ 4)) + 1 < real (l\<^sup>2)" proof - have "(\ l :: nat. (real l * log 2 (real (l\<^sup>2 ^ 4)) + 1) / real (l\<^sup>2)) \ 0" by real_asymp from LIMSEQ_D[OF this, of 1] obtain l0 where "\l\l0. \1 + real l * log 2 (real l ^ 8)\ / (real l)\<^sup>2 < 1" by (auto simp: field_simps) hence "\ l \ max 1 l0. real l * log 2 (real (l\<^sup>2 ^ 4)) + 1 < real (l\<^sup>2)" by (auto simp: field_simps) hence "\ l0. \ l \ l0. real l * log 2 (real (l\<^sup>2 ^ 4)) + 1 < real (l\<^sup>2)" by blast from someI_ex[OF this, folded L0''_def, rule_format, OF assms] show ?thesis . qed definition M0' :: nat where "M0' = (SOME x0. \ x \ x0. real x powr (2 / 3) \ x powr (3 / 4) - 1)" locale third_assumptions = second_assumptions + assumes pllog: "l * log 2 m \ p" "real p \ l * log 2 m + 1" and L0: "l \ L0" and L0': "l \ L0'" and M0': "m \ M0'" and M0: "m \ M0" begin lemma approximation1: "(real (k - 1)) ^ (m - l) * prod (\ i. real (k - 1 - i)) {0.. (real (k - 1)) ^ m / 3" proof - have "real (k - 1) ^ (m - l) * (\i = 0..i = 0.. > (real (k - 1)) ^ m * (1/3)" proof (rule mult_strict_left_mono) define f where "f l = (1 + (-1) / real l) ^ l" for l define e1 :: real where "e1 = exp (- 1)" define lim :: real where "lim = 1 / 3" from tendsto_exp_limit_sequentially[of "-1", folded f_def] have f: "f \ e1" by (simp add: e1_def) have "lim < (1 - 1 / real 6) ^ 6" unfolding lim_def by code_simp also have " \ \ exp (- 1)" by (rule exp_ge_one_minus_x_over_n_power_n, auto) finally have "lim < e1" unfolding e1_def by auto with f have "\ l0. \ l. l \ l0 \ f l > lim" by (metis eventually_sequentially order_tendstoD(1)) from someI_ex[OF this[unfolded f_def lim_def], folded L0_def] L0 have fl: "f l > 1/3" unfolding f_def by auto define start where "start = inverse (real (k - 1)) ^ l * (\i = 0.. _. inverse (real (k - 1))) {0.. i. real (k - 1 - i)) {0 ..< l})" by (simp add: start_def) also have "\ = uminus (prod (\ i. inverse (real (k - 1)) * real (k - 1 - i)) {0.. \ uminus (prod (\ i. inverse (real (k - 1)) * real (k - 1 - (l - 1))) {0.. = uminus ((inverse (real (k - 1)) * real (k - l)) ^ l)" by simp also have "inverse (real (k - 1)) * real (k - l) = inverse (real (k - 1)) * ((real (k - 1)) - (real l - 1))" using l2 k2 k by simp also have "\ = 1 - (real l - 1) / (real (k - 1))" using l2 k2 k by (simp add: field_simps) also have "real (k - 1) = real k - 1" using k2 by simp also have "\ = (real l - 1) * (real l + 1)" unfolding kl2 of_nat_power by (simp add: field_simps power2_eq_square) also have "(real l - 1) / \ = inverse (real l + 1)" using l2 by (smt (verit, best) divide_divide_eq_left' divide_inverse nat_1_add_1 nat_less_real_le nonzero_mult_div_cancel_left of_nat_1 of_nat_add) also have "- ((1 - inverse (real l + 1)) ^ l) \ - ((1 - inverse (real l)) ^ l)" unfolding neg_le_iff_le by (intro power_mono, insert l2, auto simp: field_simps) also have "\ < - (1/3)" using fl unfolding f_def by (auto simp: field_simps) finally have start: "start > 1 / 3" by simp thus "inverse (real (k - 1)) ^ l * (\i = 0.. 1/3" unfolding start_def by simp qed (insert k2, auto) finally show ?thesis by simp qed lemma approximation2: fixes s :: nat assumes "m choose k \ s * L\<^sup>2 * (m - l - 1 choose (k - l - 1))" shows "((m - l) / k)^l / (6 * L^2) < s" proof - let ?r = real define q where "q = (?r (L\<^sup>2) * ?r (m - l - 1 choose (k - l - 1)))" have q: "q > 0" unfolding q_def by (insert L3 km, auto) have "?r (m choose k) \ ?r (s * L\<^sup>2 * (m - l - 1 choose (k - l - 1)))" unfolding of_nat_le_iff using assms by simp hence "m choose k \ s * q" unfolding q_def by simp hence *: "s \ (m choose k) / q" using q by (metis mult_imp_div_pos_le) have "(((m - l) / k)^l / (L^2)) / 6 < ((m - l) / k)^l / (L^2) / 1" by (rule divide_strict_left_mono, insert m2 L3 lm k, auto intro!: mult_pos_pos divide_pos_pos zero_less_power) also have "\ = ((m - l) / k)^l / (L^2)" by simp also have "\ \ ((m choose k) / (m - l - 1 choose (k - l - 1))) / (L^2)" proof (rule divide_right_mono) define b where "b = ?r (m - l - 1 choose (k - l - 1))" define c where "c = (?r k)^l" have b0: "b > 0" unfolding b_def using km l2 by simp have c0: "c > 0" unfolding c_def using k by auto define aim where "aim = (((m - l) / k)^l \ (m choose k) / (m - l - 1 choose (k - l - 1)))" have "aim \ ((m - l) / k)^l \ (m choose k) / b" unfolding b_def aim_def by simp also have "\ \ b * ((m - l) / k)^l \ (m choose k)" using b0 by (simp add: mult.commute pos_le_divide_eq) also have "\ \ b * (m - l)^l / c \ (m choose k)" by (simp add: power_divide c_def) also have "\ \ b * (m - l)^l \ (m choose k) * c" using c0 b0 by (auto simp add: mult.commute pos_divide_le_eq) also have "(m choose k) = fact m / (fact k * fact (m - k))" by (rule binomial_fact, insert km, auto) also have "b = fact (m - l - 1) / (fact (k - l - 1) * fact (m - l - 1 - (k - l - 1)))" unfolding b_def by (rule binomial_fact, insert k km, auto) finally have "aim \ fact (m - l - 1) / fact (k - l - 1) * (m - l) ^ l / fact (m - l - 1 - (k - l - 1)) \ (fact m / fact k) * (?r k)^l / fact (m - k)" unfolding c_def by simp also have "m - l - 1 - (k - l - 1) = m - k" using l2 k km by simp finally have "aim \ fact (m - l - 1) / fact (k - l - 1) * ?r (m - l) ^ l \ fact m / fact k * ?r k ^ l" unfolding divide_le_cancel using km by simp also have "\ \ (fact (m - (l + 1)) * ?r (m - l) ^ l) * fact k \ (fact m / k) * (fact (k - (l + 1)) * (?r k * ?r k ^ l))" using k2 by (simp add: field_simps) also have "\" proof (intro mult_mono) have "fact k \ fact (k - (l + 1)) * (?r k ^ (l + 1))" by (rule fact_approx_minus, insert k, auto) also have "\ = (fact (k - (l + 1)) * ?r k ^ l) * ?r k" by simp finally show "fact k \ fact (k - (l + 1)) * (?r k * ?r k ^ l)" by (simp add: field_simps) have "fact (m - (l + 1)) * real (m - l) ^ l \ fact m / k \ (fact (m - (l + 1)) * ?r k) * real (m - l) ^ l \ fact m" using k2 by (simp add: field_simps) also have "\" proof - have "(fact (m - (l + 1)) * ?r k) * ?r (m - l) ^ l \ (fact (m - (l + 1)) * ?r (m - l)) * ?r (m - l) ^ l" by (intro mult_mono, insert kml, auto) also have "((fact (m - (l + 1)) * ?r (m - l)) * ?r (m - l) ^ l) = (fact (m - (l + 1)) * ?r (m - l) ^ (l + 1))" by simp also have "\ \ fact m" by (rule fact_approx_upper_minus, insert km k, auto) finally show "fact (m - (l + 1)) * real k * real (m - l) ^ l \ fact m" . qed finally show "fact (m - (l + 1)) * real (m - l) ^ l \ fact m / k" . qed auto finally show "((m - l) / k)^l \ (m choose k) / (m - l - 1 choose (k - l - 1))" unfolding aim_def . qed simp also have "\ = (m choose k) / q" unfolding q_def by simp also have "\ \ s" using q * by metis finally show "((m - l) / k)^l / (6 * L^2) < s" by simp qed lemma approximation3: fixes s :: nat assumes "(k - 1)^m / 3 < (s * (L\<^sup>2 * (k - 1) ^ m)) / 2 ^ (p - 1)" shows "((m - l) / k)^l / (6 * L^2) < s" proof - define A where "A = real (L\<^sup>2 * (k - 1) ^ m)" have A0: "A > 0" unfolding A_def using L3 k2 m2 by simp from mult_strict_left_mono[OF assms, of "2 ^ (p - 1)"] have "2^(p - 1) * (k - 1)^m / 3 < s * A" by (simp add: A_def) from divide_strict_right_mono[OF this, of A] A0 have "2^(p - 1) * (k - 1)^m / 3 / A < s" by simp also have "2^(p - 1) * (k - 1)^m / 3 / A = 2^(p - 1) / (3 * L^2)" unfolding A_def using k2 by simp also have "\ = 2^p / (6 * L^2)" using p by (cases p, auto) also have "2^p = 2 powr p" by (simp add: powr_realpow) finally have *: "2 powr p / (6 * L\<^sup>2) < s" . have "m ^ l = m powr l" using m2 l2 powr_realpow by auto also have "\ = 2 powr (log 2 m * l)" unfolding powr_powr[symmetric] by (subst powr_log_cancel, insert m2, auto) also have "\ = 2 powr (l * log 2 m)" by (simp add: ac_simps) also have "\ \ 2 powr p" by (rule powr_mono, insert pllog, auto) finally have "m ^ l \ 2 powr p" . from divide_right_mono[OF this, of "6 * L\<^sup>2"] * have "m ^ l / (6 * L\<^sup>2) < s" by simp moreover have "((m - l) / k)^l / (6 * L^2) \ m^l / (6 * L^2)" proof (rule divide_right_mono, unfold of_nat_power, rule power_mono) have "real (m - l) / real k \ real (m - l) / 1" using k2 lm by (intro divide_left_mono, auto) also have "\ \ m" by simp finally show "(m - l) / k \ m" by simp qed auto ultimately show ?thesis by simp qed lemma identities: "k = root 4 m" "l = root 8 m" proof - let ?r = real have "?r k ^ 4 = ?r m" unfolding m_def by simp from arg_cong[OF this, of "root 4"] show km_id: "k = root 4 m" by (simp add: real_root_pos2) have "?r l ^ 8 = ?r m" unfolding m_def using kl2 by simp from arg_cong[OF this, of "root 8"] show lm_id: "l = root 8 m" by (simp add: real_root_pos2) qed lemma identities2: "root 4 m = m powr (1/4)" "root 8 m = m powr (1/8)" by (subst root_powr_inverse, insert m2, auto)+ lemma appendix_A_1: assumes "x \ M0'" shows "x powr (2/3) \ x powr (3/4) - 1" proof - have "(\ x. x powr (2/3) / (x powr (3/4) - 1)) \ 0" by real_asymp from LIMSEQ_D[OF this, of 1, simplified] obtain x0 :: nat where sub: "x \ x0 \ x powr (2 / 3) / \x powr (3/4) - 1\ < 1" for x by (auto simp: field_simps) have "(\ x :: real. 2 / (x powr (3/4))) \ 0" by real_asymp from LIMSEQ_D[OF this, of 1, simplified] obtain x1 :: nat where sub2: "x \ x1 \ 2 / x powr (3 / 4) < 1" for x by auto { fix x assume x: "x \ x0" "x \ x1" "x \ 1" define a where "a = x powr (3/4) - 1" from sub[OF x(1)] have small: "x powr (2 / 3) / \a\ \ 1" by (simp add: a_def) have 2: "2 \ x powr (3/4)" using sub2[OF x(2)] x(3) by simp hence a: "a > 0" by (simp add: a_def) from mult_left_mono[OF small, of a] a have "x powr (2 / 3) \ a" by (simp add: field_simps) hence "x powr (2 / 3) \ x powr (3 / 4) - 1" unfolding a_def by simp } hence "\ x0 :: nat. \ x \ x0. x powr (2 / 3) \ x powr (3 / 4) - 1" by (intro exI[of _ "max x0 (max x1 1)"], auto) from someI_ex[OF this, folded M0'_def, rule_format, OF assms] show ?thesis . qed lemma appendix_A_2: "(p - 1)^l < m powr ((1 / 8 + eps) * l)" proof - define f where "f (x :: nat) = (root 8 x * log 2 x + 1) / (x powr (1/8 + eps))" for x have "f \ 0" using eps unfolding f_def by real_asymp from LIMSEQ_D[OF this, of 1] have ex: "\ x. \ y. y \ x \ f y \ 1" by fastforce have lim: "root 8 m * log 2 m + 1 \ m powr (1 / 8 + eps)" using someI_ex[OF ex[unfolded f_def], folded M0_def, rule_format, OF M0] m2 by (simp add: field_simps) define start where "start = real (p - 1)^l" have "(p - 1)^l < p ^ l" by (rule power_strict_mono, insert p l2, auto) hence "start < real (p ^ l)" using start_def of_nat_less_of_nat_power_cancel_iff by blast also have "\ = p powr l" by (subst powr_realpow, insert p, auto) also have "\ \ (l * log 2 m + 1) powr l" by (rule powr_mono2, insert pllog, auto) also have "l = root 8 m" unfolding identities by simp finally have "start < (root 8 m * log 2 m + 1) powr root 8 m" by (simp add: identities2) also have "\ \ (m powr (1 / 8 + eps)) powr root 8 m" by (rule powr_mono2[OF _ _ lim], insert m2, auto) also have "\ = m powr ((1 / 8 + eps) * l)" unfolding powr_powr identities .. finally show ?thesis unfolding start_def by simp qed lemma appendix_A_3: "6 * real l^16 * fact l < m powr (1 / 8 * l)" proof - define f where "f = (\n. 6 * (real n)^16 * (sqrt (2 * pi * real n) * (real n / exp 1) ^ n))" define g where "g = (\ n. 6 * (real n)^16 * (sqrt (2 * 4 * real n) * (real n / 2) ^ n))" define h where "h = (\ n. ((real (n\<^sup>2 ^ 4) powr (1 / 8 * (real (n\<^sup>2 ^ 4)) powr (1/8)))))" have e: "2 \ (exp 1 :: real)" using exp_ge_add_one_self[of 1] by simp from fact_asymp_equiv have 1: "(\ n. 6 * (real n)^16 * fact n / h n) \[sequentially] (\ n. f n / h n)" unfolding f_def by (intro asymp_equiv_intros) have 2: "f n \ g n" for n unfolding f_def g_def by (intro mult_mono power_mono divide_left_mono real_sqrt_le_mono, insert pi_less_4 e, auto) have 2: "abs (f n / h n) \ abs (g n / h n)" for n unfolding abs_le_square_iff power2_eq_square by (intro mult_mono divide_right_mono 2, auto simp: h_def f_def g_def) have 2: "abs (g n / h n) < e \ abs (f n / h n) < e" for n e using 2[of n] by simp have "(\n. g n / h n) \ 0" unfolding g_def h_def by real_asymp from LIMSEQ_D[OF this] 2 have "(\n. f n / h n) \ 0" by (intro LIMSEQ_I, fastforce) with 1 have "(\n. 6 * (real n)^16 * fact n / h n) \ 0" using tendsto_asymp_equiv_cong by blast from LIMSEQ_D[OF this, of 1] obtain n0 where 3: "n \ n0 \ norm (6 * (real n)^16 * fact n / h n) < 1" for n by auto { fix n assume n: "n \ max 1 n0" hence hn: "h n > 0" unfolding h_def by auto from n have "n \ n0" by simp from 3[OF this] have "6 * n ^ 16 * fact n / abs (h n) < 1" by auto with hn have "6 * (real n) ^ 16 * fact n < h n" by simp } hence "\ n0. \ n. n \ n0 \ 6 * n ^ 16 * fact n < h n" by blast from someI_ex[OF this[unfolded h_def], folded L0'_def, rule_format, OF L0'] have "6 * real l^16 * fact l < real (l\<^sup>2 ^ 4) powr (1 / 8 * real (l\<^sup>2 ^ 4) powr (1 / 8))" by simp also have "\ = m powr (1 / 8 * l)" using identities identities2 kl2 by (metis m_def) finally show ?thesis . qed lemma appendix_A_4: "12 * L^2 \ m powr (m powr (1 / 8) * 0.51)" proof - let ?r = real define Lappr where "Lappr = m * m * fact l * p ^ l / 2" - have "L = (fact l * (p - 1) ^ l) + 1" unfolding L_def by simp - also have "\ \ (fact l * (p - 1) ^ l) + (fact l * (p - 1) ^ l)" - by (rule add_left_mono, insert l2 p, auto) - also have "\ = 2 * (fact l * (p - 1) ^ l)" by simp - finally have "real L \ real 2 * real (fact l * (p - 1) ^ l)" by linarith - also have "\ \ real (m * m div 2) * real (fact l * (p - 1) ^ l)" - by (rule mult_right_mono, insert m2, cases m, auto) - also have "\ \ (m * m / 2) * (fact l * (p - 1) ^ l)" - by (rule mult_right_mono, linarith+) - also have "\ = (m * m / 2 * fact l) * (?r (p - 1) ^ l)" by simp + have "L = (fact l * (p - 1) ^ l)" unfolding L_def by simp + hence "?r L \ (fact l * (p - 1) ^ l)" by linarith + also have "\ = (1 * ?r (fact l)) * (?r (p - 1) ^ l)" by simp + also have "\ \ ((m * m / 2) * ?r (fact l)) * (?r (p - 1) ^ l)" + by (intro mult_right_mono, insert m2, cases m; cases "m - 1", auto) also have "\ = (6 * real (m * m) * fact l) * (?r (p - 1) ^ l) / 12" by simp also have "real (m * m) = real l^16" unfolding m_def unfolding kl2 by simp also have "(6 * real l^16 * fact l) * (?r (p - 1) ^ l) / 12 \ (m powr (1 / 8 * l) * (m powr ((1 / 8 + eps) * l))) / 12" by (intro divide_right_mono mult_mono, insert appendix_A_2 appendix_A_3, auto) also have "\ = (m powr (1 / 8 * l + (1 / 8 + eps) * l)) / 12" by (simp add: powr_add) also have "1 / 8 * l + (1 / 8 + eps) * l = l * (1/4 + eps)" by (simp add: field_simps) also have "l = m powr (1/8)" unfolding identities identities2 .. finally have LL: "?r L \ m powr (m powr (1 / 8) * (1 / 4 + eps)) / 12" . from power_mono[OF this, of 2] have "L^2 \ (m powr (m powr (1 / 8) * (1 / 4 + eps)) / 12)^2" by simp also have "\ = (m powr (m powr (1 / 8) * (1 / 4 + eps)))^2 / 144" by (simp add: power2_eq_square) also have "\ = (m powr (m powr (1 / 8) * (1 / 4 + eps) * 2)) / 144" by (subst powr_realpow[symmetric], (use m2 in force), unfold powr_powr, simp) also have "\ = (m powr (m powr (1 / 8) * (1 / 2 + 2 * eps))) / 144" by (simp add: algebra_simps) also have "\ \ (m powr (m powr (1 / 8) * 0.51)) / 144" by (intro divide_right_mono powr_mono mult_left_mono, insert m2, auto simp: eps_def) finally have "L^2 \ m powr (m powr (1 / 8) * 0.51) / 144" by simp from mult_left_mono[OF this, of 12] have "12 * L^2 \ 12 * m powr (m powr (1 / 8) * 0.51) / 144" by simp also have "\ = m powr (m powr (1 / 8) * 0.51) / 12" by simp also have "\ \ m powr (m powr (1 / 8) * 0.51) / 1" by (rule divide_left_mono, auto) finally show ?thesis by simp qed lemma approximation4: fixes s :: nat assumes "s > ((m - l) / k)^l / (6 * L^2)" shows "s > 2 * k powr (4 / 7 * sqrt k)" proof - let ?r = real have diff: "?r (m - l) = ?r m - ?r l" using lm by simp have "m powr (2/3) \ m powr (3/4) - 1" using appendix_A_1[OF M0'] by auto also have "\ \ (m - m powr (1/8)) / m powr (1/4)" unfolding diff_divide_distrib by (rule diff_mono, insert m2, auto simp: divide_powr_uminus powr_mult_base powr_add[symmetric], auto simp: powr_minus_divide intro!: ge_one_powr_ge_zero) also have "\ = (m - root 8 m) / root 4 m" using m2 by (simp add: root_powr_inverse) also have "\ = (m - l) / k" unfolding identities diff by simp finally have "m powr (2/3) \ (m - l) / k" by simp from power_mono[OF this, of l] have ineq1: "(m powr (2 / 3)) ^ l \ ((m - l) / k) ^ l" using m2 by auto have "(m powr (l / 7)) \ (m powr (2 / 3 * l - l * 0.51))" by (intro powr_mono, insert m2, auto) also have "\ = (m powr (2 / 3)) powr l / (m powr (m powr (1 / 8) * 0.51))" unfolding powr_diff powr_powr identities identities2 by simp also have "\ = (m powr (2 / 3)) ^ l / (m powr (m powr (1 / 8) * 0.51))" by (subst powr_realpow, insert m2, auto) also have "\ \ (m powr (2 / 3)) ^ l / (12 * L\<^sup>2)" by (rule divide_left_mono[OF appendix_A_4], insert L3 m2, auto intro!: mult_pos_pos) also have "\ = (m powr (2 / 3)) ^ l / (?r 12 * L\<^sup>2)" by simp also have "\ \ ((m - l) / k) ^ l / (?r 12 * L\<^sup>2)" by (rule divide_right_mono[OF ineq1], insert L3, auto) also have "\ < s / 2" using assms by simp finally have "2 * m powr (real l / 7) < s" by simp also have "m powr (real l / 7) = m powr (root 8 m / 7)" unfolding identities by simp finally have "s > 2 * m powr (root 8 m / 7)" by simp also have "root 8 m = root 2 k" using m2 by (metis identities(2) kl2 of_nat_0_le_iff of_nat_power pos2 real_root_power_cancel) also have "?r m = k powr 4" unfolding m_def by simp also have "(k powr 4) powr ((root 2 k) / 7) = k powr (4 * (root 2 k) / 7)" unfolding powr_powr by simp also have "\ = k powr (4 / 7 * sqrt k)" unfolding sqrt_def by simp finally show "s > 2 * k powr (4 / 7 * sqrt k)" . qed end end \ No newline at end of file diff --git a/thys/Clique_and_Monotone_Circuits/Clique_Large_Monotone_Circuits.thy b/thys/Clique_and_Monotone_Circuits/Clique_Large_Monotone_Circuits.thy --- a/thys/Clique_and_Monotone_Circuits/Clique_Large_Monotone_Circuits.thy +++ b/thys/Clique_and_Monotone_Circuits/Clique_Large_Monotone_Circuits.thy @@ -1,1947 +1,1937 @@ theory Clique_Large_Monotone_Circuits imports Sunflowers.Erdos_Rado_Sunflower Preliminaries Assumptions_and_Approximations Monotone_Formula begin text \disable list-syntax\ no_syntax "_list" :: "args \ 'a list" ("[(_)]") no_syntax "__listcompr" :: "args \ 'a list" ("[(_)]") hide_const (open) Sigma_Algebra.measure subsection \Plain Graphs\ definition binprod :: "'a set \ 'a set \ 'a set set" (infixl "\" 60) where "X \ Y = {{x,y} | x y. x \ X \ y \ Y \ x \ y}" abbreviation sameprod :: "'a set \ 'a set set" ("(_)^\") where "X^\ \ X \ X" lemma sameprod_altdef: "X^\ = {Y. Y \ X \ card Y = 2}" unfolding binprod_def by (auto simp: card_2_iff) definition numbers :: "nat \ nat set" ("[(_)]") where "[n] \ {.. card (X^\) = card X choose 2" unfolding sameprod_altdef by (subst n_subsets, auto) lemma sameprod_mono: "X \ Y \ X^\ \ Y^\" unfolding sameprod_altdef by auto lemma sameprod_finite: "finite X \ finite (X^\)" unfolding sameprod_altdef by simp lemma numbers2_mono: "x \ y \ [x]^\ \ [y]^\" by (rule sameprod_mono, auto simp: numbers_def) lemma card_numbers[simp]: "card [n] = n" by (simp add: numbers_def) lemma card_numbers2[simp]: "card ([n]^\) = n choose 2" by (subst card_sameprod, auto simp: numbers_def) type_synonym vertex = nat type_synonym graph = "vertex set set" definition Graphs :: "vertex set \ graph set" where "Graphs V = { G. G \ V^\ }" definition Clique :: "vertex set \ nat \ graph set" where "Clique V k = { G. G \ Graphs V \ (\ C \ V. C^\ \ G \ card C = k) }" context first_assumptions begin abbreviation \ where "\ \ Graphs [m]" lemmas \_def = Graphs_def[of "[m]"] lemma empty_\[simp]: "{} \ \" unfolding \_def by auto definition v :: "graph \ vertex set" where "v G = { x . \ y. {x,y} \ G}" lemma v_union: "v (G \ H) = v G \ v H" unfolding v_def by auto definition \ :: "graph set" where "\ = { K . K \ \ \ card (v K) = k \ K = (v K)^\ }" lemma v_\: "G \ \ \ v G \ [m]" unfolding v_def \_def sameprod_altdef by auto lemma v_mono: "G \ H \ v G \ v H" unfolding v_def by auto lemma v_sameprod[simp]: assumes "card X \ 2" shows "v (X^\) = X" proof - from obtain_subset_with_card_n[OF assms] obtain Y where "Y \ X" and Y: "card Y = 2" by auto then obtain x y where "x \ X" "y \ X" and "x \ y" by (auto simp: card_2_iff) thus ?thesis unfolding sameprod_altdef v_def by (auto simp: card_2_iff doubleton_eq_iff) blast qed lemma v_mem_sub: assumes "card e = 2" "e \ G" shows "e \ v G" proof - obtain x y where e: "e = {x,y}" and xy: "x \ y" using assms by (auto simp: card_2_iff) from assms(2) have x: "x \ v G" unfolding e by (auto simp: v_def) from e have e: "e = {y,x}" unfolding e by auto from assms(2) have y: "y \ v G" unfolding e by (auto simp: v_def) show "e \ v G" using x y unfolding e by auto qed lemma v_\_2: assumes "G \ \" shows "G \ (v G)^\" proof fix e assume eG: "e \ G" with assms[unfolded \_def binprod_def] obtain x y where e: "e = {x,y}" and xy: "x \ y" by auto from eG e xy have x: "x \ v G" by (auto simp: v_def) from e have e: "e = {y,x}" unfolding e by auto from eG e xy have y: "y \ v G" by (auto simp: v_def) from x y xy show "e \ (v G)^\" unfolding binprod_def e by auto qed lemma v_numbers2[simp]: "x \ 2 \ v ([x]^\) = [x]" by (rule v_sameprod, auto) lemma sameprod_\: assumes "X \ [m]" "card X \ 2" shows "X^\ \ \" unfolding \_def using assms(2) sameprod_mono[OF assms(1)] by auto lemma finite_numbers[simp,intro]: "finite [n]" unfolding numbers_def by auto lemma finite_numbers2[simp,intro]: "finite ([n]^\)" unfolding sameprod_altdef using finite_subset[of _ "[m]"] by auto lemma finite_members_\: "G \ \ \ finite G" unfolding \_def using finite_subset[of G "[m]^\"] by auto lemma finite_\[simp,intro]: "finite \" unfolding \_def by simp lemma finite_vG: assumes "G \ \" shows "finite (v G)" proof - from finite_members_\[OF assms] show ?thesis proof (induct rule: finite_induct) case (insert xy F) show ?case proof (cases "\ x y. xy = {x,y}") case False hence "v (insert xy F) = v F" unfolding v_def by auto thus ?thesis using insert by auto next case True then obtain x y where xy: "xy = {x,y}" by auto hence "v (insert xy F) = insert x (insert y (v F))" unfolding v_def by auto thus ?thesis using insert by auto qed qed (auto simp: v_def) qed lemma v_empty[simp]: "v {} = {}" unfolding v_def by auto lemma v_card2: assumes "G \ \" "G \ {}" shows "2 \ card (v G)" proof - from assms[unfolded \_def] obtain edge where *: "edge \ G" "edge \ [m]^\" by auto then obtain x y where edge: "edge = {x,y}" "x \ y" unfolding binprod_def by auto with * have sub: "{x,y} \ v G" unfolding v_def by (smt (verit, best) insert_commute insert_compr mem_Collect_eq singleton_iff subsetI) from assms finite_vG have "finite (v G)" by auto from sub \x \ y\ this show "2 \ card (v G)" by (metis card_2_iff card_mono) qed lemma \_altdef: "\ = {V^\ | V. V \ [m] \ card V = k}" (is "_ = ?R") proof - { fix K assume "K \ \" hence K: "K \ \" and card: "card (v K) = k" and KvK: "K = (v K)^\" unfolding \_def by auto from v_\[OF K] card KvK have "K \ ?R" by auto } moreover { fix V assume 1: "V \ [m]" and "card V = k" hence "V^\ \ \" unfolding \_def using k2 sameprod_\[OF 1] by auto } ultimately show ?thesis by auto qed lemma \_\: "\ \ \" unfolding \_def by auto definition CLIQUE :: "graph set" where "CLIQUE = { G. G \ \ \ (\ K \ \. K \ G) }" lemma empty_CLIQUE[simp]: "{} \ CLIQUE" unfolding CLIQUE_def \_def using k2 by (auto simp: v_def) subsection \Test Graphs\ text \Positive test graphs are precisely the cliques of size @{term k}.\ abbreviation "POS \ \" lemma POS_\: "POS \ \" by (rule \_\) text \Negative tests are coloring-functions of vertices that encode graphs which have cliques of size at most @{term "k - 1"}.\ type_synonym colorf = "vertex \ nat" definition \ :: "colorf set" where "\ = [m] \\<^sub>E [k - 1]" lemma finite_\: "finite \" unfolding \_def numbers_def by (meson finite_PiE finite_lessThan) definition C :: "colorf \ graph" where "C f = { {x, y} | x y . {x,y} \ [m]^\ \ f x \ f y}" definition NEG :: "graph set" where "NEG = C ` \" paragraph \Lemma 1\ lemma CLIQUE_NEG: "CLIQUE \ NEG = {}" proof - { fix G assume GC: "G \ CLIQUE" and GN: "G \ NEG" from GC[unfolded CLIQUE_def] obtain K where K: "K \ \" and G: "G \ \" and KsubG: "K \ G" by auto from GN[unfolded NEG_def] obtain f where fF: "f \ \" and GCf: "G = C f" by auto from K[unfolded \_def] have KG: "K \ \" and KvK: "K = v K^\" and card1: "card (v K) = k" by auto from k2 card1 have ineq: "card (v K) > card [k - 1]" by auto from v_\[OF KG] have vKm: "v K \ [m]" by auto from fF[unfolded \_def] vKm have f: "f \ v K \ [k - 1]" by auto from card_inj[OF f] ineq have "\ inj_on f (v K)" by auto then obtain x y where *: "x \ v K" "y \ v K" "x \ y" and ineq: "f x = f y" unfolding inj_on_def by auto have "{x,y} \ G" unfolding GCf C_def using ineq by (auto simp: doubleton_eq_iff) with KsubG KvK have "{x,y} \ v K^\" by auto with * have False unfolding binprod_def by auto } thus ?thesis by auto qed lemma NEG_\: "NEG \ \" proof - { fix f assume "f \ \" hence "C f \ \" unfolding NEG_def C_def \_def by (auto simp: sameprod_altdef) } thus "NEG \ \" unfolding NEG_def by auto qed lemma finite_POS_NEG: "finite (POS \ NEG)" using POS_\ NEG_\ by (intro finite_subset[OF _ finite_\], auto) lemma POS_sub_CLIQUE: "POS \ CLIQUE" unfolding CLIQUE_def using \_\ by auto lemma POS_CLIQUE: "POS \ CLIQUE" proof - have "[k+1]^\ \ CLIQUE" unfolding CLIQUE_def proof (standard, intro conjI bexI[of _ "[k]^\"]) show "[k]^\ \ [k+1]^\" by (rule numbers2_mono, auto) show "[k]^\ \ \" unfolding \_altdef using km by (auto intro!: exI[of _ "[k]"], auto simp: numbers_def) show "[k+1]^\ \ \" using km k2 by (intro sameprod_\, auto simp: numbers_def) qed moreover have "[k+1]^\ \ POS" unfolding \_def using v_numbers2[of "k + 1"] k2 by auto ultimately show ?thesis using POS_sub_CLIQUE by blast qed lemma card_POS: "card POS = m choose k" proof - have "m choose k = card {B. B \ [m] \ card B = k}" (is "_ = card ?A") by (subst n_subsets[of "[m]" k], auto simp: numbers_def) also have "\ = card (sameprod ` ?A)" proof (rule card_image[symmetric]) { fix A assume "A \ ?A" hence "v (sameprod A) = A" using k2 by (subst v_sameprod, auto) } thus "inj_on sameprod ?A" by (rule inj_on_inverseI) qed also have "sameprod ` {B. B \ [m] \ card B = k} = POS" unfolding \_altdef by auto finally show ?thesis by simp qed subsection \Basic operations on sets of graphs\ definition odot :: "graph set \ graph set \ graph set" (infixl "\" 65) where "X \ Y = { D \ E | D E. D \ X \ E \ Y}" lemma union_\[intro]: "G \ \ \ H \ \ \ G \ H \ \" unfolding \_def by auto lemma odot_\: "X \ \ \ Y \ \ \ X \ Y \ \" unfolding odot_def by auto subsection \Acceptability\ text \Definition 2\ definition accepts :: "graph set \ graph \ bool" (infixl "\" 55) where "(X \ G) = (\ D \ X. D \ G)" lemma acceptsI[intro]: "D \ G \ D \ X \ X \ G" unfolding accepts_def by auto definition ACC :: "graph set \ graph set" where "ACC X = { G. G \ \ \ X \ G}" definition ACC_cf :: "graph set \ colorf set" where "ACC_cf X = { F. F \ \ \ X \ C F}" lemma ACC_cf_\: "ACC_cf X \ \" unfolding ACC_cf_def by auto lemma finite_ACC[intro,simp]: "finite (ACC_cf X)" by (rule finite_subset[OF ACC_cf_\ finite_\]) lemma ACC_I[intro]: "G \ \ \ X \ G \ G \ ACC X" unfolding ACC_def by auto lemma ACC_cf_I[intro]: "F \ \ \ X \ C F \ F \ ACC_cf X" unfolding ACC_cf_def by auto lemma ACC_cf_mono: "X \ Y \ ACC_cf X \ ACC_cf Y" unfolding ACC_cf_def accepts_def by auto text \Lemma 3\ lemma ACC_cf_empty: "ACC_cf {} = {}" unfolding ACC_cf_def accepts_def by auto lemma ACC_empty[simp]: "ACC {} = {}" unfolding ACC_def accepts_def by auto lemma ACC_cf_union: "ACC_cf (X \ Y) = ACC_cf X \ ACC_cf Y" unfolding ACC_cf_def accepts_def by blast lemma ACC_union: "ACC (X \ Y) = ACC X \ ACC Y" unfolding ACC_def accepts_def by blast lemma ACC_odot: "ACC (X \ Y) = ACC X \ ACC Y" proof - { fix G assume "G \ ACC (X \ Y)" from this[unfolded ACC_def accepts_def] obtain D E F :: graph where *: "D \ X" "E \ Y" "G \ \" "D \ E \ G" by (force simp: odot_def) hence "G \ ACC X \ ACC Y" unfolding ACC_def accepts_def by auto } moreover { fix G assume "G \ ACC X \ ACC Y" from this[unfolded ACC_def accepts_def] obtain D E where *: "D \ X" "E \ Y" "G \ \" "D \ G" "E \ G" by auto let ?F = "D \ E" from * have "?F \ X \ Y" unfolding odot_def using * by blast moreover have "?F \ G" using * by auto ultimately have "G \ ACC (X \ Y)" using * unfolding ACC_def accepts_def by blast } ultimately show ?thesis by blast qed lemma ACC_cf_odot: "ACC_cf (X \ Y) = ACC_cf X \ ACC_cf Y" proof - { fix G assume "G \ ACC_cf (X \ Y)" from this[unfolded ACC_cf_def accepts_def] obtain D E :: graph where *: "D \ X" "E \ Y" "G \ \" "D \ E \ C G" by (force simp: odot_def) hence "G \ ACC_cf X \ ACC_cf Y" unfolding ACC_cf_def accepts_def by auto } moreover { fix F assume "F \ ACC_cf X \ ACC_cf Y" from this[unfolded ACC_cf_def accepts_def] obtain D E where *: "D \ X" "E \ Y" "F \ \" "D \ C F" "E \ C F" by auto let ?F = "D \ E" from * have "?F \ X \ Y" unfolding odot_def using * by blast moreover have "?F \ C F" using * by auto ultimately have "F \ ACC_cf (X \ Y)" using * unfolding ACC_cf_def accepts_def by blast } ultimately show ?thesis by blast qed subsection \Approximations and deviations\ definition \l :: "graph set" where "\l = { G. G \ \ \ card (v G) \ l }" definition v_gs :: "graph set \ vertex set set" where "v_gs X = v ` X" lemma v_gs_empty[simp]: "v_gs {} = {}" unfolding v_gs_def by auto lemma v_gs_union: "v_gs (X \ Y) = v_gs X \ v_gs Y" unfolding v_gs_def by auto lemma v_gs_mono: "X \ Y \ v_gs X \ v_gs Y" using v_gs_def by auto lemma finite_v_gs: assumes "X \ \" shows "finite (v_gs X)" proof - have "v_gs X \ v ` \" using assms unfolding v_gs_def by force moreover have "finite \" using finite_\ by auto ultimately show ?thesis by (metis finite_surj) qed lemma finite_v_gs_Gl: assumes "X \ \l" shows "finite (v_gs X)" by (rule finite_v_gs, insert assms, auto simp: \l_def) definition \

L\l :: "graph set set" where "\

L\l = { X . X \ \l \ card (v_gs X) \ L}" definition odotl :: "graph set \ graph set \ graph set" (infixl "\l" 65) where - "X \l Y = {D \ E | D E. D \ X \ E \ Y \ D \ E \ \l}" + "X \l Y = (X \ Y) \ \l" lemma joinl_join: "X \l Y \ X \ Y" unfolding odot_def odotl_def by blast lemma card_v_gs_join: assumes X: "X \ \" and Y: "Y \ \" and Z: "Z \ X \ Y" shows "card (v_gs Z) \ card (v_gs X) * card (v_gs Y)" proof - note fin = finite_v_gs[OF X] finite_v_gs[OF Y] have "card (v_gs Z) \ card ((\ (A, B). A \ B) ` (v_gs X \ v_gs Y))" proof (rule card_mono[OF finite_imageI]) show "finite (v_gs X \ v_gs Y)" using fin by auto have "v_gs Z \ v_gs (X \ Y)" using v_gs_mono[OF Z] . also have "\ \ (\(x, y). x \ y) ` (v_gs X \ v_gs Y)" (is "?L \ ?R") unfolding odot_def v_gs_def by (force split: if_splits simp: v_union) finally show "v_gs Z \ (\(x, y). x \ y) ` (v_gs X \ v_gs Y)" . qed also have "\ \ card (v_gs X \ v_gs Y)" by (rule card_image_le, insert fin, auto) also have "\ = card (v_gs X) * card (v_gs Y)" by (rule card_cartesian_product) finally show ?thesis . qed text \Definition 6 -- elementary plucking step\ definition plucking_step :: "graph set \ graph set" where "plucking_step X = (let vXp = v_gs X; S = (SOME S. S \ vXp \ sunflower S \ card S = p); U = {E \ X. v E \ S}; Vs = \ S; Gs = Vs^\ in X - U \ {Gs})" end context second_assumptions begin text \Lemma 9 -- for elementary plucking step\ lemma v_sameprod_subset: "v (Vs^\) \ Vs" unfolding binprod_def v_def by (auto simp: doubleton_eq_iff) lemma plucking_step: assumes X: "X \ \l" and L: "card (v_gs X) > L" and Y: "Y = plucking_step X" shows "card (v_gs Y) \ card (v_gs X) - p + 1" "Y \ \l" "POS \ ACC X \ ACC Y" "2 ^ p * card (ACC_cf Y - ACC_cf X) \ (k - 1) ^ m" "Y \ {}" proof - let ?vXp = "v_gs X" have sf_precond: "\A\ ?vXp. finite A \ card A \ l" using X unfolding \l_def \l_def v_gs_def by (auto intro: finite_vG intro!: v_\ v_card2) note sunflower = Erdos_Rado_sunflower[OF sf_precond] from p have p0: "p \ 0" by auto have "(p - 1) ^ l * fact l < card ?vXp" using L[unfolded L_def] by (simp add: ac_simps) note sunflower = sunflower[OF this] define S where "S = (SOME S. S \ ?vXp \ sunflower S \ card S = p)" define U where "U = {E \ X. v E \ S}" define Vs where "Vs = \ S" define Gs where "Gs = Vs^\" let ?U = U let ?New = "Gs :: graph" have Y: "Y = X - U \ {?New}" using Y[unfolded plucking_step_def Let_def, folded S_def, folded U_def, folded Vs_def, folded Gs_def] . have U: "U \ \l" using X unfolding U_def by auto hence "U \ \" unfolding \l_def by auto from sunflower have "\ S. S \ ?vXp \ sunflower S \ card S = p" by auto from someI_ex[OF this, folded S_def] have S: "S \ ?vXp" "sunflower S" "card S = p" by (auto simp: Vs_def) have fin1: "finite ?vXp" using finite_v_gs_Gl[OF X] . from X have finX: "finite X" unfolding \l_def using finite_subset[of X, OF _ finite_\] by auto from fin1 S have finS: "finite S" by (metis finite_subset) from finite_subset[OF _ finX] have finU: "finite U" unfolding U_def by auto from S p have Snempty: "S \ {}" by auto have UX: "U \ X" unfolding U_def by auto { from Snempty obtain s where sS: "s \ S" by auto with S have "s \ v_gs X" by auto then obtain Sp where "Sp \ X" and sSp: "s = v Sp" unfolding v_gs_def by auto hence *: "Sp \ U" using \s \ S\ unfolding U_def by auto from * X UX have le: "card (v Sp) \ l" "finite (v Sp)" "Sp \ \" unfolding \l_def \l_def using finite_vG[of Sp] by auto hence m: "v Sp \ [m]" by (intro v_\) have "Vs \ v Sp" using sS sSp unfolding Vs_def by auto with card_mono[OF \finite (v Sp)\ this] finite_subset[OF this \finite (v Sp)\] le * m have "card Vs \ l" "U \ {}" "finite Vs" "Vs \ [m]" by auto } hence card_Vs: "card Vs \ l" and Unempty: "U \ {}" and fin_Vs: "finite Vs" and Vsm: "Vs \ [m]" by auto have vGs: "v Gs \ Vs" unfolding Gs_def by (rule v_sameprod_subset) have GsG: "Gs \ \" unfolding Gs_def \_def by (intro CollectI Inter_subset sameprod_mono Vsm) have GsGl: "Gs \ \l" unfolding \l_def using GsG vGs card_Vs card_mono[OF _ vGs] by (simp add: fin_Vs) hence DsDl: "?New \ \l" using UX unfolding \l_def \_def \l_def \_def by auto with X U show "Y \ \l" unfolding Y by auto from X have XD: "X \ \" unfolding \l_def by auto have vplus_dsU: "v_gs U = S" using S(1) unfolding v_gs_def U_def by force have vplus_dsXU: "v_gs (X - U) = v_gs X - v_gs U" unfolding v_gs_def U_def by auto have "card (v_gs Y) = card (v_gs (X - U \ {?New}))" unfolding Y by simp also have "v_gs (X - U \ {?New}) = v_gs (X - U) \ v_gs ({?New})" unfolding v_gs_union .. also have "v_gs ({?New}) = {v (Gs)}" unfolding v_gs_def image_comp o_def by simp also have "card (v_gs (X - U) \ \) \ card (v_gs (X - U)) + card \" by (rule card_Un_le) also have "\ \ card (v_gs (X - U)) + 1" by auto also have "v_gs (X - U) = v_gs X - v_gs U" by fact also have "card \ = card (v_gs X) - card (v_gs U)" by (rule card_Diff_subset, force simp: vplus_dsU finS, insert UX, auto simp: v_gs_def) also have "card (v_gs U) = card S" unfolding vplus_dsU .. finally show "card (v_gs Y) \ card (v_gs X) - p + 1" using S by auto show "Y \ {}" unfolding Y using Unempty by auto { fix G assume "G \ ACC X" and GPOS: "G \ POS" from this[unfolded ACC_def] POS_\ have G: "G \ \" "X \ G" by auto from this[unfolded accepts_def] obtain D :: graph where D: "D \ X" "D \ G" by auto have "G \ ACC Y" proof (cases "D \ Y") case True with D G show ?thesis unfolding accepts_def ACC_def by auto next case False with D have DU: "D \ U" unfolding Y by auto from GPOS[unfolded POS_def \_def] obtain K where GK: "G = (v K)^\" "card (v K) = k" by auto from DU[unfolded U_def] have "v D \ S" by auto hence "Vs \ v D" unfolding Vs_def by auto also have "\ \ v G" by (intro v_mono D) also have "\ = v K" unfolding GK by (rule v_sameprod, unfold GK, insert k2, auto) finally have "Gs \ G" unfolding Gs_def GK by (intro sameprod_mono) with D DU have "D \ ?U" "?New \ G" by (auto) hence "Y \ G" unfolding accepts_def Y by auto thus ?thesis using G by auto qed } thus "POS \ ACC X \ ACC Y" by auto from ex_bij_betw_nat_finite[OF finS, unfolded \card S = p\] obtain Si where Si: "bij_betw Si {0 ..< p} S" by auto define G where "G = (\ i. SOME Gb. Gb \ X \ v Gb = Si i)" { fix i assume "i < p" with Si have SiS: "Si i \ S" unfolding bij_betw_def by auto with S have "Si i \ v_gs X" by auto hence "\ G. G \ X \ v G = Si i" unfolding v_gs_def by auto from someI_ex[OF this] have "(G i) \ X \ v (G i) = Si i" unfolding G_def by blast hence "G i \ X" "v (G i) = Si i" "G i \ U" "v (G i) \ S" using SiS unfolding U_def by auto } note G = this have SvG: "S = v ` G ` {0 ..< p}" unfolding Si[unfolded bij_betw_def, THEN conjunct2, symmetric] image_comp o_def using G(2) by auto have injG: "inj_on G {0 ..< p}" proof (standard, goal_cases) case (1 i j) hence "Si i = Si j" using G[of i] G[of j] by simp with 1(1,2) Si show "i = j" by (metis Si bij_betw_iff_bijections) qed define r where "r = card U" have rq: "r \ p" unfolding r_def \card S = p\[symmetric] vplus_dsU[symmetric] unfolding v_gs_def by (rule card_image_le[OF finU]) let ?Vi = "\ i. v (G i)" let ?Vis = "\ i. ?Vi i - Vs" define s where "s = card Vs" define si where "si i = card (?Vi i)" for i define ti where "ti i = card (?Vis i)" for i { fix i assume i: "i < p" have Vs_Vi: "Vs \ ?Vi i" using i unfolding Vs_def using G[OF i] unfolding SvG by auto have finVi: "finite (?Vi i)" using G(4)[OF i] S(1) sf_precond by (meson finite_numbers finite_subset subset_eq) from S(1) have "G i \ \" using G(1)[OF i] X unfolding \l_def \_def \l_def by auto hence finGi: "finite (G i)" using finite_members_\ by auto have ti: "ti i = si i - s" unfolding ti_def si_def s_def by (rule card_Diff_subset[OF fin_Vs Vs_Vi]) have size1: "s \ si i" unfolding s_def si_def by (intro card_mono finVi Vs_Vi) have size2: "si i \ l" unfolding si_def using G(4)[OF i] S(1) sf_precond by auto note Vs_Vi finVi ti size1 size2 finGi \G i \ \\ } note i_props = this define fstt where "fstt e = (SOME x. x \ e \ x \ Vs)" for e define sndd where "sndd e = (SOME x. x \ e \ x \ fstt e)" for e { fix e :: "nat set" assume *: "card e = 2" "\ e \ Vs" from *(1) obtain x y where e: "e = {x,y}" "x \ y" by (meson card_2_iff) with * have "\ x. x \ e \ x \ Vs" by auto from someI_ex[OF this, folded fstt_def] have fst: "fstt e \ e" "fstt e \ Vs" by auto with * e have "\ x. x \ e \ x \ fstt e" by (metis insertCI) from someI_ex[OF this, folded sndd_def] have snd: "sndd e \ e" "sndd e \ fstt e" by auto from fst snd e have "{fstt e, sndd e} = e" "fstt e \ Vs" "fstt e \ sndd e" by auto } note fstt = this { fix f assume "f \ ACC_cf Y - ACC_cf X" hence fake: "f \ ACC_cf {?New} - ACC_cf U" unfolding Y ACC_cf_def accepts_def Diff_iff U_def Un_iff mem_Collect_eq by blast hence f: "f \ \" using ACC_cf_\ by auto hence "C f \ NEG" unfolding NEG_def by auto with NEG_\ have Cf: "C f \ \" by auto from fake have "f \ ACC_cf {?New}" by auto from this[unfolded ACC_cf_def accepts_def] Cf have GsCf: "Gs \ C f" and Cf: "C f \ \" by auto from fake have "f \ ACC_cf U" by auto from this[unfolded ACC_cf_def] Cf f have "\ (U \ C f)" by auto from this[unfolded accepts_def] have UCf: "D \ U \ \ D \ C f" for D by auto - { - fix x y - assume xy: "{x,y} \ Gs" - with GsG have mem: "{x,y} \ [m]^\" unfolding \_def by auto - from xy have "{x,y} \ C f" using GsCf by auto - hence "f x \ f y" using mem unfolding C_def - by (auto simp: doubleton_eq_iff) - } note Gs_f = this let ?prop = "\ i e. fstt e \ v (G i) - Vs \ sndd e \ v (G i) \ e \ G i \ ([m]^\) \ f (fstt e) = f (sndd e) \ f (sndd e) \ [k - 1] \ {fstt e, sndd e} = e" define pair where "pair i = (if i < p then (SOME pair. ?prop i pair) else undefined)" for i define u where "u i = fstt (pair i)" for i define w where "w i = sndd (pair i)" for i { fix i assume i: "i < p" from i have "?Vi i \ S" unfolding SvG by auto hence "Vs \ ?Vi i" unfolding Vs_def by auto from sameprod_mono[OF this, folded Gs_def] have *: "Gs \ v (G i)^\" . from i have Gi: "G i \ U" using G[OF i] by auto from UCf[OF Gi] i_props[OF i] have "\ G i \ C f" and Gi: "G i \ \" by auto then obtain edge where edgep: "edge \ G i" and edgen: "edge \ C f" by auto from edgep Gi obtain x y where edge: "edge = {x,y}" and xy: "{x,y} \ [m]^\" "{x,y} \ [m]" "card {x,y} = 2" unfolding \_def binprod_def by force define a where "a = fstt edge" define b where "b = sndd edge" from edgen[unfolded C_def edge] xy have id: "f x = f y" by simp from edgen GsCf edge have edgen: "{x,y} \ Gs" by auto from edgen[unfolded Gs_def sameprod_altdef] xy have "\ {x,y} \ Vs" by auto from fstt[OF \card {x,y} = 2\ this, folded edge, folded a_def b_def] edge have a: "a \ Vs" and id_ab: "{x,y} = {a,b}" by auto from id_ab id have id: "f a = f b" by (auto simp: doubleton_eq_iff) let ?pair = "(a,b)" note ab = xy[unfolded id_ab] from f[unfolded \_def] ab have fb: "f b \ [k - 1]" by auto note edge = edge[unfolded id_ab] from edgep[unfolded edge] v_mem_sub[OF \card {a,b} = 2\, of "G i"] id have "?prop i edge" using edge ab a fb unfolding a_def b_def by auto from someI[of "?prop i", OF this] have "?prop i (pair i)" using i unfolding pair_def by auto from this[folded u_def w_def] edgep have "u i \ v (G i) - Vs" "w i \ v (G i)" "pair i \ G i \ [m]^\" "f (u i) = f (w i)" "f (w i) \ [k - 1]" "pair i = {u i, w i}" by auto } note uw = this from uw(3) have Pi: "pair \ Pi\<^sub>E {0 ..< p} G" unfolding pair_def by auto define Us where "Us = u ` {0 ..< p}" define Ws where "Ws = [m] - Us" { fix i assume i: "i < p" note uwi = uw[OF this] from uwi have ex: "\ x \ [k - 1]. f ` {u i, w i} = {x}" by auto from uwi have *: "u i \ [m]" "w i \ [m]" "{u i, w i} \ G i" by (auto simp: sameprod_altdef) have "w i \ Us" proof assume "w i \ Us" then obtain j where j: "j < p" and wij: "w i = u j" unfolding Us_def by auto with uwi have ij: "i \ j" unfolding binprod_def by auto note uwj = uw[OF j] from ij i j Si[unfolded bij_betw_def] have diff: "v (G i) \ v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto from uwi wij have uj: "u j \ v (G i)" by auto with \sunflower S\[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uwj(1) diff have "u j \ \ S" by blast with uwj(1)[unfolded Vs_def] show False by simp qed with * have wi: "w i \ Ws" unfolding Ws_def by auto from uwi have wi2: "w i \ v (G i)" by auto define W where "W = Ws \ v (G i)" from G(1)[OF i] X[unfolded \l_def \l_def] i_props[OF i] have "finite (v (G i))" "card (v (G i)) \ l" by auto with card_mono[OF this(1), of W] have W: "finite W" "card W \ l" "W \ [m] - Us" unfolding W_def Ws_def by auto from wi wi2 have wi: "w i \ W" unfolding W_def by auto from wi ex W * have "{u i, w i} \ G i \ u i \ [m] \ w i \ [m] - Us \ f (u i) = f (w i)" by force } note uw1 = this have inj: "inj_on u {0 ..< p}" proof - { fix i j assume i: "i < p" and j: "j < p" and id: "u i = u j" and ij: "i \ j" from ij i j Si[unfolded bij_betw_def] have diff: "v (G i) \ v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto from uw[OF i] have ui: "u i \ v (G i) - Vs" by auto from uw[OF j, folded id] have uj: "u i \ v (G j)" by auto with \sunflower S\[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uw[OF i] diff have "u i \ \ S" by blast with ui have False unfolding Vs_def by auto } thus ?thesis unfolding inj_on_def by fastforce qed have card: "card ([m] - Us) = m - p" proof (subst card_Diff_subset) show "finite Us" unfolding Us_def by auto show "Us \ [m]" unfolding Us_def using uw1 by auto have "card Us = p" unfolding Us_def using inj by (simp add: card_image) thus "card [m] - card Us = m - p" by simp qed hence "(\ i < p. pair i \ G i) \ inj_on u {0 ..< p} \ (\ i < p. w i \ [m] - u ` {0 ..< p} \ f (u i) = f (w i))" using inj uw1 uw unfolding Us_def by auto from this[unfolded u_def w_def] Pi card[unfolded Us_def u_def w_def] have "\ e \ Pi\<^sub>E {0..i G i) \ card ([m] - (\i. fstt (e i)) ` {0.. (\i [m] - (\i. fstt (e i)) ` {0.. f (fstt (e i)) = f (sndd (e i)))" by blast } note fMem = this define Pi2 where "Pi2 W = Pi\<^sub>E ([m] - W) (\ _. [k - 1])" for W define merge where "merge = (\ e (g :: nat \ nat) v. if v \ (\ i. fstt (e i)) ` {0 ..< p} then g (sndd (e (SOME i. i < p \ v = fstt (e i)))) else g v)" let ?W = "\ e. (\ i. fstt (e i)) ` {0.. { merge e g | e g. e \ Pi\<^sub>E {0.. card ([m] - ?W e) = m - p \ g \ Pi2 (?W e)}" (is "_ \ ?R") proof fix f assume mem: "f \ ACC_cf Y - ACC_cf X" with ACC_cf_\ have "f \ \" by auto hence f: "f \ [m] \\<^sub>E [k - 1]" unfolding \_def . from fMem[OF mem] obtain e where e: "e \ Pi\<^sub>E {0.. i. i

e i \ G i" "card ([m] - ?W e) = m - p" "\ i. i

sndd (e i) \ [m] - ?W e \ f (fstt (e i)) = f (sndd (e i))" by auto define W where "W = ?W e" note e = e[folded W_def] let ?g = "restrict f ([m] - W)" let ?h = "merge e ?g" have "f \ ?R" proof (intro CollectI exI[of _ e] exI[of _ ?g], unfold W_def[symmetric], intro conjI e) show "?g \ Pi2 W" unfolding Pi2_def using f by auto { fix v :: nat have "?h v = f v" proof (cases "v \ W") case False thus ?thesis using f unfolding merge_def unfolding W_def[symmetric] by auto next case True from this[unfolded W_def] obtain i where i: "i < p" and v: "v = fstt (e i)" by auto define j where "j = (SOME j. j < p \ v = fstt (e j))" from i v have "\ j. j < p \ v = fstt (e j)" by auto from someI_ex[OF this, folded j_def] have j: "j < p" and v: "v = fstt (e j)" by auto have "?h v = restrict f ([m] - W) (sndd (e j))" unfolding merge_def unfolding W_def[symmetric] j_def using True by auto also have "\ = f (sndd (e j))" using e(4)[OF j] by auto also have "\ = f (fstt (e j))" using e(4)[OF j] by auto also have "\ = f v" using v by simp finally show ?thesis . qed } thus "f = ?h" by auto qed thus "f \ ?R" by auto qed also have "\ \ (\ (e,g). (merge e g)) ` (Sigma (Pi\<^sub>E {0.. {e. card ([m] - ?W e) = m - p}) (\ e. Pi2 (?W e)))" (is "_ \ ?f ` ?R") by auto finally have sub: "ACC_cf Y - ACC_cf X \ ?f ` ?R" . have fin[simp,intro]: "finite [m]" "finite [k - Suc 0]" unfolding numbers_def by auto have finPie[simp, intro]: "finite (Pi\<^sub>E {0.. card (?f ` ?R)" by (rule card_mono[OF finite_imageI[OF finR] sub]) also have "\ \ card ?R" by (rule card_image_le[OF finR]) also have "\ = (\e\(Pi\<^sub>E {0.. {e. card ([m] - ?W e) = m - p}). card (Pi2 (?W e)))" by (rule card_SigmaI, unfold Pi2_def, (intro finite_SigmaI allI finite_Int finite_PiE i_props, auto)+) also have "\ = (\e\Pi\<^sub>E {0.. {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (card ([m] - ?W e)))" by (rule sum.cong[OF refl], unfold Pi2_def, subst card_PiE, auto) also have "\ = (\e\Pi\<^sub>E {0.. {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (m - p))" by (rule sum.cong[OF refl], rule arg_cong[of _ _ "\ n. (k - 1)^n"], auto) also have "\ \ (\e\Pi\<^sub>E {0.. = card (Pi\<^sub>E {0.. = (\i = 0.. \ (\i = 0.. \" unfolding \l_def \_def \_def sameprod_altdef by force from i_props[OF i] have finGi: "finite (G i)" by auto have finvGi: "finite (v (G i))" by (rule finite_vG, insert i_props[OF i], auto) have "card (G i) \ card ((v (G i))^\)" by (intro card_mono[OF sameprod_finite], rule finvGi, rule v_\_2[OF GiG]) also have "\ \ l choose 2" proof (subst card_sameprod[OF finvGi], rule choose_mono) show "card (v (G i)) \ l" using i_props[OF i] unfolding ti_def si_def by simp qed also have "l choose 2 = l * (l - 1) div 2" unfolding choose_two by simp also have "l * (l - 1) = k - l" unfolding kl2 power2_eq_square by (simp add: algebra_simps) also have "\ div 2 \ (k - 1) div 2" by (rule div_le_mono, insert l2, auto) finally have "card (G i) \ (k - 1) div 2" . } thus ?thesis by (intro mult_right_mono prod_mono, auto) qed also have "\ = ((k - 1) div 2) ^ p * (k - 1) ^ (m - p)" by simp also have "\ \ ((k - 1) ^ p div (2^p)) * (k - 1) ^ (m - p)" by (rule mult_right_mono; auto simp: div_mult_pow_le) also have "\ \ ((k - 1) ^ p * (k - 1) ^ (m - p)) div 2^p" by (rule div_mult_le) also have "\ = (k - 1)^m div 2^p" proof - have "p + (m - p) = m" using mp by simp thus ?thesis by (subst power_add[symmetric], simp) qed finally have "card (ACC_cf Y - ACC_cf X) \ (k - 1) ^ m div 2 ^ p" . hence "2 ^ p * card (ACC_cf Y - ACC_cf X) \ 2^p * ((k - 1) ^ m div 2 ^ p)" by simp also have "\ \ (k - 1)^m" by simp finally show "2^p * card (ACC_cf Y - ACC_cf X) \ (k - 1) ^ m" . qed text \Definition 6\ function PLU_main :: "graph set \ graph set \ nat" where "PLU_main X = (if X \ \l \ L < card (v_gs X) then map_prod id Suc (PLU_main (plucking_step X)) else (X, 0))" by pat_completeness auto termination proof (relation "measure (\ X. card (v_gs X))", force, goal_cases) case (1 X) hence "X \ \l" and LL: "L < card (v_gs X)" by auto from plucking_step(1)[OF this refl] have "card (v_gs (plucking_step X)) \ card (v_gs X) - p + 1" . also have "\ < card (v_gs X)" using p L3 LL by auto finally show ?case by simp qed declare PLU_main.simps[simp del] definition PLU :: "graph set \ graph set" where "PLU X = fst (PLU_main X)" text \Lemma 7\ lemma PLU_main_n: assumes "X \ \l" and "PLU_main X = (Z, n)" shows "n * (p - 1) \ card (v_gs X)" using assms proof (induct X arbitrary: Z n rule: PLU_main.induct) case (1 X Z n) note [simp] = PLU_main.simps[of X] show ?case proof (cases "card (v_gs X) \ L") case True thus ?thesis using 1 by auto next case False define Y where "Y = plucking_step X" obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q" using \PLU_main X = (Z,n)\[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto) from False have L: "card (v_gs X) > L" by auto note step = plucking_step[OF 1(2) this Y_def] from False 1 have "X \ \l \ L < card (v_gs X)" by auto note IH = 1(1)[folded Y_def, OF this step(2) PLU] have "n * (p - 1) = (p - 1) + q * (p - 1)" unfolding n by simp also have "\ \ (p - 1) + card (v_gs Y)" using IH by simp also have "\ \ p - 1 + (card (v_gs X) - p + 1)" using step(1) by simp also have "\ = card (v_gs X)" using L Lp p by simp finally show ?thesis . qed qed text \Definition 8\ definition sqcup :: "graph set \ graph set \ graph set" (infixl "\" 65) where "X \ Y = PLU (X \ Y)" definition sqcap :: "graph set \ graph set \ graph set" (infixl "\" 65) where "X \ Y = PLU (X \l Y)" definition deviate_pos_cup :: "graph set \ graph set \ graph set" ("\\Pos") where "\\Pos X Y = POS \ ACC (X \ Y) - ACC (X \ Y)" definition deviate_pos_cap :: "graph set \ graph set \ graph set" ("\\Pos") where "\\Pos X Y = POS \ ACC (X \ Y) - ACC (X \ Y)" definition deviate_neg_cup :: "graph set \ graph set \ colorf set" ("\\Neg") where "\\Neg X Y = ACC_cf (X \ Y) - ACC_cf (X \ Y)" definition deviate_neg_cap :: "graph set \ graph set \ colorf set" ("\\Neg") where "\\Neg X Y = ACC_cf (X \ Y) - ACC_cf (X \ Y)" text \Lemma 9 -- without applying Lemma 7\ lemma PLU_main: assumes "X \ \l" and "PLU_main X = (Z, n)" shows "Z \ \

L\l \ (Z = {} \ X = {}) \ POS \ ACC X \ ACC Z \ 2 ^ p * card (ACC_cf Z - ACC_cf X) \ (k - 1) ^ m * n" using assms proof (induct X arbitrary: Z n rule: PLU_main.induct) case (1 X Z n) note [simp] = PLU_main.simps[of X] show ?case proof (cases "card (v_gs X) \ L") case True from True show ?thesis using 1 by (auto simp: id \

L\l_def) next case False define Y where "Y = plucking_step X" obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q" using \PLU_main X = (Z,n)\[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto) from False have "card (v_gs X) > L" by auto note step = plucking_step[OF 1(2) this Y_def] from False 1 have "X \ \l \ L < card (v_gs X)" by auto note IH = 1(1)[folded Y_def, OF this step(2) PLU] \Y \ {}\ let ?Diff = "\ X Y. ACC_cf X - ACC_cf Y" have finNEG: "finite NEG" using NEG_\ infinite_super by blast have "?Diff Z X \ ?Diff Z Y \ ?Diff Y X" by auto from card_mono[OF finite_subset[OF _ finite_\] this] ACC_cf_\ have "2 ^ p * card (?Diff Z X) \ 2 ^ p * card (?Diff Z Y \ ?Diff Y X)" by auto also have "\ \ 2 ^ p * (card (?Diff Z Y) + card (?Diff Y X))" by (rule mult_left_mono, rule card_Un_le, simp) also have "\ = 2 ^ p * card (?Diff Z Y) + 2 ^ p * card (?Diff Y X)" by (simp add: algebra_simps) also have "\ \ ((k - 1) ^ m) * q + (k - 1) ^ m" using IH step by auto also have "\ = ((k - 1) ^ m) * Suc q" by (simp add: ac_simps) finally have c: "2 ^ p * card (ACC_cf Z - ACC_cf X) \ ((k - 1) ^ m) * Suc q" by simp from False have "X \ {}" by auto thus ?thesis unfolding n using IH step c by auto qed qed text \Lemma 9\ lemma assumes X: "X \ \

L\l" and Y: "Y \ \

L\l" shows PLU_union: "PLU (X \ Y) \ \

L\l" and sqcup: "X \ Y \ \

L\l" and sqcup_sub: "POS \ ACC (X \ Y) \ ACC (X \ Y)" and deviate_pos_cup: "\\Pos X Y = {}" and deviate_neg_cup: "card (\\Neg X Y) < (k - 1)^m * L / 2^(p - 1)" proof - obtain Z n where res: "PLU_main (X \ Y) = (Z, n)" by force hence PLU: "PLU (X \ Y) = Z" unfolding PLU_def by simp from X Y have XY: "X \ Y \ \l" unfolding \

L\l_def by auto note main = PLU_main[OF this(1) res] from main show "PLU (X \ Y) \ \

L\l" unfolding PLU by simp thus "X \ Y \ \

L\l" unfolding sqcup_def . from main show "POS \ ACC (X \ Y) \ ACC (X \ Y)" unfolding sqcup_def PLU by simp thus "\\Pos X Y = {}" unfolding deviate_pos_cup_def PLU sqcup_def by auto have "card (v_gs (X \ Y)) \ card (v_gs X) + card (v_gs Y)" unfolding v_gs_union by (rule card_Un_le) also have "\ \ L + L" using X Y unfolding \

L\l_def by simp finally have "card (v_gs (X \ Y)) \ 2 * L" by simp with PLU_main_n[OF XY(1) res] have "n * (p - 1) \ 2 * L" by simp with p Lm m2 have n: "n < 2 * L" by (cases n, auto, cases "p - 1", auto) let ?r = real have *: "(k - 1) ^ m > 0" using k l2 by simp have "2 ^ p * card (\\Neg X Y) \ 2 ^ p * card (ACC_cf Z - ACC_cf (X \ Y))" unfolding deviate_neg_cup_def PLU sqcup_def by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_\]], insert ACC_cf_\, force, auto) also have "\ \ (k - 1) ^ m * n" using main by simp also have "\ < (k - 1) ^ m * (2 * L)" unfolding mult_less_cancel1 using n * by simp also have "\ = 2 * ((k - 1) ^ m * L)" by simp finally have "2 * (2^(p - 1) * card (\\Neg X Y)) < 2 * ((k - 1) ^ m * L)" using p by (cases p, auto) hence "2 ^ (p - 1) * card (\\Neg X Y) < (k - 1)^m * L" by simp hence "?r (2 ^ (p - 1) * card (\\Neg X Y)) < ?r ((k - 1)^m * L)" by linarith thus "card (\\Neg X Y) < (k - 1)^m * L / 2^(p - 1)" by (simp add: field_simps) qed text \Lemma 10\ lemma assumes X: "X \ \

L\l" and Y: "Y \ \

L\l" shows PLU_joinl: "PLU (X \l Y) \ \

L\l" and sqcap: "X \ Y \ \

L\l" and deviate_neg_cap: "card (\\Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" and deviate_pos_cap: "card (\\Pos X Y) \ ((m - l - 1) choose (k - l - 1)) * L^2" proof - obtain Z n where res: "PLU_main (X \l Y) = (Z, n)" by force hence PLU: "PLU (X \l Y) = Z" unfolding PLU_def by simp from X Y have XY: "X \ \l" "Y \ \l" "X \ \" "Y \ \" unfolding \

L\l_def \l_def by auto have sub: "X \l Y \ \l" unfolding odotl_def using XY by (auto split: option.splits) note main = PLU_main[OF sub res] note finV = finite_v_gs_Gl[OF XY(1)] finite_v_gs_Gl[OF XY(2)] have "X \ Y \ \" by (rule odot_\, insert XY, auto simp: \l_def) hence XYD: "X \ Y \ \" by auto have finvXY: "finite (v_gs (X \ Y))" by (rule finite_v_gs[OF XYD]) have "card (v_gs (X \ Y)) \ card (v_gs X) * card (v_gs Y)" using XY(1-2) by (intro card_v_gs_join, auto simp: \l_def) also have "\ \ L * L" using X Y unfolding \

L\l_def by (intro mult_mono, auto) also have "\ = L^2" by algebra finally have card_join: "card (v_gs (X \ Y)) \ L^2" . with card_mono[OF finvXY v_gs_mono[OF joinl_join]] have card: "card (v_gs (X \l Y)) \ L^2" by simp with PLU_main_n[OF sub res] have "n * (p - 1) \ L^2" by simp with p Lm m2 have n: "n < 2 * L^2" by (cases n, auto, cases "p - 1", auto) have *: "(k - 1) ^ m > 0" using k l2 by simp show "PLU (X \l Y) \ \

L\l" unfolding PLU using main by auto thus "X \ Y \ \

L\l" unfolding sqcap_def . let ?r = real have "2^p * card (\\Neg X Y) \ 2 ^ p * card (ACC_cf Z - ACC_cf (X \l Y))" unfolding deviate_neg_cap_def PLU sqcap_def by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_\]], insert ACC_cf_\, force, insert ACC_cf_mono[OF joinl_join, of X Y], auto) also have "\ \ (k - 1) ^ m * n" using main by simp also have "\ < (k - 1) ^ m * (2 * L^2)" unfolding mult_less_cancel1 using n * by simp finally have "2 * (2^(p - 1) * card (\\Neg X Y)) < 2 * ((k - 1) ^ m * L^2)" using p by (cases p, auto) hence "2 ^ (p - 1) * card (\\Neg X Y) < (k - 1)^m * L^2" by simp hence "?r (2 ^ (p - 1) * card (\\Neg X Y)) < (k - 1)^m * L^2" by linarith thus "card (\\Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" by (simp add: field_simps) (* now for the next approximation *) define Vs where "Vs = v_gs (X \ Y) \ {V . V \ [m] \ card V \ Suc l}" define C where "C (V :: nat set) = (SOME C. C \ V \ card C = Suc l)" for V define K where "K C = { W. W \ [m] - C \ card W = k - Suc l }" for C define merge where "merge C V = (C \ V)^\" for C V :: "nat set" define GS where "GS = { merge (C V) W | V W. V \ Vs \ W \ K (C V)}" { fix V assume V: "V \ Vs" hence card: "card V \ Suc l" and Vm: "V \ [m]" unfolding Vs_def by auto from card obtain D where C: "D \ V" and cardV: "card D = Suc l" by (rule obtain_subset_with_card_n) hence "\ C. C \ V \ card C = Suc l" by blast from someI_ex[OF this, folded C_def] have *: "C V \ V" "card (C V) = Suc l" by blast+ with Vm have sub: "C V \ [m]" by auto from finite_subset[OF this] have finCV: "finite (C V)" unfolding numbers_def by simp have "card (K (C V)) = (m - Suc l) choose (k - Suc l)" unfolding K_def proof (subst n_subsets, (rule finite_subset[of _ "[m]"], auto)[1], rule arg_cong[of _ _ "\ x. x choose _"]) show "card ([m] - C V) = m - Suc l" by (subst card_Diff_subset, insert sub * finCV, auto) qed note * finCV sub this } note Vs_C = this have finK: "finite (K V)" for V unfolding K_def by auto { fix G assume G: "G \ POS \ ACC (X \ Y)" have "G \ ACC (X \l Y) \ GS" proof (rule ccontr) assume "\ ?thesis" with G have G: "G \ POS" "G \ ACC (X \ Y)" "G \ ACC (X \l Y)" and contra: "G \ GS" by auto from G(1)[unfolded \_def] have "card (v G) = k \ (v G)^\ = G" and G0: "G \ \" by auto hence vGk: "card (v G) = k" "(v G)^\ = G" by auto from G0 have vm: "v G \ [m]" by (rule v_\) from G(2-3)[unfolded ACC_def accepts_def] obtain H where H: "H \ X \ Y" "H \ X \l Y" and HG: "H \ G" by auto from v_mono[OF HG] have vHG: "v H \ v G" by auto { from H(1)[unfolded odot_def] obtain D E where D: "D \ X" and E: "E \ Y" and HDE: "H = D \ E" by force from D E X Y have Dl: "D \ \l" "E \ \l" unfolding \

L\l_def by auto have Dp: "D \ \" using Dl by (auto simp: \l_def) have Ep: "E \ \" using Dl by (auto simp: \l_def) from Dl HDE have HD: "H \ \" unfolding \l_def by auto have HG0: "H \ \" using Dp Ep unfolding HDE by auto have HDL: "H \ \l" proof assume "H \ \l" hence "H \ X \l Y" - unfolding odotl_def HDE using D E by blast + unfolding odotl_def HDE odot_def using D E by blast thus False using H by auto qed from HDL HD have HGl: "H \ \l" unfolding \l_def by auto have vm: "v H \ [m]" using HG0 by (rule v_\) have lower: "l < card (v H)" using HGl HG0 unfolding \l_def by auto have "v H \ Vs" unfolding Vs_def using lower vm H unfolding v_gs_def by auto } note in_Vs = this note C = Vs_C[OF this] let ?C = "C (v H)" from C vHG have CG: "?C \ v G" by auto hence id: "v G = ?C \ (v G - ?C)" by auto from arg_cong[OF this, of card] vGk(1) C have "card (v G - ?C) = k - Suc l" by (metis CG card_Diff_subset) hence "v G - ?C \ K ?C" unfolding K_def using vm by auto hence "merge ?C (v G - ?C) \ GS" unfolding GS_def using in_Vs by auto also have "merge ?C (v G - ?C) = v G^\" unfolding merge_def by (rule arg_cong[of _ _ sameprod], insert id, auto) also have "\ = G" by fact finally have "G \ GS" . with contra show False .. qed } hence "\\Pos X Y \ (POS \ ACC (X \l Y) - ACC (X \ Y)) \ GS" unfolding deviate_pos_cap_def by auto also have "POS \ ACC (X \l Y) - ACC (X \ Y) = {}" proof - have "POS - ACC (X \ Y) \ UNIV - ACC (X \l Y)" unfolding sqcap_def using PLU main by auto thus ?thesis by auto qed finally have sub: "\\Pos X Y \ GS" by auto have finVs: "finite Vs" unfolding Vs_def numbers_def by simp let ?Sig = "Sigma Vs (\ V. K (C V))" have GS_def: "GS = (\ (V,W). merge (C V) W) ` ?Sig" unfolding GS_def by auto have finSig: "finite ?Sig" using finVs finK by simp have finGS: "finite GS" unfolding GS_def by (rule finite_imageI[OF finSig]) have "card (\\Pos X Y) \ card GS" by (rule card_mono[OF finGS sub]) also have "\ \ card ?Sig" unfolding GS_def by (rule card_image_le[OF finSig]) also have "\ = (\a\Vs. card (K (C a)))" by (rule card_SigmaI[OF finVs], auto simp: finK) also have "\ = (\a\Vs. (m - Suc l) choose (k - Suc l))" using Vs_C by (intro sum.cong, auto) also have "\ = ((m - Suc l) choose (k - Suc l)) * card Vs" by simp also have "\ \ ((m - Suc l) choose (k - Suc l)) * L^2" proof (rule mult_left_mono) have "card Vs \ card (v_gs (X \ Y))" by (rule card_mono[OF finvXY], auto simp: Vs_def) also have "\ \ L^2" by fact finally show "card Vs \ L^2" . qed simp finally show "card (\\Pos X Y) \ ((m - l - 1) choose (k - l - 1)) * L^2" by simp qed end subsection \Formalism\ text \Fix a variable set of cardinality m over 2.\ locale forth_assumptions = third_assumptions + fixes \ :: "'a set" and \ :: "'a \ vertex set" assumes cV: "card \ = (m choose 2)" and bij_betw_\: "bij_betw \ \ ([m]^\)" begin definition n where "n = (m choose 2)" text \the formulas over the fixed variable set\ definition \ :: "'a mformula set" where "\ = { \. vars \ \ \}" lemma \_simps[simp]: "FALSE \ \" "(Var x \ \) = (x \ \)" "(Conj \ \ \ \) = (\ \ \ \ \ \ \)" "(Disj \ \ \ \) = (\ \ \ \ \ \ \)" by (auto simp: \_def) lemma inj_on_\: "inj_on \ \" using bij_betw_\ by (metis bij_betw_imp_inj_on) lemma \m2[simp,intro]: "x \ \ \ \ x \ [m]^\" using bij_betw_\ by (rule bij_betw_apply) lemma card_v_\[simp,intro]: assumes "x \ \" shows "card (v {\ x}) = 2" proof - from \m2[OF assms] have mem: "\ x \ [m]^\" by auto from this[unfolded binprod_def] obtain a b where \: "\ x = {a,b}" and diff: "a \ b" by auto hence "v {\ x} = {a,b}" unfolding v_def by auto thus ?thesis using diff by simp qed lemma \_singleton[simp,intro]: assumes "x \ \" shows "{\ x} \ \" "{{\ x}} \ \

L\l" using assms L3 l2 by (auto simp: \_def \

L\l_def v_gs_def \l_def) lemma empty_\

L\l[simp,intro]: "{} \ \

L\l" by (auto simp: \_def \

L\l_def v_gs_def \l_def) fun SET :: "'a mformula \ graph set" where "SET FALSE = {}" | "SET (Var x) = {{\ x}}" | "SET (Disj \ \) = SET \ \ SET \" | "SET (Conj \ \) = SET \ \ SET \" lemma ACC_cf_SET[simp]: "ACC_cf (SET (Var x)) = {f \ \. \ x \ C f}" "ACC_cf (SET FALSE) = {}" "ACC_cf (SET (Disj \ \)) = ACC_cf (SET \) \ ACC_cf (SET \)" "ACC_cf (SET (Conj \ \)) = ACC_cf (SET \) \ ACC_cf (SET \)" using ACC_cf_odot by (auto simp: ACC_cf_union ACC_cf_empty, auto simp: ACC_cf_def accepts_def) lemma ACC_SET[simp]: "ACC (SET (Var x)) = {G \ \. \ x \ G}" "ACC (SET FALSE) = {}" "ACC (SET (Disj \ \)) = ACC (SET \) \ ACC (SET \)" "ACC (SET (Conj \ \)) = ACC (SET \) \ ACC (SET \)" by (auto simp: ACC_union ACC_odot, auto simp: ACC_def accepts_def) lemma SET_\: "\ \ tf_mformula \ \ \ \ \ SET \ \ \" proof (induct \ rule: tf_mformula.induct) case (tf_Conj \ \) hence "SET \ \ \" "SET \ \ \" by auto from odot_\[OF this] show ?case by simp qed auto fun APR :: "'a mformula \ graph set" where "APR FALSE = {}" | "APR (Var x) = {{\ x}}" | "APR (Disj \ \) = APR \ \ APR \" | "APR (Conj \ \) = APR \ \ APR \" lemma APR: "\ \ tf_mformula \ \ \ \ \ APR \ \ \

L\l" by (induct \ rule: tf_mformula.induct, auto intro!: sqcup sqcap) definition ACC_cf_mf :: "'a mformula \ colorf set" where "ACC_cf_mf \ = ACC_cf (SET \)" definition ACC_mf :: "'a mformula \ graph set" where "ACC_mf \ = ACC (SET \)" definition deviate_pos :: "'a mformula \ graph set" ("\Pos") where "\Pos \ = POS \ ACC_mf \ - ACC (APR \)" definition deviate_neg :: "'a mformula \ colorf set" ("\Neg") where "\Neg \ = ACC_cf (APR \) - ACC_cf_mf \" text \Lemma 11.1\ lemma deviate_subset_Disj: "\Pos (Disj \ \) \ \\Pos (APR \) (APR \) \ \Pos \ \ \Pos \" "\Neg (Disj \ \) \ \\Neg (APR \) (APR \) \ \Neg \ \ \Neg \" unfolding deviate_pos_def deviate_pos_cup_def deviate_neg_def deviate_neg_cup_def ACC_cf_mf_def ACC_cf_SET ACC_cf_union ACC_mf_def ACC_SET ACC_union by auto text \Lemma 11.2\ lemma deviate_subset_Conj: "\Pos (Conj \ \) \ \\Pos (APR \) (APR \) \ \Pos \ \ \Pos \" "\Neg (Conj \ \) \ \\Neg (APR \) (APR \) \ \Neg \ \ \Neg \" unfolding deviate_pos_def deviate_pos_cap_def ACC_mf_def ACC_SET ACC_odot deviate_neg_def deviate_neg_cap_def ACC_cf_mf_def ACC_cf_SET ACC_cf_odot by auto lemmas deviate_subset = deviate_subset_Disj deviate_subset_Conj lemma deviate_finite: "finite (\Pos \)" "finite (\Neg \)" "finite (\\Pos A B)" "finite (\\Neg A B)" "finite (\\Pos A B)" "finite (\\Neg A B)" unfolding deviate_pos_def deviate_pos_cup_def deviate_pos_cap_def deviate_neg_def deviate_neg_cup_def deviate_neg_cap_def by (intro finite_subset[OF _ finite_POS_NEG], auto)+ text \Lemma 12\ lemma no_deviation[simp]: "\Pos FALSE = {}" "\Neg FALSE = {}" "\Pos (Var x) = {}" "\Neg (Var x) = {}" unfolding deviate_pos_def deviate_neg_def by (auto simp add: ACC_cf_mf_def ACC_mf_def) text \Lemma 12.1-2\ fun approx_pos where "approx_pos (Conj phi psi) = \\Pos (APR phi) (APR psi)" | "approx_pos _ = {}" fun approx_neg where "approx_neg (Conj phi psi) = \\Neg (APR phi) (APR psi)" | "approx_neg (Disj phi psi) = \\Neg (APR phi) (APR psi)" | "approx_neg _ = {}" lemma finite_approx_pos: "finite (approx_pos \)" by (cases \, auto intro: deviate_finite) lemma finite_approx_neg: "finite (approx_neg \)" by (cases \, auto intro: deviate_finite) lemma card_deviate_Pos: assumes phi: "\ \ tf_mformula" "\ \ \" shows "card (\Pos \) \ cs \ * L\<^sup>2 * ( (m - l - 1) choose (k - l - 1))" proof - let ?Pos = "\ \. \ (approx_pos ` SUB \)" have "\Pos \ \ ?Pos \" using phi proof (induct \ rule: tf_mformula.induct) case (tf_Disj \ \) from tf_Disj have *: "\ \ tf_mformula" "\ \ tf_mformula" "\ \ \" "\ \ \" by auto note IH = tf_Disj(2)[OF *(3)] tf_Disj(4)[OF *(4)] have "\Pos (Disj \ \) \ \\Pos (APR \) (APR \) \ \Pos \ \ \Pos \" by (rule deviate_subset) also have "\\Pos (APR \) (APR \) = {}" by (rule deviate_pos_cup; intro APR * ) also have "\ \ \Pos \ \ \Pos \ \ ?Pos \ \ ?Pos \" using IH by auto also have "\ \ ?Pos (Disj \ \) \ ?Pos (Disj \ \)" by (intro Un_mono, auto) finally show ?case by simp next case (tf_Conj \ \) from tf_Conj have *: "\ \ \" "\ \ \" by (auto intro: tf_mformula.intros) note IH = tf_Conj(2)[OF *(1)] tf_Conj(4)[OF *(2)] have "\Pos (Conj \ \) \ \\Pos (APR \) (APR \) \ \Pos \ \ \Pos \" by (rule deviate_subset) also have "\ \ \\Pos (APR \) (APR \) \ ?Pos \ \ ?Pos \" using IH by auto also have "\ \ ?Pos (Conj \ \) \ ?Pos (Conj \ \) \ ?Pos (Conj \ \)" by (intro Un_mono, insert *, auto) finally show ?case by simp qed auto from card_mono[OF finite_UN_I[OF finite_SUB finite_approx_pos] this] have "card (\Pos \) \ card (\ (approx_pos ` SUB \))" by simp also have "\ \ (\i\SUB \. card (approx_pos i))" by (rule card_UN_le[OF finite_SUB]) also have "\ \ (\i\SUB \. L\<^sup>2 * ( (m - l - 1) choose (k - l - 1)))" proof (rule sum_mono, goal_cases) case (1 psi) from phi 1 have psi: "psi \ tf_mformula" "psi \ \" by (induct \ rule: tf_mformula.induct, auto intro: tf_mformula.intros) show ?case proof (cases psi) case (Conj phi1 phi2) from psi this have *: "phi1 \ tf_mformula" "phi1 \ \" "phi2 \ tf_mformula" "phi2 \ \" by (cases rule: tf_mformula.cases, auto)+ from deviate_pos_cap[OF APR[OF *(1-2)] APR[OF *(3-4)]] show ?thesis unfolding Conj by (simp add: ac_simps) qed auto qed also have "\ = cs \ * L\<^sup>2 * ( (m - l - 1) choose (k - l - 1))" unfolding cs_def by simp finally show "card (\Pos \) \ cs \ * L\<^sup>2 * (m - l - 1 choose (k - l - 1))" by simp qed lemma card_deviate_Neg: assumes phi: "\ \ tf_mformula" "\ \ \" shows "card (\Neg \) \ cs \ * L\<^sup>2 * (k - 1)^m / 2^(p - 1)" proof - let ?r = real let ?Neg = "\ \. \ (approx_neg ` SUB \)" have "\Neg \ \ ?Neg \" using phi proof (induct \ rule: tf_mformula.induct) case (tf_Disj \ \) from tf_Disj have *: "\ \ tf_mformula" "\ \ tf_mformula" "\ \ \" "\ \ \" by auto note IH = tf_Disj(2)[OF *(3)] tf_Disj(4)[OF *(4)] have "\Neg (Disj \ \) \ \\Neg (APR \) (APR \) \ \Neg \ \ \Neg \" by (rule deviate_subset) also have "\ \ \\Neg (APR \) (APR \) \ ?Neg \ \ ?Neg \" using IH by auto also have "\ \ ?Neg (Disj \ \) \ ?Neg (Disj \ \) \ ?Neg (Disj \ \)" by (intro Un_mono, auto) finally show ?case by simp next case (tf_Conj \ \) from tf_Conj have *: "\ \ \" "\ \ \" by (auto intro: tf_mformula.intros) note IH = tf_Conj(2)[OF *(1)] tf_Conj(4)[OF *(2)] have "\Neg (Conj \ \) \ \\Neg (APR \) (APR \) \ \Neg \ \ \Neg \" by (rule deviate_subset) also have "\ \ \\Neg (APR \) (APR \) \ ?Neg \ \ ?Neg \" using IH by auto also have "\ \ ?Neg (Conj \ \) \ ?Neg (Conj \ \) \ ?Neg (Conj \ \)" by (intro Un_mono, auto) finally show ?case by simp qed auto hence "\Neg \ \ \ (approx_neg ` SUB \)" by auto from card_mono[OF finite_UN_I[OF finite_SUB finite_approx_neg] this] have "card (\Neg \) \ card (\ (approx_neg ` SUB \))" . also have "\ \ (\i\SUB \. card (approx_neg i))" by (rule card_UN_le[OF finite_SUB]) finally have "?r (card (\Neg \)) \ (\i\SUB \. card (approx_neg i))" by linarith also have "\ = (\i\SUB \. ?r (card (approx_neg i)))" by simp also have "\ \ (\i\SUB \. L^2 * (k - 1)^m / 2^(p - 1))" proof (rule sum_mono, goal_cases) case (1 psi) from phi 1 have psi: "psi \ tf_mformula" "psi \ \" by (induct \ rule: tf_mformula.induct, auto intro: tf_mformula.intros) show ?case proof (cases psi) case (Conj phi1 phi2) from psi this have *: "phi1 \ tf_mformula" "phi1 \ \" "phi2 \ tf_mformula" "phi2 \ \" by (cases rule: tf_mformula.cases, auto)+ from deviate_neg_cap[OF APR[OF *(1-2)] APR[OF *(3-4)]] show ?thesis unfolding Conj by (simp add: ac_simps) next case (Disj phi1 phi2) from psi this have *: "phi1 \ tf_mformula" "phi1 \ \" "phi2 \ tf_mformula" "phi2 \ \" by (cases rule: tf_mformula.cases, auto)+ from deviate_neg_cup[OF APR[OF *(1-2)] APR[OF *(3-4)]] have "card (approx_neg psi) \ ((L * 1) * (k - 1) ^ m) / 2 ^ (p - 1)" unfolding Disj by (simp add: ac_simps) also have "\ \ ((L * L) * (k - 1) ^ m) / 2 ^ (p - 1)" by (intro divide_right_mono, unfold of_nat_le_iff, intro mult_mono, insert L3, auto) finally show ?thesis unfolding power2_eq_square by simp qed auto qed also have "\ = cs \ * L^2 * (k - 1)^m / 2^(p - 1)" unfolding cs_def by simp finally show "card (\Neg \) \ cs \ * L\<^sup>2 * (k - 1)^m / 2^(p - 1)" . qed text \Lemma 12.3\ lemma ACC_cf_non_empty_approx: assumes phi: "\ \ tf_mformula" "\ \ \" and ne: "APR \ \ {}" shows "card (ACC_cf (APR \)) > (k - 1)^m / 3" proof - from ne obtain E :: graph where Ephi: "E \ APR \" by (auto simp: ACC_def accepts_def) from APR[OF phi, unfolded \

L\l_def] Ephi have EDl: "E \ \l" by auto hence vEl: "card (v E) \ l" and ED: "E \ \" unfolding \l_def \l_def by auto have E: "E \ \" using ED[unfolded \l_def] by auto have sub: "v E \ [m]" by (rule v_\[OF E]) have "l \ card [m]" using lm by auto from exists_subset_between[OF vEl this sub finite_numbers] obtain V where V: "v E \ V" "V \ [m]" "card V = l" by auto from finite_subset[OF V(2)] have finV: "finite V" by auto have finPart: "finite A" if "A \ {P. partition_on [n] P}" for n A by (rule finite_subset[OF that finitely_many_partition_on], simp) - define um where "um n = uminus (int n)" for n - have um: "um n \ um m \ n \ m" for n m unfolding um_def by auto have finmv: "finite ([m] - V)" using finite_numbers[of m] by auto have finK: "finite [k - 1]" unfolding numbers_def by auto define F where "F = {f \ [m] \\<^sub>E [k - 1]. inj_on f V}" have FF: "F \ \" unfolding \_def F_def by auto { fix f assume f: "f \ F" { from this[unfolded F_def] have f: "f \ [m] \\<^sub>E [k - 1]" and inj: "inj_on f V" by auto from V l2 have 2: "card V \ 2" by auto then obtain x where x: "x \ V" by (cases "V = {}", auto) have "card V = card (V - {x}) + 1" using x finV by (metis One_nat_def add.right_neutral add_Suc_right card_Suc_Diff1) with 2 have "card (V - {x}) > 0" by auto hence "V - {x} \ {}" by fastforce then obtain y where y: "y \ V" and diff: "x \ y" by auto from inj diff x y have neq: "f x \ f y" by (auto simp: inj_on_def) from x y diff V have "{x, y} \ [m]^\" unfolding sameprod_altdef by auto with neq have "{x,y} \ C f" unfolding C_def by auto hence "C f \ {}" by auto } with NEG_\ FF f have CfG: "C f \ \" "C f \ {}" by (auto simp: NEG_def) have "E \ C f" proof fix e assume eE: "e \ E" with E[unfolded \_def] have em: "e \ [m]^\" by auto then obtain x y where e: "e = {x,y}" "x \ y" "{x,y} \ [m]" and card: "card e = 2" unfolding binprod_def by auto from v_mem_sub[OF card eE] have "{x,y} \ v E" using e by auto hence "{x,y} \ V" using V by auto hence "f x \ f y" using e(2) f[unfolded F_def] by (auto simp: inj_on_def) thus "e \ C f" unfolding C_def using em e by auto qed with Ephi CfG have "APR \ \ C f" unfolding accepts_def by auto hence "f \ ACC_cf (APR \)" using CfG f FF unfolding ACC_cf_def by auto } with FF have sub: "F \ ACC_cf (APR \)" by auto from card_mono[OF finite_subset[OF _ finite_ACC] this] have approx: "card F \ card (ACC_cf (APR \))" by auto from card_inj_on_subset_funcset[OF finite_numbers finK V(2), unfolded card_numbers V(3), folded F_def] have "real (card F) = (real (k - 1)) ^ (m - l) * prod (\ i. real (k - 1 - i)) {0.. > (real (k - 1)) ^ m / 3" by (rule approximation1) finally have cardF: "card F > (k - 1) ^ m / 3" by simp with approx show ?thesis by simp qed text \Theorem 13\ lemma theorem_13: assumes phi: "\ \ tf_mformula" "\ \ \" and sub: "POS \ ACC_mf \" "ACC_cf_mf \ = {}" shows "cs \ > k powr (4 / 7 * sqrt k)" proof - let ?r = "real :: nat \ real" have "cs \ > ((m - l) / k)^l / (6 * L^2)" proof (cases "POS \ ACC (APR \) = {}") case empty: True have "\Pos \ = POS \ ACC_mf \ - ACC (APR \)" unfolding deviate_pos_def by auto also have "\ = POS - ACC (APR \)" using sub by blast also have "\ = POS" using empty by auto finally have id: "\Pos \ = POS" by simp have "m choose k = card POS" by (simp add: card_POS) also have "\ = card (\Pos \)" unfolding id by simp also have "\ \ cs \ * L\<^sup>2 * (m - l - 1 choose (k - l - 1))" using card_deviate_Pos[OF phi] by auto finally have "m choose k \ cs \ * L\<^sup>2 * (m - l - 1 choose (k - l - 1))" by simp from approximation2[OF this] show "((m - l) / k)^l / (6 * L^2) < cs \" by simp next case False have "POS \ ACC (APR \) \ {}" by fact hence nempty: "APR \ \ {}" by auto have "card (\Neg \) = card (ACC_cf (APR \) - ACC_cf_mf \)" unfolding deviate_neg_def by auto also have "\ = card (ACC_cf (APR \))" using sub by auto also have "\ > (k - 1)^m / 3" using ACC_cf_non_empty_approx[OF phi nempty] . finally have "(k - 1)^m / 3 < card (\Neg \)" . also have "\ \ cs \ * L\<^sup>2 * (k - 1) ^ m / 2 ^ (p - 1)" using card_deviate_Neg[OF phi] sub by auto finally have "(k - 1)^m / 3 < (cs \ * (L\<^sup>2 * (k - 1) ^ m)) / 2 ^ (p - 1)" by simp from approximation3[OF this] show ?thesis . qed hence part1: "cs \ > ((m - l) / k)^l / (6 * L^2)" . from approximation4[OF this] show ?thesis using k2 by simp qed text \Definition 14\ definition eval_g :: "'a VAS \ graph \ bool" where "eval_g \ G = (\ v \ \. (\ v \ G \ \ v))" definition eval_gs :: "'a VAS \ graph set \ bool" where "eval_gs \ X = (\ G \ X. eval_g \ G)" lemmas eval_simps = eval_g_def eval_gs_def eval.simps lemma eval_gs_union: "eval_gs \ (X \ Y) = (eval_gs \ X \ eval_gs \ Y)" by (auto simp: eval_gs_def) lemma eval_gs_odot: assumes "X \ \" "Y \ \" shows "eval_gs \ (X \ Y) = (eval_gs \ X \ eval_gs \ Y)" proof assume "eval_gs \ (X \ Y)" from this[unfolded eval_gs_def] obtain DE where DE: "DE \ X \ Y" and eval: "eval_g \ DE" by auto from DE[unfolded odot_def] obtain D E where id: "DE = D \ E" and DE: "D \ X" "E \ Y" by auto from eval have "eval_g \ D" "eval_g \ E" unfolding id eval_g_def by auto with DE show "eval_gs \ X \ eval_gs \ Y" unfolding eval_gs_def by auto next assume "eval_gs \ X \ eval_gs \ Y" then obtain D E where DE: "D \ X" "E \ Y" and eval: "eval_g \ D" "eval_g \ E" unfolding eval_gs_def by auto from DE assms have D: "D \ \" "E \ \" by auto let ?U = "D \ E" from eval have eval: "eval_g \ ?U" unfolding eval_g_def by auto from DE have 1: "?U \ X \ Y" unfolding odot_def by auto with 1 eval show "eval_gs \ (X \ Y)" unfolding eval_gs_def by auto qed text \Lemma 15\ lemma eval_set: assumes phi: "\ \ tf_mformula" "\ \ \" shows "eval \ \ = eval_gs \ (SET \)" using phi proof (induct \ rule: tf_mformula.induct) case tf_False then show ?case unfolding eval_simps by simp next case (tf_Var x) then show ?case using inj_on_\ unfolding eval_simps by (auto simp add: inj_on_def) next case (tf_Disj \1 \2) thus ?case by (auto simp: eval_gs_union) next case (tf_Conj \1 \2) thus ?case by (simp, intro eval_gs_odot[symmetric]; intro SET_\, auto) qed definition \\<^sub>g :: "graph \ 'a VAS" where "\\<^sub>g G x = (x \ \ \ \ x \ G)" text \From here on we deviate from Gordeev's paper as we do not use positive bases, but a more direct approach.\ lemma eval_ACC: assumes phi: "\ \ tf_mformula" "\ \ \" and G: "G \ \" shows "eval (\\<^sub>g G) \ = (G \ ACC_mf \)" using phi unfolding ACC_mf_def proof (induct \ rule: tf_mformula.induct) case (tf_Var x) thus ?case by (auto simp: ACC_def G accepts_def \\<^sub>g_def) next case (tf_Disj phi psi) thus ?case by (auto simp: ACC_union) next case (tf_Conj phi psi) thus ?case by (auto simp: ACC_odot) qed simp lemma CLIQUE_solution_imp_POS_sub_ACC: assumes solution: "\ G \ \. G \ CLIQUE \ eval (\\<^sub>g G) \" and tf: "\ \ tf_mformula" and phi: "\ \ \" shows "POS \ ACC_mf \" proof fix G assume POS: "G \ POS" with POS_\ have G: "G \ \" by auto with POS solution POS_CLIQUE have "eval (\\<^sub>g G) \" by auto thus "G \ ACC_mf \" unfolding eval_ACC[OF tf phi G] . qed lemma CLIQUE_solution_imp_ACC_cf_empty: assumes solution: "\ G \ \. G \ CLIQUE \ eval (\\<^sub>g G) \" and tf: "\ \ tf_mformula" and phi: "\ \ \" shows "ACC_cf_mf \ = {}" proof (rule ccontr) assume "\ ?thesis" from this[unfolded ACC_cf_mf_def ACC_cf_def] obtain F where F: "F \ \" "SET \ \ C F" by auto define G where "G = C F" have NEG: "G \ NEG" unfolding NEG_def G_def using F by auto hence "G \ CLIQUE" using CLIQUE_NEG by auto have GG: "G \ \" unfolding G_def using F using G_def NEG NEG_\ by blast have GAcc: "SET \ \ G" using F[folded G_def] by auto then obtain D :: graph where D: "D \ SET \" and sub: "D \ G" unfolding accepts_def by blast from SET_\[OF tf phi] D have DG: "D \ \" by auto have eval: "eval (\\<^sub>g D) \" unfolding eval_set[OF tf phi] eval_gs_def by (intro bexI[OF _ D], unfold eval_g_def, insert DG, auto simp: \\<^sub>g_def) hence "D \ CLIQUE" using solution[rule_format, OF DG] by auto hence "G \ CLIQUE" using GG sub unfolding CLIQUE_def by blast with \G \ CLIQUE\ show False by auto qed subsection \Conclusion\ text \Theorem 22\ text \We first consider monotone formulas without TRUE.\ theorem Clique_not_solvable_by_small_tf_mformula: assumes solution: "\ G \ \. G \ CLIQUE \ eval (\\<^sub>g G) \" and tf: "\ \ tf_mformula" and phi: "\ \ \" shows "cs \ > k powr (4 / 7 * sqrt k)" proof - from CLIQUE_solution_imp_POS_sub_ACC[OF solution tf phi] have POS: "POS \ ACC_mf \" . from CLIQUE_solution_imp_ACC_cf_empty[OF solution tf phi] have CF: "ACC_cf_mf \ = {}" . from theorem_13[OF tf phi POS CF] show ?thesis by auto qed text \Next we consider general monotone formulas.\ theorem Clique_not_solvable_by_poly_mono: assumes solution: "\ G \ \. G \ CLIQUE \ eval (\\<^sub>g G) \" and phi: "\ \ \" shows "cs \ > k powr (4 / 7 * sqrt k)" proof - note vars = phi[unfolded \_def] have CL: "CLIQUE = Clique [k^4] k" "\ = Graphs [k^4]" unfolding CLIQUE_def \_altdef m_def Clique_def by auto with empty_CLIQUE have "{} \ Clique [k^4] k" by simp with solution[rule_format, of "{}"] have "\ eval (\\<^sub>g {}) \" by (auto simp: Graphs_def) from to_tf_mformula[OF this] obtain \ where *: "\ \ tf_mformula" "(\\. eval \ \ = eval \ \)" "vars \ \ vars \" "cs \ \ cs \" by auto with phi solution have psi: "\ \ \" and solution: "\G\\. (G \ CLIQUE) = eval (\\<^sub>g G) \" unfolding \_def by auto from Clique_not_solvable_by_small_tf_mformula[OF solution *(1) psi] show ?thesis using *(4) by auto qed text \We next expand all abbreviations and definitions of the locale, but stay within the locale\ theorem Clique_not_solvable_by_small_monotone_circuit_in_locale: assumes phi_solves_clique: "\ G \ Graphs [k^4]. G \ Clique [k^4] k \ eval (\ x. \ x \ G) \" and vars: "vars \ \ \" shows "cs \ > k powr (4 / 7 * sqrt k)" proof - { fix G assume G: "G \ \" have "eval (\ x. \ x \ G) \ = eval (\\<^sub>g G) \" using vars by (intro eval_vars, auto simp: \\<^sub>g_def) } have CL: "CLIQUE = Clique [k^4] k" "\ = Graphs [k^4]" unfolding CLIQUE_def \_altdef m_def Clique_def by auto { fix G assume G: "G \ \" have "eval (\ x. \ x \ G) \ = eval (\\<^sub>g G) \" using vars by (intro eval_vars, auto simp: \\<^sub>g_def) } with phi_solves_clique CL have solves: "\ G \ \. G \ CLIQUE \ eval (\\<^sub>g G) \" by auto from vars have inA: "\ \ \" by (auto simp: \_def) from Clique_not_solvable_by_poly_mono[OF solves inA] show ?thesis by auto qed end text \Let us now move the theorem outside the locale\ definition Large_Number where "Large_Number = Max {64, L0''^2, L0^2, L0'^2, M0, M0'}" theorem Clique_not_solvable_by_small_monotone_circuit_squared: fixes \ :: "'a mformula" assumes k: "\ l. k = l^2" and LARGE: "k \ Large_Number" and \: "bij_betw \ V [k^4]^\" and solution: "\G\Graphs [k ^ 4]. (G \ Clique [k ^ 4] k) = eval (\ x. \ x \ G) \" and vars: "vars \ \ V" shows "cs \ > k powr (4 / 7 * sqrt k)" proof - from k obtain l where kk: "k = l^2" by auto note LARGE = LARGE[unfolded Large_Number_def] have k8: "k \ 8^2" using LARGE by auto from this[unfolded kk power2_nat_le_eq_le] have l8: "l \ 8" . define p where "p = nat (ceiling (l * log 2 (k^4)))" have tedious: "l * log 2 (k ^ 4) \ 0" using l8 k8 by auto have "int p = ceiling (l * log 2 (k ^ 4))" unfolding p_def by (rule nat_0_le, insert tedious, auto) from arg_cong[OF this, of real_of_int] have rp: "real p = ceiling (l * log 2 (k ^ 4))" by simp have one: "real l * log 2 (k ^ 4) \ p" unfolding rp by simp have two: "p \ real l * log 2 (k ^ 4) + 1" unfolding rp by simp have "real l < real l + 1 " by simp also have "\ \ real l + real l" using l8 by simp also have "\ = real l * 2" by simp also have "\ = real l * log 2 (2^2)" by (subst log_pow_cancel, auto) also have "\ \ real l * log 2 (k ^ 4)" proof (intro mult_left_mono, subst log_le_cancel_iff) have "(4 :: real) \ 2^4" by simp also have "\ \ real k^4" by (rule power_mono, insert k8, auto) finally show "2\<^sup>2 \ real (k ^ 4)" by simp qed (insert k8, auto) also have "\ \ p" by fact finally have lp: "l < p" by auto interpret second_assumptions l p k proof (unfold_locales) show "2 < l" using l8 by auto show "8 \ l" by fact show "k = l^2" by fact show "l < p" by fact from LARGE have "L0''^2 \ k" by auto from this[unfolded kk power2_nat_le_eq_le] have L0''l: "L0'' \ l" . have "p \ real l * log 2 (k ^ 4) + 1" by fact also have "\ < k" unfolding kk by (intro L0'' L0''l) finally show "p < k" by simp qed interpret third_assumptions l p k proof show "real l * log 2 (real m) \ p" using one unfolding m_def . show "p \ real l * log 2 (real m) + 1" using two unfolding m_def . from LARGE have "L0^2 \ k" by auto from this[unfolded kk power2_nat_le_eq_le] show "L0 \ l" . from LARGE have "L0'^2 \ k" by auto from this[unfolded kk power2_nat_le_eq_le] show "L0' \ l" . show "M0' \ m" using km LARGE by simp show "M0 \ m" using km LARGE by simp qed interpret forth_assumptions l p k V \ by (standard, insert \ m_def, auto simp: bij_betw_same_card[OF \]) from Clique_not_solvable_by_small_monotone_circuit_in_locale[OF solution vars] show ?thesis . qed text \A variant where we get rid of the @{term "k = l^2"}-assumption by just taking squares everywhere.\ theorem Clique_not_solvable_by_small_monotone_circuit: fixes \ :: "'a mformula" assumes LARGE: "k \ Large_Number" and \: "bij_betw \ V [k^8]^\" and solution: "\G\Graphs [k ^ 8]. (G \ Clique [k ^ 8] (k^2)) = eval (\ x. \ x \ G) \" and vars: "vars \ \ V" shows "cs \ > k powr (8 / 7 * k)" proof - from LARGE have LARGE: "Large_Number \ k\<^sup>2" by (simp add: power2_nat_le_imp_le) have id: "k\<^sup>2 ^ 4 = k^8" "sqrt (k^2) = k" by auto from Clique_not_solvable_by_small_monotone_circuit_squared[of "k^2", unfolded id, OF _ LARGE \ solution vars] have "cs \ > (k^2) powr (4 / 7 * k)" by auto also have "(k^2) powr (4 / 7 * k) = k powr (8 / 7 * k)" unfolding of_nat_power using powr_powr[of "real k" 2] by simp finally show ?thesis . qed definition large_number where "large_number = Large_Number^8" text \Finally a variant, where the size is formulated depending on $n$, the number of vertices.\ theorem Clique_with_n_nodes_not_solvable_by_small_monotone_circuit: fixes \ :: "'a mformula" assumes large: "n \ large_number" and kn: "\ k. n = k^8" and \: "bij_betw \ V [n]^\" and s: "s = root 4 n" and solution: "\G\Graphs [n]. (G \ Clique [n] s) = eval (\ x. \ x \ G) \" and vars: "vars \ \ V" shows "cs \ > (root 7 n) powr (root 8 n)" proof - from kn obtain k where nk: "n = k^8" by auto have kn: "k = root 8 n" unfolding nk of_nat_power by (subst real_root_pos2, auto) have "root 4 n = root 4 ((real (k^2))^4)" unfolding nk by simp also have "\ = k^2" by (simp add: real_root_pos_unique) finally have r4: "root 4 n = k^2" by simp have s: "s = k^2" using s unfolding r4 by simp from large[unfolded nk large_number_def] have Large: "k \ Large_Number" by simp have "0 < Large_Number" unfolding Large_Number_def by simp with Large have k0: "k > 0" by auto hence n0: "n > 0" using nk by simp from Clique_not_solvable_by_small_monotone_circuit[OF Large \[unfolded nk] _ vars] solution[unfolded s] nk have "real k powr (8 / 7 * real k) < cs \" by auto also have "real k powr (8 / 7 * real k) = root 8 n powr (8 / 7 * root 8 n)" unfolding kn by simp also have "\ = ((root 8 n) powr (8 / 7)) powr (root 8 n)" unfolding powr_powr by simp also have "(root 8 n) powr (8 / 7) = root 7 n" using n0 by (simp add: root_powr_inverse powr_powr) finally show ?thesis . qed end