ody>

# Theory Preliminaries

section â¹Preliminariesâº
theory Preliminaries
imports
Main
HOL.Real
"HOL-Library.FuncSet"
begin

lemma exists_subset_between:
assumes
"card A â¤ n"
"n â¤ card C"
"A â C"
"finite C"
shows "âB. A â B â§ B â C â§ card B = n"
using assms
proof (induct n arbitrary: A C)
case 0
thus ?case using finite_subset[of A C] by (intro exI[of _ "{}"], auto)
next
case (Suc n A C)
show ?case
proof (cases "A = {}")
case True
from obtain_subset_with_card_n[OF Suc(3)]
obtain B where "B â C" "card B = Suc n" by metis
thus ?thesis unfolding True by blast
next
case False
then obtain a where a: "a â A" by auto
let ?A = "A - {a}"
let ?C = "C - {a}"
have 1: "card ?A â¤ n" using Suc(2-) a
using finite_subset by fastforce
have 2: "card ?C â¥ n" using Suc(2-) a by auto
from Suc(1)[OF 1 2 _ finite_subset[OF _ Suc(5)]] Suc(2-)
obtain B where "?A â B" "B â ?C" "card B = n" by blast
thus ?thesis using a Suc(2-)
by (intro exI[of _ "insert a B"], auto intro!: card_insert_disjoint finite_subset[of B C])
qed
qed

lemma fact_approx_add: "fact (l + n) â¤ fact l * (real l + real n) ^ n"
proof (induct n arbitrary: l)
case (Suc n l)
have "fact (l + Suc n) = (real l + Suc n) * fact (l + n)" by simp
also have "â¦ â¤ (real l + Suc n) * (fact l * (real l + real n) ^ n)"
by (intro mult_left_mono[OF Suc], auto)
also have "â¦ = fact l * ((real l + Suc n) * (real l + real n) ^ n)" by simp
also have "â¦ â¤ fact l * ((real l + Suc n) * (real l + real (Suc n)) ^ n)"
by (rule mult_left_mono, rule mult_left_mono, rule power_mono, auto)
finally show ?case by simp
qed simp

lemma fact_approx_minus: assumes "k â¥ n"
shows "fact k â¤ fact (k - n) * (real k ^ n)"
proof -
define l where "l = k - n"
from assms have k: "k = l + n" unfolding l_def by auto
show ?thesis unfolding k using fact_approx_add[of l n] by simp
qed

lemma fact_approx_upper_add: assumes al: "a â¤ Suc l" shows "fact l * real a ^ n â¤ fact (l + n)"
proof (induct n)
case (Suc n)
have "fact l * real a ^ (Suc n) = (fact l * real a ^ n) * real a" by simp
also have "â¦ â¤ fact (l + n) * real a"
by (rule mult_right_mono[OF Suc], auto)
also have "â¦ â¤ fact (l + n) * real (Suc (l + n))"
by (intro mult_left_mono, insert al, auto)
also have "â¦ = fact (Suc (l + n))" by simp
finally show ?case by simp
qed simp

lemma fact_approx_upper_minus: assumes "n â¤ k" and "n + a â¤ Suc k"
shows "fact (k - n) * real a ^ n â¤ fact k"
proof -
define l where "l = k - n"
from assms have k: "k = l + n" unfolding l_def by auto
show ?thesis using assms unfolding k
apply simp
apply (rule fact_approx_upper_add, insert assms, auto simp: l_def)
done
qed

lemma choose_mono: "n â¤ m â¹ n choose k â¤ m choose k"
unfolding binomial_def
by (rule card_mono, auto)

lemma div_mult_le: "(a div b) * c â¤ (a * c) div (b :: nat)"
by (metis div_mult2_eq div_mult_mult2 mult.commute mult_0_right times_div_less_eq_dividend)

lemma div_mult_pow_le: "(a div b)^n â¤ a^n div (b :: nat)^n"
proof (cases "b = 0")
case True
thus ?thesis by (cases n, auto)
next
case b: False
then obtain c d where a: "a = b * c + d" and id: "c = a div b" "d = a mod b" by auto
have "(a div b)^n = c^n" unfolding id by simp
also have "â¦ = (b * c)^n div b^n" using b
by (metis div_power dvd_triv_left nonzero_mult_div_cancel_left)
also have "â¦ â¤ (b * c + d)^n div b^n"
by (rule div_le_mono, rule power_mono, auto)
also have "â¦ = a^n div b^n " unfolding a by simp
finally show ?thesis .
qed

