> Am 14.01.2016 um 15:36 schrieb Makarius :
>
> 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
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
Hi Rene,
>> 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
Dear all,
>
> I have already some post-release patches in the pipeline which would add
> this instance anyway. So, there is no demand for action here at the moment.
>
> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
> thus very hardly different from syntactic classes, so
Hi all,
> This is probably a question for Florian. I introduced Euclidean rings to
> allow a more systematic derivation of (constructive) GCDs about two
> years ago or so.
>
> Since then, Florian cleaned this up and improved it a lot, but from what
> I gathered, there is much to be done yet. I sh
On Mon, 11 Jan 2016, Manuel Eberl wrote:
I also noticed the ring_gcd instance for polynomials. Finalising the
changes to the GCD class hierarchy and updating the AFP entries that
rely on half-finished versions of this change (such as Echelon_Form) is
something that I should probably take care
On Tue, 12 Jan 2016, Manuel Eberl wrote:
So why should the small proof below be not integrated for the 2016
release?
This is probably a question for Florian. I introduced Euclidean rings to
allow a more systematic derivation of (constructive) GCDs about two years ago
or so.
As for the rel
thanks a lot; in the meantime, I deleted this material from the AFP-entries.
Ironically, quite a few of those facts were already proven independently
in other AFP entries by Wenda Li and/or me. (e.g. the ones about pcompose)
> So why should the small proof below be not integrated for the 201
Hi Manuel,
> I added the efficient code equations for fact and binomial, and similar ones
> for pochhammer and gbinomial.
>
> I also adapted everything from Square_Free_Factorization and
> Missing_Polynomial that seemed to be of general interest to me (especially
> the generalisation of the ty
I added the efficient code equations for fact and binomial, and similar
ones for pochhammer and gbinomial.
I also adapted everything from Square_Free_Factorization and
Missing_Polynomial that seemed to be of general interest to me
(especially the generalisation of the type of pderiv).
I also
>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
>> algebraic number.
> Oh, yes, you're right. It's in
> https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
> .
Ah, I see. Indeed: definit
I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
algebraic number.
Oh, yes, you're right. It's in
https://bitbucket.org/isa-afp/afp-devel/src/363fdbc2f28c2503095a245f00db3d2805ed3ff9/thys/Liouville_Numbers/Liouville_Numbers_Misc.thy
.
Its definitely not optimal, and you’
Hi Manuel,
> I already moved a few small lemmas.
Thanks.
> I also defined the notion of an algebraic number; as soon as your AFP entry
> works with the development version of Isabelle again (is that already the
> case?),
Yes, it should work. (At least, on Friday afternoon, it worked)
> I wil
I already moved a few small lemmas. I also defined the notion of an
algebraic number; as soon as your AFP entry works with the development
version of Isabelle again (is that already the case?), I will prove
equivalence of my definition in Poly_Deriv.thy to your definition in
Algebraic_Numbers a
Dear all,
there are some changes I would like to add for the upcoming release. It would
be nice, if someone can integrate them:
- improved code equations for binomial coefficients and certain
divmod-algorithms.
(cf.
http://afp.sourceforge.net/browser_info/devel/AFP/Algebraic_Numbers/Improve
15 matches
Mail list logo
