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


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.