Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Tools/VSCode/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quellcode-Bibliothek Generated_Groups.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Generated_Groups.thy
    Author:     Paulo Emílio de Vilhena
*)

section \<open>Generated Groups\<close>

theory Generated_Groups
  imports Group Coset

begin

subsection \<open>Generated Groups\<close>

inductive_set generate :: "('a, 'b) monoid_scheme \ 'a set \ 'a set"
  for G and H where
    one:  "\\<^bsub>G\<^esub> \ generate G H"
  | incl: "h \ H \ h \ generate G H"
  | inv:  "h \ H \ inv\<^bsub>G\<^esub> h \ generate G H"
  | eng:  "h1 \ generate G H \ h2 \ generate G H \ h1 \\<^bsub>G\<^esub> h2 \ generate G H"

subsubsection \<open>Basic Properties\<close>

lemma (in group) generate_consistent:
  assumes "K \ H" "subgroup H G" shows "generate (G \ carrier := H \) K = generate G K"
proof
  show "generate (G \ carrier := H \) K \ generate G K"
  proof
    fix h assume "h \ generate (G \ carrier := H \) K" thus "h \ generate G K"
    proof (induction, simp add: one, simp_all add: incl[of _ K G] eng)
      case inv thus ?case
        using m_inv_consistent assms generate.inv[of _ K G] by auto
    qed
  qed
