Phil, 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. Regards, Rob. > 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 >> 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
