[isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

On 18/01/2018 11:06, Fabian Immler wrote:
> 
>> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow <nipkow at in.tum.de>:
>>
>> 1. Library/Complement contains both new generic material like "t3_space" but also new concepts like [mono_intros] for more automation in proving of inequalities. In short, there is a wealth of material that might be suitable for inclusion in HOL-Analysis.
>> I have already made a start by moving a few [simp] rules but that is it from me because I am not familiar enough with the Analysis material.
> Most of this looks like it could go to HOL-Analysis.
> 
>> 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of generic concepts that should go somewhere else.
>> We need a discussion on whether any of the theories deserve a separate AFP entry.
> In my opinion, Hausdorff_Distance and Metric_Completion are general enough to put them to HOL-Analysis.
> (They are also relatively short, so I am not sure if it is worth to create separate AFP entries.)
> 
> The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, and quasi-isometries.
> The very same definition of Lipschitz maps is also in AFP/Ordinary_Differential_Equations, so I take this as a strong indication to move Lipschitz maps to HOL-Analysis. Isometries also seem like a generically useful concept and could go to HOL-Analysis.

A lot of things are useful, but Isometries.thy is large and would also make a 
nice AFP entry.

Tobias

> My impression is that geodesic spaces and quasi-isometries are more specialised concepts (but that might also be just because I have never come across them up to now...). I have no real opinion on what to do with them.
> 
> 
> We do not have a precise specification of what HOL-Analysis is or should be. I think that makes it very hard to draw a line between material that should go to HOL-Analysis and what should remain in the AFP. So take this as just my personal view.
> 
> Fabian
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180118/cdac565e/attachment.bin>