> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow <nip...@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 
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.

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.


Attachment: smime.p7s
Description: S/MIME cryptographic signature

isabelle-dev mailing list

Reply via email to