2013-05-18 9 views

Antwort

5

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

+3

Wenn '' ist riesig, ist es bequem mit 'annehmen" ~? These "' zu beginnen. – chris

+1

Eine Nebenbemerkung: 'ccontr '(die AFAIK Abkürzung" klassischen Widerspruch ") ist auch klassische Argumentation. Daher klingt es ein bisschen komisch, das zweite Muster _classical reasoning_ zu nennen. – chris

+0

@chris, du hast recht, ich sollte diesen Verweis auf "klassisches Denken" ändern. Aber was wäre dann das beste Wort, um die Regel "klassisch" zu beschreiben? –

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.