equal
deleted
inserted
replaced
21 |
21 |
22 instance matrix :: ("{plus, times, zero}") times |
22 instance matrix :: ("{plus, times, zero}") times |
23 times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" .. |
23 times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" .. |
24 |
24 |
25 instance matrix :: (lordered_ab_group_add) abs |
25 instance matrix :: (lordered_ab_group_add) abs |
26 abs_matrix_def: "abs A \<equiv> sup A (- A)" .. |
26 abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" .. |
27 |
27 |
28 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet |
28 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet |
29 proof |
29 proof |
30 fix A B C :: "('a::lordered_ab_group_add) matrix" |
30 fix A B C :: "('a::lordered_ab_group_add) matrix" |
31 show "A + B + C = A + (B + C)" |
31 show "A + B + C = A + (B + C)" |