src/HOL/Algebra/Module.thy
 author ballarin Fri May 02 20:02:50 2003 +0200 (2003-05-02) changeset 13949 0ce528cd6f19 parent 13940 c67798653056 child 13952 6206d3e7672a permissions -rw-r--r--
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
```     1 (*  Title:      HOL/Algebra/Module
```
```     2     ID:         \$Id\$
```
```     3     Author:     Clemens Ballarin, started 15 April 2003
```
```     4     Copyright:  Clemens Ballarin
```
```     5 *)
```
```     6
```
```     7 theory Module = CRing:
```
```     8
```
```     9 section {* Modules over an Abelian Group *}
```
```    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>\<^sub>2 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>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
```
```    20     and smult_r_distr:
```
```    21       "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
```
```    22       a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
```
```    23     and smult_assoc1:
```
```    24       "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
```
```    25       (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
```
```    26     and smult_one [simp]:
```
```    27       "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 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>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
```
```    33
```
```    34 lemma moduleI:
```
```    35   assumes cring: "cring R"
```
```    36     and abelian_group: "abelian_group M"
```
```    37     and smult_closed:
```
```    38       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
```
```    39     and smult_l_distr:
```
```    40       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
```
```    41       smult M (add R a b) x = add M (smult M a x) (smult M b x)"
```
```    42     and smult_r_distr:
```
```    43       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
```
```    44       smult M a (add M x y) = add M (smult M a x) (smult M a y)"
```
```    45     and smult_assoc1:
```
```    46       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
```
```    47       smult M (mult R a b) x = smult M a (smult M b x)"
```
```    48     and smult_one:
```
```    49       "!!x. x \<in> carrier M ==> smult M (one R) x = x"
```
```    50   shows "module R M"
```
```    51   by (auto intro: module.intro cring.axioms abelian_group.axioms
```
```    52     module_axioms.intro prems)
```
```    53
```
```    54 lemma algebraI:
```
```    55   assumes R_cring: "cring R"
```
```    56     and M_cring: "cring M"
```
```    57     and smult_closed:
```
```    58       "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
```
```    59     and smult_l_distr:
```
```    60       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
```
```    61       smult M (add R a b) x = add M (smult M a x) (smult M b x)"
```
```    62     and smult_r_distr:
```
```    63       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
```
```    64       smult M a (add M x y) = add M (smult M a x) (smult M a y)"
```
```    65     and smult_assoc1:
```
```    66       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
```
```    67       smult M (mult R a b) x = smult M a (smult M b x)"
```
```    68     and smult_one:
```
```    69       "!!x. x \<in> carrier M ==> smult M (one R) x = x"
```
```    70     and smult_assoc2:
```
```    71       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
```
```    72       mult M (smult M a x) y = smult M a (mult M x y)"
```
```    73   shows "algebra R M"
```
```    74   by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms
```
```    75     module_axioms.intro prems)
```
```    76
```
```    77 lemma (in algebra) R_cring:
```
```    78   "cring R"
```
```    79   by (rule cring.intro) assumption+
```
```    80
```
```    81 lemma (in algebra) M_cring:
```
```    82   "cring M"
```
```    83   by (rule cring.intro) assumption+
```
```    84
```
```    85 lemma (in algebra) module:
```
```    86   "module R M"
```
```    87   by (auto intro: moduleI R_cring is_abelian_group
```
```    88     smult_l_distr smult_r_distr smult_assoc1)
```
```    89
```
```    90 subsection {* Basic Properties of Algebras *}
```
```    91
```
```    92 lemma (in algebra) smult_l_null [simp]:
```
```    93   "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
```
```    94 proof -
```
```    95   assume M: "x \<in> carrier M"
```
```    96   note facts = M smult_closed
```
```    97   from facts have "\<zero> \<odot>\<^sub>2 x = (\<zero> \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<zero> \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)" by algebra
```
```    98   also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
```
```    99     by (simp add: smult_l_distr del: R.l_zero R.r_zero)
```
```   100   also from facts have "... = \<zero>\<^sub>2" by algebra
```
```   101   finally show ?thesis .
```
```   102 qed
```
```   103
```
```   104 lemma (in algebra) smult_r_null [simp]:
```
```   105   "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
```
```   106 proof -
```
```   107   assume R: "a \<in> carrier R"
```
```   108   note facts = R smult_closed
```
```   109   from facts have "a \<odot>\<^sub>2 \<zero>\<^sub>2 = (a \<odot>\<^sub>2 \<zero>\<^sub>2 \<oplus>\<^sub>2 a \<odot>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
```
```   110     by algebra
```
```   111   also from R have "... = a \<odot>\<^sub>2 (\<zero>\<^sub>2 \<oplus>\<^sub>2 \<zero>\<^sub>2) \<oplus>\<^sub>2 \<ominus>\<^sub>2 (a \<odot>\<^sub>2 \<zero>\<^sub>2)"
```
```   112     by (simp add: smult_r_distr del: M.l_zero M.r_zero)
```
```   113   also from facts have "... = \<zero>\<^sub>2" by algebra
```
```   114   finally show ?thesis .
```
```   115 qed
```
```   116
```
```   117 lemma (in algebra) smult_l_minus:
```
```   118   "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
```
```   119 proof -
```
```   120   assume RM: "a \<in> carrier R" "x \<in> carrier M"
```
```   121   note facts = RM smult_closed
```
```   122   from facts have "(\<ominus>a) \<odot>\<^sub>2 x = (\<ominus>a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
```
```   123   also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
```
```   124     by (simp add: smult_l_distr)
```
```   125   also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
```
```   126   finally show ?thesis .
```
```   127 qed
```
```   128
```
```   129 lemma (in algebra) smult_r_minus:
```
```   130   "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
```
```   131 proof -
```
```   132   assume RM: "a \<in> carrier R" "x \<in> carrier M"
```
```   133   note facts = RM smult_closed
```
```   134   from facts have "a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = (a \<odot>\<^sub>2 \<ominus>\<^sub>2x \<oplus>\<^sub>2 a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
```
```   135     by algebra
```
```   136   also from RM have "... = a \<odot>\<^sub>2 (\<ominus>\<^sub>2x \<oplus>\<^sub>2 x) \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
```
```   137     by (simp add: smult_r_distr)
```
```   138   also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
```
```   139   finally show ?thesis .
```
```   140 qed
```
```   141
```
```   142 subsection {* Every Abelian Group is a \$\mathbb{Z}\$-module *}
```
```   143
```
```   144 text {* Not finished. *}
```
```   145
```
```   146 constdefs
```
```   147   INTEG :: "int ring"
```
```   148   "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
```
```   149
```
```   150 (*
```
```   151   INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
```
```   152   "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
```
```   153     zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
```
```   154 *)
```
```   155
```
```   156 lemma cring_INTEG:
```
```   157   "cring INTEG"
```
```   158   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
```
```   159     zadd_zminus_inverse2 zadd_zmult_distrib)
```
```   160
```
```   161 end
```