重新排序目标（伊莎贝尔）
Reordering goals (Isabelle)
我想知道在以下情况下如何重新排序目标：
lemma "P=Q"
proof (rule iffI, (*here I would like to swap goal order*), rule ccontr)
oops
我想要一个不涉及更改引理语句的解决方案。我意识到 prefer 和 defer 可以用在 apply-style 证明中，但我想有一个方法可以用在 proof (...) 部分。
编辑：
正如 Andreas Lochbihler 所说，写 rule iffI[rotated] 在上面的例子中有效。但是，在不改变引理的陈述的情况下，是否可以在以下情况下交换目标顺序？
lemma "P==>Q" "Q==>P"
proof ((*here I would like to swap goal order*), rule ccontr)
oops
这个例子可能看起来做作，但我觉得可能会有一些情况不方便更改引理的陈述，或者在没有先前应用规则的情况下需要交换目标顺序，例如iffI.
子目标的顺序由您应用的规则的假设顺序决定。所以交换 iffI 规则的假设就足够了，例如，使用 [rotated] 中的属性
proof(rule iffI[rotated], rule ccontr)
一般来说，没有改变目标顺序的证明方法。如果你正在考虑将它与更复杂的证明自动化一起使用，比如 auto，我强烈建议你不要做这些事情。具有大量自动化功能的证明脚本应该独立于目标的顺序工作。否则，当证明自动化设置中的某些内容发生变化时，您的证明很容易被破坏。
然而，一些低级证明策略允许使用显式目标寻址（主要是那些以 _tac 结尾的）。例如，
proof(rule iffI, rule_tac [2] ccontr)
将 ccontr 规则应用到第二个子目标而不是第一个。
我想知道在以下情况下如何重新排序目标：
lemma "P=Q"
proof (rule iffI, (*here I would like to swap goal order*), rule ccontr)
oops
我想要一个不涉及更改引理语句的解决方案。我意识到 prefer 和 defer 可以用在 apply-style 证明中，但我想有一个方法可以用在 proof (...) 部分。
编辑：
正如 Andreas Lochbihler 所说，写 rule iffI[rotated] 在上面的例子中有效。但是，在不改变引理的陈述的情况下，是否可以在以下情况下交换目标顺序？
lemma "P==>Q" "Q==>P"
proof ((*here I would like to swap goal order*), rule ccontr)
oops
这个例子可能看起来做作，但我觉得可能会有一些情况不方便更改引理的陈述，或者在没有先前应用规则的情况下需要交换目标顺序，例如iffI.
子目标的顺序由您应用的规则的假设顺序决定。所以交换 iffI 规则的假设就足够了，例如，使用 [rotated] 中的属性
proof(rule iffI[rotated], rule ccontr)
一般来说，没有改变目标顺序的证明方法。如果你正在考虑将它与更复杂的证明自动化一起使用，比如 auto，我强烈建议你不要做这些事情。具有大量自动化功能的证明脚本应该独立于目标的顺序工作。否则，当证明自动化设置中的某些内容发生变化时，您的证明很容易被破坏。
然而，一些低级证明策略允许使用显式目标寻址（主要是那些以 _tac 结尾的）。例如，
proof(rule iffI, rule_tac [2] ccontr)
将 ccontr 规则应用到第二个子目标而不是第一个。