> Am 18.01.2018 um 14:36 schrieb Tobias Nipkow <nip...@in.tum.de>:
> On 18/01/2018 11:06, Fabian Immler wrote:
>>> 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 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.
With "Isometries" I meant the part of Isometries.thy that introduces 
isometry_on (this is only 150 lines). Lipschitz maps are another 350 lines.
The rest of Isometries.thy seems to be about geodesic spaces and 
quasi-isometries could indeed make a separate AFP entry.


>> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

isabelle-dev mailing list

Reply via email to