# HG changeset patch
# User obua
# Date 1087215655 -7200
# Node ID b9ab8babd8b348a44f144315766b32bf60b62118
# Parent  29fe4a9a7cb5c0d6e1eee0f278a3517846020bf2
Further development of matrix theory

diff -r 29fe4a9a7cb5 -r b9ab8babd8b3 src/HOL/Matrix/LinProg.thy
--- a/src/HOL/Matrix/LinProg.thy	Sun Jun 13 17:57:35 2004 +0200
+++ b/src/HOL/Matrix/LinProg.thy	Mon Jun 14 14:20:55 2004 +0200
@@ -48,7 +48,7 @@
 
 lemma linprog_by_duality_approx:
   assumes
-  "(A + dA) * x <= (b::('a::pordered_matrix_element) matrix)"
+  "(A + dA) * x <= (b::('a::lordered_ring) matrix)"
   "y * A = c"
   "0 <= y"
   shows
@@ -56,17 +56,17 @@
 apply (simp add: times_matrix_def plus_matrix_def)
 apply (rule linprog_by_duality_approx_general)
 apply (simp_all)
-apply (simp_all add: associative_def matrix_add_assoc matrix_mult_assoc)
-apply (simp_all add: commutative_def matrix_add_commute)
-apply (simp_all add: distributive_def l_distributive_def r_distributive_def matrix_left_distrib matrix_right_distrib)
+apply (simp_all add: associative_def add_assoc mult_assoc)
+apply (simp_all add: commutative_def add_commute)
+apply (simp_all add: distributive_def l_distributive_def r_distributive_def left_distrib right_distrib)
 apply (simp_all! add: plus_matrix_def times_matrix_def)
-apply (simp add: pordered_add)
-apply (simp add: pordered_mult_left)
+apply (simp add: add_mono)
+apply (simp add: mult_left_mono)
 done
 
 lemma linprog_by_duality:
   assumes
-  "A * x <= (b::('a::pordered_g_semiring) matrix)"
+  "A * x <= (b::('a::lordered_ring) matrix)"
   "y * A = c"
   "0 <= y"
   shows
diff -r 29fe4a9a7cb5 -r b9ab8babd8b3 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Sun Jun 13 17:57:35 2004 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Mon Jun 14 14:20:55 2004 +0200
@@ -1,201 +1,127 @@
 (*  Title:      HOL/Matrix/Matrix.thy
     ID:         $Id$
     Author:     Steven Obua
-    License:    2004 Technische Universität München
 *)
 
-theory Matrix = MatrixGeneral:
+theory Matrix=MatrixGeneral:
+
+instance matrix :: (minus) minus 
+by intro_classes
+
+instance matrix :: (plus) plus
+by (intro_classes)
 
-axclass almost_matrix_element < zero, plus, times
-matrix_add_assoc: "(a+b)+c = a + (b+c)"
-matrix_add_commute: "a+b = b+a"
+instance matrix :: ("{plus,times}") times
+by (intro_classes)
+
+defs (overloaded)
+  plus_matrix_def: "A + B == combine_matrix (op +) A B"
+  diff_matrix_def: "A - B == combine_matrix (op -) A B"
+  minus_matrix_def: "- A == apply_matrix uminus A"
+  times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
+
+lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
+by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
 
-matrix_mult_assoc: "(a*b)*c = a*(b*c)"
-matrix_mult_left_0[simp]: "0 * a = 0"
-matrix_mult_right_0[simp]: "a * 0 = 0"
-
-matrix_left_distrib: "(a+b)*c = a*c+b*c"
-matrix_right_distrib: "a*(b+c) = a*b+a*c"
-
-axclass matrix_element < almost_matrix_element
-matrix_add_0[simp]: "0+0 = 0"
-
-instance matrix :: (plus) plus ..
-instance matrix :: (times) times ..
+instance matrix :: (lordered_ab_group) lordered_ab_group_meet
+proof 
+  fix A B C :: "('a::lordered_ab_group) matrix"
+  show "A + B + C = A + (B + C)"    
+    apply (simp add: plus_matrix_def)
+    apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
+    apply (simp_all add: add_assoc)
+    done
+  show "A + B = B + A"
+    apply (simp add: plus_matrix_def)
+    apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
+    apply (simp_all add: add_commute)
+    done
+  show "0 + A = A"
+    apply (simp add: plus_matrix_def)
+    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
+    apply (simp)
+    done
+  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)
+  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
+    by (auto intro: is_meet_combine_matrix_meet)
+  assume "A <= B"
+  then show "C + A <= C + B"
+    apply (simp add: plus_matrix_def)
+    apply (rule le_left_combine_matrix)
+    apply (simp_all)
+    done
+qed
 
 defs (overloaded)
