Email Gateway (Aug 22 2022 at 10:54): Email Gateway (Aug 22 2022 at 10:54):From: Peter Lammich <lammich@in.tum.de>
Hi list,
one of the Eisbach features that I use most is the solves-method.
In an apply-style script, I write "solves <auto>" and the like for
documentation purposes: This method is intended to solve the goal. This
makes apply-scripts much more maintainable.
However, the solves is quite tedious to write: When developing the
proof, you can only add it after your method works. And if something
breaks, you have to remove the solve to inspect the failure.
Is it possible to have some nice short suffix syntax for solves,
something like "apply auto!", similar to "apply auto []" ?
Can such a syntax be declared in without changing Isabelle, or would it
require a modification of the Isabelle sources?
Email Gateway (Aug 22 2022 at 10:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
You can use the method fail as in "apply(auto; fail)" to indicate that a proof method does
not generate new subgoals, which is equivalent to solves. This is slightly shorter than
removing solves, but you could define f as an alias to the method fail and just write
apply (auto;f)
which looks almost like what you want.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 12:29):From: Makarius <makarius@sketis.net>
Isabelle2016-RC0 allows a more systematic form:
subgoal by auto
Note that such higher structures don't work with schematic goals.
Makarius
Last updated: Apr 18 2024 at 20:16 UTC