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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
