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