--- a/src/HOL/Algebra/Group.thy Sat Mar 30 15:37:27 2019 +0100
+++ b/src/HOL/Algebra/Group.thy Mon Apr 01 17:02:43 2019 +0100
@@ -425,7 +425,20 @@
end
lemma int_pow_int: "x [^]\<^bsub>G\<^esub> (int n) = x [^]\<^bsub>G\<^esub> n"
-by(simp add: int_pow_def nat_pow_def)
+ by(simp add: int_pow_def nat_pow_def)
+
+lemma pow_nat:
+ assumes "i\<ge>0"
+ shows "x [^]\<^bsub>G\<^esub> nat i = x [^]\<^bsub>G\<^esub> i"
+proof (cases i rule: int_cases)
+ case (nonneg n)
+ then show ?thesis
+ by (simp add: int_pow_int)
+next
+ case (neg n)
+ then show ?thesis
+ using assms by linarith
+qed
lemma int_pow_0 [simp]: "x [^]\<^bsub>G\<^esub> (0::int) = \<one>\<^bsub>G\<^esub>"
by (simp add: int_pow_def)
@@ -450,6 +463,9 @@
"x \<in> carrier G \<Longrightarrow> x [^] (-i::int) = inv (x [^] i)"
by (simp add: int_pow_def2)
+lemma (in group) int_pow_neg_int: "x \<in> carrier G \<Longrightarrow> x [^] -(int n) = inv (x [^] n)"
+ by (simp add: int_pow_neg int_pow_int)
+
lemma (in group) int_pow_mult:
assumes "x \<in> carrier G" shows "x [^] (i + j::int) = x [^] i \<otimes> x [^] j"
proof -
@@ -502,6 +518,38 @@
by(simp add: inj_on_def)
+lemma (in monoid) group_commutes_pow:
+ fixes n::nat
+ shows "\<lbrakk>x \<otimes> y = y \<otimes> x; x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x [^] n \<otimes> y = y \<otimes> x [^] n"
+ apply (induction n, auto)
+ by (metis m_assoc nat_pow_closed)
+
+lemma (in monoid) pow_mult_distrib:
+ assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
+proof (induct n)
+ case (Suc n)
+ have "x \<otimes> (y [^] n \<otimes> y) = y [^] n \<otimes> x \<otimes> y"
+ by (simp add: eq group_commutes_pow m_assoc xy)
+ then show ?case
+ using assms Suc.hyps m_assoc by auto
+qed auto
+
+lemma (in group) int_pow_mult_distrib:
+ assumes eq: "x \<otimes> y = y \<otimes> x" and xy: "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+proof (cases i rule: int_cases)
+ case (nonneg n)
+ then show ?thesis
+ by (metis eq int_pow_int pow_mult_distrib xy)
+next
+ case (neg n)
+ then show ?thesis
+ unfolding neg
+ apply (simp add: xy int_pow_neg_int del: of_nat_Suc)
+ by (metis eq inv_mult_group local.nat_pow_Suc nat_pow_closed pow_mult_distrib xy)
+qed
+
subsection \<open>Submonoids\<close>
locale submonoid = \<^marker>\<open>contributor \<open>Martin Baillon\<close>\<close>
@@ -852,7 +900,7 @@
lemma id_iso: "id \<in> iso G G"
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
-corollary iso_refl : "G \<cong> G"
+corollary iso_refl [simp]: "G \<cong> G"
using iso_set_refl unfolding is_iso_def by auto
lemma trivial_hom:
@@ -901,11 +949,11 @@
corollary (in group) iso_sym: "G \<cong> H \<Longrightarrow> H \<cong> G"
using iso_set_sym unfolding is_iso_def by auto
-lemma (in group) iso_set_trans:
- "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
- by (auto simp add: iso_def hom_compose bij_betw_compose)
+lemma iso_set_trans:
+ "\<lbrakk>h \<in> Group.iso G H; i \<in> Group.iso H I\<rbrakk> \<Longrightarrow> i \<circ> h \<in> Group.iso G I"
+ by (force simp: iso_def hom_compose intro: bij_betw_trans)
-corollary (in group) iso_trans: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
+corollary iso_trans [trans]: "\<lbrakk>G \<cong> H ; H \<cong> I\<rbrakk> \<Longrightarrow> G \<cong> I"
using iso_set_trans unfolding is_iso_def by blast
lemma iso_same_card: "G \<cong> H \<Longrightarrow> card (carrier G) = card (carrier H)"
@@ -1081,6 +1129,8 @@
fixes h
assumes homh [simp]: "h \<in> hom G H"
+declare group_hom.homh [simp]
+
lemma (in group_hom) hom_mult [simp]:
"[| x \<in> carrier G; y \<in> carrier G |] ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y"
proof -
@@ -1170,14 +1220,21 @@
using subgroup.subgroup_is_group[OF assms is_group]
is_group subgroup.subset[OF assms] by auto
-lemma (in group_hom) nat_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_nat_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
"x \<in> carrier G \<Longrightarrow> h (x [^] (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
by (induction n) auto
-lemma (in group_hom) int_pow_hom: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
+lemma (in group_hom) hom_int_pow: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
"x \<in> carrier G \<Longrightarrow> h (x [^] (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
- using nat_pow_hom by (simp add: int_pow_def2)
+ using hom_nat_pow by (simp add: int_pow_def2)
+lemma hom_nat_pow:
+ "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: nat)) = (h x) [^]\<^bsub>H\<^esub> n"
+ by (simp add: group_hom.hom_nat_pow group_hom_axioms_def group_hom_def)
+
+lemma hom_int_pow:
+ "\<lbrakk>h \<in> hom G H; x \<in> carrier G; group G; group H\<rbrakk> \<Longrightarrow> h (x [^]\<^bsub>G\<^esub> (n :: int)) = (h x) [^]\<^bsub>H\<^esub> n"
+ by (simp add: group_hom.hom_int_pow group_hom_axioms.intro group_hom_def)
subsection \<open>Commutative Structures\<close>
@@ -1225,11 +1282,6 @@
shows "comm_monoid G"
by (rule comm_monoidI) (auto intro: m_assoc m_comm)
-lemma (in comm_monoid) nat_pow_distr:
- "[| x \<in> carrier G; y \<in> carrier G |] ==>
- (x \<otimes> y) [^] (n::nat) = x [^] n \<otimes> y [^] n"
- by (induct n) (simp, simp add: m_ac)
-
lemma (in comm_monoid) submonoid_is_comm_monoid :
assumes "submonoid H G"
shows "comm_monoid (G\<lparr>carrier := H\<rparr>)"
@@ -1279,6 +1331,17 @@
"[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y"
by (simp add: m_ac inv_mult_group)
+lemma (in comm_monoid) nat_pow_distrib:
+ fixes n::nat
+ assumes "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] n = x [^] n \<otimes> y [^] n"
+ by (simp add: assms pow_mult_distrib m_comm)
+
+lemma (in comm_group) int_pow_distrib:
+ assumes "x \<in> carrier G" "y \<in> carrier G"
+ shows "(x \<otimes> y) [^] (i::int) = x [^] i \<otimes> y [^] i"
+ by (simp add: assms int_pow_mult_distrib m_comm)
+
lemma (in comm_monoid) hom_imp_img_comm_monoid: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "h \<in> hom G H"
shows "comm_monoid (H \<lparr> carrier := h ` (carrier G), one := h \<one>\<^bsub>G\<^esub> \<rparr>)" (is "comm_monoid ?h_img")