<div dir="ltr"><div><div><div>I am trying to build a compatibility bridge between HOL4's standard library and the OpenTheory standard library.<br><br></div>I've thought about (and started trying) various approaches.<br><br></div>The latest idea (due mostly to Michael Norrish) is:<br><ol><li>Record a theory containing the HOL4 standard library, entirely in the HOL4 namespace, depending only on the axioms of HOL.<br></li><li>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.</li><li>Instantiate all the ungrounded constants with constants from the OpenTheory standard library, and then also add the OpenTheory standard library.<br></li><li>Prove any remaining axioms.</li></ol></div>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.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 30 January 2016 at 03:52, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<br>
There's currently no tool support for this, but I don't think it would<br>
be too difficult to implement. What is your use-case?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div class="h5"><br>
On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> Hi,<br>
><br>
> Is it possible to take a theory that makes definitions of types/constants,<br>
> and then re-present the same theory _without_ making the definitions<br>
> (instead taking them as ungrounded constants, and the definitional 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 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>
</div></div>> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>