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