src/HOL/Algebra/Module.thy
changeset 15095 63f5f4c265dd
parent 14706 71590b7733b7
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Algebra/Module.thy	Sat Jul 31 20:54:23 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Module.thy	Mon Aug 02 09:44:46 2004 +0200
     1.3 @@ -13,41 +13,41 @@
     1.4  
     1.5  locale module = cring R + abelian_group M +
     1.6    assumes smult_closed [simp, intro]:
     1.7 -      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
     1.8 +      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
     1.9      and smult_l_distr:
    1.10        "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.11 -      (a \<oplus> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 b \<odot>\<^sub>2 x"
    1.12 +      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
    1.13      and smult_r_distr:
    1.14        "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.15 -      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = a \<odot>\<^sub>2 x \<oplus>\<^sub>2 a \<odot>\<^sub>2 y"
    1.16 +      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"
    1.17      and smult_assoc1:
    1.18        "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.19 -      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.20 +      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    1.21      and smult_one [simp]:
    1.22 -      "x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
    1.23 +      "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
    1.24  
    1.25  locale algebra = module R M + cring M +
    1.26    assumes smult_assoc2:
    1.27        "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.28 -      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
    1.29 +      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    1.30  
    1.31  lemma moduleI:
    1.32    includes struct R + struct M
    1.33    assumes cring: "cring R"
    1.34      and abelian_group: "abelian_group M"
    1.35      and smult_closed:
    1.36 -      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    1.37 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
    1.38      and smult_l_distr:
    1.39        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.40 -      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.41 +      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    1.42      and smult_r_distr:
    1.43        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.44 -      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
    1.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)"
    1.46      and smult_assoc1:
    1.47        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.48 -      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.49 +      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    1.50      and smult_one:
    1.51 -      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
    1.52 +      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> 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 @@ -57,21 +57,21 @@
    1.57    assumes R_cring: "cring R"
    1.58      and M_cring: "cring M"
    1.59      and smult_closed:
    1.60 -      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
    1.61 +      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> 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 -      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.65 +      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    1.66      and smult_r_distr:
    1.67        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.68 -      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
    1.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)"
    1.70      and smult_assoc1:
    1.71        "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
    1.72 -      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
    1.73 +      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
    1.74      and smult_one:
    1.75 -      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^sub>2 x = x"
    1.76 +      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
    1.77      and smult_assoc2:
    1.78        "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
    1.79 -      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
    1.80 +      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
    1.81    shows "algebra R M"
    1.82    by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
    1.83      module_axioms.intro prems)
    1.84 @@ -93,52 +93,53 @@
    1.85  subsection {* Basic Properties of Algebras *}
    1.86  
    1.87  lemma (in algebra) smult_l_null [simp]:
    1.88 -  "x \<in> carrier M ==> \<zero> \<odot>\<^sub>2 x = \<zero>\<^sub>2"
    1.89 +  "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
    1.90  proof -
    1.91    assume M: "x \<in> carrier M"
    1.92    note facts = M smult_closed
    1.93 -  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.94 -  also from M have "... = (\<zero> \<oplus> \<zero>) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2 (\<zero> \<odot>\<^sub>2 x)"
    1.95 +  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
    1.96 +  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)"
    1.97      by (simp add: smult_l_distr del: R.l_zero R.r_zero)
    1.98 -  also from facts have "... = \<zero>\<^sub>2" by algebra
    1.99 +  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
   1.100    finally show ?thesis .
   1.101  qed
   1.102  
   1.103  lemma (in algebra) smult_r_null [simp]:
   1.104 -  "a \<in> carrier R ==> a \<odot>\<^sub>2 \<zero>\<^sub>2 = \<zero>\<^sub>2";
   1.105 +  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
   1.106  proof -
   1.107    assume R: "a \<in> carrier R"
   1.108    note facts = R smult_closed
   1.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)"
   1.110 +  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>)"
   1.111      by algebra
   1.112 -  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.113 +  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>)"
   1.114      by (simp add: smult_r_distr del: M.l_zero M.r_zero)
   1.115 -  also from facts have "... = \<zero>\<^sub>2" by algebra
   1.116 +  also from facts have "... = \<zero>\<^bsub>M\<^esub>" 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 +  "[| 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)"
   1.123  proof -
   1.124    assume RM: "a \<in> carrier R" "x \<in> carrier M"
   1.125    note facts = RM smult_closed
   1.126 -  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.127 -  also from RM have "... = (\<ominus>a \<oplus> a) \<odot>\<^sub>2 x \<oplus>\<^sub>2 \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)"
   1.128 +  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)"
   1.129 +    by algebra
   1.130 +  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)"
   1.131      by (simp add: smult_l_distr)
   1.132 -  also from facts smult_l_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   1.133 +  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   1.134    finally show ?thesis .
   1.135  qed
   1.136  
   1.137  lemma (in algebra) smult_r_minus:
   1.138 -  "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 (\<ominus>\<^sub>2x) = \<ominus>\<^sub>2 (a \<odot>\<^sub>2 x)"
   1.139 +  "[| 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)"
   1.140  proof -
   1.141    assume RM: "a \<in> carrier R" "x \<in> carrier M"
   1.142    note facts = RM smult_closed
   1.143 -  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.144 +  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)"
   1.145      by algebra
   1.146 -  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.147 +  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)"
   1.148      by (simp add: smult_r_distr)
   1.149 -  also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra
   1.150 +  also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
   1.151    finally show ?thesis .
   1.152  qed
   1.153