src/HOL/Matrix/Matrix.thy
changeset 25764 878c37886eed
parent 25502 9200b36280c0
child 27484 dbb9981c3d18
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:15 2008 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Jan 02 15:14:17 2008 +0100
     1.3 @@ -7,23 +7,69 @@
     1.4  imports MatrixGeneral
     1.5  begin
     1.6  
     1.7 -instance matrix :: ("{zero, lattice}") lattice
     1.8 -  "inf \<equiv> combine_matrix inf"
     1.9 -  "sup \<equiv> combine_matrix sup"
    1.10 +instantiation matrix :: ("{zero, lattice}") lattice
    1.11 +begin
    1.12 +
    1.13 +definition
    1.14 +  "inf = combine_matrix inf"
    1.15 +
    1.16 +definition
    1.17 +  "sup = combine_matrix sup"
    1.18 +
    1.19 +instance
    1.20    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    1.21  
    1.22 -instance matrix :: ("{plus, zero}") plus
    1.23 -  plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" ..
    1.24 +end
    1.25 +
    1.26 +instantiation matrix :: ("{plus, zero}") plus
    1.27 +begin
    1.28 +
    1.29 +definition
    1.30 +  plus_matrix_def: "A + B = combine_matrix (op +) A B"
    1.31 +
    1.32 +instance ..
    1.33 +
    1.34 +end
    1.35 +
    1.36 +instantiation matrix :: ("{uminus, zero}") uminus
    1.37 +begin
    1.38 +
    1.39 +definition
    1.40 +  minus_matrix_def: "- A = apply_matrix uminus A"
    1.41 +
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45 +
    1.46 +instantiation matrix :: ("{minus, zero}") minus
    1.47 +begin
    1.48  
    1.49 -instance matrix :: ("{minus, zero}") minus
    1.50 -  minus_matrix_def: "- A \<equiv> apply_matrix uminus A"
    1.51 -  diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" ..
    1.52 +definition
    1.53 +  diff_matrix_def: "A - B = combine_matrix (op -) A B"
    1.54 +
    1.55 +instance ..
    1.56 +
    1.57 +end
    1.58 +
    1.59 +instantiation matrix :: ("{plus, times, zero}") times
    1.60 +begin
    1.61 +
    1.62 +definition
    1.63 +  times_matrix_def: "A * B = mult_matrix (op *) (op +) A B"
    1.64  
    1.65 -instance matrix :: ("{plus, times, zero}") times
    1.66 -  times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
    1.67 +instance ..
    1.68 +
    1.69 +end
    1.70 +
    1.71 +instantiation matrix :: (lordered_ab_group_add) abs
    1.72 +begin
    1.73  
    1.74 -instance matrix :: (lordered_ab_group_add) abs
    1.75 -  abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" ..
    1.76 +definition
    1.77 +  abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
    1.78 +
    1.79 +instance ..
    1.80 +
    1.81 +end
    1.82  
    1.83  instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet
    1.84  proof