Stream: Beginner Questions

Topic: Tactic that fails with no premises


view this post on Zulip Lukas Stevens (Aug 05 2020 at 11:27):

Is there a tactic that fails if there are no premises and otherwise succeeds?

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:31):

In Isabelle, I usually just write apply (my_tac; fail) if I expect my_tac to solve everything.

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:31):

In ML, there is a SOLVED combinator.

view this post on Zulip Lukas Stevens (Aug 05 2020 at 11:32):

But there being no premises does not mean that the goal is solved. To the contrary in my case, it means that my tactic cannot do anything.

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:33):

Err, it's called SOLVE

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:33):

Oh, sorry, premises… no, I don't think so.

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:36):

It should be easy enough to write one with Subgoal.FOCUS_PREMS though.

view this post on Zulip Manuel Eberl (Aug 05 2020 at 11:37):

If it has to be fast, it might be better to write a tactic that directly examines the tactic state (using e.g. COND) without going through Subgoal.FOCUS_PREMS. Although Makarius might frown on that.


Last updated: Sep 25 2021 at 08:21 UTC