equal
deleted
inserted
replaced
19 diff_matrix_def: "A - B == combine_matrix (op -) A B" |
19 diff_matrix_def: "A - B == combine_matrix (op -) A B" |
20 minus_matrix_def: "- A == apply_matrix uminus A" |
20 minus_matrix_def: "- A == apply_matrix uminus A" |
21 times_matrix_def: "A * B == mult_matrix (op *) (op +) A B" |
21 times_matrix_def: "A * B == mult_matrix (op *) (op +) A B" |
22 |
22 |
23 lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)" |
23 lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)" |
24 by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le) |
24 by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le) |
|
25 |
|
26 lemma is_join_combine_matrix_join: "is_join (combine_matrix join)" |
|
27 by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le) |
25 |
28 |
26 instance matrix :: (lordered_ab_group) lordered_ab_group_meet |
29 instance matrix :: (lordered_ab_group) lordered_ab_group_meet |
27 proof |
30 proof |
28 fix A B C :: "('a::lordered_ab_group) matrix" |
31 fix A B C :: "('a::lordered_ab_group) matrix" |
29 show "A + B + C = A + (B + C)" |
32 show "A + B + C = A + (B + C)" |
282 apply (subst Rep_matrix_inject[symmetric]) |
285 apply (subst Rep_matrix_inject[symmetric]) |
283 apply (rule ext)+ |
286 apply (rule ext)+ |
284 apply (auto) |
287 apply (auto) |
285 done |
288 done |
286 |
289 |
287 |
290 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)" |
288 |
291 by (simp add: minus_matrix_def) |
|
292 |
|
293 lemma join_matrix: "join (A::('a::lordered_ring) matrix) B = combine_matrix join A B" |
|
294 apply (insert join_unique[of "(combine_matrix join)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join]) |
|
295 apply (simp) |
|
296 done |
|
297 |
|
298 lemma meet_matrix: "meet (A::('a::lordered_ring) matrix) B = combine_matrix meet A B" |
|
299 apply (insert meet_unique[of "(combine_matrix meet)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet]) |
|
300 apply (simp) |
|
301 done |
|
302 |
|
303 lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)" |
|
304 by (simp add: abs_lattice join_matrix) |
289 |
305 |
290 end |
306 end |