Hi Rob, you are right that we mention only the plain definitions in HOL and not the implicit ones, when we compare the definitional mechanism of HOL and Isabelle/HOL. (If this what you meant; I assume you didn't mean to say that the overloading in Isabelle is 25 years out of date). I clearly remember that one of the early versions of our paper contained the comment that the current HOL provers use the more powerful mechanism that you mentioned but I guess that it was lost during later editing. We will include it again into the journal version of the paper.
I wanted to comment on your statement that A. Pitts proved that definitions in HOL are conservative. Such statements are always a little bit puzzling to me because when you say conservative (without any modifier), I always think that you mean the notion that "nothing new can be proved if you extend your theory (by a definition)". I think a lot of people (including me) think that this is THE conservativity. There is also a notion of the model-theoretic conservativity that requires that every model of the old theory can be expanded to a model of the new theory. This is a stronger notion and implies the proof conservativity. As far as I know, A. Pitts considers only a subset of all possible models (so called standard models) in his proof and he only proves that these models can be extended from the old to the new theory. But as far as I know this does not imply the proof conservativity. Best, Ondrej On 10/22/2016 12:59 PM, Rob Arthan wrote: > 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
