[isabelle-dev] Polynomial theory

[Brian Huffman]

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