lemma choose_inj_right:
assumes id: "(n choose l) = (k choose l)"
and n0: "n choose l â  0"
and l0:  "l â  0"
shows "n = k"
proof (rule ccontr)
assume nk: "n â  k"
define m where "m = min n k"
define M where "M = max n k"
from nk have mM: "m < M" unfolding m_def M_def by auto
let ?new = "insert (M - 1) {0..< l - 1}"
let ?m = "{K â Pow {0..<m}. card K = l}"
let ?M = "{K â Pow {0..<M}. card K = l}"
from id n0 have lM :"l â¤ M" unfolding m_def M_def by auto
from id have id: "(m choose l) = (M choose l)"
unfolding m_def M_def by auto
from this[unfolded binomial_def]
have "card ?M < Suc (card ?m)"
by auto
also have "â¦ = card (insert ?new ?m)"
by (rule sym, rule card_insert_disjoint, force, insert mM, auto)
also have "â¦ â¤ card (insert ?new ?M)"
by (rule card_mono, insert mM, auto)
also have "insert ?new ?M = ?M"
by (insert mM lM l0, auto)
finally show False by simp
qed

lemma card_funcsetE: "finite A â¹ card (A ââ©E B) = card B ^ card A"
by (subst card_PiE, auto)

lemma card_inj_on_subset_funcset: assumes finB: "finite B"
and finC: "finite C"
and AB: "A â B"
shows "card { f. f â B ââ©E C â§ inj_on f A} =
card C^(card B - card A) * prod ((-) (card C)) {0 ..< card A}"
proof -
define D where "D = B - A"
from AB have B: "B = A âª D" and disj: "A â© D = {}" unfolding D_def by auto
have sub: "card B - card A = card D" unfolding D_def using finB AB
by (metis card_Diff_subset finite_subset)
have "finite A" "finite D" using finB unfolding B by auto
thus ?thesis unfolding sub unfolding B using disj
proof (induct A rule: finite_induct)
case empty
from card_funcsetE[OF this(1), of C] show ?case by auto
next
case (insert a A)
have "{f. f â insert a A âª D ââ©E C â§ inj_on f (insert a A)}
= {f(a := c) | f c. f â A âª D ââ©E C â§ inj_on f A â§ c â C - f  A}"
(is "?l = ?r")
proof
show "?r â ?l"
by (auto intro: inj_on_fun_updI split: if_splits)
{
fix f
assume f: "f â ?l"
let ?g = "f(a := undefined)"
let ?h = "?g(a := f a)"
have mem: "f a â C - ?g  A" using insert(1,2,4,5) f by auto
from f have f: "f â insert a A âª D ââ©E C" "inj_on f (insert a A)" by auto
hence "?g â A âª D ââ©E C" "inj_on ?g A" using â¹a â Aâº â¹insert a A â© D = {}âº
by (auto split: if_splits simp: inj_on_def)
with mem have "?h â ?r" by blast
also have "?h = f" by auto
finally have "f â ?r" .
}
thus "?l â ?r" by auto
qed
also have "â¦ = (Î» (f, c). f (a := c))
(Sigma {f . f â A âª D ââ©E C â§ inj_on f A} (Î» f. C - f  A))"
by auto
also have "card (...) = card (Sigma {f . f â A âª D ââ©E C â§ inj_on f A} (Î» f. C - f  A))"
proof (rule card_image, intro inj_onI, clarsimp, goal_cases)
case (1 f c g d)
let ?f = "f(a := c, a := undefined)"
let ?g = "g(a := d, a := undefined)"
from 1 have id: "f(a := c) = g(a := d)" by auto
from fun_upd_eqD[OF id]
have cd: "c = d" by auto
from id have "?f = ?g" by auto
also have "?f = f" using f â A âª D ââ©E C insert(1,2,4,5)
by (intro ext, auto)
also have "?g = g" using g â A âª D ââ©E C insert(1,2,4,5)
by (intro ext, auto)
finally show "f = g â§ c = d" using cd by auto
qed
also have "â¦ = (âfâ{f â A âª D ââ©E C. inj_on f A}. card (C - f  A))"
by (rule card_SigmaI, rule finite_subset[of _ "A âª D ââ©E C"],
insert â¹finite Câº â¹finite Dâº â¹finite Aâº, auto intro!: finite_PiE)
also have "â¦ = (âfâ{f â A âª D ââ©E C. inj_on f A}. card C - card A)"
by (rule sum.cong[OF refl], subst card_Diff_subset, insert â¹finite Aâº, auto simp: card_image)
also have "â¦ = (card C - card A) * card {f â A âª D ââ©E C. inj_on f A}"
by simp
also have "â¦ = card C ^ card D * ((card C - card A) * prod ((-) (card C)) {0..<card A})"
using insert by (auto simp: ac_simps)
also have "(card C - card A) * prod ((-) (card C)) {0..<card A} =
prod ((-) (card C)) {0..<Suc (card A)}" by simp
also have "Suc (card A) = card (insert a A)" using insert by auto
finally show ?case .
qed
qed

