Как сделать допущение о втором случае доказательства Изабель/Изар в случаях, когда явные права на месте?

У меня есть доказательство Изабель, структурированное следующим образом:

Первый случай на самом деле состоит из нескольких страниц, поэтому при чтении второго примера он уже не понятен случайному читателю, даже самому себе, к которому относится False. (Ну, это на самом деле, но не из чтения, только в интерактивной среде: если, например, в Isabelle/jEdit, вы поместите курсор после case False, вы увидите n ≠ 0 под "this" в Output панель.)

Итак, есть синтаксис, который позволяет сделать предположение о "ложном" случае явным, чтобы читатель не должен был взаимодействовать с IDE или прокручивать до ключевого слова proof, но может видеть предположение право на место?

Ответы

Ответ 1

В этом случае доказательство становится более читаемым, если явно сформулировать предположение о каждом случае:

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed

Ответ 2

Если случай False короче, просто поставьте его первым. Порядок доказательств в блоке Isar не имеет значения:

proof (cases "n = 0")
  case False
  show ?thesis sorry
next
  case True
  show ?thesis sorry
qed

Ответ 3

Isar допускает множество вариаций по одной и той же теме. Сохраняя исходный контур, вы можете сделать промежуточные факты такими:

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  from `n = 0` show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  from `n ≠ 0` show ?thesis sorry
qed

Это консервативное расширение исходного контура, т.е. оно не вносит никаких изменений в политику проверки, унификации, поиска и т.д.

Как правило, форма

note `prop`

эквивалентно

have "prop" by fact