Hi<br>Isn't there a (slower) possibility to Eval via the simplifier?<br><br>Peter <div class="quote" style="line-height: 1.5"><br><br>-------- Original Message --------<br>Subject: Re: [isabelle-dev] A suggestion: call eval with try0<br>From: Jasmin Blanchette <j.c.blanchette@vu.nl><br>To: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk><br>CC: Isabelle-dev list <isabelle-dev@mailbroy.informatik.tu-muenchen.de><br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Angeliki,<br><br>> eval is not one of the many methods called by try0, and to my experience so far Sledgehammer doesn't suggest it either.<br>> I've noticed several very simple proofs that work just "by eval" and yet automation won't suggest any proof.<br>> <br>> Do people agree that it would be practical to include eval in the methods tried with try0?<br>> <br>> and would this be feasible ?<br><br>Technically, this would be very feasible. The question is more whether it's desirable to have "try0" and Sledgehammer suggest tactics that bypass the LCF-style kernel and its strong guarantees. These are not just "academic" worries. Just a few years ago, there was a debilitating bug in "eval" that made it succeed every time, even if your conjuecture was literally "False". (I can't find it in "NEWS", but I vividly remember the discussion on the mailing list.)<br><br>Maybe a mention "(oracle)" next to "eval" would be enough? If it's clear enough that "eval" doesn't have the same status as the other tactics, I wouldn't mind enhancing "try0" in this way. Many users who rely on "try0" are novices that learn Isabelle and its tactics partly through "try0".<br><br>Cheers,<br><br>Jasmin<br><br>P.S. I believe your email might interest other users of Isabelle. You might not reach them by writing to isabelle-dev.<br><br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></blockquote></div>