HI Rob,
I think it would be pretty easy. REWR_CONV and its M-N counterpart
HO_REWR_CONV are built from REWR_CONV0 which takes a "part_match"
function which actually determines how the lhs of the rewrite rule is
matched.
Type variables occurring in the hypotheses of the rewrite rule will not be
instantiated in the match.
Konrad.
On Sun, Dec 7, 2014 at 12:49 PM, Rob Arthan <r...@lemma-one.com> 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.
>
>
> ------------------------------------------------------------------------------
> 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
>
>
------------------------------------------------------------------------------
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
