added marginal setup for code generation
authorhaftmann
Fri Jul 04 07:39:01 2008 +0200 (2008-07-04 ago)
changeset 27484dbb9981c3d18
parent 27483 7c58324cd418
child 27485 a5de2cbf548f
added marginal setup for code generation
src/HOL/IsaMakefile
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Matrix/ROOT.ML
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Matrix/cplex/Cplex.thy
src/HOL/Matrix/cplex/FloatSparseMatrix.thy
src/HOL/Matrix/cplex/MatrixLP.thy
src/HOL/Matrix/cplex/matrixlp.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Jul 03 20:53:44 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 04 07:39:01 2008 +0200
     1.3 @@ -820,13 +820,12 @@
     1.4    $(SRC)/Tools/Compute_Oracle/linker.ML					\
     1.5    $(SRC)/Tools/Compute_Oracle/am_ghc.ML					\
     1.6    $(SRC)/Tools/Compute_Oracle/am_sml.ML					\
     1.7 -  $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/MatrixGeneral.thy	\
     1.8 +  $(SRC)/Tools/Compute_Oracle/compute.ML	\
     1.9    Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy		\
    1.10    Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy	\
    1.11    Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
    1.12 -  Matrix/cplex/FloatSparseMatrix.thy					\
    1.13    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
    1.14 -  Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
    1.15 +  Matrix/cplex/matrixlp.ML
    1.16  	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
    1.17  
    1.18  
     2.1 --- a/src/HOL/Matrix/Matrix.thy	Thu Jul 03 20:53:44 2008 +0200
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 04 07:39:01 2008 +0200
     2.3 @@ -4,17 +4,1445 @@
     2.4  *)
     2.5  
     2.6  theory Matrix
     2.7 -imports MatrixGeneral
     2.8 +imports Main
     2.9  begin
    2.10  
    2.11 +types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"
    2.12 +
    2.13 +definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
    2.14 +  "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
    2.15 +
    2.16 +typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    2.17 +proof -
    2.18 +  have "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    2.19 +    by (simp add: nonzero_positions_def)
    2.20 +  then show ?thesis by auto
    2.21 +qed
    2.22 +
    2.23 +declare Rep_matrix_inverse[simp]
    2.24 +
    2.25 +lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
    2.26 +apply (rule Abs_matrix_induct)
    2.27 +by (simp add: Abs_matrix_inverse matrix_def)
    2.28 +
    2.29 +constdefs
    2.30 +  nrows :: "('a::zero) matrix \<Rightarrow> nat"
    2.31 +  "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
    2.32 +  ncols :: "('a::zero) matrix \<Rightarrow> nat"
    2.33 +  "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
    2.34 +
    2.35 +lemma nrows:
    2.36 +  assumes hyp: "nrows A \<le> m"
    2.37 +  shows "(Rep_matrix A m n) = 0" (is ?concl)
    2.38 +proof cases
    2.39 +  assume "nonzero_positions(Rep_matrix A) = {}"
    2.40 +  then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
    2.41 +next
    2.42 +  assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
    2.43 +  let ?S = "fst`(nonzero_positions(Rep_matrix A))"
    2.44 +  have c: "finite (?S)" by (simp add: finite_nonzero_positions)
    2.45 +  from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
    2.46 +  have "m \<notin> ?S"
    2.47 +    proof -
    2.48 +      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])
    2.49 +      moreover from d have "~(m <= Max ?S)" by (simp)
    2.50 +      ultimately show "m \<notin> ?S" by (auto)
    2.51 +    qed
    2.52 +  thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
    2.53 +qed
    2.54 +
    2.55 +constdefs
    2.56 +  transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
    2.57 +  "transpose_infmatrix A j i == A i j"
    2.58 +  transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"
    2.59 +  "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"
    2.60 +
    2.61 +declare transpose_infmatrix_def[simp]
    2.62 +
    2.63 +lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"
    2.64 +by ((rule ext)+, simp)
    2.65 +
    2.66 +lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
    2.67 +  apply (rule ext)+
    2.68 +  by (simp add: transpose_infmatrix_def)
    2.69 +
    2.70 +lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
    2.71 +apply (rule Abs_matrix_inverse)
    2.72 +apply (simp add: matrix_def nonzero_positions_def image_def)
    2.73 +proof -
    2.74 +  let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
    2.75 +  let ?swap = "% pos. (snd pos, fst pos)"
    2.76 +  let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
    2.77 +  have swap_image: "?swap`?A = ?B"
    2.78 +    apply (simp add: image_def)
    2.79 +    apply (rule set_ext)
    2.80 +    apply (simp)
    2.81 +    proof
    2.82 +      fix y
    2.83 +      assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
    2.84 +      thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    2.85 +        proof -
    2.86 +          from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
    2.87 +          then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
    2.88 +        qed
    2.89 +    next
    2.90 +      fix y
    2.91 +      assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    2.92 +      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
    2.93 +	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
    2.94 +    qed
    2.95 +  then have "finite (?swap`?A)"
    2.96 +    proof -
    2.97 +      have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
    2.98 +      then have "finite ?B" by (simp add: nonzero_positions_def)
    2.99 +      with swap_image show "finite (?swap`?A)" by (simp)
   2.100 +    qed
   2.101 +  moreover
   2.102 +  have "inj_on ?swap ?A" by (simp add: inj_on_def)
   2.103 +  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
   2.104 +qed
   2.105 +
   2.106 +lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
   2.107 +
   2.108 +lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
   2.109 +apply (auto)
   2.110 +apply (rule ext)+
   2.111 +apply (simp add: transpose_infmatrix)
   2.112 +apply (drule infmatrixforward)
   2.113 +apply (simp)
   2.114 +done
   2.115 +
   2.116 +lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
   2.117 +apply (simp add: transpose_matrix_def)
   2.118 +apply (subst Rep_matrix_inject[THEN sym])+
   2.119 +apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
   2.120 +done
   2.121 +
   2.122 +lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
   2.123 +by (simp add: transpose_matrix_def)
   2.124 +
   2.125 +lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
   2.126 +by (simp add: transpose_matrix_def)
   2.127 +
   2.128 +lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"
   2.129 +by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   2.130 +
   2.131 +lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"
   2.132 +by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   2.133 +
   2.134 +lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"
   2.135 +proof -
   2.136 +  assume "ncols A <= n"
   2.137 +  then have "nrows (transpose_matrix A) <= n" by (simp)
   2.138 +  then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)
   2.139 +  thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)
   2.140 +qed
   2.141 +
   2.142 +lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
   2.143 +apply (auto)
   2.144 +apply (simp add: ncols)
   2.145 +proof (simp add: ncols_def, auto)
   2.146 +  let ?P = "nonzero_positions (Rep_matrix A)"
   2.147 +  let ?p = "snd`?P"
   2.148 +  have a:"finite ?p" by (simp add: finite_nonzero_positions)
   2.149 +  let ?m = "Max ?p"
   2.150 +  assume "~(Suc (?m) <= n)"
   2.151 +  then have b:"n <= ?m" by (simp)
   2.152 +  fix a b
   2.153 +  assume "(a,b) \<in> ?P"
   2.154 +  then have "?p \<noteq> {}" by (auto)
   2.155 +  with a have "?m \<in>  ?p" by (simp)
   2.156 +  moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
   2.157 +  ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
   2.158 +  moreover assume ?st
   2.159 +  ultimately show "False" using b by (simp)
   2.160 +qed
   2.161 +
   2.162 +lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   2.163 +proof -
   2.164 +  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   2.165 +  show ?concl by (simp add: a ncols_le)
   2.166 +qed
   2.167 +
   2.168 +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)
   2.169 +apply (auto)
   2.170 +apply (subgoal_tac "ncols A <= m")
   2.171 +apply (simp)
   2.172 +apply (simp add: ncols_le)
   2.173 +apply (drule_tac x="ncols A" in spec)
   2.174 +by (simp add: ncols)
   2.175 +
   2.176 +lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
   2.177 +proof -
   2.178 +  have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)
   2.179 +  also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
   2.180 +  also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
   2.181 +  finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
   2.182 +qed
   2.183 +
   2.184 +lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   2.185 +proof -
   2.186 +  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   2.187 +  show ?concl by (simp add: a nrows_le)
   2.188 +qed
   2.189 +
   2.190 +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)
   2.191 +apply (auto)
   2.192 +apply (subgoal_tac "nrows A <= m")
   2.193 +apply (simp)
   2.194 +apply (simp add: nrows_le)
   2.195 +apply (drule_tac x="nrows A" in spec)
   2.196 +by (simp add: nrows)
   2.197 +
   2.198 +lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
   2.199 +apply (case_tac "nrows A <= m")
   2.200 +apply (simp_all add: nrows)
   2.201 +done
   2.202 +
   2.203 +lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
   2.204 +apply (case_tac "ncols A <= n")
   2.205 +apply (simp_all add: ncols)
   2.206 +done
   2.207 +
   2.208 +lemma finite_natarray1: "finite {x. x < (n::nat)}"
   2.209 +apply (induct n)
   2.210 +apply (simp)
   2.211 +proof -
   2.212 +  fix n
   2.213 +  have "{x. x < Suc n} = insert n {x. x < n}"  by (rule set_ext, simp, arith)
   2.214 +  moreover assume "finite {x. x < n}"
   2.215 +  ultimately show "finite {x. x < Suc n}" by (simp)
   2.216 +qed
   2.217 +
   2.218 +lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
   2.219 +  apply (induct m)
   2.220 +  apply (simp+)
   2.221 +  proof -
   2.222 +    fix m::nat
   2.223 +    let ?s0 = "{pos. fst pos < m & snd pos < n}"
   2.224 +    let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
   2.225 +    let ?sd = "{pos. fst pos = m & snd pos < n}"
   2.226 +    assume f0: "finite ?s0"
   2.227 +    have f1: "finite ?sd"
   2.228 +    proof -
   2.229 +      let ?f = "% x. (m, x)"
   2.230 +      have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
   2.231 +      moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
   2.232 +      ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
   2.233 +    qed
   2.234 +    have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith)
   2.235 +    from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
   2.236 +    with su show "finite ?s1" by (simp)
   2.237 +qed
   2.238 +
   2.239 +lemma RepAbs_matrix:
   2.240 +  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)
   2.241 +  shows "(Rep_matrix (Abs_matrix x)) = x"
   2.242 +apply (rule Abs_matrix_inverse)
   2.243 +apply (simp add: matrix_def nonzero_positions_def)
   2.244 +proof -
   2.245 +  from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
   2.246 +  from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
   2.247 +  let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
   2.248 +  let ?v = "{pos. fst pos < m & snd pos < n}"
   2.249 +  have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
   2.250 +  from a b have "(?u \<inter> (-?v)) = {}"
   2.251 +    apply (simp)
   2.252 +    apply (rule set_ext)
   2.253 +    apply (simp)
   2.254 +    apply auto
   2.255 +    by (rule c, auto)+
   2.256 +  then have d: "?u \<subseteq> ?v" by blast
   2.257 +  moreover have "finite ?v" by (simp add: finite_natarray2)
   2.258 +  ultimately show "finite ?u" by (rule finite_subset)
   2.259 +qed
   2.260 +
   2.261 +constdefs
   2.262 +  apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
   2.263 +  "apply_infmatrix f == % A. (% j i. f (A j i))"
   2.264 +  apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
   2.265 +  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
   2.266 +  combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
   2.267 +  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
   2.268 +  combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
   2.269 +  "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
   2.270 +
   2.271 +lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
   2.272 +by (simp add: apply_infmatrix_def)
   2.273 +
   2.274 +lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
   2.275 +by (simp add: combine_infmatrix_def)
   2.276 +
   2.277 +constdefs
   2.278 +commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
   2.279 +"commutative f == ! x y. f x y = f y x"
   2.280 +associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   2.281 +"associative f == ! x y z. f (f x y) z = f x (f y z)"
   2.282 +
   2.283 +text{*
   2.284 +To reason about associativity and commutativity of operations on matrices,
   2.285 +let's take a step back and look at the general situtation: Assume that we have
   2.286 +sets $A$ and $B$ with $B \subset A$ and an abstraction $u: A \rightarrow B$. This abstraction has to fulfill $u(b) = b$ for all $b \in B$, but is arbitrary otherwise.
   2.287 +Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.
   2.288 +It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$
   2.289 +*}
   2.290 +
   2.291 +lemma combine_infmatrix_commute:
   2.292 +  "commutative f \<Longrightarrow> commutative (combine_infmatrix f)"
   2.293 +by (simp add: commutative_def combine_infmatrix_def)
   2.294 +
   2.295 +lemma combine_matrix_commute:
   2.296 +"commutative f \<Longrightarrow> commutative (combine_matrix f)"
   2.297 +by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
   2.298 +
   2.299 +text{*
   2.300 +On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,
   2.301 +as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have
   2.302 +\[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
   2.303 +but on the other hand we have
   2.304 +\[ f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.\]
   2.305 +A way out of this problem is to assume that $f(A\times A)\subset A$ holds, and this is what we are going to do:
   2.306 +*}
   2.307 +
   2.308 +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)"
   2.309 +by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)
   2.310 +
   2.311 +lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
   2.312 +by (insert Rep_matrix [of A], simp add: matrix_def)
   2.313 +
   2.314 +lemma combine_infmatrix_closed [simp]:
   2.315 +  "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)"
   2.316 +apply (rule Abs_matrix_inverse)
   2.317 +apply (simp add: matrix_def)
   2.318 +apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])
   2.319 +by (simp_all)
   2.320 +
   2.321 +text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}
   2.322 +lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"
   2.323 +by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)
   2.324 +
   2.325 +lemma apply_infmatrix_closed [simp]:
   2.326 +  "f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"
   2.327 +apply (rule Abs_matrix_inverse)
   2.328 +apply (simp add: matrix_def)
   2.329 +apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])
   2.330 +by (simp_all)
   2.331 +
   2.332 +lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"
   2.333 +by (simp add: associative_def combine_infmatrix_def)
   2.334 +
   2.335 +lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
   2.336 +by (auto)
   2.337 +
   2.338 +lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"
   2.339 +apply (simp(no_asm) add: associative_def combine_matrix_def, auto)
   2.340 +apply (rule comb [of Abs_matrix Abs_matrix])
   2.341 +by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)
   2.342 +
   2.343 +lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"
   2.344 +by (simp add: apply_matrix_def)
   2.345 +
   2.346 +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)"
   2.347 +  by(simp add: combine_matrix_def)
   2.348 +
   2.349 +lemma combine_nrows_max: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
   2.350 +by (simp add: nrows_le)
   2.351 +
   2.352 +lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
   2.353 +by (simp add: ncols_le)
   2.354 +
   2.355 +lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
   2.356 +  by (simp add: nrows_le)
   2.357 +
   2.358 +lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
   2.359 +  by (simp add: ncols_le)
   2.360 +
   2.361 +constdefs
   2.362 +  zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
   2.363 +  "zero_r_neutral f == ! a. f a 0 = a"
   2.364 +  zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   2.365 +  "zero_l_neutral f == ! a. f 0 a = a"
   2.366 +  zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
   2.367 +  "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
   2.368 +
   2.369 +consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   2.370 +primrec
   2.371 +  "foldseq f s 0 = s 0"
   2.372 +  "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
   2.373 +
   2.374 +consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   2.375 +primrec
   2.376 +  "foldseq_transposed f s 0 = s 0"
   2.377 +  "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
   2.378 +
   2.379 +lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
   2.380 +proof -
   2.381 +  assume a:"associative f"
   2.382 +  then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   2.383 +  proof -
   2.384 +    fix n
   2.385 +    show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   2.386 +    proof (induct n)
   2.387 +      show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
   2.388 +    next
   2.389 +      fix n
   2.390 +      assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   2.391 +      have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
   2.392 +      show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
   2.393 +      proof (auto)
   2.394 +        fix N t
   2.395 +        assume Nsuc: "N <= Suc n"
   2.396 +        show "foldseq f t N = foldseq_transposed f t N"
   2.397 +        proof cases
   2.398 +          assume "N <= n"
   2.399 +          then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
   2.400 +        next
   2.401 +          assume "~(N <= n)"
   2.402 +          with Nsuc have Nsuceq: "N = Suc n" by simp
   2.403 +          have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
   2.404 +          have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
   2.405 +          show "foldseq f t N = foldseq_transposed f t N"
   2.406 +            apply (simp add: Nsuceq)
   2.407 +            apply (subst c)
   2.408 +            apply (simp)
   2.409 +            apply (case_tac "n = 0")
   2.410 +            apply (simp)
   2.411 +            apply (drule neqz)
   2.412 +            apply (erule exE)
   2.413 +            apply (simp)
   2.414 +            apply (subst assocf)
   2.415 +            proof -
   2.416 +              fix m
   2.417 +              assume "n = Suc m & Suc m <= n"
   2.418 +              then have mless: "Suc m <= n" by arith
   2.419 +              then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")
   2.420 +                apply (subst c)
   2.421 +                by simp+
   2.422 +              have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
   2.423 +              have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
   2.424 +                apply (subst c)
   2.425 +                by (simp add: mless)+
   2.426 +              have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
   2.427 +              from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
   2.428 +            qed
   2.429 +          qed
   2.430 +        qed
   2.431 +      qed
   2.432 +    qed
   2.433 +    show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
   2.434 +  qed
   2.435 +
   2.436 +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)"
   2.437 +proof -
   2.438 +  assume assoc: "associative f"
   2.439 +  assume comm: "commutative f"
   2.440 +  from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)
   2.441 +  from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)
   2.442 +  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)
   2.443 +  have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
   2.444 +    apply (induct_tac n)
   2.445 +    apply (simp+, auto)
   2.446 +    by (simp add: a b c)
   2.447 +  then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
   2.448 +qed
   2.449 +
   2.450 +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)"
   2.451 +oops
   2.452 +(* Model found
   2.453 +
   2.454 +Trying to find a model that refutes: \<lbrakk>associative f; associative g;
   2.455 + \<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;
   2.456 + \<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk>
   2.457 +\<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y)
   2.458 +Searching for a model of size 1, translating term... invoking SAT solver... no model found.
   2.459 +Searching for a model of size 2, translating term... invoking SAT solver... no model found.
   2.460 +Searching for a model of size 3, translating term... invoking SAT solver...
   2.461 +Model found:
   2.462 +Size of types: 'a: 3
   2.463 +x: a1
   2.464 +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))
   2.465 +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))
   2.466 +*)
   2.467 +
   2.468 +lemma foldseq_zero:
   2.469 +assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"
   2.470 +shows "foldseq f s n = 0"
   2.471 +proof -
   2.472 +  have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
   2.473 +    apply (induct_tac n)
   2.474 +    apply (simp)
   2.475 +    by (simp add: fz)
   2.476 +  then show "foldseq f s n = 0" by (simp add: sz)
   2.477 +qed
   2.478 +
   2.479 +lemma foldseq_significant_positions:
   2.480 +  assumes p: "! i. i <= N \<longrightarrow> S i = T i"
   2.481 +  shows "foldseq f S N = foldseq f T N" (is ?concl)
   2.482 +proof -
   2.483 +  have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
   2.484 +    apply (induct_tac m)
   2.485 +    apply (simp)
   2.486 +    apply (simp)
   2.487 +    apply (auto)
   2.488 +    proof -
   2.489 +      fix n
   2.490 +      fix s::"nat\<Rightarrow>'a"
   2.491 +      fix t::"nat\<Rightarrow>'a"
   2.492 +      assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
   2.493 +      assume b: "\<forall>i\<le>Suc n. s i = t i"
   2.494 +      have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast
   2.495 +      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)
   2.496 +      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)
   2.497 +    qed
   2.498 +  with p show ?concl by simp
   2.499 +qed
   2.500 +
   2.501 +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")
   2.502 +proof -
   2.503 +  have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
   2.504 +  have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
   2.505 +  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"
   2.506 +    apply (induct_tac n)
   2.507 +    apply (simp)
   2.508 +    apply (simp)
   2.509 +    apply (auto)
   2.510 +    apply (case_tac "m = Suc na")
   2.511 +    apply (simp)
   2.512 +    apply (rule a)
   2.513 +    apply (rule foldseq_significant_positions)
   2.514 +    apply (auto)
   2.515 +    apply (drule suc, simp+)
   2.516 +    proof -
   2.517 +      fix na m s
   2.518 +      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"
   2.519 +      assume subb:"m <= na"
   2.520 +      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
   2.521 +      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 =
   2.522 +        foldseq f (% k. s(Suc k)) na"
   2.523 +        by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)
   2.524 +      from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith
   2.525 +      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) =
   2.526 +        foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
   2.527 +        apply (simp add: subd)
   2.528 +        apply (case_tac "m=0")
   2.529 +        apply (simp)
   2.530 +        apply (drule sube)
   2.531 +        apply (auto)
   2.532 +        apply (rule a)
   2.533 +        by (simp add: subc if_def)
   2.534 +    qed
   2.535 +  then show "?p \<Longrightarrow> ?concl" by simp
   2.536 +qed
   2.537 +
   2.538 +lemma foldseq_zerotail:
   2.539 +  assumes
   2.540 +  fz: "f 0 0 = 0"
   2.541 +  and sz: "! i.  n <= i \<longrightarrow> s i = 0"
   2.542 +  and nm: "n <= m"
   2.543 +  shows
   2.544 +  "foldseq f s n = foldseq f s m"
   2.545 +proof -
   2.546 +  show "foldseq f s n = foldseq f s m"
   2.547 +    apply (simp add: foldseq_tail[OF nm, of f s])
   2.548 +    apply (rule foldseq_significant_positions)
   2.549 +    apply (auto)
   2.550 +    apply (subst foldseq_zero)
   2.551 +    by (simp add: fz sz)+
   2.552 +qed
   2.553 +
   2.554 +lemma foldseq_zerotail2:
   2.555 +  assumes "! x. f x 0 = x"
   2.556 +  and "! i. n < i \<longrightarrow> s i = 0"
   2.557 +  and nm: "n <= m"
   2.558 +  shows
   2.559 +  "foldseq f s n = foldseq f s m" (is ?concl)
   2.560 +proof -
   2.561 +  have "f 0 0 = 0" by (simp add: prems)
   2.562 +  have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
   2.563 +  have c: "0 <= m" by simp
   2.564 +  have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   2.565 +  show ?concl
   2.566 +    apply (subst foldseq_tail[OF nm])
   2.567 +    apply (rule foldseq_significant_positions)
   2.568 +    apply (auto)
   2.569 +    apply (case_tac "m=n")
   2.570 +    apply (simp+)
   2.571 +    apply (drule b[OF nm])
   2.572 +    apply (auto)
   2.573 +    apply (case_tac "k=0")
   2.574 +    apply (simp add: prems)
   2.575 +    apply (drule d)
   2.576 +    apply (auto)
   2.577 +    by (simp add: prems foldseq_zero)
   2.578 +qed
   2.579 +
   2.580 +lemma foldseq_zerostart:
   2.581 +  "! 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))"
   2.582 +proof -
   2.583 +  assume f00x: "! x. f 0 (f 0 x) = f 0 x"
   2.584 +  have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
   2.585 +    apply (induct n)
   2.586 +    apply (simp)
   2.587 +    apply (rule allI, rule impI)
   2.588 +    proof -
   2.589 +      fix n
   2.590 +      fix s
   2.591 +      have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp
   2.592 +      assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"
   2.593 +      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
   2.594 +      assume d: "! i. i <= Suc n \<longrightarrow> s i = 0"
   2.595 +      show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"
   2.596 +        apply (subst a)
   2.597 +        apply (subst c)
   2.598 +        by (simp add: d f00x)+
   2.599 +    qed
   2.600 +  then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
   2.601 +qed
   2.602 +
   2.603 +lemma foldseq_zerostart2:
   2.604 +  "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
   2.605 +proof -
   2.606 +  assume a:"! i. i<n \<longrightarrow> s i = 0"
   2.607 +  assume x:"! x. f 0 x = x"
   2.608 +  from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast
   2.609 +  have b: "!! i l. i < Suc l = (i <= l)" by arith
   2.610 +  have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   2.611 +  show "foldseq f s n = s n"
   2.612 +  apply (case_tac "n=0")
   2.613 +  apply (simp)
   2.614 +  apply (insert a)
   2.615 +  apply (drule d)
   2.616 +  apply (auto)
   2.617 +  apply (simp add: b)
   2.618 +  apply (insert f00x)
   2.619 +  apply (drule foldseq_zerostart)
   2.620 +  by (simp add: x)+
   2.621 +qed
   2.622 +
   2.623 +lemma foldseq_almostzero:
   2.624 +  assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
   2.625 +  shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
   2.626 +proof -
   2.627 +  from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
   2.628 +  from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
   2.629 +  show ?concl
   2.630 +    apply auto
   2.631 +    apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
   2.632 +    apply simp
   2.633 +    apply (subst foldseq_zerostart2)
   2.634 +    apply (simp add: f0x a)+
   2.635 +    apply (subst foldseq_zero)
   2.636 +    by (simp add: s0 f0x)+
   2.637 +qed
   2.638 +
   2.639 +lemma foldseq_distr_unary:
   2.640 +  assumes "!! a b. g (f a b) = f (g a) (g b)"
   2.641 +  shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
   2.642 +proof -
   2.643 +  have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
   2.644 +    apply (induct_tac n)
   2.645 +    apply (simp)
   2.646 +    apply (simp)
   2.647 +    apply (auto)
   2.648 +    apply (drule_tac x="% k. s (Suc k)" in spec)
   2.649 +    by (simp add: prems)
   2.650 +  then show ?concl by simp
   2.651 +qed
   2.652 +
   2.653 +constdefs
   2.654 +  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"
   2.655 +  "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)"
   2.656 +  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"
   2.657 +  "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
   2.658 +
   2.659 +lemma mult_matrix_n:
   2.660 +  assumes prems: "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
   2.661 +  shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
   2.662 +proof -
   2.663 +  show ?concl using prems
   2.664 +    apply (simp add: mult_matrix_def mult_matrix_n_def)
   2.665 +    apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   2.666 +    by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
   2.667 +qed
   2.668 +
   2.669 +lemma mult_matrix_nm:
   2.670 +  assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
   2.671 +  shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
   2.672 +proof -
   2.673 +  from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
   2.674 +  also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
   2.675 +  finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
   2.676 +qed
   2.677 +
   2.678 +constdefs
   2.679 +  r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   2.680 +  "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
   2.681 +  l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   2.682 +  "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
   2.683 +  distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   2.684 +  "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
   2.685 +
   2.686 +lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
   2.687 +lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
   2.688 +
   2.689 +lemma r_distributive_matrix:
   2.690 + assumes prems:
   2.691 +  "r_distributive fmul fadd"
   2.692 +  "associative fadd"
   2.693 +  "commutative fadd"
   2.694 +  "fadd 0 0 = 0"
   2.695 +  "! a. fmul a 0 = 0"
   2.696 +  "! a. fmul 0 a = 0"
   2.697 + shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   2.698 +proof -
   2.699 +  from prems show ?concl
   2.700 +    apply (simp add: r_distributive_def mult_matrix_def, auto)
   2.701 +    proof -
   2.702 +      fix a::"'a matrix"
   2.703 +      fix u::"'b matrix"
   2.704 +      fix v::"'b matrix"
   2.705 +      let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
   2.706 +      from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
   2.707 +        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)"
   2.708 +        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   2.709 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.710 +        apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])
   2.711 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.712 +        apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])
   2.713 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.714 +        apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
   2.715 +        apply (simp add: combine_matrix_def combine_infmatrix_def)
   2.716 +        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   2.717 +        apply (simplesubst RepAbs_matrix)
   2.718 +        apply (simp, auto)
   2.719 +        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   2.720 +        apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
   2.721 +        apply (subst RepAbs_matrix)
   2.722 +        apply (simp, auto)
   2.723 +        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   2.724 +        apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
   2.725 +        done
   2.726 +    qed
   2.727 +qed
   2.728 +
   2.729 +lemma l_distributive_matrix:
   2.730 + assumes prems:
   2.731 +  "l_distributive fmul fadd"
   2.732 +  "associative fadd"
   2.733 +  "commutative fadd"
   2.734 +  "fadd 0 0 = 0"
   2.735 +  "! a. fmul a 0 = 0"
   2.736 +  "! a. fmul 0 a = 0"
   2.737 + shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   2.738 +proof -
   2.739 +  from prems show ?concl
   2.740 +    apply (simp add: l_distributive_def mult_matrix_def, auto)
   2.741 +    proof -
   2.742 +      fix a::"'b matrix"
   2.743 +      fix u::"'a matrix"
   2.744 +      fix v::"'a matrix"
   2.745 +      let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
   2.746 +      from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
   2.747 +               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)"
   2.748 +        apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
   2.749 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.750 +        apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])
   2.751 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.752 +        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   2.753 +        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   2.754 +        apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
   2.755 +        apply (simp add: combine_matrix_def combine_infmatrix_def)
   2.756 +        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   2.757 +        apply (simplesubst RepAbs_matrix)
   2.758 +        apply (simp, auto)
   2.759 +        apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
   2.760 +        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   2.761 +        apply (subst RepAbs_matrix)
   2.762 +        apply (simp, auto)
   2.763 +        apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
   2.764 +        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   2.765 +        done
   2.766 +    qed
   2.767 +qed
   2.768 +
   2.769 +instantiation matrix :: (zero) zero
   2.770 +begin
   2.771 +
   2.772 +definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
   2.773 +
   2.774 +instance ..
   2.775 +
   2.776 +end
   2.777 +
   2.778 +lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
   2.779 +  apply (simp add: zero_matrix_def)
   2.780 +  apply (subst RepAbs_matrix)
   2.781 +  by (auto)
   2.782 +
   2.783 +lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
   2.784 +proof -
   2.785 +  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   2.786 +  show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
   2.787 +qed
   2.788 +
   2.789 +lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
   2.790 +proof -
   2.791 +  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   2.792 +  show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
   2.793 +qed
   2.794 +
   2.795 +lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
   2.796 +  by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
   2.797 +
   2.798 +lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
   2.799 +  by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
   2.800 +
   2.801 +lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
   2.802 +  apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
   2.803 +  apply (auto)
   2.804 +  by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
   2.805 +
   2.806 +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"
   2.807 +  apply (simp add: mult_matrix_n_def)
   2.808 +  apply (subst foldseq_zero)
   2.809 +  by (simp_all add: zero_matrix_def)
   2.810 +
   2.811 +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"
   2.812 +  apply (simp add: mult_matrix_n_def)
   2.813 +  apply (subst foldseq_zero)
   2.814 +  by (simp_all add: zero_matrix_def)
   2.815 +
   2.816 +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"
   2.817 +by (simp add: mult_matrix_def)
   2.818 +
   2.819 +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"
   2.820 +by (simp add: mult_matrix_def)
   2.821 +
   2.822 +lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"
   2.823 +  apply (simp add: apply_matrix_def apply_infmatrix_def)
   2.824 +  by (simp add: zero_matrix_def)
   2.825 +
   2.826 +lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"
   2.827 +  apply (simp add: combine_matrix_def combine_infmatrix_def)
   2.828 +  by (simp add: zero_matrix_def)
   2.829 +
   2.830 +lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
   2.831 +apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
   2.832 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   2.833 +apply (simp add: RepAbs_matrix)
   2.834 +done
   2.835 +
   2.836 +lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
   2.837 +  apply (simp add: apply_matrix_def apply_infmatrix_def)
   2.838 +  by (simp add: zero_matrix_def)
   2.839 +
   2.840 +constdefs
   2.841 +  singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"
   2.842 +  "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
   2.843 +  move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"
   2.844 +  "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)))"
   2.845 +  take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   2.846 +  "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
   2.847 +  take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   2.848 +  "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
   2.849 +
   2.850 +constdefs
   2.851 +  column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   2.852 +  "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
   2.853 +  row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   2.854 +  "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
   2.855 +
   2.856 +lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
   2.857 +apply (simp add: singleton_matrix_def)
   2.858 +apply (auto)
   2.859 +apply (subst RepAbs_matrix)
   2.860 +apply (rule exI[of _ "Suc m"], simp)
   2.861 +apply (rule exI[of _ "Suc n"], simp+)
   2.862 +by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
   2.863 +
   2.864 +lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
   2.865 +apply (subst Rep_matrix_inject[symmetric])
   2.866 +apply (rule ext)+
   2.867 +apply (simp)
   2.868 +done
   2.869 +
   2.870 +lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
   2.871 +  by (simp add: singleton_matrix_def zero_matrix_def)
   2.872 +
   2.873 +lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
   2.874 +proof-
   2.875 +have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   2.876 +from th show ?thesis 
   2.877 +apply (auto)
   2.878 +apply (rule le_anti_sym)
   2.879 +apply (subst nrows_le)
   2.880 +apply (simp add: singleton_matrix_def, auto)
   2.881 +apply (subst RepAbs_matrix)
   2.882 +apply auto
   2.883 +apply (simp add: Suc_le_eq)
   2.884 +apply (rule not_leE)
   2.885 +apply (subst nrows_le)
   2.886 +by simp
   2.887 +qed
   2.888 +
   2.889 +lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
   2.890 +proof-
   2.891 +have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   2.892 +from th show ?thesis 
   2.893 +apply (auto)
   2.894 +apply (rule le_anti_sym)
   2.895 +apply (subst ncols_le)
   2.896 +apply (simp add: singleton_matrix_def, auto)
   2.897 +apply (subst RepAbs_matrix)
   2.898 +apply auto
   2.899 +apply (simp add: Suc_le_eq)
   2.900 +apply (rule not_leE)
   2.901 +apply (subst ncols_le)
   2.902 +by simp
   2.903 +qed
   2.904 +
   2.905 +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)"
   2.906 +apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
   2.907 +apply (subst RepAbs_matrix)
   2.908 +apply (rule exI[of _ "Suc j"], simp)
   2.909 +apply (rule exI[of _ "Suc i"], simp)
   2.910 +apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   2.911 +apply (subst RepAbs_matrix)
   2.912 +apply (rule exI[of _ "Suc j"], simp)
   2.913 +apply (rule exI[of _ "Suc i"], simp)
   2.914 +by simp
   2.915 +
   2.916 +lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
   2.917 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   2.918 +apply (simp)
   2.919 +done
   2.920 +
   2.921 +lemma Rep_move_matrix[simp]:
   2.922 +  "Rep_matrix (move_matrix A y x) j i =
   2.923 +  (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
   2.924 +apply (simp add: move_matrix_def)
   2.925 +apply (auto)
   2.926 +by (subst RepAbs_matrix,
   2.927 +  rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
   2.928 +  rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
   2.929 +
   2.930 +lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
   2.931 +by (simp add: move_matrix_def)
   2.932 +
   2.933 +lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
   2.934 +apply (subst Rep_matrix_inject[symmetric])
   2.935 +apply (rule ext)+
   2.936 +apply (simp)
   2.937 +done
   2.938 +
   2.939 +lemma transpose_move_matrix[simp]:
   2.940 +  "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
   2.941 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   2.942 +apply (simp)
   2.943 +done
   2.944 +
   2.945 +lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
   2.946 +  (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
   2.947 +  apply (subst Rep_matrix_inject[symmetric])
   2.948 +  apply (rule ext)+
   2.949 +  apply (case_tac "j + int u < 0")
   2.950 +  apply (simp, arith)
   2.951 +  apply (case_tac "i + int v < 0")
   2.952 +  apply (simp add: neg_def, arith)
   2.953 +  apply (simp add: neg_def)
   2.954 +  apply arith
   2.955 +  done
   2.956 +
   2.957 +lemma Rep_take_columns[simp]:
   2.958 +  "Rep_matrix (take_columns A c) j i =
   2.959 +  (if i < c then (Rep_matrix A j i) else 0)"
   2.960 +apply (simp add: take_columns_def)
   2.961 +apply (simplesubst RepAbs_matrix)
   2.962 +apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   2.963 +apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   2.964 +done
   2.965 +
   2.966 +lemma Rep_take_rows[simp]:
   2.967 +  "Rep_matrix (take_rows A r) j i =
   2.968 +  (if j < r then (Rep_matrix A j i) else 0)"
   2.969 +apply (simp add: take_rows_def)
   2.970 +apply (simplesubst RepAbs_matrix)
   2.971 +apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   2.972 +apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   2.973 +done
   2.974 +
   2.975 +lemma Rep_column_of_matrix[simp]:
   2.976 +  "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"
   2.977 +  by (simp add: column_of_matrix_def)
   2.978 +
   2.979 +lemma Rep_row_of_matrix[simp]:
   2.980 +  "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   2.981 +  by (simp add: row_of_matrix_def)
   2.982 +
   2.983 +lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
   2.984 +apply (subst Rep_matrix_inject[THEN sym])
   2.985 +apply (rule ext)+
   2.986 +by (simp add: ncols)
   2.987 +
   2.988 +lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
   2.989 +apply (subst Rep_matrix_inject[THEN sym])
   2.990 +apply (rule ext)+
   2.991 +by (simp add: nrows)
   2.992 +
   2.993 +lemma mult_matrix_singleton_right[simp]:
   2.994 +  assumes prems:
   2.995 +  "! x. fmul x 0 = 0"
   2.996 +  "! x. fmul 0 x = 0"
   2.997 +  "! x. fadd 0 x = x"
   2.998 +  "! x. fadd x 0 = x"
   2.999 +  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))"
  2.1000 +  apply (simp add: mult_matrix_def)
  2.1001 +  apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
  2.1002 +  apply (auto)
  2.1003 +  apply (simp add: prems)+
  2.1004 +  apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
  2.1005 +  apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
  2.1006 +  apply (subst foldseq_almostzero[of _ j])
  2.1007 +  apply (simp add: prems)+
  2.1008 +  apply (auto)
  2.1009 +  proof -
  2.1010 +    fix k
  2.1011 +    fix l
  2.1012 +    assume a:"~neg(int l - int i)"
  2.1013 +    assume b:"nat (int l - int i) = 0"
  2.1014 +    from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
  2.1015 +    assume c: "i \<noteq> l"
  2.1016 +    from c a show "fmul (Rep_matrix A k j) e = 0" by blast
  2.1017 +  qed
  2.1018 +
  2.1019 +lemma mult_matrix_ext:
  2.1020 +  assumes
  2.1021 +  eprem:
  2.1022 +  "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)"
  2.1023 +  and fprems:
  2.1024 +  "! a. fmul 0 a = 0"
  2.1025 +  "! a. fmul a 0 = 0"
  2.1026 +  "! a. fadd a 0 = a"
  2.1027 +  "! a. fadd 0 a = a"
  2.1028 +  and contraprems:
  2.1029 +  "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
  2.1030 +  shows
  2.1031 +  "A = B"
  2.1032 +proof(rule contrapos_np[of "False"], simp)
  2.1033 +  assume a: "A \<noteq> B"
  2.1034 +  have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
  2.1035 +  have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
  2.1036 +    apply (rule contrapos_np[of "False"], simp+)
  2.1037 +    apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)
  2.1038 +    by (simp add: Rep_matrix_inject a)
  2.1039 +  then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
  2.1040 +  from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast
  2.1041 +  let ?S = "singleton_matrix I 0 e"
  2.1042 +  let ?comp = "mult_matrix fmul fadd"
  2.1043 +  have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
  2.1044 +  have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
  2.1045 +  have "~(?comp A ?S = ?comp B ?S)"
  2.1046 +    apply (rule notI)
  2.1047 +    apply (simp add: fprems eprops)
  2.1048 +    apply (simp add: Rep_matrix_inject[THEN sym])
  2.1049 +    apply (drule d[of _ _ "J"], drule d[of _ _ "0"])
  2.1050 +    by (simp add: e c eprops)
  2.1051 +  with contraprems show "False" by simp
  2.1052 +qed
  2.1053 +
  2.1054 +constdefs
  2.1055 +  foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  2.1056 +  "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
  2.1057 +  foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  2.1058 +  "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
  2.1059 +
  2.1060 +lemma foldmatrix_transpose:
  2.1061 +  assumes
  2.1062 +  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  2.1063 +  shows
  2.1064 +  "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
  2.1065 +proof -
  2.1066 +  have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
  2.1067 +  have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
  2.1068 +    apply (induct n)
  2.1069 +    apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
  2.1070 +    apply (auto)
  2.1071 +    by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
  2.1072 +  show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
  2.1073 +    apply (simp add: foldmatrix_def foldmatrix_transposed_def)
  2.1074 +    apply (induct m, simp)
  2.1075 +    apply (simp)
  2.1076 +    apply (insert tworows)
  2.1077 +    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)
  2.1078 +    by (simp add: foldmatrix_def foldmatrix_transposed_def)
  2.1079 +qed
  2.1080 +
  2.1081 +lemma foldseq_foldseq:
  2.1082 +assumes
  2.1083 +  "associative f"
  2.1084 +  "associative g"
  2.1085 +  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  2.1086 +shows
  2.1087 +  "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
  2.1088 +  apply (insert foldmatrix_transpose[of g f A m n])
  2.1089 +  by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
  2.1090 +
  2.1091 +lemma mult_n_nrows:
  2.1092 +assumes
  2.1093 +"! a. fmul 0 a = 0"
  2.1094 +"! a. fmul a 0 = 0"
  2.1095 +"fadd 0 0 = 0"
  2.1096 +shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
  2.1097 +apply (subst nrows_le)
  2.1098 +apply (simp add: mult_matrix_n_def)
  2.1099 +apply (subst RepAbs_matrix)
  2.1100 +apply (rule_tac x="nrows A" in exI)
  2.1101 +apply (simp add: nrows prems foldseq_zero)
  2.1102 +apply (rule_tac x="ncols B" in exI)
  2.1103 +apply (simp add: ncols prems foldseq_zero)
  2.1104 +by (simp add: nrows prems foldseq_zero)
  2.1105 +
  2.1106 +lemma mult_n_ncols:
  2.1107 +assumes
  2.1108 +"! a. fmul 0 a = 0"
  2.1109 +"! a. fmul a 0 = 0"
  2.1110 +"fadd 0 0 = 0"
  2.1111 +shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
  2.1112 +apply (subst ncols_le)
  2.1113 +apply (simp add: mult_matrix_n_def)
  2.1114 +apply (subst RepAbs_matrix)
  2.1115 +apply (rule_tac x="nrows A" in exI)
  2.1116 +apply (simp add: nrows prems foldseq_zero)
  2.1117 +apply (rule_tac x="ncols B" in exI)
  2.1118 +apply (simp add: ncols prems foldseq_zero)
  2.1119 +by (simp add: ncols prems foldseq_zero)
  2.1120 +
  2.1121 +lemma mult_nrows:
  2.1122 +assumes
  2.1123 +"! a. fmul 0 a = 0"
  2.1124 +"! a. fmul a 0 = 0"
  2.1125 +"fadd 0 0 = 0"
  2.1126 +shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
  2.1127 +by (simp add: mult_matrix_def mult_n_nrows prems)
  2.1128 +
  2.1129 +lemma mult_ncols:
  2.1130 +assumes
  2.1131 +"! a. fmul 0 a = 0"
  2.1132 +"! a. fmul a 0 = 0"
  2.1133 +"fadd 0 0 = 0"
  2.1134 +shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
  2.1135 +by (simp add: mult_matrix_def mult_n_ncols prems)
  2.1136 +
  2.1137 +lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
  2.1138 +  apply (auto simp add: nrows_le)
  2.1139 +  apply (rule nrows)
  2.1140 +  apply (arith)
  2.1141 +  done
  2.1142 +
  2.1143 +lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
  2.1144 +  apply (auto simp add: ncols_le)
  2.1145 +  apply (rule ncols)
  2.1146 +  apply (arith)
  2.1147 +  done
  2.1148 +
  2.1149 +lemma mult_matrix_assoc:
  2.1150 +  assumes prems:
  2.1151 +  "! a. fmul1 0 a = 0"
  2.1152 +  "! a. fmul1 a 0 = 0"
  2.1153 +  "! a. fmul2 0 a = 0"
  2.1154 +  "! a. fmul2 a 0 = 0"
  2.1155 +  "fadd1 0 0 = 0"
  2.1156 +  "fadd2 0 0 = 0"
  2.1157 +  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  2.1158 +  "associative fadd1"
  2.1159 +  "associative fadd2"
  2.1160 +  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  2.1161 +  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  2.1162 +  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  2.1163 +  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)
  2.1164 +proof -
  2.1165 +  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
  2.1166 +  have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (% k. fmul2 (s k) x) n"
  2.1167 +    by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
  2.1168 +  have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
  2.1169 +      by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
  2.1170 +  let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
  2.1171 +  show ?concl
  2.1172 +    apply (simp add: Rep_matrix_inject[THEN sym])
  2.1173 +    apply (rule ext)+
  2.1174 +    apply (simp add: mult_matrix_def)
  2.1175 +    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)"])
  2.1176 +    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  2.1177 +    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)+
  2.1178 +    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  2.1179 +    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  2.1180 +    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  2.1181 +    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  2.1182 +    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  2.1183 +    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  2.1184 +    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  2.1185 +    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  2.1186 +    apply (simp add: mult_matrix_n_def)
  2.1187 +    apply (rule comb_left)
  2.1188 +    apply ((rule ext)+, simp)
  2.1189 +    apply (simplesubst RepAbs_matrix)
  2.1190 +    apply (rule exI[of _ "nrows B"])
  2.1191 +    apply (simp add: nrows prems foldseq_zero)
  2.1192 +    apply (rule exI[of _ "ncols C"])
  2.1193 +    apply (simp add: prems ncols foldseq_zero)
  2.1194 +    apply (subst RepAbs_matrix)
  2.1195 +    apply (rule exI[of _ "nrows A"])
  2.1196 +    apply (simp add: nrows prems foldseq_zero)
  2.1197 +    apply (rule exI[of _ "ncols B"])
  2.1198 +    apply (simp add: prems ncols foldseq_zero)
  2.1199 +    apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
  2.1200 +    apply (subst foldseq_foldseq)
  2.1201 +    apply (simp add: prems)+
  2.1202 +    by (simp add: transpose_infmatrix)
  2.1203 +qed
  2.1204 +
  2.1205 +lemma
  2.1206 +  assumes prems:
  2.1207 +  "! a. fmul1 0 a = 0"
  2.1208 +  "! a. fmul1 a 0 = 0"
  2.1209 +  "! a. fmul2 0 a = 0"
  2.1210 +  "! a. fmul2 a 0 = 0"
  2.1211 +  "fadd1 0 0 = 0"
  2.1212 +  "fadd2 0 0 = 0"
  2.1213 +  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  2.1214 +  "associative fadd1"
  2.1215 +  "associative fadd2"
  2.1216 +  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  2.1217 +  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  2.1218 +  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  2.1219 +  shows
  2.1220 +  "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
  2.1221 +apply (rule ext)+
  2.1222 +apply (simp add: comp_def )
  2.1223 +by (simp add: mult_matrix_assoc prems)
  2.1224 +
  2.1225 +lemma mult_matrix_assoc_simple:
  2.1226 +  assumes prems:
  2.1227 +  "! a. fmul 0 a = 0"
  2.1228 +  "! a. fmul a 0 = 0"
  2.1229 +  "fadd 0 0 = 0"
  2.1230 +  "associative fadd"
  2.1231 +  "commutative fadd"
  2.1232 +  "associative fmul"
  2.1233 +  "distributive fmul fadd"
  2.1234 +  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)
  2.1235 +proof -
  2.1236 +  have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
  2.1237 +    by (simp! add: associative_def commutative_def)
  2.1238 +  then show ?concl
  2.1239 +    apply (subst mult_matrix_assoc)
  2.1240 +    apply (simp_all!)
  2.1241 +    by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
  2.1242 +qed
  2.1243 +
  2.1244 +lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
  2.1245 +apply (simp add: Rep_matrix_inject[THEN sym])
  2.1246 +apply (rule ext)+
  2.1247 +by simp
  2.1248 +
  2.1249 +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)"
  2.1250 +apply (simp add: Rep_matrix_inject[THEN sym])
  2.1251 +apply (rule ext)+
  2.1252 +by simp
  2.1253 +
  2.1254 +lemma Rep_mult_matrix:
  2.1255 +  assumes
  2.1256 +  "! a. fmul 0 a = 0"
  2.1257 +  "! a. fmul a 0 = 0"
  2.1258 +  "fadd 0 0 = 0"
  2.1259 +  shows
  2.1260 +  "Rep_matrix(mult_matrix fmul fadd A B) j i =
  2.1261 +  foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
  2.1262 +apply (simp add: mult_matrix_def mult_matrix_n_def)
  2.1263 +apply (subst RepAbs_matrix)
  2.1264 +apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
  2.1265 +apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
  2.1266 +by simp
  2.1267 +
  2.1268 +lemma transpose_mult_matrix:
  2.1269 +  assumes
  2.1270 +  "! a. fmul 0 a = 0"
  2.1271 +  "! a. fmul a 0 = 0"
  2.1272 +  "fadd 0 0 = 0"
  2.1273 +  "! x y. fmul y x = fmul x y"
  2.1274 +  shows
  2.1275 +  "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
  2.1276 +  apply (simp add: Rep_matrix_inject[THEN sym])
  2.1277 +  apply (rule ext)+
  2.1278 +  by (simp! add: Rep_mult_matrix max_ac)
  2.1279 +
  2.1280 +lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
  2.1281 +apply (simp add:  Rep_matrix_inject[THEN sym])
  2.1282 +apply (rule ext)+
  2.1283 +by simp
  2.1284 +
  2.1285 +lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
  2.1286 +apply (simp add: Rep_matrix_inject[THEN sym])
  2.1287 +apply (rule ext)+
  2.1288 +by simp
  2.1289 +
  2.1290 +instantiation matrix :: ("{ord, zero}") ord
  2.1291 +begin
  2.1292 +
  2.1293 +definition
  2.1294 +  le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
  2.1295 +
  2.1296 +definition
  2.1297 +  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
  2.1298 +
  2.1299 +instance ..
  2.1300 +
  2.1301 +end
  2.1302 +
  2.1303 +instance matrix :: ("{order, zero}") order
  2.1304 +apply intro_classes
  2.1305 +apply (simp_all add: le_matrix_def less_def)
  2.1306 +apply (auto)
  2.1307 +apply (drule_tac x=j in spec, drule_tac x=j in spec)
  2.1308 +apply (drule_tac x=i in spec, drule_tac x=i in spec)
  2.1309 +apply (simp)
  2.1310 +apply (simp add: Rep_matrix_inject[THEN sym])
  2.1311 +apply (rule ext)+
  2.1312 +apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
  2.1313 +apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
  2.1314 +by simp
  2.1315 +
  2.1316 +lemma le_apply_matrix:
  2.1317 +  assumes
  2.1318 +  "f 0 = 0"
  2.1319 +  "! x y. x <= y \<longrightarrow> f x <= f y"
  2.1320 +  "(a::('a::{ord, zero}) matrix) <= b"
  2.1321 +  shows
  2.1322 +  "apply_matrix f a <= apply_matrix f b"
  2.1323 +  by (simp! add: le_matrix_def)
  2.1324 +
  2.1325 +lemma le_combine_matrix:
  2.1326 +  assumes
  2.1327 +  "f 0 0 = 0"
  2.1328 +  "! a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"
  2.1329 +  "A <= B"
  2.1330 +  "C <= D"
  2.1331 +  shows
  2.1332 +  "combine_matrix f A C <= combine_matrix f B D"
  2.1333 +by (simp! add: le_matrix_def)
  2.1334 +
  2.1335 +lemma le_left_combine_matrix:
  2.1336 +  assumes
  2.1337 +  "f 0 0 = 0"
  2.1338 +  "! a b c. a <= b \<longrightarrow> f c a <= f c b"
  2.1339 +  "A <= B"
  2.1340 +  shows
  2.1341 +  "combine_matrix f C A <= combine_matrix f C B"
  2.1342 +  by (simp! add: le_matrix_def)
  2.1343 +
  2.1344 +lemma le_right_combine_matrix:
  2.1345 +  assumes
  2.1346 +  "f 0 0 = 0"
  2.1347 +  "! a b c. a <= b \<longrightarrow> f a c <= f b c"
  2.1348 +  "A <= B"
  2.1349 +  shows
  2.1350 +  "combine_matrix f A C <= combine_matrix f B C"
  2.1351 +  by (simp! add: le_matrix_def)
  2.1352 +
  2.1353 +lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
  2.1354 +  by (simp add: le_matrix_def, auto)
  2.1355 +
  2.1356 +lemma le_foldseq:
  2.1357 +  assumes
  2.1358 +  "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
  2.1359 +  "! i. i <= n \<longrightarrow> s i <= t i"
  2.1360 +  shows
  2.1361 +  "foldseq f s n <= foldseq f t n"
  2.1362 +proof -
  2.1363 +  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!)
  2.1364 +  then show "foldseq f s n <= foldseq f t n" by (simp!)
  2.1365 +qed
  2.1366 +
  2.1367 +lemma le_left_mult:
  2.1368 +  assumes
  2.1369 +  "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  2.1370 +  "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
  2.1371 +  "! a. fmul 0 a = 0"
  2.1372 +  "! a. fmul a 0 = 0"
  2.1373 +  "fadd 0 0 = 0"
  2.1374 +  "0 <= C"
  2.1375 +  "A <= B"
  2.1376 +  shows
  2.1377 +  "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
  2.1378 +  apply (simp! add: le_matrix_def Rep_mult_matrix)
  2.1379 +  apply (auto)
  2.1380 +  apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
  2.1381 +  apply (rule le_foldseq)
  2.1382 +  by (auto)
  2.1383 +
  2.1384 +lemma le_right_mult:
  2.1385 +  assumes
  2.1386 +  "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  2.1387 +  "! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
  2.1388 +  "! a. fmul 0 a = 0"
  2.1389 +  "! a. fmul a 0 = 0"
  2.1390 +  "fadd 0 0 = 0"
  2.1391 +  "0 <= C"
  2.1392 +  "A <= B"
  2.1393 +  shows
  2.1394 +  "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
  2.1395 +  apply (simp! add: le_matrix_def Rep_mult_matrix)
  2.1396 +  apply (auto)
  2.1397 +  apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
  2.1398 +  apply (rule le_foldseq)
  2.1399 +  by (auto)
  2.1400 +
  2.1401 +lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
  2.1402 +lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
  2.1403 +
  2.1404 +lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"
  2.1405 +  by (auto simp add: le_matrix_def)
  2.1406 +
  2.1407 +lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"
  2.1408 +  apply (auto)
  2.1409 +  apply (simp add: le_matrix_def)
  2.1410 +  apply (drule_tac j=j and i=i in spec2)
  2.1411 +  apply (simp)
  2.1412 +  apply (simp add: le_matrix_def)
  2.1413 +  done
  2.1414 +
  2.1415 +lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
  2.1416 +  apply (auto)
  2.1417 +  apply (simp add: le_matrix_def)
  2.1418 +  apply (drule_tac j=j and i=i in spec2)
  2.1419 +  apply (simp)
  2.1420 +  apply (simp add: le_matrix_def)
  2.1421 +  done
  2.1422 +
  2.1423 +lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
  2.1424 +  apply (auto simp add: le_matrix_def neg_def)
  2.1425 +  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  2.1426 +  apply (auto)
  2.1427 +  done
  2.1428 +
  2.1429 +lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
  2.1430 +  apply (auto simp add: le_matrix_def neg_def)
  2.1431 +  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  2.1432 +  apply (auto)
  2.1433 +  done
  2.1434 +
  2.1435 +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))"
  2.1436 +  apply (auto simp add: le_matrix_def neg_def)
  2.1437 +  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  2.1438 +  apply (auto)
  2.1439 +  done  
  2.1440 +
  2.1441  instantiation matrix :: ("{zero, lattice}") lattice
  2.1442  begin
  2.1443  
  2.1444 -definition
  2.1445 -  "inf = combine_matrix inf"
  2.1446 +definition [code func del]: "inf = combine_matrix inf"
  2.1447  
  2.1448 -definition
  2.1449 -  "sup = combine_matrix sup"
  2.1450 +definition [code func del]: "sup = combine_matrix sup"
  2.1451  
  2.1452  instance
  2.1453    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
  2.1454 @@ -25,7 +1453,7 @@
  2.1455  begin
  2.1456  
  2.1457  definition
  2.1458 -  plus_matrix_def: "A + B = combine_matrix (op +) A B"
  2.1459 +  plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
  2.1460  
  2.1461  instance ..
  2.1462  
  2.1463 @@ -35,7 +1463,7 @@
  2.1464  begin
  2.1465  
  2.1466  definition
  2.1467 -  minus_matrix_def: "- A = apply_matrix uminus A"
  2.1468 +  minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
  2.1469  
  2.1470  instance ..
  2.1471  
  2.1472 @@ -45,7 +1473,7 @@
  2.1473  begin
  2.1474  
  2.1475  definition
  2.1476 -  diff_matrix_def: "A - B = combine_matrix (op -) A B"
  2.1477 +  diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
  2.1478  
  2.1479  instance ..
  2.1480  
  2.1481 @@ -55,7 +1483,7 @@
  2.1482  begin
  2.1483  
  2.1484  definition
  2.1485 -  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
  2.1486 +  times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
  2.1487  
  2.1488  instance ..
  2.1489  
  2.1490 @@ -65,7 +1493,7 @@
  2.1491  begin
  2.1492  
  2.1493  definition
  2.1494 -  abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
  2.1495 +  abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
  2.1496  
  2.1497  instance ..
  2.1498  
     3.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Jul 03 20:53:44 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1434 +0,0 @@
     3.4 -(*  Title:      HOL/Matrix/MatrixGeneral.thy
     3.5 -    ID:         $Id$
     3.6 -    Author:     Steven Obua
     3.7 -*)
     3.8 -
     3.9 -theory MatrixGeneral
    3.10 -imports Main
    3.11 -begin
    3.12 -
    3.13 -types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"
    3.14 -
    3.15 -constdefs
    3.16 -  nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set"
    3.17 -  "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}"
    3.18 -
    3.19 -typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}"
    3.20 -apply (rule_tac x="(% j i. 0)" in exI)
    3.21 -by (simp add: nonzero_positions_def)
    3.22 -
    3.23 -declare Rep_matrix_inverse[simp]
    3.24 -
    3.25 -lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
    3.26 -apply (rule Abs_matrix_induct)
    3.27 -by (simp add: Abs_matrix_inverse matrix_def)
    3.28 -
    3.29 -constdefs
    3.30 -  nrows :: "('a::zero) matrix \<Rightarrow> nat"
    3.31 -  "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
    3.32 -  ncols :: "('a::zero) matrix \<Rightarrow> nat"
    3.33 -  "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
    3.34 -
    3.35 -lemma nrows:
    3.36 -  assumes hyp: "nrows A \<le> m"
    3.37 -  shows "(Rep_matrix A m n) = 0" (is ?concl)
    3.38 -proof cases
    3.39 -  assume "nonzero_positions(Rep_matrix A) = {}"
    3.40 -  then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
    3.41 -next
    3.42 -  assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
    3.43 -  let ?S = "fst`(nonzero_positions(Rep_matrix A))"
    3.44 -  have c: "finite (?S)" by (simp add: finite_nonzero_positions)
    3.45 -  from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
    3.46 -  have "m \<notin> ?S"
    3.47 -    proof -
    3.48 -      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])
    3.49 -      moreover from d have "~(m <= Max ?S)" by (simp)
    3.50 -      ultimately show "m \<notin> ?S" by (auto)
    3.51 -    qed
    3.52 -  thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
    3.53 -qed
    3.54 -
    3.55 -constdefs
    3.56 -  transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
    3.57 -  "transpose_infmatrix A j i == A i j"
    3.58 -  transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"
    3.59 -  "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"
    3.60 -
    3.61 -declare transpose_infmatrix_def[simp]
    3.62 -
    3.63 -lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"
    3.64 -by ((rule ext)+, simp)
    3.65 -
    3.66 -lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
    3.67 -  apply (rule ext)+
    3.68 -  by (simp add: transpose_infmatrix_def)
    3.69 -
    3.70 -lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
    3.71 -apply (rule Abs_matrix_inverse)
    3.72 -apply (simp add: matrix_def nonzero_positions_def image_def)
    3.73 -proof -
    3.74 -  let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
    3.75 -  let ?swap = "% pos. (snd pos, fst pos)"
    3.76 -  let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
    3.77 -  have swap_image: "?swap`?A = ?B"
    3.78 -    apply (simp add: image_def)
    3.79 -    apply (rule set_ext)
    3.80 -    apply (simp)
    3.81 -    proof
    3.82 -      fix y
    3.83 -      assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
    3.84 -      thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    3.85 -        proof -
    3.86 -          from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
    3.87 -          then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
    3.88 -        qed
    3.89 -    next
    3.90 -      fix y
    3.91 -      assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
    3.92 -      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
    3.93 -	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
    3.94 -    qed
    3.95 -  then have "finite (?swap`?A)"
    3.96 -    proof -
    3.97 -      have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
    3.98 -      then have "finite ?B" by (simp add: nonzero_positions_def)
    3.99 -      with swap_image show "finite (?swap`?A)" by (simp)
   3.100 -    qed
   3.101 -  moreover
   3.102 -  have "inj_on ?swap ?A" by (simp add: inj_on_def)
   3.103 -  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
   3.104 -qed
   3.105 -
   3.106 -lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
   3.107 -
   3.108 -lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
   3.109 -apply (auto)
   3.110 -apply (rule ext)+
   3.111 -apply (simp add: transpose_infmatrix)
   3.112 -apply (drule infmatrixforward)
   3.113 -apply (simp)
   3.114 -done
   3.115 -
   3.116 -lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
   3.117 -apply (simp add: transpose_matrix_def)
   3.118 -apply (subst Rep_matrix_inject[THEN sym])+
   3.119 -apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
   3.120 -done
   3.121 -
   3.122 -lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
   3.123 -by (simp add: transpose_matrix_def)
   3.124 -
   3.125 -lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
   3.126 -by (simp add: transpose_matrix_def)
   3.127 -
   3.128 -lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"
   3.129 -by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   3.130 -
   3.131 -lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"
   3.132 -by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
   3.133 -
   3.134 -lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"
   3.135 -proof -
   3.136 -  assume "ncols A <= n"
   3.137 -  then have "nrows (transpose_matrix A) <= n" by (simp)
   3.138 -  then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)
   3.139 -  thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)
   3.140 -qed
   3.141 -
   3.142 -lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
   3.143 -apply (auto)
   3.144 -apply (simp add: ncols)
   3.145 -proof (simp add: ncols_def, auto)
   3.146 -  let ?P = "nonzero_positions (Rep_matrix A)"
   3.147 -  let ?p = "snd`?P"
   3.148 -  have a:"finite ?p" by (simp add: finite_nonzero_positions)
   3.149 -  let ?m = "Max ?p"
   3.150 -  assume "~(Suc (?m) <= n)"
   3.151 -  then have b:"n <= ?m" by (simp)
   3.152 -  fix a b
   3.153 -  assume "(a,b) \<in> ?P"
   3.154 -  then have "?p \<noteq> {}" by (auto)
   3.155 -  with a have "?m \<in>  ?p" by (simp)
   3.156 -  moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
   3.157 -  ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
   3.158 -  moreover assume ?st
   3.159 -  ultimately show "False" using b by (simp)
   3.160 -qed
   3.161 -
   3.162 -lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   3.163 -proof -
   3.164 -  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   3.165 -  show ?concl by (simp add: a ncols_le)
   3.166 -qed
   3.167 -
   3.168 -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)
   3.169 -apply (auto)
   3.170 -apply (subgoal_tac "ncols A <= m")
   3.171 -apply (simp)
   3.172 -apply (simp add: ncols_le)
   3.173 -apply (drule_tac x="ncols A" in spec)
   3.174 -by (simp add: ncols)
   3.175 -
   3.176 -lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
   3.177 -proof -
   3.178 -  have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)
   3.179 -  also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
   3.180 -  also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
   3.181 -  finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
   3.182 -qed
   3.183 -
   3.184 -lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
   3.185 -proof -
   3.186 -  have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
   3.187 -  show ?concl by (simp add: a nrows_le)
   3.188 -qed
   3.189 -
   3.190 -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)
   3.191 -apply (auto)
   3.192 -apply (subgoal_tac "nrows A <= m")
   3.193 -apply (simp)
   3.194 -apply (simp add: nrows_le)
   3.195 -apply (drule_tac x="nrows A" in spec)
   3.196 -by (simp add: nrows)
   3.197 -
   3.198 -lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
   3.199 -apply (case_tac "nrows A <= m")
   3.200 -apply (simp_all add: nrows)
   3.201 -done
   3.202 -
   3.203 -lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
   3.204 -apply (case_tac "ncols A <= n")
   3.205 -apply (simp_all add: ncols)
   3.206 -done
   3.207 -
   3.208 -lemma finite_natarray1: "finite {x. x < (n::nat)}"
   3.209 -apply (induct n)
   3.210 -apply (simp)
   3.211 -proof -
   3.212 -  fix n
   3.213 -  have "{x. x < Suc n} = insert n {x. x < n}"  by (rule set_ext, simp, arith)
   3.214 -  moreover assume "finite {x. x < n}"
   3.215 -  ultimately show "finite {x. x < Suc n}" by (simp)
   3.216 -qed
   3.217 -
   3.218 -lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
   3.219 -  apply (induct m)
   3.220 -  apply (simp+)
   3.221 -  proof -
   3.222 -    fix m::nat
   3.223 -    let ?s0 = "{pos. fst pos < m & snd pos < n}"
   3.224 -    let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
   3.225 -    let ?sd = "{pos. fst pos = m & snd pos < n}"
   3.226 -    assume f0: "finite ?s0"
   3.227 -    have f1: "finite ?sd"
   3.228 -    proof -
   3.229 -      let ?f = "% x. (m, x)"
   3.230 -      have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
   3.231 -      moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
   3.232 -      ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
   3.233 -    qed
   3.234 -    have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith)
   3.235 -    from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
   3.236 -    with su show "finite ?s1" by (simp)
   3.237 -qed
   3.238 -
   3.239 -lemma RepAbs_matrix:
   3.240 -  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)
   3.241 -  shows "(Rep_matrix (Abs_matrix x)) = x"
   3.242 -apply (rule Abs_matrix_inverse)
   3.243 -apply (simp add: matrix_def nonzero_positions_def)
   3.244 -proof -
   3.245 -  from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
   3.246 -  from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
   3.247 -  let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
   3.248 -  let ?v = "{pos. fst pos < m & snd pos < n}"
   3.249 -  have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
   3.250 -  from a b have "(?u \<inter> (-?v)) = {}"
   3.251 -    apply (simp)
   3.252 -    apply (rule set_ext)
   3.253 -    apply (simp)
   3.254 -    apply auto
   3.255 -    by (rule c, auto)+
   3.256 -  then have d: "?u \<subseteq> ?v" by blast
   3.257 -  moreover have "finite ?v" by (simp add: finite_natarray2)
   3.258 -  ultimately show "finite ?u" by (rule finite_subset)
   3.259 -qed
   3.260 -
   3.261 -constdefs
   3.262 -  apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
   3.263 -  "apply_infmatrix f == % A. (% j i. f (A j i))"
   3.264 -  apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
   3.265 -  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
   3.266 -  combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
   3.267 -  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
   3.268 -  combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
   3.269 -  "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
   3.270 -
   3.271 -lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
   3.272 -by (simp add: apply_infmatrix_def)
   3.273 -
   3.274 -lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
   3.275 -by (simp add: combine_infmatrix_def)
   3.276 -
   3.277 -constdefs
   3.278 -commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
   3.279 -"commutative f == ! x y. f x y = f y x"
   3.280 -associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   3.281 -"associative f == ! x y z. f (f x y) z = f x (f y z)"
   3.282 -
   3.283 -text{*
   3.284 -To reason about associativity and commutativity of operations on matrices,
   3.285 -let's take a step back and look at the general situtation: Assume that we have
   3.286 -sets $A$ and $B$ with $B \subset A$ and an abstraction $u: A \rightarrow B$. This abstraction has to fulfill $u(b) = b$ for all $b \in B$, but is arbitrary otherwise.
   3.287 -Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.
   3.288 -It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$
   3.289 -*}
   3.290 -
   3.291 -lemma combine_infmatrix_commute:
   3.292 -  "commutative f \<Longrightarrow> commutative (combine_infmatrix f)"
   3.293 -by (simp add: commutative_def combine_infmatrix_def)
   3.294 -
   3.295 -lemma combine_matrix_commute:
   3.296 -"commutative f \<Longrightarrow> commutative (combine_matrix f)"
   3.297 -by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
   3.298 -
   3.299 -text{*
   3.300 -On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,
   3.301 -as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have
   3.302 -\[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
   3.303 -but on the other hand we have
   3.304 -\[ f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.\]
   3.305 -A way out of this problem is to assume that $f(A\times A)\subset A$ holds, and this is what we are going to do:
   3.306 -*}
   3.307 -
   3.308 -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)"
   3.309 -by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)
   3.310 -
   3.311 -lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
   3.312 -by (insert Rep_matrix [of A], simp add: matrix_def)
   3.313 -
   3.314 -lemma combine_infmatrix_closed [simp]:
   3.315 -  "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)"
   3.316 -apply (rule Abs_matrix_inverse)
   3.317 -apply (simp add: matrix_def)
   3.318 -apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])
   3.319 -by (simp_all)
   3.320 -
   3.321 -text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}
   3.322 -lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"
   3.323 -by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)
   3.324 -
   3.325 -lemma apply_infmatrix_closed [simp]:
   3.326 -  "f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"
   3.327 -apply (rule Abs_matrix_inverse)
   3.328 -apply (simp add: matrix_def)
   3.329 -apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])
   3.330 -by (simp_all)
   3.331 -
   3.332 -lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"
   3.333 -by (simp add: associative_def combine_infmatrix_def)
   3.334 -
   3.335 -lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
   3.336 -by (auto)
   3.337 -
   3.338 -lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"
   3.339 -apply (simp(no_asm) add: associative_def combine_matrix_def, auto)
   3.340 -apply (rule comb [of Abs_matrix Abs_matrix])
   3.341 -by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)
   3.342 -
   3.343 -lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"
   3.344 -by (simp add: apply_matrix_def)
   3.345 -
   3.346 -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)"
   3.347 -  by(simp add: combine_matrix_def)
   3.348 -
   3.349 -lemma combine_nrows_max: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
   3.350 -by (simp add: nrows_le)
   3.351 -
   3.352 -lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
   3.353 -by (simp add: ncols_le)
   3.354 -
   3.355 -lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
   3.356 -  by (simp add: nrows_le)
   3.357 -
   3.358 -lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
   3.359 -  by (simp add: ncols_le)
   3.360 -
   3.361 -constdefs
   3.362 -  zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
   3.363 -  "zero_r_neutral f == ! a. f a 0 = a"
   3.364 -  zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   3.365 -  "zero_l_neutral f == ! a. f 0 a = a"
   3.366 -  zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
   3.367 -  "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
   3.368 -
   3.369 -consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   3.370 -primrec
   3.371 -  "foldseq f s 0 = s 0"
   3.372 -  "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
   3.373 -
   3.374 -consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
   3.375 -primrec
   3.376 -  "foldseq_transposed f s 0 = s 0"
   3.377 -  "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
   3.378 -
   3.379 -lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
   3.380 -proof -
   3.381 -  assume a:"associative f"
   3.382 -  then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   3.383 -  proof -
   3.384 -    fix n
   3.385 -    show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   3.386 -    proof (induct n)
   3.387 -      show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
   3.388 -    next
   3.389 -      fix n
   3.390 -      assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   3.391 -      have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
   3.392 -      show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
   3.393 -      proof (auto)
   3.394 -        fix N t
   3.395 -        assume Nsuc: "N <= Suc n"
   3.396 -        show "foldseq f t N = foldseq_transposed f t N"
   3.397 -        proof cases
   3.398 -          assume "N <= n"
   3.399 -          then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
   3.400 -        next
   3.401 -          assume "~(N <= n)"
   3.402 -          with Nsuc have Nsuceq: "N = Suc n" by simp
   3.403 -          have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
   3.404 -          have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
   3.405 -          show "foldseq f t N = foldseq_transposed f t N"
   3.406 -            apply (simp add: Nsuceq)
   3.407 -            apply (subst c)
   3.408 -            apply (simp)
   3.409 -            apply (case_tac "n = 0")
   3.410 -            apply (simp)
   3.411 -            apply (drule neqz)
   3.412 -            apply (erule exE)
   3.413 -            apply (simp)
   3.414 -            apply (subst assocf)
   3.415 -            proof -
   3.416 -              fix m
   3.417 -              assume "n = Suc m & Suc m <= n"
   3.418 -              then have mless: "Suc m <= n" by arith
   3.419 -              then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")
   3.420 -                apply (subst c)
   3.421 -                by simp+
   3.422 -              have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
   3.423 -              have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
   3.424 -                apply (subst c)
   3.425 -                by (simp add: mless)+
   3.426 -              have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
   3.427 -              from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
   3.428 -            qed
   3.429 -          qed
   3.430 -        qed
   3.431 -      qed
   3.432 -    qed
   3.433 -    show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
   3.434 -  qed
   3.435 -
   3.436 -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)"
   3.437 -proof -
   3.438 -  assume assoc: "associative f"
   3.439 -  assume comm: "commutative f"
   3.440 -  from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)
   3.441 -  from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)
   3.442 -  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)
   3.443 -  have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
   3.444 -    apply (induct_tac n)
   3.445 -    apply (simp+, auto)
   3.446 -    by (simp add: a b c)
   3.447 -  then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
   3.448 -qed
   3.449 -
   3.450 -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)"
   3.451 -oops
   3.452 -(* Model found
   3.453 -
   3.454 -Trying to find a model that refutes: \<lbrakk>associative f; associative g;
   3.455 - \<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;
   3.456 - \<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk>
   3.457 -\<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y)
   3.458 -Searching for a model of size 1, translating term... invoking SAT solver... no model found.
   3.459 -Searching for a model of size 2, translating term... invoking SAT solver... no model found.
   3.460 -Searching for a model of size 3, translating term... invoking SAT solver...
   3.461 -Model found:
   3.462 -Size of types: 'a: 3
   3.463 -x: a1
   3.464 -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))
   3.465 -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))
   3.466 -*)
   3.467 -
   3.468 -lemma foldseq_zero:
   3.469 -assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"
   3.470 -shows "foldseq f s n = 0"
   3.471 -proof -
   3.472 -  have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
   3.473 -    apply (induct_tac n)
   3.474 -    apply (simp)
   3.475 -    by (simp add: fz)
   3.476 -  then show "foldseq f s n = 0" by (simp add: sz)
   3.477 -qed
   3.478 -
   3.479 -lemma foldseq_significant_positions:
   3.480 -  assumes p: "! i. i <= N \<longrightarrow> S i = T i"
   3.481 -  shows "foldseq f S N = foldseq f T N" (is ?concl)
   3.482 -proof -
   3.483 -  have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
   3.484 -    apply (induct_tac m)
   3.485 -    apply (simp)
   3.486 -    apply (simp)
   3.487 -    apply (auto)
   3.488 -    proof -
   3.489 -      fix n
   3.490 -      fix s::"nat\<Rightarrow>'a"
   3.491 -      fix t::"nat\<Rightarrow>'a"
   3.492 -      assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
   3.493 -      assume b: "\<forall>i\<le>Suc n. s i = t i"
   3.494 -      have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast
   3.495 -      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)
   3.496 -      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)
   3.497 -    qed
   3.498 -  with p show ?concl by simp
   3.499 -qed
   3.500 -
   3.501 -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")
   3.502 -proof -
   3.503 -  have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
   3.504 -  have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
   3.505 -  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"
   3.506 -    apply (induct_tac n)
   3.507 -    apply (simp)
   3.508 -    apply (simp)
   3.509 -    apply (auto)
   3.510 -    apply (case_tac "m = Suc na")
   3.511 -    apply (simp)
   3.512 -    apply (rule a)
   3.513 -    apply (rule foldseq_significant_positions)
   3.514 -    apply (auto)
   3.515 -    apply (drule suc, simp+)
   3.516 -    proof -
   3.517 -      fix na m s
   3.518 -      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"
   3.519 -      assume subb:"m <= na"
   3.520 -      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
   3.521 -      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 =
   3.522 -        foldseq f (% k. s(Suc k)) na"
   3.523 -        by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)
   3.524 -      from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith
   3.525 -      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) =
   3.526 -        foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
   3.527 -        apply (simp add: subd)
   3.528 -        apply (case_tac "m=0")
   3.529 -        apply (simp)
   3.530 -        apply (drule sube)
   3.531 -        apply (auto)
   3.532 -        apply (rule a)
   3.533 -        by (simp add: subc if_def)
   3.534 -    qed
   3.535 -  then show "?p \<Longrightarrow> ?concl" by simp
   3.536 -qed
   3.537 -
   3.538 -lemma foldseq_zerotail:
   3.539 -  assumes
   3.540 -  fz: "f 0 0 = 0"
   3.541 -  and sz: "! i.  n <= i \<longrightarrow> s i = 0"
   3.542 -  and nm: "n <= m"
   3.543 -  shows
   3.544 -  "foldseq f s n = foldseq f s m"
   3.545 -proof -
   3.546 -  show "foldseq f s n = foldseq f s m"
   3.547 -    apply (simp add: foldseq_tail[OF nm, of f s])
   3.548 -    apply (rule foldseq_significant_positions)
   3.549 -    apply (auto)
   3.550 -    apply (subst foldseq_zero)
   3.551 -    by (simp add: fz sz)+
   3.552 -qed
   3.553 -
   3.554 -lemma foldseq_zerotail2:
   3.555 -  assumes "! x. f x 0 = x"
   3.556 -  and "! i. n < i \<longrightarrow> s i = 0"
   3.557 -  and nm: "n <= m"
   3.558 -  shows
   3.559 -  "foldseq f s n = foldseq f s m" (is ?concl)
   3.560 -proof -
   3.561 -  have "f 0 0 = 0" by (simp add: prems)
   3.562 -  have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
   3.563 -  have c: "0 <= m" by simp
   3.564 -  have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   3.565 -  show ?concl
   3.566 -    apply (subst foldseq_tail[OF nm])
   3.567 -    apply (rule foldseq_significant_positions)
   3.568 -    apply (auto)
   3.569 -    apply (case_tac "m=n")
   3.570 -    apply (simp+)
   3.571 -    apply (drule b[OF nm])
   3.572 -    apply (auto)
   3.573 -    apply (case_tac "k=0")
   3.574 -    apply (simp add: prems)
   3.575 -    apply (drule d)
   3.576 -    apply (auto)
   3.577 -    by (simp add: prems foldseq_zero)
   3.578 -qed
   3.579 -
   3.580 -lemma foldseq_zerostart:
   3.581 -  "! 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))"
   3.582 -proof -
   3.583 -  assume f00x: "! x. f 0 (f 0 x) = f 0 x"
   3.584 -  have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
   3.585 -    apply (induct n)
   3.586 -    apply (simp)
   3.587 -    apply (rule allI, rule impI)
   3.588 -    proof -
   3.589 -      fix n
   3.590 -      fix s
   3.591 -      have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp
   3.592 -      assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"
   3.593 -      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
   3.594 -      assume d: "! i. i <= Suc n \<longrightarrow> s i = 0"
   3.595 -      show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"
   3.596 -        apply (subst a)
   3.597 -        apply (subst c)
   3.598 -        by (simp add: d f00x)+
   3.599 -    qed
   3.600 -  then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
   3.601 -qed
   3.602 -
   3.603 -lemma foldseq_zerostart2:
   3.604 -  "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
   3.605 -proof -
   3.606 -  assume a:"! i. i<n \<longrightarrow> s i = 0"
   3.607 -  assume x:"! x. f 0 x = x"
   3.608 -  from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast
   3.609 -  have b: "!! i l. i < Suc l = (i <= l)" by arith
   3.610 -  have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
   3.611 -  show "foldseq f s n = s n"
   3.612 -  apply (case_tac "n=0")
   3.613 -  apply (simp)
   3.614 -  apply (insert a)
   3.615 -  apply (drule d)
   3.616 -  apply (auto)
   3.617 -  apply (simp add: b)
   3.618 -  apply (insert f00x)
   3.619 -  apply (drule foldseq_zerostart)
   3.620 -  by (simp add: x)+
   3.621 -qed
   3.622 -
   3.623 -lemma foldseq_almostzero:
   3.624 -  assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
   3.625 -  shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
   3.626 -proof -
   3.627 -  from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
   3.628 -  from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
   3.629 -  show ?concl
   3.630 -    apply auto
   3.631 -    apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
   3.632 -    apply simp
   3.633 -    apply (subst foldseq_zerostart2)
   3.634 -    apply (simp add: f0x a)+
   3.635 -    apply (subst foldseq_zero)
   3.636 -    by (simp add: s0 f0x)+
   3.637 -qed
   3.638 -
   3.639 -lemma foldseq_distr_unary:
   3.640 -  assumes "!! a b. g (f a b) = f (g a) (g b)"
   3.641 -  shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
   3.642 -proof -
   3.643 -  have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
   3.644 -    apply (induct_tac n)
   3.645 -    apply (simp)
   3.646 -    apply (simp)
   3.647 -    apply (auto)
   3.648 -    apply (drule_tac x="% k. s (Suc k)" in spec)
   3.649 -    by (simp add: prems)
   3.650 -  then show ?concl by simp
   3.651 -qed
   3.652 -
   3.653 -constdefs
   3.654 -  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"
   3.655 -  "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)"
   3.656 -  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"
   3.657 -  "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
   3.658 -
   3.659 -lemma mult_matrix_n:
   3.660 -  assumes prems: "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
   3.661 -  shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
   3.662 -proof -
   3.663 -  show ?concl using prems
   3.664 -    apply (simp add: mult_matrix_def mult_matrix_n_def)
   3.665 -    apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   3.666 -    by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
   3.667 -qed
   3.668 -
   3.669 -lemma mult_matrix_nm:
   3.670 -  assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
   3.671 -  shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
   3.672 -proof -
   3.673 -  from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
   3.674 -  also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
   3.675 -  finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
   3.676 -qed
   3.677 -
   3.678 -constdefs
   3.679 -  r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   3.680 -  "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
   3.681 -  l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   3.682 -  "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
   3.683 -  distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   3.684 -  "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
   3.685 -
   3.686 -lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
   3.687 -lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
   3.688 -
   3.689 -lemma r_distributive_matrix:
   3.690 - assumes prems:
   3.691 -  "r_distributive fmul fadd"
   3.692 -  "associative fadd"
   3.693 -  "commutative fadd"
   3.694 -  "fadd 0 0 = 0"
   3.695 -  "! a. fmul a 0 = 0"
   3.696 -  "! a. fmul 0 a = 0"
   3.697 - shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   3.698 -proof -
   3.699 -  from prems show ?concl
   3.700 -    apply (simp add: r_distributive_def mult_matrix_def, auto)
   3.701 -    proof -
   3.702 -      fix a::"'a matrix"
   3.703 -      fix u::"'b matrix"
   3.704 -      fix v::"'b matrix"
   3.705 -      let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
   3.706 -      from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
   3.707 -        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)"
   3.708 -        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   3.709 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.710 -        apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])
   3.711 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.712 -        apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])
   3.713 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.714 -        apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
   3.715 -        apply (simp add: combine_matrix_def combine_infmatrix_def)
   3.716 -        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   3.717 -        apply (simplesubst RepAbs_matrix)
   3.718 -        apply (simp, auto)
   3.719 -        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   3.720 -        apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
   3.721 -        apply (subst RepAbs_matrix)
   3.722 -        apply (simp, auto)
   3.723 -        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
   3.724 -        apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
   3.725 -        done
   3.726 -    qed
   3.727 -qed
   3.728 -
   3.729 -lemma l_distributive_matrix:
   3.730 - assumes prems:
   3.731 -  "l_distributive fmul fadd"
   3.732 -  "associative fadd"
   3.733 -  "commutative fadd"
   3.734 -  "fadd 0 0 = 0"
   3.735 -  "! a. fmul a 0 = 0"
   3.736 -  "! a. fmul 0 a = 0"
   3.737 - shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
   3.738 -proof -
   3.739 -  from prems show ?concl
   3.740 -    apply (simp add: l_distributive_def mult_matrix_def, auto)
   3.741 -    proof -
   3.742 -      fix a::"'b matrix"
   3.743 -      fix u::"'a matrix"
   3.744 -      fix v::"'a matrix"
   3.745 -      let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
   3.746 -      from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
   3.747 -               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)"
   3.748 -        apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
   3.749 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.750 -        apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])
   3.751 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.752 -        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
   3.753 -        apply (simp add: max1 max2 combine_nrows combine_ncols)+
   3.754 -        apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
   3.755 -        apply (simp add: combine_matrix_def combine_infmatrix_def)
   3.756 -        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   3.757 -        apply (simplesubst RepAbs_matrix)
   3.758 -        apply (simp, auto)
   3.759 -        apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
   3.760 -        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   3.761 -        apply (subst RepAbs_matrix)
   3.762 -        apply (simp, auto)
   3.763 -        apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
   3.764 -        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
   3.765 -        done
   3.766 -    qed
   3.767 -qed
   3.768 -
   3.769 -instance matrix :: (zero) zero ..
   3.770 -
   3.771 -defs(overloaded)
   3.772 -  zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
   3.773 -
   3.774 -lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
   3.775 -  apply (simp add: zero_matrix_def)
   3.776 -  apply (subst RepAbs_matrix)
   3.777 -  by (auto)
   3.778 -
   3.779 -lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
   3.780 -proof -
   3.781 -  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   3.782 -  show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
   3.783 -qed
   3.784 -
   3.785 -lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
   3.786 -proof -
   3.787 -  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   3.788 -  show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
   3.789 -qed
   3.790 -
   3.791 -lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
   3.792 -  by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
   3.793 -
   3.794 -lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
   3.795 -  by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
   3.796 -
   3.797 -lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
   3.798 -  apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
   3.799 -  apply (auto)
   3.800 -  by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
   3.801 -
   3.802 -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"
   3.803 -  apply (simp add: mult_matrix_n_def)
   3.804 -  apply (subst foldseq_zero)
   3.805 -  by (simp_all add: zero_matrix_def)
   3.806 -
   3.807 -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"
   3.808 -  apply (simp add: mult_matrix_n_def)
   3.809 -  apply (subst foldseq_zero)
   3.810 -  by (simp_all add: zero_matrix_def)
   3.811 -
   3.812 -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"
   3.813 -by (simp add: mult_matrix_def)
   3.814 -
   3.815 -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"
   3.816 -by (simp add: mult_matrix_def)
   3.817 -
   3.818 -lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"
   3.819 -  apply (simp add: apply_matrix_def apply_infmatrix_def)
   3.820 -  by (simp add: zero_matrix_def)
   3.821 -
   3.822 -lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"
   3.823 -  apply (simp add: combine_matrix_def combine_infmatrix_def)
   3.824 -  by (simp add: zero_matrix_def)
   3.825 -
   3.826 -lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
   3.827 -apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
   3.828 -apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   3.829 -apply (simp add: RepAbs_matrix)
   3.830 -done
   3.831 -
   3.832 -lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
   3.833 -  apply (simp add: apply_matrix_def apply_infmatrix_def)
   3.834 -  by (simp add: zero_matrix_def)
   3.835 -
   3.836 -constdefs
   3.837 -  singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"
   3.838 -  "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
   3.839 -  move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"
   3.840 -  "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)))"
   3.841 -  take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   3.842 -  "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
   3.843 -  take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   3.844 -  "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
   3.845 -
   3.846 -constdefs
   3.847 -  column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   3.848 -  "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
   3.849 -  row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   3.850 -  "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
   3.851 -
   3.852 -lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
   3.853 -apply (simp add: singleton_matrix_def)
   3.854 -apply (auto)
   3.855 -apply (subst RepAbs_matrix)
   3.856 -apply (rule exI[of _ "Suc m"], simp)
   3.857 -apply (rule exI[of _ "Suc n"], simp+)
   3.858 -by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
   3.859 -
   3.860 -lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
   3.861 -apply (subst Rep_matrix_inject[symmetric])
   3.862 -apply (rule ext)+
   3.863 -apply (simp)
   3.864 -done
   3.865 -
   3.866 -lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
   3.867 -  by (simp add: singleton_matrix_def zero_matrix_def)
   3.868 -
   3.869 -lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
   3.870 -proof-
   3.871 -have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   3.872 -from th show ?thesis 
   3.873 -apply (auto)
   3.874 -apply (rule le_anti_sym)
   3.875 -apply (subst nrows_le)
   3.876 -apply (simp add: singleton_matrix_def, auto)
   3.877 -apply (subst RepAbs_matrix)
   3.878 -apply auto
   3.879 -apply (simp add: Suc_le_eq)
   3.880 -apply (rule not_leE)
   3.881 -apply (subst nrows_le)
   3.882 -by simp
   3.883 -qed
   3.884 -
   3.885 -lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
   3.886 -proof-
   3.887 -have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   3.888 -from th show ?thesis 
   3.889 -apply (auto)
   3.890 -apply (rule le_anti_sym)
   3.891 -apply (subst ncols_le)
   3.892 -apply (simp add: singleton_matrix_def, auto)
   3.893 -apply (subst RepAbs_matrix)
   3.894 -apply auto
   3.895 -apply (simp add: Suc_le_eq)
   3.896 -apply (rule not_leE)
   3.897 -apply (subst ncols_le)
   3.898 -by simp
   3.899 -qed
   3.900 -
   3.901 -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)"
   3.902 -apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
   3.903 -apply (subst RepAbs_matrix)
   3.904 -apply (rule exI[of _ "Suc j"], simp)
   3.905 -apply (rule exI[of _ "Suc i"], simp)
   3.906 -apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
   3.907 -apply (subst RepAbs_matrix)
   3.908 -apply (rule exI[of _ "Suc j"], simp)
   3.909 -apply (rule exI[of _ "Suc i"], simp)
   3.910 -by simp
   3.911 -
   3.912 -lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
   3.913 -apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   3.914 -apply (simp)
   3.915 -done
   3.916 -
   3.917 -lemma Rep_move_matrix[simp]:
   3.918 -  "Rep_matrix (move_matrix A y x) j i =
   3.919 -  (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
   3.920 -apply (simp add: move_matrix_def)
   3.921 -apply (auto)
   3.922 -by (subst RepAbs_matrix,
   3.923 -  rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
   3.924 -  rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
   3.925 -
   3.926 -lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
   3.927 -by (simp add: move_matrix_def)
   3.928 -
   3.929 -lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
   3.930 -apply (subst Rep_matrix_inject[symmetric])
   3.931 -apply (rule ext)+
   3.932 -apply (simp)
   3.933 -done
   3.934 -
   3.935 -lemma transpose_move_matrix[simp]:
   3.936 -  "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
   3.937 -apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   3.938 -apply (simp)
   3.939 -done
   3.940 -
   3.941 -lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
   3.942 -  (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
   3.943 -  apply (subst Rep_matrix_inject[symmetric])
   3.944 -  apply (rule ext)+
   3.945 -  apply (case_tac "j + int u < 0")
   3.946 -  apply (simp, arith)
   3.947 -  apply (case_tac "i + int v < 0")
   3.948 -  apply (simp add: neg_def, arith)
   3.949 -  apply (simp add: neg_def)
   3.950 -  apply arith
   3.951 -  done
   3.952 -
   3.953 -lemma Rep_take_columns[simp]:
   3.954 -  "Rep_matrix (take_columns A c) j i =
   3.955 -  (if i < c then (Rep_matrix A j i) else 0)"
   3.956 -apply (simp add: take_columns_def)
   3.957 -apply (simplesubst RepAbs_matrix)
   3.958 -apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   3.959 -apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   3.960 -done
   3.961 -
   3.962 -lemma Rep_take_rows[simp]:
   3.963 -  "Rep_matrix (take_rows A r) j i =
   3.964 -  (if j < r then (Rep_matrix A j i) else 0)"
   3.965 -apply (simp add: take_rows_def)
   3.966 -apply (simplesubst RepAbs_matrix)
   3.967 -apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
   3.968 -apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
   3.969 -done
   3.970 -
   3.971 -lemma Rep_column_of_matrix[simp]:
   3.972 -  "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"
   3.973 -  by (simp add: column_of_matrix_def)
   3.974 -
   3.975 -lemma Rep_row_of_matrix[simp]:
   3.976 -  "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   3.977 -  by (simp add: row_of_matrix_def)
   3.978 -
   3.979 -lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
   3.980 -apply (subst Rep_matrix_inject[THEN sym])
   3.981 -apply (rule ext)+
   3.982 -by (simp add: ncols)
   3.983 -
   3.984 -lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
   3.985 -apply (subst Rep_matrix_inject[THEN sym])
   3.986 -apply (rule ext)+
   3.987 -by (simp add: nrows)
   3.988 -
   3.989 -lemma mult_matrix_singleton_right[simp]:
   3.990 -  assumes prems:
   3.991 -  "! x. fmul x 0 = 0"
   3.992 -  "! x. fmul 0 x = 0"
   3.993 -  "! x. fadd 0 x = x"
   3.994 -  "! x. fadd x 0 = x"
   3.995 -  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))"
   3.996 -  apply (simp add: mult_matrix_def)
   3.997 -  apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
   3.998 -  apply (auto)
   3.999 -  apply (simp add: prems)+
  3.1000 -  apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
  3.1001 -  apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
  3.1002 -  apply (subst foldseq_almostzero[of _ j])
  3.1003 -  apply (simp add: prems)+
  3.1004 -  apply (auto)
  3.1005 -  proof -
  3.1006 -    fix k
  3.1007 -    fix l
  3.1008 -    assume a:"~neg(int l - int i)"
  3.1009 -    assume b:"nat (int l - int i) = 0"
  3.1010 -    from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
  3.1011 -    assume c: "i \<noteq> l"
  3.1012 -    from c a show "fmul (Rep_matrix A k j) e = 0" by blast
  3.1013 -  qed
  3.1014 -
  3.1015 -lemma mult_matrix_ext:
  3.1016 -  assumes
  3.1017 -  eprem:
  3.1018 -  "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)"
  3.1019 -  and fprems:
  3.1020 -  "! a. fmul 0 a = 0"
  3.1021 -  "! a. fmul a 0 = 0"
  3.1022 -  "! a. fadd a 0 = a"
  3.1023 -  "! a. fadd 0 a = a"
  3.1024 -  and contraprems:
  3.1025 -  "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
  3.1026 -  shows
  3.1027 -  "A = B"
  3.1028 -proof(rule contrapos_np[of "False"], simp)
  3.1029 -  assume a: "A \<noteq> B"
  3.1030 -  have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
  3.1031 -  have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
  3.1032 -    apply (rule contrapos_np[of "False"], simp+)
  3.1033 -    apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)
  3.1034 -    by (simp add: Rep_matrix_inject a)
  3.1035 -  then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
  3.1036 -  from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast
  3.1037 -  let ?S = "singleton_matrix I 0 e"
  3.1038 -  let ?comp = "mult_matrix fmul fadd"
  3.1039 -  have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
  3.1040 -  have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
  3.1041 -  have "~(?comp A ?S = ?comp B ?S)"
  3.1042 -    apply (rule notI)
  3.1043 -    apply (simp add: fprems eprops)
  3.1044 -    apply (simp add: Rep_matrix_inject[THEN sym])
  3.1045 -    apply (drule d[of _ _ "J"], drule d[of _ _ "0"])
  3.1046 -    by (simp add: e c eprops)
  3.1047 -  with contraprems show "False" by simp
  3.1048 -qed
  3.1049 -
  3.1050 -constdefs
  3.1051 -  foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  3.1052 -  "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
  3.1053 -  foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
  3.1054 -  "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
  3.1055 -
  3.1056 -lemma foldmatrix_transpose:
  3.1057 -  assumes
  3.1058 -  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  3.1059 -  shows
  3.1060 -  "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
  3.1061 -proof -
  3.1062 -  have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
  3.1063 -  have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
  3.1064 -    apply (induct n)
  3.1065 -    apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
  3.1066 -    apply (auto)
  3.1067 -    by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
  3.1068 -  show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
  3.1069 -    apply (simp add: foldmatrix_def foldmatrix_transposed_def)
  3.1070 -    apply (induct m, simp)
  3.1071 -    apply (simp)
  3.1072 -    apply (insert tworows)
  3.1073 -    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)
  3.1074 -    by (simp add: foldmatrix_def foldmatrix_transposed_def)
  3.1075 -qed
  3.1076 -
  3.1077 -lemma foldseq_foldseq:
  3.1078 -assumes
  3.1079 -  "associative f"
  3.1080 -  "associative g"
  3.1081 -  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
  3.1082 -shows
  3.1083 -  "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
  3.1084 -  apply (insert foldmatrix_transpose[of g f A m n])
  3.1085 -  by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
  3.1086 -
  3.1087 -lemma mult_n_nrows:
  3.1088 -assumes
  3.1089 -"! a. fmul 0 a = 0"
  3.1090 -"! a. fmul a 0 = 0"
  3.1091 -"fadd 0 0 = 0"
  3.1092 -shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
  3.1093 -apply (subst nrows_le)
  3.1094 -apply (simp add: mult_matrix_n_def)
  3.1095 -apply (subst RepAbs_matrix)
  3.1096 -apply (rule_tac x="nrows A" in exI)
  3.1097 -apply (simp add: nrows prems foldseq_zero)
  3.1098 -apply (rule_tac x="ncols B" in exI)
  3.1099 -apply (simp add: ncols prems foldseq_zero)
  3.1100 -by (simp add: nrows prems foldseq_zero)
  3.1101 -
  3.1102 -lemma mult_n_ncols:
  3.1103 -assumes
  3.1104 -"! a. fmul 0 a = 0"
  3.1105 -"! a. fmul a 0 = 0"
  3.1106 -"fadd 0 0 = 0"
  3.1107 -shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
  3.1108 -apply (subst ncols_le)
  3.1109 -apply (simp add: mult_matrix_n_def)
  3.1110 -apply (subst RepAbs_matrix)
  3.1111 -apply (rule_tac x="nrows A" in exI)
  3.1112 -apply (simp add: nrows prems foldseq_zero)
  3.1113 -apply (rule_tac x="ncols B" in exI)
  3.1114 -apply (simp add: ncols prems foldseq_zero)
  3.1115 -by (simp add: ncols prems foldseq_zero)
  3.1116 -
  3.1117 -lemma mult_nrows:
  3.1118 -assumes
  3.1119 -"! a. fmul 0 a = 0"
  3.1120 -"! a. fmul a 0 = 0"
  3.1121 -"fadd 0 0 = 0"
  3.1122 -shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
  3.1123 -by (simp add: mult_matrix_def mult_n_nrows prems)
  3.1124 -
  3.1125 -lemma mult_ncols:
  3.1126 -assumes
  3.1127 -"! a. fmul 0 a = 0"
  3.1128 -"! a. fmul a 0 = 0"
  3.1129 -"fadd 0 0 = 0"
  3.1130 -shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
  3.1131 -by (simp add: mult_matrix_def mult_n_ncols prems)
  3.1132 -
  3.1133 -lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
  3.1134 -  apply (auto simp add: nrows_le)
  3.1135 -  apply (rule nrows)
  3.1136 -  apply (arith)
  3.1137 -  done
  3.1138 -
  3.1139 -lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
  3.1140 -  apply (auto simp add: ncols_le)
  3.1141 -  apply (rule ncols)
  3.1142 -  apply (arith)
  3.1143 -  done
  3.1144 -
  3.1145 -lemma mult_matrix_assoc:
  3.1146 -  assumes prems:
  3.1147 -  "! a. fmul1 0 a = 0"
  3.1148 -  "! a. fmul1 a 0 = 0"
  3.1149 -  "! a. fmul2 0 a = 0"
  3.1150 -  "! a. fmul2 a 0 = 0"
  3.1151 -  "fadd1 0 0 = 0"
  3.1152 -  "fadd2 0 0 = 0"
  3.1153 -  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  3.1154 -  "associative fadd1"
  3.1155 -  "associative fadd2"
  3.1156 -  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  3.1157 -  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  3.1158 -  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  3.1159 -  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)
  3.1160 -proof -
  3.1161 -  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
  3.1162 -  have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (% k. fmul2 (s k) x) n"
  3.1163 -    by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
  3.1164 -  have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
  3.1165 -      by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
  3.1166 -  let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
  3.1167 -  show ?concl
  3.1168 -    apply (simp add: Rep_matrix_inject[THEN sym])
  3.1169 -    apply (rule ext)+
  3.1170 -    apply (simp add: mult_matrix_def)
  3.1171 -    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)"])
  3.1172 -    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  3.1173 -    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)+
  3.1174 -    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  3.1175 -    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  3.1176 -    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  3.1177 -    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  3.1178 -    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  3.1179 -    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  3.1180 -    apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
  3.1181 -    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
  3.1182 -    apply (simp add: mult_matrix_n_def)
  3.1183 -    apply (rule comb_left)
  3.1184 -    apply ((rule ext)+, simp)
  3.1185 -    apply (simplesubst RepAbs_matrix)
  3.1186 -    apply (rule exI[of _ "nrows B"])
  3.1187 -    apply (simp add: nrows prems foldseq_zero)
  3.1188 -    apply (rule exI[of _ "ncols C"])
  3.1189 -    apply (simp add: prems ncols foldseq_zero)
  3.1190 -    apply (subst RepAbs_matrix)
  3.1191 -    apply (rule exI[of _ "nrows A"])
  3.1192 -    apply (simp add: nrows prems foldseq_zero)
  3.1193 -    apply (rule exI[of _ "ncols B"])
  3.1194 -    apply (simp add: prems ncols foldseq_zero)
  3.1195 -    apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
  3.1196 -    apply (subst foldseq_foldseq)
  3.1197 -    apply (simp add: prems)+
  3.1198 -    by (simp add: transpose_infmatrix)
  3.1199 -qed
  3.1200 -
  3.1201 -lemma
  3.1202 -  assumes prems:
  3.1203 -  "! a. fmul1 0 a = 0"
  3.1204 -  "! a. fmul1 a 0 = 0"
  3.1205 -  "! a. fmul2 0 a = 0"
  3.1206 -  "! a. fmul2 a 0 = 0"
  3.1207 -  "fadd1 0 0 = 0"
  3.1208 -  "fadd2 0 0 = 0"
  3.1209 -  "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
  3.1210 -  "associative fadd1"
  3.1211 -  "associative fadd2"
  3.1212 -  "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
  3.1213 -  "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
  3.1214 -  "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
  3.1215 -  shows
  3.1216 -  "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
  3.1217 -apply (rule ext)+
  3.1218 -apply (simp add: comp_def )
  3.1219 -by (simp add: mult_matrix_assoc prems)
  3.1220 -
  3.1221 -lemma mult_matrix_assoc_simple:
  3.1222 -  assumes prems:
  3.1223 -  "! a. fmul 0 a = 0"
  3.1224 -  "! a. fmul a 0 = 0"
  3.1225 -  "fadd 0 0 = 0"
  3.1226 -  "associative fadd"
  3.1227 -  "commutative fadd"
  3.1228 -  "associative fmul"
  3.1229 -  "distributive fmul fadd"
  3.1230 -  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)
  3.1231 -proof -
  3.1232 -  have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
  3.1233 -    by (simp! add: associative_def commutative_def)
  3.1234 -  then show ?concl
  3.1235 -    apply (subst mult_matrix_assoc)
  3.1236 -    apply (simp_all!)
  3.1237 -    by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
  3.1238 -qed
  3.1239 -
  3.1240 -lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
  3.1241 -apply (simp add: Rep_matrix_inject[THEN sym])
  3.1242 -apply (rule ext)+
  3.1243 -by simp
  3.1244 -
  3.1245 -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)"
  3.1246 -apply (simp add: Rep_matrix_inject[THEN sym])
  3.1247 -apply (rule ext)+
  3.1248 -by simp
  3.1249 -
  3.1250 -lemma Rep_mult_matrix:
  3.1251 -  assumes
  3.1252 -  "! a. fmul 0 a = 0"
  3.1253 -  "! a. fmul a 0 = 0"
  3.1254 -  "fadd 0 0 = 0"
  3.1255 -  shows
  3.1256 -  "Rep_matrix(mult_matrix fmul fadd A B) j i =
  3.1257 -  foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
  3.1258 -apply (simp add: mult_matrix_def mult_matrix_n_def)
  3.1259 -apply (subst RepAbs_matrix)
  3.1260 -apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
  3.1261 -apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
  3.1262 -by simp
  3.1263 -
  3.1264 -lemma transpose_mult_matrix:
  3.1265 -  assumes
  3.1266 -  "! a. fmul 0 a = 0"
  3.1267 -  "! a. fmul a 0 = 0"
  3.1268 -  "fadd 0 0 = 0"
  3.1269 -  "! x y. fmul y x = fmul x y"
  3.1270 -  shows
  3.1271 -  "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
  3.1272 -  apply (simp add: Rep_matrix_inject[THEN sym])
  3.1273 -  apply (rule ext)+
  3.1274 -  by (simp! add: Rep_mult_matrix max_ac)
  3.1275 -
  3.1276 -lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
  3.1277 -apply (simp add:  Rep_matrix_inject[THEN sym])
  3.1278 -apply (rule ext)+
  3.1279 -by simp
  3.1280 -
  3.1281 -lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
  3.1282 -apply (simp add: Rep_matrix_inject[THEN sym])
  3.1283 -apply (rule ext)+
  3.1284 -by simp
  3.1285 -
  3.1286 -instantiation matrix :: ("{ord, zero}") ord
  3.1287 -begin
  3.1288 -
  3.1289 -definition
  3.1290 -  le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
  3.1291 -
  3.1292 -definition
  3.1293 -  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
  3.1294 -
  3.1295 -instance ..
  3.1296 -
  3.1297 -end
  3.1298 -
  3.1299 -instance matrix :: ("{order, zero}") order
  3.1300 -apply intro_classes
  3.1301 -apply (simp_all add: le_matrix_def less_def)
  3.1302 -apply (auto)
  3.1303 -apply (drule_tac x=j in spec, drule_tac x=j in spec)
  3.1304 -apply (drule_tac x=i in spec, drule_tac x=i in spec)
  3.1305 -apply (simp)
  3.1306 -apply (simp add: Rep_matrix_inject[THEN sym])
  3.1307 -apply (rule ext)+
  3.1308 -apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
  3.1309 -apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
  3.1310 -by simp
  3.1311 -
  3.1312 -lemma le_apply_matrix:
  3.1313 -  assumes
  3.1314 -  "f 0 = 0"
  3.1315 -  "! x y. x <= y \<longrightarrow> f x <= f y"
  3.1316 -  "(a::('a::{ord, zero}) matrix) <= b"
  3.1317 -  shows
  3.1318 -  "apply_matrix f a <= apply_matrix f b"
  3.1319 -  by (simp! add: le_matrix_def)
  3.1320 -
  3.1321 -lemma le_combine_matrix:
  3.1322 -  assumes
  3.1323 -  "f 0 0 = 0"
  3.1324 -  "! a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"
  3.1325 -  "A <= B"
  3.1326 -  "C <= D"
  3.1327 -  shows
  3.1328 -  "combine_matrix f A C <= combine_matrix f B D"
  3.1329 -by (simp! add: le_matrix_def)
  3.1330 -
  3.1331 -lemma le_left_combine_matrix:
  3.1332 -  assumes
  3.1333 -  "f 0 0 = 0"
  3.1334 -  "! a b c. a <= b \<longrightarrow> f c a <= f c b"
  3.1335 -  "A <= B"
  3.1336 -  shows
  3.1337 -  "combine_matrix f C A <= combine_matrix f C B"
  3.1338 -  by (simp! add: le_matrix_def)
  3.1339 -
  3.1340 -lemma le_right_combine_matrix:
  3.1341 -  assumes
  3.1342 -  "f 0 0 = 0"
  3.1343 -  "! a b c. a <= b \<longrightarrow> f a c <= f b c"
  3.1344 -  "A <= B"
  3.1345 -  shows
  3.1346 -  "combine_matrix f A C <= combine_matrix f B C"
  3.1347 -  by (simp! add: le_matrix_def)
  3.1348 -
  3.1349 -lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
  3.1350 -  by (simp add: le_matrix_def, auto)
  3.1351 -
  3.1352 -lemma le_foldseq:
  3.1353 -  assumes
  3.1354 -  "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
  3.1355 -  "! i. i <= n \<longrightarrow> s i <= t i"
  3.1356 -  shows
  3.1357 -  "foldseq f s n <= foldseq f t n"
  3.1358 -proof -
  3.1359 -  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!)
  3.1360 -  then show "foldseq f s n <= foldseq f t n" by (simp!)
  3.1361 -qed
  3.1362 -
  3.1363 -lemma le_left_mult:
  3.1364 -  assumes
  3.1365 -  "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  3.1366 -  "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
  3.1367 -  "! a. fmul 0 a = 0"
  3.1368 -  "! a. fmul a 0 = 0"
  3.1369 -  "fadd 0 0 = 0"
  3.1370 -  "0 <= C"
  3.1371 -  "A <= B"
  3.1372 -  shows
  3.1373 -  "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
  3.1374 -  apply (simp! add: le_matrix_def Rep_mult_matrix)
  3.1375 -  apply (auto)
  3.1376 -  apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
  3.1377 -  apply (rule le_foldseq)
  3.1378 -  by (auto)
  3.1379 -
  3.1380 -lemma le_right_mult:
  3.1381 -  assumes
  3.1382 -  "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
  3.1383 -  "! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
  3.1384 -  "! a. fmul 0 a = 0"
  3.1385 -  "! a. fmul a 0 = 0"
  3.1386 -  "fadd 0 0 = 0"
  3.1387 -  "0 <= C"
  3.1388 -  "A <= B"
  3.1389 -  shows
  3.1390 -  "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
  3.1391 -  apply (simp! add: le_matrix_def Rep_mult_matrix)
  3.1392 -  apply (auto)
  3.1393 -  apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
  3.1394 -  apply (rule le_foldseq)
  3.1395 -  by (auto)
  3.1396 -
  3.1397 -lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
  3.1398 -lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
  3.1399 -
  3.1400 -lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"
  3.1401 -  by (auto simp add: le_matrix_def)
  3.1402 -
  3.1403 -lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"
  3.1404 -  apply (auto)
  3.1405 -  apply (simp add: le_matrix_def)
  3.1406 -  apply (drule_tac j=j and i=i in spec2)
  3.1407 -  apply (simp)
  3.1408 -  apply (simp add: le_matrix_def)
  3.1409 -  done
  3.1410 -
  3.1411 -lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
  3.1412 -  apply (auto)
  3.1413 -  apply (simp add: le_matrix_def)
  3.1414 -  apply (drule_tac j=j and i=i in spec2)
  3.1415 -  apply (simp)
  3.1416 -  apply (simp add: le_matrix_def)
  3.1417 -  done
  3.1418 -
  3.1419 -lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
  3.1420 -  apply (auto simp add: le_matrix_def neg_def)
  3.1421 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  3.1422 -  apply (auto)
  3.1423 -  done
  3.1424 -
  3.1425 -lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
  3.1426 -  apply (auto simp add: le_matrix_def neg_def)
  3.1427 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  3.1428 -  apply (auto)
  3.1429 -  done
  3.1430 -
  3.1431 -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))"
  3.1432 -  apply (auto simp add: le_matrix_def neg_def)
  3.1433 -  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
  3.1434 -  apply (auto)
  3.1435 -  done  
  3.1436 -
  3.1437 -end
     4.1 --- a/src/HOL/Matrix/ROOT.ML	Thu Jul 03 20:53:44 2008 +0200
     4.2 +++ b/src/HOL/Matrix/ROOT.ML	Fri Jul 04 07:39:01 2008 +0200
     4.3 @@ -3,4 +3,4 @@
     4.4  *)
     4.5  
     4.6  use_thy "SparseMatrix";
     4.7 -with_path "cplex" use_thy "MatrixLP";
     4.8 +with_path "cplex" use_thy "Cplex";
     5.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Thu Jul 03 20:53:44 2008 +0200
     5.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Jul 04 07:39:01 2008 +0200
     5.3 @@ -3,26 +3,30 @@
     5.4      Author:     Steven Obua
     5.5  *)
     5.6  
     5.7 -theory SparseMatrix imports Matrix LP begin
     5.8 +theory SparseMatrix
     5.9 +imports Matrix
    5.10 +begin
    5.11  
    5.12  types 
    5.13    'a spvec = "(nat * 'a) list"
    5.14    'a spmat = "('a spvec) spvec"
    5.15  
    5.16 -consts
    5.17 -  sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix"
    5.18 -  sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix"
    5.19 +definition sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix" where
    5.20 +  sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
    5.21  
    5.22 -defs
    5.23 -  sparse_row_vector_def : "sparse_row_vector arr == foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
    5.24 -  sparse_row_matrix_def : "sparse_row_matrix arr == foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
    5.25 +definition sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix" where
    5.26 +  sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
    5.27  
    5.28 -lemma sparse_row_vector_empty[simp]: "sparse_row_vector [] = 0"
    5.29 +code_datatype sparse_row_vector sparse_row_matrix
    5.30 +
    5.31 +lemma sparse_row_vector_empty [simp]: "sparse_row_vector [] = 0"
    5.32    by (simp add: sparse_row_vector_def)
    5.33  
    5.34 -lemma sparse_row_matrix_empty[simp]: "sparse_row_matrix [] = 0"
    5.35 +lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
    5.36    by (simp add: sparse_row_matrix_def)
    5.37  
    5.38 +lemmas [code func] = sparse_row_vector_empty [symmetric]
    5.39 +
    5.40  lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
    5.41    by (induct l, auto)
    5.42  
    5.43 @@ -99,18 +103,15 @@
    5.44    done
    5.45  
    5.46  consts
    5.47 -  abs_spvec :: "('a::lordered_ring) spvec \<Rightarrow> 'a spvec"
    5.48 -  minus_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec"
    5.49    smult_spvec :: "('a::lordered_ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" 
    5.50 -  addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
    5.51  
    5.52 -primrec 
    5.53 +primrec minus_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
    5.54    "minus_spvec [] = []"
    5.55 -  "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
    5.56 +  | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
    5.57  
    5.58 -primrec 
    5.59 +primrec abs_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
    5.60    "abs_spvec [] = []"
    5.61 -  "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
    5.62 +  | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
    5.63  
    5.64  lemma sparse_row_vector_minus: 
    5.65    "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
    5.66 @@ -160,6 +161,7 @@
    5.67  lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
    5.68    by (simp add: smult_spvec_def)
    5.69  
    5.70 +consts addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
    5.71  recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
    5.72    "addmult_spvec (y, arr, []) = arr"
    5.73    "addmult_spvec (y, [], brr) = smult_spvec y brr"
    5.74 @@ -169,10 +171,10 @@
    5.75      else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))"
    5.76  
    5.77  lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a"
    5.78 -  by (induct a, auto)
    5.79 +  by (induct a) auto
    5.80  
    5.81  lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a"
    5.82 -  by (induct a, auto)
    5.83 +  by (induct a) auto
    5.84  
    5.85  lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow> 
    5.86    sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)"
    5.87 @@ -243,7 +245,6 @@
    5.88  
    5.89  consts 
    5.90    mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat  \<Rightarrow> 'a spvec"
    5.91 -
    5.92  recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))"
    5.93    "mult_spvec_spmat (c, [], brr) = c"
    5.94    "mult_spvec_spmat (c, arr, []) = c"
    5.95 @@ -417,6 +418,9 @@
    5.96    apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
    5.97    done
    5.98  
    5.99 +lemmas [code func] = sparse_row_add_spmat [symmetric]
   5.100 +lemmas [code func] = sparse_row_vector_add [symmetric]
   5.101 +
   5.102  lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   5.103    proof - 
   5.104      have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
   5.105 @@ -1113,57 +1117,4 @@
   5.106    by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])
   5.107  *)
   5.108  
   5.109 -lemma spm_mult_le_dual_prts: 
   5.110 -  assumes
   5.111 -  "sorted_sparse_matrix A1"
   5.112 -  "sorted_sparse_matrix A2"
   5.113 -  "sorted_sparse_matrix c1"
   5.114 -  "sorted_sparse_matrix c2"
   5.115 -  "sorted_sparse_matrix y"
   5.116 -  "sorted_sparse_matrix r1"
   5.117 -  "sorted_sparse_matrix r2"
   5.118 -  "sorted_spvec b"
   5.119 -  "le_spmat ([], y)"
   5.120 -  "sparse_row_matrix A1 \<le> A"
   5.121 -  "A \<le> sparse_row_matrix A2"
   5.122 -  "sparse_row_matrix c1 \<le> c"
   5.123 -  "c \<le> sparse_row_matrix c2"
   5.124 -  "sparse_row_matrix r1 \<le> x"
   5.125 -  "x \<le> sparse_row_matrix r2"
   5.126 -  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
   5.127 -  shows
   5.128 -  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
   5.129 -  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
   5.130 -  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
   5.131 -  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
   5.132 -  apply (simp add: Let_def)
   5.133 -  apply (insert prems)
   5.134 -  apply (simp add: sparse_row_matrix_op_simps ring_simps)  
   5.135 -  apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
   5.136 -  apply (auto)
   5.137 -  done
   5.138 -
   5.139 -lemma spm_mult_le_dual_prts_no_let: 
   5.140 -  assumes
   5.141 -  "sorted_sparse_matrix A1"
   5.142 -  "sorted_sparse_matrix A2"
   5.143 -  "sorted_sparse_matrix c1"
   5.144 -  "sorted_sparse_matrix c2"
   5.145 -  "sorted_sparse_matrix y"
   5.146 -  "sorted_sparse_matrix r1"
   5.147 -  "sorted_sparse_matrix r2"
   5.148 -  "sorted_spvec b"
   5.149 -  "le_spmat ([], y)"
   5.150 -  "sparse_row_matrix A1 \<le> A"
   5.151 -  "A \<le> sparse_row_matrix A2"
   5.152 -  "sparse_row_matrix c1 \<le> c"
   5.153 -  "c \<le> sparse_row_matrix c2"
   5.154 -  "sparse_row_matrix r1 \<le> x"
   5.155 -  "x \<le> sparse_row_matrix r2"
   5.156 -  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
   5.157 -  shows
   5.158 -  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
   5.159 -  mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
   5.160 -  by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
   5.161 - 
   5.162  end
     6.1 --- a/src/HOL/Matrix/cplex/Cplex.thy	Thu Jul 03 20:53:44 2008 +0200
     6.2 +++ b/src/HOL/Matrix/cplex/Cplex.thy	Fri Jul 04 07:39:01 2008 +0200
     6.3 @@ -4,11 +4,63 @@
     6.4  *)
     6.5  
     6.6  theory Cplex 
     6.7 -imports FloatSparseMatrix "~~/src/HOL/Tools/ComputeNumeral"
     6.8 -uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
     6.9 +imports SparseMatrix LP "~~/src/HOL/Real/Float" "~~/src/HOL/Tools/ComputeNumeral"
    6.10 +uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" ("matrixlp.ML")
    6.11  begin
    6.12  
    6.13 -end
    6.14 +lemma spm_mult_le_dual_prts: 
    6.15 +  assumes
    6.16 +  "sorted_sparse_matrix A1"
    6.17 +  "sorted_sparse_matrix A2"
    6.18 +  "sorted_sparse_matrix c1"
    6.19 +  "sorted_sparse_matrix c2"
    6.20 +  "sorted_sparse_matrix y"
    6.21 +  "sorted_sparse_matrix r1"
    6.22 +  "sorted_sparse_matrix r2"
    6.23 +  "sorted_spvec b"
    6.24 +  "le_spmat ([], y)"
    6.25 +  "sparse_row_matrix A1 \<le> A"
    6.26 +  "A \<le> sparse_row_matrix A2"
    6.27 +  "sparse_row_matrix c1 \<le> c"
    6.28 +  "c \<le> sparse_row_matrix c2"
    6.29 +  "sparse_row_matrix r1 \<le> x"
    6.30 +  "x \<le> sparse_row_matrix r2"
    6.31 +  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
    6.32 +  shows
    6.33 +  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
    6.34 +  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
    6.35 +  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
    6.36 +  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
    6.37 +  apply (simp add: Let_def)
    6.38 +  apply (insert prems)
    6.39 +  apply (simp add: sparse_row_matrix_op_simps ring_simps)  
    6.40 +  apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_simps])
    6.41 +  apply (auto)
    6.42 +  done
    6.43  
    6.44 +lemma spm_mult_le_dual_prts_no_let: 
    6.45 +  assumes
    6.46 +  "sorted_sparse_matrix A1"
    6.47 +  "sorted_sparse_matrix A2"
    6.48 +  "sorted_sparse_matrix c1"
    6.49 +  "sorted_sparse_matrix c2"
    6.50 +  "sorted_sparse_matrix y"
    6.51 +  "sorted_sparse_matrix r1"
    6.52 +  "sorted_sparse_matrix r2"
    6.53 +  "sorted_spvec b"
    6.54 +  "le_spmat ([], y)"
    6.55 +  "sparse_row_matrix A1 \<le> A"
    6.56 +  "A \<le> sparse_row_matrix A2"
    6.57 +  "sparse_row_matrix c1 \<le> c"
    6.58 +  "c \<le> sparse_row_matrix c2"
    6.59 +  "sparse_row_matrix r1 \<le> x"
    6.60 +  "x \<le> sparse_row_matrix r2"
    6.61 +  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
    6.62 +  shows
    6.63 +  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
    6.64 +  mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
    6.65 +  by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
    6.66  
    6.67 +use "matrixlp.ML"
    6.68  
    6.69 +end
     7.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrix.thy	Thu Jul 03 20:53:44 2008 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,10 +0,0 @@
     7.4 -(*  Title:      HOL/Matrix/cplex/FloatSparseMatrix.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Steven Obua
     7.7 -*)
     7.8 -
     7.9 -theory FloatSparseMatrix
    7.10 -imports "../../Real/Float" SparseMatrix
    7.11 -begin
    7.12 -
    7.13 -end
     8.1 --- a/src/HOL/Matrix/cplex/MatrixLP.thy	Thu Jul 03 20:53:44 2008 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,10 +0,0 @@
     8.4 -(*  Title:      HOL/Matrix/cplex/MatrixLP.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Steven Obua
     8.7 -*)
     8.8 -
     8.9 -theory MatrixLP 
    8.10 -imports Cplex 
    8.11 -uses "matrixlp.ML"
    8.12 -begin
    8.13 -end
     9.1 --- a/src/HOL/Matrix/cplex/matrixlp.ML	Thu Jul 03 20:53:44 2008 +0200
     9.2 +++ b/src/HOL/Matrix/cplex/matrixlp.ML	Fri Jul 04 07:39:01 2008 +0200
     9.3 @@ -25,13 +25,13 @@
     9.4  
     9.5  local
     9.6  
     9.7 -val cert =  cterm_of @{theory "Cplex"}
     9.8 +val cert =  cterm_of @{theory}
     9.9  
    9.10  in
    9.11  
    9.12  fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) =
    9.13    let
    9.14 -    val th = inst_real @{thm "SparseMatrix.spm_mult_le_dual_prts_no_let"}
    9.15 +    val th = inst_real @{thm "spm_mult_le_dual_prts_no_let"}
    9.16      fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x)
    9.17      val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2,
    9.18                                     var "r1" r1, var "r2" r2, var "b" b]) th
    9.19 @@ -67,20 +67,12 @@
    9.20    | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
    9.21  
    9.22  local
    9.23 -    val matrix_lemmas = [
    9.24 -	"ComputeHOL.compute_list_case",
    9.25 -	"ComputeHOL.compute_let",
    9.26 -        "ComputeHOL.compute_if",
    9.27 -        "Float.arith",
    9.28 -        "SparseMatrix.sparse_row_matrix_arith_simps",
    9.29 -        "ComputeHOL.compute_bool",
    9.30 -        "ComputeHOL.compute_pair", 
    9.31 -	"SparseMatrix.sorted_sp_simps",
    9.32 -        "ComputeNumeral.number_norm",
    9.33 -	"ComputeNumeral.natnorm"]
    9.34 -    fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} n)
    9.35 -    val ths = maps get_thms matrix_lemmas
    9.36 -    val computer = PCompute.make Compute.SML @{theory "Cplex"} ths []
    9.37 +    val ths = ComputeHOL.prep_thms @{thms "ComputeHOL.compute_list_case" "ComputeHOL.compute_let"
    9.38 +      "ComputeHOL.compute_if" "Float.arith" "SparseMatrix.sparse_row_matrix_arith_simps"
    9.39 +      "ComputeHOL.compute_bool" "ComputeHOL.compute_pair"
    9.40 +      "SparseMatrix.sorted_sp_simps" "ComputeNumeral.number_norm"
    9.41 +      "ComputeNumeral.natnorm"};
    9.42 +    val computer = PCompute.make Compute.SML @{theory} ths []
    9.43  in
    9.44  
    9.45  fun matrix_compute c = hd (PCompute.rewrite computer [c])
    9.46 @@ -98,7 +90,7 @@
    9.47  
    9.48  fun prove_bound lptfile prec =
    9.49      let
    9.50 -        val th = lp_dual_estimate_prt lptfile prec
    9.51 +        val th = lp_dual_estimate_llprt lptfile prec
    9.52      in
    9.53          matrix_simplify th
    9.54      end