<div dir="ltr"><div><div>Thanks Brian. I'll keep a look out for mismatched set/predicate expectations. </div>Regarding OpenTheory.thy, the problem seemed more basic than that: the reader is not picking up the lemma defining "All" and therefore complains about an axiom not being found when it needs that lemma. I haven't yet had a chance to investigate it at all, so it might be something simple to fix. </div>I'm aware of Cezary Kaliszyk's work, indeed it's been discussed on this list before :) I've mainly been looking at it from the exporter perspective, but you make a good point that he also had an importer into Isabelle for his traces, so yes that could be a source of useful information if it's been kept up to date. </div><div class="gmail_extra"> <div class="gmail_quote">On 2 October 2015 at 10:54, Brian Huffman <<a href="mailto:huffman@galois.com" target="_blank">huffman@galois.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana, I think it's great that you've revived my old opentheory importer; I haven't worked on it for years and don't remember many details about how it works. I don't plan on doing any more maintenance on my old repo, so I'm happy to have all future development move to github. If you are having problems with OpenTheory.thy, I can think of one possible reason: Sometime around 2010-2012, Isabelle changed type 'a set into an abbreviation for 'a => bool, and then later changed it back into a separate type again. I'm not 100% sure, but I think the importer was written during the 'a => bool time period. If opentheory uses 'a => bool as its set type, you might need to map opentheory set operations onto the corresponding Isabelle predicate operators instead. Another thing you might look into: Around 2012 Cezary Kaliszyk implemented an Isabelle importer for HOL Light proofs; at the time I remember looking at the code and noting that it was quite similar to my OpenTheory importer. Browsing through his publication list, I just found a paper about it: <a href="http://cl-informatik.uibk.ac.at/users/cek/docs/13/ckak-itp13.pdf" rel="noreferrer" target="_blank">http://cl-informatik.uibk.ac.at/users/cek/docs/13/ckak-itp13.pdf</a> If his importer has been maintained since then, it might be worth looking at. - Brian <div class="HOEnZb"><div class="h5"> On Thu, Oct 1, 2015 at 5:25 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: > Hello, > > Michael Norrish and I have taken Brian's importer and got it to at least > build on Isabelle2015. In the process we also converted to a git repository > and put it on GitHub. You can find it here: > > <a href="https://github.com/xrchz/isabelle-opentheory" rel="noreferrer" target="_blank">https://github.com/xrchz/isabelle-opentheory</a> > > We haven't been able to get Brian's demo OpenTheory.thy to work yet, and > it's quite possible we made mistakes in updating opentheory.ML. I hope > further updates can happen in the above repository, where it's easy for me > to accept contributions (pull requests), although further coordination on > the original repository would also be fine as long as it's being actively > maintained. > > Cheers, > Ramana > > On 31 August 2015 at 15:24, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: >> >> Hi Brian, >> >> 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. >> >> Oh, actually I just found this link: >> <a href="http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory" rel="noreferrer" target="_blank">http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory</a> >> >> So, I can get started with that, but if you have any comments or ideas >> they could probably still be helpful :) >> >> Cheers, >> Ramana >> >> On 6 July 2015 at 20:54, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote: >>> >>> 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. >>> >>> On 23 May 2015 at 15:52, Brian Huffman <<a href="mailto:brianh@cs.pdx.edu">brianh@cs.pdx.edu</a>> wrote: >>>> >>>> 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 >>>> >>>> >>>> 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>