src/HOL/Algebra/Module.thy
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19984 29bb4659f80a
     1.1 --- a/src/HOL/Algebra/Module.thy	Tue Jun 20 14:51:59 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Module.thy	Tue Jun 20 15:53:44 2006 +0200
     1.3 @@ -73,16 +73,26 @@
     1.4        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
     1.5        (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
     1.6    shows "algebra R M"
     1.7 -  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
     1.8 -    module_axioms.intro prems)
     1.9 +apply (intro_locales!)
    1.10 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    1.11 +apply (rule module_axioms.intro)
    1.12 + apply (simp add: smult_closed)
    1.13 + apply (simp add: smult_l_distr)
    1.14 + apply (simp add: smult_r_distr)
    1.15 + apply (simp add: smult_assoc1)
    1.16 + apply (simp add: smult_one)
    1.17 +apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    1.18 +apply (rule algebra_axioms.intro)
    1.19 + apply (simp add: smult_assoc2)
    1.20 +done
    1.21  
    1.22  lemma (in algebra) R_cring:
    1.23    "cring R"
    1.24 -  by (rule cring.intro)
    1.25 +  by intro_locales
    1.26  
    1.27  lemma (in algebra) M_cring:
    1.28    "cring M"
    1.29 -  by (rule cring.intro)
    1.30 +  by intro_locales
    1.31  
    1.32  lemma (in algebra) module:
    1.33    "module R M"