author | nipkow |
Sat, 23 Jun 2007 19:33:22 +0200 | |
changeset 23477 | f4b83f03cac9 |
parent 22452 | 8a86fd2a1bf0 |
child 23879 | 4776af8be741 |
permissions | -rw-r--r-- |
14593 | 1 |
(* Title: HOL/Matrix/Matrix.thy |
2 |
ID: $Id$ |
|
3 |
Author: Steven Obua |
|
4 |
*) |
|
5 |
||
17915 | 6 |
theory Matrix |
7 |
imports MatrixGeneral |
|
8 |
begin |
|
14940 | 9 |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
10 |
instance matrix :: ("{zero, lattice}") lattice |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
11 |
"inf \<equiv> combine_matrix inf" |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
12 |
"sup \<equiv> combine_matrix sup" |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
13 |
by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def) |
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
14 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
15 |
instance matrix :: ("{plus, zero}") plus |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
16 |
plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" .. |
14593 | 17 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
18 |
instance matrix :: ("{minus, zero}") minus |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
19 |
minus_matrix_def: "- A \<equiv> apply_matrix uminus A" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
20 |
diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" .. |
14940 | 21 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
22 |
instance matrix :: ("{plus, times, zero}") times |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
23 |
times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" .. |
14940 | 24 |
|
25 |
instance matrix :: (lordered_ab_group) lordered_ab_group_meet |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
26 |
abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)" |
14940 | 27 |
proof |
28 |
fix A B C :: "('a::lordered_ab_group) matrix" |
|
29 |
show "A + B + C = A + (B + C)" |
|
30 |
apply (simp add: plus_matrix_def) |
|
31 |
apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]) |
|
32 |
apply (simp_all add: add_assoc) |
|
33 |
done |
|
34 |
show "A + B = B + A" |
|
35 |
apply (simp add: plus_matrix_def) |
|
36 |
apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]) |
|
37 |
apply (simp_all add: add_commute) |
|
38 |
done |
|
39 |
show "0 + A = A" |
|
40 |
apply (simp add: plus_matrix_def) |
|
41 |
apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec]) |
|
42 |
apply (simp) |
|
43 |
done |
|
44 |
show "- A + A = 0" |
|
45 |
by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
|
46 |
show "A - B = A + - B" |
|
47 |
by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext) |
|
48 |
assume "A <= B" |
|
49 |
then show "C + A <= C + B" |
|
50 |
apply (simp add: plus_matrix_def) |
|
51 |
apply (rule le_left_combine_matrix) |
|
52 |
apply (simp_all) |
|
53 |
done |
|
54 |
qed |
|
14593 | 55 |
|
14940 | 56 |
instance matrix :: (lordered_ring) lordered_ring |
57 |
proof |
|
58 |
fix A B C :: "('a :: lordered_ring) matrix" |
|
59 |
show "A * B * C = A * (B * C)" |
|
60 |
apply (simp add: times_matrix_def) |
|
61 |
apply (rule mult_matrix_assoc) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
62 |
apply (simp_all add: associative_def ring_simps) |
14940 | 63 |
done |
64 |
show "(A + B) * C = A * C + B * C" |
|
65 |
apply (simp add: times_matrix_def plus_matrix_def) |
|
66 |
apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec]) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
67 |
apply (simp_all add: associative_def commutative_def ring_simps) |
14940 | 68 |
done |
69 |
show "A * (B + C) = A * B + A * C" |
|
70 |
apply (simp add: times_matrix_def plus_matrix_def) |
|
71 |
apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec]) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
72 |
apply (simp_all add: associative_def commutative_def ring_simps) |
14940 | 73 |
done |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
74 |
show "abs A = sup A (-A)" |
14940 | 75 |
by (simp add: abs_matrix_def) |
76 |
assume a: "A \<le> B" |
|
77 |
assume b: "0 \<le> C" |
|
78 |
from a b show "C * A \<le> C * B" |
|
79 |
apply (simp add: times_matrix_def) |
|
80 |
apply (rule le_left_mult) |
|
81 |
apply (simp_all add: add_mono mult_left_mono) |
|
82 |
done |
|
83 |
from a b show "A * C \<le> B * C" |
|
84 |
apply (simp add: times_matrix_def) |
|
85 |
apply (rule le_right_mult) |
|
86 |
apply (simp_all add: add_mono mult_right_mono) |
|
87 |
done |
|
22452
8a86fd2a1bf0
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
haftmann
parents:
22422
diff
changeset
|
88 |
qed |
14593 | 89 |
|
14940 | 90 |
lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)" |
91 |
by (simp add: plus_matrix_def) |
|
14593 | 92 |
|
14940 | 93 |
lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = |
94 |
foldseq (op +) (% k. (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))" |
|
95 |
apply (simp add: times_matrix_def) |
|
96 |
apply (simp add: Rep_mult_matrix) |
|
97 |
done |
|
14593 | 98 |
|
14940 | 99 |
lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)" |
100 |
apply (subst Rep_matrix_inject[symmetric]) |
|
14593 | 101 |
apply (rule ext)+ |
14940 | 102 |
apply (simp) |
103 |
done |
|
14593 | 104 |
|
14940 | 105 |
lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)" |
106 |
apply (subst Rep_matrix_inject[symmetric]) |
|
107 |
apply (rule ext)+ |
|
108 |
apply (simp) |
|
109 |
done |
|
14593 | 110 |
|
14940 | 111 |
lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A" |
14593 | 112 |
by (simp add: times_matrix_def mult_nrows) |
113 |
||
14940 | 114 |
lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B" |
14593 | 115 |
by (simp add: times_matrix_def mult_ncols) |
116 |
||
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
117 |
definition |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
118 |
one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
21312
diff
changeset
|
119 |
"one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)" |
14593 | 120 |
|
121 |
lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)" |
|
122 |
apply (simp add: one_matrix_def) |
|
15481 | 123 |
apply (simplesubst RepAbs_matrix) |
14593 | 124 |
apply (rule exI[of _ n], simp add: split_if)+ |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
15481
diff
changeset
|
125 |
by (simp add: split_if) |
14593 | 126 |
|
20633 | 127 |
lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _") |
14593 | 128 |
proof - |
129 |
have "?r <= n" by (simp add: nrows_le) |
|
14940 | 130 |
moreover have "n <= ?r" by (simp add:le_nrows, arith) |
14593 | 131 |
ultimately show "?r = n" by simp |
132 |
qed |
|
133 |
||
20633 | 134 |
lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _") |
14593 | 135 |
proof - |
136 |
have "?r <= n" by (simp add: ncols_le) |
|
137 |
moreover have "n <= ?r" by (simp add: le_ncols, arith) |
|
138 |
ultimately show "?r = n" by simp |
|
139 |
qed |
|
140 |
||
14940 | 141 |
lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A" |
14593 | 142 |
apply (subst Rep_matrix_inject[THEN sym]) |
143 |
apply (rule ext)+ |
|
144 |
apply (simp add: times_matrix_def Rep_mult_matrix) |
|
145 |
apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero]) |
|
146 |
apply (simp_all) |
|
147 |
by (simp add: max_def ncols) |
|
148 |
||
14940 | 149 |
lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)" |
14593 | 150 |
apply (subst Rep_matrix_inject[THEN sym]) |
151 |
apply (rule ext)+ |
|
152 |
apply (simp add: times_matrix_def Rep_mult_matrix) |
|
153 |
apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero]) |
|
154 |
apply (simp_all) |
|
155 |
by (simp add: max_def nrows) |
|
156 |
||
14940 | 157 |
lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)" |
158 |
apply (simp add: times_matrix_def) |
|
159 |
apply (subst transpose_mult_matrix) |
|
160 |
apply (simp_all add: mult_commute) |
|
161 |
done |
|
162 |
||
163 |
lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B" |
|
164 |
by (simp add: plus_matrix_def transpose_combine_matrix) |
|
165 |
||
166 |
lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B" |
|
167 |
by (simp add: diff_matrix_def transpose_combine_matrix) |
|
168 |
||
169 |
lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)" |
|
170 |
by (simp add: minus_matrix_def transpose_apply_matrix) |
|
171 |
||
172 |
constdefs |
|
173 |
right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
174 |
"right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" |
|
175 |
left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
176 |
"left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" |
|
177 |
inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" |
|
178 |
"inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)" |
|
14593 | 179 |
|
180 |
lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X" |
|
181 |
apply (insert ncols_mult[of A X], insert nrows_mult[of A X]) |
|
182 |
by (simp add: right_inverse_matrix_def) |
|
183 |
||
14940 | 184 |
lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y" |
185 |
apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) |
|
186 |
by (simp add: left_inverse_matrix_def) |
|
187 |
||
188 |
lemma left_right_inverse_matrix_unique: |
|
189 |
assumes "left_inverse_matrix A Y" "right_inverse_matrix A X" |
|
190 |
shows "X = Y" |
|
191 |
proof - |
|
192 |
have "Y = Y * one_matrix (nrows A)" |
|
193 |
apply (subst one_matrix_mult_right) |
|
194 |
apply (insert prems) |
|
195 |
by (simp_all add: left_inverse_matrix_def) |
|
196 |
also have "\<dots> = Y * (A * X)" |
|
197 |
apply (insert prems) |
|
198 |
apply (frule right_inverse_matrix_dim) |
|
199 |
by (simp add: right_inverse_matrix_def) |
|
200 |
also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc) |
|
201 |
also have "\<dots> = X" |
|
202 |
apply (insert prems) |
|
203 |
apply (frule left_inverse_matrix_dim) |
|
204 |
apply (simp_all add: left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left) |
|
205 |
done |
|
206 |
ultimately show "X = Y" by (simp) |
|
207 |
qed |
|
208 |
||
209 |
lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y" |
|
210 |
by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique) |
|
211 |
||
212 |
lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)" |
|
213 |
by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def) |
|
214 |
||
215 |
lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0" |
|
216 |
by auto |
|
217 |
||
218 |
lemma Rep_matrix_zero_imp_mult_zero: |
|
219 |
"! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0 \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)" |
|
220 |
apply (subst Rep_matrix_inject[symmetric]) |
|
221 |
apply (rule ext)+ |
|
222 |
apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero) |
|
223 |
done |
|
224 |
||
225 |
lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u" |
|
226 |
apply (simp add: plus_matrix_def) |
|
227 |
apply (rule combine_nrows) |
|
228 |
apply (simp_all) |
|
229 |
done |
|
230 |
||
231 |
lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B" |
|
232 |
apply (subst Rep_matrix_inject[symmetric]) |
|
233 |
apply (rule ext)+ |
|
234 |
apply (auto simp add: Rep_matrix_mult foldseq_zero) |
|
235 |
apply (rule_tac foldseq_zerotail[symmetric]) |
|
236 |
apply (auto simp add: nrows zero_imp_mult_zero max2) |
|
237 |
apply (rule order_trans) |
|
238 |
apply (rule ncols_move_matrix_le) |
|
239 |
apply (simp add: max1) |
|
240 |
done |
|
241 |
||
242 |
lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)" |
|
243 |
apply (subst Rep_matrix_inject[symmetric]) |
|
244 |
apply (rule ext)+ |
|
245 |
apply (auto simp add: Rep_matrix_mult foldseq_zero) |
|
246 |
apply (rule_tac foldseq_zerotail[symmetric]) |
|
247 |
apply (auto simp add: ncols zero_imp_mult_zero max1) |
|
248 |
apply (rule order_trans) |
|
249 |
apply (rule nrows_move_matrix_le) |
|
250 |
apply (simp add: max2) |
|
251 |
done |
|
252 |
||
253 |
lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group) matrix)) = (move_matrix A j i) + (move_matrix B j i)" |
|
254 |
apply (subst Rep_matrix_inject[symmetric]) |
|
255 |
apply (rule ext)+ |
|
256 |
apply (simp) |
|
257 |
done |
|
258 |
||
259 |
lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)" |
|
260 |
by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult) |
|
261 |
||
262 |
constdefs |
|
263 |
scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" |
|
264 |
"scalar_mult a m == apply_matrix (op * a) m" |
|
265 |
||
266 |
lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
267 |
by (simp add: scalar_mult_def) |
14940 | 268 |
|
269 |
lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
270 |
by (simp add: scalar_mult_def apply_matrix_add ring_simps) |
14940 | 271 |
|
272 |
lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
273 |
by (simp add: scalar_mult_def) |
14940 | 274 |
|
275 |
lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
276 |
apply (subst Rep_matrix_inject[symmetric]) |
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
277 |
apply (rule ext)+ |
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
278 |
apply (auto) |
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
279 |
done |
14940 | 280 |
|
15178 | 281 |
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)" |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
282 |
by (simp add: minus_matrix_def) |
14940 | 283 |
|
15178 | 284 |
lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)" |
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
22452
diff
changeset
|
285 |
by (simp add: abs_lattice sup_matrix_def) |
14940 | 286 |
|
14593 | 287 |
end |