isabelle - 根据伊莎贝尔，1/0 = 0 吗？

Question

以下引理:

lemma "(1::real) / 0 = 0" by simp

因为定理 division_ring_divide_zero 而通过

我发现这非常令人不安，因为如果我想证明某个分数不为零，我必须证明分子不为零且分母不为零，这可能有道理但会混淆两个不同的问题一个。

有没有办法将分数的良定义与其非零值分开？

Answer 1

Isabelle/HOL 是总函数的​​逻辑，因此没有内置的分数概念或任何其他未定义的函数应用程序。也就是说，a/b 是为所有 a 和 b 定义的，它返回它们的商，除非 b为零。但它仍然具有值(value)。

在库中，决定以 x/0 = 0 的方式完成功能。这个决定简​​化了许多证明，因为你必须处理更少的附加条件。不幸的是，它有时也会让那些期待其他东西的人感到困惑。