src/HOL/Algebra/Coset.thy
author paulson <lp15@cam.ac.uk>
Sat Jun 30 15:44:04 2018 +0100 (12 months ago)
changeset 68551 b680e74eb6f2
parent 68517 6b5f15387353
child 68555 22d51874f37d
permissions -rw-r--r--
More on Algebra by Paulo and Martin
     1 (*  Title:      HOL/Algebra/Coset.thy
     2     Authors:     Florian Kammueller, L C Paulson, Stephan Hohe
     3 With additional contributions from Martin Baillon and Paulo Emílio de Vilhena.
     4 *)
     5 
     6 theory Coset
     7 imports Group
     8 begin
     9 
    10 section \<open>Cosets and Quotient Groups\<close>
    11 
    12 definition
    13   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
    14   where "H #>\<^bsub>G\<^esub> a = (\<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a})"
    15 
    16 definition
    17   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
    18   where "a <#\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h})"
    19 
    20 definition
    21   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
    22   where "rcosets\<^bsub>G\<^esub> H = (\<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a})"
    23 
    24 definition
    25   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
    26   where "H <#>\<^bsub>G\<^esub> K = (\<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k})"
    27 
    28 definition
    29   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
    30   where "set_inv\<^bsub>G\<^esub> H = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
    31 
    32 
    33 locale normal = subgroup + group +
    34   assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)"
    35 
    36 abbreviation
    37   normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool"  (infixl "\<lhd>" 60) where
    38   "H \<lhd> G \<equiv> normal H G"
    39 
    40 (* ************************************************************************** *)
    41 (* Next two lemmas contributed by Martin Baillon.                                  *)
    42 
    43 lemma l_coset_eq_set_mult:
    44   fixes G (structure)
    45   shows "x <# H = {x} <#> H"
    46   unfolding l_coset_def set_mult_def by simp 
    47 
    48 lemma r_coset_eq_set_mult:
    49   fixes G (structure)
    50   shows "H #> x = H <#> {x}"
    51   unfolding r_coset_def set_mult_def by simp
    52 
    53 (* Next five lemmas contributed by Paulo Emílio de Vilhena.                    *)
    54 
    55 lemma (in subgroup) rcosets_non_empty:
    56   assumes "R \<in> rcosets H"
    57   shows "R \<noteq> {}"
    58 proof -
    59   obtain g where "g \<in> carrier G" "R = H #> g"
    60     using assms unfolding RCOSETS_def by blast
    61   hence "\<one> \<otimes> g \<in> R"
    62     using one_closed unfolding r_coset_def by blast
    63   thus ?thesis by blast
    64 qed
    65 
    66 lemma (in group) diff_neutralizes:
    67   assumes "subgroup H G" "R \<in> rcosets H"
    68   shows "\<And>r1 r2. \<lbrakk> r1 \<in> R; r2 \<in> R \<rbrakk> \<Longrightarrow> r1 \<otimes> (inv r2) \<in> H"
    69 proof -
    70   fix r1 r2 assume r1: "r1 \<in> R" and r2: "r2 \<in> R"
    71   obtain g where g: "g \<in> carrier G" "R = H #> g"
    72     using assms unfolding RCOSETS_def by blast
    73   then obtain h1 h2 where h1: "h1 \<in> H" "r1 = h1 \<otimes> g"
    74                       and h2: "h2 \<in> H" "r2 = h2 \<otimes> g"
    75     using r1 r2 unfolding r_coset_def by blast
    76   hence "r1 \<otimes> (inv r2) = (h1 \<otimes> g) \<otimes> ((inv g) \<otimes> (inv h2))"
    77     using inv_mult_group is_group assms(1) g(1) subgroup.mem_carrier by fastforce 
    78   also have " ... =  (h1 \<otimes> (g \<otimes> inv g) \<otimes> inv h2)"
    79     using h1 h2 assms(1) g(1) inv_closed m_closed monoid.m_assoc
    80           monoid_axioms subgroup.mem_carrier by smt
    81   finally have "r1 \<otimes> inv r2 = h1 \<otimes> inv h2"
    82     using assms(1) g(1) h1(1) subgroup.mem_carrier by fastforce
    83   thus "r1 \<otimes> inv r2 \<in> H" by (metis assms(1) h1(1) h2(1) subgroup_def)
    84 qed
    85 
    86 lemma mono_set_mult: "\<lbrakk> H \<subseteq> H'; K \<subseteq> K' \<rbrakk> \<Longrightarrow> H <#>\<^bsub>G\<^esub> K \<subseteq> H' <#>\<^bsub>G\<^esub> K'"
    87   unfolding set_mult_def by (simp add: UN_mono)
    88 
    89 
    90 subsection \<open>Stable Operations for Subgroups\<close>
    91 
    92 lemma (in group) subgroup_set_mult_equality[simp]:
    93   assumes "subgroup H G" "I \<subseteq> H" "J \<subseteq> H"
    94   shows "I <#>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> J = I <#> J"
    95   unfolding set_mult_def subgroup_mult_equality[OF assms(1)] by auto
    96 
    97 lemma (in group) subgroup_rcos_equality[simp]:
    98   assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
    99   shows "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #> h"
   100   using subgroup_set_mult_equality by (simp add: r_coset_eq_set_mult assms)
   101 
   102 lemma (in group) subgroup_lcos_equality[simp]:
   103   assumes "subgroup H G" "I \<subseteq> H" "h \<in> H"
   104   shows "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <# I"
   105   using subgroup_set_mult_equality by (simp add: l_coset_eq_set_mult assms)
   106 
   107 lemma set_mult_consistent [simp]:
   108   "N <#>\<^bsub>(G \<lparr> carrier := H \<rparr>)\<^esub> K = N <#>\<^bsub>G\<^esub> K"
   109   unfolding set_mult_def by simp
   110 
   111 lemma r_coset_consistent [simp]:
   112   "I #>\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> h = I #>\<^bsub>G\<^esub> h"
   113   unfolding r_coset_def by simp
   114 
   115 lemma l_coset_consistent [simp]:
   116   "h <#\<^bsub>G \<lparr> carrier := H \<rparr>\<^esub> I = h <#\<^bsub>G\<^esub> I"
   117   unfolding l_coset_def by simp
   118 
   119 subsection \<open>Basic Properties of set multiplication\<close>
   120 
   121 lemma (in group) setmult_subset_G:
   122   assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
   123   shows "H <#> K \<subseteq> carrier G" using assms
   124   by (auto simp add: set_mult_def subsetD)
   125 
   126 lemma (in monoid) set_mult_closed:
   127   assumes "H \<subseteq> carrier G" "K \<subseteq> carrier G"
   128   shows "H <#> K \<subseteq> carrier G"
   129   using assms by (auto simp add: set_mult_def subsetD)
   130 
   131 (* Next lemma contributed by Martin Baillon.*)
   132 lemma (in group) set_mult_assoc:
   133   assumes "M \<subseteq> carrier G" "H \<subseteq> carrier G" "K \<subseteq> carrier G"
   134   shows "(M <#> H) <#> K = M <#> (H <#> K)"
   135 proof
   136   show "(M <#> H) <#> K \<subseteq> M <#> (H <#> K)"
   137   proof
   138     fix x assume "x \<in> (M <#> H) <#> K"
   139     then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = (m \<otimes> h) \<otimes> k"
   140       unfolding set_mult_def by blast
   141     hence "x = m \<otimes> (h \<otimes> k)"
   142       using assms m_assoc by blast
   143     thus "x \<in> M <#> (H <#> K)"
   144       unfolding set_mult_def using x by blast
   145   qed
   146 next
   147   show "M <#> (H <#> K) \<subseteq> (M <#> H) <#> K"
   148   proof
   149     fix x assume "x \<in> M <#> (H <#> K)"
   150     then obtain m h k where x: "m \<in> M" "h \<in> H" "k \<in> K" "x = m \<otimes> (h \<otimes> k)"
   151       unfolding set_mult_def by blast
   152     hence "x = (m \<otimes> h) \<otimes> k"
   153       using assms m_assoc rev_subsetD by metis
   154     thus "x \<in> (M <#> H) <#> K"
   155       unfolding set_mult_def using x by blast
   156   qed
   157 qed
   158 
   159 
   160 
   161 subsection \<open>Basic Properties of Cosets\<close>
   162 
   163 lemma (in group) coset_mult_assoc:
   164   assumes "M \<subseteq> carrier G" "g \<in> carrier G" "h \<in> carrier G"
   165   shows "(M #> g) #> h = M #> (g \<otimes> h)"
   166   using assms by (force simp add: r_coset_def m_assoc)
   167 
   168 lemma (in group) coset_assoc:
   169   assumes "x \<in> carrier G" "y \<in> carrier G" "H \<subseteq> carrier G"
   170   shows "x <# (H #> y) = (x <# H) #> y"
   171   using set_mult_assoc[of "{x}" H "{y}"]
   172   by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult assms)
   173 
   174 lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M"
   175 by (force simp add: r_coset_def)
   176 
   177 lemma (in group) coset_mult_inv1:
   178   assumes "M #> (x \<otimes> (inv y)) = M"
   179     and "x \<in> carrier G" "y \<in> carrier G" "M \<subseteq> carrier G"
   180   shows "M #> x = M #> y" using assms
   181   by (metis coset_mult_assoc group.inv_solve_right is_group subgroup_def subgroup_self)
   182 
   183 lemma (in group) coset_mult_inv2:
   184   assumes "M #> x = M #> y"
   185     and "x \<in> carrier G"  "y \<in> carrier G" "M \<subseteq> carrier G"
   186   shows "M #> (x \<otimes> (inv y)) = M " using assms
   187   by (metis group.coset_mult_assoc group.coset_mult_one inv_closed is_group r_inv) 
   188 
   189 lemma (in group) coset_join1:
   190   assumes "H #> x = H"
   191     and "x \<in> carrier G" "subgroup H G"
   192   shows "x \<in> H"
   193   using assms r_coset_def l_one subgroup.one_closed sym by fastforce
   194 
   195 lemma (in group) solve_equation:
   196   assumes "subgroup H G" "x \<in> H" "y \<in> H"
   197   shows "\<exists>h \<in> H. y = h \<otimes> x"
   198 proof -
   199   have "y = (y \<otimes> (inv x)) \<otimes> x" using assms
   200     by (simp add: m_assoc subgroup.mem_carrier)
   201   moreover have "y \<otimes> (inv x) \<in> H" using assms
   202     by (simp add: subgroup_def)
   203   ultimately show ?thesis by blast
   204 qed
   205 
   206 lemma (in group) repr_independence:
   207   assumes "y \<in> H #> x" "x \<in> carrier G" "subgroup H G"
   208   shows "H #> x = H #> y" using assms
   209 by (auto simp add: r_coset_def m_assoc [symmetric]
   210                    subgroup.subset [THEN subsetD]
   211                    subgroup.m_closed solve_equation)
   212 
   213 lemma (in group) coset_join2:
   214   assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
   215   shows "H #> x = H" using assms
   216   \<comment> \<open>Alternative proof is to put @{term "x=\<one>"} in \<open>repr_independence\<close>.\<close>
   217 by (force simp add: subgroup.m_closed r_coset_def solve_equation)
   218 
   219 lemma (in group) coset_join3:
   220   assumes "x \<in> carrier G" "subgroup H G" "x \<in> H"
   221   shows "x <# H = H"
   222 proof
   223   have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> h \<in> H" using assms
   224     by (simp add: subgroup.m_closed)
   225   thus "x <# H \<subseteq> H" unfolding l_coset_def by blast
   226 next
   227   have "\<And>h. h \<in> H \<Longrightarrow> x \<otimes> ((inv x) \<otimes> h) = h"
   228     by (smt assms inv_closed l_one m_assoc r_inv subgroup.mem_carrier)
   229   moreover have "\<And>h. h \<in> H \<Longrightarrow> (inv x) \<otimes> h \<in> H"
   230     by (simp add: assms subgroup.m_closed subgroup.m_inv_closed)
   231   ultimately show "H \<subseteq> x <# H" unfolding l_coset_def by blast
   232 qed
   233 
   234 lemma (in monoid) r_coset_subset_G:
   235   "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> H #> x \<subseteq> carrier G"
   236 by (auto simp add: r_coset_def)
   237 
   238 lemma (in group) rcosI:
   239   "\<lbrakk> h \<in> H; H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> h \<otimes> x \<in> H #> x"
   240 by (auto simp add: r_coset_def)
   241 
   242 lemma (in group) rcosetsI:
   243      "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H"
   244 by (auto simp add: RCOSETS_def)
   245 
   246 lemma (in group) rcos_self:
   247   "\<lbrakk> x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> x \<in> H #> x"
   248   by (metis l_one rcosI subgroup_def)
   249 
   250 text (in group) \<open>Opposite of @{thm [source] "repr_independence"}\<close>
   251 lemma (in group) repr_independenceD:
   252   assumes "subgroup H G" "y \<in> carrier G"
   253     and "H #> x = H #> y"
   254   shows "y \<in> H #> x"
   255   using assms by (simp add: rcos_self)
   256 
   257 text \<open>Elements of a right coset are in the carrier\<close>
   258 lemma (in subgroup) elemrcos_carrier:
   259   assumes "group G" "a \<in> carrier G"
   260     and "a' \<in> H #> a"
   261   shows "a' \<in> carrier G"
   262   by (meson assms group.is_monoid monoid.r_coset_subset_G subset subsetCE)
   263 
   264 lemma (in subgroup) rcos_const:
   265   assumes "group G" "h \<in> H"
   266   shows "H #> h = H"
   267   using group.coset_join2[OF assms(1), of h H]
   268   by (simp add: assms(2) subgroup_axioms)
   269 
   270 lemma (in subgroup) rcos_module_imp:
   271   assumes "group G" "x \<in> carrier G"
   272     and "x' \<in> H #> x"
   273   shows "(x' \<otimes> inv x) \<in> H"
   274 proof -
   275   obtain h where h: "h \<in> H" "x' = h \<otimes> x"
   276     using assms(3) unfolding r_coset_def by blast
   277   hence "x' \<otimes> inv x = h"
   278     by (metis assms elemrcos_carrier group.inv_solve_right mem_carrier)
   279   thus ?thesis using h by blast
   280 qed
   281 
   282 lemma (in subgroup) rcos_module_rev:
   283   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
   284     and "(x' \<otimes> inv x) \<in> H"
   285   shows "x' \<in> H #> x"
   286 proof -
   287   obtain h where h: "h \<in> H" "x' \<otimes> inv x = h"
   288     using assms(4) unfolding r_coset_def by blast
   289   hence "x' = h \<otimes> x"
   290     by (metis assms group.inv_solve_right mem_carrier)
   291   thus ?thesis using h unfolding r_coset_def by blast
   292 qed
   293 
   294 text \<open>Module property of right cosets\<close>
   295 lemma (in subgroup) rcos_module:
   296   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
   297   shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)"
   298   using rcos_module_rev rcos_module_imp assms by blast
   299 
   300 text \<open>Right cosets are subsets of the carrier.\<close> 
   301 lemma (in subgroup) rcosets_carrier:
   302   assumes "group G" "X \<in> rcosets H"
   303   shows "X \<subseteq> carrier G"
   304   using assms elemrcos_carrier singletonD
   305   subset_eq unfolding RCOSETS_def by force 
   306 
   307 
   308 text \<open>Multiplication of general subsets\<close>
   309 
   310 lemma (in comm_group) mult_subgroups:
   311   assumes "subgroup H G" and "subgroup K G"
   312   shows "subgroup (H <#> K) G"
   313 proof (rule subgroup.intro)
   314   show "H <#> K \<subseteq> carrier G"
   315     by (simp add: setmult_subset_G assms subgroup.subset)
   316 next
   317   have "\<one> \<otimes> \<one> \<in> H <#> K"
   318     unfolding set_mult_def using assms subgroup.one_closed by blast
   319   thus "\<one> \<in> H <#> K" by simp
   320 next
   321   show "\<And>x. x \<in> H <#> K \<Longrightarrow> inv x \<in> H <#> K"
   322   proof -
   323     fix x assume "x \<in> H <#> K"
   324     then obtain h k where hk: "h \<in> H" "k \<in> K" "x = h \<otimes> k"
   325       unfolding set_mult_def by blast
   326     hence "inv x = (inv k) \<otimes> (inv h)"
   327       by (meson inv_mult_group assms subgroup.mem_carrier)
   328     hence "inv x = (inv h) \<otimes> (inv k)"
   329       by (metis hk inv_mult assms subgroup.mem_carrier)
   330     thus "inv x \<in> H <#> K"
   331       unfolding set_mult_def using hk assms
   332       by (metis (no_types, lifting) UN_iff singletonI subgroup_def)
   333   qed
   334 next
   335   show "\<And>x y. x \<in> H <#> K \<Longrightarrow> y \<in> H <#> K \<Longrightarrow> x \<otimes> y \<in> H <#> K"
   336   proof -
   337     fix x y assume "x \<in> H <#> K" "y \<in> H <#> K"
   338     then obtain h1 k1 h2 k2 where h1k1: "h1 \<in> H" "k1 \<in> K" "x = h1 \<otimes> k1"
   339                               and h2k2: "h2 \<in> H" "k2 \<in> K" "y = h2 \<otimes> k2"
   340       unfolding set_mult_def by blast
   341     hence "x \<otimes> y = (h1 \<otimes> k1) \<otimes> (h2 \<otimes> k2)" by simp
   342     also have " ... = h1 \<otimes> (k1 \<otimes> h2) \<otimes> k2"
   343       by (smt h1k1 h2k2 m_assoc m_closed assms subgroup.mem_carrier)
   344     also have " ... = h1 \<otimes> (h2 \<otimes> k1) \<otimes> k2"
   345       by (metis (no_types, hide_lams) assms m_comm h1k1(2) h2k2(1) subgroup.mem_carrier)
   346     finally have "x \<otimes> y  = (h1 \<otimes> h2) \<otimes> (k1 \<otimes> k2)"
   347       by (smt assms h1k1 h2k2 m_assoc monoid.m_closed monoid_axioms subgroup.mem_carrier)
   348     thus "x \<otimes> y \<in> H <#> K" unfolding set_mult_def
   349       using subgroup.m_closed[OF assms(1) h1k1(1) h2k2(1)]
   350             subgroup.m_closed[OF assms(2) h1k1(2) h2k2(2)] by blast
   351   qed
   352 qed
   353 
   354 lemma (in subgroup) lcos_module_rev:
   355   assumes "group G" "x \<in> carrier G" "x' \<in> carrier G"
   356     and "(inv x \<otimes> x') \<in> H"
   357   shows "x' \<in> x <# H"
   358 proof -
   359   obtain h where h: "h \<in> H" "inv x \<otimes> x' = h"
   360     using assms(4) unfolding l_coset_def by blast
   361   hence "x' = x \<otimes> h"
   362     by (metis assms group.inv_solve_left mem_carrier)
   363   thus ?thesis using h unfolding l_coset_def by blast
   364 qed
   365 
   366 
   367 subsection \<open>Normal subgroups\<close>
   368 
   369 lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G"
   370   by (simp add: normal_def subgroup_def)
   371 
   372 lemma (in group) normalI: 
   373   "subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
   374   by (simp add: normal_def normal_axioms_def is_group)
   375 
   376 lemma (in normal) inv_op_closed1:
   377   assumes "x \<in> carrier G" and "h \<in> H"
   378   shows "(inv x) \<otimes> h \<otimes> x \<in> H"
   379 proof -
   380   have "h \<otimes> x \<in> x <# H"
   381     using assms coset_eq assms(1) unfolding r_coset_def by blast 
   382   then obtain h' where "h' \<in> H" "h \<otimes> x = x \<otimes> h'"
   383     unfolding l_coset_def by blast
   384   thus ?thesis by (metis assms inv_closed l_inv l_one m_assoc mem_carrier) 
   385 qed
   386 
   387 lemma (in normal) inv_op_closed2:
   388   assumes "x \<in> carrier G" and "h \<in> H"
   389   shows "x \<otimes> h \<otimes> (inv x) \<in> H"
   390   using assms inv_op_closed1 by (metis inv_closed inv_inv) 
   391 
   392 
   393 text\<open>Alternative characterization of normal subgroups\<close>
   394 lemma (in group) normal_inv_iff:
   395      "(N \<lhd> G) = 
   396       (subgroup N G \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))"
   397       (is "_ = ?rhs")
   398 proof
   399   assume N: "N \<lhd> G"
   400   show ?rhs
   401     by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
   402 next
   403   assume ?rhs
   404   hence sg: "subgroup N G" 
   405     and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto
   406   hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
   407   show "N \<lhd> G"
   408   proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify)
   409     fix x
   410     assume x: "x \<in> carrier G"
   411     show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})"
   412     proof
   413       show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})"
   414       proof clarify
   415         fix n
   416         assume n: "n \<in> N" 
   417         show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})"
   418         proof 
   419           from closed [of "inv x"]
   420           show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n)
   421           show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}"
   422             by (simp add: x n m_assoc [symmetric] sb [THEN subsetD])
   423         qed
   424       qed
   425     next
   426       show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})"
   427       proof clarify
   428         fix n
   429         assume n: "n \<in> N" 
   430         show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})"
   431         proof 
   432           show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed)
   433           show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}"
   434             by (simp add: x n m_assoc sb [THEN subsetD])
   435         qed
   436       qed
   437     qed
   438   qed
   439 qed
   440 
   441 corollary (in group) normal_invI:
   442   assumes "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
   443   shows "N \<lhd> G"
   444   using assms normal_inv_iff by blast
   445 
   446 corollary (in group) normal_invE:
   447   assumes "N \<lhd> G" 
   448   shows "subgroup N G" and "\<And>x h. \<lbrakk> x \<in> carrier G; h \<in> N \<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> N"
   449   using assms normal_inv_iff apply blast
   450   by (simp add: assms normal.inv_op_closed2) 
   451 
   452 
   453 lemma (in group) one_is_normal :
   454    "{\<one>} \<lhd> G" 
   455 proof(intro normal_invI )
   456   show "subgroup {\<one>} G"
   457     by (simp add: subgroup_def)
   458   show "\<And>x h. x \<in> carrier G \<Longrightarrow> h \<in> {\<one>} \<Longrightarrow> x \<otimes> h \<otimes> inv x \<in> {\<one>}" by simp
   459 qed
   460 
   461 
   462 subsection\<open>More Properties of Left Cosets\<close>
   463 
   464 lemma (in group) l_repr_independence:
   465   assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G"
   466   shows "x <# H = y <# H"
   467 proof -
   468   obtain h' where h': "h' \<in> H" "y = x \<otimes> h'"
   469     using assms(1) unfolding l_coset_def by blast
   470   hence "\<And> h. h \<in> H \<Longrightarrow> x \<otimes> h = y \<otimes> ((inv h') \<otimes> h)"
   471     by (smt assms(2-3) inv_closed inv_solve_right m_assoc m_closed subgroup.mem_carrier)
   472   hence "\<And> xh. xh \<in> x <# H \<Longrightarrow> xh \<in> y <# H"
   473     unfolding l_coset_def by (metis (no_types, lifting) UN_iff assms(3) h'(1) subgroup_def) 
   474   moreover have "\<And> h. h \<in> H \<Longrightarrow> y \<otimes> h = x \<otimes> (h' \<otimes> h)"
   475     using h' by (meson assms(2) assms(3) m_assoc subgroup.mem_carrier)
   476   hence "\<And> yh. yh \<in> y <# H \<Longrightarrow> yh \<in> x <# H"
   477     unfolding l_coset_def using subgroup.m_closed[OF assms(3) h'(1)] by blast
   478   ultimately show ?thesis by blast
   479 qed
   480 
   481 lemma (in group) lcos_m_assoc:
   482   "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <# (h <# M) = (g \<otimes> h) <# M"
   483 by (force simp add: l_coset_def m_assoc)
   484 
   485 lemma (in group) lcos_mult_one: "M \<subseteq> carrier G \<Longrightarrow> \<one> <# M = M"
   486 by (force simp add: l_coset_def)
   487 
   488 lemma (in group) l_coset_subset_G:
   489   "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <# H \<subseteq> carrier G"
   490 by (auto simp add: l_coset_def subsetD)
   491 
   492 lemma (in group) l_coset_carrier:
   493   "\<lbrakk> y \<in> x <# H; x \<in> carrier G; subgroup H G \<rbrakk> \<Longrightarrow> y \<in> carrier G"
   494   by (auto simp add: l_coset_def m_assoc  subgroup.subset [THEN subsetD] subgroup.m_closed)
   495 
   496 lemma (in group) l_coset_swap:
   497   assumes "y \<in> x <# H" "x \<in> carrier G" "subgroup H G" 
   498   shows "x \<in> y <# H"
   499   using assms(2) l_repr_independence[OF assms] subgroup.one_closed[OF assms(3)]
   500   unfolding l_coset_def by fastforce
   501 
   502 lemma (in group) subgroup_mult_id:
   503   assumes "subgroup H G"
   504   shows "H <#> H = H"
   505 proof
   506   show "H <#> H \<subseteq> H"
   507     unfolding set_mult_def using subgroup.m_closed[OF assms] by (simp add: UN_subset_iff)
   508   show "H \<subseteq> H <#> H"
   509   proof
   510     fix x assume x: "x \<in> H" thus "x \<in> H <#> H" unfolding set_mult_def
   511       using subgroup.m_closed[OF assms subgroup.one_closed[OF assms] x] subgroup.one_closed[OF assms]
   512       by (smt UN_iff assms coset_join3 l_coset_def subgroup.mem_carrier)
   513   qed
   514 qed
   515 
   516 
   517 subsubsection \<open>Set of Inverses of an \<open>r_coset\<close>.\<close>
   518 
   519 lemma (in normal) rcos_inv:
   520   assumes x:     "x \<in> carrier G"
   521   shows "set_inv (H #> x) = H #> (inv x)" 
   522 proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe)
   523   fix h
   524   assume h: "h \<in> H"
   525   show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})"
   526   proof
   527     show "inv x \<otimes> inv h \<otimes> x \<in> H"
   528       by (simp add: inv_op_closed1 h x)
   529     show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}"
   530       by (simp add: h x m_assoc)
   531   qed
   532   show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})"
   533   proof
   534     show "x \<otimes> inv h \<otimes> inv x \<in> H"
   535       by (simp add: inv_op_closed2 h x)
   536     show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}"
   537       by (simp add: h x m_assoc [symmetric] inv_mult_group)
   538   qed
   539 qed
   540 
   541 
   542 subsubsection \<open>Theorems for \<open><#>\<close> with \<open>#>\<close> or \<open><#\<close>.\<close>
   543 
   544 lemma (in group) setmult_rcos_assoc:
   545   "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
   546     H <#> (K #> x) = (H <#> K) #> x"
   547   using set_mult_assoc[of H K "{x}"] by (simp add: r_coset_eq_set_mult)
   548 
   549 lemma (in group) rcos_assoc_lcos:
   550   "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow>
   551    (H #> x) <#> K = H <#> (x <# K)"
   552   using set_mult_assoc[of H "{x}" K]
   553   by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult)
   554 
   555 lemma (in normal) rcos_mult_step1:
   556   "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow>
   557    (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y"
   558   by (simp add: setmult_rcos_assoc r_coset_subset_G
   559                 subset l_coset_subset_G rcos_assoc_lcos)
   560 
   561 lemma (in normal) rcos_mult_step2:
   562      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   563       \<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y"
   564 by (insert coset_eq, simp add: normal_def)
   565 
   566 lemma (in normal) rcos_mult_step3:
   567      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   568       \<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)"
   569 by (simp add: setmult_rcos_assoc coset_mult_assoc
   570               subgroup_mult_id normal.axioms subset normal_axioms)
   571 
   572 lemma (in normal) rcos_sum:
   573      "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   574       \<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)"
   575 by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3)
   576 
   577 lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M"
   578   \<comment> \<open>generalizes \<open>subgroup_mult_id\<close>\<close>
   579   by (auto simp add: RCOSETS_def subset
   580         setmult_rcos_assoc subgroup_mult_id normal.axioms normal_axioms)
   581 
   582 
   583 subsubsection\<open>An Equivalence Relation\<close>
   584 
   585 definition
   586   r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
   587   where "rcong\<^bsub>G\<^esub> H = {(x,y). x \<in> carrier G \<and> y \<in> carrier G \<and> inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
   588 
   589 
   590 lemma (in subgroup) equiv_rcong:
   591    assumes "group G"
   592    shows "equiv (carrier G) (rcong H)"
   593 proof -
   594   interpret group G by fact
   595   show ?thesis
   596   proof (intro equivI)
   597     show "refl_on (carrier G) (rcong H)"
   598       by (auto simp add: r_congruent_def refl_on_def) 
   599   next
   600     show "sym (rcong H)"
   601     proof (simp add: r_congruent_def sym_def, clarify)
   602       fix x y
   603       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 
   604          and "inv x \<otimes> y \<in> H"
   605       hence "inv (inv x \<otimes> y) \<in> H" by simp
   606       thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group)
   607     qed
   608   next
   609     show "trans (rcong H)"
   610     proof (simp add: r_congruent_def trans_def, clarify)
   611       fix x y z
   612       assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G"
   613          and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H"
   614       hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp
   615       hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H"
   616         by (simp add: m_assoc del: r_inv Units_r_inv) 
   617       thus "inv x \<otimes> z \<in> H" by simp
   618     qed
   619   qed
   620 qed
   621 
   622 text\<open>Equivalence classes of \<open>rcong\<close> correspond to left cosets.
   623   Was there a mistake in the definitions? I'd have expected them to
   624   correspond to right cosets.\<close>
   625 
   626 (* CB: This is correct, but subtle.
   627    We call H #> a the right coset of a relative to H.  According to
   628    Jacobson, this is what the majority of group theory literature does.
   629    He then defines the notion of congruence relation ~ over monoids as
   630    equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'.
   631    Our notion of right congruence induced by K: rcong K appears only in
   632    the context where K is a normal subgroup.  Jacobson doesn't name it.
   633    But in this context left and right cosets are identical.
   634 *)
   635 
   636 lemma (in subgroup) l_coset_eq_rcong:
   637   assumes "group G"
   638   assumes a: "a \<in> carrier G"
   639   shows "a <# H = (rcong H) `` {a}"
   640 proof -
   641   interpret group G by fact
   642   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
   643 qed
   644 
   645 
   646 subsubsection\<open>Two Distinct Right Cosets are Disjoint\<close>
   647 
   648 lemma (in group) rcos_equation:
   649   assumes "subgroup H G"
   650   assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H"
   651   shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})"
   652 proof -
   653   interpret subgroup H G by fact
   654   from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"])
   655     apply blast by (simp add: inv_solve_left m_assoc)
   656 qed
   657 
   658 lemma (in group) rcos_disjoint:
   659   assumes "subgroup H G"
   660   assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b"
   661   shows "a \<inter> b = {}"
   662 proof -
   663   interpret subgroup H G by fact
   664   from p show ?thesis
   665     apply (simp add: RCOSETS_def r_coset_def)
   666     apply (blast intro: rcos_equation assms sym)
   667     done
   668 qed
   669 
   670 
   671 subsection \<open>Further lemmas for \<open>r_congruent\<close>\<close>
   672 
   673 text \<open>The relation is a congruence\<close>
   674 
   675 lemma (in normal) congruent_rcong:
   676   shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)"
   677 proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group)
   678   fix a b c
   679   assume abrcong: "(a, b) \<in> rcong H"
   680     and ccarr: "c \<in> carrier G"
   681 
   682   from abrcong
   683       have acarr: "a \<in> carrier G"
   684         and bcarr: "b \<in> carrier G"
   685         and abH: "inv a \<otimes> b \<in> H"
   686       unfolding r_congruent_def
   687       by fast+
   688 
   689   note carr = acarr bcarr ccarr
   690 
   691   from ccarr and abH
   692       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1)
   693   moreover
   694       from carr and inv_closed
   695       have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
   696       by (force cong: m_assoc)
   697   moreover 
   698       from carr and inv_closed
   699       have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)"
   700       by (simp add: inv_mult_group)
   701   ultimately
   702       have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp
   703   from carr and this
   704      have "(b \<otimes> c) \<in> (a \<otimes> c) <# H"
   705      by (simp add: lcos_module_rev[OF is_group])
   706   from carr and this and is_subgroup
   707      show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+)
   708 next
   709   fix a b c
   710   assume abrcong: "(a, b) \<in> rcong H"
   711     and ccarr: "c \<in> carrier G"
   712 
   713   from ccarr have "c \<in> Units G" by simp
   714   hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv)
   715 
   716   from abrcong
   717       have acarr: "a \<in> carrier G"
   718        and bcarr: "b \<in> carrier G"
   719        and abH: "inv a \<otimes> b \<in> H"
   720       by (unfold r_congruent_def, fast+)
   721 
   722   note carr = acarr bcarr ccarr
   723 
   724   from carr and inv_closed
   725      have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp
   726   also from carr and inv_closed
   727       have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp
   728   also from carr and inv_closed
   729       have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc)
   730   also from carr and inv_closed
   731       have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group)
   732   finally
   733       have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" .
   734   from abH and this
   735       have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp
   736 
   737   from carr and this
   738      have "(c \<otimes> b) \<in> (c \<otimes> a) <# H"
   739      by (simp add: lcos_module_rev[OF is_group])
   740   from carr and this and is_subgroup
   741      show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+)
   742 qed
   743 
   744 
   745 subsection \<open>Order of a Group and Lagrange's Theorem\<close>
   746 
   747 definition
   748   order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
   749   where "order S = card (carrier S)"
   750 
   751 lemma (in monoid) order_gt_0_iff_finite: "0 < order G \<longleftrightarrow> finite (carrier G)"
   752 by(auto simp add: order_def card_gt_0_iff)
   753 
   754 lemma (in group) rcosets_part_G:
   755   assumes "subgroup H G"
   756   shows "\<Union>(rcosets H) = carrier G"
   757 proof -
   758   interpret subgroup H G by fact
   759   show ?thesis
   760     apply (rule equalityI)
   761     apply (force simp add: RCOSETS_def r_coset_def)
   762     apply (auto simp add: RCOSETS_def intro: rcos_self assms)
   763     done
   764 qed
   765 
   766 lemma (in group) cosets_finite:
   767      "\<lbrakk>c \<in> rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   768 apply (auto simp add: RCOSETS_def)
   769 apply (simp add: r_coset_subset_G [THEN finite_subset])
   770 done
   771 
   772 text\<open>The next two lemmas support the proof of \<open>card_cosets_equal\<close>.\<close>
   773 lemma (in group) inj_on_f:
   774     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)"
   775 apply (rule inj_onI)
   776 apply (subgoal_tac "x \<in> carrier G \<and> y \<in> carrier G")
   777  prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD])
   778 apply (simp add: subsetD)
   779 done
   780 
   781 lemma (in group) inj_on_g:
   782     "\<lbrakk>H \<subseteq> carrier G;  a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H"
   783 by (force simp add: inj_on_def subsetD)
   784 
   785 (* ************************************************************************** *)
   786 
   787 lemma (in group) card_cosets_equal:
   788   assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
   789   shows "\<exists>f. bij_betw f H R"
   790 proof -
   791   obtain g where g: "g \<in> carrier G" "R = H #> g"
   792     using assms(1) unfolding RCOSETS_def by blast
   793 
   794   let ?f = "\<lambda>h. h \<otimes> g"
   795   have "\<And>r. r \<in> R \<Longrightarrow> \<exists>h \<in> H. ?f h = r"
   796   proof -
   797     fix r assume "r \<in> R"
   798     then obtain h where "h \<in> H" "r = h \<otimes> g"
   799       using g unfolding r_coset_def by blast
   800     thus "\<exists>h \<in> H. ?f h = r" by blast
   801   qed
   802   hence "R \<subseteq> ?f ` H" by blast
   803   moreover have "?f ` H \<subseteq> R"
   804     using g unfolding r_coset_def by blast
   805   ultimately show ?thesis using inj_on_g unfolding bij_betw_def
   806     using assms(2) g(1) by auto 
   807 qed
   808 
   809 corollary (in group) card_rcosets_equal:
   810   assumes "R \<in> rcosets H" "H \<subseteq> carrier G"
   811   shows "card H = card R"
   812   using card_cosets_equal assms bij_betw_same_card by blast
   813 
   814 corollary (in group) rcosets_finite:
   815   assumes "R \<in> rcosets H" "H \<subseteq> carrier G" "finite H"
   816   shows "finite R"
   817   using card_cosets_equal assms bij_betw_finite is_group by blast
   818 
   819 (* ************************************************************************** *)
   820 
   821 lemma (in group) rcosets_subset_PowG:
   822      "subgroup H G  \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)"
   823   using rcosets_part_G by auto
   824 
   825 proposition (in group) lagrange_finite:
   826      "\<lbrakk>finite(carrier G); subgroup H G\<rbrakk>
   827       \<Longrightarrow> card(rcosets H) * card(H) = order(G)"
   828 apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric])
   829 apply (subst mult.commute)
   830 apply (rule card_partition)
   831    apply (simp add: rcosets_subset_PowG [THEN finite_subset])
   832   apply (simp add: rcosets_part_G)
   833   apply (simp add: card_rcosets_equal subgroup.subset)
   834 apply (simp add: rcos_disjoint)
   835 done
   836 
   837 theorem (in group) lagrange:
   838   assumes "subgroup H G"
   839   shows "card (rcosets H) * card H = order G"
   840 proof (cases "finite (carrier G)")
   841   case True thus ?thesis using lagrange_finite assms by simp
   842 next
   843   case False note inf_G = this
   844   thus ?thesis
   845   proof (cases "finite H")
   846     case False thus ?thesis using inf_G  by (simp add: order_def)  
   847   next
   848     case True note finite_H = this
   849     have "infinite (rcosets H)"
   850     proof (rule ccontr)
   851       assume "\<not> infinite (rcosets H)"
   852       hence finite_rcos: "finite (rcosets H)" by simp
   853       hence "card (\<Union>(rcosets H)) = (\<Sum>R\<in>(rcosets H). card R)"
   854         using card_Union_disjoint[of "rcosets H"] finite_H rcos_disjoint[OF assms(1)]
   855               rcosets_finite[where ?H = H] by (simp add: assms subgroup.subset)
   856       hence "order G = (\<Sum>R\<in>(rcosets H). card R)"
   857         by (simp add: assms order_def rcosets_part_G)
   858       hence "order G = (\<Sum>R\<in>(rcosets H). card H)"
   859         using card_rcosets_equal by (simp add: assms subgroup.subset)
   860       hence "order G = (card H) * (card (rcosets H))" by simp
   861       hence "order G \<noteq> 0" using finite_rcos finite_H assms ex_in_conv
   862                                 rcosets_part_G subgroup.one_closed by fastforce
   863       thus False using inf_G order_gt_0_iff_finite by blast 
   864     qed
   865     thus ?thesis using inf_G by (simp add: order_def)
   866   qed
   867 qed
   868 
   869 
   870 subsection \<open>Quotient Groups: Factorization of a Group\<close>
   871 
   872 definition
   873   FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
   874     \<comment> \<open>Actually defined for groups rather than monoids\<close>
   875    where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
   876 
   877 lemma (in normal) setmult_closed:
   878      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
   879 by (auto simp add: rcos_sum RCOSETS_def)
   880 
   881 lemma (in normal) setinv_closed:
   882      "K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H"
   883 by (auto simp add: rcos_inv RCOSETS_def)
   884 
   885 lemma (in normal) rcosets_assoc:
   886      "\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk>
   887       \<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
   888   by (simp add: group.set_mult_assoc is_group rcosets_carrier)
   889 
   890 lemma (in subgroup) subgroup_in_rcosets:
   891   assumes "group G"
   892   shows "H \<in> rcosets H"
   893 proof -
   894   interpret group G by fact
   895   from _ subgroup_axioms have "H #> \<one> = H"
   896     by (rule coset_join2) auto
   897   then show ?thesis
   898     by (auto simp add: RCOSETS_def)
   899 qed
   900 
   901 lemma (in normal) rcosets_inv_mult_group_eq:
   902      "M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H"
   903 by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms normal_axioms)
   904 
   905 theorem (in normal) factorgroup_is_group:
   906   "group (G Mod H)"
   907 apply (simp add: FactGroup_def)
   908 apply (rule groupI)
   909     apply (simp add: setmult_closed)
   910    apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group])
   911   apply (simp add: restrictI setmult_closed rcosets_assoc)
   912  apply (simp add: normal_imp_subgroup
   913                   subgroup_in_rcosets rcosets_mult_eq)
   914 apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed)
   915 done
   916 
   917 lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
   918   by (simp add: FactGroup_def) 
   919 
   920 lemma (in normal) inv_FactGroup:
   921      "X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X"
   922 apply (rule group.inv_equality [OF factorgroup_is_group]) 
   923 apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq)
   924 done
   925 
   926 text\<open>The coset map is a homomorphism from @{term G} to the quotient group
   927   @{term "G Mod H"}\<close>
   928 lemma (in normal) r_coset_hom_Mod:
   929   "(\<lambda>a. H #> a) \<in> hom G (G Mod H)"
   930   by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum)
   931 
   932  
   933 subsection\<open>The First Isomorphism Theorem\<close>
   934 
   935 text\<open>The quotient by the kernel of a homomorphism is isomorphic to the 
   936   range of that homomorphism.\<close>
   937 
   938 definition
   939   kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
   940     \<comment> \<open>the kernel of a homomorphism\<close>
   941   where "kernel G H h = {x. x \<in> carrier G \<and> h x = \<one>\<^bsub>H\<^esub>}"
   942 
   943 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
   944 apply (rule subgroup.intro) 
   945 apply (auto simp add: kernel_def group.intro is_group) 
   946 done
   947 
   948 text\<open>The kernel of a homomorphism is a normal subgroup\<close>
   949 lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G"
   950 apply (simp add: G.normal_inv_iff subgroup_kernel)
   951 apply (simp add: kernel_def)
   952 done
   953 
   954 lemma (in group_hom) FactGroup_nonempty:
   955   assumes X: "X \<in> carrier (G Mod kernel G H h)"
   956   shows "X \<noteq> {}"
   957 proof -
   958   from X
   959   obtain g where "g \<in> carrier G" 
   960              and "X = kernel G H h #> g"
   961     by (auto simp add: FactGroup_def RCOSETS_def)
   962   thus ?thesis 
   963    by (auto simp add: kernel_def r_coset_def image_def intro: hom_one)
   964 qed
   965 
   966 
   967 lemma (in group_hom) FactGroup_the_elem_mem:
   968   assumes X: "X \<in> carrier (G Mod (kernel G H h))"
   969   shows "the_elem (h`X) \<in> carrier H"
   970 proof -
   971   from X
   972   obtain g where g: "g \<in> carrier G" 
   973              and "X = kernel G H h #> g"
   974     by (auto simp add: FactGroup_def RCOSETS_def)
   975   hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def g intro!: imageI)
   976   thus ?thesis by (auto simp add: g)
   977 qed
   978 
   979 lemma (in group_hom) FactGroup_hom:
   980      "(\<lambda>X. the_elem (h`X)) \<in> hom (G Mod (kernel G H h)) H"
   981 apply (simp add: hom_def FactGroup_the_elem_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed)
   982 proof (intro ballI)
   983   fix X and X'
   984   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
   985      and X': "X' \<in> carrier (G Mod kernel G H h)"
   986   then
   987   obtain g and g'
   988            where "g \<in> carrier G" and "g' \<in> carrier G" 
   989              and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
   990     by (auto simp add: FactGroup_def RCOSETS_def)
   991   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
   992     and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
   993     by (force simp add: kernel_def r_coset_def image_def)+
   994   hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
   995     by (auto dest!: FactGroup_nonempty intro!: image_eqI
   996              simp add: set_mult_def 
   997                        subsetD [OF Xsub] subsetD [OF X'sub]) 
   998   then show "the_elem (h ` (X <#> X')) = the_elem (h ` X) \<otimes>\<^bsub>H\<^esub> the_elem (h ` X')"
   999     by (auto simp add: all FactGroup_nonempty X X' the_elem_image_unique)
  1000 qed
  1001 
  1002 
  1003 text\<open>Lemma for the following injectivity result\<close>
  1004 lemma (in group_hom) FactGroup_subset:
  1005      "\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk>
  1006       \<Longrightarrow>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
  1007 apply (clarsimp simp add: kernel_def r_coset_def)
  1008 apply (rename_tac y)  
  1009 apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 
  1010 apply (simp add: G.m_assoc) 
  1011 done
  1012 
  1013 lemma (in group_hom) FactGroup_inj_on:
  1014      "inj_on (\<lambda>X. the_elem (h ` X)) (carrier (G Mod kernel G H h))"
  1015 proof (simp add: inj_on_def, clarify) 
  1016   fix X and X'
  1017   assume X:  "X  \<in> carrier (G Mod kernel G H h)"
  1018      and X': "X' \<in> carrier (G Mod kernel G H h)"
  1019   then
  1020   obtain g and g'
  1021            where gX: "g \<in> carrier G"  "g' \<in> carrier G" 
  1022               "X = kernel G H h #> g" "X' = kernel G H h #> g'"
  1023     by (auto simp add: FactGroup_def RCOSETS_def)
  1024   hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
  1025     by (force simp add: kernel_def r_coset_def image_def)+
  1026   assume "the_elem (h ` X) = the_elem (h ` X')"
  1027   hence h: "h g = h g'"
  1028     by (simp add: all FactGroup_nonempty X X' the_elem_image_unique) 
  1029   show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 
  1030 qed
  1031 
  1032 text\<open>If the homomorphism @{term h} is onto @{term H}, then so is the
  1033 homomorphism from the quotient group\<close>
  1034 lemma (in group_hom) FactGroup_onto:
  1035   assumes h: "h ` carrier G = carrier H"
  1036   shows "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
  1037 proof
  1038   show "(\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
  1039     by (auto simp add: FactGroup_the_elem_mem)
  1040   show "carrier H \<subseteq> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)"
  1041   proof
  1042     fix y
  1043     assume y: "y \<in> carrier H"
  1044     with h obtain g where g: "g \<in> carrier G" "h g = y"
  1045       by (blast elim: equalityE) 
  1046     hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
  1047       by (auto simp add: y kernel_def r_coset_def) 
  1048     with g show "y \<in> (\<lambda>X. the_elem (h ` X)) ` carrier (G Mod kernel G H h)" 
  1049       apply (auto intro!: bexI image_eqI simp add: FactGroup_def RCOSETS_def)
  1050       apply (subst the_elem_image_unique)
  1051       apply auto
  1052       done
  1053   qed
  1054 qed
  1055 
  1056 
  1057 text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
  1058  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
  1059 theorem (in group_hom) FactGroup_iso_set:
  1060   "h ` carrier G = carrier H
  1061    \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G Mod (kernel G H h)) H"
  1062 by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
  1063               FactGroup_onto) 
  1064 
  1065 corollary (in group_hom) FactGroup_iso :
  1066   "h ` carrier G = carrier H
  1067    \<Longrightarrow> (G Mod (kernel G H h))\<cong> H"
  1068   using FactGroup_iso_set unfolding is_iso_def by auto
  1069 
  1070 
  1071 (* Next two lemmas contributed by Paulo Emílio de Vilhena. *)
  1072 
  1073 lemma (in group_hom) trivial_hom_iff:
  1074   "(h ` (carrier G) = { \<one>\<^bsub>H\<^esub> }) = (kernel G H h = carrier G)"
  1075   unfolding kernel_def using one_closed by force
  1076 
  1077 lemma (in group_hom) trivial_ker_imp_inj:
  1078   assumes "kernel G H h = { \<one> }"
  1079   shows "inj_on h (carrier G)"
  1080 proof (rule inj_onI)
  1081   fix g1 g2 assume A: "g1 \<in> carrier G" "g2 \<in> carrier G" "h g1 = h g2"
  1082   hence "h (g1 \<otimes> (inv g2)) = \<one>\<^bsub>H\<^esub>" by simp
  1083   hence "g1 \<otimes> (inv g2) = \<one>"
  1084     using A assms unfolding kernel_def by blast
  1085   thus "g1 = g2"
  1086     using A G.inv_equality G.inv_inv by blast
  1087 qed
  1088 
  1089 
  1090 (* Next subsection contributed by Martin Baillon. *)
  1091 
  1092 subsection \<open>Theorems about Factor Groups and Direct product\<close>
  1093 
  1094 lemma (in group) DirProd_normal :
  1095   assumes "group K"
  1096     and "H \<lhd> G"
  1097     and "N \<lhd> K"
  1098   shows "H \<times> N \<lhd> G \<times>\<times> K"
  1099 proof (intro group.normal_invI[OF DirProd_group[OF group_axioms assms(1)]])
  1100   show sub : "subgroup (H \<times> N) (G \<times>\<times> K)"
  1101     using DirProd_subgroups[OF group_axioms normal_imp_subgroup[OF assms(2)]assms(1)
  1102          normal_imp_subgroup[OF assms(3)]].
  1103   show "\<And>x h. x \<in> carrier (G\<times>\<times>K) \<Longrightarrow> h \<in> H\<times>N \<Longrightarrow> x \<otimes>\<^bsub>G\<times>\<times>K\<^esub> h \<otimes>\<^bsub>G\<times>\<times>K\<^esub> inv\<^bsub>G\<times>\<times>K\<^esub> x \<in> H\<times>N"
  1104   proof-
  1105     fix x h assume xGK : "x \<in> carrier (G \<times>\<times> K)" and hHN : " h \<in> H \<times> N"
  1106     hence hGK : "h \<in> carrier (G \<times>\<times> K)" using subgroup.subset[OF sub] by auto
  1107     from xGK obtain x1 x2 where x1x2 :"x1 \<in> carrier G" "x2 \<in> carrier K" "x = (x1,x2)"
  1108       unfolding DirProd_def by fastforce
  1109     from hHN obtain h1 h2 where h1h2 : "h1 \<in> H" "h2 \<in> N" "h = (h1,h2)"
  1110       unfolding DirProd_def by fastforce
  1111     hence h1h2GK : "h1 \<in> carrier G" "h2 \<in> carrier K"
  1112       using normal_imp_subgroup subgroup.subset assms apply blast+.
  1113     have "inv\<^bsub>G \<times>\<times> K\<^esub> x = (inv\<^bsub>G\<^esub> x1,inv\<^bsub>K\<^esub> x2)"
  1114       using inv_DirProd[OF group_axioms assms(1) x1x2(1)x1x2(2)] x1x2 by auto
  1115     hence "x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x = (x1 \<otimes> h1 \<otimes> inv x1,x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)"
  1116       using h1h2 x1x2 h1h2GK by auto
  1117     moreover have "x1 \<otimes> h1 \<otimes> inv x1 \<in> H" "x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2 \<in> N"
  1118       using normal_invE group.normal_invE[OF assms(1)] assms x1x2 h1h2 apply auto.
  1119     hence "(x1 \<otimes> h1 \<otimes> inv x1, x2 \<otimes>\<^bsub>K\<^esub> h2 \<otimes>\<^bsub>K\<^esub> inv\<^bsub>K\<^esub> x2)\<in> H \<times> N" by auto
  1120     ultimately show " x \<otimes>\<^bsub>G \<times>\<times> K\<^esub> h \<otimes>\<^bsub>G \<times>\<times> K\<^esub> inv\<^bsub>G \<times>\<times> K\<^esub> x \<in> H \<times> N" by auto
  1121   qed
  1122 qed
  1123 
  1124 lemma (in group) FactGroup_DirProd_multiplication_iso_set :
  1125   assumes "group K"
  1126     and "H \<lhd> G"
  1127     and "N \<lhd> K"
  1128   shows "(\<lambda> (X, Y). X \<times> Y) \<in> iso  ((G Mod H) \<times>\<times> (K Mod N)) (G \<times>\<times> K Mod H \<times> N)"
  1129 
  1130 proof-
  1131   have R :"(\<lambda>(X, Y). X \<times> Y) \<in> carrier (G Mod H) \<times> carrier (K Mod N) \<rightarrow> carrier (G \<times>\<times> K Mod H \<times> N)"
  1132     unfolding r_coset_def Sigma_def DirProd_def FactGroup_def RCOSETS_def apply simp by blast
  1133   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
  1134                 \<forall>ya\<in>carrier (K Mod N). (x <#> xa) \<times> (y <#>\<^bsub>K\<^esub> ya) =  x \<times> y <#>\<^bsub>G \<times>\<times> K\<^esub> xa \<times> ya)"
  1135     unfolding set_mult_def by force
  1136   moreover have "(\<forall>x\<in>carrier (G Mod H). \<forall>y\<in>carrier (K Mod N). \<forall>xa\<in>carrier (G Mod H).
  1137                  \<forall>ya\<in>carrier (K Mod N).  x \<times> y = xa \<times> ya \<longrightarrow> x = xa \<and> y = ya)"
  1138     unfolding  FactGroup_def using times_eq_iff subgroup.rcosets_non_empty
  1139     by (metis assms(2) assms(3) normal_def partial_object.select_convs(1))
  1140   moreover have "(\<lambda>(X, Y). X \<times> Y) ` (carrier (G Mod H) \<times> carrier (K Mod N)) = 
  1141                                      carrier (G \<times>\<times> K Mod H \<times> N)"
  1142     unfolding image_def  apply auto using R apply force
  1143     unfolding DirProd_def FactGroup_def RCOSETS_def r_coset_def by force
  1144   ultimately show ?thesis
  1145     unfolding iso_def hom_def bij_betw_def inj_on_def by simp
  1146 qed
  1147 
  1148 corollary (in group) FactGroup_DirProd_multiplication_iso_1 :
  1149   assumes "group K"
  1150     and "H \<lhd> G"
  1151     and "N \<lhd> K"
  1152   shows "  ((G Mod H) \<times>\<times> (K Mod N)) \<cong> (G \<times>\<times> K Mod H \<times> N)"
  1153   unfolding is_iso_def using FactGroup_DirProd_multiplication_iso_set assms by auto
  1154 
  1155 corollary (in group) FactGroup_DirProd_multiplication_iso_2 :
  1156   assumes "group K"
  1157     and "H \<lhd> G"
  1158     and "N \<lhd> K"
  1159   shows "(G \<times>\<times> K Mod H \<times> N) \<cong> ((G Mod H) \<times>\<times> (K Mod N))"
  1160   using FactGroup_DirProd_multiplication_iso_1 group.iso_sym assms
  1161         DirProd_group[OF normal.factorgroup_is_group normal.factorgroup_is_group]
  1162   by blast
  1163 
  1164 subsubsection "More Lemmas about set multiplication"
  1165 
  1166 (*A group multiplied by a subgroup stays the same*)
  1167 lemma (in group) set_mult_carrier_idem:
  1168   assumes "subgroup H G"
  1169   shows "(carrier G) <#> H = carrier G"
  1170 proof
  1171   show "(carrier G)<#>H \<subseteq> carrier G" 
  1172     unfolding set_mult_def using subgroup.subset assms by blast
  1173 next
  1174   have " (carrier G) #>  \<one> = carrier G" unfolding set_mult_def r_coset_def group_axioms by simp
  1175   moreover have "(carrier G) #>  \<one> \<subseteq> (carrier G) <#> H" unfolding set_mult_def r_coset_def
  1176     using assms subgroup.one_closed[OF assms] by blast
  1177   ultimately show "carrier G \<subseteq> (carrier G) <#> H" by simp
  1178 qed
  1179 
  1180 (*Same lemma as above, but everything is included in a subgroup*)
  1181 lemma (in group) set_mult_subgroup_idem:
  1182   assumes "subgroup H G"
  1183     and "subgroup N (G\<lparr>carrier:=H\<rparr>)"
  1184   shows "H<#>N = H"
  1185   using group.set_mult_carrier_idem[OF subgroup_imp_group] subgroup.subset assms
  1186   by (metis monoid.cases_scheme order_refl partial_object.simps(1)
  1187       partial_object.update_convs(1) subgroup_set_mult_equality)
  1188 
  1189 (*A normal subgroup is commutative with set_mult*)
  1190 lemma (in group) commut_normal:
  1191   assumes "subgroup H G"
  1192     and "N\<lhd>G"
  1193   shows "H<#>N = N<#>H" 
  1194 proof-
  1195   have aux1: "{H <#> N} = {\<Union>h\<in>H. h <# N }" unfolding set_mult_def l_coset_def by auto
  1196   also have "... = {\<Union>h\<in>H. N #> h }" using assms normal.coset_eq subgroup.mem_carrier by fastforce
  1197   moreover have aux2: "{N <#> H} = {\<Union>h\<in>H. N #> h }"unfolding set_mult_def r_coset_def by auto
  1198   ultimately show "H<#>N = N<#>H" by simp
  1199 qed
  1200 
  1201 (*Same lemma as above, but everything is included in a subgroup*)
  1202 lemma (in group) commut_normal_subgroup:
  1203   assumes "subgroup H G"
  1204     and "N\<lhd>(G\<lparr>carrier:=H\<rparr>)"
  1205     and "subgroup K (G\<lparr>carrier:=H\<rparr>)"
  1206   shows "K<#>N = N<#>K"
  1207 proof-
  1208   have "N \<subseteq> carrier (G\<lparr>carrier := H\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast
  1209   hence NH : "N \<subseteq> H" by simp
  1210   have "K \<subseteq> carrier(G\<lparr>carrier := H\<rparr>)" using subgroup.subset assms by blast
  1211   hence KH : "K \<subseteq> H" by simp
  1212   have Egal : "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = N <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> K"
  1213   using group.commut_normal[where ?G = "G\<lparr>carrier :=H\<rparr>", of K N,OF subgroup_imp_group[OF assms(1)]
  1214                assms(3) assms(2)] by auto
  1215   also have "... = N <#> K" using subgroup_set_mult_equality[of H N K, OF assms(1) NH KH] by auto
  1216   moreover have "K <#>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> N = K <#> N"
  1217     using subgroup_set_mult_equality[of H K N, OF assms(1) KH NH] by auto
  1218   ultimately show "K<#>N = N<#>K" by auto
  1219 qed
  1220 
  1221 
  1222 
  1223 subsubsection "Lemmas about intersection and normal subgroups"
  1224 
  1225 lemma (in group) normal_inter:
  1226   assumes "subgroup H G"
  1227     and "subgroup K G"
  1228     and "H1\<lhd>G\<lparr>carrier := H\<rparr>"
  1229   shows " (H1\<inter>K)\<lhd>(G\<lparr>carrier:= (H\<inter>K)\<rparr>)" 
  1230 proof-
  1231   define HK and H1K and GH and GHK
  1232     where "HK = H\<inter>K" and "H1K=H1\<inter>K" and "GH =G\<lparr>carrier := H\<rparr>" and "GHK = (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
  1233   show "H1K\<lhd>GHK"
  1234   proof (intro group.normal_invI[of GHK H1K])
  1235     show "Group.group GHK"
  1236       using GHK_def subgroups_Inter_pair subgroup_imp_group assms by blast
  1237 
  1238   next
  1239     have  H1K_incl:"subgroup H1K (G\<lparr>carrier:= (H\<inter>K)\<rparr>)"
  1240     proof(intro subgroup_incl)
  1241       show "subgroup H1K G"
  1242         using assms normal_imp_subgroup subgroups_Inter_pair incl_subgroup H1K_def by blast
  1243     next
  1244       show "subgroup (H\<inter>K) G" using HK_def subgroups_Inter_pair assms by auto
  1245     next
  1246       have "H1 \<subseteq> (carrier (G\<lparr>carrier:=H\<rparr>))" 
  1247         using  assms(3) normal_imp_subgroup subgroup.subset by blast
  1248       also have "... \<subseteq> H" by simp
  1249       thus "H1K \<subseteq>H\<inter>K" 
  1250         using H1K_def calculation by auto
  1251     qed
  1252     thus "subgroup H1K GHK" using GHK_def by simp
  1253   next
  1254     show "\<And> x h. x\<in>carrier GHK \<Longrightarrow> h\<in>H1K \<Longrightarrow> x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x\<in> H1K"
  1255     proof-
  1256       have invHK: "\<lbrakk>y\<in>HK\<rbrakk> \<Longrightarrow> inv\<^bsub>GHK\<^esub> y = inv\<^bsub>GH\<^esub> y"
  1257         using subgroup_inv_equality assms HK_def GH_def GHK_def subgroups_Inter_pair by simp
  1258       have multHK : "\<lbrakk>x\<in>HK;y\<in>HK\<rbrakk> \<Longrightarrow>  x \<otimes>\<^bsub>(G\<lparr>carrier:=HK\<rparr>)\<^esub> y =  x \<otimes> y"
  1259         using HK_def by simp
  1260       fix x assume p: "x\<in>carrier GHK"
  1261       fix h assume p2 : "h:H1K"
  1262       have "carrier(GHK)\<subseteq>HK"
  1263         using GHK_def HK_def by simp
  1264       hence xHK:"x\<in>HK" using p by auto
  1265       hence invx:"inv\<^bsub>GHK\<^esub> x = inv\<^bsub>GH\<^esub> x"
  1266         using invHK assms GHK_def HK_def GH_def subgroup_inv_equality subgroups_Inter_pair by simp
  1267       have "H1\<subseteq>carrier(GH)"
  1268         using assms GH_def normal_imp_subgroup subgroup.subset by blast
  1269       hence hHK:"h\<in>HK" 
  1270         using p2 H1K_def HK_def GH_def by auto
  1271       hence xhx_egal : "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub>x =  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x"
  1272         using invx invHK multHK GHK_def GH_def by auto
  1273       have xH:"x\<in>carrier(GH)" 
  1274         using xHK HK_def GH_def by auto 
  1275       have hH:"h\<in>carrier(GH)"
  1276         using hHK HK_def GH_def by auto 
  1277       have  "(\<forall>x\<in>carrier (GH). \<forall>h\<in>H1.  x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1)"
  1278         using assms normal_invE GH_def normal.inv_op_closed2 by fastforce
  1279       hence INCL_1 : "x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1"
  1280         using  xH H1K_def p2 by blast
  1281       have " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> HK"
  1282         using assms HK_def subgroups_Inter_pair hHK xHK
  1283         by (metis GH_def inf.cobounded1 subgroup_def subgroup_incl)
  1284       hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> K" using HK_def by simp
  1285       hence " x \<otimes>\<^bsub>GH\<^esub> h \<otimes>\<^bsub>GH\<^esub> inv\<^bsub>GH\<^esub> x \<in> H1K" using INCL_1 H1K_def by auto
  1286       thus  "x \<otimes>\<^bsub>GHK\<^esub> h \<otimes>\<^bsub>GHK\<^esub> inv\<^bsub>GHK\<^esub> x \<in> H1K" using xhx_egal by simp
  1287     qed
  1288   qed
  1289 qed
  1290 
  1291 
  1292 lemma (in group) normal_inter_subgroup:
  1293   assumes "subgroup H G"
  1294     and "N \<lhd> G"
  1295   shows "(N\<inter>H) \<lhd> (G\<lparr>carrier := H\<rparr>)"
  1296 proof -
  1297   define K where "K = carrier G"
  1298   have "G\<lparr>carrier := K\<rparr> =  G" using K_def by auto
  1299   moreover have "subgroup K G" using K_def subgroup_self by blast
  1300   moreover have "normal N (G \<lparr>carrier :=K\<rparr>)" using assms K_def by simp
  1301   ultimately have "N \<inter> H \<lhd> G\<lparr>carrier := K \<inter> H\<rparr>"
  1302     using normal_inter[of K H N] assms(1) by blast
  1303   moreover have "K \<inter> H = H" using K_def assms subgroup.subset by blast
  1304   ultimately show "normal (N\<inter>H) (G\<lparr>carrier := H\<rparr>)" by auto
  1305 qed
  1306 
  1307 
  1308 end