Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] subgroup generates itself

Email Gateway (Jan 06 2025 at 15:27):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,

I needed to show that generators generate the group they generate as a
subgroup. This is akin to m_inv_consistent et al.
One of those claims that are too obvious until one tries to formalize
them.  The proof is below.

1. Is this of a general interest?
2. Is there a simpler proof? (One could try the infimum condition
   gen_subgroup_is_smallest_containing. The corresponding proof would
   apparently be of at least a similar complexity.)

Stepan

lemma (in group) gen_span_consistent: assumes "X ⊆ carrier G"
  shows "⟨X⟩⇘G⦇carrier := (⟨X⟩⇘G⇙)⦈⇙ = ⟨X⟩" (is "⟨X⟩⇘?S⇙ = ⟨X⟩")
proof
  have "X ⊆ ⟨X⟩⇘G⇙"
    using gen_span.gen_gens subset_eq by meson
  interpret span: group ?S
    using subgroup_imp_group[OF gen_subgroup_is_subgroup[OF assms]].
  show "⟨X⟩⇘?S⇙ ⊆ ⟨X⟩"
    using span.subgroupE(1)[OF span.gen_subgroup_is_subgroup] ‹X ⊆
⟨X⟩⇘G⇙› by simp
  show "⟨X⟩ ⊆ ⟨X⟩⇘?S⇙"
  proof
    fix x
    assume "x ∈ ⟨X⟩"
    then show "x ∈ ⟨X⟩⇘?S⇙"
    apply (rule gen_span.induct)
    using gen_span.simps apply fastforce
    using gen_span.gen_gens  apply fastforce
    using gen_subgroup_is_subgroup[OF assms] gen_span.gen_inv
m_inv_consistent  apply fastforce
    using gen_subgroup_is_subgroup[OF assms] gen_span.gen_mult
subgroup_mult_equality by fastforce
qed

Last updated: Jan 30 2025 at 04:21 UTC