src/HOL/Matrix/Matrix.thy
 author obua Fri Sep 03 17:10:36 2004 +0200 (2004-09-03) changeset 15178 5f621aa35c25 parent 14940 b9ab8babd8b3 child 15481 fc075ae929e4 permissions -rw-r--r--
Matrix theory, linear programming
1 (*  Title:      HOL/Matrix/Matrix.thy
2     ID:         \$Id\$
3     Author:     Steven Obua
4 *)
6 theory Matrix=MatrixGeneral:
8 instance matrix :: (minus) minus
9 by intro_classes
11 instance matrix :: (plus) plus
12 by (intro_classes)
14 instance matrix :: ("{plus,times}") times
15 by (intro_classes)
18   plus_matrix_def: "A + B == combine_matrix (op +) A B"
19   diff_matrix_def: "A - B == combine_matrix (op -) A B"
20   minus_matrix_def: "- A == apply_matrix uminus A"
21   times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
23 lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
24   by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
26 lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
27   by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
29 instance matrix :: (lordered_ab_group) lordered_ab_group_meet
30 proof
31   fix A B C :: "('a::lordered_ab_group) matrix"
32   show "A + B + C = A + (B + C)"
34     apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
36     done
37   show "A + B = B + A"
39     apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
41     done
42   show "0 + A = A"
44     apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
45     apply (simp)
46     done
47   show "- A + A = 0"
48     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
49   show "A - B = A + - B"
50     by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
51   show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
52     by (auto intro: is_meet_combine_matrix_meet)
53   assume "A <= B"
54   then show "C + A <= C + B"
56     apply (rule le_left_combine_matrix)
57     apply (simp_all)
58     done
59 qed
62   abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
64 instance matrix :: (lordered_ring) lordered_ring
65 proof
66   fix A B C :: "('a :: lordered_ring) matrix"
67   show "A * B * C = A * (B * C)"
69     apply (rule mult_matrix_assoc)
70     apply (simp_all add: associative_def ring_eq_simps)
71     done
72   show "(A + B) * C = A * C + B * C"
73     apply (simp add: times_matrix_def plus_matrix_def)
74     apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
75     apply (simp_all add: associative_def commutative_def ring_eq_simps)
76     done
77   show "A * (B + C) = A * B + A * C"
78     apply (simp add: times_matrix_def plus_matrix_def)
79     apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
80     apply (simp_all add: associative_def commutative_def ring_eq_simps)
81     done
82   show "abs A = join A (-A)"
84   assume a: "A \<le> B"
85   assume b: "0 \<le> C"
86   from a b show "C * A \<le> C * B"
88     apply (rule le_left_mult)
90     done
91   from a b show "A * C \<le> B * C"
93     apply (rule le_right_mult)
95     done
96 qed
98 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)"
101 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i =
102   foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
105 done
108 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)"
109 apply (subst Rep_matrix_inject[symmetric])
110 apply (rule ext)+
111 apply (simp)
112 done
114 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
115 apply (subst Rep_matrix_inject[symmetric])
116 apply (rule ext)+
117 apply (simp)
118 done
120 lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
121 by (simp add: times_matrix_def mult_nrows)
123 lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
124 by (simp add: times_matrix_def mult_ncols)
126 constdefs
127   one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
128   "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
130 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
132 apply (subst RepAbs_matrix)
133 apply (rule exI[of _ n], simp add: split_if)+
134 by (simp add: split_if, arith)
136 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
137 proof -
138   have "?r <= n" by (simp add: nrows_le)
139   moreover have "n <= ?r" by (simp add:le_nrows, arith)
140   ultimately show "?r = n" by simp
141 qed
143 lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
144 proof -
145   have "?r <= n" by (simp add: ncols_le)
146   moreover have "n <= ?r" by (simp add: le_ncols, arith)
147   ultimately show "?r = n" by simp
148 qed
150 lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
151 apply (subst Rep_matrix_inject[THEN sym])
152 apply (rule ext)+
153 apply (simp add: times_matrix_def Rep_mult_matrix)
154 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
155 apply (simp_all)
156 by (simp add: max_def ncols)
158 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
159 apply (subst Rep_matrix_inject[THEN sym])
160 apply (rule ext)+
161 apply (simp add: times_matrix_def Rep_mult_matrix)
162 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
163 apply (simp_all)
164 by (simp add: max_def nrows)
166 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
168 apply (subst transpose_mult_matrix)
170 done
172 lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
173 by (simp add: plus_matrix_def transpose_combine_matrix)
175 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
176 by (simp add: diff_matrix_def transpose_combine_matrix)
178 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
179 by (simp add: minus_matrix_def transpose_apply_matrix)
181 constdefs
182   right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
183   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A"
184   left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
185   "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A"
186   inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
187   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
189 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
190 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
193 lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
194 apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A])
197 lemma left_right_inverse_matrix_unique:
198   assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
199   shows "X = Y"
200 proof -
201   have "Y = Y * one_matrix (nrows A)"
202     apply (subst one_matrix_mult_right)
203     apply (insert prems)
205   also have "\<dots> = Y * (A * X)"
206     apply (insert prems)
207     apply (frule right_inverse_matrix_dim)
209   also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
210   also have "\<dots> = X"
211     apply (insert prems)
212     apply (frule left_inverse_matrix_dim)
213     apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
214     done
215   ultimately show "X = Y" by (simp)
216 qed
218 lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
219   by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
221 lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
222   by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
224 lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
225 by auto
227 lemma Rep_matrix_zero_imp_mult_zero:
228   "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
229 apply (subst Rep_matrix_inject[symmetric])
230 apply (rule ext)+
231 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
232 done
234 lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
236 apply (rule combine_nrows)
237 apply (simp_all)
238 done
240 lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
241 apply (subst Rep_matrix_inject[symmetric])
242 apply (rule ext)+
243 apply (auto simp add: Rep_matrix_mult foldseq_zero)
244 apply (rule_tac foldseq_zerotail[symmetric])
245 apply (auto simp add: nrows zero_imp_mult_zero max2)
246 apply (rule order_trans)
247 apply (rule ncols_move_matrix_le)
249 done
251 lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
252 apply (subst Rep_matrix_inject[symmetric])
253 apply (rule ext)+
254 apply (auto simp add: Rep_matrix_mult foldseq_zero)
255 apply (rule_tac foldseq_zerotail[symmetric])
256 apply (auto simp add: ncols zero_imp_mult_zero max1)
257 apply (rule order_trans)
258 apply (rule nrows_move_matrix_le)
260 done
262 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)"
263 apply (subst Rep_matrix_inject[symmetric])
264 apply (rule ext)+
265 apply (simp)
266 done
268 lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
269 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
271 constdefs
272   scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
273   "scalar_mult a m == apply_matrix (op * a) m"
275 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"
278 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
281 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)"
284 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
285   apply (subst Rep_matrix_inject[symmetric])
286   apply (rule ext)+
287   apply (auto)
288   done
290 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"