--- a/src/HOL/Algebra/Algebra.thy Tue Apr 02 15:16:56 2019 +0200
+++ b/src/HOL/Algebra/Algebra.thy Tue Apr 02 16:55:56 2019 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Algebra/Algebra.thy *)
theory Algebra
- imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
+ imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Elementary_Groups
Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
begin
end
--- a/src/HOL/Algebra/Coset.thy Tue Apr 02 15:16:56 2019 +0200
+++ b/src/HOL/Algebra/Coset.thy Tue Apr 02 16:55:56 2019 +0200
@@ -203,6 +203,10 @@
"\<lbrakk>h \<in> hom G H; group G; group H\<rbrakk> \<Longrightarrow> inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
using group_hom.inj_on_one_iff group_hom.intro group_hom_axioms.intro by blast
+lemma mon_iff_hom_one:
+ "\<lbrakk>group G; group H\<rbrakk> \<Longrightarrow> f \<in> mon G H \<longleftrightarrow> f \<in> hom G H \<and> (\<forall>x. x \<in> carrier G \<and> f x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>\<^bsub>G\<^esub>)"
+ by (auto simp: mon_def inj_on_one_iff')
+
lemma (in group_hom) iso_iff: "h \<in> iso G H \<longleftrightarrow> carrier H \<subseteq> h ` carrier G \<and> (\<forall>x\<in>carrier G. h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)"
by (auto simp: iso_def bij_betw_def inj_on_one_iff)
@@ -374,7 +378,7 @@
subsection \<open>Normal subgroups\<close>
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
- by (simp add: normal_def subgroup_def)
+ by (rule normal.axioms(1))
lemma (in group) normalI:
"subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
@@ -396,6 +400,14 @@
shows "x \<otimes> h \<otimes> (inv x) \<in> H"
using assms inv_op_closed1 by (metis inv_closed inv_inv)
+lemma (in comm_group) normal_iff_subgroup:
+ "N \<lhd> G \<longleftrightarrow> subgroup N G"
+proof
+ assume "subgroup N G"
+ then show "N \<lhd> G"
+ by unfold_locales (auto simp: subgroupE subgroup.one_closed l_coset_def r_coset_def m_comm subgroup.mem_carrier)
+qed (simp add: normal_imp_subgroup)
+
text\<open>Alternative characterization of normal subgroups\<close>
lemma (in group) normal_inv_iff:
@@ -925,8 +937,14 @@
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
done
-lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
- by (simp add: FactGroup_def)
+lemma carrier_FactGroup: "carrier(G Mod N) = (\<lambda>x. r_coset G N x) ` carrier G"
+ by (auto simp: FactGroup_def RCOSETS_def)
+
+lemma one_FactGroup [simp]: "one(G Mod N) = N"
+ by (auto simp: FactGroup_def)
+
+lemma mult_FactGroup [simp]: "monoid.mult (G Mod N) = set_mult G"
+ by (auto simp: FactGroup_def)
lemma (in normal) inv_FactGroup:
assumes "X \<in> carrier (G Mod H)"
@@ -951,6 +969,79 @@
by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
+lemma (in comm_group) set_mult_commute:
+ assumes "N \<subseteq> carrier G" "x \<in> rcosets N" "y \<in> rcosets N"
+ shows "x <#> y = y <#> x"
+ using assms unfolding set_mult_def RCOSETS_def
+ by auto (metis m_comm r_coset_subset_G subsetCE)+
+
+lemma (in comm_group) abelian_FactGroup:
+ assumes "subgroup N G" shows "comm_group(G Mod N)"
+proof (rule group.group_comm_groupI)
+ have "N \<lhd> G"
+ by (simp add: assms normal_iff_subgroup)
+ then show "Group.group (G Mod N)"
+ by (simp add: normal.factorgroup_is_group)
+ fix x :: "'a set" and y :: "'a set"
+ assume "x \<in> carrier (G Mod N)" "y \<in> carrier (G Mod N)"
+ then show "x \<otimes>\<^bsub>G Mod N\<^esub> y = y \<otimes>\<^bsub>G Mod N\<^esub> x"
+ apply (simp add: FactGroup_def subgroup_def)
+ apply (rule set_mult_commute)
+ using assms apply (auto simp: subgroup_def)
+ done
+qed
+
+
+lemma FactGroup_universal:
+ assumes "h \<in> hom G H" "N \<lhd> G"
+ and h: "\<And>x y. \<lbrakk>x \<in> carrier G; y \<in> carrier G; r_coset G N x = r_coset G N y\<rbrakk> \<Longrightarrow> h x = h y"
+ obtains g
+ where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+ obtain g where g: "\<And>x. x \<in> carrier G \<Longrightarrow> h x = g(r_coset G N x)"
+ using h function_factors_left_gen [of "\<lambda>x. x \<in> carrier G" "r_coset G N" h] by blast
+ show thesis
+ proof
+ show "g \<in> hom (G Mod N) H"
+ proof (rule homI)
+ show "g (u \<otimes>\<^bsub>G Mod N\<^esub> v) = g u \<otimes>\<^bsub>H\<^esub> g v"
+ if "u \<in> carrier (G Mod N)" "v \<in> carrier (G Mod N)" for u v
+ proof -
+ from that
+ obtain x y where xy: "x \<in> carrier G" "u = r_coset G N x" "y \<in> carrier G" "v = r_coset G N y"
+ by (auto simp: carrier_FactGroup)
+ then have "h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
+ by (metis hom_mult [OF \<open>h \<in> hom G H\<close>])
+ then show ?thesis
+ by (metis Coset.mult_FactGroup xy \<open>N \<lhd> G\<close> g group.subgroup_self normal.axioms(2) normal.rcos_sum subgroup_def)
+ qed
+ qed (use \<open>h \<in> hom G H\<close> in \<open>auto simp: carrier_FactGroup Pi_iff hom_def simp flip: g\<close>)
+ qed (auto simp flip: g)
+qed
+
+
+lemma (in normal) FactGroup_pow:
+ fixes k::nat
+ assumes "a \<in> carrier G"
+ shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+proof (induction k)
+ case 0
+ then show ?case
+ by (simp add: r_coset_def)
+next
+ case (Suc k)
+ then show ?case
+ by (simp add: assms rcos_sum)
+qed
+
+lemma (in normal) FactGroup_int_pow:
+ fixes k::int
+ assumes "a \<in> carrier G"
+ shows "pow (FactGroup G H) (r_coset G H a) k = r_coset G H (pow G a k)"
+ by (metis Group.group.axioms(1) image_eqI is_group monoid.nat_pow_closed int_pow_def2 assms
+ FactGroup_pow carrier_FactGroup inv_FactGroup rcos_inv)
+
+
subsection\<open>The First Isomorphism Theorem\<close>
text\<open>The quotient by the kernel of a homomorphism is isomorphic to the
@@ -983,6 +1074,30 @@
qed
+lemma (in group_hom) FactGroup_universal_kernel:
+ assumes "N \<lhd> G" and h: "N \<subseteq> kernel G H h"
+ obtains g where "g \<in> hom (G Mod N) H" "\<And>x. x \<in> carrier G \<Longrightarrow> g(r_coset G N x) = h x"
+proof -
+ have "h x = h y"
+ if "x \<in> carrier G" "y \<in> carrier G" "r_coset G N x = r_coset G N y" for x y
+ proof -
+ have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> N"
+ using \<open>N \<lhd> G\<close> group.rcos_self normal.axioms(2) normal_imp_subgroup
+ subgroup.rcos_module_imp that by fastforce
+ with h have xy: "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y \<in> kernel G H h"
+ by blast
+ have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = h (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> y)"
+ by (simp add: that)
+ also have "\<dots> = \<one>\<^bsub>H\<^esub>"
+ using xy by (simp add: kernel_def)
+ finally have "h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub>(h y) = \<one>\<^bsub>H\<^esub>" .
+ then show ?thesis
+ using H.inv_equality that by fastforce
+ qed
+ with FactGroup_universal [OF homh \<open>N \<lhd> G\<close>] that show thesis
+ by metis
+qed
+
lemma (in group_hom) FactGroup_the_elem_mem:
assumes X: "X \<in> carrier (G Mod (kernel G H h))"
shows "the_elem (h`X) \<in> carrier H"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Elementary_Groups.thy Tue Apr 02 16:55:56 2019 +0200
@@ -0,0 +1,382 @@
+section \<open>Elementary Group Constructions\<close>
+
+(* Title: HOL/Algebra/Elementary_Groups.thy
+ Author: LC Paulson, ported from HOL Light
+*)
+
+theory Elementary_Groups
+imports Generated_Groups
+begin
+
+subsection\<open>Direct sum/product lemmas\<close>
+
+locale group_disjoint_sum = group G + AG: subgroup A G + BG: subgroup B G for G (structure) and A B
+begin
+
+lemma subset_one: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> A \<inter> B = {\<one>}"
+ by auto
+
+lemma sub_id_iff: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>)"
+ (is "?lhs = ?rhs")
+proof -
+ have "?lhs = (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>)"
+ proof (intro ballI iffI impI)
+ fix x y
+ assume "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B" "x \<otimes> inv y = \<one>"
+ then have "y = x"
+ using group.inv_equality group_l_invI by fastforce
+ then show "x = \<one> \<and> inv y = \<one>"
+ using \<open>A \<inter> B \<subseteq> {\<one>}\<close> \<open>x \<in> A\<close> \<open>y \<in> B\<close> by fastforce
+ next
+ assume "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> inv y = \<one> \<longrightarrow> x = \<one> \<and> inv y = \<one>"
+ then show "A \<inter> B \<subseteq> {\<one>}"
+ by auto
+ qed
+ also have "\<dots> = ?rhs"
+ by (metis BG.mem_carrier BG.subgroup_axioms inv_inv subgroup_def)
+ finally show ?thesis .
+qed
+
+lemma cancel: "A \<inter> B \<subseteq> {\<one>} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+ (is "?lhs = ?rhs")
+proof -
+ have "(\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>) = ?rhs"
+ (is "?med = _")
+ proof (intro ballI iffI impI)
+ fix x y x' y'
+ assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = \<one> \<longrightarrow> x = \<one> \<and> y = \<one>"
+ and AB: "x \<in> A" "y \<in> B" "x' \<in> A" "y' \<in> B" and eq: "x \<otimes> y = x' \<otimes> y'"
+ then have carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G"
+ using AG.subset BG.subset by auto
+ then have "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = inv x' \<otimes> (x \<otimes> y) \<otimes> inv y'"
+ by (simp add: m_assoc)
+ also have "\<dots> = \<one>"
+ using carr by (simp add: eq) (simp add: m_assoc)
+ finally have 1: "inv x' \<otimes> x \<otimes> (y \<otimes> inv y') = \<one>" .
+ show "x = x' \<and> y = y'"
+ using * [OF _ _ 1] AB by simp (metis carr inv_closed inv_inv local.inv_equality)
+ next
+ fix x y
+ assume * [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y'"
+ and xy: "x \<in> A" "y \<in> B" "x \<otimes> y = \<one>"
+ show "x = \<one> \<and> y = \<one>"
+ by (rule *) (use xy in auto)
+ qed
+ then show ?thesis
+ by (simp add: sub_id_iff)
+qed
+
+lemma commuting_imp_normal1:
+ assumes sub: "carrier G \<subseteq> A <#> B"
+ and mult: "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+ shows "A \<lhd> G"
+proof -
+ have AB: "A \<subseteq> carrier G \<and> B \<subseteq> carrier G"
+ by (simp add: AG.subset BG.subset)
+ have "A #> x = x <# A"
+ if x: "x \<in> carrier G" for x
+ proof -
+ obtain a b where xeq: "x = a \<otimes> b" and "a \<in> A" "b \<in> B" and carr: "a \<in> carrier G" "b \<in> carrier G"
+ using x sub AB by (force simp: set_mult_def)
+ have Ab: "A <#> {b} = {b} <#> A"
+ using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close> mult
+ by (force simp: set_mult_def m_assoc subset_iff)
+ have "A #> x = A <#> {a \<otimes> b}"
+ by (auto simp: l_coset_eq_set_mult r_coset_eq_set_mult xeq)
+ also have "\<dots> = A <#> {a} <#> {b}"
+ using AB \<open>a \<in> A\<close> \<open>b \<in> B\<close>
+ by (auto simp: set_mult_def m_assoc subset_iff)
+ also have "\<dots> = {a} <#> A <#> {b}"
+ by (metis AG.rcos_const AG.subgroup_axioms \<open>a \<in> A\<close> coset_join3 is_group l_coset_eq_set_mult r_coset_eq_set_mult subgroup.mem_carrier)
+ also have "\<dots> = {a} <#> {b} <#> A"
+ by (simp add: is_group carr group.set_mult_assoc AB Ab)
+ also have "\<dots> = {x} <#> A"
+ by (auto simp: set_mult_def xeq)
+ finally show "A #> x = x <# A"
+ by (simp add: l_coset_eq_set_mult)
+ qed
+ then show ?thesis
+ by (auto simp: normal_def normal_axioms_def AG.subgroup_axioms is_group)
+qed
+
+lemma commuting_imp_normal2:
+ assumes"carrier G \<subseteq> A <#> B" "\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
+ shows "B \<lhd> G"
+proof (rule group_disjoint_sum.commuting_imp_normal1)
+ show "group_disjoint_sum G B A"
+ proof qed
+next
+ show "carrier G \<subseteq> B <#> A"
+ using BG.subgroup_axioms assms commut_normal commuting_imp_normal1 by blast
+qed (use assms in auto)
+
+
+lemma (in group) normal_imp_commuting:
+ assumes "A \<lhd> G" "B \<lhd> G" "A \<inter> B \<subseteq> {\<one>}" "x \<in> A" "y \<in> B"
+ shows "x \<otimes> y = y \<otimes> x"
+proof -
+ interpret AG: normal A G
+ using assms by auto
+ interpret BG: normal B G
+ using assms by auto
+ interpret group_disjoint_sum G A B
+ proof qed
+ have * [rule_format]: "(\<forall>x\<in>A. \<forall>y\<in>B. \<forall>x'\<in>A. \<forall>y'\<in>B. x \<otimes> y = x' \<otimes> y' \<longrightarrow> x = x' \<and> y = y')"
+ using cancel assms by (auto simp: normal_def)
+ have carr: "x \<in> carrier G" "y \<in> carrier G"
+ using assms AG.subset BG.subset by auto
+ then show ?thesis
+ using * [of x _ _ y] AG.coset_eq [rule_format, of y] BG.coset_eq [rule_format, of x]
+ by (clarsimp simp: l_coset_def r_coset_def set_eq_iff) (metis \<open>x \<in> A\<close> \<open>y \<in> B\<close>)
+qed
+
+lemma normal_eq_commuting:
+ assumes "carrier G \<subseteq> A <#> B" "A \<inter> B \<subseteq> {\<one>}"
+ shows "A \<lhd> G \<and> B \<lhd> G \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ by (metis assms commuting_imp_normal1 commuting_imp_normal2 normal_imp_commuting)
+
+lemma (in group) hom_group_mul_rev:
+ assumes "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G"
+ (is "?h \<in> hom ?P G")
+ and "x \<in> carrier G" "y \<in> carrier G" "x \<in> A" "y \<in> B"
+ shows "x \<otimes> y = y \<otimes> x"
+proof -
+ interpret P: group_hom ?P G ?h
+ by (simp add: assms DirProd_group group_hom.intro group_hom_axioms.intro is_group)
+ have xy: "(x,y) \<in> carrier ?P"
+ by (auto simp: assms carrier_subgroup_generated generate.incl)
+ have "x \<otimes> (x \<otimes> (y \<otimes> y)) = x \<otimes> (y \<otimes> (x \<otimes> y))"
+ using P.hom_mult [OF xy xy] by (simp add: m_assoc assms)
+ then have "x \<otimes> (y \<otimes> y) = y \<otimes> (x \<otimes> y)"
+ using assms by simp
+ then show ?thesis
+ by (simp add: assms flip: m_assoc)
+qed
+
+lemma hom_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> hom (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using hom_group_mul_rev AG.subset BG.subset by blast
+next
+ assume R: ?rhs
+ have subG: "generate G (carrier G \<inter> A) \<subseteq> carrier G" for A
+ by (simp add: generate_incl)
+ have *: "x \<otimes> u \<otimes> (y \<otimes> v) = x \<otimes> y \<otimes> (u \<otimes> v)"
+ if eq [rule_format]: "\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x"
+ and gen: "x \<in> generate G (carrier G \<inter> A)" "y \<in> generate G (carrier G \<inter> B)"
+ "u \<in> generate G (carrier G \<inter> A)" "v \<in> generate G (carrier G \<inter> B)"
+ for x y u v
+ proof -
+ have "u \<otimes> y = y \<otimes> u"
+ by (metis AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup carrier_subgroup_generated eq that(3) that(4))
+ then have "x \<otimes> u \<otimes> y = x \<otimes> y \<otimes> u"
+ using gen by (simp add: m_assoc subsetD [OF subG])
+ then show ?thesis
+ using gen by (simp add: subsetD [OF subG] flip: m_assoc)
+ qed
+ show ?lhs
+ using R by (auto simp: hom_def carrier_subgroup_generated subsetD [OF subG] *)
+qed
+
+
+lemma epi_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> epi (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+ have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+ by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+ have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+ by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+ have "(((\<lambda>(x, y). x \<otimes> y) ` (generate G (carrier G \<inter> A) \<times> generate G (carrier G \<inter> B)))) = ((A <#> B))"
+ by (auto simp: set_mult_def generate.incl pair_imageI dest: subsetD [OF subGA] subsetD [OF subGB])
+ then show ?thesis
+ by (auto simp: epi_def hom_group_mul_eq carrier_subgroup_generated)
+qed
+
+lemma mon_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> mon (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+proof -
+ have subGA: "generate G (carrier G \<inter> A) \<subseteq> A"
+ by (simp add: AG.subgroup_axioms generate_subgroup_incl)
+ have subGB: "generate G (carrier G \<inter> B) \<subseteq> B"
+ by (simp add: BG.subgroup_axioms generate_subgroup_incl)
+ show ?thesis
+ apply (auto simp: mon_def hom_group_mul_eq simp flip: subset_one)
+ apply (simp_all (no_asm_use) add: inj_on_def AG.carrier_subgroup_generated_subgroup BG.carrier_subgroup_generated_subgroup)
+ using cancel apply blast+
+ done
+qed
+
+lemma iso_group_mul_alt:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> (\<forall>x\<in>A. \<forall>y\<in>B. x \<otimes> y = y \<otimes> x)"
+ by (auto simp: iso_iff_mon_epi mon_group_mul_eq epi_group_mul_eq)
+
+lemma iso_group_mul_eq:
+ "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B = {\<one>} \<and> A <#> B = carrier G \<and> A \<lhd> G \<and> B \<lhd> G"
+ by (simp add: iso_group_mul_alt normal_eq_commuting cong: conj_cong)
+
+
+lemma (in group) iso_group_mul_gen:
+ assumes "A \<lhd> G" "B \<lhd> G"
+ shows "(\<lambda>(x,y). x \<otimes> y) \<in> iso (subgroup_generated G A \<times>\<times> subgroup_generated G B) G
+ \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G"
+proof -
+ interpret group_disjoint_sum G A B
+ using assms by (auto simp: group_disjoint_sum_def normal_def)
+ show ?thesis
+ by (simp add: subset_one iso_group_mul_eq assms)
+qed
+
+
+lemma iso_group_mul:
+ assumes "comm_group G"
+ shows "((\<lambda>(x,y). x \<otimes> y) \<in> iso (DirProd (subgroup_generated G A) (subgroup_generated G B)) G
+ \<longleftrightarrow> A \<inter> B \<subseteq> {\<one>} \<and> A <#> B = carrier G)"
+proof (rule iso_group_mul_gen)
+ interpret comm_group
+ by (rule assms)
+ show "A \<lhd> G"
+ by (simp add: AG.subgroup_axioms subgroup_imp_normal)
+ show "B \<lhd> G"
+ by (simp add: BG.subgroup_axioms subgroup_imp_normal)
+qed
+
+end
+
+
+subsection\<open>The one-element group on a given object\<close>
+
+definition singleton_group :: "'a \<Rightarrow> 'a monoid"
+ where "singleton_group a = \<lparr>carrier = {a}, monoid.mult = (\<lambda>x y. a), one = a\<rparr>"
+
+lemma singleton_group [simp]: "group (singleton_group a)"
+ unfolding singleton_group_def by (auto intro: groupI)
+
+lemma singleton_abelian_group [simp]: "comm_group (singleton_group a)"
+ by (metis group.group_comm_groupI monoid.simps(1) singleton_group singleton_group_def)
+
+lemma carrier_singleton_group [simp]: "carrier (singleton_group a) = {a}"
+ by (auto simp: singleton_group_def)
+
+lemma (in group) hom_into_singleton_iff [simp]:
+ "h \<in> hom G (singleton_group a) \<longleftrightarrow> h \<in> carrier G \<rightarrow> {a}"
+ by (auto simp: hom_def singleton_group_def)
+
+declare group.hom_into_singleton_iff [simp]
+
+lemma (in group) id_hom_singleton: "id \<in> hom (singleton_group \<one>) G"
+ by (simp add: hom_def singleton_group_def)
+
+subsection\<open>Similarly, trivial groups\<close>
+
+definition trivial_group :: "('a, 'b) monoid_scheme \<Rightarrow> bool"
+ where "trivial_group G \<equiv> group G \<and> carrier G = {one G}"
+
+lemma trivial_imp_finite_group:
+ "trivial_group G \<Longrightarrow> finite(carrier G)"
+ by (simp add: trivial_group_def)
+
+lemma trivial_singleton_group [simp]: "trivial_group(singleton_group a)"
+ by (metis monoid.simps(2) partial_object.simps(1) singleton_group singleton_group_def trivial_group_def)
+
+lemma (in group) trivial_group_subset:
+ "trivial_group G \<longleftrightarrow> carrier G \<subseteq> {one G}"
+ using is_group trivial_group_def by fastforce
+
+lemma (in group) trivial_group: "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G = {a})"
+ unfolding trivial_group_def using one_closed is_group by fastforce
+
+lemma (in group) trivial_group_alt:
+ "trivial_group G \<longleftrightarrow> (\<exists>a. carrier G \<subseteq> {a})"
+ by (auto simp: trivial_group)
+
+lemma (in group) trivial_group_subgroup_generated:
+ assumes "S \<subseteq> {one G}"
+ shows "trivial_group(subgroup_generated G S)"
+proof -
+ have "carrier (subgroup_generated G S) \<subseteq> {\<one>}"
+ using generate_empty generate_one subset_singletonD assms
+ by (fastforce simp add: carrier_subgroup_generated)
+ then show ?thesis
+ by (simp add: group.trivial_group_subset)
+qed
+
+lemma (in group) trivial_group_subgroup_generated_eq:
+ "trivial_group(subgroup_generated G s) \<longleftrightarrow> carrier G \<inter> s \<subseteq> {one G}"
+ apply (rule iffI)
+ apply (force simp: trivial_group_def carrier_subgroup_generated generate.incl)
+ by (metis subgroup_generated_restrict trivial_group_subgroup_generated)
+
+lemma isomorphic_group_triviality1:
+ assumes "G \<cong> H" "group H" "trivial_group G"
+ shows "trivial_group H"
+ using assms
+ by (auto simp: trivial_group_def is_iso_def iso_def group.is_monoid Group.group_def bij_betw_def hom_one)
+
+lemma isomorphic_group_triviality:
+ assumes "G \<cong> H" "group G" "group H"
+ shows "trivial_group G \<longleftrightarrow> trivial_group H"
+ by (meson assms group.iso_sym isomorphic_group_triviality1)
+
+lemma (in group_hom) kernel_from_trivial_group:
+ "trivial_group G \<Longrightarrow> kernel G H h = carrier G"
+ by (auto simp: trivial_group_def kernel_def)
+
+lemma (in group_hom) image_from_trivial_group:
+ "trivial_group G \<Longrightarrow> h ` carrier G = {one H}"
+ by (auto simp: trivial_group_def)
+
+lemma (in group_hom) kernel_to_trivial_group:
+ "trivial_group H \<Longrightarrow> kernel G H h = carrier G"
+ unfolding kernel_def trivial_group_def
+ using hom_closed by blast
+
+
+subsection\<open>The additive group of integers\<close>
+
+definition integer_group
+ where "integer_group = \<lparr>carrier = UNIV, monoid.mult = (+), one = (0::int)\<rparr>"
+
+lemma group_integer_group [simp]: "group integer_group"
+ unfolding integer_group_def
+proof (rule groupI; simp)
+ show "\<And>x::int. \<exists>y. y + x = 0"
+ by presburger
+qed
+
+lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
+ by (auto simp: integer_group_def)
+
+lemma one_integer_group [simp]: "\<one>\<^bsub>integer_group\<^esub> = 0"
+ by (auto simp: integer_group_def)
+
+lemma mult_integer_group [simp]: "x \<otimes>\<^bsub>integer_group\<^esub> y = x + y"
+ by (auto simp: integer_group_def)
+
+lemma inv_integer_group [simp]: "inv\<^bsub>integer_group\<^esub> x = -x"
+ by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma abelian_integer_group: "comm_group integer_group"
+ by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def)
+
+lemma group_nat_pow_integer_group [simp]:
+ fixes n::nat and x::int
+ shows "pow integer_group x n = int n * x"
+ by (induction n) (auto simp: integer_group_def algebra_simps)
+
+lemma group_int_pow_integer_group [simp]:
+ fixes n::int and x::int
+ shows "pow integer_group x n = n * x"
+ by (simp add: int_pow_def2)
+
+lemma (in group) hom_integer_group_pow:
+ "x \<in> carrier G \<Longrightarrow> pow G x \<in> hom integer_group G"
+ by (rule homI) (auto simp: int_pow_mult)
+
+end
--- a/src/HOL/Algebra/Generated_Groups.thy Tue Apr 02 15:16:56 2019 +0200
+++ b/src/HOL/Algebra/Generated_Groups.thy Tue Apr 02 16:55:56 2019 +0200
@@ -452,6 +452,19 @@
lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)"
by (auto simp: subgroup_generated_def)
+lemma (in group) subgroup_generated_subset_carrier_subset:
+ "S \<subseteq> carrier G \<Longrightarrow> S \<subseteq> carrier(subgroup_generated G S)"
+ by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI)
+
+lemma (in group) subgroup_generated_minimal:
+ "\<lbrakk>subgroup H G; S \<subseteq> H\<rbrakk> \<Longrightarrow> carrier(subgroup_generated G S) \<subseteq> H"
+ by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2)
+
+lemma (in group) carrier_subgroup_generated_subset:
+ "carrier (subgroup_generated G A) \<subseteq> 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)
@@ -520,7 +533,6 @@
"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) \<longleftrightarrow> subgroup H G \<and> H \<subseteq> carrier(subgroup_generated G B)"
(is "?lhs = ?rhs")
@@ -542,6 +554,9 @@
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 \<Rightarrow> nat \<Rightarrow> 'a)"
@@ -552,6 +567,19 @@
by force
qed
+lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S"
+proof -
+ have *: "\<And>A. carrier G \<inter> A \<subseteq> carrier (subgroup_generated (subgroup_generated G A) A)"
+ by (metis (no_types, hide_lams) 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, hide_lams) "*" 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 \<in> carrier (subgroup_generated G S)"
@@ -560,7 +588,7 @@
have "x [^] nat (- n) \<in> 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 (simp add: int_pow_def2 pow_subgroup_generated)
+ by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated)
qed
lemma kernel_from_subgroup_generated [simp]:
--- a/src/HOL/Algebra/Group.thy Tue Apr 02 15:16:56 2019 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Apr 02 16:55:56 2019 +0200
@@ -471,12 +471,12 @@
proof -
have [simp]: "-i - j = -j - i" by simp
show ?thesis
- by (auto simp add: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult )
+ by (auto simp: assms int_pow_def2 inv_solve_left inv_solve_right nat_add_distrib [symmetric] nat_pow_mult)
qed
lemma (in group) int_pow_inv:
"x \<in> carrier G \<Longrightarrow> (inv x) [^] (i :: int) = inv (x [^] i)"
- by (simp add: nat_pow_inv int_pow_def2)
+ by (metis int_pow_def2 nat_pow_inv)
lemma (in group) int_pow_pow:
assumes "x \<in> carrier G"
@@ -550,6 +550,22 @@
by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
qed
+lemma (in group) pow_eq_div2:
+ fixes m n :: nat
+ assumes x_car: "x \<in> carrier G"
+ assumes pow_eq: "x [^] m = x [^] n"
+ shows "x [^] (m - n) = \<one>"
+proof (cases "m < n")
+ case False
+ have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)
+ also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"
+ using False by (simp add: nat_pow_mult x_car)
+ also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"
+ by (simp add: pow_eq)
+ finally show ?thesis
+ by (metis nat_pow_closed one_closed right_cancel x_car)
+qed simp
+
subsection \<open>Submonoids\<close>
locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -873,6 +889,10 @@
"[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
by (fastforce simp add: hom_def compose_def)
+lemma (in group) restrict_hom_iff [simp]:
+ "(\<lambda>x. if x \<in> carrier G then f x else g x) \<in> hom G H \<longleftrightarrow> f \<in> hom G H"
+ by (simp add: hom_def Pi_iff)
+
definition iso :: "_ => _ => ('a => 'b) set"
where "iso G H = {h. h \<in> hom G H \<and> bij_betw h (carrier G) (carrier H)}"
@@ -1516,12 +1536,9 @@
then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
qed
-subsection\<open>Jeremy Avigad's \<open>More_Group\<close> material\<close>
+subsection\<open>The units in any monoid give rise to a group\<close>
-text \<open>
- Show that the units in any monoid give rise to a group.
-
- The file Residues.thy provides some infrastructure to use
+text \<open>Thanks to Jeremy Avigad. The file Residues.thy provides some infrastructure to use
facts about the unit group within the ring locale.
\<close>
@@ -1582,4 +1599,6 @@
lemma (in group) r_cancel_one' [simp]: "x \<in> carrier G \<Longrightarrow> a \<in> carrier G \<Longrightarrow> x = a \<otimes> x \<longleftrightarrow> a = one G"
using r_cancel_one by fastforce
+declare pow_nat [simp] (*causes looping if added above, especially with int_pow_def2*)
+
end
--- a/src/HOL/Algebra/Multiplicative_Group.thy Tue Apr 02 15:16:56 2019 +0200
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Tue Apr 02 16:55:56 2019 +0200
@@ -269,28 +269,135 @@
context group begin
-lemma pow_eq_div2:
- fixes m n :: nat
- assumes x_car: "x \<in> carrier G"
- assumes pow_eq: "x [^] m = x [^] n"
- shows "x [^] (m - n) = \<one>"
-proof (cases "m < n")
+definition (in group) ord :: "'a \<Rightarrow> nat" where
+ "ord x \<equiv> (@d. \<forall>n::nat. pow G x n = one G \<longleftrightarrow> d dvd n)"
+
+lemma (in group) pow_eq_id:
+ assumes "x \<in> carrier G"
+ shows "pow G x n = one G \<longleftrightarrow> (ord x) dvd n"
+proof (cases "\<forall>n::nat. pow G x n = one G \<longrightarrow> n = 0")
+ case True
+ show ?thesis
+ unfolding ord_def
+ by (rule someI2 [where a=0]) (auto simp: True)
+next
case False
- have "\<one> \<otimes> x [^] m = x [^] m" by (simp add: x_car)
- also have "\<dots> = x [^] (m - n) \<otimes> x [^] n"
- using False by (simp add: nat_pow_mult x_car)
- also have "\<dots> = x [^] (m - n) \<otimes> x [^] m"
- by (simp add: pow_eq)
- finally show ?thesis by (simp add: x_car)
-qed simp
+ define N where "N \<equiv> LEAST n::nat. x [^] n = \<one> \<and> n > 0"
+ have N: "x [^] N = \<one> \<and> N > 0"
+ using False
+ apply (simp add: N_def)
+ by (metis (mono_tags, lifting) LeastI)
+ have eq0: "n = 0" if "x [^] n = \<one>" "n < N" for n
+ using N_def not_less_Least that by fastforce
+ show ?thesis
+ unfolding ord_def
+ proof (rule someI2 [where a = N], rule allI)
+ fix n :: "nat"
+ show "(x [^] n = \<one>) \<longleftrightarrow> (N dvd n)"
+ proof (cases "n = 0")
+ case False
+ show ?thesis
+ unfolding dvd_def
+ proof safe
+ assume 1: "x [^] n = \<one>"
+ have "x [^] n = x [^] (n mod N + N * (n div N))"
+ by simp
+ also have "\<dots> = x [^] (n mod N) \<otimes> x [^] (N * (n div N))"
+ by (simp add: assms nat_pow_mult)
+ also have "\<dots> = x [^] (n mod N)"
+ by (metis N assms l_cancel_one nat_pow_closed nat_pow_one nat_pow_pow)
+ finally have "x [^] (n mod N) = \<one>"
+ by (simp add: "1")
+ then have "n mod N = 0"
+ using N eq0 mod_less_divisor by blast
+ then show "\<exists>k. n = N * k"
+ by blast
+ next
+ fix k :: "nat"
+ assume "n = N * k"
+ with N show "x [^] (N * k) = \<one>"
+ by (metis assms nat_pow_one nat_pow_pow)
+ qed
+ qed simp
+ qed blast
+qed
+
+lemma (in group) pow_ord_eq_1 [simp]:
+ "x \<in> carrier G \<Longrightarrow> x [^] ord x = \<one>"
+ by (simp add: pow_eq_id)
-definition ord where "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
+lemma (in group) int_pow_eq_id:
+ assumes "x \<in> carrier G"
+ shows "(pow G x i = one G \<longleftrightarrow> int (ord x) dvd i)"
+proof (cases i rule: int_cases2)
+ case (nonneg n)
+ then show ?thesis
+ by (simp add: int_pow_int pow_eq_id assms)
+next
+ case (nonpos n)
+ then have "x [^] i = inv (x [^] n)"
+ by (simp add: assms int_pow_int int_pow_neg)
+ then show ?thesis
+ by (simp add: assms pow_eq_id nonpos)
+qed
+
+lemma (in group) int_pow_eq:
+ "x \<in> carrier G \<Longrightarrow> (x [^] m = x [^] n) \<longleftrightarrow> int (ord x) dvd (n - m)"
+ apply (simp flip: int_pow_eq_id)
+ by (metis int_pow_closed int_pow_diff inv_closed r_inv right_cancel)
+
+lemma (in group) ord_eq_0:
+ "x \<in> carrier G \<Longrightarrow> (ord x = 0 \<longleftrightarrow> (\<forall>n::nat. n \<noteq> 0 \<longrightarrow> x [^] n \<noteq> \<one>))"
+ by (auto simp: pow_eq_id)
+
+lemma (in group) ord_unique:
+ "x \<in> carrier G \<Longrightarrow> ord x = d \<longleftrightarrow> (\<forall>n. pow G x n = one G \<longleftrightarrow> d dvd n)"
+ by (meson dvd_antisym dvd_refl pow_eq_id)
+
+lemma (in group) ord_eq_1:
+ "x \<in> carrier G \<Longrightarrow> (ord x = 1 \<longleftrightarrow> x = \<one>)"
+ by (metis pow_eq_id nat_dvd_1_iff_1 nat_pow_eone)
+
+lemma (in group) ord_id [simp]:
+ "ord (one G) = 1"
+ using ord_eq_1 by blast
+
+lemma (in group) ord_inv [simp]:
+ "x \<in> carrier G
+ \<Longrightarrow> ord (m_inv G x) = ord x"
+ by (simp add: ord_unique pow_eq_id nat_pow_inv)
+
+lemma (in group) ord_pow:
+ assumes "x \<in> carrier G" "k dvd ord x" "k \<noteq> 0"
+ shows "ord (pow G x k) = ord x div k"
+proof -
+ have "(x [^] k) [^] (ord x div k) = \<one>"
+ using assms by (simp add: nat_pow_pow)
+ moreover have "ord x dvd k * ord (x [^] k)"
+ by (metis assms(1) pow_ord_eq_1 pow_eq_id nat_pow_closed nat_pow_pow)
+ ultimately show ?thesis
+ by (metis assms div_dvd_div dvd_antisym dvd_triv_left pow_eq_id nat_pow_closed nonzero_mult_div_cancel_left)
+qed
+
+lemma (in group) ord_mul_divides:
+ assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+ shows "ord (x \<otimes> y) dvd (ord x * ord y)"
+apply (simp add: xy flip: pow_eq_id eq)
+ by (metis dvd_triv_left dvd_triv_right eq pow_eq_id one_closed pow_mult_distrib r_one xy)
+
+lemma (in comm_group) abelian_ord_mul_divides:
+ "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
+ \<Longrightarrow> ord (x \<otimes> y) dvd (ord x * ord y)"
+ by (simp add: ord_mul_divides m_comm)
+
+
+definition old_ord where "old_ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
lemma
- assumes finite:"finite (carrier G)"
- assumes a:"a \<in> carrier G"
- shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
- and pow_ord_eq_1: "a [^] ord a = \<one>"
+ assumes finite: "finite (carrier G)"
+ assumes a: "a \<in> carrier G"
+ shows old_ord_ge_1: "1 \<le> old_ord a" and old_ord_le_group_order: "old_ord a \<le> order G"
+ and pow_old_ord_eq_1: "a [^] old_ord a = \<one>"
proof -
have "\<not>inj_on (\<lambda>x. a [^] x) {0 .. order G}"
proof (rule notI)
@@ -315,25 +422,25 @@
assume "\<not>y < x" with x_y show ?thesis
by (intro that[where d="y - x"]) (auto simp add: pow_eq_div2[OF a])
qed
- hence "ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"
- unfolding ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]
+ hence "old_ord a \<in> {d \<in> {1 .. order G} . a [^] d = \<one>}"
+ unfolding old_ord_def using Min_in[of "{d \<in> {1 .. order G} . a [^] d = \<one>}"]
by fastforce
- then show "1 \<le> ord a" and "ord a \<le> order G" and "a [^] ord a = \<one>"
+ then show "1 \<le> old_ord a" and "old_ord a \<le> order G" and "a [^] old_ord a = \<one>"
by (auto simp: order_def)
qed
lemma finite_group_elem_finite_ord:
assumes "finite (carrier G)" "x \<in> carrier G"
shows "\<exists> d::nat. d \<ge> 1 \<and> x [^] d = \<one>"
- using assms ord_ge_1 pow_ord_eq_1 by auto
+ using assms old_ord_ge_1 pow_old_ord_eq_1 by auto
-lemma ord_min:
- assumes "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "ord a \<le> d"
+lemma old_ord_min:
+ assumes "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a [^] d = \<one>" shows "old_ord a \<le> d"
proof -
define Ord where "Ord = {d \<in> {1..order G}. a [^] d = \<one>}"
have fin: "finite Ord" by (auto simp: Ord_def)
- have in_ord: "ord a \<in> Ord"
- using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
+ have in_ord: "old_ord a \<in> Ord"
+ using assms pow_old_ord_eq_1 old_ord_ge_1 old_ord_le_group_order by (auto simp: Ord_def)
then have "Ord \<noteq> {}" by auto
show ?thesis
@@ -341,13 +448,49 @@
case True
then have "d \<in> Ord" using assms by (auto simp: Ord_def)
with fin in_ord show ?thesis
- unfolding ord_def Ord_def[symmetric] by simp
+ unfolding old_ord_def Ord_def[symmetric] by simp
next
case False
then show ?thesis using in_ord by (simp add: Ord_def)
qed
qed
+lemma old_ord_dvd_pow_eq_1 :
+ assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"
+ shows "old_ord a dvd k"
+proof -
+ define r where "r = k mod old_ord a"
+
+ define r q where "r = k mod old_ord a" and "q = k div old_ord a"
+ then have q: "k = q * old_ord a + r"
+ by (simp add: div_mult_mod_eq)
+ hence "a[^]k = (a[^]old_ord a)[^]q \<otimes> a[^]r"
+ using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
+ hence "a[^]k = a[^]r" using assms by (simp add: pow_old_ord_eq_1)
+ hence "a[^]r = \<one>" using assms(3) by simp
+ have "r < old_ord a" using old_ord_ge_1[OF assms(1-2)] by (simp add: r_def)
+ hence "r = 0" using \<open>a[^]r = \<one>\<close> old_ord_def[of a] old_ord_min[of r a] assms(1-2) by linarith
+ thus ?thesis using q by simp
+qed
+
+lemma (in group) ord_iff_old_ord:
+ assumes finite: "finite (carrier G)"
+ assumes a: "a \<in> carrier G"
+ shows "ord a = Min {d \<in> {1 .. order G} . a [^] d = \<one>}"
+proof -
+ have "a [^] ord a = \<one>"
+ using a pow_ord_eq_1 by blast
+ then show ?thesis
+ by (metis a dvd_antisym local.finite old_ord_def old_ord_dvd_pow_eq_1 pow_eq_id pow_old_ord_eq_1)
+qed
+
+lemma
+ assumes finite: "finite (carrier G)"
+ assumes a: "a \<in> carrier G"
+ shows ord_ge_1: "1 \<le> ord a" and ord_le_group_order: "ord a \<le> order G"
+ using a group.old_ord_ge_1 group.pow_eq_id group.pow_old_ord_eq_1 is_group local.finite apply fastforce
+ by (metis a dvd_antisym group.pow_eq_id is_group local.finite old_ord_dvd_pow_eq_1 old_ord_le_group_order pow_ord_eq_1 pow_old_ord_eq_1)
+
lemma ord_inj:
assumes finite: "finite (carrier G)"
assumes a: "a \<in> carrier G"
@@ -366,7 +509,8 @@
hence y_x:"y - x \<in> {d \<in> {1.. order G}. a [^] d = \<one>}" using y_x_range by blast
have "min (y - x) (ord a) = ord a"
- using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x] ord_def by auto
+ using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a [^] d = \<one>}\<close> y_x]
+ by (simp add: a group.ord_iff_old_ord is_group local.finite)
with \<open>y - x < ord a\<close> have False by linarith
}
note X = this
@@ -392,13 +536,13 @@
}
moreover
{ assume "x = ord a" "y < ord a"
- hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
+ hence "a [^] y = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
moreover
{ assume "y = ord a" "x < ord a"
- hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1[OF assms] A by auto
+ hence "a [^] x = a [^] (0::nat)" using pow_ord_eq_1 A by (simp add: a)
hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
hence False using A by fastforce
}
@@ -416,7 +560,7 @@
then have "x = q * ord a + r"
by (simp add: div_mult_mod_eq)
hence "y = (a[^]ord a)[^]q \<otimes> a[^]r"
- using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
+ using x assms by (metis mult.commute nat_pow_mult nat_pow_pow)
hence "y = a[^]r" using assms by (simp add: pow_ord_eq_1)
have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
@@ -448,13 +592,12 @@
proof (cases "k < 0")
assume "\<not> k < 0"
hence "b = a [^] (nat k)"
- by (simp add: int_pow_def2 k)
+ by (simp add: k)
thus ?thesis by blast
next
assume "k < 0"
hence b: "b = inv (a [^] (nat (- k)))"
- using k int_pow_def2[of G] by auto
-
+ using k \<open>a \<in> carrier G\<close> by (auto simp: int_pow_neg)
obtain m where m: "ord a * m \<ge> nat (- k)"
by (metis assms mult.left_neutral mult_le_mono1 ord_ge_1)
hence "a [^] (ord a * m) = \<one>"
@@ -490,25 +633,7 @@
by (metis dvd_triv_right empty_subsetI insert_subset)
then obtain k :: nat where "order G = ord a * k" by blast
thus ?thesis
- using assms(2) pow_ord_eq_1[OF assms] by (metis nat_pow_one nat_pow_pow)
-qed
-
-lemma ord_dvd_pow_eq_1 :
- assumes "finite (carrier G)" "a \<in> carrier G" "a [^] k = \<one>"
- shows "ord a dvd k"
-proof -
- define r where "r = k mod ord a"
-
- define r q where "r = k mod ord a" and "q = k div ord a"
- then have q: "k = q * ord a + r"
- by (simp add: div_mult_mod_eq)
- hence "a[^]k = (a[^]ord a)[^]q \<otimes> a[^]r"
- using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
- hence "a[^]k = a[^]r" using assms by (simp add: pow_ord_eq_1)
- hence "a[^]r = \<one>" using assms(3) by simp
- have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
- hence "r = 0" using \<open>a[^]r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
- thus ?thesis using q by simp
+ using assms(2) pow_ord_eq_1 by (metis nat_pow_one nat_pow_pow)
qed
lemma dvd_gcd :
@@ -526,10 +651,11 @@
shows "ord (a[^]n) = ord a div gcd n (ord a)"
proof -
have "(a[^]n) [^] ord a = (a [^] ord a) [^] n"
- by (simp add: mult.commute nat_pow_pow)
+ by (simp add: nat_pow_pow pow_eq_id)
hence "(a[^]n) [^] ord a = \<one>" by (simp add: pow_ord_eq_1)
obtain q where "n * (ord a div gcd n (ord a)) = ord a * q" by (rule dvd_gcd)
- hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q" by (simp add : nat_pow_pow)
+ hence "(a[^]n) [^] (ord a div gcd n (ord a)) = (a [^] ord a)[^]q"
+ using a nat_pow_pow by presburger
hence pow_eq_1: "(a[^]n) [^] (ord a div gcd n (ord a)) = \<one>"
by (auto simp add : pow_ord_eq_1[of a])
have "ord a \<ge> 1" using ord_ge_1 by simp
@@ -551,7 +677,7 @@
assume d_lt:"d < ord a div gcd n (ord a)"
hence pow_nd:"a[^](n*d) = \<one>" using d_elem
by (simp add : nat_pow_pow)
- hence "ord a dvd n*d" using assms by (auto simp add : ord_dvd_pow_eq_1)
+ hence "ord a dvd n*d" using assms pow_eq_id by blast
then obtain q where "ord a * q = n*d" by (metis dvd_mult_div_cancel)
hence prod_eq:"(ord a div gcd n (ord a)) * q = (n div gcd n (ord a)) * d"
by (simp add: dvd_div_mult)
@@ -577,14 +703,9 @@
\<Longrightarrow> d\<ge>ord a div gcd n (ord a)" by fastforce
have fin:"finite {d \<in> {1..order G}. (a[^]n) [^] d = \<one>}" by auto
thus ?thesis using Min_eqI[OF fin ord_gcd_min ord_gcd_elem]
- unfolding ord_def by simp
+ by (simp add: group.ord_iff_old_ord is_group)
qed
-lemma ord_1_eq_1 :
- assumes "finite (carrier G)"
- shows "ord \<one> = 1"
- using assms ord_ge_1 ord_min[of 1 \<one>] by force
-
lemma element_generates_subgroup:
assumes finite[simp]: "finite (carrier G)"
assumes a[simp]: "a \<in> carrier G"
@@ -593,7 +714,7 @@
generate_pow_on_finite_carrier[OF assms]
unfolding ord_elems[OF assms] by auto
-lemma ord_dvd_group_order: (* <- DELETE *)
+lemma ord_dvd_group_order:
assumes "finite (carrier G)" and "a \<in> carrier G"
shows "(ord a) dvd (order G)"
using lagrange[OF generate_is_subgroup[of " { a }"]] assms(2)
@@ -823,7 +944,7 @@
fix x assume "x \<in> {a[^]n | n. n \<in> {1 .. d}}"
then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" by auto
have "x[^]d =(a[^]d)[^]n" using n a ord_a by (simp add:nat_pow_pow mult.commute)
- hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF finite' a] by fastforce
+ hence "x[^]d = \<one>" using ord_a G.pow_ord_eq_1[OF a] by fastforce
thus "x \<in> {x \<in> carrier (mult_of R). x[^]d = \<one>}" using G.nat_pow_closed[OF a] n by blast
qed
@@ -845,7 +966,7 @@
proof
{ fix x assume x:"x \<in> (carrier (mult_of R)) \<and> group.ord (mult_of R) x = d"
hence "x \<in> {x \<in> carrier (mult_of R). x [^] d = \<one>}"
- by (simp add: G.pow_ord_eq_1[OF finite', of x, symmetric])
+ by (simp add: G.pow_ord_eq_1[of x, symmetric])
then obtain n where n:"x = a[^]n \<and> n \<in> {1 .. d}" using set_eq1 by blast
hence "x \<in> ?R" using x by fast
} thus "?L \<subseteq> ?R" by blast