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.
------------------------------------------------------------------------------
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
