Theory Jordan_Normal_Form.Show_Matrix

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
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