Dowód tożsamości w Sprzeczności w Isabelle?

Question

Dotychczas pisałem dowód nie wprost w następującym stylu w Isabelle (z wykorzystaniem wzoru przez Jeremy Siek):

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

Czy istnieje sposób, który działa bez zagnieżdżonego surowego dowodu zablokować { ... }?

Answer 1

Jest regułą ccontr dla klasycznych dowód nie wprost:

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

może czasem pomóc w użyciu by contradiction udowodnić ostatni krok.

Istnieje również reguła classical (który wygląda mniej intuicyjne):

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

Dla dalszych przykładów wykorzystujących classical patrz $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

Dla lepszego zrozumienia reguły classical mogą być drukowane w uporządkowany styl Isar tak:

print_statement classical 

Wyjście:

theorem classical: 
    obtains "¬ thesis" 

Zatem czystego zła intuicjonistów pojawia się nieco bardziej intuicyjny: aby udowodnić jakąś arbitralną tezę, możemy założyć, że jego negacja trzyma.

Odpowiednie kanoniczne wzór odporny to:

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

tutaj ?thesis jest konkretna praca z powyższych zastrzeżeń, w A, który może być dowolnie skomplikowany stwierdzenie. Ta quasi abstrakcja za pomocą skrótu ?thesis jest typowa dla idiomatycznego Isar, aby podkreślić strukturę rozumowania.