# Theory Clique_Large_Monotone_Circuits

```theory Clique_Large_Monotone_Circuits
imports
Preliminaries
Assumptions_and_Approximations
Monotone_Formula
begin

text ‹disable list-syntax›
no_syntax "_list" :: "args ⇒ 'a list" ("[(_)]")
no_syntax "__listcompr" :: "args ⇒ 'a list" ("[(_)]")

hide_const (open) Sigma_Algebra.measure

subsection ‹Plain Graphs›

definition binprod :: "'a set ⇒ 'a set ⇒ 'a set set" (infixl "⋅" 60) where
"X ⋅ Y = {{x,y} | x y. x ∈ X ∧ y ∈ Y ∧ x ≠ y}"

abbreviation sameprod :: "'a set ⇒ 'a set set" ("(_)^𝟮") where
"X^𝟮 ≡ X ⋅ X"

lemma sameprod_altdef: "X^𝟮 = {Y. Y ⊆ X ∧ card Y = 2}"
unfolding binprod_def by (auto simp: card_2_iff)

definition numbers :: "nat ⇒ nat set" ("[(_)]") where
"[n] ≡ {..<n}"

lemma card_sameprod: "finite X ⟹ card (X^𝟮) = card X choose 2"
unfolding sameprod_altdef
by (subst n_subsets, auto)

lemma sameprod_mono: "X ⊆ Y ⟹ X^𝟮 ⊆ Y^𝟮"
unfolding sameprod_altdef by auto

lemma sameprod_finite: "finite X ⟹ finite (X^𝟮)"
unfolding sameprod_altdef by simp

lemma numbers2_mono: "x ≤ y ⟹ [x]^𝟮 ⊆ [y]^𝟮"
by (rule sameprod_mono, auto simp: numbers_def)

lemma card_numbers[simp]: "card [n] = n"

lemma card_numbers2[simp]: "card ([n]^𝟮) = n choose 2"
by (subst card_sameprod, auto simp: numbers_def)

type_synonym vertex = nat
type_synonym graph = "vertex set set"

definition Graphs :: "vertex set ⇒ graph set" where
"Graphs V = { G. G ⊆ V^𝟮 }"

definition Clique :: "vertex set ⇒ nat ⇒ graph set" where
"Clique V k = { G. G ∈ Graphs V ∧ (∃ C ⊆ V. C^𝟮 ⊆ G ∧ card C = k) }"

context first_assumptions
begin

abbreviation 𝒢 where "𝒢 ≡ Graphs [m]"

lemmas 𝒢_def = Graphs_def[of "[m]"]

lemma empty_𝒢[simp]: "{} ∈ 𝒢" unfolding 𝒢_def by auto

definition v :: "graph ⇒ vertex set" where
"v G = { x . ∃ y. {x,y} ∈ G}"

lemma v_union: "v (G ∪ H) = v G ∪ v H"
unfolding v_def by auto

definition 𝒦 :: "graph set" where
"𝒦 = { K . K ∈ 𝒢 ∧ card (v K) = k ∧ K = (v K)^𝟮 }"

lemma v_𝒢: "G ∈ 𝒢 ⟹ v G ⊆ [m]"
unfolding v_def 𝒢_def sameprod_altdef by auto

lemma v_mono: "G ⊆ H ⟹ v G ⊆ v H" unfolding v_def by auto

lemma v_sameprod[simp]: assumes "card X ≥ 2"
shows "v (X^𝟮) = X"
proof -
from obtain_subset_with_card_n[OF assms] obtain Y where "Y ⊆ X"
and Y: "card Y = 2" by auto
then obtain x y where "x ∈ X" "y ∈ X" and "x ≠ y"
by (auto simp: card_2_iff)
thus ?thesis unfolding sameprod_altdef v_def
by (auto simp: card_2_iff doubleton_eq_iff) blast
qed

lemma v_mem_sub: assumes "card e = 2" "e ∈ G" shows "e ⊆ v G"
proof -
obtain x y where e: "e = {x,y}" and xy: "x ≠ y" using assms
by (auto simp: card_2_iff)
from assms(2) have x: "x ∈ v G" unfolding e
by (auto simp: v_def)
from e have e: "e = {y,x}" unfolding e by auto
from assms(2) have y: "y ∈ v G" unfolding e
by (auto simp: v_def)
show "e ⊆ v G" using x y unfolding e by auto
qed

lemma v_𝒢_2: assumes "G ∈ 𝒢" shows "G ⊆ (v G)^𝟮"
proof
fix e
assume eG: "e ∈ G"
with assms[unfolded 𝒢_def binprod_def] obtain x y where e: "e = {x,y}" and xy: "x ≠ y" by auto
from eG e xy have x: "x ∈ v G" by (auto simp: v_def)
from e have e: "e = {y,x}" unfolding e by auto
from eG e xy have y: "y ∈ v G" by (auto simp: v_def)
from x y xy show "e ∈ (v G)^𝟮" unfolding binprod_def e by auto
qed

lemma v_numbers2[simp]: "x ≥ 2 ⟹ v ([x]^𝟮) = [x]"
by (rule v_sameprod, auto)

lemma sameprod_𝒢: assumes "X ⊆ [m]" "card X ≥ 2"
shows "X^𝟮 ∈ 𝒢"
unfolding 𝒢_def using assms(2) sameprod_mono[OF assms(1)]
by auto

lemma finite_numbers[simp,intro]: "finite [n]"
unfolding numbers_def by auto

lemma finite_numbers2[simp,intro]: "finite ([n]^𝟮)"
unfolding sameprod_altdef using finite_subset[of _ "[m]"] by auto

lemma finite_members_𝒢: "G ∈ 𝒢 ⟹ finite G"
unfolding 𝒢_def using finite_subset[of G "[m]^𝟮"] by auto

lemma finite_𝒢[simp,intro]: "finite 𝒢"
unfolding 𝒢_def by simp

lemma finite_vG: assumes "G ∈ 𝒢"
shows "finite (v G)"
proof -
from finite_members_𝒢[OF assms]
show ?thesis
proof (induct rule: finite_induct)
case (insert xy F)
show ?case
proof (cases "∃ x y. xy = {x,y}")
case False
hence "v (insert xy F) = v F" unfolding v_def by auto
thus ?thesis using insert by auto
next
case True
then obtain x y where xy: "xy = {x,y}" by auto
hence "v (insert xy F) = insert x (insert y (v F))"
unfolding v_def by auto
thus ?thesis using insert by auto
qed
qed (auto simp: v_def)
qed

lemma v_empty[simp]: "v {} = {}" unfolding v_def by auto

lemma v_card2: assumes "G ∈ 𝒢" "G ≠ {}"
shows "2 ≤ card (v G)"
proof -
from assms[unfolded 𝒢_def] obtain edge where *: "edge ∈ G" "edge ∈ [m]^𝟮" by auto
then obtain x y where edge: "edge = {x,y}" "x ≠ y" unfolding binprod_def by auto
with * have sub: "{x,y} ⊆ v G" unfolding v_def
by (smt (verit, best) insert_commute insert_compr mem_Collect_eq singleton_iff subsetI)
from assms finite_vG have "finite (v G)" by auto
from sub ‹x ≠ y› this show "2 ≤ card (v G)"
by (metis card_2_iff card_mono)
qed

lemma 𝒦_altdef: "𝒦 = {V^𝟮 | V. V ⊆ [m] ∧ card V = k}"
(is "_ = ?R")
proof -
{
fix K
assume "K ∈ 𝒦"
hence K: "K ∈ 𝒢" and card: "card (v K) = k" and KvK: "K = (v K)^𝟮"
unfolding 𝒦_def by auto
from v_𝒢[OF K] card KvK have "K ∈ ?R" by auto
}
moreover
{
fix V
assume 1: "V ⊆ [m]" and "card V = k"
hence "V^𝟮 ∈ 𝒦" unfolding 𝒦_def using k2 sameprod_𝒢[OF 1]
by auto
}
ultimately show ?thesis by auto
qed

lemma 𝒦_𝒢: "𝒦 ⊆ 𝒢"
unfolding 𝒦_def by auto

definition CLIQUE :: "graph set" where
"CLIQUE = { G. G ∈ 𝒢 ∧ (∃ K ∈ 𝒦. K ⊆ G) }"

lemma empty_CLIQUE[simp]: "{} ∉ CLIQUE" unfolding CLIQUE_def 𝒦_def using k2 by (auto simp: v_def)

subsection ‹Test Graphs›

text ‹Positive test graphs are precisely the cliques of size @{term k}.›

abbreviation "POS ≡ 𝒦"

lemma POS_𝒢: "POS ⊆ 𝒢" by (rule 𝒦_𝒢)

text ‹Negative tests are coloring-functions of vertices that encode graphs
which have cliques of size at most @{term "k - 1"}.›

type_synonym colorf = "vertex ⇒ nat"

definition ℱ :: "colorf set" where
"ℱ = [m] →⇩E [k - 1]"

lemma finite_ℱ: "finite ℱ"
unfolding ℱ_def numbers_def
by (meson finite_PiE finite_lessThan)

definition C :: "colorf ⇒ graph" where
"C f = { {x, y} | x y . {x,y} ∈ [m]^𝟮 ∧ f x ≠ f y}"

definition NEG :: "graph set" where
"NEG = C ` ℱ"

