Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

Dear all, with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a mat”. However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get the additional constraint that the dimensions of the matrix must be non-zero. To be more precise, assume the following

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear Florian, thanks for the explanation and the hint on style. The below pattern works perfectly in our formalization. Cheers, René > Am 31.08.2017 um 14:03 schrieb Florian Haftmann > : > > Note that the pattern above is avoided nowadays by an

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear Florian, >> - There have been some changes w.r.t. code-generation which now lead >> to runtime exception in the generated code. For instance, now >> I get code like >> “f x = Code.abort …” >> whereas in 2016-1 there was a proper code like >> “f x = some ordinary right-hand side” >> We

Re: [isabelle-dev] Towards the Isabelle2017 release

Dear all, let me share my opinions after porting IsaFoR to yesterdays development version: - In total the transition from our 2016-1 source went quite smooth (~ 14 hours for whole of IsaFoR) - Most changes have been caused by integrating session-qualified theory imports. This will also

Re: [isabelle-dev] Efficient code for Discrete.log

Hi Manual, thanks for your efforts, but I believe there is already a more efficient way to compute log2. In your implementation, consider your intlog2_aux which roughly requires y iterations if log2(x) = y, since you always just add 1 to the accumulator. For some of my applications this

Re: [isabelle-dev] Theory for discrete log etc.

Dear all, thanks Manuel and Florian for pointing to other variants of discrete logarithms. I would like to mention a fairly recent one in AFP/Sqrt_Babylonian/Log_Impl.thy. It defines log_floor and log_ceiling :: “int => int => nat”. The advantage of these functions are improved code

[isabelle-dev] Problem with factorial-ring in combination with containers

Dear all, in the following theory, the export-code fails: (Isabelle 957ba35d1338, AFP 618f04bf906f) theory Problem imports "~~/src/HOL/Library/Polynomial_Factorial" "$AFP/thys/Containers/Set_Impl" begin definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where "foo x y = gcd y

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

ere 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. > > Cheer

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

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,

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

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

[isabelle-dev] Isabelle2016-RC0: potential changes

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.

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

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

Re: [isabelle-dev] Isabelle2016-RC0: potential changes

>> 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:

Re: [isabelle-dev] [isabelle] Semirings in HOL/Algebra/Ring

Dear all, can someone please integrate the attached patch which introduces a locale for semirings. I tested the patch by running all sessions of the AFP though without ISABELLE_FULL_TEST: there have been no problems. Isabelle: db0b87085c16 AFP: 55e04ff27c52 Thanks, René Looks like