next
  show "generate G K \ generate (G \ carrier := H \) K"
  proof
    note gen_simps = one incl eng
    fix h assume "h \ generate G K" thus "h \ generate (G \ carrier := H \) K"
      using gen_simps[where ?G = "G \ carrier := H \"]
    proof (induction, auto)
      fix h assume "h \ K" thus "inv h \ generate (G \ carrier := H \) K"
        using m_inv_consistent assms generate.inv[of h K "G \ carrier := H \"] by auto
    qed
  qed
qed

lemma (in group) generate_in_carrier:
  assumes "H \ carrier G" and "h \ generate G H" shows "h \ carrier G"
  using assms(2,1) by (induct h rule: generate.induct) (auto)

lemma (in group) generate_incl:
  assumes "H \ carrier G" shows "generate G H \ carrier G"
  using generate_in_carrier[OF assms(1)] by auto

lemma (in group) generate_m_inv_closed:
  assumes "H \ carrier G" and "h \ generate G H" shows "(inv h) \ generate G H"
  using assms(2,1)
proof (induction rule: generate.induct, auto simp add: one inv incl)
  fix h1 h2
  assume h1: "h1 \ generate G H" "inv h1 \ generate G H"
     and h2: "h2 \ generate G H" "inv h2 \ generate G H"
  hence "inv (h1 \ h2) = (inv h2) \ (inv h1)"
    by (meson assms generate_in_carrier group.inv_mult_group is_group)
  thus "inv (h1 \ h2) \ generate G H"
    using generate.eng[OF h2(2) h1(2)] by simp
qed

lemma (in group) generate_is_subgroup:
  assumes "H \ carrier G" shows "subgroup (generate G H) G"
  using subgroup.intro[OF generate_incl eng one generate_m_inv_closed] assms by auto

lemma (in group) mono_generate:
  assumes "K \ H" shows "generate G K \ generate G H"
proof
  fix h assume "h \ generate G K" thus "h \ generate G H"
    using assms by (induction) (auto simp add: one incl inv eng)
qed

lemma (in group) generate_subgroup_incl:
  assumes "K \ H" "subgroup H G" shows "generate G K \ H"
  using group.generate_incl[OF subgroup_imp_group[OF assms(2)], of K] assms(1)
  by (simp add: generate_consistent[OF assms])

lemma (in group) generate_minimal:
  assumes "H \ carrier G" shows "generate G H = \ { H'. subgroup H' G \ H \ H' }"
  using generate_subgroup_incl generate_is_subgroup[OF assms] incl[of _ H] by blast

lemma (in group) generateI:
  assumes "subgroup E G" "H \ E" and "\K. \ subgroup K G; H \ K \ \ E \ K"
  shows "E = generate G H"
proof -
  have subset: "H \ carrier G"
    using subgroup.subset assms by auto
  show ?thesis
    using assms unfolding generate_minimal[OF subset] by blast
qed

lemma (in group) normal_generateI:
  assumes "H \ carrier G" and "\h g. \ h \ H; g \ carrier G \ \ g \ h \ (inv g) \ H"
  shows "generate G H \ G"
proof (rule normal_invI[OF generate_is_subgroup[OF assms(1)]])
  fix g h assume g: "g \ carrier G" show "h \ generate G H \ g \ h \ (inv g) \ generate G H"
  proof (induct h rule: generate.induct)
    case one thus ?case
      using g generate.one by auto
  next
    case incl show ?case
      using generate.incl[OF assms(2)[OF incl g]] .
  next
    case (inv h)
    hence h: "h \ carrier G"
      using assms(1) by auto
    hence "inv (g \ h \ (inv g)) = g \ (inv h) \ (inv g)"
      using g by (simp add: inv_mult_group m_assoc)
    thus ?case
      using generate_m_inv_closed[OF assms(1) generate.incl[OF assms(2)[OF inv g]]] by simp
  next
    case (eng h1 h2)
    note in_carrier = eng(1,3)[THEN generate_in_carrier[OF assms(1)]]
    have "g \ (h1 \ h2) \ inv g = (g \ h1 \ inv g) \ (g \ h2 \ inv g)"
      using in_carrier g by (simp add: inv_solve_left m_assoc)
    thus ?case
      using generate.eng[OF eng(2,4)] by simp
  qed
qed

lemma (in group) subgroup_int_pow_closed:
  assumes "subgroup H G" "h \ H" shows "h [^] (k :: int) \ H"
  using group.int_pow_closed[OF subgroup_imp_group[OF assms(1)]] assms(2)
  unfolding int_pow_consistent[OF assms] by simp

lemma (in group) generate_pow:
  assumes "a \ carrier G" shows "generate G { a } = { a [^] (k :: int) | k. k \ UNIV }"
proof
  show "{ a [^] (k :: int) | k. k \ UNIV } \ generate G { a }"
    using subgroup_int_pow_closed[OF generate_is_subgroup[of "{ a }"] incl[of a]] assms by auto
next
  show "generate G { a } \ { a [^] (k :: int) | k. k \ UNIV }"
  proof
    fix h assume "h \ generate G { a }" hence "\k :: int. h = a [^] k"
    proof (induction)
      case one
      then show ?case
        using int_pow_0 [of G] by metis
    next
      case (incl h)
      then show ?case
        by (metis assms int_pow_1 singletonD)
    next
      case (inv h)
      then show ?case
        by (metis assms int_pow_1 int_pow_neg singletonD)
    next
      case (eng h1 h2)
      then show ?case
        using assms by (metis int_pow_mult)
    qed
    then show "h \ { a [^] (k :: int) | k. k \ UNIV }"
      by blast
  qed
qed

corollary (in group) generate_one: "generate G { \ } = { \ }"
  using generate_pow[of "\", OF one_closed] by simp

corollary (in group) generate_empty: "generate G {} = { \ }"
  using mono_generate[of "{}" "{ \ }"] generate.one unfolding generate_one by auto

lemma (in group_hom)
  "subgroup K G \ subgroup (h ` K) H"
  using subgroup_img_is_subgroup by auto

lemma (in group_hom) generate_img:
  assumes "K \ carrier G" shows "generate H (h ` K) = h ` (generate G K)"
proof
  have "h ` K \ h ` (generate G K)"
    using incl[of _ K G] by auto
  thus "generate H (h ` K) \ h ` (generate G K)"
    using generate_subgroup_incl subgroup_img_is_subgroup[OF G.generate_is_subgroup[OF assms]] by auto
next
  show "h ` (generate G K) \ generate H (h ` K)"
  proof
    fix a assume "a \ h ` (generate G K)"
    then obtain k where "k \ generate G K" "a = h k"
      by blast
    show "a \ generate H (h ` K)"
      using \<open>k \<in> generate G K\<close> unfolding \<open>a = h k\<close>
    proof (induct k, auto simp add: generate.one[of H] generate.incl[of _ "h ` K" H])
      case (inv k) show ?case
        using assms generate.inv[of "h k" "h ` K" H] inv by auto
    next
      case eng show ?case
        using generate.eng[OF eng(2,4)] eng(1,3)[THEN G.generate_in_carrier[OF assms]] by auto
    qed
  qed
qed

subsection \<open>Derived Subgroup\<close>

subsubsection \<open>Definitions\<close>

abbreviation derived_set :: "('a, 'b) monoid_scheme \ 'a set \ 'a set"
  where "derived_set G H \
           \<Union>h1 \<in> H. (\<Union>h2 \<in> H. { h1 \<otimes>\<^bsub>G\<^esub> h2 \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h2) })"

definition derived :: "('a, 'b) monoid_scheme \ 'a set \ 'a set" where
  "derived G H = generate G (derived_set G H)"

subsubsection \<open>Basic Properties\<close>

lemma (in group) derived_set_incl:
  assumes "K \ H" "subgroup H G" shows "derived_set G K \ H"
  using assms(1) subgroupE(3-4)[OF assms(2)] by (auto simp add: subset_iff)

lemma (in group) derived_incl:
  assumes "K \ H" "subgroup H G" shows "derived G K \ H"
  using generate_subgroup_incl[OF derived_set_incl] assms unfolding derived_def by auto

lemma (in group) derived_set_in_carrier:
  assumes "H \ carrier G" shows "derived_set G H \ carrier G"
  using derived_set_incl[OF assms subgroup_self] .

lemma (in group) derived_in_carrier:
  assumes "H \ carrier G" shows "derived G H \ carrier G"
  using derived_incl[OF assms subgroup_self] .

lemma (in group) exp_of_derived_in_carrier:
  assumes "H \ carrier G" shows "(derived G ^^ n) H \ carrier G"
  using assms derived_in_carrier by (induct n) (auto)

lemma (in group) derived_is_subgroup:
  assumes "H \ carrier G" shows "subgroup (derived G H) G"
  unfolding derived_def using generate_is_subgroup[OF derived_set_in_carrier[OF assms]] .

lemma (in group) exp_of_derived_is_subgroup:
  assumes "subgroup H G" shows "subgroup ((derived G ^^ n) H) G"
  using assms derived_is_subgroup subgroup.subset by (induct n) (auto)

lemma (in group) exp_of_derived_is_subgroup':
  assumes "H \ carrier G" shows "subgroup ((derived G ^^ (Suc n)) H) G"
  using assms derived_is_subgroup[OF subgroup.subset] derived_is_subgroup by (induct n) (auto)

lemma (in group) mono_derived_set:
  assumes "K \ H" shows "derived_set G K \ derived_set G H"
  using assms by auto

lemma (in group) mono_derived:
  assumes "K \ H" shows "derived G K \ derived G H"
  unfolding derived_def using mono_generate[OF mono_derived_set[OF assms]] .

lemma (in group) mono_exp_of_derived:
  assumes "K \ H" shows "(derived G ^^ n) K \ (derived G ^^ n) H"
  using assms mono_derived by (induct n) (auto)

lemma (in group) derived_set_consistent:
  assumes "K \ H" "subgroup H G" shows "derived_set (G \ carrier := H \) K = derived_set G K"
  using m_inv_consistent[OF assms(2)] assms(1) by (auto simp add: subset_iff)

lemma (in group) derived_consistent:
  assumes "K \ H" "subgroup H G" shows "derived (G \ carrier := H \) K = derived G K"
  using generate_consistent[OF derived_set_incl] derived_set_consistent assms by (simp add: derived_def)

lemma (in comm_group) derived_eq_singleton:
  assumes "H \ carrier G" shows "derived G H = { \ }"
proof (cases "derived_set G H = {}")
  case True show ?thesis
    using generate_empty unfolding derived_def True by simp
next
  case False
  have aux_lemma: "h \ derived_set G H \ h = \" for h
    using assms by (auto simp add: subset_iff)
       (metis (no_types, lifting) m_comm m_closed inv_closed inv_solve_right l_inv l_inv_ex)
  have "derived_set G H = { \ }"
  proof
    show "derived_set G H \ { \ }"
      using aux_lemma by auto
  next
    obtain h where h: "h \ derived_set G H"
      using False by blast
    thus "{ \ } \ derived_set G H"
      using aux_lemma[OF h] by auto
  qed
  thus ?thesis
    using generate_one unfolding derived_def by auto
qed

lemma (in group) derived_is_normal:
  assumes "H \ G" shows "derived G H \ G"
proof -
  interpret H: normal H G
    using assms .

  show ?thesis
    unfolding derived_def
  proof (rule normal_generateI[OF derived_set_in_carrier[OF H.subset]])
    fix h g assume "h \ derived_set G H" and g: "g \ carrier G"
    then obtain h1 h2 where h: "h1 \ H" "h2 \ H" "h = h1 \ h2 \ inv h1 \ inv h2"
      by auto
    hence in_carrier: "h1 \ carrier G" "h2 \ carrier G" "g \ carrier G"
      using H.subset g by auto
    have "g \ h \ inv g =
           g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g"
      unfolding h(3) by (simp add: in_carrier m_assoc)
    also have " ... =
          (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> (g \<otimes> inv h1 \<otimes> inv g) \<otimes> (g \<otimes> inv h2 \<otimes> inv g)"
      using in_carrier m_assoc inv_closed m_closed by presburger
    finally have "g \ h \ inv g =
          (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)"
      by (simp add: in_carrier inv_mult_group m_assoc)
    thus "g \ h \ inv g \ derived_set G H"
      using h(1-2)[THEN H.inv_op_closed2[OF g]] by auto
  qed
qed

lemma (in group) normal_self: "carrier G \ G"
  by (rule normal_invI[OF subgroup_self], simp)

corollary (in group) derived_self_is_normal: "derived G (carrier G) \ G"
  using derived_is_normal[OF normal_self] .

corollary (in group) derived_subgroup_is_normal:
  assumes "subgroup H G" shows "derived G H \ G \ carrier := H \"
  using group.derived_self_is_normal[OF subgroup_imp_group[OF assms]]
        derived_consistent[OF _ assms]
  by simp

corollary (in group) derived_quot_is_group: "group (G Mod (derived G (carrier G)))"
  using normal.factorgroup_is_group[OF derived_self_is_normal] by auto

lemma (in group) derived_quot_is_comm_group: "comm_group (G Mod (derived G (carrier G)))"
proof (rule group.group_comm_groupI[OF derived_quot_is_group], simp add: FactGroup_def)
  interpret DG: normal "derived G (carrier G)" G
    using derived_self_is_normal .

  fix H K assume "H \ rcosets derived G (carrier G)" and "K \ rcosets derived G (carrier G)"
  then obtain g1 g2
    where g1: "g1 \ carrier G" "H = derived G (carrier G) #> g1"
      and g2: "g2 \ carrier G" "K = derived G (carrier G) #> g2"
    unfolding RCOSETS_def by auto
  hence "H <#> K = derived G (carrier G) #> (g1 \ g2)"
    by (simp add: DG.rcos_sum)
  also have " ... = derived G (carrier G) #> (g2 \ g1)"
  proof -
    have "derived G (carrier G) #> (g1 \ g2) \ derived G (carrier G) #> (g2 \ g1)"
      if g1: "g1 \ carrier G" and g2: "g2 \ carrier G" for g1 g2
    proof
      fix h assume "h \ derived G (carrier G) #> (g1 \ g2)"
      then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)"
        using DG.subset unfolding r_coset_def by auto
      hence "h = g' \ (g1 \ g2) \ (inv g1 \ inv g2 \ g2 \ g1)"
        using g1 g2 by (simp add: m_assoc)
      hence "h = (g' \ (g1 \ g2 \ inv g1 \ inv g2)) \ (g2 \ g1)"
        using h(1) g1 g2 inv_closed m_assoc m_closed by presburger
      moreover have "g1 \ g2 \ inv g1 \ inv g2 \ derived G (carrier G)"
        using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast
      hence "g' \ (g1 \ g2 \ inv g1 \ inv g2) \ derived G (carrier G)"
        using DG.m_closed[OF h(2)] by simp
      ultimately show "h \ derived G (carrier G) #> (g2 \ g1)"
        unfolding r_coset_def by blast
    qed
    thus ?thesis
      using g1(1) g2(1) by auto
  qed
  also have " ... = K <#> H"
    by (simp add: g1 g2 DG.rcos_sum)
  finally show "H <#> K = K <#> H" .
qed

corollary (in group) derived_quot_of_subgroup_is_comm_group:
  assumes "subgroup H G" shows "comm_group ((G \ carrier := H \) Mod (derived G H))"
  using group.derived_quot_is_comm_group[OF subgroup_imp_group[OF assms]]
        derived_consistent[OF _ assms]
  by simp

proposition (in group) derived_minimal:
  assumes "H \ G" and "comm_group (G Mod H)" shows "derived G (carrier G) \ H"
proof -
  interpret H: normal H G
    using assms(1) .

  show ?thesis
    unfolding derived_def
  proof (rule generate_subgroup_incl[OF _ H.subgroup_axioms])
    show "derived_set G (carrier G) \ H"
    proof
      fix h assume "h \ derived_set G (carrier G)"
      then obtain g1 g2 where h: "g1 \ carrier G" "g2 \ carrier G" "h = g1 \ g2 \ inv g1 \ inv g2"
        by auto
      have "H #> (g1 \ g2) = (H #> g1) <#> (H #> g2)"
        by (simp add: h(1-2) H.rcos_sum)
      also have " ... = (H #> g2) <#> (H #> g1)"
        using comm_groupE(4)[OF assms(2)] h(1-2) unfolding FactGroup_def RCOSETS_def by auto
      also have " ... = H #> (g2 \ g1)"
        by (simp add: h(1-2) H.rcos_sum)
      finally have "H #> (g1 \ g2) = H #> (g2 \ g1)" .
      then obtain h' where "h' \<in> H" "\<one> \<otimes> (g1 \<otimes> g2) = h' \<otimes> (g2 \<otimes> g1)"
        using H.one_closed unfolding r_coset_def by blast
      thus "h \ H"
        using h m_assoc by auto
    qed
  qed
qed

proposition (in group) derived_of_subgroup_minimal:
  assumes "K \ G \ carrier := H \" "subgroup H G" and "comm_group ((G \ carrier := H \) Mod K)"
  shows "derived G H \ K"
  using group.derived_minimal[OF subgroup_imp_group[OF assms(2)] assms(1,3)]
        derived_consistent[OF _ assms(2)]
  by simp

lemma (in group_hom) derived_img:
  assumes "K \ carrier G" shows "derived H (h ` K) = h ` (derived G K)"
proof -
  have "derived_set H (h ` K) = h ` (derived_set G K)"
  proof
    show "derived_set H (h ` K) \ h ` derived_set G K"
    proof
      fix a assume "a \ derived_set H (h ` K)"
      then obtain k1 k2
        where "k1 \ K" "k2 \ K" "a = (h k1) \\<^bsub>H\<^esub> (h k2) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k2)"
        by auto
      hence "a = h (k1 \ k2 \ inv k1 \ inv k2)"
        using assms by (simp add: subset_iff)
      from this \<open>k1 \<in> K\<close> and \<open>k2 \<in> K\<close> show "a \<in> h ` derived_set G K" by auto
    qed
  next
    show "h ` (derived_set G K) \ derived_set H (h ` K)"
    proof
      fix a assume "a \ h ` (derived_set G K)"
      then obtain k1 k2 where "k1 \ K" "k2 \ K" "a = h (k1 \ k2 \ inv k1 \ inv k2)"
        by auto
      hence "a = (h k1) \\<^bsub>H\<^esub> (h k2) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k2)"
        using assms by (simp add: subset_iff)
      from this \<open>k1 \<in> K\<close> and \<open>k2 \<in> K\<close> show "a \<in> derived_set H (h ` K)" by auto
    qed
  qed
  thus ?thesis
    unfolding derived_def using generate_img[OF G.derived_set_in_carrier[OF assms]] by simp
qed

lemma (in group_hom) exp_of_derived_img:
  assumes "K \ carrier G" shows "(derived H ^^ n) (h ` K) = h ` ((derived G ^^ n) K)"
  using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto)

subsubsection \<open>Generated subgroup of a group\<close>

definition subgroup_generated :: "('a, 'b) monoid_scheme \ 'a set \ ('a, 'b) monoid_scheme"
  where "subgroup_generated G S = G\carrier := generate G (carrier G \ S)\"

lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \ S)"
  by (auto simp: subgroup_generated_def)

lemma (in group) subgroup_generated_subset_carrier_subset:
   "S \ carrier G \ S \ carrier(subgroup_generated G S)"
  by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI)

