CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2600

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

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?

Upvotes: 0

Views: 113

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1951

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).

Upvotes: 0

Related Questions