src/HOL/Library/Polynomial.thy
changeset 54855 d700d054d022
parent 54489 03ff4d1e6784
child 54856 356b4c0a2061
equal deleted inserted replaced
54854:3324a0078636 54855:d700d054d022
   365 
   365 
   366 subsection {* Representation of polynomials by lists of coefficients *}
   366 subsection {* Representation of polynomials by lists of coefficients *}
   367 
   367 
   368 primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
   368 primrec Poly :: "'a::zero list \<Rightarrow> 'a poly"
   369 where
   369 where
   370   "Poly [] = 0"
   370   [code_post]: "Poly [] = 0"
   371 | "Poly (a # as) = pCons a (Poly as)"
   371 | [code_post]: "Poly (a # as) = pCons a (Poly as)"
   372 
   372 
   373 lemma Poly_replicate_0 [simp]:
   373 lemma Poly_replicate_0 [simp]:
   374   "Poly (replicate n 0) = 0"
   374   "Poly (replicate n 0) = 0"
   375   by (induct n) simp_all
   375   by (induct n) simp_all
   376 
   376