lemma (in group) subgroup_generated_minimal:
   "\subgroup H G; S \ H\ \ carrier(subgroup_generated G S) \ H"
  by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2)

lemma (in group) carrier_subgroup_generated_subset:
   "carrier (subgroup_generated G A) \ carrier G"
  apply (clarsimp simp: carrier_subgroup_generated)
  by (meson Int_lower1 generate_in_carrier)

lemma (in group) group_subgroup_generated [simp]: "group (subgroup_generated G S)"
    unfolding subgroup_generated_def
    by (simp add: generate_is_subgroup subgroup_imp_group)

lemma (in group) abelian_subgroup_generated:
  assumes "comm_group G"
  shows "comm_group (subgroup_generated G S)" (is "comm_group ?GS")
proof (rule group.group_comm_groupI)
  show "Group.group ?GS"
    by simp
next
  fix x y
  assume "x \ carrier ?GS" "y \ carrier ?GS"
  with assms show "x \\<^bsub>?GS\<^esub> y = y \\<^bsub>?GS\<^esub> x"
    apply (simp add: subgroup_generated_def)
    by (meson Int_lower1 comm_groupE(4) generate_in_carrier)
qed

lemma (in group) subgroup_of_subgroup_generated:
  assumes "H \ B" "subgroup H G"
    shows "subgroup H (subgroup_generated G B)"
