Neuordnen Ziele (Isabelle)

Question

Ich mag würde wissen, wie Ziele in der folgenden Situation neu zu ordnen:

lemma "P=Q" 
    proof (rule iffI, (*here I would like to swap goal order*), rule ccontr) 
oops 

Ich würde eine Lösung wie das beinhaltet nicht die Lemma-Anweisung zu ändern. Ich realisiere, dass prefer und defer in Anwenden-Stil Beweise verwendet werden können, aber ich möchte eine Methode, die in der proof (...) Teil verwendet werden kann.

Edit:

Als Andreas Lochbihler sagt rule iffI[rotated] Arbeiten im obigen Beispiel zu schreiben. Ist es jedoch möglich, die Zielreihenfolge in der folgenden Situation zu tauschen, ohne die Aussage des Lemmas zu ändern?

lemma "P==>Q" "Q==>P" 
    proof ((*here I would like to swap goal order*), rule ccontr) 
oops 

Dieses Beispiel scheint gekünstelt, aber ich fühle, dass es Situationen geben kann, wo es unbequem ist, die Aussage des Lemmas zu ändern, oder ist es notwendig, das Tor, um zu tauschen, wenn es keine vorherige Anwendung einer Regel ist wie iffI.

Answer 1

Die Reihenfolge der Teilziele richtet sich nach der Reihenfolge der Annahmen der von Ihnen angewendeten Regel. So genügt es, die Annahmen der iffI Regel zu tauschen, zum Beispiel das Attribut [rotated] wie in

proof(rule iffI[rotated], rule ccontr) 

Im Allgemeinen gibt es keinen Beweis Verfahren die Reihenfolge der Ziele zu ändern. Und wenn Sie darüber nachdenken, dies mit einer ausgefeilteren Proofautomatisierung wie zu verwenden, rate ich Ihnen dringend davon ab, solche Dinge zu tun. Proof-Skripte mit einer hohen Automatisierung sollten unabhängig von der Reihenfolge der Ziele funktionieren. Andernfalls werden Ihre Proofs leicht beschädigt, wenn sich etwas im Proofautomatisierungs-Setup ändert.

Einige Low-Level-Proof-Taktiken erlauben jedoch die explizite Zieladressierung (meist diejenigen, die auf _tac enden). Zum Beispiel gilt

proof(rule iffI, rule_tac [2] ccontr) 

die ccontr Regel auf das zweite Teilziel anstelle der ersten.