-plus_matrix_def: "A + B == combine_matrix (op +) A B"
-times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
+  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
 
-instance matrix :: (matrix_element) matrix_element
-proof -
-  note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]
-  {
-    fix A::"('a::matrix_element) matrix"
-    fix B
-    fix C
-    have "(A + B) + C = A + (B + C)"
-      apply (simp add: plus_matrix_def)
-      apply (rule combine_matrix_assoc2)
-      by (simp_all add: matrix_add_assoc)
-  }
-  note plus_assoc = this
-  {
-    fix A::"('a::matrix_element) matrix"
-    fix B
-    fix C
-    have "(A * B) * C = A * (B * C)"
-      apply (simp add: times_matrix_def)
-      apply (rule mult_matrix_assoc_simple)
-      apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def)
-      apply (auto)
-      apply (simp_all add: matrix_add_assoc)
-      apply (simp_all add: matrix_add_commute)
-      apply (simp_all add: matrix_mult_assoc)
-      by (simp_all add: matrix_left_distrib matrix_right_distrib)
-  }
-  note mult_assoc = this
-  note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]
-  {
-    fix A::"('a::matrix_element) matrix"
-    fix B
-    have "A + B = B + A"
-      apply (simp add: plus_matrix_def)
-      apply (insert combine_matrix_commute2[of "op +"])
-      apply (rule combine_matrix_commute2)
-      by (simp add: matrix_add_commute)
-  }
-  note plus_commute = this
-  have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0"
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_zero)
-    by (simp)
-  have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def)
-  have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
-  note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
-  {
-    fix A::"('a::matrix_element) matrix"
-    fix B
-    fix C
-    have "(A + B) * C = A * C + B * C"
-      apply (simp add: plus_matrix_def)
-      apply (simp add: times_matrix_def)
-      apply (rule l_distributive_matrix2)
-      apply (simp_all add: associative_def commutative_def l_distributive_def)
-      apply (auto)
-      apply (simp_all add: matrix_add_assoc)
-      apply (simp_all add: matrix_add_commute)
-      by (simp_all add: matrix_left_distrib)
-  }
-  note left_distrib = this
-  note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
-  {
-    fix A::"('a::matrix_element) matrix"
-    fix B
-    fix C
-    have "C * (A + B) = C * A + C * B"
-      apply (simp add: plus_matrix_def)
-      apply (simp add: times_matrix_def)
-      apply (rule r_distributive_matrix2)
-      apply (simp_all add: associative_def commutative_def r_distributive_def)
-      apply (auto)
-      apply (simp_all add: matrix_add_assoc)
-      apply (simp_all add: matrix_add_commute)
-      by (simp_all add: matrix_right_distrib)
-  }
-  note right_distrib = this
-  show "OFCLASS('a matrix, matrix_element_class)"
-    apply (intro_classes)
-    apply (simp_all add: plus_assoc)
-    apply (simp_all add: plus_commute)
-    apply (simp_all add: plus_zero)
-    apply (simp_all add: mult_assoc)
-    apply (simp_all add: mult_left_zero mult_right_zero)
-    by (simp_all add: left_distrib right_distrib)
+instance matrix :: (lordered_ring) lordered_ring
+proof
+  fix A B C :: "('a :: lordered_ring) matrix"
+  show "A * B * C = A * (B * C)"
+    apply (simp add: times_matrix_def)
+    apply (rule mult_matrix_assoc)
+    apply (simp_all add: associative_def ring_eq_simps)
+    done
+  show "(A + B) * C = A * C + B * C"
+    apply (simp add: times_matrix_def plus_matrix_def)
+    apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
+    apply (simp_all add: associative_def commutative_def ring_eq_simps)
+    done
+  show "A * (B + C) = A * B + A * C"
+    apply (simp add: times_matrix_def plus_matrix_def)
+    apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
+    apply (simp_all add: associative_def commutative_def ring_eq_simps)
+    done  
+  show "abs A = join A (-A)" 
+    by (simp add: abs_matrix_def)
+  assume a: "A \<le> B"
+  assume b: "0 \<le> C"
+  from a b show "C * A \<le> C * B"
+    apply (simp add: times_matrix_def)
+    apply (rule le_left_mult)
+    apply (simp_all add: add_mono mult_left_mono)
+    done
+  from a b show "A * C \<le> B * C"
+    apply (simp add: times_matrix_def)
+    apply (rule le_right_mult)
+    apply (simp_all add: add_mono mult_right_mono)
+    done
 qed
 
