src/HOL/Algebra/Module.thy
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 29237 e90d9d51106b
child 35849 b5522b51cb1e
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14706
71590b7733b7 tuned document;
wenzelm
parents: 14651
diff changeset
     1
(*  Title:      HOL/Algebra/Module.thy
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     2
    Author:     Clemens Ballarin, started 15 April 2003
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     3
    Copyright:  Clemens Ballarin
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     4
*)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     5
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20168
diff changeset
     6
theory Module imports Ring begin
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20168
diff changeset
     7
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
     8
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20168
diff changeset
     9
section {* Modules over an Abelian Group *}
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20168
diff changeset
    10
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 20168
diff changeset
    11
subsection {* Definitions *}
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    12
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    13
record ('a, 'b) module = "'b ring" +
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    14
  smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    15
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    16
locale module = R: cring + M: abelian_group M for M (structure) +
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    17
  assumes smult_closed [simp, intro]:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    18
      "[| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    19
    and smult_l_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    20
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    21
      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> x \<oplus>\<^bsub>M\<^esub> b \<odot>\<^bsub>M\<^esub> x"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    22
    and smult_r_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    23
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    24
      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"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    25
    and smult_assoc1:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    26
      "[| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    27
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    28
    and smult_one [simp]:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    29
      "x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    30
29237
e90d9d51106b More porting to new locales.
ballarin
parents: 28823
diff changeset
    31
locale algebra = module + cring M +
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    32
  assumes smult_assoc2:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    33
      "[| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    34
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    35
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    36
lemma moduleI:
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 16417
diff changeset
    37
  fixes R (structure) and M (structure)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    38
  assumes cring: "cring R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    39
    and abelian_group: "abelian_group M"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    40
    and smult_closed:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    41
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    42
    and smult_l_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    43
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    44
      (a \<oplus> b) \<odot>\<^bsub>M\<^esub> x = (a \<odot>\<^bsub>M\<^esub> x) \<oplus>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    45
    and smult_r_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    46
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    47
      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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    48
    and smult_assoc1:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    49
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    50
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    51
    and smult_one:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    52
      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^bsub>M\<^esub> x = x"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    53
  shows "module R M"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    54
  by (auto intro: module.intro cring.axioms abelian_group.axioms
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 20318
diff changeset
    55
    module_axioms.intro assms)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    56
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    57
lemma algebraI:
19783
82f365a14960 Improved parameter management of locales.
ballarin
parents: 16417
diff changeset
    58
  fixes R (structure) and M (structure)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    59
  assumes R_cring: "cring R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    60
    and M_cring: "cring M"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    61
    and smult_closed:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    62
      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^bsub>M\<^esub> x \<in> carrier M"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    63
    and smult_l_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    64
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    66
    and smult_r_distr:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    67
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    68
      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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    69
    and smult_assoc1:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    70
      "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    71
      (a \<otimes> b) \<odot>\<^bsub>M\<^esub> x = a \<odot>\<^bsub>M\<^esub> (b \<odot>\<^bsub>M\<^esub> x)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    72
    and smult_one:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    73
      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^bsub>M\<^esub> x = x"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    74
    and smult_assoc2:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    75
      "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
    76
      (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    77
  shows "algebra R M"
19984
29bb4659f80a Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents: 19931
diff changeset
    78
apply intro_locales
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 20318
diff changeset
    79
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    80
apply (rule module_axioms.intro)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    81
 apply (simp add: smult_closed)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    82
 apply (simp add: smult_l_distr)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    83
 apply (simp add: smult_r_distr)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    84
 apply (simp add: smult_assoc1)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    85
 apply (simp add: smult_one)
27714
27b4d7c01f8b Tuned (for the sake of a meaningless log entry).
ballarin
parents: 20318
diff changeset
    86
apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms assms)+
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    87
apply (rule algebra_axioms.intro)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    88
 apply (simp add: smult_assoc2)
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19783
diff changeset
    89
done
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    90
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    91
lemma (in algebra) R_cring:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    92
  "cring R"
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 27714
diff changeset
    93
  ..
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    94
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    95
lemma (in algebra) M_cring:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    96
  "cring M"
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 27714
diff changeset
    97
  ..
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    98
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
    99
lemma (in algebra) module:
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   100
  "module R M"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   101
  by (auto intro: moduleI R_cring is_abelian_group
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   102
    smult_l_distr smult_r_distr smult_assoc1)
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   103
14651
02b8f3bcf7fe improved notation;
wenzelm
parents: 14577
diff changeset
   104
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   105
subsection {* Basic Properties of Algebras *}
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   106
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   107
lemma (in algebra) smult_l_null [simp]:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   108
  "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   109
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   110
  assume M: "x \<in> carrier M"
20168
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   111
  note facts = M smult_closed [OF R.zero_closed]
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   112
  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
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   113
  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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   114
    by (simp add: smult_l_distr del: R.l_zero R.r_zero)
20168
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   115
  also from facts have "... = \<zero>\<^bsub>M\<^esub>" apply algebra apply algebra done
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   116
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   117
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   118
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   119
lemma (in algebra) smult_r_null [simp]:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   120
  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   121
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   122
  assume R: "a \<in> carrier R"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   123
  note facts = R smult_closed
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   124
  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>)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   125
    by algebra
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   126
  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>)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   127
    by (simp add: smult_r_distr del: M.l_zero M.r_zero)
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   128
  also from facts have "... = \<zero>\<^bsub>M\<^esub>" by algebra
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   129
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   130
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   131
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   132
lemma (in algebra) smult_l_minus:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   133
  "[| 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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   134
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   135
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
20168
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   136
  from RM have a_smult: "a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   137
  from RM have ma_smult: "\<ominus>a \<odot>\<^bsub>M\<^esub> x \<in> carrier M" by simp
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   138
  note facts = RM a_smult ma_smult
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   139
  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)"
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   140
    by algebra
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   141
  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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   142
    by (simp add: smult_l_distr)
20168
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   143
  also from facts smult_l_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)"
ed7bced29e1b Reimplemented algebra method; now controlled by attribute.
ballarin
parents: 19984
diff changeset
   144
    apply algebra apply algebra done
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   145
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   146
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   147
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   148
lemma (in algebra) smult_r_minus:
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   149
  "[| 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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   150
proof -
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   151
  assume RM: "a \<in> carrier R" "x \<in> carrier M"
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   152
  note facts = RM smult_closed
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   153
  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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   154
    by algebra
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   155
  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)"
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   156
    by (simp add: smult_r_distr)
15095
63f5f4c265dd Theories now take advantage of recent syntax improvements with (structure).
ballarin
parents: 14706
diff changeset
   157
  also from facts smult_r_null have "... = \<ominus>\<^bsub>M\<^esub>(a \<odot>\<^bsub>M\<^esub> x)" by algebra
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   158
  finally show ?thesis .
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   159
qed
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   160
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents:
diff changeset
   161
end