|
1 (* Title: HOL/Matrix/Matrix.thy |
|
2 ID: $Id$ |
|
3 Author: Steven Obua |
|
4 License: 2004 Technische Universität München |
|
5 *) |
|
6 |
|
7 theory Matrix=MatrixGeneral: |
|
8 |
|
9 axclass almost_matrix_element < zero, plus, times |
|
10 matrix_add_assoc: "(a+b)+c = a + (b+c)" |
|
11 matrix_add_commute: "a+b = b+a" |
|
12 |
|
13 matrix_mult_assoc: "(a*b)*c = a*(b*c)" |
|
14 matrix_mult_left_0[simp]: "0 * a = 0" |
|
15 matrix_mult_right_0[simp]: "a * 0 = 0" |
|
16 |
|
17 matrix_left_distrib: "(a+b)*c = a*c+b*c" |
|
18 matrix_right_distrib: "a*(b+c) = a*b+a*c" |
|
19 |
|
20 axclass matrix_element < almost_matrix_element |
|
21 matrix_add_0[simp]: "0+0 = 0" |
|
22 |
|
23 instance matrix :: (plus) plus |
|
24 by (intro_classes) |
|
25 |
|
26 instance matrix :: (times) times |
|
27 by (intro_classes) |
|
28 |
|
29 defs (overloaded) |
|
30 plus_matrix_def: "A + B == combine_matrix (op +) A B" |
|
31 times_matrix_def: "A * B == mult_matrix (op *) (op +) A B" |
|
32 |
|
33 instance matrix :: (matrix_element) matrix_element |
|
34 proof - |
|
35 note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec] |
|
36 { |
|
37 fix A::"('a::matrix_element) matrix" |
|
38 fix B |
|
39 fix C |
|
40 have "(A + B) + C = A + (B + C)" |
|
41 apply (simp add: plus_matrix_def) |
|
42 apply (rule combine_matrix_assoc2) |
|
43 by (simp_all add: matrix_add_assoc) |
|
44 } |
|
45 note plus_assoc = this |
|
46 { |
|
47 fix A::"('a::matrix_element) matrix" |
|
48 fix B |
|
49 fix C |
|
50 have "(A * B) * C = A * (B * C)" |
|
51 apply (simp add: times_matrix_def) |
|
52 apply (rule mult_matrix_assoc_simple) |
|
53 apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def) |
|
54 apply (auto) |
|
55 apply (simp_all add: matrix_add_assoc) |
|
56 apply (simp_all add: matrix_add_commute) |
|
57 apply (simp_all add: matrix_mult_assoc) |
|
58 by (simp_all add: matrix_left_distrib matrix_right_distrib) |
|
59 } |
|
60 note mult_assoc = this |
|
61 note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec] |
|
62 { |
|
63 fix A::"('a::matrix_element) matrix" |
|
64 fix B |
|
65 have "A + B = B + A" |
|
66 apply (simp add: plus_matrix_def) |
|
67 apply (insert combine_matrix_commute2[of "op +"]) |
|
68 apply (rule combine_matrix_commute2) |
|
69 by (simp add: matrix_add_commute) |
|
70 } |
|
71 note plus_commute = this |
|
72 have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0" |
|
73 apply (simp add: plus_matrix_def) |
|
74 apply (rule combine_matrix_zero) |
|
75 by (simp) |
|
76 have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def) |
|
77 have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def) |
|
78 note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec] |
|
79 { |
|
80 fix A::"('a::matrix_element) matrix" |
|
81 fix B |
|
82 fix C |
|
83 have "(A + B) * C = A * C + B * C" |
|
84 apply (simp add: plus_matrix_def) |
|
85 apply (simp add: times_matrix_def) |
|
86 apply (rule l_distributive_matrix2) |
|
87 apply (simp_all add: associative_def commutative_def l_distributive_def) |
|
88 apply (auto) |
|
89 apply (simp_all add: matrix_add_assoc) |
|
90 apply (simp_all add: matrix_add_commute) |
|
91 by (simp_all add: matrix_left_distrib) |
|
92 } |
|
93 note left_distrib = this |
|
94 note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec] |
|
95 { |
|
96 fix A::"('a::matrix_element) matrix" |
|
97 fix B |
|
98 fix C |
|
99 have "C * (A + B) = C * A + C * B" |
|
100 apply (simp add: plus_matrix_def) |
|
101 apply (simp add: times_matrix_def) |
|
102 apply (rule r_distributive_matrix2) |
|
103 apply (simp_all add: associative_def commutative_def r_distributive_def) |
|
104 apply (auto) |
|
105 apply (simp_all add: matrix_add_assoc) |
|
106 apply (simp_all add: matrix_add_commute) |
|
107 by (simp_all add: matrix_right_distrib) |
|
108 } |
|
109 note right_distrib = this |
|
110 show "OFCLASS('a matrix, matrix_element_class)" |
|
111 apply (intro_classes) |
|
112 apply (simp_all add: plus_assoc) |
|
113 apply (simp_all add: plus_commute) |
|
114 apply (simp_all add: plus_zero) |
|
115 apply (simp_all add: mult_assoc) |
|
116 apply (simp_all add: mult_left_zero mult_right_zero) |
|
117 by (simp_all add: left_distrib right_distrib) |
|
118 qed |
|
119 |
|
120 axclass g_almost_semiring < almost_matrix_element |
|
121 g_add_left_0[simp]: "0 + a = a" |
|
122 |
|
123 lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a" |
|
124 by (simp add: matrix_add_commute) |
|
125 |
|
126 axclass g_semiring < g_almost_semiring |
|
127 g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c" |
|
128 |
|
129 instance g_almost_semiring < matrix_element |
|
130 by (intro_classes, simp) |
|
131 |
|
132 instance semiring < g_semiring |
|
133 apply (intro_classes) |
|
134 apply (simp_all add: add_ac) |
|
135 by (simp_all add: mult_assoc left_distrib right_distrib) |
|
136 |
|
137 instance matrix :: (g_almost_semiring) g_almost_semiring |
|
138 apply (intro_classes) |
|
139 by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def) |
|
140 |
|
141 lemma RepAbs_matrix_eq_left: " Rep_matrix(Abs_matrix f) = g \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> f = g" |
|
142 by (simp add: RepAbs_matrix) |
|
143 |
|
144 lemma RepAbs_matrix_eq_right: "g = Rep_matrix(Abs_matrix f) \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> g = f" |
|
145 by (simp add: RepAbs_matrix) |
|
146 |
|
147 instance matrix :: (g_semiring) g_semiring |
|
148 apply (intro_classes) |
|
149 apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def) |
|
150 apply (subst Rep_matrix_inject[THEN sym]) |
|
151 apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"]) |
|
152 apply (drule RepAbs_matrix_eq_left) |
|
153 apply (auto) |
|
154 apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le) |
|
155 apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le) |
|
156 apply (drule RepAbs_matrix_eq_right) |
|
157 apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le) |
|
158 apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le) |
|
159 apply (rule ext)+ |
|
160 apply (drule_tac x="x" and y="x" in comb, simp) |
|
161 apply (drule_tac x="xa" and y="xa" in comb, simp) |
|
162 apply (drule g_add_leftimp_eq) |
|
163 by simp |
|
164 |
|
165 axclass pordered_matrix_element < matrix_element, order, zero |
|
166 pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c" |
|
167 pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b" |
|
168 pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c" |
|
169 |
|
170 lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b" |
|
171 apply (insert pordered_add_right_mono[of a b c]) |
|
172 by (simp add: matrix_add_commute) |
|
173 |
|
174 lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d" |
|
175 proof - |
|
176 assume p1:"a <= b" |
|
177 assume p2:"c <= d" |
|
178 have "a+c <= b+c" by (rule pordered_add_right_mono) |
|
179 also have "\<dots> <= b+d" by (rule pordered_add_left_mono) |
|
180 ultimately show "a+c <= b+d" by simp |
|
181 qed |
|
182 |
|
183 instance matrix :: (pordered_matrix_element) pordered_matrix_element |
|
184 apply (intro_classes) |
|
185 apply (simp_all add: plus_matrix_def times_matrix_def) |
|
186 apply (rule le_combine_matrix) |
|
187 apply (simp_all) |
|
188 apply (simp_all add: pordered_add) |
|
189 apply (rule le_left_mult) |
|
190 apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0) |
|
191 apply (rule le_right_mult) |
|
192 by (simp_all add: pordered_add pordered_mult_right) |
|
193 |
|
194 axclass pordered_g_semiring < g_semiring, pordered_matrix_element |
|
195 |
|
196 instance almost_ordered_semiring < pordered_g_semiring |
|
197 apply (intro_classes) |
|
198 by (simp_all add: add_right_mono mult_right_mono mult_left_mono) |
|
199 |
|
200 instance matrix :: (pordered_g_semiring) pordered_g_semiring |
|
201 by (intro_classes) |
|
202 |
|
203 lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A" |
|
204 by (simp add: times_matrix_def mult_nrows) |
|
205 |
|
206 lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B" |
|
207 by (simp add: times_matrix_def mult_ncols) |
|
208 |
|
209 constdefs |
|
210 one_matrix :: "nat \<Rightarrow> ('a::semiring) matrix" |
|
211 "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)" |
|
212 |
|
213 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)" |
|
214 apply (simp add: one_matrix_def) |
|
215 apply (subst RepAbs_matrix) |
|
216 apply (rule exI[of _ n], simp add: split_if)+ |
|
217 by (simp add: split_if, arith) |
|
218 |
|
219 lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _") |
|
220 proof - |
|
221 have "?r <= n" by (simp add: nrows_le) |
|
222 moreover have "n <= ?r" by (simp add: le_nrows, arith) |
|
223 ultimately show "?r = n" by simp |
|
224 qed |
|
225 |
|
226 lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _") |
|
227 proof - |
|
228 have "?r <= n" by (simp add: ncols_le) |
|
229 moreover have "n <= ?r" by (simp add: le_ncols, arith) |
|
230 ultimately show "?r = n" by simp |
|
231 qed |
|
232 |
|
233 lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A" |
|
234 apply (subst Rep_matrix_inject[THEN sym]) |
|
235 apply (rule ext)+ |
|
236 apply (simp add: times_matrix_def Rep_mult_matrix) |
|
237 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
|
238 apply (simp_all) |
|
239 by (simp add: max_def ncols) |
|
240 |
|
241 lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A" |
|
242 apply (subst Rep_matrix_inject[THEN sym]) |
|
243 apply (rule ext)+ |
|
244 apply (simp add: times_matrix_def Rep_mult_matrix) |
|
245 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
|
246 apply (simp_all) |
|
247 by (simp add: max_def nrows) |
|
248 |
|
249 constdefs |
|
250 right_inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
251 "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))" |
|
252 inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
253 "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)" |
|
254 |
|
255 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X" |
|
256 apply (insert ncols_mult[of A X], insert nrows_mult[of A X]) |
|
257 by (simp add: right_inverse_matrix_def) |
|
258 |
|
259 (* to be continued \<dots> *) |
|
260 |
|
261 end |
|
262 |
|
263 |
|
264 |
|
265 |
|
266 |
|
267 |
|
268 |
|
269 |
|
270 |
|
271 |
|
272 |
|
273 |
|
274 |
|
275 |
|
276 |
|
277 |
|
278 |
|
279 |
|
280 |
|
281 |
|
282 |
|
283 |