Значение уровня объекта в Изабель / HOL

Question

Я вижу, что многие теоремы в Изабель / HOL предпочитают метауровневую импликацию:

==>

вместо

-->

логика объекта c уровень, то есть логика более высокого порядка c импликация.

Изабель вики говорит, что грубо говоря, импликация мета-уровня должна использоваться для отделения предположений от заключения в утверждениях правила .

Кроме этого, что я должен знать об использовании значения объекта и метауровня? Я вижу, что последний используется в основном. Когда и для чего мне следует использовать HOL?

Answer 1

Я думаю, что короткий ответ: используйте ==>, когда это возможно, так как с ним легче работать, чем -->.

При этом, вы не должны слишком часто видеть ==> в коде вы пишете.

1. При написании леммы часто лучше использовать синтаксис assumes и shows.
2. Для промежуточных шагов с have существует синтаксис с if: have "B" if "A" вместо have "B ==> A"
3. Мета-импликация может использоваться только на верхнем уровне, поэтому, если у вас есть предикат в качестве аргумента функции, вы не можете использовать ==> в этом предикат.