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