Re: [isabelle] Short syntax for "solves <method>"



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

On 16/07/15 13:26, Peter Lammich wrote:

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?

--
   Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.