Недавно я начал использовать больше OF как способ выполнения предположений леммы с помощью локальных теорем. Я также использую как способ дать конкретные значения переменным теоремы. Например, в следующей теореме:
periodic ?f ?k ⟹
0 < ?k ⟹
0 < ?d ⟹ sum ?f {0..?k - 1} = sum ?f {?d..?d + ?k - 1}
Я бы хотел снять periodic ?f ?k и 0 < ?k с OF, а затем применить для создания экземпляра ?d = 1. Текущий способ, которым я делаю это, состоит из двух шагов:
note lem = my_lemma[OF ...]
using lem[of ...]
Мне было интересно, есть ли более элегантный синтаксис для этого.