paragraph ‹Lemma 1›

lemma CLIQUE_NEG: "CLIQUE ∩ NEG = {}"
proof -
{
fix G
assume GC: "G ∈ CLIQUE" and GN: "G ∈ NEG"
from GC[unfolded CLIQUE_def] obtain K where
K: "K ∈ 𝒦" and G: "G ∈ 𝒢" and KsubG: "K ⊆ G" by auto
from GN[unfolded NEG_def] obtain f where fF: "f ∈ ℱ" and
GCf: "G = C f" by auto
from K[unfolded 𝒦_def] have KG: "K ∈ 𝒢" and
KvK: "K = v K^𝟮" and card1: "card (v K) = k" by auto
from k2 card1 have ineq: "card (v K) > card [k - 1]" by auto
from v_𝒢[OF KG] have vKm: "v K ⊆ [m]" by auto
from fF[unfolded ℱ_def] vKm have f: "f ∈ v K → [k - 1]"
by auto
from card_inj[OF f] ineq
have "¬ inj_on f (v K)" by auto
then obtain x y where *: "x ∈ v K" "y ∈ v K" "x ≠ y" and ineq: "f x = f y"
unfolding inj_on_def by auto
have "{x,y} ∉ G" unfolding GCf C_def using ineq
by (auto simp: doubleton_eq_iff)
with KsubG KvK have "{x,y} ∉ v K^𝟮" by auto
with * have False unfolding binprod_def by auto
}
thus ?thesis by auto
qed