proof unfold_locales
  fix x
  assume "x \ H"
  with assms show "inv\<^bsub>subgroup_generated G B\<^esub> x \ H"
    unfolding subgroup_generated_def
    by (metis IntI Int_commute Int_lower2 generate.incl generate_is_subgroup m_inv_consistent subgroup_def subsetCE)
next
  show "H \ carrier (subgroup_generated G B)"
    using assms apply (auto simp: carrier_subgroup_generated)
    by (metis Int_iff generate.incl inf.orderE subgroup.mem_carrier)
qed (use assms in \<open>auto simp: subgroup_generated_def subgroup_def\<close>)

lemma carrier_subgroup_generated_alt:
  assumes "Group.group G" "S \ carrier G"
  shows "carrier (subgroup_generated G S) = \{H. subgroup H G \ carrier G \ S \ H}"
  using assms by (auto simp: group.generate_minimal subgroup_generated_def)

lemma one_subgroup_generated [simp]: "\\<^bsub>subgroup_generated G S\<^esub> = \\<^bsub>G\<^esub>"
  by (auto simp: subgroup_generated_def)

lemma mult_subgroup_generated [simp]: "mult (subgroup_generated G S) = mult G"
  by (auto simp: subgroup_generated_def)

lemma (in group) inv_subgroup_generated [simp]:
  assumes "f \ carrier (subgroup_generated G S)"
  shows "inv\<^bsub>subgroup_generated G S\<^esub> f = inv f"
