src/HOL/Matrix/Matrix.thy
changeset 14724 021264410f87
parent 14691 e1eedc8cad37
child 14738 83f1a514dcb4
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Mon May 10 16:40:54 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Mon May 10 17:10:41 2004 +0200
     1.3 @@ -126,11 +126,6 @@
     1.4  instance g_almost_semiring < matrix_element
     1.5    by intro_classes simp
     1.6  
     1.7 -instance semiring < g_semiring
     1.8 -apply (intro_classes)
     1.9 -apply (simp_all add: add_ac)
    1.10 -by (simp_all add: mult_assoc left_distrib right_distrib)
    1.11 -
    1.12  instance matrix :: (g_almost_semiring) g_almost_semiring
    1.13  apply (intro_classes)
    1.14  by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
    1.15 @@ -190,10 +185,6 @@
    1.16  
    1.17  axclass pordered_g_semiring < g_semiring, pordered_matrix_element
    1.18  
    1.19 -instance almost_ordered_semiring < pordered_g_semiring
    1.20 -apply (intro_classes)
    1.21 -by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
    1.22 -
    1.23  instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
    1.24  
    1.25  lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
    1.26 @@ -202,6 +193,7 @@
    1.27  lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
    1.28  by (simp add: times_matrix_def mult_ncols)
    1.29  
    1.30 +(*
    1.31  constdefs
    1.32    one_matrix :: "nat \<Rightarrow> ('a::semiring) matrix"
    1.33    "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
    1.34 @@ -253,5 +245,5 @@
    1.35  by (simp add: right_inverse_matrix_def)
    1.36  
    1.37  text {* to be continued \dots *}
    1.38 -
    1.39 +*)
    1.40  end