lemma NEG_𝒢: "NEG ⊆ 𝒢"
proof -
{
fix f
assume "f ∈ ℱ"
hence "C f ∈ 𝒢"
unfolding NEG_def C_def 𝒢_def
by (auto simp: sameprod_altdef)
}
thus "NEG ⊆ 𝒢" unfolding NEG_def by auto
qed

lemma finite_POS_NEG: "finite (POS ∪ NEG)"
using POS_𝒢 NEG_𝒢
by (intro finite_subset[OF _ finite_𝒢], auto)

lemma POS_sub_CLIQUE: "POS ⊆ CLIQUE"
unfolding CLIQUE_def using 𝒦_𝒢 by auto

lemma POS_CLIQUE: "POS ⊂ CLIQUE"
proof -
have "[k+1]^𝟮 ∈ CLIQUE"
unfolding CLIQUE_def
proof (standard, intro conjI bexI[of _ "[k]^𝟮"])
show "[k]^𝟮 ⊆ [k+1]^𝟮"
by (rule numbers2_mono, auto)
show "[k]^𝟮 ∈ 𝒦" unfolding 𝒦_altdef using km
by (auto intro!: exI[of _ "[k]"], auto simp: numbers_def)
show "[k+1]^𝟮 ∈ 𝒢" using km k2
by (intro sameprod_𝒢, auto simp: numbers_def)
qed
moreover have "[k+1]^𝟮 ∉ POS" unfolding 𝒦_def using v_numbers2[of "k + 1"] k2
by auto
ultimately show ?thesis using POS_sub_CLIQUE by blast
qed

