Theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend

(*
    File:     Generated_Groups_Extend.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Generated Groups›

theory Generated_Groups_Extend
  imports Miscellaneous_Groups
begin

text ‹This section extends the lemmas and facts about ‹generate›. Starting with a basic fact.›

lemma (in group) generate_sincl:
  "A ⊆ generate G A"
  using generate.incl by fast

text ‹The following lemmas reflect some of the idempotence characteristics of ‹generate› and have
proved useful at several occasions.›

lemma (in group) generate_idem:
  assumes "A ⊆ carrier G"
  shows "generate G (generate G A) = generate G A"
  using assms generateI group.generate_is_subgroup by blast

lemma (in group) generate_idem':
  assumes "A ⊆ carrier G" "B ⊆ carrier G"
  shows "generate G (generate G A ∪ B) = generate G (A ∪ B)"
proof
  show "generate G (generate G A ∪ B) ⊆ generate G (A ∪ B)"
  proof -
    have "generate G A ∪ B ⊆ generate G (A ∪ B)"
    proof -
      have "generate G A ⊆ generate G (A ∪ B)" using mono_generate by simp
      moreover have "B ⊆ generate G (A ∪ B)" by (simp add: generate.incl subset_iff)
      ultimately show ?thesis by simp
    qed
    then have "generate G (generate G A ∪ B) ⊆ generate G (generate G (A ∪ B))"
      using mono_generate by auto
    with generate_idem[of "A ∪ B"] show ?thesis using assms by simp
  qed
  show "generate G (A ∪ B) ⊆ generate G (generate G A ∪ B)"
  proof -
    have "A ⊆ generate G A" using generate.incl by fast
    thus ?thesis using mono_generate[of "A ∪ B" "generate G A ∪ B"] by blast
  qed
qed

lemma (in group) generate_idem'_right:
  assumes "A ⊆ carrier G" "B ⊆ carrier G"
  shows "generate G (A ∪ generate G B) = generate G (A ∪ B)"
  using generate_idem'[OF assms(2) assms(1)] by (simp add: sup_commute)

lemma (in group) generate_idem_Un:
  assumes "A ⊆ carrier G"
  shows "generate G (⋃x∈A. generate G {x}) = generate G A"
proof
  have "A ⊆ (⋃x∈A. generate G {x})" using generate.incl by force
  thus "generate G A ⊆ generate G (⋃x∈A. generate G {x})" using mono_generate by presburger
  have "⋀x. x ∈ A ⟹ generate G {x} ⊆ generate G A" using mono_generate by auto
  hence "(⋃x∈A. generate G {x}) ⊆ generate G A" by blast
  thus "generate G (⋃x∈A. generate G {x}) ⊆ generate G A"
    using generate_idem[OF assms] mono_generate by blast
qed

lemma (in group) generate_idem_fUn:
  assumes "f A ⊆ carrier G"
  shows "generate G (⋃ {generate G {x} |x. x ∈ f A}) = generate G (f A)"
proof
  have "f A ⊆ ⋃ {generate G {x} |x. x ∈ f A}"
  proof
    fix x
    assume x: "x ∈ f A"
    have "x ∈ generate G {x}" using generate.incl by fast
    thus "x ∈ ⋃ {generate G {x} |x. x ∈ f A}" using x by blast
  qed
  thus "generate G (f A) ⊆ generate G (⋃ {generate G {x} |x. x ∈ f A})" using mono_generate by auto
  have "⋀x. x ∈ f A ⟹ generate G {x} ⊆ generate G (f A)" using mono_generate by simp
  hence "(⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)" by blast
  with mono_generate[OF this] show "generate G (⋃ {generate G {x} |x. x ∈ f A}) ⊆ generate G (f A)"
    using generate_idem[OF assms] by simp
qed

lemma (in group) generate_idem_fim_Un:
  assumes "⋃(f ` A) ⊆ carrier G"
  shows "generate G (⋃S ∈ A. generate G (f S)) = generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)})"
proof

  have "⋀S. S ∈ A ⟹ generate G (f S) = generate G (⋃ {generate G {x} |x. x ∈ f S})"
    using generate_idem_fUn[of f] assms by blast
  then have "generate G (⋃S ∈ A. generate G (f S))
           = generate G (⋃S ∈ A. generate G (⋃ {generate G {x} |x. x ∈ f S}))" by simp

  have "⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)} ⊆ (⋃S∈A. generate G (f S))"
  proof
    fix x
    assume x: "x ∈ ⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}"
    then obtain a where a: "x ∈ generate G {a}" "a ∈ ⋃ (f ` A)" by blast
    then obtain M where M: "a ∈ f M" "M ∈ A" by blast
    then have "generate G {a} ⊆ generate G (f M)"
      using generate.incl[OF M(1), of G] mono_generate[of "{a}" "generate G (f M)"]
            generate_idem assms by auto
    then have "x ∈ generate G (f M)" using a by blast
    thus "x ∈ (⋃S∈A. generate G (f S))" using M by blast
  qed
  thus "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}) ⊆ generate G (⋃S∈A. generate G (f S))"
    using mono_generate by simp
  have a: "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f ` A))"
  proof -
    have "⋀S. S ∈ A ⟹ generate G (f S) ⊆ generate G (⋃ (f ` A))"
      using mono_generate[of _ "⋃ (f ` A)"] by blast
    then have "(⋃S∈A. generate G (f S)) ⊆ generate G (⋃ (f ` A))" by blast
    then have "generate G (⋃S∈A. generate G (f S)) ⊆ generate G (generate G (⋃ (f ` A)))"
      using mono_generate by meson
    thus "generate G (⋃S∈A. generate G (f S)) ⊆  generate G (⋃ (f ` A))"
      using generate_idem assms by blast
  qed
  have "⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)} = (⋃x∈⋃ (f ` A). generate G {x})" by blast
  with generate_idem_Un[OF assms]
  have "generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)}) = generate G (⋃ (f ` A))" by simp
  with a show "generate G (⋃S∈A. generate G (f S))
             ⊆ generate G (⋃ {generate G {x} |x. x ∈ ⋃ (f ` A)})" by blast
qed

text ‹The following two rules allow for convenient proving of the equality of two generated sets.›

lemma (in group) generate_eqI:
  assumes "A ⊆ carrier G" "B ⊆ carrier G" "A ⊆ generate G B" "B ⊆ generate G A"
  shows "generate G A = generate G B"
  using assms generate_idem by (metis generate_idem' inf_sup_aci(5) sup.absorb2)

lemma (in group) generate_one_switched_eqI:
  assumes "A ⊆ carrier G" "a ∈ A" "B = (A - {a}) ∪ {b}"
  and "b ∈ generate G A" "a ∈ generate G B"
  shows "generate G A = generate G B"
proof(intro generate_eqI)
  show "A ⊆ carrier G" by fact
  show "B ⊆ carrier G" using assms generate_incl by blast
  show "A ⊆ generate G B" using assms generate_sincl[of B] by blast
  show "B ⊆ generate G A" using assms generate_sincl[of A] by blast
qed

lemma (in group) generate_subset_eqI:
  assumes "A ⊆ carrier G" "B ⊆ A" "A - B ⊆ generate G B"
  shows "generate G A = generate G B"
proof
  show "generate G B ⊆ generate G A" by (intro mono_generate, fact)
  show "generate G A ⊆ generate G B"
  proof(subst generate_idem[of "B", symmetric])
    show "generate G A ⊆ generate G (generate G B)"
      by (intro mono_generate, use assms generate_sincl[of B] in auto)
  qed (use assms in blast)
qed

text ‹Some smaller lemmas about ‹generate›.›

lemma (in group) generate_subset_change_eqI:
  assumes "A ⊆ carrier G" "B ⊆ carrier G" "C ⊆ carrier G" "generate G A = generate G B"
  shows "generate G (A ∪ C) = generate G (B ∪ C)"
  by (metis assms generate_idem')

lemma (in group) generate_subgroup_id:
  assumes "subgroup H G"
  shows "generate G H = H"
  using assms generateI by auto

lemma (in group) generate_consistent':
  assumes "subgroup H G" "A ⊆ H"
  shows "∀x ∈ A. generate G {x} = generate (G⦇carrier := H⦈) {x}"
  using generate_consistent assms by auto

lemma (in group) generate_singleton_one:
  assumes "generate G {a} = {𝟭}"
  shows "a = 𝟭"
  using generate.incl[of a "{a}" G] assms by auto

lemma (in group) generate_inv_eq:
  assumes "a ∈ carrier G"
  shows "generate G {a} = generate G {inv a}"
  by (intro generate_eqI;
      use assms generate.inv[of a] generate.inv[of "inv a" "{inv a}" G] inv_inv[OF assms] in auto)

lemma (in group) generate_eq_imp_subset:
  assumes "generate G A = generate G B"
  shows "A ⊆ generate G B"
  using generate.incl assms by fast


text ‹The neutral element does not play a role when generating a subgroup.›

lemma (in group) generate_one_irrel:
  "generate G A = generate G (A ∪ {𝟭})"
proof
  show "generate G A ⊆ generate G (A ∪ {𝟭})" by (intro mono_generate, blast)
  show "generate G (A ∪ {𝟭}) ⊆ generate G A"
  proof(rule subsetI)
    show "x ∈ generate G A" if "x ∈ generate G (A ∪ {𝟭})" for x using that
      by (induction rule: generate.induct;
          use generate.one generate.incl generate.inv generate.eng in auto)
  qed
qed

lemma (in group) generate_one_irrel':
  "generate G A = generate G (A - {𝟭})"
  using generate_one_irrel by (metis Un_Diff_cancel2)

text ‹Also, we can express the subgroup generated by a singleton with finite order using just its
powers up to its order.›

lemma (in group) generate_nat_pow:
  assumes "ord a ≠ 0" "a ∈ carrier G"
  shows "generate G {a} = {a [^] k |k. k ∈ {0..ord a - 1}}"
  using assms generate_pow_nat ord_elems_inf_carrier by auto

lemma (in group) generate_nat_pow':
  assumes "ord a ≠ 0" "a ∈ carrier G"
  shows "generate G {a} = {a [^] k |k. k ∈ {1..ord a}}"
proof -
  have "{a [^] k |k. k ∈ {1..ord a}} = {a [^] k |k. k ∈ {0..ord a - 1}}"
  proof -
    have "a [^] k ∈ {a [^] k |k. k ∈ {0..ord a - 1}}" if "k ∈ {1..ord a}" for k
      using that pow_nat_mod_ord[OF assms(2, 1), of "ord a"] assms by (cases "k = ord a"; force)
    moreover have "a [^] k ∈ {a [^] k |k. k ∈ {1..ord a}}" if "k ∈ {0..ord a - 1}" for k
    proof(cases "k = 0")
      case True
      hence "a [^] k = a [^] ord a" using pow_ord_eq_1[OF assms(2)] by auto
      moreover have "ord a ∈ {1..ord a}"
        using assms unfolding atLeastAtMost_def atLeast_def atMost_def by auto
      ultimately show ?thesis by blast
    next
      case False
      then show ?thesis using that by auto
    qed
    ultimately show ?thesis by blast
  qed
  with generate_nat_pow[OF assms] show ?thesis by simp
qed

end