Я пытаюсь создать очень короткое доказательство для данного факта.Я хотел бы просто использовать команды в стиле apply.Теперь структура моей теоремы выглядит следующим образом:
theorem
statement
apply(some commands)
proof -
fix t assume "some predicate"
from some assumptions "some_theorem"
by(some commands)
qed
Итак, если я хочу сделать свое доказательство минимальным, я должен действительно атаковать строки:
fix t assume "some predicate"
from some assumptions "some_theorem"
, которая в основном реализует доказательствос полным утверждением:
⋀ param. A ⟹ B
Мой вопрос: есть ли хак, который позволит мне закодировать доказательство такого утверждения в стиле apply вместо языка доказательства Isar?