src/HOL/Matrix/Matrix.thy
 author wenzelm Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) changeset 41229 d797baa3d57c parent 39302 d7728f65b353 child 41413 64cd30d6b0b8 permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (*  Title:      HOL/Matrix/Matrix.thy

     2     Author:     Steven Obua

     3 *)

     4

     5 theory Matrix

     6 imports Main Lattice_Algebras

     7 begin

     8

     9 types 'a infmatrix = "nat \<Rightarrow> nat \<Rightarrow> 'a"

    10

    11 definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where

    12   "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"

    13

    14 typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"

    15 proof -

    16   have "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"

    17     by (simp add: nonzero_positions_def)

    18   then show ?thesis by auto

    19 qed

    20

    21 declare Rep_matrix_inverse[simp]

    22

    23 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"

    24 apply (rule Abs_matrix_induct)

    25 by (simp add: Abs_matrix_inverse matrix_def)

    26

    27 definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where

    28   "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"

    29

    30 definition ncols :: "('a::zero) matrix \<Rightarrow> nat" where

    31   "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"

    32

    33 lemma nrows:

    34   assumes hyp: "nrows A \<le> m"

    35   shows "(Rep_matrix A m n) = 0"

    36 proof cases

    37   assume "nonzero_positions(Rep_matrix A) = {}"

    38   then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)

    39 next

    40   assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"

    41   let ?S = "fst(nonzero_positions(Rep_matrix A))"

    42   have c: "finite (?S)" by (simp add: finite_nonzero_positions)

    43   from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)

    44   have "m \<notin> ?S"

    45     proof -

    46       have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])

    47       moreover from d have "~(m <= Max ?S)" by (simp)

    48       ultimately show "m \<notin> ?S" by (auto)

    49     qed

    50   thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)

    51 qed

    52

    53 definition transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix" where

    54   "transpose_infmatrix A j i == A i j"

    55

    56 definition transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix" where

    57   "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"

    58

    59 declare transpose_infmatrix_def[simp]

    60

    61 lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"

    62 by ((rule ext)+, simp)

    63

    64 lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"

    65   apply (rule ext)+

    66   by (simp add: transpose_infmatrix_def)

    67

    68 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"

    69 apply (rule Abs_matrix_inverse)

    70 apply (simp add: matrix_def nonzero_positions_def image_def)

    71 proof -

    72   let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"

    73   let ?swap = "% pos. (snd pos, fst pos)"

    74   let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"

    75   have swap_image: "?swap?A = ?B"

    76     apply (simp add: image_def)

    77     apply (rule set_eqI)

    78     apply (simp)

    79     proof

    80       fix y

    81       assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"

    82       thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"

    83         proof -

    84           from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast

    85           then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)

    86         qed

    87     next

    88       fix y

    89       assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"

    90       show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"

    91         by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)

    92     qed

    93   then have "finite (?swap?A)"

    94     proof -

    95       have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)

    96       then have "finite ?B" by (simp add: nonzero_positions_def)

    97       with swap_image show "finite (?swap?A)" by (simp)

    98     qed

    99   moreover

   100   have "inj_on ?swap ?A" by (simp add: inj_on_def)

   101   ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])

   102 qed

   103

   104 lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto

   105

   106 lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"

   107 apply (auto)

   108 apply (rule ext)+

   109 apply (simp add: transpose_infmatrix)

   110 apply (drule infmatrixforward)

   111 apply (simp)

   112 done

   113

   114 lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"

   115 apply (simp add: transpose_matrix_def)

   116 apply (subst Rep_matrix_inject[THEN sym])+

   117 apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)

   118 done

   119

   120 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"

   121 by (simp add: transpose_matrix_def)

   122

   123 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"

   124 by (simp add: transpose_matrix_def)

   125

   126 lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"

   127 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)

   128

   129 lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"

   130 by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)

   131

   132 lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"

   133 proof -

   134   assume "ncols A <= n"

   135   then have "nrows (transpose_matrix A) <= n" by (simp)

   136   then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)

   137   thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)

   138 qed

   139

   140 lemma ncols_le: "(ncols A <= n) = (! j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")

   141 apply (auto)

   142 apply (simp add: ncols)

   143 proof (simp add: ncols_def, auto)

   144   let ?P = "nonzero_positions (Rep_matrix A)"

   145   let ?p = "snd?P"

   146   have a:"finite ?p" by (simp add: finite_nonzero_positions)

   147   let ?m = "Max ?p"

   148   assume "~(Suc (?m) <= n)"

   149   then have b:"n <= ?m" by (simp)

   150   fix a b

   151   assume "(a,b) \<in> ?P"

   152   then have "?p \<noteq> {}" by (auto)

   153   with a have "?m \<in>  ?p" by (simp)

   154   moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)

   155   ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)

   156   moreover assume ?st

   157   ultimately show "False" using b by (simp)

   158 qed

   159

   160 lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)"

   161 proof -

   162   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith

   163   show ?thesis by (simp add: a ncols_le)

   164 qed

   165

   166 lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"

   167 apply (auto)

   168 apply (subgoal_tac "ncols A <= m")

   169 apply (simp)

   170 apply (simp add: ncols_le)

   171 apply (drule_tac x="ncols A" in spec)

   172 by (simp add: ncols)

   173

   174 lemma nrows_le: "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)

   175 proof -

   176   have "(nrows A <= n) = (ncols (transpose_matrix A) <= n)" by (simp)

   177   also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)

   178   also have "\<dots> = (! j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)

   179   finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)

   180 qed

   181

   182 lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)"

   183 proof -

   184   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith

   185   show ?thesis by (simp add: a nrows_le)

   186 qed

   187

   188 lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"

   189 apply (auto)

   190 apply (subgoal_tac "nrows A <= m")

   191 apply (simp)

   192 apply (simp add: nrows_le)

   193 apply (drule_tac x="nrows A" in spec)

   194 by (simp add: nrows)

   195

   196 lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"

   197 apply (case_tac "nrows A <= m")

   198 apply (simp_all add: nrows)

   199 done

   200

   201 lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"

   202 apply (case_tac "ncols A <= n")

   203 apply (simp_all add: ncols)

   204 done

   205

   206 lemma finite_natarray1: "finite {x. x < (n::nat)}"

   207 apply (induct n)

   208 apply (simp)

   209 proof -

   210   fix n

   211   have "{x. x < Suc n} = insert n {x. x < n}"  by (rule set_eqI, simp, arith)

   212   moreover assume "finite {x. x < n}"

   213   ultimately show "finite {x. x < Suc n}" by (simp)

   214 qed

   215

   216 lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"

   217   apply (induct m)

   218   apply (simp+)

   219   proof -

   220     fix m::nat

   221     let ?s0 = "{pos. fst pos < m & snd pos < n}"

   222     let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"

   223     let ?sd = "{pos. fst pos = m & snd pos < n}"

   224     assume f0: "finite ?s0"

   225     have f1: "finite ?sd"

   226     proof -

   227       let ?f = "% x. (m, x)"

   228       have "{pos. fst pos = m & snd pos < n} = ?f  {x. x < n}" by (rule set_eqI, simp add: image_def, auto)

   229       moreover have "finite {x. x < n}" by (simp add: finite_natarray1)

   230       ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)

   231     qed

   232     have su: "?s0 \<union> ?sd = ?s1" by (rule set_eqI, simp, arith)

   233     from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)

   234     with su show "finite ?s1" by (simp)

   235 qed

   236

   237 lemma RepAbs_matrix:

   238   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)

   239   shows "(Rep_matrix (Abs_matrix x)) = x"

   240 apply (rule Abs_matrix_inverse)

   241 apply (simp add: matrix_def nonzero_positions_def)

   242 proof -

   243   from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)

   244   from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)

   245   let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"

   246   let ?v = "{pos. fst pos < m & snd pos < n}"

   247   have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)

   248   from a b have "(?u \<inter> (-?v)) = {}"

   249     apply (simp)

   250     apply (rule set_eqI)

   251     apply (simp)

   252     apply auto

   253     by (rule c, auto)+

   254   then have d: "?u \<subseteq> ?v" by blast

   255   moreover have "finite ?v" by (simp add: finite_natarray2)

   256   ultimately show "finite ?u" by (rule finite_subset)

   257 qed

   258

   259 definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where

   260   "apply_infmatrix f == % A. (% j i. f (A j i))"

   261

   262 definition apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix" where

   263   "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"

   264

   265 definition combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix" where

   266   "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"

   267

   268 definition combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix" where

   269   "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"

   270

   271 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"

   272 by (simp add: apply_infmatrix_def)

   273

   274 lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"

   275 by (simp add: combine_infmatrix_def)

   276

   277 definition commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" where

   278 "commutative f == ! x y. f x y = f y x"

   279

   280 definition associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where

   281 "associative f == ! x y z. f (f x y) z = f x (f y z)"

   282

   283 text{*

   284 To reason about associativity and commutativity of operations on matrices,

   285 let's take a step back and look at the general situtation: Assume that we have

   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.

   287 Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.

   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.$

   289 *}

   290

   291 lemma combine_infmatrix_commute:

   292   "commutative f \<Longrightarrow> commutative (combine_infmatrix f)"

   293 by (simp add: commutative_def combine_infmatrix_def)

   294

   295 lemma combine_matrix_commute:

   296 "commutative f \<Longrightarrow> commutative (combine_matrix f)"

   297 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)

   298

   299 text{*

   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\}$,

   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

   302 $f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1,$

   303 but on the other hand we have

   304 $f' 1 (f' 1 -1) = u (f 1 (u (f 1 -1))) = u (f 1 0) = 1.$

   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:

   306 *}

   307

   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)"

   309 by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)

   310

   311 lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"

   312 by (insert Rep_matrix [of A], simp add: matrix_def)

   313

   314 lemma combine_infmatrix_closed [simp]:

   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)"

   316 apply (rule Abs_matrix_inverse)

   317 apply (simp add: matrix_def)

   318 apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])

   319 by (simp_all)

   320

   321 text {* We need the next two lemmas only later, but it is analog to the above one, so we prove them now: *}

   322 lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"

   323 by (rule subsetI, simp add: nonzero_positions_def apply_infmatrix_def, auto)

   324

   325 lemma apply_infmatrix_closed [simp]:

   326   "f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"

   327 apply (rule Abs_matrix_inverse)

   328 apply (simp add: matrix_def)

   329 apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])

   330 by (simp_all)

   331

   332 lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"

   333 by (simp add: associative_def combine_infmatrix_def)

   334

   335 lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"

   336 by (auto)

   337

   338 lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"

   339 apply (simp(no_asm) add: associative_def combine_matrix_def, auto)

   340 apply (rule comb [of Abs_matrix Abs_matrix])

   341 by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)

   342

   343 lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"

   344 by (simp add: apply_matrix_def)

   345

   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)"

   347   by(simp add: combine_matrix_def)

   348

   349 lemma combine_nrows_max: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"

   350 by (simp add: nrows_le)

   351

   352 lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"

   353 by (simp add: ncols_le)

   354

   355 lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"

   356   by (simp add: nrows_le)

   357

   358 lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"

   359   by (simp add: ncols_le)

   360

   361 definition zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool" where

   362   "zero_r_neutral f == ! a. f a 0 = a"

   363

   364 definition zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where

   365   "zero_l_neutral f == ! a. f 0 a = a"

   366

   367 definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where

   368   "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"

   369

   370 primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"

   371 where

   372   "foldseq f s 0 = s 0"

   373 | "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"

   374

   375 primrec foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"

   376 where

   377   "foldseq_transposed f s 0 = s 0"

   378 | "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"

   379

   380 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"

   381 proof -

   382   assume a:"associative f"

   383   then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"

   384   proof -

   385     fix n

   386     show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"

   387     proof (induct n)

   388       show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp

   389     next

   390       fix n

   391       assume b:"! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"

   392       have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)

   393       show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"

   394       proof (auto)

   395         fix N t

   396         assume Nsuc: "N <= Suc n"

   397         show "foldseq f t N = foldseq_transposed f t N"

   398         proof cases

   399           assume "N <= n"

   400           then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)

   401         next

   402           assume "~(N <= n)"

   403           with Nsuc have Nsuceq: "N = Suc n" by simp

   404           have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith

   405           have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)

   406           show "foldseq f t N = foldseq_transposed f t N"

   407             apply (simp add: Nsuceq)

   408             apply (subst c)

   409             apply (simp)

   410             apply (case_tac "n = 0")

   411             apply (simp)

   412             apply (drule neqz)

   413             apply (erule exE)

   414             apply (simp)

   415             apply (subst assocf)

   416             proof -

   417               fix m

   418               assume "n = Suc m & Suc m <= n"

   419               then have mless: "Suc m <= n" by arith

   420               then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")

   421                 apply (subst c)

   422                 by simp+

   423               have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp

   424               have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")

   425                 apply (subst c)

   426                 by (simp add: mless)+

   427               have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp

   428               from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp

   429             qed

   430           qed

   431         qed

   432       qed

   433     qed

   434     show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)

   435   qed

   436

   437 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)"

   438 proof -

   439   assume assoc: "associative f"

   440   assume comm: "commutative f"

   441   from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)

   442   from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)

   443   from assoc comm have c: "!! x y z. f x (f y z) = f y (f x z)" by (simp add: commutative_def associative_def)

   444   have "!! n. (! u v. foldseq f (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"

   445     apply (induct_tac n)

   446     apply (simp+, auto)

   447     by (simp add: a b c)

   448   then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp

   449 qed

   450

   451 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)"

   452 oops

   453 (* Model found

   454

   455 Trying to find a model that refutes: \<lbrakk>associative f; associative g;

   456  \<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;

   457  \<exists>x y. g x \<noteq> g y; f x x = x; g x x = x\<rbrakk>

   458 \<Longrightarrow> f = g \<or> (\<forall>y. f y x = y) \<or> (\<forall>y. g y x = y)

   459 Searching for a model of size 1, translating term... invoking SAT solver... no model found.

   460 Searching for a model of size 2, translating term... invoking SAT solver... no model found.

   461 Searching for a model of size 3, translating term... invoking SAT solver...

   462 Model found:

   463 Size of types: 'a: 3

   464 x: a1

   465 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))

   466 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))

   467 *)

   468

   469 lemma foldseq_zero:

   470 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"

   471 shows "foldseq f s n = 0"

   472 proof -

   473   have "!! n. ! s. (! i. i <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"

   474     apply (induct_tac n)

   475     apply (simp)

   476     by (simp add: fz)

   477   then show "foldseq f s n = 0" by (simp add: sz)

   478 qed

   479

   480 lemma foldseq_significant_positions:

   481   assumes p: "! i. i <= N \<longrightarrow> S i = T i"

   482   shows "foldseq f S N = foldseq f T N"

   483 proof -

   484   have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"

   485     apply (induct_tac m)

   486     apply (simp)

   487     apply (simp)

   488     apply (auto)

   489     proof -

   490       fix n

   491       fix s::"nat\<Rightarrow>'a"

   492       fix t::"nat\<Rightarrow>'a"

   493       assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"

   494       assume b: "\<forall>i\<le>Suc n. s i = t i"

   495       have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast

   496       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)

   497       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)

   498     qed

   499   with p show ?thesis by simp

   500 qed

   501

   502 lemma foldseq_tail:

   503   assumes "M <= N"

   504   shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M"

   505 proof -

   506   have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith

   507   have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast

   508   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"

   509     apply (induct_tac n)

   510     apply (simp)

   511     apply (simp)

   512     apply (auto)

   513     apply (case_tac "m = Suc na")

   514     apply (simp)

   515     apply (rule a)

   516     apply (rule foldseq_significant_positions)

   517     apply (auto)

   518     apply (drule suc, simp+)

   519     proof -

   520       fix na m s

   521       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"

   522       assume subb:"m <= na"

   523       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

   524       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 =

   525         foldseq f (% k. s(Suc k)) na"

   526         by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)

   527       from subb have sube: "m \<noteq> 0 \<Longrightarrow> ? mm. m = Suc mm & mm <= na" by arith

   528       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) =

   529         foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"

   530         apply (simp add: subd)

   531         apply (cases "m = 0")

   532         apply (simp)

   533         apply (drule sube)

   534         apply (auto)

   535         apply (rule a)

   536         by (simp add: subc cong del: if_cong)

   537     qed

   538   then show ?thesis using assms by simp

   539 qed

   540

   541 lemma foldseq_zerotail:

   542   assumes

   543   fz: "f 0 0 = 0"

   544   and sz: "! i.  n <= i \<longrightarrow> s i = 0"

   545   and nm: "n <= m"

   546   shows

   547   "foldseq f s n = foldseq f s m"

   548 proof -

   549   show "foldseq f s n = foldseq f s m"

   550     apply (simp add: foldseq_tail[OF nm, of f s])

   551     apply (rule foldseq_significant_positions)

   552     apply (auto)

   553     apply (subst foldseq_zero)

   554     by (simp add: fz sz)+

   555 qed

   556

   557 lemma foldseq_zerotail2:

   558   assumes "! x. f x 0 = x"

   559   and "! i. n < i \<longrightarrow> s i = 0"

   560   and nm: "n <= m"

   561   shows "foldseq f s n = foldseq f s m"

   562 proof -

   563   have "f 0 0 = 0" by (simp add: assms)

   564   have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith

   565   have c: "0 <= m" by simp

   566   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith

   567   show ?thesis

   568     apply (subst foldseq_tail[OF nm])

   569     apply (rule foldseq_significant_positions)

   570     apply (auto)

   571     apply (case_tac "m=n")

   572     apply (simp+)

   573     apply (drule b[OF nm])

   574     apply (auto)

   575     apply (case_tac "k=0")

   576     apply (simp add: assms)

   577     apply (drule d)

   578     apply (auto)

   579     apply (simp add: assms foldseq_zero)

   580     done

   581 qed

   582

   583 lemma foldseq_zerostart:

   584   "! 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))"

   585 proof -

   586   assume f00x: "! x. f 0 (f 0 x) = f 0 x"

   587   have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"

   588     apply (induct n)

   589     apply (simp)

   590     apply (rule allI, rule impI)

   591     proof -

   592       fix n

   593       fix s

   594       have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp

   595       assume b: "! s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"

   596       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

   597       assume d: "! i. i <= Suc n \<longrightarrow> s i = 0"

   598       show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"

   599         apply (subst a)

   600         apply (subst c)

   601         by (simp add: d f00x)+

   602     qed

   603   then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp

   604 qed

   605

   606 lemma foldseq_zerostart2:

   607   "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"

   608 proof -

   609   assume a:"! i. i<n \<longrightarrow> s i = 0"

   610   assume x:"! x. f 0 x = x"

   611   from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast

   612   have b: "!! i l. i < Suc l = (i <= l)" by arith

   613   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith

   614   show "foldseq f s n = s n"

   615   apply (case_tac "n=0")

   616   apply (simp)

   617   apply (insert a)

   618   apply (drule d)

   619   apply (auto)

   620   apply (simp add: b)

   621   apply (insert f00x)

   622   apply (drule foldseq_zerostart)

   623   by (simp add: x)+

   624 qed

   625

   626 lemma foldseq_almostzero:

   627   assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"

   628   shows "foldseq f s n = (if (j <= n) then (s j) else 0)"

   629 proof -

   630   from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp

   631   from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp

   632   show ?thesis

   633     apply auto

   634     apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])

   635     apply simp

   636     apply (subst foldseq_zerostart2)

   637     apply (simp add: f0x a)+

   638     apply (subst foldseq_zero)

   639     by (simp add: s0 f0x)+

   640 qed

   641

   642 lemma foldseq_distr_unary:

   643   assumes "!! a b. g (f a b) = f (g a) (g b)"

   644   shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n"

   645 proof -

   646   have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"

   647     apply (induct_tac n)

   648     apply (simp)

   649     apply (simp)

   650     apply (auto)

   651     apply (drule_tac x="% k. s (Suc k)" in spec)

   652     by (simp add: assms)

   653   then show ?thesis by simp

   654 qed

   655

   656 definition 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" where

   657   "mult_matrix_n n fmul fadd A B == Abs_matrix(% j i. foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n)"

   658

   659 definition 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" where

   660   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"

   661

   662 lemma mult_matrix_n:

   663   assumes "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"

   664   shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B"

   665 proof -

   666   show ?thesis using assms

   667     apply (simp add: mult_matrix_def mult_matrix_n_def)

   668     apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)

   669     apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms)

   670     done

   671 qed

   672

   673 lemma mult_matrix_nm:

   674   assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"

   675   shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"

   676 proof -

   677   from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B"

   678     by (simp add: mult_matrix_n)

   679   also from assms have "\<dots> = mult_matrix_n m fmul fadd A B"

   680     by (simp add: mult_matrix_n[THEN sym])

   681   finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp

   682 qed

   683

   684 definition r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where

   685   "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"

   686

   687 definition l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where

   688   "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"

   689

   690 definition distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where

   691   "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"

   692

   693 lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)

   694 lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)

   695

   696 lemma r_distributive_matrix:

   697  assumes

   698   "r_distributive fmul fadd"

   699   "associative fadd"

   700   "commutative fadd"

   701   "fadd 0 0 = 0"

   702   "! a. fmul a 0 = 0"

   703   "! a. fmul 0 a = 0"

   704  shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"

   705 proof -

   706   from assms show ?thesis

   707     apply (simp add: r_distributive_def mult_matrix_def, auto)

   708     proof -

   709       fix a::"'a matrix"

   710       fix u::"'b matrix"

   711       fix v::"'b matrix"

   712       let ?mx = "max (ncols a) (max (nrows u) (nrows v))"

   713       from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =

   714         combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"

   715         apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])

   716         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   717         apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])

   718         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   719         apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])

   720         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   721         apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])

   722         apply (simp add: combine_matrix_def combine_infmatrix_def)

   723         apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)

   724         apply (simplesubst RepAbs_matrix)

   725         apply (simp, auto)

   726         apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)

   727         apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)

   728         apply (subst RepAbs_matrix)

   729         apply (simp, auto)

   730         apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)

   731         apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)

   732         done

   733     qed

   734 qed

   735

   736 lemma l_distributive_matrix:

   737  assumes

   738   "l_distributive fmul fadd"

   739   "associative fadd"

   740   "commutative fadd"

   741   "fadd 0 0 = 0"

   742   "! a. fmul a 0 = 0"

   743   "! a. fmul 0 a = 0"

   744  shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"

   745 proof -

   746   from assms show ?thesis

   747     apply (simp add: l_distributive_def mult_matrix_def, auto)

   748     proof -

   749       fix a::"'b matrix"

   750       fix u::"'a matrix"

   751       fix v::"'a matrix"

   752       let ?mx = "max (nrows a) (max (ncols u) (ncols v))"

   753       from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =

   754                combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"

   755         apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])

   756         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   757         apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])

   758         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   759         apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])

   760         apply (simp add: max1 max2 combine_nrows combine_ncols)+

   761         apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])

   762         apply (simp add: combine_matrix_def combine_infmatrix_def)

   763         apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)

   764         apply (simplesubst RepAbs_matrix)

   765         apply (simp, auto)

   766         apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)

   767         apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)

   768         apply (subst RepAbs_matrix)

   769         apply (simp, auto)

   770         apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)

   771         apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)

   772         done

   773     qed

   774 qed

   775

   776 instantiation matrix :: (zero) zero

   777 begin

   778

   779 definition zero_matrix_def: "0 = Abs_matrix (\<lambda>j i. 0)"

   780

   781 instance ..

   782

   783 end

   784

   785 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"

   786   apply (simp add: zero_matrix_def)

   787   apply (subst RepAbs_matrix)

   788   by (auto)

   789

   790 lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"

   791 proof -

   792   have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)

   793   show "nrows 0 = 0" by (rule a, subst nrows_le, simp)

   794 qed

   795

   796 lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"

   797 proof -

   798   have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)

   799   show "ncols 0 = 0" by (rule a, subst ncols_le, simp)

   800 qed

   801

   802 lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"

   803   by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)

   804

   805 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"

   806   by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)

   807

   808 lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"

   809   apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)

   810   apply (auto)

   811   by (subst foldseq_zero, (simp add: zero_matrix_def)+)+

   812

   813 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"

   814   apply (simp add: mult_matrix_n_def)

   815   apply (subst foldseq_zero)

   816   by (simp_all add: zero_matrix_def)

   817

   818 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"

   819   apply (simp add: mult_matrix_n_def)

   820   apply (subst foldseq_zero)

   821   by (simp_all add: zero_matrix_def)

   822

   823 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"

   824 by (simp add: mult_matrix_def)

   825

   826 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"

   827 by (simp add: mult_matrix_def)

   828

   829 lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"

   830   apply (simp add: apply_matrix_def apply_infmatrix_def)

   831   by (simp add: zero_matrix_def)

   832

   833 lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"

   834   apply (simp add: combine_matrix_def combine_infmatrix_def)

   835   by (simp add: zero_matrix_def)

   836

   837 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"

   838 apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)

   839 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)

   840 apply (simp add: RepAbs_matrix)

   841 done

   842

   843 lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"

   844   apply (simp add: apply_matrix_def apply_infmatrix_def)

   845   by (simp add: zero_matrix_def)

   846

   847 definition singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix" where

   848   "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"

   849

   850 definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where

   851   "move_matrix A y x == Abs_matrix(% j i. if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"

   852

   853 definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where

   854   "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"

   855

   856 definition take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where

   857   "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"

   858

   859 definition column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where

   860   "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"

   861

   862 definition row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where

   863   "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"

   864

   865 lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"

   866 apply (simp add: singleton_matrix_def)

   867 apply (auto)

   868 apply (subst RepAbs_matrix)

   869 apply (rule exI[of _ "Suc m"], simp)

   870 apply (rule exI[of _ "Suc n"], simp+)

   871 by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+

   872

   873 lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"

   874 apply (subst Rep_matrix_inject[symmetric])

   875 apply (rule ext)+

   876 apply (simp)

   877 done

   878

   879 lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"

   880   by (simp add: singleton_matrix_def zero_matrix_def)

   881

   882 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"

   883 proof-

   884 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+

   885 from th show ?thesis

   886 apply (auto)

   887 apply (rule le_antisym)

   888 apply (subst nrows_le)

   889 apply (simp add: singleton_matrix_def, auto)

   890 apply (subst RepAbs_matrix)

   891 apply auto

   892 apply (simp add: Suc_le_eq)

   893 apply (rule not_leE)

   894 apply (subst nrows_le)

   895 by simp

   896 qed

   897

   898 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"

   899 proof-

   900 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+

   901 from th show ?thesis

   902 apply (auto)

   903 apply (rule le_antisym)

   904 apply (subst ncols_le)

   905 apply (simp add: singleton_matrix_def, auto)

   906 apply (subst RepAbs_matrix)

   907 apply auto

   908 apply (simp add: Suc_le_eq)

   909 apply (rule not_leE)

   910 apply (subst ncols_le)

   911 by simp

   912 qed

   913

   914 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)"

   915 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)

   916 apply (subst RepAbs_matrix)

   917 apply (rule exI[of _ "Suc j"], simp)

   918 apply (rule exI[of _ "Suc i"], simp)

   919 apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)

   920 apply (subst RepAbs_matrix)

   921 apply (rule exI[of _ "Suc j"], simp)

   922 apply (rule exI[of _ "Suc i"], simp)

   923 by simp

   924

   925 lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"

   926 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)

   927 apply (simp)

   928 done

   929

   930 lemma Rep_move_matrix[simp]:

   931   "Rep_matrix (move_matrix A y x) j i =

   932   (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"

   933 apply (simp add: move_matrix_def)

   934 apply (auto)

   935 by (subst RepAbs_matrix,

   936   rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,

   937   rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+

   938

   939 lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"

   940 by (simp add: move_matrix_def)

   941

   942 lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"

   943 apply (subst Rep_matrix_inject[symmetric])

   944 apply (rule ext)+

   945 apply (simp)

   946 done

   947

   948 lemma transpose_move_matrix[simp]:

   949   "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"

   950 apply (subst Rep_matrix_inject[symmetric], (rule ext)+)

   951 apply (simp)

   952 done

   953

   954 lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i =

   955   (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"

   956   apply (subst Rep_matrix_inject[symmetric])

   957   apply (rule ext)+

   958   apply (case_tac "j + int u < 0")

   959   apply (simp, arith)

   960   apply (case_tac "i + int v < 0")

   961   apply (simp add: neg_def, arith)

   962   apply (simp add: neg_def)

   963   apply arith

   964   done

   965

   966 lemma Rep_take_columns[simp]:

   967   "Rep_matrix (take_columns A c) j i =

   968   (if i < c then (Rep_matrix A j i) else 0)"

   969 apply (simp add: take_columns_def)

   970 apply (simplesubst RepAbs_matrix)

   971 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)

   972 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)

   973 done

   974

   975 lemma Rep_take_rows[simp]:

   976   "Rep_matrix (take_rows A r) j i =

   977   (if j < r then (Rep_matrix A j i) else 0)"

   978 apply (simp add: take_rows_def)

   979 apply (simplesubst RepAbs_matrix)

   980 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)

   981 apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)

   982 done

   983

   984 lemma Rep_column_of_matrix[simp]:

   985   "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"

   986   by (simp add: column_of_matrix_def)

   987

   988 lemma Rep_row_of_matrix[simp]:

   989   "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"

   990   by (simp add: row_of_matrix_def)

   991

   992 lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"

   993 apply (subst Rep_matrix_inject[THEN sym])

   994 apply (rule ext)+

   995 by (simp add: ncols)

   996

   997 lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"

   998 apply (subst Rep_matrix_inject[THEN sym])

   999 apply (rule ext)+

  1000 by (simp add: nrows)

  1001

  1002 lemma mult_matrix_singleton_right[simp]:

  1003   assumes

  1004   "! x. fmul x 0 = 0"

  1005   "! x. fmul 0 x = 0"

  1006   "! x. fadd 0 x = x"

  1007   "! x. fadd x 0 = x"

  1008   shows "(mult_matrix fmul fadd A (singleton_matrix j i e)) = apply_matrix (% x. fmul x e) (move_matrix (column_of_matrix A j) 0 (int i))"

  1009   apply (simp add: mult_matrix_def)

  1010   apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])

  1011   apply (auto)

  1012   apply (simp add: assms)+

  1013   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)

  1014   apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)

  1015   apply (subst foldseq_almostzero[of _ j])

  1016   apply (simp add: assms)+

  1017   apply (auto)

  1018   apply (metis add_0 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)

  1019   done

  1020

  1021 lemma mult_matrix_ext:

  1022   assumes

  1023   eprem:

  1024   "? e. (! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)"

  1025   and fprems:

  1026   "! a. fmul 0 a = 0"

  1027   "! a. fmul a 0 = 0"

  1028   "! a. fadd a 0 = a"

  1029   "! a. fadd 0 a = a"

  1030   and contraprems:

  1031   "mult_matrix fmul fadd A = mult_matrix fmul fadd B"

  1032   shows

  1033   "A = B"

  1034 proof(rule contrapos_np[of "False"], simp)

  1035   assume a: "A \<noteq> B"

  1036   have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)

  1037   have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"

  1038     apply (rule contrapos_np[of "False"], simp+)

  1039     apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)

  1040     by (simp add: Rep_matrix_inject a)

  1041   then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast

  1042   from eprem obtain e where eprops:"(! a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast

  1043   let ?S = "singleton_matrix I 0 e"

  1044   let ?comp = "mult_matrix fmul fadd"

  1045   have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast

  1046   have e: "(% x. fmul x e) 0 = 0" by (simp add: assms)

  1047   have "~(?comp A ?S = ?comp B ?S)"

  1048     apply (rule notI)

  1049     apply (simp add: fprems eprops)

  1050     apply (simp add: Rep_matrix_inject[THEN sym])

  1051     apply (drule d[of _ _ "J"], drule d[of _ _ "0"])

  1052     by (simp add: e c eprops)

  1053   with contraprems show "False" by simp

  1054 qed

  1055

  1056 definition foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where

  1057   "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"

  1058

  1059 definition foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where

  1060   "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"

  1061

  1062 lemma foldmatrix_transpose:

  1063   assumes

  1064   "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"

  1065   shows

  1066   "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"

  1067 proof -

  1068   have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto

  1069   have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"

  1070     apply (induct n)

  1071     apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+

  1072     apply (auto)

  1073     by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)

  1074   show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"

  1075     apply (simp add: foldmatrix_def foldmatrix_transposed_def)

  1076     apply (induct m, simp)

  1077     apply (simp)

  1078     apply (insert tworows)

  1079     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)

  1080     by (simp add: foldmatrix_def foldmatrix_transposed_def)

  1081 qed

  1082

  1083 lemma foldseq_foldseq:

  1084 assumes

  1085   "associative f"

  1086   "associative g"

  1087   "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"

  1088 shows

  1089   "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"

  1090   apply (insert foldmatrix_transpose[of g f A m n])

  1091   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)

  1092

  1093 lemma mult_n_nrows:

  1094 assumes

  1095 "! a. fmul 0 a = 0"

  1096 "! a. fmul a 0 = 0"

  1097 "fadd 0 0 = 0"

  1098 shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"

  1099 apply (subst nrows_le)

  1100 apply (simp add: mult_matrix_n_def)

  1101 apply (subst RepAbs_matrix)

  1102 apply (rule_tac x="nrows A" in exI)

  1103 apply (simp add: nrows assms foldseq_zero)

  1104 apply (rule_tac x="ncols B" in exI)

  1105 apply (simp add: ncols assms foldseq_zero)

  1106 apply (simp add: nrows assms foldseq_zero)

  1107 done

  1108

  1109 lemma mult_n_ncols:

  1110 assumes

  1111 "! a. fmul 0 a = 0"

  1112 "! a. fmul a 0 = 0"

  1113 "fadd 0 0 = 0"

  1114 shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"

  1115 apply (subst ncols_le)

  1116 apply (simp add: mult_matrix_n_def)

  1117 apply (subst RepAbs_matrix)

  1118 apply (rule_tac x="nrows A" in exI)

  1119 apply (simp add: nrows assms foldseq_zero)

  1120 apply (rule_tac x="ncols B" in exI)

  1121 apply (simp add: ncols assms foldseq_zero)

  1122 apply (simp add: ncols assms foldseq_zero)

  1123 done

  1124

  1125 lemma mult_nrows:

  1126 assumes

  1127 "! a. fmul 0 a = 0"

  1128 "! a. fmul a 0 = 0"

  1129 "fadd 0 0 = 0"

  1130 shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"

  1131 by (simp add: mult_matrix_def mult_n_nrows assms)

  1132

  1133 lemma mult_ncols:

  1134 assumes

  1135 "! a. fmul 0 a = 0"

  1136 "! a. fmul a 0 = 0"

  1137 "fadd 0 0 = 0"

  1138 shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"

  1139 by (simp add: mult_matrix_def mult_n_ncols assms)

  1140

  1141 lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"

  1142   apply (auto simp add: nrows_le)

  1143   apply (rule nrows)

  1144   apply (arith)

  1145   done

  1146

  1147 lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"

  1148   apply (auto simp add: ncols_le)

  1149   apply (rule ncols)

  1150   apply (arith)

  1151   done

  1152

  1153 lemma mult_matrix_assoc:

  1154   assumes

  1155   "! a. fmul1 0 a = 0"

  1156   "! a. fmul1 a 0 = 0"

  1157   "! a. fmul2 0 a = 0"

  1158   "! a. fmul2 a 0 = 0"

  1159   "fadd1 0 0 = 0"

  1160   "fadd2 0 0 = 0"

  1161   "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"

  1162   "associative fadd1"

  1163   "associative fadd2"

  1164   "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"

  1165   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"

  1166   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"

  1167   shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)"

  1168 proof -

  1169   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

  1170   have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (% k. fmul2 (s k) x) n"

  1171     by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all)

  1172   have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"

  1173     using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all)

  1174   let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"

  1175   show ?thesis

  1176     apply (simp add: Rep_matrix_inject[THEN sym])

  1177     apply (rule ext)+

  1178     apply (simp add: mult_matrix_def)

  1179     apply (simplesubst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"])

  1180     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1181     apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])

  1182     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1183     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])

  1184     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1185     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])

  1186     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1187     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])

  1188     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1189     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])

  1190     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+

  1191     apply (simp add: mult_matrix_n_def)

  1192     apply (rule comb_left)

  1193     apply ((rule ext)+, simp)

  1194     apply (simplesubst RepAbs_matrix)

  1195     apply (rule exI[of _ "nrows B"])

  1196     apply (simp add: nrows assms foldseq_zero)

  1197     apply (rule exI[of _ "ncols C"])

  1198     apply (simp add: assms ncols foldseq_zero)

  1199     apply (subst RepAbs_matrix)

  1200     apply (rule exI[of _ "nrows A"])

  1201     apply (simp add: nrows assms foldseq_zero)

  1202     apply (rule exI[of _ "ncols B"])

  1203     apply (simp add: assms ncols foldseq_zero)

  1204     apply (simp add: fmul2fadd1fold fmul1fadd2fold assms)

  1205     apply (subst foldseq_foldseq)

  1206     apply (simp add: assms)+

  1207     apply (simp add: transpose_infmatrix)

  1208     done

  1209 qed

  1210

  1211 lemma

  1212   assumes

  1213   "! a. fmul1 0 a = 0"

  1214   "! a. fmul1 a 0 = 0"

  1215   "! a. fmul2 0 a = 0"

  1216   "! a. fmul2 a 0 = 0"

  1217   "fadd1 0 0 = 0"

  1218   "fadd2 0 0 = 0"

  1219   "! a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"

  1220   "associative fadd1"

  1221   "associative fadd2"

  1222   "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"

  1223   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"

  1224   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"

  1225   shows

  1226   "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"

  1227 apply (rule ext)+

  1228 apply (simp add: comp_def )

  1229 apply (simp add: mult_matrix_assoc assms)

  1230 done

  1231

  1232 lemma mult_matrix_assoc_simple:

  1233   assumes

  1234   "! a. fmul 0 a = 0"

  1235   "! a. fmul a 0 = 0"

  1236   "fadd 0 0 = 0"

  1237   "associative fadd"

  1238   "commutative fadd"

  1239   "associative fmul"

  1240   "distributive fmul fadd"

  1241   shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)"

  1242 proof -

  1243   have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"

  1244     using assms by (simp add: associative_def commutative_def)

  1245   then show ?thesis

  1246     apply (subst mult_matrix_assoc)

  1247     using assms

  1248     apply simp_all

  1249     apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def)

  1250     done

  1251 qed

  1252

  1253 lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"

  1254 apply (simp add: Rep_matrix_inject[THEN sym])

  1255 apply (rule ext)+

  1256 by simp

  1257

  1258 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)"

  1259 apply (simp add: Rep_matrix_inject[THEN sym])

  1260 apply (rule ext)+

  1261 by simp

  1262

  1263 lemma Rep_mult_matrix:

  1264   assumes

  1265   "! a. fmul 0 a = 0"

  1266   "! a. fmul a 0 = 0"

  1267   "fadd 0 0 = 0"

  1268   shows

  1269   "Rep_matrix(mult_matrix fmul fadd A B) j i =

  1270   foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"

  1271 apply (simp add: mult_matrix_def mult_matrix_n_def)

  1272 apply (subst RepAbs_matrix)

  1273 apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero)

  1274 apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero)

  1275 apply simp

  1276 done

  1277

  1278 lemma transpose_mult_matrix:

  1279   assumes

  1280   "! a. fmul 0 a = 0"

  1281   "! a. fmul a 0 = 0"

  1282   "fadd 0 0 = 0"

  1283   "! x y. fmul y x = fmul x y"

  1284   shows

  1285   "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"

  1286   apply (simp add: Rep_matrix_inject[THEN sym])

  1287   apply (rule ext)+

  1288   using assms

  1289   apply (simp add: Rep_mult_matrix max_ac)

  1290   done

  1291

  1292 lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"

  1293 apply (simp add:  Rep_matrix_inject[THEN sym])

  1294 apply (rule ext)+

  1295 by simp

  1296

  1297 lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"

  1298 apply (simp add: Rep_matrix_inject[THEN sym])

  1299 apply (rule ext)+

  1300 by simp

  1301

  1302 instantiation matrix :: ("{zero, ord}") ord

  1303 begin

  1304

  1305 definition

  1306   le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"

  1307

  1308 definition

  1309   less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"

  1310

  1311 instance ..

  1312

  1313 end

  1314

  1315 instance matrix :: ("{zero, order}") order

  1316 apply intro_classes

  1317 apply (simp_all add: le_matrix_def less_def)

  1318 apply (auto)

  1319 apply (drule_tac x=j in spec, drule_tac x=j in spec)

  1320 apply (drule_tac x=i in spec, drule_tac x=i in spec)

  1321 apply (simp)

  1322 apply (simp add: Rep_matrix_inject[THEN sym])

  1323 apply (rule ext)+

  1324 apply (drule_tac x=xa in spec, drule_tac x=xa in spec)

  1325 apply (drule_tac x=xb in spec, drule_tac x=xb in spec)

  1326 apply simp

  1327 done

  1328

  1329 lemma le_apply_matrix:

  1330   assumes

  1331   "f 0 = 0"

  1332   "! x y. x <= y \<longrightarrow> f x <= f y"

  1333   "(a::('a::{ord, zero}) matrix) <= b"

  1334   shows

  1335   "apply_matrix f a <= apply_matrix f b"

  1336   using assms by (simp add: le_matrix_def)

  1337

  1338 lemma le_combine_matrix:

  1339   assumes

  1340   "f 0 0 = 0"

  1341   "! a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"

  1342   "A <= B"

  1343   "C <= D"

  1344   shows

  1345   "combine_matrix f A C <= combine_matrix f B D"

  1346   using assms by (simp add: le_matrix_def)

  1347

  1348 lemma le_left_combine_matrix:

  1349   assumes

  1350   "f 0 0 = 0"

  1351   "! a b c. a <= b \<longrightarrow> f c a <= f c b"

  1352   "A <= B"

  1353   shows

  1354   "combine_matrix f C A <= combine_matrix f C B"

  1355   using assms by (simp add: le_matrix_def)

  1356

  1357 lemma le_right_combine_matrix:

  1358   assumes

  1359   "f 0 0 = 0"

  1360   "! a b c. a <= b \<longrightarrow> f a c <= f b c"

  1361   "A <= B"

  1362   shows

  1363   "combine_matrix f A C <= combine_matrix f B C"

  1364   using assms by (simp add: le_matrix_def)

  1365

  1366 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"

  1367   by (simp add: le_matrix_def, auto)

  1368

  1369 lemma le_foldseq:

  1370   assumes

  1371   "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"

  1372   "! i. i <= n \<longrightarrow> s i <= t i"

  1373   shows

  1374   "foldseq f s n <= foldseq f t n"

  1375 proof -

  1376   have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n"

  1377     by (induct n) (simp_all add: assms)

  1378   then show "foldseq f s n <= foldseq f t n" using assms by simp

  1379 qed

  1380

  1381 lemma le_left_mult:

  1382   assumes

  1383   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"

  1384   "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"

  1385   "! a. fmul 0 a = 0"

  1386   "! a. fmul a 0 = 0"

  1387   "fadd 0 0 = 0"

  1388   "0 <= C"

  1389   "A <= B"

  1390   shows

  1391   "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"

  1392   using assms

  1393   apply (simp add: le_matrix_def Rep_mult_matrix)

  1394   apply (auto)

  1395   apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+

  1396   apply (rule le_foldseq)

  1397   apply (auto)

  1398   done

  1399

  1400 lemma le_right_mult:

  1401   assumes

  1402   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"

  1403   "! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"

  1404   "! a. fmul 0 a = 0"

  1405   "! a. fmul a 0 = 0"

  1406   "fadd 0 0 = 0"

  1407   "0 <= C"

  1408   "A <= B"

  1409   shows

  1410   "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"

  1411   using assms

  1412   apply (simp add: le_matrix_def Rep_mult_matrix)

  1413   apply (auto)

  1414   apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+

  1415   apply (rule le_foldseq)

  1416   apply (auto)

  1417   done

  1418

  1419 lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast

  1420 lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast

  1421

  1422 lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"

  1423   by (auto simp add: le_matrix_def)

  1424

  1425 lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"

  1426   apply (auto)

  1427   apply (simp add: le_matrix_def)

  1428   apply (drule_tac j=j and i=i in spec2)

  1429   apply (simp)

  1430   apply (simp add: le_matrix_def)

  1431   done

  1432

  1433 lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"

  1434   apply (auto)

  1435   apply (simp add: le_matrix_def)

  1436   apply (drule_tac j=j and i=i in spec2)

  1437   apply (simp)

  1438   apply (simp add: le_matrix_def)

  1439   done

  1440

  1441 lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"

  1442   apply (auto simp add: le_matrix_def neg_def)

  1443   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)

  1444   apply (auto)

  1445   done

  1446

  1447 lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"

  1448   apply (auto simp add: le_matrix_def neg_def)

  1449   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)

  1450   apply (auto)

  1451   done

  1452

  1453 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))"

  1454   apply (auto simp add: le_matrix_def neg_def)

  1455   apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)

  1456   apply (auto)

  1457   done

  1458

  1459 instantiation matrix :: ("{lattice, zero}") lattice

  1460 begin

  1461

  1462 definition "inf = combine_matrix inf"

  1463

  1464 definition "sup = combine_matrix sup"

  1465

  1466 instance

  1467   by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)

  1468

  1469 end

  1470

  1471 instantiation matrix :: ("{plus, zero}") plus

  1472 begin

  1473

  1474 definition

  1475   plus_matrix_def: "A + B = combine_matrix (op +) A B"

  1476

  1477 instance ..

  1478

  1479 end

  1480

  1481 instantiation matrix :: ("{uminus, zero}") uminus

  1482 begin

  1483

  1484 definition

  1485   minus_matrix_def: "- A = apply_matrix uminus A"

  1486

  1487 instance ..

  1488

  1489 end

  1490

  1491 instantiation matrix :: ("{minus, zero}") minus

  1492 begin

  1493

  1494 definition

  1495   diff_matrix_def: "A - B = combine_matrix (op -) A B"

  1496

  1497 instance ..

  1498

  1499 end

  1500

  1501 instantiation matrix :: ("{plus, times, zero}") times

  1502 begin

  1503

  1504 definition

  1505   times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"

  1506

  1507 instance ..

  1508

  1509 end

  1510

  1511 instantiation matrix :: ("{lattice, uminus, zero}") abs

  1512 begin

  1513

  1514 definition

  1515   abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"

  1516

  1517 instance ..

  1518

  1519 end

  1520

  1521 instance matrix :: (monoid_add) monoid_add

  1522 proof

  1523   fix A B C :: "'a matrix"

  1524   show "A + B + C = A + (B + C)"

  1525     apply (simp add: plus_matrix_def)

  1526     apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])

  1527     apply (simp_all add: add_assoc)

  1528     done

  1529   show "0 + A = A"

  1530     apply (simp add: plus_matrix_def)

  1531     apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])

  1532     apply (simp)

  1533     done

  1534   show "A + 0 = A"

  1535     apply (simp add: plus_matrix_def)

  1536     apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec])

  1537     apply (simp)

  1538     done

  1539 qed

  1540

  1541 instance matrix :: (comm_monoid_add) comm_monoid_add

  1542 proof

  1543   fix A B :: "'a matrix"

  1544   show "A + B = B + A"

  1545     apply (simp add: plus_matrix_def)

  1546     apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])

  1547     apply (simp_all add: add_commute)

  1548     done

  1549   show "0 + A = A"

  1550     apply (simp add: plus_matrix_def)

  1551     apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])

  1552     apply (simp)

  1553     done

  1554 qed

  1555

  1556 instance matrix :: (group_add) group_add

  1557 proof

  1558   fix A B :: "'a matrix"

  1559   show "- A + A = 0"

  1560     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)

  1561   show "A - B = A + - B"

  1562     by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)

  1563 qed

  1564

  1565 instance matrix :: (ab_group_add) ab_group_add

  1566 proof

  1567   fix A B :: "'a matrix"

  1568   show "- A + A = 0"

  1569     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)

  1570   show "A - B = A + - B"

  1571     by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)

  1572 qed

  1573

  1574 instance matrix :: (ordered_ab_group_add) ordered_ab_group_add

  1575 proof

  1576   fix A B C :: "'a matrix"

  1577   assume "A <= B"

  1578   then show "C + A <= C + B"

  1579     apply (simp add: plus_matrix_def)

  1580     apply (rule le_left_combine_matrix)

  1581     apply (simp_all)

  1582     done

  1583 qed

  1584

  1585 instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add ..

  1586 instance matrix :: (lattice_ab_group_add) semilattice_sup_ab_group_add ..

  1587

  1588 instance matrix :: (semiring_0) semiring_0

  1589 proof

  1590   fix A B C :: "'a matrix"

  1591   show "A * B * C = A * (B * C)"

  1592     apply (simp add: times_matrix_def)

  1593     apply (rule mult_matrix_assoc)

  1594     apply (simp_all add: associative_def algebra_simps)

  1595     done

  1596   show "(A + B) * C = A * C + B * C"

  1597     apply (simp add: times_matrix_def plus_matrix_def)

  1598     apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])

  1599     apply (simp_all add: associative_def commutative_def algebra_simps)

  1600     done

  1601   show "A * (B + C) = A * B + A * C"

  1602     apply (simp add: times_matrix_def plus_matrix_def)

  1603     apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])

  1604     apply (simp_all add: associative_def commutative_def algebra_simps)

  1605     done

  1606   show "0 * A = 0" by (simp add: times_matrix_def)

  1607   show "A * 0 = 0" by (simp add: times_matrix_def)

  1608 qed

  1609

  1610 instance matrix :: (ring) ring ..

  1611

  1612 instance matrix :: (ordered_ring) ordered_ring

  1613 proof

  1614   fix A B C :: "'a matrix"

  1615   assume a: "A \<le> B"

  1616   assume b: "0 \<le> C"

  1617   from a b show "C * A \<le> C * B"

  1618     apply (simp add: times_matrix_def)

  1619     apply (rule le_left_mult)

  1620     apply (simp_all add: add_mono mult_left_mono)

  1621     done

  1622   from a b show "A * C \<le> B * C"

  1623     apply (simp add: times_matrix_def)

  1624     apply (rule le_right_mult)

  1625     apply (simp_all add: add_mono mult_right_mono)

  1626     done

  1627 qed

  1628

  1629 instance matrix :: (lattice_ring) lattice_ring

  1630 proof

  1631   fix A B C :: "('a :: lattice_ring) matrix"

  1632   show "abs A = sup A (-A)"

  1633     by (simp add: abs_matrix_def)

  1634 qed

  1635

  1636 lemma Rep_matrix_add[simp]:

  1637   "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"

  1638   by (simp add: plus_matrix_def)

  1639

  1640 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i =

  1641   foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"

  1642 apply (simp add: times_matrix_def)

  1643 apply (simp add: Rep_mult_matrix)

  1644 done

  1645

  1646 lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a)

  1647   \<Longrightarrow> apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"

  1648 apply (subst Rep_matrix_inject[symmetric])

  1649 apply (rule ext)+

  1650 apply (simp)

  1651 done

  1652

  1653 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"

  1654 apply (subst Rep_matrix_inject[symmetric])

  1655 apply (rule ext)+

  1656 apply (simp)

  1657 done

  1658

  1659 lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) <= nrows A"

  1660 by (simp add: times_matrix_def mult_nrows)

  1661

  1662 lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) <= ncols B"

  1663 by (simp add: times_matrix_def mult_ncols)

  1664

  1665 definition

  1666   one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where

  1667   "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"

  1668

  1669 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"

  1670 apply (simp add: one_matrix_def)

  1671 apply (simplesubst RepAbs_matrix)

  1672 apply (rule exI[of _ n], simp add: split_if)+

  1673 by (simp add: split_if)

  1674

  1675 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")

  1676 proof -

  1677   have "?r <= n" by (simp add: nrows_le)

  1678   moreover have "n <= ?r" by (simp add:le_nrows, arith)

  1679   ultimately show "?r = n" by simp

  1680 qed

  1681

  1682 lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")

  1683 proof -

  1684   have "?r <= n" by (simp add: ncols_le)

  1685   moreover have "n <= ?r" by (simp add: le_ncols, arith)

  1686   ultimately show "?r = n" by simp

  1687 qed

  1688

  1689 lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"

  1690 apply (subst Rep_matrix_inject[THEN sym])

  1691 apply (rule ext)+

  1692 apply (simp add: times_matrix_def Rep_mult_matrix)

  1693 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])

  1694 apply (simp_all)

  1695 by (simp add: ncols)

  1696

  1697 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"

  1698 apply (subst Rep_matrix_inject[THEN sym])

  1699 apply (rule ext)+

  1700 apply (simp add: times_matrix_def Rep_mult_matrix)

  1701 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])

  1702 apply (simp_all)

  1703 by (simp add: nrows)

  1704

  1705 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"

  1706 apply (simp add: times_matrix_def)

  1707 apply (subst transpose_mult_matrix)

  1708 apply (simp_all add: mult_commute)

  1709 done

  1710

  1711 lemma transpose_matrix_add: "transpose_matrix ((A::('a::monoid_add) matrix)+B) = transpose_matrix A + transpose_matrix B"

  1712 by (simp add: plus_matrix_def transpose_combine_matrix)

  1713

  1714 lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"

  1715 by (simp add: diff_matrix_def transpose_combine_matrix)

  1716

  1717 lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"

  1718 by (simp add: minus_matrix_def transpose_apply_matrix)

  1719

  1720 definition right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where

  1721   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A"

  1722

  1723 definition left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where

  1724   "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A"

  1725

  1726 definition inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where

  1727   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"

  1728

  1729 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"

  1730 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])

  1731 by (simp add: right_inverse_matrix_def)

  1732

  1733 lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"

  1734 apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A])

  1735 by (simp add: left_inverse_matrix_def)

  1736

  1737 lemma left_right_inverse_matrix_unique:

  1738   assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"

  1739   shows "X = Y"

  1740 proof -

  1741   have "Y = Y * one_matrix (nrows A)"

  1742     apply (subst one_matrix_mult_right)

  1743     using assms

  1744     apply (simp_all add: left_inverse_matrix_def)

  1745     done

  1746   also have "\<dots> = Y * (A * X)"

  1747     apply (insert assms)

  1748     apply (frule right_inverse_matrix_dim)

  1749     by (simp add: right_inverse_matrix_def)

  1750   also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)

  1751   also have "\<dots> = X"

  1752     apply (insert assms)

  1753     apply (frule left_inverse_matrix_dim)

  1754     apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)

  1755     done

  1756   ultimately show "X = Y" by (simp)

  1757 qed

  1758

  1759 lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"

  1760   by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)

  1761

  1762 lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"

  1763   by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)

  1764

  1765 lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \<Longrightarrow> a * b = 0"

  1766 by auto

  1767

  1768 lemma Rep_matrix_zero_imp_mult_zero:

  1769   "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lattice_ring) matrix)"

  1770 apply (subst Rep_matrix_inject[symmetric])

  1771 apply (rule ext)+

  1772 apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)

  1773 done

  1774

  1775 lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"

  1776 apply (simp add: plus_matrix_def)

  1777 apply (rule combine_nrows)

  1778 apply (simp_all)

  1779 done

  1780

  1781 lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"

  1782 apply (subst Rep_matrix_inject[symmetric])

  1783 apply (rule ext)+

  1784 apply (auto simp add: Rep_matrix_mult foldseq_zero)

  1785 apply (rule_tac foldseq_zerotail[symmetric])

  1786 apply (auto simp add: nrows zero_imp_mult_zero max2)

  1787 apply (rule order_trans)

  1788 apply (rule ncols_move_matrix_le)

  1789 apply (simp add: max1)

  1790 done

  1791

  1792 lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"

  1793 apply (subst Rep_matrix_inject[symmetric])

  1794 apply (rule ext)+

  1795 apply (auto simp add: Rep_matrix_mult foldseq_zero)

  1796 apply (rule_tac foldseq_zerotail[symmetric])

  1797 apply (auto simp add: ncols zero_imp_mult_zero max1)

  1798 apply (rule order_trans)

  1799 apply (rule nrows_move_matrix_le)

  1800 apply (simp add: max2)

  1801 done

  1802

  1803 lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)"

  1804 apply (subst Rep_matrix_inject[symmetric])

  1805 apply (rule ext)+

  1806 apply (simp)

  1807 done

  1808

  1809 lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"

  1810 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)

  1811

  1812 definition scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where

  1813   "scalar_mult a m == apply_matrix (op * a) m"

  1814

  1815 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"

  1816 by (simp add: scalar_mult_def)

  1817

  1818 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"

  1819 by (simp add: scalar_mult_def apply_matrix_add algebra_simps)

  1820

  1821 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)"

  1822 by (simp add: scalar_mult_def)

  1823

  1824 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"

  1825 apply (subst Rep_matrix_inject[symmetric])

  1826 apply (rule ext)+

  1827 apply (auto)

  1828 done

  1829

  1830 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"

  1831 by (simp add: minus_matrix_def)

  1832

  1833 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"

  1834 by (simp add: abs_lattice sup_matrix_def)

  1835

  1836 end