proof (rule group.inv_equality)
  show "Group.group (subgroup_generated G S)"
    by simp
  have [simp]: "f \ carrier G"
    by (metis Int_lower1 assms carrier_subgroup_generated generate_in_carrier)
  show "inv f \\<^bsub>subgroup_generated G S\<^esub> f = \\<^bsub>subgroup_generated G S\<^esub>"
    by (simp add: assms)
  show "f \ carrier (subgroup_generated G S)"
    using assms by (simp add: generate.incl subgroup_generated_def)
  show "inv f \ carrier (subgroup_generated G S)"
    using assms by (simp add: subgroup_generated_def generate_m_inv_closed)
qed

lemma subgroup_generated_restrict [simp]:
   "subgroup_generated G (carrier G \ S) = subgroup_generated G S"
  by (simp add: subgroup_generated_def)

lemma (in subgroup) carrier_subgroup_generated_subgroup [simp]:
  "carrier (subgroup_generated G H) = H"
  by (auto simp: generate.incl carrier_subgroup_generated elim: generate.induct)

lemma (in group) subgroup_subgroup_generated_iff:
   "subgroup H (subgroup_generated G B) \ subgroup H G \ H \ carrier(subgroup_generated G B)"
(is "?lhs = ?rhs")
proof
  assume L: ?lhs
  then have Hsub: "H \ generate G (carrier G \ B)"
    by (simp add: subgroup_def subgroup_generated_def)
  then have H: "H \ carrier G" "H \ carrier(subgroup_generated G B)"
    unfolding carrier_subgroup_generated
    using generate_incl by blast+
  with Hsub have "subgroup H G"
    by (metis Int_commute Int_lower2 L carrier_subgroup_generated generate_consistent
        generate_is_subgroup inf.orderE subgroup.carrier_subgroup_generated_subgroup subgroup_generated_def)
  with H show ?rhs
    by blast
