[opentheory-users] removing definitions from theories

[Ramana Kumar]

Hi Joe,

Do you have any comments on the plan I described?

And/or would you be able to add the definition-removing functionality to
the opentheory tool?

Thanks,
Ramana

On 30 January 2016 at 12:57, Ramana Kumar <ramana at member.fsf.org> wrote:

> 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/20160203/6a69d8fb/attachment.html>