author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46988  9f492f5b0cec 
child 47455  26315a545e26 
permissions  rwrr 
14593  1 
(* Title: HOL/Matrix/Matrix.thy 
2 
Author: Steven Obua 

3 
*) 

4 

17915  5 
theory Matrix 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39302
diff
changeset

6 
imports Main "~~/src/HOL/Library/Lattice_Algebras" 
17915  7 
begin 
14940  8 

42463  9 
type_synonym 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a" 
27484  10 

44174
d1d79f0e1ea6
make more HOL theories work with separate set type
huffman
parents:
42463
diff
changeset

11 
definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where 
27484  12 
"nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}" 
13 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

14 
definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

15 

4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

16 
typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

17 
unfolding matrix_def 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

18 
proof 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

19 
show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}" 
27484  20 
by (simp add: nonzero_positions_def) 
21 
qed 

22 

23 
declare Rep_matrix_inverse[simp] 

24 

25 
lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))" 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44174
diff
changeset

26 
by (induct A) (simp add: Abs_matrix_inverse matrix_def) 
27484  27 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

28 
definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where 
27484  29 
"nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

30 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

31 
definition ncols :: "('a::zero) matrix \<Rightarrow> nat" where 
27484  32 
"ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))" 
33 

34 
lemma nrows: 

35 
assumes hyp: "nrows A \<le> m" 

35612  36 
shows "(Rep_matrix A m n) = 0" 
27484  37 
proof cases 
38 
assume "nonzero_positions(Rep_matrix A) = {}" 

39 
then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def) 

40 
next 

41 
assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}" 

42 
let ?S = "fst`(nonzero_positions(Rep_matrix A))" 

43 
have c: "finite (?S)" by (simp add: finite_nonzero_positions) 

44 
from hyp have d: "Max (?S) < m" by (simp add: a nrows_def) 

45 
have "m \<notin> ?S" 

46 
proof  

47 
have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c]) 

48 
moreover from d have "~(m <= Max ?S)" by (simp) 

49 
ultimately show "m \<notin> ?S" by (auto) 

50 
qed 

51 
thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect) 

52 
qed 

53 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

54 
definition transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix" where 
27484  55 
"transpose_infmatrix A j i == A i j" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

56 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

57 
definition transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix" where 
27484  58 
"transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix" 
59 

60 
declare transpose_infmatrix_def[simp] 

61 

62 
lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A" 

63 
by ((rule ext)+, simp) 

64 

65 
lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)" 

66 
apply (rule ext)+ 

46985  67 
by simp 
27484  68 

69 
lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)" 

70 
apply (rule Abs_matrix_inverse) 

71 
apply (simp add: matrix_def nonzero_positions_def image_def) 

72 
proof  

73 
let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}" 

74 
let ?swap = "% pos. (snd pos, fst pos)" 

75 
let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}" 

76 
have swap_image: "?swap`?A = ?B" 

77 
apply (simp add: image_def) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38526
diff
changeset

78 
apply (rule set_eqI) 
27484  79 
apply (simp) 
80 
proof 

81 
fix y 

82 
assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)" 

83 
thus "Rep_matrix x (fst y) (snd y) \<noteq> 0" 

84 
proof  

85 
from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast 

86 
then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp) 

87 
qed 

88 
next 

89 
fix y 

90 
assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0" 

91 
show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32491
diff
changeset

92 
by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp) 
27484  93 
qed 
94 
then have "finite (?swap`?A)" 

95 
proof  

96 
have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions) 

97 
then have "finite ?B" by (simp add: nonzero_positions_def) 

98 
with swap_image show "finite (?swap`?A)" by (simp) 

99 
qed 

100 
moreover 

101 
have "inj_on ?swap ?A" by (simp add: inj_on_def) 

102 
ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A]) 

103 
qed 

104 

105 
lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto 

106 

107 
lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)" 

108 
apply (auto) 

109 
apply (rule ext)+ 

110 
apply (simp add: transpose_infmatrix) 

111 
apply (drule infmatrixforward) 

112 
apply (simp) 

113 
done 

114 

115 
lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)" 

116 
apply (simp add: transpose_matrix_def) 

117 
apply (subst Rep_matrix_inject[THEN sym])+ 

118 
apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject) 

119 
done 

120 

121 
lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j" 

122 
by (simp add: transpose_matrix_def) 

123 

124 
lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A" 

125 
by (simp add: transpose_matrix_def) 

126 

127 
lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A" 

128 
by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def) 

129 

130 
lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A" 

131 
by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def) 

132 

133 
lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0" 

134 
proof  

135 
assume "ncols A <= n" 

136 
then have "nrows (transpose_matrix A) <= n" by (simp) 

137 
then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows) 

138 
thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def) 

139 
qed 

140 

141 
lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st") 

142 
apply (auto) 

143 
apply (simp add: ncols) 

144 
proof (simp add: ncols_def, auto) 

145 
let ?P = "nonzero_positions (Rep_matrix A)" 

146 
let ?p = "snd`?P" 

147 
have a:"finite ?p" by (simp add: finite_nonzero_positions) 

148 
let ?m = "Max ?p" 

149 
assume "~(Suc (?m) <= n)" 

150 
then have b:"n <= ?m" by (simp) 

151 
fix a b 

152 
assume "(a,b) \<in> ?P" 

153 
then have "?p \<noteq> {}" by (auto) 

154 
with a have "?m \<in> ?p" by (simp) 

155 
moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def) 

156 
ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp) 

157 
moreover assume ?st 

158 
ultimately show "False" using b by (simp) 

159 
qed 

160 

35612  161 
lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" 
27484  162 
proof  
163 
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith 

35612  164 
show ?thesis by (simp add: a ncols_le) 
27484  165 
qed 
166 

