Theory Show_Matrix
section ‹Converting Matrices to Strings›
text ‹We just instantiate matrices in the show-class by printing them as lists of lists.›
theory Show_Matrix
imports
Show.Show
Matrix
begin
subsection ‹For the @{class show}-class›
definition shows_vec :: "'a :: show vec ⇒ shows" where
"shows_vec v ≡ shows (list_of_vec v)"
instantiation vec :: ("show") "show"
begin
definition "shows_prec p (v :: 'a vec) ≡ shows_vec v"
definition "shows_list (vs :: 'a vec list) ≡ shows_sep shows_vec (shows '', '') vs"
instance
by standard (simp_all add: shows_vec_def show_law_simps shows_prec_vec_def shows_list_vec_def)
end
definition shows_mat :: "'a :: show mat ⇒ shows" where
"shows_mat A ≡ shows (mat_to_list A)"
instantiation mat :: ("show") "show"
begin
definition "shows_prec p (A :: 'a mat) ≡ shows_mat A"
definition "shows_list (As :: 'a mat list) ≡ shows_sep shows_mat (shows '', '') As"
instance
by standard (simp_all add: shows_mat_def show_law_simps shows_prec_mat_def shows_list_mat_def)
end
end