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