Hi, I'm in the process of importing a package from HOL Light into HOL4. I've generated an OpenTheory article, which uses the Number.Natural.bit0, which HOL4 doesn't understand. I have the numconv tool, which does conversion from bit0/bit1 numbers to bit1/bit2 numbers, but it doesn't work on whole articles yet. I would like input on how to design it so that it will. Here is what numconv does: <ul><li>Translate numeral representations within a term, producing a theorem |- t[rep1] = t[rep2]. </li><li>The input term is represented by a simple article with a single theorem containing the term.</li> <li>The output theorem is represented by an ordinary article, based on axioms in the standard library, and a few extra ones about bit2 if necessary. </li> </ul>What I would like: <ul><li>A tool to convert all numeral representations throughout an article, i.e.</li><li>turn an article based on the standard library into one that only uses numeral constants relevant to the desired representation. </li></ul>Ideas on a good route to achieve that? Cheers, Ramana <div class="gmail_quote">On Mon, Aug 20, 2012 at 8:52 PM, Ramana Kumar <<a href="mailto:ramana@xrchz.net" target="_blank">ramana@xrchz.net</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I have rewritten my standalone conversion between Norrish numerals and binary numerals. The code now lives here: <a href="https://gitorious.org/hol/ot/trees/master" target="_blank">https://gitorious.org/hol/ot/trees/master</a> (it is numconv.hs) Changes/Features: <ul><li>Now translates in both directions: Norrish -> Binary and Binary -> Norrish</li><li>Translates numerals recursively within any term (doesn't require a bare numeral as input)</li> <li> Optional "rule mode" proves t |- t' rather than |- t = t'; maybe useful for converting numerals in an already proved theorem and composing the resulting articles. </li><li>Refactored into several reusable Haskell modules</li> <li>Cleaned up code; it now doesn't emit any warnings with ghc's -Wall. </li></ul>I haven't tested it very much, especially in the from-binary direction. Test articles and use cases would be appreciated. The axioms in that direction are probably not in the standard library, but they are provable in HOL4... The next task I want to do is figure out how best to create a kind of "compatibility theory package" that would include those theorems (and other common prover-specific theorems) that can be added to the "requires:" of a package for easy use of packages coming out of specific provers. I look forward to your comments and tests for numconv :) And if you have ideas for other standalone proof tools, the OpenTheory Haskell modules are free to use.<div><div> <div class="gmail_quote"> On Fri, Apr 6, 2012 at 9:31 PM, Joe 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">Yep, looks like it works fine now, in case we ever need to de-Norrish some numerals from HOL Light. Cheers, Joe <div><div> On Thu, Apr 5, 2012 at 11:25 PM, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com" target="_blank">ramana.kumar@gmail.com</a>> wrote: > My code works fine on this article. The problem was my CGI script. It should > be fixed now. > (It had a call to runhaskell n2b.hs which got confused when called from > another directory, so now I've given it an absolute path to n2b.hs.) > > On Thu, Apr 5, 2012 at 11:10 PM, Joe Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: >> >> Hi Ramana, >> >> > My guess is that you're generating an article with HOLLight.BIT2 rather >> > than >> > Number.Natural.bit2, but I haven't actually run your attempt. >> > If that's not the problem it would be helpful if you could send me the >> > article that gets passed to the web tactic (or maybe I should have some >> > infrastructure for saving it...) >> >> I've attached the article encoding the goal: FYI the opentheory >> summary for it is: >> >> $ opentheory info n2b-goal.art >> 3 input type operators: -> bool Number.Natural.natural >> 5 input constants: F Function.K Number.Natural.bit1 Number.Natural.bit2 >> Number.Natural.zero >> 1 assumption: >> |- Function.K F >> (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0))) >> 1 theorem: >> |- Function.K F >> (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2 0))) >> >> > The function n2b near the top of the file is the algorithm. >> > It's been a while, so let's see if I can figure out the algorithm just >> > by >> > reading that code... >> >> Your algorithm looks absolutely fine, and should scale up to any size >> of natural number that a theorem prover could conceivably process. >> >> Cheers, >> >> Joe >> >> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com" target="_blank">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" target="_blank">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" target="_blank">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></div></blockquote></div>