[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.