Re: [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).

Fabian

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.

On 16 Apr 2019, at 14:08, Fabian Immler <imm...@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

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev