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.31    set_add_def set_mult_def
    1.32  
    1.33  lemma set_add_def':
    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.37  unfolding set_add_defs
    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.49  by (rule additive_subgroup_axioms)
    1.50  
    1.51  lemma additive_subgroupI:
    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.55    shows "additive_subgroup H G"
    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.83  by (fold A_RCOSETS_def set_add_def)
    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