Hi Mario, | Is there some established standard as to how to represent a function | with a domain that may be smaller than the type? More specifically, I | need a representation of arbitrary products (i.e.: The "tuples" are | functions from an arbitrary set to the elements of the tuple) to | formalize theorems about product spaces in topology.
Unless you actually need to encode domain and codomain in the function (rather than treating them as other related parameters in your theorem) a reasonable "cheap" alternative is to use ordinary functions that map to some canonical value (say ARB = @x. F) outside the domain. This at least gives a set of functions of the right size so you can do things like talk about its cardinality and about the existence of a unique function in the usual way. And it is at the same time a normal kind of HOL function and can be applied as usual etc. In HOL Light there is an EXTENSIONAL constant (introduced by Marco Maggesi) to indicate that the function is restricted in this sense to a domain. And that is in turn used to create a dependent product construct of the kind you were talking about. See the definitions of "EXTENSIONAL" and "cartesian_product" here: https://github.com/jrh13/hol-light/blob/master/sets.ml Those in turn are used to define corresponding product structures in much the way you are probably doing or intending to do. For example see "product_group" here: https://github.com/jrh13/hol-light/blob/master/Library/grouptheory.ml and "product_topology" here https://github.com/jrh13/hol-light/blob/master/Multivariate/metric.ml To show how a typical theorem looks, here is Tychonoff's theorem about compactness of a product: COMPACT_IN_CARTESIAN_PRODUCT = |- !(tops:K->A topology) s k. compact_in (product_topology k tops) (cartesian_product k s) <=> cartesian_product k s = {} \/ !i. i IN k ==> compact_in (tops i) (s i) John. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
