Re: [Isarmathlib-devel] Polynomial ring revision

[Slawomir Kolodynski]

> 1. NatOrder_ZF is no more used.
I will keep it though. It will be useful for other things.

> I am being lazy
I think you are being more diligent this way. But you do the work, you decide. 
I will do the finitely supported functions anyway.

Are you interested in getting CVS access to IsarMathLib sources repositories? I 
wouldn't like you contributions to wait until I have time to add them.

I can't wait to see when you get to proving the distributivity of the 
polynomial addition with respect to multiplication. I think it is quite 
difficult. 

Slawek

--- On Tue, 6/17/08, Sanghyeon Seo  wrote:

> From: Sanghyeon Seo 
> Subject: [Isarmathlib-devel] Polynomial ring revision
> To: address@hidden
> Date: Tuesday, June 17, 2008, 10:42 PM
> 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_______________________________________________
> Isarmathlib-devel mailing list
> address@hidden
> http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel