Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
>> The only disadvantage I can think of right now, compared to >> list-based polynomials, is that "length" is easier to reason about >> than "degree". However, this is probably just a matter of finding a >> good set of lemmas about "degree". > > I am not sure about this. I think there is still an isomorphism between > "polynomial degree" and "list length" which can be made explicit e.g. by > a constant > > coeffs :: 'a poly => 'a list > > such that > > p != 0 ==> length (coeffs p) = Suc (degree p) > > or something alike. Some proofs in Univ_Poly.thy rely on the following property of list length: length p = n ==> length q = n ==> length (p +++ q) = n Unfortunately, a similar property does not hold for degree; in the case where the leading terms cancel, the sum may have a smaller degree than either p or q. It would be rather inconvenient to have to consider this case separately in all those proofs. However, it may be more useful to note that (length p = n) for the list representation is really equivalent to the statement (degree p < n) for the abstract representation (at least, for p ~= 0). Polynomial.thy probably needs to have more lemmas for reasoning about bounds on the degree of polynomials, such as: degree p < n ==> degree q < n ==> degree (p + q) < n With the right set of such lemmas, I think the proofs in Univ_Poly.thy could be adapted rather easily. - Brian
