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