Theory Generalized_Cauchy_Davenport_preliminaries
section‹Preliminaries on well-orderings, groups, and sumsets›
theory Generalized_Cauchy_Davenport_preliminaries
imports
Complex_Main
"Jacobson_Basic_Algebra.Group_Theory"
"HOL-Library.Extended_Nat"
begin
subsection‹Well-ordering lemmas›
lemma wf_prod_lex_fibers_inter:
fixes r :: "('a × 'a) set" and s :: "('b × 'b) set" and f :: "'c ⇒ 'a" and g :: "'c ⇒ 'b" and
t :: "('c × 'c) set"
assumes h1: "wf ((inv_image r f) ∩ t)" and
h2: "⋀ a. a ∈ range f ⟹ wf (({x. f x = a} × {x. f x = a} ∩ (inv_image s g)) ∩ t)" and
h3: "trans t"
shows "wf ((inv_image (r <*lex*> s) (λ c. (f c, g c))) ∩ t)"
proof-
have h4: "(⋃ a ∈ range f. ({x. f x = a} × {x. f x = a} ∩ (inv_image s g)) ∩ t) =
(⋃ a ∈ range f. ({x. f x = a} × {x. f x = a} ∩ (inv_image s g))) ∩ t" by blast
have "(inv_image (r <*lex*> s) (λ c. (f c, g c))) ∩ t = (inv_image r f ∩ t) ∪
(⋃ a ∈ range f. {x. f x = a} × {x. f x = a} ∩ (inv_image s g) ∩ t)"
proof
show "inv_image (r <*lex*> s) (λc. (f c, g c)) ∩ t
⊆ inv_image r f ∩ t ∪ (⋃a∈range f. {x. f x = a} × {x. f x = a} ∩ inv_image s g ∩ t)"
proof
fix y assume hy: "y ∈ inv_image (r <*lex*> s) (λc. (f c, g c)) ∩ t"
then obtain a b where hx: "y = (a, b)" and "(f a, f b) ∈ r ∨ (f a = f b ∧ (g a, g b) ∈ s)"
using in_inv_image in_lex_prod Int_iff SigmaE UNIV_Times_UNIV inf_top_right by (smt (z3))
then show "y ∈ inv_image r f ∩ t ∪ (⋃a∈range f. {x. f x = a} × {x. f x = a} ∩ inv_image s g ∩ t)"
using hy by auto
qed
show "inv_image r f ∩ t ∪ (⋃a∈range f. {x. f x = a} × {x. f x = a} ∩ inv_image s g ∩ t) ⊆
inv_image (r <*lex*> s) (λc. (f c, g c)) ∩ t" using Int_iff SUP_le_iff SigmaD1 SigmaD2
in_inv_image in_lex_prod mem_Collect_eq subrelI by force
qed
moreover have "((inv_image r f) ∩ t) O
(⋃ a ∈ range f. ({x. f x = a} × {x. f x = a} ∩ (inv_image s g)) ∩ t) ⊆ (inv_image r f) ∩ t"
using h3 trans_O_subset by fastforce
moreover have "wf (⋃ a ∈ range f. {x. f x = a} × {x. f x = a} ∩ (inv_image s g) ∩ t)"
apply(rule wf_UN, auto simp add: h2)
done
ultimately show "wf (inv_image (r <*lex*> s) (λ c. (f c, g c)) ∩ t)"
using wf_union_compatible[OF h1] by fastforce
qed
lemma wf_prod_lex_fibers:
fixes r :: "('a × 'a) set" and s :: "('b × 'b) set" and f :: "'c ⇒ 'a" and g :: "'c ⇒ 'b"
assumes h1: "wf (inv_image r f)" and
h2: "⋀ a. a ∈ range f ⟹ wf ({x. f x = a} × {x. f x = a} ∩ (inv_image s g))"
shows "wf (inv_image (r <*lex*> s) (λ c. (f c, g c)))"
using assms trans_def wf_prod_lex_fibers_inter[of r f UNIV s g] inf_top_right
by (metis (mono_tags, lifting) iso_tuple_UNIV_I)
context monoid
begin
subsection‹Pointwise set multiplication in a monoid: definition and key lemmas›
inductive_set smul :: "'a set ⇒ 'a set ⇒ 'a set" for A B
where
smulI[intro]: "⟦a ∈ A; a ∈ M; b ∈ B; b ∈ M⟧ ⟹ a ⋅ b ∈ smul A B"
syntax "smul" :: "'a set ⇒ 'a set ⇒ 'a set" ("(_ ⋯ _)")
lemma smul_eq: "smul A B = {c. ∃a ∈ A ∩ M. ∃b ∈ B ∩ M. c = a ⋅ b}"
by (auto simp: smul.simps elim!: smul.cases)
lemma smul: "smul A B = (⋃a ∈ A ∩ M. ⋃b ∈ B ∩ M. {a ⋅ b})"
by (auto simp: smul_eq)
lemma smul_subset_carrier: "smul A B ⊆ M"
by (auto simp: smul_eq)
lemma smul_Int_carrier [simp]: "smul A B ∩ M = smul A B"
by (simp add: Int_absorb2 smul_subset_carrier)
lemma smul_mono: "⟦A' ⊆ A; B' ⊆ B⟧ ⟹ smul A' B' ⊆ smul A B"
by (auto simp: smul_eq)
lemma smul_insert1: "NO_MATCH {} A ⟹ smul (insert x A) B = smul {x} B ∪ smul A B"
by (auto simp: smul_eq)
lemma smul_insert2: "NO_MATCH {} B ⟹ smul A (insert x B) = smul A {x} ∪ smul A B"
by (auto simp: smul_eq)
lemma smul_subset_Un1: "smul (A ∪ A') B = smul A B ∪ smul A' B"
by (auto simp: smul_eq)
lemma smul_subset_Un2: "smul A (B ∪ B') = smul A B ∪ smul A B'"
by (auto simp: smul_eq)
lemma smul_subset_Union1: "smul (⋃ A) B = (⋃ a ∈ A. smul a B)"
by (auto simp: smul_eq)
lemma smul_subset_Union2: "smul A (⋃ B) = (⋃ b ∈ B. smul A b)"
by (auto simp: smul_eq)
lemma smul_subset_insert: "smul A B ⊆ smul A (insert x B)" "smul A B ⊆ smul (insert x A) B"
by (auto simp: smul_eq)
lemma smul_subset_Un: "smul A B ⊆ smul A (B∪C)" "smul A B ⊆ smul (A∪C) B"
by (auto simp: smul_eq)
lemma smul_empty [simp]: "smul A {} = {}" "smul {} A = {}"
by (auto simp: smul_eq)
lemma smul_empty':
assumes "A ∩ M = {}"
shows "smul B A = {}" "smul A B = {}"
using assms by (auto simp: smul_eq)
lemma smul_is_empty_iff [simp]: "smul A B = {} ⟷ A ∩ M = {} ∨ B ∩ M = {}"
by (auto simp: smul_eq)
lemma smul_D [simp]: "smul A {𝟭} = A ∩ M" "smul {𝟭} A = A ∩ M"
by (auto simp: smul_eq)
lemma smul_Int_carrier_eq [simp]: "smul A (B ∩ M) = smul A B" "smul (A ∩ M) B = smul A B"
by (auto simp: smul_eq)
lemma smul_assoc:
shows "smul (smul A B) C = smul A (smul B C)"
by (fastforce simp add: smul_eq associative Bex_def)
lemma finite_smul:
assumes "finite A" "finite B" shows "finite (smul A B)"
using assms by (auto simp: smul_eq)
lemma finite_smul':
assumes "finite (A ∩ M)" "finite (B ∩ M)"
shows "finite (smul A B)"
using assms by (auto simp: smul_eq)
subsection ‹Exponentiation in a monoid: definitions and lemmas›
primrec power :: "'a ⇒ nat ⇒ 'a" (infix "^" 100)
where
power0: "power g 0 = 𝟭"
| power_suc: "power g (Suc n) = power g n ⋅ g"
lemma power_one:
assumes "g ∈ M"
shows "power g 1 = g" using power_def power0 assms by simp
lemma power_mem_carrier:
fixes n
assumes "g ∈ M"
shows "g ^ n ∈ M"
apply (induction n, auto simp add: assms power_def)
done
lemma power_mult:
assumes "g ∈ M"
shows "g ^ n ⋅ g ^ m = g ^ (n + m)"
proof(induction m)
case 0
then show ?case using assms power0 right_unit power_mem_carrier by simp
next
case (Suc m)
assume "g ^ n ⋅ g ^ m = g ^ (n + m)"
then show ?case using power_def by (smt (verit) add_Suc_right assms associative
power_mem_carrier power_suc)
qed
lemma mult_inverse_power:
assumes "g ∈ M" and "invertible g"
shows "g ^ n ⋅ ((inverse g) ^ n) = 𝟭"
proof(induction n)
case 0
then show ?case using power_0 by auto
next
case (Suc n)
assume hind: "g ^ n ⋅ local.inverse g ^ n = 𝟭"
then have "g ^ Suc n ⋅ inverse g ^ Suc n = (g ⋅ g ^ n) ⋅ (inverse g ^ n ⋅ inverse g)"
using power_def power_mult assms by (smt (z3) add.commute invertible_inverse_closed
invertible_right_inverse left_unit monoid.associative monoid_axioms power_mem_carrier power_suc)
then show ?case using associative power_mem_carrier assms hind by (smt (verit, del_insts)
composition_closed invertible_inverse_closed invertible_right_inverse right_unit)
qed
lemma inverse_mult_power:
assumes "g ∈ M" and "invertible g"
shows "((inverse g) ^ n) ⋅ g ^ n = 𝟭" using assms by (metis invertible_inverse_closed
invertible_inverse_inverse invertible_inverse_invertible mult_inverse_power)
lemma inverse_mult_power_eq:
assumes "g ∈ M" and "invertible g"
shows "inverse (g ^ n) = (inverse g) ^ n"
using assms inverse_equality by (simp add: inverse_mult_power mult_inverse_power power_mem_carrier)
definition power_int :: "'a ⇒ int ⇒ 'a" (infixr "powi" 80) where
"power_int g n = (if n ≥ 0 then g ^ (nat n) else (inverse g) ^ (nat (-n)))"
definition nat_powers :: "'a ⇒ 'a set" where "nat_powers g = ((λ n. g ^ n) ` UNIV)"
lemma nat_powers_eq_Union: "nat_powers g = (⋃ n. {g ^ n})" using nat_powers_def by auto
definition powers :: "'a ⇒ 'a set" where "powers g = ((λ n. g powi n) ` UNIV)"
lemma nat_powers_subset:
"nat_powers g ⊆ powers g"
proof
fix x assume "x ∈ nat_powers g"
then obtain n where "x = g ^ n" and "nat n = n" using nat_powers_def by auto
then show "x ∈ powers g" using powers_def power_int_def
by (metis UNIV_I image_iff of_nat_0_le_iff)
qed
lemma inverse_nat_powers_subset:
"nat_powers (inverse g) ⊆ powers g"
proof
fix x assume "x ∈ nat_powers (inverse g)"
then obtain n where hx: "x = (inverse g) ^ n" using nat_powers_def by blast
then show "x ∈ powers g"
proof(cases "n = 0")
case True
then show ?thesis using hx power0 powers_def
by (metis nat_powers_def nat_powers_subset rangeI subsetD)
next
case False
then have hpos: "¬ (- int n) ≥ 0" by auto
then have "x = g powi (- int n)" using hx hpos power_int_def by simp
then show ?thesis using powers_def by auto
qed
qed
lemma powers_eq_union_nat_powers:
"powers g = nat_powers g ∪ nat_powers (inverse g)"
proof
show "powers g ⊆ nat_powers g ∪ nat_powers (local.inverse g)"
using powers_def nat_powers_def power_int_def by auto
next
show "nat_powers g ∪ nat_powers (inverse g) ⊆ powers g"
by (simp add: inverse_nat_powers_subset nat_powers_subset)
qed
lemma one_mem_nat_powers: "𝟭 ∈ nat_powers g"
using rangeI power0 nat_powers_def by metis
lemma nat_powers_subset_carrier:
assumes "g ∈ M"
shows "nat_powers g ⊆ M"
using nat_powers_def power_mem_carrier assms by auto
lemma nat_powers_mult_closed:
assumes "g ∈ M"
shows "⋀ x y. x ∈ nat_powers g ⟹ y ∈ nat_powers g ⟹ x ⋅ y ∈ nat_powers g"
using nat_powers_def power_mult assms by auto
lemma nat_powers_inv_mult:
assumes "g ∈ M" and "invertible g"
shows "⋀ x y. x ∈ nat_powers g ⟹ y ∈ nat_powers (inverse g) ⟹ x ⋅ y ∈ powers g"
proof-
fix x y assume "x ∈ nat_powers g" and "y ∈ nat_powers (inverse g)"
then obtain n m where hx: "x = g ^ n" and hy: "y = (inverse g) ^ m" using nat_powers_def by blast
show "x ⋅ y ∈ powers g"
proof(cases "n ≥ m")
case True
then obtain k where "n = k + m" using add.commute le_Suc_ex by blast
then have "g ^ n ⋅ (inverse g) ^ m = g ^ k" using mult_inverse_power assms associative
by (smt (verit) invertible_inverse_closed local.power_mult power_mem_carrier right_unit)
then show ?thesis using hx hy powers_eq_union_nat_powers nat_powers_def by auto
next
case False
then obtain k where "m = n + k" by (metis leI less_imp_add_positive)
then have "g ^ n ⋅ (inverse g) ^ m = (inverse g) ^ k" using inverse_mult_power assms associative
by (smt (verit) left_unit local.power_mult monoid.invertible_inverse_closed monoid_axioms
mult_inverse_power power_mem_carrier)
then show ?thesis using hx hy powers_eq_union_nat_powers nat_powers_def by auto
qed
qed
lemma inv_nat_powers_mult:
assumes "g ∈ M" and "invertible g"
shows "⋀ x y. x ∈ nat_powers (inverse g) ⟹ y ∈ nat_powers g ⟹ x ⋅ y ∈ powers g"
by (metis assms invertible_inverse_closed invertible_inverse_inverse invertible_inverse_invertible
nat_powers_inv_mult powers_eq_union_nat_powers sup_commute)
lemma powers_mult_closed:
assumes "g ∈ M" and "invertible g"
shows "⋀ x y. x ∈ powers g ⟹ y ∈ powers g ⟹ x ⋅ y ∈ powers g"
using powers_eq_union_nat_powers assms
nat_powers_mult_closed nat_powers_inv_mult inv_nat_powers_mult by fastforce
lemma nat_powers_submonoid:
assumes "g ∈ M"
shows "submonoid (nat_powers g) M (⋅) 𝟭"
apply(unfold_locales)
apply(auto simp add: assms nat_powers_mult_closed one_mem_nat_powers nat_powers_subset_carrier)
done
lemma nat_powers_monoid:
assumes "g ∈ M"
shows "Group_Theory.monoid (nat_powers g) (⋅) 𝟭"
using nat_powers_submonoid assms by (smt (verit) monoid.intro associative left_unit
one_mem_nat_powers nat_powers_mult_closed right_unit submonoid.sub)
lemma powers_submonoid:
assumes "g ∈ M" and "invertible g"
shows "submonoid (powers g) M (⋅) 𝟭"
proof
show "powers g ⊆ M" using powers_eq_union_nat_powers nat_powers_subset_carrier assms by auto
next
show "⋀a b. a ∈ powers g ⟹ b ∈ powers g ⟹ a ⋅ b ∈ powers g"
using powers_mult_closed assms by auto
next
show "𝟭 ∈ powers g" using powers_eq_union_nat_powers one_mem_nat_powers by auto
qed
lemma powers_monoid:
assumes "g ∈ M" and "invertible g"
shows "Group_Theory.monoid (powers g) (⋅) 𝟭"
by (smt (verit) monoid.intro Un_iff assms associative in_mono invertible_inverse_closed
monoid.left_unit monoid.right_unit nat_powers_monoid powers_eq_union_nat_powers
powers_mult_closed powers_submonoid submonoid.sub_unit_closed submonoid.subset)
lemma mem_nat_powers_invertible:
assumes "g ∈ M" and "invertible g" and "u ∈ nat_powers g"
shows "monoid.invertible (powers g) (⋅) 𝟭 u"
proof-
obtain n where hu: "u = g ^ n" using assms nat_powers_def by blast
then have "inverse u ∈ powers g" using assms inverse_mult_power_eq
powers_eq_union_nat_powers nat_powers_def by auto
then show ?thesis using hu assms by (metis in_mono inverse_mult_power inverse_mult_power_eq
monoid.invertibleI monoid.nat_powers_subset monoid.powers_monoid monoid_axioms mult_inverse_power)
qed
lemma mem_nat_inv_powers_invertible:
assumes "g ∈ M" and "invertible g" and "u ∈ nat_powers (inverse g)"
shows "monoid.invertible (powers g) (⋅) 𝟭 u"
using assms by (metis inf_sup_aci(5) invertible_inverse_closed invertible_inverse_inverse
invertible_inverse_invertible mem_nat_powers_invertible powers_eq_union_nat_powers)
lemma powers_group:
assumes "g ∈ M" and "invertible g"
shows "Group_Theory.group (powers g) (⋅) 𝟭"
proof-
have "⋀u. u ∈ powers g ⟹ monoid.invertible (powers g) (⋅) 𝟭 u" using assms
mem_nat_inv_powers_invertible mem_nat_powers_invertible powers_eq_union_nat_powers by auto
then show ?thesis using group_def Group_Theory.group_axioms_def assms powers_monoid by metis
qed
lemma nat_powers_ne_one:
assumes "g ∈ M" and "g ≠ 𝟭"
shows "nat_powers g ≠ {𝟭}"
proof-
have "g ∈ nat_powers g" using power_one nat_powers_def assms rangeI by metis
then show ?thesis using assms by blast
qed
lemma powers_ne_one:
assumes "g ∈ M" and "g ≠ 𝟭"
shows "powers g ≠ {𝟭}" using assms nat_powers_ne_one
by (metis all_not_in_conv nat_powers_subset one_mem_nat_powers subset_singleton_iff)
end
context group
begin
lemma powers_subgroup:
assumes "g ∈ G"
shows "subgroup (powers g) G (⋅) 𝟭"
by (simp add: assms powers_group powers_submonoid subgroup.intro)
end
context monoid
begin
subsection‹Definition of the order of an element in a monoid›
definition order
where "order g = (if (∃ n. n > 0 ∧ g ^ n = 𝟭) then Min {n. g ^ n = 𝟭 ∧ n > 0} else ∞)"
definition min_order where "min_order = Min ((order ` M) - {0})"
end
subsection‹Sumset scalar multiplication cardinality lemmas›
context group
begin
lemma card_smul_singleton_right_eq:
assumes "finite A" shows "card (smul A {a}) = (if a ∈ G then card (A ∩ G) else 0)"
proof (cases "a ∈ G")
case True
then have "smul A {a} = (λx. x ⋅ a) ` (A ∩ G)"
by (auto simp: smul_eq)
moreover have "inj_on (λx. x ⋅ a) (A ∩ G)"
by (auto simp: inj_on_def True)
ultimately show ?thesis
by (metis True card_image)
qed (auto simp: smul_eq)
lemma card_smul_singleton_left_eq:
assumes "finite A" shows "card (smul {a} A) = (if a ∈ G then card (A ∩ G) else 0)"
proof (cases "a ∈ G")
case True
then have "smul {a} A = (λx. a ⋅ x) ` (A ∩ G)"
by (auto simp: smul_eq)
moreover have "inj_on (λx. a ⋅ x) (A ∩ G)"
by (auto simp: inj_on_def True)
ultimately show ?thesis
by (metis True card_image)
qed (auto simp: smul_eq)
lemma card_smul_sing_right_le:
assumes "finite A" shows "card (smul A {a}) ≤ card A"
by (simp add: assms card_mono card_smul_singleton_right_eq)
lemma card_smul_sing_left_le:
assumes "finite A" shows "card (smul {a} A) ≤ card A"
by (simp add: assms card_mono card_smul_singleton_left_eq)
lemma card_le_smul_right:
assumes A: "finite A" "a ∈ A" "a ∈ G"
and B: "finite B" "B ⊆ G"
shows "card B ≤ card (smul A B)"
proof -
have "B ⊆ (λ x. (inverse a) ⋅ x) ` smul A B"
using A B
apply (clarsimp simp: smul image_iff)
using Int_absorb2 Int_iff invertible invertible_left_inverse2 by metis
with A B show ?thesis
by (meson finite_smul surj_card_le)
qed
lemma card_le_smul_left:
assumes A: "finite A" "b ∈ B" "b ∈ G"
and B: "finite B" "A ⊆ G"
shows "card A ≤ card (smul A B)"
proof -
have "A ⊆ (λ x. x ⋅ (inverse b)) ` smul A B"
using A B
apply (clarsimp simp: smul image_iff associative)
using Int_absorb2 Int_iff invertible invertible_right_inverse assms(5) by (metis right_unit)
with A B show ?thesis
by (meson finite_smul surj_card_le)
qed
lemma infinite_smul_right:
assumes "A ∩ G ≠ {}" and "infinite (B ∩ G)"
shows "infinite (A ⋯ B)"
proof
assume hfin: "finite (smul A B)"
obtain a where ha: "a ∈ A ∩ G" using assms by auto
then have "finite (smul {a} B)" using hfin by (metis Int_Un_eq(1) finite_subset insert_is_Un
mk_disjoint_insert smul_subset_Un(2))
moreover have "B ∩ G ⊆ (λ x. inverse a ⋅ x) ` smul {a} B"
proof
fix b assume hb: "b ∈ B ∩ G"
then have "b = inverse a ⋅ (a ⋅ b)" using associative ha by (simp add: invertible_left_inverse2)
then show "b ∈ (λ x. inverse a ⋅ x) ` smul {a} B" using smul.simps hb ha by blast
qed
ultimately show False using assms using finite_surj by blast
qed
lemma infinite_smul_left:
assumes "B ∩ G ≠ {}" and "infinite (A ∩ G)"
shows "infinite (A ⋯ B)"
proof
assume hfin: "finite (smul A B)"
obtain b where hb: "b ∈ B ∩ G" using assms by auto
then have "finite (smul A {b})" using hfin by (simp add: rev_finite_subset smul_mono)
moreover have "A ∩ G ⊆ (λ x. x ⋅ inverse b) ` smul A {b}"
proof
fix a assume ha: "a ∈ A ∩ G"
then have "a = (a ⋅ b) ⋅ inverse b" using associative hb
by (metis IntD2 invertible invertible_inverse_closed invertible_right_inverse right_unit)
then show "a ∈ (λ x. x ⋅ inverse b) ` smul A {b}" using smul.simps hb ha by blast
qed
ultimately show False using assms using finite_surj by blast
qed
subsection‹Pointwise set multiplication in a group: auxiliary lemmas›
lemma set_inverse_composition_commute:
assumes "X ⊆ G" and "Y ⊆ G"
shows "inverse ` (X ⋯ Y) = (inverse ` Y) ⋯ (inverse ` X)"
proof
show "inverse ` (X ⋯ Y) ⊆ (inverse ` Y) ⋯ (inverse ` X)"
proof
fix z assume "z ∈ inverse ` (X ⋯ Y)"
then obtain x y where "z = inverse (x ⋅ y)" and "x ∈ X" and "y ∈ Y"
by (smt (verit) image_iff smul.cases)
then show "z ∈ (inverse ` Y) ⋯ (inverse ` X)"
using inverse_composition_commute assms
by (smt (verit) image_eqI in_mono inverse_equality invertible invertibleE smul.simps)
qed
show "(inverse ` Y) ⋯ (inverse ` X) ⊆ inverse ` (X ⋯ Y)"
proof
fix z assume "z ∈ (inverse ` Y) ⋯ (inverse ` X)"
then obtain x y where "x ∈ X" and "y ∈ Y" and "z = inverse y ⋅ inverse x"
using smul.cases image_iff by blast
then show "z ∈ inverse ` (X ⋯ Y)" using inverse_composition_commute assms smul.simps
by (smt (verit) image_iff in_mono invertible)
qed
qed
lemma smul_singleton_eq_contains_nat_powers:
fixes n :: nat
assumes "X ⊆ G" and "g ∈ G" and "X ⋯ {g} = X"
shows "X ⋯ {g ^ n} = X"
proof(induction n)
case 0
then show ?case using power_def assms by auto
next
case (Suc n)
assume hXn: "X ⋯ {g ^ n} = X"
moreover have "X ⋯ {g ^ Suc n} = (X ⋯ {g ^ n}) ⋯ {g}"
proof
show "X ⋯ {g ^ Suc n} ⊆ (X ⋯ {g ^ n}) ⋯ {g}"
proof
fix z assume "z ∈ X ⋯ {g ^ Suc n}"
then obtain x where "z = x ⋅ (g ^ Suc n)" and hx: "x ∈ X" using smul.simps by auto
then have "z = (x ⋅ g ^ n) ⋅ g" using assms associative by (simp add: in_mono power_mem_carrier)
then show "z ∈ (X ⋯ {g ^ n}) ⋯ {g}" using hx assms
by (simp add: power_mem_carrier smul.smulI subsetD)
qed
next
show "(X ⋯ {g ^ n}) ⋯ {g} ⊆ X ⋯ {g ^ Suc n}"
proof
fix z assume "z ∈ (X ⋯ {g ^ n}) ⋯ {g}"
then obtain x where "z = (x ⋅ g ^ n) ⋅ g" and hx: "x ∈ X" using smul.simps by auto
then have "z = x ⋅ g ^ Suc n"
using power_def associative power_mem_carrier assms by (simp add: in_mono)
then show "z ∈ X ⋯ {g ^ Suc n}" using hx assms
by (simp add: power_mem_carrier smul.smulI subsetD)
qed
qed
ultimately show ?case using assms by simp
qed
lemma smul_singleton_eq_contains_inverse_nat_powers:
fixes n :: nat
assumes "X ⊆ G" and "g ∈ G" and "X ⋯ {g} = X"
shows "X ⋯ {(inverse g) ^ n} = X"
proof-
have "(X ⋯ {g}) ⋯ {inverse g} = X"
proof
show "(X ⋯ {g}) ⋯ {inverse g} ⊆ X"
proof
fix z assume "z ∈ (X ⋯ {g}) ⋯ {inverse g}"
then obtain y x where "y ∈ X ⋯ {g}" and "z = y ⋅ inverse g" and "x ∈ X" and "y = x ⋅ g"
using assms smul.simps by (metis empty_iff insert_iff)
then show "z ∈ X" using assms by (simp add: associative subset_eq)
qed
next
show "X ⊆ (X ⋯ {g}) ⋯ {inverse g}"
proof
fix x assume hx: "x ∈ X"
then have "x = x ⋅ g ⋅ inverse g" using assms by (simp add: associative subset_iff)
then show "x ∈ (X ⋯ {g}) ⋯ {inverse g}" using assms smul.simps hx by auto
qed
qed
then have "X ⋯ {inverse g} = X" using assms by auto
then show ?thesis using assms by (simp add: smul_singleton_eq_contains_nat_powers)
qed
lemma smul_singleton_eq_contains_powers:
fixes n :: nat
assumes "X ⊆ G" and "g ∈ G" and "X ⋯ {g} = X"
shows "X ⋯ (powers g) = X" using powers_eq_union_nat_powers smul_subset_Union2
nat_powers_eq_Union smul_singleton_eq_contains_nat_powers
smul_singleton_eq_contains_inverse_nat_powers assms smul_subset_Un2 by auto
end
subsection‹$ecard$ -- extended definition of cardinality of a set›
text‹$ecard$ -- definition of a cardinality of a set taking values in $enat$ -- extended natural numbers, defined to be $\infty$ for infinite sets›
definition ecard where "ecard A = (if finite A then card A else ∞)"
lemma ecard_eq_card_finite:
assumes "finite A"
shows "ecard A = card A"
using assms ecard_def by metis
context monoid
begin
text‹$orderOf$ -- abbreviation for the order of a monoid ›
abbreviation orderOf where "orderOf == ecard"
end
end