Thanks for the paper links. Actually I was long wondering what was under HOL’s "examples/miller/subtypes/“ folder, now I realized it’s the implementation of the idea in this paper.
There’re some example code at the end of subtypeTools.sml in that folder: tt prove (``~3 IN nzreal``, SUBTYPE_TAC (context_subtypes hol_c)); tt prove (``(MAP inv (CONS (~1) (MAP sqrt [3; 1]))) IN list nzreal``, SUBTYPE_TAC (context_subtypes hol_c)); tt prove (``(\x :: negreal. FUNPOW inv n x) IN negreal -> negreal``, SUBTYPE_TAC (context_subtypes hol_c)); tt prove (``(!x :: nzreal. x / x = 1) ==> (5 / 5 = 3 / 3)``, SIMPLIFY_TAC hol_c []); I wonder if this whole technique could also support parameters in the subtype, e.g. using n-length real-number lists as the type of points in n-dimension Euclidean space - the idea I learnt from hol-light’s Multivariate analysis formalization. Things like ``!(x :: real^M) (y :: real^N). P x y`` would be nice. P. S. currently HOL’s “real_topologyTheory” (ported from hol-light) only supports one-dimensional real number set, but the whole theory (and its original proof scripts in hol-light) were actually valid for arbitrary higher dimensions. I’d like to have the same thing for HOL4 if possible. —Chun > Il giorno 20 feb 2019, alle ore 22:10, Umair Siddique <umair....@gmail.com> > ha scritto: > > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101&rep=rep1&type=pdf > > <http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101&rep=rep1&type=pdf> > > http://www.gilith.com/talks/tphols2001-subtypes.pdf > <http://www.gilith.com/talks/tphols2001-subtypes.pdf> > > > - Umair > > On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk <fr...@cs.ru.nl > <mailto:fr...@cs.ru.nl>> wrote: > Hi Ramana, > > >I think this is exactly what is impossible to do in HOL: > >it is a logic of total functions. > > I think that in PVS you _can_ do something like that, right? > Using the predicate subtypes. Even though PVS _also_ > only has total functions. > > And I _think_ there was a paper once about how to mimic > predicate subtypes in HOL. Does anyone remember the > reference? > > Freek > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info > <https://lists.sourceforge.net/lists/listinfo/hol-info> > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
