*To*: Rob Arthan <rda at lemma-one.com>, Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?*From*: OndÅej KunÄar <kuncar at in.tum.de>*Date*: Sat, 22 Oct 2016 21:07:16 +0200*Cc*: "Prof. Andrew M. Pitts" <Andrew.Pitts at cl.cam.ac.uk>, "Prof. Thomas F. Melham" <thomas.melham at balliol.ox.ac.uk>, cl-isabelle-users at lists.cam.ac.uk, Roger Bishop Jones <rbj at rbjones.com>, "Prof. Peter B. Andrews" <andrews at cmu.edu>, Andrei Popescu <a.popescu at mdx.ac.uk>, HOL-info list <hol-info at lists.sourceforge.net>*In-reply-to*: <B9CAE32E-026D-4ECB-B0BD-9D69ED2BAC69@lemma-one.com>*References*: <mailman.58165.1476751826.9767.hol-info@lists.sourceforge.net> <ac50a36e-5a5e-a356-6878-a5de00d02282@rbjones.com> <5E3CAC59-87D9-4C98-A58E-1B435A2F1E41@kenkubota.de> <B9CAE32E-026D-4ECB-B0BD-9D69ED2BAC69@lemma-one.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0

Hi Rob,

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.

**Follow-Ups**:**Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?***From:*Scott Owens

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

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

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

- Previous by Date: Re: [isabelle] [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family
- Next by Date: Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Previous by Thread: Re: [isabelle] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Next by Thread: Re: [isabelle] [Hol-info] definability of new types (HOL), overloaded constant definitions for axiomatic type classes (Isabelle) - Re: Who is ProofPower "by" (and STT)?
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list