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':