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