src/HOL/Algebra/AbelCoset.thy
 author wenzelm Mon Nov 07 16:39:14 2011 +0100 (2011-11-07) changeset 45388 121b2db078b1 parent 45006 11a542f50fc3 child 55926 3ef14caf5637 permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Algebra/AbelCoset.thy

     2     Author:     Stephan Hohe, TU Muenchen

     3 *)

     4

     5 theory AbelCoset

     6 imports Coset Ring

     7 begin

     8

     9 subsection {* More Lifting from Groups to Abelian Groups *}

    10

    11 subsubsection {* Definitions *}

    12

    13 text {* Hiding @{text "<+>"} from @{theory Sum_Type} until I come

    14   up with better syntax here *}

    15

    16 no_notation Sum_Type.Plus (infixr "<+>" 65)

    17

    18 definition

    19   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)

    20   where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

    21

    22 definition

    23   a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)

    24   where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

    25

    26 definition

    27   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _"  80)

    28   where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"

    29

    30 definition

    31   set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)

    32   where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

    33

    34 definition

    35   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _"  80)

    36   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"

    37

    38 definition

    39   a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index>")

    40   where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"

    41

    42 definition

    43   A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)

    44     --{*Actually defined for groups rather than monoids*}

    45   where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"

    46

    47 definition

    48   a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"

    49     --{*the kernel of a homomorphism (additive)*}

    50   where "a_kernel G H h =

    51     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     by default (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 have Hcarr: "H \<subseteq> carrier G"

   259       unfolding subgroup_def by simp

   260     from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"

   261       using m_comm [simplified] 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

   520 subsubsection{*The First Isomorphism Theorem*}

   521

   522 text{*The quotient by the kernel of a homomorphism is isomorphic to the

   523   range of that homomorphism.*}

   524

   525 lemmas a_kernel_defs =

   526   a_kernel_def kernel_def

   527

   528 lemma a_kernel_def':

   529   "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"

   530 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])

   531

   532

   533 subsubsection {* Homomorphisms *}

   534

   535 lemma abelian_group_homI:

   536   assumes "abelian_group G"

   537   assumes "abelian_group H"

   538   assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)

   539                                   (| carrier = carrier H, mult = add H, one = zero H |) h"

   540   shows "abelian_group_hom G H h"

   541 proof -

   542   interpret G: abelian_group G by fact

   543   interpret H: abelian_group H by fact

   544   show ?thesis

   545     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_the_elem_mem:

   610   assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"

   611   shows "the_elem (hX) \<in> carrier H"

   612 by (rule group_hom.FactGroup_the_elem_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. the_elem (hX)) \<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. the_elem (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. the_elem (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. the_elem (hX)) \<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

   644 subsubsection {* Cosets *}

   645

   646 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}

   647

   648 lemma (in additive_subgroup) a_Hcarr [simp]:

   649   assumes hH: "h \<in> H"

   650   shows "h \<in> carrier G"

   651 by (rule subgroup.mem_carrier [OF a_subgroup,

   652     simplified monoid_record_simps]) (rule hH)

   653

   654

   655 lemma (in abelian_subgroup) a_elemrcos_carrier:

   656   assumes acarr: "a \<in> carrier G"

   657       and a': "a' \<in> H +> a"

   658   shows "a' \<in> carrier G"

   659 by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,

   660     folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')

   661

   662 lemma (in abelian_subgroup) a_rcos_const:

   663   assumes hH: "h \<in> H"

   664   shows "H +> h = H"

   665 by (rule subgroup.rcos_const [OF a_subgroup a_group,

   666     folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)

   667

   668 lemma (in abelian_subgroup) a_rcos_module_imp:

   669   assumes xcarr: "x \<in> carrier G"

   670       and x'cos: "x' \<in> H +> x"

   671   shows "(x' \<oplus> \<ominus>x) \<in> H"

   672 by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,

   673     folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)

   674

   675 lemma (in abelian_subgroup) a_rcos_module_rev:

   676   assumes "x \<in> carrier G" "x' \<in> carrier G"

   677       and "(x' \<oplus> \<ominus>x) \<in> H"

   678   shows "x' \<in> H +> x"

   679 using assms

   680 by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,

   681     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])

   682

   683 lemma (in abelian_subgroup) a_rcos_module:

   684   assumes "x \<in> carrier G" "x' \<in> carrier G"

   685   shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"

   686 using assms

   687 by (rule subgroup.rcos_module [OF a_subgroup a_group,

   688     folded a_r_coset_def a_inv_def, simplified monoid_record_simps])

   689

   690 --"variant"

   691 lemma (in abelian_subgroup) a_rcos_module_minus:

   692   assumes "ring G"

   693   assumes carr: "x \<in> carrier G" "x' \<in> carrier G"

   694   shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"

   695 proof -

   696   interpret G: ring G by fact

   697   from carr

   698   have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)

   699   with carr

   700   show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"

   701     by (simp add: minus_eq)

   702 qed

   703

   704 lemma (in abelian_subgroup) a_repr_independence':

   705   assumes y: "y \<in> H +> x"

   706       and xcarr: "x \<in> carrier G"

   707   shows "H +> x = H +> y"

   708   apply (rule a_repr_independence)

   709     apply (rule y)

   710    apply (rule xcarr)

   711   apply (rule a_subgroup)

   712   done

   713

   714 lemma (in abelian_subgroup) a_repr_independenceD:

   715   assumes ycarr: "y \<in> carrier G"

   716       and repr:  "H +> x = H +> y"

   717   shows "y \<in> H +> x"

   718 by (rule group.repr_independenceD [OF a_group a_subgroup,

   719     folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)

   720

   721

   722 lemma (in abelian_subgroup) a_rcosets_carrier:

   723   "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"

   724 by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,

   725     folded A_RCOSETS_def, simplified monoid_record_simps])

   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