35612  167 
lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" 
27484  168 
apply (auto) 
169 
apply (subgoal_tac "ncols A <= m") 

170 
apply (simp) 

171 
apply (simp add: ncols_le) 

172 
apply (drule_tac x="ncols A" in spec) 

173 
by (simp add: ncols) 

174 

175 
lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s) 

176 
proof  

177 
have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp) 

178 
also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le) 

179 
also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp) 

180 
finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto) 

181 
qed 

182 

35612  183 
lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" 
27484  184 
proof  
185 
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith 

35612  186 
show ?thesis by (simp add: a nrows_le) 
27484  187 
qed 
188 

35612  189 
lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" 
27484  190 
apply (auto) 
191 
apply (subgoal_tac "nrows A <= m") 

192 
apply (simp) 

193 
apply (simp add: nrows_le) 

194 
apply (drule_tac x="nrows A" in spec) 

195 
by (simp add: nrows) 

196 

197 
lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A" 

198 
apply (case_tac "nrows A <= m") 

199 
apply (simp_all add: nrows) 

200 
done 

201 

202 
lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A" 

203 
apply (case_tac "ncols A <= n") 

204 
apply (simp_all add: ncols) 

205 
done 

206 

207 
lemma finite_natarray1: "finite {x. x < (n::nat)}" 

208 
apply (induct n) 

209 
apply (simp) 

210 
proof  

211 
fix n 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38526
diff
changeset

212 
have "{x. x < Suc n} = insert n {x. x < n}" by (rule set_eqI, simp, arith) 
27484  213 
moreover assume "finite {x. x < n}" 
214 
ultimately show "finite {x. x < Suc n}" by (simp) 

215 
qed 

216 

217 
lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}" 

218 
apply (induct m) 

219 
apply (simp+) 

220 
proof  

221 
fix m::nat 

222 
let ?s0 = "{pos. fst pos < m & snd pos < n}" 

223 
let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}" 

224 
let ?sd = "{pos. fst pos = m & snd pos < n}" 

225 
assume f0: "finite ?s0" 

226 
have f1: "finite ?sd" 

227 
proof  

228 
let ?f = "% x. (m, x)" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38526
diff
changeset

229 
have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_eqI, simp add: image_def, auto) 
27484  230 
moreover have "finite {x. x < n}" by (simp add: finite_natarray1) 
231 
ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp) 

232 
qed 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38526
diff
changeset

233 
have su: "?s0 \<union> ?sd = ?s1" by (rule set_eqI, simp, arith) 
27484  234 
from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI) 
235 
with su show "finite ?s1" by (simp) 

236 
qed 

237 

238 
lemma RepAbs_matrix: 

239 
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) 

240 
shows "(Rep_matrix (Abs_matrix x)) = x" 

241 
apply (rule Abs_matrix_inverse) 

242 
apply (simp add: matrix_def nonzero_positions_def) 

243 
proof  

244 
from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast) 

245 
from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast) 

246 
let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}" 

247 
let ?v = "{pos. fst pos < m & snd pos < n}" 

248 
have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith) 

249 
from a b have "(?u \<inter> (?v)) = {}" 

250 
apply (simp) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
38526
diff
changeset

251 
apply (rule set_eqI) 
27484  252 
apply (simp) 
253 
apply auto 

254 
by (rule c, auto)+ 

255 
then have d: "?u \<subseteq> ?v" by blast 

256 
moreover have "finite ?v" by (simp add: finite_natarray2) 

257 
ultimately show "finite ?u" by (rule finite_subset) 

258 
qed 

259 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

260 
definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where 
27484  261 
"apply_infmatrix f == % A. (% j i. f (A j i))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

262 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

263 
definition apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix" where 
27484  264 
"apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

265 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

266 
definition combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix" where 
27484  267 
"combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

268 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

269 
definition combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix" where 
27484  270 
"combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))" 
271 

272 
lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)" 

273 
by (simp add: apply_infmatrix_def) 

274 

275 
lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)" 

276 
by (simp add: combine_infmatrix_def) 

277 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

278 
definition commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" where 
27484  279 
"commutative f == ! x y. f x y = f y x" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

280 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

281 
definition associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where 
27484  282 
"associative f == ! x y z. f (f x y) z = f x (f y z)" 
283 

284 
text{* 

285 
To reason about associativity and commutativity of operations on matrices, 

286 
let's take a step back and look at the general situtation: Assume that we have 

287 
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. 

288 
Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$. 

289 
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.$ 

290 
*} 

291 

292 
lemma combine_infmatrix_commute: 

293 
"commutative f \<Longrightarrow> commutative (combine_infmatrix f)" 

294 
by (simp add: commutative_def combine_infmatrix_def) 

295 

296 
lemma combine_matrix_commute: 

297 
"commutative f \<Longrightarrow> commutative (combine_matrix f)" 

298 
by (simp add: combine_matrix_def commutative_def combine_infmatrix_def) 

299 

300 
text{* 

301 
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\}$, 

302 
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 

303 
\[ f' (f' 1 1) 1 = u(f (u (f 1 1)) 1) = u(f (u 2) 1) = u (f 0 1) = 1, \] 

304 
but on the other hand we have 

305 
\[ f' 1 (f' 1 1) = u (f 1 (u (f 1 1))) = u (f 1 0) = 1.\] 

306 
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: 

307 
*} 

308 

309 
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)" 

310 
by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto) 

311 

312 
lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))" 

313 
by (insert Rep_matrix [of A], simp add: matrix_def) 

314 

315 
lemma combine_infmatrix_closed [simp]: 

316 
"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)" 

317 
apply (rule Abs_matrix_inverse) 

318 
apply (simp add: matrix_def) 

319 
apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"]) 

320 
by (simp_all) 

321 

322 
text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *} 

323 
lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A" 

