Проблема с интегральной теорией в Isabelle/HOL

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 будет равным нулю для всех кратных n из k, несмотря на то, что n не равно 0.

Если ваша первоначальная цель сводится к of_int i = 0 ==> i = 0, тогда, возможно, ваша первоначальная цель сохраняется только для колец с характеристикой 0, или вам нужно другое доказательство, которое не требует of_int i = 0 ==> i = 0.