[isabelle-dev] Polynomial theory
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".
> 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.
More information about the isabelle-dev