src/HOL/Matrix/Matrix.thy
changeset 35416 d8d7d1b785af
parent 35032 7efe662e41b4
child 35612 0a9fb49a086d
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -24,10 +24,10 @@
     1.4  apply (rule Abs_matrix_induct)
     1.5  by (simp add: Abs_matrix_inverse matrix_def)
     1.6  
     1.7 -constdefs
     1.8 -  nrows :: "('a::zero) matrix \<Rightarrow> nat"
     1.9 +definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where
    1.10    "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
    1.11 -  ncols :: "('a::zero) matrix \<Rightarrow> nat"
    1.12 +
    1.13 +definition ncols :: "('a::zero) matrix \<Rightarrow> nat" where
    1.14    "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
    1.15  
    1.16  lemma nrows:
    1.17 @@ -50,10 +50,10 @@
    1.18    thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
    1.19  qed
    1.20  
    1.21 -constdefs
    1.22 -  transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
    1.23 +definition transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix" where
    1.24    "transpose_infmatrix A j i == A i j"
    1.25 -  transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix"
    1.26 +
    1.27 +definition transpose_matrix :: "('a::zero) matrix \<Rightarrow> 'a matrix" where
    1.28    "transpose_matrix == Abs_matrix o transpose_infmatrix o Rep_matrix"
    1.29  
    1.30  declare transpose_infmatrix_def[simp]
    1.31 @@ -256,14 +256,16 @@
    1.32    ultimately show "finite ?u" by (rule finite_subset)
    1.33  qed
    1.34  
    1.35 -constdefs
    1.36 -  apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
    1.37 +definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where
    1.38    "apply_infmatrix f == % A. (% j i. f (A j i))"
    1.39 -  apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
    1.40 +
    1.41 +definition apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix" where
    1.42    "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
    1.43 -  combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
    1.44 +
    1.45 +definition combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix" where
    1.46    "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
    1.47 -  combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
    1.48 +
    1.49 +definition combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix" where
    1.50    "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
    1.51  
    1.52  lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
    1.53 @@ -272,10 +274,10 @@
    1.54  lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
    1.55  by (simp add: combine_infmatrix_def)
    1.56  
    1.57 -constdefs
    1.58 -commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
    1.59 +definition commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.60  "commutative f == ! x y. f x y = f y x"
    1.61 -associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
    1.62 +
    1.63 +definition associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where
    1.64  "associative f == ! x y z. f (f x y) z = f x (f y z)"
    1.65  
    1.66  text{*
    1.67 @@ -356,12 +358,13 @@
    1.68  lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
    1.69    by (simp add: ncols_le)
    1.70  
    1.71 -constdefs
    1.72 -  zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool"
    1.73 +definition zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool" where
    1.74    "zero_r_neutral f == ! a. f a 0 = a"
    1.75 -  zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
    1.76 +
    1.77 +definition zero_l_neutral :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where
    1.78    "zero_l_neutral f == ! a. f 0 a = a"
    1.79 -  zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool"
    1.80 +
    1.81 +definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where
    1.82    "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
    1.83  
    1.84  consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    1.85 @@ -648,10 +651,10 @@
    1.86    then show ?concl by simp
    1.87  qed
    1.88  
    1.89 -constdefs
    1.90 -  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"
    1.91 +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
    1.92    "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)"
    1.93 -  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"
    1.94 +
    1.95 +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
    1.96    "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
    1.97  
    1.98  lemma mult_matrix_n:
    1.99 @@ -673,12 +676,13 @@
   1.100    finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
   1.101  qed
   1.102  
   1.103 -constdefs
   1.104 -  r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   1.105 +definition r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool" where
   1.106    "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
   1.107 -  l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   1.108 +
   1.109 +definition l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.110    "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
   1.111 -  distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   1.112 +
   1.113 +definition distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.114    "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
   1.115  
   1.116  lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
   1.117 @@ -835,20 +839,22 @@
   1.118    apply (simp add: apply_matrix_def apply_infmatrix_def)
   1.119    by (simp add: zero_matrix_def)
   1.120  
   1.121 -constdefs
   1.122 -  singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix"
   1.123 +definition singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix" where
   1.124    "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
   1.125 -  move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix"
   1.126 +
   1.127 +definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where
   1.128    "move_matrix A y x == Abs_matrix(% j i. if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
   1.129 -  take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   1.130 +
   1.131 +definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   1.132    "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
   1.133 -  take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   1.134 +
   1.135 +definition take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   1.136    "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
   1.137  
   1.138 -constdefs
   1.139 -  column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   1.140 +definition column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   1.141    "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
   1.142 -  row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   1.143 +
   1.144 +definition row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   1.145    "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
   1.146  
   1.147  lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
   1.148 @@ -1042,10 +1048,10 @@
   1.149    with contraprems show "False" by simp
   1.150  qed
   1.151  
   1.152 -constdefs
   1.153 -  foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
   1.154 +definition foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
   1.155    "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
   1.156 -  foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
   1.157 +
   1.158 +definition foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
   1.159    "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
   1.160  
   1.161  lemma foldmatrix_transpose:
   1.162 @@ -1691,12 +1697,13 @@
   1.163  lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"
   1.164  by (simp add: minus_matrix_def transpose_apply_matrix)
   1.165  
   1.166 -constdefs 
   1.167 -  right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.168 +definition right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
   1.169    "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
   1.170 -  left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.171 +
   1.172 +definition left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
   1.173    "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" 
   1.174 -  inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   1.175 +
   1.176 +definition inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
   1.177    "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
   1.178  
   1.179  lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   1.180 @@ -1781,8 +1788,7 @@
   1.181  lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
   1.182  by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   1.183  
   1.184 -constdefs
   1.185 -  scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   1.186 +definition scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
   1.187    "scalar_mult a m == apply_matrix (op * a) m"
   1.188  
   1.189  lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"