324 
by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto) 

325 

326 
lemma apply_infmatrix_closed [simp]: 

327 
"f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)" 

328 
apply (rule Abs_matrix_inverse) 

329 
apply (simp add: matrix_def) 

330 
apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"]) 

331 
by (simp_all) 

332 

333 
lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)" 

334 
by (simp add: associative_def combine_infmatrix_def) 

335 

336 
lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y" 

337 
by (auto) 

338 

339 
lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)" 

340 
apply (simp(no_asm) add: associative_def combine_matrix_def, auto) 

341 
apply (rule comb [of Abs_matrix Abs_matrix]) 

342 
by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def) 

343 

344 
lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)" 

345 
by (simp add: apply_matrix_def) 

346 

347 
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)" 

348 
by(simp add: combine_matrix_def) 

349 

350 
lemma combine_nrows_max: "f 0 0 = 0 \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)" 

351 
by (simp add: nrows_le) 

352 

353 
lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)" 

354 
by (simp add: ncols_le) 

355 

356 
lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q" 

357 
by (simp add: nrows_le) 

358 

359 
lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q" 

360 
by (simp add: ncols_le) 

361 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

362 
definition zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool" where 
27484  363 
"zero_r_neutral f == ! a. f a 0 = a" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

364 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

365 
definition zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where 
27484  366 
"zero_l_neutral f == ! a. f 0 a = a" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

367 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

368 
definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where 
27484  369 
"zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)" 
370 

38273  371 
primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" 
372 
where 

27484  373 
"foldseq f s 0 = s 0" 
38273  374 
 "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)" 
27484  375 

38273  376 
primrec foldseq_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" 
377 
where 

27484  378 
"foldseq_transposed f s 0 = s 0" 
38273  379 
 "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))" 
27484  380 

381 
lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f" 

382 
proof  

383 
assume a:"associative f" 

384 
then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" 

385 
proof  

386 
fix n 

387 
show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" 

388 
proof (induct n) 

389 
show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp 

390 
next 

391 
fix n 

392 
assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" 

393 
have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b) 

394 
show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N" 

395 
proof (auto) 

396 
fix N t 

397 
assume Nsuc: "N <= Suc n" 

398 
show "foldseq f t N = foldseq_transposed f t N" 

399 
proof cases 

400 
assume "N <= n" 

401 
then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b) 

402 
next 

403 
assume "~(N <= n)" 

404 
with Nsuc have Nsuceq: "N = Suc n" by simp 

405 
have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith 

406 
have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def) 

407 
show "foldseq f t N = foldseq_transposed f t N" 

408 
apply (simp add: Nsuceq) 

409 
apply (subst c) 

410 
apply (simp) 

411 
apply (case_tac "n = 0") 

412 
apply (simp) 

413 
apply (drule neqz) 

414 
apply (erule exE) 

415 
apply (simp) 

416 
apply (subst assocf) 

417 
proof  

418 
fix m 

419 
assume "n = Suc m & Suc m <= n" 

420 
then have mless: "Suc m <= n" by arith 

421 
then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2") 

422 
apply (subst c) 

423 
by simp+ 

424 
have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp 

425 
have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4") 

426 
apply (subst c) 

427 
by (simp add: mless)+ 

428 
have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp 

429 
from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp 

430 
qed 

431 
qed 

432 
qed 

433 
qed 

434 
qed 

435 
show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto) 

436 
qed 

437 

438 
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)" 

439 
proof  

440 
assume assoc: "associative f" 

441 
assume comm: "commutative f" 

442 
from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def) 

443 
from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def) 

444 
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) 

445 
have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))" 

446 
apply (induct_tac n) 

447 
apply (simp+, auto) 

448 
by (simp add: a b c) 

449 
then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp 

450 
qed 

451 

452 
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)" 

453 
oops 

454 
(* Model found 

455 

456 
Trying to find a model that refutes: \<lbrakk>associative f; associative g; 

457 
\<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; 

458 
\<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk> 

459 
\<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y) 

460 
Searching for a model of size 1, translating term... invoking SAT solver... no model found. 

461 
Searching for a model of size 2, translating term... invoking SAT solver... no model found. 

462 
Searching for a model of size 3, translating term... invoking SAT solver... 

463 
Model found: 

464 
Size of types: 'a: 3 

465 
x: a1 

466 
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)) 

467 
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)) 

468 
*) 

469 

470 
lemma foldseq_zero: 

471 
assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0" 

472 
shows "foldseq f s n = 0" 

473 
proof  

474 
have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0" 

475 
apply (induct_tac n) 

476 
apply (simp) 

477 
by (simp add: fz) 

478 
then show "foldseq f s n = 0" by (simp add: sz) 

479 
qed 

480 

481 
lemma foldseq_significant_positions: 

482 
assumes p: "! i. i <= N \<longrightarrow> S i = T i" 

35612  483 
shows "foldseq f S N = foldseq f T N" 
27484  484 
proof  
485 
have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m" 

486 
apply (induct_tac m) 

487 
apply (simp) 

488 
apply (simp) 

489 
apply (auto) 

490 
proof  

491 
fix n 

492 
fix s::"nat\<Rightarrow>'a" 

493 
fix t::"nat\<Rightarrow>'a" 

494 
assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n" 

495 
assume b: "\<forall>i\<le>Suc n. s i = t i" 

496 
have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast 

497 
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) 

498 
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) 

499 
qed 

35612  500 
with p show ?thesis by simp 
27484  501 
qed 
502 

35612  503 
lemma foldseq_tail: 
504 
assumes "M <= N" 

505 
shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (NM)))) M" 

27484  506 
proof  
507 
have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith 

508 
have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast 

509 
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)) (nm)))) m" 

510 
apply (induct_tac n) 

511 
apply (simp) 

