src/HOL/Matrix_LP/Matrix.thy
 author blanchet Wed Feb 12 08:35:57 2014 +0100 (2014-02-12) changeset 55415 05f5fdb8d093 parent 54864 a064732223ad child 57512 cc97b347b301 permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
 wenzelm@47455  1 (* Title: HOL/Matrix_LP/Matrix.thy  obua@14593  2  Author: Steven Obua  obua@14593  3 *)  obua@14593  4 wenzelm@17915  5 theory Matrix  wenzelm@41413  6 imports Main "~~/src/HOL/Library/Lattice_Algebras"  wenzelm@17915  7 begin  obua@14940  8 wenzelm@42463  9 type_synonym 'a infmatrix = "nat \ nat \ 'a"  haftmann@27484  10 huffman@44174  11 definition nonzero_positions :: "(nat \ nat \ 'a::zero) \ (nat \ nat) set" where  haftmann@27484  12  "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"  haftmann@27484  13 wenzelm@45694  14 definition "matrix = {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}"  wenzelm@45694  15 wenzelm@49834  16 typedef 'a matrix = "matrix :: (nat \ nat \ 'a::zero) set"  wenzelm@45694  17  unfolding matrix_def  wenzelm@45694  18 proof  wenzelm@45694  19  show "(\j i. 0) \ {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}"  haftmann@27484  20  by (simp add: nonzero_positions_def)  haftmann@27484  21 qed  haftmann@27484  22 haftmann@27484  23 declare Rep_matrix_inverse[simp]  haftmann@27484  24 haftmann@27484  25 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"  wenzelm@45694  26  by (induct A) (simp add: Abs_matrix_inverse matrix_def)  haftmann@27484  27 haftmann@35416  28 definition nrows :: "('a::zero) matrix \ nat" where  haftmann@27484  29  "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"  haftmann@35416  30 haftmann@35416  31 definition ncols :: "('a::zero) matrix \ nat" where  haftmann@27484  32  "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"  haftmann@27484  33 haftmann@27484  34 lemma nrows:  haftmann@27484  35  assumes hyp: "nrows A \ m"  wenzelm@35612  36  shows "(Rep_matrix A m n) = 0"  haftmann@27484  37 proof cases  haftmann@27484  38  assume "nonzero_positions(Rep_matrix A) = {}"  haftmann@27484  39  then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)  haftmann@27484  40 next  haftmann@27484  41  assume a: "nonzero_positions(Rep_matrix A) \ {}"  haftmann@27484  42  let ?S = "fst(nonzero_positions(Rep_matrix A))"  haftmann@27484  43  have c: "finite (?S)" by (simp add: finite_nonzero_positions)  haftmann@27484  44  from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)  haftmann@27484  45  have "m \ ?S"  haftmann@27484  46  proof -  haftmann@27484  47  have "m \ ?S \ m <= Max(?S)" by (simp add: Max_ge [OF c])  haftmann@27484  48  moreover from d have "~(m <= Max ?S)" by (simp)  haftmann@27484  49  ultimately show "m \ ?S" by (auto)  haftmann@27484  50  qed  haftmann@27484  51  thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)  haftmann@27484  52 qed  haftmann@27484  53 haftmann@35416  54 definition transpose_infmatrix :: "'a infmatrix \ 'a infmatrix" where  haftmann@27484  55  "transpose_infmatrix A j i == A i j"  haftmann@35416  56 haftmann@35416  57 definition transpose_matrix :: "('a::zero) matrix \ 'a matrix" where  haftmann@27484  58  "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"  haftmann@27484  59 haftmann@27484  60 declare transpose_infmatrix_def[simp]  haftmann@27484  61 haftmann@27484  62 lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"  haftmann@27484  63 by ((rule ext)+, simp)  haftmann@27484  64 haftmann@27484  65 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"  haftmann@27484  66  apply (rule ext)+  wenzelm@46985  67  by simp  haftmann@27484  68 haftmann@27484  69 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"  haftmann@27484  70 apply (rule Abs_matrix_inverse)  haftmann@27484  71 apply (simp add: matrix_def nonzero_positions_def image_def)  haftmann@27484  72 proof -  haftmann@27484  73  let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \ 0}"  haftmann@27484  74  let ?swap = "% pos. (snd pos, fst pos)"  haftmann@27484  75  let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \ 0}"  haftmann@27484  76  have swap_image: "?swap?A = ?B"  haftmann@27484  77  apply (simp add: image_def)  nipkow@39302  78  apply (rule set_eqI)  haftmann@27484  79  apply (simp)  haftmann@27484  80  proof  haftmann@27484  81  fix y  haftmann@27484  82  assume hyp: "\a b. Rep_matrix x b a \ 0 \ y = (b, a)"  haftmann@27484  83  thus "Rep_matrix x (fst y) (snd y) \ 0"  haftmann@27484  84  proof -  haftmann@27484  85  from hyp obtain a b where "(Rep_matrix x b a \ 0 & y = (b,a))" by blast  haftmann@27484  86  then show "Rep_matrix x (fst y) (snd y) \ 0" by (simp)  haftmann@27484  87  qed  haftmann@27484  88  next  haftmann@27484  89  fix y  haftmann@27484  90  assume hyp: "Rep_matrix x (fst y) (snd y) \ 0"  haftmann@27484  91  show "\ a b. (Rep_matrix x b a \ 0 & y = (b,a))"  wenzelm@32960  92  by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)  haftmann@27484  93  qed  haftmann@27484  94  then have "finite (?swap?A)"  haftmann@27484  95  proof -  haftmann@27484  96  have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)  haftmann@27484  97  then have "finite ?B" by (simp add: nonzero_positions_def)  haftmann@27484  98  with swap_image show "finite (?swap?A)" by (simp)  haftmann@27484  99  qed  haftmann@27484  100  moreover  haftmann@27484  101  have "inj_on ?swap ?A" by (simp add: inj_on_def)  haftmann@27484  102  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])  haftmann@27484  103 qed  haftmann@27484  104 haftmann@27484  105 lemma infmatrixforward: "(x::'a infmatrix) = y \ \ a b. x a b = y a b" by auto  haftmann@27484  106 haftmann@27484  107 lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"  haftmann@27484  108 apply (auto)  haftmann@27484  109 apply (rule ext)+  haftmann@27484  110 apply (simp add: transpose_infmatrix)  haftmann@27484  111 apply (drule infmatrixforward)  haftmann@27484  112 apply (simp)  haftmann@27484  113 done  haftmann@27484  114 haftmann@27484  115 lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"  haftmann@27484  116 apply (simp add: transpose_matrix_def)  haftmann@27484  117 apply (subst Rep_matrix_inject[THEN sym])+  haftmann@27484  118 apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)  haftmann@27484  119 done  haftmann@27484  120 haftmann@27484  121 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"  haftmann@27484  122 by (simp add: transpose_matrix_def)  haftmann@27484  123 haftmann@27484  124 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"  haftmann@27484  125 by (simp add: transpose_matrix_def)  haftmann@27484  126 haftmann@27484  127 lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"  haftmann@27484  128 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)  haftmann@27484  129 haftmann@27484  130 lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"  haftmann@27484  131 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)  haftmann@27484  132 haftmann@27484  133 lemma ncols: "ncols A <= n \ Rep_matrix A m n = 0"  haftmann@27484  134 proof -  haftmann@27484  135  assume "ncols A <= n"  haftmann@27484  136  then have "nrows (transpose_matrix A) <= n" by (simp)  haftmann@27484  137  then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)  haftmann@27484  138  thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)  haftmann@27484  139 qed  haftmann@27484  140 haftmann@27484  141 lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \ (Rep_matrix A j i) = 0)" (is "_ = ?st")  haftmann@27484  142 apply (auto)  haftmann@27484  143 apply (simp add: ncols)  haftmann@27484  144 proof (simp add: ncols_def, auto)  haftmann@27484  145  let ?P = "nonzero_positions (Rep_matrix A)"  haftmann@27484  146  let ?p = "snd?P"  haftmann@27484  147  have a:"finite ?p" by (simp add: finite_nonzero_positions)  haftmann@27484  148  let ?m = "Max ?p"  haftmann@27484  149  assume "~(Suc (?m) <= n)"  haftmann@27484  150  then have b:"n <= ?m" by (simp)  haftmann@27484  151  fix a b  haftmann@27484  152  assume "(a,b) \ ?P"  haftmann@27484  153  then have "?p \ {}" by (auto)  haftmann@27484  154  with a have "?m \ ?p" by (simp)  haftmann@27484  155  moreover have "!x. (x \ ?p \ (? y. (Rep_matrix A y x) \ 0))" by (simp add: nonzero_positions_def image_def)  haftmann@27484  156  ultimately have "? y. (Rep_matrix A y ?m) \ 0" by (simp)  haftmann@27484  157  moreover assume ?st  haftmann@27484  158  ultimately show "False" using b by (simp)  haftmann@27484  159 qed  haftmann@27484  160 wenzelm@35612  161 lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \ 0)"  haftmann@27484  162 proof -  haftmann@27484  163  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith  wenzelm@35612  164  show ?thesis by (simp add: a ncols_le)  haftmann@27484  165 qed  haftmann@27484  166 wenzelm@35612  167 lemma le_ncols: "(n <= ncols A) = (\ m. (\ j i. m <= i \ (Rep_matrix A j i) = 0) \ n <= m)"  haftmann@27484  168 apply (auto)  haftmann@27484  169 apply (subgoal_tac "ncols A <= m")  haftmann@27484  170 apply (simp)  haftmann@27484  171 apply (simp add: ncols_le)  haftmann@27484  172 apply (drule_tac x="ncols A" in spec)  haftmann@27484  173 by (simp add: ncols)  haftmann@27484  174 haftmann@27484  175 lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \ (Rep_matrix A j i) = 0)" (is ?s)  haftmann@27484  176 proof -  haftmann@27484  177  have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)  haftmann@27484  178  also have "\ = (! j i. n <= i \ (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)  haftmann@27484  179  also have "\ = (! j i. n <= i \ (Rep_matrix A i j) = 0)" by (simp)  haftmann@27484  180  finally show "(nrows A <= n) = (! j i. n <= j \ (Rep_matrix A j i) = 0)" by (auto)  haftmann@27484  181 qed  haftmann@27484  182 wenzelm@35612  183 lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \ 0)"  haftmann@27484  184 proof -  haftmann@27484  185  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith  wenzelm@35612  186  show ?thesis by (simp add: a nrows_le)  haftmann@27484  187 qed  haftmann@27484  188 wenzelm@35612  189 lemma le_nrows: "(n <= nrows A) = (\ m. (\ j i. m <= j \ (Rep_matrix A j i) = 0) \ n <= m)"  haftmann@27484  190 apply (auto)  haftmann@27484  191 apply (subgoal_tac "nrows A <= m")  haftmann@27484  192 apply (simp)  haftmann@27484  193 apply (simp add: nrows_le)  haftmann@27484  194 apply (drule_tac x="nrows A" in spec)  haftmann@27484  195 by (simp add: nrows)  haftmann@27484  196 haftmann@27484  197 lemma nrows_notzero: "Rep_matrix A m n \ 0 \ m < nrows A"  haftmann@27484  198 apply (case_tac "nrows A <= m")  haftmann@27484  199 apply (simp_all add: nrows)  haftmann@27484  200 done  haftmann@27484  201 haftmann@27484  202 lemma ncols_notzero: "Rep_matrix A m n \ 0 \ n < ncols A"  haftmann@27484  203 apply (case_tac "ncols A <= n")  haftmann@27484  204 apply (simp_all add: ncols)  haftmann@27484  205 done  haftmann@27484  206 haftmann@27484  207 lemma finite_natarray1: "finite {x. x < (n::nat)}"  haftmann@27484  208 apply (induct n)  haftmann@27484  209 apply (simp)  haftmann@27484  210 proof -  haftmann@27484  211  fix n  nipkow@39302  212  have "{x. x < Suc n} = insert n {x. x < n}" by (rule set_eqI, simp, arith)  haftmann@27484  213  moreover assume "finite {x. x < n}"  haftmann@27484  214  ultimately show "finite {x. x < Suc n}" by (simp)  haftmann@27484  215 qed  haftmann@27484  216 bulwahn@50027  217 lemma finite_natarray2: "finite {(x, y). x < (m::nat) & y < (n::nat)}"  bulwahn@50027  218 by simp  haftmann@27484  219 haftmann@27484  220 lemma RepAbs_matrix:  haftmann@27484  221  assumes aem: "? m. ! j i. m <= j \ x j i = 0" (is ?em) and aen:"? n. ! j i. (n <= i \ x j i = 0)" (is ?en)  haftmann@27484  222  shows "(Rep_matrix (Abs_matrix x)) = x"  haftmann@27484  223 apply (rule Abs_matrix_inverse)  haftmann@27484  224 apply (simp add: matrix_def nonzero_positions_def)  haftmann@27484  225 proof -  haftmann@27484  226  from aem obtain m where a: "! j i. m <= j \ x j i = 0" by (blast)  haftmann@27484  227  from aen obtain n where b: "! j i. n <= i \ x j i = 0" by (blast)  bulwahn@50027  228  let ?u = "{(i, j). x i j \ 0}"  bulwahn@50027  229  let ?v = "{(i, j). i < m & j < n}"  haftmann@27484  230  have c: "!! (m::nat) a. ~(m <= a) \ a < m" by (arith)  haftmann@27484  231  from a b have "(?u \ (-?v)) = {}"  haftmann@27484  232  apply (simp)  nipkow@39302  233  apply (rule set_eqI)  haftmann@27484  234  apply (simp)  haftmann@27484  235  apply auto  haftmann@27484  236  by (rule c, auto)+  haftmann@27484  237  then have d: "?u \ ?v" by blast  haftmann@27484  238  moreover have "finite ?v" by (simp add: finite_natarray2)  bulwahn@50027  239  moreover have "{pos. x (fst pos) (snd pos) \ 0} = ?u" by auto  bulwahn@50027  240  ultimately show "finite {pos. x (fst pos) (snd pos) \ 0}"  bulwahn@50027  241  by (metis (lifting) finite_subset)  haftmann@27484  242 qed  haftmann@27484  243 haftmann@35416  244 definition apply_infmatrix :: "('a \ 'b) \ 'a infmatrix \ 'b infmatrix" where  haftmann@27484  245  "apply_infmatrix f == % A. (% j i. f (A j i))"  haftmann@35416  246 haftmann@35416  247 definition apply_matrix :: "('a \ 'b) \ ('a::zero) matrix \ ('b::zero) matrix" where  haftmann@27484  248  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"  haftmann@35416  249 haftmann@35416  250 definition combine_infmatrix :: "('a \ 'b \ 'c) \ 'a infmatrix \ 'b infmatrix \ 'c infmatrix" where  haftmann@27484  251  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"  haftmann@35416  252 haftmann@35416  253 definition combine_matrix :: "('a \ 'b \ 'c) \ ('a::zero) matrix \ ('b::zero) matrix \ ('c::zero) matrix" where  haftmann@27484  254  "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"  haftmann@27484  255 haftmann@27484  256 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"  haftmann@27484  257 by (simp add: apply_infmatrix_def)  haftmann@27484  258 haftmann@27484  259 lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"  haftmann@27484  260 by (simp add: combine_infmatrix_def)  haftmann@27484  261 haftmann@35416  262 definition commutative :: "('a \ 'a \ 'b) \ bool" where  haftmann@27484  263 "commutative f == ! x y. f x y = f y x"  haftmann@35416  264 haftmann@35416  265 definition associative :: "('a \ 'a \ 'a) \ bool" where  haftmann@27484  266 "associative f == ! x y z. f (f x y) z = f x (f y z)"  haftmann@27484  267 haftmann@27484  268 text{*  haftmann@27484  269 To reason about associativity and commutativity of operations on matrices,  haftmann@27484  270 let's take a step back and look at the general situtation: Assume that we have  haftmann@27484  271 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.  haftmann@27484  272 Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.  haftmann@27484  273 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.$  haftmann@27484  274 *}  haftmann@27484  275 haftmann@27484  276 lemma combine_infmatrix_commute:  haftmann@27484  277  "commutative f \ commutative (combine_infmatrix f)"  haftmann@27484  278 by (simp add: commutative_def combine_infmatrix_def)  haftmann@27484  279 haftmann@27484  280 lemma combine_matrix_commute:  haftmann@27484  281 "commutative f \ commutative (combine_matrix f)"  haftmann@27484  282 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)  haftmann@27484  283 haftmann@27484  284 text{*  haftmann@27484  285 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\}$,  haftmann@27484  286 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  haftmann@27484  287 $f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1,$  haftmann@27484  288 but on the other hand we have  haftmann@27484  289 $f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.$  haftmann@27484  290 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:  haftmann@27484  291 *}  haftmann@27484  292 haftmann@27484  293 lemma nonzero_positions_combine_infmatrix[simp]: "f 0 0 = 0 \ nonzero_positions (combine_infmatrix f A B) \ (nonzero_positions A) \ (nonzero_positions B)"  haftmann@27484  294 by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)  haftmann@27484  295 haftmann@27484  296 lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"  haftmann@27484  297 by (insert Rep_matrix [of A], simp add: matrix_def)  haftmann@27484  298 haftmann@27484  299 lemma combine_infmatrix_closed [simp]:  haftmann@27484  300  "f 0 0 = 0 \ Rep_matrix (Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))) = combine_infmatrix f (Rep_matrix A) (Rep_matrix B)"  haftmann@27484  301 apply (rule Abs_matrix_inverse)  haftmann@27484  302 apply (simp add: matrix_def)  haftmann@27484  303 apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \ (nonzero_positions (Rep_matrix B))"])  haftmann@27484  304 by (simp_all)  haftmann@27484  305 haftmann@27484  306 text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}  haftmann@27484  307 lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \ nonzero_positions (apply_infmatrix f A) \ nonzero_positions A"  haftmann@27484  308 by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)  haftmann@27484  309 haftmann@27484  310 lemma apply_infmatrix_closed [simp]:  haftmann@27484  311  "f 0 = 0 \ Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"  haftmann@27484  312 apply (rule Abs_matrix_inverse)  haftmann@27484  313 apply (simp add: matrix_def)  haftmann@27484  314 apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])  haftmann@27484  315 by (simp_all)  haftmann@27484  316 haftmann@27484  317 lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \ associative f \ associative (combine_infmatrix f)"  haftmann@27484  318 by (simp add: associative_def combine_infmatrix_def)  haftmann@27484  319 haftmann@27484  320 lemma comb: "f = g \ x = y \ f x = g y"  haftmann@27484  321 by (auto)  haftmann@27484  322 haftmann@27484  323 lemma combine_matrix_assoc: "f 0 0 = 0 \ associative f \ associative (combine_matrix f)"  haftmann@27484  324 apply (simp(no_asm) add: associative_def combine_matrix_def, auto)  haftmann@27484  325 apply (rule comb [of Abs_matrix Abs_matrix])  haftmann@27484  326 by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)  haftmann@27484  327 haftmann@27484  328 lemma Rep_apply_matrix[simp]: "f 0 = 0 \ Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"  haftmann@27484  329 by (simp add: apply_matrix_def)  haftmann@27484  330 haftmann@27484  331 lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \ Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"  haftmann@27484  332  by(simp add: combine_matrix_def)  haftmann@27484  333 haftmann@27484  334 lemma combine_nrows_max: "f 0 0 = 0 \ nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"  haftmann@27484  335 by (simp add: nrows_le)  haftmann@27484  336 haftmann@27484  337 lemma combine_ncols_max: "f 0 0 = 0 \ ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"  haftmann@27484  338 by (simp add: ncols_le)  haftmann@27484  339 haftmann@27484  340 lemma combine_nrows: "f 0 0 = 0 \ nrows A <= q \ nrows B <= q \ nrows(combine_matrix f A B) <= q"  haftmann@27484  341  by (simp add: nrows_le)  haftmann@27484  342 haftmann@27484  343 lemma combine_ncols: "f 0 0 = 0 \ ncols A <= q \ ncols B <= q \ ncols(combine_matrix f A B) <= q"  haftmann@27484  344  by (simp add: ncols_le)  haftmann@27484  345 haftmann@35416  346 definition zero_r_neutral :: "('a \ 'b::zero \ 'a) \ bool" where  haftmann@27484  347  "zero_r_neutral f == ! a. f a 0 = a"  haftmann@35416  348 haftmann@35416  349 definition zero_l_neutral :: "('a::zero \ 'b \ 'b) \ bool" where  haftmann@27484  350  "zero_l_neutral f == ! a. f 0 a = a"  haftmann@35416  351 haftmann@35416  352 definition zero_closed :: "(('a::zero) \ ('b::zero) \ ('c::zero)) \ bool" where  haftmann@27484  353  "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"  haftmann@27484  354 wenzelm@38273  355 primrec foldseq :: "('a \ 'a \ 'a) \ (nat \ 'a) \ nat \ 'a"  wenzelm@38273  356 where  haftmann@27484  357  "foldseq f s 0 = s 0"  wenzelm@38273  358 | "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"  haftmann@27484  359 wenzelm@38273  360 primrec foldseq_transposed :: "('a \ 'a \ 'a) \ (nat \ 'a) \ nat \ 'a"  wenzelm@38273  361 where  haftmann@27484  362  "foldseq_transposed f s 0 = s 0"  wenzelm@38273  363 | "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"  haftmann@27484  364 haftmann@27484  365 lemma foldseq_assoc : "associative f \ foldseq f = foldseq_transposed f"  haftmann@27484  366 proof -  haftmann@27484  367  assume a:"associative f"  haftmann@27484  368  then have sublemma: "!! n. ! N s. N <= n \ foldseq f s N = foldseq_transposed f s N"  haftmann@27484  369  proof -  haftmann@27484  370  fix n  haftmann@27484  371  show "!N s. N <= n \ foldseq f s N = foldseq_transposed f s N"  haftmann@27484  372  proof (induct n)  haftmann@27484  373  show "!N s. N <= 0 \ foldseq f s N = foldseq_transposed f s N" by simp  haftmann@27484  374  next  haftmann@27484  375  fix n  haftmann@27484  376  assume b:"! N s. N <= n \ foldseq f s N = foldseq_transposed f s N"  haftmann@27484  377  have c:"!!N s. N <= n \ foldseq f s N = foldseq_transposed f s N" by (simp add: b)  haftmann@27484  378  show "! N t. N <= Suc n \ foldseq f t N = foldseq_transposed f t N"  haftmann@27484  379  proof (auto)  haftmann@27484  380  fix N t  haftmann@27484  381  assume Nsuc: "N <= Suc n"  haftmann@27484  382  show "foldseq f t N = foldseq_transposed f t N"  haftmann@27484  383  proof cases  haftmann@27484  384  assume "N <= n"  haftmann@27484  385  then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)  haftmann@27484  386  next  haftmann@27484  387  assume "~(N <= n)"  haftmann@27484  388  with Nsuc have Nsuceq: "N = Suc n" by simp  haftmann@27484  389  have neqz: "n \ 0 \ ? m. n = Suc m & Suc m <= n" by arith  haftmann@27484  390  have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)  haftmann@27484  391  show "foldseq f t N = foldseq_transposed f t N"  haftmann@27484  392  apply (simp add: Nsuceq)  haftmann@27484  393  apply (subst c)  haftmann@27484  394  apply (simp)  haftmann@27484  395  apply (case_tac "n = 0")  haftmann@27484  396  apply (simp)  haftmann@27484  397  apply (drule neqz)  haftmann@27484  398  apply (erule exE)  haftmann@27484  399  apply (simp)  haftmann@27484  400  apply (subst assocf)  haftmann@27484  401  proof -  haftmann@27484  402  fix m  haftmann@27484  403  assume "n = Suc m & Suc m <= n"  haftmann@27484  404  then have mless: "Suc m <= n" by arith  haftmann@27484  405  then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")  haftmann@27484  406  apply (subst c)  haftmann@27484  407  by simp+  haftmann@27484  408  have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp  haftmann@27484  409  have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")  haftmann@27484  410  apply (subst c)  haftmann@27484  411  by (simp add: mless)+  haftmann@27484  412  have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp  haftmann@27484  413  from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp  haftmann@27484  414  qed  haftmann@27484  415  qed  haftmann@27484  416  qed  haftmann@27484  417  qed  haftmann@27484  418  qed  haftmann@27484  419  show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)  haftmann@27484  420  qed  haftmann@27484  421 haftmann@27484  422 lemma foldseq_distr: "\associative f; commutative f\ \ foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"  haftmann@27484  423 proof -  haftmann@27484  424  assume assoc: "associative f"  haftmann@27484  425  assume comm: "commutative f"  haftmann@27484  426  from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)  haftmann@27484  427  from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)  haftmann@27484  428  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)  haftmann@27484  429  have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"  haftmann@27484  430  apply (induct_tac n)  haftmann@27484  431  apply (simp+, auto)  haftmann@27484  432  by (simp add: a b c)  haftmann@27484  433  then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp  haftmann@27484  434 qed  haftmann@27484  435 haftmann@27484  436 theorem "\associative f; associative g; \a b c d. g (f a b) (f c d) = f (g a c) (g b d); ? x y. (f x) \ (f y); ? x y. (g x) \ (g y); f x x = x; g x x = x\ \ f=g | (! y. f y x = y) | (! y. g y x = y)"  haftmann@27484  437 oops  haftmann@27484  438 (* Model found  haftmann@27484  439 haftmann@27484  440 Trying to find a model that refutes: \associative f; associative g;  haftmann@27484  441  \a b c d. g (f a b) (f c d) = f (g a c) (g b d); \x y. f x \ f y;  haftmann@27484  442  \x y. g x \ g y; f x x = x; g x x = x\  haftmann@27484  443 \ f = g \ (\y. f y x = y) \ (\y. g y x = y)  haftmann@27484  444 Searching for a model of size 1, translating term... invoking SAT solver... no model found.  haftmann@27484  445 Searching for a model of size 2, translating term... invoking SAT solver... no model found.  haftmann@27484  446 Searching for a model of size 3, translating term... invoking SAT solver...  haftmann@27484  447 Model found:  haftmann@27484  448 Size of types: 'a: 3  haftmann@27484  449 x: a1  haftmann@27484  450 g: (a0\(a0\a1, a1\a0, a2\a1), a1\(a0\a0, a1\a1, a2\a0), a2\(a0\a1, a1\a0, a2\a1))  haftmann@27484  451 f: (a0\(a0\a0, a1\a0, a2\a0), a1\(a0\a1, a1\a1, a2\a1), a2\(a0\a0, a1\a0, a2\a0))  haftmann@27484  452 *)  haftmann@27484  453 haftmann@27484  454 lemma foldseq_zero:  haftmann@27484  455 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \ s i = 0"  haftmann@27484  456 shows "foldseq f s n = 0"  haftmann@27484  457 proof -  haftmann@27484  458  have "!! n. ! s. (! i. i <= n \ s i = 0) \ foldseq f s n = 0"  haftmann@27484  459  apply (induct_tac n)  haftmann@27484  460  apply (simp)  haftmann@27484  461  by (simp add: fz)  haftmann@27484  462  then show "foldseq f s n = 0" by (simp add: sz)  haftmann@27484  463 qed  haftmann@27484  464 haftmann@27484  465 lemma foldseq_significant_positions:  haftmann@27484  466  assumes p: "! i. i <= N \ S i = T i"  wenzelm@35612  467  shows "foldseq f S N = foldseq f T N"  haftmann@27484  468 proof -  haftmann@27484  469  have "!! m . ! s t. (! i. i<=m \ s i = t i) \ foldseq f s m = foldseq f t m"  haftmann@27484  470  apply (induct_tac m)  haftmann@27484  471  apply (simp)  haftmann@27484  472  apply (simp)  haftmann@27484  473  apply (auto)  haftmann@27484  474  proof -  haftmann@27484  475  fix n  haftmann@27484  476  fix s::"nat\'a"  haftmann@27484  477  fix t::"nat\'a"  haftmann@27484  478  assume a: "\s t. (\i\n. s i = t i) \ foldseq f s n = foldseq f t n"  haftmann@27484  479  assume b: "\i\Suc n. s i = t i"  haftmann@27484  480  have c:"!! a b. a = b \ f (t 0) a = f (t 0) b" by blast  haftmann@27484  481  have d:"!! s t. (\i\n. s i = t i) \ foldseq f s n = foldseq f t n" by (simp add: a)  haftmann@27484  482  show "f (t 0) (foldseq f (\k. s (Suc k)) n) = f (t 0) (foldseq f (\k. t (Suc k)) n)" by (rule c, simp add: d b)  haftmann@27484  483  qed  wenzelm@35612  484  with p show ?thesis by simp  haftmann@27484  485 qed  haftmann@27484  486 wenzelm@35612  487 lemma foldseq_tail:  wenzelm@35612  488  assumes "M <= N"  wenzelm@35612  489  shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M"  haftmann@27484  490 proof -  haftmann@27484  491  have suc: "!! a b. \a <= Suc b; a \ Suc b\ \ a <= b" by arith  haftmann@27484  492  have a:"!! a b c . a = b \ f c a = f c b" by blast  haftmann@27484  493  have "!! n. ! m s. m <= n \ foldseq f s n = foldseq f (% k. (if k < m then (s k) else (foldseq f (% k. s(k+m)) (n-m)))) m"  haftmann@27484  494  apply (induct_tac n)  haftmann@27484  495  apply (simp)  haftmann@27484  496  apply (simp)  haftmann@27484  497  apply (auto)  haftmann@27484  498  apply (case_tac "m = Suc na")  haftmann@27484  499  apply (simp)  haftmann@27484  500  apply (rule a)  haftmann@27484  501  apply (rule foldseq_significant_positions)  haftmann@27484  502  apply (auto)  haftmann@27484  503  apply (drule suc, simp+)  haftmann@27484  504  proof -  haftmann@27484  505  fix na m s  haftmann@27484  506  assume suba:"\m\na. \s. foldseq f s na = foldseq f (\k. if k < m then s k else foldseq f (\k. s (k + m)) (na - m))m"  haftmann@27484  507  assume subb:"m <= na"  haftmann@27484  508  from suba have subc:"!! m s. m <= na \foldseq f s na = foldseq f (\k. if k < m then s k else foldseq f (\k. s (k + m)) (na - m))m" by simp  haftmann@27484  509  have subd: "foldseq f (\k. if k < m then s (Suc k) else foldseq f (\k. s (Suc (k + m))) (na - m)) m =  haftmann@27484  510  foldseq f (% k. s(Suc k)) na"  haftmann@27484  511  by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)  haftmann@27484  512  from subb have sube: "m \ 0 \ ? mm. m = Suc mm & mm <= na" by arith  haftmann@27484  513  show "f (s 0) (foldseq f (\k. if k < m then s (Suc k) else foldseq f (\k. s (Suc (k + m))) (na - m)) m) =  haftmann@27484  514  foldseq f (\k. if k < m then s k else foldseq f (\k. s (k + m)) (Suc na - m)) m"  haftmann@27484  515  apply (simp add: subd)  haftmann@38526  516  apply (cases "m = 0")  haftmann@27484  517  apply (simp)  haftmann@27484  518  apply (drule sube)  haftmann@27484  519  apply (auto)  haftmann@27484  520  apply (rule a)  haftmann@38526  521  by (simp add: subc cong del: if_cong)  haftmann@27484  522  qed  wenzelm@35612  523  then show ?thesis using assms by simp  haftmann@27484  524 qed  haftmann@27484  525 haftmann@27484  526 lemma foldseq_zerotail:  haftmann@27484  527  assumes  haftmann@27484  528  fz: "f 0 0 = 0"  haftmann@27484  529  and sz: "! i. n <= i \ s i = 0"  haftmann@27484  530  and nm: "n <= m"  haftmann@27484  531  shows  haftmann@27484  532  "foldseq f s n = foldseq f s m"  haftmann@27484  533 proof -  haftmann@27484  534  show "foldseq f s n = foldseq f s m"  haftmann@27484  535  apply (simp add: foldseq_tail[OF nm, of f s])  haftmann@27484  536  apply (rule foldseq_significant_positions)  haftmann@27484  537  apply (auto)  haftmann@27484  538  apply (subst foldseq_zero)  haftmann@27484  539  by (simp add: fz sz)+  haftmann@27484  540 qed  haftmann@27484  541 haftmann@27484  542 lemma foldseq_zerotail2:  haftmann@27484  543  assumes "! x. f x 0 = x"  haftmann@27484  544  and "! i. n < i \ s i = 0"  haftmann@27484  545  and nm: "n <= m"  wenzelm@35612  546  shows "foldseq f s n = foldseq f s m"  haftmann@27484  547 proof -  wenzelm@35612  548  have "f 0 0 = 0" by (simp add: assms)  haftmann@27484  549  have b:"!! m n. n <= m \ m \ n \ ? k. m-n = Suc k" by arith  haftmann@27484  550  have c: "0 <= m" by simp  haftmann@27484  551  have d: "!! k. k \ 0 \ ? l. k = Suc l" by arith  wenzelm@35612  552  show ?thesis  haftmann@27484  553  apply (subst foldseq_tail[OF nm])  haftmann@27484  554  apply (rule foldseq_significant_positions)  haftmann@27484  555  apply (auto)  haftmann@27484  556  apply (case_tac "m=n")  haftmann@27484  557  apply (simp+)  haftmann@27484  558  apply (drule b[OF nm])  haftmann@27484  559  apply (auto)  haftmann@27484  560  apply (case_tac "k=0")  wenzelm@35612  561  apply (simp add: assms)  haftmann@27484  562  apply (drule d)  haftmann@27484  563  apply (auto)  wenzelm@35612  564  apply (simp add: assms foldseq_zero)  wenzelm@35612  565  done  haftmann@27484  566 qed  haftmann@27484  567 haftmann@27484  568 lemma foldseq_zerostart:  haftmann@27484  569  "! x. f 0 (f 0 x) = f 0 x \ ! i. i <= n \ s i = 0 \ foldseq f s (Suc n) = f 0 (s (Suc n))"  haftmann@27484  570 proof -  haftmann@27484  571  assume f00x: "! x. f 0 (f 0 x) = f 0 x"  haftmann@27484  572  have "! s. (! i. i<=n \ s i = 0) \ foldseq f s (Suc n) = f 0 (s (Suc n))"  haftmann@27484  573  apply (induct n)  haftmann@27484  574  apply (simp)  haftmann@27484  575  apply (rule allI, rule impI)  haftmann@27484  576  proof -  haftmann@27484  577  fix n  haftmann@27484  578  fix s  haftmann@27484  579  have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp  haftmann@27484  580  assume b: "! s. ((\i\n. s i = 0) \ foldseq f s (Suc n) = f 0 (s (Suc n)))"  haftmann@27484  581  from b have c:"!! s. (\i\n. s i = 0) \ foldseq f s (Suc n) = f 0 (s (Suc n))" by simp  haftmann@27484  582  assume d: "! i. i <= Suc n \ s i = 0"  haftmann@27484  583  show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"  haftmann@27484  584  apply (subst a)  haftmann@27484  585  apply (subst c)  haftmann@27484  586  by (simp add: d f00x)+  haftmann@27484  587  qed  haftmann@27484  588  then show "! i. i <= n \ s i = 0 \ foldseq f s (Suc n) = f 0 (s (Suc n))" by simp  haftmann@27484  589 qed  haftmann@27484  590 haftmann@27484  591 lemma foldseq_zerostart2:  haftmann@27484  592  "! x. f 0 x = x \ ! i. i < n \ s i = 0 \ foldseq f s n = s n"  haftmann@27484  593 proof -  haftmann@27484  594  assume a:"! i. i s i = 0"  haftmann@27484  595  assume x:"! x. f 0 x = x"  haftmann@27484  596  from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast  haftmann@27484  597  have b: "!! i l. i < Suc l = (i <= l)" by arith  haftmann@27484  598  have d: "!! k. k \ 0 \ ? l. k = Suc l" by arith  haftmann@27484  599  show "foldseq f s n = s n"  haftmann@27484  600  apply (case_tac "n=0")  haftmann@27484  601  apply (simp)  haftmann@27484  602  apply (insert a)  haftmann@27484  603  apply (drule d)  haftmann@27484  604  apply (auto)  haftmann@27484  605  apply (simp add: b)  haftmann@27484  606  apply (insert f00x)  haftmann@27484  607  apply (drule foldseq_zerostart)  haftmann@27484  608  by (simp add: x)+  haftmann@27484  609 qed  haftmann@27484  610 haftmann@27484  611 lemma foldseq_almostzero:  haftmann@27484  612  assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \ j \ s i = 0"  wenzelm@35612  613  shows "foldseq f s n = (if (j <= n) then (s j) else 0)"  haftmann@27484  614 proof -  haftmann@27484  615  from s0 have a: "! i. i < j \ s i = 0" by simp  haftmann@27484  616  from s0 have b: "! i. j < i \ s i = 0" by simp  wenzelm@35612  617  show ?thesis  haftmann@27484  618  apply auto  haftmann@27484  619  apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])  haftmann@27484  620  apply simp  haftmann@27484  621  apply (subst foldseq_zerostart2)  haftmann@27484  622  apply (simp add: f0x a)+  haftmann@27484  623  apply (subst foldseq_zero)  haftmann@27484  624  by (simp add: s0 f0x)+  haftmann@27484  625 qed  haftmann@27484  626 haftmann@27484  627 lemma foldseq_distr_unary:  haftmann@27484  628  assumes "!! a b. g (f a b) = f (g a) (g b)"  wenzelm@35612  629  shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n"  haftmann@27484  630 proof -  haftmann@27484  631  have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"  haftmann@27484  632  apply (induct_tac n)  haftmann@27484  633  apply (simp)  haftmann@27484  634  apply (simp)  haftmann@27484  635  apply (auto)  haftmann@27484  636  apply (drule_tac x="% k. s (Suc k)" in spec)  wenzelm@35612  637  by (simp add: assms)  wenzelm@35612  638  then show ?thesis by simp  haftmann@27484  639 qed  haftmann@27484  640 haftmann@35416  641 definition mult_matrix_n :: "nat \ (('a::zero) \ ('b::zero) \ ('c::zero)) \ ('c \ 'c \ 'c) \ 'a matrix \ 'b matrix \ 'c matrix" where  haftmann@27484  642  "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)"  haftmann@35416  643 haftmann@35416  644 definition mult_matrix :: "(('a::zero) \ ('b::zero) \ ('c::zero)) \ ('c \ 'c \ 'c) \ 'a matrix \ 'b matrix \ 'c matrix" where  haftmann@27484  645  "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"  haftmann@27484  646 haftmann@27484  647 lemma mult_matrix_n:  wenzelm@35612  648  assumes "ncols A \ n" (is ?An) "nrows B \ n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"  wenzelm@35612  649  shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B"  haftmann@27484  650 proof -  wenzelm@35612  651  show ?thesis using assms  haftmann@27484  652  apply (simp add: mult_matrix_def mult_matrix_n_def)  haftmann@27484  653  apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)  wenzelm@35612  654  apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms)  wenzelm@35612  655  done  haftmann@27484  656 qed  haftmann@27484  657 haftmann@27484  658 lemma mult_matrix_nm:  wenzelm@35612  659  assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"  haftmann@27484  660  shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"  haftmann@27484  661 proof -  wenzelm@35612  662  from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B"  wenzelm@35612  663  by (simp add: mult_matrix_n)  wenzelm@35612  664  also from assms have "\ = mult_matrix_n m fmul fadd A B"  wenzelm@35612  665  by (simp add: mult_matrix_n[THEN sym])  haftmann@27484  666  finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp  haftmann@27484  667 qed  haftmann@27484  668 haftmann@35416  669 definition r_distributive :: "('a \ 'b \ 'b) \ ('b \ 'b \ 'b) \ bool" where  haftmann@27484  670  "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"  haftmann@35416  671 haftmann@35416  672 definition l_distributive :: "('a \ 'b \ 'a) \ ('a \ 'a \ 'a) \ bool" where  haftmann@27484  673  "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"  haftmann@35416  674 haftmann@35416  675 definition distributive :: "('a \ 'a \ 'a) \ ('a \ 'a \ 'a) \ bool" where  haftmann@27484  676  "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"  haftmann@27484  677 haftmann@27484  678 lemma max1: "!! a x y. (a::nat) <= x \ a <= max x y" by (arith)  haftmann@27484  679 lemma max2: "!! b x y. (b::nat) <= y \ b <= max x y" by (arith)  haftmann@27484  680 haftmann@27484  681 lemma r_distributive_matrix:  wenzelm@35612  682  assumes  haftmann@27484  683  "r_distributive fmul fadd"  haftmann@27484  684  "associative fadd"  haftmann@27484  685  "commutative fadd"  haftmann@27484  686  "fadd 0 0 = 0"  haftmann@27484  687  "! a. fmul a 0 = 0"  haftmann@27484  688  "! a. fmul 0 a = 0"  wenzelm@35612  689  shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"  haftmann@27484  690 proof -  wenzelm@35612  691  from assms show ?thesis  haftmann@27484  692  apply (simp add: r_distributive_def mult_matrix_def, auto)  haftmann@27484  693  proof -  haftmann@27484  694  fix a::"'a matrix"  haftmann@27484  695  fix u::"'b matrix"  haftmann@27484  696  fix v::"'b matrix"  haftmann@27484  697  let ?mx = "max (ncols a) (max (nrows u) (nrows v))"  wenzelm@35612  698  from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =  haftmann@27484  699  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)"  haftmann@27484  700  apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])  haftmann@27484  701  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  702  apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])  haftmann@27484  703  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  704  apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])  haftmann@27484  705  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  706  apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])  haftmann@27484  707  apply (simp add: combine_matrix_def combine_infmatrix_def)  haftmann@27484  708  apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)  haftmann@27484  709  apply (simplesubst RepAbs_matrix)  haftmann@27484  710  apply (simp, auto)  haftmann@27484  711  apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)  haftmann@27484  712  apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)  haftmann@27484  713  apply (subst RepAbs_matrix)  haftmann@27484  714  apply (simp, auto)  haftmann@27484  715  apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)  haftmann@27484  716  apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)  haftmann@27484  717  done  haftmann@27484  718  qed  haftmann@27484  719 qed  haftmann@27484  720 haftmann@27484  721 lemma l_distributive_matrix:  wenzelm@35612  722  assumes  haftmann@27484  723  "l_distributive fmul fadd"  haftmann@27484  724  "associative fadd"  haftmann@27484  725  "commutative fadd"  haftmann@27484  726  "fadd 0 0 = 0"  haftmann@27484  727  "! a. fmul a 0 = 0"  haftmann@27484  728  "! a. fmul 0 a = 0"  wenzelm@35612  729  shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"  haftmann@27484  730 proof -  wenzelm@35612  731  from assms show ?thesis  haftmann@27484  732  apply (simp add: l_distributive_def mult_matrix_def, auto)  haftmann@27484  733  proof -  haftmann@27484  734  fix a::"'b matrix"  haftmann@27484  735  fix u::"'a matrix"  haftmann@27484  736  fix v::"'a matrix"  haftmann@27484  737  let ?mx = "max (nrows a) (max (ncols u) (ncols v))"  wenzelm@35612  738  from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =  haftmann@27484  739  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)"  haftmann@27484  740  apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])  haftmann@27484  741  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  742  apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])  haftmann@27484  743  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  744  apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])  haftmann@27484  745  apply (simp add: max1 max2 combine_nrows combine_ncols)+  haftmann@27484  746  apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])  haftmann@27484  747  apply (simp add: combine_matrix_def combine_infmatrix_def)  haftmann@27484  748  apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)  haftmann@27484  749  apply (simplesubst RepAbs_matrix)  haftmann@27484  750  apply (simp, auto)  haftmann@27484  751  apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)  haftmann@27484  752  apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)  haftmann@27484  753  apply (subst RepAbs_matrix)  haftmann@27484  754  apply (simp, auto)  haftmann@27484  755  apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)  haftmann@27484  756  apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)  haftmann@27484  757  done  haftmann@27484  758  qed  haftmann@27484  759 qed  haftmann@27484  760 haftmann@27484  761 instantiation matrix :: (zero) zero  haftmann@27484  762 begin  haftmann@27484  763 haftmann@37765  764 definition zero_matrix_def: "0 = Abs_matrix (\j i. 0)"  haftmann@27484  765 haftmann@27484  766 instance ..  haftmann@27484  767 haftmann@27484  768 end  haftmann@27484  769 haftmann@27484  770 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"  haftmann@27484  771  apply (simp add: zero_matrix_def)  haftmann@27484  772  apply (subst RepAbs_matrix)  haftmann@27484  773  by (auto)  haftmann@27484  774 haftmann@27484  775 lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"  haftmann@27484  776 proof -  haftmann@27484  777  have a:"!! (x::nat). x <= 0 \ x = 0" by (arith)  haftmann@27484  778  show "nrows 0 = 0" by (rule a, subst nrows_le, simp)  haftmann@27484  779 qed  haftmann@27484  780 haftmann@27484  781 lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"  haftmann@27484  782 proof -  haftmann@27484  783  have a:"!! (x::nat). x <= 0 \ x = 0" by (arith)  haftmann@27484  784  show "ncols 0 = 0" by (rule a, subst ncols_le, simp)  haftmann@27484  785 qed  haftmann@27484  786 haftmann@27484  787 lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \ zero_l_neutral (combine_matrix f)"  haftmann@27484  788  by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)  haftmann@27484  789 haftmann@27484  790 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \ zero_r_neutral (combine_matrix f)"  haftmann@27484  791  by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)  haftmann@27484  792 haftmann@27484  793 lemma mult_matrix_zero_closed: "\fadd 0 0 = 0; zero_closed fmul\ \ zero_closed (mult_matrix fmul fadd)"  haftmann@27484  794  apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)  haftmann@27484  795  apply (auto)  haftmann@27484  796  by (subst foldseq_zero, (simp add: zero_matrix_def)+)+  haftmann@27484  797 haftmann@27484  798 lemma mult_matrix_n_zero_right[simp]: "\fadd 0 0 = 0; !a. fmul a 0 = 0\ \ mult_matrix_n n fmul fadd A 0 = 0"  haftmann@27484  799  apply (simp add: mult_matrix_n_def)  haftmann@27484  800  apply (subst foldseq_zero)  haftmann@27484  801  by (simp_all add: zero_matrix_def)  haftmann@27484  802 haftmann@27484  803 lemma mult_matrix_n_zero_left[simp]: "\fadd 0 0 = 0; !a. fmul 0 a = 0\ \ mult_matrix_n n fmul fadd 0 A = 0"  haftmann@27484  804  apply (simp add: mult_matrix_n_def)  haftmann@27484  805  apply (subst foldseq_zero)  haftmann@27484  806  by (simp_all add: zero_matrix_def)  haftmann@27484  807 haftmann@27484  808 lemma mult_matrix_zero_left[simp]: "\fadd 0 0 = 0; !a. fmul 0 a = 0\ \ mult_matrix fmul fadd 0 A = 0"  haftmann@27484  809 by (simp add: mult_matrix_def)  haftmann@27484  810 haftmann@27484  811 lemma mult_matrix_zero_right[simp]: "\fadd 0 0 = 0; !a. fmul a 0 = 0\ \ mult_matrix fmul fadd A 0 = 0"  haftmann@27484  812 by (simp add: mult_matrix_def)  haftmann@27484  813 haftmann@27484  814 lemma apply_matrix_zero[simp]: "f 0 = 0 \ apply_matrix f 0 = 0"  haftmann@27484  815  apply (simp add: apply_matrix_def apply_infmatrix_def)  haftmann@27484  816  by (simp add: zero_matrix_def)  haftmann@27484  817 haftmann@27484  818 lemma combine_matrix_zero: "f 0 0 = 0 \ combine_matrix f 0 0 = 0"  haftmann@27484  819  apply (simp add: combine_matrix_def combine_infmatrix_def)  haftmann@27484  820  by (simp add: zero_matrix_def)  haftmann@27484  821 haftmann@27484  822 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"  wenzelm@46985  823 apply (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix)  haftmann@27484  824 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)  haftmann@27484  825 apply (simp add: RepAbs_matrix)  haftmann@27484  826 done  haftmann@27484  827 haftmann@27484  828 lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"  haftmann@27484  829  apply (simp add: apply_matrix_def apply_infmatrix_def)  haftmann@27484  830  by (simp add: zero_matrix_def)  haftmann@27484  831 haftmann@35416  832 definition singleton_matrix :: "nat \ nat \ ('a::zero) \ 'a matrix" where  haftmann@27484  833  "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"  haftmann@35416  834 haftmann@35416  835 definition move_matrix :: "('a::zero) matrix \ int \ int \ 'a matrix" where  huffman@46702  836  "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)))"  haftmann@35416  837 haftmann@35416  838 definition take_rows :: "('a::zero) matrix \ nat \ 'a matrix" where  haftmann@27484  839  "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"  haftmann@35416  840 haftmann@35416  841 definition take_columns :: "('a::zero) matrix \ nat \ 'a matrix" where  haftmann@27484  842  "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"  haftmann@27484  843 haftmann@35416  844 definition column_of_matrix :: "('a::zero) matrix \ nat \ 'a matrix" where  haftmann@27484  845  "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"  haftmann@35416  846 haftmann@35416  847 definition row_of_matrix :: "('a::zero) matrix \ nat \ 'a matrix" where  haftmann@27484  848  "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"  haftmann@27484  849 haftmann@27484  850 lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"  haftmann@27484  851 apply (simp add: singleton_matrix_def)  haftmann@27484  852 apply (auto)  haftmann@27484  853 apply (subst RepAbs_matrix)  haftmann@27484  854 apply (rule exI[of _ "Suc m"], simp)  haftmann@27484  855 apply (rule exI[of _ "Suc n"], simp+)  haftmann@27484  856 by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+  haftmann@27484  857 haftmann@27484  858 lemma apply_singleton_matrix[simp]: "f 0 = 0 \ apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"  haftmann@27484  859 apply (subst Rep_matrix_inject[symmetric])  haftmann@27484  860 apply (rule ext)+  haftmann@27484  861 apply (simp)  haftmann@27484  862 done  haftmann@27484  863 haftmann@27484  864 lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"  haftmann@27484  865  by (simp add: singleton_matrix_def zero_matrix_def)  haftmann@27484  866 haftmann@27484  867 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"  haftmann@27484  868 proof-  haftmann@27484  869 have th: "\ (\m. m \ j)" "\n. \ n \ i" by arith+  haftmann@27484  870 from th show ?thesis  haftmann@27484  871 apply (auto)  nipkow@33657  872 apply (rule le_antisym)  haftmann@27484  873 apply (subst nrows_le)  haftmann@27484  874 apply (simp add: singleton_matrix_def, auto)  haftmann@27484  875 apply (subst RepAbs_matrix)  haftmann@27484  876 apply auto  haftmann@27484  877 apply (simp add: Suc_le_eq)  haftmann@27484  878 apply (rule not_leE)  haftmann@27484  879 apply (subst nrows_le)  haftmann@27484  880 by simp  haftmann@27484  881 qed  haftmann@27484  882 haftmann@27484  883 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"  haftmann@27484  884 proof-  haftmann@27484  885 have th: "\ (\m. m \ j)" "\n. \ n \ i" by arith+  haftmann@27484  886 from th show ?thesis  haftmann@27484  887 apply (auto)  nipkow@33657  888 apply (rule le_antisym)  haftmann@27484  889 apply (subst ncols_le)  haftmann@27484  890 apply (simp add: singleton_matrix_def, auto)  haftmann@27484  891 apply (subst RepAbs_matrix)  haftmann@27484  892 apply auto  haftmann@27484  893 apply (simp add: Suc_le_eq)  haftmann@27484  894 apply (rule not_leE)  haftmann@27484  895 apply (subst ncols_le)  haftmann@27484  896 by simp  haftmann@27484  897 qed  haftmann@27484  898 haftmann@27484  899 lemma combine_singleton: "f 0 0 = 0 \ combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"  haftmann@27484  900 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)  haftmann@27484  901 apply (subst RepAbs_matrix)  haftmann@27484  902 apply (rule exI[of _ "Suc j"], simp)  haftmann@27484  903 apply (rule exI[of _ "Suc i"], simp)  haftmann@27484  904 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)  haftmann@27484  905 apply (subst RepAbs_matrix)  haftmann@27484  906 apply (rule exI[of _ "Suc j"], simp)  haftmann@27484  907 apply (rule exI[of _ "Suc i"], simp)  haftmann@27484  908 by simp  haftmann@27484  909 haftmann@27484  910 lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"  haftmann@27484  911 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)  haftmann@27484  912 apply (simp)  haftmann@27484  913 done  haftmann@27484  914 haftmann@27484  915 lemma Rep_move_matrix[simp]:  haftmann@27484  916  "Rep_matrix (move_matrix A y x) j i =  huffman@46702  917  (if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"  haftmann@27484  918 apply (simp add: move_matrix_def)  haftmann@27484  919 apply (auto)  haftmann@27484  920 by (subst RepAbs_matrix,  haftmann@27484  921  rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,  haftmann@27484  922  rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+  haftmann@27484  923 haftmann@27484  924 lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"  haftmann@27484  925 by (simp add: move_matrix_def)  haftmann@27484  926 haftmann@27484  927 lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"  haftmann@27484  928 apply (subst Rep_matrix_inject[symmetric])  haftmann@27484  929 apply (rule ext)+  haftmann@27484  930 apply (simp)  haftmann@27484  931 done  haftmann@27484  932 haftmann@27484  933 lemma transpose_move_matrix[simp]:  haftmann@27484  934  "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"  haftmann@27484  935 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)  haftmann@27484  936 apply (simp)  haftmann@27484  937 done  haftmann@27484  938 haftmann@27484  939 lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i =  haftmann@27484  940  (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"  haftmann@27484  941  apply (subst Rep_matrix_inject[symmetric])  haftmann@27484  942  apply (rule ext)+  haftmann@27484  943  apply (case_tac "j + int u < 0")  haftmann@27484  944  apply (simp, arith)  haftmann@27484  945  apply (case_tac "i + int v < 0")  huffman@46702  946  apply (simp, arith)  huffman@46702  947  apply simp  haftmann@27484  948  apply arith  haftmann@27484  949  done  haftmann@27484  950 haftmann@27484  951 lemma Rep_take_columns[simp]:  haftmann@27484  952  "Rep_matrix (take_columns A c) j i =  haftmann@27484  953  (if i < c then (Rep_matrix A j i) else 0)"  haftmann@27484  954 apply (simp add: take_columns_def)  haftmann@27484  955 apply (simplesubst RepAbs_matrix)  haftmann@27484  956 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)  haftmann@27484  957 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)  haftmann@27484  958 done  haftmann@27484  959 haftmann@27484  960 lemma Rep_take_rows[simp]:  haftmann@27484  961  "Rep_matrix (take_rows A r) j i =  haftmann@27484  962  (if j < r then (Rep_matrix A j i) else 0)"  haftmann@27484  963 apply (simp add: take_rows_def)  haftmann@27484  964 apply (simplesubst RepAbs_matrix)  haftmann@27484  965 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)  haftmann@27484  966 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)  haftmann@27484  967 done  haftmann@27484  968 haftmann@27484  969 lemma Rep_column_of_matrix[simp]:  haftmann@27484  970  "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"  haftmann@27484  971  by (simp add: column_of_matrix_def)  haftmann@27484  972 haftmann@27484  973 lemma Rep_row_of_matrix[simp]:  haftmann@27484  974  "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"  haftmann@27484  975  by (simp add: row_of_matrix_def)  haftmann@27484  976 haftmann@27484  977 lemma column_of_matrix: "ncols A <= n \ column_of_matrix A n = 0"  haftmann@27484  978 apply (subst Rep_matrix_inject[THEN sym])  haftmann@27484  979 apply (rule ext)+  haftmann@27484  980 by (simp add: ncols)  haftmann@27484  981 haftmann@27484  982 lemma row_of_matrix: "nrows A <= n \ row_of_matrix A n = 0"  haftmann@27484  983 apply (subst Rep_matrix_inject[THEN sym])  haftmann@27484  984 apply (rule ext)+  haftmann@27484  985 by (simp add: nrows)  haftmann@27484  986 haftmann@27484  987 lemma mult_matrix_singleton_right[simp]:  wenzelm@35612  988  assumes  haftmann@27484  989  "! x. fmul x 0 = 0"  haftmann@27484  990  "! x. fmul 0 x = 0"  haftmann@27484  991  "! x. fadd 0 x = x"  haftmann@27484  992  "! x. fadd x 0 = x"  haftmann@27484  993  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))"  haftmann@27484  994  apply (simp add: mult_matrix_def)  haftmann@27484  995  apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])  haftmann@27484  996  apply (auto)  wenzelm@35612  997  apply (simp add: assms)+  haftmann@27484  998  apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)  haftmann@27484  999  apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)  haftmann@27484  1000  apply (subst foldseq_almostzero[of _ j])  wenzelm@35612  1001  apply (simp add: assms)+  haftmann@27484  1002  apply (auto)  nipkow@29700  1003  done  haftmann@27484  1004 haftmann@27484  1005 lemma mult_matrix_ext:  haftmann@27484  1006  assumes  haftmann@27484  1007  eprem:  haftmann@27484  1008  "? e. (! a b. a \ b \ fmul a e \ fmul b e)"  haftmann@27484  1009  and fprems:  haftmann@27484  1010  "! a. fmul 0 a = 0"  haftmann@27484  1011  "! a. fmul a 0 = 0"  haftmann@27484  1012  "! a. fadd a 0 = a"  haftmann@27484  1013  "! a. fadd 0 a = a"  haftmann@27484  1014  and contraprems:  haftmann@27484  1015  "mult_matrix fmul fadd A = mult_matrix fmul fadd B"  haftmann@27484  1016  shows  haftmann@27484  1017  "A = B"  haftmann@27484  1018 proof(rule contrapos_np[of "False"], simp)  haftmann@27484  1019  assume a: "A \ B"  haftmann@27484  1020  have b: "!! f g. (! x y. f x y = g x y) \ f = g" by ((rule ext)+, auto)  haftmann@27484  1021  have "? j i. (Rep_matrix A j i) \ (Rep_matrix B j i)"  haftmann@27484  1022  apply (rule contrapos_np[of "False"], simp+)  haftmann@27484  1023  apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)  haftmann@27484  1024  by (simp add: Rep_matrix_inject a)  haftmann@27484  1025  then obtain J I where c:"(Rep_matrix A J I) \ (Rep_matrix B J I)" by blast  haftmann@27484  1026  from eprem obtain e where eprops:"(! a b. a \ b \ fmul a e \ fmul b e)" by blast  haftmann@27484  1027  let ?S = "singleton_matrix I 0 e"  haftmann@27484  1028  let ?comp = "mult_matrix fmul fadd"  haftmann@27484  1029  have d: "!!x f g. f = g \ f x = g x" by blast  wenzelm@35612  1030  have e: "(% x. fmul x e) 0 = 0" by (simp add: assms)  haftmann@27484  1031  have "~(?comp A ?S = ?comp B ?S)"  haftmann@27484  1032  apply (rule notI)  haftmann@27484  1033  apply (simp add: fprems eprops)  haftmann@27484  1034  apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1035  apply (drule d[of _ _ "J"], drule d[of _ _ "0"])  haftmann@27484  1036  by (simp add: e c eprops)  haftmann@27484  1037  with contraprems show "False" by simp  haftmann@27484  1038 qed  haftmann@27484  1039 haftmann@35416  1040 definition foldmatrix :: "('a \ 'a \ 'a) \ ('a \ 'a \ 'a) \ ('a infmatrix) \ nat \ nat \ 'a" where  haftmann@27484  1041  "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"  haftmann@35416  1042 haftmann@35416  1043 definition foldmatrix_transposed :: "('a \ 'a \ 'a) \ ('a \ 'a \ 'a) \ ('a infmatrix) \ nat \ nat \ 'a" where  haftmann@27484  1044  "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"  haftmann@27484  1045 haftmann@27484  1046 lemma foldmatrix_transpose:  haftmann@27484  1047  assumes  haftmann@27484  1048  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"  haftmann@27484  1049  shows  wenzelm@35612  1050  "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"  haftmann@27484  1051 proof -  haftmann@27484  1052  have forall:"!! P x. (! x. P x) \ P x" by auto  haftmann@27484  1053  have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"  haftmann@27484  1054  apply (induct n)  wenzelm@35612  1055  apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+  haftmann@27484  1056  apply (auto)  haftmann@27484  1057  by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)  haftmann@27484  1058  show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"  haftmann@27484  1059  apply (simp add: foldmatrix_def foldmatrix_transposed_def)  haftmann@27484  1060  apply (induct m, simp)  haftmann@27484  1061  apply (simp)  haftmann@27484  1062  apply (insert tworows)  haftmann@27484  1063  apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\u. A u i) m) else (A (Suc m) i))" in spec)  haftmann@27484  1064  by (simp add: foldmatrix_def foldmatrix_transposed_def)  haftmann@27484  1065 qed  haftmann@27484  1066 haftmann@27484  1067 lemma foldseq_foldseq:  haftmann@27484  1068 assumes  haftmann@27484  1069  "associative f"  haftmann@27484  1070  "associative g"  haftmann@27484  1071  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"  haftmann@27484  1072 shows  haftmann@27484  1073  "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"  haftmann@27484  1074  apply (insert foldmatrix_transpose[of g f A m n])  wenzelm@35612  1075  by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)  haftmann@27484  1076 haftmann@27484  1077 lemma mult_n_nrows:  haftmann@27484  1078 assumes  haftmann@27484  1079 "! a. fmul 0 a = 0"  haftmann@27484  1080 "! a. fmul a 0 = 0"  haftmann@27484  1081 "fadd 0 0 = 0"  haftmann@27484  1082 shows "nrows (mult_matrix_n n fmul fadd A B) \ nrows A"  haftmann@27484  1083 apply (subst nrows_le)  haftmann@27484  1084 apply (simp add: mult_matrix_n_def)  haftmann@27484  1085 apply (subst RepAbs_matrix)  haftmann@27484  1086 apply (rule_tac x="nrows A" in exI)  wenzelm@35612  1087 apply (simp add: nrows assms foldseq_zero)  haftmann@27484  1088 apply (rule_tac x="ncols B" in exI)  wenzelm@35612  1089 apply (simp add: ncols assms foldseq_zero)  wenzelm@35612  1090 apply (simp add: nrows assms foldseq_zero)  wenzelm@35612  1091 done  haftmann@27484  1092 haftmann@27484  1093 lemma mult_n_ncols:  haftmann@27484  1094 assumes  haftmann@27484  1095 "! a. fmul 0 a = 0"  haftmann@27484  1096 "! a. fmul a 0 = 0"  haftmann@27484  1097 "fadd 0 0 = 0"  haftmann@27484  1098 shows "ncols (mult_matrix_n n fmul fadd A B) \ ncols B"  haftmann@27484  1099 apply (subst ncols_le)  haftmann@27484  1100 apply (simp add: mult_matrix_n_def)  haftmann@27484  1101 apply (subst RepAbs_matrix)  haftmann@27484  1102 apply (rule_tac x="nrows A" in exI)  wenzelm@35612  1103 apply (simp add: nrows assms foldseq_zero)  haftmann@27484  1104 apply (rule_tac x="ncols B" in exI)  wenzelm@35612  1105 apply (simp add: ncols assms foldseq_zero)  wenzelm@35612  1106 apply (simp add: ncols assms foldseq_zero)  wenzelm@35612  1107 done  haftmann@27484  1108 haftmann@27484  1109 lemma mult_nrows:  haftmann@27484  1110 assumes  haftmann@27484  1111 "! a. fmul 0 a = 0"  haftmann@27484  1112 "! a. fmul a 0 = 0"  haftmann@27484  1113 "fadd 0 0 = 0"  haftmann@27484  1114 shows "nrows (mult_matrix fmul fadd A B) \ nrows A"  wenzelm@35612  1115 by (simp add: mult_matrix_def mult_n_nrows assms)  haftmann@27484  1116 haftmann@27484  1117 lemma mult_ncols:  haftmann@27484  1118 assumes  haftmann@27484  1119 "! a. fmul 0 a = 0"  haftmann@27484  1120 "! a. fmul a 0 = 0"  haftmann@27484  1121 "fadd 0 0 = 0"  haftmann@27484  1122 shows "ncols (mult_matrix fmul fadd A B) \ ncols B"  wenzelm@35612  1123 by (simp add: mult_matrix_def mult_n_ncols assms)  haftmann@27484  1124 haftmann@27484  1125 lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"  haftmann@27484  1126  apply (auto simp add: nrows_le)  haftmann@27484  1127  apply (rule nrows)  haftmann@27484  1128  apply (arith)  haftmann@27484  1129  done  haftmann@27484  1130 haftmann@27484  1131 lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"  haftmann@27484  1132  apply (auto simp add: ncols_le)  haftmann@27484  1133  apply (rule ncols)  haftmann@27484  1134  apply (arith)  haftmann@27484  1135  done  haftmann@27484  1136 haftmann@27484  1137 lemma mult_matrix_assoc:  wenzelm@35612  1138  assumes  haftmann@27484  1139  "! a. fmul1 0 a = 0"  haftmann@27484  1140  "! a. fmul1 a 0 = 0"  haftmann@27484  1141  "! a. fmul2 0 a = 0"  haftmann@27484  1142  "! a. fmul2 a 0 = 0"  haftmann@27484  1143  "fadd1 0 0 = 0"  haftmann@27484  1144  "fadd2 0 0 = 0"  haftmann@27484  1145  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"  haftmann@27484  1146  "associative fadd1"  haftmann@27484  1147  "associative fadd2"  haftmann@27484  1148  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"  haftmann@27484  1149  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"  haftmann@27484  1150  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"  wenzelm@35612  1151  shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)"  haftmann@27484  1152 proof -  haftmann@27484  1153  have comb_left: "!! A B x y. A = B \ (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast  haftmann@27484  1154  have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n) x = foldseq fadd1 (% k. fmul2 (s k) x) n"  wenzelm@35612  1155  by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all)  haftmann@27484  1156  have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"  wenzelm@35612  1157  using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all)  haftmann@27484  1158  let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"  wenzelm@35612  1159  show ?thesis  haftmann@27484  1160  apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1161  apply (rule ext)+  haftmann@27484  1162  apply (simp add: mult_matrix_def)  haftmann@27484  1163  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)"])  wenzelm@35612  1164  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  wenzelm@35612  1165  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)"])  wenzelm@35612  1166  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  haftmann@27484  1167  apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])  wenzelm@35612  1168  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  haftmann@27484  1169  apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])  wenzelm@35612  1170  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  haftmann@27484  1171  apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])  wenzelm@35612  1172  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  haftmann@27484  1173  apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])  wenzelm@35612  1174  apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+  haftmann@27484  1175  apply (simp add: mult_matrix_n_def)  haftmann@27484  1176  apply (rule comb_left)  haftmann@27484  1177  apply ((rule ext)+, simp)  haftmann@27484  1178  apply (simplesubst RepAbs_matrix)  haftmann@27484  1179  apply (rule exI[of _ "nrows B"])  wenzelm@35612  1180  apply (simp add: nrows assms foldseq_zero)  haftmann@27484  1181  apply (rule exI[of _ "ncols C"])  wenzelm@35612  1182  apply (simp add: assms ncols foldseq_zero)  haftmann@27484  1183  apply (subst RepAbs_matrix)  haftmann@27484  1184  apply (rule exI[of _ "nrows A"])  wenzelm@35612  1185  apply (simp add: nrows assms foldseq_zero)  haftmann@27484  1186  apply (rule exI[of _ "ncols B"])  wenzelm@35612  1187  apply (simp add: assms ncols foldseq_zero)  wenzelm@35612  1188  apply (simp add: fmul2fadd1fold fmul1fadd2fold assms)  haftmann@27484  1189  apply (subst foldseq_foldseq)  wenzelm@35612  1190  apply (simp add: assms)+  wenzelm@35612  1191  apply (simp add: transpose_infmatrix)  wenzelm@35612  1192  done  haftmann@27484  1193 qed  haftmann@27484  1194 haftmann@27484  1195 lemma  wenzelm@35612  1196  assumes  haftmann@27484  1197  "! a. fmul1 0 a = 0"  haftmann@27484  1198  "! a. fmul1 a 0 = 0"  haftmann@27484  1199  "! a. fmul2 0 a = 0"  haftmann@27484  1200  "! a. fmul2 a 0 = 0"  haftmann@27484  1201  "fadd1 0 0 = 0"  haftmann@27484  1202  "fadd2 0 0 = 0"  haftmann@27484  1203  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"  haftmann@27484  1204  "associative fadd1"  haftmann@27484  1205  "associative fadd2"  haftmann@27484  1206  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"  haftmann@27484  1207  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"  haftmann@27484  1208  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"  haftmann@27484  1209  shows  haftmann@27484  1210  "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"  haftmann@27484  1211 apply (rule ext)+  haftmann@27484  1212 apply (simp add: comp_def )  wenzelm@35612  1213 apply (simp add: mult_matrix_assoc assms)  wenzelm@35612  1214 done  haftmann@27484  1215 haftmann@27484  1216 lemma mult_matrix_assoc_simple:  wenzelm@35612  1217  assumes  haftmann@27484  1218  "! a. fmul 0 a = 0"  haftmann@27484  1219  "! a. fmul a 0 = 0"  haftmann@27484  1220  "fadd 0 0 = 0"  haftmann@27484  1221  "associative fadd"  haftmann@27484  1222  "commutative fadd"  haftmann@27484  1223  "associative fmul"  haftmann@27484  1224  "distributive fmul fadd"  wenzelm@35612  1225  shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)"  haftmann@27484  1226 proof -  haftmann@27484  1227  have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"  wenzelm@35612  1228  using assms by (simp add: associative_def commutative_def)  wenzelm@35612  1229  then show ?thesis  haftmann@27484  1230  apply (subst mult_matrix_assoc)  wenzelm@35612  1231  using assms  wenzelm@35612  1232  apply simp_all  wenzelm@35612  1233  apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def)  wenzelm@35612  1234  done  haftmann@27484  1235 qed  haftmann@27484  1236 haftmann@27484  1237 lemma transpose_apply_matrix: "f 0 = 0 \ transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"  haftmann@27484  1238 apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1239 apply (rule ext)+  haftmann@27484  1240 by simp  haftmann@27484  1241 haftmann@27484  1242 lemma transpose_combine_matrix: "f 0 0 = 0 \ transpose_matrix (combine_matrix f A B) = combine_matrix f (transpose_matrix A) (transpose_matrix B)"  haftmann@27484  1243 apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1244 apply (rule ext)+  haftmann@27484  1245 by simp  haftmann@27484  1246 haftmann@27484  1247 lemma Rep_mult_matrix:  haftmann@27484  1248  assumes  haftmann@27484  1249  "! a. fmul 0 a = 0"  haftmann@27484  1250  "! a. fmul a 0 = 0"  haftmann@27484  1251  "fadd 0 0 = 0"  haftmann@27484  1252  shows  haftmann@27484  1253  "Rep_matrix(mult_matrix fmul fadd A B) j i =  haftmann@27484  1254  foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"  haftmann@27484  1255 apply (simp add: mult_matrix_def mult_matrix_n_def)  haftmann@27484  1256 apply (subst RepAbs_matrix)  wenzelm@35612  1257 apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero)  wenzelm@35612  1258 apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero)  wenzelm@35612  1259 apply simp  wenzelm@35612  1260 done  haftmann@27484  1261 haftmann@27484  1262 lemma transpose_mult_matrix:  haftmann@27484  1263  assumes  haftmann@27484  1264  "! a. fmul 0 a = 0"  haftmann@27484  1265  "! a. fmul a 0 = 0"  haftmann@27484  1266  "fadd 0 0 = 0"  haftmann@27484  1267  "! x y. fmul y x = fmul x y"  haftmann@27484  1268  shows  haftmann@27484  1269  "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"  haftmann@27484  1270  apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1271  apply (rule ext)+  wenzelm@35612  1272  using assms  haftmann@54864  1273  apply (simp add: Rep_mult_matrix ac_simps)  wenzelm@35612  1274  done  haftmann@27484  1275 haftmann@27484  1276 lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"  haftmann@27484  1277 apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1278 apply (rule ext)+  haftmann@27484  1279 by simp  haftmann@27484  1280 haftmann@27484  1281 lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"  haftmann@27484  1282 apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1283 apply (rule ext)+  haftmann@27484  1284 by simp  haftmann@27484  1285 haftmann@27580  1286 instantiation matrix :: ("{zero, ord}") ord  haftmann@27484  1287 begin  haftmann@27484  1288 haftmann@27484  1289 definition  haftmann@27484  1290  le_matrix_def: "A \ B \ (\j i. Rep_matrix A j i \ Rep_matrix B j i)"  haftmann@27484  1291 haftmann@27484  1292 definition  wenzelm@28637  1293  less_def: "A < (B\'a matrix) \ A \ B \ \ B \ A"  haftmann@27484  1294 haftmann@27484  1295 instance ..  haftmann@27484  1296 haftmann@27484  1297 end  haftmann@27484  1298 haftmann@27580  1299 instance matrix :: ("{zero, order}") order  haftmann@27484  1300 apply intro_classes  haftmann@27484  1301 apply (simp_all add: le_matrix_def less_def)  haftmann@27484  1302 apply (auto)  haftmann@27484  1303 apply (drule_tac x=j in spec, drule_tac x=j in spec)  haftmann@27484  1304 apply (drule_tac x=i in spec, drule_tac x=i in spec)  haftmann@27484  1305 apply (simp)  haftmann@27484  1306 apply (simp add: Rep_matrix_inject[THEN sym])  haftmann@27484  1307 apply (rule ext)+  haftmann@27484  1308 apply (drule_tac x=xa in spec, drule_tac x=xa in spec)  haftmann@27484  1309 apply (drule_tac x=xb in spec, drule_tac x=xb in spec)  wenzelm@28637  1310 apply simp  wenzelm@28637  1311 done  haftmann@27484  1312 haftmann@27484  1313 lemma le_apply_matrix:  haftmann@27484  1314  assumes  haftmann@27484  1315  "f 0 = 0"  haftmann@27484  1316  "! x y. x <= y \ f x <= f y"  haftmann@27484  1317  "(a::('a::{ord, zero}) matrix) <= b"  haftmann@27484  1318  shows  haftmann@27484  1319  "apply_matrix f a <= apply_matrix f b"  wenzelm@35612  1320  using assms by (simp add: le_matrix_def)  haftmann@27484  1321 haftmann@27484  1322 lemma le_combine_matrix:  haftmann@27484  1323  assumes  haftmann@27484  1324  "f 0 0 = 0"  haftmann@27484  1325  "! a b c d. a <= b & c <= d \ f a c <= f b d"  haftmann@27484  1326  "A <= B"  haftmann@27484  1327  "C <= D"  haftmann@27484  1328  shows  haftmann@27484  1329  "combine_matrix f A C <= combine_matrix f B D"  wenzelm@35612  1330  using assms by (simp add: le_matrix_def)  haftmann@27484  1331 haftmann@27484  1332 lemma le_left_combine_matrix:  haftmann@27484  1333  assumes  haftmann@27484  1334  "f 0 0 = 0"  haftmann@27484  1335  "! a b c. a <= b \ f c a <= f c b"  haftmann@27484  1336  "A <= B"  haftmann@27484  1337  shows  haftmann@27484  1338  "combine_matrix f C A <= combine_matrix f C B"  wenzelm@35612  1339  using assms by (simp add: le_matrix_def)  haftmann@27484  1340 haftmann@27484  1341 lemma le_right_combine_matrix:  haftmann@27484  1342  assumes  haftmann@27484  1343  "f 0 0 = 0"  haftmann@27484  1344  "! a b c. a <= b \ f a c <= f b c"  haftmann@27484  1345  "A <= B"  haftmann@27484  1346  shows  haftmann@27484  1347  "combine_matrix f A C <= combine_matrix f B C"  wenzelm@35612  1348  using assms by (simp add: le_matrix_def)  haftmann@27484  1349 haftmann@27484  1350 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"  haftmann@27484  1351  by (simp add: le_matrix_def, auto)  haftmann@27484  1352 haftmann@27484  1353 lemma le_foldseq:  haftmann@27484  1354  assumes  haftmann@27484  1355  "! a b c d . a <= b & c <= d \ f a c <= f b d"  haftmann@27484  1356  "! i. i <= n \ s i <= t i"  haftmann@27484  1357  shows  haftmann@27484  1358  "foldseq f s n <= foldseq f t n"  haftmann@27484  1359 proof -  wenzelm@35612  1360  have "! s t. (! i. i<=n \ s i <= t i) \ foldseq f s n <= foldseq f t n"  wenzelm@35612  1361  by (induct n) (simp_all add: assms)  wenzelm@35612  1362  then show "foldseq f s n <= foldseq f t n" using assms by simp  haftmann@27484  1363 qed  haftmann@27484  1364 haftmann@27484  1365 lemma le_left_mult:  haftmann@27484  1366  assumes  haftmann@27484  1367  "! a b c d. a <= b & c <= d \ fadd a c <= fadd b d"  haftmann@27484  1368  "! c a b. 0 <= c & a <= b \ fmul c a <= fmul c b"  haftmann@27484  1369  "! a. fmul 0 a = 0"  haftmann@27484  1370  "! a. fmul a 0 = 0"  haftmann@27484  1371  "fadd 0 0 = 0"  haftmann@27484  1372  "0 <= C"  haftmann@27484  1373  "A <= B"  haftmann@27484  1374  shows  haftmann@27484  1375  "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"  wenzelm@35612  1376  using assms  wenzelm@35612  1377  apply (simp add: le_matrix_def Rep_mult_matrix)  haftmann@27484  1378  apply (auto)  haftmann@27484  1379  apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+  haftmann@27484  1380  apply (rule le_foldseq)  wenzelm@35612  1381  apply (auto)  wenzelm@35612  1382  done  haftmann@27484  1383 haftmann@27484  1384 lemma le_right_mult:  haftmann@27484  1385  assumes  haftmann@27484  1386  "! a b c d. a <= b & c <= d \ fadd a c <= fadd b d"  haftmann@27484  1387  "! c a b. 0 <= c & a <= b \ fmul a c <= fmul b c"  haftmann@27484  1388  "! a. fmul 0 a = 0"  haftmann@27484  1389  "! a. fmul a 0 = 0"  haftmann@27484  1390  "fadd 0 0 = 0"  haftmann@27484  1391  "0 <= C"  haftmann@27484  1392  "A <= B"  haftmann@27484  1393  shows  haftmann@27484  1394  "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"  wenzelm@35612  1395  using assms  wenzelm@35612  1396  apply (simp add: le_matrix_def Rep_mult_matrix)  haftmann@27484  1397  apply (auto)  haftmann@27484  1398  apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+  haftmann@27484  1399  apply (rule le_foldseq)  wenzelm@35612  1400  apply (auto)  wenzelm@35612  1401  done  haftmann@27484  1402 haftmann@27484  1403 lemma spec2: "! j i. P j i \ P j i" by blast  haftmann@27484  1404 lemma neg_imp: "(\ Q \ \ P) \ P \ Q" by blast  haftmann@27484  1405 haftmann@27484  1406 lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"  haftmann@27484  1407  by (auto simp add: le_matrix_def)  haftmann@27484  1408 haftmann@27484  1409 lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"  haftmann@27484  1410  apply (auto)  haftmann@27484  1411  apply (simp add: le_matrix_def)  haftmann@27484  1412  apply (drule_tac j=j and i=i in spec2)  haftmann@27484  1413  apply (simp)  haftmann@27484  1414  apply (simp add: le_matrix_def)  haftmann@27484  1415  done  haftmann@27484  1416 haftmann@27484  1417 lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"  haftmann@27484  1418  apply (auto)  haftmann@27484  1419  apply (simp add: le_matrix_def)  haftmann@27484  1420  apply (drule_tac j=j and i=i in spec2)  haftmann@27484  1421  apply (simp)  haftmann@27484  1422  apply (simp add: le_matrix_def)  haftmann@27484  1423  done  haftmann@27484  1424 haftmann@27484  1425 lemma move_matrix_le_zero[simp]: "0 <= j \ 0 <= i \ (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"  huffman@46702  1426  apply (auto simp add: le_matrix_def)  haftmann@27484  1427  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)  haftmann@27484  1428  apply (auto)  haftmann@27484  1429  done  haftmann@27484  1430 haftmann@27484  1431 lemma move_matrix_zero_le[simp]: "0 <= j \ 0 <= i \ (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"  huffman@46702  1432  apply (auto simp add: le_matrix_def)  haftmann@27484  1433  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)  haftmann@27484  1434  apply (auto)  haftmann@27484  1435  done  haftmann@27484  1436 haftmann@27484  1437 lemma move_matrix_le_move_matrix_iff[simp]: "0 <= j \ 0 <= i \ (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))"  huffman@46702  1438  apply (auto simp add: le_matrix_def)  haftmann@27484  1439  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)  haftmann@27484  1440  apply (auto)  haftmann@27484  1441  done  haftmann@27484  1442 haftmann@27580  1443 instantiation matrix :: ("{lattice, zero}") lattice  haftmann@25764  1444 begin  haftmann@25764  1445 haftmann@37765  1446 definition "inf = combine_matrix inf"  haftmann@25764  1447 haftmann@37765  1448 definition "sup = combine_matrix sup"  haftmann@25764  1449 haftmann@25764  1450 instance  wenzelm@46985  1451  by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)  haftmann@22452  1452 haftmann@25764  1453 end  haftmann@25764  1454 haftmann@25764  1455 instantiation matrix :: ("{plus, zero}") plus  haftmann@25764  1456 begin  haftmann@25764  1457 haftmann@25764  1458 definition  haftmann@37765  1459  plus_matrix_def: "A + B = combine_matrix (op +) A B"  haftmann@25764  1460 haftmann@25764  1461 instance ..  haftmann@25764  1462 haftmann@25764  1463 end  haftmann@25764  1464 haftmann@25764  1465 instantiation matrix :: ("{uminus, zero}") uminus  haftmann@25764  1466 begin  haftmann@25764  1467 haftmann@25764  1468 definition  haftmann@37765  1469  minus_matrix_def: "- A = apply_matrix uminus A"  haftmann@25764  1470 haftmann@25764  1471 instance ..  haftmann@25764  1472 haftmann@25764  1473 end  haftmann@25764  1474 haftmann@25764  1475 instantiation matrix :: ("{minus, zero}") minus  haftmann@25764  1476 begin  obua@14593  1477 haftmann@25764  1478 definition  haftmann@37765  1479  diff_matrix_def: "A - B = combine_matrix (op -) A B"  haftmann@25764  1480 haftmann@25764  1481 instance ..  haftmann@25764  1482 haftmann@25764  1483 end  haftmann@25764  1484 haftmann@25764  1485 instantiation matrix :: ("{plus, times, zero}") times  haftmann@25764  1486 begin  haftmann@25764  1487 haftmann@25764  1488 definition  haftmann@37765  1489  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"  obua@14940  1490 haftmann@25764  1491 instance ..  haftmann@25764  1492 haftmann@25764  1493 end  haftmann@25764  1494 haftmann@27653  1495 instantiation matrix :: ("{lattice, uminus, zero}") abs  haftmann@25764  1496 begin  obua@14940  1497 haftmann@25764  1498 definition  haftmann@37765  1499  abs_matrix_def: "abs (A \ 'a matrix) = sup A (- A)"  haftmann@25764  1500 haftmann@25764  1501 instance ..  haftmann@25764  1502 haftmann@25764  1503 end  haftmann@23879  1504 haftmann@27653  1505 instance matrix :: (monoid_add) monoid_add  haftmann@27653  1506 proof  haftmann@27653  1507  fix A B C :: "'a matrix"  obua@14940  1508  show "A + B + C = A + (B + C)"  obua@14940  1509  apply (simp add: plus_matrix_def)  obua@14940  1510  apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])  obua@14940  1511  apply (simp_all add: add_assoc)  obua@14940  1512  done  haftmann@27653  1513  show "0 + A = A"  haftmann@27653  1514  apply (simp add: plus_matrix_def)  haftmann@27653  1515  apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])  haftmann@27653  1516  apply (simp)  haftmann@27653  1517  done  haftmann@27653  1518  show "A + 0 = A"  haftmann@27653  1519  apply (simp add: plus_matrix_def)  haftmann@27653  1520  apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec])  haftmann@27653  1521  apply (simp)  haftmann@27653  1522  done  haftmann@27653  1523 qed  haftmann@27653  1524 haftmann@27653  1525 instance matrix :: (comm_monoid_add) comm_monoid_add  haftmann@27653  1526 proof  haftmann@27653  1527  fix A B :: "'a matrix"  obua@14940  1528  show "A + B = B + A"  obua@14940  1529  apply (simp add: plus_matrix_def)  obua@14940  1530  apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])  obua@14940  1531  apply (simp_all add: add_commute)  obua@14940  1532  done  obua@14940  1533  show "0 + A = A"  obua@14940  1534  apply (simp add: plus_matrix_def)  obua@14940  1535  apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])  obua@14940  1536  apply (simp)  obua@14940  1537  done  haftmann@27653  1538 qed  haftmann@27653  1539 haftmann@27653  1540 instance matrix :: (group_add) group_add  haftmann@27653  1541 proof  haftmann@27653  1542  fix A B :: "'a matrix"  haftmann@27653  1543  show "- A + A = 0"  haftmann@27653  1544  by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)  haftmann@54230  1545  show "A + - B = A - B"  haftmann@54230  1546  by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext)  haftmann@27653  1547 qed  haftmann@27653  1548 haftmann@27653  1549 instance matrix :: (ab_group_add) ab_group_add  haftmann@27653  1550 proof  haftmann@27653  1551  fix A B :: "'a matrix"  obua@14940  1552  show "- A + A = 0"  obua@14940  1553  by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)  obua@14940  1554  show "A - B = A + - B"  obua@14940  1555  by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)  haftmann@27653  1556 qed  haftmann@27653  1557 haftmann@35028  1558 instance matrix :: (ordered_ab_group_add) ordered_ab_group_add  haftmann@27653  1559 proof  haftmann@27653  1560  fix A B C :: "'a matrix"  obua@14940  1561  assume "A <= B"  obua@14940  1562  then show "C + A <= C + B"  obua@14940  1563  apply (simp add: plus_matrix_def)  obua@14940  1564  apply (rule le_left_combine_matrix)  obua@14940  1565  apply (simp_all)  obua@14940  1566  done  obua@14940  1567 qed  haftmann@27653  1568   haftmann@35028  1569 instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add ..  haftmann@35028  1570 instance matrix :: (lattice_ab_group_add) semilattice_sup_ab_group_add ..  obua@14593  1571 hoelzl@34872  1572 instance matrix :: (semiring_0) semiring_0  obua@14940  1573 proof  haftmann@27653  1574  fix A B C :: "'a matrix"  obua@14940  1575  show "A * B * C = A * (B * C)"  obua@14940  1576  apply (simp add: times_matrix_def)  obua@14940  1577  apply (rule mult_matrix_assoc)  nipkow@29667  1578  apply (simp_all add: associative_def algebra_simps)  obua@14940  1579  done  obua@14940  1580  show "(A + B) * C = A * C + B * C"  obua@14940  1581  apply (simp add: times_matrix_def plus_matrix_def)  obua@14940  1582  apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])  nipkow@29667  1583  apply (simp_all add: associative_def commutative_def algebra_simps)  obua@14940  1584  done  obua@14940  1585  show "A * (B + C) = A * B + A * C"  obua@14940  1586  apply (simp add: times_matrix_def plus_matrix_def)  obua@14940  1587  apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])  nipkow@29667  1588  apply (simp_all add: associative_def commutative_def algebra_simps)  haftmann@27653  1589  done  hoelzl@34872  1590  show "0 * A = 0" by (simp add: times_matrix_def)  hoelzl@34872  1591  show "A * 0 = 0" by (simp add: times_matrix_def)  hoelzl@34872  1592 qed  hoelzl@34872  1593 hoelzl@34872  1594 instance matrix :: (ring) ring ..  haftmann@27653  1595 haftmann@35028  1596 instance matrix :: (ordered_ring) ordered_ring  haftmann@27653  1597 proof  haftmann@27653  1598  fix A B C :: "'a matrix"  obua@14940  1599  assume a: "A \ B"  obua@14940  1600  assume b: "0 \ C"  obua@14940  1601  from a b show "C * A \ C * B"  obua@14940  1602  apply (simp add: times_matrix_def)  obua@14940  1603  apply (rule le_left_mult)  obua@14940  1604  apply (simp_all add: add_mono mult_left_mono)  obua@14940  1605  done  obua@14940  1606  from a b show "A * C \ B * C"  obua@14940  1607  apply (simp add: times_matrix_def)  obua@14940  1608  apply (rule le_right_mult)  obua@14940  1609  apply (simp_all add: add_mono mult_right_mono)  obua@14940  1610  done  haftmann@27653  1611 qed  haftmann@27653  1612 haftmann@35028  1613 instance matrix :: (lattice_ring) lattice_ring  haftmann@27653  1614 proof  haftmann@35028  1615  fix A B C :: "('a :: lattice_ring) matrix"  haftmann@27653  1616  show "abs A = sup A (-A)"  haftmann@27653  1617  by (simp add: abs_matrix_def)  haftmann@27653  1618 qed  obua@14593  1619 haftmann@25303  1620 lemma Rep_matrix_add[simp]:  haftmann@27653  1621  "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i = (Rep_matrix a j i) + (Rep_matrix b j i)"  haftmann@27653  1622  by (simp add: plus_matrix_def)  obua@14593  1623 hoelzl@34872  1624 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i =  obua@14940  1625  foldseq (op +) (% k. (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"  obua@14940  1626 apply (simp add: times_matrix_def)  obua@14940  1627 apply (simp add: Rep_mult_matrix)  obua@14940  1628 done  obua@14593  1629 haftmann@27653  1630 lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \ f 0 = (0::'a)  haftmann@27653  1631  \ apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"  obua@14940  1632 apply (subst Rep_matrix_inject[symmetric])  obua@14593  1633 apply (rule ext)+  obua@14940  1634 apply (simp)  obua@14940  1635 done  obua@14593  1636 haftmann@27653  1637 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"  obua@14940  1638 apply (subst Rep_matrix_inject[symmetric])  obua@14940  1639 apply (rule ext)+  obua@14940  1640 apply (simp)  obua@14940  1641 done  obua@14593  1642 hoelzl@34872  1643 lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) <= nrows A"  obua@14593  1644 by (simp add: times_matrix_def mult_nrows)  obua@14593  1645 hoelzl@34872  1646 lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) <= ncols B"  obua@14593  1647 by (simp add: times_matrix_def mult_ncols)  obua@14593  1648 haftmann@22422  1649 definition  haftmann@22422  1650  one_matrix :: "nat \ ('a::{zero,one}) matrix" where  haftmann@22422  1651  "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"  obua@14593  1652 obua@14593  1653 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"  obua@14593  1654 apply (simp add: one_matrix_def)  paulson@15481  1655 apply (simplesubst RepAbs_matrix)  obua@14593  1656 apply (rule exI[of _ n], simp add: split_if)+  nipkow@16733  1657 by (simp add: split_if)  obua@14593  1658 wenzelm@20633  1659 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")  obua@14593  1660 proof -  obua@14593  1661  have "?r <= n" by (simp add: nrows_le)  obua@14940  1662  moreover have "n <= ?r" by (simp add:le_nrows, arith)  obua@14593  1663  ultimately show "?r = n" by simp  obua@14593  1664 qed  obua@14593  1665 wenzelm@20633  1666 lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")  obua@14593  1667 proof -  obua@14593  1668  have "?r <= n" by (simp add: ncols_le)  obua@14593  1669  moreover have "n <= ?r" by (simp add: le_ncols, arith)  obua@14593  1670  ultimately show "?r = n" by simp  obua@14593  1671 qed  obua@14593  1672 hoelzl@34872  1673 lemma one_matrix_mult_right[simp]: "ncols A <= n \ (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"  obua@14593  1674 apply (subst Rep_matrix_inject[THEN sym])  obua@14593  1675 apply (rule ext)+  obua@14593  1676 apply (simp add: times_matrix_def Rep_mult_matrix)  obua@14593  1677 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])  obua@14593  1678 apply (simp_all)  nipkow@32440  1679 by (simp add: ncols)  obua@14593  1680 hoelzl@34872  1681 lemma one_matrix_mult_left[simp]: "nrows A <= n \ (one_matrix n) * A = (A::('a::semiring_1) matrix)"  obua@14593  1682 apply (subst Rep_matrix_inject[THEN sym])  obua@14593  1683 apply (rule ext)+  obua@14593  1684 apply (simp add: times_matrix_def Rep_mult_matrix)  obua@14593  1685 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])  obua@14593  1686 apply (simp_all)  nipkow@32440  1687 by (simp add: nrows)  obua@14593  1688 haftmann@27653  1689 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"  obua@14940  1690 apply (simp add: times_matrix_def)  obua@14940  1691 apply (subst transpose_mult_matrix)  obua@14940  1692 apply (simp_all add: mult_commute)  obua@14940  1693 done  obua@14940  1694 haftmann@27653  1695 lemma transpose_matrix_add: "transpose_matrix ((A::('a::monoid_add) matrix)+B) = transpose_matrix A + transpose_matrix B"  obua@14940  1696 by (simp add: plus_matrix_def transpose_combine_matrix)  obua@14940  1697 haftmann@27653  1698 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"  obua@14940  1699 by (simp add: diff_matrix_def transpose_combine_matrix)  obua@14940  1700 haftmann@27653  1701 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"  obua@14940  1702 by (simp add: minus_matrix_def transpose_apply_matrix)  obua@14940  1703 haftmann@35416  1704 definition right_inverse_matrix :: "('a::{ring_1}) matrix \ 'a matrix \ bool" where  obua@14940  1705  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \ nrows X \ ncols A"  haftmann@35416  1706 haftmann@35416  1707 definition left_inverse_matrix :: "('a::{ring_1}) matrix \ 'a matrix \ bool" where  obua@14940  1708  "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \ ncols X \ nrows A"  haftmann@35416  1709 haftmann@35416  1710 definition inverse_matrix :: "('a::{ring_1}) matrix \ 'a matrix \ bool" where  obua@14940  1711  "inverse_matrix A X == (right_inverse_matrix A X) \ (left_inverse_matrix A X)"  obua@14593  1712 obua@14593  1713 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \ nrows A = ncols X"  obua@14593  1714 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])  obua@14593  1715 by (simp add: right_inverse_matrix_def)  obua@14593  1716 obua@14940  1717 lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \ ncols A = nrows Y"  obua@14940  1718 apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A])  obua@14940  1719 by (simp add: left_inverse_matrix_def)  obua@14940  1720 obua@14940  1721 lemma left_right_inverse_matrix_unique:  obua@14940  1722  assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"  obua@14940  1723  shows "X = Y"  obua@14940  1724 proof -  obua@14940  1725  have "Y = Y * one_matrix (nrows A)"  obua@14940  1726  apply (subst one_matrix_mult_right)  wenzelm@35612  1727  using assms  wenzelm@35612  1728  apply (simp_all add: left_inverse_matrix_def)  wenzelm@35612  1729  done  obua@14940  1730  also have "\ = Y * (A * X)"  wenzelm@35612  1731  apply (insert assms)  obua@14940  1732  apply (frule right_inverse_matrix_dim)  obua@14940  1733  by (simp add: right_inverse_matrix_def)  obua@14940  1734  also have "\ = (Y * A) * X" by (simp add: mult_assoc)  obua@14940  1735  also have "\ = X"  wenzelm@35612  1736  apply (insert assms)  obua@14940  1737  apply (frule left_inverse_matrix_dim)  obua@14940  1738  apply (simp_all add: left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)  obua@14940  1739  done  obua@14940  1740  ultimately show "X = Y" by (simp)  obua@14940  1741 qed  obua@14940  1742 obua@14940  1743 lemma inverse_matrix_inject: "\ inverse_matrix A X; inverse_matrix A Y \ \ X = Y"  obua@14940  1744  by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)  obua@14940  1745 obua@14940  1746 lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"  obua@14940  1747  by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)  obua@14940  1748 hoelzl@34872  1749 lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \ a * b = 0"  obua@14940  1750 by auto  obua@14940  1751 obua@14940  1752 lemma Rep_matrix_zero_imp_mult_zero:  haftmann@35028  1753  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0 \ A * B = (0::('a::lattice_ring) matrix)"  obua@14940  1754 apply (subst Rep_matrix_inject[symmetric])  obua@14940  1755 apply (rule ext)+  obua@14940  1756 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)  obua@14940  1757 done  obua@14940  1758 haftmann@27653  1759 lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \ nrows B <= u \ nrows (A + B) <= u"  obua@14940  1760 apply (simp add: plus_matrix_def)  obua@14940  1761 apply (rule combine_nrows)  obua@14940  1762 apply (simp_all)  obua@14940  1763 done  obua@14940  1764 hoelzl@34872  1765 lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"  obua@14940  1766 apply (subst Rep_matrix_inject[symmetric])  obua@14940  1767 apply (rule ext)+  obua@14940  1768 apply (auto simp add: Rep_matrix_mult foldseq_zero)  obua@14940  1769 apply (rule_tac foldseq_zerotail[symmetric])  obua@14940  1770 apply (auto simp add: nrows zero_imp_mult_zero max2)  obua@14940  1771 apply (rule order_trans)  obua@14940  1772 apply (rule ncols_move_matrix_le)  obua@14940  1773 apply (simp add: max1)  obua@14940  1774 done  obua@14940  1775 hoelzl@34872  1776 lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"  obua@14940  1777 apply (subst Rep_matrix_inject[symmetric])  obua@14940  1778 apply (rule ext)+  obua@14940  1779 apply (auto simp add: Rep_matrix_mult foldseq_zero)  obua@14940  1780 apply (rule_tac foldseq_zerotail[symmetric])  obua@14940  1781 apply (auto simp add: ncols zero_imp_mult_zero max1)  obua@14940  1782 apply (rule order_trans)  obua@14940  1783 apply (rule nrows_move_matrix_le)  obua@14940  1784 apply (simp add: max2)  obua@14940  1785 done  obua@14940  1786 haftmann@27653  1787 lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)"  obua@14940  1788 apply (subst Rep_matrix_inject[symmetric])  obua@14940  1789 apply (rule ext)+  obua@14940  1790 apply (simp)  obua@14940  1791 done  obua@14940  1792 hoelzl@34872  1793 lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"  obua@14940  1794 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)  obua@14940  1795 haftmann@35416  1796 definition scalar_mult :: "('a::ring) \ 'a matrix \ 'a matrix" where  obua@14940  1797  "scalar_mult a m == apply_matrix (op * a) m"  obua@14940  1798 obua@14940  1799 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"  nipkow@23477  1800 by (simp add: scalar_mult_def)  obua@14940  1801 obua@14940  1802 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"  nipkow@29667  1803 by (simp add: scalar_mult_def apply_matrix_add algebra_simps)  obua@14940  1804 obua@14940  1805 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)"  nipkow@23477  1806 by (simp add: scalar_mult_def)  obua@14940  1807 obua@14940  1808 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"  nipkow@23477  1809 apply (subst Rep_matrix_inject[symmetric])  nipkow@23477  1810 apply (rule ext)+  nipkow@23477  1811 apply (auto)  nipkow@23477  1812 done  obua@14940  1813 haftmann@27653  1814 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"  nipkow@23477  1815 by (simp add: minus_matrix_def)  obua@14940  1816 haftmann@35028  1817 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"  nipkow@23477  1818 by (simp add: abs_lattice sup_matrix_def)  obua@14940  1819 obua@14593  1820 end `