next
  assume ?rhs
  then show ?lhs
    by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl)
qed

lemma (in group) subgroup_subgroup_generated:
   "subgroup (carrier(subgroup_generated G S)) G"
  using group.subgroup_self group_subgroup_generated subgroup_subgroup_generated_iff by blast

lemma pow_subgroup_generated:
   "pow (subgroup_generated G S) = (pow G :: 'a \ nat \ 'a)"
proof -
  have "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n" for x and n::nat
    by (induction n) auto
  then show ?thesis
    by force
qed

lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S"
proof -
  have *: "\A. carrier G \ A \ carrier (subgroup_generated (subgroup_generated G A) A)"
    by (metis (no_types, opaque_lifting) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff)
  show ?thesis
  apply (auto intro!: monoid.equality)
    using group.carrier_subgroup_generated_subset group_subgroup_generated apply blast
     apply (metis (no_types, opaque_lifting) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal
        subgroup_generated_restrict subgroup_subgroup_generated_iff subset_eq)
    apply (simp add: subgroup_generated_def)
    done
qed

lemma (in group) int_pow_subgroup_generated:
  fixes n::int
  assumes "x \ carrier (subgroup_generated G S)"
  shows "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n"
proof -
  have "x [^] nat (- n) \ carrier (subgroup_generated G S)"
    by (metis assms group.is_monoid group_subgroup_generated monoid.nat_pow_closed pow_subgroup_generated)
  then show ?thesis
    by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated)
