[isabelle-dev] beta redexes

Makarius makarius at sketis.net
Tue Nov 20 16:28:19 CET 2012

Refurbishing the old ref manual in sunny Sicily recently, I've come across 
the following tidbit, which is now updated in Isabelle/c5cc24781cbf for 
the isar-ref manual:

   \item Higher-order patterns in the sense of \cite{nipkow-patterns}.
   These are terms in @{text "\<beta>"}-normal form (this will
   always be the case unless you have done something strange) ...

This was probably written by Tobias about 20 years ago, in the heroic 
times when the advanced higher-order rewriting engine was implemented.

So beta redexes within rewrite rules are considered "strange".  From 
empirical observations in the past 10 years, I can confirm that they are 
also "strange" in the terms being simplified, and in other situations as 

One can put a filter before things like rewrite_conv to smash incoming 
redexes, but it is futile to make non-normal terms the general rule.  Many 
other tools will suddenly become "broken" by such a "fix".


More information about the isabelle-dev mailing list