Re: [isabelle] Polynomials over GF(2)



Hi Mark,

The Isabelle distribution contains two different formalizations of polynomials, each with its own tradeoffs.

First, there is Univ_Poly.thy, created by Amine Chaieb for use in his proof of the fundamental theorem of algebra. This theory is automatically included if your theory imports Complex_Main. It does not define a type constructor for polynomials, but rather implements all operations in terms of lists.

Second, there is the collection of theories in HOL/Algebra/poly, created by Clemens Ballarin. These theories define an actual type constructor for polynomials, and they also include a formalization of long division for polynomials, which I expect you would need for your application. Unfortunately, the theories are rather out of date, and do not use the same hierarchy of algebraic classes as the rest of Isabelle/HOL. If you use them, you might have to provide some extra instance proofs for the duplicated axclasses, and the proof automation is not as good as it could be (since many simprocs in Isabelle/HOL are specific to the type classes defined in Ring_and_Field.thy).

It would be nice to eventually merge these two theories, so that we could have a type constructor for polynomials that supports all of the usual operations, and is also integrated with the current type class hierarchy. I have already done a bit of tinkering with these theories, so if there is enough interest I would probably be willing to work on this some more.

For GF(2), you could just import the HOL-Word image and use 1-bit words. However, the Word library does not provide a field class instance for this type. It probably wouldn't be too much work to just define the type yourself.

Hope this helps,
- Brian


Quoting "Janney, Mark-P26816" <Mark.Janney at gdc4s.com>:

Greetings -

I am working on a formal development of an efficient software algorithm
to calculate a proprietary cyclic redundancy check (CRC). This CRC
itself is defined in the usual fashion in terms of polynomials over
GF(2).

Rather than re-invent the wheel, I'd like to re-use existing Isabelle
theories as much as possible.  I'm interested in theories in any of the
following areas:
  --  polynomials over a field
  --  GF(2)
  --  CRC specifications and algorithms

If anyone can point me towards such material, I would be grateful.
Thanks - Mark Janney








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.