[isabelle-dev] semiring_gcd [was: Isabelle2016-RC0: potential changes]
florian.haftmann at informatik.tu-muenchen.de
Thu Feb 18 17:00:55 CET 2016
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 836 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev