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。