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