Как проверить на ложность в последствиях?

Question

В сложной лемме, которая, по сути, является следствием, можно ошибочно сформировать антецедент, который оказывается ложным.Есть ли какая-то поддержка в Изабель, чтобы избежать этой ситуации?

Answer 1

Вы можете использовать quickcheck для этого.В доказательстве, в котором вы подозреваете, что ваши предшественники не имеют места, локально попытайтесь доказать False:

lemma "P ∧ ¬ P ⟹ foobar"
proof -
  have False
    quickcheck

В случае, если вам нужен частный антецедент, вы также можете сделать это следующим образом:

context
  assumes "P ∧ ¬ P"
begin

lemma False
  nitpick
  quickcheck

end

Команда context открывает новый безымянный контекст с локальными гипотезами.Когда вы выходите из контекста, предположение добавляется ко всем теоремам.Там вы также можете использовать nitpick для поиска проблем.