Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?

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.


On 10/22/2016 12:59 PM, Rob Arthan wrote:

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.