要求澄清伊莎贝尔理论中涉及自然数的理论中明显实数强制的出现

如何解决要求澄清伊莎贝尔理论中涉及自然数的理论中明显实数强制的出现

我正在 Isabelle2020 /jEdit 中检查以下理论：

theory Sqrt
imports Complex_Main "HOL-computational_Algebra.Primes"
begin

theorem
  assumes "prime (p::nat)"
  shows "sqrt p ∉ ℚ"
proof
  from ‹prime p› have p: "1 < p" by (simp add: prime_nat_iff)
  assume "sqrt p ∈ ℚ"
  then obtain m n :: nat where
      n: "n ≠ 0" and sqrt_rat: "¦sqrt p¦ = m / n"
    and "coprime m n" by (rule Rats_abs_nat_div_natE)

[we omit the remainder of the proof]

输出窗格显示证明状态：

have (⋀m n. n ≠ 0 ⟹ ¦sqrt (real p)¦ = real m / real n ⟹ coprime m n ⟹ ?thesis) ⟹ ?thesis 
proof (state)
this:
    n ≠ 0
    ¦sqrt (real p)¦ = real m / real n
    coprime m n

goal (1 subgoal):
 1. sqrt (real p) ∈ ℚ ⟹ False

我的问题是：这些“真实”的外表是一种类型的强制吗？我已经阅读了 Isabelle 发行版附带的所谓教程中讨论类型的第 8 章（标题为高阶逻辑证明助手）。我阅读了 Florian Haftman 的文档标题 Isabelle/HOL 类型类层次结构（也是 Isabelle 发行版的一部分）。上述理论陈述中使用的规则 Rats_abs_nat_div_natE 是 Real.thy 理论中的一个引理。

我在该理论文件中查找参考文献，并查看了证明中的第 8.4.5 节高阶逻辑助理在那里我发现了数字类型 nat 是线性有序半环，类型 int 是有序环，并且类型 real 是一个有序字段。属性可能不适用于特定的类，例如，类型 nat 没有涉及减法的抽象属性（因为，当然，一个可能以负数结束，这不是自然数）。相反，提供了特定的定理来解决 nat 类型的减法。更重要的是，“所有涉及除法的抽象属性都需要一个域。”（高阶逻辑证明助手。）

那么，我们是否在这里看到商类型被用来将自然或整数类型的除法提升为抽象实数类型以满足领域要求（参见 §11.9 Isabelle/Isar 参考手册）？商类型实数是根据 realrel 文件中的等价关系定义 Real.thy 创建的。

我惊讶地看到证明中的实项取决于素数、正整数和有理数，并想确保我至少已经接近解释为什么会在 Isabelle 证明中出现这种情况。

解决方法

函数 sqrt 仅在实数上定义。因此，您需要将其参数 p 从 nat 转换为 real。有一种强制会自动为您执行此操作；因此，您可以使用 real 函数。

之后，输入 m/n 的唯一方法是 real m / real n。

通常，重载语法对于证明助手来说是一个问题。例如，纸上的2/3可以是Isabelle中的有理数Fract 2 3，实数2/3，或者F_5中的3的倒数乘以2，或者什么否则。

在 Isabelle 中，这是通过（在一定程度上）避免重载和使用不同的符号来解决的。