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 <makar...@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-...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