end

# Theory Monotone_Formula

section â¹Monotone Formulasâº

text â¹We define monotone formulas, i.e., without negation,
and show that usually the constant TRUE is not required.âº

theory Monotone_Formula
imports Main
begin

subsection â¹Definitionâº

datatype 'a mformula =
TRUE | FALSE |            â â¹True and Falseâº
Var 'a |                  â â¹propositional variablesâº
Conj "'a mformula" "'a mformula" |  â â¹conjunctionâº
Disj "'a mformula" "'a mformula"    â â¹disjunctionâº

text â¹the set of subformulas of a mformulaâº

fun SUB :: "'a mformula â 'a mformula set" where
"SUB (Conj Ï Ï) = {Conj Ï Ï} âª SUB Ï âª SUB Ï"
| "SUB (Disj Ï Ï) = {Disj Ï Ï} âª SUB Ï âª SUB Ï"
| "SUB (Var x) = {Var x}"
| "SUB FALSE = {FALSE}"
| "SUB TRUE = {TRUE}"

text â¹the variables of a mformulaâº

fun vars :: "'a mformula â 'a set" where
"vars (Var x) = {x}"
| "vars (Conj Ï Ï) = vars Ï âª vars Ï"
| "vars (Disj Ï Ï) = vars Ï âª vars Ï"
| "vars FALSE = {}"
| "vars TRUE = {}"

lemma finite_SUB[simp, intro]: "finite (SUB Ï)"
by (induct Ï, auto)

text â¹The circuit-size of a mformula: number of subformulasâº

definition cs :: "'a mformula â nat" where
"cs Ï = card (SUB Ï)"

text â¹variable assignmentsâº

type_synonym 'a VAS = "'a â bool"

text â¹evaluation of mformulasâº

fun eval :: "'a VAS â 'a mformula â bool" where
"eval Î¸ FALSE = False"
| "eval Î¸ TRUE = True"
| "eval Î¸ (Var x) = Î¸ x"
| "eval Î¸ (Disj Ï Ï) = (eval Î¸ Ï â¨ eval Î¸ Ï)"
| "eval Î¸ (Conj Ï Ï) = (eval Î¸ Ï â§ eval Î¸ Ï)"

lemma eval_vars: assumes "â x. x â vars Ï â¹ Î¸1 x = Î¸2 x"
shows "eval Î¸1 Ï = eval Î¸2 Ï"
using assms by (induct Ï, auto)

subsection â¹Conversion of mformulas to true-free mformulasâº

inductive_set tf_mformula :: "'a mformula set" where
tf_False: "FALSE â tf_mformula"
| tf_Var: "Var x â tf_mformula"
| tf_Disj: "Ï â tf_mformula â¹ Ï â tf_mformula â¹ Disj Ï Ï â tf_mformula"
| tf_Conj: "Ï â tf_mformula â¹ Ï â tf_mformula â¹ Conj Ï Ï â tf_mformula"

fun to_tf_formula where
"to_tf_formula (Disj phi psi) = (let phi' = to_tf_formula phi; psi' = to_tf_formula psi
in (if phi' = TRUE â¨ psi' = TRUE then TRUE else Disj phi' psi'))"
| "to_tf_formula (Conj phi psi) = (let phi' = to_tf_formula phi; psi' = to_tf_formula psi
in (if phi' = TRUE then psi' else if psi' = TRUE then phi' else Conj phi' psi'))"
| "to_tf_formula phi = phi"

lemma eval_to_tf_formula: "eval Î¸ (to_tf_formula Ï) = eval Î¸ Ï"
by (induct Ï rule: to_tf_formula.induct, auto simp: Let_def)

lemma to_tf_formula: "to_tf_formula Ï â  TRUE â¹ to_tf_formula Ï â tf_mformula"
by (induct Ï, auto simp: Let_def intro: tf_mformula.intros)

lemma vars_to_tf_formula: "vars (to_tf_formula Ï) â vars Ï"
by (induct Ï rule: to_tf_formula.induct, auto simp: Let_def)

lemma SUB_to_tf_formula: "SUB (to_tf_formula Ï) â to_tf_formula  SUB Ï"
by (induct Ï rule: to_tf_formula.induct, auto simp: Let_def)

