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