# [isabelle-dev] Polynomial theory

Brian Huffman brianh at cs.pdx.edu
Mon Jan 12 16:46:54 CET 2009

```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".
>
> "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