# [isabelle] Trouble with the Int Theory

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.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*