Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-19 Thread Manuel Eberl
Oh, well, yes, a special case of metric completion (the reals) was
mentioned in passing, I think. And a more general notion (something like
the completion of a topological group, I think?) featured in my Algebra
1 course, which was an elective. But "metric completion" as such I have
not heard before.

Lipschitz continuity is certainly undergraduate material. That probably
appears in any introductory Analysis lecture, even those for computer
scientists.

Manuel


On 2018-01-19 12:01, Tjark Weber wrote:
> On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
>>> One possible criterion: which results 
>>> are part of a standard undergraduate  athematics curriculum?
>> It sounds like a reasonable criterion. Can you tell us what that means for 
>> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?
> Metric completion features prominently, e.g., in the construction of
> the reals. Lipschitz continuity (along with the Picard–Lindelöf
> theorem) should be part of any course on differential equations.
>
> I can't recall whether I've been taught about Hausdorff distance or
> even isometries during my undergraduate years. Of course, these are
> fairly simple concepts.
>
> Best,
> Tjark
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-19 Thread Tjark Weber
On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote:
> > One possible criterion: which results 
> > are part of a standard undergraduate  athematics curriculum?
> 
> It sounds like a reasonable criterion. Can you tell us what that means for 
> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?

Metric completion features prominently, e.g., in the construction of
the reals. Lipschitz continuity (along with the Picard–Lindelöf
theorem) should be part of any course on differential equations.

I can't recall whether I've been taught about Hausdorff distance or
even isometries during my undergraduate years. Of course, these are
fairly simple concepts.

Best,
Tjark


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Lawrence Paulson
I'm afraid I've no idea. I didn't study much analysis for my first degree, not 
even the basics of complex analysis.

Larry

> On 18 Jan 2018, at 14:29, Tobias Nipkow  wrote:
> 
> So what is the situation wrt the theories I asked about?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Manuel Eberl
I for one have not encountered any of these things in my undergraduate
mathematics lectures. But the situation may well be different in other
universities.


On 2018-01-18 15:29, Tobias Nipkow wrote:
> So what is the situation wrt the theories I asked about?
>
> Tobias
>
> On 18/01/2018 15:11, Lawrence Paulson wrote:
>> This is mainly a negative criterion, i.e., something outside the
>> undergraduate curriculum probably should not be in our core
>> libraries. But I would guess for example mathematicians cover Gödel's
>> theorem, which we would not want to move to our core libraries.
>>
>> Larry
>>
>>> On 18 Jan 2018, at 13:31, Tobias Nipkow  wrote:
>>>
>>> It sounds like a reasonable criterion. Can you tell us what that
>>> means for Hausdorff_Distance, Metric_Completion and Isometries (as
>>> detailed by Fabian)?
>>
>
>
>
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Tobias Nipkow

So what is the situation wrt the theories I asked about?

Tobias

On 18/01/2018 15:11, Lawrence Paulson wrote:

This is mainly a negative criterion, i.e., something outside the undergraduate 
curriculum probably should not be in our core libraries. But I would guess for 
example mathematicians cover Gödel's theorem, which we would not want to move 
to our core libraries.

Larry


On 18 Jan 2018, at 13:31, Tobias Nipkow  wrote:

It sounds like a reasonable criterion. Can you tell us what that means for 
Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?






smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Lawrence Paulson
This is mainly a negative criterion, i.e., something outside the undergraduate 
curriculum probably should not be in our core libraries. But I would guess for 
example mathematicians cover Gödel's theorem, which we would not want to move 
to our core libraries.

Larry

> On 18 Jan 2018, at 13:31, Tobias Nipkow  wrote:
> 
> It sounds like a reasonable criterion. Can you tell us what that means for 
> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Fabian Immler


> Am 18.01.2018 um 14:36 schrieb Tobias Nipkow :
> 
> 
> 
> On 18/01/2018 11:06, Fabian Immler wrote:
>>> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow :
>>> 
>>> 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.

Fabian

>> 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



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Tobias Nipkow



On 18/01/2018 11:06, Fabian Immler wrote:



Am 18.01.2018 um 08:32 schrieb Tobias Nipkow :

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Tobias Nipkow


On 18/01/2018 12:48, Lawrence Paulson wrote:

We certainly need to solve this problem.


Absolutely. For practical reasons I would put as much in the AFP as possible, 
(One could make exceptions for small theories, but this could get out of hand 
again).


One possible criterion: which results 
are part of a standard undergraduate  athematics curriculum?


It sounds like a reasonable criterion. Can you tell us what that means for 
Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?


Tobias


Larry

On 18 Jan 2018, at 10:06, Fabian Immler > wrote:


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.




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Lawrence Paulson
We certainly need to solve this problem. One possible criterion: which results 
are part of a standard undergraduate  athematics curriculum?
Larry

> On 18 Jan 2018, at 10:06, Fabian Immler  wrote:
> 
> 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.



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] Gromov Hyperbolicity

2018-01-18 Thread Fabian Immler

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

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



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev