src/HOL/Algebra/AbelCoset.thy
 author haftmann Wed Feb 17 21:51:56 2016 +0100 (2016-02-17) changeset 62343 24106dc44def parent 61565 352c73a689da child 63167 0909deb8059b permissions -rw-r--r--
prefer abbreviations for compound operators INFIMUM and SUPREMUM
 wenzelm@35849  1 (* Title: HOL/Algebra/AbelCoset.thy  wenzelm@35849  2  Author: Stephan Hohe, TU Muenchen  ballarin@20318  3 *)  ballarin@20318  4 ballarin@20318  5 theory AbelCoset  ballarin@20318  6 imports Coset Ring  ballarin@20318  7 begin  ballarin@20318  8 wenzelm@61382  9 subsection \More Lifting from Groups to Abelian Groups\  ballarin@20318  10 wenzelm@61382  11 subsubsection \Definitions\  ballarin@20318  12 wenzelm@61382  13 text \Hiding @{text "<+>"} from @{theory Sum_Type} until I come  wenzelm@61382  14  up with better syntax here\  ballarin@20318  15 nipkow@40271  16 no_notation Sum_Type.Plus (infixr "<+>" 65)  ballarin@20318  17 wenzelm@35847  18 definition  ballarin@20318  19  a_r_coset :: "[_, 'a set, 'a] \ 'a set" (infixl "+>\" 60)  wenzelm@35848  20  where "a_r_coset G = r_coset \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  21 wenzelm@35847  22 definition  ballarin@20318  23  a_l_coset :: "[_, 'a, 'a set] \ 'a set" (infixl "<+\" 60)  wenzelm@35848  24  where "a_l_coset G = l_coset \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  25 wenzelm@35847  26 definition  ballarin@20318  27  A_RCOSETS :: "[_, 'a set] \ ('a set)set" ("a'_rcosets\ _" [81] 80)  wenzelm@35848  28  where "A_RCOSETS G H = RCOSETS \carrier = carrier G, mult = add G, one = zero G\ H"  ballarin@20318  29 wenzelm@35847  30 definition  ballarin@20318  31  set_add :: "[_, 'a set ,'a set] \ 'a set" (infixl "<+>\" 60)  wenzelm@35848  32  where "set_add G = set_mult \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  33 wenzelm@35847  34 definition  ballarin@20318  35  A_SET_INV :: "[_,'a set] \ 'a set" ("a'_set'_inv\ _" [81] 80)  wenzelm@35848  36  where "A_SET_INV G H = SET_INV \carrier = carrier G, mult = add G, one = zero G\ H"  ballarin@20318  37 wenzelm@35847  38 definition  wenzelm@45006  39  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \ ('a*'a)set" ("racong\")  wenzelm@35848  40  where "a_r_congruent G = r_congruent \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  41 wenzelm@35848  42 definition  wenzelm@35848  43  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \ ('a set) monoid" (infixl "A'_Mod" 65)  wenzelm@61382  44  --\Actually defined for groups rather than monoids\  wenzelm@35848  45  where "A_FactGroup G H = FactGroup \carrier = carrier G, mult = add G, one = zero G\ H"  ballarin@20318  46 wenzelm@35848  47 definition  wenzelm@35848  48  a_kernel :: "('a, 'm) ring_scheme \ ('b, 'n) ring_scheme \ ('a \ 'b) \ 'a set"  wenzelm@61382  49  --\the kernel of a homomorphism (additive)\  wenzelm@35848  50  where "a_kernel G H h =  wenzelm@35848  51  kernel \carrier = carrier G, mult = add G, one = zero G\  wenzelm@35848  52  \carrier = carrier H, mult = add H, one = zero H\ h"  ballarin@20318  53 ballarin@61565  54 locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H  ballarin@29237  55  for G (structure) and H (structure) +  ballarin@29237  56  fixes h  wenzelm@55926  57  assumes a_group_hom: "group_hom \carrier = carrier G, mult = add G, one = zero G\  wenzelm@55926  58  \carrier = carrier H, mult = add H, one = zero H\ h"  ballarin@20318  59 ballarin@20318  60 lemmas a_r_coset_defs =  ballarin@20318  61  a_r_coset_def r_coset_def  ballarin@20318  62 ballarin@20318  63 lemma a_r_coset_def':  ballarin@27611  64  fixes G (structure)  ballarin@20318  65  shows "H +> a \ \h\H. {h \ a}"  ballarin@20318  66 unfolding a_r_coset_defs  ballarin@20318  67 by simp  ballarin@20318  68 ballarin@20318  69 lemmas a_l_coset_defs =  ballarin@20318  70  a_l_coset_def l_coset_def  ballarin@20318  71 ballarin@20318  72 lemma a_l_coset_def':  ballarin@27611  73  fixes G (structure)  ballarin@20318  74  shows "a <+ H \ \h\H. {a \ h}"  ballarin@20318  75 unfolding a_l_coset_defs  ballarin@20318  76 by simp  ballarin@20318  77 ballarin@20318  78 lemmas A_RCOSETS_defs =  ballarin@20318  79  A_RCOSETS_def RCOSETS_def  ballarin@20318  80 ballarin@20318  81 lemma A_RCOSETS_def':  ballarin@27611  82  fixes G (structure)  ballarin@20318  83  shows "a_rcosets H \ \a\carrier G. {H +> a}"  ballarin@20318  84 unfolding A_RCOSETS_defs  ballarin@20318  85 by (fold a_r_coset_def, simp)  ballarin@20318  86 ballarin@20318  87 lemmas set_add_defs =  ballarin@20318  88  set_add_def set_mult_def  ballarin@20318  89 ballarin@20318  90 lemma set_add_def':  ballarin@27611  91  fixes G (structure)  ballarin@20318  92  shows "H <+> K \ \h\H. \k\K. {h \ k}"  ballarin@20318  93 unfolding set_add_defs  ballarin@20318  94 by simp  ballarin@20318  95 ballarin@20318  96 lemmas A_SET_INV_defs =  ballarin@20318  97  A_SET_INV_def SET_INV_def  ballarin@20318  98 ballarin@20318  99 lemma A_SET_INV_def':  ballarin@27611  100  fixes G (structure)  ballarin@20318  101  shows "a_set_inv H \ \h\H. {\ h}"  ballarin@20318  102 unfolding A_SET_INV_defs  ballarin@20318  103 by (fold a_inv_def)  ballarin@20318  104 ballarin@20318  105 wenzelm@61382  106 subsubsection \Cosets\  ballarin@20318  107 ballarin@20318  108 lemma (in abelian_group) a_coset_add_assoc:  ballarin@20318  109  "[| M \ carrier G; g \ carrier G; h \ carrier G |]  ballarin@20318  110  ==> (M +> g) +> h = M +> (g \ h)"  ballarin@20318  111 by (rule group.coset_mult_assoc [OF a_group,  ballarin@20318  112  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  113 ballarin@20318  114 lemma (in abelian_group) a_coset_add_zero [simp]:  ballarin@20318  115  "M \ carrier G ==> M +> \ = M"  ballarin@20318  116 by (rule group.coset_mult_one [OF a_group,  ballarin@20318  117  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  118 ballarin@20318  119 lemma (in abelian_group) a_coset_add_inv1:  ballarin@20318  120  "[| M +> (x \ (\ y)) = M; x \ carrier G ; y \ carrier G;  ballarin@20318  121  M \ carrier G |] ==> M +> x = M +> y"  ballarin@20318  122 by (rule group.coset_mult_inv1 [OF a_group,  ballarin@20318  123  folded a_r_coset_def a_inv_def, simplified monoid_record_simps])  ballarin@20318  124 ballarin@20318  125 lemma (in abelian_group) a_coset_add_inv2:  ballarin@20318  126  "[| M +> x = M +> y; x \ carrier G; y \ carrier G; M \ carrier G |]  ballarin@20318  127  ==> M +> (x \ (\ y)) = M"  ballarin@20318  128 by (rule group.coset_mult_inv2 [OF a_group,  ballarin@20318  129  folded a_r_coset_def a_inv_def, simplified monoid_record_simps])  ballarin@20318  130 ballarin@20318  131 lemma (in abelian_group) a_coset_join1:  wenzelm@55926  132  "[| H +> x = H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H"  ballarin@20318  133 by (rule group.coset_join1 [OF a_group,  ballarin@20318  134  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  135 ballarin@20318  136 lemma (in abelian_group) a_solve_equation:  wenzelm@55926  137  "\subgroup H \carrier = carrier G, mult = add G, one = zero G\; x \ H; y \ H\ \ \h\H. y = h \ x"  ballarin@20318  138 by (rule group.solve_equation [OF a_group,  ballarin@20318  139  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  140 ballarin@20318  141 lemma (in abelian_group) a_repr_independence:  ballarin@20318  142  "\y \ H +> x; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ \ H +> x = H +> y"  ballarin@20318  143 by (rule group.repr_independence [OF a_group,  ballarin@20318  144  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  145 ballarin@20318  146 lemma (in abelian_group) a_coset_join2:  ballarin@20318  147  "\x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\; x\H\ \ H +> x = H"  ballarin@20318  148 by (rule group.coset_join2 [OF a_group,  ballarin@20318  149  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  150 ballarin@20318  151 lemma (in abelian_monoid) a_r_coset_subset_G:  ballarin@20318  152  "[| H \ carrier G; x \ carrier G |] ==> H +> x \ carrier G"  ballarin@20318  153 by (rule monoid.r_coset_subset_G [OF a_monoid,  ballarin@20318  154  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  155 ballarin@20318  156 lemma (in abelian_group) a_rcosI:  ballarin@20318  157  "[| h \ H; H \ carrier G; x \ carrier G|] ==> h \ x \ H +> x"  ballarin@20318  158 by (rule group.rcosI [OF a_group,  ballarin@20318  159  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  160 ballarin@20318  161 lemma (in abelian_group) a_rcosetsI:  ballarin@20318  162  "\H \ carrier G; x \ carrier G\ \ H +> x \ a_rcosets H"  ballarin@20318  163 by (rule group.rcosetsI [OF a_group,  ballarin@20318  164  folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  165 wenzelm@61382  166 text\Really needed?\  ballarin@20318  167 lemma (in abelian_group) a_transpose_inv:  ballarin@20318  168  "[| x \ y = z; x \ carrier G; y \ carrier G; z \ carrier G |]  ballarin@20318  169  ==> (\ x) \ z = y"  ballarin@20318  170 by (rule group.transpose_inv [OF a_group,  ballarin@20318  171  folded a_r_coset_def a_inv_def, simplified monoid_record_simps])  ballarin@20318  172 ballarin@20318  173 (*  ballarin@20318  174 --"duplicate"  ballarin@20318  175 lemma (in abelian_group) a_rcos_self:  ballarin@20318  176  "[| x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> x \ H +> x"  ballarin@20318  177 by (rule group.rcos_self [OF a_group,  ballarin@20318  178  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  179 *)  ballarin@20318  180 ballarin@20318  181 wenzelm@61382  182 subsubsection \Subgroups\  ballarin@20318  183 ballarin@29237  184 locale additive_subgroup =  ballarin@29237  185  fixes H and G (structure)  ballarin@20318  186  assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  187 ballarin@20318  188 lemma (in additive_subgroup) is_additive_subgroup:  ballarin@20318  189  shows "additive_subgroup H G"  wenzelm@26203  190 by (rule additive_subgroup_axioms)  ballarin@20318  191 ballarin@20318  192 lemma additive_subgroupI:  ballarin@27611  193  fixes G (structure)  ballarin@20318  194  assumes a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  195  shows "additive_subgroup H G"  wenzelm@23350  196 by (rule additive_subgroup.intro) (rule a_subgroup)  ballarin@20318  197 ballarin@20318  198 lemma (in additive_subgroup) a_subset:  ballarin@20318  199  "H \ carrier G"  ballarin@20318  200 by (rule subgroup.subset[OF a_subgroup,  ballarin@20318  201  simplified monoid_record_simps])  ballarin@20318  202 ballarin@20318  203 lemma (in additive_subgroup) a_closed [intro, simp]:  ballarin@20318  204  "\x \ H; y \ H\ \ x \ y \ H"  ballarin@20318  205 by (rule subgroup.m_closed[OF a_subgroup,  ballarin@20318  206  simplified monoid_record_simps])  ballarin@20318  207 ballarin@20318  208 lemma (in additive_subgroup) zero_closed [simp]:  ballarin@20318  209  "\ \ H"  ballarin@20318  210 by (rule subgroup.one_closed[OF a_subgroup,  ballarin@20318  211  simplified monoid_record_simps])  ballarin@20318  212 ballarin@20318  213 lemma (in additive_subgroup) a_inv_closed [intro,simp]:  ballarin@20318  214  "x \ H \ \ x \ H"  ballarin@20318  215 by (rule subgroup.m_inv_closed[OF a_subgroup,  ballarin@20318  216  folded a_inv_def, simplified monoid_record_simps])  ballarin@20318  217 ballarin@20318  218 wenzelm@61382  219 subsubsection \Additive subgroups are normal\  ballarin@20318  220 wenzelm@61382  221 text \Every subgroup of an @{text "abelian_group"} is normal\  ballarin@20318  222 ballarin@29237  223 locale abelian_subgroup = additive_subgroup + abelian_group G +  ballarin@20318  224  assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  225 ballarin@20318  226 lemma (in abelian_subgroup) is_abelian_subgroup:  ballarin@20318  227  shows "abelian_subgroup H G"  wenzelm@26203  228 by (rule abelian_subgroup_axioms)  ballarin@20318  229 ballarin@20318  230 lemma abelian_subgroupI:  ballarin@20318  231  assumes a_normal: "normal H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  232  and a_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \\<^bsub>G\<^esub> y = y \\<^bsub>G\<^esub> x"  ballarin@20318  233  shows "abelian_subgroup H G"  ballarin@20318  234 proof -  ballarin@29237  235  interpret normal "H" "\carrier = carrier G, mult = add G, one = zero G\"  wenzelm@44655  236  by (rule a_normal)  ballarin@20318  237 ballarin@20318  238  show "abelian_subgroup H G"  wenzelm@61169  239  by standard (simp add: a_comm)  ballarin@20318  240 qed  ballarin@20318  241 ballarin@20318  242 lemma abelian_subgroupI2:  ballarin@27611  243  fixes G (structure)  ballarin@20318  244  assumes a_comm_group: "comm_group \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  245  and a_subgroup: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  246  shows "abelian_subgroup H G"  ballarin@20318  247 proof -  ballarin@29237  248  interpret comm_group "\carrier = carrier G, mult = add G, one = zero G\"  wenzelm@45388  249  by (rule a_comm_group)  ballarin@29237  250  interpret subgroup "H" "\carrier = carrier G, mult = add G, one = zero G\"  wenzelm@45388  251  by (rule a_subgroup)  ballarin@20318  252 ballarin@20318  253  show "abelian_subgroup H G"  wenzelm@45388  254  apply unfold_locales  ballarin@20318  255  proof (simp add: r_coset_def l_coset_def, clarsimp)  ballarin@20318  256  fix x  ballarin@20318  257  assume xcarr: "x \ carrier G"  wenzelm@45388  258  from a_subgroup have Hcarr: "H \ carrier G"  wenzelm@45388  259  unfolding subgroup_def by simp  wenzelm@45388  260  from xcarr Hcarr show "(\h\H. {h \\<^bsub>G\<^esub> x}) = (\h\H. {x \\<^bsub>G\<^esub> h})"  haftmann@62343  261  using m_comm [simplified] by fastforce  ballarin@20318  262  qed  ballarin@20318  263 qed  ballarin@20318  264 ballarin@20318  265 lemma abelian_subgroupI3:  ballarin@27611  266  fixes G (structure)  ballarin@20318  267  assumes asg: "additive_subgroup H G"  ballarin@20318  268  and ag: "abelian_group G"  ballarin@20318  269  shows "abelian_subgroup H G"  ballarin@20318  270 apply (rule abelian_subgroupI2)  ballarin@20318  271  apply (rule abelian_group.a_comm_group[OF ag])  ballarin@20318  272 apply (rule additive_subgroup.a_subgroup[OF asg])  ballarin@20318  273 done  ballarin@20318  274 ballarin@20318  275 lemma (in abelian_subgroup) a_coset_eq:  ballarin@20318  276  "(\x \ carrier G. H +> x = x <+ H)"  ballarin@20318  277 by (rule normal.coset_eq[OF a_normal,  ballarin@20318  278  folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  279 ballarin@20318  280 lemma (in abelian_subgroup) a_inv_op_closed1:  ballarin@20318  281  shows "\x \ carrier G; h \ H\ \ (\ x) \ h \ x \ H"  ballarin@20318  282 by (rule normal.inv_op_closed1 [OF a_normal,  ballarin@20318  283  folded a_inv_def, simplified monoid_record_simps])  ballarin@20318  284 ballarin@20318  285 lemma (in abelian_subgroup) a_inv_op_closed2:  ballarin@20318  286  shows "\x \ carrier G; h \ H\ \ x \ h \ (\ x) \ H"  ballarin@20318  287 by (rule normal.inv_op_closed2 [OF a_normal,  ballarin@20318  288  folded a_inv_def, simplified monoid_record_simps])  ballarin@20318  289 wenzelm@61382  290 text\Alternative characterization of normal subgroups\  ballarin@20318  291 lemma (in abelian_group) a_normal_inv_iff:  ballarin@20318  292  "(N \ \carrier = carrier G, mult = add G, one = zero G\) =  ballarin@20318  293  (subgroup N \carrier = carrier G, mult = add G, one = zero G\ & (\x \ carrier G. \h \ N. x \ h \ (\ x) \ N))"  ballarin@20318  294  (is "_ = ?rhs")  ballarin@20318  295 by (rule group.normal_inv_iff [OF a_group,  ballarin@20318  296  folded a_inv_def, simplified monoid_record_simps])  ballarin@20318  297 ballarin@20318  298 lemma (in abelian_group) a_lcos_m_assoc:  ballarin@20318  299  "[| M \ carrier G; g \ carrier G; h \ carrier G |]  ballarin@20318  300  ==> g <+ (h <+ M) = (g \ h) <+ M"  ballarin@20318  301 by (rule group.lcos_m_assoc [OF a_group,  ballarin@20318  302  folded a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  303 ballarin@20318  304 lemma (in abelian_group) a_lcos_mult_one:  ballarin@20318  305  "M \ carrier G ==> \ <+ M = M"  ballarin@20318  306 by (rule group.lcos_mult_one [OF a_group,  ballarin@20318  307  folded a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  308 ballarin@20318  309 ballarin@20318  310 lemma (in abelian_group) a_l_coset_subset_G:  ballarin@20318  311  "[| H \ carrier G; x \ carrier G |] ==> x <+ H \ carrier G"  ballarin@20318  312 by (rule group.l_coset_subset_G [OF a_group,  ballarin@20318  313  folded a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  314 ballarin@20318  315 ballarin@20318  316 lemma (in abelian_group) a_l_coset_swap:  ballarin@20318  317  "\y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\\ \ x \ y <+ H"  ballarin@20318  318 by (rule group.l_coset_swap [OF a_group,  ballarin@20318  319  folded a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  320 ballarin@20318  321 lemma (in abelian_group) a_l_coset_carrier:  ballarin@20318  322  "[| y \ x <+ H; x \ carrier G; subgroup H \carrier = carrier G, mult = add G, one = zero G\ |] ==> y \ carrier G"  ballarin@20318  323 by (rule group.l_coset_carrier [OF a_group,  ballarin@20318  324  folded a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  325 ballarin@20318  326 lemma (in abelian_group) a_l_repr_imp_subset:  ballarin@20318  327  assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  328  shows "y <+ H \ x <+ H"  wenzelm@23350  329 apply (rule group.l_repr_imp_subset [OF a_group,  ballarin@20318  330  folded a_l_coset_def, simplified monoid_record_simps])  wenzelm@23350  331 apply (rule y)  wenzelm@23350  332 apply (rule x)  wenzelm@23350  333 apply (rule sb)  wenzelm@23350  334 done  ballarin@20318  335 ballarin@20318  336 lemma (in abelian_group) a_l_repr_independence:  ballarin@20318  337  assumes y: "y \ x <+ H" and x: "x \ carrier G" and sb: "subgroup H \carrier = carrier G, mult = add G, one = zero G\"  ballarin@20318  338  shows "x <+ H = y <+ H"  wenzelm@23350  339 apply (rule group.l_repr_independence [OF a_group,  ballarin@20318  340  folded a_l_coset_def, simplified monoid_record_simps])  wenzelm@23350  341 apply (rule y)  wenzelm@23350  342 apply (rule x)  wenzelm@23350  343 apply (rule sb)  wenzelm@23350  344 done  ballarin@20318  345 ballarin@20318  346 lemma (in abelian_group) setadd_subset_G:  ballarin@20318  347  "\H \ carrier G; K \ carrier G\ \ H <+> K \ carrier G"  ballarin@20318  348 by (rule group.setmult_subset_G [OF a_group,  ballarin@20318  349  folded set_add_def, simplified monoid_record_simps])  ballarin@20318  350 ballarin@20318  351 lemma (in abelian_group) subgroup_add_id: "subgroup H \carrier = carrier G, mult = add G, one = zero G\ \ H <+> H = H"  ballarin@20318  352 by (rule group.subgroup_mult_id [OF a_group,  ballarin@20318  353  folded set_add_def, simplified monoid_record_simps])  ballarin@20318  354 ballarin@20318  355 lemma (in abelian_subgroup) a_rcos_inv:  ballarin@20318  356  assumes x: "x \ carrier G"  ballarin@20318  357  shows "a_set_inv (H +> x) = H +> (\ x)"  ballarin@20318  358 by (rule normal.rcos_inv [OF a_normal,  wenzelm@23350  359  folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)  ballarin@20318  360 ballarin@20318  361 lemma (in abelian_group) a_setmult_rcos_assoc:  ballarin@20318  362  "\H \ carrier G; K \ carrier G; x \ carrier G\  ballarin@20318  363  \ H <+> (K +> x) = (H <+> K) +> x"  ballarin@20318  364 by (rule group.setmult_rcos_assoc [OF a_group,  ballarin@20318  365  folded set_add_def a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  366 ballarin@20318  367 lemma (in abelian_group) a_rcos_assoc_lcos:  ballarin@20318  368  "\H \ carrier G; K \ carrier G; x \ carrier G\  ballarin@20318  369  \ (H +> x) <+> K = H <+> (x <+ K)"  ballarin@20318  370 by (rule group.rcos_assoc_lcos [OF a_group,  ballarin@20318  371  folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  372 ballarin@20318  373 lemma (in abelian_subgroup) a_rcos_sum:  ballarin@20318  374  "\x \ carrier G; y \ carrier G\  ballarin@20318  375  \ (H +> x) <+> (H +> y) = H +> (x \ y)"  ballarin@20318  376 by (rule normal.rcos_sum [OF a_normal,  ballarin@20318  377  folded set_add_def a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  378 ballarin@20318  379 lemma (in abelian_subgroup) rcosets_add_eq:  ballarin@20318  380  "M \ a_rcosets H \ H <+> M = M"  wenzelm@61382  381  -- \generalizes @{text subgroup_mult_id}\  ballarin@20318  382 by (rule normal.rcosets_mult_eq [OF a_normal,  ballarin@20318  383  folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  384 ballarin@20318  385 wenzelm@61382  386 subsubsection \Congruence Relation\  ballarin@20318  387 ballarin@20318  388 lemma (in abelian_subgroup) a_equiv_rcong:  ballarin@20318  389  shows "equiv (carrier G) (racong H)"  ballarin@20318  390 by (rule subgroup.equiv_rcong [OF a_subgroup a_group,  ballarin@20318  391  folded a_r_congruent_def, simplified monoid_record_simps])  ballarin@20318  392 ballarin@20318  393 lemma (in abelian_subgroup) a_l_coset_eq_rcong:  ballarin@20318  394  assumes a: "a \ carrier G"  ballarin@20318  395  shows "a <+ H = racong H  {a}"  ballarin@20318  396 by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,  wenzelm@23350  397  folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)  ballarin@20318  398 ballarin@20318  399 lemma (in abelian_subgroup) a_rcos_equation:  ballarin@20318  400  shows  ballarin@20318  401  "\ha \ a = h \ b; a \ carrier G; b \ carrier G;  ballarin@20318  402  h \ H; ha \ H; hb \ H\  ballarin@20318  403  \ hb \ a \ (\h\H. {h \ b})"  ballarin@20318  404 by (rule group.rcos_equation [OF a_group a_subgroup,  ballarin@20318  405  folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])  ballarin@20318  406 ballarin@20318  407 lemma (in abelian_subgroup) a_rcos_disjoint:  ballarin@20318  408  shows "\a \ a_rcosets H; b \ a_rcosets H; a\b\ \ a \ b = {}"  ballarin@20318  409 by (rule group.rcos_disjoint [OF a_group a_subgroup,  ballarin@20318  410  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  411 ballarin@20318  412 lemma (in abelian_subgroup) a_rcos_self:  ballarin@20318  413  shows "x \ carrier G \ x \ H +> x"  wenzelm@26310  414 by (rule group.rcos_self [OF a_group _ a_subgroup,  ballarin@20318  415  folded a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  416 ballarin@20318  417 lemma (in abelian_subgroup) a_rcosets_part_G:  ballarin@20318  418  shows "\(a_rcosets H) = carrier G"  ballarin@20318  419 by (rule group.rcosets_part_G [OF a_group a_subgroup,  ballarin@20318  420  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  421 ballarin@20318  422 lemma (in abelian_subgroup) a_cosets_finite:  ballarin@20318  423  "\c \ a_rcosets H; H \ carrier G; finite (carrier G)\ \ finite c"  ballarin@20318  424 by (rule group.cosets_finite [OF a_group,  ballarin@20318  425  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  426 ballarin@20318  427 lemma (in abelian_group) a_card_cosets_equal:  ballarin@20318  428  "\c \ a_rcosets H; H \ carrier G; finite(carrier G)\  ballarin@20318  429  \ card c = card H"  ballarin@20318  430 by (rule group.card_cosets_equal [OF a_group,  ballarin@20318  431  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  432 ballarin@20318  433 lemma (in abelian_group) rcosets_subset_PowG:  ballarin@20318  434  "additive_subgroup H G \ a_rcosets H \ Pow(carrier G)"  ballarin@20318  435 by (rule group.rcosets_subset_PowG [OF a_group,  ballarin@20318  436  folded A_RCOSETS_def, simplified monoid_record_simps],  ballarin@20318  437  rule additive_subgroup.a_subgroup)  ballarin@20318  438 ballarin@20318  439 theorem (in abelian_group) a_lagrange:  ballarin@20318  440  "\finite(carrier G); additive_subgroup H G\  ballarin@20318  441  \ card(a_rcosets H) * card(H) = order(G)"  ballarin@20318  442 by (rule group.lagrange [OF a_group,  ballarin@20318  443  folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])  ballarin@20318  444  (fast intro!: additive_subgroup.a_subgroup)+  ballarin@20318  445 ballarin@20318  446 wenzelm@61382  447 subsubsection \Factorization\  ballarin@20318  448 ballarin@20318  449 lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def  ballarin@20318  450 ballarin@20318  451 lemma A_FactGroup_def':  ballarin@27611  452  fixes G (structure)  ballarin@20318  453  shows "G A_Mod H \ \carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\"  ballarin@20318  454 unfolding A_FactGroup_defs  ballarin@20318  455 by (fold A_RCOSETS_def set_add_def)  ballarin@20318  456 ballarin@20318  457 ballarin@20318  458 lemma (in abelian_subgroup) a_setmult_closed:  ballarin@20318  459  "\K1 \ a_rcosets H; K2 \ a_rcosets H\ \ K1 <+> K2 \ a_rcosets H"  ballarin@20318  460 by (rule normal.setmult_closed [OF a_normal,  ballarin@20318  461  folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])  ballarin@20318  462 ballarin@20318  463 lemma (in abelian_subgroup) a_setinv_closed:  ballarin@20318  464  "K \ a_rcosets H \ a_set_inv K \ a_rcosets H"  ballarin@20318  465 by (rule normal.setinv_closed [OF a_normal,  ballarin@20318  466  folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])  ballarin@20318  467 ballarin@20318  468 lemma (in abelian_subgroup) a_rcosets_assoc:  ballarin@20318  469  "\M1 \ a_rcosets H; M2 \ a_rcosets H; M3 \ a_rcosets H\  ballarin@20318  470  \ M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"  ballarin@20318  471 by (rule normal.rcosets_assoc [OF a_normal,  ballarin@20318  472  folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])  ballarin@20318  473 ballarin@20318  474 lemma (in abelian_subgroup) a_subgroup_in_rcosets:  ballarin@20318  475  "H \ a_rcosets H"  ballarin@20318  476 by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,  ballarin@20318  477  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  478 ballarin@20318  479 lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:  ballarin@20318  480  "M \ a_rcosets H \ a_set_inv M <+> M = H"  ballarin@20318  481 by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,  ballarin@20318  482  folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])  ballarin@20318  483 ballarin@20318  484 theorem (in abelian_subgroup) a_factorgroup_is_group:  ballarin@20318  485  "group (G A_Mod H)"  ballarin@20318  486 by (rule normal.factorgroup_is_group [OF a_normal,  ballarin@20318  487  folded A_FactGroup_def, simplified monoid_record_simps])  ballarin@20318  488 wenzelm@61382  489 text \Since the Factorization is based on an \emph{abelian} subgroup, is results in  wenzelm@61382  490  a commutative group\  ballarin@20318  491 theorem (in abelian_subgroup) a_factorgroup_is_comm_group:  ballarin@20318  492  "comm_group (G A_Mod H)"  ballarin@20318  493 apply (intro comm_group.intro comm_monoid.intro) prefer 3  ballarin@20318  494  apply (rule a_factorgroup_is_group)  ballarin@20318  495  apply (rule group.axioms[OF a_factorgroup_is_group])  ballarin@20318  496 apply (rule comm_monoid_axioms.intro)  ballarin@20318  497 apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)  ballarin@20318  498 apply (simp add: a_rcos_sum a_comm)  ballarin@20318  499 done  ballarin@20318  500 ballarin@20318  501 lemma add_A_FactGroup [simp]: "X \\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"  ballarin@20318  502 by (simp add: A_FactGroup_def set_add_def)  ballarin@20318  503 ballarin@20318  504 lemma (in abelian_subgroup) a_inv_FactGroup:  ballarin@20318  505  "X \ carrier (G A_Mod H) \ inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"  ballarin@20318  506 by (rule normal.inv_FactGroup [OF a_normal,  ballarin@20318  507  folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])  ballarin@20318  508 wenzelm@61382  509 text\The coset map is a homomorphism from @{term G} to the quotient group  wenzelm@61382  510  @{term "G Mod H"}\  ballarin@20318  511 lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:  ballarin@20318  512  "(\a. H +> a) \ hom \carrier = carrier G, mult = add G, one = zero G\ (G A_Mod H)"  ballarin@20318  513 by (rule normal.r_coset_hom_Mod [OF a_normal,  ballarin@20318  514  folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])  ballarin@20318  515 wenzelm@61382  516 text \The isomorphism theorems have been omitted from lifting, at  wenzelm@61382  517  least for now\  ballarin@20318  518 wenzelm@35849  519 wenzelm@61382  520 subsubsection\The First Isomorphism Theorem\  ballarin@20318  521 wenzelm@61382  522 text\The quotient by the kernel of a homomorphism is isomorphic to the  wenzelm@61382  523  range of that homomorphism.\  ballarin@20318  524 ballarin@20318  525 lemmas a_kernel_defs =  ballarin@20318  526  a_kernel_def kernel_def  ballarin@20318  527 ballarin@20318  528 lemma a_kernel_def':  wenzelm@35848  529  "a_kernel R S h = {x \ carrier R. h x = \\<^bsub>S\<^esub>}"  ballarin@20318  530 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])  ballarin@20318  531 ballarin@20318  532 wenzelm@61382  533 subsubsection \Homomorphisms\  ballarin@20318  534 ballarin@20318  535 lemma abelian_group_homI:  ballarin@27611  536  assumes "abelian_group G"  ballarin@27611  537  assumes "abelian_group H"  wenzelm@55926  538  assumes a_group_hom: "group_hom \carrier = carrier G, mult = add G, one = zero G\  wenzelm@55926  539  \carrier = carrier H, mult = add H, one = zero H\ h"  ballarin@20318  540  shows "abelian_group_hom G H h"  ballarin@27611  541 proof -  wenzelm@30729  542  interpret G: abelian_group G by fact  wenzelm@30729  543  interpret H: abelian_group H by fact  wenzelm@45388  544  show ?thesis  wenzelm@45388  545  apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)  wenzelm@45388  546  apply fact  wenzelm@45388  547  apply fact  ballarin@27611  548  apply (rule a_group_hom)  ballarin@27611  549  done  ballarin@27611  550 qed  ballarin@20318  551 ballarin@20318  552 lemma (in abelian_group_hom) is_abelian_group_hom:  ballarin@20318  553  "abelian_group_hom G H h"  haftmann@28823  554  ..  ballarin@20318  555 ballarin@20318  556 lemma (in abelian_group_hom) hom_add [simp]:  ballarin@20318  557  "[| x : carrier G; y : carrier G |]  ballarin@20318  558  ==> h (x \\<^bsub>G\<^esub> y) = h x \\<^bsub>H\<^esub> h y"  ballarin@20318  559 by (rule group_hom.hom_mult[OF a_group_hom,  ballarin@20318  560  simplified ring_record_simps])  ballarin@20318  561 ballarin@20318  562 lemma (in abelian_group_hom) hom_closed [simp]:  ballarin@20318  563  "x \ carrier G \ h x \ carrier H"  ballarin@20318  564 by (rule group_hom.hom_closed[OF a_group_hom,  ballarin@20318  565  simplified ring_record_simps])  ballarin@20318  566 ballarin@20318  567 lemma (in abelian_group_hom) zero_closed [simp]:  ballarin@20318  568  "h \ \ carrier H"  ballarin@20318  569 by (rule group_hom.one_closed[OF a_group_hom,  ballarin@20318  570  simplified ring_record_simps])  ballarin@20318  571 ballarin@20318  572 lemma (in abelian_group_hom) hom_zero [simp]:  ballarin@20318  573  "h \ = \\<^bsub>H\<^esub>"  ballarin@20318  574 by (rule group_hom.hom_one[OF a_group_hom,  ballarin@20318  575  simplified ring_record_simps])  ballarin@20318  576 ballarin@20318  577 lemma (in abelian_group_hom) a_inv_closed [simp]:  ballarin@20318  578  "x \ carrier G ==> h (\x) \ carrier H"  ballarin@20318  579 by (rule group_hom.inv_closed[OF a_group_hom,  ballarin@20318  580  folded a_inv_def, simplified ring_record_simps])  ballarin@20318  581 ballarin@20318  582 lemma (in abelian_group_hom) hom_a_inv [simp]:  ballarin@20318  583  "x \ carrier G ==> h (\x) = \\<^bsub>H\<^esub> (h x)"  ballarin@20318  584 by (rule group_hom.hom_inv[OF a_group_hom,  ballarin@20318  585  folded a_inv_def, simplified ring_record_simps])  ballarin@20318  586 ballarin@20318  587 lemma (in abelian_group_hom) additive_subgroup_a_kernel:  ballarin@20318  588  "additive_subgroup (a_kernel G H h) G"  ballarin@20318  589 apply (rule additive_subgroup.intro)  ballarin@20318  590 apply (rule group_hom.subgroup_kernel[OF a_group_hom,  ballarin@20318  591  folded a_kernel_def, simplified ring_record_simps])  ballarin@20318  592 done  ballarin@20318  593 wenzelm@61382  594 text\The kernel of a homomorphism is an abelian subgroup\  ballarin@20318  595 lemma (in abelian_group_hom) abelian_subgroup_a_kernel:  ballarin@20318  596  "abelian_subgroup (a_kernel G H h) G"  ballarin@20318  597 apply (rule abelian_subgroupI)  ballarin@20318  598 apply (rule group_hom.normal_kernel[OF a_group_hom,  ballarin@20318  599  folded a_kernel_def, simplified ring_record_simps])  ballarin@20318  600 apply (simp add: G.a_comm)  ballarin@20318  601 done  ballarin@20318  602 ballarin@20318  603 lemma (in abelian_group_hom) A_FactGroup_nonempty:  ballarin@20318  604  assumes X: "X \ carrier (G A_Mod a_kernel G H h)"  ballarin@20318  605  shows "X \ {}"  ballarin@20318  606 by (rule group_hom.FactGroup_nonempty[OF a_group_hom,  wenzelm@23350  607  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)  ballarin@20318  608 haftmann@39910  609 lemma (in abelian_group_hom) FactGroup_the_elem_mem:  ballarin@20318  610  assumes X: "X \ carrier (G A_Mod (a_kernel G H h))"  haftmann@39910  611  shows "the_elem (hX) \ carrier H"  haftmann@39910  612 by (rule group_hom.FactGroup_the_elem_mem[OF a_group_hom,  wenzelm@23350  613  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)  ballarin@20318  614 ballarin@20318  615 lemma (in abelian_group_hom) A_FactGroup_hom:  haftmann@39910  616  "(\X. the_elem (hX)) \ hom (G A_Mod (a_kernel G H h))  ballarin@20318  617  \carrier = carrier H, mult = add H, one = zero H\"  ballarin@20318  618 by (rule group_hom.FactGroup_hom[OF a_group_hom,  ballarin@20318  619  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])  ballarin@20318  620 ballarin@20318  621 lemma (in abelian_group_hom) A_FactGroup_inj_on:  haftmann@39910  622  "inj_on (\X. the_elem (h  X)) (carrier (G A_Mod a_kernel G H h))"  ballarin@20318  623 by (rule group_hom.FactGroup_inj_on[OF a_group_hom,  ballarin@20318  624  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])  ballarin@20318  625 wenzelm@61382  626 text\If the homomorphism @{term h} is onto @{term H}, then so is the  wenzelm@61382  627 homomorphism from the quotient group\  ballarin@20318  628 lemma (in abelian_group_hom) A_FactGroup_onto:  ballarin@20318  629  assumes h: "h  carrier G = carrier H"  haftmann@39910  630  shows "(\X. the_elem (h  X))  carrier (G A_Mod a_kernel G H h) = carrier H"  ballarin@20318  631 by (rule group_hom.FactGroup_onto[OF a_group_hom,  wenzelm@23350  632  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)  ballarin@20318  633 wenzelm@61382  634 text\If @{term h} is a homomorphism from @{term G} onto @{term H}, then the  wenzelm@61382  635  quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\  ballarin@20318  636 theorem (in abelian_group_hom) A_FactGroup_iso:  ballarin@20318  637  "h  carrier G = carrier H  haftmann@39910  638  \ (\X. the_elem (hX)) \ (G A_Mod (a_kernel G H h)) \  wenzelm@55926  639  \carrier = carrier H, mult = add H, one = zero H\"  ballarin@20318  640 by (rule group_hom.FactGroup_iso[OF a_group_hom,  ballarin@20318  641  folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])  ballarin@20318  642 wenzelm@35849  643 wenzelm@61382  644 subsubsection \Cosets\  ballarin@20318  645 wenzelm@61382  646 text \Not eveything from \texttt{CosetExt.thy} is lifted here.\  ballarin@20318  647 ballarin@20318  648 lemma (in additive_subgroup) a_Hcarr [simp]:  ballarin@20318  649  assumes hH: "h \ H"  ballarin@20318  650  shows "h \ carrier G"  ballarin@20318  651 by (rule subgroup.mem_carrier [OF a_subgroup,  wenzelm@23350  652  simplified monoid_record_simps]) (rule hH)  ballarin@20318  653 ballarin@20318  654 ballarin@20318  655 lemma (in abelian_subgroup) a_elemrcos_carrier:  ballarin@20318  656  assumes acarr: "a \ carrier G"  ballarin@20318  657  and a': "a' \ H +> a"  ballarin@20318  658  shows "a' \ carrier G"  ballarin@20318  659 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,  wenzelm@23350  660  folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')  ballarin@20318  661 ballarin@20318  662 lemma (in abelian_subgroup) a_rcos_const:  ballarin@20318  663  assumes hH: "h \ H"  ballarin@20318  664  shows "H +> h = H"  ballarin@20318  665 by (rule subgroup.rcos_const [OF a_subgroup a_group,  wenzelm@23350  666  folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)  ballarin@20318  667 ballarin@20318  668 lemma (in abelian_subgroup) a_rcos_module_imp:  ballarin@20318  669  assumes xcarr: "x \ carrier G"  ballarin@20318  670  and x'cos: "x' \ H +> x"  ballarin@20318  671  shows "(x' \ \x) \ H"  ballarin@20318  672 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,  wenzelm@23350  673  folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)  ballarin@20318  674 ballarin@20318  675 lemma (in abelian_subgroup) a_rcos_module_rev:  wenzelm@23350  676  assumes "x \ carrier G" "x' \ carrier G"  wenzelm@23350  677  and "(x' \ \x) \ H"  ballarin@20318  678  shows "x' \ H +> x"  wenzelm@23350  679 using assms  ballarin@20318  680 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,  ballarin@20318  681  folded a_r_coset_def a_inv_def, simplified monoid_record_simps])  ballarin@20318  682 ballarin@20318  683 lemma (in abelian_subgroup) a_rcos_module:  wenzelm@23350  684  assumes "x \ carrier G" "x' \ carrier G"  ballarin@20318  685  shows "(x' \ H +> x) = (x' \ \x \ H)"  wenzelm@23350  686 using assms  ballarin@20318  687 by (rule subgroup.rcos_module [OF a_subgroup a_group,  ballarin@20318  688  folded a_r_coset_def a_inv_def, simplified monoid_record_simps])  ballarin@20318  689 ballarin@20318  690 --"variant"  ballarin@20318  691 lemma (in abelian_subgroup) a_rcos_module_minus:  ballarin@27611  692  assumes "ring G"  ballarin@20318  693  assumes carr: "x \ carrier G" "x' \ carrier G"  ballarin@20318  694  shows "(x' \ H +> x) = (x' \ x \ H)"  ballarin@20318  695 proof -  wenzelm@30729  696  interpret G: ring G by fact  ballarin@20318  697  from carr  wenzelm@23350  698  have "(x' \ H +> x) = (x' \ \x \ H)" by (rule a_rcos_module)  wenzelm@23350  699  with carr  wenzelm@23350  700  show "(x' \ H +> x) = (x' \ x \ H)"  wenzelm@23350  701  by (simp add: minus_eq)  ballarin@20318  702 qed  ballarin@20318  703 ballarin@20318  704 lemma (in abelian_subgroup) a_repr_independence':  wenzelm@23463  705  assumes y: "y \ H +> x"  wenzelm@23463  706  and xcarr: "x \ carrier G"  ballarin@20318  707  shows "H +> x = H +> y"  wenzelm@23463  708  apply (rule a_repr_independence)  wenzelm@23463  709  apply (rule y)  wenzelm@23463  710  apply (rule xcarr)  wenzelm@23463  711  apply (rule a_subgroup)  wenzelm@23463  712  done  ballarin@20318  713 ballarin@20318  714 lemma (in abelian_subgroup) a_repr_independenceD:  ballarin@20318  715  assumes ycarr: "y \ carrier G"  ballarin@20318  716  and repr: "H +> x = H +> y"  ballarin@20318  717  shows "y \ H +> x"  ballarin@20318  718 by (rule group.repr_independenceD [OF a_group a_subgroup,  wenzelm@23383  719  folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)  ballarin@20318  720 ballarin@20318  721 ballarin@20318  722 lemma (in abelian_subgroup) a_rcosets_carrier:  ballarin@20318  723  "X \ a_rcosets H \ X \ carrier G"  ballarin@20318  724 by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,  ballarin@20318  725  folded A_RCOSETS_def, simplified monoid_record_simps])  ballarin@20318  726 ballarin@20318  727 wenzelm@61382  728 subsubsection \Addition of Subgroups\  ballarin@20318  729 ballarin@20318  730 lemma (in abelian_monoid) set_add_closed:  ballarin@20318  731  assumes Acarr: "A \ carrier G"  ballarin@20318  732  and Bcarr: "B \ carrier G"  ballarin@20318  733  shows "A <+> B \ carrier G"  ballarin@20318  734 by (rule monoid.set_mult_closed [OF a_monoid,  wenzelm@23383  735  folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)  ballarin@20318  736 ballarin@20318  737 lemma (in abelian_group) add_additive_subgroups:  ballarin@20318  738  assumes subH: "additive_subgroup H G"  ballarin@20318  739  and subK: "additive_subgroup K G"  ballarin@20318  740  shows "additive_subgroup (H <+> K) G"  ballarin@20318  741 apply (rule additive_subgroup.intro)  ballarin@20318  742 apply (unfold set_add_def)  ballarin@20318  743 apply (intro comm_group.mult_subgroups)  ballarin@20318  744  apply (rule a_comm_group)  ballarin@20318  745  apply (rule additive_subgroup.a_subgroup[OF subH])  ballarin@20318  746 apply (rule additive_subgroup.a_subgroup[OF subK])  ballarin@20318  747 done  ballarin@20318  748 ballarin@20318  749 end