src/HOL/Algebra/Module.thy
 author ballarin Mon Aug 02 09:44:46 2004 +0200 (2004-08-02) changeset 15095 63f5f4c265dd parent 14706 71590b7733b7 child 16417 9bc16273c2d4 permissions -rw-r--r--
Theories now take advantage of recent syntax improvements with (structure).
```     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 = CRing:
```
```    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   includes struct R + struct M
```
```    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   includes struct R + struct M
```
```    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   by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms
```
```    77     module_axioms.intro prems)
```
```    78
```
```    79 lemma (in algebra) R_cring:
```
```    80   "cring R"
```
```    81   by (rule cring.intro)
```
```    82
```
```    83 lemma (in algebra) M_cring:
```
```    84   "cring M"
```
```    85   by (rule cring.intro)
```
```    86
```
```    87 lemma (in algebra) module:
```
```    88   "module R M"
```
```    89   by (auto intro: moduleI R_cring is_abelian_group
```
```    90     smult_l_distr smult_r_distr smult_assoc1)
```
```    91
```
```    92
```
```    93 subsection {* Basic Properties of Algebras *}
```
```    94
```
```    95 lemma (in algebra) smult_l_null [simp]:
```
```    96   "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
```
```    97 proof -
```
```    98   assume M: "x \<in> carrier M"
```
```    99   note facts = M smult_closed
```
```   100   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
```
```   101   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)"
```
```   102     by (simp add: smult_l_distr del: R.l_zero R.r_zero)
```
```   103   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
```
```   104   finally show ?thesis .
```
```   105 qed
```
```   106
```
```   107 lemma (in algebra) smult_r_null [simp]:
```
```   108   "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
```
```   109 proof -
```
```   110   assume R: "a \<in> carrier R"
```
```   111   note facts = R smult_closed
```
```   112   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>)"
```
```   113     by algebra
```
```   114   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>)"
```
```   115     by (simp add: smult_r_distr del: M.l_zero M.r_zero)
```
```   116   also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
```
```   117   finally show ?thesis .
```
```   118 qed
```
```   119
```
```   120 lemma (in algebra) smult_l_minus:
```
```   121   "[| 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)"
```
```   122 proof -
```
```   123   assume RM: "a \<in> carrier R" "x \<in> carrier M"
```
```   124   note facts = RM smult_closed
```
```   125   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)"
```
```   126     by algebra
```
```   127   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)"
```
```   128     by (simp add: smult_l_distr)
```
```   129   also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
```
```   130   finally show ?thesis .
```
```   131 qed
```
```   132
```
```   133 lemma (in algebra) smult_r_minus:
```
```   134   "[| 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)"
```
```   135 proof -
```
```   136   assume RM: "a \<in> carrier R" "x \<in> carrier M"
```
```   137   note facts = RM smult_closed
```
```   138   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)"
```
```   139     by algebra
```
```   140   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)"
```
```   141     by (simp add: smult_r_distr)
```
```   142   also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
```
```   143   finally show ?thesis .
```
```   144 qed
```
```   145
```
```   146 end
```