objectifs Réorganiser (Isabelle)

Question

Je voudrais savoir comment réorganiser les objectifs dans la situation suivante:

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

Je voudrais une solution qui n'implique pas changer la déclaration lemme. Je me rends compte que prefer et defer peuvent être utilisés dans les épreuves de style, mais j'aimerais avoir une méthode qui peut être utilisée dans la partie proof (...).

Edit:

Comme dit Andreas Lochbihler, écrit rule iffI[rotated] œuvres dans l'exemple ci-dessus. Cependant, est-il possible d'échanger l'ordre des buts dans la situation suivante sans changer l'énoncé du lemme?

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

Cet exemple peut sembler artificiel, mais je pense qu'il peut y avoir des situations où il est pratique de changer l'énoncé du lemme, ou il est nécessaire d'échanger l'ordre de but quand il n'y a pas d'application précédente d'une règle tel que iffI.

Answer 1

L'ordre des sous-objectifs est déterminé par l'ordre des hypothèses de la règle que vous appliquez. Donc, il suffit d'échanger les hypothèses de la règle iffI, par exemple, en utilisant l'attribut [rotated] comme dans

proof(rule iffI[rotated], rule ccontr) 

En général, il n'y a pas de méthode de preuve pour changer l'ordre des objectifs. Et si vous songez à l'utiliser avec une automatisation de preuve plus sophistiquée comme auto, je vous déconseille vivement de faire ce genre de choses. Les scripts de preuve avec beaucoup d'automatisation devraient fonctionner indépendamment de l'ordre des objectifs. Dans le cas contraire, vos épreuves se casseront facilement si quelque chose change dans la configuration de l'automatisation de la preuve.

Cependant, quelques tactiques de preuve de bas niveau permettent d'utiliser l'adressage explicite des objectifs (principalement ceux qui se terminent par _tac). Par exemple,

proof(rule iffI, rule_tac [2] ccontr) 

applique la règle ccontr au second sous-but au lieu de la première.