[Isarmathlib-devel] Polynomial ring revision

[Sanghyeon Seo]

A new revision.

1. NatOrder_ZF is no more used.
2. Per suggestion, use TheNeutralElement(R,A) instead of Z.
3. Problem of the zero polynomial and using the idea of finitely
supported functions. I am being lazy, and I revised the definition as:
{x : nat -> R. EX N:nat. ALL n:nat. N<n --> x`(n)=0}
This simplifies proofs.
4. Dropped the degree section.
5. Closure of addition. Thanks for noting func1_1_L1A.

Proof document at:
http://sparcs.kaist.ac.kr/~tinuviel/devel/isabelle/

-- 
Seo Sanghyeon

PolynomialRing_ZF.thy
Description: Binary data