src/HOL/Matrix/Matrix.thy
changeset 15178 5f621aa35c25
parent 14940 b9ab8babd8b3
child 15481 fc075ae929e4
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Sep 03 10:27:05 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Sep 03 17:10:36 2004 +0200
     1.3 @@ -21,7 +21,10 @@
     1.4    times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
     1.5  
     1.6  lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
     1.7 -by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
     1.8 +  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
     1.9 +
    1.10 +lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
    1.11 +  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
    1.12  
    1.13  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.14  proof 
    1.15 @@ -284,7 +287,20 @@
    1.16    apply (auto)
    1.17    done
    1.18  
    1.19 +lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
    1.20 +  by (simp add: minus_matrix_def)
    1.21  
    1.22 +lemma join_matrix: "join (A::('a::lordered_ring) matrix) B = combine_matrix join A B"  
    1.23 +  apply (insert join_unique[of "(combine_matrix join)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_join_combine_matrix_join])
    1.24 +  apply (simp)
    1.25 +  done
    1.26  
    1.27 +lemma meet_matrix: "meet (A::('a::lordered_ring) matrix) B = combine_matrix meet A B"
    1.28 +  apply (insert meet_unique[of "(combine_matrix meet)::('a matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix)", simplified is_meet_combine_matrix_meet])
    1.29 +  apply (simp)
    1.30 +  done
    1.31 +
    1.32 +lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
    1.33 +  by (simp add: abs_lattice join_matrix)
    1.34  
    1.35  end