-axclass g_almost_semiring < almost_matrix_element
-g_add_left_0[simp]: "0 + a = a"
-
-lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a"
-by (simp add: matrix_add_commute)
-
-axclass g_semiring < g_almost_semiring
-g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
-
-instance g_almost_semiring < matrix_element
-  by intro_classes simp
-
-instance matrix :: (g_almost_semiring) g_almost_semiring
-apply (intro_classes)
-by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
+lemma Rep_matrix_add[simp]: "Rep_matrix ((a::('a::lordered_ab_group)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
+by (simp add: plus_matrix_def)
 
-lemma RepAbs_matrix_eq_left: " Rep_matrix(Abs_matrix f) = g \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> f = g"
-by (simp add: RepAbs_matrix)
-
-lemma RepAbs_matrix_eq_right: "g = Rep_matrix(Abs_matrix f) \<Longrightarrow> \<exists>m. \<forall>j i. m \<le> j \<longrightarrow> f j i = 0 \<Longrightarrow> \<exists>n. \<forall>j i. n \<le> i \<longrightarrow> f j i = 0 \<Longrightarrow> g = f"
-by (simp add: RepAbs_matrix)
+lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
+  foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
+apply (simp add: times_matrix_def)
+apply (simp add: Rep_mult_matrix)
+done
+ 
 
-instance matrix :: (g_semiring) g_semiring
-apply (intro_classes)
-apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
-apply (subst Rep_matrix_inject[THEN sym])
-apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"])
-apply (drule RepAbs_matrix_eq_left)
-apply (auto)
-apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le)
-apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le)
-apply (drule RepAbs_matrix_eq_right)
-apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le)
-apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le)
+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) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
+apply (subst Rep_matrix_inject[symmetric])
 apply (rule ext)+
-apply (drule_tac x="x" and y="x" in comb, simp)
-apply (drule_tac x="xa" and y="xa" in comb, simp)
-apply (drule g_add_leftimp_eq)
-by simp
-
-axclass pordered_matrix_element < matrix_element, order, zero
-pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c"
-pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b"
-pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c"
-
-lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b"
-apply (insert pordered_add_right_mono[of a b c])
-by (simp add: matrix_add_commute)
+apply (simp)
+done
 
-lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d"
-proof -
-  assume p1:"a <= b"
-  assume p2:"c <= d"
-  have "a+c <= b+c" by (rule pordered_add_right_mono)
-  also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
-  ultimately show "a+c <= b+d" by simp
-qed
+lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (simp)
+done
 
-instance matrix :: (pordered_matrix_element) pordered_matrix_element
-apply (intro_classes)
-apply (simp_all add: plus_matrix_def times_matrix_def)
-apply (rule le_combine_matrix)
-apply (simp_all)
-apply (simp_all add: pordered_add)
-apply (rule le_left_mult)
-apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0)
-apply (rule le_right_mult)
-by (simp_all add: pordered_add pordered_mult_right)
-
-axclass pordered_g_semiring < g_semiring, pordered_matrix_element
-
-instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
-
-lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
+lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
 by (simp add: times_matrix_def mult_nrows)
 
-lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
+lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
 by (simp add: times_matrix_def mult_ncols)
 
-(*
 constdefs
-  one_matrix :: "nat \<Rightarrow> ('a::comm_semiring_1_cancel) matrix"
+  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
   "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
 
 lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
@@ -204,21 +130,21 @@
 apply (rule exI[of _ n], simp add: split_if)+
 by (simp add: split_if, arith)
 
-lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _")
+lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
 proof -
   have "?r <= n" by (simp add: nrows_le)
-  moreover have "n <= ?r" by (simp add: le_nrows, arith)
+  moreover have "n <= ?r" by (simp add:le_nrows, arith)
   ultimately show "?r = n" by simp
 qed
 
-lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _")
+lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
 proof -
   have "?r <= n" by (simp add: ncols_le)
   moreover have "n <= ?r" by (simp add: le_ncols, arith)
   ultimately show "?r = n" by simp
 qed
 
-lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A"
+lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
 apply (subst Rep_matrix_inject[THEN sym])
 apply (rule ext)+
 apply (simp add: times_matrix_def Rep_mult_matrix)
@@ -226,7 +152,7 @@
 apply (simp_all)
 by (simp add: max_def ncols)
 
-lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A"
+lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
 apply (subst Rep_matrix_inject[THEN sym])
 apply (rule ext)+
 apply (simp add: times_matrix_def Rep_mult_matrix)
@@ -234,16 +160,131 @@
 apply (simp_all)
 by (simp add: max_def nrows)
 
-constdefs
-  right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
-  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
-  inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
-  "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
+lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
+apply (simp add: times_matrix_def)
+apply (subst transpose_mult_matrix)
+apply (simp_all add: mult_commute)
+done
+
+lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
+by (simp add: plus_matrix_def transpose_combine_matrix)
+
+lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
+by (simp add: diff_matrix_def transpose_combine_matrix)
+
+lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
+by (simp add: minus_matrix_def transpose_apply_matrix)
+
+constdefs 
+  right_inverse_matrix :: "('a::{lordered_ring, 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 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 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"
 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
 by (simp add: right_inverse_matrix_def)
 
-text {* to be continued \dots *}
-*)
+lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
+apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) 
+by (simp add: left_inverse_matrix_def)
+
+lemma left_right_inverse_matrix_unique: 
+  assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
+  shows "X = Y"
+proof -
+  have "Y = Y * one_matrix (nrows A)" 
+    apply (subst one_matrix_mult_right)
+    apply (insert prems)
+    by (simp_all add: left_inverse_matrix_def)
+  also have "\<dots> = Y * (A * X)" 
+    apply (insert prems)
+    apply (frule right_inverse_matrix_dim)
+    by (simp add: right_inverse_matrix_def)
+  also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
+  also have "\<dots> = X" 
+    apply (insert prems)
+    apply (frule left_inverse_matrix_dim)
+    apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
+    done
+  ultimately show "X = Y" by (simp)
+qed
+
+lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
+  by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
+
+lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
+  by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
+
+lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
+by auto
+
+lemma Rep_matrix_zero_imp_mult_zero:
+  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+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"
+apply (simp add: plus_matrix_def)
+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"
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (auto simp add: Rep_matrix_mult foldseq_zero)
+apply (rule_tac foldseq_zerotail[symmetric])
+apply (auto simp add: nrows zero_imp_mult_zero max2)
+apply (rule order_trans)
+apply (rule ncols_move_matrix_le)
+apply (simp add: max1)
+done
+
+lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_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)
+apply (rule_tac foldseq_zerotail[symmetric])
+apply (auto simp add: ncols zero_imp_mult_zero max1)
+apply (rule order_trans)
+apply (rule nrows_move_matrix_le)
+apply (simp add: max2)
+done
+
+lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::lordered_ab_group) 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)"
+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 m == apply_matrix (op * a) m"
+
+lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
+  by (simp add: scalar_mult_def)
+
+lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
+  by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
+
+lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
+  by (simp add: scalar_mult_def)
+
+lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
+  apply (subst Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply (auto)
+  done
+
+
+
+
 end
diff -r 29fe4a9a7cb5 -r b9ab8babd8b3 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Sun Jun 13 17:57:35 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Jun 14 14:20:55 2004 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Matrix/MatrixGeneral.thy
     ID:         $Id$
     Author:     Steven Obua
-    License:    2004 Technische Universitaet Muenchen
 *)
 
 theory MatrixGeneral = Main:
