src/HOL/Matrix/Matrix.thy

     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
 
-instance matrix :: (pordered_ab_group_add) pordered_ab_group_add
+instance matrix :: (ordered_ab_group_add) ordered_ab_group_add
 proof
   fix A B C :: "'a matrix"
   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
   
-instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet ..
-instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_join ..
+instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add ..
+instance matrix :: (lattice_ab_group_add) semilattice_sup_ab_group_add ..
 
 instance matrix :: (semiring_0) semiring_0
 proof
   fix A B C :: "'a matrix"
   show "A * B * C = A * (B * C)"

   show "A * 0 = 0" by (simp add: times_matrix_def)
 qed
 
 instance matrix :: (ring) ring ..
 
-instance matrix :: (pordered_ring) pordered_ring
+instance matrix :: (ordered_ring) ordered_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"

     apply (rule le_right_mult)
     apply (simp_all add: add_mono mult_right_mono)
     done
 qed
 
-instance matrix :: (lordered_ring) lordered_ring
+instance matrix :: (lattice_ring) lattice_ring
 proof
-  fix A B C :: "('a :: lordered_ring) matrix"
+  fix A B C :: "('a :: lattice_ring) matrix"
   show "abs A = sup A (-A)" 
     by (simp add: abs_matrix_def)
 qed
 
 lemma Rep_matrix_add[simp]:

 
 lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 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)"
+  "! j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lattice_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
 

 done
 
 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
 by (simp add: minus_matrix_def)
 
-lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ab_group_add)) x y = abs (Rep_matrix A x y)"
+lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lattice_ab_group_add)) x y = abs (Rep_matrix A x y)"
 by (simp add: abs_lattice sup_matrix_def)
 
 end