Further development of matrix theory
authorobua
Mon Jun 14 14:20:55 2004 +0200 (2004-06-14)
changeset 14940b9ab8babd8b3
parent 14939 29fe4a9a7cb5
child 14941 1edb674e0c33
Further development of matrix theory
src/HOL/Matrix/LinProg.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Matrix/LinProg.thy	Sun Jun 13 17:57:35 2004 +0200
     1.2 +++ b/src/HOL/Matrix/LinProg.thy	Mon Jun 14 14:20:55 2004 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  lemma linprog_by_duality_approx:
     1.6    assumes
     1.7 -  "(A + dA) * x <= (b::('a::pordered_matrix_element) matrix)"
     1.8 +  "(A + dA) * x <= (b::('a::lordered_ring) matrix)"
     1.9    "y * A = c"
    1.10    "0 <= y"
    1.11    shows
    1.12 @@ -56,17 +56,17 @@
    1.13  apply (simp add: times_matrix_def plus_matrix_def)
    1.14  apply (rule linprog_by_duality_approx_general)
    1.15  apply (simp_all)
    1.16 -apply (simp_all add: associative_def matrix_add_assoc matrix_mult_assoc)
    1.17 -apply (simp_all add: commutative_def matrix_add_commute)
    1.18 -apply (simp_all add: distributive_def l_distributive_def r_distributive_def matrix_left_distrib matrix_right_distrib)
    1.19 +apply (simp_all add: associative_def add_assoc mult_assoc)
    1.20 +apply (simp_all add: commutative_def add_commute)
    1.21 +apply (simp_all add: distributive_def l_distributive_def r_distributive_def left_distrib right_distrib)
    1.22  apply (simp_all! add: plus_matrix_def times_matrix_def)
    1.23 -apply (simp add: pordered_add)
    1.24 -apply (simp add: pordered_mult_left)
    1.25 +apply (simp add: add_mono)
    1.26 +apply (simp add: mult_left_mono)
    1.27  done
    1.28  
    1.29  lemma linprog_by_duality:
    1.30    assumes
    1.31 -  "A * x <= (b::('a::pordered_g_semiring) matrix)"
    1.32 +  "A * x <= (b::('a::lordered_ring) matrix)"
    1.33    "y * A = c"
    1.34    "0 <= y"
    1.35    shows
     2.1 --- a/src/HOL/Matrix/Matrix.thy	Sun Jun 13 17:57:35 2004 +0200
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon Jun 14 14:20:55 2004 +0200
     2.3 @@ -1,201 +1,127 @@
     2.4  (*  Title:      HOL/Matrix/Matrix.thy
     2.5      ID:         $Id$
     2.6      Author:     Steven Obua
     2.7 -    License:    2004 Technische Universität München
     2.8  *)
     2.9  
    2.10 -theory Matrix = MatrixGeneral:
    2.11 +theory Matrix=MatrixGeneral:
    2.12 +
    2.13 +instance matrix :: (minus) minus 
    2.14 +by intro_classes
    2.15 +
    2.16 +instance matrix :: (plus) plus
    2.17 +by (intro_classes)
    2.18  
    2.19 -axclass almost_matrix_element < zero, plus, times
    2.20 -matrix_add_assoc: "(a+b)+c = a + (b+c)"
    2.21 -matrix_add_commute: "a+b = b+a"
    2.22 +instance matrix :: ("{plus,times}") times
    2.23 +by (intro_classes)
    2.24 +
    2.25 +defs (overloaded)
    2.26 +  plus_matrix_def: "A + B == combine_matrix (op +) A B"
    2.27 +  diff_matrix_def: "A - B == combine_matrix (op -) A B"
    2.28 +  minus_matrix_def: "- A == apply_matrix uminus A"
    2.29 +  times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    2.30 +
    2.31 +lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
    2.32 +by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
    2.33  
    2.34 -matrix_mult_assoc: "(a*b)*c = a*(b*c)"
    2.35 -matrix_mult_left_0[simp]: "0 * a = 0"
    2.36 -matrix_mult_right_0[simp]: "a * 0 = 0"
    2.37 -
    2.38 -matrix_left_distrib: "(a+b)*c = a*c+b*c"
    2.39 -matrix_right_distrib: "a*(b+c) = a*b+a*c"
    2.40 -
    2.41 -axclass matrix_element < almost_matrix_element
    2.42 -matrix_add_0[simp]: "0+0 = 0"
    2.43 -
    2.44 -instance matrix :: (plus) plus ..
    2.45 -instance matrix :: (times) times ..
    2.46 +instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    2.47 +proof 
    2.48 +  fix A B C :: "('a::lordered_ab_group) matrix"
    2.49 +  show "A + B + C = A + (B + C)"    
    2.50 +    apply (simp add: plus_matrix_def)
    2.51 +    apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
    2.52 +    apply (simp_all add: add_assoc)
    2.53 +    done
    2.54 +  show "A + B = B + A"
    2.55 +    apply (simp add: plus_matrix_def)
    2.56 +    apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
    2.57 +    apply (simp_all add: add_commute)
    2.58 +    done
    2.59 +  show "0 + A = A"
    2.60 +    apply (simp add: plus_matrix_def)
    2.61 +    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
    2.62 +    apply (simp)
    2.63 +    done
    2.64 +  show "- A + A = 0" 
    2.65 +    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    2.66 +  show "A - B = A + - B" 
    2.67 +    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
    2.68 +  show "\<exists>m\<Colon>'a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix. is_meet m"
    2.69 +    by (auto intro: is_meet_combine_matrix_meet)
    2.70 +  assume "A <= B"
    2.71 +  then show "C + A <= C + B"
    2.72 +    apply (simp add: plus_matrix_def)
    2.73 +    apply (rule le_left_combine_matrix)
    2.74 +    apply (simp_all)
    2.75 +    done
    2.76 +qed
    2.77  
    2.78  defs (overloaded)
    2.79 -plus_matrix_def: "A + B == combine_matrix (op +) A B"
    2.80 -times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
    2.81 +  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == join A (- A)"
    2.82  
    2.83 -instance matrix :: (matrix_element) matrix_element
    2.84 -proof -
    2.85 -  note combine_matrix_assoc2 = combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec]
    2.86 -  {
    2.87 -    fix A::"('a::matrix_element) matrix"
    2.88 -    fix B
    2.89 -    fix C
    2.90 -    have "(A + B) + C = A + (B + C)"
    2.91 -      apply (simp add: plus_matrix_def)
    2.92 -      apply (rule combine_matrix_assoc2)
    2.93 -      by (simp_all add: matrix_add_assoc)
    2.94 -  }
    2.95 -  note plus_assoc = this
    2.96 -  {
    2.97 -    fix A::"('a::matrix_element) matrix"
    2.98 -    fix B
    2.99 -    fix C
   2.100 -    have "(A * B) * C = A * (B * C)"
   2.101 -      apply (simp add: times_matrix_def)
   2.102 -      apply (rule mult_matrix_assoc_simple)
   2.103 -      apply (simp_all add: associative_def commutative_def distributive_def l_distributive_def r_distributive_def)
   2.104 -      apply (auto)
   2.105 -      apply (simp_all add: matrix_add_assoc)
   2.106 -      apply (simp_all add: matrix_add_commute)
   2.107 -      apply (simp_all add: matrix_mult_assoc)
   2.108 -      by (simp_all add: matrix_left_distrib matrix_right_distrib)
   2.109 -  }
   2.110 -  note mult_assoc = this
   2.111 -  note combine_matrix_commute2 = combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec]
   2.112 -  {
   2.113 -    fix A::"('a::matrix_element) matrix"
   2.114 -    fix B
   2.115 -    have "A + B = B + A"
   2.116 -      apply (simp add: plus_matrix_def)
   2.117 -      apply (insert combine_matrix_commute2[of "op +"])
   2.118 -      apply (rule combine_matrix_commute2)
   2.119 -      by (simp add: matrix_add_commute)
   2.120 -  }
   2.121 -  note plus_commute = this
   2.122 -  have plus_zero: "(0::('a::matrix_element) matrix) + 0 = 0"
   2.123 -    apply (simp add: plus_matrix_def)
   2.124 -    apply (rule combine_matrix_zero)
   2.125 -    by (simp)
   2.126 -  have mult_left_zero: "!! A. (0::('a::matrix_element) matrix) * A = 0" by(simp add: times_matrix_def)
   2.127 -  have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
   2.128 -  note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
   2.129 -  {
   2.130 -    fix A::"('a::matrix_element) matrix"
   2.131 -    fix B
   2.132 -    fix C
   2.133 -    have "(A + B) * C = A * C + B * C"
   2.134 -      apply (simp add: plus_matrix_def)
   2.135 -      apply (simp add: times_matrix_def)
   2.136 -      apply (rule l_distributive_matrix2)
   2.137 -      apply (simp_all add: associative_def commutative_def l_distributive_def)
   2.138 -      apply (auto)
   2.139 -      apply (simp_all add: matrix_add_assoc)
   2.140 -      apply (simp_all add: matrix_add_commute)
   2.141 -      by (simp_all add: matrix_left_distrib)
   2.142 -  }
   2.143 -  note left_distrib = this
   2.144 -  note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
   2.145 -  {
   2.146 -    fix A::"('a::matrix_element) matrix"
   2.147 -    fix B
   2.148 -    fix C
   2.149 -    have "C * (A + B) = C * A + C * B"
   2.150 -      apply (simp add: plus_matrix_def)
   2.151 -      apply (simp add: times_matrix_def)
   2.152 -      apply (rule r_distributive_matrix2)
   2.153 -      apply (simp_all add: associative_def commutative_def r_distributive_def)
   2.154 -      apply (auto)
   2.155 -      apply (simp_all add: matrix_add_assoc)
   2.156 -      apply (simp_all add: matrix_add_commute)
   2.157 -      by (simp_all add: matrix_right_distrib)
   2.158 -  }
   2.159 -  note right_distrib = this
   2.160 -  show "OFCLASS('a matrix, matrix_element_class)"
   2.161 -    apply (intro_classes)
   2.162 -    apply (simp_all add: plus_assoc)
   2.163 -    apply (simp_all add: plus_commute)
   2.164 -    apply (simp_all add: plus_zero)
   2.165 -    apply (simp_all add: mult_assoc)
   2.166 -    apply (simp_all add: mult_left_zero mult_right_zero)
   2.167 -    by (simp_all add: left_distrib right_distrib)
   2.168 +instance matrix :: (lordered_ring) lordered_ring
   2.169 +proof
   2.170 +  fix A B C :: "('a :: lordered_ring) matrix"
   2.171 +  show "A * B * C = A * (B * C)"
   2.172 +    apply (simp add: times_matrix_def)
   2.173 +    apply (rule mult_matrix_assoc)
   2.174 +    apply (simp_all add: associative_def ring_eq_simps)
   2.175 +    done
   2.176 +  show "(A + B) * C = A * C + B * C"
   2.177 +    apply (simp add: times_matrix_def plus_matrix_def)
   2.178 +    apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
   2.179 +    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   2.180 +    done
   2.181 +  show "A * (B + C) = A * B + A * C"
   2.182 +    apply (simp add: times_matrix_def plus_matrix_def)
   2.183 +    apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
   2.184 +    apply (simp_all add: associative_def commutative_def ring_eq_simps)
   2.185 +    done  
   2.186 +  show "abs A = join A (-A)" 
   2.187 +    by (simp add: abs_matrix_def)
   2.188 +  assume a: "A \<le> B"
   2.189 +  assume b: "0 \<le> C"
   2.190 +  from a b show "C * A \<le> C * B"
   2.191 +    apply (simp add: times_matrix_def)
   2.192 +    apply (rule le_left_mult)
   2.193 +    apply (simp_all add: add_mono mult_left_mono)
   2.194 +    done
   2.195 +  from a b show "A * C \<le> B * C"
   2.196 +    apply (simp add: times_matrix_def)
   2.197 +    apply (rule le_right_mult)
   2.198 +    apply (simp_all add: add_mono mult_right_mono)
   2.199 +    done
   2.200  qed
   2.201  
   2.202 -axclass g_almost_semiring < almost_matrix_element
   2.203 -g_add_left_0[simp]: "0 + a = a"
   2.204 -
   2.205 -lemma g_add_right_0[simp]: "(a::'a::g_almost_semiring) + 0 = a"
   2.206 -by (simp add: matrix_add_commute)
   2.207 -
   2.208 -axclass g_semiring < g_almost_semiring
   2.209 -g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
   2.210 -
   2.211 -instance g_almost_semiring < matrix_element
   2.212 -  by intro_classes simp
   2.213 -
   2.214 -instance matrix :: (g_almost_semiring) g_almost_semiring
   2.215 -apply (intro_classes)
   2.216 -by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   2.217 +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)"
   2.218 +by (simp add: plus_matrix_def)
   2.219  
   2.220 -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"
   2.221 -by (simp add: RepAbs_matrix)
   2.222 -
   2.223 -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"
   2.224 -by (simp add: RepAbs_matrix)
   2.225 +lemma Rep_matrix_mult: "Rep_matrix ((a::('a::lordered_ring) matrix) * b) j i = 
   2.226 +  foldseq (op +) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
   2.227 +apply (simp add: times_matrix_def)
   2.228 +apply (simp add: Rep_mult_matrix)
   2.229 +done
   2.230 + 
   2.231  
   2.232 -instance matrix :: (g_semiring) g_semiring
   2.233 -apply (intro_classes)
   2.234 -apply (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
   2.235 -apply (subst Rep_matrix_inject[THEN sym])
   2.236 -apply (drule ssubst[OF Rep_matrix_inject, of "% x. x"])
   2.237 -apply (drule RepAbs_matrix_eq_left)
   2.238 -apply (auto)
   2.239 -apply (rule_tac x="max (nrows a) (nrows b)" in exI, simp add: nrows_le)
   2.240 -apply (rule_tac x="max (ncols a) (ncols b)" in exI, simp add: ncols_le)
   2.241 -apply (drule RepAbs_matrix_eq_right)
   2.242 -apply (rule_tac x="max (nrows a) (nrows c)" in exI, simp add: nrows_le)
   2.243 -apply (rule_tac x="max (ncols a) (ncols c)" in exI, simp add: ncols_le)
   2.244 +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)"
   2.245 +apply (subst Rep_matrix_inject[symmetric])
   2.246  apply (rule ext)+
   2.247 -apply (drule_tac x="x" and y="x" in comb, simp)
   2.248 -apply (drule_tac x="xa" and y="xa" in comb, simp)
   2.249 -apply (drule g_add_leftimp_eq)
   2.250 -by simp
   2.251 -
   2.252 -axclass pordered_matrix_element < matrix_element, order, zero
   2.253 -pordered_add_right_mono: "a <= b \<Longrightarrow> a + c <= b + c"
   2.254 -pordered_mult_left: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> c*a <= c*b"
   2.255 -pordered_mult_right: "0 <= c \<Longrightarrow> a <= b \<Longrightarrow> a*c <= b*c"
   2.256 -
   2.257 -lemma pordered_add_left_mono: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> c + a <= c + b"
   2.258 -apply (insert pordered_add_right_mono[of a b c])
   2.259 -by (simp add: matrix_add_commute)
   2.260 +apply (simp)
   2.261 +done
   2.262  
   2.263 -lemma pordered_add: "(a::'a::pordered_matrix_element) <= b \<Longrightarrow> (c::'a::pordered_matrix_element) <= d \<Longrightarrow> a+c <= b+d"
   2.264 -proof -
   2.265 -  assume p1:"a <= b"
   2.266 -  assume p2:"c <= d"
   2.267 -  have "a+c <= b+c" by (rule pordered_add_right_mono)
   2.268 -  also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
   2.269 -  ultimately show "a+c <= b+d" by simp
   2.270 -qed
   2.271 +lemma singleton_matrix_add: "singleton_matrix j i ((a::_::lordered_ab_group)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
   2.272 +apply (subst Rep_matrix_inject[symmetric])
   2.273 +apply (rule ext)+
   2.274 +apply (simp)
   2.275 +done
   2.276  
   2.277 -instance matrix :: (pordered_matrix_element) pordered_matrix_element
   2.278 -apply (intro_classes)
   2.279 -apply (simp_all add: plus_matrix_def times_matrix_def)
   2.280 -apply (rule le_combine_matrix)
   2.281 -apply (simp_all)
   2.282 -apply (simp_all add: pordered_add)
   2.283 -apply (rule le_left_mult)
   2.284 -apply (simp_all add: matrix_add_0 g_add_left_0 pordered_add pordered_mult_left matrix_mult_left_0 matrix_mult_right_0)
   2.285 -apply (rule le_right_mult)
   2.286 -by (simp_all add: pordered_add pordered_mult_right)
   2.287 -
   2.288 -axclass pordered_g_semiring < g_semiring, pordered_matrix_element
   2.289 -
   2.290 -instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
   2.291 -
   2.292 -lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
   2.293 +lemma nrows_mult: "nrows ((A::('a::lordered_ring) matrix) * B) <= nrows A"
   2.294  by (simp add: times_matrix_def mult_nrows)
   2.295  
   2.296 -lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
   2.297 +lemma ncols_mult: "ncols ((A::('a::lordered_ring) matrix) * B) <= ncols B"
   2.298  by (simp add: times_matrix_def mult_ncols)
   2.299  
   2.300 -(*
   2.301  constdefs
   2.302 -  one_matrix :: "nat \<Rightarrow> ('a::comm_semiring_1_cancel) matrix"
   2.303 +  one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix"
   2.304    "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
   2.305  
   2.306  lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
   2.307 @@ -204,21 +130,21 @@
   2.308  apply (rule exI[of _ n], simp add: split_if)+
   2.309  by (simp add: split_if, arith)
   2.310  
   2.311 -lemma nrows_one_matrix[simp]: "nrows (one_matrix n) = n" (is "?r = _")
   2.312 +lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
   2.313  proof -
   2.314    have "?r <= n" by (simp add: nrows_le)
   2.315 -  moreover have "n <= ?r" by (simp add: le_nrows, arith)
   2.316 +  moreover have "n <= ?r" by (simp add:le_nrows, arith)
   2.317    ultimately show "?r = n" by simp
   2.318  qed
   2.319  
   2.320 -lemma ncols_one_matrix[simp]: "ncols (one_matrix n) = n" (is "?r = _")
   2.321 +lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
   2.322  proof -
   2.323    have "?r <= n" by (simp add: ncols_le)
   2.324    moreover have "n <= ?r" by (simp add: le_ncols, arith)
   2.325    ultimately show "?r = n" by simp
   2.326  qed
   2.327  
   2.328 -lemma one_matrix_mult_right: "ncols A <= n \<Longrightarrow> A * (one_matrix n) = A"
   2.329 +lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{lordered_ring,ring_1}) matrix) * (one_matrix n) = A"
   2.330  apply (subst Rep_matrix_inject[THEN sym])
   2.331  apply (rule ext)+
   2.332  apply (simp add: times_matrix_def Rep_mult_matrix)
   2.333 @@ -226,7 +152,7 @@
   2.334  apply (simp_all)
   2.335  by (simp add: max_def ncols)
   2.336  
   2.337 -lemma one_matrix_mult_left: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = A"
   2.338 +lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::{lordered_ring, ring_1}) matrix)"
   2.339  apply (subst Rep_matrix_inject[THEN sym])
   2.340  apply (rule ext)+
   2.341  apply (simp add: times_matrix_def Rep_mult_matrix)
   2.342 @@ -234,16 +160,131 @@
   2.343  apply (simp_all)
   2.344  by (simp add: max_def nrows)
   2.345  
   2.346 -constdefs
   2.347 -  right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   2.348 -  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
   2.349 -  inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   2.350 -  "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
   2.351 +lemma transpose_matrix_mult: "transpose_matrix ((A::('a::{lordered_ring,comm_ring}) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
   2.352 +apply (simp add: times_matrix_def)
   2.353 +apply (subst transpose_mult_matrix)
   2.354 +apply (simp_all add: mult_commute)
   2.355 +done
   2.356 +
   2.357 +lemma transpose_matrix_add: "transpose_matrix ((A::('a::lordered_ab_group) matrix)+B) = transpose_matrix A + transpose_matrix B"
   2.358 +by (simp add: plus_matrix_def transpose_combine_matrix)
   2.359 +
   2.360 +lemma transpose_matrix_diff: "transpose_matrix ((A::('a::lordered_ab_group) matrix)-B) = transpose_matrix A - transpose_matrix B"
   2.361 +by (simp add: diff_matrix_def transpose_combine_matrix)
   2.362 +
   2.363 +lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::lordered_ring) matrix)) = - transpose_matrix (A::('a::lordered_ring) matrix)"
   2.364 +by (simp add: minus_matrix_def transpose_apply_matrix)
   2.365 +
   2.366 +constdefs 
   2.367 +  right_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   2.368 +  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
   2.369 +  left_inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   2.370 +  "left_inverse_matrix A X == (X * A = one_matrix (max(nrows X) (ncols A))) \<and> ncols X \<le> nrows A" 
   2.371 +  inverse_matrix :: "('a::{lordered_ring, ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   2.372 +  "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
   2.373  
   2.374  lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
   2.375  apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
   2.376  by (simp add: right_inverse_matrix_def)
   2.377  
   2.378 -text {* to be continued \dots *}
   2.379 -*)
   2.380 +lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
   2.381 +apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) 
   2.382 +by (simp add: left_inverse_matrix_def)
   2.383 +
   2.384 +lemma left_right_inverse_matrix_unique: 
   2.385 +  assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
   2.386 +  shows "X = Y"
   2.387 +proof -
   2.388 +  have "Y = Y * one_matrix (nrows A)" 
   2.389 +    apply (subst one_matrix_mult_right)
   2.390 +    apply (insert prems)
   2.391 +    by (simp_all add: left_inverse_matrix_def)
   2.392 +  also have "\<dots> = Y * (A * X)" 
   2.393 +    apply (insert prems)
   2.394 +    apply (frule right_inverse_matrix_dim)
   2.395 +    by (simp add: right_inverse_matrix_def)
   2.396 +  also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
   2.397 +  also have "\<dots> = X" 
   2.398 +    apply (insert prems)
   2.399 +    apply (frule left_inverse_matrix_dim)
   2.400 +    apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
   2.401 +    done
   2.402 +  ultimately show "X = Y" by (simp)
   2.403 +qed
   2.404 +
   2.405 +lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
   2.406 +  by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
   2.407 +
   2.408 +lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
   2.409 +  by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
   2.410 +
   2.411 +lemma zero_imp_mult_zero: "(a::'a::ring) = 0 | b = 0 \<Longrightarrow> a * b = 0"
   2.412 +by auto
   2.413 +
   2.414 +lemma Rep_matrix_zero_imp_mult_zero:
   2.415 +  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
   2.416 +apply (subst Rep_matrix_inject[symmetric])
   2.417 +apply (rule ext)+
   2.418 +apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
   2.419 +done
   2.420 +
   2.421 +lemma add_nrows: "nrows (A::('a::comm_monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
   2.422 +apply (simp add: plus_matrix_def)
   2.423 +apply (rule combine_nrows)
   2.424 +apply (simp_all)
   2.425 +done
   2.426 +
   2.427 +lemma move_matrix_row_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) j 0 = (move_matrix A j 0) * B"
   2.428 +apply (subst Rep_matrix_inject[symmetric])
   2.429 +apply (rule ext)+
   2.430 +apply (auto simp add: Rep_matrix_mult foldseq_zero)
   2.431 +apply (rule_tac foldseq_zerotail[symmetric])
   2.432 +apply (auto simp add: nrows zero_imp_mult_zero max2)
   2.433 +apply (rule order_trans)
   2.434 +apply (rule ncols_move_matrix_le)
   2.435 +apply (simp add: max1)
   2.436 +done
   2.437 +
   2.438 +lemma move_matrix_col_mult: "move_matrix ((A::('a::lordered_ring) matrix) * B) 0 i = A * (move_matrix B 0 i)"
   2.439 +apply (subst Rep_matrix_inject[symmetric])
   2.440 +apply (rule ext)+
   2.441 +apply (auto simp add: Rep_matrix_mult foldseq_zero)
   2.442 +apply (rule_tac foldseq_zerotail[symmetric])
   2.443 +apply (auto simp add: ncols zero_imp_mult_zero max1)
   2.444 +apply (rule order_trans)
   2.445 +apply (rule nrows_move_matrix_le)
   2.446 +apply (simp add: max2)
   2.447 +done
   2.448 +
   2.449 +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)" 
   2.450 +apply (subst Rep_matrix_inject[symmetric])
   2.451 +apply (rule ext)+
   2.452 +apply (simp)
   2.453 +done
   2.454 +
   2.455 +lemma move_matrix_mult: "move_matrix ((A::('a::lordered_ring) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
   2.456 +by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
   2.457 +
   2.458 +constdefs
   2.459 +  scalar_mult :: "('a::lordered_ring) \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix"
   2.460 +  "scalar_mult a m == apply_matrix (op * a) m"
   2.461 +
   2.462 +lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
   2.463 +  by (simp add: scalar_mult_def)
   2.464 +
   2.465 +lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
   2.466 +  by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
   2.467 +
   2.468 +lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
   2.469 +  by (simp add: scalar_mult_def)
   2.470 +
   2.471 +lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
   2.472 +  apply (subst Rep_matrix_inject[symmetric])
   2.473 +  apply (rule ext)+
   2.474 +  apply (auto)
   2.475 +  done
   2.476 +
   2.477 +
   2.478 +
   2.479 +
   2.480  end
     3.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Sun Jun 13 17:57:35 2004 +0200
     3.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Jun 14 14:20:55 2004 +0200
     3.3 @@ -1,7 +1,6 @@
     3.4  (*  Title:      HOL/Matrix/MatrixGeneral.thy
     3.5      ID:         $Id$
     3.6      Author:     Steven Obua
     3.7 -    License:    2004 Technische Universitaet Muenchen
     3.8  *)
     3.9  
    3.10  theory MatrixGeneral = Main:
    3.11 @@ -99,6 +98,22 @@
    3.12    ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
    3.13  qed
    3.14  
    3.15 +lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
    3.16 +
    3.17 +lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
    3.18 +apply (auto)
    3.19 +apply (rule ext)+
    3.20 +apply (simp add: transpose_infmatrix)
    3.21 +apply (drule infmatrixforward)
    3.22 +apply (simp)
    3.23 +done
    3.24 +
    3.25 +lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
    3.26 +apply (simp add: transpose_matrix_def)
    3.27 +apply (subst Rep_matrix_inject[THEN sym])+
    3.28 +apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
    3.29 +done
    3.30 +
    3.31  lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
    3.32  by (simp add: transpose_matrix_def)
    3.33  
    3.34 @@ -175,6 +190,16 @@
    3.35  apply (drule_tac x="nrows A" in spec)
    3.36  by (simp add: nrows)
    3.37  
    3.38 +lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
    3.39 +apply (case_tac "nrows A <= m")
    3.40 +apply (simp_all add: nrows)
    3.41 +done
    3.42 +
    3.43 +lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
    3.44 +apply (case_tac "ncols A <= n")
    3.45 +apply (simp_all add: ncols)
    3.46 +done
    3.47 +
    3.48  lemma finite_natarray1: "finite {x. x < (n::nat)}"
    3.49  apply (induct n)
    3.50  apply (simp)
    3.51 @@ -768,6 +793,10 @@
    3.52    show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
    3.53  qed
    3.54  
    3.55 +lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
    3.56 +  by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
    3.57 +
    3.58 +
    3.59  lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
    3.60    by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
    3.61  
    3.62 @@ -800,6 +829,12 @@
    3.63    apply (simp add: combine_matrix_def combine_infmatrix_def)
    3.64    by (simp add: zero_matrix_def)
    3.65  
    3.66 +lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
    3.67 +apply (simp add: transpose_matrix_def transpose_infmatrix_def zero_matrix_def RepAbs_matrix)
    3.68 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
    3.69 +apply (simp add: RepAbs_matrix)
    3.70 +done
    3.71 +
    3.72  lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
    3.73    apply (simp add: apply_matrix_def apply_infmatrix_def)
    3.74    by (simp add: zero_matrix_def)
    3.75 @@ -828,6 +863,12 @@
    3.76  apply (rule exI[of _ "Suc n"], simp+)
    3.77  by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
    3.78  
    3.79 +lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
    3.80 +apply (subst Rep_matrix_inject[symmetric])
    3.81 +apply (rule ext)+
    3.82 +apply (simp)
    3.83 +done
    3.84 +
    3.85  lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
    3.86    by (simp add: singleton_matrix_def zero_matrix_def)
    3.87  
    3.88 @@ -870,6 +911,11 @@
    3.89  apply (rule exI[of _ "Suc i"], simp)
    3.90  by simp
    3.91  
    3.92 +lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
    3.93 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
    3.94 +apply (simp)
    3.95 +done
    3.96 +
    3.97  lemma Rep_move_matrix[simp]:
    3.98    "Rep_matrix (move_matrix A y x) j i =
    3.99    (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
   3.100 @@ -879,6 +925,33 @@
   3.101    rule exI[of _ "(nrows A)+(nat (abs y))"], auto, rule nrows, arith,
   3.102    rule exI[of _ "(ncols A)+(nat (abs x))"], auto, rule ncols, arith)+
   3.103  
   3.104 +lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
   3.105 +by (simp add: move_matrix_def)
   3.106 +
   3.107 +lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
   3.108 +apply (subst Rep_matrix_inject[symmetric])
   3.109 +apply (rule ext)+
   3.110 +apply (simp)
   3.111 +done
   3.112 +
   3.113 +lemma transpose_move_matrix[simp]:
   3.114 +  "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
   3.115 +apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
   3.116 +apply (simp)
   3.117 +done
   3.118 +
   3.119 +lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
   3.120 +  (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
   3.121 +  apply (subst Rep_matrix_inject[symmetric])
   3.122 +  apply (rule ext)+
   3.123 +  apply (case_tac "j + int u < 0")
   3.124 +  apply (simp, arith)
   3.125 +  apply (case_tac "i + int v < 0")
   3.126 +  apply (simp add: neg_def, arith)
   3.127 +  apply (simp add: neg_def)
   3.128 +  apply arith
   3.129 +  done
   3.130 +
   3.131  lemma Rep_take_columns[simp]:
   3.132    "Rep_matrix (take_columns A c) j i =
   3.133    (if i < c then (Rep_matrix A j i) else 0)"
   3.134 @@ -905,6 +978,16 @@
   3.135    "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   3.136    by (simp add: row_of_matrix_def)
   3.137  
   3.138 +lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
   3.139 +apply (subst Rep_matrix_inject[THEN sym])
   3.140 +apply (rule ext)+
   3.141 +by (simp add: ncols)
   3.142 +
   3.143 +lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
   3.144 +apply (subst Rep_matrix_inject[THEN sym])
   3.145 +apply (rule ext)+
   3.146 +by (simp add: nrows)
   3.147 +
   3.148  lemma mult_matrix_singleton_right[simp]:
   3.149    assumes prems:
   3.150    "! x. fmul x 0 = 0"
   3.151 @@ -1052,6 +1135,18 @@
   3.152  shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
   3.153  by (simp add: mult_matrix_def mult_n_ncols prems)
   3.154  
   3.155 +lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
   3.156 +  apply (auto simp add: nrows_le)
   3.157 +  apply (rule nrows)
   3.158 +  apply (arith)
   3.159 +  done
   3.160 +
   3.161 +lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
   3.162 +  apply (auto simp add: ncols_le)
   3.163 +  apply (rule ncols)
   3.164 +  apply (arith)
   3.165 +  done
   3.166 +
   3.167  lemma mult_matrix_assoc:
   3.168    assumes prems:
   3.169    "! a. fmul1 0 a = 0"
   3.170 @@ -1183,6 +1278,16 @@
   3.171    apply (rule ext)+
   3.172    by (simp! add: Rep_mult_matrix max_ac)
   3.173  
   3.174 +lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
   3.175 +apply (simp add:  Rep_matrix_inject[THEN sym])
   3.176 +apply (rule ext)+
   3.177 +by simp
   3.178 +
   3.179 +lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
   3.180 +apply (simp add: Rep_matrix_inject[THEN sym])
   3.181 +apply (rule ext)+
   3.182 +by simp
   3.183 +
   3.184  instance matrix :: ("{ord, zero}") ord ..
   3.185  
   3.186  defs (overloaded)
   3.187 @@ -1224,8 +1329,7 @@
   3.188  lemma le_left_combine_matrix:
   3.189    assumes
   3.190    "f 0 0 = 0"
   3.191 -  "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b"
   3.192 -  "0 <= C"
   3.193 +  "! a b c. a <= b \<longrightarrow> f c a <= f c b"
   3.194    "A <= B"
   3.195    shows
   3.196    "combine_matrix f C A <= combine_matrix f C B"
   3.197 @@ -1234,8 +1338,7 @@
   3.198  lemma le_right_combine_matrix:
   3.199    assumes
   3.200    "f 0 0 = 0"
   3.201 -  "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c"
   3.202 -  "0 <= C"
   3.203 +  "! a b c. a <= b \<longrightarrow> f a c <= f b c"
   3.204    "A <= B"
   3.205    shows
   3.206    "combine_matrix f A C <= combine_matrix f B C"
   3.207 @@ -1258,7 +1361,7 @@
   3.208  lemma le_left_mult:
   3.209    assumes
   3.210    "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
   3.211 -  "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
   3.212 +  "! c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
   3.213    "! a. fmul 0 a = 0"
   3.214    "! a. fmul a 0 = 0"
   3.215    "fadd 0 0 = 0"
   3.216 @@ -1289,4 +1392,7 @@
   3.217    apply (rule le_foldseq)
   3.218    by (auto)
   3.219  
   3.220 +lemma singleton_matrix_le[simp]: "(singleton_matrix j i a <= singleton_matrix j i b) = (a <= (b::_::order))"
   3.221 +  by (auto simp add: le_matrix_def)
   3.222 +
   3.223  end
     4.1 --- a/src/HOL/Ring_and_Field.thy	Sun Jun 13 17:57:35 2004 +0200
     4.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Jun 14 14:20:55 2004 +0200
     4.3 @@ -27,6 +27,8 @@
     4.4  
     4.5  axclass semiring_0 \<subseteq> semiring, comm_monoid_add
     4.6  
     4.7 +axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
     4.8 +
     4.9  axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
    4.10    mult_commute: "a * b = b * a"
    4.11    distrib: "(a + b) * c = a * c + b * c"
    4.12 @@ -45,6 +47,10 @@
    4.13  
    4.14  instance comm_semiring_0 \<subseteq> semiring_0 ..
    4.15  
    4.16 +axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
    4.17 +
    4.18 +instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
    4.19 +
    4.20  axclass axclass_0_neq_1 \<subseteq> zero, one
    4.21    zero_neq_one [simp]: "0 \<noteq> 1"
    4.22  
    4.23 @@ -57,20 +63,30 @@
    4.24  axclass axclass_no_zero_divisors \<subseteq> zero, times
    4.25    no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    4.26  
    4.27 +axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
    4.28 +
    4.29 +instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
    4.30 +
    4.31  axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
    4.32  
    4.33 +instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
    4.34 +
    4.35 +instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
    4.36 +
    4.37  axclass ring \<subseteq> semiring, ab_group_add
    4.38  
    4.39 -instance ring \<subseteq> semiring_0 ..
    4.40 +instance ring \<subseteq> semiring_0_cancel ..
    4.41  
    4.42  axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
    4.43  
    4.44  instance comm_ring \<subseteq> ring ..
    4.45  
    4.46 -instance comm_ring \<subseteq> comm_semiring_0 ..
    4.47 +instance comm_ring \<subseteq> comm_semiring_0_cancel ..
    4.48  
    4.49  axclass ring_1 \<subseteq> ring, semiring_1
    4.50  
    4.51 +instance ring_1 \<subseteq> semiring_1_cancel ..
    4.52 +
    4.53  axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
    4.54  
    4.55  instance comm_ring_1 \<subseteq> ring_1 ..
    4.56 @@ -83,7 +99,7 @@
    4.57    left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
    4.58    divide_inverse:      "a / b = a * inverse b"
    4.59  
    4.60 -lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"
    4.61 +lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
    4.62  proof -
    4.63    have "0*a + 0*a = 0*a + 0"
    4.64      by (simp add: left_distrib [symmetric])
    4.65 @@ -91,7 +107,7 @@
    4.66      by (simp only: add_left_cancel)
    4.67  qed
    4.68  
    4.69 -lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"
    4.70 +lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
    4.71  proof -
    4.72    have "a*0 + a*0 = a*0 + 0"
    4.73      by (simp add: right_distrib [symmetric])
    4.74 @@ -155,10 +171,14 @@
    4.75  
    4.76  axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
    4.77  
    4.78 +instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
    4.79 +
    4.80  axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
    4.81    mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
    4.82    mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
    4.83  
    4.84 +instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
    4.85 +
    4.86  instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring
    4.87  apply intro_classes
    4.88  apply (case_tac "a < b & 0 < c")
    4.89 @@ -200,6 +220,10 @@
    4.90  
    4.91  axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
    4.92  
    4.93 +instance lordered_ring \<subseteq> lordered_ab_group_meet ..
    4.94 +
    4.95 +instance lordered_ring \<subseteq> lordered_ab_group_join ..
    4.96 +
    4.97  axclass axclass_abs_if \<subseteq> minus, ord, zero
    4.98    abs_if: "abs a = (if (a < 0) then (-a) else a)"
    4.99