And what about metric spaces themselves? (Not that we could include very much in the next release, but still) Larry
> On 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#l90 > > >> Larry >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