lemma card_POS: "card POS = m choose k"
proof -
have "m choose k =
card {B. B ⊆ [m] ∧ card B = k}" (is "_ = card ?A")
by (subst n_subsets[of "[m]" k], auto simp: numbers_def)
also have "… = card (sameprod ` ?A)"
proof (rule card_image[symmetric])
{
fix A
assume "A ∈ ?A"
hence "v (sameprod A) = A" using k2
by (subst v_sameprod, auto)
}
thus "inj_on sameprod ?A" by (rule inj_on_inverseI)
qed
also have "sameprod ` {B. B ⊆ [m] ∧ card B = k} = POS"
unfolding 𝒦_altdef by auto
finally show ?thesis by simp
qed

subsection ‹Basic operations on sets of graphs›

definition odot :: "graph set ⇒ graph set ⇒ graph set" (infixl "⊙" 65) where
"X ⊙ Y = { D ∪ E | D E. D ∈ X ∧ E ∈ Y}"

lemma union_𝒢[intro]: "G ∈ 𝒢 ⟹ H ∈ 𝒢 ⟹ G ∪ H ∈ 𝒢"
unfolding 𝒢_def by auto

lemma odot_𝒢: "X ⊆ 𝒢 ⟹ Y ⊆ 𝒢 ⟹ X ⊙ Y ⊆ 𝒢"
unfolding odot_def by auto

subsection ‹Acceptability›

text ‹Definition 2›

definition accepts :: "graph set ⇒ graph ⇒ bool" (infixl "⊩" 55) where
"(X ⊩ G) = (∃ D ∈ X. D ⊆ G)"

lemma acceptsI[intro]: "D ⊆ G ⟹ D ∈ X ⟹ X ⊩ G"
unfolding accepts_def by auto

definition ACC :: "graph set ⇒ graph set" where
"ACC X = { G. G ∈ 𝒢 ∧ X ⊩ G}"

definition ACC_cf :: "graph set ⇒ colorf set" where
"ACC_cf X = { F. F ∈ ℱ ∧ X ⊩ C F}"

lemma ACC_cf_ℱ: "ACC_cf X ⊆ ℱ"
unfolding ACC_cf_def by auto

lemma finite_ACC[intro,simp]: "finite (ACC_cf X)"
by (rule finite_subset[OF ACC_cf_ℱ finite_ℱ])

lemma ACC_I[intro]: "G ∈ 𝒢 ⟹ X ⊩ G ⟹ G ∈ ACC X"
unfolding ACC_def by auto

lemma ACC_cf_I[intro]: "F ∈ ℱ ⟹ X ⊩ C F ⟹ F ∈ ACC_cf X"
unfolding ACC_cf_def by auto

lemma ACC_cf_mono: "X ⊆ Y ⟹ ACC_cf X ⊆ ACC_cf Y"
unfolding ACC_cf_def accepts_def by auto

text ‹Lemma 3›

lemma ACC_cf_empty: "ACC_cf {} = {}"
unfolding ACC_cf_def accepts_def by auto

lemma ACC_empty[simp]: "ACC {} = {}"
unfolding ACC_def accepts_def by auto

lemma ACC_cf_union: "ACC_cf (X ∪ Y) = ACC_cf X ∪ ACC_cf Y"
unfolding ACC_cf_def accepts_def by blast

lemma ACC_union: "ACC (X ∪ Y) = ACC X ∪ ACC Y"
unfolding ACC_def accepts_def by blast

lemma ACC_odot: "ACC (X ⊙ Y) = ACC X ∩ ACC Y"
proof -
{
fix G
assume "G ∈ ACC (X ⊙ Y)"
from this[unfolded ACC_def accepts_def]
obtain D E F :: graph where *: "D ∈ X" "E ∈ Y" "G ∈ 𝒢" "D ∪ E ⊆ G"
by (force simp: odot_def)
hence "G ∈ ACC X ∩ ACC Y"
unfolding ACC_def accepts_def by auto
}
moreover
{
fix G
assume "G ∈ ACC X ∩ ACC Y"
from this[unfolded ACC_def accepts_def]
obtain D E where *: "D ∈ X" "E ∈ Y" "G ∈ 𝒢" "D ⊆ G" "E ⊆ G"
by auto
let ?F = "D ∪ E"
from * have "?F ∈ X ⊙ Y" unfolding odot_def using * by blast
moreover have "?F ⊆ G" using * by auto
ultimately have "G ∈ ACC (X ⊙ Y)" using *
unfolding ACC_def accepts_def by blast
}
ultimately show ?thesis by blast
qed

