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/HOL/Algebra/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 12 kB

SSL Sylow.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/Sylow.thy
    Author:     Florian Kammueller, with new proofs by L C Paulson
*)

theory Sylow
  imports Coset Exponent
begin

text \<open>See also \<^cite>\<open>"Kammueller-Paulson:1999"\<close>.\<close>

text \<open>The combinatorial argument is in theory \<open>Exponent\<close>.\<close>

lemma le_extend_mult: "\0 < c; a \ b\ \ a \ b * c" for c :: nat
  using gr0_conv_Suc by fastforce

locale sylow = group +
  fixes p and a and m and calM and RelM
  assumes prime_p: "prime p"
    and order_G: "order G = (p^a) * m"
    and finite_G[iff]: "finite (carrier G)"
  defines "calM \ {s. s \ carrier G \ card s = p^a}"
    and "RelM \ {(N1, N2). N1 \ calM \ N2 \ calM \ (\g \ carrier G. N1 = N2 #> g)}"
begin

lemma RelM_subset: "RelM \ calM \ calM"
  by (auto simp only: RelM_def)

lemma RelM_refl_on: "refl_on calM RelM"
  by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric])

lemma RelM_sym: "sym RelM"
  unfolding sym_def RelM_def calM_def
  using coset_mult_assoc coset_mult_one r_inv_ex
  by (smt (verit, best) case_prod_conv mem_Collect_eq)

lemma RelM_trans: "trans RelM"
  by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)

lemma RelM_equiv: "equiv calM RelM"
  using RelM_subset RelM_refl_on RelM_sym RelM_trans by (intro equivI)

lemma M_subset_calM_prep: "M' \ calM // RelM \ M' \ calM"
  unfolding RelM_def by (blast elim!: quotientE)

end

subsection \<open>Main Part of the Proof\<close>

locale sylow_central = sylow +
  fixes H and M1 and M
  assumes M_in_quot: "M \ calM // RelM"
    and not_dvd_M: "\ (p ^ Suc (multiplicity p m) dvd card M)"
    and M1_in_M: "M1 \ M"
  defines "H \ {g. g \ carrier G \ M1 #> g = M1}"
begin

lemma M_subset_calM: "M \ calM"
  by (simp add: M_in_quot M_subset_calM_prep)

lemma card_M1: "card M1 = p^a"
  using M1_in_M M_subset_calM calM_def by blast

lemma exists_x_in_M1: "\x. x \ M1"
  using prime_p [THEN prime_gt_Suc_0_nat] card_M1 one_in_subset by fastforce

lemma M1_subset_G [simp]: "M1 \ carrier G"
  using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast

lemma M1_inj_H: "\f \ H\M1. inj_on f H"
proof -
  from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1"..
  show ?thesis
  proof
    have "m1 \ carrier G"
      by (simp add: m1M M1_subset_G [THEN subsetD])
    then show "inj_on (\z\H. m1 \ z) H"
      by (simp add: H_def inj_on_def)
    show "restrict ((\) m1) H \ H \ M1"
      using H_def m1M rcosI by auto
  qed
qed

end

subsection \<open>Discharging the Assumptions of \<open>sylow_central\<close>\<close>

context sylow
begin

lemma EmptyNotInEquivSet: "{} \ calM // RelM"
  using RelM_equiv in_quotient_imp_non_empty by blast

lemma existsM1inM: "M \ calM // RelM \ \M1. M1 \ M"
  using RelM_equiv equiv_Eps_in by blast

lemma zero_less_o_G: "0 < order G"
  by (simp add: order_def card_gt_0_iff carrier_not_empty)

lemma zero_less_m: "m > 0"
  using zero_less_o_G by (simp add: order_G)

lemma card_calM: "card calM = (p^a) * m choose p^a"
  by (simp add: calM_def n_subsets order_G [symmetric] order_def)

lemma zero_less_card_calM: "card calM > 0"
  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)

lemma max_p_div_calM: "\ (p ^ Suc (multiplicity p m) dvd card calM)"
proof
  assume "p ^ Suc (multiplicity p m) dvd card calM"
  with zero_less_card_calM prime_p
  have "Suc (multiplicity p m) \ multiplicity p (card calM)"
    by (intro multiplicity_geI) auto
  then show False
    by (simp add: card_calM const_p_fac prime_p zero_less_m)
qed

