This practically goes back to the dawn of time. Any theorem produced by resolution would be beta-eta-normal. And this includes most theorems, but certainly not all. Larry
On 4 Aug 2010, at 02:50, Thomas Sewell wrote: > 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