lemma cs_to_tf_formula: "cs (to_tf_formula Ï) â¤ cs Ï"
proof -
have "cs (to_tf_formula Ï) â¤ card (to_tf_formula  SUB Ï)"
unfolding cs_def by (rule card_mono[OF finite_imageI[OF finite_SUB] SUB_to_tf_formula])
also have "â¦ â¤ cs Ï" unfolding cs_def
by (rule card_image_le[OF finite_SUB])
finally show "cs (to_tf_formula Ï) â¤ cs Ï" .
qed

lemma to_tf_mformula: assumes "Â¬ eval Î¸ Ï"
shows "â Ï â tf_mformula. (â Î¸. eval Î¸ Ï = eval Î¸ Ï) â§ vars Ï â vars Ï â§ cs Ï â¤ cs Ï"
proof (intro bexI[of _ "to_tf_formula Ï"] conjI allI eval_to_tf_formula[symmetric] vars_to_tf_formula to_tf_formula)
from assms have "Â¬ eval Î¸ (to_tf_formula Ï)" by (simp add: eval_to_tf_formula)
thus "to_tf_formula Ï â  TRUE" by auto
show "cs (to_tf_formula Ï) â¤ cs Ï" by (rule cs_to_tf_formula)
qed

end
tle>

# Theory Assumptions_and_Approximations

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"

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â§2 ^ 4) powr (1 / 8 * real (nâ§2 ^ 4) powr (1 / 8)))"

definition L0'' :: nat where "L0'' = (SOME l0. â l â¥ l0. real l * log 2 (real (lâ§2 ^ 4)) + 1 < real (lâ§2))"

lemma L0'': assumes "l â¥ L0''" shows "real l * log 2 (real (lâ§2 ^ 4)) + 1 < real (lâ§2)"
proof -
have "(Î» l :: nat. (real l * log 2 (real (lâ§2 ^ 4)) + 1) / real (lâ§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)â§2 < 1" by (auto simp: field_simps)
hence "â l â¥ max 1 l0. real l * log 2 (real (lâ§2 ^ 4)) + 1 < real (lâ§2)"
by (auto simp: field_simps)
hence "â l0. â l â¥ l0. real l * log 2 (real (lâ§2 ^ 4)) + 1 < real (lâ§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..<l}
> (real (k - 1)) ^ m / 3"
proof -
have "real (k - 1) ^ (m - l) * (âi = 0..<l. real (k - 1 - i)) =
real (k - 1) ^ m *
(inverse (real (k - 1)) ^ l * (âi = 0..<l. real (k - 1 - i)))"
by (subst power_diff_conv_inverse, insert k2 lm, auto)
also have "â¦ > (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..<l. real (k - 1 - i))"
have "uminus start
= uminus (prod (Î» _. inverse (real (k - 1))) {0..<l} * prod (Î» i. real (k - 1 - i)) {0 ..< l})"
also have "â¦ = uminus (prod (Î» i. inverse (real (k - 1)) * real (k - 1 - i)) {0..<l})"
by (subst prod.distrib, simp)
also have "â¦ â¤ uminus (prod (Î» i. inverse (real (k - 1)) * real (k - 1 - (l - 1))) {0..<l})"
unfolding neg_le_iff_le
by (intro prod_mono conjI mult_left_mono, insert k2 l2, auto intro!: diff_le_mono2)
also have "â¦ = 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
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
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..<l. real (k - 1 - i)) > 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â§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â§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â§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
also have "â¦ â· b * (m - l)^l / c â¤ (m choose k)"
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
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â§2 * (k - 1) ^ m)) / 2 ^ (p - 1)"
shows "((m - l) / k)^l / (6 * L^2) < s"
proof -
define A where "A = real (Lâ§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"
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"
finally have *: "2 powr p / (6 * Lâ§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â§2"] *
have "m ^ l / (6 * Lâ§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"
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"
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
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"
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â§2 ^ 4) powr (1 / 8 * (real (nâ§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â§2 ^ 4) powr (1 / 8 * real (lâ§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
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"
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"
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"
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
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â§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â§2)" by simp
also have "â¦ â¤ ((m - l) / k) ^ l / (?r 12 * Lâ§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
tle>

# Theory Clique_Large_Monotone_Circuits

theory Clique_Large_Monotone_Circuits
imports
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] â¡ {..<n}"

lemma card_sameprod: "finite X â¹ 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"

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] ââ©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}"

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)
from p have p0: "p â  0" by auto
have "(p - 1) ^ l * fact l < card ?vXp"  using L[unfolded L_def]
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]
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