author wenzelm Mon Nov 07 16:39:14 2011 +0100 (2011-11-07) changeset 45388 121b2db078b1 parent 45385 7c1375ba1424 child 45389 bc0d50f8ae19
tuned proofs;
```     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 14:59:58 2011 +0100
1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 07 16:39:14 2011 +0100
1.3 @@ -246,21 +246,19 @@
1.4    shows "abelian_subgroup H G"
1.5  proof -
1.6    interpret comm_group "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.7 -  by (rule a_comm_group)
1.8 +    by (rule a_comm_group)
1.9    interpret subgroup "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
1.10 -  by (rule a_subgroup)
1.11 +    by (rule a_subgroup)
1.12
1.13    show "abelian_subgroup H G"
1.14 -  apply unfold_locales
1.15 +    apply unfold_locales
1.16    proof (simp add: r_coset_def l_coset_def, clarsimp)
1.17      fix x
1.18      assume xcarr: "x \<in> carrier G"
1.19 -    from a_subgroup
1.20 -        have Hcarr: "H \<subseteq> carrier G" by (unfold subgroup_def, simp)
1.21 -    from xcarr Hcarr
1.22 -        show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
1.23 -        using m_comm[simplified]
1.24 -        by fast
1.25 +    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
1.26 +      unfolding subgroup_def by simp
1.27 +    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
1.28 +      using m_comm [simplified] by fast
1.29    qed
1.30  qed
1.31
1.32 @@ -543,9 +541,10 @@
1.33  proof -
1.34    interpret G: abelian_group G by fact
1.35    interpret H: abelian_group H by fact
1.36 -  show ?thesis apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.37 -    apply fact
1.38 -    apply fact
1.39 +  show ?thesis
1.40 +    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
1.41 +      apply fact
1.42 +     apply fact
1.43      apply (rule a_group_hom)
1.44      done
1.45  qed
```