diff -r 474f8ba9dfa9 -r 878c37886eed src/HOL/Matrix/Matrix.thy --- a/src/HOL/Matrix/Matrix.thy Wed Jan 02 15:14:15 2008 +0100 +++ b/src/HOL/Matrix/Matrix.thy Wed Jan 02 15:14:17 2008 +0100 @@ -7,23 +7,69 @@ imports MatrixGeneral begin -instance matrix :: ("{zero, lattice}") lattice - "inf \ combine_matrix inf" - "sup \ combine_matrix sup" +instantiation matrix :: ("{zero, lattice}") lattice +begin + +definition + "inf = combine_matrix inf" + +definition + "sup = combine_matrix sup" + +instance by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def) -instance matrix :: ("{plus, zero}") plus - plus_matrix_def: "A + B \ combine_matrix (op +) A B" .. +end + +instantiation matrix :: ("{plus, zero}") plus +begin + +definition + plus_matrix_def: "A + B = combine_matrix (op +) A B" + +instance .. + +end + +instantiation matrix :: ("{uminus, zero}") uminus +begin + +definition + minus_matrix_def: "- A = apply_matrix uminus A" + +instance .. + +end + +instantiation matrix :: ("{minus, zero}") minus +begin -instance matrix :: ("{minus, zero}") minus - minus_matrix_def: "- A \ apply_matrix uminus A" - diff_matrix_def: "A - B \ combine_matrix (op -) A B" .. +definition + diff_matrix_def: "A - B = combine_matrix (op -) A B" + +instance .. + +end + +instantiation matrix :: ("{plus, times, zero}") times +begin + +definition + times_matrix_def: "A * B = mult_matrix (op *) (op +) A B" -instance matrix :: ("{plus, times, zero}") times - times_matrix_def: "A * B \ mult_matrix (op *) (op +) A B" .. +instance .. + +end + +instantiation matrix :: (lordered_ab_group_add) abs +begin -instance matrix :: (lordered_ab_group_add) abs - abs_matrix_def: "abs (A \ 'a matrix) \ sup A (- A)" .. +definition + abs_matrix_def: "abs (A \ 'a matrix) = sup A (- A)" + +instance .. + +end instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet proof