src/HOL/Matrix/MatrixGeneral.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 23373 ead82c82da9e
child 25502 9200b36280c0
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Matrix/MatrixGeneral.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 theory MatrixGeneral imports Main begin
     7 
     8 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
     9 
    10 constdefs
    11   nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set"
    12   "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}"
    13 
    14 typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}"
    15 apply (rule_tac x="(% j i. 0)" in exI)
    16 by (simp add: nonzero_positions_def)
    17 
    18 declare Rep_matrix_inverse[simp]
    19 
    20 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
    21 apply (rule Abs_matrix_induct)
    22 by (simp add: Abs_matrix_inverse matrix_def)
    23 
    24 constdefs
    25   nrows :: "('a::zero) matrix \<Rightarrow> nat"
    26   "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
    27   ncols :: "('a::zero) matrix \<Rightarrow> nat"
    28   "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
    29 
    30 lemma nrows:
    31   assumes hyp: "nrows A \<le> m"
    32   shows "(Rep_matrix A m n) = 0" (is ?concl)
    33 proof cases
    34   assume "nonzero_positions(Rep_matrix A) = {}"
    35   then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
    36 next
    37   assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
    38   let ?S = "fst`(nonzero_positions(Rep_matrix A))"
    39   from a have b: "?S \<noteq> {}" by (simp)
    40   have c: "finite (?S)" by (simp add: finite_nonzero_positions)
    41   from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
    42   have "m \<notin> ?S"
    43     proof -
    44       have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge[OF c b])
    45       moreover from d have "~(m <= Max ?S)" by (simp)
    46       ultimately show "m \<notin> ?S" by (auto)
    47     qed
    48   thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
    49 qed
    50 
    51 constdefs
    52   transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
    53   "transpose_infmatrix A j i == A i j"
    54   transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"
    55   "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"
    56 
    57 declare transpose_infmatrix_def[simp]
    58 
    59 lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"
    60 by ((rule ext)+, simp)
    61 
    62 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
    63   apply (rule ext)+
    64   by (simp add: transpose_infmatrix_def)
    65 
    66 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
    67 apply (rule Abs_matrix_inverse)
    68 apply (simp add: matrix_def nonzero_positions_def image_def)
    69 proof -
    70   let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
    71   let ?swap = "% pos. (snd pos, fst pos)"
    72   let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
    73   have swap_image: "?swap`?A = ?B"
    74     apply (simp add: image_def)
    75     apply (rule set_ext)
    76     apply (simp)
    77     proof
    78       fix y
    79       assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
    80       thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    81         proof -
    82           from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
    83           then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
    84         qed
    85     next
    86       fix y
    87       assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    88       show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
    89 	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
    90     qed
    91   then have "finite (?swap`?A)"
    92     proof -
    93       have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
    94       then have "finite ?B" by (simp add: nonzero_positions_def)
    95       with swap_image show "finite (?swap`?A)" by (simp)
    96     qed
    97   moreover
    98   have "inj_on ?swap ?A" by (simp add: inj_on_def)
    99   ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
   100 qed
   101 
   102 lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
   103 
   104 lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
   105 apply (auto)
   106 apply (rule ext)+
   107 apply (simp add: transpose_infmatrix)
   108 apply (drule infmatrixforward)
   109 apply (simp)
   110 done
   111 
   112 lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
   113 apply (simp add: transpose_matrix_def)
   114 apply (subst Rep_matrix_inject[THEN sym])+
   115 apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
   116 done
   117 
   118 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
   119 by (simp add: transpose_matrix_def)
   120 
   121 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
   122 by (simp add: transpose_matrix_def)
   123 
   124 lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"
   125 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   126 
   127 lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"
   128 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   129 
   130 lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"
   131 proof -
   132   assume "ncols A <= n"
   133   then have "nrows (transpose_matrix A) <= n" by (simp)
   134   then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)
   135   thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)
   136 qed
   137 
   138 lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
   139 apply (auto)
   140 apply (simp add: ncols)
   141 proof (simp add: ncols_def, auto)
   142   let ?P = "nonzero_positions (Rep_matrix A)"
   143   let ?p = "snd`?P"
   144   have a:"finite ?p" by (simp add: finite_nonzero_positions)
   145   let ?m = "Max ?p"
   146   assume "~(Suc (?m) <= n)"
   147   then have b:"n <= ?m" by (simp)
   148   fix a b
   149   assume "(a,b) \<in> ?P"
   150   then have "?p \<noteq> {}" by (auto)
   151   with a have "?m \<in>  ?p" by (simp)
   152   moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
   153   ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
   154   moreover assume ?st
   155   ultimately show "False" using b by (simp)
   156 qed
   157 
   158 lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   159 proof -
   160   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   161   show ?concl by (simp add: a ncols_le)
   162 qed
   163 
   164 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)
   165 apply (auto)
   166 apply (subgoal_tac "ncols A <= m")
   167 apply (simp)
   168 apply (simp add: ncols_le)
   169 apply (drule_tac x="ncols A" in spec)
   170 by (simp add: ncols)
   171 
   172 lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
   173 proof -
   174   have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)
   175   also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
   176   also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
   177   finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
   178 qed
   179 
   180 lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   181 proof -
   182   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   183   show ?concl by (simp add: a nrows_le)
   184 qed
   185 
   186 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)
   187 apply (auto)
   188 apply (subgoal_tac "nrows A <= m")
   189 apply (simp)
   190 apply (simp add: nrows_le)
   191 apply (drule_tac x="nrows A" in spec)
   192 by (simp add: nrows)
   193 
   194 lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
   195 apply (case_tac "nrows A <= m")
   196 apply (simp_all add: nrows)
   197 done
   198 
   199 lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
   200 apply (case_tac "ncols A <= n")
   201 apply (simp_all add: ncols)
   202 done
   203 
   204 lemma finite_natarray1: "finite {x. x < (n::nat)}"
   205 apply (induct n)
   206 apply (simp)
   207 proof -
   208   fix n
   209   have "{x. x < Suc n} = insert n {x. x < n}"  by (rule set_ext, simp, arith)
   210   moreover assume "finite {x. x < n}"
   211   ultimately show "finite {x. x < Suc n}" by (simp)
   212 qed
   213 
   214 lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
   215   apply (induct m)
   216   apply (simp+)
   217   proof -
   218     fix m::nat
   219     let ?s0 = "{pos. fst pos < m & snd pos < n}"
   220     let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
   221     let ?sd = "{pos. fst pos = m & snd pos < n}"
   222     assume f0: "finite ?s0"
   223     have f1: "finite ?sd"
   224     proof -
   225       let ?f = "% x. (m, x)"
   226       have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
   227       moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
   228       ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
   229     qed
   230     have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith)
   231     from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
   232     with su show "finite ?s1" by (simp)
   233 qed
   234 
   235 lemma RepAbs_matrix:
   236   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)
   237   shows "(Rep_matrix (Abs_matrix x)) = x"
   238 apply (rule Abs_matrix_inverse)
   239 apply (simp add: matrix_def nonzero_positions_def)
   240 proof -
   241   from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
   242   from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
   243   let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
   244   let ?v = "{pos. fst pos < m & snd pos < n}"
   245   have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
   246   from a b have "(?u \<inter> (-?v)) = {}"
   247     apply (simp)
   248     apply (rule set_ext)
   249     apply (simp)
   250     apply auto
   251     by (rule c, auto)+
   252   then have d: "?u \<subseteq> ?v" by blast
   253   moreover have "finite ?v" by (simp add: finite_natarray2)
   254   ultimately show "finite ?u" by (rule finite_subset)
   255 qed
   256 
   257 constdefs
   258   apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
   259   "apply_infmatrix f == % A. (% j i. f (A j i))"
   260   apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
   261   "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
   262   combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
   263   "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
   264   combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
   265   "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
   266 
   267 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
   268 by (simp add: apply_infmatrix_def)
   269 
   270 lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
   271 by (simp add: combine_infmatrix_def)
   272 
   273 constdefs
   274 commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
   275 "commutative f == ! x y. f x y = f y x"
   276 associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   277 "associative f == ! x y z. f (f x y) z = f x (f y z)"
   278 
   279 text{*
   280 To reason about associativity and commutativity of operations on matrices,
   281 let's take a step back and look at the general situtation: Assume that we have
   282 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.
   283 Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.
   284 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.$
   285 *}
   286 
   287 lemma combine_infmatrix_commute:
   288   "commutative f \<Longrightarrow> commutative (combine_infmatrix f)"
   289 by (simp add: commutative_def combine_infmatrix_def)
   290 
   291 lemma combine_matrix_commute:
   292 "commutative f \<Longrightarrow> commutative (combine_matrix f)"
   293 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
   294 
   295 text{*
   296 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\}$,
   297 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
   298 \[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
   299 but on the other hand we have
   300 \[ f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.\]
   301 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:
   302 *}
   303 
   304 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)"
   305 by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)
   306 
   307 lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
   308 by (insert Rep_matrix [of A], simp add: matrix_def)
   309 
   310 lemma combine_infmatrix_closed [simp]:
   311   "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)"
   312 apply (rule Abs_matrix_inverse)
   313 apply (simp add: matrix_def)
   314 apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])
   315 by (simp_all)
   316 
   317 text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}
   318 lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"
   319 by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)
   320 
   321 lemma apply_infmatrix_closed [simp]:
   322   "f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"
   323 apply (rule Abs_matrix_inverse)
   324 apply (simp add: matrix_def)
   325 apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])
   326 by (simp_all)
   327 
   328 lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"
   329 by (simp add: associative_def combine_infmatrix_def)
   330 
   331 lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
   332 by (auto)
   333 
   334 lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"
   335 apply (simp(no_asm) add: associative_def combine_matrix_def, auto)
   336 apply (rule comb [of Abs_matrix Abs_matrix])
   337 by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)
   338 
   339 lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"
   340 by (simp add: apply_matrix_def)
   341 
   342 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)"
   343   by(simp add: combine_matrix_def)
   344 
   345 lemma combine_nrows: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
   346 by (simp add: nrows_le)
   347 
   348 lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
   349 by (simp add: ncols_le)
   350 
   351 lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
   352   by (simp add: nrows_le)
   353 
   354 lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
   355   by (simp add: ncols_le)
   356 
   357 constdefs
   358   zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
   359   "zero_r_neutral f == ! a. f a 0 = a"
   360   zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   361   "zero_l_neutral f == ! a. f 0 a = a"
   362   zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
   363   "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
   364 
   365 consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   366 primrec
   367   "foldseq f s 0 = s 0"
   368   "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
   369 
   370 consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   371 primrec
   372   "foldseq_transposed f s 0 = s 0"
   373   "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
   374 
   375 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
   376 proof -
   377   assume a:"associative f"
   378   then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   379   proof -
   380     fix n
   381     show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   382     proof (induct n)
   383       show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
   384     next
   385       fix n
   386       assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   387       have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
   388       show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
   389       proof (auto)
   390         fix N t
   391         assume Nsuc: "N <= Suc n"
   392         show "foldseq f t N = foldseq_transposed f t N"
   393         proof cases
   394           assume "N <= n"
   395           then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
   396         next
   397           assume "~(N <= n)"
   398           with Nsuc have Nsuceq: "N = Suc n" by simp
   399           have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
   400           have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
   401           show "foldseq f t N = foldseq_transposed f t N"
   402             apply (simp add: Nsuceq)
   403             apply (subst c)
   404             apply (simp)
   405             apply (case_tac "n = 0")
   406             apply (simp)
   407             apply (drule neqz)
   408             apply (erule exE)
   409             apply (simp)
   410             apply (subst assocf)
   411             proof -
   412               fix m
   413               assume "n = Suc m & Suc m <= n"
   414               then have mless: "Suc m <= n" by arith
   415               then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")
   416                 apply (subst c)
   417                 by simp+
   418               have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
   419               have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
   420                 apply (subst c)
   421                 by (simp add: mless)+
   422               have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
   423               from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
   424             qed
   425           qed
   426         qed
   427       qed
   428     qed
   429     show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
   430   qed
   431 
   432 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)"
   433 proof -
   434   assume assoc: "associative f"
   435   assume comm: "commutative f"
   436   from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)
   437   from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)
   438   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)
   439   have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
   440     apply (induct_tac n)
   441     apply (simp+, auto)
   442     by (simp add: a b c)
   443   then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
   444 qed
   445 
   446 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)"
   447 oops
   448 (* Model found
   449 
   450 Trying to find a model that refutes: \<lbrakk>associative f; associative g;
   451  \<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;
   452  \<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk>
   453 \<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y)
   454 Searching for a model of size 1, translating term... invoking SAT solver... no model found.
   455 Searching for a model of size 2, translating term... invoking SAT solver... no model found.
   456 Searching for a model of size 3, translating term... invoking SAT solver...
   457 Model found:
   458 Size of types: 'a: 3
   459 x: a1
   460 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))
   461 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))
   462 *)
   463 
   464 lemma foldseq_zero:
   465 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"
   466 shows "foldseq f s n = 0"
   467 proof -
   468   have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
   469     apply (induct_tac n)
   470     apply (simp)
   471     by (simp add: fz)
   472   then show "foldseq f s n = 0" by (simp add: sz)
   473 qed
   474 
   475 lemma foldseq_significant_positions:
   476   assumes p: "! i. i <= N \<longrightarrow> S i = T i"
   477   shows "foldseq f S N = foldseq f T N" (is ?concl)
   478 proof -
   479   have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
   480     apply (induct_tac m)
   481     apply (simp)
   482     apply (simp)
   483     apply (auto)
   484     proof -
   485       fix n
   486       fix s::"nat\<Rightarrow>'a"
   487       fix t::"nat\<Rightarrow>'a"
   488       assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
   489       assume b: "\<forall>i\<le>Suc n. s i = t i"
   490       have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast
   491       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)
   492       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)
   493     qed
   494   with p show ?concl by simp
   495 qed
   496 
   497 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")
   498 proof -
   499   have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
   500   have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
   501   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"
   502     apply (induct_tac n)
   503     apply (simp)
   504     apply (simp)
   505     apply (auto)
   506     apply (case_tac "m = Suc na")
   507     apply (simp)
   508     apply (rule a)
   509     apply (rule foldseq_significant_positions)
   510     apply (auto)
   511     apply (drule suc, simp+)
   512     proof -
   513       fix na m s
   514       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"
   515       assume subb:"m <= na"
   516       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
   517       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 =
   518         foldseq f (% k. s(Suc k)) na"
   519         by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)
   520       from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith
   521       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) =
   522         foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
   523         apply (simp add: subd)
   524         apply (case_tac "m=0")
   525         apply (simp)
   526         apply (drule sube)
   527         apply (auto)
   528         apply (rule a)
   529         by (simp add: subc if_def)
   530     qed
   531   then show "?p \<Longrightarrow> ?concl" by simp
   532 qed
   533 
   534 lemma foldseq_zerotail:
   535   assumes
   536   fz: "f 0 0 = 0"
   537   and sz: "! i.  n <= i \<longrightarrow> s i = 0"
   538   and nm: "n <= m"
   539   shows
   540   "foldseq f s n = foldseq f s m"
   541 proof -
   542   show "foldseq f s n = foldseq f s m"
   543     apply (simp add: foldseq_tail[OF nm, of f s])
   544     apply (rule foldseq_significant_positions)
   545     apply (auto)
   546     apply (subst foldseq_zero)
   547     by (simp add: fz sz)+
   548 qed
   549 
   550 lemma foldseq_zerotail2:
   551   assumes "! x. f x 0 = x"
   552   and "! i. n < i \<longrightarrow> s i = 0"
   553   and nm: "n <= m"
   554   shows
   555   "foldseq f s n = foldseq f s m" (is ?concl)
   556 proof -
   557   have "f 0 0 = 0" by (simp add: prems)
   558   have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
   559   have c: "0 <= m" by simp
   560   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   561   show ?concl
   562     apply (subst foldseq_tail[OF nm])
   563     apply (rule foldseq_significant_positions)
   564     apply (auto)
   565     apply (case_tac "m=n")
   566     apply (simp+)
   567     apply (drule b[OF nm])
   568     apply (auto)
   569     apply (case_tac "k=0")
   570     apply (simp add: prems)
   571     apply (drule d)
   572     apply (auto)
   573     by (simp add: prems foldseq_zero)
   574 qed
   575 
   576 lemma foldseq_zerostart:
   577   "! 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))"
   578 proof -
   579   assume f00x: "! x. f 0 (f 0 x) = f 0 x"
   580   have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
   581     apply (induct n)
   582     apply (simp)
   583     apply (rule allI, rule impI)
   584     proof -
   585       fix n
   586       fix s
   587       have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp
   588       assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"
   589       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
   590       assume d: "! i. i <= Suc n \<longrightarrow> s i = 0"
   591       show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"
   592         apply (subst a)
   593         apply (subst c)
   594         by (simp add: d f00x)+
   595     qed
   596   then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
   597 qed
   598 
   599 lemma foldseq_zerostart2:
   600   "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
   601 proof -
   602   assume a:"! i. i<n \<longrightarrow> s i = 0"
   603   assume x:"! x. f 0 x = x"
   604   from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast
   605   have b: "!! i l. i < Suc l = (i <= l)" by arith
   606   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   607   show "foldseq f s n = s n"
   608   apply (case_tac "n=0")
   609   apply (simp)
   610   apply (insert a)
   611   apply (drule d)
   612   apply (auto)
   613   apply (simp add: b)
   614   apply (insert f00x)
   615   apply (drule foldseq_zerostart)
   616   by (simp add: x)+
   617 qed
   618 
   619 lemma foldseq_almostzero:
   620   assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
   621   shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
   622 proof -
   623   from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
   624   from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
   625   show ?concl
   626     apply auto
   627     apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
   628     apply simp
   629     apply (subst foldseq_zerostart2)
   630     apply (simp add: f0x a)+
   631     apply (subst foldseq_zero)
   632     by (simp add: s0 f0x)+
   633 qed
   634 
   635 lemma foldseq_distr_unary:
   636   assumes "!! a b. g (f a b) = f (g a) (g b)"
   637   shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
   638 proof -
   639   have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
   640     apply (induct_tac n)
   641     apply (simp)
   642     apply (simp)
   643     apply (auto)
   644     apply (drule_tac x="% k. s (Suc k)" in spec)
   645     by (simp add: prems)
   646   then show ?concl by simp
   647 qed
   648 
   649 constdefs
   650   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"
   651   "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)"
   652   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"
   653   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
   654 
   655 lemma mult_matrix_n:
   656   assumes prems: "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
   657   shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
   658 proof -
   659   show ?concl using prems
   660     apply (simp add: mult_matrix_def mult_matrix_n_def)
   661     apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   662     by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
   663 qed
   664 
   665 lemma mult_matrix_nm:
   666   assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
   667   shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
   668 proof -
   669   from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
   670   also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
   671   finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
   672 qed
   673 
   674 constdefs
   675   r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   676   "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
   677   l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   678   "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
   679   distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   680   "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
   681 
   682 lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
   683 lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
   684 
   685 lemma r_distributive_matrix:
   686  assumes prems:
   687   "r_distributive fmul fadd"
   688   "associative fadd"
   689   "commutative fadd"
   690   "fadd 0 0 = 0"
   691   "! a. fmul a 0 = 0"
   692   "! a. fmul 0 a = 0"
   693  shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   694 proof -
   695   from prems show ?concl
   696     apply (simp add: r_distributive_def mult_matrix_def, auto)
   697     proof -
   698       fix a::"'a matrix"
   699       fix u::"'b matrix"
   700       fix v::"'b matrix"
   701       let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
   702       from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
   703         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)"
   704         apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   705         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   706         apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])
   707         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   708         apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])
   709         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   710         apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
   711         apply (simp add: combine_matrix_def combine_infmatrix_def)
   712         apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   713         apply (simplesubst RepAbs_matrix)
   714         apply (simp, auto)
   715         apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   716         apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
   717         apply (subst RepAbs_matrix)
   718         apply (simp, auto)
   719         apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   720         apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
   721         done
   722     qed
   723 qed
   724 
   725 lemma l_distributive_matrix:
   726  assumes prems:
   727   "l_distributive fmul fadd"
   728   "associative fadd"
   729   "commutative fadd"
   730   "fadd 0 0 = 0"
   731   "! a. fmul a 0 = 0"
   732   "! a. fmul 0 a = 0"
   733  shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   734 proof -
   735   from prems show ?concl
   736     apply (simp add: l_distributive_def mult_matrix_def, auto)
   737     proof -
   738       fix a::"'b matrix"
   739       fix u::"'a matrix"
   740       fix v::"'a matrix"
   741       let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
   742       from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
   743                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)"
   744         apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
   745         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   746         apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])
   747         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   748         apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   749         apply (simp add: max1 max2 combine_nrows combine_ncols)+
   750         apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
   751         apply (simp add: combine_matrix_def combine_infmatrix_def)
   752         apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   753         apply (simplesubst RepAbs_matrix)
   754         apply (simp, auto)
   755         apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
   756         apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   757         apply (subst RepAbs_matrix)
   758         apply (simp, auto)
   759         apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
   760         apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   761         done
   762     qed
   763 qed
   764 
   765 instance matrix :: (zero) zero ..
   766 
   767 defs(overloaded)
   768   zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
   769 
   770 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
   771   apply (simp add: zero_matrix_def)
   772   apply (subst RepAbs_matrix)
   773   by (auto)
   774 
   775 lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
   776 proof -
   777   have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   778   show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
   779 qed
   780 
   781 lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
   782 proof -
   783   have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   784   show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
   785 qed
   786 
   787 lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
   788   by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
   789 
   790 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
   791   by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
   792 
   793 lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
   794   apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
   795   apply (auto)
   796   by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
   797 
   798 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"
   799   apply (simp add: mult_matrix_n_def)
   800   apply (subst foldseq_zero)
   801   by (simp_all add: zero_matrix_def)
   802 
   803 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"
   804   apply (simp add: mult_matrix_n_def)
   805   apply (subst foldseq_zero)
   806   by (simp_all add: zero_matrix_def)
   807 
   808 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"
   809 by (simp add: mult_matrix_def)
   810 
   811 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"
   812 by (simp add: mult_matrix_def)
   813 
   814 lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"
   815   apply (simp add: apply_matrix_def apply_infmatrix_def)
   816   by (simp add: zero_matrix_def)
   817 
   818 lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"
   819   apply (simp add: combine_matrix_def combine_infmatrix_def)
   820   by (simp add: zero_matrix_def)
   821 
   822 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
   823 apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
   824 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   825 apply (simp add: RepAbs_matrix)
   826 done
   827 
   828 lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
   829   apply (simp add: apply_matrix_def apply_infmatrix_def)
   830   by (simp add: zero_matrix_def)
   831 
   832 constdefs
   833   singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"
   834   "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
   835   move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"
   836   "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)))"
   837   take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   838   "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
   839   take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   840   "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
   841 
   842 constdefs
   843   column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   844   "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
   845   row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   846   "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
   847 
   848 lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
   849 apply (simp add: singleton_matrix_def)
   850 apply (auto)
   851 apply (subst RepAbs_matrix)
   852 apply (rule exI[of _ "Suc m"], simp)
   853 apply (rule exI[of _ "Suc n"], simp+)
   854 by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
   855 
   856 lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
   857 apply (subst Rep_matrix_inject[symmetric])
   858 apply (rule ext)+
   859 apply (simp)
   860 done
   861 
   862 lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
   863   by (simp add: singleton_matrix_def zero_matrix_def)
   864 
   865 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
   866 proof-
   867 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   868 from th show ?thesis 
   869 apply (auto)
   870 apply (rule le_anti_sym)
   871 apply (subst nrows_le)
   872 apply (simp add: singleton_matrix_def, auto)
   873 apply (subst RepAbs_matrix)
   874 apply auto
   875 apply (simp add: Suc_le_eq)
   876 apply (rule not_leE)
   877 apply (subst nrows_le)
   878 by simp
   879 qed
   880 
   881 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
   882 proof-
   883 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   884 from th show ?thesis 
   885 apply (auto)
   886 apply (rule le_anti_sym)
   887 apply (subst ncols_le)
   888 apply (simp add: singleton_matrix_def, auto)
   889 apply (subst RepAbs_matrix)
   890 apply auto
   891 apply (simp add: Suc_le_eq)
   892 apply (rule not_leE)
   893 apply (subst ncols_le)
   894 by simp
   895 qed
   896 
   897 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)"
   898 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
   899 apply (subst RepAbs_matrix)
   900 apply (rule exI[of _ "Suc j"], simp)
   901 apply (rule exI[of _ "Suc i"], simp)
   902 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   903 apply (subst RepAbs_matrix)
   904 apply (rule exI[of _ "Suc j"], simp)
   905 apply (rule exI[of _ "Suc i"], simp)
   906 by simp
   907 
   908 lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
   909 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   910 apply (simp)
   911 done
   912 
   913 lemma Rep_move_matrix[simp]:
   914   "Rep_matrix (move_matrix A y x) j i =
   915   (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
   916 apply (simp add: move_matrix_def)
   917 apply (auto)
   918 by (subst RepAbs_matrix,
   919   rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
   920   rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
   921 
   922 lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
   923 by (simp add: move_matrix_def)
   924 
   925 lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
   926 apply (subst Rep_matrix_inject[symmetric])
   927 apply (rule ext)+
   928 apply (simp)
   929 done
   930 
   931 lemma transpose_move_matrix[simp]:
   932   "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
   933 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   934 apply (simp)
   935 done
   936 
   937 lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
   938   (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
   939   apply (subst Rep_matrix_inject[symmetric])
   940   apply (rule ext)+
   941   apply (case_tac "j + int u < 0")
   942   apply (simp, arith)
   943   apply (case_tac "i + int v < 0")
   944   apply (simp add: neg_def, arith)
   945   apply (simp add: neg_def)
   946   apply arith
   947   done
   948 
   949 lemma Rep_take_columns[simp]:
   950   "Rep_matrix (take_columns A c) j i =
   951   (if i < c then (Rep_matrix A j i) else 0)"
   952 apply (simp add: take_columns_def)
   953 apply (simplesubst RepAbs_matrix)
   954 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   955 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   956 done
   957 
   958 lemma Rep_take_rows[simp]:
   959   "Rep_matrix (take_rows A r) j i =
   960   (if j < r then (Rep_matrix A j i) else 0)"
   961 apply (simp add: take_rows_def)
   962 apply (simplesubst RepAbs_matrix)
   963 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   964 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   965 done
   966 
   967 lemma Rep_column_of_matrix[simp]:
   968   "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"
   969   by (simp add: column_of_matrix_def)
   970 
   971 lemma Rep_row_of_matrix[simp]:
   972   "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   973   by (simp add: row_of_matrix_def)
   974 
   975 lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
   976 apply (subst Rep_matrix_inject[THEN sym])
   977 apply (rule ext)+
   978 by (simp add: ncols)
   979 
   980 lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
   981 apply (subst Rep_matrix_inject[THEN sym])
   982 apply (rule ext)+
   983 by (simp add: nrows)
   984 
   985 lemma mult_matrix_singleton_right[simp]:
   986   assumes prems:
   987   "! x. fmul x 0 = 0"
   988   "! x. fmul 0 x = 0"
   989   "! x. fadd 0 x = x"
   990   "! x. fadd x 0 = x"
   991   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))"
   992   apply (simp add: mult_matrix_def)
   993   apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
   994   apply (auto)
   995   apply (simp add: prems)+
   996   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
   997   apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
   998   apply (subst foldseq_almostzero[of _ j])
   999   apply (simp add: prems)+
  1000   apply (auto)
  1001   proof -
  1002     fix k
  1003     fix l
  1004     assume a:"~neg(int l - int i)"
  1005     assume b:"nat (int l - int i) = 0"
  1006     from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
  1007     assume c: "i \<noteq> l"
  1008     from c a show "fmul (Rep_matrix A k j) e = 0" by blast
  1009   qed
  1010 
  1011 lemma mult_matrix_ext:
  1012   assumes
  1013   eprem:
  1014   "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)"
  1015   and fprems:
  1016   "! a. fmul 0 a = 0"
  1017   "! a. fmul a 0 = 0"
  1018   "! a. fadd a 0 = a"
  1019   "! a. fadd 0 a = a"
  1020   and contraprems:
  1021   "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
  1022   shows
  1023   "A = B"
  1024 proof(rule contrapos_np[of "False"], simp)
  1025   assume a: "A \<noteq> B"
  1026   have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
  1027   have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
  1028     apply (rule contrapos_np[of "False"], simp+)
  1029     apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)
  1030     by (simp add: Rep_matrix_inject a)
  1031   then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
  1032   from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast
  1033   let ?S = "singleton_matrix I 0 e"
  1034   let ?comp = "mult_matrix fmul fadd"
  1035   have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
  1036   have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
  1037   have "~(?comp A ?S = ?comp B ?S)"
  1038     apply (rule notI)
  1039     apply (simp add: fprems eprops)
  1040     apply (simp add: Rep_matrix_inject[THEN sym])
  1041     apply (drule d[of _ _ "J"], drule d[of _ _ "0"])
  1042     by (simp add: e c eprops)
  1043   with contraprems show "False" by simp
  1044 qed
  1045 
  1046 constdefs
  1047   foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  1048   "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
  1049   foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  1050   "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
  1051 
  1052 lemma foldmatrix_transpose:
  1053   assumes
  1054   "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  1055   shows
  1056   "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
  1057 proof -
  1058   have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
  1059   have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
  1060     apply (induct n)
  1061     apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
  1062     apply (auto)
  1063     by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
  1064   show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
  1065     apply (simp add: foldmatrix_def foldmatrix_transposed_def)
  1066     apply (induct m, simp)
  1067     apply (simp)
  1068     apply (insert tworows)
  1069     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)
  1070     by (simp add: foldmatrix_def foldmatrix_transposed_def)
  1071 qed
  1072 
  1073 lemma foldseq_foldseq:
  1074 assumes
  1075   "associative f"
  1076   "associative g"
  1077   "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  1078 shows
  1079   "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
  1080   apply (insert foldmatrix_transpose[of g f A m n])
  1081   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
  1082 
  1083 lemma mult_n_nrows:
  1084 assumes
  1085 "! a. fmul 0 a = 0"
  1086 "! a. fmul a 0 = 0"
  1087 "fadd 0 0 = 0"
  1088 shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
  1089 apply (subst nrows_le)
  1090 apply (simp add: mult_matrix_n_def)
  1091 apply (subst RepAbs_matrix)
  1092 apply (rule_tac x="nrows A" in exI)
  1093 apply (simp add: nrows prems foldseq_zero)
  1094 apply (rule_tac x="ncols B" in exI)
  1095 apply (simp add: ncols prems foldseq_zero)
  1096 by (simp add: nrows prems foldseq_zero)
  1097 
  1098 lemma mult_n_ncols:
  1099 assumes
  1100 "! a. fmul 0 a = 0"
  1101 "! a. fmul a 0 = 0"
  1102 "fadd 0 0 = 0"
  1103 shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
  1104 apply (subst ncols_le)
  1105 apply (simp add: mult_matrix_n_def)
  1106 apply (subst RepAbs_matrix)
  1107 apply (rule_tac x="nrows A" in exI)
  1108 apply (simp add: nrows prems foldseq_zero)
  1109 apply (rule_tac x="ncols B" in exI)
  1110 apply (simp add: ncols prems foldseq_zero)
  1111 by (simp add: ncols prems foldseq_zero)
  1112 
  1113 lemma mult_nrows:
  1114 assumes
  1115 "! a. fmul 0 a = 0"
  1116 "! a. fmul a 0 = 0"
  1117 "fadd 0 0 = 0"
  1118 shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
  1119 by (simp add: mult_matrix_def mult_n_nrows prems)
  1120 
  1121 lemma mult_ncols:
  1122 assumes
  1123 "! a. fmul 0 a = 0"
  1124 "! a. fmul a 0 = 0"
  1125 "fadd 0 0 = 0"
  1126 shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
  1127 by (simp add: mult_matrix_def mult_n_ncols prems)
  1128 
  1129 lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
  1130   apply (auto simp add: nrows_le)
  1131   apply (rule nrows)
  1132   apply (arith)
  1133   done
  1134 
  1135 lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
  1136   apply (auto simp add: ncols_le)
  1137   apply (rule ncols)
  1138   apply (arith)
  1139   done
  1140 
  1141 lemma mult_matrix_assoc:
  1142   assumes prems:
  1143   "! a. fmul1 0 a = 0"
  1144   "! a. fmul1 a 0 = 0"
  1145   "! a. fmul2 0 a = 0"
  1146   "! a. fmul2 a 0 = 0"
  1147   "fadd1 0 0 = 0"
  1148   "fadd2 0 0 = 0"
  1149   "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  1150   "associative fadd1"
  1151   "associative fadd2"
  1152   "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  1153   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  1154   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  1155   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)
  1156 proof -
  1157   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
  1158   have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (% k. fmul2 (s k) x) n"
  1159     by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
  1160   have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
  1161       by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
  1162   let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
  1163   show ?concl
  1164     apply (simp add: Rep_matrix_inject[THEN sym])
  1165     apply (rule ext)+
  1166     apply (simp add: mult_matrix_def)
  1167     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)"])
  1168     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  1169     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)+
  1170     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  1171     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  1172     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  1173     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  1174     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  1175     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  1176     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  1177     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  1178     apply (simp add: mult_matrix_n_def)
  1179     apply (rule comb_left)
  1180     apply ((rule ext)+, simp)
  1181     apply (simplesubst RepAbs_matrix)
  1182     apply (rule exI[of _ "nrows B"])
  1183     apply (simp add: nrows prems foldseq_zero)
  1184     apply (rule exI[of _ "ncols C"])
  1185     apply (simp add: prems ncols foldseq_zero)
  1186     apply (subst RepAbs_matrix)
  1187     apply (rule exI[of _ "nrows A"])
  1188     apply (simp add: nrows prems foldseq_zero)
  1189     apply (rule exI[of _ "ncols B"])
  1190     apply (simp add: prems ncols foldseq_zero)
  1191     apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
  1192     apply (subst foldseq_foldseq)
  1193     apply (simp add: prems)+
  1194     by (simp add: transpose_infmatrix)
  1195 qed
  1196 
  1197 lemma
  1198   assumes prems:
  1199   "! a. fmul1 0 a = 0"
  1200   "! a. fmul1 a 0 = 0"
  1201   "! a. fmul2 0 a = 0"
  1202   "! a. fmul2 a 0 = 0"
  1203   "fadd1 0 0 = 0"
  1204   "fadd2 0 0 = 0"
  1205   "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  1206   "associative fadd1"
  1207   "associative fadd2"
  1208   "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  1209   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  1210   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  1211   shows
  1212   "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
  1213 apply (rule ext)+
  1214 apply (simp add: comp_def )
  1215 by (simp add: mult_matrix_assoc prems)
  1216 
  1217 lemma mult_matrix_assoc_simple:
  1218   assumes prems:
  1219   "! a. fmul 0 a = 0"
  1220   "! a. fmul a 0 = 0"
  1221   "fadd 0 0 = 0"
  1222   "associative fadd"
  1223   "commutative fadd"
  1224   "associative fmul"
  1225   "distributive fmul fadd"
  1226   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)
  1227 proof -
  1228   have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
  1229     by (simp! add: associative_def commutative_def)
  1230   then show ?concl
  1231     apply (subst mult_matrix_assoc)
  1232     apply (simp_all!)
  1233     by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
  1234 qed
  1235 
  1236 lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
  1237 apply (simp add: Rep_matrix_inject[THEN sym])
  1238 apply (rule ext)+
  1239 by simp
  1240 
  1241 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)"
  1242 apply (simp add: Rep_matrix_inject[THEN sym])
  1243 apply (rule ext)+
  1244 by simp
  1245 
  1246 lemma Rep_mult_matrix:
  1247   assumes
  1248   "! a. fmul 0 a = 0"
  1249   "! a. fmul a 0 = 0"
  1250   "fadd 0 0 = 0"
  1251   shows
  1252   "Rep_matrix(mult_matrix fmul fadd A B) j i =
  1253   foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
  1254 apply (simp add: mult_matrix_def mult_matrix_n_def)
  1255 apply (subst RepAbs_matrix)
  1256 apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
  1257 apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
  1258 by simp
  1259 
  1260 lemma transpose_mult_matrix:
  1261   assumes
  1262   "! a. fmul 0 a = 0"
  1263   "! a. fmul a 0 = 0"
  1264   "fadd 0 0 = 0"
  1265   "! x y. fmul y x = fmul x y"
  1266   shows
  1267   "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
  1268   apply (simp add: Rep_matrix_inject[THEN sym])
  1269   apply (rule ext)+
  1270   by (simp! add: Rep_mult_matrix max_ac)
  1271 
  1272 lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
  1273 apply (simp add:  Rep_matrix_inject[THEN sym])
  1274 apply (rule ext)+
  1275 by simp
  1276 
  1277 lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
  1278 apply (simp add: Rep_matrix_inject[THEN sym])
  1279 apply (rule ext)+
  1280 by simp
  1281 
  1282 instance matrix :: ("{ord, zero}") ord
  1283   le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
  1284   less_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
  1285 
  1286 instance matrix :: ("{order, zero}") order
  1287 apply intro_classes
  1288 apply (simp_all add: le_matrix_def less_def)
  1289 apply (auto)
  1290 apply (drule_tac x=j in spec, drule_tac x=j in spec)
  1291 apply (drule_tac x=i in spec, drule_tac x=i in spec)
  1292 apply (simp)
  1293 apply (simp add: Rep_matrix_inject[THEN sym])
  1294 apply (rule ext)+
  1295 apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
  1296 apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
  1297 by simp
  1298 
  1299 lemma le_apply_matrix:
  1300   assumes
  1301   "f 0 = 0"
  1302   "! x y. x <= y \<longrightarrow> f x <= f y"
  1303   "(a::('a::{ord, zero}) matrix) <= b"
  1304   shows
  1305   "apply_matrix f a <= apply_matrix f b"
  1306   by (simp! add: le_matrix_def)
  1307 
  1308 lemma le_combine_matrix:
  1309   assumes
  1310   "f 0 0 = 0"
  1311   "! a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"
  1312   "A <= B"
  1313   "C <= D"
  1314   shows
  1315   "combine_matrix f A C <= combine_matrix f B D"
  1316 by (simp! add: le_matrix_def)
  1317 
  1318 lemma le_left_combine_matrix:
  1319   assumes
  1320   "f 0 0 = 0"
  1321   "! a b c. a <= b \<longrightarrow> f c a <= f c b"
  1322   "A <= B"
  1323   shows
  1324   "combine_matrix f C A <= combine_matrix f C B"
  1325   by (simp! add: le_matrix_def)
  1326 
  1327 lemma le_right_combine_matrix:
  1328   assumes
  1329   "f 0 0 = 0"
  1330   "! a b c. a <= b \<longrightarrow> f a c <= f b c"
  1331   "A <= B"
  1332   shows
  1333   "combine_matrix f A C <= combine_matrix f B C"
  1334   by (simp! add: le_matrix_def)
  1335 
  1336 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
  1337   by (simp add: le_matrix_def, auto)
  1338 
  1339 lemma le_foldseq:
  1340   assumes
  1341   "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
  1342   "! i. i <= n \<longrightarrow> s i <= t i"
  1343   shows
  1344   "foldseq f s n <= foldseq f t n"
  1345 proof -
  1346   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!)
  1347   then show "foldseq f s n <= foldseq f t n" by (simp!)
  1348 qed
  1349 
  1350 lemma le_left_mult:
  1351   assumes
  1352   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  1353   "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
  1354   "! a. fmul 0 a = 0"
  1355   "! a. fmul a 0 = 0"
  1356   "fadd 0 0 = 0"
  1357   "0 <= C"
  1358   "A <= B"
  1359   shows
  1360   "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
  1361   apply (simp! add: le_matrix_def Rep_mult_matrix)
  1362   apply (auto)
  1363   apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
  1364   apply (rule le_foldseq)
  1365   by (auto)
  1366 
  1367 lemma le_right_mult:
  1368   assumes
  1369   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  1370   "! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
  1371   "! a. fmul 0 a = 0"
  1372   "! a. fmul a 0 = 0"
  1373   "fadd 0 0 = 0"
  1374   "0 <= C"
  1375   "A <= B"
  1376   shows
  1377   "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
  1378   apply (simp! add: le_matrix_def Rep_mult_matrix)
  1379   apply (auto)
  1380   apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
  1381   apply (rule le_foldseq)
  1382   by (auto)
  1383 
  1384 lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
  1385 lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
  1386 
  1387 lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"
  1388   by (auto simp add: le_matrix_def)
  1389 
  1390 lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"
  1391   apply (auto)
  1392   apply (simp add: le_matrix_def)
  1393   apply (drule_tac j=j and i=i in spec2)
  1394   apply (simp)
  1395   apply (simp add: le_matrix_def)
  1396   done
  1397 
  1398 lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
  1399   apply (auto)
  1400   apply (simp add: le_matrix_def)
  1401   apply (drule_tac j=j and i=i in spec2)
  1402   apply (simp)
  1403   apply (simp add: le_matrix_def)
  1404   done
  1405 
  1406 lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
  1407   apply (auto simp add: le_matrix_def neg_def)
  1408   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  1409   apply (auto)
  1410   done
  1411 
  1412 lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
  1413   apply (auto simp add: le_matrix_def neg_def)
  1414   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  1415   apply (auto)
  1416   done
  1417 
  1418 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))"
  1419   apply (auto simp add: le_matrix_def neg_def)
  1420   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  1421   apply (auto)
  1422   done  
  1423 
  1424 end