Rob,

Rob Arthan wrote:
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?

Yes.


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.

Yes, I don't expect it to given that HOL lambda is totally different to Z lambda.


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'm guessing you mean use e.g. HOL function application instead of Z function application, HOL for all instead of Z for all etc. as required? I may well take up that idea if a theorem exposes the underlying HOL anyway but probably wouldn't want to 'dirty' otherwise pure Z theorems.


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.

I may have a think about that once I've had a look at your HOL version!

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@lemma-one.com <mailto:Proofpower@lemma-one.com>
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com




_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com <mailto:Proofpower@lemma-one.com>
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


------------------------------------------------------------------------

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com




_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to