512 
apply (simp) 

513 
apply (auto) 

514 
apply (case_tac "m = Suc na") 

515 
apply (simp) 

516 
apply (rule a) 

517 
apply (rule foldseq_significant_positions) 

518 
apply (auto) 

519 
apply (drule suc, simp+) 

520 
proof  

521 
fix na m s 

522 
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" 

523 
assume subb:"m <= na" 

524 
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 

525 
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 = 

526 
foldseq f (% k. s(Suc k)) na" 

527 
by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb) 

528 
from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith 

529 
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) = 

530 
foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na  m)) m" 

531 
apply (simp add: subd) 

38526  532 
apply (cases "m = 0") 
27484  533 
apply (simp) 
534 
apply (drule sube) 

535 
apply (auto) 

536 
apply (rule a) 

38526  537 
by (simp add: subc cong del: if_cong) 
27484  538 
qed 
35612  539 
then show ?thesis using assms by simp 
27484  540 
qed 
541 

542 
lemma foldseq_zerotail: 

543 
assumes 

544 
fz: "f 0 0 = 0" 

545 
and sz: "! i. n <= i \<longrightarrow> s i = 0" 

546 
and nm: "n <= m" 

547 
shows 

548 
"foldseq f s n = foldseq f s m" 

549 
proof  

550 
show "foldseq f s n = foldseq f s m" 

551 
apply (simp add: foldseq_tail[OF nm, of f s]) 

552 
apply (rule foldseq_significant_positions) 

553 
apply (auto) 

554 
apply (subst foldseq_zero) 

555 
by (simp add: fz sz)+ 

556 
qed 

557 

558 
lemma foldseq_zerotail2: 

559 
assumes "! x. f x 0 = x" 

560 
and "! i. n < i \<longrightarrow> s i = 0" 

561 
and nm: "n <= m" 

35612  562 
shows "foldseq f s n = foldseq f s m" 
27484  563 
proof  
35612  564 
have "f 0 0 = 0" by (simp add: assms) 
27484  565 
have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. mn = Suc k" by arith 
566 
have c: "0 <= m" by simp 

567 
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith 

35612  568 
show ?thesis 
27484  569 
apply (subst foldseq_tail[OF nm]) 
570 
apply (rule foldseq_significant_positions) 

571 
apply (auto) 

572 
apply (case_tac "m=n") 

573 
apply (simp+) 

574 
apply (drule b[OF nm]) 

575 
apply (auto) 

576 
apply (case_tac "k=0") 

35612  577 
apply (simp add: assms) 
27484  578 
apply (drule d) 
579 
apply (auto) 

35612  580 
apply (simp add: assms foldseq_zero) 
581 
done 

27484  582 
qed 
583 

584 
lemma foldseq_zerostart: 

585 
"! 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))" 

586 
proof  

587 
assume f00x: "! x. f 0 (f 0 x) = f 0 x" 

588 
have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" 

589 
apply (induct n) 

590 
apply (simp) 

591 
apply (rule allI, rule impI) 

592 
proof  

593 
fix n 

594 
fix s 

595 
have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp 

596 
assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))" 

597 
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 

598 
assume d: "! i. i <= Suc n \<longrightarrow> s i = 0" 

599 
show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))" 

600 
apply (subst a) 

601 
apply (subst c) 

602 
by (simp add: d f00x)+ 

603 
qed 

604 
then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp 

605 
qed 

606 

607 
lemma foldseq_zerostart2: 

608 
"! x. f 0 x = x \<Longrightarrow> ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n" 

609 
proof  

610 
assume a:"! i. i<n \<longrightarrow> s i = 0" 

611 
assume x:"! x. f 0 x = x" 

612 
from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast 

613 
have b: "!! i l. i < Suc l = (i <= l)" by arith 

614 
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith 

615 
show "foldseq f s n = s n" 

616 
apply (case_tac "n=0") 

617 
apply (simp) 

618 
apply (insert a) 

619 
apply (drule d) 

620 
apply (auto) 

621 
apply (simp add: b) 

622 
apply (insert f00x) 

623 
apply (drule foldseq_zerostart) 

624 
by (simp add: x)+ 

625 
qed 

626 

627 
lemma foldseq_almostzero: 

628 
assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0" 

35612  629 
shows "foldseq f s n = (if (j <= n) then (s j) else 0)" 
27484  630 
proof  
631 
from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp 

632 
from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp 

35612  633 
show ?thesis 
27484  634 
apply auto 
635 
apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym]) 

636 
apply simp 

637 
apply (subst foldseq_zerostart2) 

638 
apply (simp add: f0x a)+ 

639 
apply (subst foldseq_zero) 

640 
by (simp add: s0 f0x)+ 

641 
qed 

642 

643 
lemma foldseq_distr_unary: 

644 
assumes "!! a b. g (f a b) = f (g a) (g b)" 

35612  645 
shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" 
27484  646 
proof  
647 
have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n" 

648 
apply (induct_tac n) 

649 
apply (simp) 

650 
apply (simp) 

651 
apply (auto) 

652 
apply (drule_tac x="% k. s (Suc k)" in spec) 

35612  653 
by (simp add: assms) 
654 
then show ?thesis by simp 

27484  655 
qed 
656 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

657 
definition 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" where 
27484  658 
"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)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

659 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

660 
definition 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" where 
27484  661 
"mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B" 
662 

663 
lemma mult_matrix_n: 

35612  664 
assumes "ncols A \<le> n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0" 
665 
shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" 

27484  666 
proof  
35612  667 
show ?thesis using assms 
27484  668 
apply (simp add: mult_matrix_def mult_matrix_n_def) 
669 
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) 

35612  670 
apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms) 
671 
done 

27484  672 
qed 
673 

674 
lemma mult_matrix_nm: 

