author haftmann Fri, 18 Jul 2008 18:25:57 +0200 changeset 27653 180e28bab764 parent 27652 818666de6c24 child 27654 0f8e2dcabbf9
more class instantiations
 src/HOL/Matrix/Matrix.thy file | annotate | diff | comparison | revisions src/HOL/Matrix/SparseMatrix.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Matrix/Matrix.thy	Fri Jul 18 18:25:56 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 18 18:25:57 2008 +0200
@@ -1489,7 +1489,7 @@

end

+instantiation matrix :: ("{lattice, uminus, zero}") abs
begin

definition
@@ -1499,14 +1499,29 @@

end

-proof
-  fix A B C :: "('a::lordered_ab_group_add) matrix"
+proof
+  fix A B C :: "'a matrix"
show "A + B + C = A + (B + C)"
apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
done
+  show "0 + A = A"
+    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
+    apply (simp)
+    done
+  show "A + 0 = A"
+    apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec])
+    apply (simp)
+    done
+qed
+
+proof
+  fix A B :: "'a matrix"
show "A + B = B + A"
apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
@@ -1517,10 +1532,29 @@
apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
apply (simp)
done
+qed
+
+proof
+  fix A B :: "'a matrix"
+  show "- A + A = 0"
+    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
+  show "A - B = A + - B"
+    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)
+qed
+
+proof
+  fix A B :: "'a matrix"
show "- A + A = 0"
by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
show "A - B = A + - B"
by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
+qed
+
+proof
+  fix A B C :: "'a matrix"
assume "A <= B"
then show "C + A <= C + B"
@@ -1528,10 +1562,13 @@
apply (simp_all)
done
qed
+

-instance matrix :: (lordered_ring) lordered_ring
+instance matrix :: (ring) ring
proof
-  fix A B C :: "('a :: lordered_ring) matrix"
+  fix A B C :: "'a matrix"
show "A * B * C = A * (B * C)"
apply (rule mult_matrix_assoc)
@@ -1546,9 +1583,12 @@
apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
apply (simp_all add: associative_def commutative_def ring_simps)
-    done
-  show "abs A = sup A (-A)"
+    done
+qed
+
+instance matrix :: (pordered_ring) pordered_ring
+proof
+  fix A B C :: "'a matrix"
assume a: "A \<le> B"
assume b: "0 \<le> C"
from a b show "C * A \<le> C * B"
@@ -1561,34 +1601,42 @@
apply (rule le_right_mult)
done
-qed
+qed
+
+instance matrix :: (lordered_ring) lordered_ring
+proof
+  fix A B C :: "('a :: lordered_ring) matrix"
+  show "abs A = sup A (-A)"
+qed

-  "Rep_matrix ((a::('a::lordered_ab_group_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
+  "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"

-lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i =
+lemma Rep_matrix_mult: "Rep_matrix ((a::('a::ring) matrix) * b) j i =
foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
done

-lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a) \<Longrightarrow> apply_matrix f ((a::('a::lordered_ab_group_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
+lemma apply_matrix_add: "! x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a)
+  \<Longrightarrow> apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
done

-lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
+lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
done

-lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
+lemma nrows_mult: "nrows ((A::('a::ring) matrix) * B) <= nrows A"

-lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
+lemma ncols_mult: "ncols ((A::('a::ring) matrix) * B) <= ncols B"

definition
@@ -1615,7 +1663,7 @@
ultimately show "?r = n" by simp
qed

-lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
+lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{ring_1}) matrix) * (one_matrix n) = A"
apply (subst Rep_matrix_inject[THEN sym])
apply (rule ext)+
@@ -1623,7 +1671,7 @@
apply (simp_all)

-lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
+lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
apply (subst Rep_matrix_inject[THEN sym])
apply (rule ext)+
@@ -1631,27 +1679,27 @@
apply (simp_all)

-lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
+lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
apply (subst transpose_mult_matrix)
done

-lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
+lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"

-lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
+lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"

constdefs
-  right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
+  right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
"right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A"
-  left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
+  left_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
"left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A"
-  inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
+  inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
"inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"

lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
@@ -1699,13 +1747,13 @@
apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
done

-lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
+lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
apply (rule combine_nrows)
apply (simp_all)
done

-lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
+lemma move_matrix_row_mult: "move_matrix ((A::('a::ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (auto simp add: Rep_matrix_mult foldseq_zero)
@@ -1716,7 +1764,7 @@
done

-lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
+lemma move_matrix_col_mult: "move_matrix ((A::('a::ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (auto simp add: Rep_matrix_mult foldseq_zero)
@@ -1727,17 +1775,17 @@
done

-lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)"
+lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)"
apply (subst Rep_matrix_inject[symmetric])
apply (rule ext)+
apply (simp)
done

-lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
+lemma move_matrix_mult: "move_matrix ((A::('a::ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)

constdefs
-  scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
+  scalar_mult :: "('a::ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
"scalar_mult a m == apply_matrix (op * a) m"

lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"
@@ -1755,10 +1803,10 @@
apply (auto)
done

-lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group_add)) x y = - (Rep_matrix A x y)"
+lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"

-lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
+lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ab_group_add)) x y = abs (Rep_matrix A x y)"

end```
```--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Jul 18 18:25:56 2008 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Jul 18 18:25:57 2008 +0200
@@ -4,17 +4,17 @@
*)

theory SparseMatrix
-imports Matrix
+imports "./Matrix"
begin

types
'a spvec = "(nat * 'a) list"
'a spmat = "('a spvec) spvec"

-definition sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix" where
+definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"

-definition sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix" where
+definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"

code_datatype sparse_row_vector sparse_row_matrix
@@ -30,14 +30,16 @@
lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
by (induct l, auto)

-lemma sparse_row_vector_cons[simp]: "sparse_row_vector (a#arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
+lemma sparse_row_vector_cons[simp]:
+  "sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
apply (induct arr)
-  apply (simp add: foldl_distrstart[of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
+  apply (simp add: foldl_distrstart [of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
done

-lemma sparse_row_vector_append[simp]: "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
-  by (induct a, auto)
+lemma sparse_row_vector_append[simp]:
+  "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
+  by (induct a) auto

lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
apply (induct x)
@@ -56,17 +58,13 @@
done

-consts
-  sorted_spvec :: "'a spvec \<Rightarrow> bool"
-  sorted_spmat :: "'a spmat \<Rightarrow> bool"
+primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
+  "sorted_spvec [] = True"
+  | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))"

-primrec
+primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
"sorted_spmat [] = True"
-  "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
-
-primrec
-  "sorted_spvec [] = True"
-sorted_spvec_step:  "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))"
+  | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"

declare sorted_spvec.simps [simp del]

@@ -102,14 +100,11 @@
done

-consts
-  smult_spvec :: "('a::lordered_ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
-
-primrec minus_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
+primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
"minus_spvec [] = []"
| "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"

-primrec abs_spvec ::  "('a::lordered_ring) spvec \<Rightarrow> 'a spvec" where
+primrec abs_spvec ::  "('a::lordered_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
"abs_spvec [] = []"
| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"

@@ -122,10 +117,14 @@
apply simp
done

+apply default
+unfolding abs_matrix_def .. (*FIXME move*)
+
lemma sparse_row_vector_abs:
-  "sorted_spvec v \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
+  "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
apply (induct v)
+  apply simp_all
apply (frule_tac sorted_spvec_cons1, simp)
apply (simp only: Rep_matrix_inject[symmetric])
apply (rule ext)+
@@ -152,8 +151,8 @@
done

-defs
-  smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr"
+definition
+  "smult_spvec y = map (% a. (fst a, y * snd a))"

lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
@@ -161,7 +160,7 @@
lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"

-consts addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
+consts addmult_spvec :: "('a::ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
"addmult_spvec (y, arr, []) = arr"
"addmult_spvec (y, [], brr) = smult_spvec y brr"
@@ -951,7 +950,7 @@

lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)

-lemma sparse_row_vector_pprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
+lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
apply (induct v)
apply (simp_all)
apply (frule sorted_spvec_cons1, auto)
@@ -961,7 +960,7 @@
apply auto
done

-lemma sparse_row_vector_nprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
+lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
apply (induct v)
apply (simp_all)
apply (frule sorted_spvec_cons1, auto)
@@ -988,7 +987,7 @@
apply (simp)
done

-lemma sparse_row_matrix_pprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
+lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
apply (induct m)
apply simp
apply simp
@@ -1004,7 +1003,7 @@