qed

lemma kernel_from_subgroup_generated [simp]:
  "subgroup S G \ kernel (subgroup_generated G S) H f = kernel G H f \ S"
  using subgroup.carrier_subgroup_generated_subgroup subgroup.subset
  by (fastforce simp add: kernel_def set_eq_iff)

lemma kernel_to_subgroup_generated [simp]:
  "kernel G (subgroup_generated H S) f = kernel G H f"
  by (simp add: kernel_def)

subsection \<open>And homomorphisms\<close>

lemma (in group) hom_from_subgroup_generated:
   "h \ hom G H \ h \ hom(subgroup_generated G A) H"
  apply (simp add: hom_def carrier_subgroup_generated Pi_iff)
  apply (metis group.generate_in_carrier inf_le1 is_group)
  done

lemma hom_into_subgroup:
   "\h \ hom G G'; h ` (carrier G) \ H\ \ h \ hom G (subgroup_generated G' H)"
  by (auto simp: hom_def carrier_subgroup_generated Pi_iff generate.incl image_subset_iff)

lemma hom_into_subgroup_eq_gen:
    "group G \
     h \<in> hom K (subgroup_generated G H)
\<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> carrier(subgroup_generated G H)"
  using group.carrier_subgroup_generated_subset [of G H] by (auto simp: hom_def)

lemma hom_into_subgroup_eq:
   "\subgroup H G; group G\
    \<Longrightarrow> (h \<in> hom K (subgroup_generated G H) \<longleftrightarrow> h \<in> hom K G \<and> h ` (carrier K) \<subseteq> H)"
  by (simp add: hom_into_subgroup_eq_gen image_subset_iff subgroup.carrier_subgroup_generated_subgroup)

lemma (in group_hom) hom_between_subgroups:
  assumes "h ` A \ B"
  shows "h \ hom (subgroup_generated G A) (subgroup_generated H B)"
