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 t
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 interpretation
> with mixin definitions:
>
> lo
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 d
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 requ
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 implem
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 equations
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 x
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
> 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
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 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’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
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
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
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 lik
Dear Peter,
>> It's the operation identification phase of Autoref,
>> quite difficult to debug ... I have not yet looked at it due to
>> ITP-deadline.
>
> I found the culprit:
>
> summary: adapting entries to new Deriving mechanism
>
> in LTL_to_GBA-theory, this removes a linorder-constrai
16 matches
Mail list logo