[isabelle-dev] Eisbach and HOL-Analysis

[Wenda Li]

Hi Fabian,

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.

Best,
Wenda

> 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 [1], 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,
> Fabian
> 
> [1] https://arxiv.org/pdf/0904.3482
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev