Idiomatischer Beweis durch Widerspruch in Isabelle?

Question

Bisher habe ich Beweise von Widerspruch in der folgenden Art in Isabelle (ein Muster von Jeremy Siek verwenden):

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

Gibt es eine Möglichkeit, die ohne den verschachtelten rohen Beweis funktioniert { ... } blockieren?

Answer 1

Es ist die Regel ccontr für klassische Beweise durch Widerspruch:

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

Es manchmal by contradiction verwenden kann helfen, den letzten Schritt zu beweisen.

Es gibt auch die Regel classical (die weniger intuitiv aussieht):

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

Weitere Beispiele classical finden Sie unter $ISABELLE_HOME/src/HOL/Isar_Examples/Drinker.thy

Answer 2

Zum besseren Verständnis der Regel classical es kann in strukturiertem Isar Stil gedruckt werden wie folgt:

print_statement classical 

Ausgabe:

theorem classical: 
    obtains "¬ thesis" 

So das reine Böse Intuitionisten erscheint ein bisschen mehr intuitiv: um eine willkürliche These zu beweisen, können wir davon ausgehen, dass ihre Negation hält.

Das entsprechende kanonische Nachweis Muster ist folgende:

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

?thesis Hier ist die konkrete These der obigen Ansprüche von A, die eine beliebig komplexen Anweisung sein kann. Diese Quasi-Abstraktion über die Abkürzung ?thesis ist typisch für idiomatische Isar, um die Denkstruktur zu betonen.