35612  675 
assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0" 
27484  676 
shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" 
677 
proof  

35612  678 
from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" 
679 
by (simp add: mult_matrix_n) 

680 
also from assms have "\<dots> = mult_matrix_n m fmul fadd A B" 

681 
by (simp add: mult_matrix_n[THEN sym]) 

27484  682 
finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp 
683 
qed 

684 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

685 
definition r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where 
27484  686 
"r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

687 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

688 
definition l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where 
27484  689 
"l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

690 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

691 
definition distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where 
27484  692 
"distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd" 
693 

694 
lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith) 

695 
lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith) 

696 

697 
lemma r_distributive_matrix: 

35612  698 
assumes 
27484  699 
"r_distributive fmul fadd" 
700 
"associative fadd" 

701 
"commutative fadd" 

702 
"fadd 0 0 = 0" 

703 
"! a. fmul a 0 = 0" 

704 
"! a. fmul 0 a = 0" 

35612  705 
shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" 
27484  706 
proof  
35612  707 
from assms show ?thesis 
27484  708 
apply (simp add: r_distributive_def mult_matrix_def, auto) 
709 
proof  

710 
fix a::"'a matrix" 

711 
fix u::"'b matrix" 

712 
fix v::"'b matrix" 

713 
let ?mx = "max (ncols a) (max (nrows u) (nrows v))" 

35612  714 
from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) = 
27484  715 
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)" 
716 
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) 

717 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

718 
apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul]) 

719 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

720 
apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul]) 

721 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

722 
apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd]) 

723 
apply (simp add: combine_matrix_def combine_infmatrix_def) 

724 
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) 

725 
apply (simplesubst RepAbs_matrix) 

726 
apply (simp, auto) 

727 
apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero) 

728 
apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero) 

729 
apply (subst RepAbs_matrix) 

730 
apply (simp, auto) 

731 
apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero) 

732 
apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero) 

733 
done 

734 
qed 

735 
qed 

736 

737 
lemma l_distributive_matrix: 

35612  738 
assumes 
27484  739 
"l_distributive fmul fadd" 
740 
"associative fadd" 

741 
"commutative fadd" 

742 
"fadd 0 0 = 0" 

743 
"! a. fmul a 0 = 0" 

744 
"! a. fmul 0 a = 0" 

35612  745 
shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" 
27484  746 
proof  
35612  747 
from assms show ?thesis 
27484  748 
apply (simp add: l_distributive_def mult_matrix_def, auto) 
749 
proof  

750 
fix a::"'b matrix" 

751 
fix u::"'a matrix" 

752 
fix v::"'a matrix" 

753 
let ?mx = "max (nrows a) (max (ncols u) (ncols v))" 

35612  754 
from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a = 
27484  755 
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)" 
756 
apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul]) 

757 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

758 
apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul]) 

759 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

760 
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) 

761 
apply (simp add: max1 max2 combine_nrows combine_ncols)+ 

762 
apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd]) 

763 
apply (simp add: combine_matrix_def combine_infmatrix_def) 

764 
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) 

765 
apply (simplesubst RepAbs_matrix) 

766 
apply (simp, auto) 

767 
apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero) 

768 
apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero) 

769 
apply (subst RepAbs_matrix) 

770 
apply (simp, auto) 

771 
apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero) 

772 
apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero) 

773 
done 

774 
qed 

775 
qed 

776 

777 
instantiation matrix :: (zero) zero 

778 
begin 

779 

37765  780 
definition zero_matrix_def: "0 = Abs_matrix (\<lambda>j i. 0)" 
27484  781 

782 
instance .. 

783 

784 
end 

785 

786 
lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0" 

787 
apply (simp add: zero_matrix_def) 

788 
apply (subst RepAbs_matrix) 

789 
by (auto) 

790 

791 
lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0" 

792 
proof  

793 
have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith) 

794 
show "nrows 0 = 0" by (rule a, subst nrows_le, simp) 

795 
qed 

796 

797 
lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0" 

798 
proof  

799 
have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith) 

800 
show "ncols 0 = 0" by (rule a, subst ncols_le, simp) 

801 
qed 

802 

803 
lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)" 

804 
by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def) 

805 

806 
lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)" 

807 
by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def) 

808 

809 
lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)" 

810 
apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def) 

811 
apply (auto) 

812 
by (subst foldseq_zero, (simp add: zero_matrix_def)+)+ 

813 

814 
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" 

815 
apply (simp add: mult_matrix_n_def) 

816 
apply (subst foldseq_zero) 

817 
by (simp_all add: zero_matrix_def) 

818 

819 
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" 

820 
apply (simp add: mult_matrix_n_def) 

821 
apply (subst foldseq_zero) 

822 
by (simp_all add: zero_matrix_def) 

823 

824 
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" 

825 
by (simp add: mult_matrix_def) 

826 

827 
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" 

828 
by (simp add: mult_matrix_def) 

829 

830 
lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0" 

831 
apply (simp add: apply_matrix_def apply_infmatrix_def) 

832 
by (simp add: zero_matrix_def) 

833 

834 
lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0" 

835 
apply (simp add: combine_matrix_def combine_infmatrix_def) 

836 
by (simp add: zero_matrix_def) 

837 

838 
lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0" 

46985  839 
apply (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix) 
27484  840 
apply (subst Rep_matrix_inject[symmetric], (rule ext)+) 
841 
apply (simp add: RepAbs_matrix) 

842 
done 

843 

844 
lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0" 

845 
apply (simp add: apply_matrix_def apply_infmatrix_def) 

846 
by (simp add: zero_matrix_def) 

847 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

848 
definition singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix" where 
27484  849 
"singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

850 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

