<div dir="ltr"><div><div><div>Hi Brian,<br><br></div>Could I trouble you to look for a copy of your OpenTheory-related code for Isabelle? I'd like to see if I can get it working.<br><br></div><div>Oh, actually I just found this link: <a href="http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory">http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory</a><br><br></div><div>So, I can get started with that, but if you have any comments or ideas they could probably still be helpful :)<br></div><div><br></div>Cheers,<br></div>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 6 July 2015 at 20:54, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Yes, if it works (or is close to working) I would like to get it incorporated into the Isabelle codebase. I'm not yet sure how to contribute things to Isabelle, but I imagine I'll find out within the next few months.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 23 May 2015 at 15:52, Brian Huffman <span dir="ltr"><<a href="mailto:brianh@cs.pdx.edu" target="_blank">brianh@cs.pdx.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I've hardly looked at it since I wrote it. It was never incorporated<br>
into the Isabelle codebase. I suppose it would probably work with the<br>
latest Isabelle, because it uses only the low-level proof kernel api,<br>
which doesn't change much any more.<br>
<br>
I'll have to look around to see where I have a copy of the source<br>
code; that was a couple of computers ago. Did you want to try to do<br>
something with it?<br>
<span><font color="#888888"><br>
- Brian<br>
</font></span><div><div><br>
<br>
On Sat, May 23, 2015 at 5:13 AM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>> wrote:<br>
> Hi Brian,<br>
><br>
> What's the status of your OpenTheory importer? Does it work with the<br>
> latest Isabelle? Was it incorporated into the main code base?<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
> On 15 April 2011 at 17:34, Brian Huffman <<a href="mailto:brianh@cs.pdx.edu" target="_blank">brianh@cs.pdx.edu</a>> wrote:<br>
>> On Thu, Apr 14, 2011 at 7:03 PM, Joe Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:<br>
>>> Hi Brian,<br>
>>><br>
>>> That is really great work! Am I right in thinking you can import the<br>
>>> parser-1.5 article binding all the input symbols and axioms to<br>
>>> existing ones in Isabelle? I would have guessed that Isabelle type<br>
>>> classes would have managed to get in the way at some point, but<br>
>>> perhaps this would only be for converting Isabelle proofs to<br>
>>> OpenTheory format?<br>
>><br>
>> Yes, each of the input constants of the article is mapped to a<br>
>> pre-existing Isabelle constant. Some of these existing Isabelle<br>
>> constants happen to be overloaded, but that doesn't cause any<br>
>> problems. This mapping of constant names does not even need to be<br>
>> one-to-one; for example, I imagine that "Number.Natural.+" and<br>
>> "Number.Integer.+" would map to the same overloaded "plus" constant in<br>
>> Isabelle.<br>
>><br>
>> Of course, exporting proofs from Isabelle is a completely different story.<br>
>><br>
>>> You mentioned that you prove a lot of theorems that the OpenTheory<br>
>>> article relies on, but it seems you could reduce this by processing a<br>
>>> set of OpenTheory packages that don't make any definitions. When I was<br>
>>> designing the standard theory library I tried to isolate packages that<br>
>>> made definitions and have them export just a minimal theorem interface<br>
>>> - most of the theorems are proved in packages that make no definitions<br>
>>> and so can be safely run to populate the [opentheory] set of theorems.<br>
>><br>
>> Your idea of keeping definitions in separate, minimal modules is a<br>
>> good design. I'm sure I could have greatly reduced the number of<br>
>> [opentheory] lemmas that I needed by finding the right additional<br>
>> article files to import; I was just too lazy to figure out how the<br>
>> packages were organized.<br>
>><br>
>>>> The importer should also extend these tables whenever it defines a new<br>
>>>> constant or type, but I haven't implemented this yet. Another nice<br>
>>>> feature would be a way for users to influence how the importer chooses<br>
>>>> names for newly-defined constants and types. Right now it takes the<br>
>>>> names directly from the strings in the article file, which isn't so<br>
>>>> nice for names like "HOLLight._dest_rec" (Isabelle's parser can't<br>
>>>> handle names that start with underscores).<br>
>>><br>
>>> You should find that constants and type operators with names like this<br>
>>> are never exported from a theory (i.e., never appear in exported<br>
>>> theorems), so it's perfectly safe to normalize their names to<br>
>>> something more acceptable to Isabelle. They are `local definitions'<br>
>>> that are used only in proofs.<br>
>><br>
>> Actually, it seems like it would be safe to rename *any* constant<br>
>> (whether exported or not) to any name that I want in Isabelle, as long<br>
>> as the importer keeps track of the name mapping so that later imports<br>
>> can use the same names.<br>
>><br>
>> I suppose I should write an "import_name" function that converts from<br>
>> OpenTheory names to Isabelle-friendly ones. It would be nice to<br>
>> parameterize this by a list of user-specified exceptions to the<br>
>> mapping, so you could say something like, "import this article, but<br>
>> when you define constant 'foo', call it 'bar' instead."<br>
>><br>
>>>> Once I clean up the code, I'm not sure what I should do with it... I<br>
>>>> suppose I could add it to the Isabelle repo, but I'm not sure if I<br>
>>>> want to advertise to Munich crowd that I've been doing all this work<br>
>>>> that is unrelated to finishing my thesis :)<br>
>>><br>
>>> I would very much like to see it live on in some fashion - my hope is<br>
>>> that more and more theories will be converted to OpenTheory packages,<br>
>>> and your code could be used to import them into Isabelle in a<br>
>>> principled way.<br>
>><br>
>> I suppose I'll add it to the Isabelle distribution at some point,<br>
>> maybe after I finish writing my thesis. In the meantime, I guess I can<br>
>> post the code to the list, so it will be archived and people can try<br>
>> it out.<br>
>><br>
>> - Brian<br>
>><br>
>> _______________________________________________<br>
>> opentheory-users mailing list<br>
>> <a href="mailto:opentheory-users@gilith.com" target="_blank">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>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>