author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 29237  e90d9d51106b 
child 35849  b5522b51cb1e 
permissions  rwrr 
14706  1 
(* Title: HOL/Algebra/Module.thy 
13936  2 
Author: Clemens Ballarin, started 15 April 2003 
3 
Copyright: Clemens Ballarin 

4 
*) 

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  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  12 

13 
record ('a, 'b) module = "'b ring" + 

14 
smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70) 

15 

29237  16 
locale module = R: cring + M: abelian_group M for M (structure) + 
13936  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  19 
and smult_l_distr: 
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  22 
and smult_r_distr: 
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  25 
and smult_assoc1: 
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  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  30 

29237  31 
locale algebra = module + cring M + 
13936  32 
assumes smult_assoc2: 
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  35 

36 
lemma moduleI: 

19783  37 
fixes R (structure) and M (structure) 
13936  38 
assumes cring: "cring R" 
39 
and abelian_group: "abelian_group M" 

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  42 
and smult_l_distr: 
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  45 
and smult_r_distr: 
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  48 
and smult_assoc1: 
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  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  53 
shows "module R M" 
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  56 

57 
lemma algebraI: 

19783  58 
fixes R (structure) and M (structure) 
13936  59 
assumes R_cring: "cring R" 
60 
and M_cring: "cring M" 

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  63 
and smult_l_distr: 
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  66 
and smult_r_distr: 
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  69 
and smult_assoc1: 
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  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  74 
and smult_assoc2: 
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  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  90 

91 
lemma (in algebra) R_cring: 

92 
"cring R" 

28823  93 
.. 
13936  94 

95 
lemma (in algebra) M_cring: 

96 
"cring M" 

28823  97 
.. 
13936  98 

99 
lemma (in algebra) module: 

100 
"module R M" 

101 
by (auto intro: moduleI R_cring is_abelian_group 

102 
smult_l_distr smult_r_distr smult_assoc1) 

103 

14651  104 

13936  105 
subsection {* Basic Properties of Algebras *} 
106 

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  109 
proof  
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  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  116 
finally show ?thesis . 
117 
qed 

118 

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  121 
proof  
122 
assume R: "a \<in> carrier R" 

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  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  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  129 
finally show ?thesis . 
130 
qed 

131 

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  134 
proof  
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  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  145 
finally show ?thesis . 
146 
qed 

147 

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  150 
proof  
151 
assume RM: "a \<in> carrier R" "x \<in> carrier M" 

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  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  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  158 
finally show ?thesis . 
159 
qed 

160 

161 
end 