diff --git a/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy b/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy new file mode 100644 --- /dev/null +++ b/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy @@ -0,0 +1,845 @@ +section\Kneser's Theorem and the Cauchy–Davenport Theorem: main proofs\ + +(* + Session: Kneser_Cauchy_Davenport + Title: Kneser_Cauchy_Davenport_main_proofs.thy + Authors: Mantas Bakšys and Angeliki Koutsoukou-Argyraki, University of Cambridge. + Date: September 2022 +*) + +theory Kneser_Cauchy_Davenport_main_proofs + imports + Kneser_Cauchy_Davenport_preliminaries + +begin + +context additive_abelian_group + +begin + +subsection\Proof of Kneser's Theorem\ + +text\The proof we formalise follows the paper \cite{DeVos_Kneser}. This version of Kneser's Theorem +corresponds to Theorem 3.2 in \cite{Ruzsa_book}, or to Theorem 4.3 in \cite{Nathanson_book}. \ + +theorem Kneser: + assumes "A \ G" and "B \ G" and "finite A" and "finite B" and hAne: "A \ {}" and hBne: "B \ {}" + shows "card (sumset A B) \ card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))" +proof- + have "\ n A B. additive_abelian_group G (\) \ \ A \ G \ B \ G \ + finite A \ finite B \ A \ {} \ B \ {} \ card (sumset A B) + card A = n \ + card (sumset A B) \ card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card ((stabilizer (sumset A B)))" + proof- + fix n + show "\ A B. additive_abelian_group G (\) \ \ A \ G \ B \ G \ + finite A \ finite B \ A \ {} \ B \ {} \ card (sumset A B) + card A = n \ + card (sumset A B) \ card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card ((stabilizer (sumset A B)))" + proof(induction n arbitrary : G "(\)" \ rule: nat_less_induct) + fix n + fix A B G :: "'a set" + fix add (infixl "[\]" 65) + fix zero ("[\]") + assume hind: "\mx xa xb :: 'a set. \ xc xd. + additive_abelian_group xb xc xd \ x \ xb \ + xa \ xb \ finite x \ finite xa \ x \ {} \ xa \ {} \ + card (additive_abelian_group.sumset xb xc x xa) + card x = m \ + card (additive_abelian_group.sumset xb xc x (additive_abelian_group.stabilizer xb xc + (additive_abelian_group.sumset xb xc x xa))) + card (additive_abelian_group.sumset xb xc xa + (additive_abelian_group.stabilizer xb xc (additive_abelian_group.sumset xb xc x xa))) - + card (additive_abelian_group.stabilizer xb xc (additive_abelian_group.sumset xb xc x xa)) + \ card (additive_abelian_group.sumset xb xc x xa)" and + hGroupG: "additive_abelian_group G ([\]) [\]" and hAG: "A \ G" and hBG: "B \ G" and + hA: "finite A" and hB: "finite B" and hAne: "A \ {}" and hBne: "B \ {}" and + hcardsum: "card (additive_abelian_group.sumset G ([\]) A B) + card A = n" + interpret G: additive_abelian_group G "([\])" "[\]" using hGroupG by simp + have hindG: "\mC D. C \ G \ + D \ G \ finite C \ finite D \ C \ {} \ D \ {} \ + card (G.sumset C D) + card C = m \ + card (G.sumset C (G.stabilizer + (G.sumset C D))) + card (G.sumset D + (G.stabilizer (G.sumset C D))) - + card (G.stabilizer (G.sumset C D)) + \ card (G.sumset C D)" using hind hGroupG by blast + show "card (G.sumset A (G.stabilizer (G.sumset A B))) + + card (G.sumset B (G.stabilizer (G.sumset A B))) - + card (G.stabilizer (G.sumset A B)) \ card (G.sumset A B)" + proof(cases "G.stabilizer (G.sumset A B) = {[\]}") + case hstab0: True + show ?thesis + proof (cases "card A = 1") + case True + then obtain a where "A = {a}" and "a \ G" + by (metis hAG card_1_singletonE insert_subset) + then show ?thesis using G.card_sumset_singleton_subset_eq + G.stabilizer_left_sumset_invariant G.stabilizer_subset_group G.sumset_commute + G.sumset_stabilizer_eq_self hBG by (metis diff_add_inverse eq_imp_le) + next + case False + then have "card A \ 2" using Suc_1 order_antisym_conv + by (metis Suc_eq_plus1 bot.extremum card_seteq hA hAne le_add2 not_less_eq_eq) + then obtain a a' where haA: "{a', a} \ A" and hanot: "a' \ a" and ha1G: "a \ G" and + ha2G: "a' \ G" + by (smt (verit, ccfv_threshold) card_2_iff hAG insert_subset + obtain_subset_with_card_n subset_trans) + then have "(a' [\] (G.inverse a)) \ G.stabilizer B" using G.stabilizer_sub_sumset_right + hstab0 subset_singletonD by (metis G.commutative G.inverse_closed + G.invertible G.invertible_right_inverse2 G.right_unit empty_iff insert_iff) + then obtain b where hb: "b \ B" and "(a' [\] (G.inverse a)) [\] b \ B" + using G.stabilizer_def G.not_mem_stabilizer_obtain hBG hB hBne ha1G ha2G + G.composition_closed G.inverse_closed by (metis (no_types, lifting)) + then have habG: "a' [\] b [\] G.inverse a \ B" + using hb hBG ha1G ha2G by (metis G.associative G.commutative G.inverse_closed subset_iff) + have hbG: "b \ G" using hb hBG by auto + let ?B' = "G.sumset (G.differenceset B {b}) {a}" + have hB': "finite ?B'" using hB + by (simp add: G.finite_minusset G.finite_sumset) + have hB'G: "?B' \ G" using G.sumset_subset_carrier by blast + have hB'ne: "?B' \ {}" using hBne hbG ha1G sumset_is_empty_iff hBG by auto + have hstabeq: "G.stabilizer (G.sumset A B) = G.stabilizer (G.sumset A ?B')" + using hbG ha1G hAG hBG G.stabilizer_unchanged by blast + have hstab0': "G.stabilizer (G.sumset A ?B') = {[\]}" using hstab0 hstabeq by blast + have ha1B': "a \ ?B'" + proof- + have "(b [\] G.inverse b) [\] a \ ?B'" using hBG hbG ha1G hb G.minusset.minussetI by blast + thus "a \ ?B'" by (simp add: hbG ha1G) + qed + then have hinter_nempty: "A \ ?B' \ {}" using ha1B' haA by blast + have ha2B': "a' \ ?B'" + proof- + have h1: "(a' [\] b [\] G.inverse a) [\] G.inverse b \ G.differenceset B {b}" + proof + assume "(a' [\] b [\] G.inverse a) [\] G.inverse b \ G.differenceset B {b}" + then obtain b' where "(a' [\] b [\] G.inverse a) [\] G.inverse b = b' [\] G.inverse b" + and "b' \ B" using hbG G.minusset.simps G.sumset.cases by force + then have "(a' [\] b [\] G.inverse a) \ B" using hbG + by (smt (verit) G.composition_closed hBG ha1G ha2G G.inverse_closed G.invertible + G.invertible_right_cancel subsetD) + thus "False" using habG by auto + qed + have "((a' [\] b [\] G.inverse a) [\] G.inverse b) [\] a \ ?B'" + proof + assume "((a' [\] b [\] G.inverse a) [\] G.inverse b) [\] a \ ?B'" + then obtain b' where "((a' [\] b [\] G.inverse a) [\] G.inverse b) [\] a = b' [\] a" + and "b' \ G.differenceset B {b}" using ha1G G.sumset.simps by auto + then have "((a' [\] b [\] G.inverse a) [\] G.inverse b) \ G.differenceset B {b}" + using ha1G by (smt (z3) G.sumset.simps G.additive_abelian_group_axioms + G.composition_closed ha2G hbG G.inverse_closed G.invertible G.invertible_right_cancel) + thus "False" using h1 by auto + qed + thus "a' \ ?B'" using ha1G hbG + by (smt (verit, del_insts) G.associative G.commutative G.composition_closed ha2G + G.inverse_closed G.invertible G.invertible_left_inverse G.right_unit) + qed + have hinterA: "A \ ?B' \ A" using haA ha2B' by auto + have hintercard0: "0 < card (A \ ?B')" + using hA hB hinter_nempty card_gt_0_iff by blast + have hintercardA: "card (A \ ?B') < card A" using hA hB hinterA card_mono + by (simp add: psubsetI psubset_card_mono) + have inj: "inj_on (\ x. x [\] G.inverse b [\] a) G" using inj_onI ha1G hb G.invertible + G.inverse_closed G.composition_closed by (smt (verit) G.invertible_right_cancel hbG) + have 1: "card (G.sumset A B) = card (G.sumset A ?B')" + using G.card_differenceset_singleton_mem_eq G.card_sumset_singleton_subset_eq hAG hB'G + ha1G hbG G.sumset_assoc G.sumset_commute G.sumset_subset_carrier + by (smt (verit, del_insts)) + obtain C where hCconv: "G.convergent C A ?B'" and hCmin: "\ Y. Y \ G.convergent_set A ?B' + \ card (G.stabilizer Y) \ card (G.stabilizer C)" + using G.exists_convergent_min_stabilizer[of n A ?B'] + hindG hA hB' hAG hB'G hinter_nempty hAne hcardsum hintercardA 1 hGroupG by auto + have hC: "C \ G.sumset A ?B'" and hCne: "C \ {}" and + hCcard: "card C + card (G.stabilizer C) \ + card (A \ ?B') + card (G.sumset (A \ ?B') (G.stabilizer C))" + using G.convergent_def hCconv by auto + then have hCfinite: "finite C" using hC G.finite_sumset hA hB' + by (meson finite_subset) + have htranslate: "card (G.sumset A {[\]}) + card (G.sumset ?B' {[\]}) - card {[\]} \ + card (G.sumset A ?B')" + proof(cases "G.stabilizer C = {[\]}") + case hCstab0: True + have "card (G.sumset A {[\]}) + card (G.sumset ?B' {[\]}) - card {[\]} = card A + card ?B' - + card {[\]}" using hAG hB'G G.card_minusset' by fastforce + also have "... = card (A \ ?B') + card (A \ ?B') - card {[\]}" + using hA hB' card_Un_Int by fastforce + also have "... = card (A \ ?B') + card (G.sumset (A \ ?B') {[\]}) - card {[\]}" + by (simp add: Int_absorb1 Int_commute hAG G.sumset_subset_carrier) + also have "... \ card C" using hCcard hCstab0 by auto + also have "... \ card (G.sumset A ?B')" + using hC card_mono G.finite_sumset hA hB' by metis + finally show ?thesis by simp + next + case hCstab_ne0: False + have hCG: "C \ G" using hC by (meson subset_trans G.sumset_subset_carrier) + then have hstabC: "finite (G.stabilizer C)" using G.stabilizer_finite hCne hC + G.finite_sumset hA hB' by (metis Nat.add_0_right add_leE card.infinite hCcard + hintercard0 le_0_eq not_gr0) + then have hcardstabC_gt_1: "card (G.stabilizer C) > 1" using G.zero_mem_stabilizer + hCstab_ne0 hCG by (metis card_1_singletonE card_gt_0_iff diffs0_imp_equal empty_iff + gr_zeroI insertE less_one zero_less_diff) + have "G.sumset (G.stabilizer C) (G.sumset A ?B') \ G.sumset A ?B'" + using G.finite_sumset G.stabilizer_is_nonempty G.stabilizer_subset_group + G.sumset_eq_sub_stabilizer G.sumset_subset_carrier hA hB' hCstab_ne0 hstab0' + subset_singletonD by metis + moreover have "card (G.sumset (G.stabilizer C) (G.sumset A ?B')) \ card (G.sumset A ?B')" + using G.card_le_sumset G.finite_sumset hA hB' hstabC + by (meson hCG G.sumset_subset_carrier G.unit_closed G.zero_mem_stabilizer) + ultimately have "\ G.sumset (G.stabilizer C) (G.sumset A ?B') \ G.sumset A ?B'" + using G.finite_sumset hA hB' card_seteq by metis + then obtain x where hx1: "x \ G.sumset (G.stabilizer C) (G.sumset A ?B')" and + hx2: "x \ G.sumset A ?B'" by auto + then obtain a1 b1 c where "x = c [\] (a1 [\] b1)" and "c \ G.stabilizer C" and + ha1A: "a1 \ A" and hb1B': "b1 \ ?B'" and ha1memG: "a1 \ G" and hb1memG: "b1 \ G" + by (metis (no_types, lifting) G.sumset.cases) + then have hx: "x \ G.sumset (G.stabilizer C) {a1 [\] b1}" + using hx1 by (meson G.composition_closed hAG hB'G insertI1 G.stabilizer_subset_group + subsetD G.sumset.sumsetI) + then have hnotsubAB: "\ G.sumset {a1 [\] b1} (G.stabilizer C) \ G.sumset A ?B'" + using hx2 G.sumset_commute by auto + let ?A1 = "A \ (G.sumset {a1} (G.stabilizer C))" + let ?A2 = "A \ (G.sumset {b1} (G.stabilizer C))" + let ?B1 = "?B' \ (G.sumset {b1} (G.stabilizer C))" + let ?B2 = "?B' \ (G.sumset {a1} (G.stabilizer C))" + let ?C1 = "C \ (G.sumset ?A1 ?B1)" + let ?C2 = "C \ (G.sumset ?A2 ?B2)" + let ?H1 = "G.stabilizer (G.sumset ?A1 ?B1)" + let ?H2 = "G.stabilizer (G.sumset ?A2 ?B2)" + have hA1ne: "?A1 \ {}" using ha1A G.zero_mem_stabilizer hCG + by (metis (full_types) disjoint_iff_not_equal hAG insertCI G.right_unit subset_eq + G.sumset.sumsetI G.unit_closed) + have hB1ne: "?B1 \ {}" using hb1B' G.zero_mem_stabilizer hCG + by (metis G.composition_closed disjoint_iff_not_equal insertCI G.left_unit + G.sumset.cases G.sumset.sumsetI G.sumset_commute G.unit_closed) + have hnotsubC: "\ G.sumset {a1 [\] b1} (G.stabilizer C) \ C" using hnotsubAB hC by blast + have habstabempty: "G.sumset {a1 [\] b1} (G.stabilizer C) \ C = {}" + proof(rule ccontr) + assume "G.sumset {a1 [\] b1} (G.stabilizer C) \ C \ {}" + then obtain z where + hz: "G.sumset {a1 [\] b1} (G.stabilizer C) \ G.sumset {z} (G.stabilizer C) \ {}" and + hzC: "z \ C" using G.stabilizer_coset_Un hCG by blast + then have "G.sumset {a1 [\] b1} (G.stabilizer C) = G.sumset {z} (G.stabilizer C)" using hz + G.sumset_stabilizer_eq_iff hCG G.sumset.simps hx by auto + then have "G.sumset {a1 [\] b1} (G.stabilizer C) \ C" using hzC + by (simp add: hCG G.stabilizer_coset_subset) + thus "False" using hnotsubC by simp + qed + have hA1B1sub: "G.sumset ?A1 ?B1 \ G.sumset {a1 [\] b1} (G.stabilizer C)" and + hB2A2sub: "G.sumset ?B2 ?A2 \ G.sumset {a1 [\] b1} (G.stabilizer C)" + using G.sumset_Inter_subset_sumset ha1memG hb1memG by auto + then have hA1B1Cempty: "G.sumset ?A1 ?B1 \ C = {}" using habstabempty by blast + then have hcardC1: "card ?C1 = card C + card (G.sumset ?A1 ?B1)" using card_Un_disjoint + G.finite_sumset hA hB' finite_Int hC finite_subset Int_commute by metis + have hA1B1cardless: "card (G.sumset ?A1 ?B1) < card (G.sumset A B)" + proof- + have "G.sumset ?A1 ?B1 \ G.sumset A ?B'" using G.sumset_mono by auto + moreover have "G.sumset ?A1 ?B1 \ G.sumset A ?B'" + using hA1B1Cempty hC hCne hA1B1sub by auto + ultimately show "card (G.sumset ?A1 ?B1) < card (G.sumset A B)" + using G.finite_sumset hA hB' psubset_card_mono psubset_eq 1 by metis + qed + have hB2A2Cempty: "G.sumset ?B2 ?A2 \ C = {}" using habstabempty hB2A2sub by blast + then have hcardC2: "card ?C2 = card C + card (G.sumset ?B2 ?A2)" using card_Un_disjoint + G.finite_sumset hA hB' finite_Int hC finite_subset Int_commute G.sumset_commute by metis + have hA2B2cardless: "card (G.sumset ?A2 ?B2) < card (G.sumset A B)" + proof- + have "G.sumset ?A2 ?B2 \ G.sumset A ?B'" + using G.sumset_mono hB2A2Cempty hC hCne hB2A2sub G.sumset_commute psubset_eq + by (metis Int_absorb1 Int_lower1) + then show ?thesis by (simp add: 1 G.finite_sumset hA hB' psubset_card_mono) + qed + have "card ?A1 \ card A" using card_mono hA by (metis Int_lower1) + then have "card (G.sumset ?A1 ?B1) + card ?A1 < card (G.sumset A B) + card A" + using hA1B1cardless by linarith + then obtain l where hln: "l < n" and hind1: "card (G.sumset ?A1 ?B1) + card ?A1 = l" + using hcardsum by auto + have "card ?A2 \ card A" using card_mono hA Int_lower1 by metis + then have "card (G.sumset ?A2 ?B2) + card ?A2 < card (G.sumset A B) + card A" + using hA2B2cardless by linarith + then obtain k where hkn: "k < n" and hind2: "card (G.sumset ?A2 ?B2) + card ?A2 = k" + using hcardsum by auto + have hH1stabC: "?H1 \ G.stabilizer C" using G.stabilizer_sumset_psubset_stabilizer + hA1ne hB1ne ha1memG hb1memG hnotsubAB by presburger + then have "card ?H1 < card (G.stabilizer C)" using psubset_card_mono hstabC by auto + moreover have hC1H1: "?H1 = G.stabilizer ?C1" using G.stabilizer_eq_stabilizer_union + by (metis Int_commute hA hA1B1Cempty hA1ne hB' hB1ne hC hCfinite hCne ha1memG hb1memG hnotsubAB) + ultimately have hC1notconv: "\ G.convergent ?C1 A ?B'" using hCmin G.convergent_set_def + le_antisym less_imp_le_nat less_not_refl2 by fastforce + have hC1ne: "?C1 \ {}" and hC2ne: "?C2 \ {}" using hCne by auto + have hC1AB': "?C1 \ G.sumset A ?B'" and hC2AB': "?C2 \ G.sumset A ?B'" using hC + by (auto simp add: G.sumset_mono) + have hA1G: "?A1 \ G" and hA1 : "finite ?A1" and hB1G: "?B1 \ G" and hB1: "finite ?B1" + using hAG hB'G hA hB' finite_Int by auto + then have hindA1B1: "card (G.sumset ?A1 ?H1) + card (G.sumset ?B1 ?H1) - card ?H1 \ + card (G.sumset ?A1 ?B1)" using hindG hGroupG hA1ne hB1ne hind1 hln hAG hB'G + hA hB' by metis + have hC1notconv_ineq: + "(int (card ?C1) + card ?H1 - card (A \ ?B')) < int (card (G.sumset (A \ ?B') ?H1))" + using hC1notconv hC1ne hC1AB' hC1H1 G.convergent_def by auto + have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H1) + \ (int (card C) + card (G.stabilizer C) - card (A \ ?B')) - card (G.sumset (A \ ?B') ?H1)" + using hCcard by linarith + then have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H1) < + (int (card C) + card (G.stabilizer C) - card (A \ ?B')) - + (int (card ?C1) + card ?H1 - card (A \ ?B'))" using hC1notconv_ineq by linarith + also have "... = int (card (G.stabilizer C)) - card ?H1 - card (G.sumset ?A1 ?B1)" + using hcardC1 by presburger + also have "... \ int (card (G.stabilizer C)) - card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)" + using hindA1B1 by linarith + text\ Finally, we deduce the inequality that is referred to as + inequality (1) in \cite{DeVos_Kneser} for @{term ?A1} and @{term ?B1}. \ + finally have hA1B1ineq: "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - + card (G.sumset (A \ ?B') ?H1) < int (card (G.stabilizer C)) - + card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)" by simp + have hB2ne: "?B2 \ {}" using G.sumset_inter_ineq hA1B1ineq ha1A ha1G hA hB' hAne hB'ne + hstabC hH1stabC ha1memG of_nat_0_le_iff by (smt (verit, del_insts)) + have hA2ne: "?A2 \ {}" using G.sumset_inter_ineq[of "A" "b1" "C" "?B'" "a1"] hA1B1ineq + hb1B' hb1memG hA hB' hAne hB'ne hstabC hH1stabC of_nat_0_le_iff G.sumset_commute Un_commute by (smt (verit, ccfv_SIG)) + have hH2stabC: "?H2 \ G.stabilizer C" using G.stabilizer_sumset_psubset_stabilizer + G.commutative hA2ne hB2ne ha1memG hb1memG hnotsubAB by presburger + then have "card ?H2 < card (G.stabilizer C)" using psubset_card_mono hstabC by auto + moreover have hC2H2: "?H2 = G.stabilizer ?C2" using G.stabilizer_eq_stabilizer_union + by (smt (verit, ccfv_threshold) G.sumset_commute Int_commute hA hA2ne hB' hB2A2Cempty + hB2ne hC hCfinite hCne ha1memG hb1memG hnotsubAB) + ultimately have hC2notconv: "\ G.convergent ?C2 A ?B'" + using hCmin G.convergent_set_def le_antisym less_imp_le_nat less_not_refl2 + by fastforce + have hA2G: "?A2 \ G" and hA2 : "finite ?A2" and hB2G: "?B2 \ G" and hB2: "finite ?B2" + using hAG hB'G hA hB' finite_Int by auto + then have hindA2B2: "card (G.sumset ?A2 ?H2) + card (G.sumset ?B2 ?H2) - card ?H2 \ + card (G.sumset ?A2 ?B2)" + using hindG hGroupG hA2ne hB2ne hind2 hkn hAG hB'G hA hB' by metis + have hC2notconv_ineq: + "(int (card ?C2) + card ?H2 - card (A \ ?B')) < int (card (G.sumset (A \ ?B') ?H2))" + using hC2notconv hC2ne hC2AB' hC2H2 G.convergent_def by auto + have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H2) + \ (int (card C) + card (G.stabilizer C) - card (A \ ?B')) - card (G.sumset (A \ ?B') ?H2)" + using hCcard by linarith + then have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H2) < + (int (card C) + card (G.stabilizer C) - card (A \ ?B')) - + (int (card ?C2) + card ?H2 - card (A \ ?B'))" using hC2notconv_ineq by linarith + also have "... = int (card (G.stabilizer C)) - card ?H2 - card (G.sumset ?A2 ?B2)" + using hcardC2 G.sumset_commute by simp + also have "... \ int (card (G.stabilizer C)) - card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)" + using hindA2B2 by linarith + + text\ Analogously, we deduce the inequality that is referred to as + inequality (1) in \cite{DeVos_Kneser} for @{term ?A2} and @{term ?B2}. \ + + finally have hA2B2ineq: "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - + card (G.sumset (A \ ?B') ?H2) < int (card (G.stabilizer C)) - + card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)" by simp + have hfinsumH2:"finite (G.sumset (A \ ?B') ?H2)" + using G.finite_sumset hA hB' finite_UnI hstabC hH2stabC finite_subset psubset_imp_subset + by metis + have hsubsumH2: "G.sumset (A \ ?B') ?H2 \ G.sumset (A \ ?B') (G.stabilizer C)" + using G.sumset.cases hAG hB'G G.stabilizer_subset_group hH2stabC psubset_imp_subset + by (smt (verit, best) subset_Un_eq G.sumset_commute G.sumset_subset_Un1) + then have hsumH2card_le: "card (G.sumset (A \ ?B') ?H2) \ + card (G.sumset (A \ ?B') (G.stabilizer C))" + using card_mono G.finite_sumset G.stabilizer_finite hC hCne hCG hA hB' + by (metis finite_UnI hstabC) + have hfinsumH1: "finite (G.sumset (A \ ?B') ?H1)" + using finite_sumset finite_Un psubsetE by (metis G.finite_sumset G.stabilizer_finite + G.sumset_subset_carrier Int_Un_eq(4) hA hA1 hB' hB1 hC1H1 hH1stabC habstabempty) + have hsubsumH1: "G.sumset (A \ ?B') ?H1 \ G.sumset (A \ ?B') (G.stabilizer C)" + using G.sumset.cases psubsetE subset_refl G.sumset_mono hH1stabC by simp + have hsumH1card_le: "card (G.sumset (A \ ?B') ?H1) \ card (G.sumset (A \ ?B') (G.stabilizer C))" + using card_mono G.finite_sumset G.stabilizer_finite by (metis finite_UnI hA hB' hstabC hsubsumH1) + have ha1b1stabCne: "G.sumset {a1} (G.stabilizer C) \ G.sumset {b1} (G.stabilizer C)" + proof + assume ha1b1: "G.sumset {a1} (G.stabilizer C) = G.sumset {b1} (G.stabilizer C)" + have hfin: "finite (G.sumset ?A1 ?H1 \ G.sumset ?B1 ?H1)" + using finite_UnI G.finite_sumset hA1 hB1 hH1stabC hstabC psubset_imp_subset + by (metis finite_subset) + have "int (card (G.sumset {a1} (G.stabilizer C))) - card (G.sumset ?A1 ?H1) - + card (G.sumset ?B1 ?H1) \ int (card (G.sumset {a1} (G.stabilizer C))) - + card (G.sumset ?A1 ?H1 \ G.sumset ?B1 ?H1)" + using card_Un_le[of "G.sumset ?A1 ?H1" "G.sumset ?B1 ?H1"] by linarith + also have "... \ card (G.sumset {a1} (G.stabilizer C) - (G.sumset ?A1 ?H1 \ G.sumset ?B1 ?H1))" + using diff_card_le_card_Diff[of "G.sumset ?A1 ?H1 \ G.sumset ?B1 ?H1" + "G.sumset {a1} (G.stabilizer C)"] hfin by linarith + also have "... \ card (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1 \ ?B1) ?H1)" + using G.sumset_subset_Un1 by auto + also have "... \ card (G.sumset (A \ ?B') (G.stabilizer C) - G.sumset (A \ ?B') ?H1)" + proof- + have hsub: "G.sumset {a1} (G.stabilizer C) - G.sumset (?A1 \ ?B1) ?H1 \ + G.sumset (A \ ?B') (G.stabilizer C) - G.sumset (A \ ?B') ?H1" + proof + fix x assume hx: "x \ G.sumset {a1} (G.stabilizer C) - G.sumset (?A1 \ ?B1) ?H1" + then obtain c where hxac: "x = a1 [\] c" and hc: "c \ G.stabilizer C" + using G.sumset.cases by blast + then have "x \ G.sumset (A \ ?B') (G.stabilizer C)" using ha1A hAG + G.stabilizer_subset_group by (simp add: subset_iff G.sumset.sumsetI) + moreover have "x \ G.sumset (A \ ?B') ?H1" + proof + assume hx1: "x \ G.sumset (A \ ?B') ?H1" + then obtain y h1 where hxy: "x = y [\] h1" and hy: "y \ A \ ?B'" and + hh1: "h1 \ ?H1" using G.sumset.cases by blast + then have hyG: "y \ G" and hcG: "c \ G" and hh1G: "h1 \ G" + using hAG hB'G G.stabilizer_subset_group hc by auto + then have "y = a1 [\] (c [\] G.inverse h1)" using hxac hxy ha1A hAG + by (metis G.associative G.commutative G.composition_closed in_mono + G.inverse_closed G.invertible G.invertible_left_inverse2) + moreover have "h1 \ G.stabilizer C" using hh1 hH1stabC by auto + moreover hence "c [\] G.inverse h1 \ G.stabilizer C" using hc + G.stabilizer_is_subgroup subgroup_def G.group_axioms + group.invertible subgroup.subgroup_inverse_iff + submonoid.sub_composition_closed hh1G by metis + ultimately have "y \ G.sumset {a1} (G.stabilizer C)" using ha1G hcG hAG ha1A hh1G + by blast + then have "y \ ?A1 \ ?B1" using hy by (simp add: ha1b1) + thus "False" using hx hxy hh1 hh1G hyG by auto + qed + ultimately show "x \ G.sumset (A \ ?B') (G.stabilizer C) - G.sumset (A \ ?B') ?H1" by simp + qed + moreover have "finite (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1 \ ?B1) ?H1)" + using finite_subset G.finite_sumset hstabC by simp + moreover hence "finite (G.sumset (A \ ?B') (G.stabilizer C) - G.sumset (A \ ?B') ?H1)" + using finite_subset G.finite_sumset hstabC hA hB' finite_UnI by simp + moreover have "card (G.sumset {a1} (G.stabilizer C) - G.sumset (?A1 \ ?B1) ?H1) \ + card (G.sumset (A \ ?B') (G.stabilizer C) - G.sumset (A \ ?B') ?H1)" + using card_mono hsub calculation(3) by auto + ultimately show ?thesis using card_Diff_subset by linarith + qed + also have "... = int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H1)" + using card_Diff_subset[OF hfinsumH1 hsubsumH1] hsumH1card_le by linarith + finally have "int (card (G.stabilizer C)) - card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1) + \ int (card (G.sumset (A \ ?B') (G.stabilizer C))) - card (G.sumset (A \ ?B') ?H1)" + using hCG subset_iff G.card_sumset_singleton_subset_eq G.stabilizer_subset_group + hAG ha1A by auto + thus "False" using hA1B1ineq by linarith + qed + have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - + card (G.sumset (A \ ?B') ?H1) \ 0" by (simp add: hsumH1card_le) + then have "int (card (G.stabilizer C)) - + card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1) > 0" using hA1B1ineq by linarith + moreover have "int (card ?H1) dvd int (card (G.stabilizer C)) - + card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1)" using + G.stabilizer_subset_stabilizer_dvd hH1stabC psubset_imp_subset int_dvd_int_iff dvd_diff + G.card_stabilizer_divide_sumset[OF hA1G] G.card_stabilizer_divide_sumset[OF hB1G] + by fastforce + ultimately have "int (card (G.stabilizer C)) - + card (G.sumset ?A1 ?H1) - card (G.sumset ?B1 ?H1) \ int (card ?H1)" + using zdvd_imp_le by blast + moreover have hA1_le_sum: "card ?A1 \ card (G.sumset ?A1 ?H1)" + using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer hA1G hA1 hH1stabC hstabC + by (metis finite_subset psubset_imp_subset G.unit_closed) + moreover have hB1_le_sum: "card ?B1 \ card (G.sumset ?B1 ?H1)" + using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer hB1G hB1 hH1stabC hstabC + by (metis finite_subset psubset_imp_subset G.unit_closed) + + text\ The above facts combined allow us to deduce the inequality that is referred to as + inequality (2) in \cite{DeVos_Kneser} for @{term ?A1}, @{term ?B1} and @{term ?H1}. \ + + ultimately have 21: "int (card (G.stabilizer C)) \ int (card ?H1) + card ?A1 + card ?B1" + by linarith + have "int (card (G.sumset (A \ ?B') (G.stabilizer C))) - + card (G.sumset (A \ ?B') ?H2) \ 0" by (simp add: hsumH2card_le) + then have "int (card (G.stabilizer C)) - + card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2) > 0" using hA2B2ineq by linarith + moreover have "int (card ?H2) dvd int (card (G.stabilizer C)) - + card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2)" using psubset_imp_subset + G.stabilizer_subset_stabilizer_dvd hH2stabC int_dvd_int_iff dvd_diff + G.card_stabilizer_divide_sumset[OF hA2G] G.card_stabilizer_divide_sumset[OF hB2G] + by fastforce + ultimately have "int (card (G.stabilizer C)) - + card (G.sumset ?A2 ?H2) - card (G.sumset ?B2 ?H2) \ int (card ?H2)" + using zdvd_imp_le by blast + moreover have hA2_le_sum: "card ?A2 \ card (G.sumset ?A2 ?H2)" + using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer G.stabilizer_subset_group + hA2G hA2 hH2stabC hstabC psubset_imp_subset by (metis finite_subset G.unit_closed) + moreover have hB2_le_sum: "card ?B2 \ card (G.sumset ?B2 ?H2)" + using G.sumset_commute G.card_le_sumset G.zero_mem_stabilizer G.stabilizer_subset_group + hB2G hB2 hH2stabC hstabC psubset_imp_subset by (metis finite_subset G.unit_closed) + + text\Analogously, the above facts combined allow us to deduce the inequality that is referred to as + inequality (2) in \cite{DeVos_Kneser} for @{term ?A2}, @{term ?B2} and @{term ?H2}. \ + + ultimately have 22: "int (card (G.stabilizer C)) \ int (card ?H2) + card ?A2 + card ?B2" + by linarith + let ?S = "G.sumset {a1} (G.stabilizer C) - (?A1 \ ?B2)" + let ?T = "G.sumset {b1} (G.stabilizer C) - (?A2 \ ?B1)" + have hS : "finite ?S" and hT: "finite ?T" using G.finite_sumset hstabC by auto + have hST: "?S \ ?T = {}" using ha1b1stabCne Diff_Int2 Diff_Int_distrib2 Int_Diff Int_Un_eq(4) + Int_absorb Int_commute Int_empty_right Int_insert_right Un_empty empty_Diff hA1ne + hA2ne G.sumset_commute G.sumset_is_empty_iff G.sumset_stabilizer_eq_iff + by (smt (verit, ccfv_threshold) G.sumset_assoc) + have hSTcard_le: "card ?S + card ?T + card (G.sumset (A \ ?B') {[\]}) \ + card (G.sumset (A \ ?B') (G.stabilizer C))" + proof- + have "G.sumset {a1} (G.stabilizer C) \ G.sumset (A \ ?B') (G.stabilizer C)" and + "G.sumset {b1} (G.stabilizer C) \ G.sumset (A \ ?B') (G.stabilizer C)" + using G.sumset_mono ha1A hb1B' subset_refl empty_subsetI insert_subset by auto + moreover have "(G.sumset (A \ ?B') {[\]}) \ G.sumset (A \ ?B') (G.stabilizer C)" + using G.sumset_mono subset_refl empty_subsetI insert_subset G.zero_mem_stabilizer + by metis + ultimately have hsub: "?S \ ?T \ (G.sumset (A \ ?B') {[\]}) \ + G.sumset (A \ ?B') (G.stabilizer C)" by blast + have "?S \ G.sumset (A \ ?B') {[\]} = {}" by auto + moreover have "(?S \ ?T) \ G.sumset (A \ ?B') {[\]} = {}" by auto + ultimately have "card ?S + card ?T + card (G.sumset (A \ ?B') {[\]}) = + card (?S \ ?T \ (G.sumset (A \ ?B') {[\]}))" using card_Un_disjoint hS hT + G.finite_sumset finite_UnI hA hB' hST by (metis finite.emptyI finite.insertI) + also have "... \ card (G.sumset (A \ ?B') (G.stabilizer C))" using card_mono + G.finite_sumset finite_UnI hA hB' hstabC hsub by metis + finally show ?thesis by simp + qed + have hAB_not_conv: "\ G.convergent (G.sumset A ?B') A ?B'" using hCmin hstab0 + G.convergent_set_def hcardstabC_gt_1 hstab0' by fastforce + then have "card (G.sumset A ?B') + card {[\]} < card (A \ ?B') + + card (G.sumset (A \ ?B') {[\]})" using G.convergent_def hAne hB'ne hAG hB'G hstab0' + subset_refl by auto + then have hAB'sum: "int (card (G.sumset (A \ ?B') {[\]})) + card (A \ ?B') - + card (G.sumset A ?B') > 1" by simp + moreover have "int (card ?A1) + card ?B1 \ int (card (G.sumset ?A1 ?H1)) + + card (G.sumset ?B1 ?H1)" using hA1_le_sum hB1_le_sum by linarith + moreover hence "int (card ?A1) + card ?B1 - card ?H1 \ card (G.sumset ?A1 ?B1)" + using hindA1B1 by linarith + ultimately have "int (card ?S) + card ?T + card ?A1 + card ?B1 - card ?H1 < + int (card ?S) + card ?T + card (G.sumset (A \ ?B') {[\]}) + card (A \ ?B') - + card (G.sumset A ?B') + card (G.sumset ?A1 ?B1)" by linarith + also have "... \ int (card (G.sumset (A \ ?B') (G.stabilizer C))) + card (A \ ?B') - card C" + proof- + have "G.sumset ?A1 ?B1 \ C \ G.sumset A ?B'" using hC G.sumset_mono by auto + then have "card (G.sumset ?A1 ?B1) + card C \ + card (G.sumset A ?B')" using card_Un_disjoint hCfinite G.finite_sumset hA1 hB1 hA1B1Cempty + card_mono hA hB' by metis + then show ?thesis using hSTcard_le by linarith + qed + + text\From this, inequality (3) \cite{DeVos_Kneser} follows for @{term ?A1}, + @{term ?B1} and @{term ?H1}.\ + + finally have 31: "int (card ?S) + card ?T + card ?A1 + card ?B1 - card ?H1 < + card (G.stabilizer C)" using hCcard by linarith + have "int (card ?A2) + card ?B2 \ int (card (G.sumset ?A2 ?H2)) + + card (G.sumset ?B2 ?H2)" using hA2_le_sum hB2_le_sum by linarith + moreover hence "int (card ?A2) + card ?B2 - card ?H2 \ card (G.sumset ?A2 ?B2)" + using hindA2B2 by linarith + ultimately have "int (card ?S) + card ?T + card ?A2 + card ?B2 - card ?H2 < + int (card ?S) + card ?T + card (G.sumset (A \ ?B') {[\]}) + card (A \ ?B') - + card (G.sumset A ?B') + card (G.sumset ?A2 ?B2)" using hAB'sum by linarith + also have "... \ int (card (G.sumset (A \ ?B') (G.stabilizer C))) + card (A \ ?B') - card C" + proof- + have "G.sumset ?A2 ?B2 \ C \ G.sumset A ?B'" using hC G.sumset_mono by auto + then have "card (G.sumset ?A2 ?B2) + card C \ + card (G.sumset A ?B')" using card_Un_disjoint hCfinite G.finite_sumset hA2 hB2 hA1B1Cempty + card_mono hA hB' hB2A2Cempty G.sumset_commute by metis + then show ?thesis using hSTcard_le by linarith + qed + + text\From this, inequality (3) \cite{DeVos_Kneser} follows for @{term ?A2}, + @{term ?B2} and @{term ?H2}.\ + + finally have 32: "int (card ?S) + card ?T + card ?A2 + card ?B2 - card ?H2 < + card (G.stabilizer C)" using hCcard by linarith + + text\ Adding together the four inequalities obtained by versions of inequalities + (2) and (3) and dividing by 2 gives the following inequality: \ + + have 4: "2 * int (card (G.stabilizer C)) > int (card ?A1) + card ?B2 + card ?S + card ?T + card ?B1 + card ?A2" + using 21 22 31 32 by linarith + have "G.sumset {a1} (G.stabilizer C) = (?S \ ?A1) \ ?B2" and + hb1T: "G.sumset {b1} (G.stabilizer C) = (?T \ ?A2) \ ?B1" by auto + then have "card (G.stabilizer C) \ card ?S + card ?A1 + card ?B2" + using card_Un_le[of "?S" "?A1"] card_Un_le[of "?S \ ?A1" "?B2"] + G.card_sumset_singleton_subset_eq G.stabilizer_subset_group ha1A hAG by auto + moreover have "card (G.stabilizer C) \ card ?T + card ?A2 + card ?B1" + using hb1T card_Un_le[of "?T" "?A2"] card_Un_le[of "?T \ ?A2" "?B1"] + G.card_sumset_singleton_subset_eq G.stabilizer_subset_group hb1B' hB'G by auto + + text\ Combining the inequality labelled @{term 4} above with the above facts, the claim + follows:\ + ultimately show ?thesis using 4 by linarith + qed + + text\It remains to transfer the statement of inequality labelled @{term 1} into an analogous + one, which replaces @{term ?B'} with @{term B}. \ + + have 2: "card (G.sumset A (G.stabilizer (G.sumset A B))) = + card (G.sumset A (G.stabilizer (G.sumset A ?B')))" + using hstabeq by auto + have 3: "card (G.sumset B (G.stabilizer (G.sumset A B))) = + card (G.sumset ?B' (G.stabilizer (G.sumset A ?B')))" using hstabeq hstab0' G.sumset_commute + by (metis G.card_differenceset_singleton_mem_eq G.card_sumset_singleton_subset_eq + G.sumset_D(1) G.sumset_commute G.sumset_subset_carrier Int_absorb1 Int_commute hBG ha1G hbG) + then show ?thesis using 1 2 3 hstabeq hstab0' htranslate by auto + qed + next + case hstabne0: False + let ?K = "G.stabilizer (G.sumset A B)" + have hcardK_gt_1: "card ?K > 1" using G.stabilizer_finite G.sumset_subset_carrier G.finite_sumset + hA hB hstabne0 G.zero_mem_stabilizer by (metis card_0_eq card_1_singletonE G.card_sumset_0_iff + empty_iff hAG hAne hBG hBne insertE less_one linorder_neqE_nat) + interpret K: subgroup_of_additive_abelian_group ?K G "([\])" "[\]" + using G.stabilizer_is_subgroup subgroup_of_additive_abelian_group_def + by (metis G.abelian_group_axioms G.group_axioms hGroupG subgroup_of_abelian_group_def + subgroup_of_group.intro) + let ?\ = "K.Class" + have h\: "\ a. a \ G \ ?\ a = (\ x. G.sumset {x} ?K) a" + using K.Left_Coset_Class_unit G.Left_Coset_eq_sumset_stabilizer by simp + interpret GK: additive_abelian_group "G.Factor_Group G ?K" K.quotient_composition "K.Class [\]" + proof + fix x y assume "x \ K.Partition" and "y \ K.Partition" + then obtain a b where "x = K.Class a" and "y = K.Class b" and "a \ G" and "b \ G" + by (meson K.representant_exists) + then show "K.quotient_composition x y = K.quotient_composition y x" + using K.Class_commutes_with_composition G.commutative by presburger + qed + have hGroupGK: "additive_abelian_group (G.Factor_Group G ?K) K.quotient_composition (K.Class [\])" .. + + text\Here, we specialize the induction hypothesis to the factor group.\ + + let ?K_repr = "K.\ ` K.Partition" + have "\ x y. x \ ?K_repr \ y \ ?K_repr \ K.quot_comp_alt x y = K.quot_comp_alt y x" + using K.quot_comp_alt_def G.commutative K.phi_image_subset subsetD by (metis (full_types)) + then interpret K_repr: additive_abelian_group ?K_repr K.quot_comp_alt "K.\ ?K" + using Group_Theory.group.axioms(1)[OF K.phi_image_group] + by (auto simp add: additive_abelian_group_def abelian_group_def K.phi_image_group + commutative_monoid_axioms_def commutative_monoid_def) + have hindrepr: "\ m C D. m < n \ C \ ?K_repr \ D \ ?K_repr \ finite C \ + finite D \ C \ {} \ D \ {} \ card (K_repr.sumset C D) + card C = m \ + card (K_repr.sumset C (K_repr.stabilizer (K_repr.sumset C D))) + + card (K_repr.sumset D (K_repr.stabilizer (K_repr.sumset C D))) - card (K_repr.stabilizer (K_repr.sumset C D)) \ + card (K_repr.sumset C D)" using hind K_repr.additive_abelian_group_axioms by blast + have hindfactor: "\ m C D. m < n \ C \ K.Partition \ D \ K.Partition \ finite C \ + finite D \ C \ {} \ D \ {} \ card (GK.sumset C D) + card C = m \ + card (GK.sumset C (GK.stabilizer (GK.sumset C D))) + + card (GK.sumset D (GK.stabilizer (GK.sumset C D))) - card (GK.stabilizer (GK.sumset C D)) \ + card (GK.sumset C D)" + proof(intro impI) + fix m C D assume hmn: "m < n" and hCK: "C \ K.Partition" and hDK: "D \ K.Partition" and + hC: "finite C" and hD: "finite D" and hCne: "C \ {}" and hDne: "D \ {}" and + hCDcard: "card (GK.sumset C D) + card C = m" + let ?C = "K.\ ` C" and ?D = "K.\ ` D" + have hCrepr: "?C \ ?K_repr" and hDrepr: "?D \ ?K_repr" using hCK hDK by auto + have hCfin: "finite ?C" and hDfin: "finite ?D" and hCne_1: "?C \ {}" and hDne_1: "?D \ {}" using hC hD hCne hDne by auto + have hcardC: "card ?C = card C" using K.phi_inj_on hC card_image inj_on_subset hCK by metis + have "card (GK.sumset C D) = card (K_repr.sumset ?C ?D)" + using card_image K.phi_inj_on inj_on_subset K.phi_image_sumset_eq + GK.sumset_subset_carrier hCK hDK by (smt (verit, best)) + then have "card (K_repr.sumset ?C ?D) + card ?C = m" using hCDcard hcardC by presburger + then have "card (K_repr.sumset ?C (K_repr.stabilizer (K_repr.sumset ?C ?D))) + + card (K_repr.sumset ?D (K_repr.stabilizer (K_repr.sumset ?C ?D))) - card (K_repr.stabilizer (K_repr.sumset ?C ?D)) \ + card (K_repr.sumset ?C ?D)" + using hindrepr hCfin hDfin hCne_1 hDne_1 hCrepr hDrepr hmn by blast + then show "card (GK.sumset C (GK.stabilizer (GK.sumset C D))) + + card (GK.sumset D (GK.stabilizer (GK.sumset C D))) - card (GK.stabilizer (GK.sumset C D)) \ + card (GK.sumset C D)" using K.phi_image_sumset_eq K.phi_image_stabilizer_eq + K.phi_inj_on inj_on_subset hCK hDK card_image + by (smt (z3) GK.stabilizer_subset_group GK.sumset_subset_carrier) + qed + have hstab0: "GK.stabilizer (?\ ` (G.sumset A B)) = {K.Class [\]}" + proof + show "GK.stabilizer (?\ ` G.sumset A B) \ {K.Class [\]}" + proof + fix x assume hx: "x \ GK.stabilizer (?\ ` G.sumset A B)" + moreover have "?\ ` G.sumset A B \ K.Partition" + using K.natural.map_closed G.sumset_subset_carrier by blast + ultimately have hsum: "GK.sumset {x} (?\ ` G.sumset A B) = ?\ ` G.sumset A B" + using GK.stabilizer_def by auto + obtain x' where hx\: "x = ?\ x'" and hx'G: "x' \ G" + using hx GK.stabilizer_subset_group K.representant_exists by force + have hsumset: "GK.sumset {x} (?\ ` G.sumset A B) = (\ a. ?\ (x' [\] a)) ` G.sumset A B" + proof + show "GK.sumset {x} (?\ ` G.sumset A B) \ (\a. ?\ (x' [\] a)) ` G.sumset A B" + proof + fix y assume "y \ GK.sumset {x} (?\ ` G.sumset A B)" + then obtain z where "z \ G.sumset A B" and "y = K.quotient_composition (?\ x') (?\ z)" + using GK.sumset.cases hx\ by blast + then show "y \ (\a. ?\ (x' [\] a)) ` G.sumset A B" + using K.Class_commutes_with_composition G.composition_closed hx'G G.sumset.cases + imageI by metis + qed + next + show "(\a. ?\ (x' [\] a)) ` G.sumset A B \ GK.sumset {x} (?\ ` G.sumset A B)" + proof + fix y assume "y \ (\a. ?\ (x' [\] a)) ` G.sumset A B" + then obtain z where hz: "z \ G.sumset A B" and "y = ?\ (x' [\] z)" by blast + then have "y = K.quotient_composition (?\ x') (?\ z)" using + K.Class_commutes_with_composition G.composition_closed hx'G G.sumset.cases by metis + then show "y \ GK.sumset {x} (?\ ` G.sumset A B)" + using hx\ hz imageI hx GK.sumset.sumsetI K.natural.map_closed + by (metis G.composition_closed hx'G insertCI G.sumset.cases) + qed + qed + have "G.sumset {x'} (G.sumset A B) \ G.sumset (G.sumset A B) ?K" + proof + fix y assume "y \ G.sumset {x'} (G.sumset A B)" + then obtain z where hz: "z \ G.sumset A B" and hy: "y = x' [\] z" using G.sumset.cases by blast + then have "?\ (x' [\] z) \ ?\ ` G.sumset A B" using hsum hsumset by blast + then obtain w where hw: "{w} \ G.sumset A B" and "w \ G.sumset A B" + and "?\ (x' [\] z) = ?\ w" by auto + then have "(x' [\] z) \ G.differenceset (G.sumset {w} ?K) ?K" + using h\ G.sumset_subset_carrier hx'G hz G.sumset_eq_subset_differenceset + G.composition_closed G.stabilizer_is_nonempty G.stabilizer_subset_group G.sumset.cases + K.Class_self G.differenceset_stabilizer_eq G.sumset_assoc by metis + moreover have "G.differenceset (G.sumset {w} ?K) ?K \ G.sumset {w} ?K" + using hw by (simp add: G.differenceset_stabilizer_eq G.sumset_assoc) + ultimately show "y \ G.sumset (G.sumset A B) ?K" using hy hw G.sumset_mono subsetD + subset_refl by blast + qed + moreover have "G.sumset (G.sumset A B) ?K = G.sumset A B" + using G.sumset_commute G.sumset_stabilizer_eq_self G.sumset_subset_carrier by auto + ultimately have "G.sumset {x'} (G.sumset A B) = G.sumset A B" + by (metis G.finite_sumset G.sumset_subset_carrier card_subset_eq + G.card_sumset_singleton_subset_eq hA hB hx'G) + then have "x' \ ?K" using hx'G by (meson empty_subsetI G.finite_sumset hA hB insert_subset + G.sumset_eq_sub_stabilizer G.sumset_subset_carrier) + then show "x \ {K.Class [\]}" using hx\ + by (metis K.Block_self K.Normal_def K.quotient.unit_closed insertCI) + qed + next + show "{K.Class [\]} \ GK.stabilizer (K.Class ` G.sumset A B)" + using GK.zero_mem_stabilizer by auto + qed + interpret group_epimorphism ?\ G "([\])" "[\]" "G.Factor_Group G ?K" + K.quotient_composition "K.Class [\]" .. + interpret GKN: normal_subgroup_in_kernel K.Class G "([\])" "[\]" "G.Factor_Group G ?K" + K.quotient_composition "K.Class [\]" ?K + proof + show "?K \ Ker" using K.Block_self K.Normal_def K.quotient.unit_closed by blast + qed + have hsumK: "card (G.sumset A B) = card ?K * card (?\ ` (G.sumset A B))" + using G.finite_sumset hA hB G.sumset_subset_carrier G.Union_stabilizer_Class_eq + G.sumset_subset_carrier K.Union_Coset_card_eq by simp + have hGKsumset: "GK.sumset (?\ ` A) (?\ ` B) = ?\ ` (G.sumset A B)" + proof + show "GK.sumset (?\ ` A) (?\ ` B) \ ?\ ` G.sumset A B" + proof + fix x assume "x \ GK.sumset (?\ ` A) (?\ ` B)" + then obtain a b where ha: "a \ A" and hb: "b \ B" and + "x = K.quotient_composition (?\ a) (?\ b)" using GK.sumset.cases by blast + then have "x = ?\ (a [\] b)" by (meson K.Class_commutes_with_composition hAG hBG in_mono) + then show "x \ ?\ ` G.sumset A B" using ha hb hAG hBG by blast + qed + next + show "?\ ` G.sumset A B \ GK.sumset (?\ ` A) (?\ ` B)" + proof + fix x assume "x \ ?\ ` G.sumset A B" + then obtain c where "c \ G.sumset A B" and "x = ?\ c" by blast + then obtain a b where "a \ A" and "b \ B" and "x = ?\ (a [\] b)" + using G.sumset.cases by metis + then show "x \ GK.sumset (?\ ` A) (?\ ` B)" using GK.sumset.cases + K.Class_commutes_with_composition hAG hBG in_mono + by (smt (verit, best) GK.sumset.simps K.natural.map_closed imageI) + qed + qed + have hAK: "card (G.sumset A ?K) = card ?K * card (?\ ` A)" using hAG K.Union_Coset_card_eq hA + G.sumset_stabilizer_eq_Class_Union G.Class_image_sumset_stabilizer_eq + by (smt (verit, ccfv_threshold) card_0_eq G.card_sumset_0_iff G.finite_sumset hAne hB hBG hBne + G.stabilizer_finite G.sumset_subset_carrier) + have hBK: "card (G.sumset B ?K) = card ?K * card (?\ ` B)" using hBG K.Union_Coset_card_eq hB + G.sumset_stabilizer_eq_Class_Union G.Class_image_sumset_stabilizer_eq + by (smt (verit, ccfv_SIG) card_0_eq G.card_sumset_0_iff G.finite_sumset hA hAG hAne hBne + G.stabilizer_finite G.sumset_subset_carrier) + have "card (?\ ` A) \ card A" by (simp add: card_image_le hA) + moreover have "card (?\ ` (G.sumset A B)) < card (G.sumset A B)" using hsumK hcardK_gt_1 + G.card_sumset_0_iff hA hB hAne hBne by (metis card_eq_0_iff card_image_le hAG hBG + le_neq_implies_less less_not_refl3 mult_cancel2 nat_mult_1) + ultimately have "card (GK.sumset (?\ ` A) (?\ ` B)) + card (?\ ` A) < card (G.sumset A B) + card A" + using hGKsumset by auto + then obtain m where "m < n" and "card (GK.sumset (?\ ` A) (?\ ` B)) + card (?\ ` A) = m" + using hcardsum by blast + moreover have h\Asub: "?\ ` A \ G.Factor_Group G ?K" + proof + fix x assume "x \ ?\ ` A" then obtain a where "a \ G" and "?\ a = x" using hAG by blast + then show "x \ G.Factor_Group G ?K" by blast + qed + moreover have h\Bsub: "?\ ` B \ G.Factor_Group G ?K" + proof + fix x assume "x \ ?\ ` B" then obtain b where "b \ G" and "?\ b = x" using hBG by blast + then show "x \ G.Factor_Group G ?K" by blast + qed + moreover have h\A: "finite (?\ ` A)" and h\B: "finite (?\ ` B)" and h\Ane: "?\ ` A \ {}" and + h\Bne: "?\ ` B \ {}" using hA hB hAne hBne by auto + moreover have "additive_abelian_group (G.Factor_Group G ?K) K.quotient_composition + (K.Class [\])" .. + moreover have "GK.stabilizer (GK.sumset (?\ ` A) (?\ ` B)) = {K.Class [\]}" + using hstab0 hGKsumset by auto + ultimately have hind\: "card (GK.sumset (?\ ` A) (?\ ` B)) \ + card (GK.sumset (?\ ` A) {K.Class [\]}) + card (GK.sumset (?\ ` B) {K.Class [\]}) - 1" + using hindfactor[of "m" "?\ ` A" "?\ ` B"] by simp + have h\sumA: "GK.sumset (?\ ` A) {K.Class [\]} = ?\ ` A" + by (simp add: Int_absorb1 Int_commute h\Asub) + have h\sumB: "GK.sumset (?\ ` B) {K.Class [\]} = ?\ ` B" + by (simp add: Int_absorb1 Int_commute h\Bsub) + have "card (G.sumset A ?K) + card (G.sumset B ?K) - card ?K = + card ?K * (card (?\ ` A) + card (?\ ` B) - 1)" + using hAK hBK add_mult_distrib2 diff_mult_distrib2 nat_mult_1_right by presburger + also have "... \ card ?K * card (GK.sumset (?\ ` A) (?\ ` B))" + using hind\ h\sumA h\sumB by simp + finally show ?thesis by (simp add: hGKsumset hsumK) + qed + qed + qed + thus ?thesis using assms hAne hBne additive_abelian_group_axioms by blast +qed + +subsection\Strict version of Kneser's Theorem\ + +text\We show a strict version of Kneser's Theorem as presented in Theorem 3.2 of \cite{Ruzsa_book}.\ + +theorem Kneser_strict_aux: fixes A and B assumes hAG: "A \ G" and hBG: "B \ G" and hA: "finite A" + and hB: "finite B" and hAne: "A \ {}" and hBne: "B \ {}" and + hineq: "card (sumset A B) > card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))" + shows "card (sumset A B) \ card A + card B" + +proof- + let ?H = "stabilizer (sumset A B)" + have hfin: "finite ?H" using stabilizer_subset_group stabilizer_finite sumset_subset_carrier + finite_sumset assms sumset_is_empty_iff sumset_stabilizer_eq_self by metis + have "card ?H dvd card (sumset A B)" and "card ?H dvd (card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card ?H)" + using card_stabilizer_divide_sumset hAG hBG card_stabilizer_sumset_divide_sumset by auto + then have "card (sumset A B) \ card (sumset A ?H) + card (sumset B ?H)" using hineq + by (metis diff_le_mono2 dvd_add_right_iff dvd_imp_le le_diff_conv less_imp_add_positive) + moreover have "card A + card B \ card (sumset A ?H) + card (sumset B ?H)" + using card_le_sumset sumset_commute assms stabilizer_subset_group stabilizer_is_nonempty + Int_emptyI inf.orderE add_mono hfin by metis + ultimately show ?thesis by linarith +qed + + +theorem Kneser_strict: fixes A and B assumes "A \ G" and "B\ G" and "finite A" and "finite B" + and "stabilizer (sumset A B) = H" and "A \ {}" and "B \ {}" and " card (sumset A B) < card A + card B" + shows "card (sumset A B) = card (sumset A (stabilizer (sumset A B))) + + card (sumset B (stabilizer (sumset A B))) - card (stabilizer (sumset A B))" + using Kneser Kneser_strict_aux assms le_antisym nat_less_le by metis + +subsection\The Cauchy–Davenport Theorem\ + +text\We show the Cauchy–Davenport Theorem as a corollary of Kneser's Theorem, following a comment on + Theorem 3.2 in \cite{Ruzsa_book}.\ + + +interpretation Z_p: additive_abelian_group "{0..int ((p :: nat)-1)}" "(\ x y. ((x + y) mod int p))" "0::int" + using additive_abelian_group_def residue_group[of "p"] by fastforce + +theorem Cauchy_Davenport: + fixes p :: nat + assumes "prime p" and "A \ {}" and "B \ {}" and "finite A" and "finite B" and + "A \ {0..p-1}" and "B \ {0..p-1}" + shows "card (Z_p.sumset p A B) \ Min {p, card A + card B -1}" + +proof(cases "Z_p.stabilizer p (Z_p.sumset p A B) = {0}") + case True + moreover have "Z_p.sumset p A {0} = A" and "Z_p.sumset p B {0} = B" using assms Z_p.sumset_D(1) by auto + ultimately show ?thesis using Z_p.Kneser[of "A" "p" "B"] assms by fastforce +next + case hne: False + let ?H = "Z_p.stabilizer p (Z_p.sumset p A B)" + have "?H = {0..int(p-1)}" using hne Z_p.stabilizer_is_subgroup[of "p" "Z_p.sumset p A B"] + residue_group_simple[OF assms(1)] by blast + moreover have "p \ 2" using assms(1) by (simp add: prime_ge_2_nat) + ultimately have "card ?H = p" using card_atLeastAtMost by (simp add: of_nat_diff) + then have "p \ card (Z_p.sumset p A B)" + using Z_p.card_stabilizer_le card_0_eq assms Z_p.card_sumset_0_iff Z_p.sumset.cases + Z_p.sumset_subset_carrier Z_p.finite_sumset by metis + then show ?thesis by auto +qed + + +end +end diff --git a/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_preliminaries.thy b/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_preliminaries.thy new file mode 100644 --- /dev/null +++ b/thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_preliminaries.thy @@ -0,0 +1,1387 @@ +section\Preliminaries\ + +(* + Session: Kneser_Cauchy_Davenport + Title: Kneser_Cauchy_Davenport_preliminaries.thy + Authors: Mantas Bakšys and Angeliki Koutsoukou-Argyraki + Affiliation: University of Cambridge + Date: September 2022. +*) + + +theory Kneser_Cauchy_Davenport_preliminaries + imports + Complex_Main + "Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality" + "HOL-Number_Theory.Prime_Powers" + +begin + +context subgroup_of_group + +begin + +interpretation left: left_translations_of_group .. +interpretation right: right_translations_of_group .. + + +interpretation transformation_group "left.translation ` H" G .. + +lemma Right_Coset_eq_iff: + assumes "x \ G" and "y \ G" + shows "H |\ x = (H |\ y) \ H |\ x \ (H |\ y) \ {}" + using assms Right_Coset_is_orbit + by (metis Int_absorb orbit.disjoint orbit.natural.map_closed orbit.non_vacuous) + +end + +context additive_abelian_group + + +begin + + +subsection\Elementary lemmas on sumsets \ (*this subsection can be moved to + Pluennecke_Ruzsa_Inequality. *) + +lemma sumset_translate_eq_right: + assumes "A \ G" and "B \ G" and "x \ G" + shows "(sumset A {x} = sumset B {x}) \ A = B" using assms + by (smt (verit, best) Diff_Int_distrib2 Diff_eq_empty_iff + Int_Un_eq(1) Int_absorb2 Un_Diff_cancel2 Un_commute insert_disjoint(2) +subset_refl sumset_is_empty_iff sumsetdiff_sing) + +lemma sumset_translate_eq_left: + assumes "A \ G" and "B \ G" and "x \ G" + shows " (sumset {x} A = sumset {x} B) \ A = B" using assms + by (simp add: sumset_commute sumset_translate_eq_right) + +lemma differenceset_translate_eq_right: + assumes "A \ G" and "B \ G" and "x \ G" + shows "(differenceset A {x} = differenceset B {x}) \ A = B" using assms + by (metis Int_absorb2 differenceset_commute minus_minusset minusset_subset_carrier + sumset_translate_eq_left) + +lemma differenceset_translate_eq_left: + assumes "A \ G" and "B \ G" and "x \ G" + shows "(differenceset {x} A = differenceset {x} B) \ A = B" using assms + by (metis differenceset_commute differenceset_translate_eq_right) + +lemma sumset_inter_union_subset: + "sumset (A \ B) (A \ B) \ sumset A B" + by (metis Int_Diff_Un Int_Un_eq(2) Un_subset_iff sumset_commute sumset_subset_Un(2) + sumset_subset_Un2) + +lemma differenceset_group_eq: + "G = differenceset G G" + using equalityE minusset_eq minusset_triv subset_antisym sumset_D(1) sumset_subset_carrier + sumset_mono image_mono Int_absorb by metis + +lemma card_sumset_singleton_subset_eq: + assumes "a \ G" and "A \ G" + shows "card (sumset {a} A) = card A" + using assms card_sumset_singleton_eq card.infinite card_sumset_0_iff' le_iff_inf sumset_commute + by metis + +lemma card_differenceset_singleton_mem_eq: + assumes "a \ G" and "A \ G" + shows "card A = card (differenceset A {a})" + using assms by (metis card_minusset' card_sumset_singleton_subset_eq differenceset_commute + minusset_subset_carrier) + +lemma card_singleton_differenceset_eq: + assumes "a \ G" and "A \ G" + shows "card A = card (differenceset {a} A)" + using assms by (metis card_minusset' card_sumset_singleton_subset_eq minusset_subset_carrier) + +lemma sumset_eq_Union_left: + assumes "A \ G" + shows "sumset A B = (\ a \ A. sumset {a} B)" +proof + show "sumset A B \ (\ a \ A. sumset {a} B)" + using assms sumset.cases Int_absorb2 Int_iff UN_iff singletonI sumset.sumsetI + by (smt (verit, del_insts) subsetI) + next + show "(\ a \ A. sumset {a} B) \ sumset A B" + using sumset by auto + qed + +lemma sumset_eq_Union_right: + assumes "B \ G" + shows "sumset A B = (\ b \ B. sumset A {b})" + using assms sumset_commute sumset_eq_Union_left by (metis (no_types, lifting) Sup.SUP_cong) + + +lemma sumset_singletons_eq: + assumes "a \ G" and "b \ G" + shows "sumset {a} {b} = {a \ b}" + using assms sumset.simps subset_antisym by auto + +lemma sumset_eq_subset_differenceset: + assumes "K \ G" and "K \ {}" and "A \ G" and "sumset A K = sumset B K" + shows "A \ differenceset (sumset B K) K" +proof + fix a assume ha: "a \ A" + obtain k where hk: "k \ K" using assms(2) by blast + then have "a \ k \ sumset B K" using assms sumset.sumsetI ha by blast + then have "a \ (k \ k) \ differenceset (sumset B K) K" using hk assms ha minusset.minussetI + subset_iff sumset.sumsetI by (smt (verit) associative composition_closed inverse_closed) + then show "a \ differenceset (sumset B K) K" using hk ha subsetD assms right_unit + by (metis invertible invertible_right_inverse) +qed + +end + +locale subgroup_of_additive_abelian_group = + subgroup_of_abelian_group H G "(\)" \ + additive_abelian_group G "(\)" \ + for H G and addition (infixl "\" 65) and zero ("\") + +begin + +notation Left_Coset (infixl "\|" 70) + +lemma Left_Coset_eq_sumset: + assumes "x \ G" + shows "sumset {x} H = x \| H" + using assms Left_Coset_memI sumset.simps by fastforce + +lemma sumset_subgroup_eq_iff: + assumes "a \ G" and "b \ G" + shows "sumset {a} H = sumset {b} H \ + (sumset {a} H) \ (sumset {b} H) \ {}" + using Right_Coset_eq_iff assms Left_Coset_eq_sumset Left_equals_Right_coset by presburger + +lemma card_divide_sumset: + assumes "A \ G" + shows "card H dvd card (sumset A H)" +proof(cases "finite H \ finite A") + case hfin: True + then have hfinsum: "\ X. X \ ((\ a. sumset {a} H) ` A) \ finite X" + using finite_sumset by force + moreover have "pairwise disjnt ((\ a. sumset {a} H) ` A)" + using pairwise_imageI disjnt_def sumset_subgroup_eq_iff subset_eq assms by (smt (verit, best)) + moreover have "card H dvd sum card ((\ a. sumset {a} H) ` A)" + proof(intro dvd_sum) + fix X assume "X \ (\ a. sumset {a} H) ` A" + then show "card H dvd card X" using dvd_refl + using Left_equals_Right_coset Right_Coset_cardinality assms Left_Coset_eq_sumset by auto + qed + ultimately show ?thesis using assms sumset_eq_Union_left card_Union_disjoint by metis +next + case False + then show ?thesis using assms card_sumset_0_iff by (metis card_eq_0_iff dvd_0_right sub subsetI) +qed + +lemma sumset_subgroup_eq_Class_Union: + assumes "A \ G" + shows "sumset A H = (\ (Class ` A))" +proof + show "sumset A H \ \ (Class ` A)" + proof + fix x assume "x \ sumset A H" + then obtain a b where ha: "a \ A" and "b \ H" and "x = a \ b" + using sumset.cases by blast + then have "x \ Class a" using Left_Coset_Class_unit Left_Coset_eq_sumset assms by blast + thus "x \ \ (Class ` A)" using ha by blast + qed +next + show "\ (Class ` A) \ sumset A H" + proof(intro Union_least) + fix X assume "X \ Class ` A" + then obtain a where "a \ A" and "X = Class a" by blast + moreover hence "{a} \ A" by auto + ultimately show "X \ sumset A H" using Left_Coset_Class_unit + Left_Coset_eq_sumset assms sumset_mono subset_refl in_mono by metis + qed +qed + +lemma Class_image_sumset_subgroup_eq: + assumes "A \ G" + shows "Class ` (sumset A H) = Class ` A" +proof + show "Class ` sumset A H \ Class ` A" + proof + fix x assume "x \ Class ` sumset A H" + then obtain c where hc: "c \ sumset A H" and "x = Class c" by blast + moreover obtain a b where ha: "a \ A" and "b \ H" and "c = a \ b" using hc sumset.cases + by blast + ultimately show "x \ Class ` A" using ha Class_eq CongruenceI assms composition_closed + sumset.cases Partition_def commutative image_eqI left_unit sub unit_closed + by (smt (verit, ccfv_threshold) Block_self Class_cong Normal_def) + qed +next + show "Class ` A \ Class ` sumset A H" using assms right_unit subsetD subsetI sumset.sumsetI + unit_closed by (smt (verit, del_insts) image_subset_iff sub_unit_closed) +qed + +lemma Class_cover_imp_subset_or_disj: + assumes "A = (\ (Class ` C))" and "x \ G" and "C \ G" + shows "Class x \ A \ Class x \ A = {}" +proof(intro disjCI) + assume "Class x \ A \ {}" + then obtain c where "c \ C" and "Class x \ Class c \ {}" using assms by blast + then show "Class x \ A" using assms not_disjoint_implies_equal Sup_upper imageI subset_iff + by blast +qed + +end + +context additive_abelian_group + +begin + +subsection\Stabilizer and basic properties\ + + +text\We define the stabilizer or group of periods of a nonempty subset of an abelian group.\ + +definition stabilizer::"'a set \ 'a set " where +"stabilizer S \ {x \ G. sumset {x} (S \ G) = S \ G}" + +lemma stabilizer_is_subgroup: fixes S :: "'a set" + shows "subgroup (stabilizer S) G (\) (\)" +proof (intro subgroupI) + show "stabilizer S \ G" using stabilizer_def by auto +next + show "\ \ stabilizer S" using stabilizer_def by (simp add: Int_absorb1 Int_commute) +next + fix a b assume haS: "a \ stabilizer S" and hbS: "b \ stabilizer S" + then have haG: "a \ G" and hbG: "b \ G" using stabilizer_def by auto + have "sumset {a \ b} (S \ G) = sumset {a} (sumset {b} (S \ G))" + proof + show "sumset {a \ b} (S \ G) \ sumset {a} (sumset {b} (S \ G))" using haG hbG + empty_subsetI insert_subset subsetI sumset.simps sumset_assoc sumset_mono + by metis + show "sumset {a} (sumset {b} (S \ G)) \ sumset {a \ b} (S \ G)" + using empty_iff insert_iff sumset.simps sumset_assoc by (smt (verit, best) subsetI) + qed + then show "a \ b \ stabilizer S" using haS hbS stabilizer_def by auto +next + fix g assume "g \ stabilizer S" + thus "invertible g" using stabilizer_def by auto +next + fix g assume hgS: "g \ stabilizer S" + then have hinvsum : "inverse g \ g = \" using stabilizer_def by simp + have "sumset {inverse g} (sumset {g} (S \ G)) = (S \ G)" + proof + show "sumset {inverse g} (sumset {g} (S \ G)) \ (S \ G)" using + empty_iff insert_iff sumset.simps sumset_assoc subsetI left_unit hinvsum + by (smt (verit, ccfv_threshold)) + show "(S \ G) \ sumset {inverse g} (sumset {g} (S \ G))" + proof + fix s assume hs: "s \ (S \ G)" + then have "inverse g \ g \ s \ sumset {inverse g} (sumset {g} (S \ G))" using + hgS stabilizer_def additive_abelian_group.sumset.sumsetI + additive_abelian_group_axioms associative in_mono inverse_closed mem_Collect_eq singletonI + by (smt (z3) IntD2) + thus "s \ sumset {inverse g} (sumset {g} (S \ G))" using hinvsum hs + by simp + qed + qed + thus "inverse g \ stabilizer S" using hgS stabilizer_def by auto +qed + +interpretation subgroup_of_additive_abelian_group "stabilizer A" "G" "(\)" "\" + using stabilizer_is_subgroup subgroup_of_abelian_group_def + by (metis abelian_group_axioms additive_abelian_group_axioms group_axioms + subgroup_of_additive_abelian_group_def subgroup_of_group_def) + +lemma zero_mem_stabilizer: "\ \ stabilizer A" .. + +lemma stabilizer_is_nonempty: + shows "stabilizer S \ {}" + using sub_unit_closed by blast + +lemma Left_Coset_eq_sumset_stabilizer: + assumes "x \ G" + shows "sumset {x} (stabilizer B) = x \| (stabilizer B)" + by (simp add: Left_Coset_eq_sumset assms) + +lemma stabilizer_subset_difference_singleton: + assumes "S \ G" and "s \ S" + shows "stabilizer S \ differenceset S {s}" +proof + fix x assume hx: "x \ stabilizer S" + then obtain t where ht: "t \ S" and "x \ s = t" using assms stabilizer_def by blast + then have "x = t \ s" using hx stabilizer_def assms associative + by (metis (no_types, lifting) in_mono inverse_closed invertible invertible_right_inverse sub + sub.right_unit) + thus "x \ differenceset S {s}" using ht assms + by (simp add: minusset.minussetI subsetD sumset.sumsetI) +qed + +lemma stabilizer_subset_singleton_difference: + assumes "S \ G" and "s \ S" + shows "stabilizer S \ differenceset {s} S" +proof- + have "stabilizer S \ minusset (stabilizer S)" using assms Int_absorb2 minusset_eq + subgroup.image_of_inverse submonoid.sub subset_eq + by (smt (verit) stabilizer_is_subgroup stabilizer_subset_difference_singleton + sumset_subset_carrier) + moreover have "minusset (stabilizer S) \ minusset (differenceset S {s})" + proof + fix x assume hx1: "x \ minusset (stabilizer S)" + then have hx: "inverse x \ stabilizer S" + by (metis invertible invertible_inverse_inverse minusset.cases) + then obtain t where ht: "t \ S" and "inverse x \ s = t" using assms stabilizer_def by blast + then have hx2: "inverse x = t \ s" using hx stabilizer_def assms + by (smt (verit, ccfv_threshold) commutative in_mono inverse_closed invertible + invertible_left_inverse2 sub) + thus "x \ minusset (differenceset S {s})" using ht assms + by (smt (verit, best) hx1 additive_abelian_group.sumset.sumsetI additive_abelian_group_axioms + inverse_closed invertible invertible_inverse_inverse minusset.cases minusset.minussetI + singletonI subset_iff) + qed + ultimately show ?thesis using differenceset_commute assms by blast +qed + +lemma stabilizer_subset_nempty: + assumes "S \ {}" and "S \ G" + shows "stabilizer S \ differenceset S S" +proof + fix x assume hx: "x \ stabilizer S" + then obtain s where hs: "s \ S \ G" using assms by blast + then have "x \ s \ S \ G" using stabilizer_def assms hx mem_Collect_eq singletonI + sumset.sumsetI sumset_Int_carrier by blast + then obtain t where ht: "t \ S" and "x \ s = t" by blast + then have "x = t \ s" using hx stabilizer_def assms(2) hs ht associative + by (metis IntD2 inverse_closed invertible invertible_right_inverse sub sub.right_unit) + thus "x \ differenceset S S" using ht hs using assms(2) by blast +qed + +lemma stabilizer_coset_subset: + assumes "A \ G" and "x \ A" + shows "sumset {x} (stabilizer A) \ A" +proof + fix y assume "y \ sumset {x} (stabilizer A)" + moreover hence "stabilizer A \ differenceset A {x}" using assms + stabilizer_subset_difference_singleton by auto + moreover have "sumset {x} (differenceset A {x}) \ A" + proof + fix z assume "z \ sumset {x} (differenceset A {x})" + then obtain a where "a \ A" and "z = x \ (a \ x)" + using additive_abelian_group.sumset.cases additive_abelian_group_axioms singletonD + minusset.cases assms subsetD by (smt (verit, ccfv_SIG)) + thus "z \ A" using assms + by (metis additive_abelian_group.inverse_closed additive_abelian_group_axioms + commutative in_mono invertible invertible_right_inverse2) + qed + ultimately show "y \ A" by (meson in_mono subset_singleton_iff sumset_mono) + qed + +lemma stabilizer_subset_stabilizer_dvd: + assumes "stabilizer A \ stabilizer B" + shows "card (stabilizer A) dvd card (stabilizer B)" +proof(cases "finite (stabilizer B)") + case hB: True + interpret H: subgroup_of_group "stabilizer A" "stabilizer B" "(\)" "\" + proof(unfold_locales) + show "stabilizer A \ stabilizer B" using assms by blast + next + show "\a b. a \ stabilizer A \ b \ stabilizer A \ a \ b \ stabilizer A" + using stabilizer_is_subgroup group_axioms by simp + next + show "\ \ stabilizer A" using sub_unit_closed by blast + qed + show ?thesis using H.lagrange hB by auto +next + case False + then show ?thesis by simp +qed + +lemma stabilizer_coset_Un: + assumes "A \ G" + shows "(\ x \ A. sumset {x} (stabilizer A)) = A" +proof + show "(\x\A. sumset {x} (stabilizer A)) \ A" + using stabilizer_coset_subset assms by blast +next + show "A \ (\x\A. sumset {x} (stabilizer A))" + proof + fix x assume hx: "x \ A" + then have "x \ sumset {x} (stabilizer A)" using sub_unit_closed assms + by (metis in_mono right_unit singletonI sumset.sumsetI unit_closed) + thus "x \ (\x\A. sumset {x} (stabilizer A))" using hx by blast + qed +qed + +lemma stabilizer_empty: "stabilizer {} = G" + using sumset_empty Int_empty_left stabilizer_def subset_antisym + by (smt (verit, best) mem_Collect_eq subsetI sumset_Int_carrier_eq(1) sumset_commute) + +lemma stabilizer_finite: + assumes "S \ G" and "S \ {}" and "finite S" + shows "finite (stabilizer S)" + using stabilizer_subset_nempty assms + by (meson finite_minusset finite_sumset rev_finite_subset) + +lemma stabilizer_subset_group: + shows "stabilizer S \ G" using stabilizer_def by blast + +lemma sumset_stabilizer_eq_iff: + assumes "a \ G" and "b \ G" + shows "sumset {a} (stabilizer A) = sumset {b} (stabilizer A) \ + (sumset {a} (stabilizer A)) \ (sumset {b} (stabilizer A)) \ {}" + by (simp add: assms sumset_subgroup_eq_iff) + +lemma sumset_stabilizer_eq_Class_Union: + assumes "A \ G" + shows "sumset A (stabilizer B) = (\ (Class B ` A))" + by (simp add: assms sumset_subgroup_eq_Class_Union) + +lemma card_stabilizer_divide_sumset: + assumes "A \ G" + shows "card (stabilizer B) dvd card (sumset A (stabilizer B))" + by (simp add: assms card_divide_sumset) + +lemma Class_image_sumset_stabilizer_eq: + assumes "A \ G" + shows "Class B ` (sumset A (stabilizer B)) = Class B ` A" + by (simp add: Class_image_sumset_subgroup_eq assms) + +lemma Class_cover_imp_subset_or_disj: + assumes "A = (\ (Class B ` C))" and "x \ G" and "C \ G" + shows "Class B x \ A \ Class B x \ A = {}" + by (simp add: Class_cover_imp_subset_or_disj assms) + +lemma stabilizer_sumset_disjoint: + fixes S1 S2 :: "'a set" + assumes "stabilizer S1 \ stabilizer S2 = {\}" and "S1 \ G" and "S2 \ G" + and "finite S1" and "finite S2" and "S1 \ {}" and "S2 \ {}" + shows "card (sumset (stabilizer S1) (stabilizer S2)) = + card (stabilizer S1) * card (stabilizer S2)" +proof- + have inj_on : "inj_on (\ (a, b). a \ b) (stabilizer S1 \ stabilizer S2)" + proof(intro inj_onI) + fix x y assume "x \ stabilizer S1 \ stabilizer S2" and "y \ stabilizer S1 \ stabilizer S2" and + "(case x of (a, b) \ a \ b) = (case y of (a, b) \ a \ b)" + then obtain a b c d where hx: "x = (a, b)" and hy: "y = (c, d)" and ha: "a \ stabilizer S1" and + hb: "b \ stabilizer S2" and hc: "c \ stabilizer S1" and hd: "d \ stabilizer S2" and + habcd: "a \ b = c \ d" by auto + then have haG: "a \ G" using stabilizer_def by blast + have hbG: "b \ G" using hb stabilizer_def by blast + have hcG: "c \ G" using hc stabilizer_def by blast + have hdG: "d \ G" using hd stabilizer_def by blast + then have "a \ c = d \ b" using habcd haG hbG hcG hdG + by (metis (full_types) associative commutative composition_closed inverse_equality invertible + invertible_def invertible_left_inverse2) + moreover have "a \ c \ stabilizer S1" using ha hc stabilizer_is_subgroup + subgroup.axioms(1) submonoid.sub_composition_closed + by (metis group.invertible group_axioms hcG subgroup.subgroup_inverse_iff) + moreover have "d \ b \ stabilizer S2" using hd hb stabilizer_is_subgroup + subgroup.axioms(1) submonoid.sub_composition_closed + by (metis group.invertible group_axioms hbG subgroup.subgroup_inverse_iff) + ultimately have "a \ c = \" and "d \ b = \" using assms(1) by auto + thus "x = y" using hx hy haG hbG hcG hdG + by (metis inverse_closed invertible invertible_right_cancel invertible_right_inverse) + qed + moreover have himage : "(\ (a, b). a \ b) ` (stabilizer S1 \ stabilizer S2) = + sumset (stabilizer S1) (stabilizer S2)" + proof + show "(\(a, b). a \ b) ` (stabilizer S1 \ stabilizer S2) \ sumset (stabilizer S1) (stabilizer S2)" + using stabilizer_subset_group by force + + next + show "sumset (stabilizer S1) (stabilizer S2) \ (\(a, b). a \ b) ` (stabilizer S1 \ stabilizer S2)" + proof + fix x assume "x \ sumset (stabilizer S1) (stabilizer S2)" + then obtain s1 s2 where hs1: "s1 \ stabilizer S1" and hs2: "s2 \ stabilizer S2" and + "x = s1 \ s2" by (meson sumset.cases) + thus "x \ (\(a, b). a \ b) ` (stabilizer S1 \ stabilizer S2)" using hs1 hs2 by auto + qed + qed + ultimately show ?thesis using card_image card_cartesian_product by fastforce +qed + +lemma stabilizer_sub_sumset_left: + "stabilizer A \ stabilizer (sumset A B)" +proof + fix x assume hx: "x \ stabilizer A" + then have "sumset {x} (sumset A B) = sumset A B" using stabilizer_def sumset_assoc + mem_Collect_eq by (smt (verit, del_insts) sumset_Int_carrier_eq(1) sumset_commute) + thus "x \ stabilizer (sumset A B)" using hx stabilizer_def + by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier) +qed + +lemma stabilizer_sub_sumset_right: + "stabilizer B \ stabilizer (sumset A B)" + using stabilizer_sub_sumset_left sumset_commute by fastforce + +lemma not_mem_stabilizer_obtain: + assumes "A \ {}" and "x \ stabilizer A" and "x \ G" and "A \ G" and "finite A" + obtains a where "a \ A" and "x \ a \ A" +proof- + have "sumset {x} A \ A" using assms stabilizer_def + by (metis (mono_tags, lifting) inf.orderE mem_Collect_eq) + moreover have "card (sumset {x} A) = card A" using assms + by (metis card_sumset_singleton_eq inf.orderE sumset_commute) + ultimately obtain y where "y \ sumset {x} A" and "y \ A" using assms + by (meson card_subset_eq subsetI) + then obtain a where "a \ A" and "x \ a \ A" using assms + by (metis singletonD sumset.cases) + thus ?thesis using that by blast +qed + +lemma sumset_eq_sub_stabilizer: + assumes "A \ G" and "B \ G" and "finite B" + shows "sumset A B = B \ A \ stabilizer B" +proof + fix x assume hsum: "sumset A B = B" and hx: "x \ A" + have "sumset {x} B = B" + proof- + have "sumset {x} B \ B" using hsum hx + by (metis empty_subsetI equalityE insert_subset sumset_mono) + moreover have "card (sumset {x} B) = card B" using assms + by (metis IntD1 Int_absorb1 card_sumset_singleton_eq hx inf_commute sumset_commute) + ultimately show ?thesis using card_subset_eq assms(3) by auto + qed + thus "x \ stabilizer B" using hx assms(1) stabilizer_def + by (metis (mono_tags, lifting) assms(2) inf.orderE mem_Collect_eq subsetD) +qed + + +lemma sumset_stabilizer_eq: + shows "sumset (stabilizer A) (stabilizer A) = stabilizer A" +proof + show "sumset (stabilizer A) (stabilizer A) \ stabilizer A" + using stabilizer_is_subgroup subgroup.axioms(1) subsetI + by (metis (mono_tags, lifting) additive_abelian_group.sumset.simps additive_abelian_group_axioms + submonoid.sub_composition_closed) +next + show "stabilizer A \ sumset (stabilizer A) (stabilizer A)" + using Left_Coset_eq_sumset stabilizer_is_nonempty + stabilizer_subset_group sub_unit_closed additive_abelian_group_axioms right_unit + subset_iff sumsetI by (smt (verit, best)) +qed + + +lemma differenceset_stabilizer_eq: + shows "differenceset (stabilizer A) (stabilizer A) = stabilizer A" +proof + show "differenceset (stabilizer A) (stabilizer A) \ stabilizer A" + proof + fix x assume "x \ differenceset (stabilizer A) (stabilizer A)" + then obtain a b where "a \ stabilizer A" and "b \ stabilizer A" and "x = a \ b" + by (metis minusset.cases sumset.cases) + thus "x \ stabilizer A" using stabilizer_is_subgroup subgroup.axioms(1) + by (smt (verit, ccfv_threshold) in_mono invertible stabilizer_subset_group + subgroup_inverse_iff sub_composition_closed) + qed +next + show "stabilizer A \ differenceset (stabilizer A) (stabilizer A)" + proof + fix x assume hx: "x \ stabilizer A" + then have "x \ \ \ differenceset (stabilizer A) (stabilizer A)" by blast + then show "x \ differenceset (stabilizer A) (stabilizer A)" using hx by simp + qed +qed + +lemma stabilizer2_sub_stabilizer: + shows "stabilizer(stabilizer A) \ stabilizer A" +proof(cases "A \ {}") + case True + then have "stabilizer(stabilizer A) \ differenceset (stabilizer A) (stabilizer A)" + by (simp add: stabilizer_is_nonempty stabilizer_subset_group stabilizer_subset_nempty) + thus ?thesis using differenceset_stabilizer_eq by blast +next + case False + then show ?thesis by (simp add: stabilizer_empty stabilizer_subset_group) +qed + +lemma stabilizer_left_sumset_invariant: + assumes "a \ G" and "A \ G" + shows "stabilizer (sumset {a} A) = stabilizer A" + +proof + show "stabilizer (sumset {a} A) \ stabilizer A" + proof + fix x assume hx: "x \ stabilizer (sumset {a} A)" + then have hxG: "x \ G" using stabilizer_def by blast + have "sumset {x} (sumset {a} A) = sumset {a} A" using stabilizer_def hx + by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier) + then have "sumset {x} A = A" using assms + by (metis (full_types) sumset_assoc sumset_commute sumset_subset_carrier + sumset_translate_eq_right) + thus "x \ stabilizer A" using hxG stabilizer_def + by (metis (mono_tags, lifting) mem_Collect_eq sumset_Int_carrier) + qed +next + show "stabilizer A \ stabilizer (sumset {a} A)" using stabilizer_def + using stabilizer_sub_sumset_right by meson +qed + +lemma stabilizer_right_sumset_invariant: + assumes "a \ G" and "A \ G" + shows "stabilizer (sumset A {a}) = stabilizer A" + using sumset_commute stabilizer_left_sumset_invariant assms by simp + +lemma stabilizer_right_differenceset_invariant: + assumes "b \ G" and "A \ G" + shows "stabilizer (differenceset A {b}) = stabilizer A" + using assms minusset_eq stabilizer_right_sumset_invariant by auto + +lemma stabilizer_unchanged: + assumes "a \ G" and "b \ G" + shows "stabilizer (sumset A B) = stabilizer (sumset A (sumset (differenceset B {b}) {a}))" + +proof- + have "sumset A (sumset (differenceset B {b}) {a}) = sumset (differenceset (sumset A B) {b}) {a}" + by (simp add: sumset_assoc) + thus ?thesis using stabilizer_right_sumset_invariant + stabilizer_right_differenceset_invariant assms sumset_subset_carrier by simp +qed + + +lemma subset_stabilizer_of_subset_sumset: + assumes "A \ sumset {x} (stabilizer B)" and "x \ G" and "A \ {}" and "A \ G" + shows "stabilizer A \ stabilizer B" +proof- + obtain a where ha: "a \ A" using assms by blast + moreover then obtain b where hb: "b \ stabilizer B" and haxb: "a = x \ b" using sumset.cases assms by blast + ultimately have "stabilizer A \ differenceset A {a}" using assms sumset_subset_carrier + stabilizer_subset_difference_singleton by (meson subset_trans) + also have "... = sumset {inverse a} A" using sumset_commute ha assms(4) inverse_closed + subsetD minusset_eq by auto + also have "... \ sumset {inverse x \ inverse b} (sumset {x} (stabilizer B))" + using assms sumset_mono haxb inverse_closed hb stabilizer_subset_group subsetD + commutative inverse_composition_commute by (metis invertible subset_singleton_iff) + also have "... = sumset {inverse b} (stabilizer B)" using sumset_singletons_eq commutative + assms sumset_assoc hb stabilizer_subset_group inverse_closed invertible + by (metis composition_closed invertible_right_inverse2 sub) + also have "... = stabilizer B" using hb Left_Coset_eq_sumset sub_unit_closed sub subset_iff + additive_abelian_group_axioms calculation disjoint_iff_not_equal factor_unit inverse_closed + sumset_subgroup_eq_iff by (smt (verit, del_insts)) + finally show ?thesis . +qed + +lemma sumset_stabilizer_eq_self: + assumes "A \ G" + shows "sumset (stabilizer A) A = A" + using assms sumset_eq_Union_left[OF "stabilizer_subset_group"] + Int_absorb2 stabilizer_coset_Un sumset_commute sumset_eq_Union_left by presburger + +lemma stabilizer_neq_subset_sumset: + assumes "A \ sumset {x} (stabilizer B)" and "x \ A" and "\ sumset {x} (stabilizer B) \ C" and + "A \ C" and "C \ G" + shows "stabilizer A \ stabilizer B" +proof + assume heq: "stabilizer A = stabilizer B" + obtain a where "a \ sumset {x} (stabilizer B)" and + "a \ C" using assms by blast + moreover then obtain b where "b \ stabilizer B" and "a = x \ b" using sumset.cases by blast + ultimately have "b \ x \ A" using commutative stabilizer_subset_group assms in_mono by metis + thus False using assms heq stabilizer_coset_subset subset_trans by metis +qed + +lemma subset_stabilizer_Un: + shows "stabilizer A \ stabilizer B \ stabilizer (A \ B)" +proof + fix x assume hx: "x \ stabilizer A \ stabilizer B" + then have "sumset {x} (A \ G) = A \ G" using stabilizer_def by blast + moreover have "sumset {x} (B \ G) = (B \ G)" using stabilizer_def hx by blast + ultimately have "sumset {x} ((A \ B) \ G) = (A \ B) \ G" using sumset_subset_Un2 + boolean_algebra.conj_disj_distrib2 by auto + then show "x \ stabilizer (A \ B)" using hx stabilizer_subset_group stabilizer_def by blast +qed + +lemma mem_stabilizer_Un_and_left_imp_right: + assumes "finite B" and "x \ stabilizer (A \ B)" and "x \ stabilizer A" and "disjnt A B" + shows "x \ stabilizer B" +proof- + have "(A \ G) \ sumset {x} (B \ G) = (A \ G) \ (B \ G)" + using assms(2) sumset_subset_Un2[of "{x}" "A \ G" "B \ G"] stabilizer_def[of "A \ B"] + Int_Un_distrib2[of "A" "B" "G"] assms(3) stabilizer_def + by (metis (mono_tags, lifting) mem_Collect_eq) + then have "B \ G \ sumset {x} (B \ G)" using assms(4) disjnt_def Int_Un_distrib2 Int_commute + sumset_subset_Un1 by (smt (verit, del_insts) Int_assoc Un_Int_eq(2) inf.orderI insert_is_Un + sumset_empty(2)) + then show "x \ stabilizer B" using stabilizer_def[of "B"] assms(1) assms(3) card_subset_eq + card_sumset_singleton_subset_eq finite.emptyI finite.insertI finite_Int finite_sumset + inf.cobounded2 stabilizer_subset_group subsetD by (smt (verit) mem_Collect_eq) +qed + +lemma mem_stabilizer_Un_and_right_imp_left: + assumes "finite A" and "x \ stabilizer (A \ B)" and "x \ stabilizer B" and "disjnt A B" + shows "x \ stabilizer A" + using mem_stabilizer_Un_and_left_imp_right Un_commute assms disjnt_sym by metis + +lemma Union_stabilizer_Class_eq: + assumes "A \ G" + shows "A = (\ (Class A ` A))" using assms sumset_commute sumset_subgroup_eq_Class_Union + sumset_stabilizer_eq_self by presburger + +lemma card_stabilizer_sumset_divide_sumset: + "card (stabilizer (sumset A B)) dvd card (sumset A B)" using card_divide_sumset + sumset_commute sumset_stabilizer_eq_self sumset_subset_carrier by metis + +lemma card_stabilizer_le: + assumes "A \ G" and "finite A" and "A \ {}" + shows "card (stabilizer A) \ card A" using assms + by (metis card_le_sumset finite.cases insertCI insert_subset stabilizer_finite + stabilizer_subset_group sumset_commute sumset_stabilizer_eq_self) + +lemma sumset_Inter_subset_sumset: + assumes "a \ G" and "b \ G" + shows "sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C)) \ + sumset {a \ b} (stabilizer C)" (is "sumset ?A ?B \ _") +proof + fix x assume "x \ sumset ?A ?B" + then obtain d1 d2 where "d1 \ sumset {a} (stabilizer C)" and + "d2 \ sumset {b} (stabilizer C)" and "x = d1 \ d2" by (meson IntD2 sumset.cases) + then obtain c1 c2 where hc1: "c1 \ stabilizer C" and hc2: "c2 \ stabilizer C" and + "x = (a \ c1) \ (b \ c2)" using sumset.simps by auto + then have "x = (a \ b) \ (c1 \ c2)" using hc1 hc2 assms associative commutative + stabilizer_subset_group by simp + thus "x \ sumset {a \ b} (stabilizer C)" using stabilizer_is_subgroup hc1 hc2 + stabilizer_subset_group sumset.simps sumset_stabilizer_eq assms by blast +qed + +subsection\Convergent\ + +(* I manually exclude the empty set from this definition as its stabilizer is too big *) +definition convergent :: "'a set \ 'a set \ 'a set \ bool" where +"convergent C A B \ C \ sumset A B \ C \ {} \ + card C + card (stabilizer C) \ card (A \ B) + card (sumset (A \ B) (stabilizer C))" + +definition convergent_set :: "'a set \ 'a set \ 'a set set" where +"convergent_set A B = Collect (\ C. convergent C A B)" + +lemma convergent_set_sub_powerset: + "convergent_set A B \ Pow (sumset A B)" using convergent_set_def convergent_def by blast + +lemma finite_convergent_set: + assumes "finite A" and "finite B" + shows "finite (convergent_set A B)" + using convergent_set_sub_powerset finite_Pow_iff finite_sumset assms finite_subset by metis + +subsection\Technical lemmas from DeVos's proof of Kneser's Theorem\ + +text\The following lemmas correspond to intermediate arguments in the proof of Kneser's Theorem +by DeVos that we will be following \cite{DeVos_Kneser}. \ + +lemma stabilizer_sumset_psubset_stabilizer: + assumes "a \ G" and "b \ G" and "A \ sumset {a} (stabilizer C) \ {}" and + "B \ sumset {b} (stabilizer C) \ {}" and hnotsub: "\ sumset {a \ b} (stabilizer C) \ sumset A B" + shows "stabilizer (sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))) \ + stabilizer C" (is "?H \ _") +proof + have "sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C)) \ {}" + using assms by (simp add: inf_assoc) + then show "?H \ stabilizer C" + by (meson assms(1) assms(2) composition_closed subset_stabilizer_of_subset_sumset sumset_Inter_subset_sumset sumset_subset_carrier) +next + obtain c1 c2 where "a \ c1 \ A" and "b \ c2 \ B" and hc1: "c1 \ stabilizer C" and hc2: "c2 \ stabilizer C" + using assms(1, 2, 3, 4) Left_Coset_eq_sumset_stabilizer by fastforce + then have hac1mem: "(a \ c1) \ A \ sumset {a} (stabilizer C)" and hac1G: "a \ c1 \ G" and + hbc2mem: "(b \ c2) \ B \ sumset {b} (stabilizer C)" and hbc2G: "b \ c2 \ G" + by (auto simp add: assms(1, 2) sumset.sumsetI) + have "(a \ c1) \ (b \ c2) \ sumset {a \ b} (stabilizer C)" using assms hc1 hc2 + by (smt (verit) associative commutative composition_closed insertI1 sub sub_composition_closed sumset.sumsetI) + then have "sumset {a \ b} (stabilizer C) \ sumset {(a \ c1) \ (b \ c2)} (stabilizer C) \ {}" + using zero_mem_stabilizer by (smt (verit, ccfv_threshold) composition_closed + disjoint_iff_not_equal hac1G hbc2G insertCI right_unit sumset.sumsetI unit_closed) + then have hsumeq: "sumset {a \ b} (stabilizer C) = sumset {(a \ c1) \ (b \ c2)} (stabilizer C)" + using sumset_stabilizer_eq_iff assms hac1G hbc2G composition_closed by presburger + have "(sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))) \ sumset {a \ b} (stabilizer C)" + by (simp add: assms(1, 2) sumset_Inter_subset_sumset) + have hsummem: "(a \ c1) \ (b \ c2) \ sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))" + using hac1mem hbc2mem hac1G hbc2G sumset.sumsetI by blast + show "?H \ stabilizer C" + using stabilizer_neq_subset_sumset[OF _ hsummem] hnotsub hsumeq sumset_Inter_subset_sumset assms + sumset_subset_carrier composition_closed sumset_mono sumset.sumsetI zero_mem_stabilizer + inf.cobounded1 right_unit unit_closed by metis +qed + +lemma stabilizer_eq_stabilizer_union: + assumes "a \ G" and "b \ G" and"A \ sumset {a} (stabilizer C) \ {}" and + "B \ sumset {b} (stabilizer C) \ {}" and hnotsub: "\ sumset {a \ b} (stabilizer C) \ sumset A B" and + "C \ sumset A B" and "finite C" and + "C \ sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C)) = {}" and "C \ {}" and + "finite A" and "finite B" + shows "stabilizer (sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))) = + stabilizer (C \ sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C)))" (is "stabilizer ?H = stabilizer ?K") +proof + show "stabilizer ?H \ stabilizer ?K" using subset_stabilizer_Un Int_absorb1 + stabilizer_sumset_psubset_stabilizer psubset_imp_subset assms by metis +next + have hCG : "C \ G" using assms(6) sumset_subset_carrier by force + show "stabilizer ?K \ stabilizer ?H" + proof + fix x assume hxC1: "x \ stabilizer ?K" + moreover have "x \ stabilizer C" + proof- + have hC_Un: "C = (\ (Class C ` C))" using Union_stabilizer_Class_eq hCG by simp + have hCsumx: "sumset {x} C = (\ y \ Class C ` C. sumset {x} y)" + proof + show "sumset {x} C \ \ (sumset {x} ` Class C ` C)" + proof + fix y assume hy: "y \ sumset {x} C" + then obtain c where hc: "c \ C" and hyxc: "y = x \ c" using sumset.cases by blast + then obtain K where hK: "K \ Class C ` C" and "c \ K" using hC_Un by blast + then have "y \ sumset {x} K" using hyxc hc by (metis sumset.cases + sumset.sumsetI hCG hy singletonD subset_iff) + then show "y \ \ (sumset {x} ` Class C ` C)" using hK by auto + qed + next + show "\ (sumset {x} ` Class C ` C) \ sumset {x} C" + proof(intro Union_least) + fix X assume "X \ sumset {x} ` Class C ` C" + then obtain K where "K \ Class C ` C" and "X = sumset {x} K" by blast + then show "X \ sumset {x} C" using sumset_mono[of "{x}" "{x}" "K" "C"] + hC_Un subset_refl by blast + qed + qed + have "x \ stabilizer C \ False" + proof- + assume hxC: "x \ stabilizer C" + then have hxG: "x \ G" using hxC1 stabilizer_subset_group by blast + then have hxCne: "sumset {x} C \ C" using stabilizer_def[of "C"] hCG Int_absorb2 + hxC by (metis (mono_tags, lifting) mem_Collect_eq) + moreover have hxsplit: "sumset {x} C \ sumset {x} ?H = C \ ?H" + using hxC1 stabilizer_def[of "?K"] sumset_subset_carrier assms(6) sumset_subset_Un2 by force + have "sumset {x} C \ ?H \ {}" + proof + assume "sumset {x} C \ ?H = {}" + then have "sumset {x} C \ C" using hxsplit hxCne by blast + thus "False" using hCG assms(6) assms(7) hxC1 stabilizer_subset_group psubset_card_mono + by (metis card_sumset_singleton_eq sumset_Int_carrier sumset_commute + sumset_stabilizer_eq_self hxG less_irrefl_nat) + qed + then obtain c where hc: "c \ C" and + hxcne: "sumset {x} (Class C c) \ ?H \ {}" using hCsumx by blast + then have hxc: "sumset {x} (Class C c) = Class C (x \ c)" + using hxG assms(6) Left_Coset_Class_unit Left_Coset_eq_sumset_stabilizer sumset_assoc + sumset_singletons_eq composition_closed sumset.cases sumset_stabilizer_eq_self hCG by (smt (verit)) + have hClassCempty: "Class C (x \ c) \ C = {}" + proof- + have "\ Class C (x \ c) \ C" using hxc hxcne assms(8) by blast + then show ?thesis using Class_cover_imp_subset_or_disj[OF hC_Un _ hCG] + by (meson composition_closed hCG hc hxG subsetD) + qed + have "Class C (x \ c) \ sumset {x} C" using hCsumx hc hxc by blast + then have "Class C (x \ c) \ ?H" using hClassCempty hxsplit by auto + moreover have "card (Class C (x \ c)) = card (stabilizer C)" using hxG hc hCG + composition_closed Right_Coset_Class_unit Right_Coset_cardinality sumset_Int_carrier + Class_cover_imp_subset_or_disj assms by auto + ultimately have "card (stabilizer C) \ card ?H" using card_mono finite_sumset assms(10, 11) finite_Int by metis + moreover have "card ?H < card (sumset {a \ b} (stabilizer C))" + proof (intro psubset_card_mono psubsetI sumset_Inter_subset_sumset assms(1) assms(2)) + show "finite (sumset {a \ b} (stabilizer C))" + using stabilizer_finite assms finite_sumset by (simp add: hCG) + next + show "?H \ sumset {a \ b} (stabilizer C)" + using hnotsub sumset_mono by (metis Int_lower1) + qed + ultimately show "False" + using assms(1, 2) stabilizer_subset_group by (simp add: card_sumset_singleton_subset_eq) + qed + then show ?thesis by auto + qed + moreover have "finite ?H" using finite_sumset assms(10, 11) finite_Int by simp + ultimately show "x \ stabilizer ?H" using mem_stabilizer_Un_and_right_imp_left[of "?H" "x" "C"] + disjnt_def assms Un_commute by (metis disjoint_iff_not_equal) + qed +qed + +lemma sumset_inter_ineq: + assumes "B \ sumset {a} (stabilizer C) = {}" and "stabilizer (sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))) \ stabilizer C" and + "a \ A" and "a \ G" and "finite A" and "finite B" and "A \ {}" and "B \ {}" and "finite (stabilizer C)" + shows "int (card (sumset (A \ B) (stabilizer C))) - card (sumset (A \ B) (stabilizer (sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C))))) \ + int (card (stabilizer C)) - card (sumset (A \ sumset {a} (stabilizer C)) (stabilizer (sumset (A \ sumset {a} (stabilizer C)) (B \ sumset {b} (stabilizer C)))))" + (is "int (card (sumset (A \ B) (stabilizer C))) - card (sumset (A \ B) ?H1) \ + int (card (stabilizer C)) - card (sumset ?A1 ?H1)") +proof- + have hfinsumH1:"finite (sumset (A \ B) ?H1)" + using finite_sumset assms by (meson finite_Un psubsetE rev_finite_subset) + have hsubsumH1: "sumset (A \ B) ?H1 \ sumset (A \ B) (stabilizer C)" + using sumset.cases assms by (meson psubsetE subset_refl sumset_mono) + have hsumH1card_le: "card (sumset (A \ B) ?H1) \ card (sumset (A \ B) (stabilizer C))" + using card_mono finite_sumset stabilizer_finite assms + by (metis equalityE finite_UnI psubset_imp_subset sumset_mono) + have hsub: "sumset ?A1 ?H1 \ sumset {a} (stabilizer C)" + proof + fix x assume "x \ sumset ?A1 ?H1" + then obtain h1 f where "h1 \ ?A1" and hf: "f \ ?H1" and + hx: "x = h1 \ f" by (meson sumset.cases) + then obtain c where hc: "c \ stabilizer C" and hac: "h1 = a \ c" + by (metis Int_iff empty_iff insert_iff sumset.cases) + then have hcf: "c \ f \ stabilizer C" using hf assms(2) stabilizer_is_subgroup + subgroup_def monoid_axioms Group_Theory.group.axioms(1) + Group_Theory.monoid_def subset_iff psubset_imp_subset + by (smt (verit) stabilizer_subset_group sumset.sumsetI sumset_stabilizer_eq) + have hcG: "c \ G" using hc stabilizer_subset_group by auto + have hfG: "f \ G" using hf stabilizer_subset_group by auto + show "x \ sumset {a} (stabilizer C)" using hx hac assms stabilizer_subset_group hcf + using Left_Coset_eq_sumset_stabilizer Left_Coset_memI associative hcG hfG by presburger + qed + moreover have "finite (sumset ?A1 ?H1)" using finite_sumset assms stabilizer_finite finite_subset + by (metis finite.simps hsub) + ultimately have "card (sumset {a} (stabilizer C)) - card (sumset ?A1 ?H1) = + card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)" + using card_Diff_subset by metis + moreover have "card (sumset ?A1 ?H1) \ card (sumset {a} (stabilizer C))" + using card_mono hsub finite_sumset assms by (metis finite.simps) + ultimately have "int (card (sumset {a} (stabilizer C))) - card (sumset ?A1 ?H1) = + card (sumset {a} (stabilizer C) - sumset ?A1 ?H1)" by linarith + also have "... \ card ((sumset (A \ B) (stabilizer C)) - (sumset (A \ B) ?H1))" + proof- + have "sumset {a} (stabilizer C) - sumset ?A1 ?H1 \ sumset (A \ B) (stabilizer C) - sumset (A \ B) ?H1" + proof + fix x assume hx: "x \ sumset {a} (stabilizer C) - sumset ?A1 ?H1" + then obtain c where hxac: "x = a \ c" and hc: "c \ stabilizer C" and hcG: "c \ G" + using sumset.cases by blast + then have "x \ sumset (A \ B) (stabilizer C)" using assms sumset.cases by blast + moreover have "x \ sumset (A \ B) ?H1" + proof + assume "x \ sumset (A \ B) ?H1" + then obtain y h1 where hy: "y \ A \ B" and hyG: "y \ G" and hh1G: "h1 \ G" + and hh1: "h1 \ ?H1" and hxy: "x = y \ h1" by (meson sumset.cases) + then have "y = a \ (c \ inverse h1)" using hxac hxy assms associative commutative composition_closed + inverse_closed invertible invertible_left_inverse2 by (metis hcG) + moreover have "h1 \ stabilizer C" using hh1 assms by auto + moreover hence "c \ inverse h1 \ stabilizer C" using hc stabilizer_is_subgroup subgroup_def + group_axioms invertible subgroup.subgroup_inverse_iff submonoid.sub_composition_closed hh1G by metis + ultimately have "y \ sumset {a} (stabilizer C)" + using assms hcG hh1G by blast + moreover hence "y \ A" using assms(1) hy by auto + ultimately have "x \ sumset ?A1 ?H1" using hxy hh1 + by (simp add: hyG hh1G sumset.sumsetI) + thus "False" using hx by auto + qed + ultimately show "x \ sumset (A \ B) (stabilizer C) - sumset (A \ B) ?H1" + by simp + qed + thus ?thesis using card_mono finite_Diff finite_sumset assms + by (metis finite_UnI nat_int_comparison(3)) + qed + also have "... = int (card (sumset (A \ B) (stabilizer C))) - + card (sumset (A \ B) ?H1)" + using card_Diff_subset[OF hfinsumH1 hsubsumH1] hsumH1card_le by linarith + finally show "int (card (sumset (A \ B) (stabilizer C))) - card (sumset (A \ B) ?H1) \ + int (card (stabilizer C)) - card (sumset ?A1 ?H1)" + using assms by (metis card_sumset_singleton_subset_eq stabilizer_subset_group) +qed + +lemma exists_convergent_min_stabilizer: + assumes hind: "\mC D. C \ G \ D \ G \ finite C \ finite D \ C \ {} \ + D \ {} \ card (sumset C D) + card C = m \ + card (sumset C (stabilizer (sumset C D))) + card (sumset D (stabilizer (sumset C D))) - + card ((stabilizer (sumset C D))) + \ card (sumset C D)" and hAG: "A \ G" and hBG: "B \ G" and hA: "finite A" and + hB: "finite B" and hAne: "A \ {}" and "A \ B \ {}" and + hcardsum: "card (sumset A B) + card A = n" and hintercardA: "card (A \ B) < card A" + obtains X where "convergent X A B" and "\ Y. Y \ convergent_set A B \ + card (stabilizer Y) \ card (stabilizer X)" +proof- + let ?C0 = "sumset (A \ B) (A \ B)" + have hC0ne: "?C0 \ {}" using assms by fast + moreover have "finite ?C0" using sumset_inter_union_subset finite_sumset assms by auto + ultimately have "finite (stabilizer ?C0)" using stabilizer_finite + using sumset_subset_carrier by presburger + then have hcard_sumset_le: "card (A \ B) \ card (sumset (A \ B) (stabilizer ?C0))" + using card_le_sumset sumset_commute sub_unit_closed assms + by (metis Int_Un_eq(3) Un_subset_iff finite_Int unit_closed) + have "card ?C0 \ card (sumset A B)" + using card_mono sumset_inter_union_subset finite_sumset assms + by (simp add: card_mono finite_sumset hA hB sumset_inter_union_subset) + then have "card ?C0 + card (A \ B) < card (sumset A B) + card A" + using hintercardA by auto + then obtain m where "m < n" and "card ?C0 + card (A \ B) = m" using hcardsum by auto + then have "card (sumset (A \ B) (stabilizer ?C0)) + + card (sumset (A \ B) (stabilizer ?C0)) - card (stabilizer ?C0) \ card ?C0" + using assms finite_Un finite_Int + by (metis Int_Un_eq(4) Un_empty Un_subset_iff) + then have "card ?C0 + card (stabilizer ?C0) \ + card (A \ B) + card (sumset (A \ B) (stabilizer ?C0))" using hcard_sumset_le + by auto + then have "?C0 \ convergent_set A B" using convergent_set_def convergent_def + sumset_inter_union_subset hC0ne by auto + then have hconvergent_ne: "convergent_set A B \ {}" by auto + define KS where "KS \ (\ X. card (stabilizer X)) ` convergent_set A B" + define K where "K \ Min KS" + define C where "C \ @C. C \ convergent_set A B \ K = card (stabilizer C)" + obtain KS: "finite KS" "KS \ {}" + using hconvergent_ne finite_convergent_set assms KS_def by auto + then have "K \ KS" using K_def Min_in by blast + then have "\ X. X \ convergent_set A B \ K = card (stabilizer X)" + using KS_def by auto + then obtain "C \ convergent_set A B" and Keq: "K = card (stabilizer C)" + by (metis (mono_tags, lifting) C_def someI_ex) + then have hC: "C \ sumset A B" and hCne: "C \ {}" and + hCcard: "card C + card (stabilizer C) \ + card (A \ B) + card (sumset (A \ B) (stabilizer C))" + using convergent_set_def convergent_def by auto + have hCmin: "\ Y. Y \ convergent_set A B \ + card (stabilizer Y) \ card (stabilizer C)" + using K_def KS_def Keq Min_le KS(1) by auto + show ?thesis using hCmin hC hCcard hCne local.convergent_def that by presburger +qed + +end + +context normal_subgroup +begin + +subsection\ A function that picks coset representatives randomly\ + +definition \ :: "'a set \ 'a" where + "\ = (\ x. if x \ G // K then (SOME a. a \ G \ x = a \| K) else undefined)" + +definition quot_comp_alt :: "'a \ 'a \ 'a" where "quot_comp_alt a b = \ ((a \ b) \| K)" + +lemma phi_eq_coset: + assumes "\ x = a" and "a \ G" and "x \ G // K" + shows "x = a \| K" +proof- + have "(SOME a. a \ G \ x = a \| K) = a" using \_def assms by simp + then show ?thesis using some_eq_ex representant_exists Left_Coset_Class_unit assms + by (metis (mono_tags, lifting)) +qed + +lemma phi_coset_mem: + assumes "a \ G" + shows "\ (a \| K) \ a \| K" +proof- + obtain x where hx: "x = \ (a \| K)" by auto + then have "x = (SOME x. x \ G \ a \| K = x \| K)" using \_def assms + Class_in_Partition Left_Coset_Class_unit by presburger + then show ?thesis using \_def Class_self Left_Coset_Class_unit hx assms + by (smt (verit, ccfv_SIG) tfl_some) +qed + +lemma phi_coset_eq: + assumes "a \ G" and "\ x = a" and "x \ G // K" + shows "\ (a \| K) = a" using phi_eq_coset assms by metis + +lemma phi_inverse_right: + assumes "g \ G" + shows "quot_comp_alt g (\ (inverse g \| K)) = \ K" +proof- + have "g \ (\ (inverse g \| K)) \ (g \ (inverse g) \| K)" + using phi_coset_mem assms by (smt (z3) Left_Coset_memE factor_unit invertible invertible_right_inverse + invertible_inverse_closed invertible_inverse_inverse sub invertible_left_inverse2) + then have "g \ (\ (inverse g \| K)) \| K = K" + using Block_self Left_Coset_Class_unit Normal_def quotient.unit_closed sub + by (metis assms composition_closed invertible invertible_inverse_closed invertible_right_inverse) + then show ?thesis using quot_comp_alt_def by auto +qed + +lemma phi_inverse_left: + assumes "g \ G" + shows "quot_comp_alt (\ (inverse g \| K)) g = \ K" +proof- + have "(\ (inverse g \| K)) \ g \ ((inverse g) \ g) \| K" using phi_coset_mem assms + by (metis Left_Coset_memE factor_unit invertible invertible_inverse_closed invertible_left_inverse normal) + then have "(\ (inverse g \| K)) \ g \| K = K" using Block_self Left_Coset_Class_unit Normal_def + quotient.unit_closed sub by (smt (verit, best) assms composition_closed invertible invertible_inverse_closed + invertible_left_inverse) + then show ?thesis using quot_comp_alt_def by auto +qed + +lemma phi_mem_coset_eq: + assumes "a \ G // K" and "b \ G" + shows "\ a \ b \| K \ a = (b \| K)" +proof- + assume "\ a \ b \| K" + then have "a \ (b \| K) \ {}" + by (metis Class_closed Class_is_Left_Coset Int_iff assms empty_iff phi_coset_mem phi_eq_coset) + then show "a = b \| K" by (metis Class_in_Partition Class_is_Left_Coset assms disjoint) +qed + + +lemma forall_unique_repr: + "\ x \ G // K. \! k \ \ ` (G // K). x = k \| K" +proof + fix x assume hx: "x \ G // K" + then have "\ x \| K = x" + by (metis Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset representant_exists) + then have hex: "\ k \ \ ` (G // K). x = k \| K" using hx by blast + moreover have "\ a b. a \ \ ` (G // K) \ x = a \| K \ b \ \ ` (G // K) \ x = b \| K \ + a = b" + proof- + fix a b assume "a \ \ ` (G // K)" and hxa: "x = a \| K" and "b \ \ ` (G // K)" and + hxb: "x = b \| K" + then obtain z w where "a = \ (z \| K)" and "b = \ (w \| K)" and "z \ G" and "w \ G" + using representant_exists Left_Coset_Class_unit by force + then show "a = b" using hxa hxb + by (metis Class_in_Partition Class_is_Left_Coset block_closed phi_coset_mem phi_eq_coset) + qed + ultimately show "\! k \ \ ` (G // K). x = k \| K" by blast +qed + +lemma phi_inj_on: + shows "inj_on \ (G // K)" +proof(intro inj_onI) + fix x y assume "x \ G // K" and hy: "y \ G // K" and hxy: "\ x = \ y" + then obtain a b where "x = a \| K" and "y = b \| K" and "a \ G" and "b \ G" + using representant_exists Left_Coset_Class_unit by metis + then show "x = y" using hxy hy by (metis phi_coset_mem phi_mem_coset_eq) +qed + +lemma phi_coset_eq_self: + assumes "a \ G // K" + shows "\ a \| K = a" + by (metis Class_closed Class_is_Left_Coset assms phi_coset_mem phi_eq_coset representant_exists) + +lemma phi_coset_comp_eq: + assumes "a \ G // K" and "b \ G // K" + shows "\ a \ \ b \| K = a [\] b" using assms phi_coset_eq_self + by (metis Class_is_Left_Coset block_closed factor_composition phi_coset_mem representant_exists) + +lemma phi_comp_eq: + assumes "a \ G // K" and "b \ G // K" + shows "\ (a [\] b) = quot_comp_alt (\ a) (\ b)" + using phi_coset_comp_eq quot_comp_alt_def assms by auto + +lemma phi_image_subset: + "\ ` (G // K) \ G" +proof(intro image_subsetI, simp add: \_def) + fix x assume "x \ G // K" + then show "(SOME a. a \ G \ x = a \| K) \ G" + using Left_Coset_Class_unit representant_exists someI_ex by (metis (mono_tags, lifting)) +qed + +lemma phi_image_group: + "Group_Theory.group (\ ` (G // K)) quot_comp_alt (\ K)" +proof- + have hmonoid: "Group_Theory.monoid (\ ` (G // K)) quot_comp_alt (\ K)" + proof + show "\a b. a \ \ ` (G // K) \ b \ \ ` (G // K) \ + quot_comp_alt a b \ \ ` (G // K)" using quot_comp_alt_def imageI phi_image_subset + by (metis Class_in_Partition Left_Coset_Class_unit composition_closed subset_iff) + next + show "(\ K) \ \ ` (G // K)" using \_def Left_Coset_Class_unit imageI Normal_def by blast + next + show "\a b c. a \ \ ` Partition \ b \ \ ` Partition \ c \ \ ` Partition \ + quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)" + proof- + fix a b c assume ha: "a \ \ ` (G // K)" and hb: "b \ \ ` (G // K)" and hc: "c \ \ ` (G // K)" + have habc: "a \ b \ c \ G" using ha hb hc composition_closed phi_image_subset by (meson subsetD) + have hab: "quot_comp_alt a b \ (a \ b) \| K" using phi_image_subset quot_comp_alt_def ha hb + by (metis composition_closed phi_coset_mem subsetD) + then have "quot_comp_alt (quot_comp_alt a b) c \ (a \ b \ c) \| K" using quot_comp_alt_def phi_image_subset ha hb hc + by (smt (z3) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit composition_closed + natural.commutes_with_composition phi_coset_mem subset_iff) + moreover have hbc: "quot_comp_alt b c \ (b \ c) \| K" using hb hc phi_image_subset quot_comp_alt_def + by (metis composition_closed phi_coset_mem subset_iff) + moreover hence "quot_comp_alt a (quot_comp_alt b c) \ (a \ b \ c) \| K" using quot_comp_alt_def phi_image_subset ha hb hc + by (smt (verit, del_insts) Block_self Class_closed Class_in_Partition Left_Coset_Class_unit + associative composition_closed natural.commutes_with_composition phi_coset_mem subset_iff) + moreover have "a \ (quot_comp_alt b c) \| K \ G // K" using ha hb hc phi_image_subset + by (metis Class_closed Class_in_Partition Class_is_Left_Coset hbc composition_closed in_mono subset_eq) + moreover have "(quot_comp_alt a b) \ c \| K \ G // K" using ha hb hc phi_image_subset + by (metis Class_closed Class_in_Partition Left_Coset_Class_unit hab composition_closed in_mono) + ultimately show "quot_comp_alt (quot_comp_alt a b) c = quot_comp_alt a (quot_comp_alt b c)" + using phi_mem_coset_eq[OF _ habc] quot_comp_alt_def by metis + qed + next + show "\a. a \ \ ` Partition \ quot_comp_alt (\ K) a = a" using quot_comp_alt_def \_def + phi_image_subset image_iff phi_coset_eq subsetD by (smt (z3) Normal_def Partition_def + natural.image.sub_unit_closed phi_comp_eq quotient.left_unit) + next + show "\a. a \ \ ` Partition \ quot_comp_alt a (\ K) = a" using quot_comp_alt_def \_def + phi_image_subset image_iff phi_coset_eq subsetD by (smt (verit) Normal_def + factor_composition factor_unit normal_subgroup.phi_coset_eq_self normal_subgroup_axioms + quotient.unit_closed right_unit unit_closed) + qed + moreover show "Group_Theory.group (\ ` (G // K)) quot_comp_alt (\ K)" + proof(simp add: group_def group_axioms_def hmonoid) + show "\u. u \ \ ` Partition \ monoid.invertible (\ ` Partition) quot_comp_alt (\ K) u" + proof(intro allI impI) + fix g assume hg: "g \ \ ` (G // K)" + then have "quot_comp_alt g (\ ((inverse g) \| K)) = (\ K)" + and "quot_comp_alt (\ ((inverse g) \| K)) g = (\ K)" + using phi_image_subset phi_inverse_right phi_inverse_left by auto + moreover have "\ ((inverse g) \| K) \ \ ` (G // K)" using imageI hg phi_image_subset + by (metis (no_types, opaque_lifting) Class_in_Partition Left_Coset_Class_unit in_mono + invertible invertible_inverse_closed) + ultimately show "monoid.invertible (\ ` Partition) quot_comp_alt (\ K) g" + using monoid.invertibleI[OF hmonoid] hg by presburger + qed + qed +qed + +lemma phi_map: "Set_Theory.map \ Partition (\ ` Partition)" + by (auto simp add: Set_Theory.map_def \_def) + +lemma phi_image_isomorphic: + "group_isomorphism \ (G // K) ([\]) (Class \) (\ ` (G // K)) quot_comp_alt (\ K)" +proof - + have "bijective_map \ Partition (\ ` Partition)" + using bijective_map_def bijective_def bij_betw_def phi_inj_on phi_map by blast + moreover have "Group_Theory.monoid (\ ` Partition) quot_comp_alt (\ K)" + using phi_image_group group_def by metis + moreover have "\ (Class \) = \ K" using Left_Coset_Class_unit Normal_def by auto + ultimately show ?thesis + by (auto simp add: group_isomorphism_def group_homomorphism_def monoid_homomorphism_def + phi_image_group quotient.monoid_axioms quotient.group_axioms monoid_homomorphism_axioms_def + phi_comp_eq phi_map) +qed + +end + +context subgroup_of_additive_abelian_group + +begin + +lemma Union_Coset_card_eq: + assumes hSG: "S \ G" and hSU: "(\ (Class ` S)) = S" + shows "card S = card H * card (Class ` S)" +proof(cases "finite H") + case hH: True + have hfin: "\A. A \ Class ` S \ finite A" using hSG Right_Coset_Class_unit + Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD + by (smt (verit, del_insts) imageE) + have "card S = card H * card (Class ` S)" when hS: "finite S" + proof- + have hdisj: "pairwise (\s t. disjnt s t) (Class ` S)" + proof (intro pairwiseI) + fix x y assume "x \ Class ` S" and "y \ Class ` S" and hxy: "x \ y" + then obtain a b where "x = Class a" and "y = Class b" and + "a \ S" and "b \ S" by blast + then show "disjnt x y" using disjnt_def hxy + by (smt (verit, ccfv_threshold) not_disjoint_implies_equal hSG subsetD) + qed + then have "card (\ (Class ` S)) = sum card (Class ` S)" using card_Union_disjoint hfin by blast + moreover have "finite (Class ` S)" using hS by blast + ultimately have "card (\ (Class ` S)) = (\ a \ Class ` S. card a)" + using sum_card_image hdisj by blast + moreover have "\ a. a \ Class ` S \ card a = card H" + using hSG Right_Coset_Class_unit Right_Coset_cardinality by auto + ultimately show "card S = card H * card (Class ` S)" + using hSU by simp + qed + moreover have "card S = card H * card (Class ` S)" when hS: "\ finite S" + using finite_Union hfin hS hSU by (metis card_eq_0_iff mult_0_right) + ultimately show ?thesis by blast +next + case hH: False + have "card S = card H * card (Class ` S)" when "S = {}" + by (simp add: that) + then have hinf: "\ A. A \ Class ` S \ infinite A" using hSG Right_Coset_Class_unit + Right_Coset_cardinality hH card_eq_0_iff empty_iff sub_unit_closed subsetD + by (smt (verit) Class_self imageE) + moreover have "card S = card H * card (Class ` S)" when "S \ {}" using hSU by (metis Class_closed2 + Normal_def card.infinite card_sumset_0_iff hH hSG mult_is_0 sumset_subgroup_eq_Class_Union unit_closed) + ultimately show ?thesis by fastforce +qed + +end + +context subgroup_of_abelian_group +begin + +interpretation GH: additive_abelian_group "G // H" "([\])" "Class \" +proof + fix x y assume "x \ G // H" and "y \ G // H" + then show "x [\] y = y [\] x" using Class_commutes_with_composition commutative representant_exists + by metis +qed + +interpretation GH_repr: additive_abelian_group "\ ` (G // H)" "quot_comp_alt" "\ H" +proof(simp add: additive_abelian_group_def abelian_group_def phi_image_group + commutative_monoid_def commutative_monoid_axioms_def, intro conjI allI impI) + show "Group_Theory.monoid (\ ` Partition) quot_comp_alt (\ H)" + using phi_image_group group_def by metis +next + show "\ x y. x \ \ ` Partition \ y \ \ ` Partition \ quot_comp_alt x y = quot_comp_alt y x" + by (auto) (metis GH.commutative phi_comp_eq) +qed + +lemma phi_image_sumset_eq: + assumes "A \ G // H" and "B \ G // H" + shows "\ ` (GH.sumset A B) = GH_repr.sumset (\ ` A) (\ ` B)" +proof(intro subset_antisym image_subsetI subsetI) + fix x assume "x \ GH.sumset A B" + then obtain c d where "x = quotient_composition c d" and hc: "c \ A" and hd: "d \ B" + using GH.sumset.cases by blast + then have "\ x = quot_comp_alt (\ c) (\ d)" + using phi_comp_eq assms subsetD by blast + then show "\ x \ GH_repr.sumset (\ ` A) (\ ` B)" + using hc hd assms subsetD GH_repr.sumsetI imageI by auto +next + fix x assume "x \ GH_repr.sumset (\ ` A) (\ ` B)" + then obtain a b where "x = quot_comp_alt a b" and ha: "a \ \ ` A" and hb: "b \ \ ` B" + using GH_repr.sumset.cases by metis + moreover obtain c d where "a = \ c" and "b = \ d" and "c \ A" and "d \ B" + using ha hb by blast + ultimately show "x \ \ ` GH.sumset A B" using phi_comp_eq assms imageI GH.sumsetI + by (smt (verit, del_insts) subsetD) +qed + +lemma phi_image_stabilizer_eq: + assumes "A \ G // H" + shows "\ ` (GH.stabilizer A) = GH_repr.stabilizer (\ ` A)" +proof(intro subset_antisym image_subsetI subsetI) + fix x assume "x \ GH.stabilizer A" + then have "GH.sumset {x} A = A" and hx: "x \ G // H" using GH.stabilizer_def assms by auto + then have "GH_repr.sumset (\ ` {x}) (\ ` A) = \ ` A" using assms phi_image_sumset_eq + by (metis empty_subsetI insert_subset) + then show "\ x \ GH_repr.stabilizer (\ ` A)" using GH_repr.stabilizer_def assms + by (smt (z3) GH_repr.sumset_Int_carrier hx image_empty image_eqI image_insert mem_Collect_eq) +next + fix x assume "x \ GH_repr.stabilizer (\ ` A)" + then have hstab: "GH_repr.sumset {x} (\ ` A) = (\ ` A)" and hx: "x \ \ ` (G // H)" + using GH_repr.stabilizer_def assms phi_image_subset by auto + then obtain B where hB: "B \ G // H" and hBx: "\ B = x" by blast + then have "GH_repr.sumset (\ ` {B}) (\ ` A) = \ ` A" using hstab by auto + then have "GH.sumset {B} A = A" using phi_image_sumset_eq phi_inj_on assms hB + GH.sumset_subset_carrier by (smt (z3) GH.sumset_singletons_eq inj_on_image_eq_iff + quotient.right_unit quotient.unit_closed) + then show "x \ \ ` (GH.stabilizer A)" using assms hBx GH.stabilizer_def + by (smt (z3) GH.sumset_Int_carrier hB image_iff mem_Collect_eq) +qed + +end + +subsection\Useful group-theoretic results\ + +lemma residue_group: "abelian_group {0..(m :: nat)-1} (\ x y. ((x + y) mod m)) (0 :: int)" +proof(cases "m > 1") + case hm: True + then have hmonoid: "Group_Theory.monoid {0..m-1} (\ x y. ((x + y) mod m)) (0 :: int)" + by (unfold_locales, auto simp add: of_nat_diff, presburger) + moreover have "monoid.invertible {0..int (m - 1)} (\x y. (x + y) mod int m) 0 u" if "u \ {0..int (m - 1)}" for u + proof(cases "u = 0") + case True + then show ?thesis using monoid.invertible_def[OF hmonoid that] monoid.unit_invertible[OF hmonoid] by simp + next + case hx: False + then have "((m - u) + u) mod m = 0" and "(u + (m - u)) mod m = 0" and "m - u \ {0..int(m-1)}" + using atLeastAtMost_iff hx that by auto + then show ?thesis using monoid.invertible_def[OF hmonoid that] by metis + qed + moreover have "commutative_monoid {0..m-1} (\ x y. ((x + y) mod m)) (0 :: int)" + using hmonoid commutative_monoid_def commutative_monoid_axioms_def by (smt (verit)) + ultimately show ?thesis by (simp add: abelian_group_def group_def group_axioms_def + hmonoid) +next + case hm: False + moreover have hmonoid: "Group_Theory.monoid {0} (\ x y. ((x + y) mod m)) (0 :: int)" + by (unfold_locales, auto) + moreover have "monoid.invertible {0} (\x y. (x + y) mod int m) 0 0" using monoid.invertible_def[OF hmonoid] + monoid.unit_invertible[OF hmonoid] hm by simp + ultimately show ?thesis by (unfold_locales, auto) +qed + +lemma (in subgroup_of_group) prime_order_simple: + assumes "prime (card G)" + shows "H = {\} \ H = G" +proof- + have "card H dvd card G" using lagrange assms card.infinite dvdI not_prime_0 by fastforce + then have "card H = 1 \ card H = card G" using assms prime_nat_iff by blast + then show ?thesis using card_1_singletonE sub_unit_closed card.infinite card_subset_eq sub + assms not_prime_0 subsetI insertE empty_iff by metis +qed + +lemma residue_group_simple: + assumes "prime p" and "subgroup H {0..(p :: nat)-1} (\ x y. ((x + y) mod p)) (0 :: int)" + shows "H = {0} \ H = {0..int(p-1)}" +proof- + have hprime: "prime (card {0..int(p-1)})" using card_atLeastAtMost_int assms int_ops by auto + moreover have hsub:"subgroup_of_group H {0..(p :: nat)-1} (\ x y. ((x + y) mod p)) (0 :: int)" + using subgroup_of_group_def assms abelian_group_def residue_group by fast + ultimately show ?thesis using assms subgroup_of_group.prime_order_simple[OF hsub hprime] by blast +qed + +end diff --git a/thys/Kneser_Cauchy_Davenport/ROOT b/thys/Kneser_Cauchy_Davenport/ROOT new file mode 100644 --- /dev/null +++ b/thys/Kneser_Cauchy_Davenport/ROOT @@ -0,0 +1,13 @@ +chapter AFP + +session Kneser_Cauchy_Davenport (AFP) = "HOL-Number_Theory" + + options [timeout = 900] + sessions + Pluennecke_Ruzsa_Inequality + Jacobson_Basic_Algebra + theories + Kneser_Cauchy_Davenport_preliminaries + Kneser_Cauchy_Davenport_main_proofs + document_files + "root.bib" + "root.tex" diff --git a/thys/Kneser_Cauchy_Davenport/document/root.bib b/thys/Kneser_Cauchy_Davenport/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Kneser_Cauchy_Davenport/document/root.bib @@ -0,0 +1,43 @@ +%% This BibTeX bibliography file was created using BibDesk. +%% http://bibdesk.sourceforge.net/ + + + + +%% Saved with string encoding Unicode (UTF-8) + + +@InProceedings{DeVos_Kneser, +author={DeVos, Matt}, +editor={Nathanson, Melvyn B.}, +title={A Short Proof of Kneser's Addition Theorem for Abelian Groups}, +booktitle={Combinatorial and Additive Number Theory}, +year={2014}, +publisher={Springer New York}, +address={New York, NY}, +pages={39--41}, +isbn={978-1-4939-1601-6} +} + + +@Book{Nathanson_book, + author = {Nathanson, Melvyn B}, + title = { Additive Number Theory: +Inverse Problems and the Geometry of Sumsets}, + publisher = {Springer-Verlag}, + year = {1996}, + volume = {165}, + series = {Graduate Texts in Mathematics}, + isbn={978-0-387-94655-9} +} + + + +@misc{Ruzsa_book, + author = {Ruzsa, Imre Z.}, + note = { Course notes, available on +\url{https://www.math.cmu.edu/users/af1p/Teaching/AdditiveCombinatorics/Additive-Combinatorics.pdf}}, + title = {Sumsets and Structure}, + year = {2008} +} + diff --git a/thys/Kneser_Cauchy_Davenport/document/root.tex b/thys/Kneser_Cauchy_Davenport/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Kneser_Cauchy_Davenport/document/root.tex @@ -0,0 +1,48 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amssymb} +\usepackage{isabelle,isabellesym} +\usepackage[english]{babel} % for guillemots + +% 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{Kneser's Theorem and the Cauchy--Davenport Theorem} +\author{Mantas Bak\v{s}ys and Angeliki Koutsoukou-Argyraki \\ +University of Cambridge\\ +\texttt{\{mb2412, ak2110\}@cam.ac.uk}} + +\maketitle + +\begin{abstract} +We formalise Kneser's Theorem in combinatorics \cite{Nathanson_book, Ruzsa_book} following the proof from the 2014 paper "A short proof of Kneser’s addition theorem for abelian groups" by Matt DeVos \cite{DeVos_Kneser}. We also show a strict version of Kneser's Theorem as well as the Cauchy--Davenport Theorem as a corollary of Kneser's Theorem. +\end{abstract} +\newpage +\tableofcontents + +\subsection*{Acknowledgements} +Angeliki Koutsoukou-Argyraki is funded by the ERC Advanced Grant ALEXANDRIA (Project GA +742178) funded by the European Research Council and led by Lawrence C. Paulson +(University of Cambridge, Department of Computer Science and Technology). +Mantas Bak\v{s}ys received funding for his internship supervised by Koutsoukou-Argyraki by the +Cambridge Mathematics Placements (CMP) Programme and by the ALEXANDRIA Project. +We wish to thank Manuel Eberl for his useful +suggestion for treating induction when there is a type discrepancy between the induction hypothesis +and the induction step. +\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,717 +1,718 @@ 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 Balog_Szemeredi_Gowers 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 Boolos_Curious_Inference Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRYSTALS-Kyber 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 CHERI-C_Memory_Model Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Commuting_Hermitian 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 DPRM_Theorem 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 FSM_Tests 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 Finite_Fields 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 Hales_Jewett 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 IMP_Compiler_Reuse IP_Addresses Imperative_Insertion_Sort Implicational_Logic 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 Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model IsaNet Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra +Kneser_Cauchy_Davenport 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 Maximum_Segment_Sum 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 Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON 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 Number_Theoretic_Transform 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 PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Padic_Field 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 Query_Optimization 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 Real_Time_Deque 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 Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending 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 Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma SCC_Bloemen_Sequential Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded 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 Solidity Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic 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 Turans_Graph_Theorem Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory 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_Arithmetic_Geometric_Mean 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