Rather than subtyping, I believe the approach in HOL Light is to use the finite cartesian products framework to write things analogous to
!x : real[‘a] y : real [‘b]. … The same sort of thing is possible in HOL if you inherit from fcpTheory. The HOL4 uses of fcp have been very focused on the hardware applications, but the infrastructure needed for HOL Light’s stuff may not be too hard to port. Michael From: "Chun Tian (binghe)" <binghe.l...@gmail.com> Date: Thursday, 21 February 2019 at 10:35 To: Umair Siddique <umair....@gmail.com> Cc: hol-info <hol-info@lists.sourceforge.net>, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>, Michael Norrish <michael.norr...@data61.csiro.au> Subject: subtypeTools (was Re: [Hol-info] 0 / 0 = 0 ???) 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<mailto:umair....@gmail.com>> ha scritto: 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 - 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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> 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
