1 (* Title: HOL/Matrix/MatrixGeneral.thy |
1 (* Title: HOL/Matrix/MatrixGeneral.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua |
3 Author: Steven Obua |
4 License: 2004 Technische UniversitÃ\<currency>t MÃ\<onequarter>nchen |
4 License: 2004 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 theory MatrixGeneral = Main: |
7 theory MatrixGeneral = Main: |
8 |
8 |
9 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a" |
9 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a" |
10 |
10 |
11 constdefs |
11 constdefs |
12 nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set" |
12 nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set" |
13 "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}" |
13 "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}" |
14 |
14 |
15 typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}" |
15 typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}" |
16 apply (rule_tac x="(% j i. 0)" in exI) |
16 apply (rule_tac x="(% j i. 0)" in exI) |
17 by (simp add: nonzero_positions_def) |
17 by (simp add: nonzero_positions_def) |
18 |
18 |
19 declare Rep_matrix_inverse[simp] |
19 declare Rep_matrix_inverse[simp] |
20 |
20 |
21 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))" |
21 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))" |
22 apply (rule Abs_matrix_induct) |
22 apply (rule Abs_matrix_induct) |
23 by (simp add: Abs_matrix_inverse matrix_def) |
23 by (simp add: Abs_matrix_inverse matrix_def) |
24 |
24 |
25 constdefs |
25 constdefs |
26 nrows :: "('a::zero) matrix \<Rightarrow> nat" |
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))))" |
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" |
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))))" |
29 "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))" |
30 |
30 |
31 lemma nrows: |
31 lemma nrows: |
32 assumes hyp: "nrows A \<le> m" |
32 assumes hyp: "nrows A \<le> m" |
33 shows "(Rep_matrix A m n) = 0" (is ?concl) |
33 shows "(Rep_matrix A m n) = 0" (is ?concl) |
34 proof cases |
34 proof cases |
35 assume "nonzero_positions(Rep_matrix A) = {}" |
35 assume "nonzero_positions(Rep_matrix A) = {}" |
36 then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def) |
36 then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def) |
37 next |
37 next |
38 assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}" |
38 assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}" |
39 let ?S = "fst`(nonzero_positions(Rep_matrix A))" |
39 let ?S = "fst`(nonzero_positions(Rep_matrix A))" |
40 from a have b: "?S \<noteq> {}" by (simp) |
40 from a have b: "?S \<noteq> {}" by (simp) |
41 have c: "finite (?S)" by (simp add: finite_nonzero_positions) |
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) |
42 from hyp have d: "Max (?S) < m" by (simp add: a nrows_def) |
43 have "m \<notin> ?S" |
43 have "m \<notin> ?S" |
44 proof - |
44 proof - |
45 have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max[OF c b]) |
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) |
46 moreover from d have "~(m <= Max ?S)" by (simp) |
47 ultimately show "m \<notin> ?S" by (auto) |
47 ultimately show "m \<notin> ?S" by (auto) |
48 qed |
48 qed |
49 thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect) |
49 thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect) |
50 qed |
50 qed |
51 text {* \matrix cool *} |
51 |
52 constdefs |
52 constdefs |
53 transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix" |
53 transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix" |
54 "transpose_infmatrix A j i == A i j" |
54 "transpose_infmatrix A j i == A i j" |
55 transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix" |
55 transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix" |
56 "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix" |
56 "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix" |
62 |
62 |
63 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)" |
63 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)" |
64 apply (rule ext)+ |
64 apply (rule ext)+ |
65 by (simp add: transpose_infmatrix_def) |
65 by (simp add: transpose_infmatrix_def) |
66 |
66 |
67 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)" |
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) |
68 apply (rule Abs_matrix_inverse) |
69 apply (simp add: matrix_def nonzero_positions_def image_def) |
69 apply (simp add: matrix_def nonzero_positions_def image_def) |
70 proof - |
70 proof - |
71 let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}" |
71 let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}" |
72 let ?swap = "% pos. (snd pos, fst pos)" |
72 let ?swap = "% pos. (snd pos, fst pos)" |
73 let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}" |
73 let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}" |
74 have swap_image: "?swap`?A = ?B" |
74 have swap_image: "?swap`?A = ?B" |
75 apply (simp add: image_def) |
75 apply (simp add: image_def) |
76 apply (rule set_ext) |
76 apply (rule set_ext) |
77 apply (simp) |
77 apply (simp) |
78 proof |
78 proof |
79 fix y |
79 fix y |
80 assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)" |
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" |
81 thus "Rep_matrix x (fst y) (snd y) \<noteq> 0" |
82 proof - |
82 proof - |
83 from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast |
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) |
84 then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp) |
85 qed |
85 qed |
86 next |
86 next |
87 fix y |
87 fix y |
88 assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0" |
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) |
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 |
90 qed |
91 then have "finite (?swap`?A)" |
91 then have "finite (?swap`?A)" |
92 proof - |
92 proof - |
93 have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions) |
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) |
94 then have "finite ?B" by (simp add: nonzero_positions_def) |
95 with swap_image show "finite (?swap`?A)" by (simp) |
95 with swap_image show "finite (?swap`?A)" by (simp) |
96 qed |
96 qed |
97 moreover |
97 moreover |
98 have "inj_on ?swap ?A" by (simp add: inj_on_def) |
98 have "inj_on ?swap ?A" by (simp add: inj_on_def) |
99 ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A]) |
99 ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A]) |
100 qed |
100 qed |
101 |
101 |
102 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j" |
102 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j" |
103 by (simp add: transpose_matrix_def) |
103 by (simp add: transpose_matrix_def) |
104 |
104 |
105 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A" |
105 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A" |
106 by (simp add: transpose_matrix_def) |
106 by (simp add: transpose_matrix_def) |
107 |
107 |
108 lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A" |
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) |
109 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def) |
110 |
110 |
111 lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A" |
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) |
112 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def) |
113 |
113 |
114 lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0" |
114 lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0" |
115 proof - |
115 proof - |
116 assume "ncols A <= n" |
116 assume "ncols A <= n" |
117 then have "nrows (transpose_matrix A) <= n" by (simp) |
117 then have "nrows (transpose_matrix A) <= n" by (simp) |
118 then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows) |
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) |
119 thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def) |
120 qed |
120 qed |
121 |
121 |
122 lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st") |
122 lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st") |
192 fix m::nat |
192 fix m::nat |
193 let ?s0 = "{pos. fst pos < m & snd pos < n}" |
193 let ?s0 = "{pos. fst pos < m & snd pos < n}" |
194 let ?s1 = "{pos. fst pos < (Suc 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}" |
195 let ?sd = "{pos. fst pos = m & snd pos < n}" |
196 assume f0: "finite ?s0" |
196 assume f0: "finite ?s0" |
197 have f1: "finite ?sd" |
197 have f1: "finite ?sd" |
198 proof - |
198 proof - |
199 let ?f = "% x. (m, x)" |
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) |
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) |
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) |
202 ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp) |
203 qed |
203 qed |
204 have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith) |
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) |
205 from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI) |
206 with su show "finite ?s1" by (simp) |
206 with su show "finite ?s1" by (simp) |
207 qed |
207 qed |
208 |
208 |
209 lemma RepAbs_matrix: |
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) |
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" |
211 shows "(Rep_matrix (Abs_matrix x)) = x" |
212 apply (rule Abs_matrix_inverse) |
212 apply (rule Abs_matrix_inverse) |
213 apply (simp add: matrix_def nonzero_positions_def) |
213 apply (simp add: matrix_def nonzero_positions_def) |
214 proof - |
214 proof - |
215 from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast) |
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) |
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}" |
217 let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}" |
218 let ?v = "{pos. fst pos < m & snd pos < n}" |
218 let ?v = "{pos. fst pos < m & snd pos < n}" |
219 have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith) |
219 have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith) |
220 from a b have "(?u \<inter> (-?v)) = {}" |
220 from a b have "(?u \<inter> (-?v)) = {}" |
221 apply (simp) |
221 apply (simp) |
222 apply (rule set_ext) |
222 apply (rule set_ext) |
223 apply (simp) |
223 apply (simp) |
224 apply auto |
224 apply auto |
226 then have d: "?u \<subseteq> ?v" by blast |
226 then have d: "?u \<subseteq> ?v" by blast |
227 moreover have "finite ?v" by (simp add: finite_natarray2) |
227 moreover have "finite ?v" by (simp add: finite_natarray2) |
228 ultimately show "finite ?u" by (rule finite_subset) |
228 ultimately show "finite ?u" by (rule finite_subset) |
229 qed |
229 qed |
230 |
230 |
231 constdefs |
231 constdefs |
232 apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" |
232 apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" |
233 "apply_infmatrix f == % A. (% j i. f (A j i))" |
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" |
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))" |
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" |
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))" |
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" |
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))" |
239 "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))" |
240 |
240 |
241 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)" |
241 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)" |
242 by (simp add: apply_infmatrix_def) |
242 by (simp add: apply_infmatrix_def) |
243 |
243 |
244 lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)" |
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) |
245 by (simp add: combine_infmatrix_def) |
246 |
246 |
247 constdefs |
247 constdefs |
248 commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" |
248 commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" |
249 "commutative f == ! x y. f x y = f y x" |
249 "commutative f == ! x y. f x y = f y x" |
250 associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" |
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)" |
251 "associative f == ! x y z. f (f x y) z = f x (f y z)" |
252 |
252 |
253 text{* |
253 text{* |
254 To reason about associativity and commutativity of operations on matrices, |
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 |
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. |
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$. |
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.$ |
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 *} |
259 *} |
260 |
260 |
261 lemma combine_infmatrix_commute: |
261 lemma combine_infmatrix_commute: |
262 "commutative f \<Longrightarrow> commutative (combine_infmatrix f)" |
262 "commutative f \<Longrightarrow> commutative (combine_infmatrix f)" |
263 by (simp add: commutative_def combine_infmatrix_def) |
263 by (simp add: commutative_def combine_infmatrix_def) |
264 |
264 |
265 lemma combine_matrix_commute: |
265 lemma combine_matrix_commute: |
266 "commutative f \<Longrightarrow> commutative (combine_matrix f)" |
266 "commutative f \<Longrightarrow> commutative (combine_matrix f)" |
267 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def) |
267 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def) |
268 |
268 |
269 text{* |
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\}$, |
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 |
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, \] |
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 |
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.\] |
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: |
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: |
347 "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))" |
347 "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))" |
348 |
348 |
349 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f" |
349 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f" |
350 proof - |
350 proof - |
351 assume a:"associative f" |
351 assume a:"associative f" |
352 then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" |
352 then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" |
353 proof - |
353 proof - |
354 fix n |
354 fix n |
355 show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" |
355 show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" |
356 proof (induct n) |
356 proof (induct n) |
357 show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp |
357 show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp |
358 next |
358 next |
359 fix n |
359 fix n |
360 assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s 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) |
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" |
362 show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N" |
363 proof (auto) |
363 proof (auto) |
364 fix N t |
364 fix N t |
365 assume Nsuc: "N <= Suc n" |
365 assume Nsuc: "N <= Suc n" |
366 show "foldseq f t N = foldseq_transposed f t N" |
366 show "foldseq f t N = foldseq_transposed f t N" |
367 proof cases |
367 proof cases |
368 assume "N <= n" |
368 assume "N <= n" |
369 then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b) |
369 then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b) |
370 next |
370 next |
371 assume "~(N <= n)" |
371 assume "~(N <= n)" |
372 with Nsuc have Nsuceq: "N = Suc n" by simp |
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 |
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) |
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" |
375 show "foldseq f t N = foldseq_transposed f t N" |
376 apply (simp add: Nsuceq) |
376 apply (simp add: Nsuceq) |
377 apply (subst c) |
377 apply (subst c) |
378 apply (simp) |
378 apply (simp) |
379 apply (case_tac "n = 0") |
379 apply (case_tac "n = 0") |
380 apply (simp) |
380 apply (simp) |
381 apply (drule neqz) |
381 apply (drule neqz) |
382 apply (erule exE) |
382 apply (erule exE) |
383 apply (simp) |
383 apply (simp) |
384 apply (subst assocf) |
384 apply (subst assocf) |
385 proof - |
385 proof - |
386 fix m |
386 fix m |
387 assume "n = Suc m & Suc m <= n" |
387 assume "n = Suc m & Suc m <= n" |
388 then have mless: "Suc m <= n" by arith |
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") |
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) |
390 apply (subst c) |
391 by simp+ |
391 by simp+ |
392 have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") 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") |
393 have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4") |
394 apply (subst c) |
394 apply (subst c) |
395 by (simp add: mless)+ |
395 by (simp add: mless)+ |
396 have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp |
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 |
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 |
398 qed |
399 qed |
399 qed |
400 qed |
400 qed |
401 qed |
401 qed |
402 qed |
402 qed |
403 show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto) |
403 show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto) |
404 qed |
404 qed |
405 |
405 |
433 x: a1 |
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)) |
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)) |
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 *) |
436 *) |
437 |
437 |
438 lemma foldseq_zero: |
438 lemma foldseq_zero: |
439 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0" |
439 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0" |
440 shows "foldseq f s n = 0" |
440 shows "foldseq f s n = 0" |
441 proof - |
441 proof - |
442 have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0" |
442 have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0" |
443 apply (induct_tac n) |
443 apply (induct_tac n) |
444 apply (simp) |
444 apply (simp) |
445 by (simp add: fz) |
445 by (simp add: fz) |
446 then show "foldseq f s n = 0" by (simp add: sz) |
446 then show "foldseq f s n = 0" by (simp add: sz) |
447 qed |
447 qed |
448 |
448 |
449 lemma foldseq_significant_positions: |
449 lemma foldseq_significant_positions: |
450 assumes p: "! i. i <= N \<longrightarrow> S i = T i" |
450 assumes p: "! i. i <= N \<longrightarrow> S i = T i" |
451 shows "foldseq f S N = foldseq f T N" (is ?concl) |
451 shows "foldseq f S N = foldseq f T N" (is ?concl) |
452 proof - |
452 proof - |
453 have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m" |
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) |
454 apply (induct_tac m) |
455 apply (simp) |
455 apply (simp) |
456 apply (simp) |
456 apply (simp) |
457 apply (auto) |
457 apply (auto) |
458 proof - |
458 proof - |
459 fix n |
459 fix n |
460 fix s::"nat\<Rightarrow>'a" |
460 fix s::"nat\<Rightarrow>'a" |
461 fix t::"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" |
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" |
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 |
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) |
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) |
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 |
467 qed |
468 with p show ?concl by simp |
468 with p show ?concl by simp |
469 qed |
469 qed |
470 |
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") |
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 - |
472 proof - |
473 have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith |
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 |
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 |
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 |
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" |
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) |
478 apply (induct_tac n) |
479 apply (simp) |
479 apply (simp) |
480 apply (simp) |
480 apply (simp) |
481 apply (auto) |
481 apply (auto) |
482 apply (case_tac "m = Suc na") |
482 apply (case_tac "m = Suc na") |
483 apply (simp) |
483 apply (simp) |
484 apply (rule a) |
484 apply (rule a) |
485 apply (rule foldseq_significant_positions) |
485 apply (rule foldseq_significant_positions) |
486 apply (simp, auto) |
486 apply (simp, auto) |
487 apply (drule eq, simp+) |
487 apply (drule eq, simp+) |
488 apply (drule suc, simp+) |
488 apply (drule suc, simp+) |
489 proof - |
489 proof - |
490 fix na m s |
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" |
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" |
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 |
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 = |
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" |
495 foldseq f (% k. s(Suc k)) na" |
496 by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb) |
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 |
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) = |
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" |
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) |
500 apply (simp add: subd) |
501 apply (case_tac "m=0") |
501 apply (case_tac "m=0") |
502 apply (simp) |
502 apply (simp) |
503 apply (drule sube) |
503 apply (drule sube) |
504 apply (auto) |
504 apply (auto) |
505 apply (rule a) |
505 apply (rule a) |
506 by (simp add: subc if_def) |
506 by (simp add: subc if_def) |
507 qed |
507 qed |
508 then show "?p \<Longrightarrow> ?concl" by simp |
508 then show "?p \<Longrightarrow> ?concl" by simp |
509 qed |
509 qed |
510 |
510 |
511 lemma foldseq_zerotail: |
511 lemma foldseq_zerotail: |
512 assumes |
512 assumes |
513 fz: "f 0 0 = 0" |
513 fz: "f 0 0 = 0" |
514 and sz: "! i. n <= i \<longrightarrow> s i = 0" |
514 and sz: "! i. n <= i \<longrightarrow> s i = 0" |
515 and nm: "n <= m" |
515 and nm: "n <= m" |
516 shows |
516 shows |
517 "foldseq f s n = foldseq f s m" |
517 "foldseq f s n = foldseq f s m" |
518 proof - |
518 proof - |
519 have a: "!! a b. ~(a < b) \<Longrightarrow> a <= b \<Longrightarrow> (a::nat) = b" by simp |
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" |
520 show "foldseq f s n = foldseq f s m" |
521 apply (simp add: foldseq_tail[OF nm, of f s]) |
521 apply (simp add: foldseq_tail[OF nm, of f s]) |
522 apply (rule foldseq_significant_positions) |
522 apply (rule foldseq_significant_positions) |
570 have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp |
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)))" |
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 |
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" |
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)))" |
574 show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))" |
575 apply (subst a) |
575 apply (subst a) |
576 apply (subst c) |
576 apply (subst c) |
577 by (simp add: d f00x)+ |
577 by (simp add: d f00x)+ |
578 qed |
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 |
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 |
580 qed |
581 |
581 |
582 lemma foldseq_zerostart2: |
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" |
583 "! x. f 0 x = x \<Longrightarrow> ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n" |
584 proof - |
584 proof - |
585 assume a:"! i. i<n \<longrightarrow> s i = 0" |
585 assume a:"! i. i<n \<longrightarrow> s i = 0" |
586 assume x:"! x. f 0 x = x" |
586 assume x:"! x. f 0 x = x" |
587 from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast |
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 |
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 |
589 have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith |
590 show "foldseq f s n = s n" |
590 show "foldseq f s n = s n" |
591 apply (case_tac "n=0") |
591 apply (case_tac "n=0") |
592 apply (simp) |
592 apply (simp) |
593 apply (insert a) |
593 apply (insert a) |
594 apply (drule d) |
594 apply (drule d) |
595 apply (auto) |
595 apply (auto) |
596 apply (simp add: b) |
596 apply (simp add: b) |
597 apply (insert f00x) |
597 apply (insert f00x) |
598 apply (drule foldseq_zerostart) |
598 apply (drule foldseq_zerostart) |
599 by (simp add: x)+ |
599 by (simp add: x)+ |
600 qed |
600 qed |
601 |
601 |
602 lemma foldseq_almostzero: |
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" |
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) |
604 shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl) |
605 proof - |
605 proof - |
606 from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp |
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 |
607 from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp |
608 show ?concl |
608 show ?concl |
609 apply auto |
609 apply auto |
610 apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym]) |
610 apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym]) |
611 apply simp |
611 apply simp |
612 apply (subst foldseq_zerostart2) |
612 apply (subst foldseq_zerostart2) |
627 apply (drule_tac x="% k. s (Suc k)" in spec) |
627 apply (drule_tac x="% k. s (Suc k)" in spec) |
628 by (simp add: prems) |
628 by (simp add: prems) |
629 then show ?concl by simp |
629 then show ?concl by simp |
630 qed |
630 qed |
631 |
631 |
632 constdefs |
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" |
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)" |
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" |
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" |
636 "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B" |
637 |
637 |
638 lemma mult_matrix_n: |
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" |
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) |
640 shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl) |
641 proof - |
641 proof - |
642 show ?concl using prems |
642 show ?concl using prems |
643 apply (simp add: mult_matrix_def mult_matrix_n_def) |
643 apply (simp add: mult_matrix_def mult_matrix_n_def) |
644 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) |
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) |
645 by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems) |
646 qed |
646 qed |
647 |
647 |
648 lemma mult_matrix_nm: |
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" |
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" |
650 shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" |
651 proof - |
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) |
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]) |
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 |
654 finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp |
655 qed |
655 qed |
656 |
656 |
657 constdefs |
657 constdefs |
658 r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" |
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)" |
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" |
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)" |
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" |
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" |
663 "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd" |
664 |
664 |
665 lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith) |
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) |
666 lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith) |
667 |
667 |
668 lemma r_distributive_matrix: |
668 lemma r_distributive_matrix: |
669 assumes prems: |
669 assumes prems: |
670 "r_distributive fmul fadd" |
670 "r_distributive fmul fadd" |
671 "associative fadd" |
671 "associative fadd" |
672 "commutative fadd" |
672 "commutative fadd" |
673 "fadd 0 0 = 0" |
673 "fadd 0 0 = 0" |
674 "! a. fmul a 0 = 0" |
674 "! a. fmul a 0 = 0" |
675 "! a. fmul 0 a = 0" |
675 "! a. fmul 0 a = 0" |
676 shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) |
676 shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) |
677 proof - |
677 proof - |
678 from prems show ?concl |
678 from prems show ?concl |
679 apply (simp add: r_distributive_def mult_matrix_def, auto) |
679 apply (simp add: r_distributive_def mult_matrix_def, auto) |
680 proof - |
680 proof - |
681 fix a::"'a matrix" |
681 fix a::"'a matrix" |
682 fix u::"'b matrix" |
682 fix u::"'b matrix" |
683 fix v::"'b matrix" |
683 fix v::"'b matrix" |
684 let ?mx = "max (ncols a) (max (nrows u) (nrows v))" |
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) = |
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)" |
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]) |
687 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
688 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
688 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
689 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
689 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
690 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
690 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
691 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
691 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
692 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
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]) |
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) |
694 apply (simp add: combine_matrix_def combine_infmatrix_def) |
695 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) |
695 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) |
696 apply (subst RepAbs_matrix) |
696 apply (subst RepAbs_matrix) |
697 apply (simp, auto) |
697 apply (simp, auto) |
698 apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero) |
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) |
699 apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero) |
700 apply (subst RepAbs_matrix) |
700 apply (subst RepAbs_matrix) |
701 apply (simp, auto) |
701 apply (simp, auto) |
702 apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero) |
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) |
703 apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero) |
704 done |
704 done |
705 qed |
705 qed |
706 qed |
706 qed |
707 |
707 |
708 lemma l_distributive_matrix: |
708 lemma l_distributive_matrix: |
709 assumes prems: |
709 assumes prems: |
710 "l_distributive fmul fadd" |
710 "l_distributive fmul fadd" |
711 "associative fadd" |
711 "associative fadd" |
712 "commutative fadd" |
712 "commutative fadd" |
713 "fadd 0 0 = 0" |
713 "fadd 0 0 = 0" |
714 "! a. fmul a 0 = 0" |
714 "! a. fmul a 0 = 0" |
715 "! a. fmul 0 a = 0" |
715 "! a. fmul 0 a = 0" |
716 shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) |
716 shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl) |
717 proof - |
717 proof - |
718 from prems show ?concl |
718 from prems show ?concl |
719 apply (simp add: l_distributive_def mult_matrix_def, auto) |
719 apply (simp add: l_distributive_def mult_matrix_def, auto) |
720 proof - |
720 proof - |
721 fix a::"'b matrix" |
721 fix a::"'b matrix" |
722 fix u::"'a matrix" |
722 fix u::"'a matrix" |
723 fix v::"'a matrix" |
723 fix v::"'a matrix" |
724 let ?mx = "max (nrows a) (max (ncols u) (ncols v))" |
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 = |
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)" |
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]) |
727 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
728 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
728 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
729 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
729 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
730 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
730 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
731 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
731 apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul]) |
732 apply (simp add: max1 max2 combine_nrows combine_ncols)+ |
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]) |
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) |
734 apply (simp add: combine_matrix_def combine_infmatrix_def) |
735 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) |
735 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+) |
736 apply (subst RepAbs_matrix) |
736 apply (subst RepAbs_matrix) |
737 apply (simp, auto) |
737 apply (simp, auto) |
738 apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero) |
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) |
739 apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero) |
740 apply (subst RepAbs_matrix) |
740 apply (subst RepAbs_matrix) |
741 apply (simp, auto) |
741 apply (simp, auto) |
742 apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero) |
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) |
743 apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero) |
744 done |
744 done |
745 qed |
745 qed |
746 qed |
746 qed |
747 |
747 |
748 |
748 |
749 instance matrix :: (zero)zero by intro_classes |
749 instance matrix :: (zero)zero by intro_classes |
750 |
750 |
751 defs(overloaded) |
751 defs(overloaded) |
752 zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)" |
752 zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)" |
753 |
753 |
754 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0" |
754 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0" |
755 apply (simp add: zero_matrix_def) |
755 apply (simp add: zero_matrix_def) |
756 apply (subst RepAbs_matrix) |
756 apply (subst RepAbs_matrix) |
757 by (auto) |
757 by (auto) |
868 apply (subst RepAbs_matrix) |
868 apply (subst RepAbs_matrix) |
869 apply (rule exI[of _ "Suc j"], simp) |
869 apply (rule exI[of _ "Suc j"], simp) |
870 apply (rule exI[of _ "Suc i"], simp) |
870 apply (rule exI[of _ "Suc i"], simp) |
871 by simp |
871 by simp |
872 |
872 |
873 lemma Rep_move_matrix[simp]: |
873 lemma Rep_move_matrix[simp]: |
874 "Rep_matrix (move_matrix A y x) j i = |
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)))" |
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) |
876 apply (simp add: move_matrix_def) |
877 apply (auto) |
877 apply (auto) |
878 by (subst RepAbs_matrix, |
878 by (subst RepAbs_matrix, |
879 rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith, |
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)+ |
880 rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+ |
881 |
881 |
882 lemma Rep_take_columns[simp]: |
882 lemma Rep_take_columns[simp]: |
883 "Rep_matrix (take_columns A c) j i = |
883 "Rep_matrix (take_columns A c) j i = |
884 (if i < c then (Rep_matrix A j i) else 0)" |
884 (if i < c then (Rep_matrix A j i) else 0)" |
885 apply (simp add: take_columns_def) |
885 apply (simp add: take_columns_def) |
886 apply (subst RepAbs_matrix) |
886 apply (subst RepAbs_matrix) |
887 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) |
887 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) |
888 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) |
888 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) |
889 done |
889 done |
890 |
890 |
891 lemma Rep_take_rows[simp]: |
891 lemma Rep_take_rows[simp]: |
892 "Rep_matrix (take_rows A r) j i = |
892 "Rep_matrix (take_rows A r) j i = |
893 (if j < r then (Rep_matrix A j i) else 0)" |
893 (if j < r then (Rep_matrix A j i) else 0)" |
894 apply (simp add: take_rows_def) |
894 apply (simp add: take_rows_def) |
895 apply (subst RepAbs_matrix) |
895 apply (subst RepAbs_matrix) |
896 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) |
896 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le) |
897 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) |
897 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le) |
898 done |
898 done |
971 |
971 |
972 constdefs |
972 constdefs |
973 foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" |
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" |
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" |
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" |
976 "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m" |
977 |
977 |
978 lemma foldmatrix_transpose: |
978 lemma foldmatrix_transpose: |
979 assumes |
979 assumes |
980 "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" |
980 "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" |
981 shows |
981 shows |
982 "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl) |
982 "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl) |
983 proof - |
983 proof - |
984 have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto |
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" |
985 have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1" |
986 apply (induct n) |
986 apply (induct n) |
987 apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+ |
987 apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+ |
988 apply (auto) |
988 apply (auto) |
989 by (drule_tac x1="(% j i. A j (Suc i))" in forall, simp) |
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" |
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) |
991 apply (simp add: foldmatrix_def foldmatrix_transposed_def) |
992 apply (induct m, simp) |
992 apply (induct m, simp) |
993 apply (simp) |
993 apply (simp) |
994 apply (insert tworows) |
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) |
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) |
996 by (simp add: foldmatrix_def foldmatrix_transposed_def) |
997 qed |
997 qed |
998 |
998 |
999 lemma foldseq_foldseq: |
999 lemma foldseq_foldseq: |
1000 assumes |
1000 assumes |
1001 "associative f" |
1001 "associative f" |
1002 "associative g" |
1002 "associative g" |
1003 "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" |
1003 "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" |
1004 shows |
1004 shows |
1005 "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n" |
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]) |
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) |
1007 by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems) |
1008 |
1008 |
1009 lemma mult_n_nrows: |
1009 lemma mult_n_nrows: |
1010 assumes |
1010 assumes |
1011 "! a. fmul 0 a = 0" |
1011 "! a. fmul 0 a = 0" |
1012 "! a. fmul a 0 = 0" |
1012 "! a. fmul a 0 = 0" |
1013 "fadd 0 0 = 0" |
1013 "fadd 0 0 = 0" |
1014 shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A" |
1014 shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A" |
1015 apply (subst nrows_le) |
1015 apply (subst nrows_le) |
1222 by (simp! add: le_matrix_def) |
1222 by (simp! add: le_matrix_def) |
1223 |
1223 |
1224 lemma le_left_combine_matrix: |
1224 lemma le_left_combine_matrix: |
1225 assumes |
1225 assumes |
1226 "f 0 0 = 0" |
1226 "f 0 0 = 0" |
1227 "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b" |
1227 "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b" |
1228 "0 <= C" |
1228 "0 <= C" |
1229 "A <= B" |
1229 "A <= B" |
1230 shows |
1230 shows |
1231 "combine_matrix f C A <= combine_matrix f C B" |
1231 "combine_matrix f C A <= combine_matrix f C B" |
1232 by (simp! add: le_matrix_def) |
1232 by (simp! add: le_matrix_def) |
1233 |
1233 |
1234 lemma le_right_combine_matrix: |
1234 lemma le_right_combine_matrix: |
1235 assumes |
1235 assumes |
1236 "f 0 0 = 0" |
1236 "f 0 0 = 0" |
1237 "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c" |
1237 "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c" |
1238 "0 <= C" |
1238 "0 <= C" |
1239 "A <= B" |
1239 "A <= B" |
1240 shows |
1240 shows |
1241 "combine_matrix f A C <= combine_matrix f B C" |
1241 "combine_matrix f A C <= combine_matrix f B C" |
1242 by (simp! add: le_matrix_def) |
1242 by (simp! add: le_matrix_def) |
1243 |
1243 |
1244 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)" |
1244 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)" |
1245 by (simp add: le_matrix_def, auto) |
1245 by (simp add: le_matrix_def, auto) |
1246 |
1246 |
1247 lemma le_foldseq: |
1247 lemma le_foldseq: |
1248 assumes |
1248 assumes |
1249 "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d" |
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" |
1250 "! i. i <= n \<longrightarrow> s i <= t i" |
1251 shows |
1251 shows |
1252 "foldseq f s n <= foldseq f t n" |
1252 "foldseq f s n <= foldseq f t n" |
1253 proof - |
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!) |
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!) |
1255 then show "foldseq f s n <= foldseq f t n" by (simp!) |
1256 qed |
1256 qed |
1257 |
1257 |
1258 lemma le_left_mult: |
1258 lemma le_left_mult: |
1259 assumes |
1259 assumes |
1260 "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d" |
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" |
1261 "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b" |
1262 "! a. fmul 0 a = 0" |
1262 "! a. fmul 0 a = 0" |
1263 "! a. fmul a 0 = 0" |
1263 "! a. fmul a 0 = 0" |
1264 "fadd 0 0 = 0" |
1264 "fadd 0 0 = 0" |
1265 "0 <= C" |
1265 "0 <= C" |
1266 "A <= B" |
1266 "A <= B" |
1267 shows |
1267 shows |
1268 "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B" |
1268 "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B" |
1269 apply (simp! add: le_matrix_def Rep_mult_matrix) |
1269 apply (simp! add: le_matrix_def Rep_mult_matrix) |