[opentheory-users] removing definitions from theories

[Joe Leslie-Hurd]

Hi Ramana,

Sorry I didn't reply sooner - I'm actually working right now on adding
functionality to the opentheory tool to replace definitions with
theory assumptions.

Your plan seems sensible to me. And it's definitely an argument for
using Rob's new constant definition primitive as much as possible,
since classical definitions of the form |- c = t are often rather
esoteric.

I'll let you know when I have something working.

Cheers,

Joe

On Tue, Feb 2, 2016 at 9:48 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> 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:
>>
>> Record a theory containing the HOL4 standard library, entirely in the HOL4
>> namespace, depending only on the axioms of HOL.
>> 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.
>> Instantiate all the ungrounded constants with constants from the
>> OpenTheory standard library, and then also add the OpenTheory standard
>> library.
>> 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
>>
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>