[opentheory-users] removing definitions from theories
Joe Leslie-Hurd
joe at gilith.com
Fri Feb 12 08:49:10 UTC 2016
Hi Ramana,
[Sorry for the delayed responses, I am on vacation right now.]
I'm sorry, I can't think of any way of selectively deleting definitions
from an article. Currently what's implemented in --skip-definitions is an
all-or-nothing hammer.
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.
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:
http://www.gilith.com/opentheory/mailing-list/2014-March/000368.html
Cheers,
Joe
On Thu, Feb 4, 2016 at 1:42 AM, Ramana Kumar <ramana at member.fsf.org
<javascript:;>> wrote:
> Thanks very much, Joe!
>
> Do you know a simple scheme by which one could skip definitions
selectively?
> I mean skip some but not all of the definitions in an article. I imagine
> this is possible through some sequence of package unions or
interpretations
> (there's no intersection, though, is there?). If it's possible to do so
> without re-recording any articles, that would be quite useful.
>
> Cheers,
> Ramana
>
> On 4 February 2016 at 19:59, Joe Leslie-Hurd <joe at gilith.com
<javascript:;>> wrote:
>>
>> Hi Ramana,
>>
>> I've just released a new version of the opentheory tool, namely
>>
>> $ opentheory -v
>> opentheory 1.3 (release 20160204)
>>
>> which includes support for a --skip-definitions flag when generating
>> article files. This switch replaces defined symbols with external
>> symbols and definition theorems with theory assumptions.
>>
>> For example, here is the unit theory with and without definitions:
>>
>> $ opentheory info --article unit | opentheory info --theory article:-
>> 2 external type operators: -> bool
>> 8 external constants: = select ! /\ ==> ? ?! T
>> 13 assumptions:
>> |- T
>> |- !t. t ==> t
>> |- (?) = \p. p ((select) p)
>> |- !t. (!x. t) <=> t
>> |- (!) = \p. p = \x. T
>> |- !t. (t <=> T) <=> t
>> |- !t. T /\ t <=> t
>> |- (==>) = \p q. p /\ q <=> p
>> |- !x y. x = y <=> y = x
>> |- (/\) = \p q. (\f. f p q) = \f. f T T
>> |- (?) = \p. !q. (!x. p x ==> q) ==> q
>> |- !f g. (!x. f x = g x) <=> f = g
>> |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
>> 1 defined type operator: Data.Unit.unit
>> 1 defined constant: Data.Unit.()
>> 5 theorems:
>> |- !v. v = Data.Unit.()
>> |- !f g. f = g
>> |- !e. ?fn. fn Data.Unit.() = e
>> |- !e. ?!fn. fn Data.Unit.() = e
>> |- !p. p Data.Unit.() ==> !x. p x
>>
>> $ opentheory info --skip-definitions --article unit | opentheory info
>> --theory article:-
>> 3 external type operators: -> bool Data.Unit.unit
>> 10 external constants: = ! /\ ==> ? ?! T Data.Unit.() HOLLight.one_ABS
>> HOLLight.one_REP
>> 14 assumptions:
>> |- T
>> |- !t. t ==> t
>> |- !t. (!x. t) <=> t
>> |- (!) = \p. p = \x. T
>> |- (\a. HOLLight.one_ABS (HOLLight.one_REP a)) = \a. a
>> |- !t. (t <=> T) <=> t
>> |- !t. T /\ t <=> t
>> |- (==>) = \p q. p /\ q <=> p
>> |- (\r. HOLLight.one_REP (HOLLight.one_ABS r) <=> r) =
>> \r. let b <- r in b
>> |- !x y. x = y <=> y = x
>> |- (/\) = \p q. (\f. f p q) = \f. f T T
>> |- (?) = \p. !q. (!x. p x ==> q) ==> q
>> |- !f g. (!x. f x = g x) <=> f = g
>> |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
>> 5 theorems:
>> |- !v. v = Data.Unit.()
>> |- !f g. f = g
>> |- !e. ?fn. fn Data.Unit.() = e
>> |- !e. ?!fn. fn Data.Unit.() = e
>> |- !p. p Data.Unit.() ==> !x. p x
>>
>> Hopefully this will help with your HOL4 interface project.
>>
>> Cheers,
>>
>> Joe
>>
>> On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <joe at gilith.com
<javascript:;>> wrote:
>> > 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
<javascript:;>>
>> > 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
<javascript:;>>
>> >> 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
<javascript:;>> 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 <javascript:;>>
>> >>>> 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 <javascript:;>
>> >>>> > http://www.gilith.com/opentheory/mailing-list
>> >>>> >
>> >>>>
>> >>>> _______________________________________________
>> >>>> opentheory-users mailing list
>> >>>> opentheory-users at gilith.com <javascript:;>
>> >>>> http://www.gilith.com/opentheory/mailing-list
>> >>>
>> >>>
>> >>
>> >>
>> >> _______________________________________________
>> >> opentheory-users mailing list
>> >> opentheory-users at gilith.com <javascript:;>
>> >> http://www.gilith.com/opentheory/mailing-list
>> >>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com <javascript:;>
>> http://www.gilith.com/opentheory/mailing-list
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com <javascript:;>
> http://www.gilith.com/opentheory/mailing-list
>
On Wed, Feb 3, 2016 at 11:42 PM, Ramana Kumar <ramana at member.fsf.org
<javascript:;>> wrote:
> Thanks very much, Joe!
>
> Do you know a simple scheme by which one could skip definitions
selectively?
> I mean skip some but not all of the definitions in an article. I imagine
> this is possible through some sequence of package unions or
interpretations
> (there's no intersection, though, is there?). If it's possible to do so
> without re-recording any articles, that would be quite useful.
>
> Cheers,
> Ramana
>
> On 4 February 2016 at 19:59, Joe Leslie-Hurd <joe at gilith.com
<javascript:;>> wrote:
>>
>> Hi Ramana,
>>
>> I've just released a new version of the opentheory tool, namely
>>
>> $ opentheory -v
>> opentheory 1.3 (release 20160204)
>>
>> which includes support for a --skip-definitions flag when generating
>> article files. This switch replaces defined symbols with external
>> symbols and definition theorems with theory assumptions.
>>
>> For example, here is the unit theory with and without definitions:
>>
>> $ opentheory info --article unit | opentheory info --theory article:-
>> 2 external type operators: -> bool
>> 8 external constants: = select ! /\ ==> ? ?! T
>> 13 assumptions:
>> |- T
>> |- !t. t ==> t
>> |- (?) = \p. p ((select) p)
>> |- !t. (!x. t) <=> t
>> |- (!) = \p. p = \x. T
>> |- !t. (t <=> T) <=> t
>> |- !t. T /\ t <=> t
>> |- (==>) = \p q. p /\ q <=> p
>> |- !x y. x = y <=> y = x
>> |- (/\) = \p q. (\f. f p q) = \f. f T T
>> |- (?) = \p. !q. (!x. p x ==> q) ==> q
>> |- !f g. (!x. f x = g x) <=> f = g
>> |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
>> 1 defined type operator: Data.Unit.unit
>> 1 defined constant: Data.Unit.()
>> 5 theorems:
>> |- !v. v = Data.Unit.()
>> |- !f g. f = g
>> |- !e. ?fn. fn Data.Unit.() = e
>> |- !e. ?!fn. fn Data.Unit.() = e
>> |- !p. p Data.Unit.() ==> !x. p x
>>
>> $ opentheory info --skip-definitions --article unit | opentheory info
>> --theory article:-
>> 3 external type operators: -> bool Data.Unit.unit
>> 10 external constants: = ! /\ ==> ? ?! T Data.Unit.() HOLLight.one_ABS
>> HOLLight.one_REP
>> 14 assumptions:
>> |- T
>> |- !t. t ==> t
>> |- !t. (!x. t) <=> t
>> |- (!) = \p. p = \x. T
>> |- (\a. HOLLight.one_ABS (HOLLight.one_REP a)) = \a. a
>> |- !t. (t <=> T) <=> t
>> |- !t. T /\ t <=> t
>> |- (==>) = \p q. p /\ q <=> p
>> |- (\r. HOLLight.one_REP (HOLLight.one_ABS r) <=> r) =
>> \r. let b <- r in b
>> |- !x y. x = y <=> y = x
>> |- (/\) = \p q. (\f. f p q) = \f. f T T
>> |- (?) = \p. !q. (!x. p x ==> q) ==> q
>> |- !f g. (!x. f x = g x) <=> f = g
>> |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
>> 5 theorems:
>> |- !v. v = Data.Unit.()
>> |- !f g. f = g
>> |- !e. ?fn. fn Data.Unit.() = e
>> |- !e. ?!fn. fn Data.Unit.() = e
>> |- !p. p Data.Unit.() ==> !x. p x
>>
>> Hopefully this will help with your HOL4 interface project.
>>
>> Cheers,
>>
>> Joe
>>
>> On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <joe at gilith.com
<javascript:;>> wrote:
>> > 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
<javascript:;>>
>> > 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
<javascript:;>>
>> >> 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
<javascript:;>> 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 <javascript:;>>
>> >>>> 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 <javascript:;>
>> >>>> > http://www.gilith.com/opentheory/mailing-list
>> >>>> >
>> >>>>
>> >>>> _______________________________________________
>> >>>> opentheory-users mailing list
>> >>>> opentheory-users at gilith.com <javascript:;>
>> >>>> http://www.gilith.com/opentheory/mailing-list
>> >>>
>> >>>
>> >>
>> >>
>> >> _______________________________________________
>> >> opentheory-users mailing list
>> >> opentheory-users at gilith.com <javascript:;>
>> >> http://www.gilith.com/opentheory/mailing-list
>> >>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com <javascript:;>
>> http://www.gilith.com/opentheory/mailing-list
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com <javascript:;>
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160211/ee423490/attachment-0001.html>
More information about the opentheory-users
mailing list