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)