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