Ken, Unfortunately, the paper by Ondrej Kuncar and Andrei Popescu that you cite gives a description of the definitional mechanisms in HOL that is about 25 years out of date. The new_specification mechanism allows implicit definitions and cannot be viewed as a syntactic abbreviation mechanism. There is a proof of the conservativeness of a (generalisation of) this mechanism in Andy Pitts’ Introduction to the HOL Logic (ref. [31] in the paper). new_specification is implemented in all the "HOL-based provers” listed in the paper.
Due to tinkering on my part around 2013, new_specification has been extended to relax certain constraints on polymorphism that it imposed. The resulting gen_new_specification has been proved conservative informally by me and formally in HOL4 by Ramana Kumar, Magnus Myreen and Scott Owens (see their and my papers in ITP 2014 and/or JAR 56(3)). gen_new_specification is implemented (to my knowledge) in HOL4, ProofPower and OpenTheory. Regards, Rob. ------------------------------------------------------------------------------ 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
