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