Pull all occurrences of the induction variable into the conclusion in Isabelle

Question

I find the book "Isabelle/HOL: A Proof Assitant for Higher-Order logic" a very good reference to improve the apply-style coding in Isabelle. In several parts of the books (for instance section 9.2) the authors state that a good heuristic for induction is to:

pull all occurrence of the induction variable into the conclusion using ⟶

but the way they do this is by restating the goal as a lemma with the ⟶ instead of ⟹. I want to do this automatically in apply-style. My current goal is of the form:

⋀ param. A ⟹ B

How would you pull A into the conclusions using apply-style?

@xanonec, i mixed question that comment was intended for stackoverflow.com/questions/53486780/… — Rodrigo
@xanonec the command you indicated works perfect for me, feel free to add it as an answer — Rodrigo

user9716869 user9716869 · Accepted Answer · 2018-11-26T23:23:57

The native solution is to use the method atomize, e.g. apply(atomize (full)) (section 9.5 in the reference manual). Also, you can use apply(erule rev_mp).

Pull all occurrences of the induction variable into the conclusion in Isabelle

1 Answers