src/HOL/Algebra/AbelCoset.thy
 changeset 27611 2c01c0bdb385 parent 27192 005d4b953fdc child 27717 21bbd410ba04
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:02:10 2008 +0200
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Tue Jul 15 16:50:09 2008 +0200
1.3 @@ -60,7 +60,7 @@
1.4    a_r_coset_def r_coset_def
1.5
1.6  lemma a_r_coset_def':
1.7 -  includes struct G
1.8 +  fixes G (structure)
1.9    shows "H +> a \<equiv> \<Union>h\<in>H. {h \<oplus> a}"
1.10  unfolding a_r_coset_defs
1.11  by simp
1.12 @@ -69,7 +69,7 @@
1.13    a_l_coset_def l_coset_def
1.14
1.15  lemma a_l_coset_def':
1.16 -  includes struct G
1.17 +  fixes G (structure)
1.18    shows "a <+ H \<equiv> \<Union>h\<in>H. {a \<oplus> h}"
1.19  unfolding a_l_coset_defs
1.20  by simp
1.21 @@ -78,7 +78,7 @@
1.22    A_RCOSETS_def RCOSETS_def
1.23
1.24  lemma A_RCOSETS_def':
1.25 -  includes struct G
1.26 +  fixes G (structure)
1.27    shows "a_rcosets H \<equiv> \<Union>a\<in>carrier G. {H +> a}"
1.28  unfolding A_RCOSETS_defs
1.29  by (fold a_r_coset_def, simp)
1.30 @@ -87,7 +87,7 @@
1.32
1.34 -  includes struct G
1.35 +  fixes G (structure)
1.36    shows "H <+> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<oplus> k}"
1.38  by simp
1.39 @@ -96,7 +96,7 @@
1.40    A_SET_INV_def SET_INV_def
1.41
1.42  lemma A_SET_INV_def':
1.43 -  includes struct G
1.44 +  fixes G (structure)
1.45    shows "a_set_inv H \<equiv> \<Union>h\<in>H. {\<ominus> h}"
1.46  unfolding A_SET_INV_defs
1.47  by (fold a_inv_def)
1.48 @@ -188,7 +188,7 @@
1.50
1.52 -  includes struct G
1.53 +  fixes G (structure)
1.54    assumes a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.56  by (rule additive_subgroup.intro) (rule a_subgroup)
1.57 @@ -240,7 +240,7 @@
1.58  qed
1.59
1.60  lemma abelian_subgroupI2:
1.61 -  includes struct G
1.62 +  fixes G (structure)
1.63    assumes a_comm_group: "comm_group \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.64        and a_subgroup: "subgroup H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.65    shows "abelian_subgroup H G"
1.66 @@ -265,7 +265,7 @@
1.67  qed
1.68
1.69  lemma abelian_subgroupI3:
1.70 -  includes struct G
1.71 +  fixes G (structure)
1.72    assumes asg: "additive_subgroup H G"
1.73        and ag: "abelian_group G"
1.74    shows "abelian_subgroup H G"
1.75 @@ -451,7 +451,7 @@
1.76  lemmas A_FactGroup_defs = A_FactGroup_def FactGroup_def
1.77
1.78  lemma A_FactGroup_def':
1.79 -  includes struct G
1.80 +  fixes G (structure)
1.81    shows "G A_Mod H \<equiv> \<lparr>carrier = a_rcosets\<^bsub>G\<^esub> H, mult = set_add G, one = H\<rparr>"
1.82  unfolding A_FactGroup_defs
1.84 @@ -534,16 +534,20 @@
1.85  subsection {* Homomorphisms *}
1.86
1.87  lemma abelian_group_homI:
1.88 -  includes abelian_group G
1.89 -  includes abelian_group H
1.90 +  assumes "abelian_group G"
1.91 +  assumes "abelian_group H"
1.92    assumes a_group_hom: "group_hom (| carrier = carrier G, mult = add G, one = zero G |)
1.93                                    (| carrier = carrier H, mult = add H, one = zero H |) h"
1.94    shows "abelian_group_hom G H h"
1.95 -apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.96 -  apply (rule G.abelian_group_axioms)
1.97 - apply (rule H.abelian_group_axioms)
1.98 -apply (rule a_group_hom)
1.99 -done
1.100 +proof -
1.101 +  interpret G: abelian_group [G] by fact
1.102 +  interpret H: abelian_group [H] by fact
1.103 +  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.104 +    apply fact
1.105 +    apply fact
1.106 +    apply (rule a_group_hom)
1.107 +    done
1.108 +qed
1.109
1.110  lemma (in abelian_group_hom) is_abelian_group_hom:
1.111    "abelian_group_hom G H h"
1.112 @@ -688,10 +692,11 @@
1.113
1.114  --"variant"
1.115  lemma (in abelian_subgroup) a_rcos_module_minus:
1.116 -  includes ring G
1.117 +  assumes "ring G"
1.118    assumes carr: "x \<in> carrier G" "x' \<in> carrier G"
1.119    shows "(x' \<in> H +> x) = (x' \<ominus> x \<in> H)"
1.120  proof -
1.121 +  interpret G: ring [G] by fact
1.122    from carr
1.123    have "(x' \<in> H +> x) = (x' \<oplus> \<ominus>x \<in> H)" by (rule a_rcos_module)
1.124    with carr
```