到目前为止，我在Isabelle 中使用Jeremy Siek 提出的以下方式来写矛盾证明（使用这个模式）： lemma "<expression>" proof - { assume "¬ <expression>" then have Fals...

我有一个以以下方式结构化的Isabelle证明:proof (cases "n = 0") case True (* lots of stuff here *) show ?thesis sorry next case False (* lots of stuff here...

在Isar-style的Isabelle证明中，这个很好用： from `a ∨ b` have foo proof assume a show foo sorry next assume b show foo sorry qed proof 中调用的隐式规则是 rule...

我想了解Isabelle/HOL的子类型。我在上一个SO问题的部分答案中解释了为什么这对我很重要：尝试将类型类和子类型视为集合和子集基本上，我只有一个类型，所以如果我可以通过子类型利用HOL类型的功能，那对我可能会很有用。我已经在Isabelle文档、Web和Isabelle邮件列表中进行了搜...

大多数证明助手都是具有依赖类型的函数式编程语言。它们可以用于证明程序/算法。我对适用于数学且仅限于微积分等领域的证明助手感兴趣。你能推荐一个吗？我听说过Mizar，但我不喜欢源代码是闭源的。如果它确实是最适合数学的，我会使用它。新语言Agda和Idris是否适用于数学证明？

除了 assume，在Isar证明块中还有一个命令叫做presume，用于引入事实。从文档中可以看到，它不需要假设（推测？）在目标中明确列出，并且似乎会添加一个条件，以显示假定语句是从其他目标中推导得出的。 那么问题来了：什么时候应该使用presume而不是assume，并且我能用presu...