Trouble with Int Theory in Isabelle/HOL

Question

I am working on a proof which I was able to reduce to “of_int i = 0 ==> i = 0”. This seemed like a simple application of the rule “of_int_eq_0_iff” however I was unable to successfully apply this rule. On further probing I found that I was unable to prove the following lemma

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

by any means whatsoever. That is, unless I declare the lemma within the context ring_char_0. Then the lemma can easily be proved as follows:

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

But then I cannot apply this lemma outside of this context, which is what my main theorem requires (it resides within a different context).

Any help would be greatly appreciated.

Manuel Eberl Manuel Eberl · Accepted Answer · 2014-10-31T22:08:37

The fact that you can only prove your lemma inside ring_char_0 should make you suspicious. The reason for this is that the lemma of_int_eq_0_iff is defined in the context of ring_char_0 itself. You can see this by typing e.g.

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

The reason for this is that in a ring with a characteristic k ≠ 0, this does not hold. In such a ring, of_int n will be zero for all multiples n of k, despite n not being 0.

If your original goal reduces to of_int i = 0 ==> i = 0 then maybe your original goal only holds for rings of characteristic 0, or you need a different proof, one that does not require of_int i = 0 ==> i = 0.

Trouble with Int Theory in Isabelle/HOL

1 Answers