[isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]

[Thiemann, Rene]

Dear Florian,

thanks for the info.

Concerning the factorial semiring, we also made some development in that direction which we required
for the algebraic numbers. To be more precise, we have an instance of

poly :: (ufd) ufd

where ufd is a unique factorization domain, cf.

http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Domain.html
and
http://afp.sourceforge.net/browser_info/current/AFP/Algebraic_Numbers/Unique_Factorization_Poly.html

Perhaps we should share efforts on this topic (but please after the ITP deadline).

Cheers,
René

> Am 18.02.2016 um 17:00 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> 
> Hi Rene,
> 
> see now fd049b54ad68 for an abstract semiring_gcd with a corresponding
> poly :: (field) semiring_gcd instance.
> 
> Btw. in my pipeline there is an abstract factorial ring with
> 
> 	subclass (in factorial_semiring) semiring_gcd
> 
> and hence the possibility to formulate also the other prominent instance
> 
> 	poly :: (factorial_semiring) factorial_semiring
> 
> This will still take some time however.
> 
> Cheers,
> 	Florian
> 
> Am 15.01.2016 um 12:12 schrieb Thiemann, Rene:
>> 
>>> Am 14.01.2016 um 15:36 schrieb Makarius <makarius at sketis.net>:
>>> 
>>> On Thu, 14 Jan 2016, Florian Haftmann wrote:
>>> 
>>>>>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>>>>>> thus very hardly different from syntactic classes, so there is no loss
>>>>>> of generality here.
>>>>> 
>>>>> I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015 have
>>>>> the three essential lemmas:
>>>>> 
>>>>> gcd_dvd1, gcd_dvd2, and gcd_greatest.
>>>> 
>>>> indeed, but these are exactly the assumptions of the type class.
>>>> 
>>>>> And since you want to include the patch anyway, why not include at least the instance now?
>>>> 
>>>> It sits on top of a couple of other patches definitely not suitable for
>>>> inclusion by now.
>>> 
>>> Does it mean this thread is closed concerning Isabelle2016?
>> 
>> If Florian has a post-release patch available and wants to insert exactly that patch,
>> then that’s fine for me.
>> 
>> Then Isabelle users (including myself) can just load the proposed instance declaration from the AFP to
>> uniformly access the gcd-properties via the semiring-class(-axioms) in Isabelle 2016.
>> 
>> Cheers,
>> René
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> --
> 
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160222/1b361776/attachment.sig>