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.

score 2 · Accepted Answer · answered Dec 19 '13 at 17:50

2

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.

answered Dec 19 '13 at 17:50

Brian Huffman

961
1
6
6

Brilliant, thanks Brian. That's just what I was after. Final question: do you have any tips for dealing with the case where `bar` is a very long formula? Can I, for instance, just tell `erule_tac` to work on assumption number 2? – John Wickerson Dec 20 '13 at 12:28
I should mention that `apply (erule rev_mp) back` works, but `back` is a bit ugly... – John Wickerson Dec 20 '13 at 12:29

score 1 · Answer 2 · answered Dec 19 '13 at 13:21

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.

Isabelle: Opposite of "intro impI"

2 Answers2