lemma finite_calM: "finite calM"
  unfolding calM_def by (rule finite_subset [where B = "Pow (carrier G)"]) auto

lemma lemma_A1: "\M \ calM // RelM. \ (p ^ Suc (multiplicity p m) dvd card M)"
  using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast

end

subsubsection \<open>Introduction and Destruct Rules for \<open>H\<close>\<close>

context sylow_central
begin

lemma H_I: "\g \ carrier G; M1 #> g = M1\ \ g \ H"
  by (simp add: H_def)

lemma H_into_carrier_G: "x \ H \ x \ carrier G"
  by (simp add: H_def)

lemma in_H_imp_eq: "g \ H \ M1 #> g = M1"
  by (simp add: H_def)

lemma H_m_closed: "\x \ H; y \ H\ \ x \ y \ H"
  by (simp add: H_def coset_mult_assoc [symmetric])

lemma H_not_empty: "H \ {}"
  by (force simp add: H_def intro: exI [of _ \<one>])

lemma H_is_subgroup: "subgroup H G"
proof (rule subgroupI)
  show "H \ carrier G"
    using H_into_carrier_G by blast
  show "\a. a \ H \ inv a \ H"
    by (metis H_I H_into_carrier_G M1_subset_G coset_mult_assoc coset_mult_one in_H_imp_eq inv_closed r_inv)
  show "\a b. \a \ H; b \ H\ \ a \ b \ H"
    by (blast intro: H_m_closed)
qed (use H_not_empty in auto)

lemma rcosetGM1g_subset_G: "\g \ carrier G; x \ M1 #> g\ \ x \ carrier G"
  by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])

lemma finite_M1: "finite M1"
  by (rule finite_subset [OF M1_subset_G finite_G])

lemma finite_rcosetGM1g: "g \ carrier G \ finite (M1 #> g)"
  using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast

lemma M1_cardeq_rcosetGM1g: "g \ carrier G \ card (M1 #> g) = card M1"
  by (metis M1_subset_G card_rcosets_equal rcosetsI)

lemma M1_RelM_rcosetGM1g:
  assumes "g \ carrier G"
  shows "(M1, M1 #> g) \ RelM"
proof -
  have "M1 #> g \ carrier G"
    by (simp add: assms r_coset_subset_G)
  moreover have "card (M1 #> g) = p ^ a"
    using assms by (simp add: card_M1 M1_cardeq_rcosetGM1g)
  moreover have "\h\carrier G. M1 = M1 #> g #> h"
    by (metis assms M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
  ultimately show ?thesis
    by (simp add: RelM_def calM_def card_M1)
qed

end

subsection \<open>Equal Cardinalities of \<open>M\<close> and the Set of Cosets\<close>

text \<open>Injections between \<^term>\<open>M\<close> and \<^term>\<open>rcosets\<^bsub>G\<^esub> H\<close> show that
their cardinalities are equal.\<close>

lemma ElemClassEquiv: "\equiv A r; C \ A // r\ \ \x \ C. \y \ C. (x, y) \ r"
  unfolding equiv_def quotient_def sym_def trans_def by blast

context sylow_central
begin

lemma M_elem_map: "M2 \ M \ \g. g \ carrier G \ M1 #> g = M2"
  using M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]
  by (simp add: RelM_def) (blast dest!: bspec)

lemmas M_elem_map_carrier = M_elem_map [THEN someI_ex, THEN conjunct1]

lemmas M_elem_map_eq = M_elem_map [THEN someI_ex, THEN conjunct2]

lemma M_funcset_rcosets_H:
  "(\x\M. H #> (SOME g. g \ carrier G \ M1 #> g = x)) \ M \ rcosets H"
  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)

lemma inj_M_GmodH: "\f \ M \ rcosets H. inj_on f M"
proof
  let ?inv = "\x. SOME g. g \ carrier G \ M1 #> g = x"
  show "inj_on (\x\M. H #> ?inv x) M"
  proof (rule inj_onI, simp)
    fix x y
    assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \ M" "y \ M"
    have "x = M1 #> ?inv x"
      by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
    also have "\ = M1 #> ?inv y"
    proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
      show "H #> ?inv x \ inv (?inv y) = H"
        by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
    qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
    also have "\ = y"
      using M_elem_map_eq \<open>y \<in> M\<close> by simp
    finally show "x=y" .
  qed
  show "(\x\M. H #> ?inv x) \ M \ rcosets H"
    by (rule M_funcset_rcosets_H)
