5 |
5 |
6 theory Matrix |
6 theory Matrix |
7 imports MatrixGeneral |
7 imports MatrixGeneral |
8 begin |
8 begin |
9 |
9 |
10 instance matrix :: ("{zero, lattice}") lattice |
10 instantiation matrix :: ("{zero, lattice}") lattice |
11 "inf \<equiv> combine_matrix inf" |
11 begin |
12 "sup \<equiv> combine_matrix sup" |
12 |
|
13 definition |
|
14 "inf = combine_matrix inf" |
|
15 |
|
16 definition |
|
17 "sup = combine_matrix sup" |
|
18 |
|
19 instance |
13 by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def) |
20 by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def) |
14 |
21 |
15 instance matrix :: ("{plus, zero}") plus |
22 end |
16 plus_matrix_def: "A + B \<equiv> combine_matrix (op +) A B" .. |
23 |
17 |
24 instantiation matrix :: ("{plus, zero}") plus |
18 instance matrix :: ("{minus, zero}") minus |
25 begin |
19 minus_matrix_def: "- A \<equiv> apply_matrix uminus A" |
26 |
20 diff_matrix_def: "A - B \<equiv> combine_matrix (op -) A B" .. |
27 definition |
21 |
28 plus_matrix_def: "A + B = combine_matrix (op +) A B" |
22 instance matrix :: ("{plus, times, zero}") times |
29 |
23 times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" .. |
30 instance .. |
24 |
31 |
25 instance matrix :: (lordered_ab_group_add) abs |
32 end |
26 abs_matrix_def: "abs (A \<Colon> 'a matrix) \<equiv> sup A (- A)" .. |
33 |
|
34 instantiation matrix :: ("{uminus, zero}") uminus |
|
35 begin |
|
36 |
|
37 definition |
|
38 minus_matrix_def: "- A = apply_matrix uminus A" |
|
39 |
|
40 instance .. |
|
41 |
|
42 end |
|
43 |
|
44 instantiation matrix :: ("{minus, zero}") minus |
|
45 begin |
|
46 |
|
47 definition |
|
48 diff_matrix_def: "A - B = combine_matrix (op -) A B" |
|
49 |
|
50 instance .. |
|
51 |
|
52 end |
|
53 |
|
54 instantiation matrix :: ("{plus, times, zero}") times |
|
55 begin |
|
56 |
|
57 definition |
|
58 times_matrix_def: "A * B = mult_matrix (op *) (op +) A B" |
|
59 |
|
60 instance .. |
|
61 |
|
62 end |
|
63 |
|
64 instantiation matrix :: (lordered_ab_group_add) abs |
|
65 begin |
|
66 |
|
67 definition |
|
68 abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)" |
|
69 |
|
70 instance .. |
|
71 |
|
72 end |
27 |
73 |
28 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet |
74 instance matrix :: (lordered_ab_group_add) lordered_ab_group_add_meet |
29 proof |
75 proof |
30 fix A B C :: "('a::lordered_ab_group_add) matrix" |
76 fix A B C :: "('a::lordered_ab_group_add) matrix" |
31 show "A + B + C = A + (B + C)" |
77 show "A + B + C = A + (B + C)" |