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

2010-08-05 Thread 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

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

2010-08-04 Thread Lawrence Paulson
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

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

2010-08-04 Thread Tjark Weber
On Wed, 2010-08-04 at 11:50 +1000, Thomas Sewell wrote: 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? There are various pieces of code that expect terms and

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

2010-08-03 Thread Thomas Sewell
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

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

2010-08-03 Thread 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