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

Question

Я пытаюсь доказать теорему, но застрял на подзадаче (которую я предпочитаю пропустить и доказать позже). Как я могу пропустить это и доказать другие?

Сначала я попробовал oops а также sorry но они оба прерывают все доказательство (вместо единственной подцели). Я также попытался поместить подцель в фиктивную лемму (предполагая, что sorryзатем использовать его (apply (rule [my dummy lemma])) но он применяет фиктивную лемму ко всем другим подзадачам (не только к первым).

Answer 1

Это в основном зависит от того, используете ли вы архаику (извините за это;)) в стиле apply или правильно структурированный Isar для доказательства. Я приведу небольшой пример, чтобы охватить оба стиля. Предположим, вы хотели доказать

lemma "A & B"

куда A а также B просто служить заполнителями для потенциально огромных формул.

В качестве структурированного доказательства вы бы сделали что-то вроде:

proof
  show "A" sorry
next
  show "B" sorry
qed

Т.е. в этом стиле вы можете использовать sorry опустить доказательства для подцелей.

В стиле применения вы могли бы сделать

apply (rule conjI)
defer -- "moves the first subgoal to the last position"
apply (*proof for subgoal "B"*)
apply (*proof for subgoal "A"*)

Также есть команда apply-style prefer n который движется подцель n спереди.