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