Эквивалентность между применяемыми и изарскими стилями в Изабель

Question

Являются ли применяемые эквиваленты стиля и Isar-доказательства? Это вопрос, который у меня есть в течение некоторого времени. Конечно, доказательства Isar гораздо более читабельны, удобны в обращении и их легко написать (?), Но мой вопрос в том, можете ли вы доказать одно и то же в обоих стилях.

Например, в настоящее время я работаю над доказательством, в котором мне нужно уйти:

apply(simp split: prod.splits) 
using some_lemma by fastforce

Какова эквивалентная форма этих команд в стиле apply и Isar? На самом деле, меня больше интересует стиль Изар, поскольку мне говорят, что смешивать стили - это плохой стиль.

Answer 1

Эквивалентный стиль Изара будет:

have "P"
  using some_lemma by fastforce
then have "Q"
  by (simp split: prod.splits)

Где «P» представляет промежуточное целевое состояние после первого apply.

В общем, все доказуемое может быть доказано как в Изаре, так и в стиле apply; оба имеют свои сильные и слабые стороны.

Я лично использую стиль, в котором я пытаюсь структурировать свои доказательства снаружи-внутри: снаружи (например, индукция) Изара и, если необходимо, внутри (например, упрощение, низкоуровневые вещи) с помощью apply.

В общем, хотя я рекомендую вам как можно дольше оставаться в Изаре.