[isabelle-dev] Beta/Eta normalisation and net matching.

[Makarius]

On Wed, 4 Aug 2010, Thomas Sewell wrote:

> I was about to have another attempt at speeding up a tactic we 
> implemented for L4.verified using net-matching. In reading Pure/net.ML I 
> spotted the comment "Requires operands to be beta-eta-normal." In 
> rereading the existing biresolution_from_nets_tac code, however, I 
> didn't spot any attempt to beta/eta normalise the terms passed.

BTW, Pure/item_net.ML provides a more modern interface to the same index 
structure, which is one of the main work-horses for efficient retrieval of 
rules.  In recent years it seems to be hardly known to newcomers to 
Isabelle.

There might be some corner cases where it fails to work, but I cannot 
recall to have this ever encountered in practice.  The usual survival 
strategy is to "do things how they are usually done", e.g. in the 
Simplifier, Classical Reasoner, many other proof tools.

In the worst case, your tool will fail to find rules where they are 
expected.  I do have my private collection of "formal Isabelle jokes" with 
extreme corner cases that are not really seen in practice, but we can 
ignore them here.


> It occurs to me that I don't even know whether theorems in Isabelle can 
> be assumed to be beta/eta normal.

The abstract type thm does not impose any particular form, but proper 
facts (those stored as official results for the user) are almost always 
normal according to Goal.norm_result.  This does not include beta/eta 
normalization, only the most basic rule format to make things work in 
practice.  This form has emerged over the years as a compromise of 
simplicity vs. flexibility for more exotic applications, where slightly 
non-normal theorems are required.  (Many years ago I did have beta 
normalization in the Isar internalization phase for terms.)


 	Makarius