<div dir="ltr">I was mainly just being lazy about trying to generate an article for a theorem that I "know must be somewhere as an intermediate in the standard library" (although maybe it actually wasn't). I ended up generating an article for it in HOL4, so I don't have a particularly strong need for these features any more. Thanks for your help though - the tips for putting together packages with exact dependencies etc. were useful. </div><div class="gmail_extra"> <div class="gmail_quote">On Fri, Jan 2, 2015 at 7:31 PM, 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, What you're proposing is certainly possible, but first I'd like to understand a bit more about your use-case for accessing intermediate theorems. At present the article standard and opentheory tool conspire to create an illusion that the intermediate theorems of the theory are irrelevant, and that only the imported assumptions and exported theorems are important. As a consequence of this abstraction, tools that process articles may feel free to replace any or all intermediate theorems so long as the assumption/theorem interface is maintained. Supporting post-hoc extraction of intermediate theorems and promoting them to exported theorems goes against this philosophy, because an article processing tool that changed intermediate theorems could break something downstream that was relying on them having a particular form to extract and export. Given the above, could you please elaborate on your use-case for accessing intermediate theorems of articles? Cheers, Joe <div class="HOEnZb"><div class="h5"> On Sat, Dec 20, 2014 at 9:31 PM, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote: > Hi Joe, > > On Sat, Dec 20, 2014 at 9:09 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >> >> > Show me the intermediate (i.e. unexported) theorems that arise when >> > running >> > an article. >> >> No, unfortunately not. The best it can do is tell you *how many* >> theorems are generated, by using the --inference option. >> >> Did you have any thoughts on a way to present intermediate theorems to the >> user? > > > What would be useful to me is if I could search for intermediate theorems > with a pattern. I'd guess you'd rather stay away from specifying parsing of > such patterns. I wouldn't mind, however, writing my pattern as OpenTheory > article commands for creating a term. I'd then like to get back all > intermediate theorems that match. > >> >> > Create an article that exports a previously unexported theorem, taking >> > an >> > existing article as input. >> >> Also no I'm afraid. > > > That's a pity. Would it be hard to add? Presuming we solve the problem above > of specifying an intermediate theorem. > > I guess for the moment I can get around this by using a custom reader that > looks for the theorem I want and cuts off the article as soon as it finds it > (and adds on an export). It would be nice if the opentheory tool had enough > features to support this itself, but maybe it's a little outside your design > goals? On the other hand, I think a good suite of powerful manipulations on > OpenTheory packages for a variety of purposes would help buy-in. > >> >> > Minimise an article for what is required for a particular theorem (I >> > think >> > the answer here is yes, by creating a package with the desired theorem >> > and >> > then asking for an article for it to be generated...?) >> >> Indeed. Suppose article foo.art exports a set of theorems containing a >> theorem T of interest, then you can create an article bar.art that >> proves T by axiom, and then run >> >> echo 'a { article: "foo.art" } main { import: a article: "bar.art" }' >> | opentheory info --article -o baz.art theory:- >> >> to get a minimal article baz.art proving T. > > > Great, thanks. > </div></div><div class="HOEnZb"><div class="h5">> _______________________________________________ > 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" 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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> </div>