Session Clique_and_Monotone_Circuits

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 (n2 ^ 4) powr (1 / 8 * real (n2 ^ 4) powr (1 / 8)))" 

definition L0'' :: nat where "L0'' = (SOME l0. ∀ l ≥ l0. real l * log 2 (real (l2 ^ 4)) + 1 < real (l2))" 

lemma L0'': assumes "l ≥ L0''" shows "real l * log 2 (real (l2 ^ 4)) + 1 < real (l2)"
proof -
  have "(λ l :: nat. (real l * log 2 (real (l2 ^ 4)) + 1) / real (l2)) ⇢ 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 (l2 ^ 4)) + 1 < real (l2)" 
    by (auto simp: field_simps)
  hence "∃ l0. ∀ l ≥ l0. real l * log 2 (real (l2 ^ 4)) + 1 < real (l2)" 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})" 
      by (simp add: start_def)
    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 
      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..<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 * L2 * (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 (L2) * ?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 * L2 * (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 * (L2 * (k - 1) ^ m)) / 2 ^ (p - 1)" 
  shows "((m - l) / k)^l / (6 * L^2) < s" 
proof -
  define A where "A = real (L2 * (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 * L2) < 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 * L2"] *
  have "m ^ l / (6 * L2) < 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 (n2 ^ 4) powr (1 / 8 * (real (n2 ^ 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 (l2 ^ 4) powr (1 / 8 * real (l2 ^ 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" 
    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 * L2)" 
    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 * L2)" by simp
  also have "… ≤ ((m - l) / k) ^ l / (?r 12 * L2)" 
    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 
  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] ≡ {..<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" 
  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] →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)
  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