[isabelle-dev] Eisbach and HOL-Analysis
wl302 at cam.ac.uk
Tue Apr 30 18:18:31 CEST 2019
It is good to know that we are going to have another wonderful decision procedure in Isabelle.
Personally, I will vote for the Isabelle/ML approach, since well-written Isabelle/ML code does not seem much harder to understand (to me) than Eisbach implementations. Also, if we consider the Analysis library a basic library (compared to those in the AFP), reduced dependency might be preferred.
> On 30 Apr 2019, at 16:33, Fabian Immler <immler at in.tum.de> wrote:
> Hey everyone,
> Maximilian (in cc) ported HOL-Light's decision procedure for metric spaces , and currently has two prototype implementations, one in Isabelle/ML, and the other one as an Eisbach method.
> Now we are wondering which one to finalize and include in HOL-Analysis (the idea is to use it to automate and simplify proofs about metric spaces in the library, as well).
> The Eisbach method is more readable and therefore easier to understand and maintain, but it would pull in Eisbach as an additional dependency.
> Any opinions on whether or not adding Eisbach to the dependencies of HOL-Analysis would be a bad idea?
> I remember that at some point, importing Eisbach changed the implementation of the "of" attribute or something like that and therefore caused some problems down the line.
> (This is probably not relevant for Isabelle2019)
> Best regards,
>  https://arxiv.org/pdf/0904.3482
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev