# Re: [isabelle] Trouble with the Int Theory

Hi,
try
note [[ show_sorts]]
thm of_int_eq_0_iff
here, you will see that the of_int_eq_0_iff lemma only works
if the right hand side is in the ring_char_0 typeclass.
So make sure that your 0 on the RHS also is in this typeclass.
--
Peter
On Fr, 2014-10-31 at 17:38 -0400, Scott Constable wrote:
> 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.*