Вытащить все вхождения переменной индукции в заключение в Изабель

Question

Я считаю книгу «Изабель / HOL: помощник по проверке логики высшего порядка» очень хорошим справочным материалом для улучшения кодирования в стиле применения в Изабель.В нескольких частях книг (например, в разделе 9.2) авторы утверждают, что хорошей эвристикой для индукции является:

извлечение всех вхождений переменной индукции в заключение с помощью ⟶

но способ, которым они это делают, заключается в повторении цели как леммы с m вместо ⟹.Я хочу сделать это автоматически в стиле применения.Моя текущая цель имеет вид:

⋀ param. A ⟹ B

Как бы вы применили А к выводам, используя apply-style?

Answer 1

Собственным решением является использование метода atomize, например apply(atomize (full)) (раздел 9.5 в справочном руководстве).Также вы можете использовать apply(erule rev_mp).