[opentheory-users] removing definitions from theories

[Ramana Kumar]

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> 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> 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>
> 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
> >>
>
> _______________________________________________
> 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/20160204/976231b3/attachment-0001.html>