src/HOL/Algebra/AbelCoset.thy
 changeset 23350 50c5b0912a0c parent 21502 7f3ea2b3bab6 child 23383 5460951833fa
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Wed Jun 13 00:01:38 2007 +0200
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Jun 13 00:01:41 2007 +0200
1.3 @@ -185,13 +185,13 @@
1.4
1.5  lemma (in additive_subgroup) is_additive_subgroup:
1.6    shows "additive_subgroup H G"
1.7 -by -
1.8 +by fact
1.9
1.10  lemma additive_subgroupI:
1.11    includes struct G
1.12    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.13    shows "additive_subgroup H G"
1.14 -by (rule additive_subgroup.intro)
1.15 +by (rule additive_subgroup.intro) (rule a_subgroup)
1.16
1.17  lemma (in additive_subgroup) a_subset:
1.18       "H \<subseteq> carrier G"
1.19 @@ -225,7 +225,7 @@
1.20
1.21  lemma (in abelian_subgroup) is_abelian_subgroup:
1.22    shows "abelian_subgroup H G"
1.23 -by -
1.24 +by fact
1.25
1.26  lemma abelian_subgroupI:
1.27    assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.28 @@ -328,14 +328,22 @@
1.29  lemma (in abelian_group) a_l_repr_imp_subset:
1.30    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.31    shows "y <+ H \<subseteq> x <+ H"
1.32 -by (rule group.l_repr_imp_subset [OF a_group,
1.33 +apply (rule group.l_repr_imp_subset [OF a_group,
1.34      folded a_l_coset_def, simplified monoid_record_simps])
1.35 +apply (rule y)
1.36 +apply (rule x)
1.37 +apply (rule sb)
1.38 +done
1.39
1.40  lemma (in abelian_group) a_l_repr_independence:
1.41    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.42    shows "x <+ H = y <+ H"
1.43 -by (rule group.l_repr_independence [OF a_group,
1.44 +apply (rule group.l_repr_independence [OF a_group,
1.45      folded a_l_coset_def, simplified monoid_record_simps])
1.46 +apply (rule y)
1.47 +apply (rule x)
1.48 +apply (rule sb)
1.49 +done
1.50
1.51  lemma (in abelian_group) setadd_subset_G:
1.52       "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <+> K \<subseteq> carrier G"
1.53 @@ -350,7 +358,7 @@
1.54    assumes x:     "x \<in> carrier G"
1.55    shows "a_set_inv (H +> x) = H +> (\<ominus> x)"
1.56  by (rule normal.rcos_inv [OF a_normal,
1.57 -    folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps])
1.58 +  folded a_r_coset_def a_inv_def A_SET_INV_def, simplified monoid_record_simps]) (rule x)
1.59
1.60  lemma (in abelian_group) a_setmult_rcos_assoc:
1.61       "\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk>
1.62 @@ -388,7 +396,7 @@
1.63    assumes a: "a \<in> carrier G"
1.64    shows "a <+ H = racong H `` {a}"
1.65  by (rule subgroup.l_coset_eq_rcong [OF a_subgroup a_group,
1.66 -    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps])
1.67 +    folded a_r_congruent_def a_l_coset_def, simplified monoid_record_simps]) (rule a)
1.68
1.69  lemma (in abelian_subgroup) a_rcos_equation:
1.70    shows
1.71 @@ -531,7 +539,11 @@
1.72    assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
1.73                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
1.74    shows "abelian_group_hom G H h"
1.75 -by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.76 +apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.77 +  apply (rule G.abelian_group_axioms)
1.78 + apply (rule H.abelian_group_axioms)
1.79 +apply (rule a_group_hom)
1.80 +done
1.81
1.82  lemma (in abelian_group_hom) is_abelian_group_hom:
1.83    "abelian_group_hom G H h"
1.84 @@ -588,13 +600,13 @@
1.85    assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
1.86    shows "X \<noteq> {}"
1.87  by (rule group_hom.FactGroup_nonempty[OF a_group_hom,
1.88 -    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
1.89 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
1.90
1.91  lemma (in abelian_group_hom) FactGroup_contents_mem:
1.92    assumes X: "X \<in> carrier (G A_Mod (a_kernel G H h))"
1.93    shows "contents (h`X) \<in> carrier H"
1.94  by (rule group_hom.FactGroup_contents_mem[OF a_group_hom,
1.95 -    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
1.96 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule X)
1.97
1.98  lemma (in abelian_group_hom) A_FactGroup_hom:
1.99       "(\<lambda>X. contents (h`X)) \<in> hom (G A_Mod (a_kernel G H h))
1.100 @@ -613,7 +625,7 @@
1.101    assumes h: "h ` carrier G = carrier H"
1.102    shows "(\<lambda>X. contents (h ` X)) ` carrier (G A_Mod a_kernel G H h) = carrier H"
1.103  by (rule group_hom.FactGroup_onto[OF a_group_hom,
1.104 -    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
1.105 +    folded a_kernel_def A_FactGroup_def, simplified ring_record_simps]) (rule h)
1.106
1.107  text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
1.108   quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
1.109 @@ -634,7 +646,7 @@
1.110    assumes hH: "h \<in> H"
1.111    shows "h \<in> carrier G"
1.112  by (rule subgroup.mem_carrier [OF a_subgroup,
1.113 -    simplified monoid_record_simps])
1.114 +    simplified monoid_record_simps]) (rule hH)
1.115
1.116
1.117  subsection {* Lemmas for Right Cosets *}
1.118 @@ -644,31 +656,33 @@
1.119        and a': "a' \<in> H +> a"
1.120    shows "a' \<in> carrier G"
1.121  by (rule subgroup.elemrcos_carrier [OF a_subgroup a_group,
1.122 -    folded a_r_coset_def, simplified monoid_record_simps])
1.123 +    folded a_r_coset_def, simplified monoid_record_simps]) (rule acarr, rule a')
1.124
1.125  lemma (in abelian_subgroup) a_rcos_const:
1.126    assumes hH: "h \<in> H"
1.127    shows "H +> h = H"
1.128  by (rule subgroup.rcos_const [OF a_subgroup a_group,
1.129 -    folded a_r_coset_def, simplified monoid_record_simps])
1.130 +    folded a_r_coset_def, simplified monoid_record_simps]) (rule hH)
1.131
1.132  lemma (in abelian_subgroup) a_rcos_module_imp:
1.133    assumes xcarr: "x \<in> carrier G"
1.134        and x'cos: "x' \<in> H +> x"
1.135    shows "(x' \<oplus> \<ominus>x) \<in> H"
1.136  by (rule subgroup.rcos_module_imp [OF a_subgroup a_group,
1.137 -    folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
1.138 +    folded a_r_coset_def a_inv_def, simplified monoid_record_simps]) (rule xcarr, rule x'cos)
1.139
1.140  lemma (in abelian_subgroup) a_rcos_module_rev:
1.141 -  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
1.142 -      and xixH: "(x' \<oplus> \<ominus>x) \<in> H"
1.143 +  assumes "x \<in> carrier G" "x' \<in> carrier G"
1.144 +      and "(x' \<oplus> \<ominus>x) \<in> H"
1.145    shows "x' \<in> H +> x"
1.146 +using assms
1.147  by (rule subgroup.rcos_module_rev [OF a_subgroup a_group,
1.148      folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
1.149
1.150  lemma (in abelian_subgroup) a_rcos_module:
1.151 -  assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
1.152 +  assumes "x \<in> carrier G" "x' \<in> carrier G"
1.153    shows "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)"
1.154 +using assms
1.155  by (rule subgroup.rcos_module [OF a_subgroup a_group,
1.156      folded a_r_coset_def a_inv_def, simplified monoid_record_simps])
1.157
1.158 @@ -679,10 +693,10 @@
1.159    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
1.160  proof -
1.161    from carr
1.162 -      have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
1.163 -  from this and carr
1.164 -      show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
1.165 -      by (simp add: minus_eq)
1.166 +  have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
1.167 +  with carr
1.168 +  show "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
1.169 +    by (simp add: minus_eq)
1.170  qed
1.171
1.172  lemma (in abelian_subgroup) a_repr_independence':
```