tuned proofs;
authorwenzelm
Mon Nov 07 16:39:14 2011 +0100 (2011-11-07)
changeset 45388121b2db078b1
parent 45385 7c1375ba1424
child 45389 bc0d50f8ae19
tuned proofs;
src/HOL/Algebra/AbelCoset.thy
     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