Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Weak lemma: HOL-Algebra.Multiplicative_Group.g...


view this post on Zulip Email Gateway (Nov 13 2020 at 18:30):

From: Jakub Kądziołka <kuba@kadziolka.net>
Greetings,

currently, generate_pow_card assumes "finite (carrier G)". This is
unnecessary, as evidenced by the modified proof I'm including below.
I modified two lemmas above it to only assume that a relevant subgroup
is finite, instead of the entire group. Also, the removed assumption
leads to a simpler proof of ord_dvd_group_order.

Regards,
Jakub Kądziołka

theory Scratch
imports "HOL-Algebra.Algebra"
begin

context group begin

lemma ord_elems_inf_carrier:
assumes "a ∈ carrier G" "ord a ≠ 0"
shows "{a[^]x | x. x ∈ (UNIV :: nat set)} = {a[^]x | x. x ∈ {0 .. ord a - 1}}" (is "?L = ?R")
proof
show "?R ⊆ ?L" by blast
{ fix y assume "y ∈ ?L"
then obtain x::nat where x: "y = a[^]x" by auto
define r q where "r = x mod ord a" and "q = x div ord a"
then have "x = q * ord a + r"
by (simp add: div_mult_mod_eq)
hence "y = (a[^]ord a)[^]q ⊗ a[^]r"
using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
hence "y = a[^]r" using assms by simp
have "r < ord a" using assms by (simp add: r_def)
hence "r ∈ {0 .. ord a - 1}" by (force simp: r_def)
hence "y ∈ {a[^]x | x. x ∈ {0 .. ord a - 1}}" using ‹y=a[^]r› by blast
}
thus "?L ⊆ ?R" by auto
qed

lemma generate_pow_nat:
assumes a: "a ∈ carrier G" and "ord a ≠ 0"
shows "generate G { a } = { a [^] k | k. k ∈ (UNIV :: nat set) }"
proof
show "{ a [^] k | k. k ∈ (UNIV :: nat set) } ⊆ generate G { a }"
proof
fix b assume "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
then obtain k :: nat where "b = a [^] k" by blast
hence "b = a [^] (int k)"
by (simp add: int_pow_int)
thus "b ∈ generate G { a }"
unfolding generate_pow[OF a] by blast
qed
next
show "generate G { a } ⊆ { a [^] k | k. k ∈ (UNIV :: nat set) }"
proof
fix b assume "b ∈ generate G { a }"
then obtain k :: int where k: "b = a [^] k"
unfolding generate_pow[OF a] by blast
show "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }"
proof (cases "k < 0")
assume "¬ k < 0"
hence "b = a [^] (nat k)"
by (simp add: k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
using k a by (auto simp: int_pow_neg)
obtain m where m: "ord a * m ≥ nat (- k)"
by (metis assms(2) dvd_imp_le dvd_triv_right le_zero_eq mult_eq_0_iff not_gr_zero)
hence "a [^] (ord a * m) = 𝟭"
by (metis a nat_pow_one nat_pow_pow pow_ord_eq_1)
then obtain k' :: nat where "(a [^] (nat (- k))) ⊗ (a [^] k') = 𝟭"
using m a nat_le_iff_add nat_pow_mult by auto
hence "b = a [^] k'"
using b a by (metis inv_unique' nat_pow_closed nat_pow_comm)
thus "b ∈ { a [^] k | k. k ∈ (UNIV :: nat set) }" by blast
qed
qed
qed

lemma generate_pow_card:
assumes a: "a ∈ carrier G"
shows "ord a = card (generate G { a })"
proof (cases "ord a = 0")
case True
then have "infinite (carrier (subgroup_generated G {a}))"
using infinite_cyclic_subgroup_order[OF a] by auto
then have "infinite (generate G {a})"
unfolding subgroup_generated_def
using a by simp
then show ?thesis
using ord a = 0 by auto
next
case False
note finite_subgroup = this
then have "generate G { a } = (([^]) a) ` {0..ord a - 1}"
using generate_pow_nat ord_elems_inf_carrier a by auto
hence "card (generate G {a}) = card {0..ord a - 1}"
using ord_inj[OF a] card_image by metis
also have "... = ord a" using finite_subgroup by auto
finally show ?thesis..
qed

lemma ord_dvd_group_order:
assumes "a ∈ carrier G"
shows "(ord a) dvd (order G)"
proof -
show ?thesis
using lagrange[OF generate_is_subgroup[of "{a}"]] assms
unfolding generate_pow_card[OF assms]
by (metis dvd_triv_right empty_subsetI insert_subset)
qed

end
end


Last updated: Jul 15 2022 at 23:21 UTC