Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Algebra/Module.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 35849 b5522b51cb1e
child 58860 fee7cfa69c50
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf 
     1 (*  Title:      HOL/Algebra/Module.thy

     2     Author:     Clemens Ballarin, started 15 April 2003

     3     Copyright:  Clemens Ballarin

     4 *)

     5 

     6 theory Module

     7 imports Ring

     8 begin

     9 

    10 section {* Modules over an Abelian Group *}

    11 

    12 subsection {* Definitions *}

    13 

    14 record ('a, 'b) module = "'b ring" +

    15   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)

    16 

    17 locale module = R: cring + M: abelian_group M for M (structure) +

    18   assumes smult_closed [simp, intro]:

    19       "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"

    20     and smult_l_distr:

    21       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    22       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"

    23     and smult_r_distr:

    24       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>

    25       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"

    26     and smult_assoc1:

    27       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    28       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"

    29     and smult_one [simp]:

    30       "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"

    31 

    32 locale algebra = module + cring M +

    33   assumes smult_assoc2:

    34       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>

    35       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"

    36 

    37 lemma moduleI:

    38   fixes R (structure) and M (structure)

    39   assumes cring: "cring R"

    40     and abelian_group: "abelian_group M"

    41     and smult_closed:

    42       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"

    43     and smult_l_distr:

    44       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    45       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"

    46     and smult_r_distr:

    47       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>

    48       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)"

    49     and smult_assoc1:

    50       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    51       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"

    52     and smult_one:

    53       "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"

    54   shows "module R M"

    55   by (auto intro: module.intro cring.axioms abelian_group.axioms

    56     module_axioms.intro assms)

    57 

    58 lemma algebraI:

    59   fixes R (structure) and M (structure)

    60   assumes R_cring: "cring R"

    61     and M_cring: "cring M"

    62     and smult_closed:

    63       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"

    64     and smult_l_distr:

    65       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    66       (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"

    67     and smult_r_distr:

    68       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>

    69       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)"

    70     and smult_assoc1:

    71       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>

    72       (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"

    73     and smult_one:

    74       "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"

    75     and smult_assoc2:

    76       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>

    77       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"

    78   shows "algebra R M"

    79 apply intro_locales

    80 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+

    81 apply (rule module_axioms.intro)

    82  apply (simp add: smult_closed)

    83  apply (simp add: smult_l_distr)

    84  apply (simp add: smult_r_distr)

    85  apply (simp add: smult_assoc1)

    86  apply (simp add: smult_one)

    87 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+

    88 apply (rule algebra_axioms.intro)

    89  apply (simp add: smult_assoc2)

    90 done

    91 

    92 lemma (in algebra) R_cring:

    93   "cring R"

    94   ..

    95 

    96 lemma (in algebra) M_cring:

    97   "cring M"

    98   ..

    99 

   100 lemma (in algebra) module:

   101   "module R M"

   102   by (auto intro: moduleI R_cring is_abelian_group

   103     smult_l_distr smult_r_distr smult_assoc1)

   104 

   105 

   106 subsection {* Basic Properties of Algebras *}

   107 

   108 lemma (in algebra) smult_l_null [simp]:

   109   "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"

   110 proof -

   111   assume M: "x \<in> carrier M"

   112   note facts = M smult_closed [OF R.zero_closed]

   113   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

   114   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)"

   115     by (simp add: smult_l_distr del: R.l_zero R.r_zero)

   116   also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done

   117   finally show ?thesis .

   118 qed

   119 

   120 lemma (in algebra) smult_r_null [simp]:

   121   "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";

   122 proof -

   123   assume R: "a \<in> carrier R"

   124   note facts = R smult_closed

   125   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>)"

   126     by algebra

   127   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>)"

   128     by (simp add: smult_r_distr del: M.l_zero M.r_zero)

   129   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra

   130   finally show ?thesis .

   131 qed

   132 

   133 lemma (in algebra) smult_l_minus:

   134   "[| 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)"

   135 proof -

   136   assume RM: "a \<in> carrier R" "x \<in> carrier M"

   137   from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp

   138   from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp

   139   note facts = RM a_smult ma_smult

   140   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)"

   141     by algebra

   142   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)"

   143     by (simp add: smult_l_distr)

   144   also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"

   145     apply algebra apply algebra done

   146   finally show ?thesis .

   147 qed

   148 

   149 lemma (in algebra) smult_r_minus:

   150   "[| 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)"

   151 proof -

   152   assume RM: "a \<in> carrier R" "x \<in> carrier M"

   153   note facts = RM smult_closed

   154   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)"

   155     by algebra

   156   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)"

   157     by (simp add: smult_r_distr)

   158   also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra

   159   finally show ?thesis .

   160 qed

   161 

   162 end
isabelle