我已经与Isabelle/HOL合作了几个月，但我一直无法弄清楚使用_tac的确切意图。
具体来说，我说的是case_tac和induct与intut_tac(尽管知道tac的一般含义会很好，因为我也在使用其他方法，如cut_tac(。
我注意到我不能使用带有⋀绑定变量的apply来使用case或induct，但如果它是结构化证明，我可以。为什么？
例如：
lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
apply (rule ccontr)
apply (erule notE)
apply (rule allI)
apply (case_tac "P x")
apply (erule notE)
apply (erule exI)
apply assumption
done
另一方面，我注意到induct和intuct_tac之间的另一个区别是，我可以对后者使用双感应，但不能对前者使用双感应。再说一遍，我不知道为什么。
提前谢谢。
*_tac是apply脚本中使用的内置策略。特别是，在Isabelle/Isar中，case_tac和induct_tac基本上已经被cases和induction的证明方法所取代。正如您提到的，case_tac和induct_tac可以处理绑定变量。然而，这是非常脆弱的，因为它们的名称通常是自动生成的，并且当Isabelle更改时可能会更改(当然，您可以使用rename_tac来选择固定名称(。这就是为什么现在结构化的证明方法比非结构化的战术脚本更受欢迎的原因之一。现在，回到您的示例：为了能够使用cases，您可以引入如下结构化块：
lemma "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
apply (rule ccontr)
apply (erule notE)
proof (intro allI)
fix x
assume "∄x. P x"
then show "¬ P x"
apply (cases "P x")
apply (erule notE)
apply (erule exI)
apply assumption
done
qed
正如您所看到的，结构化证明通常是冗长的，但比线性apply脚本可读性高得多。
如果你仍然对"；双感应"；问题，一个例子将是非常受欢迎的。最后，如果你想了解更多关于使用Isabelle/Isar语言环境的结构化证明的信息，我强烈建议你阅读本教程中的Isabelle/HOL和《Isabelle/伊萨尔参考手册》，了解更多详细信息。