subsection ‹Displaying Polynomials›
text ‹We define a method which converts polynomials to strings and registers it in the Show class.›
theory Show_Poly
imports
Show_Instances
"HOL-Computational_Algebra.Polynomial"
begin
fun show_factor :: "nat ⇒ string" where
"show_factor 0 = []"
| "show_factor (Suc 0) = ''x''"
| "show_factor n = ''x^'' @ show n"
fun show_coeff_factor where
"show_coeff_factor c n = (if n = 0 then show c else if c = 1 then show_factor n else show c @ show_factor n)"
fun show_poly_main :: "nat ⇒ 'a :: {zero,one,show} list ⇒ string" where
"show_poly_main _ [] = ''0''"
| "show_poly_main n [c] = show_coeff_factor c n"
| "show_poly_main n (c # cs) = (if c = 0 then show_poly_main (Suc n) cs else
show_coeff_factor c n @ '' + '' @ show_poly_main (Suc n) cs)"
definition show_poly :: "'a :: {zero,one,show}poly ⇒ string" where
"show_poly p = show_poly_main 0 (coeffs p)"
definition showsp_poly :: "'a :: {zero,one,show}poly showsp"
where
"showsp_poly p x = shows_string (show_poly x)"
instantiation poly :: ("{show,one,zero}") "show"
begin
definition "shows_prec p (x :: 'a poly) = showsp_poly p x"
definition "shows_list (ps :: 'a poly list) = showsp_list shows_prec 0 ps"
lemma show_law_poly [show_law_simps]:
"shows_prec p (a :: 'a poly) (r @ s) = shows_prec p a r @ s"
by (simp add: shows_prec_poly_def showsp_poly_def show_law_simps)
instance by standard (auto simp: shows_list_poly_def show_law_simps)
end
end