Rob, Rob Arthan wrote:

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

This sounds very useful - only today I was having to introduce lambdaterms 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 implementedfor Z also? If not, does the updated rewriting infrastructure supporta corresponding implementation for ProofPower-Z?The infrastructure will support any way of turning a theorem into a paircomprising a pattern term and a conversion to apply to terms that matchthe pattern. But bear in mind that higher-order matching for HOL justwon'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 ashigher-order rewrite rules, it might be simpler to write them in amixture 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 butexpecting the domain condition as per z_%beta%_conv seems ok.I think you will find there are several other complications - not leastof 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 implementit will involve adding an extra parameter to the functionsprim_rewrite_conv, prim_rewrite_rule and prim_rewrite_tac (which Isuspect aren't very widely used). The parameter value will beoptional and supplying Nil will give the same behaviour as currently.If anybody has code that would be badly affected by this, please letme 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