src/HOL/Algebra/Module.thy
changeset 13936 d3671b878828
child 13940 c67798653056
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/Module.thy	Wed Apr 30 10:01:35 2003 +0200
     1.3 @@ -0,0 +1,161 @@
     1.4 +(*  Title:      HOL/Algebra/Module
     1.5 +    ID:         $Id$
     1.6 +    Author:     Clemens Ballarin, started 15 April 2003
     1.7 +    Copyright:  Clemens Ballarin
     1.8 +*)
     1.9 +
    1.10 +theory Module = CRing:
    1.11 +
    1.12 +section {* Modules over an Abelian Group *}
    1.13 +
    1.14 +record ('a, 'b) module = "'b ring" +
    1.15 +  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
    1.16 +
    1.17 +locale module = cring R + abelian_group M +
    1.18 +  assumes smult_closed [simp, intro]:
    1.19 +      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    1.20 +    and smult_l_distr:
    1.21 +      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.22 +      (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
    1.23 +    and smult_r_distr:
    1.24 +      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.25 +      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
    1.26 +    and smult_assoc1:
    1.27 +      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.28 +      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.29 +    and smult_one [simp]:
    1.30 +      "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
    1.31 +
    1.32 +locale algebra = module R M + cring M +
    1.33 +  assumes smult_assoc2:
    1.34 +      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.35 +      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
    1.36 +
    1.37 +lemma moduleI:
    1.38 +  assumes cring: "cring R"
    1.39 +    and abelian_group: "abelian_group M"
    1.40 +    and smult_closed:
    1.41 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    1.42 +    and smult_l_distr:
    1.43 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.44 +      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    1.45 +    and smult_r_distr:
    1.46 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.47 +      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    1.48 +    and smult_assoc1:
    1.49 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.50 +      smult M (mult R a b) x = smult M a (smult M b x)"
    1.51 +    and smult_one:
    1.52 +      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    1.53 +  shows "module R M"
    1.54 +  by (auto intro: module.intro cring.axioms abelian_group.axioms
    1.55 +    module_axioms.intro prems)
    1.56 +
    1.57 +lemma algebraI:
    1.58 +  assumes R_cring: "cring R"
    1.59 +    and M_cring: "cring M"
    1.60 +    and smult_closed:
    1.61 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
    1.62 +    and smult_l_distr:
    1.63 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.64 +      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
    1.65 +    and smult_r_distr:
    1.66 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.67 +      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
    1.68 +    and smult_assoc1:
    1.69 +      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.70 +      smult M (mult R a b) x = smult M a (smult M b x)"
    1.71 +    and smult_one:
    1.72 +      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
    1.73 +    and smult_assoc2:
    1.74 +      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.75 +      mult M (smult M a x) y = smult M a (mult M x y)"
    1.76 +  shows "algebra R M"
    1.77 +  by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
    1.78 +    module_axioms.intro prems)
    1.79 +
    1.80 +lemma (in algebra) R_cring:
    1.81 +  "cring R"
    1.82 +  by (rule cring.intro) assumption+
    1.83 +
    1.84 +lemma (in algebra) M_cring:
    1.85 +  "cring M"
    1.86 +  by (rule cring.intro) assumption+
    1.87 +
    1.88 +lemma (in algebra) module:
    1.89 +  "module R M"
    1.90 +  by (auto intro: moduleI R_cring is_abelian_group
    1.91 +    smult_l_distr smult_r_distr smult_assoc1)
    1.92 +
    1.93 +subsection {* Basic Properties of Algebras *}
    1.94 +
    1.95 +lemma (in algebra) smult_l_null [simp]:
    1.96 +  "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
    1.97 +proof -
    1.98 +  assume M: "x \<in> carrier M"
    1.99 +  note facts = M smult_closed
   1.100 +  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
   1.101 +  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
   1.102 +    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
   1.103 +  also from facts have "... = \<zero>\<^sub>2" by algebra
   1.104 +  finally show ?thesis .
   1.105 +qed
   1.106 +
   1.107 +lemma (in algebra) smult_r_null [simp]:
   1.108 +  "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
   1.109 +proof -
   1.110 +  assume R: "a \<in> carrier R"
   1.111 +  note facts = R smult_closed
   1.112 +  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)"
   1.113 +    by algebra
   1.114 +  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)"
   1.115 +    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
   1.116 +  also from facts have "... = \<zero>\<^sub>2" by algebra
   1.117 +  finally show ?thesis .
   1.118 +qed
   1.119 +
   1.120 +lemma (in algebra) smult_l_minus:
   1.121 +  "[| a \<in> carrier R; x \<in> carrier M |] ==> (\<ominus>a) \<odot>\<^sub>2 x = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
   1.122 +proof -
   1.123 +  assume RM: "a \<in> carrier R" "x \<in> carrier M"
   1.124 +  note facts = RM smult_closed
   1.125 +  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
   1.126 +  also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
   1.127 +    by (simp add: smult_l_distr)
   1.128 +  also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   1.129 +  finally show ?thesis .
   1.130 +qed
   1.131 +
   1.132 +lemma (in algebra) smult_r_minus:
   1.133 +  "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
   1.134 +proof -
   1.135 +  assume RM: "a \<in> carrier R" "x \<in> carrier M"
   1.136 +  note facts = RM smult_closed
   1.137 +  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)"
   1.138 +    by algebra
   1.139 +  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)"
   1.140 +    by (simp add: smult_r_distr)
   1.141 +  also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   1.142 +  finally show ?thesis .
   1.143 +qed
   1.144 +
   1.145 +subsection {* Every Abelian Group is a $\mathbb{Z}$-module *}
   1.146 +
   1.147 +text {* Not finished. *}
   1.148 +
   1.149 +constdefs
   1.150 +  INTEG :: "int ring"
   1.151 +  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
   1.152 +
   1.153 +(*
   1.154 +  INTEG_MODULE :: "('a, 'm) ring_scheme => (int, 'a) module"
   1.155 +  "INTEG_MODULE R == (| carrier = carrier R, mult = mult R, one = one R,
   1.156 +    zero = zero R, add = add R, smult = (%n. %x:carrier R. ... ) |)"
   1.157 +*)
   1.158 +
   1.159 +lemma cring_INTEG:
   1.160 +  "cring INTEG"
   1.161 +  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
   1.162 +    zadd_zminus_inverse2 zadd_zmult_distrib)
   1.163 +
   1.164 +end