qed

end

subsubsection \<open>The Opposite Injection\<close>

context sylow_central
begin

lemma H_elem_map: "H1 \ rcosets H \ \g. g \ carrier G \ H #> g = H1"
  by (auto simp: RCOSETS_def)

lemmas H_elem_map_carrier = H_elem_map [THEN someI_ex, THEN conjunct1]

lemmas H_elem_map_eq = H_elem_map [THEN someI_ex, THEN conjunct2]

lemma rcosets_H_funcset_M:
  "(\C \ rcosets H. M1 #> (SOME g. g \ carrier G \ H #> g = C)) \ rcosets H \ M"
  using in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g]
  by (simp add: M1_in_M H_elem_map_carrier RCOSETS_def)

lemma inj_GmodH_M: "\g \ rcosets H\M. inj_on g (rcosets H)"
proof
  let ?inv = "\x. SOME g. g \ carrier G \ H #> g = x"
  show "inj_on (\C\rcosets H. M1 #> ?inv C) (rcosets H)"
  proof (rule inj_onI, simp)
    fix x y
    assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \ rcosets H" "y \ rcosets H"
    have "x = H #> ?inv x"
      by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
    also have "\ = H #> ?inv y"
    proof (rule coset_mult_inv1 [OF coset_join2])
      show "?inv x \ inv (?inv y) \ carrier G"
        by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
      then show "(?inv x) \ inv (?inv y) \ H"
        by (simp add: H_I H_elem_map_carrier xy coset_mult_inv2 eq)
      show "H \ carrier G"
        by (simp add: H_is_subgroup subgroup.subset)
    qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
    also have "\ = y"
      by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
    finally show "x=y" .
  qed
  show "(\C\rcosets H. M1 #> ?inv C) \ rcosets H \ M"
    using rcosets_H_funcset_M by blast
qed

lemma calM_subset_PowG: "calM \ Pow (carrier G)"
  by (auto simp: calM_def)

lemma finite_M: "finite M"
  by (metis M_subset_calM finite_calM rev_finite_subset)

lemma cardMeqIndexH: "card M = card (rcosets H)"
  using inj_M_GmodH inj_GmodH_M
  by (metis H_is_subgroup card_bij finite_G finite_M finite_UnionD rcosets_part_G)

lemma index_lem: "card M * card H = order G"
  by (simp add: cardMeqIndexH lagrange H_is_subgroup)

lemma card_H_eq: "card H = p^a"
proof (rule antisym)
  show "p^a \ card H"
  proof (rule dvd_imp_le)
    have "p ^ (a + multiplicity p m) dvd card M * card H"
      by (simp add: index_lem multiplicity_dvd order_G power_add)
    then show "p ^ a dvd card H"
      using div_combine not_dvd_M prime_p by blast
    show "0 < card H"
      by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
  qed
next
  show "card H \ p^a"
    using M1_inj_H card_M1 card_inj finite_M1 by fastforce
qed

end

lemma (in sylow) sylow_thm: "\H. subgroup H G \ card H = p^a"
proof -
  obtain M where M: "M \ calM // RelM" "\ (p ^ Suc (multiplicity p m) dvd card M)"
    using lemma_A1 by blast
  then obtain M1 where "M1 \ M"
    by (metis existsM1inM)
  define H where "H \ {g. g \ carrier G \ M1 #> g = M1}"
  with M \<open>M1 \<in> M\<close>
  interpret sylow_central G p a m calM RelM H M1 M
    by unfold_locales (auto simp add: H_def calM_def RelM_def)
  show ?thesis
    using H_is_subgroup card_H_eq by blast
qed

text \<open>Needed because the locale's automatic definition refers to
  \<^term>\<open>semigroup G\<close> and \<^term>\<open>group_axioms G\<close> rather than
  simply to \<^term>\<open>group G\<close>.\<close>
lemma sylow_eq: "sylow G p a m \ group G \ sylow_axioms G p a m"
  by (simp add: sylow_def group_def)

subsection \<open>Sylow's Theorem\<close>

theorem sylow_thm:
  "\prime p; group G; order G = (p^a) * m; finite (carrier G)\
    \<Longrightarrow> \<exists>H. subgroup H G \<and> card H = p^a"
  by (rule sylow.sylow_thm [of G p a m]) (simp add: sylow_eq sylow_axioms_def)

end

quality99%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.