851 
definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where 
46702  852 
"move_matrix A y x == Abs_matrix(% j i. if (((int j)y) < 0)  (((int i)x) < 0) then 0 else Rep_matrix A (nat ((int j)y)) (nat ((int i)x)))" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

853 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

854 
definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where 
27484  855 
"take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

856 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

857 
definition take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where 
27484  858 
"take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)" 
859 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

860 
definition column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where 
27484  861 
"column_of_matrix A n == take_columns (move_matrix A 0 ( int n)) 1" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

862 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

863 
definition row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where 
27484  864 
"row_of_matrix A m == take_rows (move_matrix A ( int m) 0) 1" 
865 

866 
lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)" 

867 
apply (simp add: singleton_matrix_def) 

868 
apply (auto) 

869 
apply (subst RepAbs_matrix) 

870 
apply (rule exI[of _ "Suc m"], simp) 

871 
apply (rule exI[of _ "Suc n"], simp+) 

872 
by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+ 

873 

874 
lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))" 

875 
apply (subst Rep_matrix_inject[symmetric]) 

876 
apply (rule ext)+ 

877 
apply (simp) 

878 
done 

879 

880 
lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0" 

881 
by (simp add: singleton_matrix_def zero_matrix_def) 

882 

883 
lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)" 

884 
proof 

885 
have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+ 

886 
from th show ?thesis 

887 
apply (auto) 

33657  888 
apply (rule le_antisym) 
27484  889 
apply (subst nrows_le) 
890 
apply (simp add: singleton_matrix_def, auto) 

891 
apply (subst RepAbs_matrix) 

892 
apply auto 

893 
apply (simp add: Suc_le_eq) 

894 
apply (rule not_leE) 

895 
apply (subst nrows_le) 

896 
by simp 

897 
qed 

898 

899 
lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)" 

900 
proof 

901 
have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+ 

902 
from th show ?thesis 

903 
apply (auto) 

33657  904 
apply (rule le_antisym) 
27484  905 
apply (subst ncols_le) 
906 
apply (simp add: singleton_matrix_def, auto) 

907 
apply (subst RepAbs_matrix) 

908 
apply auto 

909 
apply (simp add: Suc_le_eq) 

910 
apply (rule not_leE) 

911 
apply (subst ncols_le) 

912 
by simp 

913 
qed 

914 

915 
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)" 

916 
apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def) 

917 
apply (subst RepAbs_matrix) 

918 
apply (rule exI[of _ "Suc j"], simp) 

919 
apply (rule exI[of _ "Suc i"], simp) 

920 
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) 

921 
apply (subst RepAbs_matrix) 

922 
apply (rule exI[of _ "Suc j"], simp) 

923 
apply (rule exI[of _ "Suc i"], simp) 

924 
by simp 

925 

926 
lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a" 

927 
apply (subst Rep_matrix_inject[symmetric], (rule ext)+) 

928 
apply (simp) 

929 
done 

930 

931 
lemma Rep_move_matrix[simp]: 

932 
"Rep_matrix (move_matrix A y x) j i = 

46702  933 
(if (((int j)y) < 0)  (((int i)x) < 0) then 0 else Rep_matrix A (nat((int j)y)) (nat((int i)x)))" 
27484  934 
apply (simp add: move_matrix_def) 
935 
apply (auto) 

936 
by (subst RepAbs_matrix, 

937 
rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith, 

938 
rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+ 

939 

940 
lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A" 

941 
by (simp add: move_matrix_def) 

942 

943 
lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i" 

944 
apply (subst Rep_matrix_inject[symmetric]) 

945 
apply (rule ext)+ 

946 
apply (simp) 

947 
done 

948 

949 
lemma transpose_move_matrix[simp]: 

950 
"transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x" 

951 
apply (subst Rep_matrix_inject[symmetric], (rule ext)+) 

952 
apply (simp) 

953 
done 

954 

955 
lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 

956 
(if (j + int u < 0)  (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))" 

957 
apply (subst Rep_matrix_inject[symmetric]) 

958 
apply (rule ext)+ 

959 
apply (case_tac "j + int u < 0") 

960 
apply (simp, arith) 

961 
apply (case_tac "i + int v < 0") 

46702  962 
apply (simp, arith) 
963 
apply simp 

27484  964 
apply arith 
965 
done 

966 

967 
lemma Rep_take_columns[simp]: 

968 
"Rep_matrix (take_columns A c) j i = 

969 
(if i < c then (Rep_matrix A j i) else 0)" 

970 
apply (simp add: take_columns_def) 

971 
apply (simplesubst RepAbs_matrix) 

972 
apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) 

973 
apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) 

974 
done 

975 

976 
lemma Rep_take_rows[simp]: 

977 
"Rep_matrix (take_rows A r) j i = 

978 
(if j < r then (Rep_matrix A j i) else 0)" 

979 
apply (simp add: take_rows_def) 

980 
apply (simplesubst RepAbs_matrix) 

981 
apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) 

982 
apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) 

983 
done 

984 

985 
lemma Rep_column_of_matrix[simp]: 

986 
"Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)" 

987 
by (simp add: column_of_matrix_def) 

988 

989 
lemma Rep_row_of_matrix[simp]: 

990 
"Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)" 

991 
by (simp add: row_of_matrix_def) 

992 

993 
lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0" 

994 
apply (subst Rep_matrix_inject[THEN sym]) 

995 
apply (rule ext)+ 

996 
by (simp add: ncols) 

997 

998 
lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0" 

999 
apply (subst Rep_matrix_inject[THEN sym]) 

1000 
apply (rule ext)+ 

1001 
by (simp add: nrows) 

1002 

1003 
lemma mult_matrix_singleton_right[simp]: 

35612  1004 
assumes 
27484  1005 
"! x. fmul x 0 = 0" 
1006 
"! x. fmul 0 x = 0" 

