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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
