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 = (X ⊙ Y) ∩ 𝒢l"
lemma joinl_join: "X ⊙l Y ⊆ X ⊙ Y"
unfolding odot_def odotl_def by blast
lemma card_v_gs_join: assumes X: "X ⊆ 𝒢" and Y: "Y ⊆ 𝒢"
and Z: "Z ⊆ X ⊙ Y"
shows "card (v_gs Z) ≤ card (v_gs X) * card (v_gs Y)"
proof -
note fin = finite_v_gs[OF X] finite_v_gs[OF Y]
have "card (v_gs Z) ≤ card ((λ (A, B). A ∪ B) ` (v_gs X × v_gs Y))"
proof (rule card_mono[OF finite_imageI])
show "finite (v_gs X × v_gs Y)"
using fin by auto
have "v_gs Z ⊆ v_gs (X ⊙ Y)"
using v_gs_mono[OF Z] .
also have "… ⊆ (λ(x, y). x ∪ y) ` (v_gs X × v_gs Y)" (is "?L ⊆ ?R")
unfolding odot_def v_gs_def by (force split: if_splits simp: v_union)
finally show "v_gs Z ⊆ (λ(x, y). x ∪ y) ` (v_gs X × v_gs Y)" .
qed
also have "… ≤ card (v_gs X × v_gs Y)"
by (rule card_image_le, insert fin, auto)
also have "… = card (v_gs X) * card (v_gs Y)"
by (rule card_cartesian_product)
finally show ?thesis .
qed
text ‹Definition 6 -- elementary plucking step›
definition plucking_step :: "graph set ⇒ graph set" where
"plucking_step X = (let vXp = v_gs X;
S = (SOME S. S ⊆ vXp ∧ sunflower S ∧ card S = p);
U = {E ∈ X. v E ∈ S};
Vs = ⋂ S;
Gs = Vs^𝟮
in X - U ∪ {Gs})"
end
context second_assumptions
begin
text ‹Lemma 9 -- for elementary plucking step›
lemma v_sameprod_subset: "v (Vs^𝟮) ⊆ Vs" unfolding binprod_def v_def
by (auto simp: doubleton_eq_iff)
lemma plucking_step: assumes X: "X ⊆ 𝒢l"
and L: "card (v_gs X) > L"
and Y: "Y = plucking_step X"
shows "card (v_gs Y) ≤ card (v_gs X) - p + 1"
"Y ⊆ 𝒢l"
"POS ∩ ACC X ⊆ ACC Y"
"2 ^ p * card (ACC_cf Y - ACC_cf X) ≤ (k - 1) ^ m"
"Y ≠ {}"
proof -
let ?vXp = "v_gs X"
have sf_precond: "∀A∈ ?vXp. finite A ∧ card A ≤ l"
using X unfolding 𝒢l_def 𝒢l_def v_gs_def by (auto intro: finite_vG intro!: v_𝒢 v_card2)
note sunflower = Erdos_Rado_sunflower[OF sf_precond]
from p have p0: "p ≠ 0" by auto
have "(p - 1) ^ l * fact l < card ?vXp" using L[unfolded L_def]
by (simp add: ac_simps)
note sunflower = sunflower[OF this]
define S where "S = (SOME S. S ⊆ ?vXp ∧ sunflower S ∧ card S = p)"
define U where "U = {E ∈ X. v E ∈ S}"
define Vs where "Vs = ⋂ S"
define Gs where "Gs = Vs^𝟮"
let ?U = U
let ?New = "Gs :: graph"
have Y: "Y = X - U ∪ {?New}"
using Y[unfolded plucking_step_def Let_def, folded S_def, folded U_def,
folded Vs_def, folded Gs_def] .
have U: "U ⊆ 𝒢l" using X unfolding U_def by auto
hence "U ⊆ 𝒢" unfolding 𝒢l_def by auto
from sunflower
have "∃ S. S ⊆ ?vXp ∧ sunflower S ∧ card S = p" by auto
from someI_ex[OF this, folded S_def]
have S: "S ⊆ ?vXp" "sunflower S" "card S = p" by (auto simp: Vs_def)
have fin1: "finite ?vXp" using finite_v_gs_Gl[OF X] .
from X have finX: "finite X" unfolding 𝒢l_def
using finite_subset[of X, OF _ finite_𝒢] by auto
from fin1 S have finS: "finite S" by (metis finite_subset)
from finite_subset[OF _ finX] have finU: "finite U" unfolding U_def by auto
from S p have Snempty: "S ≠ {}" by auto
have UX: "U ⊆ X" unfolding U_def by auto
{
from Snempty obtain s where sS: "s ∈ S" by auto
with S have "s ∈ v_gs X" by auto
then obtain Sp where "Sp ∈ X" and sSp: "s = v Sp"
unfolding v_gs_def by auto
hence *: "Sp ∈ U" using ‹s ∈ S› unfolding U_def by auto
from * X UX have le: "card (v Sp) ≤ l" "finite (v Sp)" "Sp ∈ 𝒢"
unfolding 𝒢l_def 𝒢l_def using finite_vG[of Sp] by auto
hence m: "v Sp ⊆ [m]" by (intro v_𝒢)
have "Vs ⊆ v Sp" using sS sSp unfolding Vs_def by auto
with card_mono[OF ‹finite (v Sp)› this] finite_subset[OF this ‹finite (v Sp)›] le * m
have "card Vs ≤ l" "U ≠ {}" "finite Vs" "Vs ⊆ [m]" by auto
}
hence card_Vs: "card Vs ≤ l" and Unempty: "U ≠ {}"
and fin_Vs: "finite Vs" and Vsm: "Vs ⊆ [m]" by auto
have vGs: "v Gs ⊆ Vs" unfolding Gs_def by (rule v_sameprod_subset)
have GsG: "Gs ∈ 𝒢" unfolding Gs_def 𝒢_def
by (intro CollectI Inter_subset sameprod_mono Vsm)
have GsGl: "Gs ∈ 𝒢l" unfolding 𝒢l_def using GsG vGs card_Vs card_mono[OF _ vGs]
by (simp add: fin_Vs)
hence DsDl: "?New ∈ 𝒢l" using UX
unfolding 𝒢l_def 𝒢_def 𝒢l_def 𝒢_def by auto
with X U show "Y ⊆ 𝒢l" unfolding Y by auto
from X have XD: "X ⊆ 𝒢" unfolding 𝒢l_def by auto
have vplus_dsU: "v_gs U = S" using S(1)
unfolding v_gs_def U_def by force
have vplus_dsXU: "v_gs (X - U) = v_gs X - v_gs U"
unfolding v_gs_def U_def by auto
have "card (v_gs Y) = card (v_gs (X - U ∪ {?New}))"
unfolding Y by simp
also have "v_gs (X - U ∪ {?New}) = v_gs (X - U) ∪ v_gs ({?New})"
unfolding v_gs_union ..
also have "v_gs ({?New}) = {v (Gs)}" unfolding v_gs_def image_comp o_def by simp
also have "card (v_gs (X - U) ∪ …) ≤ card (v_gs (X - U)) + card …"
by (rule card_Un_le)
also have "… ≤ card (v_gs (X - U)) + 1" by auto
also have "v_gs (X - U) = v_gs X - v_gs U" by fact
also have "card … = card (v_gs X) - card (v_gs U)"
by (rule card_Diff_subset, force simp: vplus_dsU finS,
insert UX, auto simp: v_gs_def)
also have "card (v_gs U) = card S" unfolding vplus_dsU ..
finally show "card (v_gs Y) ≤ card (v_gs X) - p + 1"
using S by auto
show "Y ≠ {}" unfolding Y using Unempty by auto
{
fix G
assume "G ∈ ACC X" and GPOS: "G ∈ POS"
from this[unfolded ACC_def] POS_𝒢 have G: "G ∈ 𝒢" "X ⊩ G" by auto
from this[unfolded accepts_def] obtain D :: graph where
D: "D ∈ X" "D ⊆ G" by auto
have "G ∈ ACC Y"
proof (cases "D ∈ Y")
case True
with D G show ?thesis unfolding accepts_def ACC_def by auto
next
case False
with D have DU: "D ∈ U" unfolding Y by auto
from GPOS[unfolded POS_def 𝒦_def] obtain K where GK: "G = (v K)^𝟮" "card (v K) = k" by auto
from DU[unfolded U_def] have "v D ∈ S" by auto
hence "Vs ⊆ v D" unfolding Vs_def by auto
also have "… ⊆ v G"
by (intro v_mono D)
also have "… = v K" unfolding GK
by (rule v_sameprod, unfold GK, insert k2, auto)
finally have "Gs ⊆ G" unfolding Gs_def GK
by (intro sameprod_mono)
with D DU have "D ∈ ?U" "?New ⊆ G" by (auto)
hence "Y ⊩ G" unfolding accepts_def Y by auto
thus ?thesis using G by auto
qed
}
thus "POS ∩ ACC X ⊆ ACC Y" by auto
from ex_bij_betw_nat_finite[OF finS, unfolded ‹card S = p›]
obtain Si where Si: "bij_betw Si {0 ..< p} S" by auto
define G where "G = (λ i. SOME Gb. Gb ∈ X ∧ v Gb = Si i)"
{
fix i
assume "i < p"
with Si have SiS: "Si i ∈ S" unfolding bij_betw_def by auto
with S have "Si i ∈ v_gs X" by auto
hence "∃ G. G ∈ X ∧ v G = Si i"
unfolding v_gs_def by auto
from someI_ex[OF this]
have "(G i) ∈ X ∧ v (G i) = Si i"
unfolding G_def by blast
hence "G i ∈ X" "v (G i) = Si i"
"G i ∈ U" "v (G i) ∈ S" using SiS unfolding U_def
by auto
} note G = this
have SvG: "S = v ` G ` {0 ..< p}" unfolding Si[unfolded bij_betw_def,
THEN conjunct2, symmetric] image_comp o_def using G(2) by auto
have injG: "inj_on G {0 ..< p}"
proof (standard, goal_cases)
case (1 i j)
hence "Si i = Si j" using G[of i] G[of j] by simp
with 1(1,2) Si show "i = j"
by (metis Si bij_betw_iff_bijections)
qed
define r where "r = card U"
have rq: "r ≥ p" unfolding r_def ‹card S = p›[symmetric] vplus_dsU[symmetric]
unfolding v_gs_def
by (rule card_image_le[OF finU])
let ?Vi = "λ i. v (G i)"
let ?Vis = "λ i. ?Vi i - Vs"
define s where "s = card Vs"
define si where "si i = card (?Vi i)" for i
define ti where "ti i = card (?Vis i)" for i
{
fix i
assume i: "i < p"
have Vs_Vi: "Vs ⊆ ?Vi i" using i unfolding Vs_def
using G[OF i] unfolding SvG by auto
have finVi: "finite (?Vi i)"
using G(4)[OF i] S(1) sf_precond
by (meson finite_numbers finite_subset subset_eq)
from S(1) have "G i ∈ 𝒢" using G(1)[OF i] X unfolding 𝒢l_def 𝒢_def 𝒢l_def by auto
hence finGi: "finite (G i)"
using finite_members_𝒢 by auto
have ti: "ti i = si i - s" unfolding ti_def si_def s_def
by (rule card_Diff_subset[OF fin_Vs Vs_Vi])
have size1: "s ≤ si i" unfolding s_def si_def
by (intro card_mono finVi Vs_Vi)
have size2: "si i ≤ l" unfolding si_def using G(4)[OF i] S(1) sf_precond by auto
note Vs_Vi finVi ti size1 size2 finGi ‹G i ∈ 𝒢›
} note i_props = this
define fstt where "fstt e = (SOME x. x ∈ e ∧ x ∉ Vs)" for e
define sndd where "sndd e = (SOME x. x ∈ e ∧ x ≠ fstt e)" for e
{
fix e :: "nat set"
assume *: "card e = 2" "¬ e ⊆ Vs"
from *(1) obtain x y where e: "e = {x,y}" "x ≠ y"
by (meson card_2_iff)
with * have "∃ x. x ∈ e ∧ x ∉ Vs" by auto
from someI_ex[OF this, folded fstt_def]
have fst: "fstt e ∈ e" "fstt e ∉ Vs" by auto
with * e have "∃ x. x ∈ e ∧ x ≠ fstt e"
by (metis insertCI)
from someI_ex[OF this, folded sndd_def] have snd: "sndd e ∈ e" "sndd e ≠ fstt e" by auto
from fst snd e have "{fstt e, sndd e} = e" "fstt e ∉ Vs" "fstt e ≠ sndd e" by auto
} note fstt = this
{
fix f
assume "f ∈ ACC_cf Y - ACC_cf X"
hence fake: "f ∈ ACC_cf {?New} - ACC_cf U" unfolding Y ACC_cf_def accepts_def
Diff_iff U_def Un_iff mem_Collect_eq by blast
hence f: "f ∈ ℱ" using ACC_cf_ℱ by auto
hence "C f ∈ NEG" unfolding NEG_def by auto
with NEG_𝒢 have Cf: "C f ∈ 𝒢" by auto
from fake have "f ∈ ACC_cf {?New}" by auto
from this[unfolded ACC_cf_def accepts_def] Cf
have GsCf: "Gs ⊆ C f" and Cf: "C f ∈ 𝒢" by auto
from fake have "f ∉ ACC_cf U" by auto
from this[unfolded ACC_cf_def] Cf f have "¬ (U ⊩ C f)" by auto
from this[unfolded accepts_def]
have UCf: "D ∈ U ⟹ ¬ D ⊆ C f" for D by auto
let ?prop = "λ i e. fstt e ∈ v (G i) - Vs ∧
sndd e ∈ v (G i) ∧ e ∈ G i ∩ ([m]^𝟮)
∧ f (fstt e) = f (sndd e) ∧ f (sndd e) ∈ [k - 1] ∧ {fstt e, sndd e} = e"
define pair where "pair i = (if i < p then (SOME pair. ?prop i pair) else undefined)" for i
define u where "u i = fstt (pair i)" for i
define w where "w i = sndd (pair i)" for i
{
fix i
assume i: "i < p"
from i have "?Vi i ∈ S" unfolding SvG by auto
hence "Vs ⊆ ?Vi i" unfolding Vs_def by auto
from sameprod_mono[OF this, folded Gs_def]
have *: "Gs ⊆ v (G i)^𝟮" .
from i have Gi: "G i ∈ U" using G[OF i] by auto
from UCf[OF Gi] i_props[OF i] have "¬ G i ⊆ C f" and Gi: "G i ∈ 𝒢" by auto
then obtain edge where
edgep: "edge ∈ G i" and edgen: "edge ∉ C f" by auto
from edgep Gi obtain x y where edge: "edge = {x,y}"
and xy: "{x,y} ∈ [m]^𝟮" "{x,y} ⊆ [m]" "card {x,y} = 2" unfolding 𝒢_def binprod_def
by force
define a where "a = fstt edge"
define b where "b = sndd edge"
from edgen[unfolded C_def edge] xy have id: "f x = f y" by simp
from edgen GsCf edge have edgen: "{x,y} ∉ Gs" by auto
from edgen[unfolded Gs_def sameprod_altdef] xy have "¬ {x,y} ⊆ Vs" by auto
from fstt[OF ‹card {x,y} = 2› this, folded edge, folded a_def b_def] edge
have a: "a ∉ Vs" and id_ab: "{x,y} = {a,b}" by auto
from id_ab id have id: "f a = f b" by (auto simp: doubleton_eq_iff)
let ?pair = "(a,b)"
note ab = xy[unfolded id_ab]
from f[unfolded ℱ_def] ab have fb: "f b ∈ [k - 1]" by auto
note edge = edge[unfolded id_ab]
from edgep[unfolded edge] v_mem_sub[OF ‹card {a,b} = 2›, of "G i"] id
have "?prop i edge" using edge ab a fb unfolding a_def b_def by auto
from someI[of "?prop i", OF this] have "?prop i (pair i)" using i unfolding pair_def by auto
from this[folded u_def w_def] edgep
have "u i ∈ v (G i) - Vs" "w i ∈ v (G i)" "pair i ∈ G i ∩ [m]^𝟮"
"f (u i) = f (w i)" "f (w i) ∈ [k - 1]" "pair i = {u i, w i}"
by auto
} note uw = this
from uw(3) have Pi: "pair ∈ Pi⇩E {0 ..< p} G" unfolding pair_def by auto
define Us where "Us = u ` {0 ..< p}"
define Ws where "Ws = [m] - Us"
{
fix i
assume i: "i < p"
note uwi = uw[OF this]
from uwi have ex: "∃ x ∈ [k - 1]. f ` {u i, w i} = {x}" by auto
from uwi have *: "u i ∈ [m]" "w i ∈ [m]" "{u i, w i} ∈ G i" by (auto simp: sameprod_altdef)
have "w i ∉ Us"
proof
assume "w i ∈ Us"
then obtain j where j: "j < p" and wij: "w i = u j" unfolding Us_def by auto
with uwi have ij: "i ≠ j" unfolding binprod_def by auto
note uwj = uw[OF j]
from ij i j Si[unfolded bij_betw_def]
have diff: "v (G i) ≠ v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto
from uwi wij have uj: "u j ∈ v (G i)" by auto
with ‹sunflower S›[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uwj(1) diff
have "u j ∈ ⋂ S" by blast
with uwj(1)[unfolded Vs_def] show False by simp
qed
with * have wi: "w i ∈ Ws" unfolding Ws_def by auto
from uwi have wi2: "w i ∈ v (G i)" by auto
define W where "W = Ws ∩ v (G i)"
from G(1)[OF i] X[unfolded 𝒢l_def 𝒢l_def] i_props[OF i]
have "finite (v (G i))" "card (v (G i)) ≤ l" by auto
with card_mono[OF this(1), of W] have
W: "finite W" "card W ≤ l" "W ⊆ [m] - Us" unfolding W_def Ws_def by auto
from wi wi2 have wi: "w i ∈ W" unfolding W_def by auto
from wi ex W * have "{u i, w i} ∈ G i ∧ u i ∈ [m] ∧ w i ∈ [m] - Us ∧ f (u i) = f (w i)" by force
} note uw1 = this
have inj: "inj_on u {0 ..< p}"
proof -
{
fix i j
assume i: "i < p" and j: "j < p"
and id: "u i = u j" and ij: "i ≠ j"
from ij i j Si[unfolded bij_betw_def]
have diff: "v (G i) ≠ v (G j)" unfolding G(2)[OF i] G(2)[OF j] inj_on_def by auto
from uw[OF i] have ui: "u i ∈ v (G i) - Vs" by auto
from uw[OF j, folded id] have uj: "u i ∈ v (G j)" by auto
with ‹sunflower S›[unfolded sunflower_def, rule_format] G(4)[OF i] G(4)[OF j] uw[OF i] diff
have "u i ∈ ⋂ S" by blast
with ui have False unfolding Vs_def by auto
}
thus ?thesis unfolding inj_on_def by fastforce
qed
have card: "card ([m] - Us) = m - p"
proof (subst card_Diff_subset)
show "finite Us" unfolding Us_def by auto
show "Us ⊆ [m]" unfolding Us_def using uw1 by auto
have "card Us = p" unfolding Us_def using inj
by (simp add: card_image)
thus "card [m] - card Us = m - p" by simp
qed
hence "(∀ i < p. pair i ∈ G i) ∧ inj_on u {0 ..< p} ∧ (∀ i < p. w i ∈ [m] - u ` {0 ..< p} ∧ f (u i) = f (w i))"
using inj uw1 uw unfolding Us_def by auto
from this[unfolded u_def w_def] Pi card[unfolded Us_def u_def w_def]
have "∃ e ∈ Pi⇩E {0..<p} G. (∀i<p. e i ∈ G i) ∧
card ([m] - (λi. fstt (e i)) ` {0..<p}) = m - p ∧
(∀i<p. sndd (e i) ∈ [m] - (λi. fstt (e i)) ` {0..<p} ∧ f (fstt (e i)) = f (sndd (e i)))"
by blast
} note fMem = this
define Pi2 where "Pi2 W = Pi⇩E ([m] - W) (λ _. [k - 1])" for W
define merge where "merge =
(λ e (g :: nat ⇒ nat) v. if v ∈ (λ i. fstt (e i)) ` {0 ..< p} then g (sndd (e (SOME i. i < p ∧ v = fstt (e i)))) else g v)"
let ?W = "λ e. (λ i. fstt (e i)) ` {0..<p}"
have "ACC_cf Y - ACC_cf X ⊆ { merge e g | e g. e ∈ Pi⇩E {0..<p} G ∧ card ([m] - ?W e) = m - p ∧ g ∈ Pi2 (?W e)}"
(is "_ ⊆ ?R")
proof
fix f
assume mem: "f ∈ ACC_cf Y - ACC_cf X"
with ACC_cf_ℱ have "f ∈ ℱ" by auto
hence f: "f ∈ [m] →⇩E [k - 1]" unfolding ℱ_def .
from fMem[OF mem] obtain e where e: "e ∈ Pi⇩E {0..<p} G"
"⋀ i. i<p ⟹ e i ∈ G i"
"card ([m] - ?W e) = m - p"
"⋀ i. i<p ⟹ sndd (e i) ∈ [m] - ?W e ∧ f (fstt (e i)) = f (sndd (e i))" by auto
define W where "W = ?W e"
note e = e[folded W_def]
let ?g = "restrict f ([m] - W)"
let ?h = "merge e ?g"
have "f ∈ ?R"
proof (intro CollectI exI[of _ e] exI[of _ ?g], unfold W_def[symmetric], intro conjI e)
show "?g ∈ Pi2 W" unfolding Pi2_def using f by auto
{
fix v :: nat
have "?h v = f v"
proof (cases "v ∈ W")
case False
thus ?thesis using f unfolding merge_def unfolding W_def[symmetric] by auto
next
case True
from this[unfolded W_def] obtain i where i: "i < p" and v: "v = fstt (e i)" by auto
define j where "j = (SOME j. j < p ∧ v = fstt (e j))"
from i v have "∃ j. j < p ∧ v = fstt (e j)" by auto
from someI_ex[OF this, folded j_def] have j: "j < p" and v: "v = fstt (e j)" by auto
have "?h v = restrict f ([m] - W) (sndd (e j))"
unfolding merge_def unfolding W_def[symmetric] j_def using True by auto
also have "… = f (sndd (e j))" using e(4)[OF j] by auto
also have "… = f (fstt (e j))" using e(4)[OF j] by auto
also have "… = f v" using v by simp
finally show ?thesis .
qed
}
thus "f = ?h" by auto
qed
thus "f ∈ ?R" by auto
qed
also have "… ⊆ (λ (e,g). (merge e g)) ` (Sigma (Pi⇩E {0..<p} G ∩ {e. card ([m] - ?W e) = m - p}) (λ e. Pi2 (?W e)))"
(is "_ ⊆ ?f ` ?R")
by auto
finally have sub: "ACC_cf Y - ACC_cf X ⊆ ?f ` ?R" .
have fin[simp,intro]: "finite [m]" "finite [k - Suc 0]" unfolding numbers_def by auto
have finPie[simp, intro]: "finite (Pi⇩E {0..<p} G)"
by (intro finite_PiE, auto intro: i_props)
have finR: "finite ?R" unfolding Pi2_def
by (intro finite_SigmaI finite_Int allI finite_PiE i_props, auto)
have "card (ACC_cf Y - ACC_cf X) ≤ card (?f ` ?R)"
by (rule card_mono[OF finite_imageI[OF finR] sub])
also have "… ≤ card ?R"
by (rule card_image_le[OF finR])
also have "… = (∑e∈(Pi⇩E {0..<p} G ∩ {e. card ([m] - ?W e) = m - p}). card (Pi2 (?W e)))"
by (rule card_SigmaI, unfold Pi2_def,
(intro finite_SigmaI allI finite_Int finite_PiE i_props, auto)+)
also have "… = (∑e∈Pi⇩E {0..<p} G ∩ {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (card ([m] - ?W e)))"
by (rule sum.cong[OF refl], unfold Pi2_def, subst card_PiE, auto)
also have "… = (∑e∈Pi⇩E {0..<p} G ∩ {e. card ([m] - ?W e) = m - p}. (k - 1) ^ (m - p))"
by (rule sum.cong[OF refl], rule arg_cong[of _ _ "λ n. (k - 1)^n"], auto)
also have "… ≤ (∑e∈Pi⇩E {0..<p} G. (k - 1) ^ (m - p))"
by (rule sum_mono2, auto)
also have "… = card (Pi⇩E {0..<p} G) * (k - 1) ^ (m - p)" by simp
also have "… = (∏i = 0..<p. card (G i)) * (k - 1) ^ (m - p)"
by (subst card_PiE, auto)
also have "… ≤ (∏i = 0..<p. (k - 1) div 2) * (k - 1) ^ (m - p)"
proof -
{
fix i
assume i: "i < p"
from G[OF i] X
have GiG: "G i ∈ 𝒢"
unfolding 𝒢l_def 𝒢_def 𝒢_def sameprod_altdef by force
from i_props[OF i] have finGi: "finite (G i)" by auto
have finvGi: "finite (v (G i))" by (rule finite_vG, insert i_props[OF i], auto)
have "card (G i) ≤ card ((v (G i))^𝟮)"
by (intro card_mono[OF sameprod_finite], rule finvGi, rule v_𝒢_2[OF GiG])
also have "… ≤ l choose 2"
proof (subst card_sameprod[OF finvGi], rule choose_mono)
show "card (v (G i)) ≤ l" using i_props[OF i] unfolding ti_def si_def by simp
qed
also have "l choose 2 = l * (l - 1) div 2" unfolding choose_two by simp
also have "l * (l - 1) = k - l" unfolding kl2 power2_eq_square by (simp add: algebra_simps)
also have "… div 2 ≤ (k - 1) div 2"
by (rule div_le_mono, insert l2, auto)
finally have "card (G i) ≤ (k - 1) div 2" .
}
thus ?thesis by (intro mult_right_mono prod_mono, auto)
qed
also have "… = ((k - 1) div 2) ^ p * (k - 1) ^ (m - p)"
by simp
also have "… ≤ ((k - 1) ^ p div (2^p)) * (k - 1) ^ (m - p)"
by (rule mult_right_mono; auto simp: div_mult_pow_le)
also have "… ≤ ((k - 1) ^ p * (k - 1) ^ (m - p)) div 2^p"
by (rule div_mult_le)
also have "… = (k - 1)^m div 2^p"
proof -
have "p + (m - p) = m" using mp by simp
thus ?thesis by (subst power_add[symmetric], simp)
qed
finally have "card (ACC_cf Y - ACC_cf X) ≤ (k - 1) ^ m div 2 ^ p" .
hence "2 ^ p * card (ACC_cf Y - ACC_cf X) ≤ 2^p * ((k - 1) ^ m div 2 ^ p)" by simp
also have "… ≤ (k - 1)^m" by simp
finally show "2^p * card (ACC_cf Y - ACC_cf X) ≤ (k - 1) ^ m" .
qed
text ‹Definition 6›
function PLU_main :: "graph set ⇒ graph set × nat" where
"PLU_main X = (if X ⊆ 𝒢l ∧ L < card (v_gs X) then
map_prod id Suc (PLU_main (plucking_step X)) else
(X, 0))"
by pat_completeness auto
termination
proof (relation "measure (λ X. card (v_gs X))", force, goal_cases)
case (1 X)
hence "X ⊆ 𝒢l" and LL: "L < card (v_gs X)" by auto
from plucking_step(1)[OF this refl]
have "card (v_gs (plucking_step X)) ≤ card (v_gs X) - p + 1" .
also have "… < card (v_gs X)" using p L3 LL
by auto
finally show ?case by simp
qed
declare PLU_main.simps[simp del]
definition PLU :: "graph set ⇒ graph set" where
"PLU X = fst (PLU_main X)"
text ‹Lemma 7›
lemma PLU_main_n: assumes "X ⊆ 𝒢l" and "PLU_main X = (Z, n)"
shows "n * (p - 1) ≤ card (v_gs X)"
using assms
proof (induct X arbitrary: Z n rule: PLU_main.induct)
case (1 X Z n)
note [simp] = PLU_main.simps[of X]
show ?case
proof (cases "card (v_gs X) ≤ L")
case True
thus ?thesis using 1 by auto
next
case False
define Y where "Y = plucking_step X"
obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q"
using ‹PLU_main X = (Z,n)›[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto)
from False have L: "card (v_gs X) > L" by auto
note step = plucking_step[OF 1(2) this Y_def]
from False 1 have "X ⊆ 𝒢l ∧ L < card (v_gs X)" by auto
note IH = 1(1)[folded Y_def, OF this step(2) PLU]
have "n * (p - 1) = (p - 1) + q * (p - 1)" unfolding n by simp
also have "… ≤ (p - 1) + card (v_gs Y)" using IH by simp
also have "… ≤ p - 1 + (card (v_gs X) - p + 1)" using step(1) by simp
also have "… = card (v_gs X)" using L Lp p by simp
finally show ?thesis .
qed
qed
text ‹Definition 8›
definition sqcup :: "graph set ⇒ graph set ⇒ graph set" (infixl "⊔" 65) where
"X ⊔ Y = PLU (X ∪ Y)"
definition sqcap :: "graph set ⇒ graph set ⇒ graph set" (infixl "⊓" 65) where
"X ⊓ Y = PLU (X ⊙l Y)"
definition deviate_pos_cup :: "graph set ⇒ graph set ⇒ graph set" ("∂⊔Pos") where
"∂⊔Pos X Y = POS ∩ ACC (X ∪ Y) - ACC (X ⊔ Y)"
definition deviate_pos_cap :: "graph set ⇒ graph set ⇒ graph set" ("∂⊓Pos") where
"∂⊓Pos X Y = POS ∩ ACC (X ⊙ Y) - ACC (X ⊓ Y)"
definition deviate_neg_cup :: "graph set ⇒ graph set ⇒ colorf set" ("∂⊔Neg") where
"∂⊔Neg X Y = ACC_cf (X ⊔ Y) - ACC_cf (X ∪ Y)"
definition deviate_neg_cap :: "graph set ⇒ graph set ⇒ colorf set" ("∂⊓Neg") where
"∂⊓Neg X Y = ACC_cf (X ⊓ Y) - ACC_cf (X ⊙ Y)"
text ‹Lemma 9 -- without applying Lemma 7›
lemma PLU_main: assumes "X ⊆ 𝒢l"
and "PLU_main X = (Z, n)"
shows "Z ∈ 𝒫L𝒢l
∧ (Z = {} ⟷ X = {})
∧ POS ∩ ACC X ⊆ ACC Z
∧ 2 ^ p * card (ACC_cf Z - ACC_cf X) ≤ (k - 1) ^ m * n"
using assms
proof (induct X arbitrary: Z n rule: PLU_main.induct)
case (1 X Z n)
note [simp] = PLU_main.simps[of X]
show ?case
proof (cases "card (v_gs X) ≤ L")
case True
from True show ?thesis using 1 by (auto simp: id 𝒫L𝒢l_def)
next
case False
define Y where "Y = plucking_step X"
obtain q where PLU: "PLU_main Y = (Z, q)" and n: "n = Suc q"
using ‹PLU_main X = (Z,n)›[unfolded PLU_main.simps[of X], folded Y_def] using False 1(2) by (cases "PLU_main Y", auto)
from False have "card (v_gs X) > L" by auto
note step = plucking_step[OF 1(2) this Y_def]
from False 1 have "X ⊆ 𝒢l ∧ L < card (v_gs X)" by auto
note IH = 1(1)[folded Y_def, OF this step(2) PLU] ‹Y ≠ {}›
let ?Diff = "λ X Y. ACC_cf X - ACC_cf Y"
have finNEG: "finite NEG"
using NEG_𝒢 infinite_super by blast
have "?Diff Z X ⊆ ?Diff Z Y ∪ ?Diff Y X" by auto
from card_mono[OF finite_subset[OF _ finite_ℱ] this] ACC_cf_ℱ
have "2 ^ p * card (?Diff Z X) ≤ 2 ^ p * card (?Diff Z Y ∪ ?Diff Y X)" by auto
also have "… ≤ 2 ^ p * (card (?Diff Z Y) + card (?Diff Y X))"
by (rule mult_left_mono, rule card_Un_le, simp)
also have "… = 2 ^ p * card (?Diff Z Y) + 2 ^ p * card (?Diff Y X)"
by (simp add: algebra_simps)
also have "… ≤ ((k - 1) ^ m) * q + (k - 1) ^ m" using IH step by auto
also have "… = ((k - 1) ^ m) * Suc q" by (simp add: ac_simps)
finally have c: "2 ^ p * card (ACC_cf Z - ACC_cf X) ≤ ((k - 1) ^ m) * Suc q" by simp
from False have "X ≠ {}" by auto
thus ?thesis unfolding n using IH step c by auto
qed
qed
text ‹Lemma 9›
lemma assumes X: "X ∈ 𝒫L𝒢l" and Y: "Y ∈ 𝒫L𝒢l"
shows PLU_union: "PLU (X ∪ Y) ∈ 𝒫L𝒢l" and
sqcup: "X ⊔ Y ∈ 𝒫L𝒢l" and
sqcup_sub: "POS ∩ ACC (X ∪ Y) ⊆ ACC (X ⊔ Y)" and
deviate_pos_cup: "∂⊔Pos X Y = {}" and
deviate_neg_cup: "card (∂⊔Neg X Y) < (k - 1)^m * L / 2^(p - 1)"
proof -
obtain Z n where res: "PLU_main (X ∪ Y) = (Z, n)" by force
hence PLU: "PLU (X ∪ Y) = Z" unfolding PLU_def by simp
from X Y have XY: "X ∪ Y ⊆ 𝒢l" unfolding 𝒫L𝒢l_def by auto
note main = PLU_main[OF this(1) res]
from main show "PLU (X ∪ Y) ∈ 𝒫L𝒢l" unfolding PLU by simp
thus "X ⊔ Y ∈ 𝒫L𝒢l" unfolding sqcup_def .
from main show "POS ∩ ACC (X ∪ Y) ⊆ ACC (X ⊔ Y)"
unfolding sqcup_def PLU by simp
thus "∂⊔Pos X Y = {}" unfolding deviate_pos_cup_def PLU sqcup_def by auto
have "card (v_gs (X ∪ Y)) ≤ card (v_gs X) + card (v_gs Y)"
unfolding v_gs_union by (rule card_Un_le)
also have "… ≤ L + L" using X Y unfolding 𝒫L𝒢l_def by simp
finally have "card (v_gs (X ∪ Y)) ≤ 2 * L" by simp
with PLU_main_n[OF XY(1) res] have "n * (p - 1) ≤ 2 * L" by simp
with p Lm m2 have n: "n < 2 * L" by (cases n, auto, cases "p - 1", auto)
let ?r = real
have *: "(k - 1) ^ m > 0" using k l2 by simp
have "2 ^ p * card (∂⊔Neg X Y) ≤ 2 ^ p * card (ACC_cf Z - ACC_cf (X ∪ Y))" unfolding deviate_neg_cup_def PLU sqcup_def
by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_ℱ]], insert ACC_cf_ℱ, force, auto)
also have "… ≤ (k - 1) ^ m * n" using main by simp
also have "… < (k - 1) ^ m * (2 * L)" unfolding mult_less_cancel1 using n * by simp
also have "… = 2 * ((k - 1) ^ m * L)" by simp
finally have "2 * (2^(p - 1) * card (∂⊔Neg X Y)) < 2 * ((k - 1) ^ m * L)" using p by (cases p, auto)
hence "2 ^ (p - 1) * card (∂⊔Neg X Y) < (k - 1)^m * L" by simp
hence "?r (2 ^ (p - 1) * card (∂⊔Neg X Y)) < ?r ((k - 1)^m * L)" by linarith
thus "card (∂⊔Neg X Y) < (k - 1)^m * L / 2^(p - 1)" by (simp add: field_simps)
qed
text ‹Lemma 10›
lemma assumes X: "X ∈ 𝒫L𝒢l" and Y: "Y ∈ 𝒫L𝒢l"
shows PLU_joinl: "PLU (X ⊙l Y) ∈ 𝒫L𝒢l" and
sqcap: "X ⊓ Y ∈ 𝒫L𝒢l" and
deviate_neg_cap: "card (∂⊓Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" and
deviate_pos_cap: "card (∂⊓Pos X Y) ≤ ((m - l - 1) choose (k - l - 1)) * L^2"
proof -
obtain Z n where res: "PLU_main (X ⊙l Y) = (Z, n)" by force
hence PLU: "PLU (X ⊙l Y) = Z" unfolding PLU_def by simp
from X Y have XY: "X ⊆ 𝒢l" "Y ⊆ 𝒢l" "X ⊆ 𝒢" "Y ⊆ 𝒢" unfolding 𝒫L𝒢l_def 𝒢l_def by auto
have sub: "X ⊙l Y ⊆ 𝒢l" unfolding odotl_def using XY
by (auto split: option.splits)
note main = PLU_main[OF sub res]
note finV = finite_v_gs_Gl[OF XY(1)] finite_v_gs_Gl[OF XY(2)]
have "X ⊙ Y ⊆ 𝒢" by (rule odot_𝒢, insert XY, auto simp: 𝒢l_def)
hence XYD: "X ⊙ Y ⊆ 𝒢" by auto
have finvXY: "finite (v_gs (X ⊙ Y))" by (rule finite_v_gs[OF XYD])
have "card (v_gs (X ⊙ Y)) ≤ card (v_gs X) * card (v_gs Y)"
using XY(1-2) by (intro card_v_gs_join, auto simp: 𝒢l_def)
also have "… ≤ L * L" using X Y unfolding 𝒫L𝒢l_def
by (intro mult_mono, auto)
also have "… = L^2" by algebra
finally have card_join: "card (v_gs (X ⊙ Y)) ≤ L^2" .
with card_mono[OF finvXY v_gs_mono[OF joinl_join]]
have card: "card (v_gs (X ⊙l Y)) ≤ L^2" by simp
with PLU_main_n[OF sub res] have "n * (p - 1) ≤ L^2" by simp
with p Lm m2 have n: "n < 2 * L^2" by (cases n, auto, cases "p - 1", auto)
have *: "(k - 1) ^ m > 0" using k l2 by simp
show "PLU (X ⊙l Y) ∈ 𝒫L𝒢l" unfolding PLU using main by auto
thus "X ⊓ Y ∈ 𝒫L𝒢l" unfolding sqcap_def .
let ?r = real
have "2^p * card (∂⊓Neg X Y) ≤ 2 ^ p * card (ACC_cf Z - ACC_cf (X ⊙l Y))"
unfolding deviate_neg_cap_def PLU sqcap_def
by (rule mult_left_mono, rule card_mono[OF finite_subset[OF _ finite_ℱ]], insert ACC_cf_ℱ, force,
insert ACC_cf_mono[OF joinl_join, of X Y], auto)
also have "… ≤ (k - 1) ^ m * n" using main by simp
also have "… < (k - 1) ^ m * (2 * L^2)" unfolding mult_less_cancel1 using n * by simp
finally have "2 * (2^(p - 1) * card (∂⊓Neg X Y)) < 2 * ((k - 1) ^ m * L^2)" using p by (cases p, auto)
hence "2 ^ (p - 1) * card (∂⊓Neg X Y) < (k - 1)^m * L^2" by simp
hence "?r (2 ^ (p - 1) * card (∂⊓Neg X Y)) < (k - 1)^m * L^2" by linarith
thus "card (∂⊓Neg X Y) < (k - 1)^m * L^2 / 2^(p - 1)" by (simp add: field_simps)
define Vs where "Vs = v_gs (X ⊙ Y) ∩ {V . V ⊆ [m] ∧ card V ≥ Suc l}"
define C where "C (V :: nat set) = (SOME C. C ⊆ V ∧ card C = Suc l)" for V
define K where "K C = { W. W ⊆ [m] - C ∧ card W = k - Suc l }" for C
define merge where "merge C V = (C ∪ V)^𝟮" for C V :: "nat set"
define GS where "GS = { merge (C V) W | V W. V ∈ Vs ∧ W ∈ K (C V)}"
{
fix V
assume V: "V ∈ Vs"
hence card: "card V ≥ Suc l" and Vm: "V ⊆ [m]" unfolding Vs_def by auto
from card obtain D where C: "D ⊆ V" and cardV: "card D = Suc l"
by (rule obtain_subset_with_card_n)
hence "∃ C. C ⊆ V ∧ card C = Suc l" by blast
from someI_ex[OF this, folded C_def] have *: "C V ⊆ V" "card (C V) = Suc l"
by blast+
with Vm have sub: "C V ⊆ [m]" by auto
from finite_subset[OF this] have finCV: "finite (C V)" unfolding numbers_def by simp
have "card (K (C V)) = (m - Suc l) choose (k - Suc l)" unfolding K_def
proof (subst n_subsets, (rule finite_subset[of _ "[m]"], auto)[1], rule arg_cong[of _ _ "λ x. x choose _"])
show "card ([m] - C V) = m - Suc l"
by (subst card_Diff_subset, insert sub * finCV, auto)
qed
note * finCV sub this
} note Vs_C = this
have finK: "finite (K V)" for V unfolding K_def by auto
{
fix G
assume G: "G ∈ POS ∩ ACC (X ⊙ Y)"
have "G ∈ ACC (X ⊙l Y) ∪ GS"
proof (rule ccontr)
assume "¬ ?thesis"
with G have G: "G ∈ POS" "G ∈ ACC (X ⊙ Y)" "G ∉ ACC (X ⊙l Y)"
and contra: "G ∉ GS" by auto
from G(1)[unfolded 𝒦_def] have "card (v G) = k ∧ (v G)^𝟮 = G" and G0: "G ∈ 𝒢"
by auto
hence vGk: "card (v G) = k" "(v G)^𝟮 = G" by auto
from G0 have vm: "v G ⊆ [m]" by (rule v_𝒢)
from G(2-3)[unfolded ACC_def accepts_def] obtain H
where H: "H ∈ X ⊙ Y" "H ∉ X ⊙l Y"
and HG: "H ⊆ G" by auto
from v_mono[OF HG] have vHG: "v H ⊆ v G" by auto
{
from H(1)[unfolded odot_def] obtain D E where D: "D ∈ X" and E: "E ∈ Y" and HDE: "H = D ∪ E"
by force
from D E X Y have Dl: "D ∈ 𝒢l" "E ∈ 𝒢l" unfolding 𝒫L𝒢l_def by auto
have Dp: "D ∈ 𝒢" using Dl by (auto simp: 𝒢l_def)
have Ep: "E ∈ 𝒢" using Dl by (auto simp: 𝒢l_def)
from Dl HDE have HD: "H ∈ 𝒢" unfolding 𝒢l_def by auto
have HG0: "H ∈ 𝒢" using Dp Ep unfolding HDE by auto
have HDL: "H ∉ 𝒢l"
proof
assume "H ∈ 𝒢l"
hence "H ∈ X ⊙l Y"
unfolding odotl_def HDE odot_def using D E by blast
thus False using H by auto
qed
from HDL HD have HGl: "H ∉ 𝒢l" unfolding 𝒢l_def by auto
have vm: "v H ⊆ [m]" using HG0 by (rule v_𝒢)
have lower: "l < card (v H)" using HGl HG0 unfolding 𝒢l_def by auto
have "v H ∈ Vs" unfolding Vs_def using lower vm H unfolding v_gs_def by auto
} note in_Vs = this
note C = Vs_C[OF this]
let ?C = "C (v H)"
from C vHG have CG: "?C ⊆ v G" by auto
hence id: "v G = ?C ∪ (v G - ?C)" by auto
from arg_cong[OF this, of card] vGk(1) C
have "card (v G - ?C) = k - Suc l"
by (metis CG card_Diff_subset)
hence "v G - ?C ∈ K ?C" unfolding K_def using vm by auto
hence "merge ?C (v G - ?C) ∈ GS" unfolding GS_def using in_Vs by auto
also have "merge ?C (v G - ?C) = v G^𝟮" unfolding merge_def
by (rule arg_cong[of _ _ sameprod], insert id, auto)
also have "… = G" by fact
finally have "G ∈ GS" .
with contra show False ..
qed
}
hence "∂⊓Pos X Y ⊆ (POS ∩ ACC (X ⊙l Y) - ACC (X ⊓ Y)) ∪ GS"
unfolding deviate_pos_cap_def by auto
also have "POS ∩ ACC (X ⊙l Y) - ACC (X ⊓ Y) = {}"
proof -
have "POS - ACC (X ⊓ Y) ⊆ UNIV - ACC (X ⊙l Y)"
unfolding sqcap_def using PLU main by auto
thus ?thesis by auto
qed
finally have sub: "∂⊓Pos X Y ⊆ GS" by auto
have finVs: "finite Vs" unfolding Vs_def numbers_def by simp
let ?Sig = "Sigma Vs (λ V. K (C V))"
have GS_def: "GS = (λ (V,W). merge (C V) W) ` ?Sig" unfolding GS_def
by auto
have finSig: "finite ?Sig" using finVs finK by simp
have finGS: "finite GS" unfolding GS_def
by (rule finite_imageI[OF finSig])
have "card (∂⊓Pos X Y) ≤ card GS" by (rule card_mono[OF finGS sub])
also have "… ≤ card ?Sig" unfolding GS_def
by (rule card_image_le[OF finSig])
also have "… = (∑a∈Vs. card (K (C a)))"
by (rule card_SigmaI[OF finVs], auto simp: finK)
also have "… = (∑a∈Vs. (m - Suc l) choose (k - Suc l))" using Vs_C
by (intro sum.cong, auto)
also have "… = ((m - Suc l) choose (k - Suc l)) * card Vs"
by simp
also have "… ≤ ((m - Suc l) choose (k - Suc l)) * L^2"
proof (rule mult_left_mono)
have "card Vs ≤ card (v_gs (X ⊙ Y))"
by (rule card_mono[OF finvXY], auto simp: Vs_def)
also have "… ≤ L^2" by fact
finally show "card Vs ≤ L^2" .
qed simp
finally show "card (∂⊓Pos X Y) ≤ ((m - l - 1) choose (k - l - 1)) * L^2"
by simp
qed
end
subsection ‹Formalism›
text ‹Fix a variable set of cardinality m over 2.›
locale forth_assumptions = third_assumptions +
fixes 𝒱 :: "'a set" and π :: "'a ⇒ vertex set"
assumes cV: "card 𝒱 = (m choose 2)"
and bij_betw_π: "bij_betw π 𝒱 ([m]^𝟮)"
begin
definition n where "n = (m choose 2)"
text ‹the formulas over the fixed variable set›
definition 𝒜 :: "'a mformula set" where
"𝒜 = { φ. vars φ ⊆ 𝒱}"
lemma 𝒜_simps[simp]:
"FALSE ∈ 𝒜"
"(Var x ∈ 𝒜) = (x ∈ 𝒱)"
"(Conj φ ψ ∈ 𝒜) = (φ ∈ 𝒜 ∧ ψ ∈ 𝒜)"
"(Disj φ ψ ∈ 𝒜) = (φ ∈ 𝒜 ∧ ψ ∈ 𝒜)"
by (auto simp: 𝒜_def)
lemma inj_on_π: "inj_on π 𝒱"
using bij_betw_π by (metis bij_betw_imp_inj_on)
lemma πm2[simp,intro]: "x ∈ 𝒱 ⟹ π x ∈ [m]^𝟮"
using bij_betw_π by (rule bij_betw_apply)
lemma card_v_π[simp,intro]: assumes "x ∈ 𝒱"
shows "card (v {π x}) = 2"
proof -
from πm2[OF assms] have mem: "π x ∈ [m]^𝟮" by auto
from this[unfolded binprod_def] obtain a b where π: "π x = {a,b}" and diff: "a ≠ b"
by auto
hence "v {π x} = {a,b}" unfolding v_def by auto
thus ?thesis using diff by simp
qed
lemma π_singleton[simp,intro]: assumes "x ∈ 𝒱"
shows "{π x} ∈ 𝒢"
"{{π x}} ∈ 𝒫L𝒢l"
using assms L3 l2
by (auto simp: 𝒢_def 𝒫L𝒢l_def v_gs_def 𝒢l_def)
lemma empty_𝒫L𝒢l[simp,intro]: "{} ∈ 𝒫L𝒢l"
by (auto simp: 𝒢_def 𝒫L𝒢l_def v_gs_def 𝒢l_def)
fun SET :: "'a mformula ⇒ graph set" where
"SET FALSE = {}"
| "SET (Var x) = {{π x}}"
| "SET (Disj φ ψ) = SET φ ∪ SET ψ"
| "SET (Conj φ ψ) = SET φ ⊙ SET ψ"
lemma ACC_cf_SET[simp]:
"ACC_cf (SET (Var x)) = {f ∈ ℱ. π x ∈ C f}"
"ACC_cf (SET FALSE) = {}"
"ACC_cf (SET (Disj φ ψ)) = ACC_cf (SET φ) ∪ ACC_cf (SET ψ)"
"ACC_cf (SET (Conj φ ψ)) = ACC_cf (SET φ) ∩ ACC_cf (SET ψ)"
using ACC_cf_odot
by (auto simp: ACC_cf_union ACC_cf_empty, auto simp: ACC_cf_def accepts_def)
lemma ACC_SET[simp]:
"ACC (SET (Var x)) = {G ∈ 𝒢. π x ∈ G}"
"ACC (SET FALSE) = {}"
"ACC (SET (Disj φ ψ)) = ACC (SET φ) ∪ ACC (SET ψ)"
"ACC (SET (Conj φ ψ)) = ACC (SET φ) ∩ ACC (SET ψ)"
by (auto simp: ACC_union ACC_odot, auto simp: ACC_def accepts_def)
lemma SET_𝒢: "φ ∈ tf_mformula ⟹ φ ∈ 𝒜 ⟹ SET φ ⊆ 𝒢"
proof (induct φ rule: tf_mformula.induct)
case (tf_Conj φ ψ)
hence "SET φ ⊆ 𝒢" "SET ψ ⊆ 𝒢" by auto
from odot_𝒢[OF this] show ?case by simp
qed auto
fun APR :: "'a mformula ⇒ graph set" where
"APR FALSE = {}"
| "APR (Var x) = {{π x}}"
| "APR (Disj φ ψ) = APR φ ⊔ APR ψ"
| "APR (Conj φ ψ) = APR φ ⊓ APR ψ"
lemma APR: "φ ∈ tf_mformula ⟹ φ ∈ 𝒜 ⟹ APR φ ∈ 𝒫L𝒢l"
by (induct φ rule: tf_mformula.induct, auto intro!: sqcup sqcap)
definition ACC_cf_mf :: "'a mformula ⇒ colorf set" where
"ACC_cf_mf φ = ACC_cf (SET φ)"
definition ACC_mf :: "'a mformula ⇒ graph set" where
"ACC_mf φ = ACC (SET φ)"
definition deviate_pos :: "'a mformula ⇒ graph set" ("∂Pos") where
"∂Pos φ = POS ∩ ACC_mf φ - ACC (APR φ)"
definition deviate_neg :: "'a mformula ⇒ colorf set" ("∂Neg") where
"∂Neg φ = ACC_cf (APR φ) - ACC_cf_mf φ"
text ‹Lemma 11.1›
lemma deviate_subset_Disj:
"∂Pos (Disj φ ψ) ⊆ ∂⊔Pos (APR φ) (APR ψ) ∪ ∂Pos φ ∪ ∂Pos ψ"
"∂Neg (Disj φ ψ) ⊆ ∂⊔Neg (APR φ) (APR ψ) ∪ ∂Neg φ ∪ ∂Neg ψ"
unfolding
deviate_pos_def deviate_pos_cup_def
deviate_neg_def deviate_neg_cup_def
ACC_cf_mf_def ACC_cf_SET ACC_cf_union
ACC_mf_def ACC_SET ACC_union
by auto
text ‹Lemma 11.2›
lemma deviate_subset_Conj:
"∂Pos (Conj φ ψ) ⊆ ∂⊓Pos (APR φ) (APR ψ) ∪ ∂Pos φ ∪ ∂Pos ψ"
"∂Neg (Conj φ ψ) ⊆ ∂⊓Neg (APR φ) (APR ψ) ∪ ∂Neg φ ∪ ∂Neg ψ"
unfolding
deviate_pos_def deviate_pos_cap_def
ACC_mf_def ACC_SET ACC_odot
deviate_neg_def deviate_neg_cap_def
ACC_cf_mf_def ACC_cf_SET ACC_cf_odot
by auto
lemmas deviate_subset = deviate_subset_Disj deviate_subset_Conj
lemma deviate_finite:
"finite (∂Pos φ)"
"finite (∂Neg φ)"
"finite (∂⊔Pos A B)"
"finite (∂⊔Neg A B)"
"finite (∂⊓Pos A B)"
"finite (∂⊓Neg A B)"
unfolding
deviate_pos_def deviate_pos_cup_def deviate_pos_cap_def
deviate_neg_def deviate_neg_cup_def deviate_neg_cap_def
by (intro finite_subset[OF _ finite_POS_NEG], auto)+
text ‹Lemma 12›
lemma no_deviation[simp]:
"∂Pos FALSE = {}"
"∂Neg FALSE = {}"
"∂Pos (Var x) = {}"
"∂Neg (Var x) = {}"
unfolding deviate_pos_def deviate_neg_def
by (auto simp add: ACC_cf_mf_def ACC_mf_def)
text ‹Lemma 12.1-2›
fun approx_pos where
"approx_pos (Conj phi psi) = ∂⊓Pos (APR phi) (APR psi)"
| "approx_pos _ = {}"
fun approx_neg where
"approx_neg (Conj phi psi) = ∂⊓Neg (APR phi) (APR psi)"
| "approx_neg (Disj phi psi) = ∂⊔Neg (APR phi) (APR psi)"
| "approx_neg _ = {}"
lemma finite_approx_pos: "finite (approx_pos φ)"
by (cases φ, auto intro: deviate_finite)
lemma finite_approx_neg: "finite (approx_neg φ)"
by (cases φ, auto intro: deviate_finite)
lemma card_deviate_Pos: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
shows "card (∂Pos φ) ≤ cs φ * L⇧2 * ( (m - l - 1) choose (k - l - 1))"
proof -
let ?Pos = "λ φ. ⋃ (approx_pos ` SUB φ)"
have "∂Pos φ ⊆ ?Pos φ"
using phi
proof (induct φ rule: tf_mformula.induct)
case (tf_Disj φ ψ)
from tf_Disj have *: "φ ∈ tf_mformula" "ψ ∈ tf_mformula" "φ ∈ 𝒜" "ψ ∈ 𝒜" by auto
note IH = tf_Disj(2)[OF *(3)] tf_Disj(4)[OF *(4)]
have "∂Pos (Disj φ ψ) ⊆ ∂⊔Pos (APR φ) (APR ψ) ∪ ∂Pos φ ∪ ∂Pos ψ"
by (rule deviate_subset)
also have "∂⊔Pos (APR φ) (APR ψ) = {}"
by (rule deviate_pos_cup; intro APR * )
also have "… ∪ ∂Pos φ ∪ ∂Pos ψ ⊆ ?Pos φ ∪ ?Pos ψ" using IH by auto
also have "… ⊆ ?Pos (Disj φ ψ) ∪ ?Pos (Disj φ ψ)"
by (intro Un_mono, auto)
finally show ?case by simp
next
case (tf_Conj φ ψ)
from tf_Conj have *: "φ ∈ 𝒜" "ψ ∈ 𝒜"
by (auto intro: tf_mformula.intros)
note IH = tf_Conj(2)[OF *(1)] tf_Conj(4)[OF *(2)]
have "∂Pos (Conj φ ψ) ⊆ ∂⊓Pos (APR φ) (APR ψ) ∪ ∂Pos φ ∪ ∂Pos ψ"
by (rule deviate_subset)
also have "… ⊆ ∂⊓Pos (APR φ) (APR ψ) ∪ ?Pos φ ∪ ?Pos ψ" using IH by auto
also have "… ⊆ ?Pos (Conj φ ψ) ∪ ?Pos (Conj φ ψ) ∪ ?Pos (Conj φ ψ)"
by (intro Un_mono, insert *, auto)
finally show ?case by simp
qed auto
from card_mono[OF finite_UN_I[OF finite_SUB finite_approx_pos] this]
have "card (∂Pos φ) ≤ card (⋃ (approx_pos ` SUB φ))" by simp
also have "… ≤ (∑i∈SUB φ. card (approx_pos i))"
by (rule card_UN_le[OF finite_SUB])
also have "… ≤ (∑i∈SUB φ. L⇧2 * ( (m - l - 1) choose (k - l - 1)))"
proof (rule sum_mono, goal_cases)
case (1 psi)
from phi 1 have psi: "psi ∈ tf_mformula" "psi ∈ 𝒜"
by (induct φ rule: tf_mformula.induct, auto intro: tf_mformula.intros)
show ?case
proof (cases psi)
case (Conj phi1 phi2)
from psi this have *: "phi1 ∈ tf_mformula" "phi1 ∈ 𝒜" "phi2 ∈ tf_mformula" "phi2 ∈ 𝒜"
by (cases rule: tf_mformula.cases, auto)+
from deviate_pos_cap[OF APR[OF *(1-2)] APR[OF *(3-4)]]
show ?thesis unfolding Conj by (simp add: ac_simps)
qed auto
qed
also have "… = cs φ * L⇧2 * ( (m - l - 1) choose (k - l - 1))" unfolding cs_def by simp
finally show "card (∂Pos φ) ≤ cs φ * L⇧2 * (m - l - 1 choose (k - l - 1))" by simp
qed
lemma card_deviate_Neg: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
shows "card (∂Neg φ) ≤ cs φ * L⇧2 * (k - 1)^m / 2^(p - 1)"
proof -
let ?r = real
let ?Neg = "λ φ. ⋃ (approx_neg ` SUB φ)"
have "∂Neg φ ⊆ ?Neg φ"
using phi
proof (induct φ rule: tf_mformula.induct)
case (tf_Disj φ ψ)
from tf_Disj have *: "φ ∈ tf_mformula" "ψ ∈ tf_mformula" "φ ∈ 𝒜" "ψ ∈ 𝒜" by auto
note IH = tf_Disj(2)[OF *(3)] tf_Disj(4)[OF *(4)]
have "∂Neg (Disj φ ψ) ⊆ ∂⊔Neg (APR φ) (APR ψ) ∪ ∂Neg φ ∪ ∂Neg ψ"
by (rule deviate_subset)
also have "… ⊆ ∂⊔Neg (APR φ) (APR ψ) ∪ ?Neg φ ∪ ?Neg ψ" using IH by auto
also have "… ⊆ ?Neg (Disj φ ψ) ∪ ?Neg (Disj φ ψ) ∪ ?Neg (Disj φ ψ)"
by (intro Un_mono, auto)
finally show ?case by simp
next
case (tf_Conj φ ψ)
from tf_Conj have *: "φ ∈ 𝒜" "ψ ∈ 𝒜"
by (auto intro: tf_mformula.intros)
note IH = tf_Conj(2)[OF *(1)] tf_Conj(4)[OF *(2)]
have "∂Neg (Conj φ ψ) ⊆ ∂⊓Neg (APR φ) (APR ψ) ∪ ∂Neg φ ∪ ∂Neg ψ"
by (rule deviate_subset)
also have "… ⊆ ∂⊓Neg (APR φ) (APR ψ) ∪ ?Neg φ ∪ ?Neg ψ" using IH by auto
also have "… ⊆ ?Neg (Conj φ ψ) ∪ ?Neg (Conj φ ψ) ∪ ?Neg (Conj φ ψ)"
by (intro Un_mono, auto)
finally show ?case by simp
qed auto
hence "∂Neg φ ⊆ ⋃ (approx_neg ` SUB φ)" by auto
from card_mono[OF finite_UN_I[OF finite_SUB finite_approx_neg] this]
have "card (∂Neg φ) ≤ card (⋃ (approx_neg ` SUB φ))" .
also have "… ≤ (∑i∈SUB φ. card (approx_neg i))"
by (rule card_UN_le[OF finite_SUB])
finally have "?r (card (∂Neg φ)) ≤ (∑i∈SUB φ. card (approx_neg i))" by linarith
also have "… = (∑i∈SUB φ. ?r (card (approx_neg i)))" by simp
also have "… ≤ (∑i∈SUB φ. L^2 * (k - 1)^m / 2^(p - 1))"
proof (rule sum_mono, goal_cases)
case (1 psi)
from phi 1 have psi: "psi ∈ tf_mformula" "psi ∈ 𝒜"
by (induct φ rule: tf_mformula.induct, auto intro: tf_mformula.intros)
show ?case
proof (cases psi)
case (Conj phi1 phi2)
from psi this have *: "phi1 ∈ tf_mformula" "phi1 ∈ 𝒜" "phi2 ∈ tf_mformula" "phi2 ∈ 𝒜"
by (cases rule: tf_mformula.cases, auto)+
from deviate_neg_cap[OF APR[OF *(1-2)] APR[OF *(3-4)]]
show ?thesis unfolding Conj by (simp add: ac_simps)
next
case (Disj phi1 phi2)
from psi this have *: "phi1 ∈ tf_mformula" "phi1 ∈ 𝒜" "phi2 ∈ tf_mformula" "phi2 ∈ 𝒜"
by (cases rule: tf_mformula.cases, auto)+
from deviate_neg_cup[OF APR[OF *(1-2)] APR[OF *(3-4)]]
have "card (approx_neg psi) ≤ ((L * 1) * (k - 1) ^ m) / 2 ^ (p - 1)"
unfolding Disj by (simp add: ac_simps)
also have "… ≤ ((L * L) * (k - 1) ^ m) / 2 ^ (p - 1)"
by (intro divide_right_mono, unfold of_nat_le_iff, intro mult_mono, insert L3, auto)
finally show ?thesis unfolding power2_eq_square by simp
qed auto
qed
also have "… = cs φ * L^2 * (k - 1)^m / 2^(p - 1)" unfolding cs_def by simp
finally show "card (∂Neg φ) ≤ cs φ * L⇧2 * (k - 1)^m / 2^(p - 1)" .
qed
text ‹Lemma 12.3›
lemma ACC_cf_non_empty_approx: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
and ne: "APR φ ≠ {}"
shows "card (ACC_cf (APR φ)) > (k - 1)^m / 3"
proof -
from ne obtain E :: graph where Ephi: "E ∈ APR φ"
by (auto simp: ACC_def accepts_def)
from APR[OF phi, unfolded 𝒫L𝒢l_def] Ephi
have EDl: "E ∈ 𝒢l" by auto
hence vEl: "card (v E) ≤ l" and ED: "E ∈ 𝒢"
unfolding 𝒢l_def 𝒢l_def by auto
have E: "E ∈ 𝒢" using ED[unfolded 𝒢l_def] by auto
have sub: "v E ⊆ [m]" by (rule v_𝒢[OF E])
have "l ≤ card [m]" using lm by auto
from exists_subset_between[OF vEl this sub finite_numbers]
obtain V where V: "v E ⊆ V" "V ⊆ [m]" "card V = l" by auto
from finite_subset[OF V(2)] have finV: "finite V" by auto
have finPart: "finite A" if "A ⊆ {P. partition_on [n] P}" for n A
by (rule finite_subset[OF that finitely_many_partition_on], simp)
have finmv: "finite ([m] - V)" using finite_numbers[of m] by auto
have finK: "finite [k - 1]" unfolding numbers_def by auto
define F where "F = {f ∈ [m] →⇩E [k - 1]. inj_on f V}"
have FF: "F ⊆ ℱ" unfolding ℱ_def F_def by auto
{
fix f
assume f: "f ∈ F"
{
from this[unfolded F_def]
have f: "f ∈ [m] →⇩E [k - 1]" and inj: "inj_on f V" by auto
from V l2 have 2: "card V ≥ 2" by auto
then obtain x where x: "x ∈ V" by (cases "V = {}", auto)
have "card V = card (V - {x}) + 1" using x finV
by (metis One_nat_def add.right_neutral add_Suc_right card_Suc_Diff1)
with 2 have "card (V - {x}) > 0" by auto
hence "V - {x} ≠ {}" by fastforce
then obtain y where y: "y ∈ V" and diff: "x ≠ y" by auto
from inj diff x y have neq: "f x ≠ f y" by (auto simp: inj_on_def)
from x y diff V have "{x, y} ∈ [m]^𝟮" unfolding sameprod_altdef by auto
with neq have "{x,y} ∈ C f" unfolding C_def by auto
hence "C f ≠ {}" by auto
}
with NEG_𝒢 FF f have CfG: "C f ∈ 𝒢" "C f ≠ {}" by (auto simp: NEG_def)
have "E ⊆ C f"
proof
fix e
assume eE: "e ∈ E"
with E[unfolded 𝒢_def] have em: "e ∈ [m]^𝟮" by auto
then obtain x y where e: "e = {x,y}" "x ≠ y" "{x,y} ⊆ [m]"
and card: "card e = 2"
unfolding binprod_def by auto
from v_mem_sub[OF card eE]
have "{x,y} ⊆ v E" using e by auto
hence "{x,y} ⊆ V" using V by auto
hence "f x ≠ f y" using e(2) f[unfolded F_def] by (auto simp: inj_on_def)
thus "e ∈ C f" unfolding C_def using em e by auto
qed
with Ephi CfG have "APR φ ⊩ C f"
unfolding accepts_def by auto
hence "f ∈ ACC_cf (APR φ)" using CfG f FF unfolding ACC_cf_def by auto
}
with FF have sub: "F ⊆ ACC_cf (APR φ)" by auto
from card_mono[OF finite_subset[OF _ finite_ACC] this]
have approx: "card F ≤ card (ACC_cf (APR φ))" by auto
from card_inj_on_subset_funcset[OF finite_numbers finK V(2), unfolded card_numbers V(3),
folded F_def]
have "real (card F) = (real (k - 1)) ^ (m - l) * prod (λ i. real (k - 1 - i)) {0..<l}"
by simp
also have "… > (real (k - 1)) ^ m / 3"
by (rule approximation1)
finally have cardF: "card F > (k - 1) ^ m / 3" by simp
with approx show ?thesis by simp
qed
text ‹Theorem 13›
lemma theorem_13: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
and sub: "POS ⊆ ACC_mf φ" "ACC_cf_mf φ = {}"
shows "cs φ > k powr (4 / 7 * sqrt k)"
proof -
let ?r = "real :: nat ⇒ real"
have "cs φ > ((m - l) / k)^l / (6 * L^2)"
proof (cases "POS ∩ ACC (APR φ) = {}")
case empty: True
have "∂Pos φ = POS ∩ ACC_mf φ - ACC (APR φ)" unfolding deviate_pos_def by auto
also have "… = POS - ACC (APR φ)" using sub by blast
also have "… = POS" using empty by auto
finally have id: "∂Pos φ = POS" by simp
have "m choose k = card POS" by (simp add: card_POS)
also have "… = card (∂Pos φ)" unfolding id by simp
also have "… ≤ cs φ * L⇧2 * (m - l - 1 choose (k - l - 1))" using card_deviate_Pos[OF phi] by auto
finally have "m choose k ≤ cs φ * L⇧2 * (m - l - 1 choose (k - l - 1))"
by simp
from approximation2[OF this]
show "((m - l) / k)^l / (6 * L^2) < cs φ" by simp
next
case False
have "POS ∩ ACC (APR φ) ≠ {}" by fact
hence nempty: "APR φ ≠ {}" by auto
have "card (∂Neg φ) = card (ACC_cf (APR φ) - ACC_cf_mf φ)" unfolding deviate_neg_def by auto
also have "… = card (ACC_cf (APR φ))" using sub by auto
also have "… > (k - 1)^m / 3" using ACC_cf_non_empty_approx[OF phi nempty] .
finally have "(k - 1)^m / 3 < card (∂Neg φ)" .
also have "… ≤ cs φ * L⇧2 * (k - 1) ^ m / 2 ^ (p - 1)"
using card_deviate_Neg[OF phi] sub by auto
finally have "(k - 1)^m / 3 < (cs φ * (L⇧2 * (k - 1) ^ m)) / 2 ^ (p - 1)" by simp
from approximation3[OF this] show ?thesis .
qed
hence part1: "cs φ > ((m - l) / k)^l / (6 * L^2)" .
from approximation4[OF this] show ?thesis using k2 by simp
qed
text ‹Definition 14›
definition eval_g :: "'a VAS ⇒ graph ⇒ bool" where
"eval_g θ G = (∀ v ∈ 𝒱. (π v ∈ G ⟶ θ v))"
definition eval_gs :: "'a VAS ⇒ graph set ⇒ bool" where
"eval_gs θ X = (∃ G ∈ X. eval_g θ G)"
lemmas eval_simps = eval_g_def eval_gs_def eval.simps
lemma eval_gs_union:
"eval_gs θ (X ∪ Y) = (eval_gs θ X ∨ eval_gs θ Y)"
by (auto simp: eval_gs_def)
lemma eval_gs_odot: assumes "X ⊆ 𝒢" "Y ⊆ 𝒢"
shows "eval_gs θ (X ⊙ Y) = (eval_gs θ X ∧ eval_gs θ Y)"
proof
assume "eval_gs θ (X ⊙ Y)"
from this[unfolded eval_gs_def] obtain DE where DE: "DE ∈ X ⊙ Y"
and eval: "eval_g θ DE" by auto
from DE[unfolded odot_def] obtain D E where id: "DE = D ∪ E" and DE: "D ∈ X" "E ∈ Y"
by auto
from eval have "eval_g θ D" "eval_g θ E" unfolding id eval_g_def
by auto
with DE show "eval_gs θ X ∧ eval_gs θ Y" unfolding eval_gs_def by auto
next
assume "eval_gs θ X ∧ eval_gs θ Y"
then obtain D E where DE: "D ∈ X" "E ∈ Y" and eval: "eval_g θ D" "eval_g θ E"
unfolding eval_gs_def by auto
from DE assms have D: "D ∈ 𝒢" "E ∈ 𝒢" by auto
let ?U = "D ∪ E"
from eval have eval: "eval_g θ ?U"
unfolding eval_g_def by auto
from DE have 1: "?U ∈ X ⊙ Y" unfolding odot_def by auto
with 1 eval show "eval_gs θ (X ⊙ Y)" unfolding eval_gs_def by auto
qed
text ‹Lemma 15›
lemma eval_set: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
shows "eval θ φ = eval_gs θ (SET φ)"
using phi
proof (induct φ rule: tf_mformula.induct)
case tf_False
then show ?case unfolding eval_simps by simp
next
case (tf_Var x)
then show ?case using inj_on_π unfolding eval_simps
by (auto simp add: inj_on_def)
next
case (tf_Disj φ1 φ2)
thus ?case by (auto simp: eval_gs_union)
next
case (tf_Conj φ1 φ2)
thus ?case by (simp, intro eval_gs_odot[symmetric]; intro SET_𝒢, auto)
qed
definition θ⇩g :: "graph ⇒ 'a VAS" where
"θ⇩g G x = (x ∈ 𝒱 ∧ π x ∈ G)"
text ‹From here on we deviate from Gordeev's paper as we do not use positive bases, but a more
direct approach.›
lemma eval_ACC: assumes phi: "φ ∈ tf_mformula" "φ ∈ 𝒜"
and G: "G ∈ 𝒢"
shows "eval (θ⇩g G) φ = (G ∈ ACC_mf φ)"
using phi unfolding ACC_mf_def
proof (induct φ rule: tf_mformula.induct)
case (tf_Var x)
thus ?case by (auto simp: ACC_def G accepts_def θ⇩g_def)
next
case (tf_Disj phi psi)
thus ?case by (auto simp: ACC_union)
next
case (tf_Conj phi psi)
thus ?case by (auto simp: ACC_odot)
qed simp
lemma CLIQUE_solution_imp_POS_sub_ACC: assumes solution: "∀ G ∈ 𝒢. G ∈ CLIQUE ⟷ eval (θ⇩g G) φ"
and tf: "φ ∈ tf_mformula"
and phi: "φ ∈ 𝒜"
shows "POS ⊆ ACC_mf φ"
proof
fix G
assume POS: "G ∈ POS"
with POS_𝒢 have G: "G ∈ 𝒢" by auto
with POS solution POS_CLIQUE
have "eval (θ⇩g G) φ" by auto
thus "G ∈ ACC_mf φ" unfolding eval_ACC[OF tf phi G] .
qed
lemma CLIQUE_solution_imp_ACC_cf_empty: assumes solution: "∀ G ∈ 𝒢. G ∈ CLIQUE ⟷ eval (θ⇩g G) φ"
and tf: "φ ∈ tf_mformula"
and phi: "φ ∈ 𝒜"
shows "ACC_cf_mf φ = {}"
proof (rule ccontr)
assume "¬ ?thesis"
from this[unfolded ACC_cf_mf_def ACC_cf_def]
obtain F where F: "F ∈ ℱ" "SET φ ⊩ C F" by auto
define G where "G = C F"
have NEG: "G ∈ NEG" unfolding NEG_def G_def using F by auto
hence "G ∉ CLIQUE" using CLIQUE_NEG by auto
have GG: "G ∈ 𝒢" unfolding G_def using F
using G_def NEG NEG_𝒢 by blast
have GAcc: "SET φ ⊩ G" using F[folded G_def] by auto
then obtain D :: graph where
D: "D ∈ SET φ" and sub: "D ⊆ G"
unfolding accepts_def by blast
from SET_𝒢[OF tf phi] D
have DG: "D ∈ 𝒢" by auto
have eval: "eval (θ⇩g D) φ" unfolding eval_set[OF tf phi] eval_gs_def
by (intro bexI[OF _ D], unfold eval_g_def, insert DG, auto simp: θ⇩g_def)
hence "D ∈ CLIQUE" using solution[rule_format, OF DG] by auto
hence "G ∈ CLIQUE" using GG sub unfolding CLIQUE_def by blast
with ‹G ∉ CLIQUE› show False by auto
qed
subsection ‹Conclusion›
text ‹Theorem 22›
text ‹We first consider monotone formulas without TRUE.›
theorem Clique_not_solvable_by_small_tf_mformula: assumes solution: "∀ G ∈ 𝒢. G ∈ CLIQUE ⟷ eval (θ⇩g G) φ"
and tf: "φ ∈ tf_mformula"
and phi: "φ ∈ 𝒜"
shows "cs φ > k powr (4 / 7 * sqrt k)"
proof -
from CLIQUE_solution_imp_POS_sub_ACC[OF solution tf phi] have POS: "POS ⊆ ACC_mf φ" .
from CLIQUE_solution_imp_ACC_cf_empty[OF solution tf phi] have CF: "ACC_cf_mf φ = {}" .
from theorem_13[OF tf phi POS CF]
show ?thesis by auto
qed
text ‹Next we consider general monotone formulas.›
theorem Clique_not_solvable_by_poly_mono: assumes solution: "∀ G ∈ 𝒢. G ∈ CLIQUE ⟷ eval (θ⇩g G) φ"
and phi: "φ ∈ 𝒜"
shows "cs φ > k powr (4 / 7 * sqrt k)"
proof -
note vars = phi[unfolded 𝒜_def]
have CL: "CLIQUE = Clique [k^4] k" "𝒢 = Graphs [k^4]"
unfolding CLIQUE_def 𝒦_altdef m_def Clique_def by auto
with empty_CLIQUE have "{} ∉ Clique [k^4] k" by simp
with solution[rule_format, of "{}"]
have "¬ eval (θ⇩g {}) φ" by (auto simp: Graphs_def)
from to_tf_mformula[OF this]
obtain ψ where *: "ψ ∈ tf_mformula"
"(∀θ. eval θ φ = eval θ ψ)" "vars ψ ⊆ vars φ" "cs ψ ≤ cs φ" by auto
with phi solution have psi: "ψ ∈ 𝒜"
and solution: "∀G∈𝒢. (G ∈ CLIQUE) = eval (θ⇩g G) ψ" unfolding 𝒜_def by auto
from Clique_not_solvable_by_small_tf_mformula[OF solution *(1) psi]
show ?thesis using *(4) by auto
qed
text ‹We next expand all abbreviations and definitions of the locale, but stay within the locale›
theorem Clique_not_solvable_by_small_monotone_circuit_in_locale: assumes phi_solves_clique:
"∀ G ∈ Graphs [k^4]. G ∈ Clique [k^4] k ⟷ eval (λ x. π x ∈ G) φ"
and vars: "vars φ ⊆ 𝒱"
shows "cs φ > k powr (4 / 7 * sqrt k)"
proof -
{
fix G
assume G: "G ∈ 𝒢"
have "eval (λ x. π x ∈ G) φ = eval (θ⇩g G) φ" using vars
by (intro eval_vars, auto simp: θ⇩g_def)
}
have CL: "CLIQUE = Clique [k^4] k" "𝒢 = Graphs [k^4]"
unfolding CLIQUE_def 𝒦_altdef m_def Clique_def by auto
{
fix G
assume G: "G ∈ 𝒢"
have "eval (λ x. π x ∈ G) φ = eval (θ⇩g G) φ" using vars
by (intro eval_vars, auto simp: θ⇩g_def)
}
with phi_solves_clique CL have solves: "∀ G ∈ 𝒢. G ∈ CLIQUE ⟷ eval (θ⇩g G) φ"
by auto
from vars have inA: "φ ∈ 𝒜" by (auto simp: 𝒜_def)
from Clique_not_solvable_by_poly_mono[OF solves inA]
show ?thesis by auto
qed
end
text ‹Let us now move the theorem outside the locale›
definition Large_Number where "Large_Number = Max {64, L0''^2, L0^2, L0'^2, M0, M0'}"
theorem Clique_not_solvable_by_small_monotone_circuit_squared:
fixes φ :: "'a mformula"
assumes k: "∃ l. k = l^2"
and LARGE: "k ≥ Large_Number"
and π: "bij_betw π V [k^4]^𝟮"
and solution: "∀G∈Graphs [k ^ 4]. (G ∈ Clique [k ^ 4] k) = eval (λ x. π x ∈ G) φ"
and vars: "vars φ ⊆ V"
shows "cs φ > k powr (4 / 7 * sqrt k)"
proof -
from k obtain l where kk: "k = l^2" by auto
note LARGE = LARGE[unfolded Large_Number_def]
have k8: "k ≥ 8^2" using LARGE by auto
from this[unfolded kk power2_nat_le_eq_le]
have l8: "l ≥ 8" .
define p where "p = nat (ceiling (l * log 2 (k^4)))"
have tedious: "l * log 2 (k ^ 4) ≥ 0" using l8 k8 by auto
have "int p = ceiling (l * log 2 (k ^ 4))" unfolding p_def
by (rule nat_0_le, insert tedious, auto)
from arg_cong[OF this, of real_of_int]
have rp: "real p = ceiling (l * log 2 (k ^ 4))" by simp
have one: "real l * log 2 (k ^ 4) ≤ p" unfolding rp by simp
have two: "p ≤ real l * log 2 (k ^ 4) + 1" unfolding rp by simp
have "real l < real l + 1 " by simp
also have "… ≤ real l + real l" using l8 by simp
also have "… = real l * 2" by simp
also have "… = real l * log 2 (2^2)"
by (subst log_pow_cancel, auto)
also have "… ≤ real l * log 2 (k ^ 4)"
proof (intro mult_left_mono, subst log_le_cancel_iff)
have "(4 :: real) ≤ 2^4" by simp
also have "… ≤ real k^4"
by (rule power_mono, insert k8, auto)
finally show "2⇧2 ≤ real (k ^ 4)" by simp
qed (insert k8, auto)
also have "… ≤ p" by fact
finally have lp: "l < p" by auto
interpret second_assumptions l p k
proof (unfold_locales)
show "2 < l" using l8 by auto
show "8 ≤ l" by fact
show "k = l^2" by fact
show "l < p" by fact
from LARGE have "L0''^2 ≤ k" by auto
from this[unfolded kk power2_nat_le_eq_le]
have L0''l: "L0'' ≤ l" .
have "p ≤ real l * log 2 (k ^ 4) + 1" by fact
also have "… < k" unfolding kk
by (intro L0'' L0''l)
finally show "p < k" by simp
qed
interpret third_assumptions l p k
proof
show "real l * log 2 (real m) ≤ p" using one unfolding m_def .
show "p ≤ real l * log 2 (real m) + 1" using two unfolding m_def .
from LARGE have "L0^2 ≤ k" by auto
from this[unfolded kk power2_nat_le_eq_le]
show "L0 ≤ l" .
from LARGE have "L0'^2 ≤ k" by auto
from this[unfolded kk power2_nat_le_eq_le]
show "L0' ≤ l" .
show "M0' ≤ m" using km LARGE by simp
show "M0 ≤ m" using km LARGE by simp
qed
interpret forth_assumptions l p k V π
by (standard, insert π m_def, auto simp: bij_betw_same_card[OF π])
from Clique_not_solvable_by_small_monotone_circuit_in_locale[OF solution vars]
show ?thesis .
qed
text ‹A variant where we get rid of the @{term "k = l^2"}-assumption by just taking squares everywhere.›
theorem Clique_not_solvable_by_small_monotone_circuit:
fixes φ :: "'a mformula"
assumes LARGE: "k ≥ Large_Number"
and π: "bij_betw π V [k^8]^𝟮"
and solution: "∀G∈Graphs [k ^ 8]. (G ∈ Clique [k ^ 8] (k^2)) = eval (λ x. π x ∈ G) φ"
and vars: "vars φ ⊆ V"
shows "cs φ > k powr (8 / 7 * k)"
proof -
from LARGE have LARGE: "Large_Number ≤ k⇧2"
by (simp add: power2_nat_le_imp_le)
have id: "k⇧2 ^ 4 = k^8" "sqrt (k^2) = k" by auto
from Clique_not_solvable_by_small_monotone_circuit_squared[of "k^2", unfolded id, OF _ LARGE π solution vars]
have "cs φ > (k^2) powr (4 / 7 * k)" by auto
also have "(k^2) powr (4 / 7 * k) = k powr (8 / 7 * k)"
unfolding of_nat_power using powr_powr[of "real k" 2] by simp
finally show ?thesis .
qed
definition large_number where "large_number = Large_Number^8"
text ‹Finally a variant, where the size is formulated depending on $n$, the number of vertices.›
theorem Clique_with_n_nodes_not_solvable_by_small_monotone_circuit:
fixes φ :: "'a mformula"
assumes large: "n ≥ large_number"
and kn: "∃ k. n = k^8"
and π: "bij_betw π V [n]^𝟮"
and s: "s = root 4 n"
and solution: "∀G∈Graphs [n]. (G ∈ Clique [n] s) = eval (λ x. π x ∈ G) φ"
and vars: "vars φ ⊆ V"
shows "cs φ > (root 7 n) powr (root 8 n)"
proof -
from kn obtain k where nk: "n = k^8" by auto
have kn: "k = root 8 n" unfolding nk of_nat_power
by (subst real_root_pos2, auto)
have "root 4 n = root 4 ((real (k^2))^4)" unfolding nk by simp
also have "… = k^2" by (simp add: real_root_pos_unique)
finally have r4: "root 4 n = k^2" by simp
have s: "s = k^2" using s unfolding r4 by simp
from large[unfolded nk large_number_def] have Large: "k ≥ Large_Number" by simp
have "0 < Large_Number" unfolding Large_Number_def by simp
with Large have k0: "k > 0" by auto
hence n0: "n > 0" using nk by simp
from Clique_not_solvable_by_small_monotone_circuit[OF Large π[unfolded nk] _ vars]
solution[unfolded s] nk
have "real k powr (8 / 7 * real k) < cs φ" by auto
also have "real k powr (8 / 7 * real k) = root 8 n powr (8 / 7 * root 8 n)"
unfolding kn by simp
also have "… = ((root 8 n) powr (8 / 7)) powr (root 8 n)"
unfolding powr_powr by simp
also have "(root 8 n) powr (8 / 7) = root 7 n" using n0
by (simp add: root_powr_inverse powr_powr)
finally show ?thesis .
qed
end