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 "… <