src/HOL/Matrix/Matrix.thy
changeset 35028 108662d50512
parent 34872 6ca970cfa873
child 35032 7efe662e41b4
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Feb 05 14:33:31 2010 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Feb 05 14:33:50 2010 +0100
     1.3 @@ -1545,7 +1545,7 @@
     1.4      by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
     1.5  qed
     1.6  
     1.7 -instance matrix :: (pordered_ab_group_add) pordered_ab_group_add
     1.8 +instance matrix :: (ordered_ab_group_add) ordered_ab_group_add
     1.9  proof
    1.10    fix A B C :: "'a matrix"
    1.11    assume "A <= B"
    1.12 @@ -1556,8 +1556,8 @@
    1.13      done
    1.14  qed
    1.15    
    1.16 -instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet ..
    1.17 -instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join ..
    1.18 +instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add ..
    1.19 +instance matrix :: (lattice_ab_group_add) semilattice_sup_ab_group_add ..
    1.20  
    1.21  instance matrix :: (semiring_0) semiring_0
    1.22  proof
    1.23 @@ -1583,7 +1583,7 @@
    1.24  
    1.25  instance matrix :: (ring) ring ..
    1.26  
    1.27 -instance matrix :: (pordered_ring) pordered_ring
    1.28 +instance matrix :: (ordered_ring) ordered_ring
    1.29  proof
    1.30    fix A B C :: "'a matrix"
    1.31    assume a: "A \<le> B"
    1.32 @@ -1600,9 +1600,9 @@
    1.33      done
    1.34  qed
    1.35  
    1.36 -instance matrix :: (lordered_ring) lordered_ring
    1.37 +instance matrix :: (lattice_ring) lattice_ring
    1.38  proof
    1.39 -  fix A B C :: "('a :: lordered_ring) matrix"
    1.40 +  fix A B C :: "('a :: lattice_ring) matrix"
    1.41    show "abs A = sup A (-A)" 
    1.42      by (simp add: abs_matrix_def)
    1.43  qed
    1.44 @@ -1738,7 +1738,7 @@
    1.45  by auto
    1.46  
    1.47  lemma Rep_matrix_zero_imp_mult_zero:
    1.48 -  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lordered_ring) matrix)"
    1.49 +  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lattice_ring) matrix)"
    1.50  apply (subst Rep_matrix_inject[symmetric])
    1.51  apply (rule ext)+
    1.52  apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
    1.53 @@ -1803,7 +1803,7 @@
    1.54  lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
    1.55  by (simp add: minus_matrix_def)
    1.56  
    1.57 -lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ab_group_add)) x y = abs (Rep_matrix A x y)"
    1.58 +lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"
    1.59  by (simp add: abs_lattice sup_matrix_def)
    1.60  
    1.61  end