lemma ACC_cf_odot: "ACC_cf (X ⊙ Y) = ACC_cf X ∩ ACC_cf Y"
proof -
{
fix G
assume "G ∈ ACC_cf (X ⊙ Y)"
from this[unfolded ACC_cf_def accepts_def]
obtain D E :: graph where *: "D ∈ X" "E ∈ Y" "G ∈ ℱ" "D ∪ E ⊆ C G"
by (force simp: odot_def)
hence "G ∈ ACC_cf X ∩ ACC_cf Y"
unfolding ACC_cf_def accepts_def by auto
}
moreover
{
fix F
assume "F ∈ ACC_cf X ∩ ACC_cf Y"
from this[unfolded ACC_cf_def accepts_def]
obtain D E where *: "D ∈ X" "E ∈ Y" "F ∈ ℱ" "D ⊆ C F" "E ⊆ C F"
by auto
let ?F = "D ∪ E"
from * have "?F ∈ X ⊙ Y" unfolding odot_def using * by blast
moreover have "?F ⊆ C F" using * by auto
ultimately have "F ∈ ACC_cf (X ⊙ Y)" using *
unfolding ACC_cf_def accepts_def by blast
}
ultimately show ?thesis by blast
qed

subsection ‹Approximations and deviations›

definition 𝒢l :: "graph set" where
"𝒢l = { G. G ∈ 𝒢 ∧ card (v G) ≤ l }"

definition v_gs :: "graph set ⇒ vertex set set" where
"v_gs X = v ` X"

lemma v_gs_empty[simp]: "v_gs {} = {}"
unfolding v_gs_def by auto

lemma v_gs_union: "v_gs (X ∪ Y) = v_gs X ∪ v_gs Y"
unfolding v_gs_def by auto

lemma v_gs_mono: "X ⊆ Y ⟹ v_gs X ⊆ v_gs Y"
using v_gs_def by auto

lemma finite_v_gs: assumes "X ⊆ 𝒢"
shows "finite (v_gs X)"
proof -
have "v_gs X ⊆ v ` 𝒢"
using assms unfolding v_gs_def by force
moreover have "finite 𝒢" using finite_𝒢 by auto
ultimately show ?thesis by (metis finite_surj)
qed

lemma finite_v_gs_Gl: assumes "X ⊆ 𝒢l"
shows "finite (v_gs X)"
by (rule finite_v_gs, insert assms, auto simp: 𝒢l_def)

definition 𝒫L𝒢l :: "graph set set" where
"𝒫L𝒢l = { X . X ⊆ 𝒢l ∧ card (v_gs X) ≤ L}"

