src/HOL/Algebra/AbelCoset.thy
changeset 20318 0e0ea63fe768
child 21502 7f3ea2b3bab6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Thu Aug 03 14:57:26 2006 +0200
     1.3 @@ -0,0 +1,734 @@
     1.4 +(*
     1.5 +  Title:     HOL/Algebra/AbelCoset.thy
     1.6 +  Id:        $Id$
     1.7 +  Author:    Stephan Hohe, TU Muenchen
     1.8 +*)
     1.9 +
    1.10 +theory AbelCoset
    1.11 +imports Coset Ring
    1.12 +begin
    1.13 +
    1.14 +
    1.15 +section {* More Lifting from Groups to Abelian Groups *}
    1.16 +
    1.17 +subsection {* Definitions *}
    1.18 +
    1.19 +text {* Hiding @{text "<+>"} from \texttt{Sum\_Type.thy} until I come
    1.20 +  up with better syntax here *}
    1.21 +
    1.22 +hide const Plus
    1.23 +
    1.24 +constdefs (structure G)
    1.25 +  a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
    1.26 +  "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.27 +
    1.28 +  a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
    1.29 +  "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.30 +
    1.31 +  A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
    1.32 +  "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.33 +
    1.34 +  set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
    1.35 +  "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.36 +
    1.37 +  A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
    1.38 +  "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.39 +
    1.40 +constdefs (structure G)
    1.41 +  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
    1.42 +                  ("racong\<index> _")
    1.43 +   "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
    1.44 +
    1.45 +constdefs
    1.46 +  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid"
    1.47 +     (infixl "A'_Mod" 65)
    1.48 +    --{*Actually defined for groups rather than monoids*}
    1.49 +  "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
    1.50 +
    1.51 +constdefs
    1.52 +  a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> 
    1.53 +             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 
    1.54 +    --{*the kernel of a homomorphism (additive)*}
    1.55 +  "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
    1.56 +                              \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
    1.57 +
    1.58 +locale abelian_group_hom = abelian_group G + abelian_group H + var h +
    1.59 +  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
    1.60 +                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
    1.61 +
    1.62 +lemmas a_r_coset_defs =
    1.63 +  a_r_coset_def r_coset_def
    1.64 +
    1.65 +lemma a_r_coset_def':
    1.66 +  includes struct G
    1.67 +  shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
    1.68 +unfolding a_r_coset_defs
    1.69 +by simp
    1.70 +
    1.71 +lemmas a_l_coset_defs =
    1.72 +  a_l_coset_def l_coset_def
    1.73 +
    1.74 +lemma a_l_coset_def':
    1.75 +  includes struct G
    1.76 +  shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
    1.77 +unfolding a_l_coset_defs
    1.78 +by simp
    1.79 +
    1.80 +lemmas A_RCOSETS_defs =
    1.81 +  A_RCOSETS_def RCOSETS_def
    1.82 +
    1.83 +lemma A_RCOSETS_def':
    1.84 +  includes struct G
    1.85 +  shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
    1.86 +unfolding A_RCOSETS_defs
    1.87 +by (fold a_r_coset_def, simp)
    1.88 +
    1.89 +lemmas set_add_defs =
    1.90 +  set_add_def set_mult_def
    1.91 +
    1.92 +lemma set_add_def':
    1.93 +  includes struct G
    1.94 +  shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
    1.95 +unfolding set_add_defs
    1.96 +by simp
    1.97 +
    1.98 +lemmas A_SET_INV_defs =
    1.99 +  A_SET_INV_def SET_INV_def
   1.100 +
   1.101 +lemma A_SET_INV_def':
   1.102 +  includes struct G
   1.103 +  shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
   1.104 +unfolding A_SET_INV_defs
   1.105 +by (fold a_inv_def)
   1.106 +
   1.107 +
   1.108 +subsection {* Cosets *}
   1.109 +
   1.110 +lemma (in abelian_group) a_coset_add_assoc:
   1.111 +     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
   1.112 +      ==> (M +> g) +> h = M +> (g \<oplus> h)"
   1.113 +by (rule group.coset_mult_assoc [OF a_group,
   1.114 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.115 +
   1.116 +lemma (in abelian_group) a_coset_add_zero [simp]:
   1.117 +  "M \<subseteq> carrier G ==> M +> \<zero> = M"
   1.118 +by (rule group.coset_mult_one [OF a_group,
   1.119 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.120 +
   1.121 +lemma (in abelian_group) a_coset_add_inv1:
   1.122 +     "[| M +> (x \<oplus> (\<ominus> y)) = M;  x \<in> carrier G ; y \<in> carrier G;
   1.123 +         M \<subseteq> carrier G |] ==> M +> x = M +> y"
   1.124 +by (rule group.coset_mult_inv1 [OF a_group,
   1.125 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.126 +
   1.127 +lemma (in abelian_group) a_coset_add_inv2:
   1.128 +     "[| M +> x = M +> y;  x \<in> carrier G;  y \<in> carrier G;  M \<subseteq> carrier G |]
   1.129 +      ==> M +> (x \<oplus> (\<ominus> y)) = M"
   1.130 +by (rule group.coset_mult_inv2 [OF a_group,
   1.131 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.132 +
   1.133 +lemma (in abelian_group) a_coset_join1:
   1.134 +     "[| H +> x = H;  x \<in> carrier G;  subgroup H (|carrier = carrier G, mult = add G, one = zero G|) |] ==> x \<in> H"
   1.135 +by (rule group.coset_join1 [OF a_group,
   1.136 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.137 +
   1.138 +lemma (in abelian_group) a_solve_equation:
   1.139 +    "\<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"
   1.140 +by (rule group.solve_equation [OF a_group,
   1.141 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.142 +
   1.143 +lemma (in abelian_group) a_repr_independence:
   1.144 +     "\<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"
   1.145 +by (rule group.repr_independence [OF a_group,
   1.146 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.147 +
   1.148 +lemma (in abelian_group) a_coset_join2:
   1.149 +     "\<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"
   1.150 +by (rule group.coset_join2 [OF a_group,
   1.151 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.152 +
   1.153 +lemma (in abelian_monoid) a_r_coset_subset_G:
   1.154 +     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> H +> x \<subseteq> carrier G"
   1.155 +by (rule monoid.r_coset_subset_G [OF a_monoid,
   1.156 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.157 +
   1.158 +lemma (in abelian_group) a_rcosI:
   1.159 +     "[| h \<in> H; H \<subseteq> carrier G; x \<in> carrier G|] ==> h \<oplus> x \<in> H +> x"
   1.160 +by (rule group.rcosI [OF a_group,
   1.161 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.162 +
   1.163 +lemma (in abelian_group) a_rcosetsI:
   1.164 +     "\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H +> x \<in> a_rcosets H"
   1.165 +by (rule group.rcosetsI [OF a_group,
   1.166 +    folded a_r_coset_def A_RCOSETS_def, simplified monoid_record_simps])
   1.167 +
   1.168 +text{*Really needed?*}
   1.169 +lemma (in abelian_group) a_transpose_inv:
   1.170 +     "[| x \<oplus> y = z;  x \<in> carrier G;  y \<in> carrier G;  z \<in> carrier G |]
   1.171 +      ==> (\<ominus> x) \<oplus> z = y"
   1.172 +by (rule group.transpose_inv [OF a_group,
   1.173 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.174 +
   1.175 +(*
   1.176 +--"duplicate"
   1.177 +lemma (in abelian_group) a_rcos_self:
   1.178 +     "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
   1.179 +by (rule group.rcos_self [OF a_group,
   1.180 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.181 +*)
   1.182 +
   1.183 +
   1.184 +subsection {* Subgroups *}
   1.185 +
   1.186 +locale additive_subgroup = var H + struct G +
   1.187 +  assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.188 +
   1.189 +lemma (in additive_subgroup) is_additive_subgroup:
   1.190 +  shows "additive_subgroup H G"
   1.191 +by -
   1.192 +
   1.193 +lemma additive_subgroupI:
   1.194 +  includes struct G
   1.195 +  assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.196 +  shows "additive_subgroup H G"
   1.197 +by (rule additive_subgroup.intro)
   1.198 +
   1.199 +lemma (in additive_subgroup) a_subset:
   1.200 +     "H \<subseteq> carrier G"
   1.201 +by (rule subgroup.subset[OF a_subgroup,
   1.202 +    simplified monoid_record_simps])
   1.203 +
   1.204 +lemma (in additive_subgroup) a_closed [intro, simp]:
   1.205 +     "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> y \<in> H"
   1.206 +by (rule subgroup.m_closed[OF a_subgroup,
   1.207 +    simplified monoid_record_simps])
   1.208 +
   1.209 +lemma (in additive_subgroup) zero_closed [simp]:
   1.210 +     "\<zero> \<in> H"
   1.211 +by (rule subgroup.one_closed[OF a_subgroup,
   1.212 +    simplified monoid_record_simps])
   1.213 +
   1.214 +lemma (in additive_subgroup) a_inv_closed [intro,simp]:
   1.215 +     "x \<in> H \<Longrightarrow> \<ominus> x \<in> H"
   1.216 +by (rule subgroup.m_inv_closed[OF a_subgroup,
   1.217 +    folded a_inv_def, simplified monoid_record_simps])
   1.218 +
   1.219 +
   1.220 +subsection {* Normal additive subgroups *}
   1.221 +
   1.222 +subsubsection {* Definition of @{text "abelian_subgroup"} *}
   1.223 +
   1.224 +text {* Every subgroup of an @{text "abelian_group"} is normal *}
   1.225 +
   1.226 +locale abelian_subgroup = additive_subgroup H G + abelian_group G +
   1.227 +  assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.228 +
   1.229 +lemma (in abelian_subgroup) is_abelian_subgroup:
   1.230 +  shows "abelian_subgroup H G"
   1.231 +by -
   1.232 +
   1.233 +lemma abelian_subgroupI:
   1.234 +  assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.235 +      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"
   1.236 +  shows "abelian_subgroup H G"
   1.237 +proof -
   1.238 +  interpret normal ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
   1.239 +  by (rule a_normal)
   1.240 +
   1.241 +  show "abelian_subgroup H G"
   1.242 +  by (unfold_locales, simp add: a_comm)
   1.243 +qed
   1.244 +
   1.245 +lemma abelian_subgroupI2:
   1.246 +  includes struct G
   1.247 +  assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.248 +      and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
   1.249 +  shows "abelian_subgroup H G"
   1.250 +proof -
   1.251 +  interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
   1.252 +  by (rule a_comm_group)
   1.253 +  interpret subgroup ["H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
   1.254 +  by (rule a_subgroup)
   1.255 +
   1.256 +  show "abelian_subgroup H G"
   1.257 +  apply unfold_locales
   1.258 +  proof (simp add: r_coset_def l_coset_def, clarsimp)
   1.259 +    fix x
   1.260 +    assume xcarr: "x \<in> carrier G"
   1.261 +    from a_subgroup
   1.262 +        have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
   1.263 +    from xcarr Hcarr
   1.264 +        show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
   1.265 +        using m_comm[simplified]
   1.266 +        by fast
   1.267 +  qed
   1.268 +qed
   1.269 +
   1.270 +lemma abelian_subgroupI3:
   1.271 +  includes struct G
   1.272 +  assumes asg: "additive_subgroup H G"
   1.273 +      and ag: "abelian_group G"
   1.274 +  shows "abelian_subgroup H G"
   1.275 +apply (rule abelian_subgroupI2)
   1.276 + apply (rule abelian_group.a_comm_group[OF ag])
   1.277 +apply (rule additive_subgroup.a_subgroup[OF asg])
   1.278 +done
   1.279 +
   1.280 +lemma (in abelian_subgroup) a_coset_eq:
   1.281 +     "(\<forall>x \<in> carrier G. H +> x = x <+ H)"
   1.282 +by (rule normal.coset_eq[OF a_normal,
   1.283 +    folded a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
   1.284 +
   1.285 +lemma (in abelian_subgroup) a_inv_op_closed1:
   1.286 +  shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (\<ominus> x) \<oplus> h \<oplus> x \<in> H"
   1.287 +by (rule normal.inv_op_closed1 [OF a_normal,
   1.288 +    folded a_inv_def, simplified monoid_record_simps])
   1.289 +
   1.290 +lemma (in abelian_subgroup) a_inv_op_closed2:
   1.291 +  shows "\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<oplus> h \<oplus> (\<ominus> x) \<in> H"
   1.292 +by (rule normal.inv_op_closed2 [OF a_normal,
   1.293 +    folded a_inv_def, simplified monoid_record_simps])
   1.294 +
   1.295 +text{*Alternative characterization of normal subgroups*}
   1.296 +lemma (in abelian_group) a_normal_inv_iff:
   1.297 +     "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) = 
   1.298 +      (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))"
   1.299 +      (is "_ = ?rhs")
   1.300 +by (rule group.normal_inv_iff [OF a_group,
   1.301 +    folded a_inv_def, simplified monoid_record_simps])
   1.302 +
   1.303 +lemma (in abelian_group) a_lcos_m_assoc:
   1.304 +     "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
   1.305 +      ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
   1.306 +by (rule group.lcos_m_assoc [OF a_group,
   1.307 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.308 +
   1.309 +lemma (in abelian_group) a_lcos_mult_one:
   1.310 +     "M \<subseteq> carrier G ==> \<zero> <+ M = M"
   1.311 +by (rule group.lcos_mult_one [OF a_group,
   1.312 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.313 +
   1.314 +
   1.315 +lemma (in abelian_group) a_l_coset_subset_G:
   1.316 +     "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
   1.317 +by (rule group.l_coset_subset_G [OF a_group,
   1.318 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.319 +
   1.320 +
   1.321 +lemma (in abelian_group) a_l_coset_swap:
   1.322 +     "\<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"
   1.323 +by (rule group.l_coset_swap [OF a_group,
   1.324 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.325 +
   1.326 +lemma (in abelian_group) a_l_coset_carrier:
   1.327 +     "[| 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"
   1.328 +by (rule group.l_coset_carrier [OF a_group,
   1.329 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.330 +
   1.331 +lemma (in abelian_group) a_l_repr_imp_subset:
   1.332 +  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>"
   1.333 +  shows "y <+ H \<subseteq> x <+ H"
   1.334 +by (rule group.l_repr_imp_subset [OF a_group,
   1.335 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.336 +
   1.337 +lemma (in abelian_group) a_l_repr_independence:
   1.338 +  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>"
   1.339 +  shows "x <+ H = y <+ H"
   1.340 +by (rule group.l_repr_independence [OF a_group,
   1.341 +    folded a_l_coset_def, simplified monoid_record_simps])
   1.342 +
   1.343 +lemma (in abelian_group) setadd_subset_G:
   1.344 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
   1.345 +by (rule group.setmult_subset_G [OF a_group,
   1.346 +    folded set_add_def, simplified monoid_record_simps])
   1.347 +
   1.348 +lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
   1.349 +by (rule group.subgroup_mult_id [OF a_group,
   1.350 +    folded set_add_def, simplified monoid_record_simps])
   1.351 +
   1.352 +lemma (in abelian_subgroup) a_rcos_inv:
   1.353 +  assumes x:     "x \<in> carrier G"
   1.354 +  shows "a_set_inv (H +> x) = H +> (\<ominus> x)" 
   1.355 +by (rule normal.rcos_inv [OF a_normal,
   1.356 +    folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps])
   1.357 +
   1.358 +lemma (in abelian_group) a_setmult_rcos_assoc:
   1.359 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   1.360 +      \<Longrightarrow> H <+> (K +> x) = (H <+> K) +> x"
   1.361 +by (rule group.setmult_rcos_assoc [OF a_group,
   1.362 +    folded set_add_def a_r_coset_def, simplified monoid_record_simps])
   1.363 +
   1.364 +lemma (in abelian_group) a_rcos_assoc_lcos:
   1.365 +     "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
   1.366 +      \<Longrightarrow> (H +> x) <+> K = H <+> (x <+ K)"
   1.367 +by (rule group.rcos_assoc_lcos [OF a_group,
   1.368 +     folded set_add_def a_r_coset_def a_l_coset_def, simplified monoid_record_simps])
   1.369 +
   1.370 +lemma (in abelian_subgroup) a_rcos_sum:
   1.371 +     "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk>
   1.372 +      \<Longrightarrow> (H +> x) <+> (H +> y) = H +> (x \<oplus> y)"
   1.373 +by (rule normal.rcos_sum [OF a_normal,
   1.374 +    folded set_add_def a_r_coset_def, simplified monoid_record_simps])
   1.375 +
   1.376 +lemma (in abelian_subgroup) rcosets_add_eq:
   1.377 +  "M \<in> a_rcosets H \<Longrightarrow> H <+> M = M"
   1.378 +  -- {* generalizes @{text subgroup_mult_id} *}
   1.379 +by (rule normal.rcosets_mult_eq [OF a_normal,
   1.380 +    folded set_add_def A_RCOSETS_def, simplified monoid_record_simps])
   1.381 +
   1.382 +
   1.383 +subsection {* Congruence Relation *}
   1.384 +
   1.385 +lemma (in abelian_subgroup) a_equiv_rcong:
   1.386 +   shows "equiv (carrier G) (racong H)"
   1.387 +by (rule subgroup.equiv_rcong [OF a_subgroup a_group,
   1.388 +    folded a_r_congruent_def, simplified monoid_record_simps])
   1.389 +
   1.390 +lemma (in abelian_subgroup) a_l_coset_eq_rcong:
   1.391 +  assumes a: "a \<in> carrier G"
   1.392 +  shows "a <+ H = racong H `` {a}"
   1.393 +by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
   1.394 +    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
   1.395 +
   1.396 +lemma (in abelian_subgroup) a_rcos_equation:
   1.397 +  shows
   1.398 +     "\<lbrakk>ha \<oplus> a = h \<oplus> b; a \<in> carrier G;  b \<in> carrier G;  
   1.399 +        h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
   1.400 +      \<Longrightarrow> hb \<oplus> a \<in> (\<Union>h\<in>H. {h \<oplus> b})"
   1.401 +by (rule group.rcos_equation [OF a_group a_subgroup,
   1.402 +    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
   1.403 +
   1.404 +lemma (in abelian_subgroup) a_rcos_disjoint:
   1.405 +  shows "\<lbrakk>a \<in> a_rcosets H; b \<in> a_rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
   1.406 +by (rule group.rcos_disjoint [OF a_group a_subgroup,
   1.407 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.408 +
   1.409 +lemma (in abelian_subgroup) a_rcos_self:
   1.410 +  shows "x \<in> carrier G \<Longrightarrow> x \<in> H +> x"
   1.411 +by (rule group.rcos_self [OF a_group a_subgroup,
   1.412 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.413 +
   1.414 +lemma (in abelian_subgroup) a_rcosets_part_G:
   1.415 +  shows "\<Union>(a_rcosets H) = carrier G"
   1.416 +by (rule group.rcosets_part_G [OF a_group a_subgroup,
   1.417 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.418 +
   1.419 +lemma (in abelian_subgroup) a_cosets_finite:
   1.420 +     "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G;  finite (carrier G)\<rbrakk> \<Longrightarrow> finite c"
   1.421 +by (rule group.cosets_finite [OF a_group,
   1.422 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.423 +
   1.424 +lemma (in abelian_group) a_card_cosets_equal:
   1.425 +     "\<lbrakk>c \<in> a_rcosets H;  H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
   1.426 +      \<Longrightarrow> card c = card H"
   1.427 +by (rule group.card_cosets_equal [OF a_group,
   1.428 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.429 +
   1.430 +lemma (in abelian_group) rcosets_subset_PowG:
   1.431 +     "additive_subgroup H G  \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
   1.432 +by (rule group.rcosets_subset_PowG [OF a_group,
   1.433 +    folded A_RCOSETS_def, simplified monoid_record_simps],
   1.434 +    rule additive_subgroup.a_subgroup)
   1.435 +
   1.436 +theorem (in abelian_group) a_lagrange:
   1.437 +     "\<lbrakk>finite(carrier G); additive_subgroup H G\<rbrakk>
   1.438 +      \<Longrightarrow> card(a_rcosets H) * card(H) = order(G)"
   1.439 +by (rule group.lagrange [OF a_group,
   1.440 +    folded A_RCOSETS_def, simplified monoid_record_simps order_def, folded order_def])
   1.441 +    (fast intro!: additive_subgroup.a_subgroup)+
   1.442 +
   1.443 +
   1.444 +subsection {* Factorization *}
   1.445 +
   1.446 +lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
   1.447 +
   1.448 +lemma A_FactGroup_def':
   1.449 +  includes struct G
   1.450 +  shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
   1.451 +unfolding A_FactGroup_defs
   1.452 +by (fold A_RCOSETS_def set_add_def)
   1.453 +
   1.454 +
   1.455 +lemma (in abelian_subgroup) a_setmult_closed:
   1.456 +     "\<lbrakk>K1 \<in> a_rcosets H; K2 \<in> a_rcosets H\<rbrakk> \<Longrightarrow> K1 <+> K2 \<in> a_rcosets H"
   1.457 +by (rule normal.setmult_closed [OF a_normal,
   1.458 +    folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
   1.459 +
   1.460 +lemma (in abelian_subgroup) a_setinv_closed:
   1.461 +     "K \<in> a_rcosets H \<Longrightarrow> a_set_inv K \<in> a_rcosets H"
   1.462 +by (rule normal.setinv_closed [OF a_normal,
   1.463 +    folded A_RCOSETS_def A_SET_INV_def, simplified monoid_record_simps])
   1.464 +
   1.465 +lemma (in abelian_subgroup) a_rcosets_assoc:
   1.466 +     "\<lbrakk>M1 \<in> a_rcosets H; M2 \<in> a_rcosets H; M3 \<in> a_rcosets H\<rbrakk>
   1.467 +      \<Longrightarrow> M1 <+> M2 <+> M3 = M1 <+> (M2 <+> M3)"
   1.468 +by (rule normal.rcosets_assoc [OF a_normal,
   1.469 +    folded A_RCOSETS_def set_add_def, simplified monoid_record_simps])
   1.470 +
   1.471 +lemma (in abelian_subgroup) a_subgroup_in_rcosets:
   1.472 +     "H \<in> a_rcosets H"
   1.473 +by (rule subgroup.subgroup_in_rcosets [OF a_subgroup a_group,
   1.474 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.475 +
   1.476 +lemma (in abelian_subgroup) a_rcosets_inv_mult_group_eq:
   1.477 +     "M \<in> a_rcosets H \<Longrightarrow> a_set_inv M <+> M = H"
   1.478 +by (rule normal.rcosets_inv_mult_group_eq [OF a_normal,
   1.479 +    folded A_RCOSETS_def A_SET_INV_def set_add_def, simplified monoid_record_simps])
   1.480 +
   1.481 +theorem (in abelian_subgroup) a_factorgroup_is_group:
   1.482 +  "group (G A_Mod H)"
   1.483 +by (rule normal.factorgroup_is_group [OF a_normal,
   1.484 +    folded A_FactGroup_def, simplified monoid_record_simps])
   1.485 +
   1.486 +text {* Since the Factorization is based on an \emph{abelian} subgroup, is results in 
   1.487 +        a commutative group *}
   1.488 +theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
   1.489 +  "comm_group (G A_Mod H)"
   1.490 +apply (intro comm_group.intro comm_monoid.intro) prefer 3
   1.491 +  apply (rule a_factorgroup_is_group)
   1.492 + apply (rule group.axioms[OF a_factorgroup_is_group])
   1.493 +apply (rule comm_monoid_axioms.intro)
   1.494 +apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
   1.495 +apply (simp add: a_rcos_sum a_comm)
   1.496 +done
   1.497 +
   1.498 +lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
   1.499 +by (simp add: A_FactGroup_def set_add_def)
   1.500 +
   1.501 +lemma (in abelian_subgroup) a_inv_FactGroup:
   1.502 +     "X \<in> carrier (G A_Mod H) \<Longrightarrow> inv\<^bsub>G A_Mod H\<^esub> X = a_set_inv X"
   1.503 +by (rule normal.inv_FactGroup [OF a_normal,
   1.504 +    folded A_FactGroup_def A_SET_INV_def, simplified monoid_record_simps])
   1.505 +
   1.506 +text{*The coset map is a homomorphism from @{term G} to the quotient group
   1.507 +  @{term "G Mod H"}*}
   1.508 +lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
   1.509 +  "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
   1.510 +by (rule normal.r_coset_hom_Mod [OF a_normal,
   1.511 +    folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
   1.512 +
   1.513 +text {* The isomorphism theorems have been omitted from lifting, at
   1.514 +  least for now *}
   1.515 +
   1.516 +subsection{*The First Isomorphism Theorem*}
   1.517 +
   1.518 +text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   1.519 +  range of that homomorphism.*}
   1.520 +
   1.521 +lemmas a_kernel_defs =
   1.522 +  a_kernel_def kernel_def
   1.523 +
   1.524 +lemma a_kernel_def':
   1.525 +  "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
   1.526 +by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
   1.527 +
   1.528 +
   1.529 +subsection {* Homomorphisms *}
   1.530 +
   1.531 +lemma abelian_group_homI:
   1.532 +  includes abelian_group G
   1.533 +  includes abelian_group H
   1.534 +  assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
   1.535 +                                  (| carrier = carrier H, mult = add H, one = zero H |) h"
   1.536 +  shows "abelian_group_hom G H h"
   1.537 +by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
   1.538 +
   1.539 +lemma (in abelian_group_hom) is_abelian_group_hom:
   1.540 +  "abelian_group_hom G H h"
   1.541 +by (unfold_locales)
   1.542 +
   1.543 +lemma (in abelian_group_hom) hom_add [simp]:
   1.544 +  "[| x : carrier G; y : carrier G |]
   1.545 +        ==> h (x \<oplus>\<^bsub>G\<^esub> y) = h x \<oplus>\<^bsub>H\<^esub> h y"
   1.546 +by (rule group_hom.hom_mult[OF a_group_hom,
   1.547 +    simplified ring_record_simps])
   1.548 +
   1.549 +lemma (in abelian_group_hom) hom_closed [simp]:
   1.550 +  "x \<in> carrier G \<Longrightarrow> h x \<in> carrier H"
   1.551 +by (rule group_hom.hom_closed[OF a_group_hom,
   1.552 +    simplified ring_record_simps])
   1.553 +
   1.554 +lemma (in abelian_group_hom) zero_closed [simp]:
   1.555 +  "h \<zero> \<in> carrier H"
   1.556 +by (rule group_hom.one_closed[OF a_group_hom,
   1.557 +    simplified ring_record_simps])
   1.558 +
   1.559 +lemma (in abelian_group_hom) hom_zero [simp]:
   1.560 +  "h \<zero> = \<zero>\<^bsub>H\<^esub>"
   1.561 +by (rule group_hom.hom_one[OF a_group_hom,
   1.562 +    simplified ring_record_simps])
   1.563 +
   1.564 +lemma (in abelian_group_hom) a_inv_closed [simp]:
   1.565 +  "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
   1.566 +by (rule group_hom.inv_closed[OF a_group_hom,
   1.567 +    folded a_inv_def, simplified ring_record_simps])
   1.568 +
   1.569 +lemma (in abelian_group_hom) hom_a_inv [simp]:
   1.570 +  "x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
   1.571 +by (rule group_hom.hom_inv[OF a_group_hom,
   1.572 +    folded a_inv_def, simplified ring_record_simps])
   1.573 +
   1.574 +lemma (in abelian_group_hom) additive_subgroup_a_kernel:
   1.575 +  "additive_subgroup (a_kernel G H h) G"
   1.576 +apply (rule additive_subgroup.intro)
   1.577 +apply (rule group_hom.subgroup_kernel[OF a_group_hom,
   1.578 +       folded a_kernel_def, simplified ring_record_simps])
   1.579 +done
   1.580 +
   1.581 +text{*The kernel of a homomorphism is an abelian subgroup*}
   1.582 +lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
   1.583 +  "abelian_subgroup (a_kernel G H h) G"
   1.584 +apply (rule abelian_subgroupI)
   1.585 +apply (rule group_hom.normal_kernel[OF a_group_hom,
   1.586 +       folded a_kernel_def, simplified ring_record_simps])
   1.587 +apply (simp add: G.a_comm)
   1.588 +done
   1.589 +
   1.590 +lemma (in abelian_group_hom) A_FactGroup_nonempty:
   1.591 +  assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
   1.592 +  shows "X \<noteq> {}"
   1.593 +by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
   1.594 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.595 +
   1.596 +lemma (in abelian_group_hom) FactGroup_contents_mem:
   1.597 +  assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
   1.598 +  shows "contents (h`X) \<in> carrier H"
   1.599 +by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
   1.600 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.601 +
   1.602 +lemma (in abelian_group_hom) A_FactGroup_hom:
   1.603 +     "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
   1.604 +          \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
   1.605 +by (rule group_hom.FactGroup_hom[OF a_group_hom,
   1.606 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.607 +
   1.608 +lemma (in abelian_group_hom) A_FactGroup_inj_on:
   1.609 +     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G A_Mod a_kernel G H h))"
   1.610 +by (rule group_hom.FactGroup_inj_on[OF a_group_hom,
   1.611 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.612 +
   1.613 +text{*If the homomorphism @{term h} is onto @{term H}, then so is the
   1.614 +homomorphism from the quotient group*}
   1.615 +lemma (in abelian_group_hom) A_FactGroup_onto:
   1.616 +  assumes h: "h ` carrier G = carrier H"
   1.617 +  shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
   1.618 +by (rule group_hom.FactGroup_onto[OF a_group_hom,
   1.619 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.620 +
   1.621 +text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
   1.622 + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
   1.623 +theorem (in abelian_group_hom) A_FactGroup_iso:
   1.624 +  "h ` carrier G = carrier H
   1.625 +   \<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
   1.626 +          (| carrier = carrier H, mult = add H, one = zero H |)"
   1.627 +by (rule group_hom.FactGroup_iso[OF a_group_hom,
   1.628 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
   1.629 +
   1.630 +section {* Lemmas Lifted from CosetExt.thy *}
   1.631 +
   1.632 +text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
   1.633 +
   1.634 +subsection {* General Lemmas from \texttt{AlgebraExt.thy} *}
   1.635 +
   1.636 +lemma (in additive_subgroup) a_Hcarr [simp]:
   1.637 +  assumes hH: "h \<in> H"
   1.638 +  shows "h \<in> carrier G"
   1.639 +by (rule subgroup.mem_carrier [OF a_subgroup,
   1.640 +    simplified monoid_record_simps])
   1.641 +
   1.642 +
   1.643 +subsection {* Lemmas for Right Cosets *}
   1.644 +
   1.645 +lemma (in abelian_subgroup) a_elemrcos_carrier:
   1.646 +  assumes acarr: "a \<in> carrier G"
   1.647 +      and a': "a' \<in> H +> a"
   1.648 +  shows "a' \<in> carrier G"
   1.649 +by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
   1.650 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.651 +
   1.652 +lemma (in abelian_subgroup) a_rcos_const:
   1.653 +  assumes hH: "h \<in> H"
   1.654 +  shows "H +> h = H"
   1.655 +by (rule subgroup.rcos_const [OF a_subgroup a_group,
   1.656 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.657 +
   1.658 +lemma (in abelian_subgroup) a_rcos_module_imp:
   1.659 +  assumes xcarr: "x \<in> carrier G"
   1.660 +      and x'cos: "x' \<in> H +> x"
   1.661 +  shows "(x' \<oplus> \<ominus>x) \<in> H"
   1.662 +by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
   1.663 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.664 +
   1.665 +lemma (in abelian_subgroup) a_rcos_module_rev:
   1.666 +  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   1.667 +      and xixH: "(x' \<oplus> \<ominus>x) \<in> H"
   1.668 +  shows "x' \<in> H +> x"
   1.669 +by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
   1.670 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.671 +
   1.672 +lemma (in abelian_subgroup) a_rcos_module:
   1.673 +  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   1.674 +  shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
   1.675 +by (rule subgroup.rcos_module [OF a_subgroup a_group,
   1.676 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
   1.677 +
   1.678 +--"variant"
   1.679 +lemma (in abelian_subgroup) a_rcos_module_minus:
   1.680 +  includes ring G
   1.681 +  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
   1.682 +  shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
   1.683 +proof -
   1.684 +  from carr
   1.685 +      have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
   1.686 +  from this and carr
   1.687 +      show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
   1.688 +      by (simp add: minus_eq)
   1.689 +qed
   1.690 +
   1.691 +lemma (in abelian_subgroup) a_repr_independence':
   1.692 +  assumes "y \<in> H +> x"
   1.693 +      and "x \<in> carrier G"
   1.694 +  shows "H +> x = H +> y"
   1.695 +apply (rule a_repr_independence, assumption+)
   1.696 +apply (rule a_subgroup)
   1.697 +done
   1.698 +
   1.699 +lemma (in abelian_subgroup) a_repr_independenceD:
   1.700 +  assumes ycarr: "y \<in> carrier G"
   1.701 +      and repr:  "H +> x = H +> y"
   1.702 +  shows "y \<in> H +> x"
   1.703 +by (rule group.repr_independenceD [OF a_group a_subgroup,
   1.704 +    folded a_r_coset_def, simplified monoid_record_simps])
   1.705 +
   1.706 +
   1.707 +subsection {* Lemmas for the Set of Right Cosets *}
   1.708 +
   1.709 +lemma (in abelian_subgroup) a_rcosets_carrier:
   1.710 +  "X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
   1.711 +by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
   1.712 +    folded A_RCOSETS_def, simplified monoid_record_simps])
   1.713 +
   1.714 +
   1.715 +
   1.716 +subsection {* Addition of Subgroups *}
   1.717 +
   1.718 +lemma (in abelian_monoid) set_add_closed:
   1.719 +  assumes Acarr: "A \<subseteq> carrier G"
   1.720 +      and Bcarr: "B \<subseteq> carrier G"
   1.721 +  shows "A <+> B \<subseteq> carrier G"
   1.722 +by (rule monoid.set_mult_closed [OF a_monoid,
   1.723 +    folded set_add_def, simplified monoid_record_simps])
   1.724 +
   1.725 +lemma (in abelian_group) add_additive_subgroups:
   1.726 +  assumes subH: "additive_subgroup H G"
   1.727 +      and subK: "additive_subgroup K G"
   1.728 +  shows "additive_subgroup (H <+> K) G"
   1.729 +apply (rule additive_subgroup.intro)
   1.730 +apply (unfold set_add_def)
   1.731 +apply (intro comm_group.mult_subgroups)
   1.732 +  apply (rule a_comm_group)
   1.733 + apply (rule additive_subgroup.a_subgroup[OF subH])
   1.734 +apply (rule additive_subgroup.a_subgroup[OF subK])
   1.735 +done
   1.736 +
   1.737 +end