@@ -99,6 +98,22 @@
   ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
 qed
 
+lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
+
+lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
+apply (auto)
+apply (rule ext)+
+apply (simp add: transpose_infmatrix)
+apply (drule infmatrixforward)
+apply (simp)
+done
+
+lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
+apply (simp add: transpose_matrix_def)
+apply (subst Rep_matrix_inject[THEN sym])+
+apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
+done
+
 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
 by (simp add: transpose_matrix_def)
 
@@ -175,6 +190,16 @@
 apply (drule_tac x="nrows A" in spec)
 by (simp add: nrows)
 
+lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
+apply (case_tac "nrows A <= m")
+apply (simp_all add: nrows)
+done
+
+lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
+apply (case_tac "ncols A <= n")
+apply (simp_all add: ncols)
+done
+
 lemma finite_natarray1: "finite {x. x < (n::nat)}"
 apply (induct n)
 apply (simp)
@@ -768,6 +793,10 @@
   show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
 qed
 
+lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
+  by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
+
+
 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
   by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
 
@@ -800,6 +829,12 @@
   apply (simp add: combine_matrix_def combine_infmatrix_def)
   by (simp add: zero_matrix_def)
 
+lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
+apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
+apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
+apply (simp add: RepAbs_matrix)
+done
+
 lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
   apply (simp add: apply_matrix_def apply_infmatrix_def)
   by (simp add: zero_matrix_def)
@@ -828,6 +863,12 @@
 apply (rule exI[of _ "Suc n"], simp+)
 by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
 
+lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (simp)
+done
+
 lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
   by (simp add: singleton_matrix_def zero_matrix_def)
 
@@ -870,6 +911,11 @@
 apply (rule exI[of _ "Suc i"], simp)
 by simp
 
+lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
+apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
+apply (simp)
+done
+
 lemma Rep_move_matrix[simp]:
   "Rep_matrix (move_matrix A y x) 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)))"
@@ -879,6 +925,33 @@
   rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
   rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
 
+lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
+by (simp add: move_matrix_def)
+
+lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (simp)
+done
+
+lemma transpose_move_matrix[simp]:
+  "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
+apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
+apply (simp)
+done
+
+lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
+  (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
+  apply (subst Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply (case_tac "j + int u < 0")
+  apply (simp, arith)
+  apply (case_tac "i + int v < 0")
+  apply (simp add: neg_def, arith)
+  apply (simp add: neg_def)
+  apply arith
+  done
+
 lemma Rep_take_columns[simp]:
   "Rep_matrix (take_columns A c) j i =
   (if i < c then (Rep_matrix A j i) else 0)"
@@ -905,6 +978,16 @@
   "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   by (simp add: row_of_matrix_def)
 
+lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
+apply (subst Rep_matrix_inject[THEN sym])
+apply (rule ext)+
+by (simp add: ncols)
+
+lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
+apply (subst Rep_matrix_inject[THEN sym])
+apply (rule ext)+
+by (simp add: nrows)
+
 lemma mult_matrix_singleton_right[simp]:
   assumes prems:
   "! x. fmul x 0 = 0"
@@ -1052,6 +1135,18 @@
 shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
 by (simp add: mult_matrix_def mult_n_ncols prems)
 
+lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
+  apply (auto simp add: nrows_le)
+  apply (rule nrows)
+  apply (arith)
+  done
+
+lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
+  apply (auto simp add: ncols_le)
+  apply (rule ncols)
+  apply (arith)
+  done
+
 lemma mult_matrix_assoc:
   assumes prems:
   "! a. fmul1 0 a = 0"
@@ -1183,6 +1278,16 @@
   apply (rule ext)+
   by (simp! add: Rep_mult_matrix max_ac)
 
+lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
+apply (simp add:  Rep_matrix_inject[THEN sym])
+apply (rule ext)+
+by simp
+
+lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
+apply (simp add: Rep_matrix_inject[THEN sym])
+apply (rule ext)+
+by simp
+
 instance matrix :: ("{ord, zero}") ord ..
 
 defs (overloaded)
@@ -1224,8 +1329,7 @@
 lemma le_left_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b"
-  "0 <= C"
+  "! a b c. a <= b \<longrightarrow> f c a <= f c b"
   "A <= B"
   shows
   "combine_matrix f C A <= combine_matrix f C B"
@@ -1234,8 +1338,7 @@
 lemma le_right_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c"
-  "0 <= C"
+  "! a b c. a <= b \<longrightarrow> f a c <= f b c"
   "A <= B"
   shows
   "combine_matrix f A C <= combine_matrix f B C"
@@ -1258,7 +1361,7 @@
 lemma le_left_mult:
   assumes
   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
-  "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
+  "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
   "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
   "fadd 0 0 = 0"
@@ -1289,4 +1392,7 @@
   apply (rule le_foldseq)
   by (auto)
 
+lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"
+  by (auto simp add: le_matrix_def)
+
 end
diff -r 29fe4a9a7cb5 -r b9ab8babd8b3 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Sun Jun 13 17:57:35 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Jun 14 14:20:55 2004 +0200
@@ -27,6 +27,8 @@
 
 axclass semiring_0 \<subseteq> semiring, comm_monoid_add
 
+axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
+
 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
   mult_commute: "a * b = b * a"
   distrib: "(a + b) * c = a * c + b * c"
@@ -45,6 +47,10 @@
 
 instance comm_semiring_0 \<subseteq> semiring_0 ..
 
+axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
+
+instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
+
 axclass axclass_0_neq_1 \<subseteq> zero, one
   zero_neq_one [simp]: "0 \<noteq> 1"
 
@@ -57,20 +63,30 @@
 axclass axclass_no_zero_divisors \<subseteq> zero, times
   no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
+axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
+
+instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
+
 axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
 
+instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
+
+instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
+
 axclass ring \<subseteq> semiring, ab_group_add
 
-instance ring \<subseteq> semiring_0 ..
+instance ring \<subseteq> semiring_0_cancel ..
 
 axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
 
 instance comm_ring \<subseteq> ring ..
 
-instance comm_ring \<subseteq> comm_semiring_0 ..
+instance comm_ring \<subseteq> comm_semiring_0_cancel ..
 
 axclass ring_1 \<subseteq> ring, semiring_1
 
+instance ring_1 \<subseteq> semiring_1_cancel ..
+
 axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
 
 instance comm_ring_1 \<subseteq> ring_1 ..
@@ -83,7 +99,7 @@
   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
   divide_inverse:      "a / b = a * inverse b"
 
-lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"
+lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
 proof -
   have "0*a + 0*a = 0*a + 0"
     by (simp add: left_distrib [symmetric])
@@ -91,7 +107,7 @@
     by (simp only: add_left_cancel)
 qed
 
-lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"
+lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
 proof -
   have "a*0 + a*0 = a*0 + 0"
     by (simp add: right_distrib [symmetric])
@@ -155,10 +171,14 @@
 
 axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
 
+instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
+
 axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
   mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 
+instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
+
 instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring
 apply intro_classes
 apply (case_tac "a < b & 0 < c")
@@ -200,6 +220,10 @@
 
 axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
 
+instance lordered_ring \<subseteq> lordered_ab_group_meet ..
+
+instance lordered_ring \<subseteq> lordered_ab_group_join ..
+
 axclass axclass_abs_if \<subseteq> minus, ord, zero
   abs_if: "abs a = (if (a < 0) then (-a) else a)"