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">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 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 class="HOEnZb"><div class="h5"> On Thu, Apr 5, 2012 at 11:25 PM, Ramana Kumar <<a href="mailto:ramana.kumar@gmail.com">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">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">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> >> > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a> </div></div></blockquote></div>