1007 
"! x. fadd 0 x = x" 

1008 
"! x. fadd x 0 = x" 

1009 
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))" 

1010 
apply (simp add: mult_matrix_def) 

1011 
apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"]) 

1012 
apply (auto) 

35612  1013 
apply (simp add: assms)+ 
27484  1014 
apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def) 
1015 
apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+) 

1016 
apply (subst foldseq_almostzero[of _ j]) 

35612  1017 
apply (simp add: assms)+ 
27484  1018 
apply (auto) 
29700  1019 
done 
27484  1020 

1021 
lemma mult_matrix_ext: 

1022 
assumes 

1023 
eprem: 

1024 
"? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" 

1025 
and fprems: 

1026 
"! a. fmul 0 a = 0" 

1027 
"! a. fmul a 0 = 0" 

1028 
"! a. fadd a 0 = a" 

1029 
"! a. fadd 0 a = a" 

1030 
and contraprems: 

1031 
"mult_matrix fmul fadd A = mult_matrix fmul fadd B" 

1032 
shows 

1033 
"A = B" 

1034 
proof(rule contrapos_np[of "False"], simp) 

1035 
assume a: "A \<noteq> B" 

1036 
have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto) 

1037 
have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)" 

1038 
apply (rule contrapos_np[of "False"], simp+) 

1039 
apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp) 

1040 
by (simp add: Rep_matrix_inject a) 

1041 
then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast 

1042 
from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast 

1043 
let ?S = "singleton_matrix I 0 e" 

1044 
let ?comp = "mult_matrix fmul fadd" 

1045 
have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast 

35612  1046 
have e: "(% x. fmul x e) 0 = 0" by (simp add: assms) 
27484  1047 
have "~(?comp A ?S = ?comp B ?S)" 
1048 
apply (rule notI) 

1049 
apply (simp add: fprems eprops) 

1050 
apply (simp add: Rep_matrix_inject[THEN sym]) 

1051 
apply (drule d[of _ _ "J"], drule d[of _ _ "0"]) 

1052 
by (simp add: e c eprops) 

1053 
with contraprems show "False" by simp 

1054 
qed 

1055 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

1056 
definition foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where 
27484  1057 
"foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m" 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

1058 

d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35032
diff
changeset

1059 
definition foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where 
27484  1060 
"foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m" 
1061 

1062 
lemma foldmatrix_transpose: 

1063 
assumes 

1064 
"! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" 

1065 
shows 

35612  1066 
"foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" 
27484  1067 
proof  
1068 
have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto 

1069 
have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1" 

1070 
apply (induct n) 

35612  1071 
apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+ 
27484  1072 
apply (auto) 
1073 
by (drule_tac x="(% j i. A j (Suc i))" in forall, simp) 

1074 
show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" 

1075 
apply (simp add: foldmatrix_def foldmatrix_transposed_def) 

1076 
apply (induct m, simp) 

1077 
apply (simp) 

1078 
apply (insert tworows) 

1079 
apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec) 

1080 
by (simp add: foldmatrix_def foldmatrix_transposed_def) 

1081 
qed 

1082 

1083 
lemma foldseq_foldseq: 

1084 
assumes 

1085 
"associative f" 

1086 
"associative g" 

1087 
"! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" 

1088 
shows 

1089 
"foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n" 

1090 
apply (insert foldmatrix_transpose[of g f A m n]) 

35612  1091 
by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms) 
27484  1092 

1093 
lemma mult_n_nrows: 

1094 
assumes 

1095 
"! a. fmul 0 a = 0" 

1096 
"! a. fmul a 0 = 0" 

1097 
"fadd 0 0 = 0" 

1098 
shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A" 

1099 
apply (subst nrows_le) 

1100 
apply (simp add: mult_matrix_n_def) 

1101 
apply (subst RepAbs_matrix) 

1102 
apply (rule_tac x="nrows A" in exI) 

35612  1103 
apply (simp add: nrows assms foldseq_zero) 
27484  1104 
apply (rule_tac x="ncols B" in exI) 
35612  1105 
apply (simp add: ncols assms foldseq_zero) 
1106 
apply (simp add: nrows assms foldseq_zero) 

1107 
done 

27484  1108 

1109 
lemma mult_n_ncols: 

1110 
assumes 

1111 
"! a. fmul 0 a = 0" 

1112 
"! a. fmul a 0 = 0" 

1113 
"fadd 0 0 = 0" 

1114 
shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B" 

1115 
apply (subst ncols_le) 

1116 
apply (simp add: mult_matrix_n_def) 

1117 
apply (subst RepAbs_matrix) 

1118 
apply (rule_tac x="nrows A" in exI) 

35612  1119 
apply (simp add: nrows assms foldseq_zero) 
27484  1120 
apply (rule_tac x="ncols B" in exI) 
35612  1121 
apply (simp add: ncols assms foldseq_zero) 
1122 
apply (simp add: ncols assms foldseq_zero) 

1123 
done 

27484  1124 

1125 
lemma mult_nrows: 

1126 
assumes 

1127 
"! a. fmul 0 a = 0" 

1128 
"! a. fmul a 0 = 0" 

1129 
"fadd 0 0 = 0" 

1130 
shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A" 

35612  1131 
by (simp add: mult_matrix_def mult_n_nrows assms) 
27484  1132 

1133 
lemma mult_ncols: 

1134 
assumes 

1135 
"! a. fmul 0 a = 0" 

1136 
"! a. fmul a 0 = 0" 

1137 
"fadd 0 0 = 0" 

1138 
shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B" 

35612  1139 
by (simp add: mult_matrix_def mult_n_ncols assms) 
27484  1140 

1141 
lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)" 

1142 
apply (auto simp add: nrows_le) 

1143 
apply (rule nrows) 

