[isabelle-dev] locales, groups, metric spaces?

[Fabian Immler]

On 4/16/2019 10:26 AM, Lawrence Paulson wrote:
> In HOL Light, a metric space is an abstract type represented by pairs (S,d) where S is the carrier and d is the distance function. Could that be the best approach for us, or should we use a locale? But then the notion of a metric space is a property rather than a type.
Such an abstract type is a useful idiom to formalize mathematical 
structures (there are successful applications for measure spaces, 
topologies, homeomorphisms).

One advantage (of such an abstract type, compared to locales) is that 
the projection to the distance function is a global constant. This makes 
it easy to use find_theorems.

I don't know if anyone has experience with the abstract type idiom for 
hierarchies of structures. A disadvantage might be that instead of 
sublocale relations, I guess one would need to work with coercions from 
normed vector spaces, metric spaces, topological spaces, etc.
I don't really know what the limitations are and how well that works out 
in practice.

Fabian


>> On 16 Apr 2019, at 14:08, Fabian Immler <immler at in.tum.de> wrote:
>>
>> Combining it with the anonymous relativization efforts
>> https://github.com/xanonec/HOL-Types_To_Sets_Ext/blob/master/Topology/Topological_Space_OW.thy#L52
>> it could look like this:
>>
>> locale topological_space_ow =
>>   fixes 𝔘 :: "'at set" and τ :: "'at set ⇒ bool"
>>   assumes open_UNIV[simp, intro]: "τ 𝔘"
>>   assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
>>   assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
>>
>> locale metric_space_ow = topological_space_ow +
>>   fixes dist:: "'at ⇒ 'at ⇒ real"
>>   assumes open_dist: "S ⊆ 𝔘 ⟹ τ S ⟷ (∀x∈S. ∃e>0. ∀y. dist y x < e ⟶ y ∈ S)"
>>   assumes dist_eq_0_iff [simp]: "x ∈ 𝔘 ⟹ y ∈ 𝔘 ⟹ dist x y = 0 ⟷ x = y"
>>     and dist_triangle2: "x ∈ 𝔘 ⟹ y ∈ 𝔘 ⟹ dist x y ≤ dist x z + dist y z"
>>
>>
>> Of course, this is yet another approach and different from the "topology-as-value" approach from Abstract_Topology (http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Analysis/Abstract_Topology.thy#l19)
>>
>> One would need to think about if or how it makes sense to combine such a "locale-only" approach with a "topology-as-value"/"metric-space-as-value" approach.  (Projecting the topology out of the metric-space value and having these as parameters of the locales?)
>>
>> Fabian
> 

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