Идиоматическое доказательство противоречия в Изабель?

Question

До сих пор я писал доказательство от противного в следующем стиле в Изабелле (с использованием шаблона по Jeremy Siek):

lemma "<expression>" 
proof - 
    { 
    assume "¬ <expression>" 
    then have False sorry 
    } 
    then show ?thesis by blast 
qed 

Есть ли способ, который работает без вложенного необработанного доказательства блок { ... }?

Answer 1

Существует правило ccontr для классических доказательств от противного:

have "<expression>" 
proof (rule ccontr) 
    assume "¬ <expression>" 
    then show False sorry 
qed 

Это иногда может помочь использовать by contradiction доказать последний шаг.

Существует также правило classical (который выглядит менее интуитивным):

have "<expression>" 
proof (rule classical) 
    assume "¬ <expression>" 
    then show "<expression>" sorry 
qed 

Для дальнейших примеров использования classical см $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

Для лучшего понимания правила classical это может быть распечатано в структурированном стиле Изара например:

print_statement classical 

Выход:

theorem classical: 
    obtains "¬ thesis" 

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

Соответствующей каноническая модель Доказательства заключается в следующем:

notepad 
begin 
    have A 
    proof (rule classical) 
    assume "¬ ?thesis" 
    then show ?thesis sorry 
    qed 
end 

Здесь ?thesis является конкретным тезисом выше претензий A, который может быть произвольно сложным утверждением. Эта квази абстракция через аббревиатуру ?thesis типична для идиоматического Изара, чтобы подчеркнуть структуру рассуждений.