[opentheory-users] removing definitions from theories

[Ramana Kumar]

I am trying to build a compatibility bridge between HOL4's standard library
and the OpenTheory standard library.

I've thought about (and started trying) various approaches.

The latest idea (due mostly to Michael Norrish) is:

   1. Record a theory containing the HOL4 standard library, entirely in the
   HOL4 namespace, depending only on the axioms of HOL.
   2. Remove from this theory all definitions of things that are already in
   the OpenTheory standard library. The constants should then become
   ungrounded, and where they were defined the article should instead add the
   definitional axioms as axioms.
   3. Instantiate all the ungrounded constants with constants from the
   OpenTheory standard library, and then also add the OpenTheory standard
   library.
   4. Prove any remaining axioms.

The feature I requested is for step 2. I realise now that I need to be able
to remove definitions selectively, not just remove them all. There may be
some way to accomplish that even if the primitive functionality is to
remove them all, though.

On 30 January 2016 at 03:52, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> There's currently no tool support for this, but I don't think it would
> be too difficult to implement. What is your use-case?
>
> Cheers,
>
> Joe
>
> On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Hi,
> >
> > Is it possible to take a theory that makes definitions of
> types/constants,
> > and then re-present the same theory _without_ making the definitions
> > (instead taking them as ungrounded constants, and the definitional
> theorems
> > as axioms).
> >
> > I know there is already this command:
> >
> > opentheory info --theorems ...
> >
> > which removes all the proofs, but it still keeps the definitions in.
> >
> > Can I also remove the definitions?
> >
> > In essence, I want a totally axiomatic presentation of a theory.
> >
> > Thanks,
> > Ramana
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160130/d5a6354c/attachment.html>