Yes, that's called code_simp. The difference, however, is often several orders of magnitude, which makes code_simp unfeasible in most cases.
I always wondered /why/ it is that slow and whether this is just not optimised that well or whether it's some unavoidable bottleneck. Manuel On 17/08/2020 13:30, [email protected] wrote: > Hi > Isn't there a (slower) possibility to Eval via the simplifier? > > Peter > > > -------- Original Message -------- > Subject: Re: [isabelle-dev] A suggestion: call eval with try0 > From: Jasmin Blanchette <[email protected]> > To: "Dr A. Koutsoukou-Argyraki" <[email protected]> > CC: Isabelle-dev list <[email protected]> > > > Dear Angeliki, > > > eval is not one of the many methods called by try0, and to my > experience so far Sledgehammer doesn't suggest it either. > > I've noticed several very simple proofs that work just "by eval" > and yet automation won't suggest any proof. > > > > Do people agree that it would be practical to include eval in the > methods tried with try0? > > > > and would this be feasible ? > > 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.) > > 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". > > Cheers, > > Jasmin > > P.S. I believe your email might interest other users of Isabelle. > You might not reach them by writing to isabelle-dev. > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
