src/HOL/Matrix/MatrixGeneral.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 23373 ead82c82da9e child 25502 9200b36280c0 permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/Matrix/MatrixGeneral.thy

     2     ID:         $Id$

     3     Author:     Steven Obua

     4 *)

     5

     6 theory MatrixGeneral imports Main begin

     7

     8 types 'a infmatrix = "[nat, nat] \<Rightarrow> 'a"

     9

    10 constdefs

    11   nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set"

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

    13

    14 typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}"

    15 apply (rule_tac x="(% j i. 0)" in exI)

    16 by (simp add: nonzero_positions_def)

    17

    18 declare Rep_matrix_inverse[simp]

    19

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

    21 apply (rule Abs_matrix_induct)

    22 by (simp add: Abs_matrix_inverse matrix_def)

    23

    24 constdefs

    25   nrows :: "('a::zero) matrix \<Rightarrow> nat"

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

    27   ncols :: "('a::zero) matrix \<Rightarrow> nat"

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

    29

    30 lemma nrows:

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

    32   shows "(Rep_matrix A m n) = 0" (is ?concl)

    33 proof cases

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

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

    36 next

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

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

    39   from a have b: "?S \<noteq> {}" by (simp)

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

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

    42   have "m \<notin> ?S"

    43     proof -

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

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

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

    47     qed

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

    49 qed

    50

    51 constdefs

    52   transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"

    53   "transpose_infmatrix A j i == A i j"

    54   transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"

    55   "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"

    56

    57 declare transpose_infmatrix_def[simp]

    58

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

    60 by ((rule ext)+, simp)

    61

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

    63   apply (rule ext)+

    64   by (simp add: transpose_infmatrix_def)

    65

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

    67 apply (rule Abs_matrix_inverse)

    68 apply (simp add: matrix_def nonzero_positions_def image_def)

    69 proof -

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

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

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

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

    74     apply (simp add: image_def)

    75     apply (rule set_ext)

    76     apply (simp)

    77     proof

    78       fix y

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

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

    81         proof -

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

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

    84         qed

    85     next

    86       fix y

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

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

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

    90     qed

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

    92     proof -

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

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

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

    96     qed

    97   moreover

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

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

   100 qed

   101

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

   103

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

   105 apply (auto)

   106 apply (rule ext)+

   107 apply (simp add: transpose_infmatrix)

   108 apply (drule infmatrixforward)

   109 apply (simp)

   110 done

   111

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

   113 apply (simp add: transpose_matrix_def)

   114 apply (subst Rep_matrix_inject[THEN sym])+

   115 apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)

   116 done

   117

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

   119 by (simp add: transpose_matrix_def)

   120

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

   122 by (simp add: transpose_matrix_def)

   123

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

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

   126

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

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

   129

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

   131 proof -

   132   assume "ncols A <= n"

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

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

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

   136 qed

   137

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

   139 apply (auto)

   140 apply (simp add: ncols)

   141 proof (simp add: ncols_def, auto)

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

   143   let ?p = "snd?P"

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

   145   let ?m = "Max ?p"

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

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

   148   fix a b

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

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

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

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

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

   154   moreover assume ?st

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

   156 qed

   157

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

   159 proof -

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

   161   show ?concl by (simp add: a ncols_le)

   162 qed

   163

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

   165 apply (auto)

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

   167 apply (simp)

   168 apply (simp add: ncols_le)

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

   170 by (simp add: ncols)

   171

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

   173 proof -

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

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

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

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

   178 qed

   179

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

   181 proof -

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

   183   show ?concl by (simp add: a nrows_le)

   184 qed

   185

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

   187 apply (auto)

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

   189 apply (simp)

   190 apply (simp add: nrows_le)

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

   192 by (simp add: nrows)

   193

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

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

   196 apply (simp_all add: nrows)

   197 done

   198

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

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

   201 apply (simp_all add: ncols)

   202 done

   203

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

   205 apply (induct n)

   206 apply (simp)

   207 proof -

   208   fix n

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

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

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

   212 qed

   213

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

   215   apply (induct m)

   216   apply (simp+)

   217   proof -

   218     fix m::nat

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

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

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

   222     assume f0: "finite ?s0"

   223     have f1: "finite ?sd"

   224     proof -

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

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

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

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

   229     qed

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

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

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

   233 qed

   234

   235 lemma RepAbs_matrix:

   236   assumes aem: "? m. ! j i. m <= j \<longrightarrow> x j i = 0" (is ?em) and aen:"? n. ! j i. (n <= i \<longrightarrow> x j i = 0)" (is ?en)

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

   238 apply (rule Abs_matrix_inverse)

   239 apply (simp add: matrix_def nonzero_positions_def)

   240 proof -

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

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

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

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

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

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

   247     apply (simp)

   248     apply (rule set_ext)

   249     apply (simp)

   250     apply auto

   251     by (rule c, auto)+

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

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

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

   255 qed

   256

   257 constdefs

   258   apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"

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

   260   apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"

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

   262   combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"

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

   264   combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"

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

   266

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

   268 by (simp add: apply_infmatrix_def)

   269

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

   271 by (simp add: combine_infmatrix_def)

   272

   273 constdefs

   274 commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"

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

   276 associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"

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

   278

   279 text{*

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

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

   282 sets $A$ and $B$ with $B \subset A$ and an abstraction $u: A \rightarrow B$. This abstraction has to fulfill $u(b) = b$ for all $b \in B$, but is arbitrary otherwise.

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

   284 It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$

   285 *}

   286

   287 lemma combine_infmatrix_commute:

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

   289 by (simp add: commutative_def combine_infmatrix_def)

   290

   291 lemma combine_matrix_commute:

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

   293 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)

   294

   295 text{*

   296 On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,

   297 as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have

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

   299 but on the other hand we have

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

   301 A way out of this problem is to assume that $f(A\times A)\subset A$ holds, and this is what we are going to do:

   302 *}

   303

   304 lemma nonzero_positions_combine_infmatrix[simp]: "f 0 0 = 0 \<Longrightarrow> nonzero_positions (combine_infmatrix f A B) \<subseteq> (nonzero_positions A) \<union> (nonzero_positions B)"

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

   306

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

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

   309

   310 lemma combine_infmatrix_closed [simp]:

   311   "f 0 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))) = combine_infmatrix f (Rep_matrix A) (Rep_matrix B)"

   312 apply (rule Abs_matrix_inverse)

   313 apply (simp add: matrix_def)

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

   315 by (simp_all)

   316

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

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

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

   320

   321 lemma apply_infmatrix_closed [simp]:

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

   323 apply (rule Abs_matrix_inverse)

   324 apply (simp add: matrix_def)

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

   326 by (simp_all)

   327

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

   329 by (simp add: associative_def combine_infmatrix_def)

   330

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

   332 by (auto)

   333

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

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

   336 apply (rule comb [of Abs_matrix Abs_matrix])

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

   338

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

   340 by (simp add: apply_matrix_def)

   341

   342 lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \<Longrightarrow> Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"

   343   by(simp add: combine_matrix_def)

   344

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

   346 by (simp add: nrows_le)

   347

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

   349 by (simp add: ncols_le)

   350

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

   352   by (simp add: nrows_le)

   353

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

   355   by (simp add: ncols_le)

   356

   357 constdefs

   358   zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"

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

   360   zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"

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

   362   zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"

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

   364

   365 consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"

   366 primrec

   367   "foldseq f s 0 = s 0"

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

   369

   370 consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"

   371 primrec

   372   "foldseq_transposed f s 0 = s 0"

   373   "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"

   374

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

   376 proof -

   377   assume a:"associative f"

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

   379   proof -

   380     fix n

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

   382     proof (induct n)

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

   384     next

   385       fix n

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

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

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

   389       proof (auto)

   390         fix N t

   391         assume Nsuc: "N <= Suc n"

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

   393         proof cases

   394           assume "N <= n"

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

   396         next

   397           assume "~(N <= n)"

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

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

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

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

   402             apply (simp add: Nsuceq)

   403             apply (subst c)

   404             apply (simp)

   405             apply (case_tac "n = 0")

   406             apply (simp)

   407             apply (drule neqz)

   408             apply (erule exE)

   409             apply (simp)

   410             apply (subst assocf)

   411             proof -

   412               fix m

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

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

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

   416                 apply (subst c)

   417                 by simp+

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

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

   420                 apply (subst c)

   421                 by (simp add: mless)+

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

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

   424             qed

   425           qed

   426         qed

   427       qed

   428     qed

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

   430   qed

   431

   432 lemma foldseq_distr: "\<lbrakk>associative f; commutative f\<rbrakk> \<Longrightarrow> foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"

   433 proof -

   434   assume assoc: "associative f"

   435   assume comm: "commutative f"

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

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

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

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

   440     apply (induct_tac n)

   441     apply (simp+, auto)

   442     by (simp add: a b c)

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

   444 qed

   445

   446 theorem "\<lbrakk>associative f; associative g; \<forall>a b c d. g (f a b) (f c d) = f (g a c) (g b d); ? x y. (f x) \<noteq> (f y); ? x y. (g x) \<noteq> (g y); f x x = x; g x x = x\<rbrakk> \<Longrightarrow> f=g | (! y. f y x = y) | (! y. g y x = y)"

   447 oops

   448 (* Model found

   449

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

   451  \<forall>a b c d. g (f a b) (f c d) = f (g a c) (g b d); \<exists>x y. f x \<noteq> f y;

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

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

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

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

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

   457 Model found:

   458 Size of types: 'a: 3

   459 x: a1

   460 g: (a0\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a0, a2\<mapsto>a1), a1\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a1, a2\<mapsto>a0), a2\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a0, a2\<mapsto>a1))

   461 f: (a0\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0), a1\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a1, a2\<mapsto>a1), a2\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0))

   462 *)

   463

   464 lemma foldseq_zero:

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

   466 shows "foldseq f s n = 0"

   467 proof -

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

   469     apply (induct_tac n)

   470     apply (simp)

   471     by (simp add: fz)

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

   473 qed

   474

   475 lemma foldseq_significant_positions:

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

   477   shows "foldseq f S N = foldseq f T N" (is ?concl)

   478 proof -

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

   480     apply (induct_tac m)

   481     apply (simp)

   482     apply (simp)

   483     apply (auto)

   484     proof -

   485       fix n

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

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

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

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

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

   491       have d:"!! s t. (\<forall>i\<le>n. s i = t i) \<Longrightarrow> foldseq f s n = foldseq f t n" by (simp add: a)

   492       show "f (t 0) (foldseq f (\<lambda>k. s (Suc k)) n) = f (t 0) (foldseq f (\<lambda>k. t (Suc k)) n)" by (rule c, simp add: d b)

   493     qed

   494   with p show ?concl by simp

   495 qed

   496

   497 lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")

   498 proof -

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

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

   501   have "!! n. ! m s. m <= n \<longrightarrow> foldseq f s n = foldseq f (% k. (if k < m then (s k) else (foldseq f (% k. s(k+m)) (n-m)))) m"

   502     apply (induct_tac n)

   503     apply (simp)

   504     apply (simp)

   505     apply (auto)

   506     apply (case_tac "m = Suc na")

   507     apply (simp)

   508     apply (rule a)

   509     apply (rule foldseq_significant_positions)

   510     apply (auto)

   511     apply (drule suc, simp+)

   512     proof -

   513       fix na m s

   514       assume suba:"\<forall>m\<le>na. \<forall>s. foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m"

   515       assume subb:"m <= na"

   516       from suba have subc:"!! m s. m <= na \<Longrightarrow>foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m" by simp

   517       have subd: "foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m =

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

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

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

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

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

   523         apply (simp add: subd)

   524         apply (case_tac "m=0")

   525         apply (simp)

   526         apply (drule sube)

   527         apply (auto)

   528         apply (rule a)

   529         by (simp add: subc if_def)

   530     qed

   531   then show "?p \<Longrightarrow> ?concl" by simp

   532 qed

   533

   534 lemma foldseq_zerotail:

   535   assumes

   536   fz: "f 0 0 = 0"

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

   538   and nm: "n <= m"

   539   shows

   540   "foldseq f s n = foldseq f s m"

   541 proof -

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

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

   544     apply (rule foldseq_significant_positions)

   545     apply (auto)

   546     apply (subst foldseq_zero)

   547     by (simp add: fz sz)+

   548 qed

   549

   550 lemma foldseq_zerotail2:

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

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

   553   and nm: "n <= m"

   554   shows

   555   "foldseq f s n = foldseq f s m" (is ?concl)

   556 proof -

   557   have "f 0 0 = 0" by (simp add: prems)

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

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

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

   561   show ?concl

   562     apply (subst foldseq_tail[OF nm])

   563     apply (rule foldseq_significant_positions)

   564     apply (auto)

   565     apply (case_tac "m=n")

   566     apply (simp+)

   567     apply (drule b[OF nm])

   568     apply (auto)

   569     apply (case_tac "k=0")

   570     apply (simp add: prems)

   571     apply (drule d)

   572     apply (auto)

   573     by (simp add: prems foldseq_zero)

   574 qed

   575

   576 lemma foldseq_zerostart:

   577   "! x. f 0 (f 0 x) = f 0 x \<Longrightarrow>  ! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"

   578 proof -

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

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

   581     apply (induct n)

   582     apply (simp)

   583     apply (rule allI, rule impI)

   584     proof -

   585       fix n

   586       fix s

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

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

   589       from b have c:"!! s. (\<forall>i\<le>n. s i = 0) \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp

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

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

   592         apply (subst a)

   593         apply (subst c)

   594         by (simp add: d f00x)+

   595     qed

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

   597 qed

   598

   599 lemma foldseq_zerostart2:

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

   601 proof -

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

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

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

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

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

   607   show "foldseq f s n = s n"

   608   apply (case_tac "n=0")

   609   apply (simp)

   610   apply (insert a)

   611   apply (drule d)

   612   apply (auto)

   613   apply (simp add: b)

   614   apply (insert f00x)

   615   apply (drule foldseq_zerostart)

   616   by (simp add: x)+

   617 qed

   618

   619 lemma foldseq_almostzero:

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

   621   shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)

   622 proof -

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

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

   625   show ?concl

   626     apply auto

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

   628     apply simp

   629     apply (subst foldseq_zerostart2)

   630     apply (simp add: f0x a)+

   631     apply (subst foldseq_zero)

   632     by (simp add: s0 f0x)+

   633 qed

   634

   635 lemma foldseq_distr_unary:

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

   637   shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)

   638 proof -

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

   640     apply (induct_tac n)

   641     apply (simp)

   642     apply (simp)

   643     apply (auto)

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

   645     by (simp add: prems)

   646   then show ?concl by simp

   647 qed

   648

   649 constdefs

   650   mult_matrix_n :: "nat \<Rightarrow> (('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix"

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

   652   mult_matrix :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix"

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

   654

   655 lemma mult_matrix_n:

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

   657   shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)

   658 proof -

   659   show ?concl using prems

   660     apply (simp add: mult_matrix_def mult_matrix_n_def)

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

   662     by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)

   663 qed

   664

   665 lemma mult_matrix_nm:

   666   assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"

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

   668 proof -

   669   from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)

   670   also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])

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

   672 qed

   673

   674 constdefs

   675   r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"

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

   677   l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"

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

   679   distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"

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

   681

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

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

   684

   685 lemma r_distributive_matrix:

   686  assumes prems:

   687   "r_distributive fmul fadd"

   688   "associative fadd"

   689   "commutative fadd"

   690   "fadd 0 0 = 0"

   691   "! a. fmul a 0 = 0"

   692   "! a. fmul 0 a = 0"

   693  shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)

   694 proof -

   695   from prems show ?concl

   696     apply (simp add: r_distributive_def mult_matrix_def, auto)

   697     proof -

   698       fix a::"'a matrix"

   699       fix u::"'b matrix"

   700       fix v::"'b matrix"

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

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

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

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

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

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

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

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

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

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

   711         apply (simp add: combine_matrix_def combine_infmatrix_def)

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

   713         apply (simplesubst RepAbs_matrix)

   714         apply (simp, auto)

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

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

   717         apply (subst RepAbs_matrix)

   718         apply (simp, auto)

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

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

   721         done

   722     qed

   723 qed

   724

   725 lemma l_distributive_matrix:

   726  assumes prems:

   727   "l_distributive fmul fadd"

   728   "associative fadd"

   729   "commutative fadd"

   730   "fadd 0 0 = 0"

   731   "! a. fmul a 0 = 0"

   732   "! a. fmul 0 a = 0"

   733  shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)

   734 proof -

   735   from prems show ?concl

   736     apply (simp add: l_distributive_def mult_matrix_def, auto)

   737     proof -

   738       fix a::"'b matrix"

   739       fix u::"'a matrix"

   740       fix v::"'a matrix"

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

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

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

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

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

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

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

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

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

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

   751         apply (simp add: combine_matrix_def combine_infmatrix_def)

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

   753         apply (simplesubst RepAbs_matrix)

   754         apply (simp, auto)

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

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

   757         apply (subst RepAbs_matrix)

   758         apply (simp, auto)

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

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

   761         done

   762     qed

   763 qed

   764

   765 instance matrix :: (zero) zero ..

   766

   767 defs(overloaded)

   768   zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"

   769

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

   771   apply (simp add: zero_matrix_def)

   772   apply (subst RepAbs_matrix)

   773   by (auto)

   774

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

   776 proof -

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

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

   779 qed

   780

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

   782 proof -

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

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

   785 qed

   786

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

   788   by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)

   789

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

   791   by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)

   792

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

   794   apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)

   795   apply (auto)

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

   797

   798 lemma mult_matrix_n_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd A 0 = 0"

   799   apply (simp add: mult_matrix_n_def)

   800   apply (subst foldseq_zero)

   801   by (simp_all add: zero_matrix_def)

   802

   803 lemma mult_matrix_n_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd 0 A = 0"

   804   apply (simp add: mult_matrix_n_def)

   805   apply (subst foldseq_zero)

   806   by (simp_all add: zero_matrix_def)

   807

   808 lemma mult_matrix_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd 0 A = 0"

   809 by (simp add: mult_matrix_def)

   810

   811 lemma mult_matrix_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; !a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd A 0 = 0"

   812 by (simp add: mult_matrix_def)

   813

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

   815   apply (simp add: apply_matrix_def apply_infmatrix_def)

   816   by (simp add: zero_matrix_def)

   817

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

   819   apply (simp add: combine_matrix_def combine_infmatrix_def)

   820   by (simp add: zero_matrix_def)

   821

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

   823 apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)

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

   825 apply (simp add: RepAbs_matrix)

   826 done

   827

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

   829   apply (simp add: apply_matrix_def apply_infmatrix_def)

   830   by (simp add: zero_matrix_def)

   831

   832 constdefs

   833   singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"

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

   835   move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"

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

   837   take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"

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

   839   take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"

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

   841

   842 constdefs

   843   column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"

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

   845   row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"

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

   847

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

   849 apply (simp add: singleton_matrix_def)

   850 apply (auto)

   851 apply (subst RepAbs_matrix)

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

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

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

   855

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

   857 apply (subst Rep_matrix_inject[symmetric])

   858 apply (rule ext)+

   859 apply (simp)

   860 done

   861

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

   863   by (simp add: singleton_matrix_def zero_matrix_def)

   864

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

   866 proof-

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

   868 from th show ?thesis

   869 apply (auto)

   870 apply (rule le_anti_sym)

   871 apply (subst nrows_le)

   872 apply (simp add: singleton_matrix_def, auto)

   873 apply (subst RepAbs_matrix)

   874 apply auto

   875 apply (simp add: Suc_le_eq)

   876 apply (rule not_leE)

   877 apply (subst nrows_le)

   878 by simp

   879 qed

   880

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

   882 proof-

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

   884 from th show ?thesis

   885 apply (auto)

   886 apply (rule le_anti_sym)

   887 apply (subst ncols_le)

   888 apply (simp add: singleton_matrix_def, auto)

   889 apply (subst RepAbs_matrix)

   890 apply auto

   891 apply (simp add: Suc_le_eq)

   892 apply (rule not_leE)

   893 apply (subst ncols_le)

   894 by simp

   895 qed

   896

   897 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"

   898 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)

   899 apply (subst RepAbs_matrix)

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

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

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

   903 apply (subst RepAbs_matrix)

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

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

   906 by simp

   907

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

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

   910 apply (simp)

   911 done

   912

   913 lemma Rep_move_matrix[simp]:

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

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

   916 apply (simp add: move_matrix_def)

   917 apply (auto)

   918 by (subst RepAbs_matrix,

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

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

   921

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

   923 by (simp add: move_matrix_def)

   924

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

   926 apply (subst Rep_matrix_inject[symmetric])

   927 apply (rule ext)+

   928 apply (simp)

   929 done

   930

   931 lemma transpose_move_matrix[simp]:

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

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

   934 apply (simp)

   935 done

   936

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

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

   939   apply (subst Rep_matrix_inject[symmetric])

   940   apply (rule ext)+

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

   942   apply (simp, arith)

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

   944   apply (simp add: neg_def, arith)

   945   apply (simp add: neg_def)

   946   apply arith

   947   done

   948

   949 lemma Rep_take_columns[simp]:

   950   "Rep_matrix (take_columns A c) j i =

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

   952 apply (simp add: take_columns_def)

   953 apply (simplesubst RepAbs_matrix)

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

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

   956 done

   957

   958 lemma Rep_take_rows[simp]:

   959   "Rep_matrix (take_rows A r) j i =

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

   961 apply (simp add: take_rows_def)

   962 apply (simplesubst RepAbs_matrix)

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

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

   965 done

   966

   967 lemma Rep_column_of_matrix[simp]:

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

   969   by (simp add: column_of_matrix_def)

   970

   971 lemma Rep_row_of_matrix[simp]:

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

   973   by (simp add: row_of_matrix_def)

   974

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

   976 apply (subst Rep_matrix_inject[THEN sym])

   977 apply (rule ext)+

   978 by (simp add: ncols)

   979

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

   981 apply (subst Rep_matrix_inject[THEN sym])

   982 apply (rule ext)+

   983 by (simp add: nrows)

   984

   985 lemma mult_matrix_singleton_right[simp]:

   986   assumes prems:

   987   "! x. fmul x 0 = 0"

   988   "! x. fmul 0 x = 0"

   989   "! x. fadd 0 x = x"

   990   "! x. fadd x 0 = x"

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

   992   apply (simp add: mult_matrix_def)

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

   994   apply (auto)

   995   apply (simp add: prems)+

   996   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)

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

   998   apply (subst foldseq_almostzero[of _ j])

   999   apply (simp add: prems)+

  1000   apply (auto)

  1001   proof -

  1002     fix k

  1003     fix l

  1004     assume a:"~neg(int l - int i)"

  1005     assume b:"nat (int l - int i) = 0"

  1006     from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)

  1007     assume c: "i \<noteq> l"

  1008     from c a show "fmul (Rep_matrix A k j) e = 0" by blast

  1009   qed

  1010

  1011 lemma mult_matrix_ext:

  1012   assumes

  1013   eprem:

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

  1015   and fprems:

  1016   "! a. fmul 0 a = 0"

  1017   "! a. fmul a 0 = 0"

  1018   "! a. fadd a 0 = a"

  1019   "! a. fadd 0 a = a"

  1020   and contraprems:

  1021   "mult_matrix fmul fadd A = mult_matrix fmul fadd B"

  1022   shows

  1023   "A = B"

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

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

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

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

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

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

  1030     by (simp add: Rep_matrix_inject a)

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

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

  1033   let ?S = "singleton_matrix I 0 e"

  1034   let ?comp = "mult_matrix fmul fadd"

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

  1036   have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)

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

  1038     apply (rule notI)

  1039     apply (simp add: fprems eprops)

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

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

  1042     by (simp add: e c eprops)

  1043   with contraprems show "False" by simp

  1044 qed

  1045

  1046 constdefs

  1047   foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"

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

  1049   foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"

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

  1051

  1052 lemma foldmatrix_transpose:

  1053   assumes

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

  1055   shows

  1056   "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)

  1057 proof -

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

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

  1060     apply (induct n)

  1061     apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+

  1062     apply (auto)

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

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

  1065     apply (simp add: foldmatrix_def foldmatrix_transposed_def)

  1066     apply (induct m, simp)

  1067     apply (simp)

  1068     apply (insert tworows)

  1069     apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)

  1070     by (simp add: foldmatrix_def foldmatrix_transposed_def)

  1071 qed

  1072

  1073 lemma foldseq_foldseq:

  1074 assumes

  1075   "associative f"

  1076   "associative g"

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

  1078 shows

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

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

  1081   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)

  1082

  1083 lemma mult_n_nrows:

  1084 assumes

  1085 "! a. fmul 0 a = 0"

  1086 "! a. fmul a 0 = 0"

  1087 "fadd 0 0 = 0"

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

  1089 apply (subst nrows_le)

  1090 apply (simp add: mult_matrix_n_def)

  1091 apply (subst RepAbs_matrix)

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

  1093 apply (simp add: nrows prems foldseq_zero)

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

  1095 apply (simp add: ncols prems foldseq_zero)

  1096 by (simp add: nrows prems foldseq_zero)

  1097

  1098 lemma mult_n_ncols:

  1099 assumes

  1100 "! a. fmul 0 a = 0"

  1101 "! a. fmul a 0 = 0"

  1102 "fadd 0 0 = 0"

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

  1104 apply (subst ncols_le)

  1105 apply (simp add: mult_matrix_n_def)

  1106 apply (subst RepAbs_matrix)

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

  1108 apply (simp add: nrows prems foldseq_zero)

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

  1110 apply (simp add: ncols prems foldseq_zero)

  1111 by (simp add: ncols prems foldseq_zero)

  1112

  1113 lemma mult_nrows:

  1114 assumes

  1115 "! a. fmul 0 a = 0"

  1116 "! a. fmul a 0 = 0"

  1117 "fadd 0 0 = 0"

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

  1119 by (simp add: mult_matrix_def mult_n_nrows prems)

  1120

  1121 lemma mult_ncols:

  1122 assumes

  1123 "! a. fmul 0 a = 0"

  1124 "! a. fmul a 0 = 0"

  1125 "fadd 0 0 = 0"

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

  1127 by (simp add: mult_matrix_def mult_n_ncols prems)

  1128

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

  1130   apply (auto simp add: nrows_le)

  1131   apply (rule nrows)

  1132   apply (arith)

  1133   done

  1134

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

  1136   apply (auto simp add: ncols_le)

  1137   apply (rule ncols)

  1138   apply (arith)

  1139   done

  1140

  1141 lemma mult_matrix_assoc:

  1142   assumes prems:

  1143   "! a. fmul1 0 a = 0"

  1144   "! a. fmul1 a 0 = 0"

  1145   "! a. fmul2 0 a = 0"

  1146   "! a. fmul2 a 0 = 0"

  1147   "fadd1 0 0 = 0"

  1148   "fadd2 0 0 = 0"

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

  1150   "associative fadd1"

  1151   "associative fadd2"

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

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

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

  1155   shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" (is ?concl)

  1156 proof -

  1157   have comb_left:  "!! A B x y. A = B \<Longrightarrow> (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast

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

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

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

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

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

  1163   show ?concl

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

  1165     apply (rule ext)+

  1166     apply (simp add: mult_matrix_def)

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

  1168     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

  1169     apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

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

  1171     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

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

  1173     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

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

  1175     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

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

  1177     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+

  1178     apply (simp add: mult_matrix_n_def)

  1179     apply (rule comb_left)

  1180     apply ((rule ext)+, simp)

  1181     apply (simplesubst RepAbs_matrix)

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

  1183     apply (simp add: nrows prems foldseq_zero)

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

  1185     apply (simp add: prems ncols foldseq_zero)

  1186     apply (subst RepAbs_matrix)

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

  1188     apply (simp add: nrows prems foldseq_zero)

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

  1190     apply (simp add: prems ncols foldseq_zero)

  1191     apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)

  1192     apply (subst foldseq_foldseq)

  1193     apply (simp add: prems)+

  1194     by (simp add: transpose_infmatrix)

  1195 qed

  1196

  1197 lemma

  1198   assumes prems:

  1199   "! a. fmul1 0 a = 0"

  1200   "! a. fmul1 a 0 = 0"

  1201   "! a. fmul2 0 a = 0"

  1202   "! a. fmul2 a 0 = 0"

  1203   "fadd1 0 0 = 0"

  1204   "fadd2 0 0 = 0"

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

  1206   "associative fadd1"

  1207   "associative fadd2"

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

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

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

  1211   shows

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

  1213 apply (rule ext)+

  1214 apply (simp add: comp_def )

  1215 by (simp add: mult_matrix_assoc prems)

  1216

  1217 lemma mult_matrix_assoc_simple:

  1218   assumes prems:

  1219   "! a. fmul 0 a = 0"

  1220   "! a. fmul a 0 = 0"

  1221   "fadd 0 0 = 0"

  1222   "associative fadd"

  1223   "commutative fadd"

  1224   "associative fmul"

  1225   "distributive fmul fadd"

  1226   shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" (is ?concl)

  1227 proof -

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

  1229     by (simp! add: associative_def commutative_def)

  1230   then show ?concl

  1231     apply (subst mult_matrix_assoc)

  1232     apply (simp_all!)

  1233     by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+

  1234 qed

  1235

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

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

  1238 apply (rule ext)+

  1239 by simp

  1240

  1241 lemma transpose_combine_matrix: "f 0 0 = 0 \<Longrightarrow> transpose_matrix (combine_matrix f A B) = combine_matrix f (transpose_matrix A) (transpose_matrix B)"

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

  1243 apply (rule ext)+

  1244 by simp

  1245

  1246 lemma Rep_mult_matrix:

  1247   assumes

  1248   "! a. fmul 0 a = 0"

  1249   "! a. fmul a 0 = 0"

  1250   "fadd 0 0 = 0"

  1251   shows

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

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

  1254 apply (simp add: mult_matrix_def mult_matrix_n_def)

  1255 apply (subst RepAbs_matrix)

  1256 apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)

  1257 apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)

  1258 by simp

  1259

  1260 lemma transpose_mult_matrix:

  1261   assumes

  1262   "! a. fmul 0 a = 0"

  1263   "! a. fmul a 0 = 0"

  1264   "fadd 0 0 = 0"

  1265   "! x y. fmul y x = fmul x y"

  1266   shows

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

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

  1269   apply (rule ext)+

  1270   by (simp! add: Rep_mult_matrix max_ac)

  1271

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

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

  1274 apply (rule ext)+

  1275 by simp

  1276

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

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

  1279 apply (rule ext)+

  1280 by simp

  1281

  1282 instance matrix :: ("{ord, zero}") ord

  1283   le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"

  1284   less_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..

  1285

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

  1287 apply intro_classes

  1288 apply (simp_all add: le_matrix_def less_def)

  1289 apply (auto)

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

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

  1292 apply (simp)

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

  1294 apply (rule ext)+

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

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

  1297 by simp

  1298

  1299 lemma le_apply_matrix:

  1300   assumes

  1301   "f 0 = 0"

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

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

  1304   shows

  1305   "apply_matrix f a <= apply_matrix f b"

  1306   by (simp! add: le_matrix_def)

  1307

  1308 lemma le_combine_matrix:

  1309   assumes

  1310   "f 0 0 = 0"

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

  1312   "A <= B"

  1313   "C <= D"

  1314   shows

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

  1316 by (simp! add: le_matrix_def)

  1317

  1318 lemma le_left_combine_matrix:

  1319   assumes

  1320   "f 0 0 = 0"

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

  1322   "A <= B"

  1323   shows

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

  1325   by (simp! add: le_matrix_def)

  1326

  1327 lemma le_right_combine_matrix:

  1328   assumes

  1329   "f 0 0 = 0"

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

  1331   "A <= B"

  1332   shows

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

  1334   by (simp! add: le_matrix_def)

  1335

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

  1337   by (simp add: le_matrix_def, auto)

  1338

  1339 lemma le_foldseq:

  1340   assumes

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

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

  1343   shows

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

  1345 proof -

  1346   have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!)

  1347   then show "foldseq f s n <= foldseq f t n" by (simp!)

  1348 qed

  1349

  1350 lemma le_left_mult:

  1351   assumes

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

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

  1354   "! a. fmul 0 a = 0"

  1355   "! a. fmul a 0 = 0"

  1356   "fadd 0 0 = 0"

  1357   "0 <= C"

  1358   "A <= B"

  1359   shows

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

  1361   apply (simp! add: le_matrix_def Rep_mult_matrix)

  1362   apply (auto)

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

  1364   apply (rule le_foldseq)

  1365   by (auto)

  1366

  1367 lemma le_right_mult:

  1368   assumes

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

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

  1371   "! a. fmul 0 a = 0"

  1372   "! a. fmul a 0 = 0"

  1373   "fadd 0 0 = 0"

  1374   "0 <= C"

  1375   "A <= B"

  1376   shows

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

  1378   apply (simp! add: le_matrix_def Rep_mult_matrix)

  1379   apply (auto)

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

  1381   apply (rule le_foldseq)

  1382   by (auto)

  1383

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

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

  1386

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

  1388   by (auto simp add: le_matrix_def)

  1389

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

  1391   apply (auto)

  1392   apply (simp add: le_matrix_def)

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

  1394   apply (simp)

  1395   apply (simp add: le_matrix_def)

  1396   done

  1397

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

  1399   apply (auto)

  1400   apply (simp add: le_matrix_def)

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

  1402   apply (simp)

  1403   apply (simp add: le_matrix_def)

  1404   done

  1405

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

  1407   apply (auto simp add: le_matrix_def neg_def)

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

  1409   apply (auto)

  1410   done

  1411

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

  1413   apply (auto simp add: le_matrix_def neg_def)

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

  1415   apply (auto)

  1416   done

  1417

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

  1419   apply (auto simp add: le_matrix_def neg_def)

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

  1421   apply (auto)

  1422   done

  1423

  1424 end