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

[Florian Haftmann]

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: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160218/acf099f7/attachment.asc>