Isabelle/HOL中Int理论的麻烦

Question

我正在做一个证明，我能够将它简化为“of_int i=0 ==> i=0”。这看起来像是规则“of_int_eq__iff”的一个简单应用，但是我无法成功地应用这个规则。在进一步的研究中，我发现我无法证明下面的引理

lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”

不管用什么方式。也就是说，除非我在context ring_char_0中声明了引理。然后，引理可以很容易地证明如下：

context ring_char_0 begin
lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
  using of_int_eq_iff [of i 0] by simp
end

但是我不能在这个上下文之外应用这个引理，这是我的主要定理所要求的(它驻留在不同的上下文中)。

任何帮助都将不胜感激。

Answer 1

您只能在ring_char_0中证明您的引理，这一事实应该会让您产生怀疑。这是因为引理of_int_eq_0_iff是在ring_char_0本身的上下文中定义的。你可以通过输入下面的命令来查看。

declare [[show_sorts]]
thm of_int_eq_0_iff
> (of_int (?z∷int) = (0∷?'a∷ring_char_0)) = (?z = (0∷int))

这样做的原因是，在具有特征k≠0的环中，这不成立。在这样的环中，对于k的所有倍数n，of_int n将为零，尽管n不为0。

如果您的原始目标简化为of_int i = 0 ==> i = 0，则可能您的原始目标仅适用于特征为0的环，或者您需要一个不需要of_int i = 0 ==> i = 0的不同证明。