Die Reihenfolge der Geschäftsräume

Question

Wie ändert man die Reihenfolge der Geschäftsräume in einer Regel? Zum Beispiel in Isabelles natürlichen Abtragungsregel:

mp: ?P ⟶ ?Q ⟹ ?P ⟹ ?Q 

Können wir die Reihenfolge zu ändern:

?P ⟹ ?P ⟶ ?Q ⟹ ?Q 

kann ich rev_mp verwenden oder ein neues Lemma definieren, aber was ich suche ist, ob es ist ein Theoremmodifikator, der die Reihenfolge der Prämissen ändert.

Answer 1

Die Prämissen eines Satzes können mit dem Attribut rotated rotiert werden. Sie können auch die Anzahl der zu drehenden Räume angeben, z. B. mp[rotated 1]. AFAIK gibt es kein Attribut für willkürliche Permutierung der Räumlichkeiten.