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