--- a/src/HOL/Algebra/AbelCoset.thy Tue Jun 12 11:18:35 2018 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Tue Jun 12 16:08:57 2018 +0100
@@ -17,45 +17,42 @@
definition
a_r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "+>\<index>" 60)
- where "a_r_coset G = r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_r_coset G = r_coset (add_monoid G)"
definition
a_l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<+\<index>" 60)
- where "a_l_coset G = l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_l_coset G = l_coset (add_monoid G)"
definition
A_RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("a'_rcosets\<index> _" [81] 80)
- where "A_RCOSETS G H = RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_RCOSETS G H = RCOSETS (add_monoid G) H"
definition
set_add :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
- where "set_add G = set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "set_add G = set_mult (add_monoid G)"
definition
A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("a'_set'_inv\<index> _" [81] 80)
- where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_SET_INV G H = SET_INV (add_monoid G) H"
definition
a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set" ("racong\<index>")
- where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ where "a_r_congruent G = r_congruent (add_monoid G)"
definition
A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
\<comment> \<open>Actually defined for groups rather than monoids\<close>
- where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+ where "A_FactGroup G H = FactGroup (add_monoid G) H"
definition
a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
\<comment> \<open>the kernel of a homomorphism (additive)\<close>
- where "a_kernel G H h =
- kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+ where "a_kernel G H h = kernel (add_monoid G) (add_monoid H) h"
locale abelian_group_hom = G?: abelian_group G + H?: abelian_group H
for G (structure) and H (structure) +
fixes h
- assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+ assumes a_group_hom: "group_hom (add_monoid G) (add_monoid H) h"
lemmas a_r_coset_defs =
a_r_coset_def r_coset_def
@@ -63,8 +60,7 @@
lemma a_r_coset_def':
fixes G (structure)
shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
-unfolding a_r_coset_defs
-by simp
+ unfolding a_r_coset_defs by simp
lemmas a_l_coset_defs =
a_l_coset_def l_coset_def
@@ -72,8 +68,7 @@
lemma a_l_coset_def':
fixes G (structure)
shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
-unfolding a_l_coset_defs
-by simp
+ unfolding a_l_coset_defs by simp
lemmas A_RCOSETS_defs =
A_RCOSETS_def RCOSETS_def
@@ -81,8 +76,7 @@
lemma A_RCOSETS_def':
fixes G (structure)
shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
-unfolding A_RCOSETS_defs
-by (fold a_r_coset_def, simp)
+ unfolding A_RCOSETS_defs by (fold a_r_coset_def, simp)
lemmas set_add_defs =
set_add_def set_mult_def
@@ -90,8 +84,7 @@
lemma set_add_def':
fixes G (structure)
shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
-unfolding set_add_defs
-by simp
+ unfolding set_add_defs by simp
lemmas A_SET_INV_defs =
A_SET_INV_def SET_INV_def
@@ -99,18 +92,53 @@
lemma A_SET_INV_def':
fixes G (structure)
shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
-unfolding A_SET_INV_defs
-by (fold a_inv_def)
+ unfolding A_SET_INV_defs by (fold a_inv_def)
subsubsection \<open>Cosets\<close>
+sublocale abelian_group <
+ add: group "(add_monoid G)"
+ rewrites "carrier (add_monoid G) = carrier G"
+ and " mult (add_monoid G) = add G"
+ and " one (add_monoid G) = zero G"
+ and " m_inv (add_monoid G) = a_inv G"
+ and "finprod (add_monoid G) = finsum G"
+ and "r_coset (add_monoid G) = a_r_coset G"
+ and "l_coset (add_monoid G) = a_l_coset G"
+ and "(\<lambda>a k. pow (add_monoid G) a k) = (\<lambda>a k. add_pow G k a)"
+ by (rule a_group)
+ (auto simp: m_inv_def a_inv_def finsum_def a_r_coset_def a_l_coset_def add_pow_def)
+
+context abelian_group
+begin
+
+thm add.coset_mult_assoc
+lemmas a_repr_independence' = add.repr_independence
+
+(*
+lemmas a_coset_add_assoc = add.coset_mult_assoc
+lemmas a_coset_add_zero [simp] = add.coset_mult_one
+lemmas a_coset_add_inv1 = add.coset_mult_inv1
+lemmas a_coset_add_inv2 = add.coset_mult_inv2
+lemmas a_coset_join1 = add.coset_join1
+lemmas a_coset_join2 = add.coset_join2
+lemmas a_solve_equation = add.solve_equation
+lemmas a_repr_independence = add.repr_independence
+lemmas a_rcosI = add.rcosI
+lemmas a_rcosetsI = add.rcosetsI
+*)
+
+end
+
lemma (in abelian_group) a_coset_add_assoc:
"[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
==> (M +> g) +> h = M +> (g \<oplus> h)"
by (rule group.coset_mult_assoc [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
+thm abelian_group.a_coset_add_assoc
+
lemma (in abelian_group) a_coset_add_zero [simp]:
"M \<subseteq> carrier G ==> M +> \<zero> = M"
by (rule group.coset_mult_one [OF a_group,
@@ -129,22 +157,22 @@
folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
lemma (in abelian_group) a_coset_join1:
- "[| H +> x = H; x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H"
+ "[| H +> x = H; x \<in> carrier G; subgroup H (add_monoid G) |] ==> x \<in> H"
by (rule group.coset_join1 [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_solve_equation:
- "\<lbrakk>subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
+ "\<lbrakk>subgroup H (add_monoid G); x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<oplus> x"
by (rule group.solve_equation [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_repr_independence:
- "\<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"
-by (rule group.repr_independence [OF a_group,
- folded a_r_coset_def, simplified monoid_record_simps])
+ "\<lbrakk> y \<in> H +> x; x \<in> carrier G; subgroup H (add_monoid G) \<rbrakk> \<Longrightarrow>
+ H +> x = H +> y"
+ using a_repr_independence' by (simp add: a_r_coset_def)
lemma (in abelian_group) a_coset_join2:
- "\<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"
+ "\<lbrakk>x \<in> carrier G; subgroup H (add_monoid G); x\<in>H\<rbrakk> \<Longrightarrow> H +> x = H"
by (rule group.coset_join2 [OF a_group,
folded a_r_coset_def, simplified monoid_record_simps])
@@ -167,23 +195,15 @@
lemma (in abelian_group) a_transpose_inv:
"[| x \<oplus> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]
==> (\<ominus> x) \<oplus> z = y"
-by (rule group.transpose_inv [OF a_group,
- folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
+ using r_neg1 by blast
-(*
---"duplicate"
-lemma (in abelian_group) a_rcos_self:
- "[| x \<in> carrier G; subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> |] ==> x \<in> H +> x"
-by (rule group.rcos_self [OF a_group,
- folded a_r_coset_def, simplified monoid_record_simps])
-*)
subsubsection \<open>Subgroups\<close>
locale additive_subgroup =
fixes H and G (structure)
- assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ assumes a_subgroup: "subgroup H (add_monoid G)"
lemma (in additive_subgroup) is_additive_subgroup:
shows "additive_subgroup H G"
@@ -191,7 +211,7 @@
lemma additive_subgroupI:
fixes G (structure)
- assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ assumes a_subgroup: "subgroup H (add_monoid G)"
shows "additive_subgroup H G"
by (rule additive_subgroup.intro) (rule a_subgroup)
@@ -221,18 +241,18 @@
text \<open>Every subgroup of an \<open>abelian_group\<close> is normal\<close>
locale abelian_subgroup = additive_subgroup + abelian_group G +
- assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ assumes a_normal: "normal H (add_monoid G)"
lemma (in abelian_subgroup) is_abelian_subgroup:
shows "abelian_subgroup H G"
by (rule abelian_subgroup_axioms)
lemma abelian_subgroupI:
- assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ assumes a_normal: "normal H (add_monoid G)"
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"
shows "abelian_subgroup H G"
proof -
- interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ interpret normal "H" "(add_monoid G)"
by (rule a_normal)
show "abelian_subgroup H G"
@@ -241,13 +261,13 @@
lemma abelian_subgroupI2:
fixes G (structure)
- assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ assumes a_comm_group: "comm_group (add_monoid G)"
+ and a_subgroup: "subgroup H (add_monoid G)"
shows "abelian_subgroup H G"
proof -
- interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ interpret comm_group "(add_monoid G)"
by (rule a_comm_group)
- interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+ interpret subgroup "H" "(add_monoid G)"
by (rule a_subgroup)
show "abelian_subgroup H G"
@@ -264,13 +284,10 @@
lemma abelian_subgroupI3:
fixes G (structure)
- assumes asg: "additive_subgroup H G"
- and ag: "abelian_group G"
+ assumes "additive_subgroup H G"
+ and "abelian_group G"
shows "abelian_subgroup H G"
-apply (rule abelian_subgroupI2)
- apply (rule abelian_group.a_comm_group[OF ag])
-apply (rule additive_subgroup.a_subgroup[OF asg])
-done
+ using assms abelian_subgroupI2 abelian_group.a_comm_group additive_subgroup_def by blast
lemma (in abelian_subgroup) a_coset_eq:
"(\<forall>x \<in> carrier G. H +> x = x <+ H)"
@@ -289,15 +306,14 @@
text\<open>Alternative characterization of normal subgroups\<close>
lemma (in abelian_group) a_normal_inv_iff:
- "(N \<lhd> \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>) =
- (subgroup N \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<and> (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
+ "(N \<lhd> (add_monoid G)) =
+ (subgroup N (add_monoid G) & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
(is "_ = ?rhs")
by (rule group.normal_inv_iff [OF a_group,
folded a_inv_def, simplified monoid_record_simps])
lemma (in abelian_group) a_lcos_m_assoc:
- "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
- ==> g <+ (h <+ M) = (g \<oplus> h) <+ M"
+ "\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M"
by (rule group.lcos_m_assoc [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
@@ -308,33 +324,28 @@
lemma (in abelian_group) a_l_coset_subset_G:
- "[| H \<subseteq> carrier G; x \<in> carrier G |] ==> x <+ H \<subseteq> carrier G"
+ "\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G"
by (rule group.l_coset_subset_G [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_coset_swap:
- "\<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"
+ "\<lbrakk>y \<in> x <+ H; x \<in> carrier G; subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
by (rule group.l_coset_swap [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_coset_carrier:
- "[| 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"
+ "[| y \<in> x <+ H; x \<in> carrier G; subgroup H (add_monoid G) |] ==> y \<in> carrier G"
by (rule group.l_coset_carrier [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
lemma (in abelian_group) a_l_repr_imp_subset:
- 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>"
+ assumes "y \<in> x <+ H" "x \<in> carrier G" "subgroup H (add_monoid G)"
shows "y <+ H \<subseteq> x <+ H"
-apply (rule group.l_repr_imp_subset [OF a_group,
- folded a_l_coset_def, simplified monoid_record_simps])
-apply (rule y)
-apply (rule x)
-apply (rule sb)
-done
+ by (metis (full_types) a_l_coset_defs(1) add.l_repr_independence assms set_eq_subset)
lemma (in abelian_group) a_l_repr_independence:
- 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>"
+ assumes y: "y \<in> x <+ H" and x: "x \<in> carrier G" and sb: "subgroup H (add_monoid G)"
shows "x <+ H = y <+ H"
apply (rule group.l_repr_independence [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])
@@ -348,7 +359,7 @@
by (rule group.setmult_subset_G [OF a_group,
folded set_add_def, simplified monoid_record_simps])
-lemma (in abelian_group) subgroup_add_id: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> \<Longrightarrow> H <+> H = H"
+lemma (in abelian_group) subgroup_add_id: "subgroup H (add_monoid G) \<Longrightarrow> H <+> H = H"
by (rule group.subgroup_mult_id [OF a_group,
folded set_add_def, simplified monoid_record_simps])
@@ -427,8 +438,7 @@
lemma (in abelian_group) a_card_cosets_equal:
"\<lbrakk>c \<in> a_rcosets H; H \<subseteq> carrier G; finite(carrier G)\<rbrakk>
\<Longrightarrow> card c = card H"
-by (rule group.card_cosets_equal [OF a_group,
- folded A_RCOSETS_def, simplified monoid_record_simps])
+ by (simp add: A_RCOSETS_defs(1) add.card_rcosets_equal)
lemma (in abelian_group) rcosets_subset_PowG:
"additive_subgroup H G \<Longrightarrow> a_rcosets H \<subseteq> Pow(carrier G)"
@@ -509,7 +519,7 @@
text\<open>The coset map is a homomorphism from @{term G} to the quotient group
@{term "G Mod H"}\<close>
lemma (in abelian_subgroup) a_r_coset_hom_A_Mod:
- "(\<lambda>a. H +> a) \<in> hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> (G A_Mod H)"
+ "(\<lambda>a. H +> a) \<in> hom (add_monoid G) (G A_Mod H)"
by (rule normal.r_coset_hom_Mod [OF a_normal,
folded A_FactGroup_def a_r_coset_def, simplified monoid_record_simps])
@@ -535,8 +545,8 @@
lemma abelian_group_homI:
assumes "abelian_group G"
assumes "abelian_group H"
- assumes a_group_hom: "group_hom \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+ assumes a_group_hom: "group_hom (add_monoid G)
+ (add_monoid H) h"
shows "abelian_group_hom G H h"
proof -
interpret G: abelian_group G by fact
@@ -614,7 +624,7 @@
lemma (in abelian_group_hom) A_FactGroup_hom:
"(\<lambda>X. the_elem (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
+ (add_monoid H)"
by (rule group_hom.FactGroup_hom[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
@@ -633,13 +643,16 @@
text\<open>If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.\<close>
-theorem (in abelian_group_hom) A_FactGroup_iso:
+theorem (in abelian_group_hom) A_FactGroup_iso_set:
"h ` carrier G = carrier H
- \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> (G A_Mod (a_kernel G H h)) \<cong>
- \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr>"
-by (rule group_hom.FactGroup_iso[OF a_group_hom,
+ \<Longrightarrow> (\<lambda>X. the_elem (h`X)) \<in> iso (G A_Mod (a_kernel G H h)) (add_monoid H)"
+by (rule group_hom.FactGroup_iso_set[OF a_group_hom,
folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
+corollary (in abelian_group_hom) A_FactGroup_iso :
+ "h ` carrier G = carrier H
+ \<Longrightarrow> (G A_Mod (a_kernel G H h)) \<cong> (add_monoid H)"
+ using A_FactGroup_iso_set unfolding is_iso_def by auto
subsubsection \<open>Cosets\<close>