proof -
  have [simp]: "group G" "group H"
    by (simp_all add: G.is_group H.is_group)
  have "x \ generate G (carrier G \ A) \ h x \ generate H (carrier H \ B)" for x
  proof (induction x rule: generate.induct)
    case (incl h)
    then show ?case
      by (meson IntE IntI assms generate.incl hom_closed image_subset_iff)
  next
    case (inv h)
    then show ?case
      by (metis G.inv_closed G.inv_inv IntE IntI assms generate.simps hom_inv image_subset_iff local.inv_closed)
  next
    case (eng h1 h2)
    then show ?case
      by (metis G.generate_in_carrier generate.simps inf.cobounded1 local.hom_mult)
  qed (auto simp: generate.intros)
  then have "h ` carrier (subgroup_generated G A) \ carrier (subgroup_generated H B)"
    using group.carrier_subgroup_generated_subset [of G A]
    by (auto simp: carrier_subgroup_generated)
  then show ?thesis
    by (simp add: hom_into_subgroup_eq_gen group.hom_from_subgroup_generated homh)
qed

lemma (in group_hom) subgroup_generated_by_image:
  assumes "S \ carrier G"
  shows "carrier (subgroup_generated H (h ` S)) = h ` (carrier(subgroup_generated G S))"
proof
  have "x \ generate H (carrier H \ h ` S) \ x \ h ` generate G (carrier G \ S)" for x
  proof (erule generate.induct)
    show "\\<^bsub>H\<^esub> \ h ` generate G (carrier G \ S)"
      using generate.one by force
  next
    fix f
    assume "f \ carrier H \ h ` S"
    with assms show "f \ h ` generate G (carrier G \ S)" "inv\<^bsub>H\<^esub> f \ h ` generate G (carrier G \ S)"
       apply (auto simp: Int_absorb1 generate.incl)
      apply (metis generate.simps hom_inv imageI subsetCE)
      done
  next
    fix h1 h2
    assume
      "h1 \ generate H (carrier H \ h ` S)" "h1 \ h ` generate G (carrier G \ S)"
      "h2 \ generate H (carrier H \ h ` S)" "h2 \ h ` generate G (carrier G \ S)"
    then show "h1 \\<^bsub>H\<^esub> h2 \ h ` generate G (carrier G \ S)"
      using H.subgroupE(4) group.generate_is_subgroup subgroup_img_is_subgroup
      by (simp add: G.generate_is_subgroup)
  qed
  then
  show "carrier (subgroup_generated H (h ` S)) \ h ` carrier (subgroup_generated G S)"
    by (auto simp: carrier_subgroup_generated)
next
  have "h ` S \ carrier H"
    by (metis (no_types) assms hom_closed image_subset_iff subsetCE)
  then show "h ` carrier (subgroup_generated G S) \ carrier (subgroup_generated H (h ` S))"
    apply (clarsimp simp: carrier_subgroup_generated)
    by (metis Int_absorb1 assms generate_img imageI)
qed

lemma (in group_hom) iso_between_subgroups:
  assumes "h \ iso G H" "S \ carrier G" "h ` S = T"
  shows "h \ iso (subgroup_generated G S) (subgroup_generated H T)"
  using assms
  by (metis G.carrier_subgroup_generated_subset Group.iso_iff hom_between_subgroups inj_on_subset subgroup_generated_by_image subsetI)

lemma (in group) subgroup_generated_group_carrier:
  "subgroup_generated G (carrier G) = G"
proof (rule monoid.equality)
  show "carrier (subgroup_generated G (carrier G)) = carrier G"
    by (simp add: subgroup.carrier_subgroup_generated_subgroup subgroup_self)
qed (auto simp: subgroup_generated_def)

lemma iso_onto_image:
  assumes "group G" "group H"
  shows
   "f \ iso G (subgroup_generated H (f ` carrier G)) \ f \ hom G H \ inj_on f (carrier G)"
  using assms
  apply (auto simp: iso_def bij_betw_def hom_into_subgroup_eq_gen carrier_subgroup_generated hom_carrier generate.incl Int_absorb1 Int_absorb2)
  by (metis group.generateI group.subgroupE(1) group.subgroup_self group_hom.generate_img group_hom.intro group_hom_axioms.intro)

lemma (in group) iso_onto_image:
   "group H \ f \ iso G (subgroup_generated H (f ` carrier G)) \ f \ mon G H"
  by (simp add: mon_def epi_def hom_into_subgroup_eq_gen iso_onto_image)

end

quality100%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.