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 On 4/16/2019 7:29 AM, Lawrence Paulson wrote:
And what about metric spaces themselves? (Not that we could include very much in the next release, but still) LarryOn 15 Apr 2019, at 16:31, Fabian Immler <[email protected]> wrote: On 4/15/2019 5:57 AM, Lawrence Paulson wrote:In the context of the recent discussions about Algebra, we could revisit these issues in the context of metric spaces, which we still donβt have (except as type classes). A metric space has a carrier and a binary relation, so syntactically itβs similar to a monoid, except that we donβt expect to extend one with additional fields. So, at least, we should be able to avoid records. But what about the path from metric spaces to normed vector spaces, etc.?Do you mean with explicit carrier sets and without records? The algebraic part could look like this [1]: locale semigroup_add_on_with = fixes S::"'a set" and pls::"'aβ'aβ'a" assumes add_assoc: "a β S βΉ b β S βΉ c β S βΉ pls (pls a b) c = pls a (pls b c)" assumes add_mem: "a β S βΉ b β S βΉ pls a b β S" Which leads up to the notion of vector space [2]: "vector_space_on_with S pls mns um zero (scl::'a::field\<Rightarrow>_)" which looks horrible here because of the explicit mention of all of the parameters (I don't recall why). Written as a locale with named parameters, it would look much nicer: locale vector_space_on_with = ab_group_add_on_with + fixes scl::"'f::comm_ring_1β_" assumes "x β S βΉ y β S βΉ scl a (pls x y) = pls (scl a x) (scl a y)" β¦ For a normed vector space, I guess one would write something like this (assuming that the parameters for the carrier set have the same name in metric_space and vector_space_on_with) locale normed_vector_space = metric_space + vector_space_on_with + fixes norm::"'a => real" assumes "dist x y = norm (x - y)" assumes "norm (x + y) <= norm x + norm y" ... Fabian [1] http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Types_To_Sets/Examples/Group_On_With.thy#l12 [2] http://isabelle.in.tum.de/repos/isabelle/file/538919322852/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On_With.thy#l90Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
