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

[Tobias Nipkow]

There is no requirement or guarantee that theorems in general are in any
kind of normal form.

Tobias

Thomas Sewell schrieb:
> Hello Isabelle developers.
> 
> 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.
> 
> It occurs to me that I don't even know whether theorems in Isabelle can be assumed to be beta/eta normal. Does anyone have any quick pointers on that? Is there a potential bug here? Don't go searching for it - I'm happy to build some test cases and search for the answer myself if noone knows.
> 
> Yours,
>     Thomas.
> 
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev