我拿着Isabelle/HOL教程中的一个例子来更好地理解Isar和Tactices证明之间的对应关系。
这是一个有效的版本：
lemma rtrancl_converseD: "(x,y) ∈ (r ^-1 )^* ⟹ (y,x) ∈ r^* "
proof (induct y rule: rtrancl_induct)
case base
then show ?case ..
next case (step y z)
then have "(z, y) ∈ r" using rtrancl_converseD by simp
with `(y,x)∈ r^*` show "(z,x) ∈ r^*" using [[unify_trace_failure]]
apply (subgoal_tac "1=(1::nat)")
apply (rule converse_rtrancl_into_rtrancl)
apply simp_all
done
qed
我想实例化证明(?a, ?b) ∈ ?r ⟹ (?b, ?c) ∈ ?r^* ⟹ (?a, ?c) ∈ ?r^*的converse_rtrancl_into_rtrancl
但如果没有看似荒谬的apply (subgoal_tac "1=(1::nat)")行，就会出现此错误
Clash: r =/= Transitive_Closure.rtrancl
Failed to apply proof method⌂:
using this:
(y, x) ∈ r^*
(z, y) ∈ r
goal (1 subgoal):
1. (z, x) ∈ r^*
如果我完全实例化规则apply (rule converse_rtrancl_into_rtrancl[of z y r x])，则它变为Clash: z__ =/= ya__。
这给我留下了三个问题：为什么这个特定的案例会破裂？我该怎么修？我怎么才能弄清楚这些情况下出了什么问题，因为我真的不明白unify_trace_failure消息想告诉我什么。
rule-策略通常对前提的顺序很敏感。前提在converse_rtrancl_into_rtrancl中的顺序和在你的证明状态中的顺序不匹配。使用rotate_tac在证明状态下切换前提的顺序将使它们匹配规则，这样您就可以像这样直接应用fact：
... show "(z,x) ∈ r^*"
apply (rotate_tac)
apply (fact converse_rtrancl_into_rtrancl)
done
或者，如果你想包含某种rule策略，这看起来像这样：
apply (rotate_tac)
apply (erule converse_rtrancl_into_rtrancl)
apply (assumption)
(我个人在日常工作中从来没有使用过应用程序脚本。所以应用程序风格的大师可能知道处理这种情况的更优雅的方法。(
关于您的1=(1::nat)/simp_all修复：
整个目标可以通过simp_all直接解决。因此，尝试添加像1=1这样的东西可能并没有真正告诉你其他方法对解决证明有多大贡献。
然而，额外的假设似乎实际上帮助Isabelle正确匹配converse_rtrancl_into_rtrancl。(别问我为什么！(所以，人们确实可以通过添加这个虚假的假设来规避这个问题，然后用refl再次消除它，比如：
apply (subgoal_tac "1=(1::nat)")
apply (erule converse_rtrancl_into_rtrancl)
apply (assumption)
apply (rule refl)
当然，这看起来并不是特别优雅。
[[unify_trace_failure]]可能只有在熟悉Nipkow的高阶统一算法的内部工作方式的情况下才真正有帮助。(我不是。(我认为这里对未来的暗示实际上是，人们必须密切关注一些策略的前提顺序(而不是统一的调试输出(。
我在Isar参考文件6.4.3中找到了解释。
with b1..bn命令等效于from b1..bn and this，即它进入证明链接模式，将它们作为(结构化(假设添加到证明方法中。
基本的证明方法(如规则(期望给出多个事实按照它们的正确顺序，对应于所涉及的规则。请注意，使用例如，类似于from，a和b。这涉及到平凡规则PROPψ=⇒PROPψ，在Isabelle/Pure中被束缚为"_"(下划线(。
自动化方法(如simp或auto(只插入任何给定的事实在正常操作之前。取决于程序的类型涉及到这一点，事实的顺序在这里就不那么重要了。
给定有关"with"翻译的信息，并且该规则要求按顺序链接事实，我们可以尝试翻转链接事实。这确实有效：
from this and `(y,x)∈ r^*` show "(z,x) ∈ r^*"
by (rule converse_rtrancl_into_rtrancl)
我认为"6.4.3基本方法和属性"；也是相关的，因为它描述了基本方法如何与传入事实交互。值得注意的是，"-"noop有时在开始证明时使用，它将正向链接转化为对目标的假设。
with `(y,x)∈ r^*` show "(z,x) ∈ r^*"
apply -
apply (rule converse_rtrancl_into_rtrancl; assumption)
done
这是因为第一个apply消耗了所有链接的事实，所以第二个应用是纯反向链接。这也是subgoal_tac或rotate_tac工作的原因，但前提是它们位于单独的应用命令中。