definition odotl :: "graph set ⇒ graph set ⇒ graph set" (infixl "⊙l" 65) where
"X ⊙l Y = (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)
from p have p0: "p ≠ 0" by auto
have "(p - 1) ^ l * fact l < card ?vXp"  using L[unfolded L_def]
note sunflower = sunflower[OF this]
define S where "S = (SOME S. S ⊆ ?vXp ∧ sunflower S ∧ card S = p)"
define U where "U = {E ∈ X. v E ∈ S}"
define Vs where "Vs = ⋂ S"
define Gs where "Gs = Vs^𝟮"
let ?U = U
let ?New = "Gs :: graph"
have Y: "Y = X - U ∪ {?New}"
using Y[unfolded plucking_step_def Let_def, folded S_def, folded U_def,
folded Vs_def, folded Gs_def] .
have U: "U ⊆ 𝒢l" using X unfolding U_def by auto
hence "U ⊆ 𝒢" unfolding 𝒢l_def by auto
from sunflower
have "∃ S. S ⊆ ?vXp ∧ sunflower S ∧ card S = p" by auto
from someI_ex[OF this, folded S_def]
have S: "S ⊆ ?vXp" "sunflower S" "card S = p" by (auto simp: Vs_def)
have fin1: "finite ?vXp" using finite_v_gs_Gl[OF X] .
from X have finX: "finite X" unfolding 𝒢l_def
using finite_subset[of X, OF _  finite_𝒢] by auto
from fin1 S have finS: "finite S" by (metis finite_subset)
from finite_subset[OF _ finX] have finU: "finite U" unfolding U_def by auto
from S p have Snempty: "S ≠ {}" by auto
have UX: "U ⊆ X" unfolding U_def by auto
{
from Snempty obtain s where sS: "s ∈ S" by auto
with S have "s ∈ v_gs X" by auto
then obtain Sp where "Sp ∈ X" and sSp: "s = v Sp"
unfolding v_gs_def by auto
hence *: "Sp ∈ U" using ‹s ∈ S› unfolding U_def by auto
from * X UX have le: "card (v Sp) ≤ l" "finite (v Sp)" "Sp ∈ 𝒢"
unfolding 𝒢l_def 𝒢l_def using finite_vG[of Sp] by auto
hence m: "v Sp ⊆ [m]" by (intro v_𝒢)
have "Vs ⊆ v Sp" using sS sSp unfolding Vs_def by auto
with card_mono[OF ‹finite (v Sp)› this] finite_subset[OF this ‹finite (v Sp)›] le * m
have "card Vs ≤ l" "U ≠ {}" "finite Vs" "Vs ⊆ [m]" by auto
}
hence card_Vs: "card Vs ≤ l" and Unempty: "U ≠ {}"
and fin_Vs: "finite Vs" and Vsm: "Vs ⊆ [m]" by auto
have vGs: "v Gs ⊆ Vs" unfolding Gs_def by (rule v_sameprod_subset)
have GsG: "Gs ∈ 𝒢" unfolding Gs_def 𝒢_def
by (intro CollectI Inter_subset sameprod_mono Vsm)
have GsGl: "Gs ∈ 𝒢l" unfolding 𝒢l_def using GsG vGs card_Vs card_mono[OF _ vGs]
hence DsDl: "?New ∈ 𝒢l" using UX
unfolding 𝒢l_def 𝒢_def 𝒢l_def 𝒢_def by auto
with X U show "Y ⊆ 𝒢l" unfolding Y by auto
from X have XD: "X ⊆ 𝒢" unfolding 𝒢l_def by auto
have vplus_dsU: "v_gs U = S" using S(1)
unfolding v_gs_def U_def by force
have vplus_dsXU: "v_gs (X - U) = v_gs X - v_gs U"
unfolding v_gs_def U_def by auto
have "card (v_gs Y) = card (v_gs (X - U ∪ {?New}))"
unfolding Y by simp
also have "v_gs (X - U ∪ {?New}) = v_gs (X - U) ∪ v_gs ({?New})"
unfolding v_gs_union ..
also have "v_gs ({?New}) = {v (Gs)}" unfolding v_gs_def image_comp o_def by simp
also have "card (v_gs (X - U) ∪ …) ≤ card (v_gs (X - U)) + card …"
by (rule card_Un_le)
also have "… ≤ card (v_gs (X - U)) + 1" by auto
also have "v_gs (X - U) = v_gs X - v_gs U" by fact
also have "card … = card (v_gs X) - card (v_gs U)"
by (rule card_Diff_subset, force simp: vplus_dsU finS,
insert UX, auto simp: v_gs_def)
also have "card (v_gs U) = card S" unfolding vplus_dsU ..
finally show "card (v_gs Y) ≤ card (v_gs X) - p + 1"
using S by auto
show "Y ≠ {}" unfolding Y using Unempty by auto
{
fix G
assume "G ∈ ACC X" and GPOS: "G ∈ POS"
from this[unfolded ACC_def] POS_𝒢 have G: "G ∈ 𝒢" "X ⊩ G" by auto
from this[unfolded accepts_def] obtain D :: graph where
D: "D ∈ X" "D ⊆ G" by auto
have "G ∈ ACC Y"
proof (cases "D ∈ Y")
case True
with D G show ?thesis unfolding accepts_def ACC_def by auto
next
case False
with D have DU: "D ∈ U" unfolding Y by auto
from GPOS[unfolded POS_def 𝒦_def] obtain K where GK: "G = (v K)^𝟮" "card (v K) = k" by auto
from DU[unfolded U_def] have "v D ∈ S" by auto
hence "Vs ⊆ v D" unfolding Vs_def by auto
also have "… ⊆ v G"
by (intro v_mono D)
also have "… = v K" unfolding GK
by (rule v_sameprod, unfold GK, insert k2, auto)
finally 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
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)"
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 "… < ```