As Konrad said, we have two flavours of rewriter. The FREEZE_THEN thm_tactical can also be used to automate the "trick" whereby free variables get "frozen" in assumptions. See
http://hol.sourceforge.net/kananaskis-10-helpdocs/help/Docfiles/HTML/Tactic.FREEZE_THEN.html for documentation. This will indeed prevent type variable instantiation, though I'm struggling to imagine a scenario when you'd want it: how often do you have goals with free variables of the same name but different types? Michael On 08/12/14 05:49, Rob Arthan wrote: > I am working on a paper about a proof procedure and realised that > I was about to write something rather specific to ProofPower. > In ProofPower, the rewriting conversions and tactics treat > free variables on the left-hand side of the equations you are > rewriting with as constants and will only instantiate them to a > variable of the same name. I believe that HOL4 and > HOL Light don’t do this, i.e., the rewriting functions in those > systems will happily instantiate free variables on the left-hand side > of the equations. > > My question is this: how easy is it to code something like the > ProofPower behaviour in HOL4 or HOL Light? (The HOL4 > documentation for REWR_CONV implies that you can prevent x > being instantiated by adding x = x to the assumptions of the > rewriting theorems and then eliminating it afterwards, > but I couldn’t work out whether that would also inhibit > type instantiation, which I wouldn’t want to do.) > > If it makes any difference, I am specifically interested in rewriting > with Miller-Nipkow style higher-order matching rather than first-order > matching. I believe that the HOL Light rewriting functions all > use M-N style matching. I couldn’t figure out from the REWR_CONV > documentation what goes on in HOL4. > > Regards, > > Rob. ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server from Actuate! Instantly Supercharge Your Business Reports and Dashboards with Interactivity, Sharing, Native Excel Exports, App Integration & more Get technology previously reserved for billion-dollar corporations, FREE http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
