Isabelle/HOL中的Int理论问题

Question

我正在研究一个我能够减少到“of_int i = 0 ==> i = 0”的证明。这似乎是“of_int_eq_0_iff”规则的一个简单应用，但我无法成功应用此规则。 关于进一步探索，我发现我无法通过任何方式来证明下面的引理

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

。也就是说，除非我在上下文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的环中，这不成立。在这样的环中，of_int n对于k的所有倍数将为零，尽管n不是0.

如果您的原始目标减少到of_int i = 0 ==> i = 0那么也许您的原始目标仅适用于特性为0的环，或者您需要不同的证明，不需要of_int i = 0 ==> i = 0。