src/HOL/Algebra/Module.thy
author ballarin
Tue Jun 20 15:53:44 2006 +0200 (2006-06-20)
changeset 19931 fb32b43e7f80
parent 19783 82f365a14960
child 19984 29bb4659f80a
permissions -rw-r--r--
Restructured locales with predicates: import is now an interpretation.
New method intro_locales.
     1 (*  Title:      HOL/Algebra/Module.thy
     2     ID:         $Id$
     3     Author:     Clemens Ballarin, started 15 April 2003
     4     Copyright:  Clemens Ballarin
     5 *)
     6 
     7 header {* Modules over an Abelian Group *}
     8 
     9 theory Module imports CRing begin
    10 
    11 record ('a, 'b) module = "'b ring" +
    12   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    13 
    14 locale module = cring R + abelian_group M +
    15   assumes smult_closed [simp, intro]:
    16       "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    17     and smult_l_distr:
    18       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    19       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
    20     and smult_r_distr:
    21       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    22       a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> y"
    23     and smult_assoc1:
    24       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    25       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    26     and smult_one [simp]:
    27       "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    28 
    29 locale algebra = module R M + cring M +
    30   assumes smult_assoc2:
    31       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    32       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    33 
    34 lemma moduleI:
    35   fixes R (structure) and M (structure)
    36   assumes cring: "cring R"
    37     and abelian_group: "abelian_group M"
    38     and smult_closed:
    39       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    40     and smult_l_distr:
    41       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    42       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    43     and smult_r_distr:
    44       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    45       a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> y)"
    46     and smult_assoc1:
    47       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    48       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    49     and smult_one:
    50       "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    51   shows "module R M"
    52   by (auto intro: module.intro cring.axioms abelian_group.axioms
    53     module_axioms.intro prems)
    54 
    55 lemma algebraI:
    56   fixes R (structure) and M (structure)
    57   assumes R_cring: "cring R"
    58     and M_cring: "cring M"
    59     and smult_closed:
    60       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    61     and smult_l_distr:
    62       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    63       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    64     and smult_r_distr:
    65       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    66       a \<odot>\<^bsub>M\<^esub> (x \<oplus>\<^bsub>M\<^esub> y) = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> y)"
    67     and smult_assoc1:
    68       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    69       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    70     and smult_one:
    71       "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
    72     and smult_assoc2:
    73       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    74       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    75   shows "algebra R M"
    76 apply (intro_locales!)
    77 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    78 apply (rule module_axioms.intro)
    79  apply (simp add: smult_closed)
    80  apply (simp add: smult_l_distr)
    81  apply (simp add: smult_r_distr)
    82  apply (simp add: smult_assoc1)
    83  apply (simp add: smult_one)
    84 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
    85 apply (rule algebra_axioms.intro)
    86  apply (simp add: smult_assoc2)
    87 done
    88 
    89 lemma (in algebra) R_cring:
    90   "cring R"
    91   by intro_locales
    92 
    93 lemma (in algebra) M_cring:
    94   "cring M"
    95   by intro_locales
    96 
    97 lemma (in algebra) module:
    98   "module R M"
    99   by (auto intro: moduleI R_cring is_abelian_group
   100     smult_l_distr smult_r_distr smult_assoc1)
   101 
   102 
   103 subsection {* Basic Properties of Algebras *}
   104 
   105 lemma (in algebra) smult_l_null [simp]:
   106   "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
   107 proof -
   108   assume M: "x \<in> carrier M"
   109   note facts = M smult_closed
   110   from facts have "\<zero> \<odot>\<^bsub>M\<^esub> x = (\<zero> \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<zero> \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)" by algebra
   111   also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (\<zero> \<odot>\<^bsub>M\<^esub> x)"
   112     by (simp add: smult_l_distr del: R.l_zero R.r_zero)
   113   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
   114   finally show ?thesis .
   115 qed
   116 
   117 lemma (in algebra) smult_r_null [simp]:
   118   "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
   119 proof -
   120   assume R: "a \<in> carrier R"
   121   note facts = R smult_closed
   122   from facts have "a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
   123     by algebra
   124   also from R have "... = a \<odot>\<^bsub>M\<^esub> (\<zero>\<^bsub>M\<^esub> \<oplus>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub>)"
   125     by (simp add: smult_r_distr del: M.l_zero M.r_zero)
   126   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
   127   finally show ?thesis .
   128 qed
   129 
   130 lemma (in algebra) smult_l_minus:
   131   "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^bsub>M\<^esub> x = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
   132 proof -
   133   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   134   note facts = RM smult_closed
   135   from facts have "(\<ominus>a) \<odot>\<^bsub>M\<^esub> x = (\<ominus>a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   136     by algebra
   137   also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   138     by (simp add: smult_l_distr)
   139   also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   140   finally show ?thesis .
   141 qed
   142 
   143 lemma (in algebra) smult_r_minus:
   144   "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = \<ominus>\<^bsub>M\<^esub> (a \<odot>\<^bsub>M\<^esub> x)"
   145 proof -
   146   assume RM: "a \<in> carrier R" "x \<in> carrier M"
   147   note facts = RM smult_closed
   148   from facts have "a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x) = (a \<odot>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   149     by algebra
   150   also from RM have "... = a \<odot>\<^bsub>M\<^esub> (\<ominus>\<^bsub>M\<^esub>x \<oplus>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
   151     by (simp add: smult_r_distr)
   152   also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   153   finally show ?thesis .
   154 qed
   155 
   156 end