Hi Ramana,<br>
<br>
[Sorry for the delayed responses, I am on vacation right now.]<br>
<br>
I'm sorry, I can't think of any way of selectively deleting definitions from an article<span></span>. Currently what's implemented in --skip-definitions is an all-or-nothing hammer.<br>
<br>
If you structured your export as a series of articles then you could use --skip-definitions on the ones that contained the definitions you wanted to skip, and then concatenate them together again using a suitable theory file.<br>
<br>
This is how the OpenTheory standard theory library is structured, with all definitions (of exported symbols) living in *-def theories, which export the defining properties of the symbols rather than the exact internal definition that you see with --skip-definitions. This structure allows you to replace all the definitions in the standard theory library with theory assumptions for their defining properties in one ugly command, as I demonstrate here:<br>
<br>
<a href="http://www.gilith.com/opentheory/mailing-list/2014-March/000368.html" target="_blank">http://www.gilith.com/opentheory/mailing-list/2014-March/000368.html</a><br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
On Thu, Feb 4, 2016 at 1:42 AM, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>> wrote:<br>
> Thanks very much, Joe!<br>
><br>
> Do you know a simple scheme by which one could skip definitions selectively?<br>
> I mean skip some but not all of the definitions in an article. I imagine<br>
> this is possible through some sequence of package unions or interpretations<br>
> (there's no intersection, though, is there?). If it's possible to do so<br>
> without re-recording any articles, that would be quite useful.<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
> On 4 February 2016 at 19:59, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>><br>
>> Hi Ramana,<br>
>><br>
>> I've just released a new version of the opentheory tool, namely<br>
>><br>
>> $ opentheory -v<br>
>> opentheory 1.3 (release 20160204)<br>
>><br>
>> which includes support for a --skip-definitions flag when generating<br>
>> article files. This switch replaces defined symbols with external<br>
>> symbols and definition theorems with theory assumptions.<br>
>><br>
>> For example, here is the unit theory with and without definitions:<br>
>><br>
>> $ opentheory info --article unit | opentheory info --theory article:-<br>
>> 2 external type operators: -> bool<br>
>> 8 external constants: = select ! /\ ==> ? ?! T<br>
>> 13 assumptions:<br>
>>   |- T<br>
>>   |- !t. t ==> t<br>
>>   |- (?) = \p. p ((select) p)<br>
>>   |- !t. (!x. t) <=> t<br>
>>   |- (!) = \p. p = \x. T<br>
>>   |- !t. (t <=> T) <=> t<br>
>>   |- !t. T /\ t <=> t<br>
>>   |- (==>) = \p q. p /\ q <=> p<br>
>>   |- !x y. x = y <=> y = x<br>
>>   |- (/\) = \p q. (\f. f p q) = \f. f T T<br>
>>   |- (?) = \p. !q. (!x. p x ==> q) ==> q<br>
>>   |- !f g. (!x. f x = g x) <=> f = g<br>
>>   |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'<br>
>> 1 defined type operator: Data.Unit.unit<br>
>> 1 defined constant: Data.Unit.()<br>
>> 5 theorems:<br>
>>   |- !v. v = Data.Unit.()<br>
>>   |- !f g. f = g<br>
>>   |- !e. ?fn. fn Data.Unit.() = e<br>
>>   |- !e. ?!fn. fn Data.Unit.() = e<br>
>>   |- !p. p Data.Unit.() ==> !x. p x<br>
>><br>
>> $ opentheory info --skip-definitions --article unit | opentheory info<br>
>> --theory article:-<br>
>> 3 external type operators: -> bool Data.Unit.unit<br>
>> 10 external constants: = ! /\ ==> ? ?! T Data.Unit.() HOLLight.one_ABS<br>
>>   HOLLight.one_REP<br>
>> 14 assumptions:<br>
>>   |- T<br>
>>   |- !t. t ==> t<br>
>>   |- !t. (!x. t) <=> t<br>
>>   |- (!) = \p. p = \x. T<br>
>>   |- (\a. HOLLight.one_ABS (HOLLight.one_REP a)) = \a. a<br>
>>   |- !t. (t <=> T) <=> t<br>
>>   |- !t. T /\ t <=> t<br>
>>   |- (==>) = \p q. p /\ q <=> p<br>
>>   |- (\r. HOLLight.one_REP (HOLLight.one_ABS r) <=> r) =<br>
>>      \r. let b <- r in b<br>
>>   |- !x y. x = y <=> y = x<br>
>>   |- (/\) = \p q. (\f. f p q) = \f. f T T<br>
>>   |- (?) = \p. !q. (!x. p x ==> q) ==> q<br>
>>   |- !f g. (!x. f x = g x) <=> f = g<br>
>>   |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'<br>
>> 5 theorems:<br>
>>   |- !v. v = Data.Unit.()<br>
>>   |- !f g. f = g<br>
>>   |- !e. ?fn. fn Data.Unit.() = e<br>
>>   |- !e. ?!fn. fn Data.Unit.() = e<br>
>>   |- !p. p Data.Unit.() ==> !x. p x<br>
>><br>
>> Hopefully this will help with your HOL4 interface project.<br>
>><br>
>> Cheers,<br>
>><br>
>> Joe<br>
>><br>
>> On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>> > Hi Ramana,<br>
>> ><br>
>> > Sorry I didn't reply sooner - I'm actually working right now on adding<br>
>> > functionality to the opentheory tool to replace definitions with<br>
>> > theory assumptions.<br>
>> ><br>
>> > Your plan seems sensible to me. And it's definitely an argument for<br>
>> > using Rob's new constant definition primitive as much as possible,<br>
>> > since classical definitions of the form |- c = t are often rather<br>
>> > esoteric.<br>
>> ><br>
>> > I'll let you know when I have something working.<br>
>> ><br>
>> > Cheers,<br>
>> ><br>
>> > Joe<br>
>> ><br>
>> > On Tue, Feb 2, 2016 at 9:48 PM, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> > wrote:<br>
>> >> Hi Joe,<br>
>> >><br>
>> >> Do you have any comments on the plan I described?<br>
>> >><br>
>> >> And/or would you be able to add the definition-removing functionality<br>
>> >> to the<br>
>> >> opentheory tool?<br>
>> >><br>
>> >> Thanks,<br>
>> >> Ramana<br>
>> >><br>
>> >> On 30 January 2016 at 12:57, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> >> wrote:<br>
>> >>><br>
>> >>> I am trying to build a compatibility bridge between HOL4's standard<br>
>> >>> library and the OpenTheory standard library.<br>
>> >>><br>
>> >>> I've thought about (and started trying) various approaches.<br>
>> >>><br>
>> >>> The latest idea (due mostly to Michael Norrish) is:<br>
>> >>><br>
>> >>> Record a theory containing the HOL4 standard library, entirely in the<br>
>> >>> HOL4<br>
>> >>> namespace, depending only on the axioms of HOL.<br>
>> >>> Remove from this theory all definitions of things that are already in<br>
>> >>> the<br>
>> >>> OpenTheory standard library. The constants should then become<br>
>> >>> ungrounded,<br>
>> >>> and where they were defined the article should instead add the<br>
>> >>> definitional<br>
>> >>> axioms as axioms.<br>
>> >>> Instantiate all the ungrounded constants with constants from the<br>
>> >>> OpenTheory standard library, and then also add the OpenTheory standard<br>
>> >>> library.<br>
>> >>> Prove any remaining axioms.<br>
>> >>><br>
>> >>> The feature I requested is for step 2. I realise now that I need to be<br>
>> >>> able to remove definitions selectively, not just remove them all.<br>
>> >>> There may<br>
>> >>> be some way to accomplish that even if the primitive functionality is<br>
>> >>> to<br>
>> >>> remove them all, though.<br>
>> >>><br>
>> >>> On 30 January 2016 at 03:52, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>> >>>><br>
>> >>>> Hi Ramana,<br>
>> >>>><br>
>> >>>> There's currently no tool support for this, but I don't think it<br>
>> >>>> would<br>
>> >>>> be too difficult to implement. What is your use-case?<br>
>> >>>><br>
>> >>>> Cheers,<br>
>> >>>><br>
>> >>>> Joe<br>
>> >>>><br>
>> >>>> On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar<br>
>> >>>> <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> >>>> wrote:<br>
>> >>>> > Hi,<br>
>> >>>> ><br>
>> >>>> > Is it possible to take a theory that makes definitions of<br>
>> >>>> > types/constants,<br>
>> >>>> > and then re-present the same theory _without_ making the<br>
>> >>>> > definitions<br>
>> >>>> > (instead taking them as ungrounded constants, and the definitional<br>
>> >>>> > theorems<br>
>> >>>> > as axioms).<br>
>> >>>> ><br>
>> >>>> > I know there is already this command:<br>
>> >>>> ><br>
>> >>>> > opentheory info --theorems ...<br>
>> >>>> ><br>
>> >>>> > which removes all the proofs, but it still keeps the definitions<br>
>> >>>> > in.<br>
>> >>>> ><br>
>> >>>> > Can I also remove the definitions?<br>
>> >>>> ><br>
>> >>>> > In essence, I want a totally axiomatic presentation of a theory.<br>
>> >>>> ><br>
>> >>>> > Thanks,<br>
>> >>>> > Ramana<br>
>> >>>> ><br>
>> >>>> > _______________________________________________<br>
>> >>>> > opentheory-users mailing list<br>
>> >>>> > <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >>>> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >>>> ><br>
>> >>>><br>
>> >>>> _______________________________________________<br>
>> >>>> opentheory-users mailing list<br>
>> >>>> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >>>> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >>><br>
>> >>><br>
>> >><br>
>> >><br>
>> >> _______________________________________________<br>
>> >> opentheory-users mailing list<br>
>> >> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >><br>
>><br>
>> _______________________________________________<br>
>> opentheory-users mailing list<br>
>> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
On Wed, Feb 3, 2016 at 11:42 PM, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>> wrote:<br>
> Thanks very much, Joe!<br>
><br>
> Do you know a simple scheme by which one could skip definitions selectively?<br>
> I mean skip some but not all of the definitions in an article. I imagine<br>
> this is possible through some sequence of package unions or interpretations<br>
> (there's no intersection, though, is there?). If it's possible to do so<br>
> without re-recording any articles, that would be quite useful.<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
> On 4 February 2016 at 19:59, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>><br>
>> Hi Ramana,<br>
>><br>
>> I've just released a new version of the opentheory tool, namely<br>
>><br>
>> $ opentheory -v<br>
>> opentheory 1.3 (release 20160204)<br>
>><br>
>> which includes support for a --skip-definitions flag when generating<br>
>> article files. This switch replaces defined symbols with external<br>
>> symbols and definition theorems with theory assumptions.<br>
>><br>
>> For example, here is the unit theory with and without definitions:<br>
>><br>
>> $ opentheory info --article unit | opentheory info --theory article:-<br>
>> 2 external type operators: -> bool<br>
>> 8 external constants: = select ! /\ ==> ? ?! T<br>
>> 13 assumptions:<br>
>>   |- T<br>
>>   |- !t. t ==> t<br>
>>   |- (?) = \p. p ((select) p)<br>
>>   |- !t. (!x. t) <=> t<br>
>>   |- (!) = \p. p = \x. T<br>
>>   |- !t. (t <=> T) <=> t<br>
>>   |- !t. T /\ t <=> t<br>
>>   |- (==>) = \p q. p /\ q <=> p<br>
>>   |- !x y. x = y <=> y = x<br>
>>   |- (/\) = \p q. (\f. f p q) = \f. f T T<br>
>>   |- (?) = \p. !q. (!x. p x ==> q) ==> q<br>
>>   |- !f g. (!x. f x = g x) <=> f = g<br>
>>   |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'<br>
>> 1 defined type operator: Data.Unit.unit<br>
>> 1 defined constant: Data.Unit.()<br>
>> 5 theorems:<br>
>>   |- !v. v = Data.Unit.()<br>
>>   |- !f g. f = g<br>
>>   |- !e. ?fn. fn Data.Unit.() = e<br>
>>   |- !e. ?!fn. fn Data.Unit.() = e<br>
>>   |- !p. p Data.Unit.() ==> !x. p x<br>
>><br>
>> $ opentheory info --skip-definitions --article unit | opentheory info<br>
>> --theory article:-<br>
>> 3 external type operators: -> bool Data.Unit.unit<br>
>> 10 external constants: = ! /\ ==> ? ?! T Data.Unit.() HOLLight.one_ABS<br>
>>   HOLLight.one_REP<br>
>> 14 assumptions:<br>
>>   |- T<br>
>>   |- !t. t ==> t<br>
>>   |- !t. (!x. t) <=> t<br>
>>   |- (!) = \p. p = \x. T<br>
>>   |- (\a. HOLLight.one_ABS (HOLLight.one_REP a)) = \a. a<br>
>>   |- !t. (t <=> T) <=> t<br>
>>   |- !t. T /\ t <=> t<br>
>>   |- (==>) = \p q. p /\ q <=> p<br>
>>   |- (\r. HOLLight.one_REP (HOLLight.one_ABS r) <=> r) =<br>
>>      \r. let b <- r in b<br>
>>   |- !x y. x = y <=> y = x<br>
>>   |- (/\) = \p q. (\f. f p q) = \f. f T T<br>
>>   |- (?) = \p. !q. (!x. p x ==> q) ==> q<br>
>>   |- !f g. (!x. f x = g x) <=> f = g<br>
>>   |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'<br>
>> 5 theorems:<br>
>>   |- !v. v = Data.Unit.()<br>
>>   |- !f g. f = g<br>
>>   |- !e. ?fn. fn Data.Unit.() = e<br>
>>   |- !e. ?!fn. fn Data.Unit.() = e<br>
>>   |- !p. p Data.Unit.() ==> !x. p x<br>
>><br>
>> Hopefully this will help with your HOL4 interface project.<br>
>><br>
>> Cheers,<br>
>><br>
>> Joe<br>
>><br>
>> On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>> > Hi Ramana,<br>
>> ><br>
>> > Sorry I didn't reply sooner - I'm actually working right now on adding<br>
>> > functionality to the opentheory tool to replace definitions with<br>
>> > theory assumptions.<br>
>> ><br>
>> > Your plan seems sensible to me. And it's definitely an argument for<br>
>> > using Rob's new constant definition primitive as much as possible,<br>
>> > since classical definitions of the form |- c = t are often rather<br>
>> > esoteric.<br>
>> ><br>
>> > I'll let you know when I have something working.<br>
>> ><br>
>> > Cheers,<br>
>> ><br>
>> > Joe<br>
>> ><br>
>> > On Tue, Feb 2, 2016 at 9:48 PM, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> > wrote:<br>
>> >> Hi Joe,<br>
>> >><br>
>> >> Do you have any comments on the plan I described?<br>
>> >><br>
>> >> And/or would you be able to add the definition-removing functionality<br>
>> >> to the<br>
>> >> opentheory tool?<br>
>> >><br>
>> >> Thanks,<br>
>> >> Ramana<br>
>> >><br>
>> >> On 30 January 2016 at 12:57, Ramana Kumar <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> >> wrote:<br>
>> >>><br>
>> >>> I am trying to build a compatibility bridge between HOL4's standard<br>
>> >>> library and the OpenTheory standard library.<br>
>> >>><br>
>> >>> I've thought about (and started trying) various approaches.<br>
>> >>><br>
>> >>> The latest idea (due mostly to Michael Norrish) is:<br>
>> >>><br>
>> >>> Record a theory containing the HOL4 standard library, entirely in the<br>
>> >>> HOL4<br>
>> >>> namespace, depending only on the axioms of HOL.<br>
>> >>> Remove from this theory all definitions of things that are already in<br>
>> >>> the<br>
>> >>> OpenTheory standard library. The constants should then become<br>
>> >>> ungrounded,<br>
>> >>> and where they were defined the article should instead add the<br>
>> >>> definitional<br>
>> >>> axioms as axioms.<br>
>> >>> Instantiate all the ungrounded constants with constants from the<br>
>> >>> OpenTheory standard library, and then also add the OpenTheory standard<br>
>> >>> library.<br>
>> >>> Prove any remaining axioms.<br>
>> >>><br>
>> >>> The feature I requested is for step 2. I realise now that I need to be<br>
>> >>> able to remove definitions selectively, not just remove them all.<br>
>> >>> There may<br>
>> >>> be some way to accomplish that even if the primitive functionality is<br>
>> >>> to<br>
>> >>> remove them all, though.<br>
>> >>><br>
>> >>> On 30 January 2016 at 03:52, Joe Leslie-Hurd <<a href="javascript:;" onclick="_e(event, 'cvml', 'joe@gilith.com')">joe@gilith.com</a>> wrote:<br>
>> >>>><br>
>> >>>> Hi Ramana,<br>
>> >>>><br>
>> >>>> There's currently no tool support for this, but I don't think it<br>
>> >>>> would<br>
>> >>>> be too difficult to implement. What is your use-case?<br>
>> >>>><br>
>> >>>> Cheers,<br>
>> >>>><br>
>> >>>> Joe<br>
>> >>>><br>
>> >>>> On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar<br>
>> >>>> <<a href="javascript:;" onclick="_e(event, 'cvml', 'ramana@member.fsf.org')">ramana@member.fsf.org</a>><br>
>> >>>> wrote:<br>
>> >>>> > Hi,<br>
>> >>>> ><br>
>> >>>> > Is it possible to take a theory that makes definitions of<br>
>> >>>> > types/constants,<br>
>> >>>> > and then re-present the same theory _without_ making the<br>
>> >>>> > definitions<br>
>> >>>> > (instead taking them as ungrounded constants, and the definitional<br>
>> >>>> > theorems<br>
>> >>>> > as axioms).<br>
>> >>>> ><br>
>> >>>> > I know there is already this command:<br>
>> >>>> ><br>
>> >>>> > opentheory info --theorems ...<br>
>> >>>> ><br>
>> >>>> > which removes all the proofs, but it still keeps the definitions<br>
>> >>>> > in.<br>
>> >>>> ><br>
>> >>>> > Can I also remove the definitions?<br>
>> >>>> ><br>
>> >>>> > In essence, I want a totally axiomatic presentation of a theory.<br>
>> >>>> ><br>
>> >>>> > Thanks,<br>
>> >>>> > Ramana<br>
>> >>>> ><br>
>> >>>> > _______________________________________________<br>
>> >>>> > opentheory-users mailing list<br>
>> >>>> > <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >>>> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >>>> ><br>
>> >>>><br>
>> >>>> _______________________________________________<br>
>> >>>> opentheory-users mailing list<br>
>> >>>> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >>>> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >>><br>
>> >>><br>
>> >><br>
>> >><br>
>> >> _______________________________________________<br>
>> >> opentheory-users mailing list<br>
>> >> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>> >><br>
>><br>
>> _______________________________________________<br>
>> opentheory-users mailing list<br>
>> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
>> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="javascript:;" onclick="_e(event, 'cvml', 'opentheory-users@gilith.com')">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>