<div dir="ltr"><div><div><div>Thanks very much, Joe! </div>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. </div>Cheers, </div>Ramana </div><div class="gmail_extra"> <div class="gmail_quote">On 4 February 2016 at 19:59, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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 <div class="HOEnZb"><div class="h5"> On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> 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 <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> 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 <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> 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 <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> >>>> 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 >>>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> > >>>> >>>> _______________________________________________ >>>> opentheory-users mailing list >>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>> >>> >> >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> </div>