diff --git a/thys/Pluennecke_Ruzsa_Inequality/Pluennecke_Ruzsa_Inequality.thy b/thys/Pluennecke_Ruzsa_Inequality/Pluennecke_Ruzsa_Inequality.thy new file mode 100644 --- /dev/null +++ b/thys/Pluennecke_Ruzsa_Inequality/Pluennecke_Ruzsa_Inequality.thy @@ -0,0 +1,750 @@ +section\The Pl\"{u}nnecke-Ruzsa Inequality\ + +text\Authors: Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson, University of Cambridge.\ + +text\We formalise Pl\"{u}nnecke's inequality and the Pl\"{u}nnecke-Ruzsa inequality, +following the notes by Timothy Gowers: "Introduction to Additive +Combinatorics" (2022) for the University of Cambridge. To this end, we first introduce basic definitions +and prove elementary facts on sumsets and difference sets. Then, we show (two versions of) +the Ruzsa triangle inequality. We follow with a proof due to Petridis. \ + +theory Pluennecke_Ruzsa_Inequality + imports + "Jacobson_Basic_Algebra.Ring_Theory" + Complex_Main + +begin + +notation plus (infixl "+" 65) +notation minus (infixl "-" 65) +notation uminus ("- _" [81] 80) + +subsection \Key definitions (sumset, difference set) and basic lemmas \ + +text \Working in an arbitrary Abelian group, with additive syntax\ + +locale additive_abelian_group = abelian_group G "(\)" \ + for G and addition (infixl "\" 65) and zero ("\") + +begin + +abbreviation G_minus:: "'a \ 'a \ 'a" (infixl "\" 70) + where "x \ y \ x \ inverse y " + +lemma inverse_closed: "x \ G \ inverse x \ G" + by blast + + +subsubsection \Sumsets\ + +inductive_set sumset :: "'a set \ 'a set \ 'a set" for A B + where + sumsetI[intro]: "\a \ A; a \ G; b \ B; b \ G\ \ a \ b \ sumset A B" + +lemma sumset_eq: "sumset A B = {c. \a \ A \ G. \b \ B \ G. c = a \ b}" + by (auto simp: sumset.simps elim!: sumset.cases) + +lemma sumset: "sumset A B = (\a \ A \ G. \b \ B \ G. {a \ b})" + by (auto simp: sumset_eq) + +lemma sumset_subset_carrier: "sumset A B \ G" + by (auto simp: sumset_eq) + +lemma sumset_Int_carrier [simp]: "sumset A B \ G = sumset A B" + by (simp add: Int_absorb2 sumset_subset_carrier) + +lemma sumset_mono: "\A' \ A; B' \ B\ \ sumset A' B' \ sumset A B" + by (auto simp: sumset_eq) + +lemma sumset_insert1: "NO_MATCH {} A \ sumset (insert x A) B = sumset {x} B \ sumset A B" + by (auto simp: sumset_eq) + +lemma sumset_insert2: "NO_MATCH {} B \ sumset A (insert x B) = sumset A {x} \ sumset A B" + by (auto simp: sumset_eq) + +lemma sumset_subset_Un1: "sumset (A \ A') B = sumset A B \ sumset A' B" + by (auto simp: sumset_eq) + +lemma sumset_subset_Un2: "sumset A (B \ B') = sumset A B \ sumset A B'" + by (auto simp: sumset_eq) + +lemma sumset_subset_insert: "sumset A B \ sumset A (insert x B)" "sumset A B \ sumset (insert x A) B" + by (auto simp: sumset_eq) + +lemma sumset_subset_Un: "sumset A B \ sumset A (B\C)" "sumset A B \ sumset (A\C) B" + by (auto simp: sumset_eq) + +lemma sumset_empty [simp]: "sumset A {} = {}" "sumset {} A = {}" + by (auto simp: sumset_eq) + +lemma sumset_empty': + assumes "A \ G = {}" + shows "sumset B A = {}" "sumset A B = {}" + using assms by (auto simp: sumset_eq) + +lemma sumset_is_empty_iff [simp]: "sumset A B = {} \ A \ G = {} \ B \ G = {}" + by (auto simp: sumset_eq) + +lemma sumset_D [simp]: "sumset A {\} = A \ G" "sumset {\} A = A \ G" + by (auto simp: sumset_eq) + +lemma sumset_Int_carrier_eq [simp]: "sumset A (B \ G) = sumset A B" "sumset (A \ G) B = sumset A B" + by (auto simp: sumset_eq) + +lemma sumset_assoc: + shows "sumset (sumset A B) C = sumset A (sumset B C)" + by (fastforce simp add: sumset_eq associative Bex_def) + +lemma sumset_commute: + shows "sumset A B = sumset B A" + by (auto simp: sumset_eq; meson Int_iff commutative) + +lemma finite_sumset: + assumes "finite A" "finite B" shows "finite (sumset A B)" + using assms by (auto simp: sumset_eq) + +lemma finite_sumset': + assumes "finite (A \ G)" "finite (B \ G)" + shows "finite (sumset A B)" + using assms by (auto simp: sumset_eq) + +lemma sumsetdiff_sing: "sumset (A - B) {x} = sumset A {x} - sumset B {x}" + by (auto simp: sumset_eq) + +lemma card_sumset_singleton_eq: + assumes "finite A" shows "card (sumset A {a}) = (if a \ G then card (A \ G) else 0)" +proof (cases "a \ G") + case True + then have "sumset A {a} = (\x. x \ a) ` (A \ G)" + by (auto simp: sumset_eq) + moreover have "inj_on (\x. x \ a) (A \ G)" + by (auto simp: inj_on_def True) + ultimately show ?thesis + by (metis True card_image) +qed (auto simp: sumset_eq) + +lemma card_sumset_le: + assumes "finite A" shows "card (sumset A {a}) \ card A" + by (simp add: assms card_mono card_sumset_singleton_eq) + +lemma infinite_sumset_aux: + assumes "infinite (A \ G)" + shows "infinite (sumset A B) \ B \ G \ {}" +proof (cases "B \ G = {}") + case False + then obtain b where b: "b \ B" "b \ G" by blast + with assms commutative have "((\)b) ` (A \ G) \ sumset A B" + by (auto simp: sumset) + moreover have "inj_on ((\)b) (A \ G)" + by (meson IntD2 b inj_onI invertible invertible_left_cancel) + ultimately show ?thesis + by (metis False assms inj_on_finite) +qed (auto simp: sumset_eq) + +lemma infinite_sumset_iff: + shows "infinite (sumset A B) \ infinite (A \ G) \ B \ G \ {} \ A \ G \ {} \ infinite (B \ G)" + by (metis (no_types, lifting) finite_sumset' infinite_sumset_aux sumset_commute) + +lemma card_le_sumset: + assumes A: "finite A" "a \ A" "a \ G" + and B: "finite B" "B \ G" + shows "card B \ card (sumset A B)" +proof - + have "B \ (\) (inverse a) ` sumset A B" + using A B + apply (clarsimp simp: sumset image_iff) + by (metis Int_absorb2 Int_iff invertible invertible_left_inverse2) + with A B show ?thesis + by (meson finite_sumset surj_card_le) +qed + +lemma card_sumset_0_iff': "card (sumset A B) = 0 \ card (A \ G) = 0 \ card (B \ G) = 0" +proof (cases "infinite (A \ G) \ infinite (B \ G)") + case True + then show ?thesis + by (metis card_eq_0_iff infinite_sumset_iff sumset_empty') +qed (auto simp: sumset_eq) + +lemma card_sumset_0_iff: + assumes "A \ G" "B \ G" + shows "card (sumset A B) = 0 \ card A = 0 \ card B = 0" + by (metis assms le_iff_inf card_sumset_0_iff') + +lemma card_sumset_leq: + assumes "A \ G" + shows "card(sumset A A) \ Suc(card A) choose 2" + using assms +proof (induction "card A" arbitrary: A) + case 0 + then show ?case + by (metis card_sumset_0_iff zero_le) +next + case (Suc n A) + then obtain a A' where a: "a \ A" "A' = A - {a}" "a \ G" + by (metis Zero_neq_Suc card_eq_0_iff subset_empty subset_eq) + then have n: "card A' = n" + by (metis Suc(2) card_Diff_singleton diff_Suc_Suc minus_nat.diff_0 One_nat_def) + have "finite A" + by (metis Suc(2) Zero_neq_Suc card.infinite) + have "card (sumset A A) \ card (sumset A' A') + card A" + proof - + have A: "A = A' \ {a}" + using a by auto + then have "sumset A A = (sumset A' A') \ (sumset A {a})" + by (auto simp: sumset_eq commutative) + with a \finite A\ card_sumset_le show ?thesis + by (simp add: order_trans[OF card_Un_le]) + qed + also have "\ \ (card A) choose 2 + card A" + using Suc a by (metis add_le_mono1 insert_Diff_single insert_absorb insert_subset n) + also have "\ \ Suc (card A) choose 2" + by (simp add: numeral_2_eq_2) + finally show ?case . +qed + + +subsubsection \Iterated sumsets\ + +definition sumset_iterated :: "'a set \ nat \ 'a set" + where "sumset_iterated A r \ Finite_Set.fold (sumset \ (\_. A)) {\} {..}" + by (simp add: sumset_iterated_def) + +lemma sumset_iterated_Suc [simp]: "sumset_iterated A (Suc k) = sumset A (sumset_iterated A k)" + (is "?lhs = ?rhs") +proof - + interpret comp_fun_commute_on "{..k}" "sumset \ (\_. A)" + using sumset_assoc sumset_commute by (auto simp: comp_fun_commute_on_def) + have "?lhs = (sumset \ (\_. A)) k (Finite_Set.fold (sumset \ (\_. A)) {\} {.. = ?rhs" + by (simp add: sumset_iterated_def) + finally show ?thesis . +qed + +lemma sumset_iterated_2: + shows "sumset_iterated A 2 = sumset A A" + by (simp add: eval_nat_numeral) + +lemma sumset_iterated_r: "r > 0 \ sumset_iterated A r = sumset A (sumset_iterated A (r-1))" + using gr0_conv_Suc by force + +lemma sumset_iterated_subset_carrier: "sumset_iterated A k \ G" + by (cases k; simp add: sumset_subset_carrier) + +lemma finite_sumset_iterated: "finite A \ finite (sumset_iterated A r)" + by(induction r) (auto simp: finite_sumset) + +lemma sumset_iterated_empty: "r>0 \ sumset_iterated {} r = {}" + by (induction r) auto + +subsubsection \Difference sets\ + +inductive_set minusset :: "'a set \ 'a set" for A + where + minussetI[intro]: "\a \ A; a \ G\ \ inverse a \ minusset A" + +lemma minusset_eq: "minusset A = inverse ` (A \ G)" + by (auto simp: minusset.simps) + + +abbreviation "differenceset A B \ sumset A (minusset B)" + +lemma minusset_is_empty_iff [simp]: "minusset A = {} \ A \ G = {}" + by (auto simp: minusset_eq) + +lemma minusset_triv [simp]: "minusset {\} = {\}" + by (auto simp: minusset_eq) + +lemma minusset_subset_carrier: "minusset A \ G" + by (auto simp: minusset_eq) + +lemma minus_minusset [simp]: "minusset (minusset A) = A \ G" + apply (auto simp: minusset_eq) + by (metis inverse_equality invertible invertibleE minusset.minussetI minusset_eq) + +lemma card_minusset [simp]: "card (minusset A) = card (A \ G)" +proof (rule bij_betw_same_card) + show "bij_betw (inverse) (minusset A) (A \ G)" + unfolding minusset_eq by (force intro: bij_betwI) +qed + +lemma card_minusset': "A \ G \ card (minusset A) = card A" + by (simp add: Int_absorb2) + +lemma diff_minus_set: + "differenceset (minusset A) B = minusset (sumset A B)" (is "?lhs = ?rhs") +proof (rule Set.set_eqI) + fix u + have "u \ ?lhs \ + (\x \ A \ G. \y \ B \ G. u = inverse x \ y)" + by (auto simp: sumset minusset_eq) + also have "\ \ (\x \ A \ G. \y \ B \ G. u = inverse (y \ x))" + using inverse_composition_commute by auto + also have "\ \ u \ ?rhs" + by (auto simp: sumset minusset_eq commutative) + finally show "u \ ?lhs \ u \ ?rhs" . +qed + +lemma differenceset_commute [simp]: + shows "minusset (differenceset B A) = differenceset A B " + by (metis diff_minus_set minus_minusset sumset_Int_carrier_eq(1) sumset_commute) + +lemma minusset_distrib_sum: + shows "minusset (sumset A B) = sumset (minusset A) (minusset B)" + by (simp add: diff_minus_set) + +lemma minusset_iterated_minusset: "sumset_iterated (minusset A) k = minusset (sumset_iterated A k)" + by (induction k) (auto simp: diff_minus_set) + +lemma card_sumset_iterated_minusset: + "card (sumset_iterated (minusset A) k) = card (sumset_iterated A k)" + by (metis card_minusset' minusset_iterated_minusset sumset_iterated_subset_carrier) + +lemma finite_minusset: "finite A \ finite (minusset A)" + by (simp add: minusset_eq) + + +subsection\The Ruzsa triangle inequality\ + +lemma Ruzsa_triangle_ineq1: + assumes U: "finite U" "U \ G" + and V: "finite V" "V \ G" + and W: "finite W" "W \ G" + shows "(card U) * card(differenceset V W) \ card (differenceset U V) * card (differenceset U W)" +proof - + have fin: "finite (differenceset U V)" "finite (differenceset U W)" + using U V W finite_minusset finite_sumset by auto + have "\v w. v \ V \ w \ W \ x = v \ w" if "x \ differenceset V W" for x + using that by (auto simp: sumset_eq minusset_eq) + then obtain v w where vinV: "v x \ V" and winW: "w x \ W" and vw_eq: "v x \ (w x) = x" + if "x \ differenceset V W" for x by metis + have vinG: "v x \ G" and winG: "w x \ G" if "x \ differenceset V W" for x + using V W that vinV winW by auto + define \ where "\ \ \(u,x). (u \ (v x), u \ (w x))" + have "inj_on \ (U \ differenceset V W)" + proof (clarsimp simp add: \_def inj_on_def) + fix u1 :: 'a and x1 :: 'a and u2 :: 'a and x2 :: 'a + assume "u1 \ U" "u2 \ U" + and x1: "x1 \ differenceset V W" + and x2: "x2 \ differenceset V W" + and v: "u1 \ v x1 = u2 \ v x2" + and w: "u1 \ w x1 = u2 \ w x2" + then obtain "u1 \ G" "u2 \ G" "x1 \ G" "x2 \ G" + by (meson \U \ G\ subset_iff sumset_subset_carrier) + show "u1 = u2 \ x1 = x2" + proof + have "v x1 \ w x1 = (u1 \ w x1) \ (u1 \ v x1)" + by (smt (verit, del_insts) \u1 \ G\ associative commutative composition_closed inverse_closed + invertible invertible_right_inverse2 vinG winG x1) + also have "\ = (u2 \ w x2) \ (u2 \ v x2)" + using v w by presburger + also have "\ = v x2 \ w x2" + by (smt (verit, del_insts) \u2 \ G\ associative commutative composition_closed inverse_equality + invertible invertible_def invertible_right_inverse2 vinG winG x2) + finally have "v x1 \ w x1 = v x2 \ w x2" . + then show "x1=x2" + by (simp add: x1 x2 vw_eq) + then show "u1=u2" + using \u1 \ G\ \u2 \ G\ w winG x1 by force + qed + qed + moreover have "\ \ (U \ differenceset V W) \ (differenceset U V) \ (differenceset U W)" + using \U \ G\ \V \ G\ \W \ G\ + by (fastforce simp: \_def intro: vinV winW) + ultimately have "card (U \ differenceset V W) \ card (differenceset U V \ differenceset U W)" + using card_inj fin by blast + then show ?thesis + by (simp flip: card_cartesian_product) +qed + + + +definition Ruzsa_distance:: "'a set \ 'a set \ real" + where "Ruzsa_distance A B \ card(differenceset A B)/(sqrt(card A) * sqrt(card B))" + +lemma Ruzsa_triangle_ineq2: + assumes U: "finite U" "U \ G" "U \ {}" + and V: "finite V" "V \ G" + and W: "finite W" "W \ G" + shows "Ruzsa_distance V W \ (Ruzsa_distance V U) * (Ruzsa_distance U W)" +proof - + have "card U * card (differenceset V W) \ card (differenceset U V) * card (differenceset U W)" + using assms Ruzsa_triangle_ineq1 by metis + \\now divide both sides with the same quantity\ + then have "card U * card (differenceset V W) / (card U * sqrt (card V) * sqrt (card W)) + \ card (differenceset U V) * card (differenceset U W) / (card U * sqrt (card V) * sqrt (card W))" + using assms + by (metis divide_right_mono mult_eq_0_iff mult_left_mono of_nat_0_le_iff of_nat_mono real_sqrt_ge_0_iff) + then have *: "card(differenceset V W) / (sqrt(card V) * sqrt(card W)) \ + card (differenceset U V) * card (differenceset U W) + / (card U * sqrt(card V) * sqrt(card W))" + using assms by simp + have "card (differenceset U V) * card (differenceset U W)/(card U * sqrt(card V) * sqrt(card W)) + = card(differenceset V U) / (sqrt(card U) * sqrt(card V))* + card(differenceset U W) / (sqrt(card U) * sqrt(card W))" + using assms + by (simp add: divide_simps) (metis card_minusset differenceset_commute minus_minusset) + then have + "card(differenceset V W) / (sqrt(card V) * sqrt(card W)) \ + card(differenceset V U) / (sqrt(card U) * sqrt(card V)) * + card(differenceset U W) / (sqrt(card U) * sqrt(card W))" + using * assms by auto + then show ?thesis unfolding Ruzsa_distance_def + by (metis divide_divide_eq_left divide_divide_eq_left' times_divide_eq_right) +qed + + +subsection \Petridis's proof of the Pl\"{u}nnecke-Ruzsa inequality \ + +lemma Plu_2_2: + assumes K0: "card (sumset A0 B) \ K0 * real (card A0)" + and A0: "finite A0" "A0 \ G" "A0 \ {}" + and B: "finite B" "B \ G" "B \ {}" + obtains A K + where "A \ A0" "A \ {}" "0 < K" "K \ K0" + and "\C. C \ G \ finite C \ card (sumset A (sumset B C)) \ K * real (card(sumset A C))" +proof + define KS where "KS \ (\A. card (sumset A B) / real (card A)) ` (Pow A0 - {{}})" + define K where "K \ Min KS" + define A where "A \ @A. A \ Pow A0 - {{}} \ K = card (sumset A B) / real (card A)" + obtain KS: "finite KS" "KS \ {}" + using KS_def A0 by blast + then have "K \ KS" + using K_def Min_in by blast + then have "\A. A \ Pow A0 - {{}} \ K = card (sumset A B) / real (card A)" + using KS_def by blast + then obtain "A \ Pow A0 - {{}}" and Keq: "K = card (sumset A B) / real (card A)" + by (metis (mono_tags, lifting) A_def someI_ex) + then show A: "A \ A0" "A \ {}" + by auto + with A0 finite_subset have "A \ G" "finite A" + by blast+ + have gt0: "0 < real (card (sumset A B)) / real (card A)" if "A \ {}" and "A \ A0" for A + using that assms + by (smt (verit, best) order_trans card_0_eq card_sumset_0_iff divide_pos_pos of_nat_le_0_iff finite_subset) + then show "K > 0" + using A Keq by presburger + have K_cardA: "K * (card A) = card (sumset A B)" + unfolding Keq using Keq \0 < K\ by force + have K_le: "real (card (sumset A' B)) / card A' \ K" if "A' \ A" "A' \ {}" for A' + using KS K_def KS_def \A \ A0\ that by force + with A0 have "card (sumset A0 B) / real (card A0) \ KS" + by (auto simp: KS_def) + with A0 show "K \ K0" + by (metis KS K_def Min_le_iff card_gt_0_iff mult_imp_div_pos_le of_nat_0_less_iff K0) + show "card (sumset A (sumset B C)) \ K * real (card(sumset A C))" + if "finite C" "C \ G" for C + using that + proof (induction C) + case empty + then show ?case by simp + \ \This is actually trivial: it does not follow from @{term "card (sumset A B) = K * card A"} + as claimed in the notes.\ + next + case (insert x C) + then have "x \ G" "C \ G" "finite C" + by auto + define A' where "A' \ A \ {a. (a\x) \ sumset A C}" + with \finite A\ have "finite A'" "A' \ A" by auto + then have [simp]: "real (card A - card A') = real (card A) - real (card A')" + by (meson \finite A\ card_mono of_nat_diff) + have 0: "sumset A C \ sumset (A - A') {x} = {}" + by (clarsimp simp add: A'_def sumset_eq disjoint_iff) (metis IntI) + have 1: "sumset A (insert x C) = sumset A C \ sumset (A - A') {x}" + by (auto simp: A'_def sumset_eq) + have "card (sumset A (insert x C)) = card (sumset A C) + card (sumset (A - A') {x})" + by (simp add: 0 1 \finite A\ card_Un_disjoint finite_sumset local.insert) + also have "\ = card (sumset A C) + card ((A - A') \ G)" + using \finite A\ \x \ G\ by (simp add: card_sumset_singleton_eq) + also have "\ = card (sumset A C) + card (A - A')" + by (metis \A \ G\ Int_absorb2 Int_Diff Int_commute) + also have "\ = card (sumset A C) + (card A - card A')" + by (simp add: A'_def \finite A\ card_Diff_subset) + finally have *: "card (sumset A (insert x C)) = card (sumset A C) + (card A - card A')" . + have "sumset A' (sumset B {x}) \ sumset A (sumset B C)" + by (clarsimp simp add: A'_def sumset_eq Bex_def) (metis associative commutative composition_closed) + then have "sumset A (sumset B (insert x C)) + \ sumset A (sumset B C) \ (sumset A (sumset B {x}) - sumset A' (sumset B {x}))" + by (auto simp: sumset_insert2 sumset_subset_Un2) + then have "card (sumset A (sumset B (insert x C))) \ card (sumset A (sumset B C)) + + card ((sumset A (sumset B {x}) - sumset A' (sumset B {x})))" + by (smt (verit, best) B(1) \finite A\ \finite C\ order_trans card_Un_le card_mono finite.emptyI + finite.insertI finite_Diff finite_Un finite_sumset) + also have "\ = card (sumset A (sumset B C)) + (card (sumset A (sumset B {x})) - card (sumset A' (sumset B {x})))" + by (simp add: \A' \ A\ \finite A'\ \finite B\ card_Diff_subset finite_sumset sumset_mono) + also have "\ \ card (sumset A (sumset B C)) + (card (sumset A B) - card (sumset A' B))" + using \finite A\ \finite A'\ \finite B\ by (simp add: card_sumset_singleton_eq finite_sumset flip: sumset_assoc) + also have "\ \ K * card (sumset A C) + (K * card A - K * card A')" + proof (cases "A' = {}") + case True + with local.insert \C \ G\ K_cardA show ?thesis by auto + next + case False + then have "K * card A' \ real (card (sumset A' B))" + using K_le[OF \A' \ A\] by (simp add: divide_simps split: if_split_asm) + then have "real (card (sumset A B) - card (sumset A' B)) \ K * real (card A) - K * real (card A')" + by (simp add: B(1) K_cardA \A' \ A\ \finite A\ card_mono finite_sumset of_nat_diff sumset_mono) + with local.insert show ?thesis by simp + qed + also have "\ \ K * real (card (sumset A (insert x C)))" + using * \A' \ A\ by (simp add: algebra_simps) + finally show ?case + using of_nat_mono by blast + qed +qed + +lemma Cor_Plu_2_3: + assumes K: "card (sumset A B) \ K * real (card A)" + and A: "finite A" "A \ G" "A \ {}" + and B: "finite B" "B \ G" + obtains A' where "A' \ A" "A' \ {}" + "\r. card (sumset A' (sumset_iterated B r)) \ K^r * real (card A')" +proof (cases "B = {}") + case True + have "K \ 0" + using assms by (simp add: True zero_le_mult_iff) + moreover have *: "sumset_iterated B r = (if r=0 then {\} else {})" for r + by (metis True sumset_iterated_0 sumset_iterated_empty zero_less_iff_neq_zero) + ultimately have "real (card (sumset A (sumset_iterated B r))) + \ K ^ r * real (card A)" for r + by (simp add: "*" Int_commute Int_absorb2 \A \ G\) + with \A \ {}\ that show ?thesis by blast +next + case False + obtain A' K' + where A': "A' \ A" "A' \ {}" "0 < K'" "K' \ K" + and A'_card: "\C. C \ G \ finite C \ card (sumset A' (sumset B C)) \ K' * real (card(sumset A' C))" + by (metis A B Plu_2_2 K False) + with A have "A' \ G" by blast + have *: "card (sumset A' (sumset_iterated B (Suc r))) \ K' * card (sumset A' (sumset_iterated B r))" + (is "?lhs \ ?rhs") + for r + proof - + have "?lhs = card (sumset A' (sumset B (sumset_iterated B r)))" + using that by (simp add: sumset_iterated_r) + also have "\ \ ?rhs" + using A'_card B finite_sumset_iterated sumset_iterated_subset_carrier by meson + finally show ?thesis . + qed + have **: "card (sumset A' (sumset_iterated B r)) \ K'^r * real (card A')" for r + proof (induction r) + case 0 + with \A' \ G\ show ?case + by (simp add: Int_absorb2) + next + case (Suc r) + then show ?case + by (smt (verit) "*" \0 < K'\ mult.commute mult.left_commute mult_le_cancel_left_pos power_Suc) + qed + show thesis + proof + show "real (card (sumset A' (sumset_iterated B r))) \ K ^ r * real (card A')" for r + by (meson "**" A' order_trans less_eq_real_def mult_right_mono of_nat_0_le_iff power_mono) + qed (use A' in auto) +qed + + +text\The following Corollary of the above is an important special case, +also referred to as the original version of Pl\"{u}nnecke's inequality first shown by Pl\"{u}nnecke. \ + +lemma Cor_Plu_2_3_Pluennecke_ineq: + assumes K: "card (sumset A B) \ K * real (card A)" + and A: "finite A" "A \ G" "A \ {}" + and B: "finite B" "B \ G" + shows "real (card (sumset_iterated B r)) \ K ^ r * real (card A)" +proof- + obtain A' where *:"A' \ A" "A' \ {}" + "card (sumset A' (sumset_iterated B r)) \ K^r * real (card A')" + using assms Cor_Plu_2_3 by metis + with assms have **: "card (sumset_iterated B r) \ card (sumset A' (sumset_iterated B r))" + by (meson card_le_sumset finite_subset finite_sumset_iterated subset_empty subset_iff sumset_iterated_subset_carrier) + with * show ?thesis + by (smt (verit, best) A(1) K card_mono mult_left_mono of_nat_0_le_iff of_nat_le_iff zero_le_mult_iff zero_le_power) +qed + +text \Special case where @{term "B=A"}\ +lemma Cor_Plu_2_3_1: + assumes K: "card (sumset A A) \ K * real (card A)" + and A: "finite A" "A \ G" "A \ {}" + shows "card (sumset_iterated A r) \ K^r * real (card A)" +proof - + have "K > 0" + by (meson A K Plu_2_2 less_le_trans) + obtain A' where A': "A' \ A" "A' \ {}" + and A'_card: "\r. card (sumset A' (sumset_iterated A r)) \ K^r * real (card A')" + by (meson A Cor_Plu_2_3 K) + with A obtain a where "a \ A'" "a \ G" "finite A'" + by (metis ex_in_conv finite_subset subset_iff) + then have "card (sumset_iterated A r) \ card (sumset A' (sumset_iterated A r))" + using A card_le_sumset finite_sumset_iterated sumset_iterated_subset_carrier by meson + also have "\ \ K^r * real (card A')" + using A'_card by meson + also have "\ \ K^r * real (card A)" + by (simp add: \A' \ A\ \finite A\ \0 < K\ card_mono) + finally show ?thesis + by linarith +qed + + +text \Special case where @{term "B=-A"}\ +lemma Cor_Plu_2_3_2: + assumes K: "card (differenceset A A) \ K * real (card A)" + and A: "finite A" "A \ G" "A \ {}" + shows "card (sumset_iterated A r) \ K^r * real (card A)" +proof - + have "card A > 0" + by (simp add: A card_gt_0_iff) + with K have "K \ 0" + by (smt (verit, del_insts) of_nat_0_less_iff of_nat_less_0_iff zero_le_mult_iff) + obtain A' where A': "A' \ A" "A' \ {}" + and A'_card: "\r. card (sumset A' (sumset_iterated (minusset A) r)) \ K^r * real (card A')" + by (metis A Cor_Plu_2_3 assms(1) card_eq_0_iff card_minusset' minusset_subset_carrier) + with A obtain a where "a \ A'" "a \ G" "finite A'" + by (metis ex_in_conv finite_subset subset_iff) + then have "card (sumset_iterated A r) \ card (sumset A' (sumset_iterated (minusset A) r))" + by (metis A(1) card_le_sumset card_sumset_iterated_minusset finite_minusset finite_sumset_iterated sumset_iterated_subset_carrier) + also have "\ \ K^r * real (card A')" + using A'_card by meson + also have "\ \ K^r * real (card A)" + by (simp add: \A' \ A\ \finite A\ \0 \ K\ card_mono mult_left_mono) + finally show ?thesis + by linarith +qed + +text \The following result is known as the Pl\"{u}nnecke-Ruzsa inequality (Theorem 2.5 +in Gowers's notes). The proof will make use of the Ruzsa triangle inequality.\ + +theorem Pluennecke_Ruzsa_ineq: + assumes K: "card (sumset A B) \ K * real (card A)" + and A: "finite A" "A \ G" "A \ {}" + and B: "finite B" "B \ G" + and "0 < r" "0 < s" + shows "card (differenceset (sumset_iterated B r) (sumset_iterated B s)) \ K^(r+s) * real(card A)" +proof - + have "card A > 0" + by (simp add: A card_gt_0_iff) + with K have "K \ 0" + by (smt (verit, del_insts) of_nat_0_less_iff of_nat_less_0_iff zero_le_mult_iff) + obtain A' where A': "A' \ A" "A' \ {}" + and A'_le: "\r. card (sumset A' (sumset_iterated B r)) \ K^r * real (card A')" + using Cor_Plu_2_3 assms by metis + define C where "C \ minusset A'" + have "minusset C = A'" and "C \{}" and cardA: "card A' \ card A" and cardC: "card C = card A'" + using A' A card_mono by (auto simp: C_def card_minusset' Int_absorb2) + then have cardCA: "card C \ card A" by linarith + have "\r. card (differenceset C (sumset_iterated B r)) \ K^r * real (card A')" + using A'_le C_def card_minusset' diff_minus_set sumset_subset_carrier by presburger + then have r: "card (differenceset C (sumset_iterated B r)) \ K^r * real (card C)" + and s: "card (differenceset C (sumset_iterated B s)) \ K^s * real (card C)" + using cardC by presburger+ + have "card C > 0" + by (metis A' \finite A\ cardC card_gt_0_iff finite_subset) + moreover have "C \ G" + by (simp add: C_def minusset_subset_carrier) + ultimately have "card C * card (differenceset (sumset_iterated B r) (sumset_iterated B s)) + \ card (differenceset C (sumset_iterated B r)) * + card (differenceset C (sumset_iterated B s))" + by (meson Ruzsa_triangle_ineq1 B card_gt_0_iff finite_sumset_iterated sumset_iterated_subset_carrier) + also have "\ \ K^(r+s) * card C * card C" + using mult_mono [OF r s] \0 \ K\ by (simp add: power_add field_simps) + finally have "card (differenceset (sumset_iterated B r) (sumset_iterated B s)) \ K^(r+s) * card C" + using \card C > 0\ by (simp add: field_simps) + then show ?thesis + by (smt (verit, ccfv_SIG) \0 \ K\ cardA cardC mult_left_mono of_nat_mono zero_le_power) +qed + +text \The following is an alternative version of the Pl\"{u}nnecke-Ruzsa inequality (Theorem 2.1 +in Gowers's notes).\ + +theorem Pluennecke_Ruzsa_ineq_alt: + assumes "finite A" "A \ G" + and "card (sumset A A) \ K * real (card A)" "r > 0" "s > 0" + shows "card (differenceset (sumset_iterated A r) (sumset_iterated A s)) \ K^(r+s) * real(card A)" +proof (cases "A = {}") + case True + then have "sumset_iterated A r = {}" if "r>0" for r + using sumset_iterated_empty that by force + with assms show ?thesis + by (auto simp: True) +next + case False + with assms Pluennecke_Ruzsa_ineq show ?thesis by presburger +qed + +theorem Pluennecke_Ruzsa_ineq_alt_2: + assumes "finite A" "A \ G" + and "card (differenceset A A) \ K * real (card A)" "r > 0" "s > 0" + shows "card (differenceset (sumset_iterated A r) (sumset_iterated A s)) \ K^(r+s) * real(card A)" +proof (cases "A = {}") + case True + then have "sumset_iterated A r = {}" if "r>0" for r + using sumset_iterated_empty that by force + with assms show ?thesis + by (auto simp: True) +next + case False + with assms Pluennecke_Ruzsa_ineq show ?thesis + by (smt (verit, ccfv_threshold) card_minusset' differenceset_commute finite_minusset + minusset_distrib_sum minusset_iterated_minusset minusset_subset_carrier) +qed + +end + + +subsection \Supplementary material on sumsets for sets of integers: basic inequalities\ + +lemma moninv_int: "monoid.invertible UNIV (+) 0 u" for u::int + using monoid.invertibleI [where v = "-u"] by (simp add: Group_Theory.monoid_def) + +interpretation int: additive_abelian_group UNIV "(+)" "0::int" + by unfold_locales (use moninv_int in auto) + +lemma card_sumset_geq1: + assumes A: "A \ {}" "finite A" and B: "B \ {}" "finite B" + shows "card(int.sumset A B) \ (card A) + (card B) - 1" + using A +proof (induction "card A" arbitrary: A) + case (Suc n) + define a where "a = Max A" + define A' where "A' \ A - {a}" + then obtain a: "a \ A" "A' = A - {a}" "finite A'" "a \ A'" and A: "A = insert a A'" + using Max_in Suc a_def by blast + with Suc have n: "card A' = n" + by (metis card_Diff_singleton diff_Suc_Suc minus_nat.diff_0 One_nat_def) + show ?case + proof (cases "A' = {}") + case True + then show ?thesis + by (simp add: A B(2) int.card_sumset_singleton_eq int.sumset_commute) + next + case False + have "a + Max B \ int.sumset A' B" + using \finite A\ \finite B\ + by (smt (verit, best) DiffE Max_ge a a_def int.sumset.cases singleton_iff) + then have *: "\ int.sumset A' B \ (+) a ` B \ int.sumset A' B" + using B Max_in by blast + have "card A + card B - 1 \ Suc (card (int.sumset A' B))" + using Suc False A a using le_diff_conv by force + also have "\ \ card (int.sumset A' B \ (+) a ` B)" + using a B + by (metis "*" card_seteq finite_Un finite_imageI int.finite_sumset not_less_eq_eq sup_ge1) + also have "\ \ card (int.sumset A B)" + proof (rule card_mono) + show "finite (int.sumset A B)" + using B Suc.prems int.finite_sumset by blast + show "int.sumset A' B \ (+) a ` B \ int.sumset A B" + using A by (force simp: int.sumset) + qed + finally show ?thesis . + qed +qed auto + +lemma card_sumset_geq2: + shows "card(int.sumset A A) \ 2 * (card A) - 1" + using card_sumset_geq1 [of A] + by (metis mult.commute Nat.add_0_right card_eq_0_iff diff_0_eq_0 le0 mult_2_right) + +end diff --git a/thys/Pluennecke_Ruzsa_Inequality/ROOT b/thys/Pluennecke_Ruzsa_Inequality/ROOT new file mode 100644 --- /dev/null +++ b/thys/Pluennecke_Ruzsa_Inequality/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session Pluennecke_Ruzsa_Inequality (AFP) = "HOL-Library" + + options [timeout = 600] + sessions + "Jacobson_Basic_Algebra" + theories + Pluennecke_Ruzsa_Inequality + document_files + "root.tex" + "root.bib" + diff --git a/thys/Pluennecke_Ruzsa_Inequality/document/root.bib b/thys/Pluennecke_Ruzsa_Inequality/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Pluennecke_Ruzsa_Inequality/document/root.bib @@ -0,0 +1,22 @@ +%% This BibTeX bibliography file was created using BibDesk. +%% http://bibdesk.sourceforge.net/ + + +%% Created for Larry Paulson at 2022-05-24 14:39:58 +0100 + + +%% Saved with string encoding Unicode (UTF-8) + + + +@inproceedings{petridis-plunnecke-ruzsa, + abstract = {In this expository article we present an overview of the Pl{\"u}nnecke--Ruzsa inequality: the known proofs, some of its well-known applications and possible extensions. We begin with the graph-theoretic setting in which Pl{\"u}nnecke and later Ruzsa worked in. The more purely combinatorial proofs of the inequality are subsequently presented. In the concluding sections we discuss the sharpness of the various results presented thus far and possible extensions of the inequality to the non-commutative setting.}, + author = {Petridis, G.}, + booktitle = {Combinatorial and Additive Number Theory}, + date-modified = {2022-05-24 14:39:58 +0100}, + editor = {Nathanson, Melvyn B.}, + isbn = {978-1-4939-1601-6}, + pages = {229-241}, + publisher = {Springer}, + title = {The {Pl{\"u}nnecke--Ruzsa} Inequality: An Overview}, + year = {2014}} diff --git a/thys/Pluennecke_Ruzsa_Inequality/document/root.tex b/thys/Pluennecke_Ruzsa_Inequality/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Pluennecke_Ruzsa_Inequality/document/root.tex @@ -0,0 +1,42 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amssymb} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + + +\begin{document} + +\title{The Pl\"{u}nnecke-Ruzsa Inequality} +\author{Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson} +\maketitle + +\begin{abstract} +We formalise Pl\"{u}nnecke's inequality and the Pl\"{u}nnecke-Ruzsa inequality, +following the notes by Timothy Gowers: "Introduction to Additive +Combinatorics" (2022) for the University of Cambridge. To this end, we first introduce basic definitions +and prove elementary facts on sumsets and difference sets. Then, we show two versions of +the Ruzsa triangle inequality. We follow with a proof due to Petridis~\cite{petridis-plunnecke-ruzsa}. +\end{abstract} + +\newpage +\tableofcontents + +\paragraph*{Acknowledgements} +The authors were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council. + +\newpage + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,681 +1,682 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multiset_Ordering_NPC Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker Package_logic PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates +Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL