14593
|
1 |
(* Title: HOL/Matrix/MatrixGeneral.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Steven Obua
|
14654
|
4 |
License: 2004 Technische UniversitÃ\<currency>t MÃ\<onequarter>nchen
|
14593
|
5 |
*)
|
|
6 |
|
|
7 |
theory MatrixGeneral = Main:
|
|
8 |
|
|
9 |
types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
|
|
10 |
|
|
11 |
constdefs
|
|
12 |
nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set"
|
|
13 |
"nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}"
|
|
14 |
|
|
15 |
typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}"
|
|
16 |
apply (rule_tac x="(% j i. 0)" in exI)
|
|
17 |
by (simp add: nonzero_positions_def)
|
|
18 |
|
|
19 |
declare Rep_matrix_inverse[simp]
|
|
20 |
|
|
21 |
lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
|
|
22 |
apply (rule Abs_matrix_induct)
|
|
23 |
by (simp add: Abs_matrix_inverse matrix_def)
|
|
24 |
|
|
25 |
constdefs
|
|
26 |
nrows :: "('a::zero) matrix \<Rightarrow> nat"
|
|
27 |
"nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
|
|
28 |
ncols :: "('a::zero) matrix \<Rightarrow> nat"
|
|
29 |
"ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
|
|
30 |
|
|
31 |
lemma nrows:
|
|
32 |
assumes hyp: "nrows A \<le> m"
|
|
33 |
shows "(Rep_matrix A m n) = 0" (is ?concl)
|
|
34 |
proof cases
|
|
35 |
assume "nonzero_positions(Rep_matrix A) = {}"
|
|
36 |
then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
|
|
37 |
next
|
|
38 |
assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
|
|
39 |
let ?S = "fst`(nonzero_positions(Rep_matrix A))"
|
|
40 |
from a have b: "?S \<noteq> {}" by (simp)
|
|
41 |
have c: "finite (?S)" by (simp add: finite_nonzero_positions)
|
|
42 |
from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
|
|
43 |
have "m \<notin> ?S"
|
|
44 |
proof -
|
|
45 |
have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max[OF c b])
|
|
46 |
moreover from d have "~(m <= Max ?S)" by (simp)
|
|
47 |
ultimately show "m \<notin> ?S" by (auto)
|
|
48 |
qed
|
|
49 |
thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
|
|
50 |
qed
|
|
51 |
text {* \matrix cool *}
|
|
52 |
constdefs
|
|
53 |
transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
|
|
54 |
"transpose_infmatrix A j i == A i j"
|
|
55 |
transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"
|
|
56 |
"transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"
|
|
57 |
|
|
58 |
declare transpose_infmatrix_def[simp]
|
|
59 |
|
|
60 |
lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"
|
|
61 |
by ((rule ext)+, simp)
|
|
62 |
|
|
63 |
lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
|
|
64 |
apply (rule ext)+
|
|
65 |
by (simp add: transpose_infmatrix_def)
|
|
66 |
|
|
67 |
lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
|
|
68 |
apply (rule Abs_matrix_inverse)
|
|
69 |
apply (simp add: matrix_def nonzero_positions_def image_def)
|
|
70 |
proof -
|
|
71 |
let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
|
|
72 |
let ?swap = "% pos. (snd pos, fst pos)"
|
|
73 |
let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
|
|
74 |
have swap_image: "?swap`?A = ?B"
|
|
75 |
apply (simp add: image_def)
|
|
76 |
apply (rule set_ext)
|
|
77 |
apply (simp)
|
|
78 |
proof
|
|
79 |
fix y
|
|
80 |
assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
|
|
81 |
thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
|
|
82 |
proof -
|
|
83 |
from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
|
|
84 |
then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
|
|
85 |
qed
|
|
86 |
next
|
|
87 |
fix y
|
|
88 |
assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
|
|
89 |
show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" by (rule exI[of _ "snd y"], rule exI[of _ "fst y"], simp)
|
|
90 |
qed
|
|
91 |
then have "finite (?swap`?A)"
|
|
92 |
proof -
|
|
93 |
have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
|
|
94 |
then have "finite ?B" by (simp add: nonzero_positions_def)
|
|
95 |
with swap_image show "finite (?swap`?A)" by (simp)
|
|
96 |
qed
|
|
97 |
moreover
|
|
98 |
have "inj_on ?swap ?A" by (simp add: inj_on_def)
|
|
99 |
ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
|
|
100 |
qed
|
|
101 |
|
|
102 |
lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
|
|
103 |
by (simp add: transpose_matrix_def)
|
|
104 |
|
|
105 |
lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
|
|
106 |
by (simp add: transpose_matrix_def)
|
|
107 |
|
|
108 |
lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"
|
|
109 |
by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
|
|
110 |
|
|
111 |
lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"
|
|
112 |
by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
|
|
113 |
|
|
114 |
lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"
|
|
115 |
proof -
|
|
116 |
assume "ncols A <= n"
|
|
117 |
then have "nrows (transpose_matrix A) <= n" by (simp)
|
|
118 |
then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)
|
|
119 |
thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)
|
|
120 |
qed
|
|
121 |
|
|
122 |
lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
|
|
123 |
apply (auto)
|
|
124 |
apply (simp add: ncols)
|
|
125 |
proof (simp add: ncols_def, auto)
|
|
126 |
let ?P = "nonzero_positions (Rep_matrix A)"
|
|
127 |
let ?p = "snd`?P"
|
|
128 |
have a:"finite ?p" by (simp add: finite_nonzero_positions)
|
|
129 |
let ?m = "Max ?p"
|
|
130 |
assume "~(Suc (?m) <= n)"
|
|
131 |
then have b:"n <= ?m" by (simp)
|
|
132 |
fix a b
|
|
133 |
assume "(a,b) \<in> ?P"
|
|
134 |
then have "?p \<noteq> {}" by (auto)
|
|
135 |
with a have "?m \<in> ?p" by (simp)
|
|
136 |
moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
|
|
137 |
ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
|
|
138 |
moreover assume ?st
|
|
139 |
ultimately show "False" using b by (simp)
|
|
140 |
qed
|
|
141 |
|
|
142 |
lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
|
|
143 |
proof -
|
|
144 |
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
|
|
145 |
show ?concl by (simp add: a ncols_le)
|
|
146 |
qed
|
|
147 |
|
|
148 |
lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
|
|
149 |
apply (auto)
|
|
150 |
apply (subgoal_tac "ncols A <= m")
|
|
151 |
apply (simp)
|
|
152 |
apply (simp add: ncols_le)
|
|
153 |
apply (drule_tac x="ncols A" in spec)
|
|
154 |
by (simp add: ncols)
|
|
155 |
|
|
156 |
lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
|
|
157 |
proof -
|
|
158 |
have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)
|
|
159 |
also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
|
|
160 |
also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
|
|
161 |
finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
|
|
162 |
qed
|
|
163 |
|
|
164 |
lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
|
|
165 |
proof -
|
|
166 |
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
|
|
167 |
show ?concl by (simp add: a nrows_le)
|
|
168 |
qed
|
|
169 |
|
|
170 |
lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
|
|
171 |
apply (auto)
|
|
172 |
apply (subgoal_tac "nrows A <= m")
|
|
173 |
apply (simp)
|
|
174 |
apply (simp add: nrows_le)
|
|
175 |
apply (drule_tac x="nrows A" in spec)
|
|
176 |
by (simp add: nrows)
|
|
177 |
|
|
178 |
lemma finite_natarray1: "finite {x. x < (n::nat)}"
|
|
179 |
apply (induct n)
|
|
180 |
apply (simp)
|
|
181 |
proof -
|
|
182 |
fix n
|
|
183 |
have "{x. x < Suc n} = insert n {x. x < n}" by (rule set_ext, simp, arith)
|
|
184 |
moreover assume "finite {x. x < n}"
|
|
185 |
ultimately show "finite {x. x < Suc n}" by (simp)
|
|
186 |
qed
|
|
187 |
|
|
188 |
lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
|
|
189 |
apply (induct m)
|
|
190 |
apply (simp+)
|
|
191 |
proof -
|
|
192 |
fix m::nat
|
|
193 |
let ?s0 = "{pos. fst pos < m & snd pos < n}"
|
|
194 |
let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
|
|
195 |
let ?sd = "{pos. fst pos = m & snd pos < n}"
|
|
196 |
assume f0: "finite ?s0"
|
|
197 |
have f1: "finite ?sd"
|
|
198 |
proof -
|
|
199 |
let ?f = "% x. (m, x)"
|
|
200 |
have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
|
|
201 |
moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
|
|
202 |
ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
|
|
203 |
qed
|
|
204 |
have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith)
|
|
205 |
from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
|
|
206 |
with su show "finite ?s1" by (simp)
|
|
207 |
qed
|
|
208 |
|
|
209 |
lemma RepAbs_matrix:
|
|
210 |
assumes aem: "? m. ! j i. m <= j \<longrightarrow> x j i = 0" (is ?em) and aen:"? n. ! j i. (n <= i \<longrightarrow> x j i = 0)" (is ?en)
|
|
211 |
shows "(Rep_matrix (Abs_matrix x)) = x"
|
|
212 |
apply (rule Abs_matrix_inverse)
|
|
213 |
apply (simp add: matrix_def nonzero_positions_def)
|
|
214 |
proof -
|
|
215 |
from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
|
|
216 |
from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
|
|
217 |
let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
|
|
218 |
let ?v = "{pos. fst pos < m & snd pos < n}"
|
|
219 |
have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
|
|
220 |
from a b have "(?u \<inter> (-?v)) = {}"
|
|
221 |
apply (simp)
|
|
222 |
apply (rule set_ext)
|
|
223 |
apply (simp)
|
|
224 |
apply auto
|
|
225 |
by (rule c, auto)+
|
|
226 |
then have d: "?u \<subseteq> ?v" by blast
|
|
227 |
moreover have "finite ?v" by (simp add: finite_natarray2)
|
|
228 |
ultimately show "finite ?u" by (rule finite_subset)
|
|
229 |
qed
|
|
230 |
|
|
231 |
constdefs
|
|
232 |
apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
|
|
233 |
"apply_infmatrix f == % A. (% j i. f (A j i))"
|
|
234 |
apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
|
|
235 |
"apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
|
|
236 |
combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
|
|
237 |
"combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
|
|
238 |
combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
|
|
239 |
"combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
|
|
240 |
|
|
241 |
lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
|
|
242 |
by (simp add: apply_infmatrix_def)
|
|
243 |
|
|
244 |
lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
|
|
245 |
by (simp add: combine_infmatrix_def)
|
|
246 |
|
|
247 |
constdefs
|
|
248 |
commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
|
|
249 |
"commutative f == ! x y. f x y = f y x"
|
|
250 |
associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
|
|
251 |
"associative f == ! x y z. f (f x y) z = f x (f y z)"
|
|
252 |
|
|
253 |
text{*
|
|
254 |
To reason about associativity and commutativity of operations on matrices,
|
|
255 |
let's take a step back and look at the general situtation: Assume that we have
|
|
256 |
sets $A$ and $B$ with $B \subset A$ and an abstraction $u: A \rightarrow B$. This abstraction has to fulfill $u(b) = b$ for all $b \in B$, but is arbitrary otherwise.
|
|
257 |
Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.
|
|
258 |
It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$
|
|
259 |
*}
|
|
260 |
|
|
261 |
lemma combine_infmatrix_commute:
|
|
262 |
"commutative f \<Longrightarrow> commutative (combine_infmatrix f)"
|
|
263 |
by (simp add: commutative_def combine_infmatrix_def)
|
|
264 |
|
|
265 |
lemma combine_matrix_commute:
|
|
266 |
"commutative f \<Longrightarrow> commutative (combine_matrix f)"
|
|
267 |
by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
|
|
268 |
|
|
269 |
text{*
|
|
270 |
On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,
|
|
271 |
as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by $u(a) = 0$ for $a \notin B$. Then we have
|
|
272 |
\[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
|
|
273 |
but on the other hand we have
|
|
274 |
\[ f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.\]
|
|
275 |
A way out of this problem is to assume that $f(A\times A)\subset A$ holds, and this is what we are going to do:
|
|
276 |
*}
|
|
277 |
|
|
278 |
lemma nonzero_positions_combine_infmatrix[simp]: "f 0 0 = 0 \<Longrightarrow> nonzero_positions (combine_infmatrix f A B) \<subseteq> (nonzero_positions A) \<union> (nonzero_positions B)"
|
|
279 |
by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)
|
|
280 |
|
|
281 |
lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
|
|
282 |
by (insert Rep_matrix [of A], simp add: matrix_def)
|
|
283 |
|
|
284 |
lemma combine_infmatrix_closed [simp]:
|
|
285 |
"f 0 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))) = combine_infmatrix f (Rep_matrix A) (Rep_matrix B)"
|
|
286 |
apply (rule Abs_matrix_inverse)
|
|
287 |
apply (simp add: matrix_def)
|
|
288 |
apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])
|
|
289 |
by (simp_all)
|
|
290 |
|
|
291 |
text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}
|
|
292 |
lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"
|
|
293 |
by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)
|
|
294 |
|
|
295 |
lemma apply_infmatrix_closed [simp]:
|
|
296 |
"f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"
|
|
297 |
apply (rule Abs_matrix_inverse)
|
|
298 |
apply (simp add: matrix_def)
|
|
299 |
apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])
|
|
300 |
by (simp_all)
|
|
301 |
|
|
302 |
lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"
|
|
303 |
by (simp add: associative_def combine_infmatrix_def)
|
|
304 |
|
|
305 |
lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
|
|
306 |
by (auto)
|
|
307 |
|
|
308 |
lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"
|
|
309 |
apply (simp(no_asm) add: associative_def combine_matrix_def, auto)
|
|
310 |
apply (rule comb [of Abs_matrix Abs_matrix])
|
|
311 |
by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)
|
|
312 |
|
|
313 |
lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"
|
|
314 |
by (simp add: apply_matrix_def)
|
|
315 |
|
|
316 |
lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \<Longrightarrow> Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"
|
|
317 |
by(simp add: combine_matrix_def)
|
|
318 |
|
|
319 |
lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
|
|
320 |
by (simp add: nrows_le)
|
|
321 |
|
|
322 |
lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
|
|
323 |
by (simp add: ncols_le)
|
|
324 |
|
|
325 |
lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
|
|
326 |
by (simp add: nrows_le)
|
|
327 |
|
|
328 |
lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
|
|
329 |
by (simp add: ncols_le)
|
|
330 |
|
|
331 |
constdefs
|
14654
|
332 |
zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
|
14593
|
333 |
"zero_r_neutral f == ! a. f a 0 = a"
|
14654
|
334 |
zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
|
14593
|
335 |
"zero_l_neutral f == ! a. f 0 a = a"
|
|
336 |
zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
|
|
337 |
"zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
|
|
338 |
|
|
339 |
consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
|
|
340 |
primrec
|
|
341 |
"foldseq f s 0 = s 0"
|
|
342 |
"foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
|
|
343 |
|
|
344 |
consts foldseq_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
|
|
345 |
primrec
|
|
346 |
"foldseq_transposed f s 0 = s 0"
|
|
347 |
"foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
|
|
348 |
|
|
349 |
lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
|
|
350 |
proof -
|
|
351 |
assume a:"associative f"
|
|
352 |
then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
|
|
353 |
proof -
|
|
354 |
fix n
|
|
355 |
show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
|
|
356 |
proof (induct n)
|
|
357 |
show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
|
|
358 |
next
|
|
359 |
fix n
|
|
360 |
assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
|
|
361 |
have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
|
|
362 |
show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
|
|
363 |
proof (auto)
|
|
364 |
fix N t
|
|
365 |
assume Nsuc: "N <= Suc n"
|
|
366 |
show "foldseq f t N = foldseq_transposed f t N"
|
|
367 |
proof cases
|
|
368 |
assume "N <= n"
|
|
369 |
then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
|
|
370 |
next
|
|
371 |
assume "~(N <= n)"
|
|
372 |
with Nsuc have Nsuceq: "N = Suc n" by simp
|
|
373 |
have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
|
|
374 |
have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
|
|
375 |
show "foldseq f t N = foldseq_transposed f t N"
|
|
376 |
apply (simp add: Nsuceq)
|
|
377 |
apply (subst c)
|
|
378 |
apply (simp)
|
|
379 |
apply (case_tac "n = 0")
|
|
380 |
apply (simp)
|
|
381 |
apply (drule neqz)
|
|
382 |
apply (erule exE)
|
|
383 |
apply (simp)
|
|
384 |
apply (subst assocf)
|
|
385 |
proof -
|
|
386 |
fix m
|
|
387 |
assume "n = Suc m & Suc m <= n"
|
|
388 |
then have mless: "Suc m <= n" by arith
|
|
389 |
then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")
|
|
390 |
apply (subst c)
|
|
391 |
by simp+
|
|
392 |
have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
|
|
393 |
have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
|
|
394 |
apply (subst c)
|
|
395 |
by (simp add: mless)+
|
|
396 |
have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
|
|
397 |
from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
|
|
398 |
qed
|
|
399 |
qed
|
|
400 |
qed
|
|
401 |
qed
|
|
402 |
qed
|
|
403 |
show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
|
|
404 |
qed
|
|
405 |
|
|
406 |
lemma foldseq_distr: "\<lbrakk>associative f; commutative f\<rbrakk> \<Longrightarrow> foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"
|
|
407 |
proof -
|
|
408 |
assume assoc: "associative f"
|
|
409 |
assume comm: "commutative f"
|
|
410 |
from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)
|
|
411 |
from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)
|
|
412 |
from assoc comm have c: "!! x y z. f x (f y z) = f y (f x z)" by (simp add: commutative_def associative_def)
|
|
413 |
have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
|
|
414 |
apply (induct_tac n)
|
|
415 |
apply (simp+, auto)
|
|
416 |
by (simp add: a b c)
|
|
417 |
then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
|
|
418 |
qed
|
|
419 |
|
|
420 |
theorem "\<lbrakk>associative f; associative g; \<forall>a b c d. g (f a b) (f c d) = f (g a c) (g b d); ? x y. (f x) \<noteq> (f y); ? x y. (g x) \<noteq> (g y); f x x = x; g x x = x\<rbrakk> \<Longrightarrow> f=g | (! y. f y x = y) | (! y. g y x = y)"
|
|
421 |
oops
|
|
422 |
(* Model found
|
|
423 |
|
|
424 |
Trying to find a model that refutes: \<lbrakk>associative f; associative g;
|
|
425 |
\<forall>a b c d. g (f a b) (f c d) = f (g a c) (g b d); \<exists>x y. f x \<noteq> f y;
|
|
426 |
\<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk>
|
|
427 |
\<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y)
|
|
428 |
Searching for a model of size 1, translating term... invoking SAT solver... no model found.
|
|
429 |
Searching for a model of size 2, translating term... invoking SAT solver... no model found.
|
|
430 |
Searching for a model of size 3, translating term... invoking SAT solver...
|
|
431 |
Model found:
|
|
432 |
Size of types: 'a: 3
|
|
433 |
x: a1
|
|
434 |
g: (a0\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a0, a2\<mapsto>a1), a1\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a1, a2\<mapsto>a0), a2\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a0, a2\<mapsto>a1))
|
|
435 |
f: (a0\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0), a1\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a1, a2\<mapsto>a1), a2\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0))
|
|
436 |
*)
|
|
437 |
|
|
438 |
lemma foldseq_zero:
|
|
439 |
assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"
|
|
440 |
shows "foldseq f s n = 0"
|
|
441 |
proof -
|
|
442 |
have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
|
|
443 |
apply (induct_tac n)
|
|
444 |
apply (simp)
|
|
445 |
by (simp add: fz)
|
|
446 |
then show "foldseq f s n = 0" by (simp add: sz)
|
|
447 |
qed
|
|
448 |
|
|
449 |
lemma foldseq_significant_positions:
|
|
450 |
assumes p: "! i. i <= N \<longrightarrow> S i = T i"
|
|
451 |
shows "foldseq f S N = foldseq f T N" (is ?concl)
|
|
452 |
proof -
|
|
453 |
have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
|
|
454 |
apply (induct_tac m)
|
|
455 |
apply (simp)
|
|
456 |
apply (simp)
|
|
457 |
apply (auto)
|
|
458 |
proof -
|
|
459 |
fix n
|
|
460 |
fix s::"nat\<Rightarrow>'a"
|
|
461 |
fix t::"nat\<Rightarrow>'a"
|
|
462 |
assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
|
|
463 |
assume b: "\<forall>i\<le>Suc n. s i = t i"
|
|
464 |
have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast
|
|
465 |
have d:"!! s t. (\<forall>i\<le>n. s i = t i) \<Longrightarrow> foldseq f s n = foldseq f t n" by (simp add: a)
|
|
466 |
show "f (t 0) (foldseq f (\<lambda>k. s (Suc k)) n) = f (t 0) (foldseq f (\<lambda>k. t (Suc k)) n)" by (rule c, simp add: d b)
|
|
467 |
qed
|
|
468 |
with p show ?concl by simp
|
|
469 |
qed
|
|
470 |
|
|
471 |
lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")
|
|
472 |
proof -
|
|
473 |
have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
|
|
474 |
have suc2: "!! a b. \<lbrakk>a <= Suc b; ~ (a <= b)\<rbrakk> \<Longrightarrow> a = (Suc b)" by arith
|
|
475 |
have eq: "!! (a::nat) b. \<lbrakk>~(a < b); a <= b\<rbrakk> \<Longrightarrow> a = b" by arith
|
|
476 |
have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
|
|
477 |
have "!! n. ! m s. m <= n \<longrightarrow> foldseq f s n = foldseq f (% k. (if k < m then (s k) else (foldseq f (% k. s(k+m)) (n-m)))) m"
|
|
478 |
apply (induct_tac n)
|
|
479 |
apply (simp)
|
|
480 |
apply (simp)
|
|
481 |
apply (auto)
|
|
482 |
apply (case_tac "m = Suc na")
|
|
483 |
apply (simp)
|
|
484 |
apply (rule a)
|
|
485 |
apply (rule foldseq_significant_positions)
|
|
486 |
apply (simp, auto)
|
|
487 |
apply (drule eq, simp+)
|
|
488 |
apply (drule suc, simp+)
|
|
489 |
proof -
|
|
490 |
fix na m s
|
|
491 |
assume suba:"\<forall>m\<le>na. \<forall>s. foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m"
|
|
492 |
assume subb:"m <= na"
|
|
493 |
from suba have subc:"!! m s. m <= na \<Longrightarrow>foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m" by simp
|
|
494 |
have subd: "foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m =
|
|
495 |
foldseq f (% k. s(Suc k)) na"
|
|
496 |
by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)
|
|
497 |
from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith
|
|
498 |
show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
|
|
499 |
foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
|
|
500 |
apply (simp add: subd)
|
|
501 |
apply (case_tac "m=0")
|
|
502 |
apply (simp)
|
|
503 |
apply (drule sube)
|
|
504 |
apply (auto)
|
|
505 |
apply (rule a)
|
|
506 |
by (simp add: subc if_def)
|
|
507 |
qed
|
|
508 |
then show "?p \<Longrightarrow> ?concl" by simp
|
|
509 |
qed
|
|
510 |
|
|
511 |
lemma foldseq_zerotail:
|
|
512 |
assumes
|
|
513 |
fz: "f 0 0 = 0"
|
|
514 |
and sz: "! i. n <= i \<longrightarrow> s i = 0"
|
|
515 |
and nm: "n <= m"
|
|
516 |
shows
|
|
517 |
"foldseq f s n = foldseq f s m"
|
|
518 |
proof -
|
|
519 |
have a: "!! a b. ~(a < b) \<Longrightarrow> a <= b \<Longrightarrow> (a::nat) = b" by simp
|
|
520 |
show "foldseq f s n = foldseq f s m"
|
|
521 |
apply (simp add: foldseq_tail[OF nm, of f s])
|
|
522 |
apply (rule foldseq_significant_positions)
|
|
523 |
apply (auto)
|
|
524 |
apply (drule a)
|
|
525 |
apply (simp+)
|
|
526 |
apply (subst foldseq_zero)
|
|
527 |
by (simp add: fz sz)+
|
|
528 |
qed
|
|
529 |
|
|
530 |
lemma foldseq_zerotail2:
|
|
531 |
assumes "! x. f x 0 = x"
|
|
532 |
and "! i. n < i \<longrightarrow> s i = 0"
|
|
533 |
and nm: "n <= m"
|
|
534 |
shows
|
|
535 |
"foldseq f s n = foldseq f s m" (is ?concl)
|
|
536 |
proof -
|
|
537 |
have "f 0 0 = 0" by (simp add: prems)
|
|
538 |
have a:"!! (i::nat) m. ~(i < m) \<Longrightarrow> i <= m \<Longrightarrow> i = m" by arith
|
|
539 |
have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
|
|
540 |
have c: "0 <= m" by simp
|
|
541 |
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
|
|
542 |
show ?concl
|
|
543 |
apply (subst foldseq_tail[OF nm])
|
|
544 |
apply (rule foldseq_significant_positions)
|
|
545 |
apply (auto)
|
|
546 |
apply (case_tac "m=n")
|
|
547 |
apply (drule a, simp+)
|
|
548 |
apply (drule b[OF nm])
|
|
549 |
apply (auto)
|
|
550 |
apply (drule a)
|
|
551 |
apply simp+
|
|
552 |
apply (case_tac "k=0")
|
|
553 |
apply (simp add: prems)
|
|
554 |
apply (drule d)
|
|
555 |
apply (auto)
|
|
556 |
by (simp add: prems foldseq_zero)
|
|
557 |
qed
|
|
558 |
|
|
559 |
lemma foldseq_zerostart:
|
|
560 |
"! x. f 0 (f 0 x) = f 0 x \<Longrightarrow> ! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
|
|
561 |
proof -
|
|
562 |
assume f00x: "! x. f 0 (f 0 x) = f 0 x"
|
|
563 |
have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
|
|
564 |
apply (induct n)
|
|
565 |
apply (simp)
|
|
566 |
apply (rule allI, rule impI)
|
|
567 |
proof -
|
|
568 |
fix n
|
|
569 |
fix s
|
|
570 |
have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp
|
|
571 |
assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"
|
|
572 |
from b have c:"!! s. (\<forall>i\<le>n. s i = 0) \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
|
|
573 |
assume d: "! i. i <= Suc n \<longrightarrow> s i = 0"
|
|
574 |
show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"
|
|
575 |
apply (subst a)
|
|
576 |
apply (subst c)
|
|
577 |
by (simp add: d f00x)+
|
|
578 |
qed
|
|
579 |
then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
|
|
580 |
qed
|
|
581 |
|
|
582 |
lemma foldseq_zerostart2:
|
|
583 |
"! x. f 0 x = x \<Longrightarrow> ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
|
|
584 |
proof -
|
|
585 |
assume a:"! i. i<n \<longrightarrow> s i = 0"
|
|
586 |
assume x:"! x. f 0 x = x"
|
|
587 |
from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast
|
|
588 |
have b: "!! i l. i < Suc l = (i <= l)" by arith
|
|
589 |
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
|
|
590 |
show "foldseq f s n = s n"
|
|
591 |
apply (case_tac "n=0")
|
|
592 |
apply (simp)
|
|
593 |
apply (insert a)
|
|
594 |
apply (drule d)
|
|
595 |
apply (auto)
|
|
596 |
apply (simp add: b)
|
|
597 |
apply (insert f00x)
|
|
598 |
apply (drule foldseq_zerostart)
|
|
599 |
by (simp add: x)+
|
|
600 |
qed
|
|
601 |
|
|
602 |
lemma foldseq_almostzero:
|
|
603 |
assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
|
|
604 |
shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
|
|
605 |
proof -
|
|
606 |
from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
|
|
607 |
from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
|
|
608 |
show ?concl
|
|
609 |
apply auto
|
|
610 |
apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
|
|
611 |
apply simp
|
|
612 |
apply (subst foldseq_zerostart2)
|
|
613 |
apply (simp add: f0x a)+
|
|
614 |
apply (subst foldseq_zero)
|
|
615 |
by (simp add: s0 f0x)+
|
|
616 |
qed
|
|
617 |
|
|
618 |
lemma foldseq_distr_unary:
|
|
619 |
assumes "!! a b. g (f a b) = f (g a) (g b)"
|
|
620 |
shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
|
|
621 |
proof -
|
|
622 |
have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
|
|
623 |
apply (induct_tac n)
|
|
624 |
apply (simp)
|
|
625 |
apply (simp)
|
|
626 |
apply (auto)
|
|
627 |
apply (drule_tac x="% k. s (Suc k)" in spec)
|
|
628 |
by (simp add: prems)
|
|
629 |
then show ?concl by simp
|
|
630 |
qed
|
|
631 |
|
|
632 |
constdefs
|
|
633 |
mult_matrix_n :: "nat \<Rightarrow> (('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix"
|
|
634 |
"mult_matrix_n n fmul fadd A B == Abs_matrix(% j i. foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n)"
|
|
635 |
mult_matrix :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix"
|
|
636 |
"mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
|
|
637 |
|
|
638 |
lemma mult_matrix_n:
|
|
639 |
assumes prems: "ncols A \<le> n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
|
|
640 |
shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
|
|
641 |
proof -
|
|
642 |
show ?concl using prems
|
|
643 |
apply (simp add: mult_matrix_def mult_matrix_n_def)
|
|
644 |
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
|
|
645 |
by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
|
|
646 |
qed
|
|
647 |
|
|
648 |
lemma mult_matrix_nm:
|
|
649 |
assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
|
|
650 |
shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
|
|
651 |
proof -
|
|
652 |
from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
|
|
653 |
also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
|
|
654 |
finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
|
|
655 |
qed
|
|
656 |
|
|
657 |
constdefs
|
|
658 |
r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
|
|
659 |
"r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
|
|
660 |
l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
|
|
661 |
"l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
|
|
662 |
distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
|
|
663 |
"distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
|
|
664 |
|
|
665 |
lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
|
|
666 |
lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
|
|
667 |
|
|
668 |
lemma r_distributive_matrix:
|
|
669 |
assumes prems:
|
|
670 |
"r_distributive fmul fadd"
|
|
671 |
"associative fadd"
|
|
672 |
"commutative fadd"
|
|
673 |
"fadd 0 0 = 0"
|
|
674 |
"! a. fmul a 0 = 0"
|
|
675 |
"! a. fmul 0 a = 0"
|
|
676 |
shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
|
|
677 |
proof -
|
|
678 |
from prems show ?concl
|
|
679 |
apply (simp add: r_distributive_def mult_matrix_def, auto)
|
|
680 |
proof -
|
|
681 |
fix a::"'a matrix"
|
|
682 |
fix u::"'b matrix"
|
|
683 |
fix v::"'b matrix"
|
|
684 |
let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
|
|
685 |
from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
|
|
686 |
combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"
|
|
687 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
688 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
689 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
690 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
691 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
692 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
693 |
apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
|
|
694 |
apply (simp add: combine_matrix_def combine_infmatrix_def)
|
|
695 |
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
|
|
696 |
apply (subst RepAbs_matrix)
|
|
697 |
apply (simp, auto)
|
|
698 |
apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
|
|
699 |
apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
|
|
700 |
apply (subst RepAbs_matrix)
|
|
701 |
apply (simp, auto)
|
|
702 |
apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
|
|
703 |
apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
|
|
704 |
done
|
|
705 |
qed
|
|
706 |
qed
|
|
707 |
|
|
708 |
lemma l_distributive_matrix:
|
|
709 |
assumes prems:
|
|
710 |
"l_distributive fmul fadd"
|
|
711 |
"associative fadd"
|
|
712 |
"commutative fadd"
|
|
713 |
"fadd 0 0 = 0"
|
|
714 |
"! a. fmul a 0 = 0"
|
|
715 |
"! a. fmul 0 a = 0"
|
|
716 |
shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
|
|
717 |
proof -
|
|
718 |
from prems show ?concl
|
|
719 |
apply (simp add: l_distributive_def mult_matrix_def, auto)
|
|
720 |
proof -
|
|
721 |
fix a::"'b matrix"
|
|
722 |
fix u::"'a matrix"
|
|
723 |
fix v::"'a matrix"
|
|
724 |
let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
|
|
725 |
from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
|
|
726 |
combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"
|
|
727 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
728 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
729 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
730 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
731 |
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
|
|
732 |
apply (simp add: max1 max2 combine_nrows combine_ncols)+
|
|
733 |
apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
|
|
734 |
apply (simp add: combine_matrix_def combine_infmatrix_def)
|
|
735 |
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
|
|
736 |
apply (subst RepAbs_matrix)
|
|
737 |
apply (simp, auto)
|
|
738 |
apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
|
|
739 |
apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
|
|
740 |
apply (subst RepAbs_matrix)
|
|
741 |
apply (simp, auto)
|
|
742 |
apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
|
|
743 |
apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
|
|
744 |
done
|
|
745 |
qed
|
|
746 |
qed
|
|
747 |
|
|
748 |
|
|
749 |
instance matrix :: (zero)zero by intro_classes
|
|
750 |
|
|
751 |
defs(overloaded)
|
|
752 |
zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
|
|
753 |
|
|
754 |
lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
|
|
755 |
apply (simp add: zero_matrix_def)
|
|
756 |
apply (subst RepAbs_matrix)
|
|
757 |
by (auto)
|
|
758 |
|
|
759 |
lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
|
|
760 |
proof -
|
|
761 |
have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
|
|
762 |
show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
|
|
763 |
qed
|
|
764 |
|
|
765 |
lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
|
|
766 |
proof -
|
|
767 |
have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
|
|
768 |
show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
|
|
769 |
qed
|
|
770 |
|
|
771 |
lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
|
|
772 |
by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
|
|
773 |
|
|
774 |
lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
|
|
775 |
apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
|
|
776 |
apply (auto)
|
|
777 |
by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
|
|
778 |
|
|
779 |
lemma mult_matrix_n_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd A 0 = 0"
|
|
780 |
apply (simp add: mult_matrix_n_def)
|
|
781 |
apply (subst foldseq_zero)
|
|
782 |
by (simp_all add: zero_matrix_def)
|
|
783 |
|
|
784 |
lemma mult_matrix_n_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd 0 A = 0"
|
|
785 |
apply (simp add: mult_matrix_n_def)
|
|
786 |
apply (subst foldseq_zero)
|
|
787 |
by (simp_all add: zero_matrix_def)
|
|
788 |
|
|
789 |
lemma mult_matrix_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd 0 A = 0"
|
|
790 |
by (simp add: mult_matrix_def)
|
|
791 |
|
|
792 |
lemma mult_matrix_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd A 0 = 0"
|
|
793 |
by (simp add: mult_matrix_def)
|
|
794 |
|
|
795 |
lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"
|
|
796 |
apply (simp add: apply_matrix_def apply_infmatrix_def)
|
|
797 |
by (simp add: zero_matrix_def)
|
|
798 |
|
|
799 |
lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"
|
|
800 |
apply (simp add: combine_matrix_def combine_infmatrix_def)
|
|
801 |
by (simp add: zero_matrix_def)
|
|
802 |
|
|
803 |
lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
|
|
804 |
apply (simp add: apply_matrix_def apply_infmatrix_def)
|
|
805 |
by (simp add: zero_matrix_def)
|
|
806 |
|
|
807 |
constdefs
|
|
808 |
singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"
|
|
809 |
"singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
|
|
810 |
move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"
|
|
811 |
"move_matrix A y x == Abs_matrix(% j i. if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
|
|
812 |
take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
|
|
813 |
"take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
|
|
814 |
take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
|
|
815 |
"take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
|
|
816 |
|
|
817 |
constdefs
|
|
818 |
column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
|
|
819 |
"column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
|
|
820 |
row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
|
|
821 |
"row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
|
|
822 |
|
|
823 |
lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
|
|
824 |
apply (simp add: singleton_matrix_def)
|
|
825 |
apply (auto)
|
|
826 |
apply (subst RepAbs_matrix)
|
|
827 |
apply (rule exI[of _ "Suc m"], simp)
|
|
828 |
apply (rule exI[of _ "Suc n"], simp+)
|
|
829 |
by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
|
|
830 |
|
|
831 |
lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
|
|
832 |
by (simp add: singleton_matrix_def zero_matrix_def)
|
|
833 |
|
|
834 |
lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
|
|
835 |
apply (auto)
|
|
836 |
apply (rule le_anti_sym)
|
|
837 |
apply (subst nrows_le)
|
|
838 |
apply (simp add: singleton_matrix_def, auto)
|
|
839 |
apply (subst RepAbs_matrix)
|
|
840 |
apply (simp, arith)
|
|
841 |
apply (simp, arith)
|
|
842 |
apply (simp)
|
|
843 |
apply (simp add: Suc_le_eq)
|
|
844 |
apply (rule not_leE)
|
|
845 |
apply (subst nrows_le)
|
|
846 |
by simp
|
|
847 |
|
|
848 |
lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
|
|
849 |
apply (auto)
|
|
850 |
apply (rule le_anti_sym)
|
|
851 |
apply (subst ncols_le)
|
|
852 |
apply (simp add: singleton_matrix_def, auto)
|
|
853 |
apply (subst RepAbs_matrix)
|
|
854 |
apply (simp, arith)
|
|
855 |
apply (simp, arith)
|
|
856 |
apply (simp)
|
|
857 |
apply (simp add: Suc_le_eq)
|
|
858 |
apply (rule not_leE)
|
|
859 |
apply (subst ncols_le)
|
|
860 |
by simp
|
|
861 |
|
|
862 |
lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"
|
|
863 |
apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
|
|
864 |
apply (subst RepAbs_matrix)
|
|
865 |
apply (rule exI[of _ "Suc j"], simp)
|
|
866 |
apply (rule exI[of _ "Suc i"], simp)
|
|
867 |
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
|
|
868 |
apply (subst RepAbs_matrix)
|
|
869 |
apply (rule exI[of _ "Suc j"], simp)
|
|
870 |
apply (rule exI[of _ "Suc i"], simp)
|
|
871 |
by simp
|
|
872 |
|
|
873 |
lemma Rep_move_matrix[simp]:
|
|
874 |
"Rep_matrix (move_matrix A y x) j i =
|
|
875 |
(if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
|
|
876 |
apply (simp add: move_matrix_def)
|
|
877 |
apply (auto)
|
|
878 |
by (subst RepAbs_matrix,
|
|
879 |
rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
|
|
880 |
rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
|
|
881 |
|
|
882 |
lemma Rep_take_columns[simp]:
|
|
883 |
"Rep_matrix (take_columns A c) j i =
|
|
884 |
(if i < c then (Rep_matrix A j i) else 0)"
|
|
885 |
apply (simp add: take_columns_def)
|
|
886 |
apply (subst RepAbs_matrix)
|
|
887 |
apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
|
|
888 |
apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
|
|
889 |
done
|
|
890 |
|
|
891 |
lemma Rep_take_rows[simp]:
|
|
892 |
"Rep_matrix (take_rows A r) j i =
|
|
893 |
(if j < r then (Rep_matrix A j i) else 0)"
|
|
894 |
apply (simp add: take_rows_def)
|
|
895 |
apply (subst RepAbs_matrix)
|
|
896 |
apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
|
|
897 |
apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
|
|
898 |
done
|
|
899 |
|
|
900 |
lemma Rep_column_of_matrix[simp]:
|
|
901 |
"Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"
|
|
902 |
by (simp add: column_of_matrix_def)
|
|
903 |
|
|
904 |
lemma Rep_row_of_matrix[simp]:
|
|
905 |
"Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
|
|
906 |
by (simp add: row_of_matrix_def)
|
|
907 |
|
|
908 |
lemma mult_matrix_singleton_right[simp]:
|
|
909 |
assumes prems:
|
|
910 |
"! x. fmul x 0 = 0"
|
|
911 |
"! x. fmul 0 x = 0"
|
|
912 |
"! x. fadd 0 x = x"
|
|
913 |
"! x. fadd x 0 = x"
|
|
914 |
shows "(mult_matrix fmul fadd A (singleton_matrix j i e)) = apply_matrix (% x. fmul x e) (move_matrix (column_of_matrix A j) 0 (int i))"
|
|
915 |
apply (simp add: mult_matrix_def)
|
|
916 |
apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
|
|
917 |
apply (simp add: max_def)+
|
|
918 |
apply (auto)
|
|
919 |
apply (simp add: prems)+
|
|
920 |
apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
|
|
921 |
apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
|
|
922 |
apply (subst foldseq_almostzero[of _ j])
|
|
923 |
apply (simp add: prems)+
|
|
924 |
apply (auto)
|
|
925 |
apply (insert ncols_le[of A j])
|
|
926 |
apply (arith)
|
|
927 |
proof -
|
|
928 |
fix k
|
|
929 |
fix l
|
|
930 |
assume a:"~neg(int l - int i)"
|
|
931 |
assume b:"nat (int l - int i) = 0"
|
|
932 |
from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
|
|
933 |
assume c: "i \<noteq> l"
|
|
934 |
from c a show "fmul (Rep_matrix A k j) e = 0" by blast
|
|
935 |
qed
|
|
936 |
|
|
937 |
lemma mult_matrix_ext:
|
|
938 |
assumes
|
|
939 |
eprem:
|
|
940 |
"? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)"
|
|
941 |
and fprems:
|
|
942 |
"! a. fmul 0 a = 0"
|
|
943 |
"! a. fmul a 0 = 0"
|
|
944 |
"! a. fadd a 0 = a"
|
|
945 |
"! a. fadd 0 a = a"
|
|
946 |
and contraprems:
|
|
947 |
"mult_matrix fmul fadd A = mult_matrix fmul fadd B"
|
|
948 |
shows
|
|
949 |
"A = B"
|
|
950 |
proof(rule contrapos_np[of "False"], simp)
|
|
951 |
assume a: "A \<noteq> B"
|
|
952 |
have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
|
|
953 |
have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
|
|
954 |
apply (rule contrapos_np[of "False"], simp+)
|
|
955 |
apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)
|
|
956 |
by (simp add: Rep_matrix_inject a)
|
|
957 |
then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
|
|
958 |
from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast
|
|
959 |
let ?S = "singleton_matrix I 0 e"
|
|
960 |
let ?comp = "mult_matrix fmul fadd"
|
|
961 |
have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
|
|
962 |
have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
|
|
963 |
have "~(?comp A ?S = ?comp B ?S)"
|
|
964 |
apply (rule notI)
|
|
965 |
apply (simp add: fprems eprops)
|
|
966 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
967 |
apply (drule d[of _ _ "J"], drule d[of _ _ "0"])
|
|
968 |
by (simp add: e c eprops)
|
|
969 |
with contraprems show "False" by simp
|
|
970 |
qed
|
|
971 |
|
|
972 |
constdefs
|
|
973 |
foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
|
|
974 |
"foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
|
|
975 |
foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
|
|
976 |
"foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
|
|
977 |
|
|
978 |
lemma foldmatrix_transpose:
|
|
979 |
assumes
|
|
980 |
"! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
|
|
981 |
shows
|
|
982 |
"foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
|
|
983 |
proof -
|
|
984 |
have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
|
|
985 |
have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
|
|
986 |
apply (induct n)
|
|
987 |
apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
|
|
988 |
apply (auto)
|
|
989 |
by (drule_tac x1="(% j i. A j (Suc i))" in forall, simp)
|
|
990 |
show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
|
|
991 |
apply (simp add: foldmatrix_def foldmatrix_transposed_def)
|
|
992 |
apply (induct m, simp)
|
|
993 |
apply (simp)
|
|
994 |
apply (insert tworows)
|
|
995 |
apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) na) else (A (Suc na) i))" in spec)
|
|
996 |
by (simp add: foldmatrix_def foldmatrix_transposed_def)
|
|
997 |
qed
|
|
998 |
|
|
999 |
lemma foldseq_foldseq:
|
|
1000 |
assumes
|
|
1001 |
"associative f"
|
|
1002 |
"associative g"
|
|
1003 |
"! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
|
|
1004 |
shows
|
|
1005 |
"foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
|
|
1006 |
apply (insert foldmatrix_transpose[of g f A m n])
|
|
1007 |
by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
|
|
1008 |
|
|
1009 |
lemma mult_n_nrows:
|
|
1010 |
assumes
|
|
1011 |
"! a. fmul 0 a = 0"
|
|
1012 |
"! a. fmul a 0 = 0"
|
|
1013 |
"fadd 0 0 = 0"
|
|
1014 |
shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
|
|
1015 |
apply (subst nrows_le)
|
|
1016 |
apply (simp add: mult_matrix_n_def)
|
|
1017 |
apply (subst RepAbs_matrix)
|
|
1018 |
apply (rule_tac x="nrows A" in exI)
|
|
1019 |
apply (simp add: nrows prems foldseq_zero)
|
|
1020 |
apply (rule_tac x="ncols B" in exI)
|
|
1021 |
apply (simp add: ncols prems foldseq_zero)
|
|
1022 |
by (simp add: nrows prems foldseq_zero)
|
|
1023 |
|
|
1024 |
lemma mult_n_ncols:
|
|
1025 |
assumes
|
|
1026 |
"! a. fmul 0 a = 0"
|
|
1027 |
"! a. fmul a 0 = 0"
|
|
1028 |
"fadd 0 0 = 0"
|
|
1029 |
shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
|
|
1030 |
apply (subst ncols_le)
|
|
1031 |
apply (simp add: mult_matrix_n_def)
|
|
1032 |
apply (subst RepAbs_matrix)
|
|
1033 |
apply (rule_tac x="nrows A" in exI)
|
|
1034 |
apply (simp add: nrows prems foldseq_zero)
|
|
1035 |
apply (rule_tac x="ncols B" in exI)
|
|
1036 |
apply (simp add: ncols prems foldseq_zero)
|
|
1037 |
by (simp add: ncols prems foldseq_zero)
|
|
1038 |
|
|
1039 |
lemma mult_nrows:
|
|
1040 |
assumes
|
|
1041 |
"! a. fmul 0 a = 0"
|
|
1042 |
"! a. fmul a 0 = 0"
|
|
1043 |
"fadd 0 0 = 0"
|
|
1044 |
shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
|
|
1045 |
by (simp add: mult_matrix_def mult_n_nrows prems)
|
|
1046 |
|
|
1047 |
lemma mult_ncols:
|
|
1048 |
assumes
|
|
1049 |
"! a. fmul 0 a = 0"
|
|
1050 |
"! a. fmul a 0 = 0"
|
|
1051 |
"fadd 0 0 = 0"
|
|
1052 |
shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
|
|
1053 |
by (simp add: mult_matrix_def mult_n_ncols prems)
|
|
1054 |
|
|
1055 |
lemma mult_matrix_assoc:
|
|
1056 |
assumes prems:
|
|
1057 |
"! a. fmul1 0 a = 0"
|
|
1058 |
"! a. fmul1 a 0 = 0"
|
|
1059 |
"! a. fmul2 0 a = 0"
|
|
1060 |
"! a. fmul2 a 0 = 0"
|
|
1061 |
"fadd1 0 0 = 0"
|
|
1062 |
"fadd2 0 0 = 0"
|
|
1063 |
"! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
|
|
1064 |
"associative fadd1"
|
|
1065 |
"associative fadd2"
|
|
1066 |
"! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
|
|
1067 |
"! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
|
|
1068 |
"! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
|
|
1069 |
shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" (is ?concl)
|
|
1070 |
proof -
|
|
1071 |
have comb_left: "!! A B x y. A = B \<Longrightarrow> (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast
|
|
1072 |
have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n) x = foldseq fadd1 (% k. fmul2 (s k) x) n"
|
|
1073 |
by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
|
|
1074 |
have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
|
|
1075 |
by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
|
|
1076 |
let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
|
|
1077 |
show ?concl
|
|
1078 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
1079 |
apply (rule ext)+
|
|
1080 |
apply (simp add: mult_matrix_def)
|
|
1081 |
apply (subst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"])
|
|
1082 |
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1083 |
apply (subst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"]) apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1084 |
apply (subst mult_matrix_nm[of _ _ _ "?N"])
|
|
1085 |
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1086 |
apply (subst mult_matrix_nm[of _ _ _ "?N"])
|
|
1087 |
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1088 |
apply (subst mult_matrix_nm[of _ _ _ "?N"])
|
|
1089 |
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1090 |
apply (subst mult_matrix_nm[of _ _ _ "?N"])
|
|
1091 |
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
|
|
1092 |
apply (simp add: mult_matrix_n_def)
|
|
1093 |
apply (rule comb_left)
|
|
1094 |
apply ((rule ext)+, simp)
|
|
1095 |
apply (subst RepAbs_matrix)
|
|
1096 |
apply (rule exI[of _ "nrows B"])
|
|
1097 |
apply (simp add: nrows prems foldseq_zero)
|
|
1098 |
apply (rule exI[of _ "ncols C"])
|
|
1099 |
apply (simp add: prems ncols foldseq_zero)
|
|
1100 |
apply (subst RepAbs_matrix)
|
|
1101 |
apply (rule exI[of _ "nrows A"])
|
|
1102 |
apply (simp add: nrows prems foldseq_zero)
|
|
1103 |
apply (rule exI[of _ "ncols B"])
|
|
1104 |
apply (simp add: prems ncols foldseq_zero)
|
|
1105 |
apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
|
|
1106 |
apply (subst foldseq_foldseq)
|
|
1107 |
apply (simp add: prems)+
|
|
1108 |
by (simp add: transpose_infmatrix)
|
|
1109 |
qed
|
|
1110 |
|
|
1111 |
lemma
|
|
1112 |
assumes prems:
|
|
1113 |
"! a. fmul1 0 a = 0"
|
|
1114 |
"! a. fmul1 a 0 = 0"
|
|
1115 |
"! a. fmul2 0 a = 0"
|
|
1116 |
"! a. fmul2 a 0 = 0"
|
|
1117 |
"fadd1 0 0 = 0"
|
|
1118 |
"fadd2 0 0 = 0"
|
|
1119 |
"! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
|
|
1120 |
"associative fadd1"
|
|
1121 |
"associative fadd2"
|
|
1122 |
"! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
|
|
1123 |
"! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
|
|
1124 |
"! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
|
|
1125 |
shows
|
|
1126 |
"(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
|
|
1127 |
apply (rule ext)+
|
|
1128 |
apply (simp add: comp_def )
|
|
1129 |
by (simp add: mult_matrix_assoc prems)
|
|
1130 |
|
|
1131 |
lemma mult_matrix_assoc_simple:
|
|
1132 |
assumes prems:
|
|
1133 |
"! a. fmul 0 a = 0"
|
|
1134 |
"! a. fmul a 0 = 0"
|
|
1135 |
"fadd 0 0 = 0"
|
|
1136 |
"associative fadd"
|
|
1137 |
"commutative fadd"
|
|
1138 |
"associative fmul"
|
|
1139 |
"distributive fmul fadd"
|
|
1140 |
shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" (is ?concl)
|
|
1141 |
proof -
|
|
1142 |
have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
|
|
1143 |
by (simp! add: associative_def commutative_def)
|
|
1144 |
then show ?concl
|
|
1145 |
apply (subst mult_matrix_assoc)
|
|
1146 |
apply (simp_all!)
|
|
1147 |
by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
|
|
1148 |
qed
|
|
1149 |
|
|
1150 |
lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
|
|
1151 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
1152 |
apply (rule ext)+
|
|
1153 |
by simp
|
|
1154 |
|
|
1155 |
lemma transpose_combine_matrix: "f 0 0 = 0 \<Longrightarrow> transpose_matrix (combine_matrix f A B) = combine_matrix f (transpose_matrix A) (transpose_matrix B)"
|
|
1156 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
1157 |
apply (rule ext)+
|
|
1158 |
by simp
|
|
1159 |
|
|
1160 |
lemma Rep_mult_matrix:
|
|
1161 |
assumes
|
|
1162 |
"! a. fmul 0 a = 0"
|
|
1163 |
"! a. fmul a 0 = 0"
|
|
1164 |
"fadd 0 0 = 0"
|
|
1165 |
shows
|
|
1166 |
"Rep_matrix(mult_matrix fmul fadd A B) j i =
|
|
1167 |
foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
|
|
1168 |
apply (simp add: mult_matrix_def mult_matrix_n_def)
|
|
1169 |
apply (subst RepAbs_matrix)
|
|
1170 |
apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
|
|
1171 |
apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
|
|
1172 |
by simp
|
|
1173 |
|
|
1174 |
lemma transpose_mult_matrix:
|
|
1175 |
assumes
|
|
1176 |
"! a. fmul 0 a = 0"
|
|
1177 |
"! a. fmul a 0 = 0"
|
|
1178 |
"fadd 0 0 = 0"
|
|
1179 |
"! x y. fmul y x = fmul x y"
|
|
1180 |
shows
|
|
1181 |
"transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
|
|
1182 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
1183 |
apply (rule ext)+
|
|
1184 |
by (simp! add: Rep_mult_matrix max_ac)
|
|
1185 |
|
|
1186 |
instance matrix :: ("{ord,zero}") ord by intro_classes
|
|
1187 |
|
|
1188 |
defs (overloaded)
|
|
1189 |
le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
|
|
1190 |
less_def: "(A::('a::{ord,zero}) matrix) < B == (A <= B) & (A \<noteq> B)"
|
|
1191 |
|
|
1192 |
instance matrix :: ("{order, zero}") order
|
|
1193 |
apply intro_classes
|
|
1194 |
apply (simp_all add: le_matrix_def less_def)
|
|
1195 |
apply (auto)
|
|
1196 |
apply (drule_tac x=j in spec, drule_tac x=j in spec)
|
|
1197 |
apply (drule_tac x=i in spec, drule_tac x=i in spec)
|
|
1198 |
apply (simp)
|
|
1199 |
apply (simp add: Rep_matrix_inject[THEN sym])
|
|
1200 |
apply (rule ext)+
|
|
1201 |
apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
|
|
1202 |
apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
|
|
1203 |
by simp
|
|
1204 |
|
|
1205 |
lemma le_apply_matrix:
|
|
1206 |
assumes
|
|
1207 |
"f 0 = 0"
|
|
1208 |
"! x y. x <= y \<longrightarrow> f x <= f y"
|
|
1209 |
"(a::('a::{ord, zero}) matrix) <= b"
|
|
1210 |
shows
|
|
1211 |
"apply_matrix f a <= apply_matrix f b"
|
|
1212 |
by (simp! add: le_matrix_def)
|
|
1213 |
|
|
1214 |
lemma le_combine_matrix:
|
|
1215 |
assumes
|
|
1216 |
"f 0 0 = 0"
|
|
1217 |
"! a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"
|
|
1218 |
"A <= B"
|
|
1219 |
"C <= D"
|
|
1220 |
shows
|
|
1221 |
"combine_matrix f A C <= combine_matrix f B D"
|
|
1222 |
by (simp! add: le_matrix_def)
|
|
1223 |
|
|
1224 |
lemma le_left_combine_matrix:
|
|
1225 |
assumes
|
|
1226 |
"f 0 0 = 0"
|
|
1227 |
"! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b"
|
|
1228 |
"0 <= C"
|
|
1229 |
"A <= B"
|
|
1230 |
shows
|
|
1231 |
"combine_matrix f C A <= combine_matrix f C B"
|
|
1232 |
by (simp! add: le_matrix_def)
|
|
1233 |
|
|
1234 |
lemma le_right_combine_matrix:
|
|
1235 |
assumes
|
|
1236 |
"f 0 0 = 0"
|
|
1237 |
"! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c"
|
|
1238 |
"0 <= C"
|
|
1239 |
"A <= B"
|
|
1240 |
shows
|
|
1241 |
"combine_matrix f A C <= combine_matrix f B C"
|
|
1242 |
by (simp! add: le_matrix_def)
|
|
1243 |
|
|
1244 |
lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
|
|
1245 |
by (simp add: le_matrix_def, auto)
|
|
1246 |
|
|
1247 |
lemma le_foldseq:
|
|
1248 |
assumes
|
|
1249 |
"! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
|
|
1250 |
"! i. i <= n \<longrightarrow> s i <= t i"
|
|
1251 |
shows
|
|
1252 |
"foldseq f s n <= foldseq f t n"
|
|
1253 |
proof -
|
|
1254 |
have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!)
|
|
1255 |
then show "foldseq f s n <= foldseq f t n" by (simp!)
|
|
1256 |
qed
|
|
1257 |
|
|
1258 |
lemma le_left_mult:
|
|
1259 |
assumes
|
|
1260 |
"! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
|
|
1261 |
"! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
|
|
1262 |
"! a. fmul 0 a = 0"
|
|
1263 |
"! a. fmul a 0 = 0"
|
|
1264 |
"fadd 0 0 = 0"
|
|
1265 |
"0 <= C"
|
|
1266 |
"A <= B"
|
|
1267 |
shows
|
|
1268 |
"mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
|
|
1269 |
apply (simp! add: le_matrix_def Rep_mult_matrix)
|
|
1270 |
apply (auto)
|
|
1271 |
apply (subst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
|
|
1272 |
apply (rule le_foldseq)
|
|
1273 |
by (auto)
|
|
1274 |
|
|
1275 |
lemma le_right_mult:
|
|
1276 |
assumes
|
|
1277 |
"! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
|
|
1278 |
"! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
|
|
1279 |
"! a. fmul 0 a = 0"
|
|
1280 |
"! a. fmul a 0 = 0"
|
|
1281 |
"fadd 0 0 = 0"
|
|
1282 |
"0 <= C"
|
|
1283 |
"A <= B"
|
|
1284 |
shows
|
|
1285 |
"mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
|
|
1286 |
apply (simp! add: le_matrix_def Rep_mult_matrix)
|
|
1287 |
apply (auto)
|
|
1288 |
apply (subst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
|
|
1289 |
apply (rule le_foldseq)
|
|
1290 |
by (auto)
|
|
1291 |
|
|
1292 |
end
|