On 15 May 2011, at 19:28, Phil Clayton wrote:

> This sounds very useful - only today I was having to introduce lambda terms 
> for rewriting to match with... but in Z, not HOL.  

Presumably this is to use theorems involving Z applications?

> Will these higher-order matching/rewriting facilities be implemented for Z 
> also? If not, does the updated rewriting infrastructure support a 
> corresponding implementation for ProofPower-Z?

The infrastructure will support any way of turning a theorem into a pair 
comprising a pattern term and a conversion to apply to terms that match the 
pattern. But bear in mind that higher-order matching for HOL just won't work 
for Z. If you are designing theorems specifically for use as higher-order 
rewrite rules, it might be simpler to write them in a mixture of HOL and Z so 
you can use higher-order matching.

> I can see Z has complications for lambda abstractions not over U but 
> expecting the domain condition as per z_%beta%_conv seems ok.

I think you will find there are several other complications - not least of 
which will be working out what higher-order matching for Z ought to do.



> Phil
> Rob Arthan wrote:
>> Dear All,
>> I am looking at higher-order rewriting. The cleanest way to implement it 
>> will involve adding an extra parameter to the functions prim_rewrite_conv, 
>> prim_rewrite_rule and prim_rewrite_tac (which I suspect aren't very widely 
>> used). The parameter value will be optional and supplying Nil will give the 
>> same behaviour as currently. If anybody has code that would be badly 
>> affected by this, please let me know.
>> Regards,
>> Rob.
>> ------------------------------------------------------------------------
>> _______________________________________________
>> Proofpower mailing list
> _______________________________________________
> Proofpower mailing list

Proofpower mailing list

Reply via email to