Isabelle: Opposite of "intro impI"

Question

If my goal state is foo ==> bar --> qux, I know that I can use the statement

apply (intro impI)

to yield the goal state foo ==> bar ==> qux. What about the other direction? Which command will send me back to the goal state foo ==> bar --> qux?

---

The best I have come up with so far is

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar")

but that's rather clunky, and I'd like to learn if there's a nicer way.

Answer 1

Instead of

apply (rule_tac P="bar" in rev_mp, assumption, thin_tac "bar")

you can write

apply (erule_tac P="bar" in rev_mp)

where erule_tac eliminates the matched assumption for you so you don't need the thin_tac anymore.

Answer 2

I am assuming you want to stay in apply-style. Then this is just a puzzle with probably many possible solutions. Here is one:

apply (unfold atomize_imp, rule)

or a bit more explicit

apply (unfold atomize_imp, rule impI)

where the unfold atomize_imp replaces all occurrences of ==> by -->. Then, in general, you can specify the number of --> that should be replaced by ==> (starting from the left), by a corresponding number of rule (or rule impI).

Anyway, if you would use Isar-style than you just state what you want to have explicitly and almost any automatic tool will be able to fill in the rest.