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