src/HOL/Algebra/Group.thy
 changeset 68555 22d51874f37d parent 68551 b680e74eb6f2 child 68605 440aa6b7d99a
```     1.1 --- a/src/HOL/Algebra/Group.thy	Sat Jun 30 18:58:13 2018 +0100
1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Jul 01 16:13:25 2018 +0100
1.3 @@ -590,12 +590,18 @@
1.4      by (rule monoid.group_l_invI) (auto intro: l_inv mem_carrier)
1.5  qed
1.6
1.7 -lemma (in group) subgroup_inv_equality:
1.8 +lemma subgroup_is_submonoid:
1.9 +  assumes "subgroup H G" shows "submonoid H G"
1.10 +  using assms by (auto intro: submonoid.intro simp add: subgroup_def)
1.11 +
1.12 +lemma (in group) subgroup_Units:
1.13 +  assumes "subgroup H G" shows "H \<subseteq> Units (G \<lparr> carrier := H \<rparr>)"
1.14 +  using group.Units[OF subgroup.subgroup_is_group[OF assms group_axioms]] by simp
1.15 +
1.16 +lemma (in group) m_inv_consistent:
1.17    assumes "subgroup H G" "x \<in> H"
1.18 -  shows "m_inv (G \<lparr>carrier := H\<rparr>) x = inv x"
1.19 -  unfolding m_inv_def apply auto
1.20 -  using subgroup.m_inv_closed[OF assms] inv_equality
1.21 -  by (metis (no_types, hide_lams) assms subgroup.mem_carrier)
1.22 +  shows "inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x = inv x"
1.23 +  using assms m_inv_monoid_consistent[OF _ subgroup_is_submonoid] subgroup_Units[of H] by auto
1.24
1.25  lemma (in group) int_pow_consistent: (* by Paulo *)
1.26    assumes "subgroup H G" "x \<in> H"
1.27 @@ -616,7 +622,7 @@
1.28    also have " ... = (inv x) [^] (nat (- n))"
1.29      by (metis assms nat_pow_inv subgroup.mem_carrier)
1.30    also have " ... = (inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> x) [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n))"
1.31 -    using subgroup_inv_equality[OF assms] nat_pow_consistent by auto
1.32 +    using m_inv_consistent[OF assms] nat_pow_consistent by auto
1.33    also have " ... = inv\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> (nat (- n)))"
1.34      using group.nat_pow_inv[OF subgroup.subgroup_is_group[OF assms(1) is_group]] assms(2) by auto
1.35    also have " ... = x [^]\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> n"
1.36 @@ -1290,18 +1296,16 @@
1.37    thus  "I \<subseteq> carrier G \<and> (\<forall>x y. x \<in> I \<longrightarrow> y \<in> I \<longrightarrow> x \<otimes> y \<in> I)"  using H by blast
1.38    have K: "\<one> \<in> I" using assms(2) by (auto simp add: subgroup_def)
1.39    have "(\<And>x. x \<in> I \<Longrightarrow> inv x \<in> I)" using assms  subgroup.m_inv_closed H
1.40 -    by (metis H1 H2  subgroup_inv_equality subsetCE)
1.41 +    by (metis H1 H2 m_inv_consistent subsetCE)
1.42    thus "\<one> \<in> I \<and> (\<forall>x. x \<in> I \<longrightarrow> inv x \<in> I)" using K by blast
1.43  qed
1.44
1.45  (*A subgroup included in another subgroup is a subgroup of the subgroup*)
1.46  lemma (in group) subgroup_incl:
1.47 -  assumes "subgroup I G"
1.48 -    and "subgroup J G"
1.49 -    and "I\<subseteq>J"
1.50 -  shows "subgroup I (G\<lparr>carrier:=J\<rparr>)"using assms subgroup_inv_equality
1.51 -  by (auto simp add: subgroup_def)
1.52 -
1.53 +  assumes "subgroup I G" and "subgroup J G" and "I \<subseteq> J"
1.54 +  shows "subgroup I (G \<lparr> carrier := J \<rparr>)"
1.55 +  using group.group_incl_imp_subgroup[of "G \<lparr> carrier := J \<rparr>" I]
1.56 +        assms(1-2)[THEN subgroup.subgroup_is_group[OF _ group_axioms]] assms(3) by auto
1.57
1.58
1.59  subsection \<open>The Lattice of Subgroups of a Group\<close>
1.60 @@ -1433,7 +1437,7 @@
1.61  lemma units_of_one: "one (units_of G) = one G"
1.62    by (auto simp: units_of_def)
1.63
1.64 -lemma (in monoid) units_of_inv:
1.65 +lemma (in monoid) units_of_inv:
1.66    assumes "x \<in> Units G"
1.67    shows "m_inv (units_of G) x = m_inv G x"
1.68    by (simp add: assms group.inv_equality units_group units_of_carrier units_of_mult units_of_one)
```