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

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

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

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

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


proof isabelle isar
person Christoph Lange    schedule 18.05.2013    source источник
comment
Открыт снова! Давайте начнем с комментариев, не так ли?   -  person Andrew Barber    schedule 24.05.2013

Ответы (3)


arrow_upward
6
arrow_downward

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

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed
person Christoph Lange    schedule 18.05.2013
comment
NB: это не сработает, если вы измените порядок дел (как указано @LarsNoschinsiki в комментарии к моему ответу). - person Joachim Breitner; 04.09.2013

arrow_upward
5
arrow_downward

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

proof (cases "n = 0")
  case False
  show ?thesis sorry
next
  case True
  show ?thesis sorry
qed
person Joachim Breitner    schedule 19.05.2013
comment
В общем, если свойство, для которого мы проводим анализ случая, очень короткое (как в n = 0), я всегда предпочитаю явную версию вместо case False, case True для удобства чтения. (Как ни странно, с точки зрения композиционности все наоборот.) - person chris; 19.05.2013
comment
Обратите внимание, что вы можете изменить порядок наблюдений, только если вы вызываете метод cases с параметром. Если вы используете форму proof cases assume P ... next assume "~P" ..., то отрицательный случай должен быть вторым (поскольку в цели есть схемы, которые создаются первой командой show). - person Lars Noschinski; 09.06.2013
comment
Я даже не знал, что можно использовать cases без параметра :-) - person Joachim Breitner; 09.06.2013

arrow_upward
2
arrow_downward

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
person Makarius    schedule 09.10.2013