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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Feb 18 17:00:55 CET 2016

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.


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:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160218/acf099f7/attachment.asc>

More information about the isabelle-dev mailing list