These are good questions. You are right that the ring and topology examples aren’t as usable as one might like. If you want to do real formalisations of abstract algebra, you do want to be able to work with subsets of the whole of the type. See for example the treatment of groups in examples/miller/groups.
In principle, if you want to use a theory (rings say) that assumes the whole type, but you want to apply it to a subset of another type, you could define a third type that is isomorphic to your subset (this is what new_type_definition does), and then use the results from the ring theory to derive results about your new type. These results could in turn be translated to the subset of the original type through the isomorphisms that the new type principle establishes. I’m not aware of anyone trying to do this with any seriousness. The most extensive mechanisation of this sort of thing that I’m aware of for HOL4 is by my student Hing-Lun Chan. You can get it from http://bitbucket.org/jhlchan/hol It includes mechanisations of results from the theories of groups, rings and finite fields. Eventually, this mechanisation will probably end up in the HOL examples directory. - The reason that the “whole type” approach is used in places is because it’s simpler to work with, and if you are not wanting to do large developments over the full theory, it can still be quite useful. - The restricted quantifiers could be used to write results, but the support for these seems to get in the way more than help, so work in this area tends to expand the restricted quantifiers with their definitions, turning ?x::P. Q x into ?x. P x /\ Q x - I’m not sure I understand your final question. Certainly, it is easy to write contradictory axioms so that no type could be found to satisfy them. On the other hand, if there is a set that satisfies the given axioms, then it should be possible to show that a HOL type of the same cardinality does indeed satisfy those axioms. Best wishes, Michael On 4/9/17, 20:40, "Mario Castelán Castro" <marioxcc...@yandex.com> wrote: Hello. This is a question concerning the formalization of “generic” structures, like a group, ring, field, topological space, vector space, and so on. That is, structures that satisfy some “axioms” and need not be unique up to isomorphism. In the theory “ring” as found in the HOL4 library the definition of “is_ring r” requires that there is a type of elements of the ring “r”, call it “α”, and that the ring sum, product and inverse are functions “[α → ]α → α” that obey the ring axioms. It appears that if one wants to use this theory, one must have such a type “α”. Consider the case that I do not have such a type a-priory. Instead I have a larger type “β” where the elements that satisfy the predicate “P:β → bool” form a ring. Is there any way to apply the ring theory from the HOL4 library to this “subset” of β? If ringTheory used a predicate to represent ring elements “P:γ→bool” instead of a type, then there would be no such problem. Obviously this would require that the theorems of ring use the restricted quantifiers (“∀::P…”, “∃::P…”, et cetera). What is the reason that several theories in the HOL library use the approach of “type as the elements of the ring/topology/etc.” instead of “predicate as the sets of elements of the ring/topology/etc.”? Additionally, when one has a predicate and functions defined over the same type (as in my ring example above) that meet some algebraic axioms, is it always possible (in HOL4) to define a *type*, for which *all* elements meet the same algebraic axioms? Thanks. -- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