1144 
apply (arith) 

1145 
done 

1146 

1147 
lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)" 

1148 
apply (auto simp add: ncols_le) 

1149 
apply (rule ncols) 

1150 
apply (arith) 

1151 
done 

1152 

1153 
lemma mult_matrix_assoc: 

35612  1154 
assumes 
27484  1155 
"! a. fmul1 0 a = 0" 
1156 
"! a. fmul1 a 0 = 0" 

1157 
"! a. fmul2 0 a = 0" 

1158 
"! a. fmul2 a 0 = 0" 

1159 
"fadd1 0 0 = 0" 

1160 
"fadd2 0 0 = 0" 

1161 
"! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)" 

1162 
"associative fadd1" 

1163 
"associative fadd2" 

1164 
"! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)" 

1165 
"! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)" 

1166 
"! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)" 

35612  1167 
shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" 
27484  1168 
proof  
1169 
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 

1170 
have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n) x = foldseq fadd1 (% k. fmul2 (s k) x) n" 

35612  1171 
by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all) 
27484  1172 
have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n" 
35612  1173 
using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all) 
27484  1174 
let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))" 
35612  1175 
show ?thesis 
27484  1176 
apply (simp add: Rep_matrix_inject[THEN sym]) 
1177 
apply (rule ext)+ 

1178 
apply (simp add: mult_matrix_def) 

1179 
apply (simplesubst 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)"]) 

35612  1180 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 
1181 
apply (simplesubst 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)"]) 

1182 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 

27484  1183 
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) 
35612  1184 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 
27484  1185 
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) 
35612  1186 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 
27484  1187 
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) 
35612  1188 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 
27484  1189 
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"]) 
35612  1190 
apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+ 
27484  1191 
apply (simp add: mult_matrix_n_def) 
1192 
apply (rule comb_left) 

1193 
apply ((rule ext)+, simp) 

1194 
apply (simplesubst RepAbs_matrix) 

1195 
apply (rule exI[of _ "nrows B"]) 

35612  1196 
apply (simp add: nrows assms foldseq_zero) 
27484  1197 
apply (rule exI[of _ "ncols C"]) 
35612  1198 
apply (simp add: assms ncols foldseq_zero) 
27484  1199 
apply (subst RepAbs_matrix) 
1200 
apply (rule exI[of _ "nrows A"]) 

35612  1201 
apply (simp add: nrows assms foldseq_zero) 
27484  1202 
apply (rule exI[of _ "ncols B"]) 
35612  1203 
apply (simp add: assms ncols foldseq_zero) 
1204 
apply (simp add: fmul2fadd1fold fmul1fadd2fold assms) 

27484  1205 
apply (subst foldseq_foldseq) 
35612  1206 
apply (simp add: assms)+ 
1207 
apply (simp add: transpose_infmatrix) 

1208 
done 

27484  1209 
qed 
1210 

1211 
lemma 

35612  1212 
assumes 
27484  1213 
"! a. fmul1 0 a = 0" 
1214 
"! a. fmul1 a 0 = 0" 

1215 
"! a. fmul2 0 a = 0" 

1216 
"! a. fmul2 a 0 = 0" 

1217 
"fadd1 0 0 = 0" 

1218 
"fadd2 0 0 = 0" 

1219 
"! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)" 

1220 
"associative fadd1" 

1221 
"associative fadd2" 

1222 
"! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)" 

1223 
"! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)" 

1224 
"! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)" 

1225 
shows 

1226 
"(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)" 

1227 
apply (rule ext)+ 

1228 
apply (simp add: comp_def ) 

35612  1229 
apply (simp add: mult_matrix_assoc assms) 
1230 
done 

27484  1231 

1232 
lemma mult_matrix_assoc_simple: 

35612  1233 
assumes 
27484  1234 
"! a. fmul 0 a = 0" 
1235 
"! a. fmul a 0 = 0" 

1236 
"fadd 0 0 = 0" 

1237 
"associative fadd" 

1238 
"commutative fadd" 

1239 
"associative fmul" 

1240 
"distributive fmul fadd" 

35612  1241 
shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" 
27484  1242 
proof  
1243 
have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)" 

35612  1244 
using assms by (simp add: associative_def commutative_def) 
1245 
then show ?thesis 

27484  1246 
apply (subst mult_matrix_assoc) 
35612  1247 
using assms 
1248 
apply simp_all 

1249 
apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def) 

1250 
done 

27484  1251 
qed 
1252 

1253 
lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)" 

1254 
apply (simp add: Rep_matrix_inject[THEN sym]) 

1255 
apply (rule ext)+ 

1256 
by simp 

1257 

1258 
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)" 

1259 
apply (simp add: Rep_matrix_inject[THEN sym]) 

1260 
apply (rule ext)+ 

1261 
by simp 

1262 

1263 
lemma Rep_mult_matrix: 

1264 
assumes 

1265 
"! a. fmul 0 a = 0" 

1266 
"! a. fmul a 0 = 0" 

1267 
"fadd 0 0 = 0" 

1268 
shows 

1269 
"Rep_matrix(mult_matrix fmul fadd A B) j i = 

1270 
foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))" 

1271 
apply (simp add: mult_matrix_def mult_matrix_n_def) 

1272 
apply (subst RepAbs_matrix) 

35612  1273 
apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero) 
1274 
apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero) 

1275 
apply simp 

1276 
done 

27484  1277 

1278 
lemma transpose_mult_matrix: 

1279 
assumes 

1280 
"! a. fmul 0 a = 0" 

1281 
"! a. fmul a 0 = 0" 

1282 
"fadd 0 0 = 0" 

1283 
"! x y. fmul y x = fmul x y" 

1284 
shows 

1285 
"transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)" 

1286 
apply (simp add: Rep_matrix_inject[THEN sym]) 
