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 (xA. generate G {x}) = generate G A"
proof
  have "A  (xA. generate G {x})" using generate.incl by force
  thus "generate G A  generate G (xA. generate G {x})" using mono_generate by presburger
  have "x. x  A  generate G {x}  generate G A" using mono_generate by auto
  hence "(xA. generate G {x})  generate G A" by blast
  thus "generate G (xA. 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)}  (SA. 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  (SA. generate G (f S))" using M by blast
  qed
  thus "generate G ( {generate G {x} |x. x   (f ` A)})  generate G (SA. generate G (f S))"
    using mono_generate by simp
  have a: "generate G (SA. 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 "(SA. generate G (f S))  generate G ( (f ` A))" by blast
    then have "generate G (SA. generate G (f S))  generate G (generate G ( (f ` A)))"
      using mono_generate by meson
    thus "generate G (SA. 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 (SA. 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 (Gcarrier := 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